theory Equational_Reasoning_Impl
imports
Equational_Reasoning
Completion
QTRS.Trs_Impl
begin
abbreviation "shows_eqs ≡ shows_trs' shows shows ''equational system:'' '' = ''"
abbreviation "shows_eq ≡ shows_rule' shows shows '' = ''"
abbreviation shows_ln :: "nat ⇒ shows" where
"shows_ln i ≡ shows_nl +@+ shows i +@+ shows_string '': ''"
function
eq_proof_lines :: "('f::show, 'v::show) eq_proof ⇒ nat ⇒ (shows × nat × ('f, 'v) rule)"
and eq_proofs_lines :: "('f::show, 'v::show) eq_proof list ⇒ nat ⇒ (shows × nat list × ('f, 'v) term list × ('f, 'v) term list)"
where
"eq_proof_lines (Refl s) i = (shows_ln (Suc i) +@+ shows_eq (s, s) +@+ shows_string '' [refl]'', Suc i, s, s)"
| "eq_proof_lines (Sym p) i = (
let (s, i', l, r) = eq_proof_lines p i in
(s +@+ shows_ln (Suc i') +@+ shows_eq (r, l) +@+ '' [sym '' +#+ shows i' +@+ shows_string '']'', Suc i', r, l))"
| "eq_proof_lines (Trans p1 p2) i = (
let (s1, i1, s, t) = eq_proof_lines p1 i in
let (s2, i2, u, v) = eq_proof_lines p2 i1 in
(s1 +@+ s2 +@+
shows_ln (Suc i2) +@+ shows_eq (s, v) +@+ '' [trans '' +#+ shows i1 +@+ '', '' +#+ shows i2 +@+ shows_string '']'', Suc i2, s, v))"
| "eq_proof_lines (Assm (l, r) σ) i = (
let eq = (l ⋅ σ, r ⋅ σ) in
(shows_ln (Suc i) +@+ shows_eq eq +@+ '' [assm '' +#+ shows_eq (l, r) +@+ shows_string '']'', Suc i, eq))"
| "eq_proof_lines (Cong f ps) i = (
let (s, is, ls, rs) = eq_proofs_lines ps i in
let eq = (Fun f ls, Fun f rs) in
let i' = last is in
let is = butlast is in
(s +@+ shows_ln (Suc i') +@+ shows_eq eq +@+ shows_list_gen shows '' [cong]'' '' [cong '' '', '' '']'' is, Suc i', eq))"
| "eq_proofs_lines [] i = (id, [i], [], [])"
| "eq_proofs_lines (p#ps) i = (
let (s1, i', l, r) = eq_proof_lines p i in
let (s2, is, ls, rs) = eq_proofs_lines ps i' in
(s1 +@+ s2, i'#is, l#ls, r#rs))"
by (pat_completeness) auto
termination by (lexicographic_order)
abbreviation shows_eq_proof where "shows_eq_proof p ≡ fst (eq_proof_lines p 0)"
definition
check_estep ::
"('f::show, 'v::show) equation list ⇒
pos ⇒ ('f, 'v) rule ⇒ bool ⇒ ('f, 'v) term ⇒ ('f, 'v) term ⇒
shows check"
where
"check_estep E p rule l_to_r s t ≡ do {
check (∃r∈set E. rule =⇩v r)
(shows_rule rule +@+ '' is not an equation of'' +#+ shows_nl +@+ shows_eqs E +@+ shows_nl);
check (p ∈ poss s) (shows p +@+ '' is not a position of '' +#+ shows s +@+ shows_nl);
check (p ∈ poss t) (shows p +@+ '' is not a position of '' +#+ shows t +@+ shows_nl);
let C = ctxt_of_pos_term p s;
let D = ctxt_of_pos_term p t;
let u = subt_at s p;
let v = subt_at t p;
let rrule = (if l_to_r then rule else (snd rule, fst rule));
let err = (''the term '' +#+ shows t
+@+ '' does not result from a proper application of term '' +#+ shows s +@+ '' using equation ''
+#+ shows_nl +@+ shows_eq rrule +@+ '' at position '' +#+ shows p +@+ shows_nl);
(case match_list Var [(fst rrule, u), (snd rrule, v)] of
Some σ ⇒ check (C = D) err
| None ⇒ error err)
}"
lemma check_estep_sound:
assumes ok: "isOK (check_estep E p r l_to_r s t)"
shows "(s, t) ∈ estep (set E)"
proof -
let ?C = "ctxt_of_pos_term p s"
let ?D = "ctxt_of_pos_term p t"
let ?r = "if l_to_r then r else (snd r,fst r)"
let ?mlist = "[(subt_at s p, fst ?r), (subt_at t p, snd ?r)]"
note ok = ok[unfolded check_estep_def Let_def, simplified]
from ok
have ps: "p ∈ poss s" and pt: "p ∈ poss t" and "∃rule ∈ set E. r =⇩v rule" by auto
then obtain rule where rule: "rule ∈ set E" and inst: "(fst r, snd r) =⇩v (fst rule, snd rule)" by auto
from eq_rule_mod_varsE[OF inst]
obtain δ where fst: "fst r = fst rule ⋅ δ" and snd: "snd r = snd rule ⋅ δ" by auto
let ?E = "(set E)⇧↔"
have "∃ rule ∈ ?E. fst ?r = fst rule ⋅ δ ∧ snd ?r = snd rule ⋅ δ"
proof (cases l_to_r)
case True
thus ?thesis using rule fst snd by auto
next
case False
show ?thesis
by (rule bexI[of _ "(snd rule,fst rule)"], insert rule fst snd False, auto)
qed
then obtain rule where rule: "rule ∈ ?E" and fst: "fst ?r = fst rule ⋅ δ"
and snd: "snd ?r = snd rule ⋅ δ" by auto
from ok
obtain σ where some: "match_list Var [(fst ?r, subt_at s p), (snd ?r, subt_at t p)] = Some σ"
by force
from match_list_sound [OF this]
have "fst ?r ⋅ σ = s |_ p" and "snd ?r ⋅ σ = t |_ p" by auto
hence s: "s |_ p = fst rule ⋅ δ ∘⇩s σ" and t: "t = ?D⟨snd rule ⋅ δ ∘⇩s σ⟩"
using ctxt_supt_id[OF pt] fst snd by simp+
from ok and some
have DC: "?D = ?C" by simp
have "(s,t) ∈ rstep_r_p_s ?E rule p (δ ∘⇩s σ)"
unfolding rstep_r_p_s_def Let_def
by (rule, unfold split t[unfolded DC], intro conjI, rule ps, rule rule,
insert ctxt_supt_id[OF ps, unfolded s], auto)
hence "(s,t) ∈ rstep ?E" unfolding rstep_iff_rstep_r_p_s
using surjective_pairing by metis
thus ?thesis unfolding estep_def .
qed
type_synonym ('f, 'v) eseq = "(pos × ('f, 'v) equation × bool × ('f, 'v) term) list"
fun
check_conversion ::
"('f::show, 'v::show) equation list ⇒
('f, 'v) eseq ⇒ ('f, 'v) term ⇒ ('f, 'v) term ⇒ shows check"
where
"check_conversion E [] s u = check (s = u) (
''the last term of the conversion '' +#+ shows_nl +@+ shows s +@+ shows_nl +@+
''does not correspond to the goal term'' +#+ shows_nl +@+ shows u +@+ shows_nl)"
| "check_conversion E ((p, r, l_to_r, t) # c) s u = do {
check_estep E p r l_to_r s t;
check_conversion E c t u
}"
lemma check_conversion_sound:
assumes ok: "isOK (check_conversion E eseq s t)"
shows "(s, t) ∈ (estep (set E))^*"
using ok
proof (induct eseq arbitrary: s t)
case Nil
thus ?case by auto
next
case (Cons st eseq s u)
obtain p r l_to_r t where st: "st = (p,r,l_to_r,t)" by (cases st, force+)
from Cons(2)[unfolded st, simplified]
have one: "isOK(check_estep E p r l_to_r s t)" and rec: "isOK(check_conversion E eseq t u)" by auto
from check_estep_sound[OF one] Cons(1)[OF rec] show ?case by auto
qed
type_synonym ('f, 'v) subsumption_proof = "(('f, 'v) equation × ('f, 'v) eseq) list"
fun
check_subsumptions_guided :: "('f :: show, 'v :: show) equation list ⇒ ('f, 'v) subsumption_proof ⇒ shows check"
where "check_subsumptions_guided E [] = succeed"
| "check_subsumptions_guided E ((e, seq) # convs) = do {
check_conversion E seq (fst e) (snd e)
<+? (λ s. ''problem in conversion for equation '' +#+ shows_eq e +@+ shows_nl +@+ s);
check_subsumptions_guided (e # E) convs
}"
lemma check_subsumptions_guided:
assumes ok: "isOK (check_subsumptions_guided E convs)"
shows "subsumes (set E) (fst ` set convs)"
unfolding subsumes_via_rule_conversion
using ok
proof (induct convs arbitrary: E)
case Nil show ?case by simp
next
case (Cons ec convs)
obtain s t conv where ec: "ec = ((s,t),conv)" by (cases ec, force)
note Cons = Cons[unfolded ec]
from Cons(2) have rec: "isOK(check_subsumptions_guided ((s,t) # E) convs)"
and one: "isOK(check_conversion E conv s t)" by auto
from check_conversion_sound[OF one] have one: "(s,t) ∈ (estep (set E))^*" .
{
fix l r
assume "(l,r) ∈ fst ` set convs"
with Cons(1)[OF rec] have "(l,r) ∈ (estep (set ((s,t) # E)))^*" by auto
hence "(l,r) ∈ (estep (set E))^*"
proof (induct)
case base show ?case by simp
next
case (step r u)
from step(2) have "(r,u) ∈ estep {(s,t)} ∨ (r,u) ∈ estep (set E)"
unfolding estep_def using rstep_union[of "{(s,t)}^<->" "(set E)^<->"]
by auto
hence "(r,u) ∈ (estep (set E))^*"
proof
assume "(r,u) ∈ estep (set E)"
thus ?thesis by auto
next
assume step: "(r,u) ∈ estep {(s,t)}"
have "subsumes (set E) {(s,t)}"
unfolding subsumes_via_rule_conversion using one by auto
thus ?thesis unfolding subsumes_def eq_theory_is_esteps
using step by auto
qed
with step(3) show ?case by auto
qed
}
thus ?case unfolding ec using one by force
qed
definition check_subsumption_guided :: "('f :: show, 'v :: show) equation list ⇒ ('f,'v)equation list ⇒ ('f, 'v) subsumption_proof ⇒ shows check"
where "check_subsumption_guided E E' convs ≡ do {
check_subseteq E (map fst convs)
<+? (λr. ''could not find conversion for equation '' +#+ shows_eq r);
check_subsumptions_guided E' convs
}"
lemma check_subsumption_guided:
assumes ok: "isOK (check_subsumption_guided E E' convs)"
shows "subsumes (set E') (set E)"
proof -
note ok = ok[unfolded check_subsumption_guided_def]
from ok have subset: "set E ⊆ fst ` set convs" and
ok: "isOK (check_subsumptions_guided E' convs)" by auto
from check_subsumptions_guided[OF ok] subset
show ?thesis
unfolding subsumes_via_rule_conversion by blast
qed
definition check_single_subsumption :: "('f :: show, 'v :: show) equation ⇒ ('f,'v)equation list ⇒ ('f, 'v) subsumption_proof ⇒ shows check"
where "check_single_subsumption eq E convs ≡ do {
check (eq ∈ set (map fst convs)) (''could not find conversion for equation '' +#+ shows_eq eq);
check_subsumptions_guided E convs
}"
lemma check_single_subsumption:
assumes ok: "isOK (check_single_subsumption eq E convs)"
shows "eq ∈ (estep (set E))^*"
proof -
note ok = ok[unfolded check_single_subsumption_def]
from ok have mem: "eq ∈ fst ` set convs" and
ok: "isOK (check_subsumptions_guided E convs)" by auto
from check_subsumptions_guided[OF ok] mem
show ?thesis
unfolding subsumes_via_rule_conversion by force
qed
definition check_convertible_instance :: "('f :: show, 'v :: show) equation ⇒ ('f,'v)equation list ⇒ ('f, 'v) subsumption_proof ⇒ shows check"
where "check_convertible_instance eq E convs ≡ do {
check_exm (λc. check (instance_rule (fst c) eq) (''not an instance of '' +#+ shows_eq eq)) convs (λ_. shows '' no instance found'');
check_subsumptions_guided E convs
}"
lemma check_convertible_instance:
assumes ok: "isOK (check_convertible_instance (s,t) E convs)"
shows "∃σ. (s⋅σ, t⋅σ) ∈ (estep (set E))^*"
proof -
note ok = ok[unfolded check_convertible_instance_def]
from ok obtain c where inst: "fst c ∈ fst ` set convs" "instance_rule (fst c) (s,t)"
and ok: "isOK (check_subsumptions_guided E convs)" by fastforce
obtain u v where uv:"fst c = (u,v)" by fastforce
from inst obtain σ where σ: "u = s ⋅ σ ∧ v = t ⋅ σ" unfolding uv instance_rule_def by auto
note sub = check_subsumptions_guided[OF ok, unfolded subsumes_via_rule_conversion, rule_format, of "fst c"]
with σ inst(1) show ?thesis unfolding uv by force
qed
lemma check_join_NF_conversion:
assumes ok: "isOK (check_join_NF R s t)"
shows "(s,t) ∈ (estep (set R))^*"
by (rule set_mp[OF join_conversion check_join_NF_sound[OF ok]])
definition
check_subsumption_NF :: "('f::show, 'v::show) equation list ⇒ ('f, 'v) rules ⇒ shows check"
where
"check_subsumption_NF E R ≡ do {
check_allm (λ e. check_join_NF R (fst e) (snd e)
<+? (λs. ''could not join equation '' +#+ shows_eq e +@+ shows_nl +@+ s)) E
}"
lemma check_subsumption_NF:
assumes ok: "isOK (check_subsumption_NF E R)"
shows "subsumes (set R) (set E)"
proof -
note ok = ok[unfolded check_subsumption_NF_def, simplified]
show ?thesis
unfolding subsumes_via_rule_conversion
proof (clarify)
fix s t
assume "(s,t) ∈ set E"
with ok have "isOK (check_join_NF R s t)" by auto
from check_join_NF_conversion[OF this]
show "(s, t) ∈ (estep (set R))^*" .
qed
qed
definition
check_subsumption :: "('f::show, 'v::show) equation list ⇒ ('f, 'v) rules ⇒ ('f, 'v) subsumption_proof option ⇒ shows check"
where
"check_subsumption E R convs_o ≡
(case convs_o of
None ⇒ check_subsumption_NF E R
| Some convs ⇒ check_subsumption_guided E R convs)"
lemma check_subsumption:
assumes ok: "isOK (check_subsumption E R convs_o)"
shows "subsumes (set R) (set E)"
proof -
note ok = ok[unfolded check_subsumption_def]
show ?thesis
proof (cases convs_o)
case None
show ?thesis
by (rule check_subsumption_NF, insert None ok, auto)
next
case (Some convs)
show ?thesis
by (rule check_subsumption_guided, insert Some ok, auto)
qed
qed
end