section ‹Preservation of confluence by currying›
theory LS_Currying
imports LS_Modularity QTRS.Position "Check-NT.Strongly_Closed"
begin
text ‹Here we instantiate the layer framework for currying.
See @{cite ‹Section 5.4› FMZvO15}.›
locale pp_cr =
fixes sigF :: "'f ⇒ nat option" and ℛ :: "('f, 'v :: infinite) trs" and Ap :: 'f
assumes
wfR: "wf_trs ℛ" and
fresh: "sigF Ap = None" and
sigR: "funas_trs ℛ ⊆ { (f, n) . sigF f = Some n }"
begin
definition ℱ where "ℱ ≡ { (f, n) . sigF f = Some n }"
definition ℱ⇩U where "ℱ⇩U ≡ { (Ap, 2) } ∪ { (f, m). (∃n. sigF f = Some n ∧ m ≤ n)}"
definition ℱ⇩C⇩u where "ℱ⇩C⇩u ≡ { (Ap, 2) } ∪ { (f, m). (∃n. sigF f = Some n ∧ m = 0)}"
definition 𝒰 where "𝒰 ≡ { (Fun Ap ((Fun f ts) # [t]), Fun f (ts @ [t]))
| f n ts (t :: ('f, 'v) term). (f, n) ∈ ℱ ∧ length ts < n ∧
is_Var t ∧ (∀t⇩i ∈ set ts. is_Var t⇩i) ∧ distinct (ts @ [t])}"
definition arity where "arity f ≡ the (sigF f)"
lemma root_ℛ_notAp:
assumes "(Fun f ts, r) ∈ ℛ"
shows "f ≠ Ap"
using assms sigR fresh unfolding funas_trs_def funas_rule_def by fastforce
lemma size_list_butlast[termination_simp]:
"xs ≠ [] ⟹ size_list f (butlast xs) = size_list f xs - Suc (f (last xs))"
using arg_cong[OF append_butlast_last_id[of xs], of "size_list f", unfolded size_list_append]
by auto
lemma size_list_non_empty_minus_Suc[termination_simp]:
"xs ≠ [] ⟹ size_list f xs - Suc y < size_list f xs"
by (cases xs) auto
fun Cu :: "('f, 'v) term ⇒ ('f, 'v) term" where
"Cu (Var x) = Var x"
| "Cu (Fun f []) = Fun f []"
| "Cu (Fun f (x # xs)) = (if f = Ap
then Fun Ap (map Cu (x # xs))
else Fun Ap [Cu (Fun f (butlast (x # xs))), Cu (last (x # xs))])"
lemma Cu_last1 [simp]:
"Cu (Fun Ap xs) = Fun Ap (map Cu xs)"
by (induction xs) auto
lemma Cu_last2 [simp]:
"f ≠ Ap ⟹ Cu (Fun f (xs @ [x])) = Fun Ap [Cu (Fun f xs), Cu x]"
by (induction xs) auto
lemma Cu_const [simp]: "Cu (Fun f ts) = Fun f' [] ⟹ f' = f ∧ ts = []"
by (cases "f = Ap"; cases "f' = Ap"; cases ts) auto
definition Cu⇩R where "Cu⇩R ≡ λR. { (Cu l, Cu r) | l r. (l, r) ∈ R }"
lemma vars_term_Cu [simp]: "vars_term (Cu t) = vars_term t"
proof (induction t)
case (Fun f ts) thus ?case
proof (cases "f = Ap")
case notAp: False thus ?thesis using Fun
proof (induction "length ts" arbitrary: ts)
case (Suc n)
then obtain ts' a where ts_def: "ts = ts' @ [a]"
by (metis append_Nil2 append_eq_conv_conj id_take_nth_drop lessI)
have "Cu (Fun f ts) = Fun Ap [Cu (Fun f ts'), Cu a]"
using notAp unfolding ts_def by simp
hence "vars_term (Cu (Fun f ts)) = vars_term (Fun f ts') ∪ vars_term a"
using Suc(1)[of ts'] Suc(2-) ts_def by auto
moreover have "vars_term (Fun f ts) = vars_term (Fun f ts') ∪ vars_term a"
unfolding ts_def by auto
ultimately show ?case unfolding ts_def by argo
qed simp
qed ((cases ts), simp+)
qed simp
lemma wf_rule_Cu:
assumes "wf_rule (l, r)"
shows "wf_rule (Cu l, Cu r)"
using assms vars_term_Cu unfolding wf_rule_def
by (cases l) (auto, (metis (full_types) Cu.cases Cu.simps is_FunI))
lemma wf_Cu: "wf_trs (Cu⇩R ℛ)"
proof -
{ fix l r
assume "(l, r) ∈ Cu⇩R ℛ"
then obtain l' r' where "l = Cu l'" "r = Cu r'" "(l', r') ∈ ℛ" by (auto simp: Cu⇩R_def)
hence "wf_rule (l, r)" using wfR wf_rule_Cu[of l' r']
by (auto simp: wf_trs_def wf_rule_def)
}
thus ?thesis unfolding wf_trs_def wf_rule_def by force
qed
lemma funas_Cu_helper:
assumes "f ≠ Ap"
shows "funas_term (Cu (Fun f ts)) ⊆ {(f, 0)} ∪ {(Ap, 2)} ∪ (⋃t∈set ts. funas_term (Cu t))"
using assms
proof (induction "length ts" arbitrary: f ts)
case (Suc n)
then obtain ts' a where ts_def: "ts = ts' @ [a]"
by (metis append_Nil2 append_eq_conv_conj id_take_nth_drop lessI)
show ?case
proof (cases "f = Ap")
case isAp: True
show ?thesis using Suc(3) fresh unfolding isAp ℱ_def by simp
next
case notAp: False
have Cu_unfold: "Cu (Fun f (ts' @ [a])) = Fun Ap [Cu (Fun f ts'), Cu a]"
using notAp unfolding ts_def by simp
hence "funas_term (Cu (Fun f ts')) ⊆ {(f, 0)} ∪ {(Ap, 2)} ∪ (⋃t∈set ts'. funas_term (Cu t))"
using Suc(1)[OF _ Suc(3), of ts'] Suc(2) unfolding ts_def by simp
thus ?thesis using notAp unfolding ts_def Cu_unfold by auto
qed
qed simp
lemma funas_Cu: "funas_term t ⊆ ℱ ⟹ funas_term (Cu t) ⊆ ℱ⇩C⇩u"
proof (induction t)
case (Fun f ts)
hence in_ℱ: "(f, length ts) ∈ ℱ" by simp
hence "f ≠ Ap" using fresh unfolding ℱ_def by force
hence "funas_term (Cu (Fun f ts)) ⊆ {(f, 0)} ∪ {(Ap, 2)} ∪ (⋃t∈set ts. funas_term (Cu t))"
using funas_Cu_helper[of f] by blast
moreover { fix x
assume "x ∈ set ts"
hence "funas_term (Cu x) ⊆ ℱ⇩C⇩u" using Fun by auto
}
ultimately show ?case using in_ℱ unfolding ℱ⇩C⇩u_def ℱ_def by auto
qed simp
lemma funas_Cu⇩R: "funas_trs (Cu⇩R ℛ) ⊆ ℱ⇩C⇩u"
using funas_Cu sigR unfolding funas_trs_def funas_rule_def Cu⇩R_def ℱ_def
by auto (fastforce, metis (no_types, lifting) rhs_wf set_mp sigR)
fun missing_args :: "('f, 'v) mctxt ⇒ nat ⇒ nat" where
"missing_args MHole n = 0"
| "missing_args (MVar x) n = 0"
| "missing_args (MFun f Cs) n = (if f = Ap ∧ length Cs = 2
then missing_args (Cs ! 0) (Suc n) else Suc (arity f) - length Cs - n)"
inductive 𝔏⇩1 :: "('f, 'v) mctxt ⇒ bool" where
mhole [intro]: "𝔏⇩1 MHole"
| mvar [intro]: "𝔏⇩1 (MVar x)"
| mfun [intro]: "(f, m) ∈ ℱ⇩U - { (Ap, 2) } ⟹ length Cs = m ⟹
(∀C' ∈ set Cs. 𝔏⇩1 C') ⟹ 𝔏⇩1 (MFun f Cs)"
| addAp [intro]: "𝔏⇩1 C ⟹ 𝔏⇩1 C' ⟹ missing_args C (Suc 0) ≥ 1 ⟹ 𝔏⇩1 (MFun Ap [C, C'])"
inductive 𝔏⇩2 :: "('f, 'v) mctxt ⇒ bool" where
mvarhole [intro]: "𝔏⇩1 C ⟹ x = MHole ∨ x = MVar v ⟹ 𝔏⇩2 (MFun Ap [x, C])"
definition 𝔏 :: "('f, 'v) mctxt set" where
"𝔏 ≡ { C. 𝔏⇩1 C ∨ 𝔏⇩2 C }"
fun check_first_non_Ap :: "nat ⇒ ('f, 'v) term ⇒ bool" where
"check_first_non_Ap n (Var x) = False"
| "check_first_non_Ap n (Fun f ts) = (if (f, length ts) = (Ap, 2)
then check_first_non_Ap (Suc n) (ts ! 0)
else arity f ≥ n + length ts)"
lemma missing_args_unfold:
"missing_args (mctxt_of_term t) n ≥ 1 ⟷ check_first_non_Ap n t"
by (induct n t rule: check_first_non_Ap.induct) auto
declare if_cong[cong]
fun max_top_cu :: "('f, 'v) term ⇒ ('f, 'v) mctxt" where
"max_top_cu (Var x) = MVar x"
| "max_top_cu (Fun f ts) = (if check_first_non_Ap 0 (Fun f ts)
then MFun f (map max_top_cu ts)
else MHole)"
fun max_top_cu' :: "nat ⇒ ('f, 'v) term ⇒ ('f, 'v) mctxt" where
"max_top_cu' n (Var x) = MVar x"
| "max_top_cu' n (Fun f ts) =
(if check_first_non_Ap n (Fun f ts)
then if f = Ap ∧ length ts = 2
then MFun Ap [max_top_cu' (Suc n) (ts ! 0), max_top_cu' 0 (ts ! 1)]
else MFun f (map (max_top_cu' 0) ts)
else MHole)"
lemma rules_missing_persist:
assumes "r ∈ ℛ ∪ 𝒰" "is_Fun (snd r)"
shows "missing_args (mctxt_of_term (fst r ⋅ σ)) n = missing_args (mctxt_of_term (snd r ⋅ σ)) n"
(is "missing_args ?l n = missing_args ?r n")
using assms(1)
proof
assume "r ∈ ℛ"
then obtain f ts g ss where rule_def: "fst r = Fun f ts" "snd r = Fun g ss"
using wfR assms(2) unfolding wf_trs_def by (metis is_Fun_Fun_conv prod.collapse)
hence arities: "sigF f = Some (length ts)" "sigF g = Some (length ss)"
using ‹r ∈ ℛ› sigR
unfolding funas_trs_def funas_rule_def by fastforce+
hence "f ≠ Ap" "g ≠ Ap" using fresh by fastforce+
thus ?thesis using rule_def arity_def arities by simp
next
assume "r ∈ 𝒰"
then obtain f ts t m i where rule_def:
"fst r = Fun Ap [Fun f ts, t]" "snd r = Fun f (ts @ [t])"
"(f, m) ∈ ℱ" "length ts = i" "i < m"
using 𝒰_def by force
from rule_def(3-) have "f ≠ Ap" using fresh unfolding ℱ_def by fastforce
thus ?thesis using rule_def by fastforce
qed
lemma check_first_non_Ap_persists:
assumes "check_first_non_Ap n t" "m ≤ n"
shows "check_first_non_Ap m t"
using assms
by (induction t arbitrary: m rule: check_first_non_Ap.induct) auto
lemma max_top_cu_equiv' [simp]:
"n = 0 ∨ check_first_non_Ap n t ⟹ max_top_cu' n t = max_top_cu t"
proof (induction t arbitrary: n)
case (Fun f ts) thus ?case
proof (cases "check_first_non_Ap n (Fun f ts)")
case True thus ?thesis
proof (cases "f = Ap ∧ length ts = 2")
case Ap2: True
hence "check_first_non_Ap (Suc 0) (ts ! 0)"
using check_first_non_Ap_persists[OF True, of 0] by auto
moreover have "max_top_cu' (Suc n) (ts ! 0) = max_top_cu (ts ! 0)"
using Ap2 Fun(1)[of "ts ! 0" "Suc n"] Fun(2) True by auto
moreover have "max_top_cu' 0 (ts ! 1) = max_top_cu (ts ! 1)"
using Fun True Ap2 by force
moreover have " map max_top_cu ts = [max_top_cu (ts ! 0), max_top_cu (ts ! Suc 0)]"
using Ap2 unfolding map_eq_Cons_conv[of max_top_cu ts]
by (metis Cons_nth_drop_Suc Suc_leI drop_all lessI list.simps(8,9)
nth_drop_0 numeral_2_eq_2 one_add_one zero_less_two)
ultimately show ?thesis using True Ap2 by auto
next
case not_Ap2: False
thus ?thesis using Fun
by (cases "check_first_non_Ap n (Fun f ts)") auto
qed
next
case False
thus ?thesis using Fun by force
qed
qed simp
lemma max_top_cu_equiv [simp]: "max_top_cu' 0 t = max_top_cu t"
using max_top_cu_equiv' by fast
declare if_cong[cong del]
fun max_top_curry :: "('f, 'v) term ⇒ ('f, 'v) mctxt" where
"max_top_curry (Var x) = MVar x"
| "max_top_curry (Fun f ts) = (if check_first_non_Ap 0 (Fun f ts) ∨ (∃x. ts ! 0 = Var x)
then MFun f (map max_top_cu ts)
else MFun f [MHole, max_top_cu (ts ! 1)])"
lemma max_top_curry_cu_equiv [simp]: "check_first_non_Ap 0 (Fun f ts) ⟷
max_top_curry (Fun f ts) = max_top_cu (Fun f ts)"
by simp
lemma wfU: "wf_trs 𝒰"
unfolding 𝒰_def wf_trs_def by force
lemma sigU: "funas_trs 𝒰 ⊆ ℱ⇩U"
proof
fix f m
assume "(f, m) ∈ funas_trs 𝒰"
then obtain r where r_in_𝒰: "r ∈ 𝒰" "(f, m) ∈ funas_rule r" unfolding 𝒰_def funas_trs_def by blast
then obtain f' n i x ts t where r_props: "r = (Fun Ap [Fun f' ts, t], Fun f' (ts @ [t]))"
"(f', n) ∈ ℱ" "i < n" "t = Var x" "length ts = i" "∀t⇩i ∈ set ts. is_Var t⇩i"
using 𝒰_def by force
then consider "f = Ap ∧ m = 2" | "f = f' ∧ m = i" | "f = f' ∧ m = i + 1" |
"∃x∈set ts. (f, m) ∈ funas_term x"
using ℱ⇩U_def r_in_𝒰 unfolding funas_rule_def by simp linarith
thus "(f, m) ∈ ℱ⇩U" using r_props unfolding ℱ⇩U_def ℱ_def is_Var_def by (cases) auto
qed
lemma list1_map:
assumes "length ls = Suc 0"
shows "[f (ls ! 0)] = map f ls"
using assms[symmetric] unfolding Suc_length_conv by force
lemma list2_props:
assumes "P (ls ! 0) ∧ R (ls ! 1)" "length ls = 2"
shows "∃a b. ls = [a, b] ∧ P a ∧ R b"
using assms by (metis Cons_nth_drop_Suc One_nat_def Suc_leI
drop_all lessI nth_drop_0 numeral_2_eq_2 one_add_one zero_less_two)
lemma pos_mreplace_at:
assumes "p ∈ all_poss_mctxt C" "mreplace_at C p D = MFun f Cs"
"D = MHole ∨ (∃x. D = MVar x)"
shows "∃i p' Cs'. p = i <# p' ∧ i < length Cs ∧ C = MFun f Cs' ∧
p' ∈ all_poss_mctxt (Cs' ! i) ∧ i < length Cs' ∧
Cs = (take i Cs') @ mreplace_at (Cs' ! i) p' D # drop (i+1) Cs'"
using assms
proof (cases C)
case (MFun f' Cs')
thus ?thesis using assms by (cases p) (auto simp: nth_append_take)
qed auto
lemma mreplace_at_eps:
assumes "p ∈ all_poss_mctxt C" "∃x y. mreplace_at C p x = y ∧
(x = MHole ∨ (∃x'. x = MVar x')) ∧ (y = MHole ∨ (∃x'. y = MVar x'))"
shows "p = ε"
using assms
proof (induction C)
case (MFun f Cs)
thus ?case by force
qed auto
lemma replace_in_missing_args:
assumes "p ∈ all_poss_mctxt C"
"x = MHole ∨ (∃v. x = MVar v)" "y = MHole ∨ (∃v'. y = MVar v')"
shows "missing_args (mreplace_at C p y) n = missing_args (mreplace_at C p x) n"
using assms
proof (induction "mreplace_at C p x" n arbitrary: C p rule: missing_args.induct)
case (1 n)
hence "p = ε" using mreplace_at_eps by metis
thus ?case using 1 by force
next
case (2 x n)
hence "p = ε" using mreplace_at_eps by metis
thus ?case using 2 by force
next
case (3 f Cs n)
obtain Cs' where Cs'_props: "mreplace_at C p y = MFun f Cs'" "length Cs = length Cs'"
using 3(2-) by (cases C) force+
thus ?case
proof (cases "f = Ap ∧ length Cs = 2")
case True
thus ?thesis
proof (cases p)
case Empty
thus ?thesis using 3(2-) by fastforce
next
case (PCons i p')
obtain Ds where Ds_props: "C = MFun f Ds" "Cs ! i = mreplace_at (Ds ! i) p' x"
"p' ∈ all_poss_mctxt (Ds ! i)"
using pos_mreplace_at[OF 3(3) 3(2)[symmetric] 3(4)]
unfolding PCons by (metis less_imp_le_nat nth_append_take pos.inject)
consider "i = 0" | "i = 1" using True 3(2,3) less_numeral_extra(2)
unfolding Ds_props(1) PCons by force
thus ?thesis
proof (cases)
case 1
have "Cs' ! 0 = mreplace_at (Ds ! 0) p' y"
using 3(4) Cs'_props(1) Ds_props unfolding PCons 1 by auto
moreover have "missing_args (mreplace_at (Ds ! 0) p' y) (Suc n) =
missing_args (mreplace_at (Ds ! 0) p' x) (Suc n)"
using Ds_props 3(1)[OF True] 3(4,5) unfolding 1 by auto
ultimately show ?thesis using Ds_props True
unfolding PCons 1 by auto
next
case 2
have "Cs ! 0 = Ds ! 0" using 3(2,3) unfolding Ds_props(1) PCons 2
by (simp add: nth_append_take_is_nth_conv)
moreover have "Cs' ! 0 = Ds ! 0" using 3(3) Cs'_props(1)[symmetric]
unfolding Ds_props(1) PCons 2
by (simp add: nth_append_take_is_nth_conv)
ultimately have "missing_args (Cs' ! 0) (Suc n) = missing_args (Cs ! 0) (Suc n)"
using 3(2,3) missing_args.simps(3)[of f _ n] True
unfolding Ds_props(1) PCons 2 by metis
thus ?thesis using missing_args.simps(3)[of f _ n] True Cs'_props 3(2)
unfolding Ds_props(1) PCons 2 by metis
qed
qed
next
case False
thus ?thesis using 3(2) Cs'_props
by (metis missing_args.simps(3))
qed
qed
lemma replace_var_holes1_helper:
assumes "𝔏⇩1 (mreplace_at C p x)" and "p ∈ all_poss_mctxt C" and
x_def: "x = MHole ∨ (∃v. x = MVar v)" and y_def: "y = MHole ∨ (∃v'. y = MVar v')"
shows "𝔏⇩1 (mreplace_at C p y)"
using assms
proof (induction "(mreplace_at C p x)" arbitrary: C p rule: "𝔏⇩1.induct")
case mhole thus ?case by (cases C) auto
next
case mvar thus ?case by (cases C) auto
next
case (mfun f m Cs) thus ?case
proof (induction p)
case (PCons i p)
from PCons(5-6) obtain Cs' where C_def: "C = MFun f Cs'" "length Cs = length Cs'"
"i < length Cs'" "p ∈ all_poss_mctxt (Cs' ! i)"
"Cs = (take i Cs') @ mreplace_at (Cs' ! i) p x # drop (i+1) Cs'" by (cases C) auto
moreover have "Cs ! i = mreplace_at (Cs' ! i) p x"
using C_def(2-) PCons(5-6) unfolding C_def(1) by (simp add: nth_append_take)
moreover have "Cs ! i ∈ set Cs" using PCons(6) C_def(1-2) by simp
ultimately have in_𝔏⇩1: "𝔏⇩1 (mreplace_at (Cs' ! i) p y)" using PCons(4,7,8) by blast
let ?Cs' = "(take i Cs') @ mreplace_at (Cs' ! i) p y # drop (i+1) Cs'"
have "∀C'∈set Cs. 𝔏⇩1 C'" using mfun(3) by blast
hence "∀C'∈set ?Cs'. 𝔏⇩1 C'" using in_𝔏⇩1 C_def nth_mem[OF C_def(3)]
append_Cons_nth_not_middle by auto
thus ?case using in_𝔏⇩1 mfun(1-2) 𝔏⇩1.mfun unfolding C_def(1,5) by simp
qed auto
next
case (addAp C' C'') thus ?case
proof (induction p)
case (PCons i p)
from PCons(7,8) obtain D where C_def:
"(C = MFun Ap [C', D] ∧ C'' = mreplace_at D p x ∧ i = 1) ∨
(C = MFun Ap [D, C''] ∧ C' = mreplace_at D p x ∧ i = 0)"
"p ∈ all_poss_mctxt D" by (cases C) (auto simp: Cons_eq_append_conv,
(metis length_greater_0_conv nth_drop_0),
(metis Cons_nth_drop_Suc append_Cons append_Nil append_take_drop_id
length_Cons less_antisym list.size(3) not_Cons_self2 take_eq_Nil))
from C_def(1) show ?case
proof (elim disjE)
assume in_C'': "C = MFun Ap [C', D] ∧ C'' = mreplace_at D p x ∧ i = 1"
hence in_𝔏⇩1: "𝔏⇩1 (mreplace_at D p y)" using PCons(5) C_def(2) in_C'' x_def y_def by auto
show ?thesis using 𝔏⇩1.addAp[OF PCons(2) in_𝔏⇩1 PCons(6)] in_C'' C_def(2) by simp
next
assume in_C': "C = MFun Ap [D, C''] ∧ C' = mreplace_at D p x ∧ i = 0"
hence in_𝔏⇩1: "𝔏⇩1 (mreplace_at D p y)" using PCons(3) C_def(2) x_def y_def by auto
have "missing_args (mreplace_at D p y) (Suc 0) ≥ 1"
using replace_in_missing_args[OF C_def(2) x_def y_def, of "Suc 0"] PCons(6) in_C' by argo
thus ?thesis using 𝔏⇩1.addAp[OF in_𝔏⇩1 PCons(4)] in_C' C_def(2) by simp
qed
qed auto
qed
lemma replace_var_holes1:
assumes "p ∈ all_poss_mctxt C" and x_def: "x = MHole ∨ (∃v. x = MVar v)"
and y_def: "y = MHole ∨ (∃v'. y = MVar v')"
shows "𝔏⇩1 (mreplace_at C p x) = 𝔏⇩1 (mreplace_at C p y)"
using assms(2-) replace_var_holes1_helper[OF _ assms(1)] by metis
lemma replace_var_holes2_helper:
assumes "𝔏⇩2 (mreplace_at C p x)" and "p ∈ all_poss_mctxt C" and
x_def: "x = MHole ∨ (∃v. x = MVar v)" and y_def: "y = MHole ∨ (∃v'. y = MVar v')"
shows "𝔏⇩2 (mreplace_at C p y)"
using assms
proof (induction "(mreplace_at C p x)" arbitrary: C p rule: "𝔏⇩2.induct")
case (mvarhole C' x' v)
let ?Cs = "[x', C']"
from mvarhole(3-) obtain i p' Cs where props: "p = i <# p'" "i < length ?Cs"
"C = MFun Ap Cs" "p' ∈ all_poss_mctxt (Cs ! i)" "i < length Cs"
"?Cs = (take i Cs) @ mreplace_at (Cs ! i) p' x # drop (i+1) Cs"
using pos_mreplace_at[OF mvarhole(4) mvarhole(3)[symmetric]] by blast
have lengths: "length Cs = length ?Cs" using props by force
have var_occurs: "subm_at (mreplace_at (Cs ! i) p' x) p' = x"
using subm_at_mreplace_at props(4) all_poss_mctxt_conv by blast
consider "i = 0" | "i = 1" using props(2) by fastforce
thus ?case
proof cases
case i0: 1
hence is_x': "mreplace_at (Cs ! 0) p' x = x'" using props(6) by simp
hence "p' ∈ all_poss_mctxt x'" using props(4) all_poss_mctxt_conv
var_occurs all_poss_mctxt_mreplace_atI1[of p' "Cs ! 0" p' x] unfolding i0 by force
thus ?thesis using lengths var_occurs mvarhole(1,2) props(6) x_def y_def
unfolding i0 is_x' props(1,3)
by (metis (no_types, lifting) Cons_eq_append_conv 𝔏⇩2.mvarhole list.inject
mreplace_at.simps(1) mreplace_at.simps(2) mreplace_at_eps mvarhole.hyps(1)
replace_at_subm_at take_eq_Nil)
next
case i1: 2
have C'_def: "C' = mreplace_at (Cs ! i) p' x"
using mvarhole(2-) props unfolding ‹i = 1›
by simp (metis (no_types) less_imp_le_nat nth_Cons_0 nth_Cons_Suc nth_append_take)
hence "𝔏⇩1 (mreplace_at (Cs ! i) p' y)"
using mvarhole(1) replace_var_holes1[OF props(4)] x_def y_def by blast
moreover have "mreplace_at C p y = MFun Ap [x', mreplace_at (Cs ! i) p' y]"
using mvarhole(3-) props(2-) lengths
unfolding props(1,3) i1 C'_def by simp
ultimately show ?thesis using mvarhole(2) by auto
qed
qed
lemma replace_var_holes2:
assumes "p ∈ all_poss_mctxt C" and x_def: "x = MHole ∨ (∃v. x = MVar v)"
and y_def: "y = MHole ∨ (∃v'. y = MVar v')"
shows "𝔏⇩2 (mreplace_at C p x) = 𝔏⇩2 (mreplace_at C p y)"
using assms(2-) replace_var_holes2_helper[OF _ assms(1)] by metis
lemma sub_layers:
assumes "MFun f Cs ∈ 𝔏" "i < length Cs"
shows "𝔏⇩1 (Cs ! i)"
proof -
consider "𝔏⇩1 (MFun f Cs)" | "𝔏⇩2 (MFun f Cs)" using assms(1) unfolding 𝔏_def by blast
thus ?thesis
proof cases
case 1 thus ?thesis using assms(2) 𝔏_def
proof (cases "MFun f Cs" rule: 𝔏⇩1.cases)
case (addAp C C')
thus ?thesis using assms(2) 𝔏_def less_2_cases numeral_2_eq_2 by fastforce
qed simp
next
case 2
thus ?thesis using assms(2) 𝔏_def
using 𝔏⇩2.simps[of "MFun f Cs"] less_2_cases[of i] by fastforce
qed
qed
lemma subm_at_layers [simp]:
assumes "L ∈ 𝔏" "p ∈ all_poss_mctxt L"
shows "subm_at L p ∈ 𝔏 ∧ (p ≠ ε ⟶ 𝔏⇩1 (subm_at L p))"
using assms sub_layers unfolding 𝔏_def
proof (induction L arbitrary: p)
case (MFun f Cs)
thus ?case by (cases p) (simp+, (metis nth_mem subm_at.simps(1)))
qed auto
lemma disjoint:
shows "¬ (𝔏⇩1 L ∧ 𝔏⇩2 L)"
proof
assume "𝔏⇩1 L ∧ 𝔏⇩2 L"
thus "False" unfolding 𝔏⇩1.simps[of L] 𝔏⇩2.simps[of L] by fastforce
qed
lemma missing_args_persist:
fixes L N :: "('f, 'v) mctxt"
assumes missing: "missing_args L n ≥ 1" and
comp: "(L, N) ∈ comp_mctxt"
shows "missing_args (L ⊔ N) n = missing_args L n"
proof -
from missing obtain f Cs where L_def: "L = MFun f Cs"
by (metis check_first_non_Ap.simps(1) mctxt.exhaust mctxt_of_term.simps(1)
missing_args.simps(1) missing_args_unfold not_one_le_zero)
show ?thesis using assms unfolding L_def
proof (induction N arbitrary: f Cs n)
case (MVar x)
show ?case using MVar(2) unfolding MVar(1) using comp_mctxt.cases by blast
next
case (MFun f' Cs')
have comp_cond: "f = f'" "length Cs = length Cs'"
"∀ i < length Cs'. (Cs ! i, Cs' ! i) ∈ comp_mctxt"
using comp_mctxt.cases[OF MFun(3)] by fast+
consider "f = Ap ∧ length Cs = 2" "missing_args (Cs ! 0) (Suc n) ≥ 1" |
"¬(f = Ap ∧ length Cs = 2)" "Suc (arity f) - length Cs - n ≥ 1"
using missing_args.simps(3)[of f Cs n] MFun(2) by presburger
thus ?case
proof cases
case 1
thus ?thesis
proof (cases "Cs ! 0")
case gDs: (MFun g Ds)
have Cs'_0: "Cs' ! 0 ∈ set Cs'" using "1"(1) comp_cond(2) by auto
have "MFun f Cs ⊔ MFun f' Cs' = MFun Ap (map (λ(x, y). x ⊔ y) (zip Cs Cs'))"
using 1 comp_cond(1,2) by force
thus ?thesis using MFun(1)[OF Cs'_0, of g Ds "Suc n"] gDs MFun(3) 1 comp_cond
by fastforce
qed auto
next
case 2
thus ?thesis using MFun(3) comp_cond by force
qed
qed simp
qed
lemma merge_𝔏⇩1:
assumes "𝔏⇩1 L" "(L, N) ∈ comp_mctxt" "N ∈ 𝔏"
shows "L ≠ MHole ⟶ 𝔏⇩1 (L ⊔ N)"
using assms
proof (induction L arbitrary: N rule: 𝔏⇩1.induct)
case (mvar x)
thus ?case by (metis 𝔏⇩1.simps less_eq_mctxt_MVarE1 sup_mctxt_ge1)
next
case (mfun f m Cs)
thus ?case
proof (cases N)
case (MFun f' Cs')
hence similar: "f = f' ∧ length Cs = length Cs'"
using mfun(4) by (auto elim: comp_mctxt.cases)
have N_in_𝔏⇩1: "𝔏⇩1 (MFun f' Cs')" "(f', length Cs') ≠ (Ap, 2)" using similar mfun(1,2,5) 𝔏⇩2.simps
unfolding MFun 𝔏_def by auto
let ?Cs = "map (case_prod sup) (zip Cs Cs')"
have sup_def: "MFun f Cs ⊔ MFun f' Cs' = MFun f ?Cs"
using similar mfun(1,2,4) by simp
have length_combined: "length ?Cs = length Cs" "length ?Cs = length (zip Cs Cs')"
using similar by simp+
{ fix i
assume i_assm: "i < length Cs"
moreover have "𝔏⇩1 (Cs ! i)" using mfun(3) nth_mem i_assm by blast
moreover have "(Cs ! i, Cs' ! i) ∈ comp_mctxt"
using mfun(4) ‹i < length Cs› unfolding MFun by (auto elim: comp_mctxt.cases)
moreover have "𝔏⇩1 (Cs' ! i)" using sub_layers[OF mfun(5)[unfolded MFun]] i_assm similar by simp
ultimately have "𝔏⇩1 (Cs ! i ⊔ Cs' ! i)" using mfun(3) nth_mem unfolding 𝔏_def
by (cases "Cs ! i") fastforce+
}
thus ?thesis using similar mfun(2) length_combined nth_map[of _ "zip Cs Cs'" "case_prod sup"]
nth_zip[of _ Cs Cs'] 𝔏⇩1.mfun[OF mfun(1), of ?Cs] unfolding MFun sup_def
by (metis (mono_tags, lifting) all_nth_imp_all_set old.prod.case)
qed (auto elim: comp_mctxt.cases)
next
case (addAp C C') thus ?case
proof (cases N)
case (MFun f' Cs')
have Cs'_props: "length Cs' = 2" "∀i < length Cs'. ([C, C'] ! i, Cs' ! i) ∈ comp_mctxt" "f' = Ap"
using comp_mctxt.cases[OF addAp(6)] unfolding MFun
by (simp, metis length_Cons list.size(3) numeral_2_eq_2, auto)
have in_𝔏: "∀i < length Cs'. Cs' ! i ∈ 𝔏"
using sub_layers[OF addAp(7)[unfolded MFun]] 𝔏_def by simp
obtain g Ds where C_def: "C = MFun g Ds" using addAp(3)
by (metis mctxt.exhaust missing_args.simps(1) missing_args.simps(2) not_one_le_zero)
obtain C⇩1 C⇩2 where Cs'_def: "Cs' = [C⇩1, C⇩2]" using Cs'_props(1)
by (metis (no_types, lifting) length_0_conv length_Suc_conv numeral_2_eq_2)
have "𝔏⇩1 (C ⊔ C⇩1)" using Cs'_props(2) addAp(1,4) in_𝔏 unfolding Cs'_def C_def by fastforce
consider "𝔏⇩1 N" | "𝔏⇩2 N" using addAp(7) unfolding MFun 𝔏_def by blast
hence "𝔏⇩1 C⇩2" unfolding MFun Cs'_def
proof cases
case 1
thus ?thesis by (auto elim: 𝔏⇩1.cases)
next
case 2
thus ?thesis by (auto elim: 𝔏⇩2.cases)
qed
hence "𝔏⇩1 (C' ⊔ C⇩2)" using Cs'_props(2) addAp(2,5) in_𝔏 unfolding Cs'_def C_def
by (metis length_Cons lessI list.size(3) nth_Cons_0 nth_Cons_Suc
sup_mctxt_MHole sup_mctxt_comm)
have "(C, C⇩1) ∈ comp_mctxt" using Cs'_def Cs'_props(2) by auto
hence "missing_args (C ⊔ C⇩1) (Suc 0) ≥ 1" using missing_args_persist[OF addAp(3)]
using addAp.hyps(3) by auto
thus ?thesis using ‹𝔏⇩1 (C ⊔ C⇩1)› ‹𝔏⇩1 (C' ⊔ C⇩2)› Cs'_props(2,3) unfolding MFun Cs'_def by auto
qed (auto elim: comp_mctxt.cases)
qed auto
lemma merge_𝔏⇩2:
assumes "𝔏⇩2 L" "𝔏⇩2 N" "(L, N) ∈ comp_mctxt"
shows "𝔏⇩2 (L ⊔ N)"
proof -
obtain x C where L_def: "L = MFun Ap [x, C]" and "𝔏⇩1 C"
and x_def: "x = MHole ∨ (∃x'. x = MVar x')"
using 𝔏⇩2.cases[OF assms(1)] by metis
obtain y C' where N_def: "N = MFun Ap [y, C']" and "𝔏⇩1 C'"
and y_def: "y = MHole ∨ (∃y'. y = MVar y')"
using 𝔏⇩2.cases[OF assms(2)] by metis
have comp: "(x, y) ∈ comp_mctxt" "(C, C') ∈ comp_mctxt"
using comp_mctxt.cases[OF ‹(L, N) ∈ comp_mctxt›] unfolding L_def N_def
by (-, simp, (metis (no_types) length_Cons nth_Cons_0 zero_less_Suc),
simp, (metis length_Cons lessI list.size(3) nth_Cons_0 nth_Cons_Suc))
have "𝔏⇩1 (C ⊔ C')" using merge_𝔏⇩1[OF ‹𝔏⇩1 C› comp(2)] ‹𝔏⇩1 C'› 𝔏_def unfolding N_def by auto
moreover have "x ⊔ y = MHole ∨ (∃z. x ⊔ y = MVar z)"
using x_def y_def comp_mctxt.cases[OF comp(1)] by fastforce
ultimately show ?thesis using 𝔏_def x_def y_def unfolding L_def N_def by force
qed
lemma missing_mreplace:
assumes "missing_args C n ≥ 1" "∀n. missing_args (subm_at C p) n ≥ 1 ⟶ missing_args D n ≥ 1"
"p ∈ all_poss_mctxt C"
shows "missing_args (mreplace_at C p D) n ≥ 1"
using assms
proof (induction C p D arbitrary: n rule: mreplace_at.induct)
case (2 f Cs i p D)
let ?Cs = "take i Cs @ mreplace_at (Cs ! i) p D # drop (Suc i) Cs"
have length: "i < length Cs" using 2(4) by (auto simp: funposs_mctxt_def)
hence lengths: "length ?Cs = length Cs" by auto
show ?case
proof (cases "f = Ap ∧ length Cs = 2")
case True
hence missing: "missing_args (Cs ! 0) (Suc n) ≥ 1" using 2(2) by simp
consider "i = 0" | "i = 1" using True length by fastforce
thus ?thesis
proof cases
case i0: 1
have "∀n. missing_args (subm_at (Cs ! 0) p) n ≥ 1 ⟶ missing_args D n ≥ 1"
using 2(3) by (simp add: i0)
moreover have "p ∈ all_poss_mctxt (Cs ! i)"
using 2(4) length unfolding funposs_mctxt_def by simp
ultimately have "missing_args (mreplace_at (Cs ! 0) p D) (Suc n) ≥ 1"
using 2(1)[unfolded i0, OF missing] length unfolding i0 by fast
thus ?thesis using True unfolding i0 by force
next
case i1: 2
show ?thesis using True missing unfolding i1
by (simp add: nth_append_take_is_nth_conv)
qed
next
case False
hence "Suc (arity f) - length Cs - n ≥ 1" using 2(2) by (simp add: False)
thus ?thesis using lengths False mreplace_at.simps(2)[of f Cs i p]
missing_args.simps(3)[of f ?Cs n] by (metis Suc_eq_plus1)
qed
qed auto
lemma replace_𝔏⇩1:
assumes "𝔏⇩1 L" "𝔏⇩1 (subm_at L p)" "𝔏⇩1 N" "p ∈ all_poss_mctxt L" and
missing: "∀n. missing_args (subm_at L p) n ≥ 1 ⟶ missing_args N n ≥ 1"
shows "𝔏⇩1 (mreplace_at L p N)"
using assms unfolding 𝔏_def
proof (induction L p N rule: mreplace_at.induct)
case (2 f Cs i p D)
let ?Cs = "take i Cs @ mreplace_at (Cs ! i) p D # drop (Suc i) Cs"
have length: "i < length Cs" using 2(5) by (auto simp: funposs_mctxt_def)
hence lengths: "length ?Cs = length Cs" by auto
have in_𝔏⇩1: "𝔏⇩1 (Cs ! i) ⟶ 𝔏⇩1 (mreplace_at (Cs ! i) p D)" using 2 unfolding 𝔏_def
by (auto simp: funposs_mctxt_def)
from 2(2) show ?case
proof (cases rule: 𝔏⇩1.cases[of "MFun f Cs"])
case (mfun m)
hence "(f, length ?Cs) ∈ ℱ⇩U - {(Ap, 2)}" using length lengths by simp
moreover have "Ball (set ?Cs) 𝔏⇩1" using in_𝔏⇩1 length lengths mfun(3)
by (metis in_set_conv_nth less_imp_le_nat nth_append_take nth_append_take_drop_is_nth_conv)
ultimately have "𝔏⇩1 (MFun f ?Cs)" by blast
thus ?thesis by (metis Suc_eq_plus1 mreplace_at.simps(2))
next
case (addAp C C')
then consider "i = 0" | "i = 1" using length by fastforce
thus ?thesis
proof cases
case i0: 1
have "missing_args (mreplace_at C p D) (Suc 0) ≥ 1"
using addAp(5) 2(5,6) missing_mreplace[OF addAp(5), of p D]
unfolding addAp(2) i0 funposs_mctxt_def by simp
thus ?thesis using 2(3-) addAp(3-) in_𝔏⇩1 unfolding i0 addAp(1,2) by auto
next
case i1: 2
show ?thesis using addAp(3-5) in_𝔏⇩1 unfolding i1 addAp(1,2) by auto
qed
qed
qed (auto simp: funposs_mctxt_def)
lemma replace_𝔏⇩2:
assumes "𝔏⇩2 L" "𝔏⇩1 (subm_at L p)" "𝔏⇩1 N" "p ∈ funposs_mctxt L ∨ (p ∈ all_poss_mctxt L ∧ p ≠ <0>)" and
missing: "∀n. missing_args (subm_at L p) n ≥ 1 ⟶ missing_args N n ≥ 1"
shows "(mreplace_at L p N) ∈ 𝔏"
using assms unfolding 𝔏_def
proof (induction L p N rule: mreplace_at.induct)
case (2 f Cs i p D)
let ?Cs = "take i Cs @ mreplace_at (Cs ! i) p D # drop (Suc i) Cs"
have length: "i < length Cs" using 2(5) by (auto simp: funposs_mctxt_def)
hence lengths: "length ?Cs = length Cs" by auto
from 2(2) show ?case
proof (cases rule: 𝔏⇩2.cases[of "MFun f Cs"])
case (mvarhole C x v)
consider "i = 0" | "i = 1" using mvarhole(2) length by fastforce
thus ?thesis
proof cases
case i0: 1
show ?thesis using 2(5) mvarhole(4) unfolding i0 mvarhole(1,2) funposs_mctxt_def by auto
next
case i1: 2
show ?thesis using replace_𝔏⇩1[OF mvarhole(3) _ 2(4), of p] 2(3,5,6) mvarhole(4)
funposs_mctxt_subset_all_poss_mctxt[of "C"]
unfolding i1 mvarhole(1,2) funposs_mctxt_def by auto
qed
qed
qed (auto simp: funposs_mctxt_def)
lemma pp_layer_system: "layer_system ℱ⇩U 𝔏"
proof
show "𝔏 ⊆ layer_system_sig.𝒞 ℱ⇩U"
proof
fix C
assume "C ∈ 𝔏"
{ fix C
assume "𝔏⇩1 C"
hence "C ∈ layer_system_sig.𝒞 ℱ⇩U" unfolding layer_system_sig.𝒞_def
by (induction C) (auto simp: ℱ⇩U_def)
} note 𝔏⇩1_case = this
{ assume "𝔏⇩2 C"
hence "C ∈ layer_system_sig.𝒞 ℱ⇩U" using 𝔏⇩1_case
unfolding layer_system_sig.𝒞_def ℱ⇩U_def by (induction C) auto
} note 𝔏⇩2_case = this
from ‹C ∈ 𝔏› consider "𝔏⇩1 C" | "𝔏⇩2 C" unfolding 𝔏_def by blast
thus "C ∈ layer_system_sig.𝒞 ℱ⇩U" using 𝔏⇩1_case 𝔏⇩2_case by cases
qed
next
fix t :: "('f, 'v) term"
assume funas_t: "funas_term t ⊆ ℱ⇩U"
thus "∃L∈𝔏. L ≠ MHole ∧ L ≤ mctxt_of_term t"
proof (cases t)
case (Var x)
hence "mctxt_of_term t ≠ MHole ∧ mctxt_of_term t ≤ mctxt_of_term t" by simp
moreover have "𝔏⇩1 (mctxt_of_term t)" using Var by auto
ultimately show ?thesis using 𝔏_def by blast
next
case (Fun f Cs)
hence length_Cs: "(f, length Cs) ∈ ℱ⇩U" using funas_t unfolding ℱ⇩U_def by simp
let ?top = "MFun f (replicate (List.length Cs) MHole)"
have cond: "?top ≠ MHole ∧ ?top ≤ mctxt_of_term t"
using Fun by (auto simp: less_eq_mctxt_def o_def map_replicate_const)
moreover have "?top ∈ 𝔏"
proof (cases "f = Ap")
case isAp: True
have "replicate 2 MHole = [MHole, MHole]" by (simp add: numeral_2_eq_2)
hence "𝔏⇩2 ?top" using isAp Fun length_Cs ℱ⇩U_def fresh by (auto simp: 𝔏⇩2.simps)
thus ?thesis using 𝔏_def by simp
next
case notAp: False
hence "(f, length Cs) ∈ ℱ⇩U - { (Ap, 2) }" using funas_t Fun by simp
hence "𝔏⇩1 ?top" using Fun length_Cs ℱ⇩U_def by fastforce
thus ?thesis using 𝔏_def by simp
qed
ultimately show ?thesis using 𝔏_def by blast
qed
next
fix C :: "('f, 'v) mctxt" and p :: pos and x :: 'v
assume p_in_possC: "p ∈ poss_mctxt C"
thus "(mreplace_at C p (MVar x) ∈ 𝔏) = (mreplace_at C p MHole ∈ 𝔏)"
using 𝔏_def replace_var_holes1 replace_var_holes2 all_poss_mctxt_conv[of C] by fastforce
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"
consider "p = ε ∧ 𝔏⇩2 (subm_at L p)" | "𝔏⇩1 (subm_at L p)" using subm_at_layers[OF ‹L ∈ 𝔏›]
p_in_funposs funposs_mctxt_subset_all_poss_mctxt disjoint 𝔏_def by blast
thus "mreplace_at L p (subm_at L p ⊔ N) ∈ 𝔏"
proof cases
case 1
consider "𝔏⇩1 N" | "𝔏⇩2 N" using ‹N ∈ 𝔏› 𝔏_def by blast
thus ?thesis
proof cases
case N1: 1
have "(N ⊔ L) ∈ 𝔏"
using 1 𝔏_def merge_𝔏⇩1[OF N1 comp_mctxt_sym[OF comp_context]] sup_mctxt_MHole[of N]
by (cases N) force+
thus ?thesis using sup_mctxt_comm[of N L] 1 by simp
next
case N2: 2
show ?thesis using merge_𝔏⇩2[OF _ N2 comp_context] 1 𝔏_def sup_mctxt_comm[of L N]
by fastforce
qed
next
case 2
obtain f Cs where "subm_at L p = MFun f Cs"
using p_in_funposs funposs_mctxt_def[of L] funposs_fun_conv
by (metis funposs_imp_poss poss_mctxt_term_conv subm_at_subt_at_conv term_mctxt_conv.simps(3))
hence in_𝔏⇩1: "𝔏⇩1 (subm_at L p ⊔ N)" using merge_𝔏⇩1[OF 2 comp_context ‹N ∈ 𝔏›] by auto
thus ?thesis using missing_args_persist[OF _ comp_context] replace_𝔏⇩1[OF _ 2 in_𝔏⇩1]
replace_𝔏⇩2[OF _ 2 in_𝔏⇩1] p_in_funposs funposs_mctxt_subset_all_poss_mctxt
‹L ∈ 𝔏› 2 in_𝔏⇩1 p_in_funposs unfolding 𝔏_def by auto
qed
qed
interpretation layer_system ℱ⇩U 𝔏 using pp_layer_system .
lemma lhs_rhs_in_𝒯:
assumes "r ∈ ℛ ∪ 𝒰"
shows "fst r ∈ 𝒯" "snd r ∈ 𝒯"
using assms sigR sigU 𝒯_def ℱ⇩U_def unfolding funas_trs_def funas_rule_def by auto
lemma ℛ_props:
assumes "t = fst r ∨ t = snd r" "r ∈ ℛ"
shows "(Ap, 2) ∉ funas_term t" "funas_term t ⊆ ℱ⇩U"
using assms sigR ℱ⇩U_def fresh unfolding funas_trs_def funas_rule_def by auto
lemma 𝒰r_props:
assumes "r ∈ 𝒰"
shows "(Ap, 2) ∉ funas_term (snd r)" "funas_term (snd r) ⊆ ℱ⇩U"
using assms ℱ⇩U_def fresh unfolding 𝒰_def ℱ_def by fastforce+
lemma check_lhs:
assumes "r ∈ ℛ ∪ 𝒰"
shows "check_first_non_Ap 0 (fst r ⋅ σ)"
proof -
obtain f ts where fst_r_def: "fst r = Fun f ts"
using assms wfR wfU unfolding wf_trs_def by (metis UnE prod.collapse)
hence in_ℱ⇩U: "(f, length ts) ∈ ℱ⇩U"
using lhs_rhs_in_𝒯(1)[OF assms] unfolding 𝒯_def by simp
consider "r ∈ ℛ" | "r ∈ 𝒰" using assms by blast
thus ?thesis
proof cases
case 1
hence "f ≠ Ap" using root_ℛ_notAp fst_r_def by (metis prod.collapse)
thus ?thesis using in_ℱ⇩U arity_def unfolding fst_r_def ℱ⇩U_def by fastforce
next
case 2
hence Ap2: "f = Ap ∧ length ts = 2" using 𝒰_def fst_r_def by force
then obtain f' ts' where "ts ! 0 = Fun f' ts'"
"arity f' > length ts'" "f' ≠ Ap"
using 2 𝒰_def fst_r_def fresh unfolding ℱ_def ℱ⇩U_def arity_def by force
thus ?thesis using Ap2 unfolding fst_r_def by simp
qed
qed
lemma check_lhs_ℛ_k0:
assumes "r ∈ ℛ" "check_first_non_Ap k (fst r ⋅ σ)"
shows "k = 0"
proof -
obtain f ts where fst_r_def: "fst r = Fun f ts"
using assms(1) wfR unfolding wf_trs_def by (metis prod.collapse)
hence in_ℱ: "(f, length ts) ∈ ℱ"
using sigR assms(1) ℱ_def unfolding funas_trs_def funas_rule_def by force
hence "f ≠ Ap" using fresh unfolding ℱ_def by fastforce
thus ?thesis using assms(2) in_ℱ arity_def
unfolding fst_r_def ℱ_def ℱ⇩U_def by simp
qed
lemma nothing_missing_lhs_ℛ:
assumes "r ∈ ℛ"
shows "missing_args (mctxt_of_term (fst r ⋅ σ)) 0 = 1"
proof -
obtain f ts where fst_r_def: "fst r = Fun f ts"
using assms(1) wfR unfolding wf_trs_def by (metis prod.collapse)
hence in_ℱ: "(f, length ts) ∈ ℱ"
using sigR assms(1) ℱ_def unfolding funas_trs_def funas_rule_def by force
hence "f ≠ Ap" using fresh unfolding ℱ_def by fastforce
thus ?thesis using in_ℱ arity_def
unfolding fst_r_def ℱ_def ℱ⇩U_def by simp
qed
lemma check_mt_cu'_equiv:
assumes "check_first_non_Ap 0 t"
shows "max_top_curry t = max_top_cu' 0 t"
using assms
proof (induction t)
case (Fun f ts)
thus ?case unfolding max_top_cu_equiv by simp
qed simp
lemma not_missing_persists:
assumes "missing_args L n = 0" "M ≤ L"
shows "missing_args M n = 0"
proof -
{ assume "missing_args M n ≥ 1"
hence "missing_args L n ≥ 1" using assms(2)
proof (induction arbitrary: L rule: missing_args.induct)
case (3 f Cs n)
obtain Cs' where L_def: "L = MFun f Cs'" "length Cs = length Cs'"
"(⋀i. i < length Cs ⟹ Cs ! i ≤ Cs' ! i)"
using less_eq_mctxt_MFunE1[OF 3(3)] by metis
thus ?case
proof (cases "f = Ap ∧ length Cs = 2")
case True
hence "missing_args (Cs' ! 0) (Suc n) ≥ 1"
using L_def(2-) 3(1)[OF True, of "Cs' ! 0"] 3(2-) unfolding L_def(1) by auto
thus ?thesis using True L_def by simp
next
case False
hence "Suc (arity f) - length Cs' - n ≥ 1" using 3(2) L_def(2) by auto
thus ?thesis using L_def(2) False unfolding L_def(1) by auto
qed
qed auto
hence False using assms(1) by simp
}
thus ?thesis by fastforce
qed
lemma check_missing_args_equiv:
assumes "(f, length ts) = (Ap, 2)"
shows "check_first_non_Ap n (Fun f ts) = (missing_args (max_top_cu (ts ! 0)) (Suc n) ≥ 1)"
proof
assume "check_first_non_Ap n (Fun f ts)"
thus "missing_args (max_top_cu (ts ! 0)) (Suc n) ≥ 1" using assms
proof (induction n "Fun f ts" arbitrary: f ts rule: check_first_non_Ap.induct)
case (2 n f ts)
then obtain f' ts' where ts0 : "ts ! 0 = Fun f' ts'" by (cases "ts ! 0") simp+
hence check_rec: "check_first_non_Ap (Suc n) (Fun f' ts')" using 2(2,3) by fastforce
thus ?case
proof (cases "(f', length ts') = (Ap, 2)")
case Ap2: True
have "check_first_non_Ap 0 (Fun f' ts')"
using check_first_non_Ap_persists[OF check_rec, of 0] by blast
hence "max_top_cu (ts ! 0) = MFun Ap (map max_top_cu ts')"
using Ap2 unfolding ts0 by simp
moreover have "missing_args (max_top_cu (ts' ! 0)) (Suc (Suc n)) ≥ 1"
using 2(1)[OF 2(3) ts0 check_rec Ap2] .
ultimately show ?thesis using ts0 Ap2 by fastforce
next
case False
hence "arity f' ≥ (Suc n) + length ts'" using ts0 check_rec by simp
hence "length (map max_top_cu ts') + n < arity f'" by fastforce
thus ?thesis using ts0 False by auto
qed
qed
next
assume "missing_args (max_top_cu (ts ! 0)) (Suc n) ≥ 1"
thus "check_first_non_Ap n (Fun f ts)" using assms
proof (induction "max_top_cu (ts ! 0)" n arbitrary: f ts rule: missing_args.induct)
case (2 x n) thus ?case by (metis le_numeral_extra(2) missing_args.simps(2))
next
case (3 f' Cs n)
have "0 < length ts" using 3(4) by simp
obtain g ts' where ts0: "ts ! 0 = Fun g ts'"
using ‹0 < length ts› max_top_cu.elims[OF 3(2)[symmetric]] by fastforce
hence g_ts_props: "g = f'" "length ts' = length Cs"
using max_top_cu.simps(2)[of g ts'] 3(2) by (auto split: if_splits)
have "check_first_non_Ap (Suc n) (Fun f' ts')"
proof (cases "(f', length ts') = (Ap, 2)")
case True
hence missing: "missing_args (max_top_cu (ts' ! 0)) (Suc (Suc n)) ≥ 1"
using 3(2-4) ts0[unfolded ‹g = f'›] by (auto split: if_splits)
have f'Cs: "f' = Ap ∧ length Cs = 2"
using True 3(2) unfolding ts0 ‹g = f'› g_ts_props by blast
have Cs0: "Cs ! 0 = max_top_cu (ts' ! 0)" using 3(2-4) ts0 True ‹0 < length ts›
by (metis Pair_inject max_top_cu.simps(2) mctxt.inject(2) mctxt.simps(8) nth_map)
show ?thesis using 3(1)[OF f'Cs Cs0 missing True] missing by fastforce
next
case False
hence "Suc (arity f') - length ts' - (Suc n) ≥ 1"
using 3(2-4) ts0[unfolded ‹g = f'›] g_ts_props(2)
by (metis missing_args.simps(3))
thus ?thesis using False by auto
qed
thus ?case using ts0 ‹g = f'› 3(4) by simp
qed auto
qed
lemma max_top_cu_in_layers1 [simp]:
assumes "t ∈ 𝒯"
shows "𝔏⇩1 (max_top_cu t)"
using assms
proof (induction t rule: max_top_cu.induct)
case (2 f ts) thus ?case
proof (cases "(¬(check_first_non_Ap 0 (Fun f ts)) ∨
((f, length ts) = (Ap, 2) ∧ (∃x. ts ! 0 = Var x)))")
case False
hence mt_cu: "max_top_cu (Fun f ts) = MFun f (map max_top_cu ts)" by simp
have check: "check_first_non_Ap 0 (Fun f ts)" using False by blast
thus ?thesis using 2 False
proof (cases "(f, length ts) = (Ap, 2)")
case Ap2: True
then obtain C C' where C_C': "C = max_top_cu (ts ! 0)" "C' = max_top_cu (ts ! 1)" by blast
have not_var: "¬(∃x. ts ! 0 = Var x)" using Ap2 False by blast
{ fix i n
assume "i < length ts"
hence "(ts ! i) ∈ 𝒯" using 2(2) 𝒯_def by fastforce
hence "𝔏⇩1 (max_top_cu (ts ! i))" using ‹i < length ts› 2 False Ap2 by force
{ fix n
assume assms: "i = 0" "check_first_non_Ap n (Fun f ts)"
hence "missing_args (max_top_cu (ts ! i)) (Suc n) ≥ 1"
using Ap2 not_var
proof (induction n "Fun f ts" arbitrary: i f ts rule: check_first_non_Ap.induct)
case (2 n f ts)
show ?case using check_missing_args_equiv[OF 2(4), of n] 2(2,3) by blast
qed
}
hence "𝔏⇩1 (max_top_cu (ts ! i)) ∧
(i = 0 ⟶ missing_args (max_top_cu (ts ! i)) (Suc 0) ≥ 1)"
using check ‹𝔏⇩1 (max_top_cu (ts ! i))› by blast
}
hence "𝔏⇩1 C ∧ 𝔏⇩1 C' ∧ missing_args C (Suc 0) ≥ 1" using C_C' Ap2 by force
hence "𝔏⇩1 (MFun Ap [C, C'])" by auto
thus ?thesis using Ap2 nth_map[of _ ts max_top_cu] length_map[of max_top_cu ts]
unfolding mt_cu C_C'
by (metis (no_types, lifting) One_nat_def nth_Cons_Suc length_0_conv length_Suc_conv
lessI list.inject nth_drop_0 numeral_2_eq_2 one_add_one prod.inject zero_less_two)
next
case f: False
hence f_in_ℱ⇩U: "(f, length ts) ∈ ℱ⇩U - { (Ap, 2) }" using 2(2) 𝒯_def by fastforce
{ fix i
assume "i < length ts"
hence "(ts ! i) ∈ 𝒯" using 2(2) 𝒯_def by fastforce
hence "𝔏⇩1 (max_top_cu (ts ! i))" using ‹i < length ts› 2 False f by force
}
thus ?thesis using mfun[OF f_in_ℱ⇩U] nth_map[of _ ts max_top_cu]
unfolding mt_cu by (metis (no_types, lifting) in_set_conv_nth length_map)
qed
qed fastforce
qed auto
lemma check_fails_Ap:
assumes "¬ check_first_non_Ap 0 (Fun f ts)" "Fun f ts ∈ 𝒯"
shows "f = Ap ∧ length ts = 2"
using assms ℱ⇩U_def 𝒯_def by (auto simp: arity_def split: if_splits)
lemma max_top_curry_cu_equiv1:
assumes "𝔏⇩1 (max_top_curry t)" "t ∈ 𝒯"
shows "max_top_curry t = max_top_cu t"
using assms
proof (induction t rule: max_top_curry.induct)
case (2 f ts) thus ?case
proof (cases "check_first_non_Ap 0 (Fun f ts) ∨ (∃x. ts ! 0 = Var x)")
case True
thus ?thesis using 2
proof (cases "check_first_non_Ap 0 (Fun f ts)")
case check: True
thus ?thesis by fastforce
next
case not_check: False
have Ap2: "f = Ap ∧ length ts = 2" using check_fails_Ap[OF not_check 2(2)] .
have "map max_top_cu ts ! 0 = max_top_cu (ts ! 0)"
by (simp add: Ap2)
let ?P = "λx. x = max_top_cu (ts ! 0)"
let ?R = "λx. x = max_top_cu (ts ! 1)"
have mt_simp: "max_top_curry (Fun f ts) =
MFun Ap [max_top_cu (ts ! 0), max_top_cu (ts ! 1)]"
using True Ap2 using list2_props[of ?P "map max_top_cu ts" ?R] by simp
have "missing_args (max_top_cu (ts ! 0)) (Suc 0) = 0"
using check_missing_args_equiv not_check Ap2 by simp
thus ?thesis using 2(1) Ap2 unfolding mt_simp by (auto elim: 𝔏⇩1.cases)
qed
next
case False
hence Ap2: "f = Ap ∧ length ts = 2" using check_fails_Ap[OF _ 2(2)] by blast
{ assume in_𝔏⇩1: "𝔏⇩1 (MFun f [MHole, max_top_cu (ts ! Suc 0)])"
have "missing_args MHole (Suc 0) = 0" by simp
hence "False" using in_𝔏⇩1 Ap2 by (auto elim: 𝔏⇩1.cases)
}
thus ?thesis using 2(1) False by simp
qed
qed simp
lemma max_top_curry_in_layers [simp]:
assumes "t ∈ 𝒯"
shows "(max_top_curry t) ∈ 𝔏"
using assms unfolding 𝔏_def
proof (induction t rule: max_top_curry.induct)
case (2 f ts)
{ fix i
assume "i < length ts"
hence "ts ! i ∈ 𝒯" using 2(1) 𝒯_def by force
hence "𝔏⇩1 (max_top_cu (ts ! i))" by simp
} note in_𝔏⇩1 = this
thus ?case
proof (cases "check_first_non_Ap 0 (Fun f ts) ∨ (∃x. ts ! 0 = Var x)")
case False
thus ?thesis using in_𝔏⇩1[of 1] False check_fails_Ap[OF _ 2] by fastforce
next
case True thus ?thesis
proof (cases "(f, length ts) = (Ap, 2)")
case Ap2: True
hence "f = Ap" "length ts = 2" by auto
hence "ts ! Suc 0 # drop (Suc (Suc 0)) ts = drop (Suc 0) ts"
by (metis (no_types) Cons_nth_drop_Suc lessI numeral_2_eq_2)
hence ts_def: "ts = [ts ! 0, ts ! 1]" using ‹length ts = 2› by (simp add: nth_drop_0)
thus ?thesis
proof (cases "∃x. ts ! 0 = Var x")
case True
then obtain x where "ts ! 0 = Var x" by blast
hence "max_top_cu (ts ! 0) = MVar x" by auto
moreover have "𝔏⇩1 (max_top_cu (ts ! 1))" using in_𝔏⇩1[of 1] Ap2 by fastforce
ultimately have "𝔏⇩2 (MFun Ap [max_top_cu (ts ! 0), max_top_cu (ts ! 1)])"
using Ap2 by blast
thus ?thesis using True ts_def
unfolding ‹f = Ap› by simp (metis (no_types) list.simps(8,9))
next
case no_var: False
thus ?thesis using Ap2 True 2 max_top_cu_in_layers1 by fastforce
qed
next
case not_Ap2: False
hence in_ℱ⇩U: "(f, length ts) ∈ ℱ⇩U - { (Ap, 2) }" using 2 𝒯_def by fastforce
hence "𝔏⇩1 (MFun f (map max_top_cu ts))"
using mfun[OF in_ℱ⇩U, of "map max_top_cu ts"] in_𝔏⇩1 in_set_idx[of _ "map max_top_cu ts"]
length_map[of max_top_cu ts] nth_map[of _ ts max_top_cu] by metis
thus ?thesis using True by force
qed
qed
qed auto
lemma top_less_eq1 [simp]: "max_top_cu t ≤ mctxt_of_term t"
proof (induction t rule: max_top_cu.induct)
case (2 f ts)
thus ?case
proof (cases "check_first_non_Ap 0 (Fun f ts)")
case True
{ fix i
assume "i < length ts"
hence "max_top_cu (ts ! i) ≤ mctxt_of_term (ts ! i)" using 2[OF True] by simp
} note inner = this
moreover have "max_top_cu (Fun f ts) = MFun f (map max_top_cu ts)"
using True max_top_cu.simps(2)[of f ts] by argo
ultimately show ?thesis unfolding mctxt_of_term.simps(2)[of f ts]
by (metis (mono_tags, hide_lams) length_map less_eq_mctxt_intros(3) nth_map)
qed fastforce
qed simp
lemma top_less_eq [simp]:
assumes "t ∈ 𝒯"
shows "max_top_curry t ≤ mctxt_of_term t"
using assms
proof (induction t rule: max_top_curry.induct)
case (2 f ts)
thus ?case
proof (cases "check_first_non_Ap 0 (Fun f ts) ∨ (∃x. ts ! 0 = Var x)")
case False
hence "length ts = 2" using check_fails_Ap[OF _ 2] by blast
let ?mt_ts = "[MHole, max_top_cu (ts ! 1)]"
let ?mctxt_ts = "[mctxt_of_term (ts ! 0), mctxt_of_term (ts ! 1)]"
have lengths: "length ?mt_ts = length ?mctxt_ts" by fastforce
have simp_mt: "max_top_curry (Fun f ts) = MFun f ?mt_ts"
using False by simp have simp_mctxt: "mctxt_of_term (Fun f ts) = MFun f ?mctxt_ts"
using ‹length ts = 2›
by (metis Cons_nth_drop_Suc One_nat_def Suc_eq_plus1 drop_all lessI list.simps(8,9)
mctxt_of_term.simps(2) nth_drop_0 one_add_one order_refl zero_less_Suc)
have "max_top_cu (ts ! 1) ≤ mctxt_of_term (ts ! 1)" by simp
{ fix i :: nat
assume "i < length ?mt_ts"
hence "?mt_ts ! i ≤ ?mctxt_ts ! i"
using ‹max_top_cu (ts ! 1) ≤ mctxt_of_term (ts ! 1)› less_2_cases numeral_2_eq_2
by fastforce
}
thus ?thesis using less_2_cases lengths ‹length ts = 2› unfolding simp_mt simp_mctxt
by (meson less_eq_mctxt_intros(3))
next
case True
{ fix i
assume "i < length ts"
hence "max_top_cu (ts ! i) ≤ mctxt_of_term (ts ! i)" by simp
} note inner = this
moreover have "max_top_curry (Fun f ts) = MFun f (map max_top_cu ts)"
using True max_top_curry.simps(2)[of f ts] by argo
ultimately show ?thesis unfolding mctxt_of_term.simps(2)[of f ts]
by (metis (mono_tags, hide_lams) length_map less_eq_mctxt_intros(3) nth_map)
qed
qed auto
lemma mt_curry_in_tops:
assumes "t ∈ 𝒯"
shows "max_top_curry t ∈ tops t"
using topsC_def assms by simp
lemma max_top_var1: "layer_system_sig.max_top { L . 𝔏⇩1 L } (Var x) = MVar x"
proof -
let ?topsC1 = "layer_system_sig.topsC { L . 𝔏⇩1 L }"
have mvar_in_topsC: "MVar x ∈ ?topsC1 (MVar x)"
using layer_system_sig.topsC_def[of "{ L . 𝔏⇩1 L }"] by blast
have "Var x ∈ 𝒯" by (simp add: 𝒯_def)
from max_top_not_hole[OF this] have "max_top (Var x) ≠ MHole" .
thus ?thesis
using mvar_in_topsC layer_system_sig.max_topC_def[of "{ L . 𝔏⇩1 L }"]
layer_system_sig.topsC_def[of "{ L . 𝔏⇩1 L }"] by fastforce
qed
lemma max_top_cu_max:
assumes "L ≤ mctxt_of_term t" and "𝔏⇩1 L"
shows "L ≤ max_top_cu 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_cu.simps(1) term_of_mctxt.simps(1)
term_of_mctxt_mctxt_of_term_id)
next
case (3 Cs Ds f)
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)
from 3(5) show ?case using t_def (2-) 3 unfolding t_def(1)
proof (induction "MFun f Cs" arbitrary: f Cs Ds ts rule: 𝔏⇩1.induct)
case (mfun f m Cs)
hence notAp2: "(f, length ts) ≠ (Ap, 2)" by auto
thus ?case
proof (cases "check_first_non_Ap 0 (Fun f ts)")
case True
have simp_mt: "max_top_cu (Fun f ts) = MFun f (map max_top_cu ts)" using True notAp2 by auto
{ fix i
assume i_props: "i < length Cs" "Ds ! i = mctxt_of_term (ts ! i)"
hence "𝔏⇩1 (Cs ! i)" using sub_layers[OF _ i_props(1)] mfun(10) 𝔏_def by blast
hence "Cs ! i ≤ max_top_cu (ts ! i)" using mfun(8)[OF i_props] by simp
}
thus ?thesis using mfun(6,9) simp_mt mfun_leq_mfunI[of f f Cs "map max_top_cu ts"]
by (simp add: map_nth_eq_conv)
next
case False
have "arity f < length ts" using False notAp2 by auto
hence "(f, length ts) ∉ ℱ⇩U" using ℱ⇩U_def notAp2 arity_def by auto
thus ?thesis using mfun(1,2,5,6) by auto
qed
next
case (addAp C C')
from addAp(6-9) have C_leq: "C ≤ mctxt_of_term (ts ! 0)" by force
have length2: "length ts = 2" using addAp(7,8) by auto
thus ?case
proof (cases "∃x. ts ! 0 = Var x")
case is_var: True
then obtain x where "ts ! 0 = Var x" by blast
hence "Ds ! 0 = MVar x" using addAp(6-8) nth_map[of _ ts mctxt_of_term] by fastforce
moreover have "C ≤ Ds ! 0" using addAp(8,9) by force
ultimately have "C = MHole ∨ C = MVar x" using less_eq_mctxtE2(2) by fastforce
thus ?thesis using addAp(5) by fastforce
next
case not_var: False thus ?thesis
proof (cases "check_first_non_Ap 0 (Fun Ap ts)")
case True
have simp_mt: "max_top_cu (Fun Ap ts) = MFun Ap (map max_top_cu ts)"
using True not_var by auto
{ fix i
assume i_props: "i < length [C, C']" "Ds ! i = mctxt_of_term (ts ! i)"
hence "[C, C'] ! i ≤ max_top_cu (ts ! i)" using addAp(10)[OF i_props] addAp(1,3)
by (simp add: nth_Cons')
}
thus ?thesis
using addAp(8,11) simp_mt mfun_leq_mfunI[of Ap Ap "[C, C']" "map max_top_cu ts"]
by (simp add: map_nth_eq_conv)
next
case False
hence not_missing: "missing_args (mctxt_of_term (ts ! 0)) (Suc 0) = 0"
using missing_args_unfold[of "ts ! 0" "Suc 0"] length2 by simp
hence "missing_args C (Suc 0) = 0"
using not_missing_persists[OF _ C_leq] by blast
thus ?thesis using addAp(5) by linarith
qed
qed
qed
qed auto
abbreviation max_top1 where "max_top1 ≡ layer_system_sig.max_top { L . 𝔏⇩1 L }"
abbreviation max_topC1 where "max_topC1 ≡ layer_system_sig.max_topC { L . 𝔏⇩1 L }"
abbreviation tops1 where "tops1 ≡ layer_system_sig.tops { L . 𝔏⇩1 L }"
abbreviation topsC1 where "topsC1 ≡ layer_system_sig.topsC { L . 𝔏⇩1 L }"
lemmas max_topC1_def = layer_system_sig.max_topC_def[of "{ L . 𝔏⇩1 L }"]
lemmas topsC1_def = layer_system_sig.topsC_def[of "{ L . 𝔏⇩1 L }"]
lemma max_top_unique1:
shows "∃!M. M ∈ topsC1 C ∧ (∀L ∈ topsC1 C. L ≤ M)"
proof -
have sub_tops: "⋀C. topsC1 C ⊆ topsC C" using topsC_def topsC1_def 𝔏_def by blast
have mhole_in_tops: "⋀C. MHole ∈ topsC C"
using topsC_def less_eq_mctxtI1(1) using 𝔏_def by blast
then obtain M where M_props: "M ∈ topsC C" "∀L∈topsC C. L ≤ M" "M ∈ 𝔏"
using topsC_def[of C] max_topC_layer max_topC_props by meson
consider "𝔏⇩1 M" | "𝔏⇩2 M" using M_props(3) 𝔏_def by blast
thus ?thesis
proof cases
case 1
hence "∃!M. M ∈ topsC1 C ∧ (∀L∈topsC1 C. L ≤ M)"
using max_top_unique M_props topsC_def unfolding topsC1_def 𝔏_def by force
then obtain M where M_props: "M ∈ topsC1 C" "∀L∈topsC1 C. L ≤ M" "𝔏⇩1 M"
using topsC1_def[of C] by auto
hence "M ∈ topsC1 C" using M_props by (simp add: layer_system_sig.topsC_def)
moreover have "∀L∈topsC1 C. L ≤ M" using M_props(2)
by (simp add: topsC1_def)
ultimately show ?thesis using dual_order.antisym
unfolding layer_system_sig.topsC_def by blast
next
case 2
then obtain x C' where M_def: "M = MFun Ap [x, C']" "x = MHole ∨ (∃v. x = MVar v)" "𝔏⇩1 C'"
by (meson 𝔏⇩2.cases)
have "M ≤ C" using M_props(1) unfolding topsC_def by simp
obtain Cs where C_def: "C = MFun Ap Cs" "length [x, C'] = length Cs"
"(⋀i. i < length [x, C'] ⟹ [x, C'] ! i ≤ Cs ! i)"
using less_eq_mctxt_MFunE1[OF ‹M ≤ C›[unfolded M_def]] by blast
{ fix L :: "('f, 'v) mctxt"
assume "L ∈ topsC1 C"
hence "L ≤ C" using M_props layer_system_sig.topsC_def by blast
have "L ≤ M" using sub_tops ‹∀L∈topsC C. L ≤ M› ‹L ∈ topsC1 C› 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')
have props: "f' = Ap" "length Cs' = length [x, C']"
"⋀i. i < length Cs' ⟹ Cs' ! i ≤ [x, C'] ! i"
using ‹L ≤ M› less_eq_mctxt_MFunE1[of f' Cs' M] mctxt.inject(2)
unfolding M_def MFun by metis+
hence "Cs' ! 0 ≤ x" by fastforce
hence Cs'0: "Cs' ! 0 = MHole ∨ (∃v. Cs' ! 0 = MVar v)"
using M_def(2) mctxt_order_bot.bot.extremum_uniqueI
by (auto elim: less_eq_mctxt'.cases) (meson less_eq_mctxtE2(2))
obtain y C'' where Cs'_def: "Cs' = [y, C'']"
using props(2) by (auto simp: length_Suc_conv)
have "𝔏⇩1 L" using ‹L ∈ topsC1 C› topsC1_def[of C] by blast
thus ?thesis using 𝔏⇩1.simps[of L] Cs'0 unfolding MFun Cs'_def ‹f' = Ap› by force
qed
}
moreover have "⋀C. MHole ∈ topsC1 C" unfolding topsC1_def by auto
ultimately show ?thesis by blast
qed
qed
lemma max_topC_props1 [simp]:
shows "max_topC1 C ∈ topsC1 C" and "⋀L. L ∈ topsC1 C ⟹ L ≤ max_topC1 C"
by (auto simp: theI'[OF max_top_unique1] layer_system_sig.max_topC_def)
lemma max_top_cu_correct [simp]:
assumes "t ∈ 𝒯"
shows "max_top1 t = max_top_cu t"
using assms
proof (induction t)
case (Var x) thus ?case using max_top_var1 by simp
next
case (Fun f ts)
thus ?case
proof (cases "check_first_non_Ap 0 (Fun f ts)")
case True
hence simp_mt: "max_top_cu (Fun f ts) = MFun f (map max_top_cu ts)" by force
hence in_𝔏⇩1: "𝔏⇩1 (MFun f (map max_top_cu ts))" using max_top_cu_in_layers1[OF Fun(2)] by argo
have max_top_lt_mt: "(THE m. m ∈ tops1 (Fun f ts) ∧
(∀ma. ma ∈ tops1 (Fun f ts) ⟶ ma ≤ m)) ≤ MFun f (map max_top_cu ts)"
using max_top_cu_max[of _ "Fun f ts"] max_topC_props1
unfolding max_topC1_def topsC1_def simp_mt by force
have "MFun f (map max_top_cu ts) ≤ max_topC1 (MFun f (map mctxt_of_term ts))"
using top_less_eq1[of "Fun f ts"] in_𝔏⇩1 unfolding simp_mt by (simp add: topsC1_def)
thus ?thesis
using max_top_lt_mt simp_mt by (simp add: Ball_def_raw max_topC1_def)
next
case False
hence simp_mt: "max_top_cu (Fun f ts) = MHole" by force
have max_top_lt_mt: "(THE m. m ∈ tops1 (Fun f ts) ∧
(∀ma. ma ∈ tops1 (Fun f ts) ⟶ ma ≤ m)) ≤ MHole"
using max_top_cu_max[of _ "Fun f ts"] max_topC_props1
unfolding max_topC1_def topsC1_def simp_mt by force
have "MHole ≤ max_topC1 (MFun f (map mctxt_of_term ts))"
unfolding simp_mt by (simp add: topsC1_def)
thus ?thesis
using max_top_lt_mt simp_mt mctxt_order_bot.bot.extremum_uniqueI
by (simp add: Ball_def_raw max_topC1_def) fastforce
qed
qed
lemma max_top_leq_mctxt: "max_top t ≤ mctxt_of_term t"
using max_topC_prefix by simp
lemma max_top1_simp:
assumes "𝔏⇩1 (max_top t)"
shows "max_top t = max_top1 t"
using assms
by (intro max_top_mono1[symmetric]) (auto simp: 𝔏_def)
lemma 𝔏⇩2_not_missing:
assumes "𝔏⇩2 L"
shows "missing_args L n = 0"
proof -
from assms obtain x C v where "L = MFun Ap [x, C]" "x = MHole ∨ x = MVar v"
using 𝔏⇩2.cases[OF assms] by metis
thus ?thesis by force
qed
lemma missing_in_𝔏⇩1:
assumes "L ∈ 𝔏" "missing_args L 0 ≥ 1"
shows "𝔏⇩1 L"
using assms(2,1) 𝔏⇩2_not_missing 𝔏_def by force
lemma max_top_prefers_𝔏⇩1:
assumes "MFun f Cs ≤ mctxt_of_term t" "𝔏⇩1 (MFun f Cs)"
shows "𝔏⇩1 (max_top t)"
proof -
consider "𝔏⇩1 (max_top t)" | "𝔏⇩2 (max_top t)" using max_topC_layer 𝔏_def by blast
thus ?thesis
proof cases
case 2
then obtain x C v where Ap2: "max_top t = MFun Ap [x, C]" "x = MHole ∨ x = MVar v"
using 𝔏⇩2.simps by blast
obtain Ds where Ds_props: "mctxt_of_term t = MFun Ap Ds" "length [x, C] = length Ds"
using less_eq_mctxt_MFunE1[OF max_top_leq_mctxt[of t, unfolded Ap2]] by metis
then obtain ts where t_def: "t = Fun Ap ts" "length [x, C] = length ts"
by (metis length_map term_of_mctxt.simps(2) term_of_mctxt_mctxt_of_term_id)
have "length Cs = length Ds" "f = Ap"
using Ds_props(2) less_eq_mctxt_MFunE1[OF assms(1)]
unfolding Ds_props(1) t_def by (fastforce, auto)
hence "length Cs = 2" using Ds_props(2) by auto
then obtain D D' where Cs_def: "Cs = [D, D']"
using list2_props[OF _ ‹length Cs = 2›] by fastforce
have missing: "missing_args D (Suc 0) ≥ 1"
using assms(2) 𝔏⇩1.simps[of "MFun Ap [D, D']"] Cs_def ‹length Cs = 2›
unfolding ‹f = Ap› Cs_def by blast
obtain g Ds' where "D = MFun g Ds'" using missing_args.elims missing
by (metis le_numeral_extra(2))
have "MFun Ap [D, D'] ∈ tops t"
using topsC_def assms unfolding ‹f = Ap› Cs_def(1) 𝔏_def by blast
hence leq: "MFun Ap [D, D'] ≤ MFun Ap [x, C]" using max_topC_props(2) Ap2 by metis
have "D ≤ x" using less_eq_mctxt_MFunE1[OF leq]
by (metis length_greater_0_conv list.distinct(1) mctxt.inject(2) nth_Cons_0)
thus ?thesis using Ap2(2) ‹D = MFun g Ds'› using less_eq_mctxt_MFunE1 by fastforce
qed
qed
lemma max_top1_simp':
assumes "Fun f ts ∈ 𝒯" "max_top (Fun f ts) = MFun f Cs" "i < length ts"
"i > 0 ∨ check_first_non_Ap 0 (Fun f ts)"
shows "Cs ! i = max_top1 (ts ! i)"
proof -
have lengths: "length Cs = length ts"
using less_eq_mctxt_MFunE1[OF max_top_leq_mctxt[of "Fun f ts", unfolded assms(2)]]
by fastforce
{ fix i
assume "i < length ts"
have ts_i: "ts ! i ∈ 𝒯" using assms(1) ‹i < length ts› unfolding 𝒯_def by fastforce
} note in_𝒯 = this
consider "𝔏⇩1 (max_top (Fun f ts))" | "𝔏⇩2 (max_top (Fun f ts))"
using max_topC_layer 𝔏_def by blast
thus ?thesis
proof cases
case 1
thus ?thesis using assms(3) max_top1_simp[OF 1] in_𝒯
unfolding assms(2) max_top_cu_correct[OF assms(1)]
by simp (metis assms(1) assms(2) max_top_not_hole mctxt.inject(2) nth_map)
next
case 2
then obtain x C v where mt_def: "MFun f Cs = MFun Ap [x, C]" "x = MHole ∨ x = MVar v" "𝔏⇩1 C"
using 𝔏⇩2.simps[of "MFun f Cs"] unfolding assms(2) by blast
hence Ap2: "f = Ap" "length ts = 2" using lengths by auto
from assms(4) show ?thesis
proof (elim disjE)
assume "i > 0"
hence "i = 1" using mt_def(1) assms(3) lengths by auto
let ?mt = "MFun Ap [x, max_top_cu (ts ! i)]"
have leq: "MFun Ap [x, C] ≤ mctxt_of_term (Fun f ts)"
using assms(2) max_topC_prefix unfolding mt_def(1) by metis
have in_𝔏⇩1: "𝔏⇩1 (max_top_cu (ts ! i))" "max_top_cu (ts ! i) ≤ (map mctxt_of_term ts) ! i"
using assms(3) top_less_eq1 in_𝒯[OF assms(3)] unfolding topsC_def by auto
moreover { fix j
assume "j < length ts"
hence "j < 2" using Ap2(2) by auto
have "∀i<length [x, C]. [x, C] ! i ≤ (map mctxt_of_term ts) ! i"
using less_eq_mctxt_MFunE1[OF leq] Ap2 unfolding mctxt_of_term.simps(2) by fast
hence "x ≤ (map mctxt_of_term ts) ! 0" by fastforce
from less_2_cases[OF ‹j < 2›] and this have
"[x, max_top_cu (ts ! 1)] ! j ≤ (map mctxt_of_term ts) ! j"
using in_𝔏⇩1(2) Ap2(2) unfolding ‹i = 1› by (elim disjE) simp+
} note sub_leq = this
hence "?mt ≤ mctxt_of_term (Fun f ts)"
using Ap2(2) unfolding ‹i = 1› Ap2(1) mctxt_of_term.simps(2)
by (auto elim: less_eq_mctxtI1(3)) (metis One_nat_def length_Cons
length_map less_eq_mctxt_intros(3) list.size(3) numeral_2_eq_2 sub_leq)
moreover have "𝔏⇩2 ?mt" using mt_def(2) in_𝔏⇩1(1) by blast
ultimately have in_tops: "?mt ∈ tops (Fun f ts)"
using 𝔏_def unfolding topsC_def by blast
have "C ≤ mctxt_of_term (ts ! i)"
using assms(3) less_eq_mctxt_MFunE1[OF max_top_leq_mctxt[of "Fun f ts",
unfolded assms(2)[unfolded mt_def(1)]]]
unfolding ‹i = 1›
by (metis (no_types, lifting) One_nat_def lengths mctxt.inject(2)
mctxt_of_term.simps(2) mt_def(1) nth_Cons_0 nth_Cons_Suc nth_map)
hence "C ≤ max_top_cu (ts ! i)" using max_top_cu_max[OF _ ‹𝔏⇩1 C›, of "ts ! i"] by simp
moreover have "C ≥ max_top_cu (ts ! i)"
using assms(3) less_eq_mctxt_MFunE1[OF max_topC_props(2)[OF in_tops]]
unfolding ‹i = 1› assms(2) mt_def Ap2(2)
by (metis length_Cons lessI list.size(3) mctxt.inject(2) nth_Cons_0 nth_Cons_Suc)
ultimately have "C = max_top_cu (ts ! i)" by simp
thus ?thesis using mt_def(1) ‹i = 1› lengths in_𝒯[OF assms(3)] by auto
next
assume check: "check_first_non_Ap 0 (Fun f ts)"
hence missing: "missing_args (max_top_cu (ts ! 0)) (Suc 0) ≥ 1"
using check_missing_args_equiv[of f ts 0] Ap2 by force
have lengths_01: "0 < length ts" "1 < length ts" using Ap2 by simp+
have mt_cu: "max_top_curry (Fun f ts) = MFun f (map max_top_cu ts)"
"length (map max_top_cu ts) = 2"
using check Ap2 by force+
have map_simp: "⋀i. i < length ts ⟹ max_top_cu (ts ! i) = (map max_top_cu ts) ! i"
by simp
have "𝔏⇩1 (max_top_cu (ts ! 0))" "𝔏⇩1 (max_top_cu (ts ! 1))"
using Ap2 by (simp add: in_𝒯)+
then obtain C C' where CC'_props: "map max_top_cu ts = [C, C']"
"𝔏⇩1 C" "𝔏⇩1 C'" "missing_args C (Suc 0) ≥ 1"
using list2_props[OF _ mt_cu(2), of 𝔏⇩1 𝔏⇩1] missing
list2_props[OF _ mt_cu(2), of "λC. missing_args C (Suc 0) ≥ 1" _]
unfolding map_simp[OF lengths_01(1)] map_simp[OF lengths_01(2)] by fastforce
have mt_cu2: "max_top_curry (Fun f ts) = MFun Ap [C, C']" "𝔏⇩1 (MFun Ap [C, C'])"
using mt_cu Ap2 CC'_props(2-) unfolding CC'_props by auto
have max_top_𝔏⇩1: "𝔏⇩1 (max_top (Fun f ts))"
using max_top_prefers_𝔏⇩1[OF top_less_eq[OF assms(1), unfolded mt_cu2(1)] mt_cu2(2)] .
show ?thesis using assms(1,3) max_top1_simp[OF max_top_𝔏⇩1] in_𝒯 Ap2 CC'_props check map_simp
unfolding assms(2) max_top_cu_correct[OF assms(1)] by auto
qed
qed
qed
lemma max_top_curry_correct:
assumes "t ∈ 𝒯"
shows "max_top t = max_top_curry t"
proof (cases t)
case (Var x) thus ?thesis using max_top_var by simp
next
case (Fun f ts)
thus ?thesis
proof (cases "check_first_non_Ap 0 (Fun f ts) ∨ (∃x. ts ! 0 = Var x)")
case True
hence mt_cu: "max_top_curry (Fun f ts) = MFun f (map max_top_cu ts)" by auto
obtain Cs where max_top_mfun: "max_top (Fun f ts) = MFun f Cs" "length Cs = length ts"
using True assms max_topC_layer[of "mctxt_of_term t"] assms
unfolding Fun
by (metis (no_types, lifting) length_map less_eq_mctxt_MFunE2 max_topC_props(1)
max_top_not_hole mctxt_of_term.simps(2) mem_Collect_eq topsC_def)
{ fix i
assume "i < length ts"
hence poss: "<i> ∈ all_poss_mctxt (max_top (Fun f ts))" using max_top_mfun by simp
have "ts ! i ∈ 𝒯" using assms ‹i < length ts› unfolding 𝒯_def Fun by fastforce
have subm_at_simp: "subm_at (max_top (Fun f ts)) <i> = Cs ! i" using max_top_mfun by simp
have "MFun f Cs ∈ 𝔏" using max_top_mfun max_topC_layer by metis
have "𝔏⇩1 (Cs ! i)" using ‹i < length ts› sub_layers[OF ‹MFun f Cs ∈ 𝔏›]
using max_top_mfun(2) by simp
have leq: "MFun f Cs ≤ mctxt_of_term (Fun f ts)" using max_top_mfun
by (metis (no_types, lifting) max_topC_props(1) mem_Collect_eq topsC_def)
have Cs_i_leq: "Cs ! i ≤ (map mctxt_of_term ts) ! i"
using ‹i < length ts› less_eq_mctxt_MFunE1[OF leq]
unfolding mctxt_of_term.simps(2)[of f ts]
by (metis max_top_mfun(2) mctxt.inject(2))
hence "Cs ! i ≤ mctxt_of_term (ts ! i)" by (simp add: ‹i < length ts›)
have "Cs ! i = max_top_cu (ts ! i)"
proof (cases "i = 0")
case i0: True
from True show ?thesis
proof (elim disjE)
assume "check_first_non_Ap 0 (Fun f ts)"
thus ?thesis using max_top1_simp'[OF assms[unfolded Fun]
max_top_mfun(1) ‹i < length ts›] ‹ts ! i ∈ 𝒯› by fastforce
next
assume "∃x. ts ! 0 = Var x"
then obtain x where ts0_def: "ts ! 0 = Var x" by blast
then consider "Cs ! 0 = MVar x" | "Cs ! 0 = MHole"
using max_top_mfun ‹i < length ts› Cs_i_leq less_eq_mctxtE2(2) unfolding i0 by fastforce
thus ?thesis
proof cases
case 1 thus ?thesis using ts0_def i0 by simp
next
case 2
moreover have "(map max_top_cu ts) ! 0 ≤ Cs ! 0"
using max_topC_props(2)[OF mt_curry_in_tops[OF assms]] max_top_mfun(2) ‹i < length ts›
unfolding Fun mt_cu max_top_mfun(1) i0
by (metis less_eq_mctxtE2(3) mctxt.distinct(5) mctxt.inject(2))
ultimately show ?thesis
using ts0_def ‹i < length ts› i0 mctxt_order_bot.bot.extremum_uniqueI by auto
qed
qed
next
case i_greater: False
hence "i > 0" using ‹i < length ts› by simp
thus ?thesis using max_top1_simp'[OF assms[unfolded Fun] max_top_mfun(1) ‹i < length ts›]
‹ts ! i ∈ 𝒯› by fastforce
qed
hence "Cs ! i = max_top_cu (ts ! i)"
using max_top1_simp'[OF _ max_top_mfun(1)] ‹𝔏⇩1 (Cs ! i)› ‹i < length ts› ‹ts ! i ∈ 𝒯›
unfolding subm_at_simp subt_at.simps(2) by force
}
thus ?thesis using mt_cu max_top_mfun Fun by (metis map_nth_eq_conv)
next
case False
hence mt_cu: "max_top_curry (Fun f ts) = MFun f [MHole, max_top_cu (ts ! 1)]" by auto
hence Ap2: "f = Ap ∧ length ts = 2" using False check_fails_Ap[OF _ assms[unfolded Fun]] by blast
have "max_top_curry (Fun f ts) ∈ 𝔏" using max_top_curry_in_layers[OF assms] unfolding Fun .
have "ts ! 1 ∈ 𝒯" using assms Ap2 unfolding 𝒯_def Fun by force
obtain Cs where max_top_mfun: "max_top (Fun f ts) = MFun f Cs" "length Cs = 2"
using Ap2 False assms max_topC_layer[of "mctxt_of_term t"] max_top_cu_correct[OF assms]
unfolding Fun
by (metis (no_types, lifting) 𝔏⇩2.cases 𝔏_def length_Cons list.size(3) max_top_cu.simps(2)
max_top_not_hole mem_Collect_eq numeral_2_eq_2 max_top1_simp)
hence "𝔏⇩2 (max_top (Fun f ts))" using Ap2 max_top_mfun False Fun 𝔏_def max_top1_simp
by (metis (no_types, lifting) max_topC_layer max_top_cu.simps(2)
max_top_cu_correct[OF assms] mctxt.simps(8) mem_Collect_eq)
then obtain x v C where mt: "max_top (Fun f ts) = MFun Ap [x, C]"
"𝔏⇩1 C" "x = MHole ∨ x = MVar v"
using 𝔏⇩2.simps Ap2 by blast
have "f = Ap" using Ap2 by blast
have leq: "MFun Ap [x, C] ≤ mctxt_of_term (Fun f ts)"
using mt(1) by (metis (no_types, lifting) max_topC_props(1) mem_Collect_eq topsC_def)
have "x ≤ (map mctxt_of_term ts) ! 0" using Ap2 less_eq_mctxt_MFunE1[OF leq]
unfolding mctxt_of_term.simps(2)[of f ts]
by (metis length_greater_0_conv list.distinct(1) mctxt.inject(2) nth_Cons_0)
moreover have "C ≤ (map mctxt_of_term ts) ! 1" using Ap2 less_eq_mctxt_MFunE1[OF leq]
unfolding mctxt_of_term.simps(2)[of f ts]
by (metis One_nat_def length_Cons lessI list.size(3) mctxt.inject(2) nth_Cons_0 nth_Cons_Suc)
ultimately have leq2: "x ≤ mctxt_of_term (ts ! 0)"
by (simp add: Ap2)+
hence "x = MHole" using Ap2 False less_eq_mctxt_MVarE1[of _ "mctxt_of_term (ts ! 0)"] mt(3)
by (metis mctxt_of_term.simps(1) term_of_mctxt_mctxt_of_term_id)
have simp_subm_at: "subm_at (max_top (Fun f ts)) <1> = C" using mt(1) by simp
have "<1> ∈ all_poss_mctxt (max_top (Fun f ts))" unfolding mt(1) poss_mctxt_simp by simp
hence "C = max_top_cu (ts ! 1)"
using max_top1_simp'[OF _ mt(1)[unfolded ‹f = Ap›]] assms[unfolded Fun] Ap2
unfolding max_top_cu_correct[OF ‹ts ! 1 ∈ 𝒯›, symmetric] simp_subm_at by force
thus ?thesis using Ap2 unfolding Fun mt(1) mt_cu ‹x = MHole› by fast
qed
qed
abbreviation check_persists where
"check_persists s t ≡ ∀j. check_first_non_Ap j s ⟶ check_first_non_Ap j t"
abbreviation check_weak_persists where
"check_weak_persists j C s t ≡ check_first_non_Ap j C⟨s⟩ ⟶ check_first_non_Ap j C⟨t⟩"
lemma replace_check_persist:
assumes "check_persists s t"
shows "check_persists C⟨s⟩ C⟨t⟩"
using assms
proof (induction C)
case (More f ss1 D ss2)
hence check_D_s: "∀n > 0. check_first_non_Ap n D⟨s⟩ ⟶ check_first_non_Ap n D⟨t⟩" by blast
{ fix n
have "check_persists (More f ss1 D ss2)⟨s⟩ (More f ss1 D ss2)⟨t⟩"
proof (cases "length ss1 = 0")
case False
hence "⋀x. (ss1 @ x # ss2) ! 0 = ss1 ! 0" by (simp add: append_Cons_nth_left)
thus ?thesis by (auto split: if_splits)
qed (simp add: check_D_s)
}
thus ?case by blast
qed simp
lemma check_in_𝔏⇩1:
assumes "check_first_non_Ap 0 t" "t ∈ 𝒯"
shows "𝔏⇩1 (max_top_curry t)"
proof (cases t rule: max_top_curry.cases)
case (2 f ts) thus ?thesis
proof (cases "f = Ap ∧ length ts = 2")
case True
hence "missing_args (max_top_cu (ts ! 0)) (Suc 0) ≥ 1"
using assms check_missing_args_equiv[of f ts 0] unfolding 2 by fast
hence missing: "missing_args (max_top_curry t) 0 ≥ 1" using assms True unfolding 2 by simp
show ?thesis using missing_in_𝔏⇩1 assms(2) missing by auto
next
case False
thus ?thesis using assms max_top_cu_in_layers1 𝒯_def unfolding 2
by (metis max_top_cu.simps(2) max_top_curry.simps(2))
qed
qed auto
abbreviation mt_cu' where "mt_cu' ≡ λk t. mctxt_term_conv (max_top_cu' k t)"
abbreviation mt_curry where "mt_curry ≡ λ t. mctxt_term_conv (max_top_curry t)"
lemma push_mt_in_ctxt':
assumes "hole_pos C ∈ funposs_mctxt (max_top_cu' j C⟨s⟩)"
shows "∃D k. mt_cu' j C⟨s⟩ = D⟨mt_cu' k s⟩ ∧ hole_pos C = hole_pos D ∧ (C = Hole ⟶ k = j) ∧
max_top_cu' k s ≠ MHole ∧ (k = 0 ∧ C ≠ Hole ⟶ check_weak_persists j C s t) ∧
(check_persists s t ∨ k = 0 ⟶ mt_cu' j C⟨t⟩ = D⟨mt_cu' k t⟩)"
using assms
proof (induction C arbitrary: j)
case Hole
hence "max_top_cu' j s ≠ MHole" using funposs_mctxt_subset_poss_mctxt by force
thus ?case using Hole by simp (metis ctxt.cop_nil hole_pos.simps(1))
next
case (More f ss1 C' ss2)
let ?C = "More f ss1 C' ss2"
let ?ts = "ss1 @ C'⟨s⟩ # ss2"
let ?mt = "λxs. map (mt_cu' 0) xs"
let ?mt' = "λxs j. map (mt_cu' j) xs"
show ?case
proof (cases "check_first_non_Ap j ?C⟨s⟩")
case check: True thus ?thesis
proof (cases "f = Ap ∧ Suc (length ss1 + length ss2) = 2")
case Ap2: True
then consider "length ss1 = 0" | "length ss1 = Suc 0"
using nat_neq_iff by fastforce
thus ?thesis
proof cases
case 1
hence hole_pos: "hole_pos C' ∈ funposs_mctxt (max_top_cu' (Suc j) C'⟨s⟩)"
using More(2) check Ap2 by (auto simp: funposs_mctxt_def)
obtain D' k' where D'_prop:
"mt_cu' (Suc j) C'⟨s⟩ = D'⟨mt_cu' k' s⟩ ∧ hole_pos C' = hole_pos D' ∧
(C' = Hole ⟶ k' = (Suc j)) ∧ max_top_cu' k' s ≠ MHole ∧
(k' = 0 ∧ C' ≠ Hole ⟶ check_weak_persists (Suc j) C' s t) ∧
(check_persists s t ∨ k' = 0 ⟶ mt_cu' (Suc j) C'⟨t⟩ = D'⟨mt_cu' k' t⟩)"
using More(1)[OF hole_pos] by blast
let ?D = "More f (?mt ss1) D' (?mt ss2)"
have length_ss2: "length ss2 = Suc 0"
using Ap2 1 by (auto simp: length_Suc_conv[of ss2 0])
hence "mt_cu' j ?C⟨s⟩ = ?D⟨mt_cu' k' s⟩ ∧ hole_pos ?C = hole_pos ?D ∧
max_top_cu' k' s ≠ MHole ∧
(k' = 0 ∧ ?C ≠ Hole ⟶ check_weak_persists j ?C s t) ∧
(check_persists s t ∨ k' = 0 ⟶ mt_cu' j ?C⟨t⟩ = ?D⟨mt_cu' k' t⟩)"
using D'_prop check Ap2 1 list1_map[OF length_ss2, of "mt_cu' 0"]
replace_check_persist[of s t "More f ss1 C' ss2"] by force
thus ?thesis by fast
next
case 2
hence hole_pos: "hole_pos C' ∈ funposs_mctxt (max_top_cu' 0 C'⟨s⟩)"
using More(2) check Ap2 nth_append_length[of ss1 "C'⟨s⟩"]
by (auto simp: funposs_mctxt_def)
obtain D' k' where D'_prop:
"mt_cu' 0 C'⟨s⟩ = D'⟨mt_cu' k' s⟩ ∧ hole_pos C' = hole_pos D' ∧
max_top_cu' k' s ≠ MHole ∧ (k' = 0 ∧ C' ≠ Hole ⟶ check_weak_persists 0 C' s t) ∧
(check_persists s t ∨ k' = 0 ⟶ mt_cu' 0 C'⟨t⟩ = D'⟨mt_cu' k' t⟩)"
using More(1)[OF hole_pos] by blast
let ?D = "More f (mt_cu' (Suc j) (ss1 ! 0) # ?mt (drop 1 ss1)) D' (?mt ss2)"
have "mt_cu' j ?C⟨s⟩ = ?D⟨mt_cu' k' s⟩ ∧ hole_pos ?C = hole_pos ?D ∧
max_top_cu' k' s ≠ MHole ∧ (k' = 0 ∧ ?C ≠ Hole ⟶ check_weak_persists j ?C s t) ∧
(check_persists s t ∨ k' = 0 ⟶ mt_cu' j ?C⟨t⟩ = ?D⟨mt_cu' k' t⟩)"
using D'_prop check Ap2 2 by (simp add: nth_append)
thus ?thesis by fast
qed
next
case not_Ap2: False
hence hole_pos: "hole_pos C' ∈ funposs_mctxt (max_top_cu' 0 C'⟨s⟩)"
using More(2) check max_top_cu'.simps(2)[of j f ?ts]
by (simp add: funposs_mctxt_def split: if_splits) (metis nth_append_length length_map)
obtain D' k' where D'_prop:
"mt_cu' 0 C'⟨s⟩ = D'⟨mt_cu' k' s⟩ ∧ hole_pos C' = hole_pos D' ∧
max_top_cu' k' s ≠ MHole ∧ (k' = 0 ∧ C' ≠ Hole ⟶ check_weak_persists 0 C' s t) ∧
(check_persists s t ∨ k' = 0 ⟶ mt_cu' 0 C'⟨t⟩ = D'⟨mt_cu' k' t⟩)"
using More(1)[OF hole_pos] by blast
let ?D = "More f (?mt ss1) D' (?mt ss2)"
have "mt_cu' j ?C⟨s⟩ = ?D⟨mt_cu' k' s⟩ ∧ hole_pos ?C = hole_pos ?D ∧
max_top_cu' k' s ≠ MHole ∧ (k' = 0 ∧ ?C ≠ Hole ⟶ check_weak_persists j ?C s t) ∧
(check_persists s t ∨ k' = 0 ⟶ mt_cu' j ?C⟨t⟩ = ?D⟨mt_cu' k' t⟩)"
using D'_prop check not_Ap2
by (simp (no_asm) only: max_top_cu'.simps ctxt_apply_term.simps) force
thus ?thesis by blast
qed
next
case False
thus ?thesis using More(2) by (auto simp: funposs_mctxt_def)
qed
qed
lemma funposs_mt_sub:
assumes "t ∈ 𝒯"
shows "funposs (mt_curry t) ⊆ funposs t"
using top_less_eq[OF assms] funposs_mctxt_def
funposs_mctxt_mctxt_of_term funposs_mctxt_mono by blast
lemma push_mt_in_ctxt:
assumes "hole_pos C ∈ funposs_mctxt (max_top_curry C⟨s⟩)" "C⟨s⟩ ∈ 𝒯" "C⟨t⟩ ∈ 𝒯" "C ≠ Hole"
shows "∃D k. mt_curry C⟨s⟩ = D⟨mt_cu' k s⟩ ∧ hole_pos C = hole_pos D ∧ max_top_cu' k s ≠ MHole ∧
(k = 0 ∧ C ≠ Hole ⟶ check_weak_persists 0 C s t) ∧
(check_persists s t ∨ k = 0 ⟶ mt_curry C⟨t⟩ = D⟨mt_cu' k t⟩)"
proof -
consider "𝔏⇩1 (max_top_curry C⟨s⟩)" | "𝔏⇩2 (max_top_curry C⟨s⟩)" using assms(2) 𝔏_def by fastforce
thus ?thesis
proof cases
case 1
have mt_eq: "max_top_cu' 0 C⟨s⟩ = max_top_curry C⟨s⟩"
using max_top_curry_cu_equiv1[OF 1 assms(2)] by simp
moreover obtain f ts where is_fun: "C⟨s⟩ = Fun f ts"
using assms(1) funposs_mt_sub[OF assms(2)] unfolding funposs_mctxt_def
by (metis empty_iff funposs.elims subsetCE)
ultimately have check_Cs: "check_first_non_Ap 0 C⟨s⟩" using max_top_curry_cu_equiv
unfolding max_top_cu_equiv[symmetric] by metis
{ assume "check_persists s t"
hence "check_first_non_Ap 0 C⟨t⟩"
using check_Cs replace_check_persist missing_args_unfold by blast
hence "max_top_cu' 0 C⟨t⟩ = max_top_curry C⟨t⟩"
using assms(3) check_in_𝔏⇩1 max_top_curry_cu_equiv1 by auto
}
thus ?thesis
using push_mt_in_ctxt'[of C 0 s t] mt_eq assms(1)
by (metis (no_types, lifting) assms(4) check_Cs check_mt_cu'_equiv)
next
case 2
then obtain x C'' where in_𝔏⇩2:
"max_top_curry C⟨s⟩ = MFun Ap [x, C'']" "x = MHole ∨ (∃x'. x = MVar x')"
using 𝔏⇩2.simps by blast
then obtain ss1 C' ss2 where C_def: "C = More Ap ss1 C' ss2" using assms(4)
proof (induction C)
case (More f ss1 C' ss2)
from More(2,3) show ?thesis using assms(2) by (simp split: if_splits)
qed simp
have length1: "length ss1 + length ss2 = Suc 0" using assms(2) fresh
unfolding C_def layer_system_sig.𝒯_def ℱ⇩U_def by simp
then consider "length ss1 = 0" | "length ss2 = 0" by linarith
hence "C'' = max_top_cu' 0 C'⟨s⟩ ∧ length ss1 = Suc 0"
proof cases
case ss1_0: 1
hence "False" using in_𝔏⇩2 assms(1) length1
unfolding C_def funposs_mctxt_def by (simp split: if_splits) fastforce
thus ?thesis by simp
next
case ss2_0: 2
thus ?thesis using in_𝔏⇩2 assms(1) length1 unfolding C_def
by (simp split: if_splits) (metis nth_append_length)
qed
hence C''_def: "C'' = max_top_cu' 0 C'⟨s⟩" "length ss1 = Suc 0" "length ss2 = 0"
using length1 by simp+
have pos: "hole_pos C' ∈ funposs_mctxt (max_top_cu' 0 C'⟨s⟩)"
using assms(1) in_𝔏⇩2(1) C''_def(2-)
unfolding C_def C''_def(1) funposs_mctxt_def by (simp split: if_splits)
obtain D' k' where D'_def: "mt_cu' 0 C'⟨s⟩ = D'⟨mt_cu' k' s⟩ ∧ hole_pos C' = hole_pos D' ∧
max_top_cu' k' s ≠ MHole" "k' = 0 ∧ C' ≠ Hole ⟶ check_weak_persists 0 C' s t"
"check_persists s t ∨ k' = 0 ⟶ mt_cu' 0 C'⟨t⟩ = D'⟨mt_cu' k' t⟩"
using push_mt_in_ctxt'[OF pos] by meson
have mt_t: "check_persists s t ∨ k' = 0 ⟶
max_top_curry (Fun Ap (ss1 @ C'⟨t⟩ # ss2)) = MFun Ap [x, max_top_cu' 0 C'⟨t⟩]"
using in_𝔏⇩2 C''_def(2-) nth_append_length[of ss1] missing_args_unfold
unfolding C_def C''_def(1) ctxt_apply_term.simps(2)
by (simp add: nth_append split: if_splits) force
let ?D = "More Ap [mctxt_term_conv x] D' []"
have "mt_curry C⟨s⟩ = ?D⟨mt_cu' k' s⟩ ∧ hole_pos C = hole_pos ?D ∧
max_top_cu' k' s ≠ MHole ∧ (k' = 0 ∧ C ≠ Hole ⟶ check_weak_persists 0 C s t)"
using D'_def(1) in_𝔏⇩2 C''_def(2-) unfolding C_def C''_def(1) ctxt_apply_term.simps(2)
by (simp add: append_Cons_nth_left split: if_splits)
moreover { assume missing: "check_persists s t ∨ k' = 0"
hence "mt_curry C⟨t⟩ = ?D⟨mt_cu' k' t⟩"
using in_𝔏⇩2 C''_def(2-) mt_t unfolding C_def C''_def(1) ctxt_apply_term.simps(2)
D'_def(3)[THEN mp, OF missing, symmetric] by (simp split: if_splits)
}
ultimately show ?thesis by blast
qed
qed
lemma push_mt_in_subst:
assumes "(Ap, 2) ∉ funas_term t" "funas_term t ⊆ ℱ⇩U"
shows "(mt_cu' 0 t) ⋅ (case_option (Var None) (mt_cu' 0 ∘ σ)) = mt_cu' 0 (t ⋅ σ)"
using assms
proof (induction t)
case (Fun f ts)
{ fix x
assume "x ∈ set ts"
hence funas: "(Ap, 2) ∉ funas_term x"
using Fun(2) by fastforce
have "mt_cu' 0 x ⋅ (case_option (Var None) (mt_cu' 0 ∘ σ))
= mt_cu' 0 (x ⋅ σ)"
using Fun(1)[OF _ funas] ‹x ∈ set ts› Fun(2,3) by auto
}
moreover have not_Ap2: "¬(f = Ap ∧ length ts = 2)" using Fun(2) by force
moreover have check1: "check_first_non_Ap 0 (Fun f ts)"
using not_Ap2 Fun(3) 𝒯_def check_fails_Ap[of f ts] by blast
moreover have "check_first_non_Ap 0 (Fun f (map (λt. t ⋅ σ) ts))"
using not_Ap2 check1 by force
ultimately show ?case by (simp only: subst_apply_term.simps max_top_cu'.simps) force
qed auto
lemma push_mt_in_subst_k':
assumes "(Ap, 2) ∉ funas_term t" "funas_term t ⊆ ℱ⇩U"
shows "∃k'. (mt_cu' k t) ⋅ (case_option (Var None) (mt_cu' k' ∘ σ)) = mt_cu' k (t ⋅ σ) ∧
(is_Var t ∨ k' = 0)"
using assms
proof (induction t arbitrary: k)
case (Fun f ts)
{ fix i
assume "i < length ts"
hence funas: "(Ap, 2) ∉ funas_term (ts ! i)"
using Fun(2) by fastforce
hence "mt_cu' 0 (ts ! i) ⋅ (case_option (Var None) (mt_cu' 0 ∘ σ))
= mt_cu' 0 ((ts ! i) ⋅ σ)"
using push_mt_in_subst[OF funas] Fun(3) ‹i < length ts› by fastforce
} note inner = this
have not_Ap2: "¬(f = Ap ∧ length ts = 2)" using Fun(2) by force
thus ?case
proof (cases "check_first_non_Ap k (Fun f ts)")
case check: True
then obtain ts' where ts'_props: "ts' = map (λt. t ⋅ σ) ts" "length ts' = length ts"
by fastforce
hence unfold_mt: "max_top_cu' k (Fun f ts ⋅ σ) = MFun f (map (max_top_cu' 0) ts')"
using not_Ap2 check by auto
thus ?thesis using not_Ap2 check inner unfolding unfold_mt using ts'_props
by (auto simp: in_set_conv_nth[of _ ts])
next
case not_check: False
thus ?thesis using not_Ap2 by (simp split: if_splits) blast
qed
qed auto
lemma push_mt_in_subst_k_snd:
assumes "r ∈ ℛ ∪ 𝒰" "is_Fun (snd r)"
shows "(mt_cu' k (snd r)) ⋅ (case_option (Var None) (mt_cu' 0 ∘ σ)) =
mt_cu' k ((snd r) ⋅ σ)"
using push_mt_in_subst_k' 𝒰r_props ℛ_props[of "snd r" r] assms by blast
lemma push_mt_in_subst_k_ℛl:
assumes "r ∈ ℛ"
shows "(mt_cu' k (fst r)) ⋅ (case_option (Var None) (mt_cu' 0 ∘ σ)) =
mt_cu' k ((fst r) ⋅ σ)"
proof -
obtain k' where "(mt_cu' k (fst r)) ⋅ (case_option (Var None) (mt_cu' k' ∘ σ)) =
mt_cu' k ((fst r) ⋅ σ) ∧ (is_Var (fst r) ∨ k' = 0)"
using push_mt_in_subst_k'[OF ℛ_props[OF _ assms, of "fst r"]] by blast
moreover have "is_Fun (fst r)" using wfR assms unfolding wf_trs_def
by (metis is_Fun_Fun_conv prod.collapse)
ultimately show ?thesis by fastforce
qed
lemma push_mt_in_subst_k_𝒰l:
assumes "r ∈ 𝒰"
shows "(mt_cu' k (fst r)) ⋅ (case_option (Var None) (mt_cu' 0 ∘ σ)) =
mt_cu' k ((fst r) ⋅ σ)"
proof -
obtain f ts x n where term_def: "fst r = Fun Ap [(Fun f ts), x]" "is_Var x"
"(f, n) ∈ ℱ" "length ts < n" "∀t⇩i ∈ set ts. is_Var t⇩i"
using 𝒰_def assms by force
have funas: "(Ap, 2) ∉ funas_term (Fun f ts)" "funas_term (Fun f ts) ⊆ ℱ⇩U"
using term_def(2-) fresh unfolding ℱ_def ℱ⇩U_def by fastforce+
hence "(mt_cu' (Suc k) (Fun f ts)) ⋅ (case_option (Var None) (mt_cu' 0 ∘ σ)) =
mt_cu' (Suc k) (Fun f ts ⋅ σ)"
using push_mt_in_subst_k' by blast
moreover have "mt_cu' 0 x ⋅ case_option (Var None) (mt_cu' 0 ∘ σ) =
mt_cu' 0 (x ⋅ σ)"
using term_def(2) by fastforce
ultimately have core:
"mctxt_term_conv (MFun Ap [max_top_cu' (Suc k) (map (λt. t ⋅ σ) [Fun f ts, x] ! 0),
max_top_cu' 0 (map (λt. t ⋅ σ) [Fun f ts, x] ! 1)]) =
Fun Ap [mt_cu' (Suc k) (Fun f ts) ⋅ case_option (Var None) (mt_cu' 0 ∘ σ),
mt_cu' 0 x ⋅ case_option (Var None) (mt_cu' 0 ∘ σ)]" by fastforce
have check: "check_first_non_Ap k (Fun Ap [Fun f ts, x]) =
check_first_non_Ap k (Fun Ap [Fun f ts, x] ⋅ σ)"
using term_def(3-) arity_def fresh unfolding ℱ_def by force
show ?thesis using check core unfolding term_def(1) by auto
qed
lemma mt_cu'k_ℛ':
assumes "check_first_non_Ap k t" "(Ap, 2) ∉ funas_term t" "t ∈ 𝒯"
shows "max_top_cu' k t = mctxt_of_term t"
using assms
proof (induction rule: max_top_cu'.induct)
case (2 n f ts)
have not_Ap2: "¬ (f = Ap ∧ length ts = 2)" using 2(5) by simp
moreover { fix i
assume "i < length ts"
hence in_𝒯: "(ts ! i) ∈ 𝒯" using 𝒯_subt_at[OF 2(6), of "<i>"] by simp
have no_Aps: "(Ap, 2) ∉ funas_term (ts ! i)"
using 2(5) ‹i < length ts› by fastforce
hence "max_top_cu' 0 (ts ! i) = mctxt_of_term (ts ! i)"
proof (cases "is_Var (ts ! i)")
case funs: False
then obtain f' ts' where ts_i: "ts ! i = Fun f' ts'" by fast
have check0: "check_first_non_Ap 0 (ts ! i)"
using check_fails_Ap[OF _ in_𝒯[unfolded ts_i]] no_Aps
unfolding ts_i by fastforce
thus ?thesis using 2(3)[OF 2(4) not_Ap2 _ check0 no_Aps in_𝒯]
‹i < length ts› by simp
qed auto
}
thus ?case using not_Ap2 2(4) in_set_idx[of _ ts] by (auto split: if_splits)
qed simp
lemma mt_cu'k_ℛ:
assumes "check_first_non_Ap k t"
"t = fst r ∨ t = snd r" "r ∈ ℛ"
shows "max_top_cu' k t = mctxt_of_term t"
using ℛ_props[OF assms(2,3)] mt_cu'k_ℛ'[OF assms(1) _] 𝒯_def by blast
lemma mt_cu'k_𝒰r:
assumes "check_first_non_Ap k (snd r)" "r ∈ 𝒰"
shows "max_top_cu' k (snd r) = mctxt_of_term (snd r)"
using 𝒰r_props[OF assms(2)] mt_cu'k_ℛ'[OF assms(1) _] 𝒯_def by blast
lemma mt_cu'k_𝒰l:
assumes "check_first_non_Ap k (fst r)" "r ∈ 𝒰"
shows "max_top_cu' k (fst r) = mctxt_of_term (fst r)"
proof -
obtain f ts x n where term_def: "fst r = Fun Ap [(Fun f ts), x]" "is_Var x"
"(f, n) ∈ ℱ" "length ts < n" "∀t⇩i ∈ set ts. is_Var t⇩i"
using 𝒰_def assms(2) by force
have no_Aps: "(Ap, 2) ∉ funas_term (Fun f ts)"
using term_def fresh unfolding ℱ_def by fastforce
have in_𝒯: "Fun f ts ∈ 𝒯" using term_def
unfolding layer_system_sig.𝒯_def ℱ⇩U_def ℱ_def is_Var_def by auto
have inner_check: "check_first_non_Ap (Suc k) (Fun f ts)"
using assms(1) term_def by simp
show ?thesis using assms(1) mt_cu'k_ℛ'[OF inner_check no_Aps in_𝒯] term_def(1,2)
by force
qed
lemma case_option_Some:
shows "case_option n s ∘ Some = s"
by fastforce
lemma check_remove_subst_lhs_ℛ:
assumes "check_first_non_Ap k (t ⋅ σ)" "t = fst r" "r ∈ ℛ"
shows "check_first_non_Ap k t"
proof -
have funas: "(Ap, 2) ∉ funas_term t" "funas_term t ⊆ ℱ⇩U"
using ℛ_props[OF _ assms(3)] assms(2) by blast+
obtain f ts where t_def: "t = Fun f ts"
using assms(2,3) wfR unfolding wf_trs_def by (metis prod.collapse)
with assms(1) funas show ?thesis by fastforce
qed
lemma check_remove_subst_lhs_𝒰:
assumes "check_first_non_Ap k (t ⋅ σ)" "t = fst r" "r ∈ 𝒰"
shows "check_first_non_Ap k t"
proof -
obtain f ts x n where term_def: "t = Fun Ap [(Fun f ts), x]" "is_Var x"
"(f, n) ∈ ℱ" "length ts < n" "∀t⇩i ∈ set ts. is_Var t⇩i"
using 𝒰_def assms by force
have funas: "(Ap, 2) ∉ funas_term (Fun f ts)" "funas_term (Fun f ts) ⊆ ℱ⇩U"
using term_def(2-) fresh unfolding ℱ_def ℱ⇩U_def by fastforce+
obtain g ss where t_def: "t = Fun g ss"
using assms(2,3) wfU unfolding wf_trs_def by (metis prod.collapse)
with assms(1) funas term_def show ?thesis
proof (induction rule: check_first_non_Ap.induct)
case (2 n g' ss')
thus ?case by auto
qed blast
qed
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 :: "('f, 'v) term × ('f, 'v) term" and σ
assumes "s ∈ 𝒯" and "t ∈ 𝒯" and in_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 "is_Fun s"
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 = Fun f ts" using ‹is_Fun s› by auto
have max_top_curry_equiv: "max_top s = max_top_curry s"
using max_top_curry_correct[OF ‹s ∈ 𝒯›] .
have check0l: "check_first_non_Ap 0 (fst r ⋅ σ)" using check_lhs[OF ‹r ∈ ℛ ∪ 𝒰›] by simp
note in_fp = in_funposs[unfolded p_def max_top_curry_equiv]
have "∃D k. mt_curry C⟨fst r ⋅ σ⟩ = D⟨mt_cu' k (fst r ⋅ σ)⟩ ∧ hole_pos C = hole_pos D ∧
max_top_cu' k (fst r ⋅ σ) ≠ MHole ∧
(check_persists (fst r ⋅ σ) (snd r ⋅ σ) ∨ (C ≠ Hole ∧ k = 0) ⟶
mt_curry C⟨snd r ⋅ σ⟩ = D⟨mt_cu' k (snd r ⋅ σ)⟩)"
proof (cases C)
case Hole
hence "max_top_curry C⟨fst r ⋅ σ⟩ = max_top_cu' 0 C⟨fst r ⋅ σ⟩"
"max_top_cu' 0 (fst r ⋅ σ) ≠ MHole"
using max_top_curry_cu_equiv check_lhs[OF ‹r ∈ ℛ ∪ 𝒰›, of σ] ‹s = Fun f ts›
s_def_t_def(1) unfolding max_top_cu_equiv by simp+
moreover
{ assume "check_persists (fst r ⋅ σ) (snd r ⋅ σ)"
hence check0r: "check_first_non_Ap 0 (snd r ⋅ σ)"
using check0l missing_args_unfold le_trans by blast
moreover have is_fun: "is_Fun (snd r ⋅ σ)" using check0r by auto
ultimately have "max_top_curry C⟨snd r ⋅ σ⟩ = max_top_cu' 0 C⟨snd r ⋅ σ⟩"
using max_top_curry_cu_equiv s_def_t_def(2) Hole by fastforce
}
ultimately show ?thesis using Hole
by (metis ctxt_apply_term.simps(1) hole_pos.simps(1))
next
case (More f ss1 C' ss2)
show ?thesis using push_mt_in_ctxt[OF in_fp[unfolded s_def_t_def], of "snd r ⋅ σ"]
‹s ∈ 𝒯› ‹t ∈ 𝒯› unfolding s_def_t_def More by blast
qed
then obtain D k where part1:
"mt_curry C⟨fst r ⋅ σ⟩ = D⟨mt_cu' k (fst r ⋅ σ)⟩" "hole_pos C = hole_pos D"
"max_top_cu' k (fst r ⋅ σ) ≠ MHole"
"check_persists (fst r ⋅ σ) (snd r ⋅ σ) ∨ (C ≠ Hole ∧ k = 0) ⟶
mt_curry C⟨snd r ⋅ σ⟩ = D⟨mt_cu' k (snd r ⋅ σ)⟩"
by blast
from part1(3) have check_fst_σ: "check_first_non_Ap k (fst r ⋅ σ)"
using check_first_non_Ap.elims(2)[OF check_lhs[OF ‹r ∈ (ℛ ∪ 𝒰)›]]
by (metis max_top_cu'.simps(2))
hence check_fst_r: "check_first_non_Ap k (fst r)"
using check_remove_subst_lhs_ℛ[OF check_fst_σ] ‹r ∈ (ℛ ∪ 𝒰)›
check_remove_subst_lhs_𝒰[OF check_fst_σ] by blast
let ?σ' = "case_option (Var None) (mt_cu' 0 ∘ σ)"
let ?τ' = "mt_cu' 0 ∘ σ"
have part2: "mt_cu' k (fst r ⋅ σ) = (mt_cu' k (fst r)) ⋅ ?σ'"
using push_mt_in_subst_k_ℛl[of r k σ] push_mt_in_subst_k_𝒰l[of r k σ]
‹r ∈ (ℛ ∪ 𝒰)› by (metis UnE)
have part2_2: "mt_cu' k (fst r) = (fst r) ⋅ (Var ∘ Some)"
using mt_cu'k_ℛ[of k "fst r" r] mt_cu'k_𝒰l[of k r]
check_fst_r UnE[OF ‹r ∈ (ℛ ∪ 𝒰)›] mctxt_term_conv_mctxt_of_term by metis
have first_half: "mt_curry s = D⟨fst r ⋅ ?τ'⟩"
using s_def_t_def(1) part1 part2 part2_2 by (auto simp: var_subst_comp case_option_Some)
consider (is_fun) "is_Fun (snd r) ∨ C ≠ Hole" | (is_var) "is_Var (snd r) ∧ C = Hole" by blast
thus ?thesis
proof cases
case is_fun
{ assume "is_Var (snd r)"
hence "r ∈ ℛ" using 𝒰_def ‹r ∈ (ℛ ∪ 𝒰)› by fastforce
have "k = 0" using check_lhs_ℛ_k0[OF ‹r ∈ ℛ› check_fst_σ] .
} note var_imp_k0 = this
hence missing: "check_persists (fst r ⋅ σ) (snd r ⋅ σ) ∨ (C ≠ □ ∧ k = 0)"
using is_fun rules_missing_persist[OF ‹r ∈ (ℛ ∪ 𝒰)›] missing_args_unfold by metis
have part3: "(mt_cu' k (snd r)) ⋅ ?σ' = mt_cu' k (snd r ⋅ σ)"
using push_mt_in_subst_k_snd[OF ‹r ∈ (ℛ ∪ 𝒰)›] is_fun var_imp_k0
by (cases "is_Var (snd r)") force+
have part3_2: "mt_cu' k (snd r) = (snd r) ⋅ (Var ∘ Some)"
proof (cases "is_Var (snd r)")
case True
thus ?thesis using mctxt_term_conv_mctxt_of_term by auto
next
case False
have check_snd_r: "check_first_non_Ap k (snd r)"
using check_fst_r rules_missing_persist[OF ‹r ∈ (ℛ ∪ 𝒰)› False, of Var]
missing_args_unfold[of _ k] unfolding subst.cop_nil by metis
thus ?thesis using mt_cu'k_ℛ[of k "snd r" r] mt_cu'k_𝒰r[of k r]
check_snd_r UnE[OF ‹r ∈ (ℛ ∪ 𝒰)›] mctxt_term_conv_mctxt_of_term by metis
qed
have part4: "mt_curry C⟨snd r ⋅ σ⟩ = D⟨mt_cu' k (snd r ⋅ σ)⟩"
using part1(4) missing by blast
have second_half: "D⟨snd r ⋅ ?τ'⟩ = mt_curry C⟨snd r ⋅ σ⟩"
using part3 part3_2 part4 by (auto simp: var_subst_comp case_option_Some)
hence "(mt_curry C⟨fst r ⋅ σ⟩, mt_curry C⟨snd r ⋅ σ⟩)
∈ rstep_r_p_s' (ℛ ∪ 𝒰) r p ?τ'"
using first_half rstep_s_t ‹r ∈ (ℛ ∪ 𝒰)› part1(2) p_def
by (metis rstep_r_p_s'.rstep_r_p_s' s_def_t_def(1))
hence W: "∃ τ. max_top_curry C⟨snd r ⋅ σ⟩ ∈ 𝔏 ∧
(mctxt_term_conv ?M, mt_curry C⟨snd r ⋅ σ⟩)
∈ rstep_r_p_s' (ℛ ∪ 𝒰) r p τ"
using Un_iff s_def_t_def max_top_curry_equiv assms(2) by auto
then obtain τ where step_to_L: "(mctxt_term_conv ?M, mctxt_term_conv
(max_top_curry C⟨snd r ⋅ σ⟩)) ∈ rstep_r_p_s' (ℛ ∪ 𝒰) r p τ" by auto
thus ?thesis using max_top_curry_correct[OF ‹t ∈ 𝒯›]
unfolding s_def_t_def(2) max_top_curry_equiv by auto
next
case is_var
hence "r ∈ ℛ" using 𝒰_def ‹r ∈ (ℛ ∪ 𝒰)› by fastforce
have step: "(fst r ⋅ (mt_cu' 0 ∘ σ), snd r ⋅ (mt_cu' 0 ∘ σ))
∈ rstep_r_p_s' (ℛ ∪ 𝒰) r ε ?τ'"
using s_def_t_def(3)
by (metis ctxt_apply_term.simps(1) hole_pos.simps(1) rstep_r_p_s'.simps)
have hole: "C = Hole" using is_var by simp
have "D = Hole" using part1(2) hole p_def by (cases D) simp+
have "p = ε" using hole p_def by simp
thus ?thesis
proof (cases "is_Fun (snd r ⋅ σ)")
case is_fun_σ: True
then obtain g ss where term_def: "snd r ⋅ σ = Fun g ss" by blast
thus ?thesis
proof (cases "check_first_non_Ap 0 (snd r ⋅ σ)")
case check: True
hence mt_t: "mctxt_term_conv (max_top t) = snd r ⋅ (mt_cu' 0 ∘ σ)"
using is_var max_top_curry_correct[OF ‹t ∈ 𝒯›] max_top_curry_cu_equiv[of g ss] term_def
unfolding s_def_t_def(2) hole by force
show ?thesis using step
unfolding first_half max_top_curry_equiv ‹D = Hole› mt_t ‹p = ε› by auto
next
case not_check: False
hence "max_top_cu' 0 (snd r ⋅ σ) = MHole" using term_def by auto
hence mt_hole: "snd r ⋅ (mt_cu' 0 ∘ σ) = Var None" using is_var by auto
thus ?thesis using step
unfolding first_half ‹D = Hole› mt_hole max_top_curry_equiv ‹p = ε› by auto
qed
next
case is_var_σ: False
then obtain x where mt_x: "max_top_cu' 0 (snd r ⋅ σ) = MVar x" by auto
hence mt_var: "snd r ⋅ (mt_cu' 0 ∘ σ) = Var (Some x)"
using is_var is_var_σ by auto
have "max_top (snd r ⋅ σ) = MVar x" using is_var_σ mt_x by auto
thus ?thesis using step is_var is_var_σ mt_var
unfolding first_half ‹D = Hole› max_top_curry_equiv
s_def_t_def(2) hole ‹p = ε› by auto
qed
qed
qed
interpretation layered "ℱ⇩U" "𝔏" "ℛ ∪ 𝒰"
text ‹done (Franziska)›
proof
show "wf_trs (ℛ ∪ 𝒰)" using wfR wfU by (auto simp: wf_trs_def)
next
show "funas_trs (ℛ ∪ 𝒰) ⊆ ℱ⇩U" using sigR sigU unfolding ℱ⇩U_def by auto
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 "is_Fun s" | "is_Var s" using ‹s ∈ 𝒯› 𝒯_def by (cases s) auto
thus ?thesis
proof cases
case 1 thus ?thesis using lemma_C⇩1 assms rstep_s_t s_def_t_def p_def by auto
next
case 2
have wf_RU: "wf_trs (ℛ ∪ 𝒰)" using wfR wfU unfolding wf_trs_def by blast
show ?thesis
using rstep_s_t NF_Var[OF wf_RU] rstep_eq_rstep'
rstep'_iff_rstep_r_p_s' prod.collapse 2 unfolding is_Var_def by metis
qed
qed
next
fix L N :: "('f, 'v) mctxt" and p :: pos
assume assms: "N ∈ 𝔏" "L ∈ 𝔏" "L ≤ N" "p ∈ hole_poss L"
thus "mreplace_at L p (subm_at N p) ∈ 𝔏"
proof (cases p)
case Empty thus ?thesis using assms by simp
next
case (PCons i p')
have p_poss_N: "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
hence subN_𝔏⇩1: "𝔏⇩1 (subm_at N p)" using ‹N ∈ 𝔏› PCons by simp
have subL_𝔏⇩1: "𝔏⇩1 (subm_at L p)" using ‹L ∈ 𝔏› ‹p ∈ hole_poss L› PCons by auto
hence missing: "∀n. missing_args (subm_at L p) n ≥ 1
⟶ missing_args (subm_at N p) n ≥ 1"
using ‹p ∈ hole_poss L› by simp
consider "𝔏⇩1 L" | "𝔏⇩2 L" using ‹L ∈ 𝔏› unfolding 𝔏_def by blast
thus ?thesis
proof cases
case 1
have "𝔏⇩1 (mreplace_at L p (subm_at N p))"
using replace_𝔏⇩1[OF ‹𝔏⇩1 L› subL_𝔏⇩1 subN_𝔏⇩1 _ missing] ‹p ∈ hole_poss L›
all_poss_mctxt_conv by blast
thus ?thesis unfolding 𝔏_def by simp
next
case 2
then obtain C C' where L_def: "L = MFun Ap [C, C']" "𝔏⇩1 C'" using 𝔏⇩2.simps[of L] by blast
have "subm_at L p = MHole" using ‹p ∈ hole_poss L› by simp
hence "(∃f Cs. subm_at N p = MFun f Cs) ∨
𝔏⇩2 (mreplace_at L p (subm_at L p)) = 𝔏⇩2 (mreplace_at L p (subm_at N p))"
using p_poss_N replace_var_holes2[of p L "subm_at L p" "subm_at N p"]
‹p ∈ hole_poss L› all_poss_mctxt_conv[of L] by (cases "subm_at N p") blast+
moreover have "𝔏⇩2 (mreplace_at L p (subm_at L p))"
using 2 ‹p ∈ hole_poss L› all_poss_mctxt_conv[of L] replace_at_subm_at by fastforce
ultimately consider "∃f Cs. subm_at N p = MFun f Cs" | "𝔏⇩2 (mreplace_at L p (subm_at N p))"
by blast
thus ?thesis using 𝔏_def
proof cases
case mfun: 1
then obtain f' Cs' where sub_N_def: "subm_at N p = MFun f' Cs'" by blast
thus ?thesis
proof (cases "p = <0>")
case True
obtain f Cs where N_def: "N = MFun f Cs" using p_poss_N unfolding PCons
by (metis 2(1) 𝔏⇩1.simps assms(3) disjoint less_eq_mctxtE2(2) pos.distinct(1)
subm_at.elims mctxt_order_bot.bot.extremum_uniqueI)
hence f_props: "f = Ap ∧ length Cs = 2"
using 𝔏⇩2.cases[OF 2] less_eq_mctxt_MFunE2[OF ‹L ≤ N›[unfolded N_def]]
by (metis length_Cons mctxt.distinct(5) mctxt.inject(2) numeral_2_eq_2 list.size(3))
moreover have "𝔏⇩1 N" using N_def f_props sub_N_def ‹N ∈ 𝔏› 𝔏⇩2.cases[of N] unfolding 𝔏_def True
by (metis mctxt.simps(6,8) mem_Collect_eq nth_Cons_0 subm_at.simps(1,2))
ultimately have "missing_args (subm_at N p) (Suc 0) ≥ 1"
using p_poss_N sub_N_def 𝔏⇩1.simps[of "MFun f Cs"] unfolding N_def True by fastforce
hence "𝔏⇩1 (MFun Ap [subm_at N p, C'])"
using subN_𝔏⇩1 𝔏⇩1.simps[of "MFun Ap [subm_at N p, C']"] L_def(2) f_props by blast
thus ?thesis using 𝔏_def ‹p ∈ hole_poss L› f_props 2 ‹L ≤ N›
unfolding True N_def L_def(1) by force
next
case False
show ?thesis using replace_𝔏⇩2[OF ‹𝔏⇩2 L› subL_𝔏⇩1 subN_𝔏⇩1 _ missing] False
‹p ∈ hole_poss L› all_poss_mctxt_conv by blast
qed
qed auto
qed
qed
qed
abbreviation 𝒯⇩𝔏 where "𝒯⇩𝔏 ≡ { t . mctxt_of_term t ∈ 𝔏 }"
abbreviation 𝒯⇩𝔏⇩1 where "𝒯⇩𝔏⇩1 ≡ { t . 𝔏⇩1 (mctxt_of_term t) }"
abbreviation PP⇩ℛ where "PP⇩ℛ ≡ rstep (ℛ ∪ 𝒰)"
fun try_step :: "('f, 'v) term ⇒ ('f, 'v) term ⇒ ('f, 'v) term" where
"try_step (Var x) t = undefined"
| "try_step (Fun f ts) t = (if f ≠ Ap ∧ arity f > length ts
then Fun f (ts @ [t]) else Fun Ap [Fun f ts, t])"
fun NF_𝒰 :: "('f, 'v) term ⇒ ('f, 'v) term" where
"NF_𝒰 (Var x) = Var x"
| "NF_𝒰 (Fun f ts) = (if f = Ap ∧ length ts = 2 ∧ is_Fun (ts ! 0)
then try_step (NF_𝒰 (ts ! 0)) (NF_𝒰 (ts ! 1))
else Fun f (map NF_𝒰 ts))"
lemma NF_𝒰_consistent:
shows "is_Fun t = is_Fun (NF_𝒰 t)"
proof (induction t)
case (Fun f ts)
hence "length ts = 2 ∧ is_Fun (ts ! 0) ⟶ is_Fun (NF_𝒰 (ts ! 0))" by auto
thus ?case by (auto split: if_splits)
qed simp
lemma fun_args_in_NF:
assumes "∀x ∈ set ts. x ∈ NF_trs R" "∀t'. (Fun f ts, t') ∉ rrstep R"
shows "Fun f ts ∈ NF_trs R"
using assms
by (meson Fun_supt NF_I NF_subterm rstep_args_NF_imp_rrstep)
lemma try_step_correct:
assumes "try_step (Fun f ts) t = t'" "(Fun f ts) ∈ NF_trs 𝒰" "t ∈ NF_trs 𝒰"
"(Fun f ts) ∈ 𝒯" "t ∈ 𝒯"
shows "(Fun Ap [Fun f ts, t], t') ∈ (rstep 𝒰)⇧* ∧ t' ∈ NF_trs 𝒰 ∧ t' ∈ 𝒯"
using assms
proof (induction "Fun f ts" t rule: try_step.induct)
case (2 t) thus ?case
proof (cases "f ≠ Ap ∧ arity f > length ts")
case True
hence t'_def: "t' = Fun f (ts @ [t])" using 2(1) by auto
hence "t' ∈ 𝒯" using True 2(4,5) 𝒯_def ℱ⇩U_def unfolding arity_def by fastforce
obtain x :: 'v where inf: "infinite (UNIV - (vars_term t' ∪ { x }))" "x ∉ vars_term t'"
using infinite_UNIV
by (metis UNIV_eq_I Un_commute finite_Diff2 finite_insert finite_vars_term insert_is_Un)
obtain ts' :: "'v list" where ts'_props:
"(∀t⇩i∈set ts'. is_Var (Var t⇩i))" "length ts' = length ts" "distinct (ts' @ [x])"
"set ts' ∩ vars_term t' = {}"
using infinite_imp_many_elems[OF inf(1), of "length ts"] by auto
let ?vars = "map Var ts'"
have vars_props: "(∀t⇩i∈set ?vars. is_Var t⇩i)" "length ?vars = length ts"
"distinct (?vars @ [Var x])"
using ts'_props distinct_map_Var by auto
moreover obtain n where arity_f: "(f, n) ∈ ℱ" "n > length ts"
using True 2(4) unfolding layer_system_sig.𝒯_def ℱ⇩U_def ℱ_def arity_def by fastforce
ultimately obtain r where r_def:
"r = (Fun Ap [Fun f ?vars, Var x], Fun f (?vars @ [Var x])) ∧ r ∈ 𝒰"
using 𝒰_def by fastforce
let ?σ = "subst_of (zip (x # ts') (t # ts))"
have dom1: "subst_domain (subst x t) = { x }"
using subst_domain_def ‹x ∉ vars_term t'› unfolding t'_def by force
have ts'_ts_distinct: "set ts' ∩ (⋃x∈set ts. vars_term x) = {}"
using ts'_props(4) t'_def by auto
{ fix i
assume "i < length ts'"
hence "subst_of (zip ts' ts) (ts' ! i) = ts ! i"
using ts'_props(2,3) ts'_ts_distinct
proof (induction ts' ts arbitrary: i rule: zip_induct)
case (Cons_Cons a' ts' a ts) thus ?case
proof (cases i)
case 0
have "subst_domain (subst_of (zip ts' ts)) ⊆ set ts'"
using subst_domain_subst_of[of "zip ts' ts"] map_fst_zip[of ts' ts] Cons_Cons(3)
by fastforce
hence "subst_of (zip ts' ts) a' = Var a'"
using Cons_Cons(3,4) notin_subst_domain_imp_Var[of a'] by auto
thus ?thesis using Cons_Cons(2-) unfolding 0
by (auto simp: subst_compose_def)
term "(subst_of (zip ts' ts) a') ⋅ subst a' a"
next
case (Suc n)
hence "subst_of (zip ts' ts) (ts' ! n) = ts ! n"
using Cons_Cons(1)[of n] Cons_Cons(2-) by auto
thus ?thesis using Cons_Cons(2-) unfolding Suc
by (simp add: subst_compose_def)
qed
qed auto
} note maps = this
have dom2: "subst_domain (subst_of (zip ts' ts)) ⊆ set ts'"
using subst_domain_subst_of[of "zip ts' ts"] map_fst_zip[of ts' ts] ts'_props(2)
by fastforce
hence "(Var x) ⋅ (subst_of (zip ts' ts)) = (Var x)"
using vars_props notin_subst_domain_imp_Var[of x "subst_of (zip ts' ts)"] by auto
moreover have "map (λx. x ⋅ (subst_of (zip ts' ts))) ?vars = ts"
using maps vars_props(2) by (simp add: map_nth_eq_conv)
hence "map (λx. x ⋅ ?σ) ?vars = ts"
using vars_props(2) ts'_props(3) notin_subst_domain_imp_Var[of "ts' ! _" "subst x t"]
‹x ∉ vars_term t'› unfolding dom1 t'_def
by (auto simp: map_nth_eq_conv)
moreover have "(λx. x ⋅ σ ⋅ τ) ∘ Var = (λt. t ⋅ τ) ∘ ((λt. t ⋅ σ) ∘ Var)"
for σ τ :: "('f, 'v) subst" by auto
ultimately have "(Fun Ap [Fun f ts, t], t') ∈ rstep_r_p_s 𝒰 r ε ?σ"
using r_def vars_props unfolding t'_def rstep_r_p_s_def by force
hence reach:"(Fun Ap [Fun f ts, t], t') ∈ (rstep 𝒰)⇧*"
using rrstep_imp_rstep rstep_r_p_s_imp_rstep[of _ _ 𝒰 r ε ?σ] by fastforce
{ fix i
assume "i < length (ts @ [t])"
hence "(ts @ [t]) ! i ∈ NF_trs 𝒰" using 2(3) NF_subterm[OF 2(2), of "ts ! i"]
by (cases "i = length ts") (auto simp: append_Cons_nth_left)
} note args_NF = this
{ assume "∃u. (t', u) ∈ rstep 𝒰"
then obtain u where step: "(t', u) ∈ rstep 𝒰" by blast
have "(t', u) ∈ rrstep 𝒰"
using rstep_args_NF_imp_rrstep[OF step] args_NF supt_Fun_imp_arg_supteq[of f "ts @ [t]"]
in_set_idx[of _ "ts @ [t]"] NF_subterm[of "(ts @ [t]) ! _" 𝒰]
unfolding t'_def by metis
then obtain l r σ where rule_subst: "(l, r) ∈ 𝒰 ∧ t' = l⋅σ ∧ u = r⋅σ"
unfolding rrstep_def' by fast
then obtain f' ts' x where "l = Fun Ap [Fun f' ts', x]" "r = Fun f' (ts' @ [x])"
using 𝒰_def by force
hence False using rule_subst True unfolding t'_def by simp
}
hence "t' ∈ NF_trs 𝒰" by auto
thus ?thesis using reach ‹t' ∈ 𝒯› by blast
next
case False
hence t'_def: "t' = Fun Ap [Fun f ts, t]" using 2 by force
hence "t' ∈ 𝒯" using 2(4,5) 𝒯_def ℱ⇩U_def by auto
moreover {
assume "∃u. (t', u) ∈ rstep 𝒰"
then obtain u where step: "(t', u) ∈ rstep 𝒰" by blast
have "(t', u) ∈ rrstep 𝒰"
using rstep_args_NF_imp_rrstep[OF step] 2(1-3) supt_Fun_imp_arg_supteq[of Ap "[Fun f ts, t]"]
in_set_idx[of "[Fun f ts, t] ! _" "[Fun f ts, t]"] NF_subterm[of _ 𝒰]
unfolding t'_def by (metis in_set_simps(1,2))
then obtain l r σ where rule_subst: "(l, r) ∈ 𝒰 ∧ t' = l⋅σ ∧ u = r⋅σ"
unfolding rrstep_def' by fast
then obtain f' ts' x n where "l = Fun Ap [Fun f' ts', x]" "r = Fun f' (ts' @ [x])"
"(f', n) ∈ ℱ" "length ts' < n"
using 𝒰_def by force
hence False using rule_subst False fresh unfolding t'_def ℱ_def arity_def by simp
}
ultimately show ?thesis unfolding t'_def by blast
qed
qed
lemma try_step_persists_r:
shows "∃D. try_step (Fun f ts) t = D⟨t⟩ ∧ (∀s. try_step (Fun f ts) s = D⟨s⟩)"
proof -
let ?D = "More Ap [Fun f ts] □ []"
have "?D⟨t⟩ = Fun Ap [Fun f ts, t] ∧ (∀s. ?D⟨s⟩ = Fun Ap [Fun f ts, s])" by simp
hence "∃D. D⟨t⟩ = Fun Ap [Fun f ts, t] ∧ (∀s. D⟨s⟩ = Fun Ap [Fun f ts, s])" by blast
moreover have "∃D. D⟨t⟩ = Fun f (ts @ [t]) ∧ (∀s. D⟨s⟩ = Fun f (ts @ [s]))"
by (metis ctxt_apply_term.simps(1,2))
ultimately show ?thesis by auto
qed
lemma NF_𝒰_persists:
assumes "∀C' f ss2. C = C' ∘⇩c (More f [] □ ss2) ⟶ f ≠ Ap"
shows "∃D. NF_𝒰 C⟨t⟩ = D⟨NF_𝒰 t⟩ ∧
(∀s. NF_𝒰 C⟨s⟩ = D⟨NF_𝒰 s⟩)"
proof (cases C rule: ctxt_exhaust_rev)
case (More D f ss1 ss2)
let ?D' = "λx. More f (map NF_𝒰 ss1) □ (map NF_𝒰 ss2 @ x)"
have "∃g tt1 tt2. NF_𝒰 (Fun f (ss1 @ t # ss2)) = (More g tt1 □ tt2)⟨NF_𝒰 t⟩ ∧
(∀s. NF_𝒰 (Fun f (ss1 @ s # ss2)) = (More g tt1 □ tt2)⟨NF_𝒰 s⟩)"
proof (cases ss1)
case Nil
hence "f ≠ Ap" using More assms by blast
thus ?thesis using Nil by auto
next
case (Cons a ls) thus ?thesis
proof (cases "f = Ap ∧ length (ss1 @ t # ss2) = 2 ∧ is_Fun ((ss1 @ t # ss2) ! 0)")
case True
then obtain g ss where NF_a: "NF_𝒰 a = Fun g ss" using NF_𝒰_consistent[of a] Cons by auto
show ?thesis using True NF_a unfolding Cons
by auto (metis append_Cons append_Nil)+
next
case False
thus ?thesis unfolding Cons
by (simp split: if_splits) (metis append_Cons)+
qed
qed
thus ?thesis unfolding More Nil
proof (induction D)
case Hole_D: Hole thus ?case
by simp (metis ctxt_apply_term.simps(1) ctxt_apply_term.simps(2))
next
case More_D: (More f' ss1' D' ss2')
then obtain E' where inner: "NF_𝒰 (D' ∘⇩c More f ss1 □ ss2)⟨t⟩ = E'⟨NF_𝒰 t⟩ ∧
(∀s. NF_𝒰 (D' ∘⇩c More f ss1 □ ss2)⟨s⟩ = E'⟨NF_𝒰 s⟩)"
by blast
then obtain g tt1 F tt2 where E'_def: "E' = More g tt1 F tt2"
by (cases E') (auto, metis NF_𝒰.simps(1) NF_𝒰_consistent
ctxt_apply_eq_False ctxt_apply_term.simps(2) is_VarE is_VarI)
let ?ts = "λt. ss1' @ D'⟨Fun f (ss1 @ t # ss2)⟩ # ss2'"
have is_Fun_persists: "is_Fun (?ts t ! 0) = is_Fun (?ts s ! 0)" for s
by (cases ss1', cases D') auto
show ?case
proof (cases "f' = Ap ∧ length (?ts t) = 2 ∧ is_Fun (?ts t ! 0)")
case step: True
then consider "ss1' = []" | "∃a. ss1' = [a]"
by simp (metis length_0_conv length_Suc_conv one_is_add)
hence "∃D. try_step (NF_𝒰 ((ss1' @ D'⟨Fun f (ss1 @ t # ss2)⟩ # ss2') ! 0))
(NF_𝒰 ((ss1' @ D'⟨Fun f (ss1 @ t # ss2)⟩ # ss2') ! Suc 0)) =
D⟨NF_𝒰 t⟩ ∧ (∀s. try_step (NF_𝒰 ((ss1' @ D'⟨Fun f (ss1 @ s # ss2)⟩ # ss2') ! 0))
(NF_𝒰 ((ss1' @ D'⟨Fun f (ss1 @ s # ss2)⟩ # ss2') ! Suc 0)) =
D⟨NF_𝒰 s⟩)"
proof cases
case 1
thus ?thesis using inner is_Fun_persists E'_def
by (auto split: if_splits) (metis ctxt_apply_term.simps(2),
(metis (no_types) append.left_neutral ctxt_apply_term.simps(2))+)
next
case 2
then obtain a where ss1'_def: "ss1' = [a]" by blast
hence a1: "is_Fun (NF_𝒰 a)" using step NF_𝒰_consistent[of a] by auto
then obtain g' ss where NF_fun: "NF_𝒰 a = Fun g' ss" by blast
then obtain E'' where try_1: "try_step (Fun g' ss) (Fun g (tt1 @ F⟨NF_𝒰 t⟩ # tt2)) =
E''⟨Fun g (tt1 @ F⟨NF_𝒰 t⟩ # tt2)⟩ ∧ (∀s. try_step (Fun g' ss) s = E''⟨s⟩)"
using try_step_persists_r[of g' ss "Fun g (tt1 @ F⟨NF_𝒰 _⟩ # tt2)"]
by blast
let ?D = "E'' ∘⇩c E'"
have try_2: "try_step (NF_𝒰 a) (Fun g (tt1 @ F⟨NF_𝒰 t⟩ # tt2)) = ?D⟨NF_𝒰 t⟩ ∧
(∀s. try_step (NF_𝒰 a) (Fun g (tt1 @ F⟨NF_𝒰 s⟩ # tt2)) = ?D⟨NF_𝒰 s⟩)"
using try_1 unfolding E'_def NF_fun by simp
show ?thesis using inner E'_def try_2 NF_fun unfolding ss1'_def
by simp (metis NF_fun try_1 try_2)
qed
thus ?thesis using step is_Fun_persists by auto
next
case no_step: False
thus ?thesis using inner is_Fun_persists
by (auto split: if_splits) (metis ctxt_apply_term.simps(2))+
qed
qed
qed (metis ctxt.cop_nil)
lemma NF_𝒰_correct:
assumes "NF_𝒰 t = t'" "t ∈ 𝒯"
shows "(t, t') ∈ (rstep 𝒰)⇧* ∧ t' ∈ NF_trs 𝒰 ∧ t' ∈ 𝒯"
using assms
proof (induction t arbitrary: t' rule: NF_𝒰.induct)
case (1 x)
thus ?case using NF_I no_Var_rstep[OF wfU, of x] by fastforce
next
case (2 f ts) thus ?case
proof (cases "f = Ap ∧ length ts = 2 ∧ is_Fun (ts ! 0)")
case use_try_step: True
hence "ts ! 0 ∈ 𝒯" "ts ! 1 ∈ 𝒯" using 𝒯_subt_at[OF 2(5), of "<_>"] by simp+
then obtain g ss where NF_ts0: "NF_𝒰 (ts ! 0) = Fun g ss"
using NF_𝒰_consistent use_try_step by blast
hence NF_ts_props: "(ts ! 0, Fun g ss) ∈ (rstep 𝒰)⇧*" "(ts ! 1, NF_𝒰 (ts ! 1)) ∈ (rstep 𝒰)⇧*"
"Fun g ss ∈ NF_trs 𝒰" "NF_𝒰 (ts ! 1) ∈ NF_trs 𝒰"
"Fun g ss ∈ 𝒯" "NF_𝒰 (ts ! 1) ∈ 𝒯"
using 2(1)[OF use_try_step NF_ts0 ‹ts ! 0 ∈ 𝒯›] 2(2)[OF use_try_step _ ‹ts ! 1 ∈ 𝒯›]
by blast+
{ fix i
assume "i < length [ts ! 0, ts ! 1]"
hence "([ts ! 0, ts ! 1] ! i, [Fun g ss, NF_𝒰 (ts ! 1)] ! i) ∈ (rstep 𝒰)⇧*"
using NF_ts_props(1,2) less_2_cases[of i] by force
}
hence inner_steps: "∀i<length [ts ! 0, ts ! 1].
([ts ! 0, ts ! 1] ! i, [Fun g ss, NF_𝒰 (ts ! 1)] ! i) ∈ (rstep 𝒰)⇧*" by blast
hence first_part: "(Fun Ap [ts ! 0, ts ! 1], Fun Ap [Fun g ss, NF_𝒰 (ts ! 1)]) ∈ (rstep 𝒰)⇧*"
using use_try_step args_rsteps_imp_rsteps[OF _ inner_steps, of Ap]
by fastforce
moreover have "(Fun Ap [Fun g ss, NF_𝒰 (ts ! 1)], t') ∈ (rstep 𝒰)⇧* ∧ t' ∈ NF_trs 𝒰 ∧ t' ∈ 𝒯"
using try_step_correct[OF _ NF_ts_props(3-)] use_try_step NF_ts0
unfolding 2(4)[symmetric] by force
moreover have "Fun f ts = Fun Ap [ts ! 0, ts ! 1]"
using use_try_step by simp (metis Cons_nth_drop_Suc Suc_leI drop_all lessI nth_drop_0
numeral_2_eq_2 one_add_one zero_less_two)
ultimately show ?thesis by fastforce
next
case False
hence t'_def: "t' = Fun f (map NF_𝒰 ts)"
using False unfolding 2(4)[symmetric] by force
have "∀x ∈ set ts. x ∈ 𝒯" using 𝒯_subt_at[OF 2(5), of "<_>"] in_set_idx[of _ ts] by auto
hence "∀u⊲t'. u ∈ NF_trs 𝒰" using 2(3)[OF False, of _ "NF_𝒰 _"]
unfolding t'_def by fastforce
hence "∃t''. (t', t'') ∈ rstep 𝒰 ⟶ (t', t'') ∈ rrstep 𝒰"
by (simp add: rstep_args_NF_imp_rrstep)
let ?ts = "map NF_𝒰 ts"
{ fix x s :: "('f, 'v) term"
assume assms: "∃t''. (Fun f ?ts, t'') ∈ rrstep 𝒰"
then obtain t'' where "(Fun f ?ts, t'') ∈ rrstep 𝒰" by blast
then obtain r σ where to_t'': "(Fun f ?ts, t'') ∈ rstep_r_p_s 𝒰 r ε σ"
unfolding rrstep_def by fast
then obtain f' ts' y where r_def: "r = (Fun Ap [Fun f' ts', y], Fun f' (ts' @ [y]))"
using 𝒰_def by (auto simp: rstep_r_p_s_eq_rstep_r_p_s')
have "Fun Ap [Fun f' ts', y] ⋅ σ = Fun f ?ts"
using to_t'' unfolding rstep_r_p_s_def r_def by simp
hence False using False NF_𝒰_consistent[of "ts ! 0"] by force
} note no_rrstep = this
moreover have args_props:
"x ∈ set ts ⟶ (x, NF_𝒰 x) ∈ (rstep 𝒰)⇧* ∧ NF_𝒰 x ∈ NF_trs 𝒰 ∧ NF_𝒰 x ∈ 𝒯" for x
using 2(3)[OF False, of _ "NF_𝒰 _"] ‹∀x ∈ set ts. x ∈ 𝒯› by blast
ultimately have "Fun f (map NF_𝒰 ts) ∈ NF_trs 𝒰"
using fun_args_in_NF[of "map NF_𝒰 ts" 𝒰 f] by fastforce
moreover have "(Fun f ts, Fun f (map NF_𝒰 ts)) ∈ (rstep 𝒰)⇧*"
using args_props args_rsteps_imp_rsteps[of ts ?ts 𝒰 f] by simp
moreover have "Fun f (map NF_𝒰 ts) ∈ 𝒯"
using args_props 2(5) 𝒯_def mem_Collect_eq by auto
ultimately show ?thesis unfolding t'_def by blast
qed
qed
lemma NF_𝒰_Cu_subst:
assumes "funas_term t ⊆ ℱ"
shows "NF_𝒰 (Cu t ⋅ σ) = t ⋅ (NF_𝒰 ∘ σ)"
using assms
proof (induction t)
case (Fun f ts)
have arity_f: "arity f ≥ length ts" using Fun(2) ℱ_def arity_def by force
show ?case
proof (cases "f = Ap")
case isAp: True
thus ?thesis using Fun(2) fresh unfolding ℱ_def by fastforce
next
case notAp: False
have "x ∈ set ts ⟹ NF_𝒰 (Cu x ⋅ σ) = x ⋅ (NF_𝒰 ∘ σ)" for x
using Fun by fastforce
thus ?thesis using arity_f
proof (induction "length ts" arbitrary: ts)
case (Suc n)
then obtain ts' a where ts_def: "ts = ts' @ [a]"
by (metis append_Nil2 append_eq_conv_conj id_take_nth_drop lessI)
have Cu_unfold: "Cu (Fun f ts) = Fun Ap [Cu (Fun f ts'), Cu a]"
using notAp unfolding ts_def by simp
have args: "NF_𝒰 (Cu (Fun f ts') ⋅ σ) = Fun f ts' ⋅ (NF_𝒰 ∘ σ)"
"NF_𝒰 (Cu a ⋅ σ) = a ⋅ (NF_𝒰 ∘ σ)"
using Suc(1)[of ts'] Suc(2-) unfolding ts_def by force+
have "is_Fun (Cu (Fun f ts') ⋅ σ)" by (cases ts') simp+
hence NF_𝒰_unfold: "NF_𝒰 (Cu (Fun f ts) ⋅ σ) =
try_step (Fun f ts' ⋅ (NF_𝒰 ∘ σ)) (a ⋅ (NF_𝒰 ∘ σ))"
using args notAp unfolding Cu_unfold by simp
have "arity f > length ts'" using Suc(4) ts_def by simp
hence "try_step (Fun f ts' ⋅ (NF_𝒰 ∘ σ)) (a ⋅ (NF_𝒰 ∘ σ)) = Fun f ts ⋅ (NF_𝒰 ∘ σ)"
using notAp unfolding ts_def by simp
thus ?case unfolding NF_𝒰_unfold by argo
qed simp
qed
qed simp
lemma NF_𝒰_Cu:
assumes "funas_term t ⊆ ℱ"
shows "NF_𝒰 (Cu t) = t"
using NF_𝒰_Cu_subst[OF assms, of Var]
by (simp add: term_subst_eq)
lemma 𝒯_closed_under_PP⇩ℛ:
assumes "t ∈ 𝒯" "(t, t') ∈ PP⇩ℛ⇧*"
shows "t' ∈ 𝒯"
using rsteps_preserve_funas_terms[OF ℛ_sig _ assms(2)] assms(1)[unfolded 𝒯_def] 𝒯_def
by (simp add: trs)
lemma vars_term_partition:
assumes "∀t⇩i∈set ts. is_Var t⇩i" "distinct ts"
shows "is_partition (map vars_term ts)"
using assms
proof (induction ts)
case (Cons a ts)
hence part_ts: "is_partition (map vars_term ts)" by force
thus ?case using Cons(2-) is_partition_Cons by fastforce
qed (auto simp: is_partition_def)
lemma is_partition_merge:
assumes "is_partition (ls @ [a])"
shows "is_partition [⋃x∈set ls. x, a]"
using assms by (induction ls) (auto simp: is_partition_Cons)
lemma linear_𝒰: "linear_trs 𝒰"
proof -
{ fix r
assume "r ∈ 𝒰"
then obtain f ts t where r_def: "r = (Fun Ap [Fun f ts, t], Fun f (ts @ [t]))"
"is_Var t" "∀t⇩i∈set ts. is_Var t⇩i" "distinct (ts @ [t])"
using 𝒰_def by (auto simp: rstep_r_p_s_eq_rstep_r_p_s')
{ fix t :: "('f, 'v) term"
assume "is_Var t"
hence "linear_term t" by fastforce
} note var_linear = this
have partition1: "is_partition (map vars_term ts)"
using r_def(3,4) vars_term_partition[of "ts"] by simp
have partition2: "is_partition (map vars_term (ts @ [t]))"
using r_def vars_term_partition[of "ts @ [t]"] by simp
hence "linear_term (Fun f (ts @ [t]))"
using r_def(2,3) var_linear by simp
moreover have "linear_term (Fun Ap [Fun f ts, t])"
using r_def(2,3) var_linear partition1 partition2
is_partition_merge[of "map vars_term ts" "vars_term t"] by auto
ultimately have "linear_term (fst r) ∧ linear_term (snd r)"
using r_def(1) by auto
}
thus ?thesis unfolding linear_trs_def by force
qed
lemma trivial_cps_𝒰:
assumes st_step: "(s, t) ∈ rstep_r_p_s 𝒰 (l, r) p σ" and
su_step: "(s, u) ∈ rstep_r_p_s 𝒰 (l', r') p' σ'" and
p'_def: "p' = p <#> q" and
fp: "q ∈ funposs l"
shows "u = t"
proof -
obtain f ts x n where rule1_def: "l = Fun Ap [Fun f ts, x]" "r = Fun f (ts @ [x])"
"(f, n) ∈ ℱ" "is_Var x" "∀t⇩i∈set ts. is_Var t⇩i" "distinct (ts @ [x])"
using 𝒰_def st_step by (auto simp: rstep_r_p_s_eq_rstep_r_p_s')
have "f ≠ Ap" using fresh rule1_def(3) unfolding ℱ_def by fastforce
obtain g ss where l_q: "l |_ q = Fun g ss" using fp funposs_fun_conv by blast
moreover obtain C where "C⟨l ⋅ σ⟩ = s" "hole_pos C = p"
using hole_pos_ctxt_of_pos_term[of p s]
Product_Type.Collect_case_prodD[OF st_step[unfolded rstep_r_p_s_def]]
unfolding fst_conv by meson
ultimately obtain ss' where s_p': "s |_ p' = Fun g ss'"
using funposs_imp_poss[OF fp] unfolding p'_def by auto
obtain f' ts' x' where rule2_def: "l' = Fun Ap [Fun f' ts', x']" "r' = Fun f' (ts' @ [x'])"
using 𝒰_def su_step by (auto simp: rstep_r_p_s_eq_rstep_r_p_s')
thus ?thesis
proof (cases q)
case Empty
hence "g = Ap" using l_q rule1_def(1) by simp
have "p' = p" using Empty p'_def by simp
have "l ⋅ σ = l' ⋅ σ'" using ctxt_eq[of _ "l ⋅ σ" "l' ⋅ σ'"]
Product_Type.Collect_case_prodD[OF st_step[unfolded rstep_r_p_s_def]]
Product_Type.Collect_case_prodD[OF su_step[unfolded rstep_r_p_s_def]]
unfolding ‹p' = p› fst_conv by metis
thus ?thesis using Product_Type.Collect_case_prodD[OF st_step[unfolded rstep_r_p_s_def]]
Product_Type.Collect_case_prodD[OF su_step[unfolded rstep_r_p_s_def]]
unfolding ‹p' = p› rule1_def(1,2) rule2_def(1,2) by auto (metis (no_types, lifting))
next
case (PCons i q')
hence "i = 0" using rule1_def fp less_2_cases[of i] by force
moreover have "q' = ε" using rule1_def fp unfolding PCons ‹i = 0›
by auto (fastforce dest: nth_mem)
ultimately have "q = <0>" unfolding PCons by blast
hence "g = f" using rule1_def(1) l_q by auto
have "l' ⋅ σ' = Fun f ss'"
using s_p' Product_Type.Collect_case_prodD[OF su_step[unfolded rstep_r_p_s_def]]
subt_at_ctxt_of_pos_term[of "p #> 0" s "l' ⋅ σ'"]
unfolding ‹g = f› ‹q = <0>› p'_def fst_conv by metis
thus ?thesis using rule2_def(1) ‹f ≠ Ap› by simp
qed
qed
lemma 𝒰_commutes:
assumes "(s, t) ∈ rstep 𝒰" "(s, u) ∈ rstep 𝒰"
shows "∃v. (t, v) ∈ (rstep 𝒰)⇧= ∧ (u, v) ∈ (rstep 𝒰)⇧="
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
obtain l' r' p' σ' where su_step: "(s, u) ∈ rstep_r_p_s 𝒰 (l', r') p' σ'"
using rstep_iff_rstep_r_p_s[of s u 𝒰] assms(2) by blast+
consider "p ⊥ p'" | "p ≤ p'" | "p' ≤ p"
using parallel_pos[of p p'] by blast
thus ?thesis
proof cases
case parallel: 1
thus ?thesis using parallel_steps[OF st_step su_step]
by (blast dest: rstep_r_p_s_imp_rstep[of _ _ 𝒰])
next
case p'_below_p: 2
then obtain q where p'_def: "p' = p <#> q" using less_eq_pos_def by auto
thus ?thesis
proof (cases "q ∈ funposs l")
case fp: True
have "u = t" using trivial_cps_𝒰[OF st_step su_step p'_def fp] .
thus ?thesis by blast
next
case vp: False thus ?thesis
using linear_variable_overlap_commute[OF st_step su_step p'_def _ linear_𝒰] by blast
qed
next
case p_below_p': 3
then obtain q where p_def: "p = p' <#> q" using less_eq_pos_def by auto
thus ?thesis
proof (cases "q ∈ funposs l'")
case fp: True
hence "u = t" using trivial_cps_𝒰[OF su_step st_step p_def fp] by simp
thus ?thesis by blast
next
case vp: False thus ?thesis
using linear_variable_overlap_commute[OF su_step st_step p_def _ linear_𝒰] by blast
qed
qed
qed
lemma diamond_𝒰':
shows "◇ ((rstep 𝒰)⇧=)"
using 𝒰_commutes by (auto simp: diamond_def)
lemma CR_𝒰:
shows "CR (rstep 𝒰)"
using diamond_imp_CR'[OF diamond_𝒰', of "rstep 𝒰"] by blast
lemma NF_𝒰_unique:
assumes "t ∈ NF_trs 𝒰" "t' ∈ NF_trs 𝒰" "(s, t) ∈ (rstep 𝒰)⇧*" "(s, t') ∈ (rstep 𝒰)⇧*"
shows "t = t'"
using assms CR_divergence_imp_join[OF CR_𝒰 assms(3,4)] join_NF_imp_eq[of t t'] by auto
lemma NF_𝒰_in_subst:
assumes "funas_term t ⊆ ℱ"
shows "NF_𝒰 (t ⋅ σ) = t ⋅ (NF_𝒰 ∘ σ)"
using assms
proof (induction t)
case (Fun f ts)
{ fix x
assume "x ∈ set ts"
hence "NF_𝒰 (x ⋅ σ) = x ⋅ (NF_𝒰 ∘ σ)" using Fun by fastforce
} note inner = this
then obtain ts' where ts'_props: "Fun f ts ⋅ σ = Fun f ts'" "length ts' = length ts"
by simp
thus ?case
proof (cases "f = Ap ∧ length ts' = 2 ∧ is_Fun (ts' ! 0)")
case True
thus ?thesis using Fun(2) fresh unfolding ℱ_def by fastforce
next
case False
thus ?thesis using ts'_props inner
by (auto simp: term_subst_eq_conv)
qed
qed simp
lemma NF_𝒰_ℛ_step_persists:
assumes "(s, t) ∈ rstep ℛ" "NF_𝒰 s = s'" "NF_𝒰 t = t'" "s ∈ 𝒯" "𝔏⇩1 (mctxt_of_term s)"
shows "(s', t') ∈ rstep ℛ"
proof -
obtain C l r σ where s_def: "s = C⟨l ⋅ σ⟩" and t_def: "t = C⟨r ⋅ σ⟩" and in_ℛ: "(l, r) ∈ ℛ"
using assms(1) by auto
have "l ⋅ σ ∈ 𝒯" using 𝒯_subt_at[OF assms(4), of "hole_pos C"] unfolding s_def by simp
hence "r ⋅ σ ∈ 𝒯" using 𝒯_closed_under_PP⇩ℛ[of "l ⋅ σ" "r ⋅ σ"] in_ℛ by auto
have funas: "funas_term l ⊆ ℱ" "funas_term r ⊆ ℱ" using in_ℛ sigR
unfolding funas_trs_def funas_rule_def ℱ_def by fastforce+
hence NFs: "NF_𝒰 (l ⋅ σ) = l ⋅ (NF_𝒰 ∘ σ)" "NF_𝒰 (r ⋅ σ) = r ⋅ (NF_𝒰 ∘ σ)"
using NF_𝒰_in_subst funas by blast+
hence step: "(NF_𝒰 (l ⋅ σ), NF_𝒰 (r ⋅ σ)) ∈ rstep ℛ" using in_ℛ by auto
obtain f ts where l_def: "l = Fun f ts" using in_ℛ wfR unfolding wf_trs_def
by fastforce
hence "f ≠ Ap" "arity f = length ts" using in_ℛ sigR fresh
unfolding arity_def funas_trs_def funas_rule_def by fastforce+
moreover obtain ts' where lσ_def: "l ⋅ σ = Fun f ts'" "length ts' = length ts"
using l_def by auto
ultimately have check_lσ: "¬ check_first_non_Ap 1 (l ⋅ σ)" by auto
{ fix C' f' ss1 ss2
assume "C = C' ∘⇩c More f' [] □ ss2"
hence in_𝔏⇩1: "𝔏⇩1 (mctxt_of_term (Fun f' ([] @ l ⋅ σ # ss2)))"
using assms(5) subm_at_layers[of "mctxt_of_term s" "hole_pos C'"] unfolding s_def 𝔏_def
by simp (metis hole_pos_poss list.simps(9) mctxt_of_term.simps(2)
subm_at.simps(1) subm_at_mctxt_of_term subt_at_hole_pos)
have "f' ≠ Ap" using 𝔏⇩1.cases[OF in_𝔏⇩1] check_lσ fresh
unfolding missing_args_unfold[symmetric] ℱ⇩U_def by simp ((cases "f' = Ap"), fastforce)
}
hence no_Ap_above: "∀C' f ss2. C = C' ∘⇩c More f [] □ ss2 ⟶ f ≠ Ap"
by blast
obtain D where "NF_𝒰 s = D⟨NF_𝒰 (l ⋅ σ)⟩ ∧ NF_𝒰 t = D⟨NF_𝒰 (r ⋅ σ)⟩"
using NF_𝒰_persists[OF no_Ap_above]
unfolding s_def t_def by blast
thus ?thesis using step unfolding assms(2,3)[symmetric] NFs s_def t_def
unfolding ctxt_apply_term.simps by force
qed
lemma uncurried_NF:
assumes "(s, t) ∈ PP⇩ℛ" "s ∈ 𝒯" "t ∈ 𝒯" "𝔏⇩1 (mctxt_of_term s)"
shows "(NF_𝒰 s, NF_𝒰 t) ∈ (rstep ℛ)⇧="
proof -
have NFs_props: "(s, NF_𝒰 s) ∈ (rstep 𝒰)⇧* ∧ NF_𝒰 s ∈ NF_trs 𝒰 ∧ NF_𝒰 s ∈ 𝒯"
using NF_𝒰_correct[OF _ assms(2)] by blast
have NFt_props: "(t, NF_𝒰 t) ∈ (rstep 𝒰)⇧* ∧ NF_𝒰 t ∈ NF_trs 𝒰 ∧ NF_𝒰 t ∈ 𝒯"
using NF_𝒰_correct[OF _ assms(3)] by blast
consider "(s, t) ∈ rstep 𝒰" | "(s, t) ∈ rstep ℛ" using assms(1) by fast
thus ?thesis
proof cases
case 𝒰_step : 1
hence "(s, NF_𝒰 t) ∈ (rstep 𝒰)⇧* ∧ NF_𝒰 t ∈ NF_trs 𝒰" using NFt_props by fastforce
hence "NF_𝒰 s = NF_𝒰 t" using NFs_props NF_𝒰_unique[of "NF_𝒰 s" "NF_𝒰 t" s] by blast
thus ?thesis by auto
next
case ℛ_step: 2
thus ?thesis using NF_𝒰_ℛ_step_persists[OF ℛ_step _ _ assms(2,4)] by blast
qed
qed
lemma rstep_r_p_s_Var_Some: "(s, t) ∈ rstep_r_p_s R (l, r) p σ ⟹
(mctxt_term_conv (mctxt_of_term s), mctxt_term_conv (mctxt_of_term t))
∈ rstep_r_p_s' R (l,r) p (σ ∘⇩s (Var ∘ Some))"
by (auto intro: rstep_r_p_s'_stable simp: rstep_r_p_s_eq_rstep_r_p_s')
lemma 𝔏⇩1_closed_under_PP⇩ℛ:
assumes "𝔏⇩1 (mctxt_of_term s)" "(s, t) ∈ PP⇩ℛ"
shows "𝔏⇩1 (mctxt_of_term t)"
proof -
let ?s = "mctxt_of_term (Fun Ap [Var undefined, s])"
let ?t = "mctxt_of_term (Fun Ap [Var undefined, t])"
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(2) by blast
have step: "(Fun Ap [Var undefined, s], Fun Ap [Var undefined, t])
∈ rstep_r_p_s (ℛ ∪ 𝒰) (l, r) (PCons 1 p) σ"
unfolding rstep_r_p_s_def
using Product_Type.Collect_case_prodD[OF st_step[unfolded rstep_r_p_s_def]]
by (auto simp: Let_def)
hence "(mctxt_term_conv ?s, mctxt_term_conv ?t)
∈ rstep_r_p_s' (ℛ ∪ 𝒰) (l, r) (PCons 1 p) (σ ∘⇩s (Var ∘ Some))"
using rstep_r_p_s_Var_Some by fast
hence "(?s, ?t) ∈ mrstep (ℛ ∪ 𝒰)"
using rstep'_iff_rstep_r_p_s' by fast
moreover have "?s ∈ 𝔏" using assms(1) 𝔏_def by auto
ultimately have "?t ∈ 𝔏"
using 𝔏_closed_under_ℛ[of ?s ?t] assms rstep'_iff_rstep_r_p_s' by fast
thus ?thesis using sub_layers by fastforce
qed
lemma uncurried_NF':
assumes "(s, t) ∈ PP⇩ℛ^^n" "s ∈ 𝒯" "𝔏⇩1 (mctxt_of_term s)"
shows "(NF_𝒰 s, NF_𝒰 t) ∈ (rstep ℛ)⇧*"
using assms
proof (induction n arbitrary: s)
case (Suc n)
obtain t' where split: "(s, t') ∈ PP⇩ℛ" "(t', t) ∈ PP⇩ℛ^^n"
using relpow_Suc_D2[OF Suc(2)] by blast
hence in_𝔏⇩1: "𝔏⇩1 (mctxt_of_term t')" using 𝔏⇩1_closed_under_PP⇩ℛ[OF Suc(4)] by blast
have "t' ∈ 𝒯" using split(1) 𝒯_closed_under_PP⇩ℛ[OF Suc(3), of t'] by blast
thus ?case using Suc(1)[OF split(2) _ in_𝔏⇩1] uncurried_NF[OF split(1) Suc(3) _ Suc(4)]
by fastforce
qed simp
lemma no_rrstep:
assumes s_def: "s = Fun Ap [Var v, t1]" and
st_step: "(s, t) ∈ rstep_r_p_s (ℛ ∪ 𝒰) r ε σ"
shows False
proof (cases "r ∈ ℛ")
case in_ℛ: True
then obtain f ts where l_def: "fst r = Fun f ts"
using wfR fst_conv unfolding wf_trs_def by (metis old.prod.exhaust)
then obtain ts' where lσ_def:
"fst r ⋅ σ = Fun f ts'" "length ts' = length ts" by simp
hence "(f, length ts') ∈ funas_term (fst r)" using l_def by auto
thus ?thesis using in_ℛ st_step sigR fresh lσ_def
unfolding rstep_r_p_s_def s_def funas_trs_def funas_rule_def by fastforce
next
case in_𝒰: False
hence "r ∈ 𝒰" using st_step unfolding rstep_r_p_s_def by force
then obtain f ts t1 where l_def: "fst r = Fun Ap [Fun f ts, t1]"
using 𝒰_def by fastforce
then obtain ts' t1' where lσ_def:
"fst r ⋅ σ = Fun Ap [Fun f ts', t1']" "length ts' = length ts" by simp
thus ?thesis using st_step unfolding rstep_r_p_s_def s_def by force
qed
lemma step_below1:
assumes "(s, t) ∈ rstep_r_p_s R r (PCons 1 p') σ" "s = Fun Ap [x, s1]"
shows "(s |_ <1>, t |_ <1>) ∈ rstep_r_p_s R r p' σ ∧ t = Fun Ap [x, t |_ <1>]"
proof -
let ?C = "ctxt_of_pos_term p' s1"
obtain C where step: "C = ctxt_of_pos_term (PCons 1 p') s" "PCons 1 p' ∈ poss s"
"C⟨fst r ⋅ σ⟩ = s ∧ C⟨snd r ⋅ σ⟩ = t" "r ∈ R"
using Product_Type.Collect_case_prodD[OF assms(1)[unfolded rstep_r_p_s_def]]
unfolding rstep_r_p_s_def assms(2) by force
hence "?C = ctxt_of_pos_term p' (s |_ <1>) ∧ p' ∈ poss (s |_ <1>) ∧
?C⟨fst r ⋅ σ⟩ = (s |_ <1>) ∧ ?C⟨snd r ⋅ σ⟩ = (t |_ <1>)"
unfolding assms(2) by simp
moreover have "t = Fun Ap [x, t |_ <1>]" using step unfolding assms(2) by auto
ultimately show ?thesis using ‹r ∈ R› unfolding rstep_r_p_s_def by force
qed
lemma 𝒯⇩𝔏_𝒯: "𝒯⇩𝔏 ⊆ 𝒯"
using 𝒯_def 𝔏_sig funas_mctxt_mctxt_of_term unfolding 𝒞_def by blast
lemma CR_on_𝒯⇩𝔏⇩1_suffices:
assumes "CR_on PP⇩ℛ 𝒯⇩𝔏⇩1"
shows "CR_on PP⇩ℛ 𝒯⇩𝔏"
proof -
{
fix s
assume "s ∈ 𝒯⇩𝔏"
hence "s ∈ 𝒯" using 𝒯⇩𝔏_𝒯 by blast
hence "NF_𝒰 s ∈ 𝒯" using NF_𝒰_correct by blast
have in_𝔏: "(mctxt_of_term s) ∈ 𝔏" using ‹s ∈ 𝒯⇩𝔏› by simp
then consider (in_𝔏⇩1) "𝔏⇩1 (mctxt_of_term s)" | (in_𝔏⇩2) "𝔏⇩2 (mctxt_of_term s)"
using 𝔏_def by blast
hence "CR_on PP⇩ℛ {s}"
proof cases
case in_𝔏⇩1
thus ?thesis using assms unfolding CR_on_def by simp
next
case in_𝔏⇩2
{
fix s t assume in_𝔏⇩2: "𝔏⇩2 (mctxt_of_term s)" "(s, t) ∈ PP⇩ℛ"
then obtain r p σ where st_step: "(s, t) ∈ rstep_r_p_s (ℛ ∪ 𝒰) r p σ"
using rstep_iff_rstep_r_p_s[of s t "ℛ ∪ 𝒰"] by blast
have "p ∈ poss s" "r ∈ ℛ ∪ 𝒰"
using Product_Type.Collect_case_prodD[OF st_step[unfolded rstep_r_p_s_def]]
unfolding fst_conv by meson+
obtain x C where "mctxt_of_term s = MFun Ap [x, C]" "x = MHole ∨ (∃v. x = MVar v)"
using in_𝔏⇩2 unfolding 𝔏⇩2.simps by blast
then obtain v t1 where s_def: "s = Fun Ap [Var v, t1]"
using term_of_mctxt_mctxt_of_term_id[of s] by auto
hence "𝔏⇩1 (mctxt_of_term (s |_ <1>)) ∧ (s |_ <1>, t |_ <1>) ∈ PP⇩ℛ ∧
(∃v s1 t1. s = Fun Ap [Var v, s1] ∧ t = Fun Ap [Var v, t1])"
proof (cases p)
case Empty
thus ?thesis using s_def no_rrstep[OF _ st_step[unfolded Empty]] by blast
next
case (PCons i p')
consider "i = 0" | "i = 1" using s_def ‹p ∈ poss s› unfolding PCons by fastforce
thus ?thesis
proof cases
case 1
have "(fst r) ⋅ σ = Var v"
using s_def st_step unfolding rstep_r_p_s_def PCons 1 by force
thus ?thesis using check_lhs[OF ‹r ∈ ℛ ∪ 𝒰›, of σ] by simp
next
case 2
have "<1> ∈ poss s" using ‹p ∈ poss s› unfolding PCons 2 by simp
hence "𝔏⇩1 (mctxt_of_term (s |_ <1>))"
using in_𝔏⇩2 𝔏_def subm_at_layers[of "mctxt_of_term s" "<1>"]
unfolding all_poss_mctxt_mctxt_of_term subm_at_mctxt_of_term[OF ‹<1> ∈ poss s›]
by blast
thus ?thesis using st_step ‹<1> ∈ poss s›
step_below1[OF st_step[unfolded PCons 2] s_def]
unfolding PCons 2 s_def by (auto simp: rstep_r_p_s_imp_rstep)
qed
qed
} note step_below_1 = this
have join_closed_ctxt: "(s, t) ∈ (rstep R)⇧↓ ⟹ (C⟨s⟩, C⟨t⟩) ∈ (rstep R)⇧↓"
for s t :: "('f, 'v) term" and R C using rsteps_closed_ctxt by auto
{
fix t u assume peak: "(s, t) ∈ PP⇩ℛ⇧*"
hence "(s |_ <1>, t |_ <1>) ∈ PP⇩ℛ⇧* ∧ 𝔏⇩1 (mctxt_of_term (s |_ <1>)) ∧
(∃v s1 t1. s = Fun Ap [Var v, s1] ∧ t = Fun Ap [Var v, t1])"
using in_𝔏⇩2
proof (induction rule: converse_rtrancl_induct)
case base
obtain x C v where mctxt_t_def:
"mctxt_of_term t = MFun Ap [x, C]" "𝔏⇩1 C" "x = MHole ∨ x = MVar v"
using 𝔏⇩2.cases[OF base] by metis
hence "t = Fun Ap (map term_of_mctxt [x, C])"
by (metis (full_types) term_of_mctxt.simps(2) term_of_mctxt_mctxt_of_term_id)
thus ?case using mctxt_t_def by auto
next
case (step s s')
obtain v s1 s1' where sub_in_𝔏⇩1: "𝔏⇩1 (mctxt_of_term (s |_ <1>))" and
step_below1: "(s |_ <1>, s' |_ <1>) ∈ PP⇩ℛ" and
s_def: "s = Fun Ap [Var v, s1]" and
s'_def: "s' = Fun Ap [Var v, s1']"
using step_below_1[OF step(4,1)] by fast+
have "𝔏⇩1 (mctxt_of_term (s' |_ <1>))"
using 𝔏⇩1_closed_under_PP⇩ℛ[OF sub_in_𝔏⇩1 step_below1] by blast
hence s'_in_𝔏⇩2: "𝔏⇩2 (mctxt_of_term s')" unfolding s'_def by auto
show ?case using sub_in_𝔏⇩1 step(3)[OF s'_in_𝔏⇩2] step_below1 s_def s'_def by auto
qed
} note main = this
{ fix t u assume st: "(s, t) ∈ PP⇩ℛ⇧*" and su: "(s, u) ∈ PP⇩ℛ⇧*"
then obtain v s1 t1 u1 where sub_in_𝔏⇩1: "𝔏⇩1 (mctxt_of_term (s |_ <1>))" and
st1: "(s |_ <1>, t |_ <1>) ∈ PP⇩ℛ⇧*" and
su1: "(s |_ <1>, u |_ <1>) ∈ PP⇩ℛ⇧*" and
term_defs: "s = Fun Ap [Var v, s1] ∧ t = Fun Ap [Var v, t1] ∧ u = Fun Ap [Var v, u1]"
using main[OF st] main[OF su] by blast
hence join: "(t |_ <1>, u |_ <1>) ∈ PP⇩ℛ⇧↓" using assms by blast
have "(t, u) ∈ PP⇩ℛ⇧↓"
using term_defs join_closed_ctxt[OF join, of "More Ap [_] Hole []"] by simp
}
thus ?thesis unfolding CR_on_def by simp
qed
}
thus ?thesis unfolding CR_on_def by simp
qed
theorem CR_on_𝔏:
assumes "CR_on (rstep ℛ) 𝒯"
shows "CR_on PP⇩ℛ 𝒯⇩𝔏"
proof -
have "𝒯⇩𝔏⇩1 ⊆ 𝒯"
using 𝒯_def 𝔏_sig 𝔏_def funas_mctxt_mctxt_of_term unfolding 𝒞_def by blast
{
fix s
assume "s ∈ 𝒯⇩𝔏⇩1"
hence "s ∈ 𝒯" using ‹𝒯⇩𝔏⇩1 ⊆ 𝒯› by blast
hence "NF_𝒰 s ∈ 𝒯" using NF_𝒰_correct by blast
have in_𝔏⇩1: "𝔏⇩1 (mctxt_of_term s)" using ‹s ∈ 𝒯⇩𝔏⇩1› by simp
{
fix t u assume "(s, t) ∈ PP⇩ℛ⇧*" and "(s, u) ∈ PP⇩ℛ⇧*"
hence "t ∈ 𝒯" "u ∈ 𝒯" using 𝒯_closed_under_PP⇩ℛ ‹s ∈ 𝒯› by blast+
from ‹(s, t) ∈ PP⇩ℛ⇧*› obtain m where "(s, t) ∈ PP⇩ℛ^^m" ..
hence left: "(NF_𝒰 s, NF_𝒰 t) ∈ (rstep ℛ)⇧*"
using uncurried_NF'[OF _ ‹s ∈ 𝒯› in_𝔏⇩1] by blast
from ‹(s, u) ∈ PP⇩ℛ⇧*› obtain n where "(s, u) ∈ PP⇩ℛ^^n" ..
hence "(NF_𝒰 s, NF_𝒰 u) ∈ (rstep ℛ)⇧*"
using uncurried_NF'[OF _ ‹s ∈ 𝒯› in_𝔏⇩1] by simp
hence "(NF_𝒰 t, NF_𝒰 u) ∈ (rstep ℛ)⇧↓"
using left assms ‹NF_𝒰 s ∈ 𝒯› by blast
then obtain v where d_props:
"(NF_𝒰 t, v) ∈ (rstep ℛ)⇧*" "(NF_𝒰 u, v) ∈ (rstep ℛ)⇧*"
by blast
moreover have "(t, NF_𝒰 t) ∈ (rstep 𝒰)⇧*" "(u, NF_𝒰 u) ∈ (rstep 𝒰)⇧*"
using NF_𝒰_correct ‹t ∈ 𝒯› ‹u ∈ 𝒯› by blast+
ultimately have "(t, v) ∈ PP⇩ℛ⇧*" "(u, v) ∈ PP⇩ℛ⇧*"
using rtrancl_trans[of t "NF_𝒰 t" PP⇩ℛ v] rtrancl_trans[of u "NF_𝒰 u" PP⇩ℛ v]
rstep_union[of ℛ 𝒰] in_rtrancl_UnI[of _ "rstep ℛ" "rstep 𝒰"] by metis+
hence "(t, u) ∈ PP⇩ℛ⇧↓" by blast
}
hence "CR_on PP⇩ℛ {s}" using CR_on_def by fastforce
}
hence "CR_on PP⇩ℛ 𝒯⇩𝔏⇩1" unfolding CR_on_def by simp
thus ?thesis using CR_on_𝒯⇩𝔏⇩1_suffices by auto
qed
lemma CR_by_reduction:
assumes cr: "CR S" and
sigR': "⋀x y. x ∈ A ⟹ (x, y) ∈ R ⟹ y ∈ A" and
prop1: "⋀x y. (x, y) ∈ R ⟹ (f x, f y) ∈ S⇧↔⇧*" and
prop2: "⋀x y'. x ∈ A ⟹ (f x, y') ∈ S⇧* ⟹ (x, g y') ∈ R⇧*"
shows "CR_on R A"
proof -
{ fix a
assume "a ∈ A"
{ fix b c
assume peak: "(a, b) ∈ R⇧*" "(a, c) ∈ R⇧*"
hence "(b, c) ∈ R⇧↓"
proof (cases "a = b")
case False
hence "b ∈ A" using rtrancl_induct[OF peak(1), of "λx. x ∈ A"] ‹a ∈ A› sigR' by blast
thus ?thesis
proof (cases "a = c")
case True
thus ?thesis using peak by blast
next
case ac: False
hence "c ∈ A" using rtrancl_induct[OF peak(2), of "λx. x ∈ A"] ‹a ∈ A› sigR' by blast
have ab_conv: "(f a, f b) ∈ S⇧↔⇧*"
using prop1 rtrancl_induct[OF ‹(a, b) ∈ R⇧*›, of "λx. (f a, f x) ∈ S⇧↔⇧*"]
by simp (metis conversion_def rtrancl_trans)+
have "(f a, f c) ∈ S⇧↔⇧*"
using prop1 rtrancl_induct[OF ‹(a, c) ∈ R⇧*›, of "λx. (f a, f x) ∈ S⇧↔⇧*"]
by simp (metis conversion_def rtrancl_trans)+
hence "(f b, f c) ∈ S⇧↔⇧*" using conversion_trans[of S] ab_conv
unfolding conversion_inv[of _ "f b"] by force
then obtain d where join: "(f b, d) ∈ S⇧* ∧ (f c, d) ∈ S⇧*"
using assms(1) unfolding CR_iff_conversion_imp_join by blast
hence "(b, g d) ∈ R⇧* ∧ (c, g d) ∈ R⇧*"
using prop2[OF ‹b ∈ A›, of d] prop2[OF ‹c ∈ A›, of d] by argo
thus ?thesis by blast
qed
qed (auto simp: peak)
hence "(b, c) ∈ R⇧↓" by blast
}
hence "CR_on R {a}" using CR_on_def by fastforce
}
thus ?thesis unfolding CR_on_def by simp
qed
abbreviation 𝒯⇩C⇩u where "𝒯⇩C⇩u ≡ { t . funas_term t ⊆ ℱ⇩C⇩u }"
lemma f_prop: "(x, y) ∈ rstep (Cu⇩R ℛ) ⟹ (x, y) ∈ PP⇩ℛ⇧↔⇧*"
proof -
assume "(x, y) ∈ (rstep (Cu⇩R ℛ))"
then obtain l r p σ where step: "(x, y) ∈ rstep_r_p_s (Cu⇩R ℛ) (l, r) p σ"
using rstep_iff_rstep_r_p_s[of x y "Cu⇩R ℛ"] by blast
obtain C where "x = C⟨l ⋅ σ⟩" "y = C⟨r ⋅ σ⟩" "p = hole_pos C" "(l, r) ∈ Cu⇩R ℛ"
using hole_pos_ctxt_of_pos_term[of p x]
Product_Type.Collect_case_prodD[OF step[unfolded rstep_r_p_s_def]]
unfolding fst_conv snd_conv by metis
obtain l' r' where l_def: "l = Cu l'" and r_def: "r = Cu r'" and in_ℛ: "(l', r') ∈ ℛ"
using ‹(l, r) ∈ Cu⇩R ℛ› Cu⇩R_def by auto
have funas: "funas_term l' ⊆ ℱ" "funas_term r' ⊆ ℱ"
using in_ℛ sigR ℱ_def unfolding funas_trs_def funas_rule_def by force+
have "l ∈ 𝒯" "r ∈ 𝒯" using ‹(l, r) ∈ Cu⇩R ℛ› funas_Cu⇩R
unfolding layer_system_sig.𝒯_def ℱ⇩U_def ℱ⇩C⇩u_def funas_trs_def funas_rule_def by force+
hence "(l, l') ∈ (rstep 𝒰)⇧*" "(r, r') ∈ (rstep 𝒰)⇧*"
using NF_𝒰_correct[OF NF_𝒰_Cu[OF funas(1)]] NF_𝒰_correct[OF NF_𝒰_Cu[OF funas(2)]]
unfolding l_def r_def by blast+
hence "(x, C⟨l' ⋅ σ⟩) ∈ rstep ((rstep 𝒰)⇧*) ∧ (y, C⟨r' ⋅ σ⟩) ∈ rstep ((rstep 𝒰)⇧*)"
unfolding ‹x = C⟨l ⋅ σ⟩› ‹y = C⟨r ⋅ σ⟩› by (metis (no_types) rstepI)
hence "(x, C⟨l' ⋅ σ⟩) ∈ PP⇩ℛ⇧↔⇧* ∧ (C⟨r' ⋅ σ⟩, y) ∈ PP⇩ℛ⇧↔⇧*"
by (simp add: in_rtrancl_UnI rstep_union conversionI' conversion_inv)
moreover have "(C⟨l' ⋅ σ⟩, C⟨r' ⋅ σ⟩) ∈ PP⇩ℛ⇧↔⇧*" using in_ℛ by blast
ultimately show ?thesis using conversion_trans[of PP⇩ℛ] unfolding trans_def by meson
qed
lemma 𝒰_step_Cu_persists:
assumes "(t, t') ∈ rstep 𝒰"
shows "Cu t' = Cu t"
using assms
proof (induction t arbitrary: t')
case (Fun f ts)
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
then obtain C where C_props: "Fun f ts = C⟨l ⋅ σ⟩" "t' = C⟨r ⋅ σ⟩" "p = hole_pos C"
and p_in_poss: "p ∈ poss (Fun f ts)"
using hole_pos_ctxt_of_pos_term[of p]
Product_Type.Collect_case_prodD[OF step[unfolded rstep_r_p_s_def]]
unfolding fst_conv snd_conv by metis
thus ?case
proof (cases p)
case Empty
hence lhs_def: "Fun f ts = l ⋅ σ" and rhs_def: "t' = r ⋅ σ" and in_𝒰: "(l, r) ∈ 𝒰"
using Product_Type.Collect_case_prodD[OF step[unfolded rstep_r_p_s_def]] by auto
then obtain f' ts' t m i where rule_def:
"l = Fun Ap [Fun f' ts', t]" "r = Fun f' (ts' @ [t])"
"(f', m) ∈ ℱ" "length ts' = i" "i < m"
using assms 𝒰_def by force
moreover have "f' ≠ Ap" using ‹(f', m) ∈ ℱ› fresh unfolding ℱ_def by fastforce
ultimately show ?thesis unfolding lhs_def rhs_def by simp
next
case (PCons i p')
hence "i < length ts" using p_in_poss by simp
have inner: "(ts ! i, t' |_ <i>) ∈ rstep_r_p_s 𝒰 (l, r) p' σ"
using rstep_i_pos_imp_rstep_arg_i_pos[OF step[unfolded PCons]] .
obtain x where t'_def: "t' = Fun f ((take i ts) @ x # (drop (Suc i) ts))"
using C_props id_take_nth_drop[OF ‹i < length ts›] unfolding PCons by (cases C) auto
have x_def: "x = t' |_ <i>" using nth_append_take[of i ts x] ‹i < length ts›
unfolding t'_def subt_at.simps by simp
hence Cu_i: "Cu x = Cu (ts ! i)"
using Fun(1)[of "ts ! i"] ‹i < length ts› rstep_r_p_s_imp_rstep[OF inner] by force
show ?thesis
proof (cases "f = Ap")
case isAp: True
show ?thesis using Cu_i id_take_nth_drop[OF ‹i < length ts›]
unfolding PCons t'_def isAp by simp (metis (no_types) list.simps(9) map_append)
next
case notAp: False
obtain ss1 y ss2 where short: "take i ts = ss1" "ts ! i = y" "drop (Suc i) ts = ss2" and
ts_def: "ts = ss1 @ y # ss2"
using id_take_nth_drop[OF ‹i < length ts›] by blast
have Cu_xy: "Cu x = Cu y" using Cu_i unfolding ‹ts ! i = y› .
show ?thesis unfolding t'_def short using ts_def unfolding ts_def
proof (induction "length ss2" arbitrary: ss2)
case (Suc n)
then obtain ss2' a where ss2_def: "ss2 = ss2' @ [a]"
by (metis append_Nil2 append_eq_conv_conj id_take_nth_drop lessI)
have inner: "Cu (Fun f (ss1 @ x # ss2')) = Cu (Fun f (ss1 @ y # ss2'))"
using Suc unfolding ss2_def by simp
have Cu_unfold: "Cu (Fun f (ss1 @ t # ss2)) = Fun Ap [Cu (Fun f (ss1 @ t # ss2')), Cu a]" for t
unfolding ss2_def append_Cons[symmetric] append.assoc[symmetric] Cu_last2[OF notAp] by simp
thus ?case using inner by simp
qed (simp add: Cu_xy notAp)
qed
qed
qed (simp add: NF_Var[OF wfU])
lemma Cu_in_ctxt:
shows "∃C'. Cu C⟨l ⋅ σ⟩ = C'⟨Cu (l ⋅ σ)⟩ ∧ Cu C⟨r ⋅ σ⟩ = C'⟨Cu (r ⋅ σ)⟩"
proof (induction C)
case Hole
then show ?case by simp (metis ctxt.cop_nil)
next
case (More f ss1 D ss2)
then obtain D' where inner: "Cu D⟨l ⋅ σ⟩ = D'⟨Cu (l ⋅ σ)⟩ ∧ Cu D⟨r ⋅ σ⟩ = D'⟨Cu (r ⋅ σ)⟩" by blast
thus ?case
proof (cases "f = Ap")
case isAp: True
have "ss1 @ D⟨t ⋅ σ⟩ # ss2 ≠ []" for t
by blast
hence Cu_unfold: "Cu (More f ss1 D ss2)⟨t ⋅ σ⟩ =
Fun Ap (map Cu (ss1 @ D⟨t ⋅ σ⟩ # ss2))" for t
unfolding isAp unfolding ctxt_apply_term.simps
by (metis Cu.simps(3) length_greater_0_conv nth_drop_0)
show ?thesis using inner unfolding Cu_unfold
by simp (meson ctxt_apply_term.simps(2))
next
case notAp: False
show ?thesis
proof (induction "length ss2" arbitrary: ss2)
case 0
let ?C = "More Ap [Cu (Fun f ss1)] D' []"
have "Cu (More f ss1 D ss2)⟨l ⋅ σ⟩ = ?C⟨Cu (l ⋅ σ)⟩ ∧
Cu (More f ss1 D ss2)⟨r ⋅ σ⟩ = ?C⟨Cu (r ⋅ σ)⟩"
using 0 notAp inner by simp
thus ?case by blast
next
case (Suc n)
then obtain ss2' a where ss2_def: "ss2 = ss2' @ [a]"
by (metis append_Nil2 append_eq_conv_conj id_take_nth_drop lessI)
let ?ts = "λt. ss1 @ D⟨t ⋅ σ⟩ # ss2'"
have Cu_unfold: "Cu (Fun f (ss1 @ D⟨t ⋅ σ⟩ # ss2)) = Fun Ap [Cu (Fun f (?ts t)), Cu a]" for t
unfolding ss2_def append_Cons[symmetric] append.assoc[symmetric] Cu_last2[OF notAp] by simp
obtain C' where C'_def: "Cu (More f ss1 D ss2')⟨l ⋅ σ⟩ = C'⟨Cu (l ⋅ σ)⟩ ∧
Cu (More f ss1 D ss2')⟨r ⋅ σ⟩ = C'⟨Cu (r ⋅ σ)⟩"
using Suc(1)[of ss2'] Suc(2) unfolding ss2_def by auto
let ?C = "More Ap [] C' [Cu a]"
have "Cu (More f ss1 D ss2)⟨l ⋅ σ⟩ = ?C⟨Cu (l ⋅ σ)⟩ ∧
Cu (More f ss1 D ss2)⟨r ⋅ σ⟩ = ?C⟨Cu (r ⋅ σ)⟩"
using C'_def unfolding ctxt_apply_term.simps Cu_unfold by simp
thus ?case by blast
qed
qed
qed
lemma Cu_in_subst:
assumes "funas_term t ⊆ ℱ"
shows "Cu (t ⋅ σ) = (Cu t) ⋅ (Cu ∘ σ)"
using assms
proof (induction t)
case (Fun f ts)
{ fix x
assume "x ∈ set ts"
hence "Cu (x ⋅ σ) = (Cu x) ⋅ (Cu ∘ σ)" using Fun by fastforce
} note inner = this
show ?case
proof (cases "f = Ap")
case isAp: True
thus ?thesis using Fun(2) fresh unfolding ℱ_def by fastforce
next
case notAp: False
show ?thesis using inner
proof (induction "length ts" arbitrary: ts)
case (Suc n)
then obtain ts' a where ts_def: "ts = ts' @ [a]"
by (metis append_Nil2 append_eq_conv_conj id_take_nth_drop lessI)
have subst_unfold: "Fun f ts ⋅ σ = Fun f (map (λx. x ⋅ σ) ts)" for ts by simp
have "Cu (Fun f ts) = Fun Ap [Cu (Fun f ts'), Cu a]"
using notAp unfolding ts_def by simp
moreover have "Cu (Fun f ts ⋅ σ) = Fun Ap [Cu (Fun f (map (λx. x ⋅ σ) ts')), Cu (a ⋅ σ)]"
using notAp unfolding ts_def subst_unfold by simp
moreover have "Cu (Fun f ts' ⋅ σ) = Cu (Fun f ts') ⋅ (Cu ∘ σ)" "Cu (a ⋅ σ) = Cu a ⋅ (Cu ∘ σ)"
using Suc(1)[of ts'] Suc(2,3) unfolding ts_def by force+
ultimately show ?case using notAp
unfolding ts_def by simp
qed simp
qed
qed simp
lemma g_prop1: "(x, y') ∈ PP⇩ℛ ⟹ (Cu x, Cu y') ∈ (rstep (Cu⇩R ℛ))⇧*"
proof -
assume "(x, y') ∈ PP⇩ℛ"
then consider (ℛ_step) "(x, y') ∈ rstep ℛ" | (𝒰_step) "(x, y') ∈ rstep 𝒰" by fast
thus ?thesis
proof cases
case ℛ_step
then obtain l r p σ where step: "(x, y') ∈ rstep_r_p_s ℛ (l, r) p σ"
using rstep_iff_rstep_r_p_s[of x y' ℛ] by blast
obtain C where x_def: "x = C⟨l ⋅ σ⟩" and y'_def: "y' = C⟨r ⋅ σ⟩" and in_ℛ: "(l, r) ∈ ℛ"
using hole_pos_ctxt_of_pos_term[of p x]
Product_Type.Collect_case_prodD[OF step[unfolded rstep_r_p_s_def]]
unfolding fst_conv snd_conv by metis
let ?σ = "Cu ∘ σ"
have funas: "funas_term l ⊆ ℱ" "funas_term r ⊆ ℱ" using in_ℛ sigR
unfolding funas_trs_def funas_rule_def ℱ_def by fastforce+
obtain C' where "Cu C⟨l ⋅ σ⟩ = C'⟨Cu (l ⋅ σ)⟩ ∧ Cu C⟨r ⋅ σ⟩ = C'⟨Cu (r ⋅ σ)⟩"
using Cu_in_ctxt by blast
hence "Cu C⟨l ⋅ σ⟩ = C'⟨(Cu l) ⋅ ?σ⟩" "Cu C⟨r ⋅ σ⟩ = C'⟨(Cu r) ⋅ ?σ⟩"
using Cu_in_subst[of _ σ] funas by force+
thus ?thesis using Cu⇩R_def in_ℛ unfolding x_def y'_def by auto
next
case 𝒰_step
show ?thesis using 𝒰_step_Cu_persists[OF 𝒰_step] by simp
qed
qed
lemma 𝒯⇩C⇩u_Cu_eq: "t ∈ 𝒯⇩C⇩u ⟹ Cu t = t"
proof (induction t)
case (Fun f ts) thus ?case
proof (cases "f = Ap")
case isAp: True
{ fix x
assume "x ∈ set ts"
hence "Cu x = x" using Fun ℱ⇩C⇩u_def by auto
}
moreover have "Cu (Fun Ap ts) = Fun Ap (map Cu ts)"
using Fun(2) Suc_length_conv[of 1 ts] fresh unfolding isAp ℱ⇩C⇩u_def by force
ultimately show ?thesis unfolding isAp by (simp add: map_idI)
qed (auto simp: ℱ⇩C⇩u_def)
qed simp
lemma 𝒯⇩C⇩u_Cu⇩R_persists: "⋀x y. x ∈ 𝒯⇩C⇩u ⟹ (x, y) ∈ rstep (Cu⇩R ℛ) ⟹ y ∈ 𝒯⇩C⇩u"
using rstep_preserves_funas_terms[OF funas_Cu⇩R _ _ wf_Cu] unfolding 𝒯_def by blast
lemma g_prop:
assumes "x ∈ 𝒯⇩C⇩u" "(x, y') ∈ PP⇩ℛ⇧*"
shows "(x, Cu y') ∈ (rstep (Cu⇩R ℛ))⇧*"
proof -
have "(Cu x, Cu y') ∈ (rstep (Cu⇩R ℛ))⇧*"
using g_prop1 assms(2) rtrancl_map[of PP⇩ℛ Cu "(rstep (Cu⇩R ℛ))⇧*" x y']
unfolding rtrancl_idemp by blast
thus ?thesis using 𝒯⇩C⇩u_Cu_eq[OF assms(1)] by argo
qed
theorem main_result_complete:
assumes "CR (rstep ℛ)"
shows "CR (rstep (Cu⇩R ℛ))"
proof -
have wf_RU: "wf_trs (ℛ ∪ 𝒰)" using wfR wfU unfolding wf_trs_def by blast
have "CR_on (rstep ℛ) 𝒯" using assms unfolding CR_defs by simp
hence "CR_on PP⇩ℛ 𝒯⇩𝔏" using CR_on_𝔏 by simp
hence CR: "CR_on PP⇩ℛ 𝒯" by (rule CR)
hence "CR PP⇩ℛ" using CR_on_imp_CR[OF wf_RU ℛ_sig] unfolding 𝒯_def by blast
have "CR_on (rstep (Cu⇩R ℛ)) 𝒯⇩C⇩u"
using CR_by_reduction[OF ‹CR PP⇩ℛ›, of 𝒯⇩C⇩u "rstep (Cu⇩R ℛ)" id Cu] 𝒯⇩C⇩u_Cu⇩R_persists
f_prop g_prop unfolding id_apply by presburger
thus ?thesis using CR_on_imp_CR[OF wf_Cu funas_Cu⇩R] unfolding 𝒯_def by blast
qed
end
end