Theory AC_Termination_Problem_Spec

(*
Author:  René Thiemann <rene.thiemann@uibk.ac.at> (2016)
License: LGPL (see file COPYING.LESSER)
*)

section ‹Operations on AC termination problems (AC-TPs)›

theory AC_Termination_Problem_Spec
imports
  QTRS.Trs_Impl
  "Check-NT.AC_Rewriting"
begin

subsection ‹Record-Based Interface›

type_synonym ('f,'v)ac_tp = "('f,'v)trs × 'f set × 'f set"

fun relation_ac_tp :: "('f,'v) ac_tp ⇒ ('f,'v)trs" where 
  "relation_ac_tp (R,A,C) = aoc_rewriting.relaoc A C R"

record ('p, 'f, 'v) ac_tp_ops =
  ac_tp :: "'p ⇒ ('f,'v)ac_tp"
  R :: "'p ⇒ ('f, 'v) rules"
  A :: "'p ⇒ 'f list"
  C :: "'p ⇒ 'f list"
  mk :: "('f, 'v) rules ⇒ 'f list ⇒ 'f list ⇒ 'p"
  delete_rules :: "'p ⇒ ('f,'v)rules ⇒ 'p"
  E :: "'p ⇒ ('f,'v)rules"


hide_const (open)
  R A C mk ac_tp delete_rules E

locale ac_tp_defs =
  fixes I :: "('p, 'f::show, 'v::show) ac_tp_ops"
begin
  abbreviation R where "R ≡ ac_tp_ops.R I"
  abbreviation A where "A ≡ ac_tp_ops.A I"
  abbreviation C where "C ≡ ac_tp_ops.C I"
  abbreviation E where "E ≡ ac_tp_ops.E I"
  abbreviation ac_tp where "ac_tp ≡ ac_tp_ops.ac_tp I"
  abbreviation mk where "mk ≡ ac_tp_ops.mk I"
  abbreviation delete_rules where "delete_rules ≡ ac_tp_ops.delete_rules I"
end

locale ac_tp_spec = ac_tp_defs I for I +
  assumes ac_tp_sound: "ac_tp tp = (set (R tp), set (A tp), set (C tp))"
    and mk_sound: 
      "set (R (mk r a c)) = (set r)"
      "set (A (mk r a c)) = (set a)"
      "set (C (mk r a c)) = (set c)"
    and delete_rules_sound: "ac_tp (delete_rules tp dr) = 
      (set (R tp) - set dr, set (A tp), set (C tp))"
    and E_sound: "rstep (set (E tp)) = acrstep (set (A tp)) (set (C tp))"
begin

lemmas ac_tp_spec_sound[simp] =
  ac_tp_sound
  mk_sound
  delete_rules_sound
  E_sound

lemma SN_relation_ac_tp: "SN (relation_ac_tp (ac_tp_ops.ac_tp I tp)) = 
  SN_rel (rstep (set (R tp))) (aoc_rewriting.AOCEQ (set (A tp)) (set (C tp)))"
  by (auto simp: aoc_rewriting.relaoc_def SN_rel_defs)

end


end