text ‹Shared analysis for main results›
theory LS_Common
imports LS_Basics "Decreasing-Diagrams-II.Decreasing_Diagrams_II"
begin
text ‹"We fix r and assume terms with rank at most r to be confluent."›
locale weakly_layered_induct = weakly_layered ℱ 𝔏 ℛ
for ℱ :: "('f × nat) set" and 𝔏 :: "('f, 'v :: infinite) mctxt set" and ℛ :: "('f, 'v) trs" +
fixes rk :: nat
assumes IH_rk: "CR_on (rstep' ℛ) {t ∈ 𝒯. rank t ≤ Suc rk}"
begin
text ‹@{cite ‹Definition 4.7› FMZvO15}, native and short terms›
definition native_terms :: "('f, 'v) term set" where
"native_terms = {t ∈ 𝒯. rank t ≤ Suc (Suc rk)}"
definition short_terms :: "('f, 'v) term set" where
"short_terms = {t ∈ 𝒯. rank t ≤ Suc rk}"
definition shorter_terms :: "('f, 'v) term set" where
"shorter_terms = {t ∈ 𝒯. rank t ≤ rk}"
lemma shorter_imp_short[simp]:
"t ∈ shorter_terms ⟹ t ∈ short_terms"
by (auto simp: short_terms_def shorter_terms_def)
lemma native_terms_closed [simp]:
"s ∈ native_terms ⟹ (s, t) ∈ rstep' ℛ ⟹ t ∈ native_terms"
unfolding native_terms_def using rank_preservation 𝒯_preservation le_trans by blast
lemma short_terms_closed [simp]:
"s ∈ short_terms ⟹ (s, t) ∈ rstep' ℛ ⟹ t ∈ short_terms"
unfolding short_terms_def using rank_preservation 𝒯_preservation le_trans by blast
lemma short_terms_closed':
assumes "s ∈ short_terms" "(s, t) ∈ (rstep' ℛ)⇧*" shows "t ∈ short_terms"
using assms(2,1) by (induct t rule: rtrancl_induct) simp_all
lemma shorter_terms_closed:
"s ∈ shorter_terms ⟹ (s, t) ∈ rstep' ℛ ⟹ t ∈ shorter_terms"
unfolding shorter_terms_def using rank_preservation 𝒯_preservation le_trans by blast
lemma shorter_terms_closed':
assumes "s ∈ shorter_terms" "(s, t) ∈ (rstep' ℛ)⇧*" shows "t ∈ shorter_terms"
using assms(2,1) by (induct t rule: rtrancl_induct) (simp_all add: shorter_terms_closed)
lemma shorter_terms_short:
"shorter_terms ⊆ short_terms"
by auto
lemma aliens_short_terms:
assumes "t ∈ native_terms"
shows "set (aliens t) ⊆ short_terms"
proof -
note * = assms[unfolded native_terms_def arg_cong[OF rank.simps, of "op ≤"]]
{ fix t' assume t': "t' ∈ set (aliens t)"
have "t' ∈ 𝒯" using * supt_imp_funas_term_subset[OF unfill_holes_max_top_subt[of t t']] t'
by (auto simp: 𝒯_def)
moreover have "rank t' ≤ Suc rk" using t' *
by auto (metis (no_types, lifting) dual_order.trans imageI max_list set_map)
moreover note calculation
}
then show ?thesis by (auto simp: short_terms_def)
qed
inductive_set mirror_step :: "(('f, 'v) term × ('f, 'v) mctxt) rel" where
[intro]: "(s, t) ∈ rstep_r_p_s' ℛ (l, r) p σ ⟹
(mctxt_term_conv L, mctxt_term_conv M) ∈ rstep_r_p_s' ℛ (l, r) p τ ⟹ ((s, L), (t, M)) ∈ mirror_step"
declare mirror_step.cases[elim]
lemma mirror_step_to_max_top:
assumes "s ∈ 𝒯" "L ∈ tops s" "((s, L), (t, M)) ∈ mirror_step"
obtains M' where "M' ∈ 𝔏" "((s, max_top s), (t, M')) ∈ mirror_step"
proof -
obtain l r p σ τ where *: "(s, t) ∈ rstep_r_p_s' ℛ (l, r) p σ"
"(mctxt_term_conv L, mctxt_term_conv M) ∈ rstep_r_p_s' ℛ (l, r) p τ"
using mirror_step.cases[OF assms(3)] by metis
have "t ∈ 𝒯" using 𝒯_preservation[OF assms(1)] *(1) rstep'_iff_rstep_r_p_s' by metis
from *(2) obtain C where "(l, r) ∈ ℛ" "p = hole_pos C" "mctxt_term_conv L = C⟨l ⋅ τ⟩" by auto
then have "p ∈ funposs_mctxt L" using hole_pos_in_filled_funposs[of "l ⋅ τ" C Var] trs
by (force simp: wf_trs_def' funposs_mctxt_def)
then have "p ∈ funposs_mctxt (max_top s)" using max_topC_props(2)[OF assms(2)] funposs_mctxt_mono by metis
from W[OF `s ∈ 𝒯` `t ∈ 𝒯` this *(1)] obtain M' τ' where
**: "M' ∈ 𝔏" "(mctxt_term_conv (max_top s), mctxt_term_conv M') ∈ rstep_r_p_s' ℛ (l, r) p τ'"
by metis
moreover have "((s, max_top s), (t, M')) ∈ mirror_step" using *(1) **(2) by auto
ultimately show ?thesis using **(1) by (intro that)
qed
lemma mirrored_steps_preserve_prefix:
fixes C :: "('f, 'v) mctxt"
assumes "C ≤ C'"
"(mctxt_term_conv C, mctxt_term_conv D) ∈ rstep_r_p_s' ℛ (l, r) p τ"
"(mctxt_term_conv C', mctxt_term_conv D') ∈ rstep_r_p_s' ℛ (l, r) p τ'"
shows "D ≤ D'"
proof -
note 1 = assms(3,2)
have 2: "num_holes C = length (unfill_holes_mctxt C C')" "l ⋅ τ' = mctxt_term_conv (fill_holes_mctxt C (unfill_holes_mctxt C C')) |_ p"
using assms(1,3) by (auto simp: fill_unfill_holes_mctxt)
from rewrite_aliens_mctxt[OF trs 1(2) this] obtain Ds where
3: "num_holes D = length Ds" "(mctxt_term_conv (fill_holes_mctxt C (unfill_holes_mctxt C C')), mctxt_term_conv (fill_holes_mctxt D Ds)) ∈ rstep_r_p_s' ℛ (l, r) p τ'"
by metis
with fill_holes_mctxt_suffix[OF this(1)[symmetric]] this(2) have [simp]: "D' = fill_holes_mctxt D Ds"
using 2(1) rstep_r_p_s'_deterministic[OF trs 1(1)] assms(1)
by (simp add: fill_unfill_holes_mctxt) (metis term_mctxt_conv_inv)
show ?thesis using 3(1) 1(2) assms(1)
by (simp add: mrstep.simps rstep'_iff_rstep_r_p_s')
qed
lemma mirror_step_preserves_prefix:
assumes "C ≤ mctxt_of_term s" "((s, C), (t, D)) ∈ mirror_step"
shows "D ≤ mctxt_of_term t"
proof -
from assms(2) obtain l r p σ τ where
1: "(s, t) ∈ rstep_r_p_s' ℛ (l, r) p σ" "(mctxt_term_conv C, mctxt_term_conv D) ∈ rstep_r_p_s' ℛ (l, r) p τ" by auto
have "(mctxt_term_conv (mctxt_of_term s),mctxt_term_conv (mctxt_of_term t)) ∈ rstep_r_p_s' ℛ (l, r) p (σ ∘⇩s (Var ∘ Some))"
using rstep_r_p_s'_stable[OF 1(1), of "Var ∘ Some"] by auto
from mirrored_steps_preserve_prefix[OF assms(1) 1(2) this] show ?thesis .
qed
lemma mirror_steps_preserve_prefix:
assumes "C ≤ mctxt_of_term s" "((s, C), (t, D)) ∈ mirror_step⇧*"
shows "D ≤ mctxt_of_term t"
using assms(2,1)
proof (induct "(t, D)" arbitrary: t D rule: rtrancl_induct)
case (step tD)
then show ?case using mirror_step_preserves_prefix[of "snd tD" "fst tD" t D] by auto
qed auto
lemma mirror_step_aliens_mono:
assumes "length ss = num_holes L" "length ts = num_holes M"
"((fill_holes L ss, L), (fill_holes M ts, M)) ∈ mirror_step"
shows "set ts ⊆ set ss"
proof -
from assms(3) obtain l r p σ τ where
1: "(fill_holes L ss, fill_holes M ts) ∈ rstep_r_p_s' ℛ (l, r) p σ"
"(mctxt_term_conv L, mctxt_term_conv M) ∈ rstep_r_p_s' ℛ (l, r) p τ" by auto
obtain ts' where ts': "num_holes M = length ts'" "set ts' ⊆ set ss"
"(fill_holes L ss, fill_holes M ts') ∈ rstep_r_p_s' ℛ (l, r) p σ"
using 1(1) assms(1) rewrite_aliens[OF trs 1(2), of ss σ thesis] by auto
have "fill_holes M ts = fill_holes M ts'" by (metis 1(1) ts'(3) trs rstep_r_p_s'_deterministic)
from arg_cong[OF this, of "unfill_holes M"] show ?thesis
using ts'(1,2) assms(2) by (auto simp: unfill_fill_holes)
qed
lemma mirror_step_stable:
assumes "length ss = num_holes L" "length ts = num_holes M"
"((fill_holes L ss, L), (fill_holes M ts, M)) ∈ mirror_step"
shows "((fill_holes L (map f ss), L), (fill_holes M (map f ts), M)) ∈ mirror_step"
by (metis assms(3) rewrite_balanced_aliens'[OF trs assms(1,2)] mirror_step.simps)
lemma mirror_step_imp_rstep:
"(sL, tM) ∈ mirror_step ⟹ (fst sL , fst tM) ∈ rstep' ℛ"
by (cases sL; cases tM) (auto 0 5 simp: rstep'_iff_rstep_r_p_s')
lemma mirror_step_imp_rstep':
"(sL, tM) ∈ mirror_step ⟹ (mctxt_term_conv (snd sL) , mctxt_term_conv (snd tM)) ∈ rstep' ℛ"
by (cases sL; cases tM) (auto 0 5 simp: rstep'_iff_rstep_r_p_s')
lemma mirror_steps_imp_rsteps:
"((s, L), (t, M)) ∈ mirror_step⇧* ⟹ (s, t) ∈ (rstep' ℛ)⇧*"
by (induct "(s, L)" "(t, M)" arbitrary: t M rule: rtrancl.induct)
(force dest!: mirror_step_imp_rstep intro: rtrancl_into_rtrancl)+
lemma mirror_steps_imp_rsteps':
"((s, L), (t, M)) ∈ mirror_step⇧* ⟹ (mctxt_term_conv L, mctxt_term_conv M) ∈ (rstep' ℛ)⇧*"
by (induct "(s, L)" "(t, M)" arbitrary: t M rule: rtrancl.induct)
(force dest!: mirror_step_imp_rstep' intro: rtrancl_into_rtrancl)+
text ‹@{cite ‹Definition 4.8› FMZvO15}, decomposition into base context and base vector›
definition base_decomp :: "('f, 'v) term ⇒ ('f, 'v) mctxt × ('f, 'v) term list" where
"base_decomp t = (let M = max_top t in let as = unfill_holes M t in
(fill_holes_mctxt M (map (λt. if rank t ≤ rk then mctxt_of_term t else MHole) as),
filter (λt. ¬ rank t ≤ rk) as))"
text ‹@{cite ‹Definition 4.10› FMZvO15}, short step›
inductive_set short_step :: "('f, 'v) term rel" where
"s ∈ native_terms ⟹
(B, ss) = base_decomp s ⟹
((s, B), (t, C)) ∈ mirror_step⇧* ⟹ (s, t) ∈ short_step"
lemmas short_stepI = short_step.intros[unfolded rtranclp_rtrancl_eq case_prod_unfold prod.collapse Collect_mem_eq]
lemmas short_stepE = short_step.cases[unfolded rtranclp_rtrancl_eq case_prod_unfold prod.collapse Collect_mem_eq]
inductive_set short_step_s :: "('f, 'v) term ⇒ ('f, 'v) term rel" for s0 where
"(s0, s) ∈ (rstep ℛ)⇧* ⟹
s ∈ native_terms ⟹
(B, ss) = base_decomp s ⟹
((s, B), (t, C)) ∈ mirror_step⇧* ⟹ (s, t) ∈ short_step_s s0"
lemmas short_step_sI = short_step_s.intros[unfolded rtranclp_rtrancl_eq case_prod_unfold prod.collapse Collect_mem_eq]
lemmas short_step_sE = short_step_s.cases[unfolded rtranclp_rtrancl_eq case_prod_unfold prod.collapse Collect_mem_eq]
lemma short_step_s_imp_short_step:
"(s, t) ∈ short_step_s s0 ⟹ (s, t) ∈ short_step"
by (auto intro: short_stepI elim: short_step_sE)
lemma short_step_implies_short_step_s:
assumes "(s, t) ∈ short_step"
obtains s0 where "(s, t) ∈ short_step_s s0"
using short_stepE[OF assms] short_step_sI rtrancl_refl by metis
lemma short_step_iff_short_step_s:
"(s, t) ∈ short_step ⟷ (∃s0. (s, t) ∈ short_step_s s0)"
by (auto intro: short_step_s_imp_short_step elim: short_step_implies_short_step_s)
text ‹@{cite ‹Definition 4.11› FMZvO15}, tall step›
inductive_set tall_step :: "('f, 'v) term rel" where
"s ∈ native_terms ⟹
(B, ss) = base_decomp s ⟹
length ts = num_holes B ⟹ t = fill_holes B ts ⟹
(⋀i. i < num_holes B ⟹ (ss ! i, ts ! i) ∈ (rstep' ℛ)⇧*) ⟹
(s, t) ∈ tall_step"
inductive_set tall_step_i :: "nat ⇒ ('f, 'v) term rel" for ι where
"(B, ss) = base_decomp s ⟹
s ∈ native_terms ⟹
length ts = num_holes B ⟹ t = fill_holes B ts ⟹
(⋀i. i < num_holes B ⟹ (ss ! i, ts ! i) ∈ (rstep' ℛ)⇧*) ⟹
ι = imbalance ts ⟹
(s, t) ∈ tall_step_i ι"
lemma tall_step_i_imp_tall_step:
"(s, t) ∈ tall_step_i ι ⟹ (s, t) ∈ tall_step"
by (auto intro: tall_step.intros elim: tall_step_i.cases)
lemma tall_step_implies_tall_step_i:
assumes "(s, t) ∈ tall_step"
obtains ι where "(s, t) ∈ tall_step_i ι"
using tall_step.cases[OF assms] tall_step_i.intros by metis
lemma tall_step_iff_tall_step_i:
"(s, t) ∈ tall_step ⟷ (∃ι. (s, t) ∈ tall_step_i ι)"
by (auto intro: tall_step_i_imp_tall_step elim: tall_step_implies_tall_step_i)
lemma short_terms_rsteps:
assumes "s ∈ short_terms" "(s, t) ∈ (rstep' ℛ)⇧*"
shows "t ∈ short_terms ∧ (s, t) ∈ (Restr (rstep' ℛ) short_terms)⇧*"
using rtrancl_on_iff_rtrancl_restr[OF _ assms(2,1)] short_terms_closed by metis
lemma native_terms_rsteps:
assumes "s ∈ native_terms" "(s, t) ∈ (rstep' ℛ)⇧*"
shows "t ∈ native_terms ∧ (s, t) ∈ (Restr (rstep' ℛ) native_terms)⇧*"
using rtrancl_on_iff_rtrancl_restr[OF _ assms(2,1)] native_terms_closed by metis
lemma short_sequence_rsteps:
assumes "length ts = length ss" "set ss ⊆ short_terms"
"⋀i. i < length ss ⟹ (ss ! i, ts ! i) ∈ (rstep' ℛ)⇧*"
shows "set ts ⊆ short_terms"
"⋀i. i < length ss ⟹ (ss ! i, ts ! i) ∈ (Restr (rstep' ℛ) short_terms)⇧*"
using assms short_terms_rsteps[OF subsetD, OF _ nth_mem] by (auto simp: in_set_conv_nth)
lemma IH_rk':
"CR (Restr (rstep' ℛ) short_terms)"
using IH_rk short_terms_rsteps[OF _ r_into_rtrancl]
by (subst CR_on_iff_CR_Restr[symmetric]) (auto simp: short_terms_def[symmetric])
text ‹@{cite ‹Lemma 4.15› FMZvO15}›
lemma balance_short_sequences:
assumes "length ts = length ss" "length us = length ss"
"set ss ⊆ short_terms"
"⋀i. i < length ss ⟹ (ss ! i, ts ! i) ∈ (rstep' ℛ)⇧*"
"⋀i. i < length ss ⟹ (ss ! i, us ! i) ∈ (rstep' ℛ)⇧*"
obtains (vs) vs where
"length vs = length ss"
"⋀i. i < length ss ⟹ (ts ! i, vs ! i) ∈ (rstep' ℛ)⇧*"
"⋀i. i < length ss ⟹ (us ! i, vs ! i) ∈ (rstep' ℛ)⇧*"
"ts ∝ vs" "us ∝ vs"
"set ts ⊆ short_terms" "set us ⊆ short_terms" "set vs ⊆ short_terms"
proof -
let ?R' = "Restr (rstep' ℛ) short_terms"
note * = rtrancl_mono[of ?R' "rstep' ℛ", OF Int_lower1, THEN subsetD]
from assms have "⋀i. i < length ss ⟹ (ss ! i, ts ! i) ∈ ?R'⇧*"
"⋀i. i < length ss ⟹ (ss ! i, us ! i) ∈ ?R'⇧*"
and s: "set ts ⊆ short_terms" "set us ⊆ short_terms"
using short_sequence_rsteps by meson+
from balance_sequences[OF IH_rk' assms(1,2) this(1,2)]
obtain vs where "length vs = length ss"
"⋀i. i < length ss ⟹ (ts ! i, vs ! i) ∈ (rstep' ℛ)⇧*"
"⋀i. i < length ss ⟹ (us ! i, vs ! i) ∈ (rstep' ℛ)⇧*"
"ts ∝ vs" "us ∝ vs"
by (metis *)
moreover from this have
"set vs ⊆ short_terms" using short_sequence_rsteps[of vs ts] assms(1) s by simp
ultimately show ?thesis using s by (intro vs)
qed
text ‹@{cite ‹Definition 4.17› FMZvO15}, shallow context›
inductive_set shallow_context :: "('f, 'v) mctxt set" where
"L ∈ 𝔏 ⟹ length Cs = num_holes L ⟹ set Cs ⊆ {MHole} ∪ mctxt_of_term ` shorter_terms
⟹ C = fill_holes_mctxt L Cs ⟹ C ∈ shallow_context"
lemma funas_shallow_context:
"C ∈ shallow_context ⟹ funas_mctxt C ⊆ ℱ"
using 𝔏_sig by (force elim!: shallow_context.cases simp: 𝒞_def 𝒯_def shorter_terms_def)
lemma base_decomp_shallow':
assumes "t ∈ 𝒯" "(B, ts) = base_decomp t"
obtains Ds where "length Ds = num_holes (max_top t)"
and "set Ds ⊆ {MHole} ∪ mctxt_of_term ` shorter_terms"
and "B = fill_holes_mctxt (max_top t) Ds"
proof -
let ?ts = "map (λt. if rank t ≤ rk then mctxt_of_term t else MHole) (aliens t)"
have "length ?ts = num_holes (max_top t)"
using assms by (auto intro!: length_unfill_holes simp: max_topC_prefix)
moreover have "set ?ts ⊆ {MHole} ∪ mctxt_of_term ` shorter_terms"
using assms subset_trans[OF supteq_imp_funas_term_subset[OF unfill_holes_subt[OF max_topC_prefix]], of _ t ℱ]
by (force simp: base_decomp_def Let_def image_def 𝒯_def shorter_terms_def)
moreover have "B = fill_holes_mctxt (max_top t) ?ts"
using assms by (auto simp: base_decomp_def Let_def)
ultimately show ?thesis ..
qed
lemma base_decomp_shallow:
assumes "t ∈ 𝒯" "(B, ts) = base_decomp t"
shows "B ∈ shallow_context"
by (metis assms shallow_context.intros base_decomp_shallow' max_top_layer)
lemma base_decomp_aliens:
assumes "t ∈ 𝒯" "(B, ts) = base_decomp t"
shows "set ts ⊆ set (aliens t)"
using assms by (auto simp: base_decomp_def Let_def)
lemma base_decomp_fill_holes:
assumes "(B, ts) = base_decomp t"
shows "length ts = num_holes B" "fill_holes B ts = t"
proof -
let ?M = "max_top t"
define as where [simp]: "as = unfill_holes ?M t"
let ?as' = "map (λt. if rank t ≤ rk then mctxt_of_term t else MHole) as"
have B[simp]: "B = fill_holes_mctxt ?M ?as'" and ts[simp]: "ts = filter (λt. ¬ rank t ≤ rk) as"
using assms by (auto simp: base_decomp_def Let_def)
show *: "length ts = num_holes B"
using num_holes_fill_holes_mctxt[of ?M "?as'"]
by (auto simp: length_unfill_holes[OF max_topC_prefix] length_filter_sum_list comp_def intro: arg_cong[of _ _ sum_list])
have **: "partition_holes (filter (λt. ¬ rank t ≤ rk) as) ?as' = map (λt. if rank t ≤ rk then [] else [t]) as"
by (induct as) auto
have ***: "map (λi. fill_holes (map (λt. if rank t ≤ rk then mctxt_of_term t else MHole) as ! i)
(map (λt. if rank t ≤ rk then [] else [t]) as ! i)) [0..<length as] = as"
by (intro nth_equalityI) auto
show "fill_holes B ts = t"
unfolding B
apply (subst fill_holes_mctxt_fill_holes)
subgoal by (auto simp: length_unfill_holes[OF max_topC_prefix])
subgoal using * by auto
subgoal unfolding ts ** using ***
by (auto simp: length_unfill_holes[OF max_topC_prefix] fill_unfill_holes[OF max_topC_prefix])
done
qed
lemma base_decomp_prefix:
assumes "(B, ts) = base_decomp t"
shows "B ≤ mctxt_of_term t"
using base_decomp_fill_holes[OF assms] by auto
lemma fill_shallow_context_imp_native:
assumes "C ∈ shallow_context" "num_holes C = length ts" "set ts ⊆ short_terms"
shows "fill_holes C ts ∈ native_terms"
proof -
have "fill_holes C ts ∈ 𝒯" using assms funas_mctxt_fill_holes[of C ts]
by (auto simp: 𝒯_def short_terms_def funas_shallow_context)
moreover obtain L Cs where *: "L ∈ 𝔏" "length Cs = num_holes L"
"set Cs ⊆ {MHole} ∪ mctxt_of_term ` shorter_terms" "C = fill_holes_mctxt L Cs"
using assms(1) by (elim shallow_context.cases) simp
{ fix i assume "i < num_holes L"
then have "fill_holes (Cs ! i) (partition_holes ts Cs ! i) ∈ short_terms"
using *(2) subsetD[OF *(3), OF nth_mem, of i] shorter_terms_short subsetD[OF assms(3), OF nth_mem]
*(4) num_holes_fill_holes_mctxt[OF *(2)[symmetric]]
sum_list_append[of "take i (map num_holes Cs)" "drop i (map num_holes Cs)", symmetric]
sum_list_take'[of 1 "drop i (map num_holes Cs)"] assms(2)
by (force simp: image_def partition_by_nth take1 hd_drop_conv_nth) }
then have "set (map (λi. fill_holes (Cs ! i) (partition_holes ts Cs ! i)) [0..<num_holes L])
⊆ short_terms" by auto
note subsetD[OF this, OF nth_mem]
moreover have "L ≤ max_top (fill_holes C ts)" using *(1,2,4) assms(2)
order.trans[OF fill_holes_mctxt_suffix[of Cs L] fill_holes_mctxt_suffix[of "map mctxt_of_term ts" "fill_holes_mctxt L Cs"]]
by (auto intro!: max_top_props(2) simp: topsC_def)
ultimately show ?thesis using assms(2) fill_holes_mctxt_fill_holes[of Cs L ts]
order.trans[OF rank_by_top[of "fill_holes C ts" L], of "rk+2"]
by (simp add: *(2,4) short_terms_def native_terms_def unfill_fill_holes max_list_bound_set)
qed
lemma max_topC_max_top_conv:
"max_top (mctxt_term_conv C ⋅ (Var ∘ from_option)) =
fill_holes_mctxt (map_vars_mctxt (from_option ∘ Some) (max_topC C)) (map (λD. if D = MHole then MVar (from_option None) else MHole) (aliensC C))"
(is "max_top ?t = fill_holes_mctxt ?C ?Cs")
proof -
let ?M = "fill_holes_mctxt ?C ?Cs"
have [simp]: "length (aliensC C) = num_holes (max_topC C)"
using max_topC_prefix[of C] by simp
have "set ?Cs ⊆ {MHole} ∪ range MVar" by auto
then have 1: "?M ∈ 𝔏" using vars_to_holes'_layer[of ?M] vars_to_holes'_layer[of "max_topC C"]
vars_to_holes'_fill_holes[of "?C" "?Cs"] by (auto)
moreover
have "?M ≤ mctxt_of_term (mctxt_term_conv (fill_holes_mctxt (max_topC C) (aliensC C)) ⋅ (Var ∘ from_option))"
apply (subst mctxt_term_conv_fill_holes_mctxt, simp)
apply (subst subst_apply_mctxt_fill_holes, simp)
apply (subst mctxt_of_term_fill_holes', simp add: subst_apply_mctxt_map_vars_mctxt_conv)
unfolding subst_apply_mctxt_map_vars_mctxt_conv map_vars_mctxt_map_vars_mctxt
by (intro less_eq_fill_holesI) simp_all
then have 2: "?M ≤ mctxt_of_term ?t" using max_topC_prefix[of C] by (auto simp: fill_unfill_holes_mctxt)
moreover {
fix D assume 3: "D ∈ 𝔏" "D ≤ mctxt_of_term ?t"
let ?E = "D ⊔ ?M" and ?C = "map_vars_mctxt (from_option ∘ Some) (max_topC C)"
have c: "(D, ?M) ∈ comp_mctxt" using 2 3 by (auto simp: prefix_mctxt_sup prefix_comp_mctxt)
have "vars_to_holes (mctxt_of_term ?t) ≤ C" by (induct C) (auto intro: less_eq_mctxtI1)
with vars_to_holes'_mono[OF 3(2)] have "vars_to_holes D ≤ C" by simp
then have "vars_to_holes D ≤ max_topC C" using 3(1) by (simp add: topsC_def vars_to_holes_layer)
moreover have "vars_to_holes ?M ≤ max_topC C" using vars_to_holes_prefix[of "max_topC C"]
by (subst vars_to_holes_fill_holes) auto
ultimately have l': "vars_to_holes ?E ≤ max_topC C" using c by (auto simp: prefix_mctxt_sup vars_to_holes_sup)
have "?C ≤ ?M" by (subst fill_holes_mctxt_suffix) auto
then have "?C ≤ ?E" using sup_mctxt_ge2[OF c] using order.trans by blast
from fill_unfill_holes_mctxt[OF this] length_unfill_holes_mctxt[OF this]
obtain Es where [simp]: "length Es = num_holes ?C" and *: "?E = fill_holes_mctxt ?C Es" by metis
have 4: "num_holes C = length Cs ⟹
vars_to_holes (fill_holes_mctxt (map_vars_mctxt f C) Cs) = vars_to_holes (fill_holes_mctxt C Cs)" for f C Cs
by (induct C Cs rule: fill_holes_induct) (auto simp: comp_def)
have 5: "num_holes C = length Cs ⟹ num_holes C = length Ds ⟹
vars_to_holes (fill_holes_mctxt C Cs) ≤ fill_holes_mctxt C Ds ⟷
fill_holes_mctxt C (map vars_to_holes Cs) ≤ fill_holes_mctxt C Ds" for C Cs Ds
by (induct C Cs Ds rule: fill_holes_induct2) (auto intro!: less_eq_mctxtI1 elim!: less_eq_mctxtE1)
have "num_holes C = length Cs ⟹ mctxt_of_term (mctxt_term_conv (fill_holes_mctxt C Cs) ⋅ (Var ∘ from_option)) =
fill_holes_mctxt (map_vars_mctxt (from_option ∘ Some) C)
(map (λD. mctxt_of_term (mctxt_term_conv D ⋅ (Var ∘ from_option))) Cs)"
for C Cs by (induct C Cs rule: fill_holes_induct) (auto simp: comp_def)
from this[of "max_topC C" "unfill_holes_mctxt (max_topC C) C"] 3(2) max_topC_prefix[of C]
have "D ≤ fill_holes_mctxt (map_vars_mctxt (from_option ∘ Some) (max_topC C)) (map (λD. mctxt_of_term (mctxt_term_conv D ⋅ (Var ∘ from_option))) (aliensC C))"
(is "_ ≤ ?U") by (simp add: fill_unfill_holes_mctxt)
moreover have "?M ≤ ?U" by (subst less_eq_fill_holesI) auto
ultimately have "?E ≤ ?U" by (auto intro: prefix_mctxt_sup)
then have "?E ≤ ?M" using l' unfolding *
apply (subst less_eq_fill_holesI, simp, simp)
apply (subst (asm) 4, simp)
apply (subst (asm) (5) fill_holes_mctxt_replicate_MHole[of "max_topC C", symmetric])
apply (subst (asm) 5, simp, simp)
apply (subst (asm) less_eq_fill_holes_iff, simp, simp)
apply (subst (asm) less_eq_fill_holes_iff, simp, simp)
subgoal premises p for i
using spec[OF p(1), of i] spec[OF p(2), of i] p(3) aliens_not_varC[of _ C]
apply (cases "Es ! i"; cases "aliensC C ! i")
apply (auto simp: set_conv_nth elim: less_eq_mctxtE1)
done
apply auto
done
then have "D ≤ ?M" using sup_mctxt_ge1[OF c] by simp
}
ultimately show ?thesis by (auto intro: max_topCI simp: topsC_def)
qed
lemma shallow_context_decomp:
assumes "C ∈ shallow_context"
obtains (1) L Cs where "L = max_topC C" "length Cs = num_holes L"
"set Cs ⊆ {MHole} ∪ mctxt_of_term ` shorter_terms - MVar ` UNIV" "fill_holes_mctxt L Cs = C"
proof -
from assms(1) obtain L' Cs' where *: "L' ∈ 𝔏" "length Cs' = num_holes L'"
"set Cs' ⊆ {MHole} ∪ mctxt_of_term ` shorter_terms" "C = fill_holes_mctxt L' Cs'"
by (metis (no_types, lifting) shallow_context.cases)
then have "C ∈ 𝒞" using 𝔏_sig unfolding shorter_terms_def 𝒞_def 𝒯_def by (auto simp: image_def subset_iff)
have T: "mctxt_term_conv C ⋅ (Var ∘ from_option) ∈ 𝒯"
using assms(1) by (auto simp: funas_term_subst funas_shallow_context 𝒯_def)
have aux: "C ≤ term_mctxt_conv t ⟹ unfill_holes (map_vars_mctxt (f ∘ Some) C) (t ⋅ (Var ∘ f)) =
map (λD. mctxt_term_conv D ⋅ (Var ∘ f)) (unfill_holes_mctxt C (term_mctxt_conv t))" for C t f
by (induct t arbitrary: C rule: term_mctxt_conv.induct; case_tac C)
(auto elim!: less_eq_mctxtE2 simp: map_concat intro!: arg_cong[of _ _ concat])
have [simp]: "rank (mctxt_term_conv (mctxt_of_term t) ⋅ (Var ∘ from_option)) = rank t" for t
by (simp add: rank_var_subst[unfolded comp_def] subst_subst_compose[symmetric] subst_compose_def del: subst_subst_compose)
have [intro]: "D ∈ set Cs' ⟹ D ≠ MHole ⟹ rank (mctxt_term_conv D ⋅ (Var ∘ from_option)) ≤ rk" for D
using *(3) by (auto dest!: subsetD simp del: subst_subst_compose simp: shorter_terms_def
subst_subst_compose[symmetric] subst_compose_def rank_var_subst[unfolded comp_def] rank_var)
have "map_vars_mctxt (from_option ∘ Some) L' ≤ mctxt_of_term (mctxt_term_conv C ⋅ (Var ∘ from_option))"
using fill_holes_mctxt_suffix[OF *(2)] unfolding *(4)[symmetric]
by (induct L' C rule: less_eq_mctxt_induct) (auto intro: less_eq_mctxtI1)
then have "map_vars_mctxt (from_option ∘ Some) L' ≤ max_top (mctxt_term_conv C ⋅ (Var ∘ from_option))"
by (auto simp: topsC_def *(1))
from rank_by_top'[OF T this] have "rank (mctxt_term_conv C ⋅ (Var ∘ from_option))
≤ 1 + max_list (map rank (filter is_Fun (map (λD. mctxt_term_conv D ⋅ (Var ∘ from_option)) Cs')))"
by (subst (asm) (2) *(4), subst (asm) aux)
(auto simp: fill_holes_mctxt_suffix[OF *(2)] comp_def unfill_fill_holes_mctxt[OF *(2)])
then have "rank (mctxt_term_conv C ⋅ (Var ∘ from_option)) ≤ 1 + rk"
using max_list_bound_set[of "map rank (filter is_Fun (map (λD. mctxt_term_conv D ⋅ (Var ∘ from_option)) Cs'))" rk]
by auto
from this[unfolded rank.simps[of "mctxt_term_conv C ⋅ (Var ∘ from_option)"]]
have rk: "D ∈ set (aliens (mctxt_term_conv C ⋅ (Var ∘ from_option))) ⟹ rank D ≤ rk" for D
using T by (auto simp: max_list_bound set_conv_nth)
note [simp] = length_unfill_holes_mctxt[OF max_topC_prefix]
note fill_holes_mctxt_suffix[OF *(2), folded *(4)]
then have "L' ≤ max_topC C" by (auto intro!: max_topC_props(2) simp: topsC_def *(1))
with max_topC_prefix[of C]
unfill_holes_mctxt_by_prefix'[of L' "unfill_holes_mctxt L' (max_topC C)" C] *(2)
have "aliensC C = concat (map (λ(x, y). unfill_holes_mctxt x y)
(zip (unfill_holes_mctxt L' (max_topC C)) Cs'))"
and "i < num_holes L' ⟹ unfill_holes_mctxt L' (max_topC C) ! i ≤ Cs' ! i" for i
using less_eq_fill_holes_iff[of "unfill_holes_mctxt L' (max_topC C)" L' Cs']
by (auto simp: fill_unfill_holes_mctxt *(4) unfill_fill_holes_mctxt[OF *(2)])
have "D ∈ set (aliensC C) ⟹ D = MHole ∨ mctxt_term_conv D ⋅ (Var ∘ from_option) ∈ set (aliens (mctxt_term_conv C ⋅ (Var ∘ from_option)))" for D
using max_top_prefix[of "mctxt_term_conv C ⋅ (Var ∘ from_option)"]
by (auto simp: max_topC_max_top_conv unfill_holes_by_prefix' zip_map1 zip_map2 zip_same_conv_map aux max_topC_prefix)
moreover {
fix D
define E where "E = max_topC C"
assume D: "mctxt_term_conv D ⋅ (Var ∘ from_option) ∈ set (aliens (mctxt_term_conv C ⋅ (Var ∘ from_option)))" "D ≠ MHole"
have "num_holes D = 0"
using *(2)[symmetric] *(3,4) `L' ≤ max_topC C` max_topC_prefix[of C] D
unfolding max_topC_max_top_conv E_def[symmetric]
proof (induct L' Cs' arbitrary: C E rule: fill_holes_induct)
case (MHole C')
obtain t where C': "C = mctxt_of_term t" using MHole by (auto elim: less_eq_mctxtE2)
show ?case using MHole(4) C' MHole(5,6)
proof (induct E C arbitrary: t rule: less_eq_mctxt_induct)
case (1 C) show ?case using 1(1,2)
proof (induct t arbitrary: C D)
case (Var x) then show ?case
using surj_imp_inj_inv[OF bij_is_surj, OF bij_from_option]
by (cases D) (auto simp: inj_on_def from_option_def)
next
case (Fun f ts) then show ?case
by (cases D) (auto simp: map_eq_conv' set_conv_nth, blast)
qed
next
case (2 x) then show ?case by (cases t) auto
next
case (3 Es Cs f)
obtain ts where t: "t = Fun f ts" "length Cs = length ts" using 3 by (cases t) auto
{ fix i assume "i < length ts"
then have "(partition_holes (map (λD. if D = MHole then MVar (from_option None) else MHole)
(concat (map (λi. unfill_holes_mctxt (Es ! i) (map mctxt_of_term ts ! i)) [0..<length ts]))) Es) ! i =
map (λD. if D = MHole then MVar (from_option None) else MHole)
(unfill_holes_mctxt (Es ! i) (map mctxt_of_term ts ! i))"
unfolding map_map_partition_by[symmetric] using 3(1,2,4) t
apply (subst (2) nth_map, simp)
apply (subst partition_holes_concat_id, simp, simp)
by simp
} note [simp] = this
show ?case using 3 t by (auto simp: comp_def)
qed
next
case (MFun f Ls xs)
from MFun(5) obtain Es where [simp]: "E = MFun f Es" "length Ls = length Es" and
*: "⋀i. i < length Es ⟹ Ls ! i ≤ Es ! i" by (auto elim: less_eq_mctxtE1)
from MFun(6) obtain Cs where [simp]: "C = MFun f Cs" "length Es = length Cs" and
**: "⋀i. i < length Cs ⟹ Es ! i ≤ Cs ! i" by (auto elim: less_eq_mctxtE1)
{ fix i assume "i < length Cs"
then have "partition_holes (map (λD. if D = MHole then MVar (from_option None) else MHole)
(concat (map (λi. unfill_holes_mctxt (Es ! i) (Cs ! i)) [0..<length Cs]))) Es ! i =
map (λD. if D = MHole then MVar (from_option None) else MHole)
(unfill_holes_mctxt (Es ! i) (Cs ! i))"
unfolding map_map_partition_by[symmetric]
by (subst partition_holes_concat_id) (auto simp: **)
} note [simp] = this
from MFun(7) obtain i where [simp]: "i < length Cs" and
***: "mctxt_term_conv D ⋅ (Var ∘ from_option) ∈ set (unfill_holes
(fill_holes_mctxt (map_vars_mctxt (from_option ∘ Some) (Es ! i))
(map (λD. if D = MHole then MVar (from_option None) else MHole)
(unfill_holes_mctxt (Es ! i) (Cs ! i))))
(mctxt_term_conv (Cs ! i) ⋅ (Var ∘ from_option)))"
by (auto simp: comp_def)
show ?case using MFun(1,3,4) nth_subset_concat[of i "partition_holes xs Ls"]
by (auto intro!: MFun(2)[of i, OF _ _ _ * ** ***]
simp: MFun(8) dest: arg_cong[of Cs _ "λCs. Cs ! i"])
qed auto
then obtain t where D': "D = mctxt_of_term t" by (metis mctxt_of_term_term_of_mctxt_id)
have [simp]: "t ∈ 𝒯" using `C ∈ 𝒞` D' imageI[OF D(1), of funas_term]
arg_cong[OF fill_unfill_holes[OF max_topC_prefix, of "mctxt_term_conv C ⋅ (Var ∘ from_option)"], of funas_term]
by (auto simp: 𝒯_def 𝒞_def funas_mctxt_fill_holes funas_term_subst length_unfill_holes[OF max_topC_prefix])
have "D ∈ mctxt_of_term ` shorter_terms" using rk[OF D(1)] D
by (auto intro!: exI[of _ "term_of_mctxt D"] simp del: subst_subst_compose
simp: shorter_terms_def subst_subst_compose[symmetric] subst_compose_def rank_var_subst[unfolded comp_def] D')
}
ultimately have "D ∈ set (aliensC C) ⟹ D ∈ {MHole} ∪ mctxt_of_term ` shorter_terms - range MVar" for D
by (auto simp: aliens_not_varC image_def)
then show ?thesis
by (auto intro!: 1[of "max_topC C" "aliensC C"] simp: fill_unfill_holes_mctxt[OF max_topC_prefix])
qed
text ‹@{cite ‹Lemma 4.18› FMZvO15}›
lemma shallow_context_closed:
assumes "C ∈ shallow_context" "(mctxt_term_conv C, mctxt_term_conv D) ∈ rstep' ℛ"
shows "D ∈ shallow_context"
proof -
from assms(2) obtain l r p σ where assms2:
"(mctxt_term_conv C, mctxt_term_conv D) ∈ rstep_r_p_s' ℛ (l, r) p σ" by (metis rstep'_iff_rstep_r_p_s')
from assms(1) obtain L Cs
where *: "L = max_topC C" "length Cs = num_holes L"
"set Cs ⊆ {MHole} ∪ mctxt_of_term ` shorter_terms - MVar ` UNIV" "fill_holes_mctxt L Cs = C"
using shallow_context_decomp by (metis (no_types, lifting))
then have **: "set Cs ∩ MVar ` UNIV = {}" by auto
show ?thesis using trs *(2)[symmetric] assms2[folded *(4)]
proof (cases rule: rewrite_cases_mctxt_wf)
case outer
let ?to_c = "map_vars_mctxt (from_option ∘ Some)"
let ?to_t = "λC. mctxt_term_conv C ⋅ (Var ∘ from_option)"
have "(?to_t C, ?to_t D) ∈ rstep_r_p_s' ℛ (l, r) p (σ ∘⇩s (Var ∘ from_option))"
using assms2 by (intro rstep_r_p_s'_stable)
moreover have "mctxt_term_conv C ⋅ (Var ∘ from_option) ∈ 𝒯"
using assms(1) by (elim shallow_context.cases, auto simp: shorter_terms_def 𝒯_def funas_term_subst subset_eq)
(insert 𝔏_sig, auto simp: 𝒞_def)
moreover
let ?C' = "?to_t C"
let ?L' = "fill_holes_mctxt (?to_c L) (map (λC. if C = MHole then MVar (from_option None) else MHole) Cs)"
let ?Cs' = "concat (map (λC. if C = MHole then [] else [?to_t C]) Cs)"
have "partition_by ?Cs' (map (λC. if C = MHole then 0 else 1) Cs) =
map (λC. if C = MHole then [] else [?to_t C]) Cs"
by (auto intro: partition_by_concat_id)
then have C': "fill_holes ?L' ?Cs' = ?C'" "num_holes ?L' = length ?Cs'"
using fill_holes_mctxt_fill_holes[of
"map (λC. if C = MHole then MVar (from_option None) else MHole) Cs" "?to_c L" ?Cs']
*(2) num_holes_fill_holes_mctxt[of "map_vars_mctxt (from_option ∘ Some) L"
"map (λC. if C = MHole then MVar (from_option None) else MHole) Cs"]
by (auto simp: *(4)[symmetric] comp_def length_concat if_distrib mctxt_term_conv_fill_holes_mctxt
subst_apply_mctxt_fill_holes subst_apply_mctxt_map_vars_mctxt_conv[unfolded comp_def]
cong: if_cong intro!: arg_cong[of _ _ "fill_holes _"] nth_equalityI)
{ have "vars_to_holes ?L' = vars_to_holes L" using *(2)[symmetric]
by (induct L Cs rule: fill_holes_induct) (auto intro!: nth_equalityI simp: comp_def)
from vars_to_holes_layer[of ?L', unfolded this]
have "?L' ∈ 𝔏" using *(1) by (simp add: vars_to_holes_layer)
moreover have "?L' ≤ mctxt_of_term ?C'" using fill_holes_suffix[OF C'(2)] C'(1) by simp
moreover {
fix L' assume "L' ∈ tops ?C'"
hence "L' ∈ 𝔏" "L' ≤ mctxt_of_term ?C'" by (auto simp: topsC_def)
from vars_to_holes'_mono[OF this(2)] have "vars_to_holes L' ≤ C"
proof (induct L' arbitrary: C)
case o: (MFun f Ls) thus ?case
proof (cases C)
case (MFun g Cs)
then show ?thesis using o(1)[of "Ls ! i" "Cs ! i" for i] o(2)
by (auto intro!: less_eq_mctxtI1(3)[of _ _ Cs] elim: less_eq_mctxtE1)
qed (auto elim: less_eq_mctxtE1)
qed auto
hence "vars_to_holes L' ≤ L"
using *(1) max_topC_props(2) vars_to_holes_layer topsC_def ‹L' ∈ 𝔏› by blast
with *(2)[symmetric] `L' ≤ mctxt_of_term ?C'` ** have "L' ≤ ?L'" unfolding *(4)[symmetric]
proof (induct L Cs arbitrary: L' rule: fill_holes_induct)
case (MHole C) thus ?case by (cases C; cases L') (auto elim: less_eq_mctxtE1)
next
case (MFun f Ls Cs)
have "i < length Ls ⟹ set (partition_holes Cs Ls ! i) ∩ MVar ` UNIV = {}" for i
using MFun(1,4) nth_subset_concat[of i "partition_holes Cs Ls"] by auto
with MFun show ?case
by (cases L') (auto elim!: less_eq_mctxtE1 intro: less_eq_mctxtI1(3) nth_equalityI simp: comp_def)
qed auto
}
ultimately have "max_top ?C' = ?L'" by (auto intro: max_topCI simp: topsC_def)
} note max_top_C' = this
have "p ∈ funposs_mctxt (max_top ?C')" using *(2)[symmetric] outer(1) unfolding max_top_C'
by (induct L Cs arbitrary: p rule: fill_holes_induct)
(auto simp: funposs_mctxt_def comp_def)
ultimately obtain M τ where M: "M ∈ 𝔏"
"(mctxt_term_conv (max_top ?C'), mctxt_term_conv M)
∈ rstep_r_p_s' ℛ (l, r) p τ"
by (auto dest: W')
have ***: "(mctxt_term_conv L, mctxt_term_conv (term_mctxt_conv (mctxt_term_conv M ⋅ (Var ∘ case_option None to_option))))
∈ rstep_r_p_s' ℛ (l, r) p (τ ∘⇩s (λx. case x of None ⇒ Var None | Some x ⇒ Var (to_option x)))"
(is "(_, mctxt_term_conv ?M') ∈ _ p ?τ'")
using M[unfolded max_top_C'] *(2) fill_holes_mctxt_replicate_MHole[of L]
mctxt_term_conv_fill_holes_mctxt[of L "map (λ_. MHole) Cs", symmetric]
apply (subst (asm) mctxt_term_conv_fill_holes_mctxt, simp add: C'[folded max_top_C'])
apply (drule rstep_r_p_s'_stable[where τ = "Var ∘ case_option None to_option"])
apply (simp add: subst_apply_mctxt_fill_holes subst_apply_mctxt_map_vars_mctxt_conv)
apply (simp add: comp_def if_distrib if_distrib[of "λx. x _"] option.case_distrib map_replicate_const cong: if_cong)
done
have "vars_to_holes ?M' = vars_to_holes M"
proof (induct M)
case (MVar x) thus ?case by (cases "to_option x") auto
qed auto
then have "?M' ∈ 𝔏" by (metis M(1) vars_to_holes_layer)
moreover
thm rstep_r_p_s'_stable[OF ***, where τ = "Var ∘ from_option"]
from rewrite_aliens_mctxt[OF trs *** *(2)[symmetric], of σ]
obtain Ds where
"num_holes (term_mctxt_conv (mctxt_term_conv M ⋅ (Var ∘ case_option None to_option))) = length Ds"
"(mctxt_term_conv (fill_holes_mctxt L Cs), mctxt_term_conv (fill_holes_mctxt (term_mctxt_conv (mctxt_term_conv M ⋅ (Var ∘ case_option None to_option))) Ds)) ∈ rstep_r_p_s' ℛ (l, r) p σ"
"set Ds ⊆ set Cs"
using assms2 by (auto simp: *(4) elim!: rstep_r_p_s'.cases) blast
ultimately show ?thesis using *(3)
arg_cong[OF rstep_r_p_s'_deterministic[OF trs assms2], where f = term_mctxt_conv]
by (auto intro!: shallow_context.intros[of "?M'" Ds] simp: *(4))
next
case (inner i Ci)
moreover have "L ∈ 𝔏" using * by auto
moreover
have **: "(term_of_mctxt (Cs ! i), term_of_mctxt Ci) ∈ rstep_r_p_s' ℛ (l, r) (pos_diff p (hole_poss' L ! i)) (σ ∘⇩s term_of_mctxt_subst)"
using inner(3) unfolding term_of_mctxt_to_mctxt_term_conv by (intro rstep_r_p_s'_stable)
have "Cs ! i ∈ {MHole} ∪ mctxt_of_term ` shorter_terms"
using *(3) nth_mem[OF inner(1)] by auto
then have ***: "term_of_mctxt (Cs ! i) ∈ shorter_terms" "mctxt_of_term (term_of_mctxt (Cs ! i)) = Cs ! i"
using inner(3) NF_Var'[OF trs, unfolded rstep'_iff_rstep_r_p_s'] by force+
{ have "term_of_mctxt Ci ∈ shorter_terms"
using ** ***(1) rank_preservation[of "term_of_mctxt (Cs ! i)" "term_of_mctxt Ci"]
𝒯_preservation[of "term_of_mctxt (Cs ! i)" "term_of_mctxt Ci"]
unfolding rstep'_iff_rstep_r_p_s' shorter_terms_def by force
moreover have "mctxt_term_conv (mctxt_of_term (term_of_mctxt Ci)) = mctxt_term_conv Ci"
using arg_cong[OF ***(2), of mctxt_term_conv] inner(3) trs
rstep_r_p_s'_stable[OF inner(3), of "term_of_mctxt_subst ∘⇩s (Var ∘ Some)"]
by (auto simp: term_of_mctxt_to_mctxt_term_conv intro: rstep_r_p_s'_deterministic)
note arg_cong[OF this, of term_mctxt_conv, unfolded term_mctxt_conv_inv]
ultimately have "Ci ∈ mctxt_of_term ` shorter_terms" by (auto simp: shorter_terms_def image_def)
}
then have "set (Cs[i := Ci]) ⊆ {MHole} ∪ mctxt_of_term ` shorter_terms"
using inner *(3) by (intro set_update_subsetI) auto
ultimately show ?thesis using * by (intro shallow_context.intros[of L "Cs[i := Ci]"]) auto
qed
qed
lemma shallow_context_closed':
assumes "C ∈ shallow_context" "(mctxt_term_conv C, mctxt_term_conv D) ∈ (rstep' ℛ)⇧*"
shows "D ∈ shallow_context"
using assms(2,1)
proof (induct "mctxt_term_conv D" arbitrary: D rule: rtrancl_induct)
case base show ?case by (metis base term_mctxt_conv_inv)
next
case (step c') show ?case by (metis step(2-4) shallow_context_closed mctxt_term_conv_inv)
qed
lemma set_aliensC_conv:
"set (aliensC L) ⊆ {MHole} ∪ (λt. term_mctxt_conv (t ⋅ (Var ∘ to_option))) ` set (aliens (mctxt_term_conv L ⋅ (Var ∘ from_option)))"
unfolding max_topC_max_top_conv using max_topC_prefix[of L]
proof (induct ("max_topC L") L rule: less_eq_mctxt_induct)
case (3 Cs Ds f) then show ?case
apply (auto 0 0 del: subsetI simp del: UN_simps(1) intro!: UN_mono
simp: image_UN UN_extend_simps(1) map_concat)
by (subst partition_by_concat_id) auto
qed (auto simp: subst_subst_compose[symmetric] subst_compose_def simp del: subst_subst_compose)
lemma map_vars_mctxt_id[simp]:
"map_vars_mctxt id = id"
proof
fix C show "map_vars_mctxt id C = id C" by (induct C) auto
qed
lemma shallow_context_subset_𝒞:
"shallow_context ⊆ 𝒞"
by (intro subsetI, elim shallow_context.cases)
(auto simp: 𝒞_def 𝒯_def shorter_terms_def dest!: subsetD[OF 𝔏_sig] simp: subsetD)
lemma factor_prefix_of_map_vars_mctxt:
assumes "C ≤ map_vars_mctxt f D"
obtains C' where "C = map_vars_mctxt f C'" "C' ≤ D"
using assms
proof (induct C "map_vars_mctxt f D" arbitrary: D thesis rule: less_eq_mctxt_induct)
case 1 show ?case by (auto intro: 1[of MHole])
next
case (3 Cs fDs g)
from 3(1,4) obtain Ds where [simp]: "length Cs = length Ds" "D = MFun g Ds" by (cases D) auto
have "⋀i. i < length Cs ⟹ fDs ! i = map_vars_mctxt f (Ds ! i)" using 3(4) by auto
from 3(3)[OF _ this] have "⋀i. i < length Cs ⟹ ∃C'. Cs ! i = map_vars_mctxt f C' ∧ C' ≤ Ds ! i" by metis
then obtain iCs where "⋀i. i < length Cs ⟹ Cs ! i = map_vars_mctxt f (iCs i) ∧ iCs i ≤ Ds ! i" by metis
then show ?case by (auto intro!: 3(5)[of "MFun g (map iCs [0..<length Cs])"] nth_equalityI intro!: less_eq_mctxtI1)
qed auto
lemma shallow_context_union:
assumes "C ∈ shallow_context" "D ∈ shallow_context" "(C, D) ∈ comp_mctxt"
shows "C ⊔ D ∈ shallow_context"
proof -
obtain L Cs M Ds where
C: "L ∈ 𝔏" "length Cs = num_holes L" "set Cs ⊆ {MHole} ∪ mctxt_of_term ` shorter_terms" "C = fill_holes_mctxt L Cs" and
D: "M ∈ 𝔏" "length Ds = num_holes M" "set Ds ⊆ {MHole} ∪ mctxt_of_term ` shorter_terms" "D = fill_holes_mctxt M Ds" and
*: "L ≤ C" "M ≤ D"
using assms(1,2) by (auto elim!: shallow_context.cases)
from C(1) D(1) * assms(3) have **: "(L, M) ∈ comp_mctxt" "L ⊔ M ≤ C ⊔ D" "L ⊔ M ∈ 𝔏"
by (meson order.trans dual_order.trans prefix_mctxt_sup prefix_comp_mctxt sup_mctxt_ge1 sup_mctxt_ge2 sup_mctxt_LL)+
obtain N Es where ***: "N ≤ L ⊔ M" "C ⊔ D = fill_holes_mctxt N Es" "num_holes N = length Es"
"set Es ⊆ {MHole} ∪ mctxt_of_term ` shorter_terms"
using **(1) C(2-) D(2-) assms(3)
proof (induct L M arbitrary: C D Cs Ds thesis rule: comp_mctxt.induct)
case (MHole1 M)
then consider (h) "Cs = [MHole]" | (t) t where "t ∈ shorter_terms" "Cs = [mctxt_of_term t]" by (cases Cs) auto
then show ?case
proof (cases)
case h then show ?thesis using MHole1(2-) by (intro MHole1(1)[of M Ds]) auto
next
case t then show ?thesis using MHole1(2-)
by (intro MHole1(1)[of "MHole" "Cs"]) (auto simp: mctxt_of_term_leq_imp_eq less_eq_mctxt_sup_conv2[symmetric])
qed
next
case (MHole2 L)
then consider (h) "Ds = [MHole]" | (t) t where "t ∈ shorter_terms" "Ds = [mctxt_of_term t]" by (cases Ds) auto
then show ?case
proof (cases)
case h then show ?thesis using MHole2(2-) by (intro MHole2(1)[of L Cs]) auto
next
case t then show ?thesis using MHole2(2-)
by (intro MHole2(1)[of "MHole" "Ds"]) (auto simp: mctxt_of_term_leq_imp_eq less_eq_mctxt_sup_conv1[symmetric])
qed
next
case (MVar x y)
show ?case using MVar(1,3,5,6,8) by (intro MVar(2)[of "MVar x" "[]"]) auto
next
case (MFun f g Ls Ms)
{ fix i x y assume "i < length Ms"
note * = MFun(3)[rule_format, OF this, THEN conjunct1]
MFun(3)[rule_format, OF this, THEN conjunct2, rule_format,
OF _ _ _ refl _ _ refl,
of "partition_holes Cs Ls ! i" "partition_holes Ds Ms ! i"]
have [dest!]: "x ∈ set (partition_holes Cs Ls ! i) ⟹ x ∈ set Cs" for x
using `i < length Ms` MFun(5)[unfolded num_holes.simps]
by (metis MFun.hyps(2) in_set_idx length_map length_partition_by_nth partition_by_nth_nth_elem)
have [dest!]: "x ∈ set (partition_holes Ds Ms ! i) ⟹ x ∈ set Ds" for x
using `i < length Ms` MFun(8)[unfolded num_holes.simps]
by (metis MFun.hyps(2) in_set_idx length_map length_partition_by_nth partition_by_nth_nth_elem)
have "∃Ni Esi. Ni ≤ Ls ! i ⊔ Ms ! i ∧
fill_holes_mctxt (Ls ! i) (partition_holes Cs Ls ! i) ⊔
fill_holes_mctxt (Ms ! i) (partition_holes Ds Ms ! i) = fill_holes_mctxt Ni Esi ∧
num_holes Ni = length Esi ∧
set Esi ⊆ {MHole} ∪ mctxt_of_term ` shorter_terms"
using `i < length Ms` MFun(1,2,5-11) by (subst *(2)) (auto dest!: comp_MFunD)
}
then obtain Nf Esf where
*: "i < length Ms ⟹ Nf i ≤ Ls ! i ⊔ Ms ! i ∧
fill_holes_mctxt (Ls ! i) (partition_holes Cs Ls ! i) ⊔
fill_holes_mctxt (Ms ! i) (partition_holes Ds Ms ! i) = fill_holes_mctxt (Nf i) (Esf i) ∧
num_holes (Nf i) = length (Esf i) ∧
set (Esf i) ⊆ {MHole} ∪ mctxt_of_term ` shorter_terms" for i by metis
let ?Ns = "map Nf [0..<length Ms]" and ?Ess = "map Esf [0..<length Ms]"
show ?case
using * MFun(1,2,5-) partition_by_concat_id[of ?Ess "map num_holes ?Ns"]
apply (intro MFun(4)[OF less_eq_mctxtI1(3), of f "map (λ(x,y). x ⊔ y) (zip Ls Ms)" ?Ns "concat ?Ess"])
apply (auto intro!: nth_equalityI[of "map _ _"] arg_cong[of _ _ sum_list]
arg_cong[of _ _ "fill_holes_mctxt (Nf _)"]
simp: length_concat in_set_conv_nth[of _ ?Ess])
apply blast
done
qed
have "mctxt_term_conv (C ⊔ D) ⋅ (Var ∘ from_option) ∈ 𝒯" using assms
by (auto simp: 𝒯_def funas_term_subst funas_mctxt_sup_mctxt 𝒞_def dest!: subsetD[OF shallow_context_subset_𝒞])
moreover {
have "N ≤ max_topC (C ⊔ D)"
by (metis (no_types, lifting) **(2,3) ***(1) dual_order.trans max_topC_props(2) mem_Collect_eq topsC_def)
note map_vars_mctxt_mono[OF this, of "from_option ∘ Some"]
moreover have "map_vars_mctxt (from_option ∘ Some) (max_topC (C ⊔ D)) ≤ mctxt_of_term (mctxt_term_conv (C ⊔ D) ⋅ (Var ∘ from_option))"
using map_vars_mctxt_mono[OF max_topC_prefix, of "from_option ∘ Some" "C ⊔ D"]
map_vars_mctxt_mono[OF map_vars_Some_le_mctxt_of_term_mctxt_term_conv, of from_option "C ⊔ D"]
by (simp add: mctxt_of_term_var_subst)
then have "map_vars_mctxt (from_option ∘ Some) (max_topC (C ⊔ D)) ∈ tops (mctxt_term_conv (C ⊔ D) ⋅ (Var ∘ from_option))"
by (simp add: topsC_def)
note max_topC_props(2)[OF this]
ultimately have "map_vars_mctxt (from_option ∘ Some) N ≤ max_top (mctxt_term_conv (C ⊔ D) ⋅ (Var ∘ from_option))"
by simp
} note N = this
moreover have "max_list (map rank (filter is_Fun (map (λE. mctxt_term_conv E ⋅ (λx. Var (from_option x))) Es))) ≤ rk"
using ***(1-3) subsetD[OF ***(4), simplified, dest!]
by (auto intro!: max_list_mono[of _ "[rk]", unfolded max_list.simps max_0R]
simp del: subst_subst_compose simp: subst_subst_compose[symmetric] subst_compose_def rank_var_subst[unfolded comp_def] rank_var shorter_terms_def)
ultimately have rk: "max_list (map rank (aliens (mctxt_term_conv (C ⊔ D) ⋅ (Var ∘ from_option)))) ≤ rk"
using rank_by_top'[of "mctxt_term_conv (C ⊔ D) ⋅ (Var ∘ from_option)" "map_vars_mctxt (from_option ∘ Some) N", unfolded rank.simps[of "_ ⋅ _"]]
*** unfill_holes_var_subst[of "map_vars_mctxt Some N" "mctxt_term_conv (C ⊔ D)" from_option]
order.trans[OF map_vars_mctxt_mono[of N "C ⊔ D" Some] map_vars_Some_le_mctxt_of_term_mctxt_term_conv[of "C ⊔ D"]]
by (auto simp: comp_def unfill_holes_map_vars_mctxt_Some_mctxt_term_conv_conv unfill_fill_holes_mctxt)
{ { fix f s t
assume "map_vars_term f s ⊵ t" "s ∈ 𝒯"
then consider s' where "s' ∈ 𝒯" "map_vars_term f s' = t" unfolding 𝒯_def
proof (induct "map_vars_term f s" t arbitrary: s thesis)
case (subt u ss t f) then show ?case by (cases s) (auto simp: UN_subset_iff, blast)
qed simp
} note [elim] = this
fix M s t f
assume x: "M ≤ mctxt_of_term (s ⋅ (Var ∘ f))" "t ∈ set (unfill_holes M (s ⋅ (Var ∘ f)))" "s ∈ 𝒯"
then have "∃s'. s' ∈ 𝒯 ∧ t = s' ⋅ (Var ∘ f)"
by (auto dest!: unfill_holes_subt simp: map_vars_term_eq[symmetric])
} note **** = this[unfolded comp_def]
{ fix s
define M where "M = max_top (mctxt_term_conv (fill_holes_mctxt N Es) ⋅ (Var ∘ from_option))"
from max_top_prefix[of "mctxt_term_conv (fill_holes_mctxt N Es) ⋅ (Var ∘ from_option)", folded M_def]
obtain M' where M': "M = map_vars_mctxt from_option M'" "M' ≤ mctxt_of_term (mctxt_term_conv (fill_holes_mctxt N Es))"
by (auto simp: mctxt_of_term_var_subst elim: factor_prefix_of_map_vars_mctxt)
assume s: "s ∈ set (aliens (mctxt_term_conv (C ⊔ D) ⋅ (Var ∘ from_option)))"
have "s = Var (from_option None) ∨ (∃s'. s' ∈ 𝒯 ∧ s = s' ⋅ (Var ∘ from_option ∘ Some))"
using ***(3) s map_vars_mctxt_mono[OF N, of to_option] M'(2)
unfolding ***(2) M_def[symmetric] M'(1)
apply (subst (asm) unfill_holes_var_subst, simp add: M'(2))
unfolding map_vars_mctxt_map_vars_mctxt comp_def to_from_option map_vars_mctxt_id Multihole_Context.map_vars_mctxt_id
apply (subst (asm) (2) mctxt_term_conv_fill_holes_mctxt; (simp; fail)?)
apply (subst (asm) (1) mctxt_of_term_fill_holes'; (simp; fail)?)
apply (subst (asm) (1 3) fill_unfill_holes_mctxt[of "map_vars_mctxt Some N" M', symmetric]; (simp; fail)?)
apply (subst (asm) less_eq_fill_holes_iff; (simp; fail)?)
apply (subst (asm) unfill_holes_by_prefix'; (simp add: fill_unfill_holes_mctxt M'(2); fail)?)
using subsetD[OF ***(4), OF nth_mem]
by (force simp: shorter_terms_def set_conv_nth[of "zip _ _"]
mctxt_term_conv_fill_holes_mctxt unfill_fill_holes comp_def
subst_subst_compose[symmetric] subst_compose_def simp del: subst_subst_compose
elim!: less_eq_mctxt_MVarE2
dest!: ****[of "unfill_holes_mctxt (map_vars_mctxt Some N) M' ! _" _ Some]
)
with s order.trans[OF imageI[OF s, of rank, folded set_map, THEN max_list] rk]
have "s ∈ {Var (from_option None)} ∪ (shorter_terms ⋅⇩s⇩e⇩t (Var ∘ from_option ∘ Some))"
by (auto simp: shorter_terms_def image_def rank_var_subst[of _ "_ ∘ _", unfolded o_assoc])
}
note [dest!] = this show ?thesis
by (intro shallow_context.intros[of "max_topC (C ⊔ D)" "aliensC (C ⊔ D)"]
length_unfill_holes_mctxt max_topC_prefix fill_unfill_holes_mctxt[symmetric] max_topC_layer
subset_trans[OF set_aliensC_conv])
(auto simp: image_def subst_subst_compose[symmetric] subst_compose_def
term_mctxt_conv_mctxt_of_term_conv[unfolded comp_def] simp del: subst_subst_compose)
qed
lemma max_top_le_base:
assumes "(B, ts) = base_decomp t"
shows "max_top t ≤ B"
using assms
by (auto simp: base_decomp_def Let_def intro!: fill_holes_mctxt_suffix length_unfill_holes max_top_prefix)
text ‹@{cite ‹Lemma 4.19› FMZvO15}›
lemma base_decomp_max:
assumes t: "t ∈ native_terms" and C: "C ∈ shallow_context" "C ≤ mctxt_of_term t"
and bd: "(B, ts) = base_decomp t"
shows "C ≤ B"
proof -
have B: "B ∈ shallow_context" "B ≤ mctxt_of_term t" using assms(1,4)
using t C by (auto simp: native_terms_def base_decomp_shallow base_decomp_prefix)
have c: "(B, C) ∈ comp_mctxt" using B C by (intro prefix_comp_mctxt)
have mt: "max_topC (B ⊔ C) = max_top t"
using B C max_top_le_base[OF bd] sup_mctxt_ge1[OF c]
by (auto intro!: antisym intro: max_topC_mono prefix_mctxt_sup max_topC_props(2) simp: topsC_def)
have "B ⊔ C ∈ shallow_context" using B C c by (intro shallow_context_union)
from shallow_context_decomp[OF this]
obtain Ds where Ds: "length Ds = num_holes (max_top t)"
"set Ds ⊆ {MHole} ∪ mctxt_of_term ` shorter_terms - range MVar"
"B ⊔ C = fill_holes_mctxt (max_top t) Ds" by (metis mt)
note * = trans[OF arg_cong[OF fill_unfill_holes[of "max_top t" t], of mctxt_of_term, symmetric]
mctxt_of_term_fill_holes'[of "max_top t" "aliens t"], OF max_top_prefix length_unfill_holes[symmetric, OF max_top_prefix]]
have "B ≥ B ⊔ C"
using B(2) sup_mctxt_least[OF c B(2) C(2)] max_top_prefix[of t] Ds(1) subsetD[OF Ds(2), OF nth_mem] bd
unfolding Ds(3)
apply (simp only: base_decomp_def Let_def prod.inject native_terms_def)
apply (subst (asm) (3 5) *)
apply (subst (asm) (1 2) less_eq_fill_holes_iff; (simp; fail)?)
apply (subst (1) less_eq_fill_holes_iff; (simp; fail)?)
apply (auto simp: native_terms_def max_list_bound shorter_terms_def image_def intro!: less_eq_mctxtI2)
by (metis mctxt_of_term_inj mctxt_of_term_leq_imp_eq)
then show ?thesis using c antisym sup_mctxt_ge2 by fastforce
qed
text ‹This is a refinement of @{cite ‹Lemma 3.8› FMZvO15} (@{thm rank_by_top}}, but seems hard to
extract from the existing proof.›
lemma shallow_to_base_no_new_holes:
assumes "C ∈ shallow_context" "num_holes C = length ts" "set ts ⊆ short_terms"
"(B, ss) = base_decomp (fill_holes C ts)"
shows "hole_poss B ⊆ hole_poss C"
proof (intro subsetI, rule ccontr)
let ?t = "fill_holes C ts"
have t: "?t ∈ native_terms" using assms by (intro fill_shallow_context_imp_native)
then have "C ≤ B" using assms
by (auto intro: base_decomp_max[of ?t C B ss])
fix p assume p: "p ∈ hole_poss B" "p ∉ hole_poss C"
then obtain q where q: "q ∈ hole_poss C" "q < p"
by (auto elim: factor_hole_pos_by_prefix[OF `C ≤ B`] simp: less_pos_def)
then have "fill_holes C ts |_ q ∈ set ts"
using subt_at_fill_holes[OF assms(2)[symmetric]] set_hole_poss'
by (metis assms(2) in_set_conv_nth length_hole_poss')
then have "rank (fill_holes C ts |_ q) ≤ Suc rk" using assms(3) by (auto simp: short_terms_def)
with q(2) show False
proof (induct "size p - size q" arbitrary: q rule: less_induct)
case less note q = less(2,3)
obtain i where i: "i < num_holes (max_top ?t)" "p = hole_poss' (max_top ?t) ! i"
"¬ rank (aliens ?t ! i) ≤ rk"
using assms(2,4) p(1) hole_poss_fill_holes_mctxt[of "max_top ?t"
"map (λt. if rank t ≤ rk then mctxt_of_term t else MHole) (aliens ?t)"]
by (auto simp: base_decomp_def Let_def max_top_prefix split: if_splits)
then have r: "rank (aliens ?t ! i) = Suc rk" and p': "p ∈ hole_poss (max_top ?t)"
using subsetD[OF aliens_short_terms[OF t], OF nth_mem, of i]
by (auto simp: short_terms_def max_top_prefix set_hole_poss'[symmetric])
have "q ∈ funposs_mctxt (max_top ?t)" using q(1) i
proper_prefix_hole_poss_imp_funposs[of p "max_top ?t" q]
nth_mem[of i "hole_poss' (max_top ?t)", unfolded set_hole_poss']
by auto
note x = this subsetD[OF funposs_mctxt_subset_poss_mctxt, OF this]
subsetD[OF funposs_mctxt_subset_all_poss_mctxt, OF this]
moreover have y: "q ∈ poss ?t" using q(1) assms(2)
using all_poss_mctxt_mctxt_of_term all_poss_mctxt_mono max_topC_prefix x(3) by blast
moreover have "(subm_at (max_top (fill_holes C ts)) q, max_top (fill_holes C ts |_ q)) ∈ comp_mctxt"
using less_eq_subm_at[OF _ max_top_prefix[of ?t], of q] x
subm_at_mctxt_of_term[of q ?t]
by (auto intro!: prefix_comp_mctxt[of _ "mctxt_of_term (?t |_ q)"] max_top_prefix simp: y)
ultimately have "max_top (fill_holes C ts |_ q) ≤ subm_at (max_top (fill_holes C ts)) q"
using L⇩3[of "max_top ?t" "max_top (?t |_ q)" q, OF max_top_layer max_top_layer]
apply (subst less_eq_mctxt_sup_conv2, simp add: comp_mctxt_sym)
apply (subst (1) sup_mctxt_idem[symmetric, of "subm_at _ _"])
apply (subst sup_mctxt_assoc; (simp add: comp_mctxt_refl comp_mctxt_sym; fail)?)
apply (subst less_eq_mctxt_sup_conv2[symmetric])
apply (intro prefix_comp_mctxt[of _ "subm_at (max_top ?t) q"])
apply (auto simp: merge_mreplace_at replace_at_subm_at[unfolded all_poss_mctxt_conv, OF UnI1]
intro!: iffD1[OF compare_mreplace_at[of q "max_top ?t" _ "subm_at _ _"]] max_top_props(2))
using compare_mreplace_atI[OF max_top_prefix max_top_prefix, of q ?t "?t |_ q"]
subm_at_mctxt_of_term[of q ?t] replace_at_subm_at[of q "mctxt_of_term ?t"]
by (auto simp: topsC_def max_top_prefix intro!: prefix_mctxt_sup)
moreover have "pos_diff p q ∈ hole_poss (subm_at (max_top (fill_holes C ts)) q)"
using p' q(1) by (auto intro: pos_diff_hole_possI)
ultimately obtain "q'" where q': "q' ≤ pos_diff p q" "q' ∈ hole_poss (max_top (?t |_ q))"
using factor_hole_pos_by_prefix by blast
moreover have sig: "mctxt_of_term (?t |_ q) ∈ 𝒞" "?t |_ q ∈ 𝒯" using x y t
by (auto simp: 𝒞_def native_terms_def 𝒯_def funas_term_subt_at)
ultimately have q'': "q' ≠ ε" using non_empty_max_top_non_empty[of "mctxt_of_term (?t |_ q)"]
by (cases "max_top (fill_holes C ts |_ q)") auto
have "?t |_ (q <#> q') ∈ set (aliens (?t |_ q))" using y q'
by (auto simp: unfill_holes_conv max_top_prefix image_def set_hole_poss')
then have qq': "rank (?t |_ (q <#> q')) ≤ rk"
using q(2) sig by (subst (asm) rank.simps) (auto simp: max_list_bound_set)
show ?case
proof (cases "q' = pos_diff p q")
case True
moreover have "rank (?t |_ p) = Suc rk" using r i by (simp add: unfill_holes_conv max_top_prefix)
ultimately show ?thesis using qq' q by simp
next
case False then show ?thesis using q q' qq' q''
by (auto intro!: less(1)[of "q <#> q'"] simp: diff_less_mono2)
(metis less_pos_def less_simps(2) prefix_pos_diff)
qed
qed
qed
text ‹@{cite ‹Lemma 4.16› FMZvO15}›
lemma single_step_to_short_step:
assumes "s ∈ native_terms"
"(B, ss) = base_decomp s" "p ∈ poss_mctxt B" "(s, t) ∈ rstep_r_p_s' ℛ (l, r) p σ"
shows "(s, t) ∈ short_step"
proof -
note trs
moreover have "num_holes (max_top s) = length (aliens s)"
by (simp add: max_top_prefix)
moreover have "(fill_holes (max_top s) (aliens s), t) ∈ rstep_r_p_s' ℛ (l, r) p σ"
using assms(4) by (simp add: max_top_prefix fill_unfill_holes)
ultimately
obtain τ C where "(mctxt_term_conv B, mctxt_term_conv C) ∈ rstep_r_p_s' ℛ (l, r) p τ"
proof (cases rule: rewrite_cases_wf)
case outer
let ?ss = "map (λt. if rank t ≤ rk then mctxt_of_term t else MHole) (aliens s)"
have "s ∈ 𝒯" using assms(1) by (auto simp: native_terms_def)
from W'[OF this outer(1) assms(4)] obtain D τ where
D: "D ∈ 𝔏" "(mctxt_term_conv (max_top s), mctxt_term_conv D) ∈ rstep_r_p_s' ℛ (l, r) p τ"
by blast
have x: "l ⋅ σ = s |_ p" "p ∈ poss s" using assms(4) by auto
have "mctxt_term_conv B = fill_holes (map_vars_mctxt Some (max_top s)) (map mctxt_term_conv ?ss)"
using assms(2) by (auto simp: base_decomp_def Let_def mctxt_term_conv_fill_holes_mctxt max_top_prefix)
moreover have "map (map_vars_term Some) (aliens s) ∝ map mctxt_term_conv ?ss"
by (intro refines_trans[OF refines_map[of _ "map_vars_term (the_inv Some)"]])
(auto simp: refines_def inj_map_vars_term_the_inv[OF inj_Some])
ultimately obtain ts' τ' where "num_holes D = length ts'"
"(mctxt_term_conv B, mctxt_term_conv (term_mctxt_conv (
fill_holes (map_vars_mctxt Some D) ts'))) ∈ rstep_r_p_s' ℛ (l, r) p τ'"
"set ts' ⊆ set (map mctxt_term_conv ?ss)"
using rewrite_balanced_aliens[OF trs, of
"map_vars_mctxt Some (max_top s)" "map_vars_mctxt Some D" l r p
"map_vars_term (map_option Some) ∘ τ" "map (map_vars_term Some) (aliens s)"
"map_vars_term Some ∘ σ" "map mctxt_term_conv ?ss"]
rstep_r_p_s'_stable[OF D(2), of "Var ∘ map_option Some"]
arg_cong[OF x(1), of "λt. t ⋅ (Var ∘ Some)"] x(2)
by (auto simp: subst_compose_def comp_def mctxt_term_conv_map_vars_mctxt_subst
map_vars_term_eq max_top_prefix map_vars_term_fill_holes[symmetric] fill_unfill_holes
subst_subst_compose[symmetric] simp del: subst_subst_compose)
then show ?thesis using that by blast
next
case (inner i ti)
obtain q where *: "p = hole_poss' (max_top s) ! i <#> q" and [simp]: "pos_diff p (hole_poss' (max_top s) ! i) = q"
using inner(4) by (auto intro!: that)
let ?ss' = "map (λt. if rank t ≤ rk then mctxt_of_term t else MHole) (aliens s)"
have B: "B = fill_holes_mctxt (max_top s) ?ss'" using assms(1,2) by (auto simp: base_decomp_def Let_def)
have r: "rank (aliens s ! i) ≤ rk"
using assms(3) inner unfolding B * poss_mctxt_append_poss_mctxt
by (subst (asm) subm_at_fill_holes_mctxt) (auto simp: max_top_prefix split: if_splits)
show ?thesis
apply (intro that[of "fill_holes_mctxt (max_top s) (?ss'[i := mctxt_of_term ti])" "mctxt_term_conv ∘ mctxt_of_term ∘ σ"])
apply (subst B)
apply (subst (1 2) mctxt_term_conv_fill_holes_mctxt; (simp add: max_top_prefix; fail)?)
unfolding map_update *
apply (subst hole_poss'_map_vars_mctxt[of Some "max_top s", symmetric])
apply (subst fill_holes_rstep_r_p_s')
using inner(1-2) rstep_r_p_s'_stable[OF inner(3), of "Var ∘ Some"]
apply (auto simp: max_top_prefix comp_def subst_compose_def r)
done
qed
then show ?thesis
by (auto intro!: mirror_step.intros[OF assms(4)] short_stepI[OF assms(1,2), OF r_into_rtrancl])
qed
lemma single_step_to_tall_step:
assumes "s ∈ native_terms"
"(B, ss) = base_decomp s" "p ∉ poss_mctxt B" "(s, t) ∈ rstep_r_p_s' ℛ (l, r) p σ"
shows "(s, t) ∈ tall_step"
proof -
obtain i ti where "i < length ss" "t = fill_holes B (ss[i := ti])"
"(ss ! i, ti) ∈ rstep_r_p_s' ℛ (l, r) (pos_diff p (hole_poss' B ! i)) σ"
using assms rewrite_cases[of B ss t ℛ l r p σ]
by (simp only: base_decomp_fill_holes) metis
then show ?thesis using assms
by (intro tall_step.intros[of s B ss "ss[i := ti]" t])
(fastforce simp: base_decomp_fill_holes nth_list_update rstep'_iff_rstep_r_p_s')+
qed
lemma single_step_to_any_step:
"s ∈ native_terms ⟹ (s, t) ∈ rstep' ℛ ⟹ (s, t) ∈ short_step ∪ tall_step"
using single_step_to_short_step[of s] single_step_to_tall_step[of s]
by (auto simp: rstep'_iff_rstep_r_p_s') (metis surj_pair)
lemma mirror_step_to_short_step:
assumes "L ∈ shallow_context" "set ss ⊆ short_terms"
"length ss = num_holes L" "length ts = num_holes M"
"((fill_holes L ss, L), (fill_holes M ts, M)) ∈ mirror_step"
shows "(fill_holes L ss, fill_holes M ts) ∈ short_step"
proof -
obtain l r p σ τ where *: "(fill_holes L ss, fill_holes M ts) ∈ rstep_r_p_s' ℛ (l, r) p σ"
"(mctxt_term_conv L, mctxt_term_conv M) ∈ rstep_r_p_s' ℛ (l, r) p τ"
using assms(5) by auto
note ** = fill_shallow_context_imp_native[OF assms(1) assms(3)[symmetric] assms(2)]
moreover have "p ∈ poss_mctxt L" using wf_trs_implies_funposs[OF trs *(2)]
funposs_mctxt_subset_poss_mctxt by (auto simp: funposs_mctxt_def[symmetric])
then have "p ∈ poss_mctxt (fst (base_decomp (fill_holes L ss)))"
using base_decomp_max[OF ** assms(1) _ prod.collapse] assms(3) poss_mctxt_mono by fastforce
ultimately show ?thesis
by (intro single_step_to_short_step[OF _ prod.collapse _ *(1)])
qed
lemma mirror_steps_to_short_steps:
assumes "L ∈ shallow_context" "set ss ⊆ short_terms"
"length ss = num_holes L" "length ts = num_holes M"
"((fill_holes L ss, L), (fill_holes M ts, M)) ∈ mirror_step⇧*"
shows "(fill_holes L ss, fill_holes M ts) ∈ short_step⇧*"
using assms(5,1-4)
proof (induct "(fill_holes L ss, L)" arbitrary: L ss rule: converse_rtrancl_induct)
case (step z)
obtain z1 z2 where z: "z = (z1, z2)" by (metis prod.collapse)
note mirror_step_preserves_prefix[OF _ step(1)[unfolded z]]
moreover then have "(fill_holes z2 (unfill_holes z2 z1), fill_holes M ts) ∈ short_step⇧*"
using step(1,4,5,6) assms(4) mirror_step_aliens_mono[OF step(6), of "unfill_holes z2 z1" z2]
by (intro step(3))
(auto simp: fill_unfill_holes z rstep'_iff_rstep_r_p_s' intro!: shallow_context_closed[OF step(4), of z2], blast)
ultimately show ?case
using mirror_step_to_short_step[OF step(4,5,6), of "unfill_holes z2 z1" z2] step(1,6)
by (auto simp: z fill_unfill_holes)
qed auto
text ‹@{cite ‹Lemma 4.21› FMZvO15}›
lemma tall_short:
assumes
"C ∈ shallow_context" "set ss ⊆ short_terms"
"num_holes C = length ss" "num_holes C = length ts"
"⋀i. i < length ss ⟹ (ss ! i, ts ! i) ∈ (rstep' ℛ)⇧*"
obtains ss' ι where
"num_holes C = length ss'"
"(fill_holes C ss, fill_holes C ss') ∈ tall_step_i ι" "ι ≤ imbalance ts"
"(fill_holes C ss', fill_holes C ts) ∈ short_step⇧*"
proof -
let ?s = "fill_holes C ss"
have "?s ∈ native_terms" "?s ∈ 𝒯"
using fill_shallow_context_imp_native[OF assms(1,3,2)] by (simp_all add: native_terms_def)
obtain B ss0 where B: "(B, ss0) = base_decomp ?s" "hole_poss B ⊆ hole_poss C"
using shallow_to_base_no_new_holes[OF assms(1,3,2)] by (metis surj_pair)
let ?Bs = "unfill_holes_mctxt C B"
have "C ≤ B" using base_decomp_max[OF `?s ∈ native_terms` assms(1) fill_holes_suffix[OF assms(3)] B(1)] .
let ?ss' = "map (λi. if ?Bs ! i = MHole then ts ! i else ss ! i) [0..<num_holes C]"
let ?ts' = "map (λi. ts ! i) (filter (λi. ?Bs ! i = MHole) [0..<num_holes C])"
have hp: "[p←hole_poss' C . subm_at B p = MHole] = hole_poss' B"
using `C ≤ B` `hole_poss B ⊆ hole_poss C` unfolding set_hole_poss'[symmetric]
proof (induct C B rule: less_eq_mctxt_induct)
case (1 B)
then show ?case by (cases B, auto simp: UN_subset_iff image_subset_iff)
next
case (3 cs ds f) show ?case using 3(1,4)
by (auto simp: filter_concat filter_map comp_def intro!: arg_cong[of _ _ "concat"] arg_cong[of _ _ "map _"] 3(3))
(auto simp: image_def dest!: subsetD)
qed auto
have ss0: "ss0 = map (op ! ss) [i←[0..<num_holes C] . unfill_holes_mctxt C B ! i = MHole]"
using assms(3) filter_map[of "λp. subm_at B p = MHole" "op ! (hole_poss' C)" "[0..<num_holes C]", unfolded comp_def]
map_nth[of "hole_poss' C"]
unfolding unfill_holes_mctxt_conv[OF `C ≤ B`] hp[symmetric]
unfill_fill_holes[OF base_decomp_fill_holes(1)[OF B(1)], symmetric, unfolded filter_map base_decomp_fill_holes(2)[OF B(1)] unfill_holes_conv[OF base_decomp_prefix[OF B(1)]]]
by (auto simp: comp_def) (auto intro!: map_cong subt_at_fill_holes filter_cong)
have "p ∈ hole_poss C ⟹ subm_at B p ≠ MHole ⟹ subm_at (mctxt_of_term ?s) p = subm_at B p" for p
unfolding base_decomp_fill_holes(2)[OF B(1), symmetric] using `C ≤ B` B(2) base_decomp_fill_holes(1)[OF B(1), symmetric]
proof (induct C B arbitrary: p ss0 rule: less_eq_mctxt_induct)
case (1 B) moreover then have "hole_poss B = {}"
by auto (metis 1(1,2) empty_iff hole_poss.simps(2) subm_at_hole_poss subset_singletonD)
ultimately show ?case using length_hole_poss'[of B] set_hole_poss'[of B]
by (auto simp del: length_hole_poss') (metis fill_holes_suffix list.size(3) unfill_by_itselfD unfill_fill_holes)
next
case (3 cs ds f) show ?case using 3(1,2,4,5,6,7) by (auto intro!: 3(3)) auto
qed auto
from this[OF nth_mem[of _ "hole_poss' C", unfolded set_hole_poss']]
have B': "B = fill_holes_mctxt C (map (λi. if unfill_holes_mctxt C B ! i = MHole then MHole else mctxt_of_term (ss ! i)) [0..<num_holes C])"
apply (subst fill_unfill_holes_mctxt[OF `C ≤ B`, symmetric])
using `C ≤ B` subm_at_fill_holes_mctxt[of "map mctxt_of_term ss" C, symmetric]
by (auto intro!: nth_equalityI arg_cong[of _ _ "fill_holes_mctxt C"] simp: unfill_holes_mctxt_conv assms(3))
have ts: "set ts ⊆ short_terms" by (metis assms(2-5) short_sequence_rsteps(1))
show thesis
proof (intro that[of ?ss' "imbalance ?ts'"], goal_cases)
case 2 thus ?case
proof (intro tall_step_i.intros[OF B(1) `?s ∈ native_terms` _ _ _ refl, of ?ts'], goal_cases)
case 1
have *: "filter (λp. subm_at B p = MHole) (hole_poss' C) =
map (op ! (hole_poss' C)) [i←[0..<num_holes C] . map (subm_at B) (hole_poss' C) ! i = MHole]"
using filter_map[of "λp. subm_at B p = MHole" "op ! (hole_poss' C)" "[0..<num_holes C]"]
by (auto simp: comp_def length_hole_poss'[of C, symmetric] map_nth simp del: length_hole_poss'
cong: map_cong intro!: arg_cong[of _ _ "map (op ! (hole_poss' C))"] filter_cong)
from arg_cong[OF hp, of length] show ?case using `C ≤ B` by (simp add: unfill_holes_mctxt_conv *)
next
case 2
show ?case using `C ≤ B`
apply (subst (2) B')
apply (subst fill_holes_mctxt_fill_holes, simp, simp add: num_holes_fill_holes_mctxt comp_def if_distrib length_filter_sum_list cong: if_cong)
apply (intro arg_cong[of _ _ "fill_holes _"] map_cong refl)
using arg_cong[OF partition_by_predicate[of _ "[0..<num_holes C]" "λi. unfill_holes_mctxt C B ! i = MHole"], of _ "map (op ! ts)"]
by (simp add: comp_def if_distrib cong: if_cong)
next
case (3 i)
show ?case using 3 base_decomp_fill_holes(1)[OF B(1), symmetric] assms(3,4) `C ≤ B`
nth_mem[of i "[i←[0..<length ss] . unfill_holes_mctxt C B ! i = MHole]"] by (auto intro!: assms(5) simp: ss0)
qed
next
case 3 thus ?case using assms(4) by (auto simp: imbalance_def image_def intro!: card_mono)
next
case 4
have *: "fill_holes_mctxt C (map (λi. if unfill_holes_mctxt C B ! i = MHole then MHole else mctxt_of_term (ss ! i)) [0..<num_holes C]) ∈ shallow_context"
unfolding B'[symmetric] using base_decomp_shallow[OF `?s ∈ 𝒯` B(1)] .
{ fix n
assume "⋀i. n ≤ i ⟹ i < num_holes C ⟹ ss ! i = ts ! i"
then have
"(fill_holes C (map (λi. if unfill_holes_mctxt C B ! i = MHole then ts ! i else ss ! i)
[0..<num_holes C]), fill_holes C ts) ∈ short_step⇧*" (is "?X ss")
using assms(3,5,2) *
proof (induct n arbitrary: ss)
case 0
then have "(map (λi. if unfill_holes_mctxt C B ! i = MHole then ts ! i else ss ! i) [0..<num_holes C]) = ts"
using assms(4) by (auto intro!: nth_equalityI)
then show ?case by simp
next
case (Suc n) thus ?case
proof (cases "n < length ss")
case True
from Suc(2) have **: "n ≤ i ⟹ i < num_holes C ⟹ ss[n := ts ! n] ! i = ts ! i"
"i < length ss ⟹ (ss[n := ts ! n] ! i, ts ! i) ∈ (rstep' ℛ)⇧*" for i
using assms(4) Suc(3,4) by (cases "n = i"; simp)+
moreover have "set (ss[n := ts ! n]) ⊆ short_terms"
using True Suc(3,5) ts assms(4) by (auto simp: set_conv_nth nth_list_update)
moreover
have *: "fill_holes_mctxt C (map (λi. if unfill_holes_mctxt C B ! i = MHole then MHole else mctxt_of_term (ss[n := ts ! n] ! i)) [0..<num_holes C]) ∈ shallow_context"
using Suc(3) Suc(4)[of n] True
by (auto simp: mctxt_term_conv_fill_holes_mctxt nth_list_update intro!: shallow_context_closed'[OF Suc(6)] fill_holes_rsteps rsteps'_stable)
ultimately have "?X (ss[n := ts ! n])" (is "(?F (ss[n := ts ! n]), _) ∈ _")
using Suc(1)[of "ss[n := ts ! n]"] Suc(3,5) by auto
moreover have "(?F ss, ?F (ss[n := ts ! n])) ∈ short_step⇧*"
using Suc(4)[OF True] True Suc(5,3,6)
proof (induct "ss ! n" arbitrary: ss rule: converse_rtrancl_induct)
case (step ssn')
obtain l r p σ where sss: "(ss ! n, ssn') ∈ rstep_r_p_s' ℛ (l, r) p σ"
using step(1)[unfolded rstep'_iff_rstep_r_p_s'] by blast
have "(?F ss, ?F (ss[n := ssn'])) ∈ short_step⇧="
proof (cases "unfill_holes_mctxt C B ! n = MHole")
case True then show ?thesis
using step(4) by (intro UnI2) (auto simp: nth_list_update intro!: arg_cong[of _ _ "fill_holes _"])
next
case False
then have *: "map (λi. if unfill_holes_mctxt C B ! i = MHole then ts ! i else ss[n := ssn'] ! i) [0..<num_holes C] =
(map (λi. if unfill_holes_mctxt C B ! i = MHole then ts ! i else ss ! i) [0..<num_holes C])[n := ssn']"
using step(4) by (auto simp: nth_list_update intro!: nth_equalityI)
show ?thesis using step(4-) ts assms(4) unfolding *
proof (intro UnI1 single_step_to_short_step[OF _ prod.collapse, of _ "hole_poss' C ! n <#> p" _ l r σ] fill_shallow_context_imp_native, goal_cases)
case 4
let ?B' = "fill_holes_mctxt C (map (λi. if unfill_holes_mctxt C B ! i = MHole then MHole else mctxt_of_term (ss ! i)) [0..<num_holes C])"
show ?case
proof (subst subsetD[OF poss_mctxt_mono[OF base_decomp_max], OF _ _ _ prod.collapse, of _ ?B'], goal_cases)
case 1 then show ?case
using assms(1,4) step(5,6) ts by (intro fill_shallow_context_imp_native) auto
next
case 2 then show ?case using step(7) .
next
case 4 then show ?case using step(4) step(6)[symmetric] set_hole_poss'[of C]
unfolding poss_mctxt_append_poss_mctxt
using subsetD[OF _ nth_mem, of _ "hole_poss C"] wf_trs_implies_funposs[OF trs sss] False
by (intro conjI subsetD[OF fill_holes_mctxt_extends_all_poss])
(auto simp: all_poss_mctxt_conv subm_at_fill_holes_mctxt funposs_imp_poss)
qed (auto simp: mctxt_of_term_fill_holes' less_eq_fill_holes_iff)
next
case 5
then show ?case using sss False
apply (subst replace_at_fill_holes[symmetric], simp, simp)
apply (intro HOL.subst[of _ _ "λt. (t, _) ∈ _", OF _ HOL.subst[of _ _ "λp. _ ∈ rstep_r_p_s' _ _ (p <#> _) _", OF _ rstep_r_p_s'_mono]],
subst ctxt_supt_id)
by (auto simp: hole_poss_in_poss_fill_holes subt_at_fill_holes)
qed (auto simp: assms(1))
qed
moreover have "set (ss[n := ssn']) ⊆ short_terms"
using short_terms_closed[OF _ step(1)] step(4,5) set_update_subset_insert[of ss n ssn']
by (auto simp: subset_eq)
moreover note step(7)
then have "fill_holes_mctxt C (map (λi. if unfill_holes_mctxt C B ! i = MHole then MHole else mctxt_of_term (ss[n := ssn'] ! i)) [0..<num_holes C]) ∈ shallow_context"
using step(1,4)
by (auto 0 3 simp: mctxt_term_conv_fill_holes_mctxt nth_list_update
intro!: shallow_context_closed'[OF step(7)] fill_holes_rsteps rsteps'_stable)
ultimately show ?case using step(3)[of "ss[n := ssn']"] step(4-6) by (auto cong: if_cong)
qed (auto cong: if_cong)
ultimately show ?thesis by auto
qed auto
qed
} note this[of "num_holes C"]
then show ?case by auto
qed auto
qed
text ‹@{cite ‹Lemma 4.23› FMZvO15}›
lemma tall_tall_peak:
assumes "(s, t) ∈ tall_step_i ι" "(s, u) ∈ tall_step_i κ"
obtains ι' κ' t' u' v where "ι' ≤ ι" "κ' ≤ κ"
"(t, t') ∈ tall_step_i κ'" "(t', v) ∈ short_step⇧*"
"(u, u') ∈ tall_step_i ι'" "(u', v) ∈ short_step⇧*"
proof -
from assms obtain B ss ts us where
s: "s ∈ native_terms" "(B, ss) = base_decomp s" and
t: "length ts = num_holes B" "t = fill_holes B ts"
"⋀i. i < num_holes B ⟹ (ss ! i, ts ! i) ∈ (rstep' ℛ)⇧*" "ι = imbalance ts" and
u: "length us = num_holes B" "u = fill_holes B us"
"⋀i. i < num_holes B ⟹ (ss ! i, us ! i) ∈ (rstep' ℛ)⇧*" "κ = imbalance us"
by (elim tall_step_i.cases) (auto, metis prod.inject)
have B: "B ∈ shallow_context" "set ss ⊆ short_terms" "num_holes B = length ss"
using s aliens_short_terms[of s] base_decomp_aliens[OF _ s(2)]
by (auto simp: native_terms_def base_decomp_shallow base_decomp_fill_holes)
then obtain vs where *: "length vs = length ss"
"⋀i. i < length ss ⟹ (ts ! i, vs ! i) ∈ (rstep' ℛ)⇧*"
"⋀i. i < length ss ⟹ (us ! i, vs ! i) ∈ (rstep' ℛ)⇧*"
"ts ∝ vs" "us ∝ vs"
"set ts ⊆ short_terms" "set us ⊆ short_terms" "set vs ⊆ short_terms"
using balance_short_sequences[of ts ss us] t(1-3) u(1-3) by auto
moreover obtain ts' ι' where "num_holes B = length ts'"
"(fill_holes B ts, fill_holes B ts') ∈ tall_step_i ι'"
"ι' ≤ imbalance vs" "(fill_holes B ts', fill_holes B vs) ∈ short_step⇧*"
using tall_short[OF B(1) *(6) t(1)[symmetric], of vs thesis] *(1,2) t(1) B(3) by auto
moreover obtain us' κ' where "num_holes B = length us'"
"(fill_holes B us, fill_holes B us') ∈ tall_step_i κ'"
"κ' ≤ imbalance vs" "(fill_holes B us', fill_holes B vs) ∈ short_step⇧*"
using tall_short[OF B(1) *(7) u(1)[symmetric], of vs thesis] *(1,3) u(1) B(3) by auto
ultimately show ?thesis
by (intro that[of κ' ι' "fill_holes B ts'" "fill_holes B vs" "fill_holes B us'"])
(auto dest!: refines_imbalance_mono simp: t(2,4) u(2,4))
qed
text ‹@{cite ‹Lemma 4.25› FMZvO15}›
lemma base_decomp_short:
assumes "t ∈ native_terms" "(B, ss) = base_decomp t"
shows "set ss ⊆ short_terms"
using aliens_short_terms[OF assms(1)] assms(2) by (auto simp: base_decomp_def Let_def)
lemma tall_short_peak:
assumes "(s, t) ∈ tall_step_i ι" "(s, u) ∈ short_step"
obtains ι' ι'' t' u' v where "ι' ≤ ι"
"t = t' ∨ ι'' < ι ∧ (t, t') ∈ tall_step_i ι''" "(t', v) ∈ short_step⇧*"
"(u, u') ∈ tall_step_i ι'" "(u', v) ∈ short_step⇧*"
proof -
obtain B ss where B: "base_decomp s = (B, ss)" by (metis prod.exhaust)
obtain ts where ts: "s ∈ native_terms" "length ts = num_holes B" "t = fill_holes B ts"
"⋀i. i < num_holes B ⟹ (ss ! i, ts ! i) ∈ (rstep' ℛ)⇧*" "ι = imbalance ts" "s ∈ 𝒯"
using assms(1) by (auto simp: B native_terms_def elim!: tall_step_i.cases)
have ss: "set ss ⊆ short_terms" "length ss = num_holes B" and s: "s = fill_holes B ss"
using base_decomp_short[OF ts(1)] by (auto simp: B base_decomp_fill_holes[OF B[symmetric]])
obtain C where C: "((s, B), (u, C)) ∈ mirror_step⇧*"
using assms(2) by (auto simp: B elim!: short_stepE)
obtain us where us: "length us = num_holes C" "u = fill_holes C us" "set us ⊆ set ss"
"((fill_holes B (map f ss), B), (fill_holes C (map f us), C)) ∈ mirror_step⇧*"
"C ∈ shallow_context" for f
using C ss(2) base_decomp_shallow[OF `s ∈ 𝒯` B(1)[symmetric]] unfolding s
proof (induct "(u, C)" arbitrary: u C thesis rule: rtrancl_induct)
case (step y)
obtain y1 y2 where [simp]: "y = (y1, y2)" by (metis prod.collapse)
obtain us where us: "length us = num_holes y2" "y1 = fill_holes y2 us" "set us ⊆ set ss"
"⋀f. ((fill_holes B (map f ss), B), (fill_holes y2 (map f us), y2)) ∈ mirror_step⇧*"
"y2 ∈ shallow_context"
using step(3)[OF prod.collapse[symmetric] _ step(5)] step(6) unfolding `y = (y1, y2)` fst_conv snd_conv by blast
have "(mctxt_term_conv y2, mctxt_term_conv C) ∈ rstep' ℛ"
by (metis step(2) `y = (y1, y2)` mirror_step.simps rstep'_iff_rstep_r_p_s')
moreover have "((fill_holes B (map f ss), B), fill_holes C (map f (unfill_holes C u)), C) ∈ mirror_step⇧*" for f
using mirror_step_preserves_prefix[of "y2" "y1" u C] step(2) us(1,2,4)
by simp (metis (no_types, lifting) fill_unfill_holes length_unfill_holes mirror_step_stable rtrancl.simps)
ultimately show ?case using mirror_step_aliens_mono[of us "y2" "unfill_holes C u" C]
mirror_step_preserves_prefix[of "y2" "y1" u C] step(2) us(1-3)
by (auto intro!: step(4)[of "unfill_holes C u"] shallow_context_closed[OF us(5)] simp: fill_unfill_holes)
qed auto
obtain vs where vs:
"⋀i. i < length ss ⟹ (ts ! i, vs ! i) ∈ (rstep' ℛ)⇧*"
"ss ∝ vs" "ts = vs ∨ imbalance vs < imbalance ts"
proof (cases "ss ∝ ts" rule: case_split)
case True then show ?thesis by (auto intro: that[of ts])
next
case False
moreover obtain vs where "⋀i. i < length ss ⟹ (ts ! i, vs ! i) ∈ (rstep' ℛ)⇧*"
"ss ∝ vs" "ts ∝ vs" "set ts ⊆ short_terms"
by (metis balance_short_sequences[of ss ss ts] ss ts(2,4) rtrancl_refl)
ultimately show ?thesis using refines_imbalance_strict_mono[of ts vs] refines_trans[of ss vs ts]
by (auto intro!: that[of vs])
qed
then have *: "⋀i. i < length ss ⟹ (ss ! i, vs ! i) ∈ (rstep' ℛ)⇧*"
using ts(2) ts(4) ss(2) by force
obtain f where f: "vs = map f ss" using `ss ∝ vs` by (auto elim: refines_imp_map)
have "((fill_holes B (map f ss), B), (fill_holes C (map f us), C)) ∈ mirror_step⇧*" using us(4) .
have "i < length us ⟹ (us ! i, map f us ! i) ∈ (rstep' ℛ)⇧*" for i
using f ss(2) us(1) * subsetD[OF us(3), unfolded in_set_conv_nth] by auto metis
with tall_short[of C us "map f us", OF us(5) subset_trans[OF us(3) ss(1)]]
obtain us' ι' where us':
"num_holes C = length us'" "(fill_holes C us, fill_holes C us') ∈ tall_step_i ι'"
"ι' ≤ imbalance (map f us)"
"(fill_holes C us', fill_holes C (map f us)) ∈ short_step⇧*" unfolding length_map us(1) by blast
moreover have "ι' ≤ ι" using us'(3) us(3) ts(5) vs(3) imbalance_mono[of "map f us" "map f ss"]
by (auto simp: image_mono f)
moreover have "set ts ⊆ short_terms" using ss(1,2) ts(2,4)
by (auto simp: in_set_conv_nth) (metis nth_mem short_terms_closed' subset_code(1))
then obtain ts' ι'' where ts':
"num_holes B = length ts'" "(fill_holes B ts, fill_holes B ts') ∈ tall_step_i ι''"
"ι'' ≤ imbalance vs"
"(fill_holes B ts', fill_holes B vs) ∈ short_step⇧*"
using base_decomp_shallow[OF ts(6) B[symmetric]] vs(1) tall_short[of B ts vs thesis]
unfolding ss(2) ts(2) conjunct1[OF `ss ∝ vs`[unfolded refines_def]] by blast
moreover have "ts = vs ∨ ι'' < ι" using vs(3) ts'(3) ts(5) by auto
moreover have "set (map f ss) ⊆ short_terms" using ss(1) short_terms_closed'[OF _ *]
using "*" f length_map short_sequence_rsteps(1) by blast
then have "(fill_holes B vs, fill_holes C (map f us)) ∈ short_step⇧*"
using us(4)[of f] base_decomp_shallow[OF ts(6) B[symmetric]] ss(2) us(1) unfolding f
by (intro mirror_steps_to_short_steps) simp_all
ultimately show ?thesis
by (intro that[of ι' "fill_holes B (if ts = vs then vs else ts')" ι'' "fill_holes C (map f us)" "fill_holes C us'"])
(auto simp: ts(3) us(2))
qed
text ‹Common analysis for short-short peaks.›
lemma rsteps_to_mirror_steps:
"(s, t) ∈ (rstep' ℛ)⇧* ⟹ ((s ⋅ σ, term_mctxt_conv (s ⋅ τ)), (t ⋅ σ, term_mctxt_conv (t ⋅ τ))) ∈ mirror_step⇧*"
proof (induct t rule: rtrancl_induct)
case (step t t')
obtain l r p σ' where "(t, t') ∈ rstep_r_p_s' ℛ (l, r) p σ'"
using step(2) by (auto simp: rstep'_iff_rstep_r_p_s')
then show ?case using mirror_step.intros[of "t ⋅ σ" "t' ⋅ σ" l r p "σ' ∘⇩s σ"
"term_mctxt_conv (t ⋅ τ)" "term_mctxt_conv (t' ⋅ τ)" "σ' ∘⇩s τ"] step(3)
by (force intro: rstep_r_p_s'_stable)
qed auto
lemma short_term_from_shallow_context:
assumes "B ∈ shallow_context" "length ss = num_holes B" "⋀s. s ∈ set ss ⟹ is_Var s"
shows "fill_holes B ss ∈ short_terms"
proof -
obtain L Cs where L: "L ∈ 𝔏" "length Cs = num_holes L" "B = fill_holes_mctxt L Cs"
"set Cs ⊆ {MHole} ∪ mctxt_of_term ` shorter_terms" by (metis shallow_context.cases[OF assms(1)])
have *: "fill_holes B ss ∈ 𝒯" using subsetD[OF funas_shallow_context[OF assms(1)]] assms(2,3)
by (force simp: 𝒯_def funas_term_fill_holes_iff is_Var_def)
define ss' where "ss' = map (λi. fill_holes (Cs ! i) (partition_holes ss Cs ! i)) [0..<num_holes L]"
have s: "fill_holes B ss = fill_holes L ss'" "length ss' = num_holes L"
using L(2) assms(2) by (auto simp add: fill_holes_mctxt_fill_holes L(3) ss'_def)
have "i < num_holes L ⟹ is_Fun (ss' ! i) ⟹ ss' ! i ∈ shorter_terms" for i
unfolding ss'_def using length_partition_by_nth[of "map num_holes Cs" ss i] assms(2,3)
partition_by_nth_nth_elem[of "map num_holes Cs" ss i 0] subsetD[OF L(4), OF nth_mem, of i]
by (cases "partition_holes ss Cs ! i") (auto simp: L(2,3) num_holes_fill_holes_mctxt)
then have "set (filter is_Fun ss') ⊆ shorter_terms" by auto (auto simp: s(2) set_conv_nth)
from subsetD[OF this] have "rank (fill_holes B ss) ≤ Suc rk" using L(1)
by (subst le_trans[OF rank_by_top'[OF * max_top_props(2), of L]])
(auto simp: s shorter_terms_def ss'_def[symmetric] unfill_fill_holes topsC_def max_list_bound_set)
then show ?thesis using * by (simp add: short_terms_def)
qed
lemma short_short_pre:
assumes "(s, t) ∈ short_step_s s0" "(s, u) ∈ short_step_s s1"
obtains B ss C D E v where
"s ∈ native_terms" "(B, ss) = base_decomp s"
"((s, B),(t, C)) ∈ mirror_step⇧*" "((s, B),(u, D)) ∈ mirror_step⇧*"
"C ∈ shallow_context" "C ≤ mctxt_of_term t"
"D ∈ shallow_context" "D ≤ mctxt_of_term u"
"t ∈ native_terms" "(s1, t) ∈ (rstep ℛ)⇧*" "((t, C), (v, E)) ∈ mirror_step⇧*"
"u ∈ native_terms" "(s0, u) ∈ (rstep ℛ)⇧*" "((u, D), (v, E)) ∈ mirror_step⇧*"
proof -
obtain B ss C D where
st: "(s0, s) ∈ (rstep ℛ)⇧*" "((s, B),(t, C)) ∈ mirror_step⇧*" and
su: "(s1, s) ∈ (rstep ℛ)⇧*" "((s, B),(u, D)) ∈ mirror_step⇧*" and
s: "s ∈ native_terms" "(B, ss) = base_decomp s"
by (metis short_step_sE[OF assms(1)] short_step_sE[OF assms(2)] Pair_inject)
have "B ∈ shallow_context" using base_decomp_shallow[OF _ s(2)] s(1)
by (simp add: native_terms_def)
have "B ≤ mctxt_of_term s" using base_decomp_prefix[OF s(2)] .
have "ss = unfill_holes B s"using base_decomp_fill_holes[OF s(2)] by (metis unfill_fill_holes)
obtain b0 σ where b0: "b0 ⋅ σ = mctxt_term_conv B" "⋀x. σ x ∈ {Var (Some x), Var None}"
"⋀D. B ≤ D ⟹ ∃τ. b0 ⋅ τ = mctxt_term_conv D ∧ (∀x. σ x = Var None ∨ τ x = Var (Some x))"
using represent_context_by_term[of B] by blast
obtain τ where τ: "b0 ⋅ τ = s ⋅ (Var ∘ Some)" "⋀x. σ x = Var None ∨ τ x = Var (Some x)"
using b0(3)[OF base_decomp_prefix[OF s(2)]] by auto
define f where "f ≡ λs. Var (SOME x. σ x = Var None ∧ τ x = s ⋅ (Var ∘ Some)) :: ('f, 'v) term"
define b where "b = fill_holes B (map f ss)"
have *: "s = b0 ⋅ τ ∘⇩s (Var ∘ the)" using `B ≤ mctxt_of_term s` τ(1)
by simp (simp del: subst_subst_compose add: subst_subst_compose[symmetric] subst_compose_def fill_unfill_holes)
have "b ∈ short_terms" using `B ∈ shallow_context` base_decomp_fill_holes(1)[OF s(2)]
unfolding b_def f_def by (auto intro!: short_term_from_shallow_context simp: is_Var_def)
have "b0 ⋅ (τ ∘⇩s (Var ∘ the) ∘⇩s (Var ∘ Some)) = b0 ⋅ τ" using τ
by simp (simp del: subst_subst_compose add: subst_subst_compose[symmetric] subst_compose_def)
then have [simp]: "x ∈ vars_term b0 ⟹ σ x = Var None ⟹ τ x ⋅ (λx. Var (Some (the x))) = τ x" for x
by (auto simp del: subst_subst_compose simp: term_subst_eq_conv subst_subst_compose[symmetric] subst_compose_def)
have "x ∈ vars_term b0 ⟹ σ x = Var None ⟹ f (τ x ⋅ (Var ∘ the)) ⋅ σ = Var None" for x
using someI[of "λy. σ y = Var None ∧ τ y = τ x ⋅ (Var ∘ the) ⋅ (Var ∘ Some)" x]
unfolding f_def subst_subst_compose[symmetric] subst_compose_def by auto
then have bB: "b ⋅ σ = mctxt_term_conv B"
unfolding b_def `ss = unfill_holes B s`
apply (subst alien_map_by_substitution[OF b0(1)[symmetric], of _ "τ ∘⇩s (Var ∘ the)"])
subgoal using b0(2) by (auto simp: is_Var_def)
subgoal using `B ≤ mctxt_of_term s` by simp
subgoal using `B ≤ mctxt_of_term s` by (simp add: fill_unfill_holes *)
using `B ≤ mctxt_of_term s` b0(2) τ(2)
unfolding b0(1)[symmetric] subst_subst_compose[symmetric] term_subst_eq_conv
by (force simp: subst_compose_def)
have "x ∈ vars_term b0 ⟹ σ x = Var None ⟹ f (τ x ⋅ (Var ∘ the)) ⋅ τ = τ x" for x
using someI[of "λy. σ y = Var None ∧ τ y = τ x ⋅ (Var ∘ the) ⋅ (Var ∘ Some)" x]
unfolding f_def subst_subst_compose[symmetric] subst_compose_def by auto
then have bs: "b ⋅ τ = s ⋅ (Var ∘ Some)"
unfolding b_def `ss = unfill_holes B s`
apply (subst alien_map_by_substitution[OF b0(1)[symmetric], of _ "τ ∘⇩s (Var ∘ the)"])
subgoal using b0(2) by (auto simp: is_Var_def)
subgoal using `B ≤ mctxt_of_term s` by simp
subgoal using `B ≤ mctxt_of_term s` by (simp add: fill_unfill_holes *)
using `B ≤ mctxt_of_term s` b0(2) τ(2)
unfolding τ(1)[symmetric] subst_subst_compose[symmetric] term_subst_eq_conv
by (force simp: subst_compose_def)
{ fix t C assume "((s, B),(t, C)) ∈ mirror_step⇧*"
then have "∃c. (b, c) ∈ (rstep' ℛ)⇧* ∧ c ⋅ σ = mctxt_term_conv C ∧ c ⋅ τ = t ⋅ (Var ∘ Some)"
using bB bs `B ≤ mctxt_of_term s` unfolding b_def `ss = unfill_holes B s`
proof (induct "(s, B)" arbitrary: s B rule: converse_rtrancl_induct)
case (step sB)
from step(1) obtain s' B' l r p σ' τ' where
sB: "sB = (s', B')" and
ss': "(s, s') ∈ rstep_r_p_s' ℛ (l, r) p σ'" and
BB': "(mctxt_term_conv B, mctxt_term_conv B') ∈ rstep_r_p_s' ℛ (l, r) p τ'"
using mirror_step.cases prod.collapse by metis
have "B' ≤ mctxt_of_term s'" using mirror_step_preserves_prefix[OF `B ≤ mctxt_of_term s` step(1)[unfolded sB]] .
let ?sf = "fill_holes B (map f (unfill_holes B s))"
let ?sf' = "fill_holes B' (map f (unfill_holes B' s'))"
obtain ρ where x: "(?sf, ?sf') ∈ rstep_r_p_s' ℛ (l, r) p ρ"
using `B ≤ mctxt_of_term s` `B' ≤ mctxt_of_term s'` ss' BB'
rewrite_balanced_aliens'[OF trs, of "unfill_holes B s" B "unfill_holes B' s'" B' l r p σ' τ' f]
by (auto simp: fill_unfill_holes)
have "(?sf, ?sf') ∈ rstep' ℛ" "?sf' ⋅ σ = mctxt_term_conv B'" "?sf' ⋅ τ = s' ⋅ (Var ∘ Some)"
using rstep_r_p_s'_stable[OF ss', of "Var ∘ Some"] BB'
rstep_r_p_s'_stable[OF x, of σ] rstep_r_p_s'_stable[OF x, of τ] x unfolding step(4,5)
by (auto intro: rstep_r_p_s'_deterministic[OF trs] simp: rstep'_iff_rstep_r_p_s')
then show ?case using step(3)[OF sB] `B' ≤ mctxt_of_term s'` by (meson converse_rtrancl_into_rtrancl)
qed auto
}
from this[OF st(2)] this[OF su(2)] obtain c d where
c: "(b, c) ∈ (rstep' ℛ)⇧*" "c ⋅ σ = mctxt_term_conv C" "c ⋅ τ = t ⋅ (Var ∘ Some)" and
d: "(b, d) ∈ (rstep' ℛ)⇧*" "d ⋅ σ = mctxt_term_conv D" "d ⋅ τ = u ⋅ (Var ∘ Some)" by blast
let ?p = "λt . (t ⋅ (τ ∘⇩s (Var ∘ the)), term_mctxt_conv (t ⋅ σ))"
obtain e where "(c, e) ∈ (rstep' ℛ)⇧*" "(d, e) ∈ (rstep' ℛ)⇧*" using c(1) d(1) `b ∈ short_terms`
by (metis CR_on_def joinE IH_rk' CR_on_iff_CR_Restr[of short_terms "rstep' ℛ", symmetric] short_terms_closed)
then have "(?p c, ?p e) ∈ mirror_step⇧*" "(?p d, ?p e) ∈ mirror_step⇧*"
by (metis rsteps_to_mirror_steps)+
moreover have "C ≤ mctxt_of_term t" "D ≤ mctxt_of_term u"
using mirror_steps_preserve_prefix[OF base_decomp_prefix, OF s(2)] st(2) su(2) by auto
moreover have "C ∈ shallow_context" "D ∈ shallow_context" using st(2) su(2)
shallow_context_closed'[OF `B ∈ shallow_context` mirror_steps_imp_rsteps'] by simp_all
moreover have "(s, t) ∈ (rstep' ℛ)⇧*" "(s, u) ∈ (rstep' ℛ)⇧*"
using st(2) su(2) by (auto simp: mirror_steps_imp_rsteps)
then have "t ∈ native_terms" "u ∈ native_terms" "(s1, t) ∈ (rstep ℛ)⇧*" "(s0, u) ∈ (rstep ℛ)⇧*"
using native_terms_rsteps[of s t] native_terms_rsteps[of s u] st(1) su(1) s(1)
unfolding rstep_eq_rstep' by simp_all
ultimately show ?thesis
using arg_cong[OF c(3), of "λt. t ⋅ (Var ∘ the)"] arg_cong[OF d(3), of "λt. t ⋅ (Var ∘ the)"]
unfolding c(2) d(2) subst_subst_compose[symmetric] subst_compose_def
by (simp add: that[OF s st(2) su(2)])
qed
end
locale weakly_layered_induct_dd = weakly_layered_induct ℱ 𝔏 ℛ rk
for ℱ :: "('f × nat) set" and 𝔏 :: "('f, 'v :: infinite) mctxt set" and ℛ :: "('f, 'v) trs"
and rk :: nat +
fixes R :: "('f, 'v) term rel"
assumes wf_R: "wf R" and trans_R: "trans R" and
short_short_peak: "⋀s t u. (s, t) ∈ short_step_s s0 ⟹ (s, u) ∈ short_step_s s1 ⟹
(t, u) ∈ ((⋃i∈under R s0. short_step_s i)⇧↔)⇧* O
(short_step_s s1)⇧= O
((⋃i∈under R s0 ∪ under R s1. short_step_s i)⇧↔)⇧* O
((short_step_s s0)¯)⇧= O ((⋃i∈under R s1. short_step_s i)⇧↔)⇧*"
begin
inductive_set R' :: "(('f, 'v) term + nat) rel" where
R'r: "x < y ⟹ (Inr x, Inr y) ∈ R'"
| R's: "(Inl x, Inr y) ∈ R'"
| R'l: "(s, t) ∈ R ⟹ (Inl s, Inl t) ∈ R'"
lemma R'_simps [simp]:
"(Inr x, Inr y) ∈ R' ⟷ x < y"
"(Inl s, Inr y) ∈ R'"
"(Inr x, Inl t) ∉ R'"
"(Inl s, Inl t) ∈ R' ⟷ (s, t) ∈ R"
by (auto intro: R'.intros elim: R'.cases)
lemma R'_cases:
"(x, y) ∈ R' ⟷ (case (x, y) of
(Inl s, Inl t) ⇒ (s, t) ∈ R
| (Inr x, Inl t) ⇒ False
| (Inl s, Inr y) ⇒ True
| (Inr x, Inr y) ⇒ x < y)"
by (cases x; cases y; simp)
primrec any_step :: "('f, 'v) term + nat ⇒ ('f, 'v) term rel" where
"any_step (Inl s0) = short_step_s s0"
| "any_step (Inr ι) = tall_step_i ι"
lemma wf_R':
"wf R'"
proof -
have [simp]: "R' = inv_image
({(x, y). x < y} <*lex*> (map_prod Inl Inl ` R ∪ map_prod Inr Inr ` {(x, y). x < y}))
(λi. case i of Inl x ⇒ (0 :: nat, i) | Inr x ⇒ (1, i))"
by (force split: sum.splits prod.splits simp: map_prod_def image_def)
show ?thesis by (auto intro!: wf_less wf_Un wf_map_prod_image wf_R)
qed
lemma trans_R':
"trans R'"
by (auto simp: trans_def R'_cases split: sum.splits(2)) (metis trans_R trans_def)
lemma under_Inl:
"(⋃i∈under R' (Inl s0). any_step i) = (⋃i∈under R s0. short_step_s i)"
by (force simp: under_def elim: R'.cases intro: R'.intros)
lemma under_Inr:
"(⋃i∈under R' (Inr ι). any_step i) = (⋃i<ι. tall_step_i i) ∪ short_step"
by (force simp: under_def short_step_iff_short_step_s elim: R'.cases intro: R'.intros)
lemma CR_any_step: "CR (⋃i. any_step i)"
proof (intro dd_cr[OF wf_R' trans_R'], goal_cases peak)
have [dest!]: "(x, y) ∈ short_step⇧* ⟹ (x, y) ∈ (short_step⇧↔)⇧*" for x y
by (simp add: in_rtrancl_UnI)
have [simp]: "(x, y) ∈ (R⇧↔)⇧* ⟷ (y, x) ∈ (R⇧↔)⇧*" for x y R
by (metis rtrancl_converseI symcl_converse)
note [intro] = subsetD[OF rtrancl_mono, of "short_step⇧↔"]
have reflcl_refl: "(x, x) ∈ R⇧=" for x R by simp
case (peak a b s t u)
show ?case
proof ((cases a; cases b), goal_cases ll lr rl rr)
case (rr ι κ)
from peak tall_tall_peak[of s t ι u κ] obtain ι' κ' t' u' v where
*: "ι' ≤ ι" "κ' ≤ κ" "(t, t') ∈ tall_step_i κ'" "(t', v) ∈ short_step⇧*"
"(u, u') ∈ tall_step_i ι'" "(u', v) ∈ short_step⇧*"
unfolding rr any_step.simps by metis
then show ?case unfolding rr UN_Un under_Inr order.order_iff_strict
apply (elim disjE)
subgoal
apply (intro relcompI[of _ t _, OF _ relcompI[of _ t, OF _ relcompI[of _ u, OF _ relcompI[of _ u]]]] rtrancl_refl reflcl_refl)
apply (subst rtrancl_trans[of _ u', OF rtrancl_trans[of _ v, OF rtrancl_trans[of _ t']]])
by auto
subgoal
apply (intro relcompI[of _ t _, OF _ relcompI[of _ t', OF _ relcompI[of _ u, OF _ relcompI[of _ u]]]] rtrancl_refl reflcl_refl)
defer
apply (subst rtrancl_trans[of _ u', OF rtrancl_trans[of _ v]])
by auto
subgoal
apply (intro relcompI[of _ t _, OF _ relcompI[of _ t, OF _ relcompI[of _ u', OF _ relcompI[of _ u]]]] rtrancl_refl reflcl_refl)
apply (subst rtrancl_trans[of _ u', OF rtrancl_trans[of _ v, OF rtrancl_trans[of _ t']]])
by auto
subgoal
apply (intro relcompI[of _ t _, OF _ relcompI[of _ t', OF _ relcompI[of _ u', OF _ relcompI[of _ u]]]] rtrancl_refl reflcl_refl)
defer
apply (subst rtrancl_trans[of _ v])
by auto
done
next
case (rl ι s1)
from peak tall_short_peak[of s t ι u] obtain ι' ι'' t' u' v where
"ι' ≤ ι" "t = t' ∨ ι'' < ι ∧ (t, t') ∈ tall_step_i ι''" "(t', v) ∈ short_step⇧*"
"(u, u') ∈ tall_step_i ι'" "(u', v) ∈ short_step⇧*"
unfolding rl any_step.simps by (metis short_step_s_imp_short_step)
then show ?case unfolding rl UN_Un under_Inr order.order_iff_strict
apply (elim disjE[of "_ < _"])
subgoal
apply (intro relcompI[of _ t _, OF _ relcompI[of _ t, OF _ relcompI[of _ u, OF _ relcompI[of _ u]]]] rtrancl_refl reflcl_refl)
apply (subst rtrancl_trans[of _ u', OF rtrancl_trans[of _ v, OF rtrancl_trans[of _ t']]])
by auto
subgoal
apply (intro relcompI[of _ t _, OF _ relcompI[of _ t, OF _ relcompI[of _ u', OF _ relcompI[of _ u]]]] rtrancl_refl reflcl_refl)
apply (subst rtrancl_trans[of _ u', OF rtrancl_trans[of _ v, OF rtrancl_trans[of _ t']]])
by auto
done
next
case (lr s0 κ)
from peak tall_short_peak[of s u κ t] obtain κ' κ'' t' u' v where
"κ' ≤ κ" "u = u' ∨ κ'' < κ ∧ (u, u') ∈ tall_step_i κ''" "(u', v) ∈ short_step⇧*"
"(t, t') ∈ tall_step_i κ'" "(t', v) ∈ short_step⇧*"
unfolding lr any_step.simps by (metis short_step_s_imp_short_step)
then show ?case unfolding lr UN_Un under_Inr order.order_iff_strict
apply (elim disjE[of "_ < _"])
subgoal
apply (intro relcompI[of _ t _, OF _ relcompI[of _ t, OF _ relcompI[of _ u, OF _ relcompI[of _ u]]]] rtrancl_refl reflcl_refl)
apply (subst rtrancl_trans[of _ u', OF rtrancl_trans[of _ v, OF rtrancl_trans[of _ t']]])
by auto
subgoal
apply (intro relcompI[of _ t _, OF _ relcompI[of _ t', OF _ relcompI[of _ u, OF _ relcompI[of _ u]]]] rtrancl_refl reflcl_refl)
defer
apply (subst rtrancl_trans[of _ u', OF rtrancl_trans[of _ v]])
by auto
done
next
case (ll s0 s1)
from peak short_short_peak[of s t s0 u s1]
show ?case by (simp only: ll UN_Un under_Inl any_step.simps)
qed
qed
lemma tall_step_imp_rsteps:
"(s, t) ∈ tall_step ⟹ (s, t) ∈ (Restr (rstep' ℛ) native_terms)⇧*"
apply (elim tall_step.cases)
apply (subst base_decomp_fill_holes(2)[symmetric])
by (auto intro!: fill_holes_rsteps conjunct2[OF native_terms_rsteps] simp: base_decomp_fill_holes)
lemma short_step_imp_rsteps:
"(s, t) ∈ short_step ⟹ (s, t) ∈ (Restr (rstep' ℛ) native_terms)⇧*"
by (auto elim!: short_stepE intro!: conjunct2[OF native_terms_rsteps] dest: mirror_steps_imp_rsteps)
lemma any_step_short_tall:
"(⋃i. any_step i) = short_step ∪ tall_step"
by auto (metis short_step_iff_short_step_s tall_step_iff_tall_step_i any_step.simps sum.exhaust)+
lemma any_step_rsteps:
"short_step ∪ tall_step ⊆ (Restr (rstep' ℛ) native_terms)⇧*"
by (auto dest: short_step_imp_rsteps tall_step_imp_rsteps)
lemma rstep_any_step:
"Restr (rstep' ℛ) native_terms ⊆ short_step ∪ tall_step"
using single_step_to_any_step by blast
lemma CR_Suc_rk:
"CR_on (rstep' ℛ) native_terms"
by (auto intro!: CR_between_imp_CR[OF _ rstep_any_step any_step_rsteps]
CR_any_step[unfolded any_step_short_tall] iffD2[OF CR_on_iff_CR_Restr])
end
text ‹@{cite ‹Lemma 4.27› FMZvO15}›
lemma (in weakly_layered) CR_main_lemma:
assumes base: "CR_on (rstep' ℛ) {t. mctxt_of_term t ∈ 𝔏}"
and step: "⋀rk. CR_on (rstep' ℛ) {t ∈ 𝒯. rank t ≤ Suc rk} ⟹ weakly_layered_induct_dd ℱ 𝔏 ℛ rk (R rk)"
shows "CR_on (rstep' ℛ) 𝒯"
proof -
have "CR_on (rstep' ℛ) {t ∈ 𝒯. rank t ≤ Suc rk}" for rk
proof (induct rk)
case 0
have "t ∈ 𝒯 ∧ rank t ≤ Suc 0 ⟷ mctxt_of_term t ∈ 𝔏" for t
using rank_1[of t] rank_gt_0[of t] 𝔏_sig by (fastforce simp: 𝒞_def 𝒯_def)
then show ?case using base by simp
next
case (Suc rk)
then interpret weakly_layered_induct_dd ℱ 𝔏 ℛ rk "R rk" by (rule step)
show ?case using CR_Suc_rk by (simp only: native_terms_def)
qed
then show ?thesis by (auto simp: CR_on_def) (metis less_Suc_eq less_Suc_eq_le less_Suc_eq_le)
qed
end