section ‹Main result for bounded duplicating systems›
theory LS_Bounded_Duplicating
imports LS_Common
begin
fun map_funs_mctxt :: "('f ⇒ 'g) ⇒ ('f, 'v) mctxt ⇒ ('g, 'v) mctxt" where
"map_funs_mctxt _ MHole = MHole"
| "map_funs_mctxt _ (MVar x) = MVar x"
| "map_funs_mctxt f (MFun g Cs) = MFun (f g) (map (map_funs_mctxt f) Cs)"
locale weakly_layered_induct_bounded_duplicating = weakly_layered_induct ℱ 𝔏 ℛ rk
for ℱ :: "('f × nat) set" and 𝔏 :: "('f, 'v :: infinite) mctxt set" and ℛ :: "('f, 'v) trs" and
rk :: nat +
fixes R :: "('f, 'v) term rel" and label :: "('f, 'v) term ⇒ ('f option, 'v) term"
assumes bd: "bounded_duplicating ℛ"
defines "label ≡ λs. fill_holes (map_funs_mctxt Some (max_top s)) (map (λt. Fun None [map_funs_term Some s]) (aliens s))"
defines "R ≡ {(s, t) | s t. (label t, label s) ∈ (relto (rstep {(Fun None [Var undefined], Var undefined)}) (rstep (map_funs_trs Some ℛ)))⇧+ }"
begin
lemma wfR:
"wf R"
using wf_inv_image[OF wf_trancl[OF bd[unfolded bounded_duplicating_def SN_rel_on_def SN_iff_wf]]]
unfolding R_def trancl_converse converse_inv_image[symmetric] by (auto simp: converse_def)
lemma transR:
"trans R"
using trans_inv_image[OF trans_trancl[of "_¯"]]
unfolding R_def trancl_converse converse_inv_image[symmetric] by (auto simp: converse_def)
lemma short_short_peak:
assumes "(s, t) ∈ short_step_s s0" "(s, u) ∈ short_step_s s1"
shows "(t, u) ∈ ((⋃i∈under R s0. short_step_s i)⇧↔)⇧* O (short_step_s s1)⇧= O
((⋃i∈under R s0 ∪ under R s1. short_step_s i)⇧↔)⇧* O
((short_step_s s0)¯)⇧= O ((⋃i∈under R s1. short_step_s i)⇧↔)⇧*"
oops
end
end