section ‹Persistence of confluence›
theory LS_Persistence
imports LS_General
begin
text ‹Here we instantiate the layer framework for persistence of confluence.
See @{cite ‹Section 5.5› FMZvO15}.›
locale many_sorted_terms =
fixes sigF :: "('f × nat) ⇒ ('t list × 't) option" and sigV :: "'v ⇒ 't option"
assumes arity: "sigF (f, n) = Some (tys, tr) ⟹ length tys = n"
begin
definition ℱ where "ℱ = { fn . sigF fn ≠ None }"
definition 𝒱 where "𝒱 = { v . sigV v ≠ None }"
inductive 𝒯⇩α :: "'t ⇒ ('f, 'v) term ⇒ bool" where
var [intro]: "sigV x = Some α ⟹ 𝒯⇩α α (Var x)"
| funs [intro]: "sigF (f, length ts) = Some (tys, α) ⟹
(∀ i < length ts. 𝒯⇩α (tys ! i) (ts ! i)) ⟹ 𝒯⇩α α (Fun f ts)"
lemma funas_𝒯⇩α:
assumes "𝒯⇩α α t" "fn ∈ funas_term t"
shows "fn ∈ ℱ"
using assms
proof (induction t)
case (funs f ts tys α)
hence "fn ∈ {(f, length ts)} ⟶ fn ∈ ℱ" using ℱ_def by blast
moreover have "fn ∈ ⋃set (map funas_term ts) ⟶ fn ∈ ℱ"
using funs(2) map_nth_eq_conv[OF length_map[of funas_term ts, symmetric]]
by auto (metis in_set_idx)
ultimately show ?thesis using funs(3) unfolding "funas_term.simps" by blast
qed auto
inductive needed_types :: "'t ⇒ 't ⇒ bool" where
base_type [intro]: "needed_types α α"
| sub_types [intro]: "sigF (f, n) = Some (tys, α) ⟹
ty ∈ set tys ⟹ needed_types α ty"
| trans [intro]: "needed_types α β ⟹ needed_types β γ ⟹ needed_types α γ"
end
locale persistent_cr = many_sorted_terms sigF sigV for
sigF :: "('f × nat) ⇒ ('t list × 't) option" and
sigV :: "'v :: infinite ⇒ 't option" +
fixes ℛ :: "('f, 'v :: infinite) trs"
assumes
wf: "wf_trs ℛ" and
R_def: "(l, r) ∈ ℛ ⟹ ∃α . 𝒯⇩α α l ∧ 𝒯⇩α α r"
begin
definition lhs_types :: "('f × nat) ⇒ 't list" where
"lhs_types ≡ λ fn. fst (the (sigF fn))"
fun rhs_type :: "('f, 'v) term ⇒ 't option" where
"rhs_type (Var x) = sigV x"
| "rhs_type (Fun f ts) = (let fn = (f, length ts) in
(if sigF fn = None then None else Some (snd (the (sigF fn)))))"
fun max_top_persistent :: "'t ⇒ ('f, 'v) term ⇒ ('f, 'v) mctxt" where
"max_top_persistent α (Var x) = MVar x"
| "max_top_persistent α (Fun f ts) = (if (∃tys. sigF (f, length ts) = Some (tys, α))
then MFun f (map (case_prod max_top_persistent) (zip (lhs_types (f, length ts)) ts))
else MHole)"
inductive max_top_persistent' :: "'t ⇒ ('f, 'v) term ⇒ ('f, 'v) mctxt ⇒ bool" where
"max_top_persistent' α (Var x) (MVar x)"
| "sigF (f, length ts) = Some (tys, α) ⟹ length ms = length ts ⟹
i < length ts ⟶ max_top_persistent' (tys ! i) (ts ! i) (ms ! i) ⟹ max_top_persistent' α (Fun f ts) (MFun f ms)"
| "sigF (f, length ts) = None ⟹ max_top_persistent' α (Fun f ts) MHole"
inductive 𝔏⇩α :: "'t ⇒ ('f, 'v) mctxt ⇒ bool" where
mhole [intro]: "𝔏⇩α α MHole"
| mvar [intro]: "𝔏⇩α α (MVar x)"
| mfun [intro]: "sigF (f, length Cs) = Some (tys, α) ⟹
(∀ i < length Cs. 𝔏⇩α (tys ! i) (Cs ! i)) ⟹ 𝔏⇩α α (MFun f Cs)"
definition 𝔏 :: "('f, 'v) mctxt set" where
"𝔏 ≡ { C. ∃α. 𝔏⇩α α C }"
abbreviation ℛ⇩α where "ℛ⇩α α ≡ { (l, r) ∈ ℛ . 𝒯⇩α α l ∧ 𝒯⇩α α r }"
abbreviation topsC_α where "topsC_α α ≡ layer_system_sig.topsC { L . 𝔏⇩α α L }"
abbreviation max_topC_α where "max_topC_α α ≡ layer_system_sig.max_topC { L . 𝔏⇩α α L }"
lemma ℛ⇩α_sub_ℛ: "ℛ⇩α α ⊆ ℛ"
using R_def by blast
lemma ℛ⇩α_Union_ℛ: "(⋃α. ℛ⇩α α) ⊆ ℛ"
using R_def by blast
lemma 𝒯⇩α_𝔏⇩α:
assumes "𝒯⇩α α t"
shows "𝔏⇩α α (mctxt_of_term t)"
using assms by (induction t) auto
lemma funas_𝔏:
assumes "L ∈ 𝔏"
shows "funas_mctxt L ⊆ ℱ"
proof -
obtain α where "𝔏⇩α α L" using assms 𝔏_def by auto
thus ?thesis using assms
proof (induction rule: 𝔏⇩α.induct)
case (mfun f Cs tys)
{
fix i
assume "i < length Cs"
hence "funas_mctxt (Cs ! i) ⊆ ℱ" using mfun 𝔏_def ‹i < length Cs› by blast
} note funas_subts = this
hence "(f, length Cs) ∈ ℱ" using mfun ℱ_def by simp
thus ?case using funas_mctxt.simps(1) funas_subts in_set_conv_nth[of _ Cs] by fastforce
qed auto
qed
lemma subm_at_sig:
fixes L :: "('f, 'v) mctxt" and p :: pos and ℱ :: "('f × nat) set"
assumes "funas_mctxt L ⊆ ℱ" and "p ∈ all_poss_mctxt L"
shows "funas_mctxt (subm_at L p) ⊆ ℱ"
using assms subt_at_imp_ctxt funas_term_ctxt_apply
unfolding funas_term_mctxt_term_conv[symmetric] subm_at_subt_at_conv[OF assms(2)]
mctxt_term_conv_inv poss_mctxt_term_conv[symmetric] by (metis le_sup_iff)
lemma fun_poss_subm_at:
assumes "p ∈ funposs_mctxt C"
shows "∃f Cs. subm_at C p = MFun f Cs"
using assms by (induction C arbitrary: p) (auto simp: funposs_mctxt_def)
lemma fun_poss_all_poss_mctxt:
assumes "p ∈ funposs_mctxt C"
shows "p ∈ all_poss_mctxt C"
using assms by (induction C arbitrary: p) (auto simp: funposs_mctxt_def)
lemma subm_at_fun:
assumes "i < length Cs"
shows "subm_at (MFun f Cs) <i> = Cs ! i" and "<i> ∈ all_poss_mctxt (MFun f Cs)"
using assms by auto
lemma funas_sub_mctxt:
fixes f :: 'f and Cs :: "('f, 'v) mctxt list"
assumes "funas_mctxt (MFun f Cs) ⊆ ℱ"
"i < length Cs"
shows "funas_mctxt (Cs ! i) ⊆ ℱ"
using assms subm_at_fun[of i Cs f] subm_at_sig[of "MFun f Cs" ℱ "<i>"] by simp
lemma funas_sup_mctxt:
fixes L N :: "('f, 'v) mctxt"
assumes cmp: "(L, N) ∈ comp_mctxt" and
funas_L: "funas_mctxt L ⊆ ℱ" and
funas_N: "funas_mctxt N ⊆ ℱ"
shows "funas_mctxt (L ⊔ N) ⊆ ℱ"
proof -
have "comp_mctxtp L N" using cmp by (auto simp: comp_mctxt_def)
thus ?thesis using funas_L funas_N
by (induction L N rule: comp_mctxtp.induct)
(auto simp: funas_sub_mctxt set_zip, blast)
qed
lemma consistent_𝔏⇩α:
assumes "𝔏⇩α α (MFun f Cs)"
shows "∃tys. sigF (f, length Cs) = Some (tys, α) ∧ (∀i < length Cs. 𝔏⇩α (tys ! i) (Cs ! i))"
using 𝔏⇩α.cases[OF assms]
by (metis (no_types, lifting) mctxt.distinct(3) mctxt.distinct(5) mctxt.inject(2))
lemma 𝔏⇩α_sup_mctxt:
fixes L N :: "('f, 'v) mctxt"
assumes cmp: "(L, N) ∈ comp_mctxt" and "𝔏⇩α α L" and "𝔏⇩α α N"
shows "𝔏⇩α α (L ⊔ N)"
proof -
have "comp_mctxtp L N" using cmp by (auto simp: comp_mctxt_def)
thus ?thesis using ‹𝔏⇩α α L› ‹𝔏⇩α α N›
proof (induction L N arbitrary: α rule: comp_mctxtp.induct)
case (MFun f f' Cs Cs')
then obtain tys where f_prop: "sigF (f, length Cs) = Some (tys, α)"
using consistent_𝔏⇩α by blast
let ?Cs = "map (λ(x, y). x ⊔ y) (zip Cs Cs')"
have lengths: "length ?Cs = length Cs" using ‹length Cs = length Cs'› by simp
hence f_Ds_prop: "sigF (f, length ?Cs) = Some (tys, α)" using f_prop by simp
{ fix i
assume "i < length Cs"
hence "𝔏⇩α (tys ! i) (Cs ! i ⊔ Cs' ! i)"
using MFun f_prop consistent_𝔏⇩α by (metis option.inject prod.inject)
}
thus ?case using MFun f_Ds_prop lengths set_zip[of Cs Cs'] by auto
qed auto
qed
lemma mreplace_at_𝔏⇩α:
assumes "𝔏⇩α α L" "𝔏⇩α β N" "p ∈ funposs_mctxt L"
"subm_at L p = MFun f Cs" "sigF (f, length Cs) = Some (tys, β)"
shows "𝔏⇩α α (mreplace_at L p N)"
using assms
proof (induction L p N arbitrary: α f Cs rule: mreplace_at.induct)
case (1 L N) thus ?case using consistent_𝔏⇩α subm_at.simps(1) by force
next
case (2 f' Cs' i p N)
have "i < length Cs'" using 2(4) funposs_mctxt_def by force
hence p_in_funposs: "p ∈ funposs_mctxt (Cs' ! i)" using 2(4) unfolding funposs_mctxt_def by simp
obtain tys' where f_props: "sigF (f', length Cs') = Some (tys', α)"
"∀j<length Cs'. 𝔏⇩α (tys' ! j) (Cs' ! j)"
"length Cs' = length tys'" "lhs_types (f', length Cs') = tys'"
using consistent_𝔏⇩α[OF 2(2)] arity lhs_types_def by fastforce
hence ith: "𝔏⇩α (tys' ! i) (Cs' ! i)" using ‹i < length Cs'› by force
let ?Cs'' = "take i Cs' @ mreplace_at (Cs' ! i) p N # drop (i + 1) Cs'"
have replace_ith: "𝔏⇩α (tys' ! i) (mreplace_at (Cs' ! i) p N)"
using 2(1)[OF ith 2(3) p_in_funposs _ 2(6)] 2(5) by fastforce
moreover have "length ?Cs'' = length Cs'"
using ‹i < length Cs'› by simp
moreover have "∀j<length ?Cs''. 𝔏⇩α (tys' ! j) (?Cs'' ! j)"
using f_props(2) replace_ith ‹i < length Cs'› ‹length ?Cs'' = length Cs'›
by (metis Suc_eq_plus1 nth_list_update_eq nth_list_update_neq upd_conv_take_nth_drop)
ultimately show ?case using f_props ‹i < length Cs'› consistent_𝔏⇩α[OF 2(2)] "𝔏⇩α.simps"
unfolding mreplace_at.simps by metis
qed (auto simp: funposs_mctxt_def consistent_𝔏⇩α)
lemma 𝔏_subm:
assumes "L ∈ 𝔏"
shows "p ∈ all_poss_mctxt L ⟹ subm_at L p ∈ 𝔏"
using assms
proof -
assume p_prop: "p ∈ all_poss_mctxt L"
thus ?thesis
proof (cases L)
case (MFun f Cs)
then obtain α where "𝔏⇩α α L" using assms 𝔏_def by blast
then obtain tys where f_prop: "sigF (f, length Cs) = Some (tys, α)" using consistent_𝔏⇩α MFun by blast
from ‹𝔏⇩α α L› p_prop show ?thesis using 𝔏_def
proof (induction "L :: ('f, 'v) mctxt" p arbitrary: α f Cs rule: subm_at.induct)
case (2 f' Cs' i p)
hence "∃β. 𝔏⇩α β (Cs' ! i)" using consistent_𝔏⇩α by (auto simp: funposs_mctxt_def) blast
thus ?case using 2 by (auto simp: funposs_mctxt_def)
qed (auto simp: funposs_mctxt_def)
qed (auto simp: 𝔏_def)
qed
lemma 𝔏_sub: "𝔏⇩α α (mctxt_of_term C⟨t⟩) ⟹ ∃β. 𝔏⇩α β (mctxt_of_term t)"
proof (induction C arbitrary: α)
case (More f ss1 C' ss2)
let ?ts = "map mctxt_of_term (ss1 @ C'⟨t⟩ # ss2)"
obtain tys where "sigF (f, length ?ts) = Some (tys, α)" using More(2) by (auto elim: 𝔏⇩α.cases)
with More(2) have "∀i<length ?ts. 𝔏⇩α (tys ! i) (?ts ! i)"
by (auto elim: 𝔏⇩α.cases)
hence "𝔏⇩α (tys ! length ss1) (?ts ! length ss1)"
by (metis length_map add_Suc_right length_Cons length_append less_add_Suc1)
thus ?case using More(1)
by (metis list.simps(9) length_map map_append nth_append_length)
qed auto
lemma leq_mctxt_𝔏⇩α_mono:
assumes "L ≤ N" "𝔏⇩α α L" "L = MFun f ts" "N ∈ 𝔏"
shows "𝔏⇩α α N"
proof -
obtain α' where "𝔏⇩α α' N" using assms(4) 𝔏_def by auto
moreover obtain ts' tys where props:
"N = MFun f ts'" "length ts' = length ts" "sigF (f, length ts) = Some (tys, α)"
using assms less_eq_mctxt_MFunE1 by (metis consistent_𝔏⇩α)
moreover have "α' = α" using props assms(2,3) ‹𝔏⇩α α' N› consistent_𝔏⇩α by force
ultimately show ?thesis using 𝔏_def by auto
qed
lemma mreplace_at_𝔏⇩α':
assumes "L ≤ N" "𝔏⇩α α L" "N ∈ 𝔏" "𝔏⇩α β (subm_at L p)" "𝔏⇩α β (subm_at N p)"
"p ∈ all_poss_mctxt L"
shows "L = MHole ∨ (∃x. L = MVar x) ∨ 𝔏⇩α α (mreplace_at L p (subm_at N p))"
using assms
proof (induction L N arbitrary: α β p rule: less_eq_mctxt_induct[consumes 0])
case (4 Cs Ds f)
then obtain tys where f_props: "sigF (f, length Cs) = Some (tys, α)"
"∀j<length Cs. 𝔏⇩α (tys ! j) (Cs ! j)"
"length Cs = length tys" "lhs_types (f, length Cs) = tys"
using consistent_𝔏⇩α[OF 4(5)] arity lhs_types_def by fastforce
have "𝔏⇩α α (MFun f Ds)" using leq_mctxt_𝔏⇩α_mono[OF 4(4) 4(5) _ 4(6), of f Cs] by simp
have Ds_props: "∀j<length Ds. 𝔏⇩α (tys ! j) (Ds ! j)"
using 4(1) f_props(1) consistent_𝔏⇩α[OF ‹𝔏⇩α α (MFun f Ds)›] by fastforce
from 4 have "𝔏⇩α α (mreplace_at (MFun f Cs) p (subm_at (MFun f Ds) p))"
proof (induction p)
case Empty thus ?case by simp (metis consistent_𝔏⇩α old.prod.inject option.sel)
next
case (PCons i p')
have "i < length Cs" using PCons(2,10) by simp
moreover have "Ds ! i ∈ 𝔏"
using ‹i < length Cs› PCons(2,7) 𝔏_def Ds_props mem_Collect_eq by auto
ultimately consider "Cs ! i = MHole ∨ (∃x. Cs ! i = MVar x)" |
"𝔏⇩α (tys ! i) (mreplace_at (Cs ! i) p' (subm_at (Ds ! i) p'))"
using PCons(4)[of i "tys ! i" β p'] PCons(2,3,8,9,10) f_props(2) by auto
thus ?case
proof (cases)
case 1
hence "p' = ε" using PCons(10) by auto
let ?Cs' = "take i Cs @ Ds ! i # drop (Suc i) Cs"
have "𝔏⇩α (tys ! i) (Ds ! i)" using Ds_props ‹i < length Cs› PCons(2) by simp
have length_Cs': "length ?Cs' = length Cs" using ‹i < length Cs› by simp
{ fix j
assume "j < length ?Cs'"
hence "𝔏⇩α (tys ! j) (?Cs' ! j)" using f_props(2,3) ‹𝔏⇩α (tys ! i) (Ds ! i)› ‹i < length Cs›
by (metis length_Cs' less_imp_le_nat nth_append_take nth_append_take_drop_is_nth_conv)
}
hence "𝔏⇩α α (MFun f ?Cs')" using f_props(1) 4(1) ‹i < length Cs› length_Cs'
by (metis 𝔏⇩α.simps)
thus ?thesis using ‹p' = ε› by simp
next
case 2
let ?Cs' = "take i Cs @ mreplace_at (Cs ! i) p' (subm_at (Ds ! i) p') # drop (Suc i) Cs"
have length_Cs': "length ?Cs' = length Cs" using ‹i < length Cs› by simp
{ fix j
assume "j < length ?Cs'"
hence "𝔏⇩α (tys ! j) (?Cs' ! j)" using f_props(2,3) 2 ‹i < length Cs›
by (metis length_Cs' less_imp_le_nat nth_append_take nth_append_take_drop_is_nth_conv)
}
hence "𝔏⇩α α (MFun f ?Cs')" using f_props(1) 4(1) ‹i < length Cs› length_Cs'
by (metis 𝔏⇩α.simps)
thus ?thesis by simp
qed
qed
thus ?case by blast
qed (auto simp: assms)
lemma mreplace_at_mhole:
assumes "p ∈ all_poss_mctxt C" and "D ≠ MHole"
shows "mreplace_at C p D ≠ MHole"
using assms
proof -
have "p ∈ all_poss_mctxt (mreplace_at C p D)"
by (simp add: all_poss_mctxt_mreplace_atI1 assms(1))
thus ?thesis using ‹D ≠ MHole› by force
qed
lemma persistent_layer_system: "layer_system ℱ 𝔏"
proof
show "𝔏 ⊆ layer_system_sig.𝒞 ℱ"
proof
fix C :: "('f, 'v) mctxt"
assume "C ∈ 𝔏"
thus "C ∈ layer_system_sig.𝒞 ℱ"
using funas_𝔏 layer_system_sig.𝒞_def by blast
qed
next
fix t :: "('f, 'v) term"
assume funas_t: "funas_term t ⊆ ℱ"
thus "∃L∈𝔏 . L ≠ MHole ∧ L ≤ mctxt_of_term t"
proof (cases t)
case (Fun f ts)
then obtain tys α where f_in_ℱ: "sigF (f, length ts) = Some (tys, α)"
using funas_t ℱ_def by fastforce
let ?top = "MFun f (replicate (List.length ts) MHole)"
have cond: "?top ≠ MHole ∧ ?top ≤ mctxt_of_term t"
using Fun by (auto simp: less_eq_mctxt_def o_def map_replicate_const)
have "?top ∈ 𝔏" using 𝔏_def f_in_ℱ by fastforce
thus ?thesis using cond by auto
qed (auto simp: 𝔏_def)
next
fix C :: "('f, 'v) mctxt" and p :: pos and x :: 'v
assume p_in_possC: "p ∈ poss_mctxt C"
{ fix α
have "𝔏⇩α α (mreplace_at C p (MVar x)) = 𝔏⇩α α (mreplace_at C p MHole)" using p_in_possC
proof (induction C p "MVar x :: ('f, 'v) mctxt" arbitrary: α rule: mreplace_at.induct)
case (2 f Cs i p)
hence p_in_poss_mctxt: "p ∈ poss_mctxt (Cs ! i)" "i < length Cs" by simp+
let ?Cs' = "take i Cs @ mreplace_at (Cs ! i) p (MVar x) # drop (Suc i) Cs"
let ?Cs'' = "take i Cs @ mreplace_at (Cs ! i) p MHole # drop (Suc i) Cs"
have lengths: "length ?Cs' = length Cs" "length ?Cs'' = length Cs"
using ‹i < length Cs› by simp+
hence length_Cs: "Suc (min (length Cs) i + (length Cs - Suc i)) = length Cs" by simp
thus ?case using 2(1)[OF p_in_poss_mctxt(1)] lengths
by (auto dest!: consistent_𝔏⇩α)
(metis lengths 𝔏⇩α.simps append_Cons_nth_not_middle nth_append_length)+
qed auto
}
thus "(mreplace_at C p (MVar x) ∈ 𝔏) = (mreplace_at C p MHole ∈ 𝔏)" using 𝔏_def by force
next
fix L N :: "('f, 'v) mctxt" and p :: pos
assume "L ∈ 𝔏" and "N ∈ 𝔏" and p_in_funposs: "p ∈ funposs_mctxt L" and
comp_context: "(subm_at L p, N) ∈ comp_mctxt"
obtain α where "𝔏⇩α α L" using ‹L ∈ 𝔏› 𝔏_def by auto
thus "mreplace_at L p (subm_at L p ⊔ N) ∈ 𝔏"
proof -
have L_p_in_ℱ: "funas_mctxt (subm_at L p) ⊆ ℱ"
using p_in_funposs subm_at_sig fun_poss_all_poss_mctxt funas_𝔏[OF ‹L ∈ 𝔏›] by blast
obtain f Cs where subm_L_p: "subm_at L p = MFun f Cs" "comp_mctxtp (MFun f Cs) N"
using ‹p ∈ funposs_mctxt L› fun_poss_subm_at comp_context
by (metis comp_mctxtp_comp_mctxt_eq)
then obtain β tys where root_in_ℱ⇩β: "𝔏⇩α β (MFun f Cs)" "sigF (f, length Cs) = Some (tys, β)"
using 𝔏_def L_p_in_ℱ consistent_𝔏⇩α
𝔏_subm[OF ‹L ∈ 𝔏› fun_poss_all_poss_mctxt[OF p_in_funposs]] by force
hence "𝔏⇩α β N"
proof (cases N)
case (MFun f' Cs')
hence "f' = f ∧ length Cs' = length Cs"
using subm_L_p comp_mctxtp.simps[of "subm_at L p" N] by auto
thus ?thesis using MFun root_in_ℱ⇩β 𝔏_def ‹N ∈ 𝔏› consistent_𝔏⇩α by force
qed auto
have "𝔏⇩α β (subm_at L p ⊔ N)"
using 𝔏⇩α_sup_mctxt[OF comp_context _ ‹𝔏⇩α β N›] root_in_ℱ⇩β subm_L_p by simp
have "𝔏⇩α α (mreplace_at L p (subm_at L p ⊔ N))"
using mreplace_at_𝔏⇩α[OF ‹𝔏⇩α α L› ‹𝔏⇩α β (subm_at L p ⊔ N)› p_in_funposs subm_L_p(1) root_in_ℱ⇩β(2)] .
thus ?thesis using 𝔏_def by auto
qed
qed
sublocale layer_system "ℱ" "𝔏" using persistent_layer_system .
context
begin
lemma max_top_persistent_in_layers: "𝔏⇩α α (max_top_persistent α t)"
proof (induction t rule: max_top_persistent.induct)
case (2 α f ts) thus ?case
proof (cases "max_top_persistent α (Fun f ts)")
case (MFun f' Cs)
then obtain tys where f_prop: "sigF (f, length ts) = Some (tys, α)" by fastforce
hence "f' = f" using MFun max_top_persistent.simps(2) mctxt.distinct(5) mctxt.inject(2) by simp
have lengths1: "length (zip (lhs_types (f, length ts)) ts) = length ts"
using arity f_prop lhs_types_def by auto
hence lengths: "length Cs = length ts"
"Cs = (map (case_prod max_top_persistent) (zip (lhs_types (f, length ts)) ts))"
using MFun max_top_persistent.simps(2) f_prop by auto
hence f'_prop: "sigF (f', length Cs) = Some (tys, α)" using MFun ‹f' = f› f_prop by simp
have tys_def: "lhs_types (f, length ts) = tys" using f_prop lhs_types_def by simp
{ fix i
assume "i < length Cs"
hence "(tys ! i, ts ! i) ∈ set (zip (lhs_types (f, length ts)) ts)" using tys_def
using in_set_conv_nth lengths1 lengths(1) nth_zip by fastforce
hence subts_in_layers: "𝔏⇩α (tys ! i) (max_top_persistent (tys ! i) (ts ! i))"
using f_prop 2 lhs_types_def by blast
hence "max_top_persistent (tys ! i) (ts ! i) = Cs ! i"
using tys_def lengths ‹i < length Cs› by simp
hence "𝔏⇩α (tys ! i) (Cs ! i)" using subts_in_layers by simp
}
thus ?thesis using MFun f'_prop lengths by auto
qed auto
qed auto
lemma max_top_persistent_mfun:
assumes "sigF (f, length ts) = Some (tys, α)"
shows "∃Cs. Cs = (map (case_prod max_top_persistent) (zip tys ts)) ∧
max_top_persistent α (Fun f ts) = MFun f Cs ∧ length Cs = length ts"
using assms arity lhs_types_def by simp
lemma top_less_eq: "max_top_persistent α t ≤ mctxt_of_term t"
proof (induction t rule: max_top_persistent.induct)
case (2 β f ts) thus ?case
proof (cases "∃tys. sigF (f, length ts) = Some (tys, β)")
case True
then obtain tys where f_props: "sigF (f, length ts) = Some (tys, β)"
"length ts = length tys" "lhs_types (f, length ts) = tys"
using arity lhs_types_def by fastforce
have lengths: "length (zip (lhs_types (f, length ts)) ts) = length ts"
using f_props by (metis (no_types) length_zip min_def)
{ fix i
assume "i < length ts"
hence "(tys ! i, ts ! i) ∈ set (zip (lhs_types (f, length ts)) ts)"
using f_props in_set_conv_nth length_zip by fastforce
hence "map (λ(x, y). max_top_persistent x y) (zip (lhs_types (f, length ts)) ts) ! i
≤ map mctxt_of_term ts ! i"
using 2 ‹i < length ts› lhs_types_def f_props(1) arity by simp
} note inner = this
thus ?thesis using lengths f_props(1)
by (metis max_top_persistent.simps(2) mctxt_of_term.simps(2) length_map mfun_leq_mfunI)
qed simp
qed simp
lemma max_top_var_α: "max_topC_α α (mctxt_of_term (Var x)) = MVar x"
proof -
have mvar_in_topsC: "MVar x ∈ topsC_α α (MVar x)"
unfolding layer_system_sig.topsC_def by blast
from max_top_not_hole[of "Var x"] have "max_top (Var x) ≠ MHole" by simp
thus ?thesis
using mvar_in_topsC unfolding layer_system_sig.max_topC_def
layer_system_sig.topsC_def by fastforce
qed
lemma max_top_unique_α:
shows "∃!M. M ∈ topsC_α α C ∧ (∀L ∈ topsC_α α C. L ≤ M)"
proof -
let ?topsC' = "layer_system_sig.topsC { L . ∃α. 𝔏⇩α α L }" and
?topsC_α = "topsC_α α"
have mhole_in_tops_α: "∀C. MHole ∈ topsC_α α C"
using layer_system_sig.topsC_def less_eq_mctxtI1(1) by blast
have "topsC C = ?topsC' C"
using topsC_def[of C] 𝔏_def layer_system_sig.topsC_def[of "{ L . ∃α. 𝔏⇩α α L }" C] by simp
hence "∃!M. M ∈ ?topsC' C ∧ (∀L∈?topsC' C. L ≤ M)"
using max_top_unique by (metis (no_types, lifting))
then obtain M β where M_props: "M ∈ ?topsC' C" "∀L∈?topsC' C. L ≤ M" "𝔏⇩α β M"
using layer_system_sig.topsC_def[of "{L. ∃α. 𝔏⇩α α L}" C] by auto
thus ?thesis
proof (cases "β = α")
case True
hence "M ∈ topsC_α α C" using M_props by (simp add: layer_system_sig.topsC_def)
moreover have "∀L∈topsC_α α C. L ≤ M" using M_props(2)
by (simp add: layer_system_sig.topsC_def) blast
ultimately show ?thesis using dual_order.antisym by (simp add: layer_system_sig.topsC_def) blast
next
case β_neq_α: False thus ?thesis
proof (cases "M = MHole ∨ (∃x. M = MVar x)")
case True
hence "M ∈ topsC_α α C" using M_props by (auto simp: layer_system_sig.topsC_def)
moreover have "∀L∈topsC_α α C. L ≤ M" using M_props(2)
by (simp add: layer_system_sig.topsC_def) blast
ultimately show ?thesis using dual_order.antisym by blast
next
case False
then obtain f Cs where M_def: "M = MFun f Cs" using mctxt_neq_mholeE by blast
then obtain tys where f_prop: "sigF (f, length Cs) = Some (tys, β)"
using M_props 𝔏⇩α.simps by blast
have "M ≤ C" using M_props layer_system_sig.topsC_def by blast
then obtain Cs' where C_def: "C = MFun f Cs'" "length Cs' = length Cs"
using M_def less_eq_mctxt_MFunE1 by metis
{ fix L :: "('f, 'v) mctxt"
assume "L ∈ topsC_α α C"
hence "L ≤ C" using M_props layer_system_sig.topsC_def by blast
hence "L = MHole"
proof (cases L)
case MVar thus ?thesis using ‹L ≤ C› C_def by (meson less_eq_mctxt_MVarE1 mctxt.simps(6))
next
case (MFun f' Cs'')
hence "f' = f ∧ length Cs'' = length Cs'"
using ‹L ≤ C› C_def(1) less_eq_mctxt_MFunE1 mctxt.inject(2) by fastforce
hence "¬ (∃tys. sigF (f', length Cs'') = Some (tys, α))"
using f_prop C_def(2) β_neq_α by simp
thus ?thesis using MFun ‹L ∈ topsC_α α C› layer_system_sig.topsC_def[of "{L. 𝔏⇩α α L}" C]
by (metis (no_types, lifting) consistent_𝔏⇩α mem_Collect_eq)
qed
}
thus ?thesis using mhole_in_tops_α by blast
qed
qed
qed
lemma max_top_persist_mono:
assumes "L ≤ mctxt_of_term t" and "𝔏⇩α α L"
shows "L ≤ max_top_persistent α t"
using assms
proof (induction L "mctxt_of_term t" arbitrary: t α rule: less_eq_mctxt_induct)
case (2 x)
thus ?case by (metis eq_iff max_top_persistent.simps(1) term_of_mctxt.simps(1)
term_of_mctxt_mctxt_of_term_id)
next
case (3 Cs Ds f)
from 3(5) obtain tys where f_prop: "sigF (f, length Cs) = Some (tys, α)" "length tys = length Cs"
using consistent_𝔏⇩α arity by blast
obtain ts where t_def: "t = Fun f ts" "map mctxt_of_term ts = Ds" "length ts = length Ds"
using 3(4) mctxt_of_term.simps(2)
by (metis length_map mctxt.inject(2) term_of_mctxt.simps(2) term_of_mctxt_mctxt_of_term_id)
hence unfolded_max_top_persist: "max_top_persistent α t = MFun f (map (case_prod max_top_persistent)
(zip tys ts))" using f_prop 3(1) max_top_persistent_mfun by force
{ fix i
assume i_props: "i < length Cs" "Ds ! i = mctxt_of_term (ts ! i)"
hence "Cs ! i ≤ Ds ! i" using 3 by fast
moreover have "𝔏⇩α (tys ! i) (Cs ! i)" using consistent_𝔏⇩α f_prop i_props 3(5) by force
ultimately have "Cs ! i ≤ max_top_persistent (tys ! i) (ts ! i)" using i_props 3(3) by simp
}
thus ?case using 3(1) 3(4) f_prop t_def unfolded_max_top_persist
mfun_leq_mfunI[of f f Cs "(map (λ(x, y). max_top_persistent x y) (zip tys ts))"]
by (simp add: map_nth_eq_conv)
qed auto
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_α] layer_system_sig.max_topC_def)
lemma max_top_persistent_correct_α:
"max_top_persistent α t = layer_system_sig.max_top { L . 𝔏⇩α α L } t"
proof (induction t)
case (Var x) thus ?case using max_top_var_α by simp
next
case (Fun f ts) thus ?case
proof (cases "∃tys. sigF (f, length ts) = Some (tys, α)")
case True
then obtain tys where f_props: "sigF (f, length ts) = Some (tys, α)"
"length ts = length tys" "lhs_types (f, length ts) = tys"
using arity lhs_types_def by fastforce
let ?Cs = "map (case_prod max_top_persistent) (zip tys ts)"
have unfold_max_top_persist: "max_top_persistent α (Fun f ts) = MFun f ?Cs"
using f_props by simp
{ fix L
assume L_props: "L ≤ MFun f (map mctxt_of_term ts)" "𝔏⇩α α L"
hence "L ≤ MFun f ?Cs" using max_top_persist_mono[of L]
by (metis mctxt_of_term.simps(2) unfold_max_top_persist)
}
hence less_than_max_top_persistent: "𝔏⇩α α L ∧ L ≤ MFun f (map mctxt_of_term ts)
⟶ L ≤ MFun f ?Cs" for L by auto
hence in_𝔏⇩α: "𝔏⇩α α (MFun f ?Cs)" using max_top_persistent_in_layers f_props by auto
have is_top: "MFun f ?Cs ≤ MFun f (map mctxt_of_term ts)"
using unfold_max_top_persist by (metis (full_types) mctxt_of_term.simps(2) top_less_eq)
have max_top_lt_max_top_persist: "layer_system_sig.max_top { L . 𝔏⇩α α L } (Fun f ts) ≤ MFun f ?Cs"
using less_than_max_top_persistent max_topC_props_α(1)
layer_system_sig.topsC_def[of "{ L . 𝔏⇩α α L }"]
by (metis (no_types, lifting) mctxt_of_term.simps(2) mem_Collect_eq)
have "MFun f ?Cs ≤ max_topC_α α (MFun f (map mctxt_of_term ts))"
using is_top in_𝔏⇩α layer_system_sig.topsC_def max_topC_props_α(2) by blast
thus ?thesis
using max_top_lt_max_top_persist unfold_max_top_persist dual_order.antisym by auto
next
case False
hence "length cs = length ts ⟶ ¬ 𝔏⇩α α (MFun f cs)" for cs by (metis consistent_𝔏⇩α)
hence top_is_hole: "𝔏⇩α α L ∧ L ≤ MFun f (map mctxt_of_term ts) ⟶ L = MHole" for L
by (auto elim: less_eq_mctxt_MFunE2)
{ fix L
assume "layer_system_sig.max_topC {L. 𝔏⇩α α L} (mctxt_of_term (Fun f ts)) = L"
hence L_props: "L ∈ layer_system_sig.topsC {L'. 𝔏⇩α α L'} (mctxt_of_term (Fun f ts)) ∧
(∀L'∈layer_system_sig.topsC {L'. 𝔏⇩α α L'} (mctxt_of_term (Fun f ts)). L' ≤ L)"
using layer_system_sig.max_topC_def[of "{L. 𝔏⇩α α L}" "(mctxt_of_term (Fun f ts))"]
max_top_unique_α[of α "(mctxt_of_term (Fun f ts))"] by (auto dest!: theI')
hence "𝔏⇩α α L" using layer_system_sig.topsC_def[of "{L. 𝔏⇩α α L}"] by blast
have "L ≤ MFun f (map mctxt_of_term ts)" using layer_system_sig.topsC_def L_props by auto
hence "L = MHole" using top_is_hole ‹𝔏⇩α α L› by simp
}
hence "layer_system_sig.max_topC {L. 𝔏⇩α α L} (mctxt_of_term (Fun f ts)) = MHole" by blast
thus ?thesis using False by simp
qed
qed
end
lemma L_not_in_𝔏⇩β:
assumes f_in_ℱ⇩α: "sigF (f, length Cs) = Some (tys, α)"
shows "L ∈ 𝔏 ∧ L ≤ MFun f Cs ⟷ 𝔏⇩α α L ∧ L ≤ MFun f Cs"
proof (cases "L ≤ MFun f Cs")
case True thus ?thesis
proof (cases L)
case (MFun f' Cs')
hence "f' = f" "length Cs' = length Cs"
using True less_eq_mctxt_MFunE2
by (fastforce, metis mctxt.distinct(5) mctxt.inject(2))
hence "α ≠ β ⟶ ¬ 𝔏⇩α β L" for β using MFun f_in_ℱ⇩α 𝔏⇩α.cases by fastforce
thus ?thesis using 𝔏_def by fast
qed auto
qed simp
lemma max_top_persistent_correct_ℱ⇩α: "sigF (f, length ts) = Some (tys, α) ⟹
max_top_persistent α (Fun f ts) = max_top (Fun f ts) ∧
(β ≠ α ⟶ max_top_persistent β (Fun f ts) = MHole)"
using max_top_persistent_correct_α[of α "Fun f ts"]
by (auto simp: layer_system_sig.max_topC_def layer_system_sig.topsC_def L_not_in_𝔏⇩β)
lemma max_top_MFun_α:
assumes "max_top t = MFun f Cs"
shows "∃α. max_top t = max_top_persistent α t"
using assms
proof (induction t arbitrary: f Cs)
case Var thus ?case using max_top_var by auto
next
case (Fun f' ts)
have similar: "f = f' ∧ length Cs = length ts" using Fun(2) max_topC_props(1) unfolding topsC_def
by (metis (no_types, lifting) length_map less_eq_mctxt_MFunE1
mctxt.inject(2) mctxt_of_term.simps(2) mem_Collect_eq)
have "MFun f Cs ∈ 𝔏" using Fun max_topC_layer[of "MFun f' (map mctxt_of_term ts)"] by simp
then obtain α tys where "sigF (f, length Cs) = Some (tys, α)"
using 𝔏_def consistent_𝔏⇩α by blast
hence "max_top (Fun f' ts) = max_top_persistent α (Fun f' ts)"
using max_top_persistent_correct_ℱ⇩α[of f' ts tys α] similar by auto
thus ?case by blast
qed
lemma max_top_Fun_α:
shows "∃α. max_top (Fun f ts) = max_top_persistent α (Fun f ts)"
using max_top_persistent_correct_ℱ⇩α max_top_MFun_α
by (metis less_eq_mctxtE2(3) max_top_persistent.simps(2) max_top_prefix mctxt_of_term.simps(2))
lemma max_top_var_weak1:
"max_top t = MVar x ⟷ Var x = t"
by (metis (no_types, lifting) less_eq_mctxt_MVarE1 max_topC_props(1)
max_top_var mem_Collect_eq term_of_mctxt_mctxt_of_term_id topsC_def)
lemma mctxt_leq_𝔏⇩α:
assumes "L ≤ N" "𝔏⇩α α N"
shows "𝔏⇩α α L"
using assms
proof (induction "L :: ('f, 'v) mctxt" N arbitrary: α rule: less_eq_mctxt_induct)
case (3 Cs Ds f α)
then obtain tys where f_prop: "sigF (f, length Ds) = Some (tys, α)" using consistent_𝔏⇩α by blast
{ fix i
assume "i < length Cs"
hence "𝔏⇩α (tys ! i) (Ds ! i)" using f_prop 3 consistent_𝔏⇩α by fastforce
hence "𝔏⇩α (tys ! i) (Cs ! i)" using ‹i < length Cs› 3(3) 3(4) by blast
}
thus ?case using 3(1) f_prop by auto
qed auto
lemma mctxt_leq_subm_at_𝔏⇩α:
assumes "L ≤ N" "p ∈ all_poss_mctxt L" "𝔏⇩α α (subm_at N p)"
shows "𝔏⇩α α (subm_at L p)"
using mctxt_leq_𝔏⇩α[OF less_eq_subm_at[OF assms(2) assms(1)], OF assms(3)] .
lemma max_max_top: "max_top_persistent α t ≤ max_top t"
using max_top_persistent_correct_ℱ⇩α
by (induction α t rule: "max_top_persistent.induct") auto
abbreviation mtp where "mtp ≡ λα x. mctxt_term_conv (max_top_persistent α x)"
abbreviation push_in_ctxt where
"push_in_ctxt s t C α D β ≡ mtp α C⟨s⟩ = D⟨mtp β s⟩ ∧ mtp α C⟨t⟩ = D⟨mtp β t⟩ ∧
hole_pos C = hole_pos D"
lemma push_mt_ctxt:
assumes "p = hole_pos C" "p ∈ funposs_mctxt (max_top_persistent α C⟨s⟩)"
shows "∃D γ. push_in_ctxt s t C α D γ"
using assms(2) unfolding assms(1)
proof (induction C arbitrary: α)
case Hole
hence "push_in_ctxt s t □ α □ α" by simp
thus ?case by blast
next
case (More f ss1 C' ss2)
let ?Cs = "ss1 @ C'⟨s⟩ # ss2"
show ?case
proof (cases "∃tys. sigF (f, length ?Cs) = Some (tys, α)")
case True
then obtain tys where f_props: "sigF (f, length ?Cs) = Some (tys, α)"
"length ?Cs = length tys" "lhs_types (f, length ?Cs) = tys"
using arity lhs_types_def by fastforce
let ?Ds = "map (λ(x, y). max_top_persistent x y) (zip (take (length ss1) tys) ss1) @
max_top_persistent (tys ! length ss1) C'⟨s⟩ #
map (λ(x, y). max_top_persistent x y) (zip (drop (Suc (length ss1)) tys) ss2)"
have "tys = (take (length ss1) tys) @ (tys ! length ss1) # (drop (Suc (length ss1)) tys)"
using f_props(2) id_take_nth_drop[of "length ss1" tys] by fastforce
then obtain tys1 ty tys2 where tys_def: "tys = tys1 @ ty # tys2" "length tys1 = length ss1"
by fastforce
have mt_unfold: "max_top_persistent α (More f ss1 C' ss2)⟨s⟩ = MFun f ?Ds"
using f_props tys_def(2) unfolding tys_def(1) by (auto simp: append_Cons_nth_middle)
have "length (map (mctxt_term_conv ∘ (λ(x, y). max_top_persistent x y)) (zip tys1 ss1)) = length ss1"
using length_map length_zip tys_def(2) by force
hence "hole_pos C' ∈ funposs_mctxt (max_top_persistent (tys ! length ss1) C'⟨s⟩)"
using f_props More(2) tys_def(2) nth_append_length
[of "map (mctxt_term_conv ∘ (λ(x, y). max_top_persistent x y)) (zip tys1 ss1)"]
unfolding tys_def(1) mt_unfold by (auto simp: funposs_mctxt_def)
then obtain D' β' where inner: "push_in_ctxt s t C' (tys ! length ss1) D' β'"
using More(1) by fast
let ?D = "More f (map (mctxt_term_conv ∘ (λ(x, y). max_top_persistent x y)) (zip tys1 ss1)) D'
(map (mctxt_term_conv ∘ (λ(x, y). max_top_persistent x y)) (zip tys2 ss2))"
have "push_in_ctxt s t (More f ss1 C' ss2) α ?D β'"
using inner f_props tys_def(2) unfolding tys_def(1)
by (simp add: append_Cons_nth_middle)
thus ?thesis by blast
next
case False thus ?thesis using More(2) by (simp add: funposs_mctxt_def)
qed
qed
lemma map_equiv:
assumes "length ls2 = length ls1" "∀i < length ls2. f (ls1 ! i, ls2 ! i) = g (ls2 ! i)"
shows "map f (zip ls1 ls2) = map g ls2"
using assms
proof (induction ls2 arbitrary: ls1)
case (Cons a ls2')
then obtain b ls1' where "ls1 = b # ls1'" by (cases ls1) auto
thus ?case using Cons by fastforce
qed simp
lemma push_mt_subst:
assumes "𝒯⇩α α t"
shows "mtp α (t ⋅ σ) = t ⋅ (λx. mtp (the (sigV x)) (σ x))"
using assms
proof (induction t)
case (funs f ts tys β)
hence lengths: "length ts = length tys" using arity by simp
let ?f = "mctxt_term_conv ∘ (λ(x, y). max_top_persistent x (y ⋅ σ))" and
?g = "λt. t ⋅ (λx. mtp (the (sigV x)) (σ x))"
have "map ?f (zip tys ts) = map ?g ts"
using funs(2) map_equiv[OF lengths, of ?f ?g] unfolding map_zip_map2 by simp
thus ?case using funs lhs_types_def by (auto simp: map_zip_map2)
qed simp
text ‹main lemma for condition C_1 in proof of layered›
lemma lemma_C⇩1:
fixes p :: pos and s t :: "('f, 'v) term" and r and σ
assumes "s ∈ 𝒯" and "t ∈ 𝒯" and p_funposs: "p ∈ funposs_mctxt (max_top s)" and
rstep_s_t: "(s, t) ∈ rstep_r_p_s' ℛ r p σ" and
s_def_t_def: "s = C⟨fst r ⋅ σ⟩" "t = C⟨snd r ⋅ σ⟩" "r ∈ ℛ" and
p_def: "p = hole_pos C" and
root_s: "∃f ts. s = Fun f ts ∧ sigF (f, length ts) = Some (tys, α)"
shows "∃τ. (mctxt_term_conv (max_top s), mctxt_term_conv (max_top t)) ∈ rstep_r_p_s' ℛ r p τ ∨
(mctxt_term_conv (max_top s), mctxt_term_conv MHole) ∈ rstep_r_p_s' ℛ r p τ"
proof -
let ?M = "max_top s" and ?L = "max_top t"
obtain f ts where s_def: "s = Fun f ts"
and f_props: "sigF (f, length ts) = Some (tys, α)" "length ts = length tys"
"lhs_types (f, length ts) = tys"
using root_s arity lhs_types_def by fastforce
hence mtp_eq: "max_top_persistent α s = max_top s"
using max_top_persistent_correct_ℱ⇩α by blast
have p_funposs_max_top: "p ∈ funposs_mctxt (max_top_persistent α s)"
using mtp_eq ‹p ∈ funposs_mctxt ?M› by simp
hence p_in_poss_max_top: "p ∈ all_poss_mctxt (max_top_persistent α C⟨t⟩)" for t
unfolding s_def_t_def p_def
using funposs_mctxt_subset_all_poss_mctxt[of "max_top_persistent α t"]
lhs_types_def
proof (induction C arbitrary: α)
case More thus ?case using funposs_mctxt_def funposs_mctxt_subset_all_poss_mctxt
by (auto simp: nth_append_length[of "map f xs" for f xs, unfolded length_map]
funposs_mctxt_def split: if_splits) blast
qed auto
let ?σ = "λx. mtp (the (sigV x)) (σ x)"
have "∃D β. push_in_ctxt (fst r ⋅ σ) t C α D β" for t
using push_mt_ctxt[OF p_def p_funposs_max_top[unfolded s_def_t_def]] by simp
then obtain D β where in_ctxt: "mtp α C⟨(fst r ⋅ σ)⟩ = D⟨mtp β (fst r ⋅ σ)⟩ ∧
mtp α C⟨(snd r ⋅ σ)⟩ = D⟨mtp β (snd r ⋅ σ)⟩"
"hole_pos C = hole_pos D" by blast
obtain β' where rule_type: "𝒯⇩α β' (fst r)" "𝒯⇩α β' (snd r)"
using ‹r ∈ ℛ› R_def[of "fst r" "snd r"] by auto
{ assume "β' ≠ β"
obtain g ss where lhs_def: "fst r = Fun g ss"
using wf ‹r ∈ ℛ› unfolding wf_trs_def by (metis prod.collapse)
obtain tys' where "sigF (g, length ss) = Some (tys', β')"
using rule_type(1) lhs_def by (metis 𝒯⇩α.simps term.distinct(1) term.inject(2))
hence "max_top_persistent β (fst r ⋅ σ) = MHole"
using max_top_persistent_correct_ℱ⇩α ‹β' ≠ β› lhs_def by simp
moreover have "hole_pos D ∈ funposs D⟨mtp β (fst r ⋅ σ)⟩"
using p_funposs_max_top in_ctxt
unfolding s_def_t_def(1) funposs_mctxt_def p_def by argo
ultimately have False by (induction D) auto
}
hence "β' = β" by blast
hence part2: "mtp β ((fst r) ⋅ σ) = (fst r) ⋅ ?σ"
and part3: "mtp β ((snd r) ⋅ σ) = (snd r) ⋅ ?σ"
using push_mt_subst rule_type by simp+
have first_half: "mctxt_term_conv (max_top s) = D⟨fst r ⋅ ?σ⟩"
using mtp_eq in_ctxt part2 unfolding s_def_t_def(1) by simp
moreover have second_half: "D⟨snd r ⋅ ?σ⟩ = mtp α (C⟨snd r ⋅ σ⟩)"
using part3 in_ctxt by metis
ultimately have "(mctxt_term_conv (max_top C⟨fst r ⋅ σ⟩), mtp α (C⟨snd r ⋅ σ⟩))
∈ rstep_r_p_s' ℛ r p ?σ"
using mtp_eq rstep_s_t ‹r ∈ ℛ› in_ctxt(2) p_def s_def_t_def(1)
by (metis (no_types, lifting) rstep_r_p_s'.rstep_r_p_s')
hence W: "∃ τ. max_top_persistent α (C⟨snd r ⋅ σ⟩) ∈ 𝔏 ∧
(mctxt_term_conv ?M, mtp α (C⟨snd r ⋅ σ⟩)) ∈ rstep_r_p_s' ℛ r p τ"
using max_top_persistent_in_layers 𝔏_def Un_iff s_def_t_def(1) [folded p_def] by blast
then obtain τ where step_to_L: "(mctxt_term_conv ?M, mtp α (C⟨snd r ⋅ σ⟩)) ∈ rstep_r_p_s' ℛ r p τ"
by auto
thus ?thesis
proof (cases t)
case (Var x)
then show ?thesis using s_def_t_def(2) step_to_L by auto
next
case (Fun g ss)
thus ?thesis using step_to_L s_def_t_def(2) max_top_persistent_correct_ℱ⇩α
by (metis Fun max_top_persistent.simps(2))
qed
qed
sublocale layered "ℱ" "𝔏"
proof
show "wf_trs ℛ" using wf .
next
show "funas_trs ℛ ⊆ ℱ"
proof
fix fn
assume "fn ∈ funas_trs ℛ"
then obtain l r :: "('f, 'v) term" where "fn ∈ funas_rule (l, r)" "(l, r) ∈ ℛ"
unfolding funas_trs_def by fast
thus "fn ∈ ℱ"
using R_def[OF ‹(l, r) ∈ ℛ›] funas_𝒯⇩α
by (metis funas_rule_def Un_iff fst_conv snd_conv)
qed
next
fix p :: pos and s t :: "('f, 'v) term" and r and σ
let ?M = "max_top s" and ?L = "max_top t"
assume assms: "s ∈ 𝒯" "t ∈ 𝒯" "p ∈ funposs_mctxt ?M" and
rstep_s_t: "(s, t) ∈ rstep_r_p_s' ℛ r p σ"
then obtain C where
s_def_t_def: "s = C⟨fst r ⋅ σ⟩" "t = C⟨snd r ⋅ σ⟩" "r ∈ ℛ" and
p_def: "p = hole_pos C"
by auto
show "∃τ. (mctxt_term_conv ?M, mctxt_term_conv ?L) ∈ rstep_r_p_s' ℛ r p τ ∨
(mctxt_term_conv ?M, mctxt_term_conv MHole) ∈ rstep_r_p_s' ℛ r p τ"
proof -
consider "∃f ts. s = Fun f ts ∧ (f, length ts) ∈ ℱ"
| "∃x. s = Var x" using ‹s ∈ 𝒯› 𝒯_def by (cases s) auto
thus ?thesis
proof cases
case 1
then obtain f ts tys α where "s = Fun f ts" "sigF (f, length ts) = Some (tys, α)"
unfolding ℱ_def by auto
thus ?thesis using lemma_C⇩1[OF assms rstep_s_t s_def_t_def p_def] by auto
next
case 2 thus ?thesis
using rstep_s_t wf NF_Var rstep_eq_rstep' rstep'_iff_rstep_r_p_s' prod.collapse
by metis
qed
qed
next
fix L N :: "('f, 'v) mctxt" and p :: pos
assume my_assms: "N ∈ 𝔏" "L ∈ 𝔏" "L ≤ N" "p ∈ hole_poss L"
thus "mreplace_at L p (subm_at N p) ∈ 𝔏"
proof -
obtain α where "𝔏⇩α α N" using ‹N ∈ 𝔏› 𝔏_def by auto
hence "𝔏⇩α α L" using ‹L ∈ 𝔏› 𝔏_def ‹L ≤ N›
proof (induction N rule: 𝔏⇩α.induct)
case mhole thus ?case using mctxt_order_bot.bot.extremum_uniqueI by auto
next
case mvar thus ?case using less_eq_mctxtE2(2) 𝔏_def by (metis 𝔏⇩α.mvar mhole)
next
case (mfun f Cs tys β) thus ?case using L_not_in_𝔏⇩β by blast
qed
have "p ∈ all_poss_mctxt N"
using ‹p ∈ hole_poss L› ‹L ≤ N› all_poss_mctxt_conv all_poss_mctxt_mono[of L N]
by auto
then obtain β where "𝔏⇩α β (subm_at N p)" using 𝔏_subm[OF ‹N ∈ 𝔏›] 𝔏_def by auto
hence "𝔏⇩α β (subm_at L p)" using mctxt_leq_subm_at_𝔏⇩α[OF ‹L ≤ N›, of p β] ‹p ∈ hole_poss L›
by auto
consider "(L = MHole ∨ (∃x. L = MVar x))" | "𝔏⇩α α (mreplace_at L p (subm_at N p))"
using mreplace_at_𝔏⇩α'[OF my_assms(3) ‹𝔏⇩α α L› my_assms(1) ‹𝔏⇩α β (subm_at L p)› ‹𝔏⇩α β (subm_at N p)›]
my_assms(4) UnCI all_poss_mctxt_conv by fastforce
thus ?thesis
proof (cases)
case 1 thus ?thesis using ‹p ∈ hole_poss L› ‹N ∈ 𝔏› by fastforce
next
case 2 thus ?thesis using 𝔏_def by auto
qed
qed
qed
lemma conserv_subst:
assumes "𝒯⇩α α (t ⋅ σ)" and "⋀x β. (sigV x = Some β ⟷ 𝒯⇩α β (Var x ⋅ σ))"
shows "𝒯⇩α α t"
using assms(1)
proof (induction t arbitrary: α)
case (Var x β)
hence "sigV x = Some β" using assms(2) by simp
thus ?case by auto
next
case (Fun f ts β)
have "length (map (λt. t ⋅ σ) ts) = length ts" by simp
then obtain tys where "sigF (f, length ts) = Some (tys, β)" "∀i<length ts. 𝒯⇩α (tys ! i) (ts ! i)"
using Fun 𝒯⇩α.cases[of β "Fun f ts ⋅ σ"] subst_apply_term.simps(2)[of f ts σ] nth_map
proof -
assume a1: "⋀tys. ⟦sigF (f, length ts) = Some (tys, β); ∀i<length ts. 𝒯⇩α (tys ! i) (ts ! i)⟧ ⟹ thesis"
have "(∃v t. β = t ∧ Fun f ts ⋅ σ = Var v ∧ sigV v = Some t) ∨ (∃fa tsa tsb t. β = t ∧ Fun f ts ⋅ σ = Fun fa tsa ∧ sigF (fa, length tsa) = Some (tsb, t) ∧ (∀n. ¬ n < length tsa ∨ 𝒯⇩α (tsb ! n) (tsa ! n)))"
by (meson Fun.prems ‹⋀P. ⟦𝒯⇩α β (Fun f ts ⋅ σ); ⋀x α. ⟦β = α; Fun f ts ⋅ σ = Var x; sigV x = Some α⟧ ⟹ P; ⋀fa tsa tys α. ⟦β = α; Fun f ts ⋅ σ = Fun fa tsa; sigF (fa, length tsa) = Some (tys, α); ∀i<length tsa. 𝒯⇩α (tys ! i) (tsa ! i)⟧ ⟹ P⟧ ⟹ P›)
thus ?thesis
using a1 Fun by auto
qed
thus ?case using Fun 𝒯⇩α.cases by blast
qed
lemma 𝒯⇩α_subt_at:
assumes "𝒯⇩α α C⟨t⟩"
shows "∃β. 𝒯⇩α β t"
using assms
proof (induction C arbitrary: α)
case (More f ss1 C' ss2)
let ?ts = "ss1 @ C'⟨t⟩ # ss2"
obtain tys where "sigF (f, length ?ts) = Some (tys, α)" using More(2) by (auto elim: 𝒯⇩α.cases)
with More(2) have "∀i<length ?ts. 𝒯⇩α (tys ! i) (?ts ! i)"
by (auto elim: 𝒯⇩α.cases)
hence "𝒯⇩α (tys ! length ss1) (?ts ! length ss1)"
by (metis add_Suc_right length_Cons length_append less_add_Suc1)
thus ?case using More(1) unfolding nth_append_length[of ss1 "C'⟨t⟩" ss2] by blast
qed auto
lemma 𝒯⇩α_subst:
assumes "𝒯⇩α α t" "⋀y γ. y ∈ vars_term t ⟹ (sigV y = Some γ ⟶ 𝒯⇩α γ (Var y ⋅ σ))"
shows "𝒯⇩α α (t ⋅ σ)"
using assms
proof (induction t)
case (funs f ts tys α)
{ fix i
assume "i < length ts"
hence "𝒯⇩α (tys ! i) (ts ! i ⋅ σ)" using funs by fastforce
}
then show ?case using funs(1) by auto
qed simp
lemma 𝔏⇩α_subst:
assumes "𝒯⇩α α t"
"⋀y γ. y ∈ vars_term t ⟹ (sigV y = Some γ ⟶ 𝔏⇩α γ (mctxt_of_term (Var y ⋅ σ)))"
shows "𝔏⇩α α (mctxt_of_term (t ⋅ σ))"
using assms
proof (induction t rule: 𝒯⇩α.induct)
case (funs f ts tys α)
{ fix i
assume "i < length ts"
hence "𝔏⇩α (tys ! i) (mctxt_of_term (ts ! i ⋅ σ))" using funs by fastforce
}
thus ?case using funs(1) by auto
qed simp
lemma conserv_𝒯⇩α:
assumes "𝒯⇩α α s"
shows "(s, t) ∈ rstep ℛ ⟹ 𝒯⇩α α t"
proof -
assume "(s, t) ∈ rstep ℛ"
from this and assms show "𝒯⇩α α t"
proof (induction rule: rstep_induct)
case (IH C σ l r)
then obtain β where type_lσ: "𝒯⇩α β (l ⋅ σ)" using 𝒯⇩α_subt_at by blast
obtain β' where rule_type: "𝒯⇩α β' l" "𝒯⇩α β' r"
using R_def[OF IH(1)] by auto
have "is_Fun l" using IH wf unfolding wf_trs_def by blast
hence "β' = β" using rule_type(1) type_lσ by (cases l) (auto elim!: 𝒯⇩α.cases)
have σ_types: "⋀y γ. y ∈ vars_term l ⟹ (sigV y = Some γ ⟶ 𝒯⇩α γ (Var y ⋅ σ))"
using type_lσ rule_type(1) unfolding ‹β' = β›
proof (induction l arbitrary: β)
case (Fun f ts)
obtain tys where type_f: "sigF (f, length ts) = Some (tys, β)"
using Fun(3) by (auto elim: 𝒯⇩α.cases)
{ fix t⇩i
assume asms: "t⇩i ∈ set ts" "y ∈ vars_term t⇩i"
then obtain i where t⇩i_def: "t⇩i = ts ! i" "i < length ts" by (meson in_set_idx)
hence "𝒯⇩α (tys ! i) t⇩i" "𝒯⇩α (tys ! i) (t⇩i ⋅ σ)" using type_f Fun(3-) by (auto elim!: 𝒯⇩α.cases)
hence "(sigV y = Some γ) ⟶ 𝒯⇩α γ (Var y ⋅ σ)" using Fun(1)[OF asms, of "tys ! i" γ] by fast
}
then show ?case using Fun(2) by auto
qed (auto elim!: 𝒯⇩α.cases)
have sub_vars: "vars_term r ⊆ vars_term l" using IH wf by (simp add: wf_trs_def)
from IH(2) show ?case
proof (induction C arbitrary: α)
case Hole
hence "β = α" using type_lσ by (auto elim!: 𝒯⇩α.cases)
hence "𝒯⇩α α r" using rule_type ‹β' = β› by blast
from 𝒯⇩α_subst[OF this] show ?case using sub_vars σ_types by auto
next
case (More f ss1 C' ss2)
let ?ts = "ss1 @ C'⟨l ⋅ σ⟩ # ss2" and ?ts' = "ss1 @ C'⟨r ⋅ σ⟩ # ss2"
obtain tys where type_f: "sigF (f, length ?ts) = Some (tys, α)"
using More(2) by (auto elim: 𝒯⇩α.cases)
with More(2) have sub_typed: "∀i<length ?ts. 𝒯⇩α (tys ! i) (?ts ! i)"
by (auto elim: 𝒯⇩α.cases)
hence "𝒯⇩α (tys ! length ss1) (?ts ! length ss1)"
by (metis add_Suc_right length_Cons length_append less_add_Suc1)
hence "𝒯⇩α (tys ! length ss1) (?ts' ! length ss1)"
using More(1) by simp
hence "∀i<length ?ts'. 𝒯⇩α (tys ! i) (?ts' ! i)"
using arity sub_typed unfolding ctxt_apply_term.simps
by (metis append_Cons_nth_not_middle length_Cons length_append)
thus ?case using type_f by auto
qed
qed
qed
lemma conserv_𝔏⇩α:
assumes "𝔏⇩α α (mctxt_of_term s)"
shows "(s, t) ∈ rstep ℛ ⟹ 𝔏⇩α α (mctxt_of_term t)"
proof -
assume "(s, t) ∈ rstep ℛ"
from this and assms show "𝔏⇩α α (mctxt_of_term t)"
proof (induction rule: rstep_induct)
case (IH C σ l r)
then obtain β where type_lσ: "𝔏⇩α β (mctxt_of_term (l ⋅ σ))"
using 𝔏_sub 𝔏_def by blast
obtain β' where rule_type: "𝒯⇩α β' l" "𝒯⇩α β' r"
using R_def[OF IH(1)] by auto
have "is_Fun l" using IH wf unfolding wf_trs_def by blast
hence "β' = β" using rule_type(1) type_lσ by (cases l) (auto elim!: 𝒯⇩α.cases 𝔏⇩α.cases)
have σ_types: "⋀y γ. y ∈ vars_term l ⟹
(sigV y = Some γ ⟶ 𝔏⇩α γ (mctxt_of_term (Var y ⋅ σ)))"
using rule_type(1) type_lσ unfolding ‹β' = β›
proof (induction β l rule: 𝒯⇩α.induct)
case (funs f ts tys α)
{ fix t⇩i
assume asms: "t⇩i ∈ set ts" "y ∈ vars_term t⇩i"
then obtain i where t⇩i_def: "t⇩i = ts ! i" "i < length ts" by (meson in_set_idx)
hence "𝔏⇩α (tys ! i) (mctxt_of_term t⇩i)" using funs(2) 𝒯⇩α_𝔏⇩α by simp
moreover have "𝔏⇩α (tys ! i) (mctxt_of_term (t⇩i ⋅ σ))"
using funs(1,4) t⇩i_def by (auto elim: 𝔏⇩α.cases)
ultimately have "(sigV y = Some γ) ⟶ 𝔏⇩α γ (mctxt_of_term (Var y ⋅ σ))"
using funs(2) asms t⇩i_def by blast
}
then show ?case using funs(3) by auto
qed auto
have sub_vars: "vars_term r ⊆ vars_term l" using IH wf by (simp add: wf_trs_def)
from IH(2) show ?case
proof (induction C arbitrary: α)
case Hole
hence "β = α" using type_lσ ‹is_Fun l› by (auto elim!: 𝔏⇩α.cases)
hence "𝒯⇩α α r" using rule_type ‹β' = β› by blast
from 𝔏⇩α_subst[OF this] show ?case using sub_vars σ_types by auto
next
case (More f ss1 C' ss2)
let ?ts = "ss1 @ C'⟨l ⋅ σ⟩ # ss2" and ?ts' = "ss1 @ C'⟨r ⋅ σ⟩ # ss2"
obtain tys where type_f: "sigF (f, length ?ts) = Some (tys, α)"
using More(2) by (auto elim: 𝔏⇩α.cases)
with More(2) have sub_typed: "∀i<length ?ts. 𝔏⇩α (tys ! i) (mctxt_of_term (?ts ! i))"
by (auto elim!: 𝔏⇩α.cases)
(metis (no_types, lifting) arity list.simps(9) map_append nth_map type_f)
hence "𝔏⇩α (tys ! length ss1) (mctxt_of_term (?ts ! length ss1))"
by (metis add_Suc_right length_Cons length_append less_add_Suc1)
hence "𝔏⇩α (tys ! length ss1) (mctxt_of_term (?ts' ! length ss1))"
using More(1) by simp
hence "∀i<length ?ts'. 𝔏⇩α (tys ! i) (mctxt_of_term (?ts' ! i))"
using arity sub_typed unfolding ctxt_apply_term.simps
by (metis append_Cons_nth_not_middle length_Cons length_append)
thus ?case using type_f arity nth_map[of _ "ss1 @ C'⟨r ⋅ σ⟩ # ss2" mctxt_of_term]
by (auto simp: map_nth_eq_conv)
qed
qed
qed
lemma conserv_star_𝒯⇩α:
assumes "(s, t) ∈ (rstep ℛ)⇧*" and "𝒯⇩α α s"
shows "𝒯⇩α α t"
using assms conserv_𝒯⇩α
by (induction rule: converse_rtrancl_induct) auto
lemma conserv_star_𝔏⇩α:
assumes "(s, t) ∈ (rstep ℛ)⇧*" and "𝔏⇩α α (mctxt_of_term s)"
shows "𝔏⇩α α (mctxt_of_term t)"
using assms conserv_𝔏⇩α
by (induction rule: converse_rtrancl_induct) auto
lemma needed_types_subt_at:
assumes "𝒯⇩α α C⟨t⟩" "𝒯⇩α β t"
shows "needed_types α β"
using assms
proof (induction C arbitrary: α)
case Hole
hence "β = α" by (auto elim!: 𝒯⇩α.cases)
thus ?case by blast
next
case (More f ss1 C' ss2)
let ?ts = "ss1 @ C'⟨t⟩ # ss2"
obtain tys where props: "sigF (f, length ?ts) = Some (tys, α)" "∀i<length ?ts. 𝒯⇩α (tys ! i) (?ts ! i)"
using More(2) by (auto elim: 𝒯⇩α.cases)
hence "needed_types α (tys ! length ss1)" using arity by auto
moreover have "𝒯⇩α (tys ! length ss1) C'⟨t⟩" using props
by (metis add_Suc_right length_Cons nth_append_length length_append less_add_Suc1)
ultimately show ?case using More(1,3) by blast
qed
lemma needed_rules_𝒯⇩α:
assumes "𝒯⇩α α s" "(s, t) ∈ rstep (ℛ⇩α β)"
shows "needed_types α β"
using assms
proof (induction s arbitrary: t)
case (var x α)
then show ?case using NF_Var[OF wf] by blast
next
case (funs f ts tys α)
then obtain l r p σ where step: "(Fun f ts, t) ∈ rstep_r_p_s (ℛ⇩α β) (l, r) p σ"
using rstep_iff_rstep_r_p_s[of "Fun f ts" t "ℛ⇩α β"] by blast
obtain C where props: "Fun f ts = C⟨l ⋅ σ⟩" "t = C⟨r ⋅ σ⟩" "p = hole_pos C" "(l, r) ∈ ℛ⇩α β"
using hole_pos_ctxt_of_pos_term Product_Type.Collect_case_prodD[OF step[unfolded rstep_r_p_s_def]]
unfolding fst_conv snd_conv by metis
then obtain g ss where l_def: "l = Fun g ss" using wf unfolding wf_trs_def by blast
then obtain tys' where type_β: "sigF (g, length ss) = Some (tys', β)"
using props(4) by (auto elim: 𝒯⇩α.cases)
obtain β' where "𝒯⇩α β' (l ⋅ σ)" using 𝒯⇩α_subt_at[of α C "l ⋅ σ"] props(1) funs(1,2) by auto
hence "β' = β" using type_β l_def by (auto elim: 𝒯⇩α.cases)
thus ?case using ‹𝒯⇩α β' (l ⋅ σ)› needed_types_subt_at[of α C "l ⋅ σ"]
funs(1,2) props(1) by auto
qed
abbreviation ℛ⇩n⇩α where "ℛ⇩n⇩α ≡ λα. ⋃{ ℛ⇩α β |β. needed_types α β}"
lemma needed_rules_𝒯⇩α_single:
assumes "(s, t) ∈ rstep ℛ" "𝒯⇩α α s"
shows "(s, t) ∈ rstep (ℛ⇩n⇩α α)"
proof -
obtain l r p σ where st_step: "(s, t) ∈ rstep_r_p_s ℛ (l, r) p σ"
using rstep_iff_rstep_r_p_s[of s t ℛ] assms(1) by blast
then obtain β where "𝒯⇩α β l" "𝒯⇩α β r" "(l, r) ∈ ℛ"
using R_def Product_Type.Collect_case_prodD[OF st_step[unfolded rstep_r_p_s_def]] by meson
hence "(s, t) ∈ rstep (ℛ⇩α β)"
using st_step rstep_r_p_s_imp_rstep[of s t "(ℛ⇩α β)" "(l, r)" p σ]
by (simp add: rstep_r_p_s_def)
then show ?thesis
using needed_rules_𝒯⇩α[OF assms(2), of t β] by blast
qed
lemma rstep_on_𝒯⇩α_iff_needed:
"Restr (rstep ℛ) {t. 𝒯⇩α α t} = Restr (rstep (ℛ⇩n⇩α α)) {t. 𝒯⇩α α t}"
using needed_rules_𝒯⇩α_single by auto
lemma CR_on_𝒯⇩α_by_needed_rules:
"CR_on (rstep ℛ) {t. 𝒯⇩α α t} ⟷ CR_on (rstep (ℛ⇩n⇩α α)) {t. 𝒯⇩α α t}"
by (subst (1 2) CR_on_iff_CR_Restr) (auto 0 3 intro: conserv_𝒯⇩α simp: rstep_on_𝒯⇩α_iff_needed)
lemma 𝒯⇩α_𝒯: "{ t. 𝒯⇩α α t } ⊆ 𝒯"
using funas_𝒯⇩α unfolding 𝒯_def by blast
text ‹The following lemma establishes the easy direction of persistence of confluence.›
lemma CR_persist':
assumes CR_union: "CR_on (rstep ℛ) 𝒯"
shows "CR_on (rstep ℛ) { t. 𝒯⇩α α t }"
using 𝒯⇩α_𝒯 assms unfolding CR_on_def by blast
end
locale persistent_cr_infinite_vars = persistent_cr sigF sigV ℛ for
sigF :: "('f × nat) ⇒ ('t list × 't) option" and
sigV :: "'v :: infinite ⇒ 't option" and
ℛ :: "('f, 'v :: infinite) trs" +
assumes inf_vars: "⋀α. infinite { v ∈ 𝒱. sigV v = Some α }"
begin
fun add_types :: "('f, 'v) term ⇒ 't ⇒ ('f, 'v * 't) term" where
"add_types (Var x) α = Var (x, α)"
| "add_types (Fun f ts) α = (case sigF (f, length ts) of
Some (tys, α) ⇒ Fun f (map (λ(t,α). add_types t α) (zip ts tys))
| None ⇒ Fun f (map (λt. add_types t undefined) ts))"
lemma drop_take_nth: "n < length ls ⟹ drop n (take (Suc n) ls) = [ls ! n]"
by (induction ls arbitrary: n) (simp, metis List.append_eq_append_conv
Suc_eq_plus1 Suc_eq_plus1_left take_Suc_conv_app_nth take_add take_drop)
lemma 𝒯⇩α_add_types_subst:
assumes "𝒯⇩α α t"
shows "add_types (t ⋅ σ) α = t ⋅ (λx. add_types (σ x) (the (sigV x)))"
using assms
proof (induction rule: 𝒯⇩α.induct)
case (funs f ts tys α)
thus ?case using arity[OF funs(1)]
by (simp add: map_nth_eq_conv)
qed simp
lemma add_types_preserves_step:
assumes "(s, t) ∈ rstep ℛ" "𝔏⇩α α (mctxt_of_term s)"
shows "(add_types s α, add_types t α) ∈ rstep' ℛ"
using assms
proof (induction arbitrary: α)
case (IH C σ l r)
obtain β where rule_type: "𝒯⇩α β l" "𝒯⇩α β r" using R_def[OF IH(1)] by blast
hence "add_types (l ⋅ σ) β = l ⋅ (λx. add_types (σ x) (the (sigV x)))"
"add_types (r ⋅ σ) β = r ⋅ (λx. add_types (σ x) (the (sigV x)))"
using 𝒯⇩α_add_types_subst by blast+
hence step': "(add_types (l ⋅ σ) β, add_types (r ⋅ σ) β) ∈ rstep' ℛ"
using rstep'[OF IH(1), of □] by auto
obtain f ts where l_def: "l = Fun f ts"
using wf IH(1) unfolding wf_trs_def by blast
then obtain tys where type_l: "sigF (f, length ts) = Some (tys, β)"
using rule_type by (auto elim: 𝒯⇩α.cases)
show ?case using IH(2)
proof (induction C arbitrary: α)
case Hole
hence "α = β" using type_l unfolding l_def by (auto elim: 𝔏⇩α.cases)
then show ?case using step' by auto
next
case (More f ss1 C' ss2)
then obtain tys where tys: "sigF (f, Suc (length ss1 + length ss2)) = Some (tys, α)"
by (auto elim!: 𝔏⇩α.cases)
hence in_𝔏⇩α: "𝔏⇩α (tys ! length ss1) (mctxt_of_term C'⟨l ⋅ σ⟩)"
using More(2) arity[OF tys] by (auto elim!: 𝔏⇩α.cases)
(metis (no_types) length_map less_add_Suc1 nth_append_length)
let ?C = "More f (map (λ(t,α). add_types t α) (zip ss1 (take (length ss1) tys))) □
(map (λ(t,α). add_types t α) (zip ss2 (drop (Suc (length ss1)) tys)))"
show ?case using tys rstep'_mono[OF More(1)[OF in_𝔏⇩α], of ?C] arity[OF tys]
by (simp add: zip_append1 zip_append1[of "[C'⟨_⟩]" _ "drop (length ss1) tys",
unfolded drop_drop[of _ "length ss1"], simplified]
take_drop drop_take_nth[of "length ss1" tys])
qed
qed
lemma add_types_preserves_steps:
assumes "(s, t) ∈ (rstep ℛ)⇧*" "𝔏⇩α α (mctxt_of_term s)"
shows "(add_types s α, add_types t α) ∈ (rstep' ℛ)⇧*"
using assms
proof (induction rule: converse_rtrancl_induct)
case (step y z)
hence "𝔏⇩α α (mctxt_of_term z)" using conserv_star_𝔏⇩α by blast
moreover have "(add_types y α, add_types z α) ∈ rstep' ℛ"
using add_types_preserves_step[OF step(1,4)] .
ultimately show ?case using step(3) by simp
qed auto
lemma 𝔏⇩α_add_types_𝒯⇩α:
assumes "𝔏⇩α α (mctxt_of_term s)"
shows "∃σ τ. 𝒯⇩α α (add_types s α ⋅ σ) ∧ (add_types s α ⋅ σ) ⋅ τ = add_types s α"
proof -
let ?typed_vts = "λs α β. { (x, β) |x. (x, β) ∈ vars_term (add_types s α) }"
let ?f = "?typed_vts s α"
let ?g = "λβ. { x ∈ 𝒱 . sigV x = Some β }"
have fin: "finite (?f β)" for β
by (auto intro: rev_finite_subset[OF finite_vars_term[of "add_types s α"]])
have inf: "infinite (?g β)" for β using inf_vars .
have disj_f: "⋀α' β. ?f α' ∩ ?f β ≠ {} ⟹ α' = β" by auto
have disj_g: "⋀α β. ?g α ∩ ?g β ≠ {} ⟹ α = β" by auto
obtain h where h_inj: "inj_on h (⋃α. ?f α)" "(∀α. h ` ?f α ⊆ ?g α)"
using finites_into_infinites[of ?f ?g, OF disj_f fin disj_g inf] by blast
let ?σ = "Var ∘ h" and ?τ = "Var ∘ (inv_into (⋃α. ?f α) h)"
have "add_types s α = add_types s α ⋅ Var" by simp
have "(add_types s α ⋅ ?σ) ⋅ ?τ = add_types s α ⋅ Var" using h_inj(1)
unfolding subst_subst_compose[symmetric] term_subst_eq_conv
by (auto simp: subst_compose_def)
moreover have "𝒯⇩α α (add_types s α ⋅ ?σ)"
using assms h_inj(2)
proof (induction "mctxt_of_term s" arbitrary: s rule: 𝔏⇩α.induct)
case (mhole α)
thus ?case by (cases s) auto
next
case (mvar β x)
hence s_def: "s = Var x" by (cases s) auto
hence "(x, α) ∈ vars_term (add_types s α)" by simp
thus ?case using mvar(2) unfolding s_def by auto
next
case (mfun f Cs tys β)
then obtain ts where s_def: "s = Fun f ts" "Cs = map mctxt_of_term ts" by (cases s) auto
let ?ts = "map ((λt. t ⋅ (Var ∘ h)) ∘ (λ(x, y). add_types x y)) (zip ts tys)"
have lengths: "length ?ts = length ts" using arity[OF mfun(1)] unfolding s_def by simp
{ fix i
assume "i < length Cs"
hence "map mctxt_of_term ts ! i = mctxt_of_term (ts ! i)" unfolding s_def by auto
have subs: "?typed_vts (ts ! i) (tys ! i) γ ⊆ ?typed_vts (Fun f ts) β γ" for γ
using mfun(1) ‹i < length Cs› arity[OF mfun(1)] nth_mem[of i "zip ts tys"]
unfolding s_def by (auto split: if_splits prod.splits)
have "∀α. h ` ?typed_vts (ts ! i) (tys ! i) α ⊆ {x ∈ 𝒱. sigV x = Some α}"
using mfun(4) image_mono[OF subs, of h] unfolding s_def by (meson subset_trans)
hence "𝒯⇩α (tys ! i) (add_types (ts ! i) (tys ! i) ⋅ ?σ)"
using mfun ‹i < length Cs› unfolding s_def by fastforce
}
thus ?case using mfun(1) arity[OF mfun(1)] unfolding s_def
by (auto simp: nth_mem[of _ "zip ts tys"] split: if_splits prod.splits)
qed
ultimately show ?thesis by auto
qed
lemma CR_on_union:
assumes CR_α: "∀α. CR_on (rstep ℛ) { t. 𝒯⇩α α t }"
shows "CR_on (rstep ℛ) { t. mctxt_of_term t ∈ 𝔏 }"
proof
fix a b c
assume a_in_L: "a ∈ { t. mctxt_of_term t ∈ 𝔏 }" and
a_to_b: "(a, b) ∈ (rstep ℛ)⇧*" and
a_to_c: "(a, c) ∈ (rstep ℛ)⇧*"
obtain α where a_in_𝔏⇩α: "𝔏⇩α α (mctxt_of_term a)" using a_in_L 𝔏_def by blast
hence b_in_𝔏⇩α: "𝔏⇩α α (mctxt_of_term b)" and
c_in_𝔏⇩α: "𝔏⇩α α (mctxt_of_term c)" using conserv_star_𝔏⇩α a_to_b a_to_c by blast+
have a_to_b': "(add_types a α, add_types b α) ∈ (rstep' ℛ)⇧*" and
a_to_c': "(add_types a α, add_types c α) ∈ (rstep' ℛ)⇧*"
using a_in_𝔏⇩α add_types_preserves_steps a_to_b a_to_c by blast+
obtain σ τ where in_𝒯⇩α: "𝒯⇩α α (add_types a α ⋅ σ)" and
inv_τ: "add_types a α ⋅ σ ⋅ τ = add_types a α"
using 𝔏⇩α_add_types_𝒯⇩α[OF a_in_𝔏⇩α] by blast
have a_to_b'': "(add_types a α ⋅ σ, add_types b α ⋅ σ) ∈ (rstep ℛ)⇧*"
using a_to_b'
proof (induction rule: converse_rtrancl_induct)
case (step y z)
have "(y ⋅ σ, z ⋅ σ) ∈ (rstep ℛ)" using rstep'_stable[OF step(1)] rstep_eq_rstep' by auto
thus ?case using step(3) by auto
qed auto
moreover have a_to_b'': "(add_types a α ⋅ σ, add_types c α ⋅ σ) ∈ (rstep ℛ)⇧*"
using a_to_c'
proof (induction rule: converse_rtrancl_induct)
case (step y z)
have "(y ⋅ σ, z ⋅ σ) ∈ (rstep ℛ)" using rstep'_stable[OF step(1)] rstep_eq_rstep' by auto
thus ?case using step(3) by auto
qed auto
ultimately have "(add_types b α ⋅ σ, add_types c α ⋅ σ) ∈ (rstep ℛ)⇧↓"
using CR_α in_𝒯⇩α unfolding CR_on_def by auto
then obtain d where join1: "(add_types b α ⋅ σ, d) ∈ (rstep ℛ)⇧*" and
join2: "(add_types c α ⋅ σ, d) ∈ (rstep ℛ)⇧*"
using joinD by fastforce
from join1 have join1': "(add_types b α ⋅ σ ⋅ τ, d ⋅ τ) ∈ (rstep' ℛ)⇧*"
proof (induction rule: converse_rtrancl_induct)
case (step y z)
thus ?case using rstep'_stable[of y z ℛ τ] by fastforce
qed auto
from join2 have join2': "(add_types c α ⋅ σ ⋅ τ, d ⋅ τ) ∈ (rstep' ℛ)⇧*"
proof (induction rule: converse_rtrancl_induct)
case (step y z)
thus ?case using rstep'_stable[of y z ℛ τ] by fastforce
qed auto
have remove_types: "add_types t α ⋅ (λ(x, α). Var x) = t" for α t
proof (induction t α rule: add_types.induct)
case (2 f ts α) thus ?case
proof (cases "sigF (f, length ts)")
case None
thus ?thesis using 2(1)[OF None] by (simp add: map_idI)
next
case (Some a)
then obtain β tys where types: "sigF (f, length ts) = Some (tys, β)" by force
have l_zip: "length (zip ts tys) = length ts"
using length_zip[of ts tys] arity[OF types] by auto
{ fix i
assume "i < length ts"
hence "(λ(t, α). add_types t α ⋅ (λ(x, α). Var x)) ((zip ts tys) ! i) = ts ! i"
using 2(2)[OF types, of tys β "zip ts tys ! i" "ts ! i" "tys ! i"]
by (auto split: prod.splits)
(metis fst_conv snd_conv nth_mem nth_zip arity[OF types] l_zip)
}
thus ?thesis using types arity[OF types] zip_nth_conv
by (simp add: map_nth_eq_conv)
qed
qed auto
from join1' have join1'':
"(add_types b α ⋅ σ ⋅ τ ⋅ (λ(x, α). Var x), d ⋅ τ ⋅ (λ(x, α). Var x)) ∈ (rstep ℛ)⇧*"
proof (induction rule: converse_rtrancl_induct)
case (step y z)
have "(y ⋅ (λ(x, α). Var x), z ⋅ (λ(x, α). Var x)) ∈ rstep ℛ"
using rstep'_stable[OF step(1)] by (auto simp: rstep_eq_rstep')
thus ?case using step(3) by fastforce
qed auto
from join2' have join2'':
"(add_types c α ⋅ σ ⋅ τ ⋅ (λ(x, α). Var x), d ⋅ τ ⋅ (λ(x, α). Var x)) ∈ (rstep ℛ)⇧*"
proof (induction rule: converse_rtrancl_induct)
case (step y z)
have "(y ⋅ (λa. case a of (x, α) ⇒ Var x), z ⋅ (λa. case a of (x, α) ⇒ Var x)) ∈ rstep ℛ"
using rstep'_stable[OF step(1)] by (auto simp: rstep_eq_rstep')
thus ?case using step(3) by fastforce
qed auto
have "∀x∈vars_term (add_types a α). (σ ∘⇩s τ) x = Var x"
using inv_τ term_subst_eq_conv[of _ "σ ∘⇩s τ" Var] by simp
hence "add_types b α ⋅ σ ⋅ τ = add_types b α" "add_types c α ⋅ σ ⋅ τ = add_types c α"
using rstep'_sub_vars[OF _ wf] a_to_b' a_to_c' term_subst_eq_conv[of _ "σ ∘⇩s τ" Var] by auto
thus "(b, c) ∈ (rstep ℛ)⇧↓" using join1'' join2'' remove_types by auto
qed
text ‹The following lemma is the interesting direction of persistence of confluence @{cite ‹Theorem 5.13› FMZvO15}.›
lemma CR_persist:
assumes "∀α. CR_on (rstep ℛ) { t. 𝒯⇩α α t}"
shows "CR_on (rstep ℛ) 𝒯"
using assms by (rule CR[OF CR_on_union])
end
subsection ‹Persistent decomposition›
lemma (in persistent_cr) root_step_𝒯⇩α_in_ℛ⇩α:
assumes "𝒯⇩α α s" "(s, t) ∈ rrstep ℛ"
shows "(s, t) ∈ rrstep (ℛ⇩α α)"
proof -
obtain l r σ where lr: "(l, r) ∈ ℛ" "s = l ⋅ σ" "t = r ⋅ σ" using assms(2) by (auto elim: rrstepE)
then obtain β where β: "𝒯⇩α β l" "𝒯⇩α β r" using R_def by blast
have "β = α" using assms(1) β(1) lr(1) trs unfolding lr(2)
by (cases l) (auto simp: wf_trs_def elim!: 𝒯⇩α.cases)
then show ?thesis using β lr by auto
qed
context persistent_cr_infinite_vars
begin
interpretation persistent_nα: persistent_cr_infinite_vars sigF sigV "ℛ⇩n⇩α α"
using trs by (unfold_locales) (auto simp: wf_trs_def R_def inf_vars)
lemma nrrsteps_Fun_imp_arg_rsteps:
"(Fun f ss, Fun f ts) ∈ (nrrstep R)⇧* ⟹ i < length ss ⟹ (ss ! i, ts ! i) ∈ (rstep R)⇧*"
apply (induct "Fun f ts" arbitrary: ts rule: rtrancl_induct)
apply auto
by (metis (no_types, hide_lams) nrrsteps_imp_arg_rsteps rtrancl.rtrancl_into_rtrancl term.sel(4))
lemma persistent_decomposition:
assumes "⋀β. ℛ⇩n⇩α β = {} ∨ (∃α ∈ S. needed_types α β)"
shows "CR_on (rstep ℛ) 𝒯 ⟷ (∀α ∈ S. CR_on (rstep (ℛ⇩n⇩α α)) 𝒯)"
proof (intro iffI ballI, goal_cases L R)
case (L α) show ?case
proof (intro persistent_nα.CR_persist allI CR_onI, goal_cases peak)
case (peak β s t u) then show ?case unfolding mem_Collect_eq
proof (induct s arbitrary: β t u rule: wf_induct[OF SN_imp_wf[OF SN_supt]])
case (1 s) show ?case
proof (cases "needed_types α β")
case True
then have *: "persistent_nα.ℛ⇩n⇩α α β = ℛ⇩n⇩α β" by auto
have "CR_on (rstep (ℛ⇩n⇩α α)) {a. 𝒯⇩α β a}" using CR_persist'[OF L(1), of β]
unfolding CR_on_𝒯⇩α_by_needed_rules persistent_nα.CR_on_𝒯⇩α_by_needed_rules * .
then show ?thesis using 1(2,3,4) by (simp add: CR_on_def)
next
case False
have *: "persistent_nα.ℛ⇩α α β = {}" using False
by auto (metis ctxt_apply_term.simps(1) needed_types.trans needed_types_subt_at)
have "(s, t) ∈ (rstep (ℛ⇩n⇩α α))⇧* ⟹ 𝒯⇩α β s ⟹ (s, t) ∈ (nrrstep (ℛ⇩n⇩α α))⇧*" for s t
proof (induct rule: converse_rtrancl_induct)
case (step s s')
have "(s, s') ∈ nrrstep (ℛ⇩n⇩α α)" using step(1,4) persistent_nα.root_step_𝒯⇩α_in_ℛ⇩α[of β s s' α]
unfolding * by (auto simp: rstep_iff_rrstep_or_nrrstep)
moreover have "𝒯⇩α β s'" using step(1,4) conserv_𝒯⇩α[of β s s'] R_def by blast
ultimately show ?case using step(2,3) by auto
qed auto
note nrpeak = this[OF 1(3,2)] this[OF 1(4,2)]
show ?thesis using 1(2)
proof (cases β s rule: 𝒯⇩α.cases)
case (var x)
from NF_Var[OF persistent_nα.wf, of x] show ?thesis using var(1) 1(3,4)
by (auto elim: converse_rtranclE)
next
case (funs f ss tys)
obtain ts where t: "t = Fun f ts" "length ts = length ss" "⋀i. i < length ss ⟹ (ss ! i, ts ! i) ∈ (rstep (ℛ⇩n⇩α α))⇧*"
using nrpeak(1) nrrsteps_preserve_root' nrrsteps_Fun_imp_arg_rsteps unfolding funs(1)
by (metis (no_types, lifting))
obtain us where u: "u = Fun f us" "length us = length ss" "⋀i. i < length ss ⟹ (ss ! i, us ! i) ∈ (rstep (ℛ⇩n⇩α α))⇧*"
using nrpeak(2) nrrsteps_preserve_root' nrrsteps_Fun_imp_arg_rsteps unfolding funs(1)
by (metis (no_types, lifting))
show ?thesis using 1(1)[rule_format, OF _ funs(3)[rule_format] t(3) u(3)]
by (auto intro: args_joinable_imp_joinable simp: funs(1) t(1,2) u(1,2))
qed
qed
qed
qed
next
case R note R = this[rule_format] show ?case
proof (intro CR_persist[unfolded CR_on_𝒯⇩α_by_needed_rules] allI, goal_cases)
case (1 β)
consider (e) "ℛ⇩n⇩α β = {}" | (n) α where "α ∈ S" "needed_types α β"
using assms(1)[of β] by blast
then show ?case
proof (cases)
case e show ?thesis unfolding e by (auto simp: CR_on_def)
next
case n
have *: "persistent_nα.ℛ⇩n⇩α α β = ℛ⇩n⇩α β" using n(2) by auto
show ?thesis using persistent_nα.CR_persist'[OF R[OF n(1)], of β]
unfolding persistent_nα.CR_on_𝒯⇩α_by_needed_rules * .
qed
qed
qed
end
end