section ‹Basic facts about layer systems›
theory LS_Basics
imports LS_Prelude QTRS.Renaming_Interpretations
begin
context layer_system
begin
lemma mvar_layer [simp]:
"MVar v ∈ 𝔏"
using L⇩1[of "Var v"] by (auto elim: less_eq_mctxtE2)
lemma mhole_layer [simp]:
"MHole ∈ 𝔏"
using L⇩2[of ε "MVar _" _] by auto
lemma L⇩3':
assumes "L ∈ 𝔏" "N ∈ 𝔏" "p ∈ poss_mctxt L" "(subm_at L p, N) ∈ comp_mctxt"
shows "mreplace_at L p (subm_at L p ⊔ N) ∈ 𝔏"
proof (cases "p ∈ funposs_mctxt L")
case True thus ?thesis using assms by (auto intro: L⇩3)
next
case False
then obtain x where "subm_at L p = MVar x" using assms(3)
proof (induct L arbitrary: p)
case (MFun f Ls)
then obtain i q where "p = i <# q" "q ∉ funposs_mctxt (Ls ! i)"
by (cases p) (auto simp: funposs_mctxt_def)
thus ?thesis using MFun(2-) by (auto intro: MFun(1)[of "Ls ! i" q])
qed auto
thus ?thesis using assms(1,3,4) replace_at_subm_at[of p L]
by (cases N) (auto elim: comp_mctxt.cases simp: all_poss_mctxt_conv)
qed
end
fun vars_to_holes :: "('f, 'v) mctxt ⇒ ('f, 'w) mctxt" where
"vars_to_holes (MVar _) = MHole"
| "vars_to_holes MHole = MHole"
| "vars_to_holes (MFun f ts) = MFun f (map vars_to_holes ts)"
abbreviation vars_to_holes' :: "('f, 'v) mctxt ⇒ ('f, 'v) mctxt" where
"vars_to_holes' ≡ vars_to_holes"
lemma vars_to_holes_idem[simp]:
"vars_to_holes (vars_to_holes C) = vars_to_holes C"
by (induct C) auto
lemma vars_to_holes_prefix:
"vars_to_holes C ≤ C"
by (induct C) (auto simp add: less_eq_mctxt_def zip_map1 zip_same_conv_map)
lemma funposs_mctxt_vars_to_holes [simp]:
"funposs_mctxt (vars_to_holes C) = funposs_mctxt C"
by (induct C) (auto simp: funposs_mctxt_def)
lemma vars_to_holes_mreplace_at [simp]:
"p ∈ poss_mctxt C ⟹ vars_to_holes (mreplace_at C p D) = mreplace_at (vars_to_holes C) p (vars_to_holes D)"
by (induct C p D rule: mreplace_at.induct) (auto simp: take_map drop_map)
lemma vars_to_holes_subm_at [simp]:
"p ∈ poss_mctxt C ⟹ vars_to_holes (subm_at C p) = subm_at (vars_to_holes C) p"
by (induct C p rule: subm_at.induct) auto
lemma vars_to_holes_merge [simp]:
"(C, D) ∈ comp_mctxt ⟹ vars_to_holes (C ⊔ D) = vars_to_holes C ⊔ vars_to_holes D"
by (induct C D rule: comp_mctxt.induct) (auto simp: zip_map1 zip_map2 in_set_conv_nth)
lemma vars_to_holes_comp_mctxt:
"(C, D) ∈ comp_mctxt ⟹ (vars_to_holes C, vars_to_holes D) ∈ comp_mctxt"
by (induct C D rule: comp_mctxt.induct) (auto intro: comp_mctxt.intros)
lemma vars_to_holes_mono:
"C ≤ D ⟹ vars_to_holes C ≤ vars_to_holes D"
unfolding less_eq_mctxt_prime
by (induct C D rule: less_eq_mctxt'.induct) (auto intro: less_eq_mctxt'.intros)
lemma vars_to_holes'_mono: "C ≤ D ⟹ vars_to_holes' C ≤ vars_to_holes' D"
by (rule vars_to_holes_mono)
lemma mctxt_term_conv_vars_to_holes:
"mctxt_term_conv (vars_to_holes C) = mctxt_term_conv C ⋅ (λ_. Var None)"
by (induct C) auto
lemma funas_term_vars_to_holes [simp]:
"funas_mctxt (vars_to_holes C) = funas_mctxt C"
by (induct C) auto
lemma vars_to_holes_map_vars_mctxt [simp]:
"vars_to_holes (map_vars_mctxt f C) = vars_to_holes C"
by (induct C) auto
lemma vars_to_holes_sup:
"(C, D) ∈ comp_mctxt ⟹ vars_to_holes (C ⊔ D) = vars_to_holes C ⊔ vars_to_holes D"
by (induct C D rule: comp_mctxt.induct) (auto simp: comp_def zip_map1 zip_map2 set_conv_nth)
lemma (in layer_system) vars_to_holes_layer:
"vars_to_holes C ∈ 𝔏 ⟷ C ∈ 𝔏"
proof (induct "mctxt_syms C" arbitrary: C rule: less_induct)
case (less C) show *: ?case
proof (cases "∃p v. p ∈ poss_mctxt C ∧ subm_at C p = MVar v")
case True
then obtain p v where p: "p ∈ poss_mctxt C" and C: "subm_at C p = MVar v" by blast
{
fix D :: "('f,'v) mctxt"
assume "D = MHole"
with p C have "vars_to_holes' (mreplace_at C p D) = vars_to_holes (mreplace_at C p (MVar v))"
and "mctxt_syms (mreplace_at C p (MVar v)) > mctxt_syms (mreplace_at C p D)"
and "mreplace_at C p (MVar v) = C"
by (induct C p D rule: mreplace_at.induct) (auto dest: id_take_nth_drop)
}
then show ?thesis using less[of "mreplace_at C p MHole"] L⇩2[OF p, of v] by auto
next
case False
{
assume "⋀p v. p ∈ poss_mctxt C ⟹ subm_at C p ≠ MVar v"
then have "vars_to_holes C = C"
proof (induct C)
case (MFun f ts)
{
fix t p v
assume "t ∈ set ts" and "p ∈ poss_mctxt t"
then have "subm_at t p ≠ MVar v"
using MFun(2)[of "PCons _ p"] in_set_conv_nth[of t ts] by auto
}
with MFun(1) show ?case using map_cong[of ts ts vars_to_holes id] by auto
qed auto
}
with False show ?thesis by simp
qed
qed
lemma (in layer_system) vars_to_holes'_layer:
"vars_to_holes' C ∈ 𝔏 ⟷ C ∈ 𝔏"
by (rule local.vars_to_holes_layer)
lemma vars_to_holes_fill_holes:
"num_holes C = length Cs ⟹ set Cs ⊆ {MHole} ∪ MVar ` UNIV ⟹ vars_to_holes (fill_holes_mctxt C Cs) = vars_to_holes C"
apply (induct C Cs rule: fill_holes_induct)
unfolding List.set_concat
by (auto intro!: nth_equalityI simp: set_conv_nth[of "partition_holes _ _"]) blast
lemma vars_to_holes'_fill_holes:
"num_holes C = length Cs ⟹ set Cs ⊆ {MHole} ∪ MVar ` UNIV ⟹ vars_to_holes' (fill_holes_mctxt C Cs) = vars_to_holes' C"
by (rule vars_to_holes_fill_holes)
lemma (in layer_system) vars_to_holes_fill_holes_layer:
assumes "num_holes C = length Cs" "set Cs ⊆ {MHole} ∪ MVar ` UNIV"
shows "fill_holes_mctxt C Cs ∈ 𝔏 ⟷ C ∈ 𝔏"
by (metis assms vars_to_holes_fill_holes vars_to_holes_layer)
fun holes_to_var where
"holes_to_var MHole = Var undefined"
| "holes_to_var (MVar x) = Var x"
| "holes_to_var (MFun f Cs) = Fun f (map holes_to_var Cs)"
abbreviation holes_to_var' where "holes_to_var' x ≡ mctxt_of_term (holes_to_var x)"
lemma vars_to_holes_holes_to_vars_conv [simp]:
"vars_to_holes (holes_to_var' C) = vars_to_holes C"
by (induct C) auto
lemma holes_to_var_subm [simp]:
"C ≤ holes_to_var' C"
by (induct C) (auto intro: less_eq_mctxtI1)
lemma funas_term_holes_to_var [simp]:
"funas_term (holes_to_var C) = funas_mctxt C"
by (induct C) auto
context layer_system
begin
lemma holes_to_var_layer:
"holes_to_var' C ∈ 𝔏 ⟷ C ∈ 𝔏"
using vars_to_holes_layer[of C] vars_to_holes_layer[of "holes_to_var' C"] by simp
lemma mfun_layer [simp]:
assumes fn: "(f, n) ∈ ℱ" shows "MFun f (replicate n MHole) ∈ 𝔏"
proof -
from fn have *: "funas_term (holes_to_var (MFun f (replicate n (MHole)))) ⊆ ℱ" by auto
obtain L where **: "L ∈ 𝔏" "L ≠ MHole" "L ≤ holes_to_var' (MFun f (replicate n (MHole)))"
using L⇩1[OF *] by blast
then obtain Cs where "L = MFun f Cs" by (cases L) (auto elim: less_eq_mctxtE1)
then have "vars_to_holes' L = MFun f (replicate n (MHole))" using vars_to_holes_mono[OF **(3)]
by (cases L) (auto elim!: less_eq_mctxtE2 intro!: nth_equalityI)
thus ?thesis using `L ∈ 𝔏` vars_to_holes_layer[of L] by simp
qed
lemma sup_mctxt_LL:
"(L, N) ∈ comp_mctxt ⟹ L ∈ 𝔏 ⟹ N ∈ 𝔏 ⟹ L ⊔ N ∈ 𝔏"
by (cases L N rule: comp_mctxt.cases) (insert L⇩3[of L N ε], auto simp: funposs_mctxt_def)
lemma comp_MFunD:
assumes "(MFun f Cs, MFun g Ds) ∈ comp_mctxt"
shows "f = g ∧ length Cs = length Ds ∧ (∀i < length Ds. (Cs ! i, Ds ! i) ∈ comp_mctxt)"
using assms by (auto elim: comp_mctxt.cases)
lemma (in layer_system) map_vars_mctxt_layer [simp]:
"map_vars_mctxt f C ∈ 𝔏 ⟷ C ∈ 𝔏"
using vars_to_holes_layer[of C] vars_to_holes_layer[of "map_vars_mctxt f C"] by simp
text ‹@{cite ‹Lemma 3.5› FMZvO15} part 1›
lemma max_top_unique:
shows "∃!M. M ∈ topsC C ∧ (∀L ∈ topsC C. L ≤ M)"
proof -
let ?r = "{ (D, E). D > E } ∩ topsC C × topsC C"
have "trans ?r" by (auto simp: trans_def)
then have "wf ?r" by (intro finite_acyclic_wf) (auto simp: finite_pre_mctxt acyclic_irrefl irrefl_def topsC_def)
have "MHole ∈ topsC C" by (simp add: topsC_def)
then have "∃L ∈ topsC C. ∀y. (y, L) ∈ ?r ⟶ y ∉ topsC C"
using `wf ?r`[unfolded wf_eq_minimal] by blast
then obtain M where M: "M ∈ topsC C" and *: "⋀L. L ∈ topsC C ⟹ ¬ L > M" by auto
{
fix L
assume L: "L ∈ topsC C"
have c: "(L, M) ∈ comp_mctxt" using L M by (auto intro: prefix_comp_mctxt simp: topsC_def)
have t: "L ⊔ M ∈ topsC C" using L M by (auto intro: sup_mctxt_LL[OF c] prefix_mctxt_sup simp: topsC_def)
have "L ⊔ M ≥ M" by (auto intro: sup_mctxt_ge2 simp: c)
then have "L ⊔ M = M" using *[OF t] by (auto simp: less_mctxt_def)
also have "L ≤ L ⊔ M" by (simp add: c)
ultimately have "L ≤ M" by simp
} note ** = this
show ?thesis
proof
show "M ∈ topsC C ∧ (∀L ∈ topsC C. L ≤ M)" by (simp add: M **)
next
fix M'
assume "M' ∈ topsC C ∧ (∀L ∈ topsC C. L ≤ M')"
then show "M' = M" by (intro antisym) (auto simp: M **)
qed
qed
lemma max_topCI:
assumes "M ∈ topsC C" "⋀L. L ∈ topsC C ⟹ L ≤ M"
shows "max_topC C = M"
using assms max_top_unique[of C] by (auto simp: max_topC_def)
lemma max_topC_props [simp]:
shows "max_topC C ∈ topsC C" and "⋀L. L ∈ topsC C ⟹ L ≤ max_topC C"
by (auto simp: theI'[OF max_top_unique] max_topC_def)
lemmas max_top_props = max_topC_props[where C = "mctxt_of_term _"]
lemma max_topC_layer [simp]:
"max_topC C ∈ 𝔏"
using max_topC_props by (auto simp: topsC_def)
lemmas max_top_layer = max_topC_layer[of "mctxt_of_term _"]
lemma max_topC_prefix:
"max_topC C ≤ C"
using max_topC_props(1) unfolding topsC_def by blast
lemmas max_top_prefix = max_topC_prefix[of "mctxt_of_term _"]
lemma max_topC_mono:
"C ≤ D ⟹ max_topC C ≤ max_topC D"
using max_topC_props(1)[of C] max_topC_props(2)[of "max_topC C" D] by (auto simp: topsC_def)
lemma max_topC_idem:
"max_topC (max_topC C) = max_topC C"
by (metis (lifting) dual_order.antisym max_topC_props mem_Collect_eq topsC_def)
text ‹@{cite ‹Lemma 3.5› FMZvO15} part 2›
lemma non_empty_max_top_non_empty:
assumes "C ∈ 𝒞" "C ≠ MHole" shows "max_topC C ≠ MHole"
proof (cases C)
case MHole thus ?thesis using assms by simp
next
case (MVar v)
then have "MVar v ≤ max_topC C" using assms by (simp add: topsC_def)
thus ?thesis by (auto simp: less_eq_mctxt_def)
next
case (MFun f ts)
then have "MFun f (replicate (length ts) MHole) ∈ topsC C" using assms MFun
by (simp add: topsC_def less_eq_mctxt_def comp_def map_replicate_const 𝒞_def)
then have "MFun f (replicate (length ts) MHole) ≤ max_topC C" by auto
thus ?thesis by (auto simp: less_eq_mctxt_def)
qed
lemma funas_max_topC [simp]:
"C ∈ 𝒞 ⟹ fn ∈ funas_mctxt (max_topC C) ⟹ fn ∈ funas_mctxt C"
using max_topC_props[of C] by (auto simp: topsC_def)
lemma max_top_not_hole [simp]:
"t ∈ 𝒯 ⟹ max_top t ≠ MHole"
by (intro non_empty_max_top_non_empty) (auto simp: 𝒯_def 𝒞_def)
lemma max_topC_mvar [simp]:
"max_topC (MVar x) = MVar x"
proof -
have "Var x ∈ 𝒯" by (simp add: 𝒯_def)
from max_top_not_hole[OF this] have "max_top (Var x) ≠ MHole" .
then show ?thesis
using max_topC_props(1)[unfolded topsC_def, of "mctxt_of_term (Var x)"]
by (cases "max_top (Var x)") (auto elim: less_eq_mctxtE1)
qed
lemma max_top_var [simp]:
"max_top (Var x) = MVar x"
by simp
lemma max_top_var_subst:
"max_top (t ⋅ (Var ∘ f)) = map_vars_mctxt f (max_top t)"
using max_topC_props(1)[of "mctxt_of_term t"] max_topC_props(2)[of _ "mctxt_of_term t"]
by (intro max_topCI) (auto simp del: max_topC_props max_topC_layer simp: topsC_def mctxt_of_term_var_subst
intro: map_vars_mctxt_mono elim!: map_vars_mctxt_less_eq_decomp)
lemma aliens_var_subst:
"aliens (t ⋅ (Var ∘ f)) = map (λt. t ⋅ (Var ∘ f)) (aliens t)"
unfolding max_top_var_subst by (auto intro: max_topC_prefix unfill_holes_var_subst)
lemma funas_term_subt_at:
"p ∈ poss t ⟹ f ∈ funas_term (subt_at t p) ⟹ f ∈ funas_term t"
by (induct t arbitrary: p) force+
lemma 𝒯_subt_at:
"t ∈ 𝒯 ⟹ p ∈ poss t ⟹ subt_at t p ∈ 𝒯"
using funas_term_subt_at[of p t] by (auto simp: 𝒯_def)
text ‹@{cite ‹Definition 3.6› FMZvO15}: decomposing terms into max-top and aliens›
lemma unfill_holes_max_top_subt:
assumes "t ∈ 𝒯" and "t' ∈ set (aliens t)"
shows "t' ⊲ t"
proof (cases t)
note * = max_top_not_hole[OF assms(1)]
have **: "max_top t ≤ mctxt_of_term t" using max_topC_props(1) by (simp add: topsC_def)
{
case (Var v) hence "max_top t = MVar v" using assms * **
by (cases "max_top t") (auto simp: less_eq_mctxt_def topsC_def split: if_splits)
thus ?thesis using assms(2) by (auto simp: Var)
next
note * = max_top_not_hole[OF assms(1)]
case (Fun f ts)
obtain Cs where l: "length Cs = length ts" and mt: "max_top t = MFun f Cs" using assms * **
by (cases "max_top t") (auto simp: less_eq_mctxt_def topsC_def Fun split: if_splits)
then obtain i where i: "i < length Cs" and "t' ∈ set (unfill_holes (Cs ! i) (ts ! i))"
using assms(2) ** by (auto simp: Fun split: if_splits dest!: in_set_idx[of _ "zip Cs ts"])
hence "t' ⊴ ts ! i" using **[unfolded mt, unfolded Fun]
by (auto intro!: unfill_holes_subt[of "Cs !i" "ts ! i" t'] simp: less_eq_mctxt_def
split: if_splits elim!: nth_equalityE)
then show ?thesis using Fun i l set_supteq_into_supt[of "ts ! i" ts t' f] by simp
}
qed
lemma unfill_holes_max_top_smaller [simp]:
"t ∈ 𝒯 ⟹ t' ∈ set (aliens t) ⟹ size t' < size t"
by (simp only: supt_size unfill_holes_max_top_subt)
lemma aliens_not_varC:
"MVar v ∉ set (aliensC C)"
proof
let ?Cs = "aliensC C"
assume "MVar v ∈ set ?Cs"
then obtain i where *: "i < length ?Cs" "?Cs ! i = MVar v" by (auto simp: set_conv_nth)
let ?Ds = "list_update (replicate (length ?Cs) MHole) i (MVar v)"
let ?M' = "fill_holes_mctxt (max_topC C) ?Ds"
have l: "length ?Ds = num_holes (max_topC C)" "max_topC C ≤ C"
using max_topC_props(1)[of C, unfolded topsC_def] by simp_all
have "set ?Ds ⊆ {MVar v, MHole}" using set_update_subset_insert[of "replicate (length ?Cs) MHole" i "MVar v"] by auto
also have "... ⊆ insert MHole (range MVar)" by auto
finally have "?M' ∈ 𝔏" using vars_to_holes_fill_holes_layer[of "max_topC C" ?Ds] l by auto
moreover
have "j < num_holes (max_topC C) ⟹ ?Ds ! j ≤ ?Cs ! j" for j
using * l by (cases "j = i") auto
then have "?M' ≤ C"
using less_eq_fill_holesI[of "?Ds" "max_topC C" ?Cs] * l by (auto simp: fill_unfill_holes_mctxt)
moreover have "max_topC C ≤ ?M'" using fill_holes_mctxt_suffix[of ?Ds "max_topC C"] l
by (simp del: fill_holes_mctxt_suffix)
moreover have "max_topC C ≠ ?M'" using fill_holes_mctxt_id[OF l(1)] l `i < length ?Cs`
set_update_memI[of i "replicate (length ?Cs) MHole" "MVar v"] by auto
ultimately show False
using max_topC_props(2)[of ?M' C] by (simp add: topsC_def del: max_topC_props length_unfill_holes_mctxt)
qed
lemma aliens_not_var:
"Var v ∉ set (aliens t)"
proof
assume "Var v ∈ set (aliens t)"
from imageI[OF this, of mctxt_of_term] aliens_not_varC[of v "mctxt_of_term t"]
max_topC_props(1)[of "mctxt_of_term t", unfolded topsC_def] unfill_holes_mctxt_mctxt_of_term[of "max_top t" t]
show False by auto
qed
text ‹@{cite ‹Definition 3.6› FMZvO15}: rank›
fun rank :: "('f, 'v) term ⇒ nat" where
[simp del]: "rank t = (if t ∈ 𝒯 then 1 + max_list (map rank (aliens t)) else 0)"
lemma rank_var:
"rank (Var v) = 1"
using rank.simps[of "Var v"] by (auto simp: 𝒯_def)
lemma rank_var_subst:
"rank (t ⋅ (Var ∘ f)) = rank t"
proof (induct t rule: rank.induct)
case (1 t)
{ assume "t ∈ 𝒯" note map_ext[OF 1[unfolded atomize_imp, THEN mp], OF this, unfolded comp_def] }
note [simp] = this aliens_var_subst[unfolded comp_def] rank.simps[of t] rank.simps[of "t ⋅ (λt. Var (f t))"]
show ?case by (cases "t ∈ 𝒯") (auto simp: comp_def 𝒯_def funas_term_subst)
qed
lemma unfill_by_itselfI [simp]:
"unfill_holes (mctxt_of_term t) t = []"
by (induct t) auto
lemma unfill_by_itselfD:
"C ≤ mctxt_of_term t ⟹ unfill_holes C t = [] ⟹ C = mctxt_of_term t"
by (induct C "mctxt_of_term t" arbitrary: t rule: less_eq_mctxt_induct; case_tac t)
(auto intro: nth_equalityI)
lemma rank_gt_0:
"t ∈ 𝒯 ⟹ rank t > 0"
by (subst rank.simps) auto
lemma rank_1:
"rank t = 1 ⟷ mctxt_of_term t ∈ 𝔏"
proof (standard, goal_cases)
case 1
then have "aliens t = []" using supt_imp_funas_term_subset[OF unfill_holes_max_top_subt[of t]]
rank_gt_0[of "hd (aliens t)"]
by (subst (asm) rank.simps, cases "aliens t") (fastforce split: if_splits simp: 𝒯_def)+
then have "aliens t = []" by (cases "aliens t") auto
then show ?case using max_top_layer[of t]
by (auto dest!: unfill_by_itselfD[OF max_topC_prefix] simp del: max_topC_layer)
next
case 2 then have "max_top t = mctxt_of_term t"
by (simp add: dual_order.antisym max_topC_prefix topsC_def)
then show ?case using subsetD[OF 𝔏_sig max_top_layer[of t]]
by (subst rank.simps) (auto simp del: max_topC_layer simp: 𝒯_def 𝒞_def)
qed
text ‹@{cite ‹Lemma 3.8› FMZvO15}›
lemma rank_by_top':
assumes "t ∈ 𝒯" and "L ≤ max_top t"
shows "rank t ≤ 1 + max_list (map rank (filter is_Fun (unfill_holes L t)))"
proof -
let ?rank' = "λt. if is_Var t then 0 else rank t"
have [simp]: "map ?rank' (aliens t) = map rank (aliens t)" for t by (auto simp: aliens_not_var)
have ml: "max_list (map rank (filter is_Fun ts)) = max_list (map ?rank' ts)" for ts
by (induct ts) auto
let ?r = "{ (C,D) . C > D } ∩ {N. N ≤ max_top t} × {N. N ≤ max_top t}"
show ?thesis unfolding ml using assms
proof (induct L rule: wf_induct[of ?r])
have "finite ?r" by (simp add: finite_pre_mctxt[of "max_top t"])
moreover have "trans ?r" by (auto simp: trans_def)
ultimately show "wf ?r" by (auto simp: wf_iff_acyclic_if_finite acyclic_def)
next
case (2 C)
{
fix D assume "C ≤ D" "D ≤ mctxt_of_term t" "t ∈ 𝒯"
hence "C = D ∨ C < fill_holes_mctxt C (map max_top (unfill_holes C t)) ⊓ D"
proof (induct C arbitrary: D t)
case MHole
moreover have "max_top t ≤ mctxt_of_term t"
using max_topC_props[of "mctxt_of_term t"] by (auto simp: topsC_def)
ultimately show ?case using max_top_not_hole[of t]
by (cases D; cases "max_top t"; cases t, auto
simp: less_mctxt_def mctxt_order_bot.bot_unique less_eq_mctxt_def split: if_splits)
next
case (MVar v) thus ?case by (cases D, auto simp: less_eq_mctxt_def split: if_splits)
next
case (MFun f Cs)
obtain Ds where Ds: "D = MFun f Ds" "length Ds = length Cs"
using MFun(2) by (cases D) (auto simp: less_eq_mctxt_def split: if_splits)
obtain ts where ts: "t = Fun f ts" "length ts = length Cs"
using MFun Ds by (cases t) (auto simp: less_eq_mctxt_def split: if_splits)
{
fix i assume i: "i < length Cs"
thm MFun(1)[OF nth_mem, of n "Ds ! n" "ts ! n" for n]
have *: "ts ! i ∈ 𝒯" using MFun(4) nth_mem[OF i[unfolded ts(2)[symmetric]]]
by (auto simp: ts 𝒯_def dest!: subsetD)
have "Cs ! i ≤ Ds ! i" "Ds ! i ≤ mctxt_of_term (ts ! i)"
using i MFun(2,3) by (auto simp: Ds ts less_eq_mctxt_def elim!: nth_equalityE)
hence **: "Cs ! i ≤ mctxt_of_term (ts ! i)" by simp
have "Cs ! i = Ds ! i ∨ Cs ! i < fill_holes_mctxt (Cs ! i) (map max_top (unfill_holes (Cs ! i) (ts ! i))) ⊓ Ds ! i"
"length (map max_top (unfill_holes (Cs ! i) (ts ! i))) = num_holes (Cs ! i)"
using MFun(2-4) Ds ts i
by (intro MFun(1))
(auto simp: length_unfill_holes[OF **] 𝒯_def set_conv_nth less_mctxt_def
dest!: subsetD elim!: nth_equalityE elim: less_eq_mctxtE1)
} note * = this
show ?case
using * arg_cong[of _ _ "map (map max_top)", OF partition_by_concat_id[of "map (λi. unfill_holes (Cs ! i) (ts ! i)) [0..<length Cs]" "map num_holes Cs"]]
apply (auto simp: less_mctxt_def Ds ts map_map_partition_by map_concat intro!: nth_equalityI less_eq_mctxtI1 elim!: nth_equalityE elim: less_eq_mctxtE1)
apply (metis preorder_class.eq_refl)
done
qed
} note * = this
let ?C' = "fill_holes_mctxt C (map max_top (unfill_holes C t)) ⊓ max_top t"
have "C = max_top t ∨ C < ?C'"
using 2(2-3) max_topC_props[of "mctxt_of_term t", unfolded topsC_def] by (intro *) (auto)
moreover
have leq: "C ≤ ?C'" using 2(3) max_topC_props[of "mctxt_of_term t", unfolded topsC_def]
by (auto intro!: fill_holes_mctxt_suffix)
have "C ≤ mctxt_of_term t" using `C ≤ max_top t` max_topC_props[of "mctxt_of_term t", unfolded topsC_def]
by auto
have "?C' ≤ mctxt_of_term t" using max_topC_props[of "mctxt_of_term t", unfolded topsC_def]
by (auto intro: inf.coboundedI2)
{
fix i assume *: "i < num_holes C" define p where "p = hole_poss' C ! i"
have "p ∈ all_poss_mctxt C"
using * set_hole_poss'[of C] by (fastforce simp: all_poss_mctxt_conv p_def)
then have **: "p ∈ all_poss_mctxt ?C'" using `C ≤ ?C'` all_poss_mctxt_mono[of C "?C'"] by auto
have ***: "length (map max_top (unfill_holes C t)) = num_holes C" and
****: "length (unfill_holes C t) = num_holes C" using `C ≤ mctxt_of_term t` by auto
have *****: "subm_at ?C' p = max_top (subt_at t p) ⊓ subm_at (max_top t) p"
using inf_subm_at[OF **] * nth_map[of _ "unfill_holes C t"] **** `C ≤ mctxt_of_term t`
by (simp add: p_def subm_at_fill_holes_mctxt[OF ***]) (simp add: unfill_holes_conv)
have "p ∈ all_poss_mctxt (max_top t)" using `p ∈ all_poss_mctxt C` `C ≤ max_top t`
all_poss_mctxt_mono[of C "max_top t"] by auto
have urk: "p ∈ all_poss_mctxt (mreplace_at (max_top t) p (subm_at (max_top t) p ⊔ max_top (t |_ p)))"
using `p ∈ all_poss_mctxt (max_top t)` by (auto intro: all_poss_mctxt_mreplace_atI1)
have "subm_at ?C' p = MHole ∨ subm_at ?C' p = max_top (subt_at t p)"
proof (cases "p ∈ hole_poss (max_top t)")
case True thus ?thesis unfolding ***** by auto
next
case False
have pmt: "p ∈ poss_mctxt (max_top t)"
using `p ∈ all_poss_mctxt (max_top t)` False by (auto simp: all_poss_mctxt_conv)
have comp: "(subm_at (max_top t) p, max_top (subt_at t p)) ∈ comp_mctxt"
proof (intro prefix_comp_mctxt[of _ "mctxt_of_term (subt_at t p)"])
show "subm_at (max_top t) p ≤ mctxt_of_term (t |_ p)"
apply (subst subm_at_mctxt_of_term[symmetric])
using pmt max_topC_props[unfolded topsC_def] all_poss_mctxt_mono[of "max_top t" "mctxt_of_term t"]
apply (auto intro: less_eq_subm_at simp: all_poss_mctxt_conv)
done
qed (insert max_topC_props[unfolded topsC_def], auto)
then have "mreplace_at (max_top t) p (subm_at (max_top t) p ⊔ max_top (t |_ p)) ∈ 𝔏"
by (intro L⇩3') (insert max_topC_props[unfolded topsC_def] pmt, auto)
moreover have "mreplace_at (max_top t) p (subm_at (max_top t) p ⊔ max_top (t |_ p)) ≤ mctxt_of_term t"
using `p ∈ all_poss_mctxt (max_top t)` max_topC_props[unfolded topsC_def] all_poss_mctxt_mono[of "max_top t" "mctxt_of_term t"]
apply (intro mreplace_at_leqI)
subgoal by auto
subgoal by auto
subgoal apply (intro sup_mctxt_least[OF comp])
subgoal by (auto intro: less_eq_subm_at)
subgoal by (subst subm_at_mctxt_of_term[symmetric]) (auto simp: all_poss_mctxt_conv intro: less_eq_subm_at)
done
done
ultimately have "mreplace_at (max_top t) p (subm_at (max_top t) p ⊔ max_top (t |_ p)) ≤ max_top t"
using max_topC_props[unfolded topsC_def] by auto
from less_eq_subm_at[OF _ this, of p]
have "max_top (t |_ p) ⊓ subm_at (max_top t) p = max_top (t |_ p)"
unfolding subm_at_mreplace_at[OF `p ∈ all_poss_mctxt (max_top t)`] less_eq_mctxt_def[symmetric]
using sup_mctxt_ge2[OF comp] urk by simp
thus ?thesis unfolding ***** by simp
qed
} note x = this
{
fix i assume "i < num_holes C"
hence "hole_poss' C ! i ∈ hole_poss C" using set_hole_poss'[of C]
unfolding length_hole_poss'[symmetric] by force
hence "hole_poss' C ! i ∈ all_poss_mctxt C" by (auto simp: all_poss_mctxt_conv)
hence "hole_poss' C ! i ∈ poss t" using `C ≤ mctxt_of_term t`
all_poss_mctxt_mono[of C "mctxt_of_term t"] by (auto simp: all_poss_mctxt_conv)
hence "t |_ hole_poss' C ! i ∈ 𝒯" using `t ∈ 𝒯` by (simp add: 𝒯_subt_at)
} note y = this
have "max_list (map ?rank' (unfill_holes ?C' t)) ≤ max_list (map ?rank' (unfill_holes C t))"
unfolding unfill_holes_by_prefix[OF `C ≤ ?C'` `?C' ≤ mctxt_of_term t`] map_concat
using `C ≤ mctxt_of_term t`
apply (intro max_list_mono_concat1)
subgoal by auto
subgoal for i using x[of i] by (auto simp: unfill_holes_conv rank.simps y)
done
ultimately show ?case using spec[OF 2(1), of ?C'] 2(2) 2(3) by auto (auto simp: rank.simps)
qed
qed
lemma rank_by_top:
assumes "t ∈ 𝒯" and "L ≤ max_top t"
shows "rank t ≤ 1 + max_list (map rank (unfill_holes L t))"
proof -
have "max_list (map rank (filter is_Fun (unfill_holes L t))) ≤ max_list (map rank (unfill_holes L t))"
by (auto intro!: max_list_mono)
then show ?thesis using rank_by_top'[OF assms] by simp
qed
end
text ‹Layered TRSs are also weakly layered.›
sublocale layered ⊆ weakly_layered
by (unfold_locales) (fact trs, fact ℛ_sig, metis C⇩1 max_topC_layer mhole_layer)
text ‹@{cite ‹Lemma 3.9› FMZvO15}›
lemma (in weakly_layered) 𝔏_closed_under_ℛ:
assumes "L ∈ 𝔏" and "(L, N) ∈ mrstep ℛ" shows "N ∈ 𝔏"
proof -
let ?f = "λt. holes_to_var (term_mctxt_conv t)" and ?sf = "case_option (Var undefined) Var"
have sf: "?f t = t ⋅ ?sf" for t by (induct t rule: term_mctxt_conv.induct) auto
let ?g = "λt. mctxt_term_conv (vars_to_holes' (term_mctxt_conv t))" and ?sg = "λx. Var None"
have sg: "?g t = t ⋅ ?sg" for t by (induct t rule: term_mctxt_conv.induct) auto
let ?h = "λt. mctxt_term_conv (vars_to_holes' (mctxt_of_term t))" and ?sh = "λx. Var None"
have sh: "?h t = t ⋅ ?sh" for t by (induct t) auto
have "(?f (mctxt_term_conv L), ?f (mctxt_term_conv N)) ∈ rstep' ℛ"
using assms(2) by (auto simp only: sf rstep'_stable mrstep.simps)
then obtain r p σ where 2: "(?f (mctxt_term_conv L), ?f (mctxt_term_conv N)) ∈ rstep_r_p_s' ℛ r p σ"
by (auto simp: rstep'_iff_rstep_r_p_s')
then obtain C where "?f (mctxt_term_conv L) = C⟨fst r ⋅ σ⟩" "p = hole_pos C" "r ∈ ℛ"
using 2 by (auto simp: rstep_r_p_s'.simps)
then have **: "p ∈ funposs_mctxt L" unfolding funposs_mctxt_def
proof (induct C arbitrary: p L)
case Hole thus ?case using trs by (cases r; cases L; force simp: wf_trs_def)
next
case (More f ss1 C ss2) thus ?case by (cases L) (auto elim: nth_equalityE)
qed
have fL: "funas_term (mctxt_term_conv L) ⊆ ℱ" using assms(1) 𝔏_sig by (auto simp: 𝒯_def 𝒞_def)
from rstep'_preserves_funas_terms[OF ℛ_sig this] trs assms(2)[unfolded mrstep.simps]
have fN: "funas_term (mctxt_term_conv N) ⊆ ℱ" by blast
have "L ∈ tops (?f (mctxt_term_conv L))" using assms(1) by (simp add: topsC_def)
then have Mbounds: "L ≤ max_top (?f (mctxt_term_conv L))"
"max_top (?f (mctxt_term_conv L)) ≤ mctxt_of_term (?f (mctxt_term_conv L))"
using max_topC_props by (auto simp: topsC_def)
with ** have 1: "p ∈ funposs_mctxt (max_top (?f (mctxt_term_conv L)))" by (simp add: funposs_mctxt_mono)
have "holes_to_var L ∈ 𝒯" "holes_to_var N ∈ 𝒯" using fL fN by (auto simp: 𝒯_def)
then obtain D τ where "D ∈ 𝔏" "(mctxt_term_conv (max_top (?f (mctxt_term_conv L))), mctxt_term_conv D) ∈ rstep_r_p_s' ℛ r p τ"
using W[OF _ _ 1 2] by auto
then have "(?g (mctxt_term_conv (max_top (?f (mctxt_term_conv L)))), ?g (mctxt_term_conv D)) ∈ rstep_r_p_s' ℛ r p (τ ∘⇩s ?sg)"
unfolding sg by (auto simp: rstep_r_p_s'.simps)
moreover have "?g (mctxt_term_conv (max_top (?f (mctxt_term_conv L)))) = ?g (mctxt_term_conv L)"
using vars_to_holes'_mono[OF Mbounds(1)] vars_to_holes'_mono[OF Mbounds(2)] by simp
ultimately have 3: "(mctxt_term_conv (vars_to_holes L), mctxt_term_conv (vars_to_holes' D)) ∈ rstep_r_p_s' ℛ r p (τ ∘⇩s ?sg)"
by simp
have "(?h (holes_to_var (term_mctxt_conv (mctxt_term_conv L))), ?h (holes_to_var (term_mctxt_conv (mctxt_term_conv N)))) ∈ rstep_r_p_s' ℛ r p (σ ∘⇩s ?sh)"
using 2 unfolding sh by (auto simp: rstep_r_p_s'.simps)
then have 4: "(mctxt_term_conv (vars_to_holes L), mctxt_term_conv (vars_to_holes' N)) ∈ rstep_r_p_s' ℛ r p (σ ∘⇩s ?sh)"
by simp
show ?thesis using arg_cong[OF rstep_r_p_s'_deterministic[OF trs 3 4], of term_mctxt_conv] `D ∈ 𝔏`
vars_to_holes_layer[of D] vars_to_holes_layer[of N] by simp
qed
lemma fresh_variables_for_holes:
fixes C :: "('f, 'v :: infinite) mctxt"
obtains xs where "num_holes C = length xs" "distinct xs" "set xs ∩ vars_mctxt C = {}"
using infinite_UNIV infinite_imp_many_elems[of "UNIV - vars_mctxt C" "num_holes C"]
sym[of "length _" "num_holes C"] by auto
lemma represent_context_by_term:
fixes C :: "('f, 'v :: infinite) mctxt"
obtains c σ where
"c ⋅ σ = mctxt_term_conv C" "⋀x. σ x ∈ {Var (Some x), Var None}"
"⋀D. C ≤ D ⟹ ∃τ. c ⋅ τ = mctxt_term_conv D ∧ (∀x. σ x = Var None ∨ τ x = Var (Some x))"
proof -
obtain xs where *: "num_holes C = length xs" "distinct xs" "set xs ∩ vars_mctxt C = {}"
using fresh_variables_for_holes .
define X where "X = set xs"
let ?c = "fill_holes C (map Var xs)"
let ?σ = "λx. if x ∈ set xs then Var None else Var (Some x)"
from *(1,3) have "?c ⋅ ?σ = mctxt_term_conv C"
unfolding X_def[symmetric] using equalityD2[OF X_def]
proof (induct C xs rule: fill_holes_induct)
case (MFun f Cs xs)
have "i < length Cs ⟹ X ∩ vars_mctxt (Cs ! i) = {}" for i using MFun(3) by fastforce
moreover have "i < length Cs ⟹ set (partition_holes xs Cs ! i) ⊆ X" for i using MFun(4) by fastforce
ultimately show ?case using MFun(1,2) by (auto simp: comp_def map_nth_eq_conv)
qed auto
moreover have "?σ x ∈ {Var (Some x), Var None}" for x by simp
moreover from * have "C ≤ D ⟹ ∃τ. ?c ⋅ τ = mctxt_term_conv D ∧ (∀x. x ∈ set xs ∧ ?σ x = Var None ∨ τ x = Var (Some x))" for D
proof (induct C xs arbitrary: D rule: fill_holes_induct)
case (MHole x) thus ?case by (intro exI[of _ "(Var ∘ Some) (x := mctxt_term_conv D)"]) auto
next
case (MVar x) thus ?case by (intro exI[of _ "Var ∘ Some"]) (auto elim: less_eq_mctxtE1)
next
case (MFun f Cs xs)
from MFun(3) obtain Ds where [simp]: "D = MFun f Ds" "length Ds = length Cs"
and **: "⋀i. i < length Cs ⟹ Cs ! i ≤ Ds ! i"
by (metis less_eq_mctxtE1(2))
have x: "i < length Cs ⟹ mset (partition_holes xs Cs ! i) ⊆# mset (concat (partition_holes xs Cs))" for i
using nth_mem_mset[of i "partition_holes xs Cs"]
by (auto simp: mset_concat_union in_mset_subset_Union)
have distinct: "i < length Cs ⟹ distinct (partition_holes xs Cs ! i)" for i using x MFun(4)
by (auto simp: distinct_count_atmost_1' mset_concat_union) (meson dual_order.trans subseteq_mset_def)
moreover have "i < length Cs ⟹ set (partition_holes xs Cs ! i) ∩ vars_mctxt (MFun f Cs) = {}" for i
using x MFun(5) nth_mem[of i "partition_holes xs Cs"] by (auto simp del: nth_mem)
then have disjoint: "i < length Cs ⟹ set (partition_holes xs Cs ! i) ∩ vars_mctxt (Cs ! i) = {}" for i
using nth_mem[of i "Cs"] by (auto simp del: nth_mem)
ultimately have "i < length Cs ⟹
∃τ. fill_holes (Cs ! i) (map Var (partition_holes xs Cs ! i)) ⋅ τ = mctxt_term_conv (Ds ! i) ∧
(∀x. x ∈ set (partition_holes xs Cs ! i) ∨ τ x = Var (Some x))" for i
using MFun(2)[OF _ **] by meson
then obtain τs where τs: "⋀i. i < length Cs ⟹
fill_holes (Cs ! i) (map Var (partition_holes xs Cs ! i)) ⋅ τs i = mctxt_term_conv (Ds ! i) ∧
(∀x. x ∈ set (partition_holes xs Cs ! i) ∨ τs i x = Var (Some x))" by metis
define τ where "τ ≡ λx. (if x ∈ set xs then τs (THE i. i < length Cs ∧ x ∈ set (partition_holes xs Cs ! i)) x else Var (Some x))"
have "i < length Cs ⟹ ∀x. x ∈ vars_mctxt (Cs ! i) ⟶ τ x = Var (Some x)" for i
using set_mset_mono[OF x[of i]] MFun(1,5) nth_mem[of i "Cs"] by (auto simp: τ_def simp del: nth_mem)
note [simp] = subst_apply_mctxt_cong[OF this]
have "i < length Cs ⟹ ∀x. x ∈ vars_mctxt (Cs ! i) ⟶ τs i x = Var (Some x)" for i
using set_mset_mono[OF x[of i]] MFun(1,5) nth_mem[of i "Cs"] τs by (auto simp del: nth_mem)
note [simp] = subst_apply_mctxt_cong[OF this]
have "i < length Cs ⟹ x ∈ set (partition_holes xs Cs ! i) ⟹
(THE i. i < length Cs ∧ x ∈ set (partition_holes xs Cs ! i)) = i" for i x
using MFun(4) by (intro the_equality) (auto simp: distinct_concat_unique_index)
then have "i < length Cs ⟹ x ∈ set (partition_holes xs Cs ! i) ⟹ τ x = τs i x" for i x
using set_mset_mono[OF x[of i]] MFun(1) by (auto simp add: τ_def)
then have [simp]: "i < length Cs ⟹ partition_holes (map ((λti. ti ⋅ τ) ∘ Var) xs) Cs ! i =
partition_holes (map ((λti. ti ⋅ τs i) ∘ Var) xs) Cs ! i" for i
unfolding map_map_partition_by[symmetric] nth_map[of _ "partition_holes xs Cs", unfolded length_map length_partition_by]
by (intro map_cong) (auto simp: τ_def)
from MFun(1,3,4,5) τs show ?case
by (intro exI[of _ τ] conjI)
(auto simp: distinct disjoint subst_apply_mctxt_fill_holes intro!: nth_equalityI, auto simp: τ_def)
qed
then have "C ≤ D ⟹ ∃τ. ?c ⋅ τ = mctxt_term_conv D ∧ (∀x. ?σ x = Var None ∨ τ x = Var (Some x))" for D
by blast
ultimately show ?thesis ..
qed
text ‹@{cite ‹Lemma 3.10› FMZvO15}›
lemma matched_mctxt_to_term:
fixes C :: "('f, 'v :: infinite) mctxt" and l :: "('f, 'w) term"
assumes "p ∈ all_poss_mctxt C" "l ⋅ σ = mctxt_term_conv (subm_at C p)"
obtains c :: "('f, 'v) term" and ρ ρ' where "mctxt_term_conv C = c ⋅ ρ" "⋀x. x ∈ vars_term c ⟹ is_Var (ρ x)"
"p ∈ poss c" "l ⋅ ρ' = subt_at c p"
"⋀D τ. C ≤ D ⟹ l ⋅ τ = mctxt_term_conv (subm_at D p) ⟹
∃τ'. (c ⋅ τ' = mctxt_term_conv D)"
proof -
obtain w_to_v :: "'w ⇒ 'v" where *: "inj_on w_to_v (vars_term l)"
using inj_on_iff_card_le[of "vars_term l"] infinite_arbitrarily_large[OF infinite_UNIV, of "card (vars_term l)"]
by fastforce
have [simp]: "l ⋅ (Var ∘ w_to_v) ⋅ (σ ∘ inv_into (vars_term l) w_to_v) = l ⋅ σ" for σ using *
by (auto simp del: subst_subst_compose simp: subst_subst subst_compose_def term_subst_eq_conv)
let ?l = l and ?σ = σ
define σ where "σ = ?σ ∘ inv_into (vars_term l) w_to_v"
define l where "l = ?l ⋅ (Var ∘ w_to_v)"
have assms: "p ∈ all_poss_mctxt C" "l ⋅ σ = mctxt_term_conv (subm_at C p)"
using assms by (auto simp: l_def σ_def)
from represent_context_by_term[of C]
obtain c0 τ where 1: "c0 ⋅ τ = mctxt_term_conv C" "⋀x. τ x ∈ {Var (Some x), Var None}"
"⋀D. C ≤ D ⟹ ∃τ'. c0 ⋅ τ' = mctxt_term_conv D ∧ (∀x. τ x = Var None ∨ τ' x = Var (Some x))" by blast
from 1(1,2) have p: "poss c0 = all_poss_mctxt C"
proof (induct c0 arbitrary: C)
case (Var x) show ?case using Var(2)[of x] Var(1) by (cases C) auto
next
case (Fun f cs) thus ?case by (cases C) (auto simp: map_eq_conv')
qed
from term_fs.rename_avoiding[unfolded supp_vars_term_eq, OF finite_vars_term]
obtain π l' where 2: "l' = π ∙ l" "vars_term c0 ∩ vars_term l' = {}" by (metis term_apply_subst_Var_Rep_perm)
have l_sop: "l' = l ⋅ sop π" using 2(1) by simp
let ?d = "replace_at c0 p l'" and ?ρ = "λx . if x ∈ vars_term l' then (σ ∘ Rep_perm (- π)) x else τ x"
have C1: "mctxt_term_conv C = c0 ⋅ ?ρ"
unfolding 1(1)[symmetric] using 2(2) by (intro term_subst_eq) auto
have l': "l' ⋅ ?ρ = l ⋅ σ" unfolding 2(1) permute_term_subst_apply_term using 2(2) Rep_perm_image[of "π" "vars_term l"]
by (intro term_subst_eq) (auto simp: 2(1) eqvt fun_cong[OF Rep_perm_add[unfolded o_def, symmetric]] Rep_perm_0 image_def)
have C2: "mctxt_term_conv C = replace_at c0 p l' ⋅ ?ρ" unfolding 1(1)[symmetric]
using cong[OF refl ctxt_supt_id[OF assms(1)[unfolded p[symmetric]]], of "λx. x ⋅ ?ρ", symmetric]
by (auto simp: l' assms(2) 1(1) C1[symmetric] subt_at_mctxt_term_conv[OF assms(1)]
subt_at_subst[symmetric, OF assms(1)[unfolded p[symmetric]]])
have "c0 ⋅ ?ρ ∘⇩s (Var ∘ from_option) = ?d ⋅ ?ρ ∘⇩s (Var ∘ from_option)" using C2 by (auto simp: unifiers_def C1)
note m = is_imgu_imp_is_mgu[OF the_mgu_is_imgu[OF this]] and t = the_mgu[OF this] and i = the_mgu_is_imgu[OF this]
let ?μ = "the_mgu c0 ?d"
let ?c = "c0 ⋅ ?μ"
from arg_cong[OF arg_cong[OF conjunct2[OF t,symmetric], of "λσ. c0 ⋅ σ", folded subst_subst, folded C1], of "λt. t ⋅ (Var ∘ to_option)"]
have ***: "mctxt_term_conv C = ?c ⋅ ?ρ"
by (simp del: subst_subst_compose add: subst_subst subst_compose_def)
moreover {
fix x assume "x ∈ vars_term ?c"
then obtain z where "z ∈ vars_term c0" "x ∈ vars_term (?μ z)" by (auto simp: vars_term_subst)
then have "is_Var (?ρ x)"
using bspec[OF 1(1)[unfolded *** subst_subst term_subst_eq_conv], of z] 1(2)[of z]
by (cases "the_mgu c0 (ctxt_of_pos_term p c0)⟨l'⟩ z", auto simp: subst_compose_def)
}
moreover have "p ∈ poss ?c" using assms(1)[folded p] by simp
moreover have "p ∈ poss ?d" using assms(1)[folded p] by (simp add: replace_at_below_poss)
then have "l ⋅ (sop π ∘⇩s ?μ) = subt_at ?c p" using l_sop[symmetric] assms(1)[folded p]
by (simp only: conjunct1[OF t] subt_at_subst replace_at_subt_at) simp
then have "?l ⋅ ((sop π ∘⇩s ?μ) ∘ w_to_v) = subt_at ?c p"
by (auto simp del: subst_subst_compose simp: subst_subst subst_compose_def comp_def l_def)
moreover {
fix D τ'' assume assms': "C ≤ D" "?l ⋅ τ'' = mctxt_term_conv (subm_at D p)"
define τ' where "τ' = τ'' ∘ inv_into (vars_term ?l) w_to_v"
have assms': "C ≤ D" "l ⋅ τ' = mctxt_term_conv (subm_at D p)"
using assms' by (auto simp: l_def τ'_def)
from assms(1) assms'(1) have pp: "p ∈ all_poss_mctxt D" using all_poss_mctxt_mono by auto
from 1(3)[OF assms'(1)] obtain τ'' where 4: "c0 ⋅ τ'' = mctxt_term_conv D"
"⋀x. τ x = Var None ∨ τ'' x = Var (Some x)" by blast
let ?τ = "λx . if x ∈ vars_term l' then (τ' ∘ Rep_perm (- π)) x else τ'' x"
have D1: "mctxt_term_conv D = c0 ⋅ ?τ"
unfolding 4(1)[symmetric] using 2(2) by (intro term_subst_eq) auto
have l': "l' ⋅ ?τ = l ⋅ τ'" unfolding 2(1) permute_term_subst_apply_term using 2(2) Rep_perm_image[of "π" "vars_term l"]
by (intro term_subst_eq) (auto simp: 2(1) eqvt fun_cong[OF Rep_perm_add[unfolded o_def, symmetric]] Rep_perm_0 image_def)
have D2: "mctxt_term_conv D = replace_at c0 p l' ⋅ ?τ" unfolding 4(1)[symmetric]
using cong[OF refl ctxt_supt_id[OF assms(1)[unfolded p[symmetric]]], of "λx. x ⋅ ?τ", symmetric]
by (auto simp: l' assms'(2) 4 D1[symmetric] subt_at_mctxt_term_conv[OF pp]
subt_at_subst[symmetric, OF assms(1)[unfolded p[symmetric]]])
note * = trans[OF sym[OF D1] D2]
obtain τ2 where foo: "?τ ∘⇩s (Var ∘ from_option) = ?μ ∘⇩s τ2"
using cong[OF refl *, of "λt. t ⋅ (Var ∘ from_option)"] unfolding subst_subst by (blast dest: the_mgu)
have bibi: "(Var ∘ from_option) ∘⇩s (Var ∘ to_option) = (Var :: 'v option ⇒ ('f,'v option) term)"
by (auto simp: subst_compose_def)
then have "c0 ⋅ ?τ = c0 ⋅ ?τ ⋅ (Var ∘ from_option) ∘⇩s (Var ∘ to_option)" by simp
then have "?c ⋅ τ2 ∘⇩s (Var ∘ to_option) = mctxt_term_conv D" by (metis D1 foo subst_subst)
then have "∃τ'. ?c ⋅ τ' = mctxt_term_conv D" by blast
}
ultimately show ?thesis ..
qed
lemma alien_set_by_substitution:
fixes c :: "('f, 'v) term" and C :: "('f, 'v) mctxt"
assumes "mctxt_term_conv C = c ⋅ ρ" "⋀x. x ∈ vars_term c ⟹ is_Var (ρ x)"
"num_holes C = length ts" "fill_holes C ts = c ⋅ τ"
shows "set ts = { τ x |x. x ∈ vars_term c ∧ ρ x = Var None }"
using assms(3,1,2,4)
proof (induct C ts arbitrary: c rule: fill_holes_induct)
case (MHole t) thus ?case by (cases c) auto
next
case (MVar x) thus ?case by (cases c) auto
next
case (MFun f Cs ts)
obtain cs where x[simp]: "length Cs = length cs" "c = Fun f cs"
using MFun(3,4) by (cases c) (auto, metis length_map)
have "i < length cs ⟹ set (partition_holes ts Cs ! i) = {τ x |x. x ∈ vars_term (cs ! i) ∧ ρ x = Var None}" for i
using MFun(1,3-) by (intro MFun(2)) (auto simp: map_eq_conv' set_conv_nth)
then show ?case unfolding set_concat unfolding x term.set(4)
by (subst set_conv_nth)+ (simp, blast)
qed
lemma alien_map_by_substitution:
fixes c :: "('f, 'v) term" and C :: "('f, 'v) mctxt"
assumes "mctxt_term_conv C = c ⋅ ρ" "⋀x. x ∈ vars_term c ⟹ is_Var (ρ x)"
"num_holes C = length ts" "fill_holes C ts = c ⋅ τ"
shows "fill_holes C (map f ts) = c ⋅ (λx. if ρ x = Var None then f (τ x) else τ x)"
using assms(3,1,2,4)
proof (induct C ts arbitrary: c rule: fill_holes_induct)
case (MHole t) thus ?case by (cases c) auto
next
case (MVar x) thus ?case by (cases c) auto
next
case (MFun g Cs ts)
obtain cs where x[simp]: "length Cs = length cs" "c = Fun g cs"
using MFun(3,4) by (cases c) (auto, metis length_map)
have "i < length cs ⟹ fill_holes (Cs ! i) (partition_holes (map f ts) Cs ! i) =
cs ! i ⋅ (λx. if ρ x = Var None then f (τ x) else τ x)" for i
using MFun(1,2,3,5) MFun(4)[unfolded x term.set, OF UN_I, of "cs ! i"] by (auto elim!: nth_equalityE)
then show ?case using MFun(1) by (auto intro!: nth_equalityI)
qed
lemma leq_mctxt_subst:
shows "term_mctxt_conv (c ⋅ ρ) ≤ term_mctxt_conv (c ⋅ τ) ⟷
(∀x. x ∈ vars_term c ⟶ term_mctxt_conv (ρ x) ≤ term_mctxt_conv (τ x))"
by (induct c) (auto elim!: less_eq_mctxtE1 intro!: less_eq_mctxtI1 simp: set_conv_nth, blast+)
lemma leq_mctxt_vars_term_subst:
assumes "vars_term d ⊆ vars_term c" "term_mctxt_conv (c ⋅ ρ) ≤ term_mctxt_conv (c ⋅ τ)"
shows "term_mctxt_conv (d ⋅ ρ) ≤ term_mctxt_conv (d ⋅ τ)"
using assms unfolding leq_mctxt_subst by blast
text ‹@{cite ‹Lemma 3.11› FMZvO15}›
lemma rewrite_aliens:
fixes C :: "('f, 'v :: infinite) mctxt" and l :: "('f, 'w) term"
assumes "wf_trs R" "(mctxt_term_conv C, mctxt_term_conv D) ∈ rstep_r_p_s' R (l, r) p σ"
"num_holes C = length ss" "l ⋅ τ = subt_at (fill_holes C ss) p"
obtains ts where "num_holes D = length ts"
"(fill_holes C ss, fill_holes D ts) ∈ rstep_r_p_s' R (l, r) p τ" "set ts ⊆ set ss"
"⋀f. ∃τ'. (fill_holes C (map f ss), fill_holes D (map f ts)) ∈ rstep_r_p_s' R (l, r) p τ'"
proof -
from assms(2) obtain E where 1: "mctxt_term_conv C = E⟨l ⋅ σ⟩" "mctxt_term_conv D = E⟨r ⋅ σ⟩"
"p = hole_pos E" "(l, r) ∈ R" by (induct rule: rstep_r_p_s'.induct) simp
from 1(4) assms(1) have rl: "vars_term r ⊆ vars_term l" by (auto simp: wf_trs_def)
from 1(3) arg_cong[OF 1(1), of term_mctxt_conv] have 2: "p ∈ all_poss_mctxt C" "l ⋅ σ = mctxt_term_conv (subm_at C p)"
using subt_at_mctxt_term_conv[of p C, symmetric] by auto
from matched_mctxt_to_term[OF this] obtain c :: "('f, 'v) term" and ρ ρ' where
3: "mctxt_term_conv C = c ⋅ ρ" "⋀x. x ∈ vars_term c ⟹ is_Var (ρ x)" "p ∈ poss c" "l ⋅ ρ' = c |_ p"
"⋀D τ. C ≤ D ⟹ l ⋅ τ = mctxt_term_conv (subm_at D p) ⟹ ∃τ'. c ⋅ τ' = mctxt_term_conv D"
by metis
let ?s = "mctxt_of_term (fill_holes C ss)" and ?τ = "τ ∘⇩s (Var ∘ Some)"
have 4: "C ≤ ?s" "l ⋅ ?τ = mctxt_term_conv (subm_at ?s p)" "p ∈ all_poss_mctxt ?s"
using assms(3,4) 2(1) subt_at_mctxt_term_conv[of p ?s, symmetric] subsetD[OF all_poss_mctxt_mono[of C ?s]]
subt_at_subst[of p "fill_holes C ss" "Var ∘ Some"] all_poss_mctxt_mctxt_of_term[of "fill_holes C ss", symmetric]
by (auto simp del: subt_at_subst all_poss_mctxt_mctxt_of_term)
from 3(5)[OF this(1,2)] obtain τ' where 5: "c ⋅ τ' = mctxt_term_conv ?s" by blast
let ?d = "replace_at c p (r ⋅ ρ')"
have 6: "(c, ?d) ∈ rstep_r_p_s' R (l, r) p ρ'"
using 1(4) 3(3,4) by (auto intro!: rstep_r_p_s'I simp: ctxt_supt_id)
from rstep_r_p_s'_deterministic[OF assms(1,2) rstep_r_p_s'_stable[OF this, of ρ, folded 3(1)]]
have 7: "mctxt_term_conv D = ?d ⋅ ρ" .
obtain d where 8: "(fill_holes C ss, d) ∈ rstep_r_p_s' R (l,r) p τ"
using rstep_r_p_s'I[OF 1(4) _ refl refl, of p "ctxt_of_pos_term p (fill_holes C ss)" τ] assms(4) 4(3)
by (simp add: ctxt_supt_id)
have "fill_holes C ss ⋅ (Var ∘ Some) ⋅ (Var ∘ the) = fill_holes C ss" unfolding subst_subst subst_compose_def by simp
note rstep_r_p_s'_stable[OF 6, of "τ' ∘⇩s (Var ∘ the)", unfolded subst_subst_compose 5 mctxt_term_conv_mctxt_of_term this]
from rstep_r_p_s'_deterministic[OF assms(1) this 8] assms(4) 8
have 9: "(fill_holes C ss, ?d ⋅ (τ' ∘⇩s (Var ∘ the))) ∈ rstep_r_p_s' R (l, r) p τ" by simp
have A: "vars_term ?d ⊆ vars_term c"
using arg_cong[OF ctxt_supt_id[OF 3(3), folded 3(4)], of vars_term, symmetric] assms(1) 1(4)
by (auto simp add: vars_term_ctxt_apply wf_trs_def vars_term_subst) blast
from leq_mctxt_vars_term_subst[OF this, of ρ τ'] have B: "D ≤ term_mctxt_conv (?d ⋅ τ')"
using arg_cong[OF 7, of "term_mctxt_conv"]
arg_cong[OF 3(1), of "λC. term_mctxt_conv C"] 4(1) arg_cong[OF 5, of "λC. term_mctxt_conv C"]
arg_cong[OF mctxt_term_conv_mctxt_of_term, of "λC. term_mctxt_conv C"]
by (simp del: subst_apply_term_ctxt_apply_distrib mctxt_term_conv_mctxt_of_term)
have X: "fill_holes C ss = c ⋅ τ' ∘⇩s (Var ∘ the)" using 5
by (simp only: mctxt_term_conv_mctxt_of_term subst_subst_compose) (simp del: subst_subst_compose add: subst_subst subst_compose_def)
have "(ctxt_of_pos_term p c)⟨r ⋅ ρ'⟩ ⋅ τ' = mctxt_term_conv (mctxt_of_term ((ctxt_of_pos_term p c)⟨r ⋅ ρ'⟩ ⋅ τ' ∘⇩s (Var ∘ the)))"
using 5 A unfolding mctxt_term_conv_mctxt_of_term subst_subst X term_subst_eq_conv by blast
from arg_cong[OF this, of term_mctxt_conv] have "D ≤ mctxt_of_term (?d ⋅ τ' ∘⇩s (Var ∘ the))" using B
by (simp only: term_mctxt_conv_inv)
note U = length_unfill_holes[OF this, symmetric] fill_unfill_holes[OF this]
let ?ts = "unfill_holes D (?d ⋅ τ' ∘⇩s (Var ∘ the))"
have W: "set ?ts ⊆ set ss"
using A alien_set_by_substitution[OF 3(1,2) assms(3) X] alien_set_by_substitution[OF 7 3(2) U] by blast
have Z: "(fill_holes C ss, fill_holes D ?ts) ∈ rstep_r_p_s' R (l, r) p τ" using 9 unfolding U .
{ fix f
let ?τ = "λx. if ρ x = Var None then f ((τ' ∘⇩s (Var ∘ the)) x) else (τ' ∘⇩s (Var ∘ the)) x"
have "term_mctxt_conv t ≤ mctxt_of_term (t ⋅ (Var ∘ the))" for t :: "('f, 'v option) term"
by (induct t; (case_tac "x :: _ option")?) (auto intro: less_eq_mctxtI1)
from this[of "?d ⋅ τ'"]
have "D ≤ mctxt_of_term (ctxt_of_pos_term p c ⋅⇩c τ' ⋅⇩c (Var ∘ the))⟨r ⋅ ρ' ⋅ τ' ⋅ (Var ∘ the)⟩"
using B by auto
then have "(fill_holes C (map f ss), fill_holes D (map f ?ts)) ∈ rstep_r_p_s' R (l, r) p (ρ' ∘⇩s ?τ)"
apply (subst alien_map_by_substitution[OF 3(1) 3(2) assms(3) X], simp)
apply (subst alien_map_by_substitution[OF 7, of _ "τ' ∘⇩s (Var ∘ the)"])
using 3(2) rstep'_sub_vars[OF r_into_rtrancl assms(1), of c ?d] 6 rstep_r_p_s'_stable[OF 6]
by (auto simp: fill_unfill_holes rstep'_iff_rstep_r_p_s')
}
with that[OF U(1) Z W] show ?thesis by blast
qed
lemma rewrite_aliens_mctxt:
fixes C :: "('f, 'v :: infinite) mctxt" and l :: "('f, 'w) term"
assumes "wf_trs R" "(mctxt_term_conv C, mctxt_term_conv D) ∈ rstep_r_p_s' R (l, r) p σ"
"num_holes C = length Cs" "l ⋅ τ = subt_at (mctxt_term_conv (fill_holes_mctxt C Cs)) p"
obtains Ds where "num_holes D = length Ds"
"(mctxt_term_conv (fill_holes_mctxt C Cs), mctxt_term_conv (fill_holes_mctxt D Ds)) ∈ rstep_r_p_s' R (l, r) p τ"
"set Ds ⊆ set Cs"
proof -
have [simp]: "mctxt_term_conv C ⋅ (Var ∘ case_option None (Some ∘ Some)) = mctxt_term_conv (map_vars_mctxt Some C)"
for C by (induct C) auto
obtain ts where
"num_holes (map_vars_mctxt Some D) = length ts"
"(fill_holes (map_vars_mctxt Some C) (map mctxt_term_conv Cs), fill_holes (map_vars_mctxt Some D) ts) ∈ rstep_r_p_s' R (l, r) p τ"
"set ts ⊆ set (map mctxt_term_conv Cs)"
using assms rstep_r_p_s'_stable[OF assms(2), of "Var ∘ case_option None (Some ∘ Some)"]
by (auto intro: rewrite_aliens[of R "map_vars_mctxt Some C" "map_vars_mctxt Some D" l r p
"σ ∘⇩s (Var ∘ case_option None (Some ∘ Some))" "map mctxt_term_conv Cs" τ] simp: mctxt_term_conv_fill_holes_mctxt)
then have "num_holes D = length (map term_mctxt_conv ts)"
"(mctxt_term_conv (fill_holes_mctxt C Cs), mctxt_term_conv (fill_holes_mctxt D (map term_mctxt_conv ts))) ∈ rstep_r_p_s' R (l, r) p τ"
"set (map term_mctxt_conv ts) ⊆ set Cs" using assms(3)
by (auto simp: mctxt_term_conv_fill_holes_mctxt comp_def)
then show ?thesis ..
qed
lemma match_balanced_aliens:
fixes C :: "('f, 'v :: infinite) mctxt" and l :: "('f, 'w) term"
assumes "p ∈ all_poss_mctxt C"
"l ⋅ σ = mctxt_term_conv (subm_at C p)"
"l ⋅ τ = subt_at (fill_holes C ss) p" "ss ∝ ts" "num_holes C = length ss"
obtains (τ') τ' where "l ⋅ τ' = subt_at (fill_holes C ts) p"
using assms
proof (induct p arbitrary: C ss ts thesis)
case Empty
have [simp]: "s ⋅ (λx. Var (Some x)) = t ⋅ (λx. Var (Some x)) ⟷ s = t" for s t
by (induct s arbitrary: t; case_tac t)
(auto intro: list.inj_map_strong[of _ _ "λt. t ⋅ (λx. Var (Some x))" "λt. t ⋅ (λx. Var (Some x))"])
obtain c :: "('f,'v) term" and ρ ρ' where ρ: "mctxt_term_conv C = c ⋅ ρ"
"⋀x. x ∈ vars_term c ⟹ is_Var (ρ x)" "ε ∈ poss c" "l ⋅ ρ' = c |_ ε" and
*: "⋀D τ. C ≤ D ⟹ l ⋅ τ = mctxt_term_conv (subm_at D ε) ⟹ ∃τ'. c ⋅ τ' = mctxt_term_conv D"
using matched_mctxt_to_term[OF Empty(2,3)] by blast
from *[of "mctxt_of_term (fill_holes C ss)" "τ ∘⇩s (Var ∘ Some)"] Empty(2,4,6)
obtain σ' where σ': "c ⋅ σ' = fill_holes C ss ⋅ (Var ∘ Some)" by auto
define s2t where "s2t = (λs. ts ! (SOME i. i < length ss ∧ ss ! i ⋅ (Var ∘ Some) = s))"
let ?τ' = "(λx. if ρ x = Var None then s2t (σ' x) else σ' x ⋅ (Var ∘ the))"
define ts' where "ts' = ts" define ss' where "ss' = ss"
have "num_holes C = length ts" "num_holes C = length ss" using Empty(5,6) by (auto simp: refines_def)
moreover have "set (zip ts ss) ⊆ set (zip ts' ss')" by (auto simp: ts'_def ss'_def)
ultimately have "l ⋅ ρ' ∘⇩s (λx. if ρ x = Var None then s2t (σ' x) else σ' x ⋅ (Var ∘ the)) = fill_holes C ts"
using σ' ρ(1,2)
unfolding subst_subst_compose ρ(4) subt_at.simps
proof (induct C ts ss arbitrary: c rule: fill_holes_induct2)
case (MHole x y)
obtain i where [simp]: "x = ts ! i" "y = ss ! i" "i < length ss" "i < length ts"
using MHole(1) by (auto simp: ss'_def ts'_def in_set_conv_nth)
from this(3,4) have "ts ! (SOME j. j < length ss ∧ ss ! j = ss ! i) = ts ! i"
using Empty(5) someI[of "λj. j < length ss ∧ ss ! j = ss ! i" i] by (auto simp: refines_def)
then show ?case
using MHole(2,3) by (cases c, auto simp: s2t_def comp_def)
next
case (MVar v) then show ?case by (cases c) auto
next
case (MFun f Cs xs ys)
then show ?case
proof (cases c)
case (Fun g cs) note [simp] = Fun
have [simp]: "i < length Cs ⟹ x ∈ vars_term (cs ! i) ⟹ is_Var (ρ x)" for i x
using MFun(6,7) by (auto) (metis length_map nth_mem)
{ fix i x y assume *: "i < length Cs" "(x, y) ∈ set (zip (partition_holes xs Cs ! i) (partition_holes ys Cs ! i))"
have [simp]: "zip (partition_holes xs Cs ! i) (partition_holes ys Cs ! i) = partition_holes (zip xs ys) Cs ! i"
"sum_list (map num_holes Cs) = length (zip xs ys)"
using *(1) MFun(1,2) by (auto simp: partition_by_of_zip)
from UN_set_partition_by[of "map num_holes Cs" "zip xs ys" "λx. {x}"] * have "(x, y) ∈ set (zip xs ys)"
by force
then have "(x, y) ∈ set (zip ts' ss')" using MFun(1,2,4) by auto
} note [simp] = this
show ?thesis using MFun(1-2,4-) by (auto 0 0 simp: map_eq_conv' intro!: MFun(3))
qed auto
qed
then show ?case by (auto intro: Empty(1)[of "ρ' ∘⇩s ?τ'"])
next
case (PCons i p)
obtain f Cs where [simp]: "C = MFun f Cs" using PCons(3) by (cases C) simp_all
let ?ss = "partition_holes ss Cs ! i" and ?ts = "partition_holes ts Cs ! i"
from PCons(3-) obtain τ' where "l ⋅ τ' = fill_holes (Cs ! i) ?ts |_ p"
proof (subst PCons(1)[of "Cs ! i" ?ts thesis ?ss], goal_cases)
case 5 show ?case using PCons(3,6) by (auto simp: partition_by_nth intro: refines_take refines_drop)
qed auto
then show ?case using PCons(2)[of τ'] PCons(3) by simp
qed
text ‹@{cite ‹Lemma 4.14› FMZvO15}›
lemma rewrite_balanced_aliens:
fixes C :: "('f, 'v :: infinite) mctxt" and l :: "('f, 'w) term"
assumes "wf_trs R" "(mctxt_term_conv C, mctxt_term_conv D) ∈ rstep_r_p_s' R (l, r) p σ"
"num_holes C = length ss" "l ⋅ τ = subt_at (fill_holes C ss) p" "ss ∝ ts"
obtains (ts') ts' τ' where "num_holes D = length ts'"
"(fill_holes C ts, fill_holes D ts') ∈ rstep_r_p_s' R (l, r) p τ'" "set ts' ⊆ set ts"
proof -
have "p ∈ all_poss_mctxt C" "l ⋅ σ = mctxt_term_conv (subm_at C p)" using
assms(2) by (auto simp del: poss_mctxt_term_conv simp: poss_mctxt_term_conv[symmetric] subt_at_mctxt_term_conv[symmetric])
from match_balanced_aliens[OF this assms(4,5,3)]
obtain τ' where "l ⋅ τ' = fill_holes C ts |_ p" by metis
from rewrite_aliens[OF assms(1-2) assms(3)[folded iffD1[OF refines_def, OF assms(5), THEN conjunct1]] this]
obtain ts' where "num_holes D = length ts'" "set ts' ⊆ set ts"
"(fill_holes C ts, fill_holes D ts') ∈ rstep_r_p_s' R (l, r) p τ'" by metis
then show ?thesis using ts'[of ts' τ'] by simp
qed
lemma rewrite_balanced_aliens':
fixes C :: "('f, 'v :: infinite) mctxt" and l :: "('f, 'w) term"
assumes "wf_trs R" "length ss = num_holes C" "length ts = num_holes D"
"(fill_holes C ss, fill_holes D ts) ∈ rstep_r_p_s' R (l, r) p σ"
"(mctxt_term_conv C, mctxt_term_conv D) ∈ rstep_r_p_s' R (l, r) p τ"
obtains σ' where "(fill_holes C (map f ss), fill_holes D (map f ts)) ∈ rstep_r_p_s' R (l, r) p σ'"
proof -
have p: "p ∈ all_poss_mctxt C" using wf_trs_implies_funposs[OF assms(1,5)]
funposs_imp_poss poss_mctxt_term_conv by blast
then have "l ⋅ σ = fill_holes C ss |_ p" using assms(4) by auto
from rewrite_aliens[OF assms(1,5) assms(2)[symmetric] this]
obtain ts' where ts': "num_holes D = length ts'"
"(fill_holes C ss, fill_holes D ts') ∈ rstep_r_p_s' R (l, r) p σ"
"⋀f. ∃τ'. (fill_holes C (map f ss), fill_holes D (map f ts')) ∈ rstep_r_p_s' R (l, r) p τ'"
by metis
have [simp]: "ts' = ts" using ts'(1) assms(3) rstep_r_p_s'_deterministic[OF assms(1,4) ts'(2)]
by (auto simp: fill_holes_inj)
show ?thesis using that ts'(3) by auto
qed
lemma rewrite_cases:
assumes "num_holes C = length ss" "(fill_holes C ss, t) ∈ rstep_r_p_s' ℛ (l, r) p σ"
obtains (outer) "p ∈ poss_mctxt C" "(fill_holes C ss, t) ∈ rstep_r_p_s' ℛ (l, r) p σ"
| (inner) i ti where "i < length ss" "t = fill_holes C (ss[i := ti])"
"(ss ! i, ti) ∈ rstep_r_p_s' ℛ (l, r) (pos_diff p (hole_poss' C ! i)) σ"
"hole_poss' C ! i ≤ p"
using assms
proof (induct C ss arbitrary: p t thesis rule: fill_holes_induct)
case (MVar x)
have "p ∈ poss_mctxt (MVar x)" using MVar by (elim rstep_r_p_s'E, case_tac C) auto
thus ?case using MVar by auto
next
case (MFun f Cs ss) show ?case
proof (cases p)
case Empty thus ?thesis using MFun(1,5) by (intro MFun(3)) auto
next
case (PCons i q)
obtain g ts ti where
*: "fill_holes (MFun f Cs) (concat (partition_holes ss Cs)) = Fun g ts" "i < length ts"
"t = Fun g (ts[i := ti])" "(ts ! i, ti) ∈ rstep_r_p_s' ℛ (l, r) q σ" by (metis rstep_r_p_s'_argE[OF MFun(5)[unfolded PCons]])
then have [simp]: "g = f" "length ts = length Cs" "ts ! i = fill_holes (Cs ! i) (partition_holes ss Cs ! i)"
using MFun(1) by auto
note * = *[unfolded this]
consider "q ∈ poss_mctxt (Cs ! i)"
"(fill_holes (Cs ! i) (partition_holes ss Cs ! i), ti) ∈ rstep_r_p_s' ℛ (l, r) q σ"
| j tj where "j < length (partition_holes ss Cs ! i)" "ti = fill_holes (Cs ! i) ((partition_holes ss Cs ! i)[j := tj])"
"(partition_holes ss Cs ! i ! j, tj) ∈ rstep_r_p_s' ℛ (l, r) (pos_diff q (hole_poss' (Cs ! i) ! j)) σ"
"hole_poss' (Cs ! i) ! j ≤ q"
using MFun(2)[OF *(2) _ _ *(4)] by metis
then show ?thesis
proof cases
case 1 thus ?thesis using *(2) MFun(5) by (intro MFun(3)) (simp_all add: PCons *)
next
case 2 let ?k = "sum_list (take i (map num_holes Cs)) + j"
have k: "?k < length ss" using MFun(1) *(2) 2(1)
concat_nth_length[of i "partition_holes ss Cs" j] by (auto simp: take_map[symmetric])
show ?thesis
proof (intro MFun(4)[of ?k tj])
show "?k < length (concat (partition_holes ss Cs))" using k MFun(1) by auto
next
have [simp]: "partition_holes (concat (partition_holes ss Cs[i := (partition_holes ss Cs ! i)[j := tj]])) Cs =
partition_holes ss Cs[i := (partition_holes ss Cs ! i)[j := tj]]" using MFun(1)
proof (intro partition_holes_concat_id)
fix k assume "sum_list (map num_holes Cs) = length ss" "k < length Cs"
thus "num_holes (Cs ! k) = length (partition_holes ss Cs[i := (partition_holes ss Cs ! i)[j := tj]] ! k)"
using MFun(1) by (cases "i = k") auto
qed simp
have "k < length Cs ⟹ ts[i := ti] ! k = fill_holes (Cs ! k) (partition_holes (ss[?k := tj]) Cs ! k)" for k
using *(1,2) list_update_concat[of i "partition_holes ss Cs" j tj, symmetric] 2 MFun(1)
by (subst nth_list_update) auto
then show "t = fill_holes (MFun f Cs) (concat (partition_holes ss Cs)[?k := tj])"
unfolding * using *(2) k MFun(1) by (auto intro!: nth_equalityI)
next
have "hole_poss' (MFun f Cs) ! (sum_list (take i (map num_holes Cs)) + j) = i <# hole_poss' (Cs ! i) ! j"
using concat_nth[of i "map (λi. map (op <# i) (hole_poss' (Cs ! i))) [0..<length Cs]" j ?k]
MFun(1) *(2) 2(1) by (auto simp: take_map[symmetric] comp_def map_upt_len_conv)
thus "(concat (partition_holes ss Cs) ! ?k, tj) ∈ rstep_r_p_s' ℛ (l, r) (pos_diff p (hole_poss' (MFun f Cs) ! ?k)) σ"
"hole_poss' (MFun f Cs) ! (sum_list (take i (map num_holes Cs)) + j) ≤ p"
using MFun(1) 2(3,4) concat_nth[of i "partition_holes ss Cs" j ?k] *(2) 2(1)
by (auto simp: PCons take_map[symmetric])
qed
qed
qed
qed auto
lemma rewrite_cases_mctxt:
assumes "num_holes C = length Cs" "(mctxt_term_conv (fill_holes_mctxt C Cs), mctxt_term_conv D) ∈ rstep_r_p_s' ℛ (l, r) p σ"
obtains (outer) "p ∈ poss_mctxt C" "(mctxt_term_conv (fill_holes_mctxt C Cs), mctxt_term_conv D) ∈ rstep_r_p_s' ℛ (l, r) p σ"
| (inner) i Ci where "i < length Cs" "D = fill_holes_mctxt C (Cs[i := Ci])"
"(mctxt_term_conv (Cs ! i), mctxt_term_conv Ci) ∈ rstep_r_p_s' ℛ (l, r) (pos_diff p (hole_poss' C ! i)) σ"
proof -
from assms rewrite_cases[of "map_vars_mctxt Some C" "map mctxt_term_conv Cs" "mctxt_term_conv D" ℛ l r p σ]
consider
(outer') "p ∈ poss_mctxt C"
"(fill_holes (map_vars_mctxt Some C) (map mctxt_term_conv Cs), mctxt_term_conv D) ∈ rstep_r_p_s' ℛ (l, r) p σ"
| (inner') i ti where "i < length Cs"
"mctxt_term_conv D = fill_holes (map_vars_mctxt Some C) (map mctxt_term_conv Cs[i := ti])"
"(map mctxt_term_conv Cs ! i, ti) ∈ rstep_r_p_s' ℛ (l, r) (pos_diff p (hole_poss' (map_vars_mctxt Some C) ! i)) σ"
by (simp add: mctxt_term_conv_fill_holes_mctxt) metis
then show thesis
proof cases
case outer'
moreover have "(mctxt_term_conv (fill_holes_mctxt C Cs), mctxt_term_conv D) ∈ rstep_r_p_s' ℛ (l, r) p σ"
using outer'(2) assms(1) by (simp add: mctxt_term_conv_fill_holes_mctxt)
ultimately show ?thesis by (intro outer)
next
case (inner' i ti)
moreover have "D = fill_holes_mctxt C (Cs[i := term_mctxt_conv ti])"
using arg_cong[OF inner'(2), of "term_mctxt_conv"] assms(1)
mctxt_term_conv_fill_holes_mctxt[of C "Cs[i := term_mctxt_conv ti]", symmetric]
by (simp add: map_update)
moreover have "(mctxt_term_conv (Cs ! i), mctxt_term_conv (term_mctxt_conv ti)) ∈ rstep_r_p_s' ℛ (l, r) (pos_diff p (hole_poss' C ! i)) σ"
using inner'(1,3) by simp
ultimately show ?thesis by (intro inner)
qed
qed
lemma rewrite_cases_wf:
assumes "wf_trs ℛ" "num_holes C = length ss" "(fill_holes C ss, t) ∈ rstep_r_p_s' ℛ (l, r) p σ"
obtains (outer) "p ∈ funposs_mctxt C" "(fill_holes C ss, t) ∈ rstep_r_p_s' ℛ (l, r) p σ"
| (inner) i ti where "i < length ss" "t = fill_holes C (ss[i := ti])"
"(ss ! i, ti) ∈ rstep_r_p_s' ℛ (l, r) (pos_diff p (hole_poss' C ! i)) σ"
"hole_poss' C ! i ≤ p"
proof -
consider (outer') "p ∈ poss_mctxt C" "(fill_holes C ss, t) ∈ rstep_r_p_s' ℛ (l, r) p σ"
| (inner') i ti where "i < length ss" "t = fill_holes C (ss[i := ti])"
"(ss ! i, ti) ∈ rstep_r_p_s' ℛ (l, r) (pos_diff p (hole_poss' C ! i)) σ"
"hole_poss' C ! i ≤ p"
using assms rewrite_cases by blast
then show ?thesis
proof (cases)
case outer' show ?thesis
proof (cases rule: outer)
case 1 show ?case using assms(2) outer'(1) wf_trs_implies_funposs[OF `wf_trs ℛ` outer'(2)]
by (induct C ss arbitrary: p rule: fill_holes_induct) (auto simp: funposs_mctxt_def)
qed fact
qed fact
qed
lemma rewrite_cases_mctxt_wf:
assumes "wf_trs ℛ" "num_holes C = length Cs" "(mctxt_term_conv (fill_holes_mctxt C Cs), mctxt_term_conv D) ∈ rstep_r_p_s' ℛ (l, r) p σ"
obtains (outer) "p ∈ funposs_mctxt C" "(mctxt_term_conv (fill_holes_mctxt C Cs), mctxt_term_conv D) ∈ rstep_r_p_s' ℛ (l, r) p σ"
| (inner) i Ci where "i < length Cs" "D = fill_holes_mctxt C (Cs[i := Ci])"
"(mctxt_term_conv (Cs ! i), mctxt_term_conv Ci) ∈ rstep_r_p_s' ℛ (l, r) (pos_diff p (hole_poss' C ! i)) σ"
proof -
consider (outer') "p ∈ poss_mctxt C" "(mctxt_term_conv (fill_holes_mctxt C Cs), mctxt_term_conv D) ∈ rstep_r_p_s' ℛ (l, r) p σ"
| (inner') i Ci where "i < length Cs" "D = fill_holes_mctxt C (Cs[i := Ci])"
"(mctxt_term_conv (Cs ! i), mctxt_term_conv Ci) ∈ rstep_r_p_s' ℛ (l, r) (pos_diff p (hole_poss' C ! i)) σ"
using assms rewrite_cases_mctxt by blast
then show ?thesis
proof (cases)
case outer' show ?thesis
proof (cases rule: outer)
case 1 show ?case using assms(2) outer'(1) wf_trs_implies_funposs[OF `wf_trs ℛ` outer'(2)]
by (induct C Cs arbitrary: p rule: fill_holes_induct) (auto simp: funposs_mctxt_def)
qed fact
qed fact
qed
lemma (in weakly_layered) 𝒯_preservation:
assumes "s ∈ 𝒯" "(s, t) ∈ rstep' ℛ" shows "t ∈ 𝒯"
using assms ℛ_sig trs rstep_preserves_funas_terms unfolding rstep_eq_rstep'[symmetric] 𝒯_def by blast
lemma (in weakly_layered) W':
assumes "s ∈ 𝒯" "p ∈ funposs_mctxt (max_top s)" "(s, t) ∈ rstep_r_p_s' ℛ r p σ"
shows "∃D τ. D ∈ 𝔏 ∧ (mctxt_term_conv (max_top s), mctxt_term_conv D) ∈ rstep_r_p_s' ℛ r p τ"
by (metis assms W rstep'_iff_rstep_r_p_s' 𝒯_preservation surjective_pairing)
text ‹@{cite ‹Lemma 3.12› FMZvO15}›
lemma (in weakly_layered) rank_preservation:
assumes "s ∈ 𝒯" "(s, t) ∈ rstep' ℛ" shows "rank t ≤ rank s"
using assms
proof (induct s arbitrary: t rule: rank.induct)
case (1 s)
note t = 𝒯_preservation[OF 1(2,3)]
from 1(3) obtain l r p σ where rs: "(s, t) ∈ rstep_r_p_s' ℛ (l, r) p σ" unfolding rstep'_iff_rstep_r_p_s' by blast
have ms: "max_top s ≤ mctxt_of_term s" using max_topC_props(1) by (simp add: topsC_def)
let ?ss = "aliens s"
note ms' = length_unfill_holes[OF ms] fill_unfill_holes[OF ms]
from 1(3) obtain l r p σ where rs: "(s, t) ∈ rstep_r_p_s' ℛ (l, r) p σ" unfolding rstep'_iff_rstep_r_p_s' by blast
then have "(fill_holes (max_top s) ?ss, t) ∈ rstep_r_p_s' ℛ (l, r) p σ" unfolding ms' .
from ms'(1)[symmetric] this show ?case
proof (cases rule: rewrite_cases)
case outer
then obtain C where *: "p ∈ poss s" "p = hole_pos C" "s = C⟨l ⋅ σ⟩" "t = C⟨r ⋅ σ⟩" "(l, r) ∈ ℛ"
by (auto elim: rstep_r_p_s'E simp: ms')
have "p ∈ funposs s" using *(2,3,5) trs hole_pos_in_filled_funposs[of "l ⋅ σ" C Var] by (force simp: wf_trs_def)
then have p: "p ∈ funposs_mctxt (max_top s)" using outer *(1) funposs_mctxt_compat[OF ms] by auto
from W[OF `s ∈ 𝒯` `t ∈ 𝒯` p rs] obtain D τ where w: "D ∈ 𝔏"
"(mctxt_term_conv (max_top s), mctxt_term_conv D) ∈ rstep_r_p_s' ℛ (l, r) p τ" by blast
from rewrite_aliens[OF trs w(2) length_unfill_holes[OF ms, symmetric], unfolded fill_unfill_holes[OF ms], of σ]
obtain ts where ts: "num_holes D = length ts" "set ts ⊆ set ?ss"
"(s, fill_holes D ts) ∈ rstep_r_p_s' ℛ (l, r) p σ" using *(2,3) by (metis subt_at_hole_pos)
have t': "t = fill_holes D ts" using rstep_r_p_s'_deterministic[OF trs rs ts(3)] .
then have ts': "ts = unfill_holes D t" using unfill_fill_holes[OF ts(1)[symmetric]] by simp
have D: "D ≤ max_top (fill_holes D ts)" using fill_holes_suffix[OF ts(1)] w(1) topsC_def max_topC_props(2) by blast
have "max_list (map rank ts) ≤ max_list (map rank ?ss)" using ts(2)
by (intro max_list_mono) auto
then show ?thesis using rank_by_top[OF `t ∈ 𝒯` D[folded t']] ts(2)
using outer trs `s ∈ 𝒯` unfolding ts'[symmetric] by (subst (2) rank.simps) auto
next
case (inner i ti)
then have "rank ti ≤ rank (?ss ! i)"
using funas_term_fill_holes_iff[OF ms'(1)[symmetric], unfolded ms'] 1(2)
by (intro 1) (force simp: rstep'_iff_rstep_r_p_s' 𝒯_def)+
then have 3: "max_list (map rank (?ss[i := ti])) ≤ max_list (map rank ?ss)"
unfolding map_update upd_conv_take_nth_drop[of i "map rank ?ss" "rank ti", unfolded length_map, OF inner(1)]
apply (subst (3) id_take_nth_drop[of i "map rank ?ss", unfolded length_map, OF inner(1)])
unfolding max_list_append max_list.simps nth_map[OF inner(1)] by linarith
have 4: "max_top s ≤ max_top t" using inner(2) fill_holes_suffix[OF ms'(1)[symmetric], unfolded ms']
by (auto simp: topsC_def)
have [simp]: "unfill_holes (max_top s) (fill_holes (max_top s) (unfill_holes (max_top s) s[i := ti])) =
unfill_holes (max_top s) s[i := ti]" by (intro unfill_fill_holes) (auto simp: ms')
show ?thesis using 3 rank_by_top[OF `t ∈ 𝒯` 4] inner(2) 1(2) by (subst (2) rank.simps) (auto simp: ms')
qed
qed
lemma (in layer_system) max_top_mono1:
assumes "𝔏' ⊆ 𝔏"
and "max_topC C ∈ 𝔏'"
shows "layer_system_sig.max_topC 𝔏' C = max_topC C"
proof -
let ?topsC' = "layer_system_sig.topsC 𝔏'"
have 1: "⋀L. L ∈ ?topsC' C ⟹ L ∈ topsC C"
"⋀L. L ∈ topsC C ⟹ L ∈ 𝔏' ⟹ L ∈ ?topsC' C" using assms(1)
unfolding layer_system_sig.topsC_def by blast+
moreover {
fix M assume *: "M ∈ ?topsC' C" "⋀L. L ∈ ?topsC' C ⟹ L ≤ M"
have "M = max_topC C"
using *(1) *(2)[of "max_topC C"] 1(2)[OF _ assms(2)] max_topC_props(2)[OF 1(1), of M] by auto
}
ultimately show ?thesis using assms(2)
unfolding layer_system_sig.max_topC_def[of "𝔏'"]
by (intro the1_equality ex1I[of _ "max_topC C"]) auto
qed
lemma (in layer_system) ls_change_vars:
"layer_system ℱ {L. vars_to_holes L ∈ 𝔏}"
proof (standard, goal_cases 𝔏_sig' L⇩1' L⇩2' L⇩3')
case 𝔏_sig' show ?case using 𝔏_sig
apply (auto simp: layer_system_sig.𝒞_def) using funas_term_vars_to_holes by blast
next
case (L⇩1' t) show ?case
proof (cases t)
case (Var x) then show ?thesis by (auto intro: exI[of _ "MVar x"])
next
case (Fun f ts)
have *: "vars_to_holes (mctxt_of_term (map_vars_term f t)) = vars_to_holes (mctxt_of_term t)" for f t
by (induct t) auto
have **: "L ≤ mctxt_of_term (map_vars_term f t) ⟹ vars_to_holes L ≤ mctxt_of_term t" for L f t
using order.trans[OF vars_to_holes_mono[of L "mctxt_of_term (map_vars_term f t)", unfolded *]
vars_to_holes_prefix[of "mctxt_of_term t"]] .
obtain L where "L ∈ 𝔏" "L ≤ mctxt_of_term (map_vars_term undefined t)" "L ≠ MHole"
using L⇩1[of "map_vars_term undefined t"] L⇩1' by auto
with Fun show ?thesis
by (intro bexI[of _ "vars_to_holes L"], cases L)
(auto elim: less_eq_mctxtE1(1) elim!: less_eq_mctxtE1(2) intro!: less_eq_mctxtI2(3) ** simp: vars_to_holes_layer)
qed
next
case (L⇩2' p C x)
then have [simp]: "vars_to_holes (mreplace_at C p (MVar x)) = vars_to_holes (mreplace_at C p (MHole))"
by (induct C p rule: subm_at.induct) auto
show ?case by auto
next
case (L⇩3' L N p) then show ?case using L⇩3[of "vars_to_holes L" "vars_to_holes N" p]
vars_to_holes_comp_mctxt[OF L⇩3'(4)] by (auto simp: subsetD[OF funposs_mctxt_subset_poss_mctxt])
qed
context layer_system
begin
lemma 𝔏_by_vars_to_holes:
"{L. vars_to_holes L ∈ 𝔏} = 𝔏"
by (auto simp: vars_to_holes_layer)
interpretation ls_change_vars: layer_system where ℱ = ℱ and 𝔏 = "{L. vars_to_holes L ∈ 𝔏}"
by (rule ls_change_vars)
lemma max_top_var_subst_change_vars:
"ls_change_vars.max_top (t ⋅ (Var ∘ f)) = map_vars_mctxt f (max_top t)"
using max_topC_props(1)[of "mctxt_of_term t"] max_topC_props(2)[of _ "mctxt_of_term t"]
by (intro ls_change_vars.max_topCI) (auto simp: ls_change_vars.topsC_def topsC_def mctxt_of_term_var_subst
vars_to_holes_layer intro: map_vars_mctxt_mono elim!: map_vars_mctxt_less_eq_decomp)
lemma rank_change_vars:
"ls_change_vars.rank (t ⋅ (Var ∘ f)) = rank t"
proof (induct t rule: rank.induct)
case (1 t) then show ?case
using ls_change_vars.rank.simps[of "t ⋅ (Var ∘ f)"] rank.simps[of t] unfill_holes_var_subst[OF max_top_prefix, of f t]
by (auto simp: max_top_var_subst_change_vars[unfolded comp_def] comp_def 𝒯_def ls_change_vars.𝒯_def funas_term_subst intro!: arg_cong[of _ _ max_list] intro!: nth_equalityI)
qed
end
context layer_system
begin
interpretation ls_change_vars: layer_system where ℱ = ℱ and 𝔏 = "{L. vars_to_holes L ∈ 𝔏}"
by (rule ls_change_vars)
lemma rank_change_vars': "ls_change_vars.rank t = rank (t ⋅ (Var ∘ f))"
using ls_change_vars.rank_change_vars[of t f] 𝔏_by_vars_to_holes by auto
lemmas rank_by_top_change_vars = ls_change_vars.rank_by_top
end
end