section ‹Things that do not belong here›
theory LS_Extras
imports "$ISAFOR/Rewriting/Multihole_Context" "$ISAFOR/Auxiliaries/Renaming"
"$ISAFOR/Rewriting/Unification"
begin
subsection ‹Trivialities›
lemma pos_diff_cons [simp]: "pos_diff (i <# p) (i <# q) = pos_diff p q"
by (auto simp: pos_diff_def)
lemma max_list_append: "max_list (xs1 @ xs2) = max (max_list xs1) (max_list xs2)"
by (induct xs1) auto
lemma max_list_bound:
"max_list xs ≤ z ⟷ (∀i < length xs. xs ! i ≤ z)"
using less_Suc_eq_0_disj by (induct xs) auto
lemma max_list_mono_concat:
assumes "length xss = length yss" and "⋀i. i < length xss ⟹ max_list (xss ! i) ≤ max_list (yss ! i)"
shows "max_list (concat xss) ≤ max_list (concat yss)"
using assms
proof (induct yss arbitrary: xss)
case (Cons ys yss) thus ?case by (cases xss) (force simp: max_list_append)+
qed auto
lemma max_list_mono_concat1:
assumes "length xss = length ys" and "⋀i. i < length xss ⟹ max_list (xss ! i) ≤ ys ! i"
shows "max_list (concat xss) ≤ max_list ys"
using assms max_list_mono_concat[of xss "map (λy. [y]) ys"] by auto
lemma nth_equalityE:
"xs = ys ⟹ (length xs = length ys ⟹ (⋀i. i < length xs ⟹ xs ! i = ys ! i) ⟹ P) ⟹ P"
by simp
lemma finite_vars_mctxt [simp]: "finite (vars_mctxt C)"
by (induct C) auto
lemma partition_by_of_zip:
"length xs = sum_list zs ⟹ length ys = sum_list zs ⟹
partition_by (zip xs ys) zs = map (λ(x,y). zip x y) (zip (partition_by xs zs) (partition_by ys zs))"
by (induct zs arbitrary: xs ys) (auto simp: take_zip drop_zip)
lemma vars_term_fill_holes':
"num_holes C = length ts ⟹ vars_term (fill_holes C ts) = ⋃(vars_term ` set ts) ∪ vars_mctxt C"
proof (induct C ts rule: fill_holes_induct)
case (MFun f Cs ts) thus ?case
using UN_upt_len_conv[of "partition_holes ts Cs" "length Cs" "λt. (⋃x∈set t. vars_term x)"]
by (simp add: UN_Un_distrib UN_set_partition_by)
qed auto
lemma distinct_count_atmost_1':
"distinct xs = (∀a. count (mset xs) a ≤ 1)"
unfolding distinct_count_atmost_1 using dual_order.antisym by fastforce
lemma nth_subset_concat:
assumes "i < length xss"
shows "set (xss ! i) ⊆ set (concat xss)"
by (metis assms concat_nth concat_nth_length in_set_idx nth_mem subsetI)
lemma subst_domain_subst_of:
"subst_domain (subst_of xs) ⊆ set (map fst xs)"
proof (induct xs)
case (Cons x xs)
moreover have "subst_domain (subst (fst x) (snd x)) ⊆ set (map fst [x])" by simp
ultimately show ?case
using subst_domain_compose[of "subst_of xs" "subst (fst x) (snd x)"] by auto
qed simp
lemma subst_apply_mctxt_cong: "(∀x. x ∈ vars_mctxt C ⟶ σ x = τ x) ⟹ C ⋅mc σ = C ⋅mc τ"
by (induct C) auto
lemma distinct_concat_unique_index:
"distinct (concat xss) ⟹ i < length xss ⟹ x ∈ set (xss ! i) ⟹ j < length xss ⟹ x ∈ set (xss ! j) ⟹ i = j"
proof (induct xss rule: List.rev_induct)
case (snoc xs xss) thus ?case using nth_mem[of i xss] nth_mem[of j xss]
by (cases "i < length xss"; cases "j < length xss") (auto simp: nth_append simp del: nth_mem)
qed auto
lemma list_update_concat:
assumes "i < length xss" "j < length (xss ! i)"
shows "concat (xss[i := (xss ! i)[j := x]]) = concat xss[sum_list (take i (map length xss)) + j := x]"
using assms
proof (induct xss arbitrary: i)
case (Cons xs xss) thus ?case
by (cases i) (auto simp: list_update_append)
qed auto
lemma length_filter_sum_list:
"length (filter p xs) = sum_list (map (λx. if p x then 1 else 0) xs)"
by (induct xs) auto
lemma mctxt_of_term_var_subst:
"mctxt_of_term (t ⋅ (Var ∘ f)) = map_vars_mctxt f (mctxt_of_term t)"
by (induct t) auto
lemma map_vars_mctxt_mono:
"C ≤ D ⟹ map_vars_mctxt f C ≤ map_vars_mctxt f D"
by (induct C D rule: less_eq_mctxt_induct) (auto intro: less_eq_mctxtI1)
lemma map_vars_mctxt_less_eq_decomp:
assumes "C ≤ map_vars_mctxt f D"
obtains C' where "map_vars_mctxt f C' = C" "C' ≤ D"
using assms
proof (induct D arbitrary: C thesis)
case (MVar x) show ?case using MVar(1)[of MHole] MVar(1)[of "MVar _"] MVar(2)
by (auto elim: less_eq_mctxtE2 intro: less_eq_mctxtI1)
next
case MHole show ?case using MHole(1)[of MHole] MHole(2) by (auto elim: less_eq_mctxtE2)
next
case (MFun g Ds) note MFun' = MFun
show ?case using MFun(3) unfolding map_vars_mctxt.simps
proof (cases rule: less_eq_mctxtE2(3))
case MHole then show ?thesis using MFun(2)[of MHole] by auto
next
case (MFun Cs)
def Cs' ≡ "map (λi. SOME Ci'. map_vars_mctxt f Ci' = Cs ! i ∧ Ci' ≤ Ds ! i) [0..<length Cs]"
{ fix i assume "i < length Cs"
obtain Ci' where "map_vars_mctxt f Ci' = Cs ! i" "Ci' ≤ Ds ! i"
using `i < length Cs` MFun MFun'(1)[OF nth_mem, of i] MFun'(3) by (auto elim!: less_eq_mctxtE2)
then have "∃Ci'. map_vars_mctxt f Ci' = Cs ! i ∧ Ci' ≤ Ds ! i" by blast
}
from someI_ex[OF this] have
"length Cs = length Cs'" and "i < length Cs ⟹ map_vars_mctxt f (Cs' ! i) = Cs ! i"
"i < length Cs ⟹ Cs' ! i ≤ Ds ! i" for i by (auto simp: Cs'_def)
then show ?thesis using MFun(1,2) MFun'(3)
by (auto intro!: MFun'(2)[of "MFun g Cs'"] nth_equalityI less_eq_mctxtI2 elim!: less_eq_mctxtE2)
qed
qed
instance option :: (infinite) infinite
by standard (simp add: infinite_UNIV)
subsection ‹Imbalance›
definition refines :: "'a list ⇒ 'b list ⇒ bool" (infix "∝" 55) where
"refines ss ts ⟷ length ts = length ss ∧ (∀i j. i < length ss ∧ j < length ts ∧ ss ! i = ss ! j ⟶ ts ! i = ts ! j)"
lemma refines_refl:
"ss ∝ ss"
by (auto simp: refines_def)
lemma refines_trans:
"ss ∝ ts ⟹ ts ∝ us ⟹ ss ∝ us"
by (auto simp: refines_def)
definition imbalance :: "'a list ⇒ nat" where
"imbalance ts = card (set ts)"
lemma imbalance_def':
"imbalance xs = card { i. i < length xs ∧ (∀j. j < length xs ∧ xs ! i = xs ! j ⟶ i ≤ j) }"
proof (induct xs rule: List.rev_induct)
case (snoc x xs)
have "{ i. i < length (xs @ [x]) ∧ (∀j. j < length (xs @ [x]) ∧ (xs @ [x]) ! i = (xs @ [x]) ! j ⟶ i ≤ j) } =
{ i. i < length xs ∧ (∀j. j < length xs ∧ xs ! i = xs ! j ⟶ i ≤ j) } ∪ { i. i = length xs ∧ x ∉ set xs }"
by (simp add: set_eq_iff less_Suc_eq dnf imp_conjL nth_append)
(metis cancel_comm_monoid_add_class.diff_cancel in_set_conv_nth nth_Cons_0)
then show ?case using snoc by (simp add: imbalance_def card_insert_if)
qed (auto simp: imbalance_def)
lemma refines_imbalance_mono:
"ss ∝ ts ⟹ imbalance ss ≥ imbalance ts"
unfolding refines_def imbalance_def' by (intro card_mono) (simp_all add: Collect_mono)
lemma refines_imbalance_strict_mono:
"ss ∝ ts ⟹ ¬ ts ∝ ss ⟹ imbalance ss > imbalance ts"
unfolding refines_def imbalance_def'
proof (intro psubset_card_mono psubsetI, goal_cases)
case 3 obtain i j where ij: "i < length ss" "j < length ss" "ts ! i = ts ! j" "ss ! i ≠ ss ! j"
using conjunct1[OF 3(1)] 3(2) by auto
def f ≡ "λi. SOME j. j < length ss ∧ ss ! j = ss ! i ∧ (∀i. ss ! j = ss ! i ⟶ j ≤ i)"
let ?ssi = "{i. i < length ss ∧ (∀j. j < length ss ∧ ss ! i = ss ! j ⟶ i ≤ j)}"
let ?tsi = "{i. i < length ts ∧ (∀j. j < length ts ∧ ts ! i = ts ! j ⟶ i ≤ j)}"
note f_def = fun_cong[OF f_def[unfolded atomize_eq]]
{ fix i assume "i < length ss"
then have "∃i'. i' < length ss ∧ ss ! i' = ss ! i ∧ (∀i. ss ! i' = ss ! i ⟶ i' ≤ i)"
proof (induct i rule: less_induct)
case (less i) then show ?case
by (cases "i < length ss ∧ ss ! i = ss ! i ∧ (∀j. ss ! i = ss ! j ⟶ i ≤ j)") auto
qed
then have "f i < length ss" "ss ! f i = ss ! i" "⋀j. ss ! f i = ss ! j ⟹ f i ≤ j"
using someI[of "λj. j < length ss ∧ ss ! j = ss ! i ∧ (∀i. ss ! j = ss ! i ⟶ j ≤ i)", folded f_def]
by auto
then have "f i < length ss" "ss ! f i = ss ! i" "f i ∈ ?ssi" "f i ∈ ?tsi ⟹ ts ! f i = ts ! i"
using 3(1) by (auto simp: `i < length ss`)
} note * = this[OF ij(1)] this[OF ij(2)]
with ij(1,2,3,4) 3(1)[THEN conjunct1]
3(1)[THEN conjunct2, rule_format, of i "f i"]
3(1)[THEN conjunct2, rule_format, of j "f j"]
have "f i ∈ ?ssi" "f j ∈ ?ssi" "ts ! f i = ts ! f j" "f i ≠ f j" by metis+
moreover from this(3,4) have "f i ∉ ?tsi ∨ f j ∉ ?tsi" using *(4,8) ij(3)
by (metis (mono_tags, lifting) dual_order.antisym mem_Collect_eq)
ultimately show ?case by argo
qed (simp_all add: Collect_mono)
lemma refines_take:
"ss ∝ ts ⟹ take n ss ∝ take n ts"
unfolding refines_def by (intro conjI impI allI; elim conjE) (simp_all add: refines_def)
lemma refines_drop:
"ss ∝ ts ⟹ drop n ss ∝ drop n ts"
unfolding refines_def
proof ((intro conjI impI allI; elim conjE), goal_cases)
case (2 i j) show ?case using 2(1,3-) 2(2)[rule_format, of "i + n" "j + n"]
by (auto simp: less_diff_eq less_diff_conv ac_simps)
qed simp
subsection ‹Abstract Rewriting›
lemma join_finite:
assumes "CR R" "finite X" "⋀x y. x ∈ X ⟹ y ∈ X ⟹ (x, y) ∈ R⇧↔⇧*"
obtains z where "⋀x. x ∈ X ⟹ (x, z) ∈ R⇧*"
using assms(2,1,3)
proof (induct X arbitrary: thesis)
case (insert x X)
then show ?case
proof (cases "X = {}")
case False
then obtain x' where "x' ∈ X" by auto
obtain z where *: "x' ∈ X ⟹ (x', z) ∈ R⇧*" for x' using insert by (metis insert_iff)
from this[of x'] `x' ∈ X` insert(6)[of x x'] have "(x, z) ∈ R⇧↔⇧*"
by (metis insert_iff converse_rtrancl_into_rtrancl conversionI' conversion_rtrancl)
with `CR R` obtain z' where "(x, z') ∈ R⇧*" "(z, z') ∈ R⇧*" by (auto simp: CR_iff_conversion_imp_join)
then show ?thesis by (auto intro!: insert(4)[of z'] dest: *)
qed auto
qed simp
lemma balance_sequence:
assumes "CR R"
obtains (ts) ts where "length ss = length ts"
"⋀i. i < length ss ⟹ (ss ! i, ts ! i) ∈ R⇧*"
"⋀i j. i < length ss ⟹ j < length ss ⟹ (ss ! i, ss ! j) ∈ R⇧↔⇧* ⟹ ts ! i = ts ! j"
proof -
define f where "f s ≡ SOME u. ∀t ∈ { t ∈ set ss. (s, t) ∈ R⇧↔⇧* }. (t, u) ∈ R⇧* " for s
{ fix i assume "i < length ss"
have "∀t ∈ { t ∈ set ss. (ss ! i, t) ∈ R⇧↔⇧* }. (t, f (ss ! i)) ∈ R⇧*"
unfolding f_def using join_finite[OF `CR R`, of "{ t ∈ set ss. (ss ! i, t) ∈ R⇧↔⇧* }"]
by (rule someI_ex) (auto, metis conversion_inv conversion_rtrancl rtrancl_trans)
with `i < length ss` have "(ss ! i, f (ss ! i)) ∈ R⇧*" by auto
} note [intro] = this
moreover {
fix i j assume "i < length ss" "j < length ss" "(ss ! i, ss ! j) ∈ R⇧↔⇧*"
then have "{ t ∈ set ss. (ss ! i, t) ∈ R⇧↔⇧* } = { t ∈ set ss. (ss ! j, t) ∈ R⇧↔⇧* }"
by auto (metis conversion_inv conversion_rtrancl rtrancl_trans)+
then have "f (ss ! i) = f (ss ! j)" by (auto simp: f_def)
} note [intro] = this
show ?thesis by (auto intro!: ts[of "map f ss"])
qed
lemma balance_sequences:
assumes "CR R" and [simp]: "length ts = length ss" "length us = length ss" and
p: "⋀i. i < length ss ⟹ (ss ! i, ts ! i) ∈ R⇧*" "⋀i. i < length ss ⟹ (ss ! i, us ! i) ∈ R⇧*"
obtains (vs) vs where
"length vs = length ss"
"⋀i. i < length ss ⟹ (ts ! i, vs ! i) ∈ R⇧*" "⋀i. i < length ss ⟹ (us ! i, vs ! i) ∈ R⇧*"
"refines ts vs" "refines us vs"
proof -
from balance_sequence[OF `CR R`, of "ts @ us"]
obtain vs where l: "length (ts @ us) = length vs" and
r: "⋀i. i < length (ts @ us) ⟹ ((ts @ us) ! i, vs ! i) ∈ R⇧*" and
e: "⋀i j. i < length (ts @ us) ⟹ j < length (ts @ us) ⟹ ((ts @ us) ! i, (ts @ us) ! j) ∈ R⇧↔⇧* ⟹ vs ! i = vs ! j"
by blast
{ fix i assume *: "i < length ss"
from * have "(ts ! i, us ! i) ∈ R⇧↔⇧*" using p[of i]
by (metis CR_imp_conversionIff_join assms(1) conversionI' conversion_rtrancl joinI_right rtrancl_trans)
with * have "vs ! (length ss + i) = vs ! i"
using e[of i "length ss + i"] by (auto simp: nth_append)
} note lp[simp] = this
show ?thesis
proof (intro vs[of "take (length ss) vs"], goal_cases)
case (2 i) then show ?case using l r[of i] by (auto simp: nth_append)
next
case (3 i) with 3 show ?case using l r[of "length ss + i"] by (auto simp: nth_append)
next
case 4
then show ?case using l by (auto simp: refines_def nth_append intro!: e)
next
case 5
{ fix i j assume "i < length ss" "j < length ss" "(us ! i, us ! j) ∈ R⇧↔⇧*"
then have "vs ! i = vs ! j"
using e[of "length ss + i" "length ss + j"] by (simp add: nth_append)
}
then show ?case using l by (auto simp: refines_def nth_append)
qed (auto simp: l[symmetric])
qed
lemma CR_on_iff_CR_Restr:
assumes "⋀x y. x ∈ A ⟹ (x, y) ∈ R ⟹ y ∈ A"
shows "CR_on R A ⟷ CR (Restr R A)"
proof ((standard; standard), goal_cases)
let ?R' = "Restr R A"
{ fix s t assume "(s, t) ∈ R⇧*" "s ∈ A"
then have "(s, t) ∈ ?R'⇧* ∧ t ∈ A"
proof (induct t rule: rtrancl_induct)
case (step t u)
then show ?case by (auto intro!: rtrancl_into_rtrancl[of _ t _ u] dest: assms)
qed auto
} note * = this
{
case (1 s t u)
then show ?case
proof (cases "s ∈ A")
case True
with 1(3,4) have "(s, t) ∈ R⇧*" "t ∈ A" "(s, u) ∈ R⇧*" "u ∈ A"
using *[of s t] *[of s u] rtrancl_mono[of ?R' R] by auto
then show ?thesis
using True 1(1)[unfolded CR_on_def, rule_format, of s t u] by (auto dest!: joinD *)
next
case False
then have "s = t" "s = u" using 1 by (metis IntD2 converse_rtranclE mem_Sigma_iff)+
then show ?thesis by auto
qed
next
case (2 s t u)
obtain v where "(t, v) ∈ ?R'⇧*" "(u, v) ∈ ?R'⇧*" using *[OF 2(3,2)] *[OF 2(4,2)] 2(1) by auto
then show ?case using rtrancl_mono[of ?R' R] by auto
}
qed
subsection ‹Bijection between 'a and 'a option for infinite types›
lemma infinite_option_bijection:
assumes "infinite (UNIV :: 'a set)" shows "∃f :: 'a ⇒ 'a option. bij f"
proof -
from infinite_countable_subset[OF assms] obtain g :: "nat ⇒ 'a" where g: "inj g" "range g ⊆ UNIV" by blast
let ?f = "λx. if x ∈ range g then (case inv g x of 0 ⇒ None | Suc n ⇒ Some (g n)) else Some x"
have "?f x = ?f y ⟹ x = y" for x y using g(1) by (auto split: nat.splits if_splits simp: inj_on_def) auto
moreover have "∃x. ?f x = y" for y
apply (cases y)
subgoal using g(1) by (intro exI[of _ "g 0"]) auto
subgoal for y using g
apply (cases "y ∈ range g")
subgoal by (intro exI[of _ "g (Suc (inv g y))"]) auto
subgoal by auto
done
done
ultimately have "bij ?f" unfolding bij_def surj_def by (intro conjI injI) metis+
thus ?thesis by blast
qed
definition to_option :: "'a :: infinite ⇒ 'a option" where
"to_option = (SOME f. bij f)"
definition from_option :: "'a :: infinite option ⇒ 'a" where
"from_option = inv to_option"
lemma bij_from_option: "bij to_option"
unfolding to_option_def using someI_ex[OF infinite_option_bijection[OF infinite_UNIV]] .
lemma from_to_option_comp[simp]: "from_option o to_option = id"
unfolding from_option_def by (intro inv_o_cancel bij_is_inj bij_from_option)
lemma from_to_option[simp]: "from_option (to_option x) = x"
by (simp add: pointfree_idE)
lemma to_from_option_comp[simp]: "to_option o from_option = id"
unfolding from_option_def surj_iff[symmetric] by (intro bij_is_surj bij_from_option)
lemma to_from_option[simp]: "to_option (from_option x) = x"
by (simp add: pointfree_idE)
lemma var_subst_comp: "t ⋅ (Var o f) ⋅ g = t ⋅ (g o f)"
by (simp add: comp_def subst_subst_compose[symmetric]
subst_compose_def del: subst_subst_compose)
subsection ‹More polymorphic rewriting›
inductive_set rstep' :: "('f, 'v) trs ⇒ ('f, 'w) term rel" for R where
rstep' [intro]: "(l, r) ∈ R ⟹ (C⟨l ⋅ σ⟩, C⟨r ⋅ σ⟩) ∈ rstep' R"
lemma rstep_eq_rstep': "rstep R = rstep' R"
by (auto elim: rstep'.cases)
lemma rstep'_mono:
assumes "(s, t) ∈ rstep' R" shows "(C⟨s⟩, C⟨t⟩) ∈ rstep' R"
proof -
from assms obtain D l r σ where "(l, r) ∈ R" "s = D⟨l ⋅ σ⟩" "t = D⟨r ⋅ σ⟩" by (auto simp add: rstep'.simps)
then show ?thesis using rstep'[of l r R "C ∘⇩c D" σ] by simp
qed
lemma rstep'_stable:
assumes "(s, t) ∈ rstep' R" shows "(s ⋅ σ, t ⋅ σ) ∈ rstep' R"
proof -
from assms obtain C l r τ where "(l, r) ∈ R" "s = C⟨l ⋅ τ⟩" "t = C⟨r ⋅ τ⟩" by (auto simp add: rstep'.simps)
then show ?thesis using rstep'[of l r R "C ⋅⇩c σ" "τ ∘⇩s σ"] by simp
qed
inductive_set rstep_r_p_s' :: "('f, 'v) trs ⇒ ('f, 'v) rule ⇒ pos ⇒ ('f, 'v, 'w) gsubst ⇒ ('f, 'w) term rel"
for R r p σ where
rstep_r_p_s' [intro]: "r ∈ R ⟹ p = hole_pos C ⟹ (C⟨fst r ⋅ σ⟩, C⟨snd r ⋅ σ⟩) ∈ rstep_r_p_s' R r p σ"
declare rstep_r_p_s'.cases [elim]
lemma rstep_r_p_s'I:
"r ∈ R ⟹ p = hole_pos C ⟹ s = C⟨fst r ⋅ σ⟩ ⟹ t = C⟨snd r ⋅ σ⟩ ⟹ (s, t) ∈ rstep_r_p_s' R r p σ"
by auto
lemma rstep_r_p_s'E:
assumes "(s, t) ∈ rstep_r_p_s' R r p σ"
obtains C where "r ∈ R" "p = hole_pos C" "s = C⟨fst r ⋅ σ⟩" "t = C⟨snd r ⋅ σ⟩"
using rstep_r_p_s'.cases assms by metis
lemma rstep_r_p_s_eq_rstep_r_p_s': "rstep_r_p_s R r p σ = rstep_r_p_s' R r p σ"
by (auto simp: rstep_r_p_s_def rstep_r_p_s'.simps) (metis hole_pos_ctxt_of_pos_term)
lemma rstep'_iff_rstep_r_p_s':
"(s, t) ∈ rstep' R ⟷ (∃l r p σ. (s, t) ∈ rstep_r_p_s' R (l, r) p σ)"
by (auto simp: rstep'.simps rstep_r_p_s'.simps)
lemma rstep_r_p_s'_deterministic:
assumes "wf_trs R" "(s, t) ∈ rstep_r_p_s' R r p σ" "(s, t') ∈ rstep_r_p_s' R r p τ"
shows "t = t'"
proof -
obtain C where 1: "r ∈ R" "s = C⟨fst r ⋅ σ⟩" "t = C⟨snd r ⋅ σ⟩" "p = hole_pos C"
using assms(2) by (auto simp: rstep_r_p_s'.simps)
obtain D where 2: "s = D⟨fst r ⋅ τ⟩" "t' = D⟨snd r ⋅ τ⟩" "p = hole_pos D"
using assms(3) by (auto simp: rstep_r_p_s'.simps)
obtain lhs rhs where 3: "r = (lhs, rhs)" by force
show ?thesis using 1(1) 2(1,3) unfolding 1(2,3,4) 2(2) 3
proof (induct C arbitrary: D)
case Hole have [simp]: "D = □" using Hole by (cases D) auto
thus ?case using `wf_trs R` Hole by (auto simp: wf_trs_def term_subst_eq_conv)
next
case (More f ss1 C' ss2) thus ?case by (cases D) auto
qed
qed
lemma rstep_r_p_s'_preserves_funas_terms:
assumes "wf_trs R" "(s, t) ∈ rstep_r_p_s' R r p σ" "funas_trs R ⊆ F" "funas_term s ⊆ F"
shows "funas_term t ⊆ F"
proof -
obtain C where 1: "r ∈ R" "s = C⟨fst r ⋅ σ⟩" "t = C⟨snd r ⋅ σ⟩" "p = hole_pos C"
using assms(2) by (auto simp: rstep_r_p_s'.simps)
then have "funas_ctxt C ⊆ F" using assms(4) by auto
obtain lhs rhs where 3: "r = (lhs, rhs)" by force
show ?thesis using 1(1) using assms(1,3,4)
by (force simp: 1(2,3,4) 3 funas_term_subst funas_trs_def funas_rule_def wf_trs_def)
qed
lemma rstep'_preserves_funas_terms:
"funas_trs R ⊆ F ⟹ funas_term s ⊆ F ⟹ (s, t) ∈ rstep' R ⟹ wf_trs R ⟹ funas_term t ⊆ F"
unfolding rstep'_iff_rstep_r_p_s' using rstep_r_p_s'_preserves_funas_terms by blast
lemma rstep_r_p_s'_stable:
"(s, t) ∈ rstep_r_p_s' R r p σ ⟹ (s ⋅ τ, t ⋅ τ) ∈ rstep_r_p_s' R r p (σ ∘⇩s τ)"
by (auto elim!: rstep_r_p_s'E intro!: rstep_r_p_s'I simp: subst_subst simp del: subst_subst_compose)
lemma rstep_r_p_s'_mono:
"(s, t) ∈ rstep_r_p_s' R r p σ ⟹ (C⟨s⟩, C⟨t⟩) ∈ rstep_r_p_s' R r (hole_pos C <#> p) σ"
proof (elim rstep_r_p_s'E)
fix D assume "r ∈ R" "p = hole_pos D" "s = D⟨fst r ⋅ σ⟩" "t = D⟨snd r ⋅ σ⟩"
then show "(C⟨s⟩, C⟨t⟩) ∈ rstep_r_p_s' R r (hole_pos C <#> p) σ"
using rstep_r_p_s'I[of r R "hole_pos C <#> p" "C ∘⇩c D" "C⟨s⟩" σ "C⟨t⟩"] by simp
qed
lemma rstep_r_p_s'_argE:
assumes "(s, t) ∈ rstep_r_p_s' R (l, r) (i <# p) σ"
obtains f ss ti where "s = Fun f ss" "i < length ss" "t = Fun f (ss[i := ti])" "(ss ! i, ti) ∈ rstep_r_p_s' R (l, r) p σ"
proof -
thm upd_conv_take_nth_drop
from assms obtain C where *: "hole_pos C = i <# p" "s = C⟨l ⋅ σ⟩" "t = C⟨r ⋅ σ⟩" "(l, r) ∈ R" by (auto elim: rstep_r_p_s'E)
then obtain f ls D rs where [simp]: "C = More f ls D rs" "i = length ls" by (cases C) auto
let ?ss = "ls @ D⟨l ⋅ σ⟩ # rs" and ?ts = "ls @ D⟨r ⋅ σ⟩ # rs" and ?ti = "D⟨r ⋅ σ⟩"
have "s = Fun f ?ss" "i < length ?ss" "t = Fun f (list_update ?ss i ?ti)" using * by simp_all
moreover have "(?ss ! i, ?ti) ∈ rstep_r_p_s' R (l, r) p σ" using * by (auto intro: rstep_r_p_s'I)
ultimately show ?thesis ..
qed
lemma rstep_r_p_s'_argI:
assumes "i < length ss" "(ss ! i, ti) ∈ rstep_r_p_s' R r p σ"
shows "(Fun f ss, Fun f (ss[i := ti])) ∈ rstep_r_p_s' R r (i <# p) σ"
using assms(1) rstep_r_p_s'_mono[OF assms(2), of "More f (take i ss) Hole (drop (Suc i) ss)"]
by (auto simp: id_take_nth_drop[symmetric] upd_conv_take_nth_drop min_def)
lemma wf_trs_implies_funposs:
assumes "wf_trs R" "(s, t) ∈ rstep_r_p_s' R (l, r) p σ"
shows "p ∈ funposs s"
proof -
obtain C where *: "(l, r) ∈ R" "s = C⟨l ⋅ σ⟩" "p = hole_pos C" using assms by auto
then show ?thesis
using assms hole_pos_in_filled_funposs[of "l ⋅ σ" C Var] by (force simp: wf_trs_def')
qed
lemma NF_Var':
assumes "wf_trs R"
shows "(Var x, t) ∉ rstep' R"
unfolding rstep'_iff_rstep_r_p_s' by (auto dest: wf_trs_implies_funposs[OF assms])
subsection ‹All positions of a multi-hole context›
fun all_poss_mctxt :: "('f, 'v) mctxt ⇒ pos set"
where
"all_poss_mctxt (MVar x) = {ε}"
| "all_poss_mctxt MHole = {ε}"
| "all_poss_mctxt (MFun f cs) = {ε} ∪ ⋃(set (map (λ i. (λ p. i <# p) ` all_poss_mctxt (cs ! i)) [0 ..< length cs]))"
lemma all_poss_mctxt_simp [simp]:
"all_poss_mctxt (MFun f cs) = {ε} ∪ {i <# p | i p. i < length cs ∧ p ∈ all_poss_mctxt (cs ! i)}"
by auto
declare all_poss_mctxt.simps(3)[simp del]
lemma all_poss_mctxt_conv:
"all_poss_mctxt C = poss_mctxt C ∪ hole_poss C"
by (induct C) auto
lemma root_in_all_poss_mctxt[simp]:
"ε ∈ all_poss_mctxt C"
by (cases C) auto
lemma hole_poss_mctxt_of_term[simp]:
"hole_poss (mctxt_of_term t) = {}"
by (induct t) auto
lemma poss_mctxt_mctxt_of_term[simp]:
"poss_mctxt (mctxt_of_term t) = poss t"
by (induct t) auto
lemma all_poss_mctxt_mctxt_of_term[simp]:
"all_poss_mctxt (mctxt_of_term t) = poss t"
by (induct t) auto
lemma mctxt_of_term_leq_imp_eq:
"mctxt_of_term t ≤ C ⟷ mctxt_of_term t = C"
by (induct t arbitrary: C) (auto elim!: less_eq_mctxtE1 simp: map_nth_eq_conv)
subsection ‹More operations on multi-hole contexts›
fun root_mctxt :: "('f, 'v) mctxt ⇒ ('f × nat) option" where
"root_mctxt MHole = None"
| "root_mctxt (MVar x) = None"
| "root_mctxt (MFun f Cs) = Some (f, length Cs)"
fun mreplace_at :: "('f, 'v) mctxt ⇒ pos ⇒ ('f, 'v) mctxt ⇒ ('f, 'v) mctxt" where
"mreplace_at C ε D = D"
| "mreplace_at (MFun f Cs) (i <# p) D = MFun f (take i Cs @ mreplace_at (Cs ! i) p D # drop (i+1) Cs)"
fun subm_at :: "('f, 'v) mctxt ⇒ pos ⇒ ('f, 'v) mctxt" where
"subm_at C ε = C"
| "subm_at (MFun f Cs) (i <# p) = subm_at (Cs ! i) p"
lemma subm_at_hole_poss[simp]:
"p ∈ hole_poss C ⟹ subm_at C p = MHole"
by (induct C arbitrary: p) auto
lemma subm_at_mctxt_of_term:
"p ∈ poss t ⟹ subm_at (mctxt_of_term t) p = mctxt_of_term (subt_at t p)"
by (induct t arbitrary: p) auto
lemma subm_at_mreplace_at[simp]:
"p ∈ all_poss_mctxt C ⟹ subm_at (mreplace_at C p D) p = D"
by (induct C arbitrary: p) (auto simp: nth_append_take)
lemma replace_at_subm_at[simp]:
"p ∈ all_poss_mctxt C ⟹ mreplace_at C p (subm_at C p) = C"
by (induct C arbitrary: p) (auto simp: id_take_nth_drop[symmetric])
lemma all_poss_mctxt_mreplace_atI1:
"p ∈ all_poss_mctxt C ⟹ q ∈ all_poss_mctxt C ⟹ ¬(q > p) ⟹ q ∈ all_poss_mctxt (mreplace_at C p D)"
apply (induct C arbitrary: p q)
apply (auto simp: nth_append_take less_pos_def nth_append_drop_is_nth_conv nth_append_take_drop_is_nth_conv)
apply linarith
apply linarith
apply (case_tac "ia = i", auto simp add: nth_append_take nth_append_take_drop_is_nth_conv)
done
lemma funas_mctxt_mreplace_at:
assumes "p ∈ all_poss_mctxt C"
shows "funas_mctxt (mreplace_at C p D) ⊆ funas_mctxt C ∪ funas_mctxt D"
using assms
proof (induct C p D rule: mreplace_at.induct)
case (2 f Cs i p D) then have Cs: "Cs = take i Cs @ Cs ! i # drop (Suc i) Cs"
by (auto simp: id_take_nth_drop)
show ?case using 2 by (subst (2) Cs) auto
qed auto
lemma funas_mctxt_mreplace_at_hole:
assumes "p ∈ hole_poss C"
shows "funas_mctxt (mreplace_at C p D) = funas_mctxt C ∪ funas_mctxt D" (is "?L = ?R")
proof
show "?R ⊆ ?L" using assms
proof (induct C p D rule: mreplace_at.induct)
case (1 C D) thus ?case by (cases C) auto
next
case (2 f Cs i p D) then have Cs: "Cs = take i Cs @ Cs ! i # drop (Suc i) Cs"
by (auto simp: id_take_nth_drop)
show ?case using 2 by (subst (1) Cs) auto
qed auto
next
show "?L ⊆ ?R" using assms by (auto simp: all_poss_mctxt_conv funas_mctxt_mreplace_at)
qed
fun mctxt_term_conv :: "('f, 'v) mctxt ⇒ ('f, 'v option) term" where
"mctxt_term_conv MHole = Var None"
| "mctxt_term_conv (MVar v) = Var (Some v)"
| "mctxt_term_conv (MFun f Cs) = Fun f (map mctxt_term_conv Cs)"
fun term_mctxt_conv :: "('f, 'v option) term ⇒ ('f, 'v) mctxt" where
"term_mctxt_conv (Var None) = MHole"
| "term_mctxt_conv (Var (Some v)) = MVar v"
| "term_mctxt_conv (Fun f ts) = MFun f (map term_mctxt_conv ts)"
lemma mctxt_term_conv_inv [simp]: "mctxt_term_conv (term_mctxt_conv t) = t"
by (induct t rule: term_mctxt_conv.induct) (auto simp: map_idI)
lemma term_mctxt_conv_inv [simp]: "term_mctxt_conv (mctxt_term_conv t) = t"
by (induct t rule: mctxt_term_conv.induct) (auto simp: map_idI)
lemma mctxt_term_conv_bij: "bij mctxt_term_conv"
by (auto intro!: o_bij[of term_mctxt_conv mctxt_term_conv])
lemma term_mctxt_conv_bij: "bij term_mctxt_conv"
by (auto intro!: o_bij[of mctxt_term_conv term_mctxt_conv])
lemma mctxt_term_conv_mctxt_of_term[simp]: "mctxt_term_conv (mctxt_of_term t) = t ⋅ (Var ∘ Some)"
by (induct t) auto
definition term_of_mctxt_subst where "term_of_mctxt_subst = case_option (term_of_mctxt MHole) Var"
lemma term_of_mctxt_to_mctxt_term_conv:
"term_of_mctxt C = mctxt_term_conv C ⋅ term_of_mctxt_subst"
by (induct C) (auto simp: term_of_mctxt_subst_def)
lemma poss_mctxt_term_conv[simp]:
"poss (mctxt_term_conv C) = all_poss_mctxt C"
by (induct C) auto
lemma funas_term_mctxt_term_conv[simp]:
"funas_term (mctxt_term_conv C) = funas_mctxt C"
by (induct C) auto
lemma all_poss_mctxt_term_mctxt_conv[simp]:
"all_poss_mctxt (term_mctxt_conv t) = poss t"
by (induct t rule: term_mctxt_conv.induct) auto
lemma funas_mctxt_term_mctxt_conv[simp]:
"funas_mctxt (term_mctxt_conv t) = funas_term t"
by (induct t rule: term_mctxt_conv.induct) auto
lemma subm_at_term_mctxt_conv:
"p ∈ poss t ⟹ subm_at (term_mctxt_conv t) p = term_mctxt_conv (subt_at t p)"
by (induct t p rule: subt_at.induct) auto
lemma subt_at_mctxt_term_conv:
"p ∈ all_poss_mctxt C ⟹ subt_at (mctxt_term_conv C) p = mctxt_term_conv (subm_at C p)"
by (induct C p rule: subm_at.induct) auto
lemma subm_at_subt_at_conv:
"p ∈ all_poss_mctxt C ⟹ subm_at C p = term_mctxt_conv (subt_at (mctxt_term_conv C) p)"
by (induct C p rule: subm_at.induct) auto
lemma mctxt_term_conv_fill_holes_mctxt:
assumes "num_holes C = length Cs"
shows "mctxt_term_conv (fill_holes_mctxt C Cs) = fill_holes (map_vars_mctxt Some C) (map mctxt_term_conv Cs)"
using assms by (induct C Cs rule: fill_holes_induct) (auto simp: comp_def)
lemma map_vars_mctxt_fill_holes_mctxt:
assumes "num_holes C = length Cs"
shows "map_vars_mctxt f (fill_holes_mctxt C Cs) = fill_holes_mctxt (map_vars_mctxt f C) (map (map_vars_mctxt f) Cs)"
using assms by (induct C Cs rule: fill_holes_induct) (auto simp: comp_def)
lemma mctxt_term_conv_map_vars_mctxt_subst:
shows "mctxt_term_conv (map_vars_mctxt f C) = mctxt_term_conv C ⋅ (Var o map_option f)"
by (induct C) auto
lemma map_vars_mctxt_map_vars_mctxt[simp]:
shows "map_vars_mctxt f (map_vars_mctxt g C) = map_vars_mctxt (f o g) C"
by (induct C) auto
lemma funas_mctxt_fill_holes_mctxt:
assumes "num_holes C = length ts"
shows "funas_term (fill_holes C ts) = funas_mctxt C ∪ ⋃(set (map funas_term ts))"
using funas_term_fill_holes_iff[OF assms] by auto
inductive_set mrstep :: "('f, 'w) trs ⇒ ('f, 'v) mctxt rel" for R where
mrstep [intro]: "(mctxt_term_conv C, mctxt_term_conv D) ∈ rstep' R ⟹ (C, D) ∈ mrstep R"
lemma mrstepD: "(C, D) ∈ mrstep R ⟹ (mctxt_term_conv C, mctxt_term_conv D) ∈ rstep' R"
by (rule mrstep.induct)
lemma mrstepI_inf:
assumes "(mctxt_term_conv C ⋅ (Var o from_option), mctxt_term_conv D ⋅ (Var o from_option)) ∈ rstep R"
shows "(C, D) ∈ mrstep R"
using rstep'_stable[OF assms[unfolded rstep_eq_rstep'], of "Var o to_option"]
by (intro mrstep.intros) (auto simp del: subst_subst_compose simp: subst_subst subst_compose_def)
lemma mrstepD_inf:
"(C, D) ∈ mrstep R ⟹ (mctxt_term_conv C ⋅ (Var o from_option), mctxt_term_conv D ⋅ (Var o from_option)) ∈ rstep R"
by (metis rstep'_stable mrstepD rstep_eq_rstep')
lemma NF_MVar_MHole:
assumes "wf_trs R" and "C = MVar x ∨ C = MHole"
shows "(C, D) ∉ mrstep R"
using NF_Var'[OF assms(1)] assms(2) by (force dest: mrstepD)
lemma mctxt_neq_mholeE:
"x ≠ MHole ⟹ (⋀v. x = MVar v ⟹ P) ⟹ (⋀f Cs. x = MFun f Cs ⟹ P) ⟹ P"
by (cases x) auto
lemma leq_mholeE:
"C ≤ MHole ⟹ (C = MHole ⟹ P) ⟹ P"
by (cases C) (auto simp: less_eq_mctxt_def)
lemma leq_mvarE:
"C ≤ MVar v ⟹ (C = MHole ⟹ P) ⟹ (C = MVar v ⟹ P) ⟹ P"
by (cases C) (auto simp: less_eq_mctxt_def split_ifs)
lemma leq_mfunE:
"C ≤ MFun f Ds ⟹ (C = MHole ⟹ P) ⟹
(⋀Cs. C = MFun f Cs ⟹ length Cs = length Ds ⟹ (⋀i. i < length Ds ⟹ Cs ! i ≤ Ds ! i) ⟹ P) ⟹ P"
by (cases C) (auto simp: less_eq_mctxt_def split_ifs list_eq_iff_nth_eq)
lemma prefix_comp_mctxt: "C ≤ E ⟹ D ≤ E ⟹ (C, D) ∈ comp_mctxt"
proof (induct E arbitrary: C D)
case (MFun f Es C D)
then show ?case
proof (elim leq_mfunE)
fix Cs Ds
assume C: "C = MFun f Cs" and D: "D = MFun f Ds"
and lC: "length Cs = length Es" and lD: "length Ds = length Es"
and Ci: "⋀i. i < length Es ⟹ Cs ! i ≤ Es ! i" and Di: "⋀i. i < length Es ⟹ Ds ! i ≤ Es ! i"
and IH: "⋀E' C' D'. E' ∈ set Es ⟹ C' ≤ E' ⟹ D' ≤ E' ⟹ (C', D') ∈ comp_mctxt"
show "(C, D) ∈ comp_mctxt"
by (auto simp: C D lC lD intro!: comp_mctxt.intros IH[OF _ Ci Di])
qed (auto intro: comp_mctxt.intros)
qed (auto elim: leq_mholeE leq_mvarE intro: comp_mctxt.intros)
lemma less_eq_mctxt_sup_conv1:
"(C, D) ∈ comp_mctxt ⟹ C ≤ D ⟷ C ⊔ D = D"
by (induct C D rule: comp_mctxt.induct) (auto elim!: less_eq_mctxtE2 nth_equalityE intro: nth_equalityI less_eq_mctxtI2(3))
lemma less_eq_mctxt_sup_conv2:
"(C, D) ∈ comp_mctxt ⟹ D ≤ C ⟷ C ⊔ D = C"
using less_eq_mctxt_sup_conv1[OF comp_mctxt_sym] by (auto simp: ac_simps)
lemma comp_mctxt_mctxt_of_term1[dest!]:
"(C, mctxt_of_term t) ∈ comp_mctxt ⟹ C ≤ mctxt_of_term t"
by (induct C "mctxt_of_term t" arbitrary: t rule: comp_mctxt.induct; case_tac t) (auto intro: less_eq_mctxtI2)
lemmas comp_mctxt_mctxt_of_term2[dest!] = comp_mctxt_mctxt_of_term1[OF comp_mctxt_sym]
lemma mfun_leq_mfunI:
"f = g ⟹ length Cs = length Ds ⟹ (⋀i. i < length Ds ⟹ Cs ! i ≤ Ds ! i) ⟹ MFun f Cs ≤ MFun g Ds"
by (auto simp: less_eq_mctxt_def list_eq_iff_nth_eq)
lemma prefix_mctxt_sup:
assumes "C ≤ (E :: ('f, 'v) mctxt)" "D ≤ E" shows "C ⊔ D ≤ E"
using assms
by (induct E arbitrary: C D) (auto elim!: leq_mholeE leq_mvarE leq_mfunE intro!: mfun_leq_mfunI)
lemma mreplace_at_leqI:
"p ∈ all_poss_mctxt C ⟹ C ≤ E ⟹ D ≤ subm_at E p ⟹ mreplace_at C p D ≤ E"
apply (induct C p D arbitrary: E rule: mreplace_at.induct)
apply (auto elim!: less_eq_mctxtE1 intro!: less_eq_mctxtI1)
apply (case_tac "ia = i")
apply (auto simp: nth_append_take_drop_is_nth_conv nth_append_take)
done
definition funposs_mctxt :: "('f, 'v) mctxt ⇒ pos set" where
"funposs_mctxt C = funposs (mctxt_term_conv C)"
lemma funposs_mctxt_subset_poss_mctxt:
"funposs_mctxt C ⊆ poss_mctxt C"
by (induct C) (force simp: funposs_mctxt_def)+
lemma funposs_mctxt_subset_all_poss_mctxt:
"funposs_mctxt C ⊆ all_poss_mctxt C"
by (induct C) (force simp: funposs_mctxt_def)+
lemma funposs_mctxt_mono:
"C ≤ D ⟹ p ∈ funposs_mctxt C ⟹ p ∈ funposs_mctxt D"
unfolding less_eq_mctxt_prime funposs_mctxt_def
by (induct C D arbitrary: p rule: less_eq_mctxt'.induct) auto
lemma funposs_mctxt_compat:
"C ≤ D ⟹ p ∈ poss_mctxt C ⟹ p ∈ funposs_mctxt D ⟹ p ∈ funposs_mctxt C"
unfolding less_eq_mctxt_prime funposs_mctxt_def
by (induct C D arbitrary: p rule: less_eq_mctxt'.induct) (auto)
lemma funposs_mctxt_mctxt_of_term[simp]:
"funposs_mctxt (mctxt_of_term t) = funposs t"
by (induct t) (auto simp: funposs_mctxt_def)
subsection ‹finiteness of prefixes›
lemma finite_set_Cons:
assumes A: "finite A" and B: "finite B"
shows "finite (set_Cons A B)"
proof -
have "set_Cons A B = case_prod (op #) ` (A × B)" by (auto simp: set_Cons_def)
then show ?thesis
by (simp add: finite_imageI[OF finite_cartesian_product[OF A B],of "case_prod (op #)"])
qed
lemma listset_finite:
assumes "∀A ∈ set As. finite A"
shows "finite (listset As)"
using assms
by (induct As) (auto simp: finite_set_Cons)
lemma elem_listset:
"xs ∈ listset As = (length xs = length As ∧ (∀i < length As. xs ! i ∈ As ! i))"
proof (induct As arbitrary: xs)
case (Cons A As xs) thus ?case
by (cases xs) (auto simp: set_Cons_def nth_Cons nat.splits)
qed auto
lemma finite_pre_mctxt:
fixes C :: "('f, 'v) mctxt"
shows "finite { N. N ≤ C }"
proof (induct C)
case MHole
have *: "{ N. N ≤ MHole } = { MHole }" by (auto simp: less_eq_mctxt_def)
show ?case by (simp add: *)
next
case (MVar x)
have *: "{ N. N ≤ MVar x } = { MHole, MVar x }"
by (auto simp: less_eq_mctxt_def split_ifs elim: mctxt_neq_mholeE)
show ?case by (simp add: *)
next
case (MFun f Cs)
have *: "{ N. N ≤ MFun f Cs } = { MHole } ∪ MFun f ` { Ds. Ds ∈ listset (map (λC. { N. N ≤ C }) Cs)}"
unfolding elem_listset
by (auto simp: image_def less_eq_mctxt_def split_ifs list_eq_iff_nth_eq elim!: mctxt_neq_mholeE) auto
show ?case
by (auto simp: * MFun listset_finite[of "map (λC. { N. N ≤ C }) Cs"])
qed
text ‹well-founded-ness of <›
fun mctxt_syms :: "('f, 'v) mctxt ⇒ nat" where
"mctxt_syms MHole = 0"
| "mctxt_syms (MVar v) = 1"
| "mctxt_syms (MFun f Cs) = 1 + sum_list (map mctxt_syms Cs)"
lemma mctxt_syms_mono:
"C ≤ D ⟹ mctxt_syms C ≤ mctxt_syms D"
by (induct D arbitrary: C; elim leq_mholeE leq_mvarE leq_mfunE)
(auto simp: map_upt_len_conv[of mctxt_syms,symmetric] intro: sum_list_mono)
lemma sum_list_strict_mono_aux:
fixes xs ys :: "nat list"
shows "length xs = length ys ⟹ (⋀i. i < length ys ⟹ xs ! i ≤ ys ! i) ⟹ sum_list xs < sum_list ys ∨ xs = ys"
proof (induct xs arbitrary: ys)
case (Cons x xs zs) note * = this
then show ?case
proof (cases zs)
case (Cons y ys)
have hd: "x ≤ y" and tl: "⋀i. i < length ys ⟹ xs ! i ≤ ys ! i"
using *(3) by (auto simp: Cons nth_Cons nat.splits)
show ?thesis using hd *(1)[OF _ tl] *(2) by (auto simp: nth_Cons Cons)
qed auto
qed auto
lemma mctxt_syms_strict_mono[simp]:
"C < D ⟹ mctxt_syms C < mctxt_syms D"
proof -
assume "C < D"
also have "C ≤ D ⟹ C = D ∨ mctxt_syms C < mctxt_syms D"
proof (induct D arbitrary: C; elim leq_mholeE leq_mvarE leq_mfunE)
fix f Ds C Cs
assume IH: "(⋀D' C'. D' ∈ set Ds ⟹ C' ≤ D' ⟹ C' = D' ∨ mctxt_syms C' < mctxt_syms D')"
and C: "C = MFun f Cs" and len: "length Cs = length Ds"
and CDi: "⋀i. i < length Ds ⟹ Cs ! i ≤ Ds ! i"
{
fix i
have "i < length Ds ⟹ mctxt_syms (Cs ! i) ≤ mctxt_syms (Ds ! i)"
using IH[OF _ CDi, of i] by auto
}
then show "C = MFun f Ds ∨ mctxt_syms C < mctxt_syms (MFun f Ds)"
using IH[OF _ CDi] sum_list_strict_mono_aux[of "map mctxt_syms Cs" "map mctxt_syms Ds"]
by (auto simp: list_eq_iff_nth_eq C len)
qed auto
ultimately show ?thesis by (auto simp: less_mctxt_def)
qed
lemma wf_less_mctxt[simp]:
"wf { (C :: ('f, 'v) mctxt, D). C < D }"
by (rule wf_subset[of "inv_image { (a, b). a < b } mctxt_syms"]) (auto simp: wf_less)
lemma map_zip2[simp]:
"n = length xs ⟹ zip xs (replicate n y) = map (λx. (x,y)) xs"
by (induct xs arbitrary: n) auto
lemma map_zip1[simp]:
"n = length ys ⟹ zip (replicate n x) ys = map (λy. (x,y)) ys"
by (induct ys arbitrary: n) auto
lemma all_poss_mctxt_mono:
"C ≤ D ⟹ all_poss_mctxt C ⊆ all_poss_mctxt D"
by (induct C D rule: less_eq_mctxt_induct) force+
lemma all_poss_mctxt_inf_mctxt:
"(C, D) ∈ comp_mctxt ⟹ all_poss_mctxt (C ⊓ D) = all_poss_mctxt C ∩ all_poss_mctxt D"
by (induct C D rule: comp_mctxt.induct) auto
lemma less_eq_subm_at:
"p ∈ all_poss_mctxt C ⟹ C ≤ D ⟹ subm_at C p ≤ subm_at D p"
by (induct C arbitrary: p D) (auto elim: less_eq_mctxtE1)
lemma inf_subm_at:
"p ∈ all_poss_mctxt (C ⊓ D) ⟹ subm_at (C ⊓ D) p = subm_at C p ⊓ subm_at D p"
proof (induct C D arbitrary: p rule: inf_mctxt.induct)
case (4 f Cs g Ds p) show ?case using 4(1) 4(2)
by (auto 4 4 intro!: 4(1)[of "(Cs ! i, Ds ! i)" "Cs ! i" "Ds ! i" for i] simp: set_zip)
qed auto
lemma less_eq_fill_holesI:
assumes "length Ds = num_holes C" "length Es = num_holes C"
"⋀i. i < num_holes C ⟹ Ds ! i ≤ Es ! i"
shows "fill_holes_mctxt C Ds ≤ fill_holes_mctxt C Es"
using assms(1,2)[symmetric] assms(3)
by (induct C Ds Es rule: fill_holes_induct2) (auto intro!: less_eq_mctxtI1 simp: partition_by_nth_nth)
lemma less_eq_fill_holesD:
assumes "length Ds = num_holes C" "length Es = num_holes C"
"fill_holes_mctxt C Ds ≤ fill_holes_mctxt C Es" "i < num_holes C"
shows "Ds ! i ≤ Es ! i"
using assms(1,2)[symmetric] assms(3,4)
proof (induct C Ds Es arbitrary: i rule: fill_holes_induct2)
case (MFun f Cs Ds Es)
obtain j k where "j < length Cs" "k < num_holes (Cs ! j)"
"zip Ds Es ! i = partition_holes (zip Ds Es) Cs ! j ! k"
using nth_concat_split[of i "partition_holes (zip Ds Es) Cs"] MFun(1,2,5) by auto
moreover then have "f (zip Ds Es ! i) = partition_holes (map f (zip Ds Es)) Cs ! j ! k" for f
using nth_map[of k "partition_holes (zip Ds Es) Cs ! j" f] MFun(1,2)
length_partition_by_nth[of "map num_holes Cs" "zip Ds Es"] by simp
from this[of fst] this[of snd] map_fst_zip[of Ds Es] map_snd_zip[of Ds Es]
have "Ds ! i = partition_holes Ds Cs ! j ! k" "Es ! i = partition_holes Es Cs ! j ! k"
using MFun(1,2,5) by simp_all
ultimately show ?case using MFun(3)[of j k] MFun(1,2,4) by (auto elim: less_eq_mctxtE1)
qed auto
lemma less_eq_fill_holes_iff:
assumes "length Ds = num_holes C" "length Es = num_holes C"
shows "fill_holes_mctxt C Ds ≤ fill_holes_mctxt C Es ⟷ (∀i < num_holes C. Ds ! i ≤ Es ! i)"
using assms by (auto intro: less_eq_fill_holesI dest: less_eq_fill_holesD)
lemma fill_holes_mctxt_suffix[simp]:
assumes "length Ds = num_holes C" shows "C ≤ fill_holes_mctxt C Ds"
using assms(1)[symmetric]
by (induct C Ds rule: fill_holes_induct) (auto simp: less_eq_mctxt_def intro: nth_equalityI)
lemma fill_holes_mctxt_id:
assumes "length Ds = num_holes C" "C = fill_holes_mctxt C Ds" shows "set Ds ⊆ {MHole}"
using assms(1)[symmetric] assms(2)
apply (induct C Ds rule: fill_holes_induct)
unfolding set_concat
by (auto simp: set_conv_nth[of "partition_holes _ _"] list_eq_iff_nth_eq[of _ "map _ _"])
lemma fill_holes_suffix[simp]:
"num_holes C = length ts ⟹ C ≤ mctxt_of_term (fill_holes C ts)"
by (induct C ts rule: fill_holes_induct) (auto intro: less_eq_mctxtI1)
subsection ‹Hole positions, left to right›
fun hole_poss' :: "('f, 'v) mctxt ⇒ pos list" where
"hole_poss' (MVar x) = []"
| "hole_poss' MHole = [ε]"
| "hole_poss' (MFun f cs) = concat (map (λi . map (op <# i) (hole_poss' (cs ! i))) [0..<length cs])"
lemma set_hole_poss': "set (hole_poss' C) = hole_poss C"
by (induct C) auto
lemma length_hole_poss'[simp]: "length (hole_poss' C) = num_holes C"
by (induct C) (auto simp: length_concat intro!: arg_cong[of _ _ sum_list] nth_equalityI)
lemma hole_poss'_map_vars_mctxt[simp]:
"hole_poss' (map_vars_mctxt f C) = hole_poss' C"
by (induct C rule: hole_poss'.induct) (auto intro: arg_cong[of _ _ concat])
lemma subt_at_fill_holes:
assumes "length ts = num_holes C" and "i < num_holes C"
shows "subt_at (fill_holes C ts) (hole_poss' C ! i) = ts ! i"
using assms(1)[symmetric] assms(2)
proof (induct C ts arbitrary: i rule: fill_holes_induct)
case (MFun f Cs ts)
have "i < length (concat (map (λi. map (op <# i) (hole_poss' (Cs ! i))) [0..<length Cs]))"
using MFun arg_cong[OF map_nth, of "map num_holes" Cs] by (auto simp: length_concat comp_def)
thus ?case
by (auto simp: nth_map[symmetric] map_concat intro!: arg_cong[of _ _ "λx. concat x ! _"])
(insert MFun, auto intro!: nth_equalityI)
qed auto
lemma subm_at_fill_holes_mctxt:
assumes "length Ds = num_holes C" and "i < num_holes C"
shows "subm_at (fill_holes_mctxt C Ds) (hole_poss' C ! i) = Ds ! i"
using assms(1)[symmetric] assms(2)
proof (induct C Ds arbitrary: i rule: fill_holes_induct)
case (MFun f Cs Ds)
have "i < length (concat (map (λi. map (op <# i) (hole_poss' (Cs ! i))) [0..<length Cs]))"
using MFun arg_cong[OF map_nth, of "map num_holes" Cs] by (auto simp: length_concat comp_def)
thus ?case
by (auto simp: nth_map[symmetric] map_concat intro!: arg_cong[of _ _ "λx. concat x ! _"])
(insert MFun, auto intro!: nth_equalityI)
qed auto
subsection ‹An inverse of @{term fill_holes}›
fun unfill_holes :: "('f, 'v) mctxt ⇒ ('f, 'v) term ⇒ ('f, 'v) term list" where
"unfill_holes MHole t = [t]"
| "unfill_holes (MVar w) (Var v) = (if v = w then [] else undefined)"
| "unfill_holes (MFun g Cs) (Fun f ts) = (if f = g ∧ length ts = length Cs then
concat (map (λi. unfill_holes (Cs ! i) (ts ! i)) [0..<length ts]) else undefined)"
lemma length_unfill_holes[simp]:
assumes "C ≤ mctxt_of_term t"
shows "length (unfill_holes C t) = num_holes C"
using assms
proof (induct C t rule: unfill_holes.induct)
case (3 f Cs g ts) with 3(1)[OF _ nth_mem] 3(2) show ?case
by (auto simp: less_eq_mctxt_def length_concat
intro!: cong[of sum_list, OF refl] nth_equalityI elim!: nth_equalityE)
qed (auto simp: less_eq_mctxt_def)
lemma fill_unfill_holes:
assumes "C ≤ mctxt_of_term t"
shows "fill_holes C (unfill_holes C t) = t"
using assms
proof (induct C t rule: unfill_holes.induct)
case (3 f Cs g ts) with 3(1)[OF _ nth_mem] 3(2) show ?case
by (auto simp: less_eq_mctxt_def length_unfill_holes
intro!: fill_holes_arbitrary elim!: nth_equalityE)
qed (auto simp: less_eq_mctxt_def split: if_splits)
lemma unfill_fill_holes:
assumes "length ts = num_holes C"
shows "unfill_holes C (fill_holes C ts) = ts"
using assms[symmetric]
proof (induct C ts rule: fill_holes_induct)
case (MFun f Cs ts) thus ?case
by (auto intro!: arg_cong[of _ _ concat] nth_equalityI[of _ "partition_holes ts Cs"]
simp del: concat_partition_by) auto
qed auto
lemma unfill_holes_subt:
assumes "C ≤ mctxt_of_term t" and "t' ∈ set (unfill_holes C t)"
shows "t' ⊴ t"
using assms
proof (induct C t rule: unfill_holes.induct)
case (3 f Cs g ts)
obtain i where "i < length Cs" and "t' ∈ set (unfill_holes (Cs ! i) (ts ! i))"
using 3 by (auto dest!: in_set_idx split: if_splits simp: less_eq_mctxt_def)
then show ?case
using 3(1)[OF _ nth_mem[of i]] 3(2,3) supteq.subt[of "ts ! i" ts t' g]
by (auto simp: less_eq_mctxt_def elim!: nth_equalityE split: if_splits)
qed (auto simp: less_eq_mctxt_def split: if_splits)
lemma unfill_holes_conv:
assumes "C ≤ mctxt_of_term t"
shows "unfill_holes C t = map (subt_at t) (hole_poss' C)"
using assms
proof (induct C t rule: unfill_holes.induct)
case (3 f Cs g ts) show ?case using 3(2)
by (auto elim!: less_eq_mctxtE2 simp: map_concat comp_def 3(1) intro!: arg_cong[of _ _ concat])
qed (auto elim: less_eq_mctxtE2)
lemma unfill_holes_by_prefix':
assumes "num_holes C = length Ds" "fill_holes_mctxt C Ds ≤ mctxt_of_term t"
shows "unfill_holes (fill_holes_mctxt C Ds) t = concat (map (λ(D, t). unfill_holes D t) (zip Ds (unfill_holes C t)))"
using assms
proof (induct C Ds arbitrary: t rule: fill_holes_induct)
case (MVar v) thus ?case by (cases t) (auto elim: less_eq_mctxtE1)
next
case (MFun f Cs Ds)
have [simp]: "length ts = length Cs ⟹ map (λi. unfill_holes (map (λi. fill_holes_mctxt (Cs ! i) (partition_holes Ds Cs ! i))
[0..<length Cs] ! i) (ts ! i)) [0..<length Cs]
= map (λi. unfill_holes (fill_holes_mctxt (Cs ! i) (partition_holes Ds Cs ! i)) (ts ! i)) [0..<length Cs]" for ts
by (auto intro: nth_equalityI)
obtain ts where lts: "length ts = length Cs" "t = Fun f ts" and
pre: "i < length Cs ⟹ fill_holes_mctxt (Cs ! i) (partition_holes Ds Cs ! i) ≤ mctxt_of_term (ts ! i)" for i
using MFun(1,3) by (cases t) (auto elim!: less_eq_mctxtE2)
have *: "i ∈ set [0..<n] ⟹ i < n" for i n by auto
have **: "(⋀i. i < n ⟹ length (f i) = length (g i)) ⟹
concat (map (λi. zip (f i) (g i)) [0..<n]) = zip (concat (map f [0..<n])) (concat (map g [0..<n]))" for f g n
by (induct n arbitrary: f g) (auto simp: map_upt_Suc simp del: upt.simps)
have ***: "i < length Cs ⟹ Cs ! i ≤ mctxt_of_term (ts ! i)" for i
using fill_holes_mctxt_suffix[of "partition_holes Ds Cs ! i" "Cs ! i", OF length_partition_holes_nth] MFun(1) pre[of i]
by (auto simp del: fill_holes_mctxt_suffix)
have [simp]: "concat (map (λi. concat (map f (zip (partition_holes Ds Cs ! i) (unfill_holes (Cs ! i) (ts ! i)))))
[0..<length Cs]) = concat (map f (zip Ds (concat (map (λi. unfill_holes (Cs ! i) (ts ! i)) [0..<length Cs]))))" for f
unfolding concat_map_concat[of "map _ _", unfolded map_map comp_def]
unfolding map_map[of "map f" "λi. zip (_ i) (_ i)", symmetric, unfolded comp_def] map_concat[symmetric]
using MFun(1) map_nth[of "partition_holes Ds Cs"] by (auto simp: length_unfill_holes[OF ***] **)
from lts pre show ?case using MFun(1) map_cong[OF refl MFun(2)[OF *], of "[0..<length Cs]" id "λi. ts ! i"]
by (auto simp del: map_eq_conv)
qed auto
lemma unfill_holes_by_prefix:
assumes "C ≤ D" and "D ≤ mctxt_of_term t"
shows "unfill_holes D t = concat (map (λp. unfill_holes (subm_at D p) (subt_at t p)) (hole_poss' C))"
using assms
proof (induct C arbitrary: D t)
case (MVar x) thus ?case by (cases t) (auto elim!: less_eq_mctxtE1)
next
case (MFun f Cs)
obtain Ds where D[simp]: "D = MFun f Ds" "length Ds = length Cs" using MFun(2) by (auto elim: less_eq_mctxtE1)
obtain ts where t[simp]: "t = Fun f ts" "length ts = length Cs" using MFun(3) by (cases t) (auto elim: less_eq_mctxtE1)
have "i < length Cs ⟹ unfill_holes (Ds ! i) (ts ! i) =
concat (map (λp. unfill_holes (subm_at (Ds ! i) p) (subt_at (ts ! i) p)) (hole_poss' (Cs ! i)))" for i
proof (intro MFun(1))
assume "i < length Cs" thus "Cs ! i ≤ Ds ! i" using MFun(2) by (auto elim: less_eq_mctxtE1)
next
assume "i < length Cs" thus "Ds ! i ≤ mctxt_of_term (ts ! i)" using MFun(3)
by (auto elim: less_eq_mctxt_MFunE1)
qed auto
then have *: "map (λi. unfill_holes (Ds ! i) (ts ! i)) [0..<length Cs] =
map (concat ∘ map (λp. unfill_holes (subm_at (MFun f Ds) p) (Fun f ts |_ p)) ∘
(λi. map (op <# i) (hole_poss' (Cs ! i)))) [0..<length Cs]"
by (intro nth_equalityI) (auto simp: o_def)
then show ?case by (auto simp add: map_concat map_map[symmetric] simp del: map_map)
qed auto
lemma unfill_holes_var_subst:
"C ≤ mctxt_of_term t ⟹ unfill_holes (map_vars_mctxt f C) (t ⋅ (Var o f)) = map (λt. t ⋅ (Var o f)) (unfill_holes C t)"
by (induct C t rule: unfill_holes.induct; (simp only: mctxt_of_term.simps; elim less_eq_mctxtE2)?)
(auto simp: map_concat intro!: arg_cong[of _ _ concat])
subsection ‹Ditto for @{term fill_holes_mctxt}›
fun unfill_holes_mctxt :: "('f, 'v) mctxt ⇒ ('f, 'v) mctxt ⇒ ('f, 'v) mctxt list" where
"unfill_holes_mctxt MHole D = [D]"
| "unfill_holes_mctxt (MVar w) (MVar v) = (if v = w then [] else undefined)"
| "unfill_holes_mctxt (MFun g Cs) (MFun f Ds) = (if f = g ∧ length Ds = length Cs then
concat (map (λi. unfill_holes_mctxt (Cs ! i) (Ds ! i)) [0..<length Ds]) else undefined)"
lemma length_unfill_holes_mctxt:
assumes "C ≤ D"
shows "length (unfill_holes_mctxt C D) = num_holes C"
using assms
proof (induct C D rule: unfill_holes_mctxt.induct)
case (3 f Cs g Ds) with 3(1)[OF _ nth_mem] 3(2) show ?case
by (auto simp: less_eq_mctxt_def length_concat
intro!: cong[of sum_list, OF refl] nth_equalityI elim!: nth_equalityE)
qed (auto simp: less_eq_mctxt_def)
lemma fill_unfill_holes_mctxt:
assumes "C ≤ D"
shows "fill_holes_mctxt C (unfill_holes_mctxt C D) = D"
using assms
proof (induct C D rule: unfill_holes_mctxt.induct)
case (3 f Cs g Ds) with 3(1)[OF _ nth_mem] 3(2) show ?case
by (auto simp: less_eq_mctxt_def length_unfill_holes_mctxt
intro!: fill_holes_arbitrary elim!: nth_equalityE)
qed (auto simp: less_eq_mctxt_def split: if_splits)
lemma unfill_fill_holes_mctxt:
assumes "length Ds = num_holes C"
shows "unfill_holes_mctxt C (fill_holes_mctxt C Ds) = Ds"
using assms[symmetric]
proof (induct C Ds rule: fill_holes_induct)
case (MFun f Cs ts) thus ?case
by (auto intro!: arg_cong[of _ _ concat] nth_equalityI[of _ "partition_holes ts Cs"]
simp del: concat_partition_by) auto
qed auto
lemma unfill_holes_mctxt_conv:
assumes "C ≤ D"
shows "unfill_holes_mctxt C D = map (subm_at D) (hole_poss' C)"
using assms
proof (induct C D rule: unfill_holes_mctxt.induct)
case (3 f Cs g Ds) show ?case using 3(2)
by (auto elim!: less_eq_mctxtE2 simp: map_concat comp_def 3(1) intro!: arg_cong[of _ _ concat])
qed (auto elim: less_eq_mctxtE2)
lemma unfill_holes_mctxt_mctxt_of_term:
assumes "C ≤ mctxt_of_term t"
shows "unfill_holes_mctxt C (mctxt_of_term t) = map mctxt_of_term (unfill_holes C t)"
using assms
proof (induct C arbitrary: t)
case (MVar x) then show ?case by (cases t) (auto elim: less_eq_mctxtE1)
next
case MHole then show ?case by (cases t) (auto elim: less_eq_mctxtE1)
next
case (MFun x1a x2) then show ?case
by (cases t) (auto elim: less_eq_mctxtE1 simp: map_concat intro!: arg_cong[of _ _ concat])
qed
lemma map_vars_Some_le_mctxt_of_term_mctxt_term_conv:
"map_vars_mctxt Some C ≤ mctxt_of_term (mctxt_term_conv C)"
by (induct C) (auto intro: less_eq_mctxtI1)
lemma unfill_holes_map_vars_mctxt_Some_mctxt_term_conv_conv:
"C ≤ E ⟹ unfill_holes (map_vars_mctxt Some C) (mctxt_term_conv E) = map mctxt_term_conv (unfill_holes_mctxt C E)"
by (induct C E rule: less_eq_mctxt_induct) (auto simp: map_concat intro!: arg_cong[of _ _ concat])
lemma unfill_holes_mctxt_by_prefix':
assumes "num_holes C = length Ds" "fill_holes_mctxt C Ds ≤ E"
shows "unfill_holes_mctxt (fill_holes_mctxt C Ds) E = concat (map (λ(D, E). unfill_holes_mctxt D E) (zip Ds (unfill_holes_mctxt C E)))"
proof -
have "C ≤ E" using assms(2) fill_holes_mctxt_suffix[OF assms(1)[symmetric]] by auto
have [simp]: "i < length Ds ⟹ Ds ! i ≤ unfill_holes_mctxt C E ! i" for i using assms
by (subst (asm) fill_unfill_holes_mctxt[OF `C ≤ E`, symmetric])
(auto simp: less_eq_fill_holes_iff length_unfill_holes_mctxt[OF `C ≤ E`])
show ?thesis using `C ≤ E` assms
arg_cong[OF unfill_holes_by_prefix'[of "map_vars_mctxt Some C" "map (map_vars_mctxt Some) Ds" "mctxt_term_conv E"], of "map term_mctxt_conv"]
order.trans[OF map_vars_mctxt_mono[OF assms(2), of Some] map_vars_Some_le_mctxt_of_term_mctxt_term_conv[of E]]
unfolding map_vars_mctxt_fill_holes_mctxt[symmetric, OF assms(1)]
by (auto simp: zip_map1 zip_map2 comp_def unfill_holes_map_vars_mctxt_Some_mctxt_term_conv_conv
prod.case_distrib map_concat in_set_conv_nth intro!: arg_cong[of _ _ concat])
qed
subsection ‹Function symbols of prefixes›
lemma funas_prefix[simp]:
"C ≤ D ⟹ fn ∈ funas_mctxt C ⟹ fn ∈ funas_mctxt D"
unfolding less_eq_mctxt_def
proof (induct C D rule: inf_mctxt.induct)
case (4 f Cs g Ds)
from 4(3) obtain i where "i < length Cs ∧ fn ∈ funas_mctxt (Cs ! i) ∨ fn = (f, length Cs)"
by (auto dest!: in_set_idx)
moreover {
assume "i < length Cs ∧ fn ∈ funas_mctxt (Cs ! i)"
hence "i < length Ds ∧ fn ∈ funas_mctxt (Ds ! i)" using 4(2)
by (auto intro!: 4(1)[of _ "Cs ! i" "Ds ! i"] split: if_splits
elim!: nth_equalityE simp: in_set_conv_nth)
hence ?case by (auto)
}
ultimately show ?case using 4(2) by auto
qed (auto)
end