theory AC_Rewriting_Impl
imports
"Check-NT.AC_Rewriting"
QTRS.Trs_Impl
"Transitive-Closure-II.RTrancl"
AC_Equivalence
begin
definition check_AC_rule :: "('f,'v)rule ⇒ bool" where
"check_AC_rule lr ≡ case lr of (l,r) ⇒ if is_Var l then False
else let f = fst (the (root l)) in
funas_term l = {(f,2)}
∧ funas_term r = {(f,2)}
∧ vars_term_ms l = vars_term_ms r
∧ funs_term_ms l = funs_term_ms r"
lemma check_AC_rule: "check_AC_rule (l,r) ⟷
funs_term_ms l = funs_term_ms r ∧ vars_term_ms l = vars_term_ms r ∧ (∃ f. funas_term l = {(f,2)} ∧ funas_term r = {(f,2)})"
unfolding check_AC_rule_def split Let_def
by (cases l, auto)
definition check_AC_theory :: "('f :: show, 'v :: show)rules ⇒ shows check" where
"check_AC_theory E ≡ check_allm (λ lr. check (check_AC_rule lr)
(shows ''rule '' o shows_rule lr o shows '' violates AC-property'')) E"
lemma check_AC_theory[simp]: "isOK(check_AC_theory E) = AC_theory (set E)"
unfolding check_AC_theory_def AC_theory_def
by (auto simp: check_AC_rule)
definition check_E_reachable :: "('f,'v)rules ⇒ ('f,'v)term ⇒ ('f,'v)term ⇒ bool" where
"check_E_reachable E s t ≡ t ∈ set (mk_rtrancl_list (op =) (rewrite E) [s])"
lemma check_E_reachable[simp]: assumes "AC_theory (set E)"
shows "check_E_reachable E s t = ((s,t) ∈ (rstep (set E))^*)"
proof -
interpret AC_theory "set E" by fact
let ?rewr = "{(a, b). b ∈ set (rewrite E a)}"
have rewr: "?rewr = rstep (set E)"
proof (subst rewrite_iff_rstep)
fix l r
assume "(l,r) ∈ set E"
from ac_ruleD(2)[OF this] show "vars_term r ⊆ vars_term l"
unfolding set_mset_vars_term_ms[symmetric] by auto
qed auto
interpret relation_subsumption_list "rewrite E" "op ="
proof
fix a
show "finite {b. (a, b) ∈ {(a, b). b ∈ set (rewrite E a)}⇧*}" unfolding rewr
by (rule finite_reachable)
qed auto
show ?thesis unfolding check_E_reachable_def mk_rtrancl_list
mk_rtrancl_no_subsumption[OF refl] symmetric_trs_def rewr by auto
qed
definition check_symmetric_AC_theory :: "('f :: show, 'v :: show)rules ⇒ shows check" where
"check_symmetric_AC_theory E ≡ do {
check_AC_theory E;
check_allm (λ (l,r). check (check_E_reachable E r l)
(shows ''rhs '' o shows r o shows '' does not rewrite to lhs '' o shows l)) E
<+? (λ s. shows ''theory is not symmetric⏎'' o s)
}"
lemma check_symmetric_AC_theory[simp]: "isOK(check_symmetric_AC_theory E) ⟷
AC_theory (set E) ∧ symmetric_trs (set E)"
by (auto simp: check_symmetric_AC_theory_def symmetric_trs_def)
definition check_size_preserving_trs :: "('f :: show, 'v :: show)rules ⇒ shows check" where
"check_size_preserving_trs E ≡ do {
check_allm (λ (l,r). check (num_symbs l = num_symbs r ∧ vars_term_ms l = vars_term_ms r)
(shows ''rule '' o shows_rule (l,r) o shows '' is not size preserving'')) E
<+? (λ s. shows ''TRS is not size-preserving⏎'' o s)
}"
lemma check_size_preserving_trs[simp]: "isOK(check_size_preserving_trs E) ⟷
size_preserving_trs (set E)"
by (auto simp: check_size_preserving_trs_def size_preserving_trs_def)
definition check_only_C_rule :: "'f set ⇒ ('f,'v)rule ⇒ bool" where
"check_only_C_rule OC lr ≡ case lr of (Fun f [s,t], r) ⇒ f ∈ OC ⟶ r = Fun f [t,s]
| _ ⇒ True"
lemma check_only_C_rule[simp]: "check_only_C_rule OC (l,r) = (∀ f. root l = Some (f,2) ⟶ f ∈ OC ⟶
(∃ s t. (l,r) = (Fun f [s,t], Fun f [t,s])))"
proof (cases "is_Fun l ∧ num_args l = 2")
case False
thus ?thesis unfolding check_only_C_rule_def
by (cases l, force, cases "args l"; cases "tl (args l)"; cases "tl (tl (args l))"; auto)
next
case True
from True obtain f s t where l: "l = Fun f [s,t]"
by (cases l, force, cases "args l"; cases "tl (args l)"; cases "tl (tl (args l))"; auto)
show ?thesis unfolding l check_only_C_rule_def by simp
qed
definition check_only_C_theory :: "'f set ⇒ ('f :: show,'v :: show)rules ⇒ shows check" where
"check_only_C_theory OC E ≡ check_allm (λ lr. check (check_only_C_rule OC lr)
(shows ''rule '' o shows_rule lr o shows '' violates only-C-property'')) E"
lemma check_only_C_theory[simp]: "AC_theory (set E) ⟹
isOK(check_only_C_theory OC E) = AC_C_theory (set E) OC"
unfolding AC_C_theory_def AC_C_theory_axioms_def check_only_C_theory_def by auto
fun check_ext_rule1 :: "('f,'v)rule ⇒ 'f ⇒ 'v set ⇒ ('f,'v)rule ⇒ bool" where
"check_ext_rule1 (l,r) f X (Fun g [l', Var x], Fun g' [r', Var x']) = (((l,r,f,f,x) = (l',r',g,g',x')) ∧ x ∉ X)"
| "check_ext_rule1 _ _ _ _ = False"
fun check_ext_rule2 :: "('f,'v)rule ⇒ 'f ⇒ 'v set ⇒ ('f,'v)rule ⇒ bool" where
"check_ext_rule2 (l,r) f X (Fun g [Var x,l'], Fun g' [Var x',r']) = (((l,r,f,f,x) = (l',r',g,g',x')) ∧ x ∉ X)"
| "check_ext_rule2 _ _ _ _ = False"
fun check_ext_rule3 :: "('f,'v)rule ⇒ 'f ⇒ 'v set ⇒ ('f,'v)rule ⇒ bool" where
"check_ext_rule3 (l,r) f X (Fun g [Fun h [Var x,l'], Var y], Fun g' [Fun h' [Var x',r'], Var y'])
= ((l,r,f,f,f,f,x,y) = (l',r',g,g',h,h',x',y') ∧ x' ≠ y' ∧ x' ∉ X ∧ y' ∉ X)"
| "check_ext_rule3 _ _ _ _ = False"
definition check_ext_rule :: "('f,'v)rules ⇒ 'f set ⇒ 'f set ⇒ ('f,'v)rule ⇒ bool" where
"check_ext_rule Rext A C lr ≡ case lr of (l,r) ⇒
if is_Var l ∨ num_args l ≠ 2 ∨ fst (the (root l)) ∉ A then True else
let f = fst (the (root l));
X = vars_rule lr
in (∃ lr' ∈ set Rext. check_ext_rule1 lr f X lr') ∧
(f ∉ C ⟶ (∃ lr' ∈ set Rext. check_ext_rule2 lr f X lr') ∧ (∃ lr' ∈ set Rext. check_ext_rule3 lr f X lr'))"
definition check_ext_trs :: "('f :: show,'v :: show)rules ⇒ 'f list ⇒ 'f list ⇒ ('f,'v)rules ⇒ shows check" where
"check_ext_trs R A C Rext ≡ let A' = set A; C' = set C in
check_allm (λ lr. check (check_ext_rule Rext A' C' lr)
(shows ''could not find extended rules for rule l -> r:⏎ '' o shows_rule lr o
shows ''⏎ expecting rule f(l,x) -> f(r,x) for all A and AC symbols,⏎'' o
shows ''and rules f(x,l) -> f(x,r) and f(f(x,l),y) -> f(f(x,r),y) for all A symbols'')) R
<+? (λ s. shows ''could not ensure validity of AC-extended system⏎'' o s)"
lemma check_ext_trs[simp]: assumes ok: "isOK(check_ext_trs R A C Rext)"
shows "is_ext_trs (set R) (set A) (set C) (set Rext)"
unfolding is_ext_trs_def
proof (intro allI impI conjI)
fix l r f
assume lr: "(l,r) ∈ set R" and f: "f ∈ set A" and l: "root l = Some (f,2)"
note ok = ok[unfolded check_ext_trs_def Let_def]
from ok lr have check: "check_ext_rule Rext (set A) (set C) (l,r)" by auto
let ?X = "vars_rule (l,r)"
from l f have "(is_Var l ∨ num_args l ≠ 2 ∨ fst (the (root l)) ∉ set A) = False"
by (cases l, auto)
note check = check[unfolded check_ext_rule_def split Let_def this if_False, unfolded l]
from check obtain l' r' where lr': "(l',r') ∈ set Rext" and "check_ext_rule1 (l,r) f ?X (l',r')" by force
then obtain x where id: "l' = Bin f l (Var x)" "r' = Bin f r (Var x)" and x: "x ∉ ?X"
by (cases rule: check_ext_rule1.cases[of "((l,r),f,?X,(l',r'))"], auto)
show "∃x. x ∉ ?X ∧ ext_AC_rule f (l, r) (Var x) ∈ set Rext"
by (intro exI conjI, rule x, insert lr'[unfolded id], auto simp: ext_AC_rule_def)
assume C: "f ∉ set C"
with check obtain l' r' where lr': "(l',r') ∈ set Rext" and "check_ext_rule2 (l,r) f ?X (l',r')" by force
then obtain x where id: "l' = Bin f (Var x) l" "r' = Bin f (Var x) r" and x: "x ∉ ?X"
by (cases rule: check_ext_rule2.cases[of "((l,r),f,?X,(l',r'))"], auto)
note 2 = lr'[unfolded id]
from C check obtain l' r' where lr': "(l',r') ∈ set Rext" and check: "check_ext_rule3 (l,r) f ?X (l',r')" by force
let ?l = "args l' ! 0" let ?r = "args r' ! 0"
from check obtain y z where id: "l' = Bin f (Bin f (Var y) l) (Var z)" "r' = Bin f (Bin f (Var y) r) (Var z)"
and yz: "y ∉ ?X" "z ∉ ?X" "y ≠ z"
by (cases rule: check_ext_rule3.cases[of "((l,r),f,?X,(l',r'))"], auto)
note 3 = lr'[unfolded id]
show "∃x y z. x ∉ ?X ∧ y ∉ ?X ∧ z ∉ ?X ∧ x ≠ y ∧
(Fun f [Var z, l], Fun f [Var z, r]) ∈ set Rext ∧
(Fun f [Fun f [Var x, l], Var y], Fun f [Fun f [Var x, r], Var y]) ∈ set Rext"
using 2 3 x yz by blast
qed
definition check_AC_same_as_E :: "'v ⇒ 'v ⇒ 'v :: show ⇒ ('f :: show) list ⇒ 'f list ⇒ ('f,'v)rules ⇒ shows check" where
"check_AC_same_as_E x y z A C E ≡ do {
let X = Var x;
let Y = Var y;
let Z = Var z;
check_allm (λ f. check (check_E_reachable E (Bin f X Y) (Bin f Y X)) f) C
<+? (λ f. shows ''could not simulate C-rules for '' o shows f o shows '' by E'');
check_allm (λ f. check (check_E_reachable E (Bin f X (Bin f Y Z)) (Bin f (Bin f X Y) Z)) f) A
<+? (λ f. shows ''could not simulate A-rules for '' o shows f o shows '' by E'');
check_allm (λ f. check (check_E_reachable E (Bin f (Bin f X Y) Z) (Bin f X (Bin f Y Z))) f) A
<+? (λ f. shows ''could not simulate A-rules for '' o shows f o shows '' by E'');
check_allm (λ (l,r). check ((l,r) ∈ aoc_rewriting.AOCEQ (set A) (set C)) (l,r)) E
<+? (λ lr. shows ''equation '' o shows_rule lr o shows '' is not AC-equivalent'')
} <+? (λ s. shows ''could not ensure that equations simulate AC-equivalence⏎'' o s)"
lemma check_AC_same_as_E[simp]: assumes xyz: "x ≠ y" "x ≠ z" "y ≠ z"
and AC: "AC_theory (set E :: ('f :: show,'v :: show)trs)"
and ok: "isOK(check_AC_same_as_E x y z A C E)"
shows "aoc_rewriting.AOCEQ (set A) (set C) = (rstep (set E))^*" (is "?l = ?r^*")
proof -
let ?A = "set A" let ?C = "set C"
let ?X = "Var x" let ?Y = "Var y" let ?Z = "Var z"
let ?AC = "AC_rules ?A ?C"
interpret aoc_rewriting ?A ?C .
def δ ≡ "λ (a :: ('f,'v)term) b c u. if u = x then a else if u = y then b else c"
have [simp]:
"⋀ a b c. δ a b c x = a"
"⋀ a b c. δ a b c y = b"
"⋀ a b c. δ a b c z = c"
unfolding δ_def using xyz by auto
have l_rstep: "AOCEQ = (rstep (?AC⇧↔))^*" unfolding conversion_def rstep_simps(5) ..
have ctxt: "ctxt.closed AOCEQ" unfolding l_rstep by auto
have subst: "subst.closed AOCEQ" unfolding l_rstep
by (rule subst.closed_rtrancl, auto)
have subst': "subst.closed (?r^*)"
by (rule subst.closed_rtrancl, auto)
note subst2 = subst.closedD[OF this]
note ok = ok[unfolded check_AC_same_as_E_def Let_def check_E_reachable[OF AC], simplified]
have "?r ⊆ ?l"
by (rule rstep_subset[OF ctxt subst], insert ok, auto)
from rtrancl_mono[OF this]
have "?r^* ⊆ ?l" by auto
moreover
{
fix l r :: "('f,'v)term"
assume "(l,r) ∈ ?AC⇧↔"
then consider (A) "(l,r) ∈ (A_rules ?A)⇧↔" | (C) "(l,r) ∈ (C_rules ?C)⇧↔" unfolding AC_rules_def by blast
hence "(l,r) ∈ ?r^*"
proof (cases)
case C
from this[unfolded C_rules_def] obtain s t f where
l: "l = Bin f s t" and r: "r = Bin f t s" and f: "f ∈ ?C" by auto
from ok f have "(Bin f ?X ?Y, Bin f ?Y ?X) ∈ ?r^*" by auto
from subst2[OF this, of "δ s t t"] show ?thesis unfolding l r by auto
next
case A
from this[unfolded A_rules_def] consider
(1) s t u f where "l = Bin f s (Bin f t u)" "r = Bin f (Bin f s t) u" "f ∈ ?A"
| (2) s t u f where "l = Bin f (Bin f s t) u" "r = Bin f s (Bin f t u)" "f ∈ ?A" by auto
thus ?thesis
proof (cases)
case 1
from 1(3) ok have "(Bin f ?X (Bin f ?Y ?Z), Bin f (Bin f ?X ?Y) ?Z) ∈ ?r^*" by auto
from subst2[OF this, of "δ s t u"] show ?thesis unfolding 1(1-2) by auto
next
case 2
from 2(3) ok have "(Bin f (Bin f ?X ?Y) ?Z, Bin f ?X (Bin f ?Y ?Z)) ∈ ?r^*" by auto
from subst2[OF this, of "δ s t u"] show ?thesis unfolding 2(1-2) by auto
qed
qed
} note main = this
have "rstep (?AC⇧↔) ⊆ ?r^*"
by (rule rstep_subset[OF _ subst'], insert main, auto)
from rtrancl_mono[OF this]
have "?l ⊆ ?r^*" unfolding l_rstep by auto
ultimately show ?thesis by auto
qed
end