theory Ordered_Completion_Impl
imports
Ordered_Completion
QTRS.Trs_Impl
"Check-NT.Q_Restricted_Rewriting_Impl"
"../Orderings/KBO_Impl"
"../Orderings/Reduction_Order_Impl"
"../Orderings/RPO"
"Equational_Reasoning"
begin
hide_const (open) Exact_Tree_Automata_Completion.fground
lemma symcl_idemp [simp]: "(r⇧↔)⇧↔ = r⇧↔" by auto
hide_const (open) Ramsey.choice
datatype ('f, 'v) oc_irule =
OC_Deduce "('f, 'v) term" "('f, 'v) term" "('f, 'v) term"
| OC_Orientl "('f, 'v) term" "('f, 'v) term"
| OC_Orientr "('f, 'v) term" "('f, 'v) term"
| OC_Delete "('f, 'v) term"
| OC_Compose "('f, 'v) term" "('f, 'v) term" "('f, 'v) term"
| OC_Simplifyl "('f, 'v) term" "('f, 'v) term" "('f, 'v) term"
| OC_Simplifyr "('f, 'v) term" "('f, 'v) term" "('f, 'v) term"
| OC_Collapse "('f, 'v) term" "('f, 'v) term" "('f, 'v) term"
definition "sym_list xs = List.union xs (map (λ(x, y). (y, x)) xs)"
lemma set_sym_list [simp]: "set (sym_list xs) = (set xs)⇧↔" by (auto simp: sym_list_def)
definition check_rstep_p
where
"check_rstep_p c ρ p s t =
(if p ∉ set (poss_list t) then error (shows ''no step possible at this position'')
else
let (l, r) = ρ in
(case match_list Var [(l, s |_ p), (r, t |_ p)] of
None ⇒ error (shows ''rule does not match'')
| Some σ ⇒
if t = replace_at s p (r ⋅ σ) then c (l ⋅ σ) (r ⋅ σ)
else error (shows ''result does not match'')))"
definition check_step_rule
where
"check_step_rule c ρ s t =
check_exm (λp. check_rstep_p c ρ p s t) (poss_list s) (λ_. shows '' is not a reduct'')"
lemma check_step_rule:
assumes ok: "isOK (check_step_rule chk (l,r) s t)"
shows "∃C σ p. s = C⟨l ⋅ σ⟩ ∧ t = C⟨r ⋅ σ⟩ ∧ isOK (chk (l ⋅ σ) (r ⋅ σ))"
proof -
from ok[unfolded check_step_rule_def case_prod_beta isOK_update_error isOK_existsM]
obtain p where ok_p:"isOK (check_rstep_p chk (l,r) p s t)" "p ∈ poss s" by auto
let ?p = "λ σ.(if t = replace_at s p (r ⋅ σ) then chk (l ⋅ σ) (r ⋅ σ)
else (error (shows ''result does not match'')))"
let ?ml = "match_list Var [(l, s |_ p), (r, t |_ p)]"
from ok_p[unfolded check_rstep_p_def] obtain σ where σ:"?ml = Some σ" "isOK(?p σ)"
by (cases ?ml, auto)
from match_list_sound[OF σ(1)] have at_p:"l ⋅ σ = s |_ p" "r ⋅ σ = t |_ p" by auto
from σ(2) have rlcheck:"isOK(chk (l ⋅ σ) (r ⋅ σ))" and t:"t = (ctxt_of_pos_term p s)⟨r ⋅ σ⟩"
unfolding split by auto
let ?C = "ctxt_of_pos_term p s"
from at_p ctxt_supt_id[OF ok_p(2)] t have s:"s = ?C⟨l ⋅ σ⟩" and t:"t = ?C⟨r ⋅ σ⟩" by auto
from s t rlcheck show ?thesis by force
qed
fun check_step
where
"check_step c [] s t =
error (shows ''no step from'' ∘ shows s ∘ shows '' and '' ∘ shows t ∘ shows '' found '')"
| "check_step c (e # E) s t =
choice [check_step_rule c e s t, check_step c E s t] <+? shows_sep id shows_nl"
declare check_step.simps[code]
lemma check_step:
assumes ok: "isOK (check_step chk es s t)"
shows "∃ C σ p l r. (l,r) ∈ set es ∧ s = C⟨l ⋅ σ⟩ ∧ t = C⟨r ⋅ σ⟩ ∧ isOK (chk (l ⋅ σ) (r ⋅ σ))"
using assms
proof (induct es)
case (Cons e es)
then obtain l r where e:"e = (l,r)" by force
note mono = ordstep_mono[OF _ subset_refl, of _ "set (e # es)"]
from Cons show ?case proof(cases "isOK(check_step_rule chk (l,r) s t)")
case True
with e check_step_rule [OF this] mono [of "set [e]"] show ?thesis by auto
next
case False
with Cons(2)[unfolded check_step.simps] e have "isOK (check_step chk es s t)" by auto
with Cons(1) mono show ?thesis by auto
qed
qed simp
abbreviation "check_rstep ≡ check_step (λ _ _. succeed)"
lemma check_rstep [dest!]:
assumes "isOK (check_rstep R s t)"
shows "(s, t) ∈ rstep (set R)"
using rstepI and check_step [OF assms] by fast
fun firstM
where
"firstM f [] = error []"
| "firstM f (x # xs) = (try f x ⪢ return x catch (λe. firstM f xs <+? Cons e))"
lemma firstM:
"isOK (firstM f xs) ⟷ (∃x∈set xs. isOK (f x))"
by (induct xs) (auto simp: catch_def split: sum.splits)
lemma firstM_Inr:
assumes "firstM f xs = Inr y"
shows "isOK (f y) ∧ y ∈ set xs"
using assms by (induct xs) (auto simp: catch_def split: sum.splits)
definition "find_variant_in_trs r R =
firstM (check_variants_rule r) R <+? (shows_sep id shows_nl)"
lemma find_variant_in_trs_Inr [elim!]:
assumes "find_variant_in_trs r R = Inr r'"
obtains p where "r' ∈ set R" and "r' = p ∙ r"
using assms by (auto simp: find_variant_in_trs_def dest!: firstM_Inr)
lemma check_first_variant_trs [elim!]:
assumes "isOK (find_variant_in_trs r R)"
obtains r' where "find_variant_in_trs r R = Inr r'"
using assms by auto
locale oc_ops =
fixes check_ord :: "('a::show, string) term ⇒ ('a, string) term ⇒ shows check"
begin
abbreviation "check_ordstep ≡ check_step check_ord"
abbreviation "check_mem_eq eq E ≡
check (eq ∈ set E) (shows eq ∘ shows '' is not an available equation'')"
abbreviation "check_mem_rl ρ R ≡
check (ρ ∈ set R) ( shows_rule ρ ∘ shows '' is not an available rule'')"
abbreviation "check_oriented ≡ check_allm (λ(l, r). check_ord l r)"
definition mytest where "mytest = error (shows ''rule does not match'')"
fun check_step
where
"check_step (E, R) (OC_Deduce s t u) = do {
let S = R @ sym_list E;
check_rstep S s t <+? (λstr. shows '' no step from '' ∘ shows_term s ∘ shows '' to '' ∘ shows_term t ∘ str);
check_rstep S s u <+? (λstr. shows '' no step from '' ∘ shows_term s ∘ shows '' to '' ∘ shows_term u ∘ str);
return ((t, u) # E, R)
} <+? (λstr. shows ''error in deduce step '' ∘ shows_term t ∘ shows '' <- '' ∘ shows_term s ∘ shows '' -> '' ∘ shows_term u ∘ str)"
| "check_step (E, R) (OC_Orientl s t) = do {
check_ord s t;
st ← find_variant_in_trs (s, t) E;
return (removeAll st E, (s, t) # R)
} <+? (λstr. shows ''error in orientl step for '' ∘ shows_term s ∘ shows '' -> '' ∘ shows_term t ∘ str)"
| "check_step (E, R) (OC_Orientr s t) = do {
check_ord t s;
st ← find_variant_in_trs (s, t) E;
return (removeAll st E, (t, s) # R)
} <+? (λstr. shows ''error in orientr step for '' ∘ shows_term s ∘ shows '' -> '' ∘ shows_term t ∘ str)"
| "check_step (E, R) (OC_Delete s) = do {
ss ← find_variant_in_trs (s, s) E;
return (removeAll ss E, R)
} <+? (λstr. shows ''error in delete step for '' ∘ shows_term s ∘ shows '' = '' ∘ shows_term s ∘ str)"
| "check_step (E, R) (OC_Compose s t u) = do {
st ← find_variant_in_trs (s, t) R;
let R'' = removeAll st R;
check_ordstep (R'' @ (sym_list E)) t u <+? (λstr. shows '' no ordstep from '' ∘ shows_term t ∘ shows '' to '' ∘ shows_term u ∘ str);
return (E, (s, u) # R'')
} <+? (λstr. shows ''error in compose step from '' ∘ shows_term s ∘ shows '' -> '' ∘ shows_term t ∘ shows '' to '' ∘
shows_term s ∘ shows '' -> '' ∘ shows_term u ∘ str)"
| "check_step (E, R) (OC_Simplifyl s t u) = do {
st ← find_variant_in_trs (s, t) E;
let E'' = removeAll st E;
check_ordstep (R @ (sym_list E'')) s u <+? (λstr. shows '' no ordstep from '' ∘ shows_term s ∘ shows '' to '' ∘ shows_term u ∘ str);
return ((u, t) # E'', R)
} <+? (λstr. shows ''error in simplifyl step from '' ∘ shows_term s ∘ shows '' = '' ∘ shows_term t ∘ shows '' to '' ∘
shows_term u ∘ shows '' = '' ∘ shows_term t ∘ str)"
| "check_step (E, R) (OC_Simplifyr s t u) = do {
st ← find_variant_in_trs (s, t) E;
let E'' = removeAll st E;
check_ordstep (R @ sym_list E'') t u <+? (λstr. shows '' no ordstep from '' ∘ shows_term t ∘ shows '' to '' ∘ shows_term u ∘ str);
return ((s, u) # E'', R)
} <+? (λstr. shows ''error in simplifyr step from '' ∘ shows_term s ∘ shows '' = '' ∘ shows_term t ∘ shows '' to '' ∘
shows_term s ∘ shows '' = '' ∘ shows_term u ∘ str)"
| "check_step (E, R) (OC_Collapse s t u) = do {
ts ← find_variant_in_trs (t, s) R;
let R'' = removeAll ts R;
check_ordstep (R'' @ (sym_list E)) t u <+? (λstr. shows '' no ordstep from '' ∘ shows_term t ∘ shows '' to '' ∘ shows_term u ∘ str);
return ((u, s) # E, R'')
} <+? (λstr. shows ''error in collapse step from '' ∘ shows_term s ∘ shows '' -> '' ∘ shows_term t ∘ shows '' to '' ∘
shows_term u ∘ shows '' = '' ∘ shows_term t ∘ str)"
fun check_oc
where
"check_oc (E, R) (E', R') [] =
check_same_set E E' <+? (λ_. shows '' equation sets do not match'') ⪢
check_same_set R R' <+? (λ_. shows '' rule sets do not match'')"
| "check_oc (E, R) (E', R') (x # xs) = do {
(E'', R'') ← check_step (E, R) x;
check_oc (E'', R'') (E', R') xs
}"
end
lemmas [code] = oc_ops.check_step.simps
lemmas [code] = oc_ops.check_oc.simps
locale oc_spec =
ordered_completion_inf less +
oc_ops check_ord
for less :: "('a::show, string) term ⇒ ('a, string) term ⇒ bool" (infix "≻" 50)
and check_ord :: "('a, string) term ⇒ ('a, string) term ⇒ shows check" +
assumes check_ord [simp]: "isOK (check_ord s t) ⟷ s ≻ t"
begin
lemma check_ordstep:
assumes "isOK (check_ordstep R s t)"
shows "(s, t) ∈ ordstep {≻} (set R)"
using ordstep.intros [of _ _ "set R"] and check_step [OF assms] by auto
lemma check_ordstep_Inr [dest!]:
assumes "check_ordstep R s t = Inr u"
shows "(s, t) ∈ ordstep {≻} (set R)"
using assms and check_ordstep by auto
lemma check_oriented:
"isOK (check_oriented rs) ⟹ (set rs) ⊆ {≻}"
by auto
lemma check_step_Inr:
assumes "check_step (E, R) step = Inr (E', R')" and "set R ⊆ {≻}"
shows "oKB' (set E, set R) (set E', set R')"
using assms
proof-
let ?R = "set R" and ?E = "set E"
{fix s t RR EE π
assume a:"(s, t) ∈ ordstep {≻} (RR ∪ EE⇧↔)" "RR ⊆ ?R"
from subst.closedI subst have "subst.closed {≻}" by auto
from ordstep_subst[OF this] a(1) have "(π ∙ s, π ∙ t) ∈ ordstep {≻} (RR ∪ EE⇧↔)"
unfolding term_apply_subst_Var_Rep_perm[symmetric] by blast
with ostep_iff_ordstep assms(2) a(2) have "(π ∙ s, π ∙ t) ∈ ostep EE RR" by blast
}
note ostep = this
show ?thesis proof(cases step)
case (OC_Deduce s t u)
note ok = assms[unfolded this check_step.simps Let_def]
hence ids:"R' = R" "E' = (t, u) # E" by auto
from ok have "isOK(check_rstep (R @ sym_list E) s t) ∧ isOK(check_rstep (R @ sym_list E) s u)" by (simp, force)
with check_rstep have rsteps:"(s, t) ∈ rstep (?R ∪ ?E⇧↔)" "(s, u) ∈ rstep (?R ∪ ?E⇧↔)" by auto
from oKB'.deduce[OF this, of 0] show ?thesis unfolding ids by auto
next
case (OC_Orientl s t)
then show ?thesis
using assms
apply (auto simp: Let_def rule_pt.permute_prod.simps elim!: bindE)
proof-
fix π
assume a:"step = OC_Orientl s t" "s ≻ t" "(π ∙ s,π ∙ t) ∈ ?E"
with a(2) have "π ∙ s ≻ π ∙ t" using less_set_permute by blast
from oKB'.orientl[OF this a(3), of _ "-π"]
show "oKB' (?E, ?R) (?E - {(π ∙ s,π ∙ t)}, insert (s,t) ?R)" by auto
qed
next
case (OC_Orientr s t)
then show ?thesis
using assms
apply (auto simp: Let_def rule_pt.permute_prod.simps elim!: bindE)
proof-
fix π
assume a:"step = OC_Orientr s t" "t ≻ s" "(π ∙ s,π ∙ t) ∈ ?E"
with a(2) have "π ∙ t ≻ π ∙ s" using less_set_permute by blast
from oKB'.orientr[OF this a(3), of _ "-π"]
show "oKB' (?E, ?R) (?E - {(π ∙ s,π ∙ t)}, insert (t,s) ?R)" by auto
qed
next
case (OC_Delete s)
then show ?thesis using assms oKB'.delete by (auto simp: rule_pt.permute_prod.simps)
next
case (OC_Compose s t u)
then show ?thesis using assms
apply (auto simp: Let_def rule_pt.permute_prod.simps elim!: bindE)
proof-
fix π
let ?Rm = "?R - {(π ∙ s, π ∙ t)}"
assume a:"(t, u) ∈ ordstep {≻} (?Rm ∪ (set E')⇧↔)" "(π ∙ s,π ∙ t) ∈ ?R"
from ostep[OF a(1)] have "(π ∙ t, π ∙ u) ∈ ostep (set E') ?Rm" by blast
from oKB'.compose[OF this a(2), of "-π"]
show "oKB' (set E', ?R) (set E', insert (s, u) ?Rm)" by force
qed
next
case (OC_Simplifyl s t u)
then show ?thesis using assms
apply (auto simp: Let_def rule_pt.permute_prod.simps elim!: bindE)
proof-
fix π
let ?Em = "?E - {(π ∙ s, π ∙ t)}"
assume a:"(s, u) ∈ ordstep {≻} (set R' ∪ ?Em⇧↔)" "(π ∙ s,π ∙ t) ∈ ?E" "R = R'"
from ostep[OF a(1)] a(3) have "(π ∙ s, π ∙ u) ∈ ostep ?Em ?R" by blast
from oKB'.simplifyl[OF this a(2), of "-π"] a(3)
show "oKB' (set E, set R') (insert (u, t) ?Em, set R')" by force
qed
next
case (OC_Simplifyr s t u)
then show ?thesis using assms
apply (auto simp: Let_def rule_pt.permute_prod.simps elim!: bindE)
proof-
fix π
let ?Em = "?E - {(π ∙ s, π ∙ t)}"
assume a:"(t, u) ∈ ordstep {≻} (set R' ∪ ?Em⇧↔)" "(π ∙ s,π ∙ t) ∈ ?E" "R = R'"
from ostep[OF a(1)] a(3) have "(π ∙ t, π ∙ u) ∈ ostep ?Em ?R" by blast
from oKB'.simplifyr[OF this a(2), of "-π"] a(3)
show "oKB' (set E, set R') (insert (s, u) ?Em, set R')" by force
qed
next
case (OC_Collapse s t u)
then show ?thesis using assms apply (auto simp: Let_def rule_pt.permute_prod.simps elim!: bindE)
proof-
fix π
let ?Rm = "?R - {(π ∙ t, π ∙ s)}"
assume a:"(t, u) ∈ ordstep {≻} (?Rm ∪ ?E⇧↔)" "(π ∙ t,π ∙ s) ∈ ?R"
from ostep[OF a(1)] have "(π ∙ t, π ∙ u) ∈ ostep ?E ?Rm" by blast
from oKB'.collapse[OF this a(2), of "-π"]
show "oKB' (set E, set R) (insert (u, s) ?E, ?Rm)" by force
qed
qed
qed
lemma oKB'_less:
assumes "(E, R) ⊢⇩o⇩K⇩B⇧π (E', R')" and "R ⊆ {≻}"
shows "R' ⊆ {≻}"
proof -
have [dest]: "(x, y) ∈ R ⟹ x ≻ y" for x y using ‹R ⊆ {≻}› by auto
note assms(1)
moreover
{ fix s t π assume "s ≻ t"
hence "π ∙ s ≻ π ∙ t" using less_set_permute by auto }
moreover
{ fix s t u π assume "(t, u) ∈ rstep (R - {(s, t)})" and "(s, t) ∈ R"
then have "s ≻ u" by (induct t u) (blast intro: subst ctxt dest: trans)
hence "π ∙ s ≻ π ∙ u" using less_set_permute by auto }
moreover
{ fix s t u π assume "(t, u) ∈ ordstep {≻} (E⇧↔)" and "(s, t) ∈ R"
then have "s ≻ u" by (cases) (auto dest: trans ctxt)
hence "π ∙ s ≻ π ∙ u" using less_set_permute by auto }
ultimately show ?thesis by (cases, (fastforce simp: ostep_def)+)
qed
lemma oKB'_rtrancl_less:
assumes "oKB'⇧*⇧* (E, R) (E', R')" and "R ⊆ {≻}"
shows "R' ⊆ {≻}"
using assms by (induct "(E, R)" "(E', R')" arbitrary: E' R') (auto dest!: oKB'_less)
lemma oKB_ER_permuted:
assumes "(E, R) ⊢⇩o⇩K⇩B⇧π (E', R')"
shows "E ∪ R ⊆ Id ∪ E' ∪ R' ∪ (rstep (E' ∪ R'))⇧↔ ∪ (rstep (E' ∪ R'))⇧↔ O (rstep (E' ∪ R'))⇧↔"
using assms
proof-
from ostep_imp_rstep_sym have orstep:"⋀s t.(s, t) ∈ ostep E' R' ⟹ (s, t) ∈ (rstep (E' ∪ R'))⇧↔" by blast
let ?step2 = "(rstep (E' ∪ R'))⇧↔ O (rstep (E' ∪ R'))⇧↔"
show ?thesis using assms
proof (cases)
case (simplifyl s u t π)
then have su:"(s, u) ∈ ostep E' R'"
by (intro ostep_mono [THEN subsetD, OF _ _ simplifyl(3)]) auto
from simplifyl have "(π ∙ u, π ∙ t) ∈ E'" by auto
from rstep.rule[OF this] have "(u,t) ∈ (rstep (E' ∪ R'))⇧↔" using rstep_permute_iff by blast
with orstep[OF su] have "(s, t) ∈ ?step2" by blast
then show ?thesis unfolding simplifyl by blast
next
case (simplifyr t u s π)
then have tu:"(t, u) ∈ ostep E' R'"
by (intro ostep_mono [THEN subsetD, OF _ _ simplifyr(3)]) auto
from simplifyr have "(π ∙ s, π ∙ u) ∈ E'" by auto
from rstep.rule[OF this] have "(s, u) ∈ (rstep (E' ∪ R'))⇧↔" using rstep_permute_iff by blast
with orstep[OF tu] have "(s, t) ∈ ?step2" unfolding simplifyr by blast
then show ?thesis unfolding simplifyr by blast
next
case (orientl s t π)
have "(s,t) ∈ (rstep R')" unfolding orientl using rstep_permute_iff
by (metis UnI2 rstep.rule rstep_union singletonI)
then show ?thesis using orientl by fast
next
case (orientr s t π)
have "(s,t) ∈ (rstep R')" unfolding orientr using rstep_permute_iff
by (metis UnI2 rstep.rule rstep_union singletonI)
then show ?thesis using orientr by fast
next
case (compose t u s π)
then have tu:"(t, u) ∈ ostep E' R'"
by (intro ostep_mono [THEN subsetD, OF _ _ compose(3)]) auto
from compose have "(π ∙ s, π ∙ u) ∈ R'" by auto
from rstep.rule[OF this] have "(s, u) ∈ (rstep (E' ∪ R'))⇧↔" using rstep_permute_iff by blast
with orstep[OF tu] have "(s, t) ∈ ?step2" by blast
then show ?thesis unfolding compose by blast
next
case (collapse t u s π)
then have tu:"(t, u) ∈ ostep E' R'"
by (intro ostep_mono [THEN subsetD, OF _ _ collapse(3)]) auto
from collapse have "(π ∙ u, π ∙ s) ∈ E'" by auto
from rstep.rule[OF this] have "(u,s) ∈ (rstep (E' ∪ R'))⇧↔" using rstep_permute_iff by blast
with orstep[OF tu] have "(t, s) ∈ ?step2" by auto
then show ?thesis unfolding collapse by blast
qed auto
qed
lemma oKB_ER_permuted_rev:
assumes "(E, R) ⊢⇩o⇩K⇩B⇧π (E', R')"
shows "E' ∪ R' ⊆ (rstep (E ∪ R))⇧↔ ∪ (rstep (E ∪ R))⇧↔ O (rstep (E ∪ R))⇧↔"
proof-
from ostep_imp_rstep_sym have orstep:"⋀s t.(s, t) ∈ ostep E R ⟹ (s, t) ∈ (rstep (E ∪ R))⇧↔" by blast
let ?step2 = "(rstep (E ∪ R))⇧↔ O (rstep (E ∪ R))⇧↔"
show ?thesis using assms
proof (cases)
case (simplifyl s u t π)
have "(s, u) ∈ ostep E R"
by (intro ostep_mono [THEN subsetD, OF _ _ simplifyl(3)]) auto
with simplifyl(4) orstep have "(u, t) ∈ ?step2" by fast
then show ?thesis unfolding simplifyl by auto
next
case (simplifyr t u s π)
have "(t, u) ∈ ostep E R"
by (intro ostep_mono [THEN subsetD, OF _ _ simplifyr(3)]) auto
with simplifyr(4) orstep have "(s, u) ∈ ?step2" by fast
then show ?thesis unfolding simplifyr by auto
next
case (deduce u s t π)
hence "(u, s) ∈ (rstep (E ∪ R))⇧↔" "(u, t) ∈ (rstep (E ∪ R))⇧↔" by auto
then have "(s, t) ∈ ?step2" by blast
with deduce show ?thesis by auto
next
case (collapse t u s π)
have "(t, u) ∈ ostep E R"
by (intro ostep_mono [THEN subsetD, OF _ _ collapse(3)]) auto
with collapse(4) orstep have "(u, s) ∈ ?step2" by fast
then show ?thesis unfolding collapse by auto
next
case (compose t u s π)
have "(t, u) ∈ ostep E R"
by (intro ostep_mono [THEN subsetD, OF _ _ compose(3)]) auto
with compose(4) orstep have "(s, u) ∈ ?step2" by fast
then show ?thesis unfolding compose by auto
qed auto
qed
lemma oKB_permuted_rstep_subset:
assumes oKB: "(E, R) ⊢⇩o⇩K⇩B⇧π (E', R')"
shows "rstep (E ∪ R) ⊆ (rstep (E' ∪ R'))⇧↔⇧*"
proof-
let ?C = "(rstep (E' ∪ R'))⇧↔⇧*"
have 1:"rstep (Id ∪ E' ∪ R') ⊆ ?C" by fast
have 2:"rstep ((rstep (E' ∪ R'))⇧↔) ⊆ ?C" by fast
from relcomp_mono[OF 2 2] have 3:"(rstep (E' ∪ R'))⇧↔ O (rstep (E' ∪ R'))⇧↔ ⊆ ?C"
unfolding conversion_O_conversion by auto
from rstep_mono[OF 3] rstep_rstep have 3:"rstep ((rstep (E' ∪ R'))⇧↔ O (rstep (E' ∪ R'))⇧↔) ⊆ ?C"
using conversion_O_conversion
by (metis relcomp_mono[OF 2 2] conversion_O_conversion rstep_relcomp_idemp1 rstep_simps(5))
show ?thesis using oKB_ER_permuted [OF oKB, THEN rstep_mono]
unfolding rstep_union[of _ "_ O _"] rstep_union[of _ "( _)⇧↔"]
using 1 2 3 by blast
qed
lemma oKB_conversion_permuted_subset:
assumes "(E, R) ⊢⇩o⇩K⇩B⇧π (E', R')"
shows "(rstep (E ∪ R))⇧↔⇧* ⊆ (rstep (E' ∪ R'))⇧↔⇧*"
using conversion_mono [OF oKB_permuted_rstep_subset [OF assms]] by auto
lemma oKB_permuted_rstep_subset_rev:
assumes oKB: "(E, R) ⊢⇩o⇩K⇩B⇧π (E', R')"
shows "rstep (E' ∪ R') ⊆ (rstep (E ∪ R))⇧↔⇧*"
proof-
let ?C = "(rstep (E ∪ R))⇧↔⇧*"
have 1:"rstep ((rstep (E ∪ R))⇧↔) ⊆ ?C" by fast
from relcomp_mono[OF 1 1] have 2:"(rstep (E ∪ R))⇧↔ O (rstep (E ∪ R))⇧↔ ⊆ ?C"
unfolding conversion_O_conversion by auto
from rstep_mono[OF 2] rstep_rstep have 3:"rstep ((rstep (E ∪ R))⇧↔ O (rstep (E ∪ R))⇧↔) ⊆ ?C"
using conversion_O_conversion
by (metis relcomp_mono[OF 1 1] conversion_O_conversion rstep_relcomp_idemp1 rstep_simps(5))
from oKB_ER_permuted_rev[OF assms, THEN rstep_mono] show ?thesis
unfolding rstep_union[of _ "_ O _"] using 1 3 by blast
qed
lemma oKB_conversion_permuted_subset_rev:
assumes "(E, R) ⊢⇩o⇩K⇩B⇧π (E', R')"
shows "(rstep (E' ∪ R'))⇧↔⇧* ⊆ (rstep (E ∪ R))⇧↔⇧*"
using conversion_mono [OF oKB_permuted_rstep_subset_rev [OF assms]] by auto
lemma oKB_step_conversion_permuted:
assumes "(E, R) ⊢⇩o⇩K⇩B⇧π (E', R')"
shows "(rstep (E' ∪ R'))⇧↔⇧* = (rstep (E ∪ R))⇧↔⇧*"
using oKB_conversion_permuted_subset[OF assms] oKB_conversion_permuted_subset_rev[OF assms] by auto
lemma oKB_steps_conversion_permuted:
assumes "oKB'⇧*⇧* (E, R) (E', R')"
shows "(rstep (E' ∪ R'))⇧↔⇧* = (rstep (E ∪ R))⇧↔⇧*"
using assms
by (induct "(E, R)" "(E', R')" arbitrary: E' R')
(force dest!: oKB_step_conversion_permuted)+
lemma oKB_steps_conversion_FGROUND:
assumes "oKB'⇧*⇧* (E, R) (E', R')"
shows "FGROUND F ((rstep (E ∪ R))⇧↔⇧*) = FGROUND F ((rstep (E' ∪ R'))⇧↔⇧*)"
unfolding FGROUND_def using oKB_steps_conversion_permuted[OF assms] by auto
lemma E_ord_ordstep:"rstep (E_ord op ≻ E) = ordstep {≻} (E⇧↔)"
proof(rule, rule)
fix s t
assume "(s,t) ∈ rstep (E_ord op ≻ E)"
from rstepE[OF this] obtain l r C τ σ where lr:"(l,r) ∈ E⇧↔" and ts:"l⋅τ ≻ r⋅τ" "s = C⟨l⋅τ⋅σ⟩" "t = C⟨r⋅τ⋅σ⟩"
unfolding E_ord_def mem_Collect_eq
by (metis Pair_inject)
from ts subst[OF ts(1)] have ts:"l⋅(τ ∘⇩s σ) ≻ r⋅(τ ∘⇩s σ)" "s = C⟨l⋅(τ ∘⇩s σ)⟩" "t = C⟨r⋅(τ ∘⇩s σ)⟩"
unfolding subst_subst_compose by auto
show "(s,t) ∈ ordstep {≻} (E⇧↔)" unfolding ordstep.simps
by(rule exI[of _ l],rule exI, rule exI,rule exI, rule exI[of _ "τ ∘⇩s σ"], insert lr ts, auto)
next
show "ordstep {≻} (E⇧↔) ⊆ rstep (E_ord op ≻ E)"
proof
fix s t
assume "(s, t) ∈ ordstep {≻} (E⇧↔)"
then obtain l r C τ where lr:"(l,r) ∈ E⇧↔" and ts:"l⋅τ ≻ r⋅τ" "s = C⟨l⋅τ⟩" "t = C⟨r⋅τ⟩" unfolding ordstep.simps by auto
hence "(l⋅τ,r⋅τ) ∈ E_ord op ≻ E" unfolding E_ord_def by auto
with lr show "(s, t) ∈ rstep (E_ord op ≻ E)" unfolding ts by auto
qed
qed
lemma FGROUND_rstep_FGROUND_ostep:
assumes "R ⊆ {≻}" and gtotal: "⋀s t. ground s ⟹ ground t ⟹ s = t ∨ s ≻ t ∨ t ≻ s"
shows "FGROUND F ((rstep (E ∪ R))⇧↔⇧*) = FGROUND F ((ostep E R)⇧↔⇧*)"
proof(rule, rule)
fix s t
assume "(s,t) ∈ FGROUND F ((rstep (E ∪ R))⇧↔⇧*)"
hence fs:"funas_term s ⊆ F" "funas_term t ⊆ F" and g:"ground s" "ground t" "(s,t) ∈ (rstep (E ∪ R))⇧↔⇧*"
unfolding FGROUND_def fground_def by auto
note gconv = gterm_conv_GROUND_conv[OF g]
interpret gtotal_reduction_order by (insert gtotal, standard, auto)
from GROUND_rstep_ordstep[of R E] have "GROUND (rstep (R ∪ E⇧↔)) ⊆ (GROUND (ostep E R))⇧↔⇧*"
unfolding ostep_def E_ord_ordstep[symmetric] rstep_union by auto
hence "GROUND (rstep (E ∪ R)) ⊆ (GROUND (ostep E R))⇧↔⇧*" unfolding rstep_union GROUND_def by auto
from conversion_mono[OF this] have "(GROUND (rstep (E ∪ R)))⇧↔⇧* ⊆ (GROUND (ostep E R))⇧↔⇧*"
unfolding conversion_conversion_idemp by auto
with gconv have "(s,t) ∈ (GROUND (ostep E R))⇧↔⇧*" by auto
with conversion_mono[OF GROUND_subset] have "(s,t) ∈ (ostep E R)⇧↔⇧*" by auto
with fs g show "(s,t) ∈ FGROUND F ((ostep E R)⇧↔⇧*)" unfolding FGROUND_def fground_def by auto
next
note ostep_conv = ostep_iff_ordstep[OF assms(1), symmetric]
from ordstep_imp_rstep[of _ _ "{≻}" "R ∪ _⇧↔", unfolded ostep_conv] have 1:"ostep E R ⊆ rstep (R ∪ E⇧↔)" by auto
have "rstep (R ∪ E⇧↔) ⊆ (rstep (E ∪ R))⇧↔⇧*" by auto
with 1 have "ostep E R ⊆ (rstep (E ∪ R))⇧↔⇧*" by auto
from conversion_mono[OF this] have "(ostep E R)⇧↔⇧* ⊆ (rstep (E ∪ R))⇧↔⇧*"
unfolding conversion_conversion_idemp by auto
thus "FGROUND F ((ostep E R)⇧↔⇧*) ⊆ FGROUND F ((rstep (E ∪ R))⇧↔⇧*)" unfolding FGROUND_def by auto
qed
lemma oKB'_rtrancl_FGROUND_conversion:
assumes "oKB'⇧*⇧* (E, R) (E', R')" and
R:"R ⊆ {≻}" and
gtotal: "⋀s t. ground s ⟹ ground t ⟹ s = t ∨ s ≻ t ∨ t ≻ s"
shows "FGROUND F ((rstep (E ∪ R))⇧↔⇧*) = FGROUND F ((ostep E' R')⇧↔⇧*)"
proof-
from assms oKB'_rtrancl_less have "R' ⊆ {≻}" by auto
from oKB_steps_conversion_FGROUND[OF assms(1)] FGROUND_rstep_FGROUND_ostep[OF this] gtotal show ?thesis by auto
qed
lemma check_oc:
assumes ok: "isOK (check_oc (E, R) (E', R') xs)" and R:"isOK (check_oriented R)"
shows "oKB'⇧*⇧* (set E, set R) (set E', set R')"
proof-
from check_oriented[OF R] have R: "set R ⊆ {≻}" by auto
with ok show ?thesis
proof (induct xs arbitrary: E R)
case Nil
then show ?case by auto
next
case (Cons x xs)
then obtain E'' and R'' where 1: "check_step (E, R) x = Inr (E'', R'')"
and 2: "isOK (check_oc (E'', R'') (E', R') xs)" by auto
note step = check_step_Inr[OF 1 Cons(3)]
from step[THEN oKB'_less] Cons(3) have less:"set R'' ⊆ {≻}" by auto
from Cons.hyps [OF 2 less] step show ?case by auto
qed
qed
end
locale oc_spec_extension =
oc:oc_spec less1 check_ord1 +
oc':oc_spec less2 check_ord2
for less1 less2 :: "('a::show, string) term ⇒ ('a, string) term ⇒ bool" and
check_ord1 check_ord2 check_ord :: "('a, string) term ⇒ ('a, string) term ⇒ shows check" +
assumes less_extension:"⋀s t. less1 s t ⟹ less2 s t"
begin
lemma ostep:"(s,t) ∈ oc.ostep E R ⟹ (s,t) ∈ oc'.ostep E R"
unfolding oc.ostep_def oc'.ostep_def Un_iff ordstep.simps
using less_extension by fast
lemma oKB'_step:
assumes "oc.oKB' (E,R) (E',R')"
shows "oc'.oKB' (E,R) (E',R')"
using assms
proof(cases)
case (deduce s t u p)
show ?thesis unfolding deduce
using deduce(3) deduce(4) oc'.oKB'.deduce by blast
next
case (orientl s t p)
show ?thesis unfolding orientl
using less_extension[OF orientl(3)] orientl(4) oc'.oKB'.orientl by blast
next
case (orientr t s p)
show ?thesis unfolding orientr
using less_extension[OF orientr(3)] orientr(4) oc'.oKB'.orientr by blast
next
case (delete s)
show ?thesis unfolding delete using delete(3) oc'.oKB'.delete by blast
next
case (compose t u s p)
show ?thesis unfolding compose
using ostep[OF compose(3)] compose(4) oc'.oKB'.compose by blast
next
case (simplifyl s u t p)
show ?thesis unfolding simplifyl
using ostep[OF simplifyl(3)] simplifyl(4) oc'.oKB'.simplifyl by blast
next
case (simplifyr t u s p)
show ?thesis unfolding simplifyr
using ostep[OF simplifyr(3)] simplifyr(4) oc'.oKB'.simplifyr by blast
next
case (collapse t u s p)
show ?thesis unfolding collapse
using ostep[OF collapse(3)] collapse(4) oc'.oKB'.collapse by blast
qed
lemma oKB'_steps:
assumes "oc.oKB'⇧*⇧* (E,R) (E',R')"
shows "oc'.oKB'⇧*⇧* (E,R) (E',R')"
using assms
by (induct "(E, R)" "(E', R')" arbitrary: E' R')
(force dest!: oKB'_step)+
end
locale gcr_ops =
fixes xvar yvar :: "'v::{show, infinite} ⇒ 'v"
and check_joinable :: "('f::show, 'v) rules ⇒ ('f, 'v) rules ⇒ ('f, 'v) term ⇒ ('f, 'v) term ⇒ shows check"
and check_instance :: "('f, 'v) rules ⇒ ('f, 'v) rules ⇒ ('f, 'v) term ⇒ ('f, 'v) term ⇒ shows check"
begin
definition "check_ooverlap E R ρ⇩1 ρ⇩2 p =
(case mgu_var_disjoint_generic xvar yvar (fst ρ⇩1) (fst ρ⇩2 |_ p) of
None ⇒ succeed
| Some (σ⇩1, σ⇩2) ⇒
let s = replace_at (fst ρ⇩2 ⋅ σ⇩2) p (snd ρ⇩1 ⋅ σ⇩1) in
let t = snd ρ⇩2 ⋅ σ⇩2 in
choice [
check_instance E R s t <+? (λe. shows ''CP '' ∘ shows_term s ∘ shows '' = '' ∘ shows_term t ∘ shows '' not an instance of an equation'' ∘ e),
check_joinable E R s t <+? (λe. shows ''CP '' ∘ shows_term s ∘ shows '' = '' ∘ shows_term t ∘ shows '' is not joinable'' ∘ e)
] <+? shows_sep id shows_nl)"
text ‹Check extended critical pairs.›
definition
"check_ECPs E R =
(let E' = sym_list E; S = List.union R E' in
check_allm (λρ⇩2. let l⇩2 = fst ρ⇩2 in check_allm (λρ⇩1. check_allm (λp.
check_ooverlap E' R ρ⇩1 ρ⇩2 p) (funposs_list l⇩2)) S) S)"
end
lemmas [code] =
gcr_ops.check_ooverlap_def gcr_ops.check_ECPs_def
definition "Rules E R = List.union R (sym_list E)"
lemma set_Rules [simp]: "set (Rules E R) = set R ∪ (set E)⇧↔" by (auto simp: Rules_def)
locale gcr_spec =
gcr_ops xvar yvar check_joinable check_instance +
gtotal_reduction_order_inf less
for xvar :: "'v::{show, infinite} ⇒ 'v"
and yvar :: "'v ⇒ 'v"
and check_joinable :: "('f::show, 'v) rules ⇒ ('f, 'v) rules ⇒ ('f, 'v) term ⇒ ('f, 'v) term ⇒ shows check"
and check_instance :: "('f, 'v) rules ⇒ ('f, 'v) rules ⇒ ('f, 'v) term ⇒ ('f, 'v) term ⇒ shows check"
and less :: "('f, 'v) term ⇒ ('f, 'v) term ⇒ bool" (infix "≻" 50)
and F :: "('f × nat) list" +
assumes joinable: "set R ⊆ {≻} ⟹ isOK (check_joinable E R s t) ⟹
(s, t) ∈ (ordstep {≻} (set (Rules E R)))⇧↓"
and "instance": "isOK (check_instance E R s t) ⟹ ∃l r σ. (l, r) ∈ set (Rules E R) ∧ s = l ⋅ σ ∧ t = r ⋅ σ"
and ren: "inj xvar" "inj yvar" "range xvar ∩ range yvar = {}"
begin
lemma check_ECPs_ooverlap:
assumes "isOK (check_ECPs E R)"
and "ooverlap {≻} (set (Rules E R)) r r' p μ s t"
and R: "set R ⊆ {≻}"
shows "(s, t) ∈ (ordstep {≻} (set (Rules E R)))⇧↓ ∨
(∃l r σ. (l, r) ∈ (set (Rules E R))⇧↔ ∧ s = l ⋅ σ ∧ t = r ⋅ σ)"
proof -
let ?R = "set (Rules E R)"
from assms(2) obtain π⇩1 and π⇩2 where rules': "π⇩1 ∙ r ∈ ?R" "π⇩2 ∙ r' ∈ ?R"
and disj: "vars_rule r ∩ vars_rule r' = {}"
and p': "p ∈ funposs (fst r')"
and mgu': "mgu (fst r) (fst r' |_ p) = Some μ"
and "¬ (snd r ⋅ μ ≻ fst r ⋅ μ)" "¬ (snd r' ⋅ μ ≻ fst r' ⋅ μ)"
and t: "t = snd r' ⋅ μ"
and s: "s = replace_at (fst r' ⋅ μ) p (snd r ⋅ μ)"
unfolding ooverlap_def by fast
define ρ⇩1 and ρ⇩2 where "ρ⇩1 = π⇩1 ∙ r" and "ρ⇩2 = π⇩2 ∙ r'"
have p: "p ∈ funposs (fst ρ⇩2)"
and "ρ⇩1 ∈ ?R" and "ρ⇩2 ∈ ?R"
using p' and rules' by (auto simp: ρ⇩1_def ρ⇩2_def rule_pt.fst_eqvt [symmetric])
with assms have *: "isOK (check_ooverlap (sym_list E) R ρ⇩1 ρ⇩2 p)" by (auto simp: check_ECPs_def)
have "(fst r' |_ p) ⋅ μ = fst r ⋅ μ" using mgu' [THEN mgu_sound] by (auto simp: is_imgu_def)
then have "(fst r' |_ p) ⋅ (μ ∘ Rep_perm (-π⇩2) ∘ Rep_perm π⇩2) =
fst r ⋅ (μ ∘ Rep_perm (-π⇩1) ∘ Rep_perm π⇩1)"
by (simp add: o_assoc [symmetric] Rep_perm_add [symmetric] Rep_perm_0)
then have "fst ρ⇩2 |_ p ⋅ (μ ∘ Rep_perm (-π⇩2)) = fst ρ⇩1 ⋅ (μ ∘ Rep_perm (-π⇩1))"
using p [THEN funposs_imp_poss]
by (auto simp: ρ⇩1_def ρ⇩2_def permute_term_subst_apply_term [symmetric] eqvt)
from mgu_var_disjoint_generic_complete [OF ren this[symmetric]] obtain μ⇩1 μ⇩2 δ
where mgu: "mgu_var_disjoint_generic xvar yvar (fst ρ⇩1) (fst ρ⇩2 |_ p) = Some (μ⇩1, μ⇩2)"
and **: "μ ∘ Rep_perm (- π⇩1) = μ⇩1 ∘⇩s δ" "μ ∘ Rep_perm (- π⇩2) = μ⇩2 ∘⇩s δ" by blast
have "vars_term (fst r) ⊆ vars_rule r" and "vars_term (fst r' |_ p) ⊆ vars_rule r'"
using p' [THEN funposs_imp_poss, THEN vars_term_subt_at] by (auto simp: vars_defs)
from mgu_imp_mgu_var_disjoint [OF mgu' ren disj this finite_vars_rule finite_vars_rule, of π⇩1 π⇩2]
obtain μ' and π
where left: "∀x∈vars_rule r. μ x = (sop π⇩1 ∘⇩s (μ' ∘ xvar) ∘⇩s sop (- π)) x" (is "∀x∈_. μ x = ?π⇩1 x")
and right: "∀x∈vars_rule r'. μ x = (sop π⇩2 ∘⇩s (μ' ∘ yvar) ∘⇩s sop (- π)) x" (is "∀x∈_. μ x = ?π⇩2 x")
and "mgu (π⇩1 ∙ (fst r) ⋅ (Var ∘ xvar)) (π⇩2 ∙ (fst r' |_ p) ⋅ (Var ∘ yvar)) = Some μ'"
by blast
then have "mgu_var_disjoint_generic xvar yvar (fst ρ⇩1) (fst ρ⇩2 |_ p) = Some (μ' ∘ xvar, μ' ∘ yvar)"
and μ⇩1: "μ⇩1 = μ' ∘ xvar" and μ⇩2: "μ⇩2 = μ' ∘ yvar"
using p' [THEN funposs_imp_poss] and mgu
unfolding ρ⇩1_def ρ⇩2_def mgu_var_disjoint_generic_def
by (auto simp del: mgu.simps
simp: map_vars_term_eq mgu_var_disjoint_generic_def ρ⇩1_def ρ⇩2_def eqvt)
let ?t = "snd ρ⇩2 ⋅ μ⇩2"
let ?t' = "snd r' ⋅ μ"
let ?s = "replace_at (fst ρ⇩2 ⋅ μ⇩2) p (snd ρ⇩1 ⋅ μ⇩1)"
let ?s' = "replace_at (fst r' ⋅ μ) p (snd r ⋅ μ)"
have "fst r' ⋅ μ = fst r' ⋅ ?π⇩2" and snd_r: "snd r' ⋅ μ = snd r' ⋅ ?π⇩2"
using right unfolding term_subst_eq_conv by (auto simp: vars_defs)
then have 1: "fst ρ⇩2 ⋅ μ⇩2 = π ∙ (fst r' ⋅ μ)"
and t': "?t' = -π ∙ ?t" by (auto simp: μ⇩2 ρ⇩2_def eqvt)
have "snd r ⋅ μ = snd r ⋅ ?π⇩1"
using left unfolding term_subst_eq_conv by (auto simp: vars_defs)
then have 2: "snd ρ⇩1 ⋅ μ⇩1 = π ∙ (snd r ⋅ μ)" by (auto simp: μ⇩1 ρ⇩1_def eqvt)
then have s': "?s' = -π ∙ ?s"
using p' [THEN funposs_imp_poss]
unfolding 1 by (auto simp: eqvt)
from snd_r have 2: "snd ρ⇩2 ⋅ μ⇩2 = π ∙ (snd r' ⋅ μ)" by (auto simp: μ⇩2 ρ⇩2_def eqvt)
consider (join) "isOK (check_joinable (sym_list E) R ?s ?t)"
| (inst) "isOK (check_instance (sym_list E) R ?s ?t)"
using * and mgu unfolding check_ooverlap_def by (auto simp: check_ooverlap_def)
then show ?thesis
proof (cases)
case join
from joinable [OF R join] have "(?s, ?t) ∈ (ordstep {≻} ?R)⇧↓" by simp
from join_subst [OF subst_closed_ordstep [OF subst_closed_less] this, of "sop (-π)"]
have "(s, t) ∈ (ordstep {≻} ?R)⇧↓"
using p [THEN funposs_imp_poss]
unfolding s t s' using term_pt.permute_flip [OF 1] term_pt.permute_flip [OF 2]
by (simp add: eqvt [symmetric])
then show ?thesis by blast
next
case inst
from "instance" [OF inst] obtain u and v and σ
where uv: "(u, v) ∈ ?R⇧↔" and "?s = u ⋅ σ" and "?t = v ⋅ σ" by auto
then have "?s' = u ⋅ (σ ∘⇩s (sop (- π)))"
and "?t' = v ⋅ (σ ∘⇩s (sop (- π)))" by (auto simp: s' t')
with uv show ?thesis unfolding s t by blast
qed
qed
lemma check_ECPs:
assumes R: "set R ⊆ {≻}" and ok: "isOK (check_ECPs E R)"
shows "GCR (ordstep {≻} (set (Rules E R)))"
proof -
{ fix s t assume "(s, t) ∈ set (Rules E R)"
with R have "s ≻ t ∨ (t, s) ∈ set (Rules E R)" by auto }
then show ?thesis
using check_ECPs_ooverlap [OF ok _ R]
by (intro GCR_ordstep) auto
qed
end
definition "check_joinable R s t =
(case (compute_rstep_NF R s, compute_rstep_NF R t) of
(Some u, Some v) ⇒ check (u = v) (shows ''normal forms differ'')
| _ ⇒ error (shows ''error: check_joinable''))"
lemma check_joinable:
assumes "isOK (check_joinable R s t)"
shows "(s, t) ∈ (rstep (set R))⇧↓"
using assms
by (auto simp: check_joinable_def split: option.splits dest: compute_rstep_NF_sound)
definition "check_rule_instance r r' =
(case match_list Var [(fst r', fst r), (snd r', snd r)] of
Some _ ⇒ succeed
| None ⇒ error (shows ''rules do not match''))"
lemma check_rule_instance [simp]:
"isOK (check_rule_instance (l, r) (l', r')) ⟷ (∃σ. l = l' ⋅ σ ∧ r = r' ⋅ σ)"
by (auto simp: check_rule_instance_def split: option.splits dest!: match_list_sound match_list_complete)
definition "check_instance E s t =
check_exm (check_rule_instance (s, t)) E (shows_sep id shows_nl)"
lemma check_instance [simp]:
"isOK (check_instance E s t) ⟷ (∃l r σ. (l, r) ∈ set E ∧ s = l ⋅ σ ∧ t = r ⋅ σ)"
by (auto simp: check_instance_def) (insert check_rule_instance, blast+)
context oc_spec
begin
lemma gcr_spec:
assumes "gtotal_reduction_order (op ≻)"
shows "gcr_spec x_var y_var (λ_. check_joinable) (λE _. check_instance E) (op ≻)"
proof -
interpret gtotal_reduction_order "(op ≻)" by fact
interpret gcr_spec x_var y_var
"(λ_. check_joinable)" "(λE _. check_instance E)"
apply (unfold_locales)
apply (drule check_joinable)
apply (rule join_mono [THEN subsetD, of "rstep (set R)" "ordstep {≻} (set (Rules E R))" for E R])
apply (simp add: ordstep_Un ordstep_rstep_conv subst_closed_less)
apply assumption
apply force+
done
show ?thesis by fact
qed
end
definition "check_ECPs =
gcr_ops.check_ECPs x_var y_var (λ_. check_joinable) (λE _. check_instance E)"
definition "check_FGCR ro F E R = do {
redord.valid ro;
check_subseteq (funas_trs_list (List.union E R)) F
<+? (λf. shows ''the function symbol '' ∘ shows f ∘ shows '' does not occur in the TRS⏎'');
check_ECPs E R
}"
lemma funas_trs_converse [simp]:
"funas_trs (R¯) = funas_trs R"
by (auto simp: funas_defs)
lemma check_FGCR:
fixes F :: "('f::{show,key} × nat) list"
assumes "isOK (check_FGCR (create_KBO_redord r F) F E R)"
and R: "set R ⊆ {(s, t). redord.less (create_KBO_redord r F) s t}"
shows "CR (FGROUND (set F) (ordstep ({(s, t). redord.less (create_KBO_redord r F) s t}) (set (Rules E R))))"
proof -
let ?F = "set F"
let ?R = "set (Rules E R)"
define less :: "('f, string) term ⇒ ('f, string) term ⇒ bool" and c :: "'f"
where
"less = redord.less (create_KBO_redord r F)" and
"c = redord.min_const (create_KBO_redord r F)"
have valid: "isOK (redord.valid (create_KBO_redord r F))"
and ecps: "isOK (check_ECPs E R)"
and F: "funas_trs ?R ⊆ ?F"
using assms by (auto simp: check_FGCR_def)
from KBO_redord.valid [OF valid] obtain less'
where ro: "reduction_order less"
and c: "(c, 0) ∈ ?F"
and fground: "∀s t. fground ?F s ∧ fground ?F t ⟶ s = t ∨ less s t ∨ less t s"
and ro': "gtotal_reduction_order less'"
and subset: "∀s t. less s t ⟶ less' s t"
and min: "∀t. ground t ⟶ less'⇧=⇧= t (Fun c [])"
by (auto simp: less_def c_def)
interpret ro: reduction_order less by fact
interpret ro': gtotal_reduction_order less' by fact
have R: "set R ⊆ ro'.less_set" using R and subset by (auto simp: less_def)
have *: "{(x, y). less x y} ⊆ ro'.less_set" using subset by auto
interpret oc: oc_spec less' "λs t. check (less' s t) (shows '''')" by (unfold_locales) simp
interpret gcr: gcr_spec x_var y_var "(λ_. check_joinable)" "(λE _. check_instance E)" less'
using oc.gcr_spec [OF ro'] .
have "isOK (gcr.check_ECPs E R)" using ecps by (auto simp: check_ECPs_def)
then have "GCR (ordstep ro'.less_set ?R)" by (rule gcr.check_ECPs [OF R])
then show ?thesis using ro'.GCR_imp_CR_FGROUND [OF * ro fground min c F] by (simp add: less_def)
qed
definition "check_FGCR_run ro F E⇩0 R⇩0 E R steps = do {
let check_ord = (λs t. check (redord.less ro s t) (shows ''term pair cannot be oriented''));
oc_ops.check_oriented check_ord R⇩0;
oc_ops.check_oc check_ord (E⇩0, R⇩0) (E, R) steps <+? (λs. shows ''the oKB run could not be reconstructed⏎'' ∘ shows_nl ∘ s);
check_FGCR ro F E R <+? (λs. shows ''ground confluence could not be verified⏎'' ∘ shows_nl ∘ s)
}"
lemma check_FGCR_run:
fixes F :: "('f::{show,key} × nat) list"
fixes E :: "(('f, char list) term × ('f, char list) term) list"
fixes ro:: "('f, string) redord"
assumes "isOK (check_FGCR_run (create_KBO_redord r F) F E⇩0 R⇩0 E R steps)"
shows "CR (FGROUND (set F) (ordstep ({(s, t). redord.less (create_KBO_redord r F) s t}) (set (Rules E R)))) ∧
equivalent (set E⇩0 ∪ set R⇩0) (set E ∪ set R)"
proof -
let ?F = "set F"
let ?ER = "set (Rules E R)"
define less :: "('f, string) term ⇒ ('f, string) term ⇒ bool" and c :: "'f"
where
"less = redord.less (create_KBO_redord r F)" and
"c = redord.min_const (create_KBO_redord r F)"
from assms have FGCR:"isOK(check_FGCR (create_KBO_redord r F) F E R)" by (auto simp: check_FGCR_run_def)
have valid: "isOK (redord.valid (create_KBO_redord r F))"
and ecps: "isOK (check_ECPs E R)"
and F: "funas_trs ?ER ⊆ ?F"
using FGCR by (auto simp: check_FGCR_def)
from KBO_redord.valid [OF valid] obtain less'
where ro: "reduction_order less"
and c: "(c, 0) ∈ ?F"
and fground: "∀s t. fground ?F s ∧ fground ?F t ⟶ s = t ∨ less s t ∨ less t s"
and ro': "gtotal_reduction_order less'"
and subset: "∀s t. less s t ⟶ less' s t"
and min: "∀t. ground t ⟶ less'⇧=⇧= t (Fun c [])"
by (auto simp: less_def c_def)
interpret ro: reduction_order less by fact
interpret ro': gtotal_reduction_order less' by fact
define check_ord where "check_ord = (λs t. check (less s t) (shows ''term pair cannot be oriented''))"
have check_ord: "⋀s t. isOK (check_ord s t) ⟷ less s t" unfolding check_ord_def by auto
define check_ord' where "check_ord' = (λs t. check (less' s t) (shows ''term pair cannot be oriented''))"
have check_ord': "⋀s t. isOK (check_ord' s t) ⟷ less' s t" unfolding check_ord'_def by auto
interpret oc: oc_spec less check_ord by (insert check_ord, unfold_locales) simp
interpret oc': oc_spec less' check_ord' by (insert check_ord', unfold_locales) simp
have oc_ok: "isOK (oc.check_oc (E⇩0, R⇩0) (E, R) steps)" and
oriented_ok: "isOK (oc.check_oriented R⇩0)"
using assms[unfolded check_FGCR_run_def] unfolding check_ord_def less_def by force+
note run = oc.check_oc[OF this]
note oriented = oc.check_oriented[OF oriented_ok]
with run oc.oKB'_rtrancl_less have "set R ⊆ ro.less_set" by auto
with check_FGCR[OF FGCR] have CR:"CR (FGROUND ?F (ordstep {(s, t). less s t} ?ER))"
using less_def by auto
note equiv = oc.oKB_steps_conversion_permuted[OF run]
with CR less_def show ?thesis
unfolding equivalent_def conversion_def by (simp add: equiv esteps_is_conversion)
qed
text ‹
We say that the system @{term E},@{term R} is a ground-complete rewrite system for the
equational system @{term E⇩0} with respect to the reduction order @{term less} iff the
respective equational theories are the same ordered rewriting with @{term E},@{term R} is
confluent on ground terms.
›
datatype 'f reduction_order_input =
RPO_Input "'f status_prec_repr"
| KBO_Input "'f prec_weight_repr"
definition
ordered_completed_rewrite_system :: "('f::{key}, 'v) trs ⇒ ('f, 'v) trs ⇒ ('f, 'v) trs ⇒ 'f reduction_order_input ⇒ bool"
where
"ordered_completed_rewrite_system E⇩0 E R ord ≡
case ord of KBO_Input precw ⇒
let (p,w,w0,lcs,scf) = prec_weight_repr_to_prec_weight_funs precw in
let less = λ s t. fst (kbo.kbo w w0 (scf_repr_to_scf scf) (λf. f ∈ set lcs) (λ f g. fst (p f g)) (λ f g. snd (p f g)) s t) in
equivalent E⇩0 (E ∪ R) ∧ CR (FGROUND (funas_trs E⇩0) (ordstep {(s, t). less s t} (E⇧↔ ∪ R)))"
end