theory Ground_mctxt
imports TRS.Multihole_Context Ground_Terms Ground_ctxt UL.Basic_Utils
begin
subsection ‹Ground multihole context›
datatype (gfuns_mctxt: 'f) gmctxt = GMHole | GMFun 'f "'f gmctxt list"
subsection ‹Basic function on ground mutlihole contexts›
primrec gmctxt_of_gterm :: "'f gterm ⇒ 'f gmctxt" where
"gmctxt_of_gterm (GFun f ts) = GMFun f (map gmctxt_of_gterm ts)"
fun num_gholes :: "'f gmctxt ⇒ nat" where
"num_gholes GMHole = 1"
| "num_gholes (GMFun _ ctxts) = sum_list (map num_gholes ctxts)"
primrec gterm_of_gmctxt :: "'f gmctxt ⇒ 'f gterm" where
"gterm_of_gmctxt (GMFun f Cs) = GFun f (map gterm_of_gmctxt Cs)"
primrec gmctxt_of_gctxt :: "'f gctxt ⇒ 'f gmctxt" where
"gmctxt_of_gctxt □⇩G = GMHole"
| "gmctxt_of_gctxt (GMore f ss C ts) =
GMFun f (map gmctxt_of_gterm ss @ gmctxt_of_gctxt C # map gmctxt_of_gterm ts)"
fun gctxt_of_gmctxt :: "'f gmctxt ⇒ 'f gctxt" where
"gctxt_of_gmctxt GMHole = □⇩G"
| "gctxt_of_gmctxt (GMFun f Cs) = (let n = nthWhile (λ C. num_gholes C = 0) Cs in
(if n < length Cs then
GMore f (map gterm_of_gmctxt (take n Cs)) (gctxt_of_gmctxt (Cs ! n)) (map gterm_of_gmctxt (drop (Suc n) Cs))
else undefined))"
primrec gmctxt_of_mctxt :: "('f, 'v) mctxt ⇒ 'f gmctxt" where
"gmctxt_of_mctxt MHole = GMHole"
| "gmctxt_of_mctxt (MFun f Cs) = GMFun f (map gmctxt_of_mctxt Cs)"
primrec mctxt_of_gmctxt :: "'f gmctxt ⇒ ('f, 'v) mctxt" where
"mctxt_of_gmctxt GMHole = MHole"
| "mctxt_of_gmctxt (GMFun f Cs) = MFun f (map mctxt_of_gmctxt Cs)"
fun funas_gmctxt :: "'f gmctxt ⇒ 'f sig" where
"funas_gmctxt (GMFun f Cs) = {(f, length Cs)} ∪ ⋃(funas_gmctxt ` set Cs)" |
"funas_gmctxt _ = {}"
"partition_gholes xs Cs ≡ partition_by xs (map num_gholes Cs)"">abbreviation "partition_gholes xs Cs ≡ partition_by xs (map num_gholes Cs)"
fun fill_gholes :: "'f gmctxt ⇒ 'f gterm list ⇒ 'f gterm" where
"fill_gholes GMHole [t] = t"
| "fill_gholes (GMFun f cs) ts = GFun f (map (λ i. fill_gholes (cs ! i)
(partition_gholes ts cs ! i)) [0 ..< length cs])"
fun fill_gholes_gmctxt :: "'f gmctxt ⇒ 'f gmctxt list ⇒ 'f gmctxt" where
"fill_gholes_gmctxt GMHole [] = GMHole" |
"fill_gholes_gmctxt GMHole [t] = t" |
"fill_gholes_gmctxt (GMFun f cs) ts = (GMFun f (map (λ i. fill_gholes_gmctxt (cs ! i)
(partition_gholes ts cs ! i)) [0 ..< length cs]))"
subsection ‹An inverse of @{term fill_gholes}›
fun unfill_gholes :: "'f gmctxt ⇒ 'f gterm ⇒ 'f gterm list" where
"unfill_gholes GMHole t = [t]"
| "unfill_gholes (GMFun g Cs) (GFun f ts) = (if f = g ∧ length ts = length Cs then
concat (map (λi. unfill_gholes (Cs ! i) (ts ! i)) [0..<length ts]) else undefined)"
fun sup_gmctxt_args :: "'f gmctxt ⇒ 'f gmctxt ⇒ 'f gmctxt list" where
"sup_gmctxt_args GMHole D = [D]" |
"sup_gmctxt_args C GMHole = replicate (num_gholes C) GMHole" |
"sup_gmctxt_args (GMFun f Cs) (GMFun g Ds) =
(if f = g ∧ length Cs = length Ds then concat (map (case_prod sup_gmctxt_args) (zip Cs Ds))
else undefined)"
fun ghole_poss :: "'f gmctxt ⇒ pos set" where
"ghole_poss GMHole = {[]}" |
"ghole_poss (GMFun f cs) = ⋃(set (map (λ i. (λ p. i # p) ` ghole_poss (cs ! i)) [0 ..< length cs]))"
"poss_rec f ts ≡ map2 (λ i t. map ((#) i) (f t)) ([0 ..< length ts]) ts"">abbreviation "poss_rec f ts ≡ map2 (λ i t. map ((#) i) (f t)) ([0 ..< length ts]) ts"
fun ghole_poss_list :: "'f gmctxt ⇒ pos list" where
"ghole_poss_list GMHole = [[]]"
| "ghole_poss_list (GMFun f cs) = concat (poss_rec ghole_poss_list cs)"
fun poss_gmctxt :: "'f gmctxt ⇒ pos set" where
"poss_gmctxt GMHole = {}" |
"poss_gmctxt (GMFun f cs) = {[]} ∪ ⋃(set (map (λ i. (λ p. i # p) ` poss_gmctxt (cs ! i)) [0 ..< length cs]))"
lemma poss_simps [simp]:
"ghole_poss (GMFun f Cs) = {i # p | i p. i < length Cs ∧ p ∈ ghole_poss (Cs ! i)}"
"poss_gmctxt (GMFun f Cs) = {[]} ∪ {i # p | i p. i < length Cs ∧ p ∈ poss_gmctxt (Cs ! i)}"
by auto
fun ghole_num_bef_pos where
"ghole_num_bef_pos [] _ = 0" |
"ghole_num_bef_pos (i # q) (GMFun f Cs) = sum_list (map num_gholes (take i Cs)) + ghole_num_bef_pos q (Cs ! i)"
fun ghole_num_at_pos where
"ghole_num_at_pos [] C = num_gholes C" |
"ghole_num_at_pos (i # q) (GMFun f Cs) = ghole_num_at_pos q (Cs ! i)"
fun subgm_at :: "'f gmctxt ⇒ pos ⇒ 'f gmctxt" where
"subgm_at C [] = C"
| "subgm_at (GMFun f Cs) (i # p) = subgm_at (Cs ! i) p"
definition gmctxt_subtgm_at_fill_args where
"gmctxt_subtgm_at_fill_args p C ts = take (ghole_num_at_pos p C) (drop (ghole_num_bef_pos p C) ts)"
declare hole_poss.simps(2)[simp del]
declare poss_mctxt.simps(2)[simp del]
instantiation gmctxt :: (type) inf
begin
fun inf_gmctxt :: "'a gmctxt ⇒ 'a gmctxt ⇒ 'a gmctxt" where
"GMHole ⊓ D = GMHole" |
"C ⊓ GMHole = GMHole" |
"GMFun f Cs ⊓ GMFun g Ds =
(if f = g ∧ length Cs = length Ds then GMFun f (map (case_prod (⊓)) (zip Cs Ds))
else GMHole)"
instance ..
end
instantiation gmctxt :: (type) sup
begin
fun sup_gmctxt :: "'a gmctxt ⇒ 'a gmctxt ⇒ 'a gmctxt" where
"GMHole ⊔ D = D" |
"C ⊔ GMHole = C" |
"GMFun f Cs ⊔ GMFun g Ds =
(if f = g ∧ length Cs = length Ds then GMFun f (map (case_prod (⊔)) (zip Cs Ds))
else undefined)"
instance ..
end
subsection ‹Orderings and compatibility of ground multihole contexts›
inductive less_eq_gmctxt :: "'f gmctxt ⇒ 'f gmctxt ⇒ bool" where
base [simp]: "less_eq_gmctxt GMHole u"
| ind[intro]: "length cs = length ds ⟹ (⋀i. i < length cs ⟹ less_eq_gmctxt (cs ! i) (ds ! i)) ⟹
less_eq_gmctxt (GMFun f cs) (GMFun f ds)"
inductive_set comp_gmctxt :: "('f gmctxt × 'f gmctxt) set" where
GMHole1 [simp]: "(GMHole, D) ∈ comp_gmctxt" |
GMHole2 [simp]: "(C, GMHole) ∈ comp_gmctxt" |
GMFun [intro]: "f = g ⟹ length Cs = length Ds ⟹ ∀i < length Ds. (Cs ! i, Ds ! i) ∈ comp_gmctxt ⟹
(GMFun f Cs, GMFun g Ds) ∈ comp_gmctxt"
definition gmctxt_closing where
"gmctxt_closing C D ⟷ less_eq_gmctxt C D ∧ ghole_poss D ⊆ ghole_poss C"
inductive eq_gfill ("(_/ =⇩G⇩f _)" [51, 51] 50) where
eqfI [intro]: "t = fill_gholes D ss ⟹ num_gholes D = length ss ⟹ t =⇩G⇩f (D, ss)"
subsection ‹Conversions from and to ground multihole contexts›
subsubsection ‹num_hole and gnum_hole›
lemma num_gholes_o_gmctxt_of_gterm [simp]:
"num_gholes ∘ gmctxt_of_gterm = (λx. 0)"
by (rule ext, induct_tac x) simp_all
lemma mctxt_of_term_term_of_mctxt_id [simp]:
"num_gholes C = 0 ⟹ gmctxt_of_gterm (gterm_of_gmctxt C) = C"
by (induct C) (simp_all add: map_idI)
lemma num_holes_mctxt_of_term [simp]:
"num_gholes (gmctxt_of_gterm t) = 0"
by (induct t) simp_all
lemma num_gholes_gmctxt_of_mctxt [simp]:
"ground_mctxt C ⟹ num_gholes (gmctxt_of_mctxt C) = num_holes C"
by (induct C) (auto intro: nth_sum_listI)
lemma num_holes_mctxt_of_gmctxt [simp]:
"num_holes (mctxt_of_gmctxt C) = num_gholes C"
by (induct C) (auto intro: nth_sum_listI)
lemma num_holes_mctxt_of_gmctxt_fun_comp [simp]:
"num_holes ∘ mctxt_of_gmctxt = num_gholes"
by (auto simp: comp_def)
lemma gmctxt_of_gctxt_num_gholes [simp]:
"num_gholes (gmctxt_of_gctxt C) = 1"
by (induct C) auto
lemma ground_mctxt_list_num_gholes_gmctxt_of_mctxt_conv [simp]:
"∀x∈set Cs. ground_mctxt x ⟹ map (num_gholes ∘ gmctxt_of_mctxt) Cs = map num_holes Cs"
by auto
lemma num_gholes_map_gmctxt [simp]:
"num_gholes (map_gmctxt f C) = num_gholes C"
by (induct C) (auto simp: comp_def, metis (no_types, lifting) map_eq_conv)
lemma map_num_gholes_map_gmctxt [simp]:
"map (num_gholes ∘ map_gmctxt f) Cs = map num_gholes Cs"
by (induct Cs) auto
subsubsection ‹Conversions gterm ⟷ gmctxt›
lemma gterm_of_gmctxt_gmctxt_of_gterm_id [simp]:
"gterm_of_gmctxt (gmctxt_of_gterm t) = t"
by (induct t) (simp_all add: map_idI)
lemma no_gholes_gmctxt_of_gterm_gterm_of_gmctxt_id [simp]:
"num_gholes C = 0 ⟹ gmctxt_of_gterm (gterm_of_gmctxt C) = C"
by (induct C) (auto simp: comp_def intro: nth_equalityI)
subsubsection ‹Conversions gctxt ⟷ gmctxt›
lemma nthWhile_gmctxt_of_gctxt [simp]:
"nthWhile (λC. num_gholes C = 0) (map gmctxt_of_gterm ss @ gmctxt_of_gctxt C # ts) = length ss"
by (induct ss) auto
lemma sum_list_nthWhile_length [simp]:
"sum_list (map num_gholes Cs) = Suc 0 ⟹ nthWhile (λC. num_gholes C = 0) Cs < length Cs"
by (induct Cs) auto
lemma gctxt_of_gmctxt_gmctxt_of_gctxt [simp]:
"gctxt_of_gmctxt (gmctxt_of_gctxt C) = C"
by (induct C) (auto simp: Let_def comp_def nth_append)
lemma gmctxt_of_gctxt_GMHole_Hole:
"gmctxt_of_gctxt C = GMHole ⟹ C = □⇩G"
by (metis gctxt_of_gmctxt.simps(1) gctxt_of_gmctxt_gmctxt_of_gctxt)
lemma gmctxt_of_gctxt_gctxt_of_gmctxt:
"num_gholes C = 1 ⟹ gmctxt_of_gctxt (gctxt_of_gmctxt C) = C"
proof (induct C)
case (GMFun f Cs)
then obtain i where nth: "i < length Cs" "i = nthWhile (λC. num_gholes C = 0) Cs"
using sum_list_nthWhile_length by auto
then have "0 < num_gholes (Cs ! i)" unfolding nth(2) using nthWhile_p
by auto
from nth(1) this have num: "num_gholes (Cs ! i) = 1" using GMFun(2)
by (auto elim!: sum_list_1_E)
then have [simp]: "map (gmctxt_of_gterm ∘ gterm_of_gmctxt) (drop (Suc i) Cs) = drop (Suc i) Cs" using GMFun(2) nth(1)
by (auto elim!: sum_list_1_E simp: comp_def intro!: nth_equalityI)
(metis add.commute add_Suc_right lessI less_diff_conv no_gholes_gmctxt_of_gterm_gterm_of_gmctxt_id not_add_less1)
have [simp]: "map (gmctxt_of_gterm ∘ gterm_of_gmctxt) (take i Cs) = take i Cs"
using nth(1) unfolding nth(2) by (induct Cs) auto
show ?case using id_take_nth_drop[OF nth(1)]
by (auto simp: Let_def GMFun(1)[OF nth_mem[OF nth(1)] num] simp flip: nth(2))
qed auto
lemma inj_gmctxt_of_gctxt: "inj gmctxt_of_gctxt"
unfolding inj_def by (metis gctxt_of_gmctxt_gmctxt_of_gctxt)
lemma inj_gctxt_of_gmctxt_on_single_hole:
"inj_on gctxt_of_gmctxt (Collect (λ C. num_gholes C = 1))"
by (metis (mono_tags, lifting) gmctxt_of_gctxt_gctxt_of_gmctxt inj_onI mem_Collect_eq)
lemma gctxt_of_gmctxt_hole_dest:
"num_gholes C = Suc 0 ⟹ gctxt_of_gmctxt C = □⇩G ⟹ C = GMHole"
by (cases C) (auto simp: Let_def split!: if_splits)
subsubsection ‹Conversions mctxt ⟷ gmctxt›
lemma mctxt_of_gmctxt_inv [simp]:
"gmctxt_of_mctxt (mctxt_of_gmctxt C) = C"
by (induct C) (simp_all add: map_idI)
lemma ground_mctxt_of_gmctxt [simp]:
"ground_mctxt (mctxt_of_gmctxt C)"
by (induct C) auto
lemma ground_mctxt_of_gmctxt' [simp]:
"mctxt_of_gmctxt C = MFun f D ⟹ ground_mctxt (MFun f D)"
by (induct C) auto
lemma gmctxt_of_mctxt_inv [simp]:
"ground_mctxt C ⟹ mctxt_of_gmctxt (gmctxt_of_mctxt C) = C"
by (induct C) (auto 0 0 intro!: nth_equalityI)
lemma ground_mctxt_of_gmctxtD:
"ground_mctxt C ⟹ ∃ D. C = mctxt_of_gmctxt D"
by (metis gmctxt_of_mctxt_inv)
lemma inj_mctxt_of_gmctxt: "inj_on mctxt_of_gmctxt X"
by (metis inj_on_def mctxt_of_gmctxt_inv)
lemma inj_gmctxt_of_mctxt_ground:
"inj_on gmctxt_of_mctxt (Collect ground_mctxt)"
using gmctxt_of_mctxt_inv inj_on_def by force
subsubsection ‹Map function on 'f symbols over mctxt and gmctxt›
lemma map_gmctxt_comp [simp]:
"map_gmctxt f (map_gmctxt g C) = map_gmctxt (f ∘ g) C"
by (induct C) auto
lemma map_mctxt_of_gmctxt:
"map_mctxt f (mctxt_of_gmctxt C) = mctxt_of_gmctxt (map_gmctxt f C)"
by (induct C) auto
lemma map_gmctxt_of_mctxt:
"ground_mctxt C ⟹ map_gmctxt f (gmctxt_of_mctxt C) = gmctxt_of_mctxt (map_mctxt f C)"
by (induct C) auto
lemma map_gmctxt_nempty [simp]:
"C ≠ GMHole ⟹ map_gmctxt f C ≠ GMHole"
by (cases C) auto
subsubsection ‹vars_mctxt of mctxt obtained by a gmctxt›
lemma vars_mctxt_of_gmctxt [simp]:
"vars_mctxt (mctxt_of_gmctxt C) = {}"
by (induct C) auto
lemma vars_mctxt_of_gmctxt_subseteq [simp]:
"vars_mctxt (mctxt_of_gmctxt C) ⊆ Q ⟷ True"
by auto
subsubsection ‹Equivalences and simplification rules›
lemma eqgfE:
assumes "t =⇩G⇩f (D, ss)" shows "t = fill_gholes D ss" "num_gholes D = length ss"
using assms[unfolded eq_gfill.simps] by auto
lemma eqgf_GMHoleE:
assumes "t =⇩G⇩f (GMHole, ss)" shows "ss = [t]" using eqgfE[OF assms]
by (cases ss) auto
lemma eqgf_GMFunE:
assumes "s =⇩G⇩f (GMFun f Cs, ss)"
obtains ts sss where "s = GFun f ts" "length ts = length Cs" "length sss = length Cs"
"⋀ i. i < length Cs ⟹ ts ! i =⇩G⇩f (Cs ! i, sss ! i)" "ss = concat sss"
proof -
from eqgfE[OF assms] have fh: "s = fill_gholes (GMFun f Cs) ss"
and nh: "sum_list (map num_gholes Cs) = length ss" by auto
from fh obtain ts where s: "s = GFun f ts" by (cases s, auto)
from fh[unfolded s]
have ts: "ts = map (λi. fill_gholes (Cs ! i) (partition_gholes ss Cs ! i)) [0..<length Cs]"
(is "_ = map (?f Cs ss) _")
by auto
let ?sss = "partition_gholes ss Cs"
from nh have *: "length ?sss = length Cs"
"⋀i. i < length Cs ⟹ ts ! i =⇩G⇩f (Cs ! i, ?sss ! i)" "ss = concat ?sss"
by (auto simp: ts length_partition_by_nth)
have len: "length ts = length Cs" unfolding ts by auto
assume ass: "⋀ts sss. s = GFun f ts ⟹
length ts = length Cs ⟹
length sss = length Cs ⟹ (⋀i. i < length Cs ⟹ ts ! i =⇩G⇩f (Cs ! i, sss ! i)) ⟹ ss = concat sss ⟹ thesis"
show thesis by (rule ass[OF s len *])
qed
lemma partition_holes_subseteq [simp]:
assumes "sum_list (map num_holes Cs) = length xs" "i < length Cs"
and "x ∈ set (partition_holes xs Cs ! i)"
shows "x ∈ set xs"
using assms partition_by_nth_nth_elem length_partition_by_nth
by (auto simp: in_set_conv_nth) fastforce
lemma partition_gholes_subseteq [simp]:
assumes "sum_list (map num_gholes Cs) = length xs" "i < length Cs"
and "x ∈ set (partition_gholes xs Cs ! i)"
shows "x ∈ set xs"
using assms partition_by_nth_nth_elem length_partition_by_nth
by (auto simp: in_set_conv_nth) fastforce
lemma list_elem_to_partition_nth [elim]:
assumes "sum_list (map num_gholes Cs) = length xs" "x ∈ set xs"
obtains i where "i < length Cs" "x ∈ set (partition_gholes xs Cs ! i)" using assms
by (metis concat_partition_by in_set_idx length_map length_partition_by nth_concat_split nth_mem)
lemma partition_holes_fill_gholes_conv':
"fill_gholes (GMFun f Cs) ts =
GFun f (map (case_prod fill_gholes) (zip Cs (partition_gholes ts Cs)))"
unfolding zip_nth_conv [of Cs "partition_gholes ts Cs", simplified]
and partition_holes_fill_holes_conv by simp
lemma unfill_gholes_conv:
assumes "length Cs = length ts"
shows "unfill_gholes (GMFun f Cs) (GFun f ts) =
concat (map (case_prod unfill_gholes) (zip Cs ts))" using assms
by (auto simp: zip_nth_conv [of Cs ts, simplified] comp_def)
lemma partition_holes_fill_gholes_gmctxt_conv:
"fill_gholes_gmctxt (GMFun f Cs) ts =
GMFun f [fill_gholes_gmctxt (Cs ! i) (partition_gholes ts Cs ! i). i ← [0 ..< length Cs]]"
by (simp add: partition_by_nth take_map)
lemma partition_holes_fill_gholes_gmctxt_conv':
"fill_gholes_gmctxt (GMFun f Cs) ts =
GMFun f (map (case_prod fill_gholes_gmctxt) (zip Cs (partition_gholes ts Cs)))"
unfolding zip_nth_conv [of Cs "partition_gholes ts Cs", simplified]
and partition_holes_fill_gholes_gmctxt_conv by simp
lemma fill_gholes_no_holes [simp]:
"num_gholes C = 0 ⟹ fill_gholes C [] = gterm_of_gmctxt C"
by (induct C) (auto simp: partition_holes_fill_gholes_conv'
simp del: fill_gholes.simps intro: nth_equalityI)
lemma fill_gholes_gmctxt_no_holes [simp]:
"num_gholes C = 0 ⟹ fill_gholes_gmctxt C [] = C"
by (induct C) (auto intro: nth_equalityI)
lemma eqgf_GMFunI:
assumes "⋀ i. i < length Cs ⟹ ss ! i =⇩G⇩f (Cs ! i, ts ! i)"
and "length Cs = length ss" "length ss = length ts"
shows "GFun f ss =⇩G⇩f (GMFun f Cs, concat ts)" using assms
apply (auto simp del: fill_gholes.simps
simp: partition_holes_fill_gholes_conv' intro!: eq_gfill.intros nth_equalityI)
apply (metis eqgfE length_map map_nth_eq_conv partition_by_concat_id)
by (metis eqgfE(2) length_concat nth_map_conv)
subsubsection ‹Induction for fill_gholes equivalent to the preexisting ones for fill_holes›
lemma length_partition_gholes_nth:
assumes "sum_list (map num_gholes cs) = length ts"
and "i < length cs"
shows "length (partition_gholes ts cs ! i) = num_gholes (cs ! i)"
using assms by (simp add: length_partition_by_nth)
lemma fill_gholes_induct2[consumes 2, case_names GMHole GMFun]:
fixes P :: "'f gmctxt ⇒ 'a list ⇒ 'b list ⇒ bool"
assumes len1: "num_gholes C = length xs" and len2: "num_gholes C = length ys"
and Hole: "⋀x y. P GMHole [x] [y]"
and Fun: "⋀f Cs xs ys. sum_list (map num_gholes Cs) = length xs ⟹
sum_list (map num_gholes Cs) = length ys ⟹
(⋀i. i < length Cs ⟹ P (Cs ! i) (partition_gholes xs Cs ! i) (partition_gholes ys Cs ! i)) ⟹
P (GMFun f Cs) (concat (partition_gholes xs Cs)) (concat (partition_gholes ys Cs))"
shows "P C xs ys"
proof (insert len1 len2, induct C arbitrary: xs ys)
case GMHole
then show ?case using Hole by (cases xs; cases ys) auto
next
case (GMFun f Cs)
then show ?case using Fun[of Cs xs ys f] by (auto simp: length_partition_by_nth)
qed
lemma fill_gholes_induct[consumes 1, case_names GMHole GMFun]:
fixes P :: "'f gmctxt ⇒ 'a list ⇒ bool"
assumes len: "num_gholes C = length xs"
and Hole: "⋀x. P GMHole [x]"
and Fun: "⋀f Cs xs. sum_list (map num_gholes Cs) = length xs ⟹
(⋀i. i < length Cs ⟹ P (Cs ! i) (partition_gholes xs Cs ! i)) ⟹
P (GMFun f Cs) (concat (partition_gholes xs Cs))"
shows "P C xs"
using fill_gholes_induct2[of C xs xs "λ C xs _. P C xs"] assms by simp
lemma eq_gfill_induct [consumes 1, case_names GMHole GMFun]:
assumes "t =⇩G⇩f (C, ts)"
and "⋀t. P t GMHole [t]"
and "⋀f ss Cs ts. ⟦length Cs = length ss; sum_list (map num_gholes Cs) = length ts;
∀i < length ss. ss ! i =⇩G⇩f (Cs ! i, partition_gholes ts Cs ! i) ∧
P (ss ! i) (Cs ! i) (partition_gholes ts Cs ! i)⟧
⟹ P (GFun f ss) (GMFun f Cs) ts"
shows "P t C ts" using assms(1)
proof (induct t arbitrary: C ts)
case (GFun f ss)
{assume "C = GMHole" and "ts = [GFun f ss]"
then have ?case using assms(2) by auto}
moreover
{fix Cs
assume C: "C = GMFun f Cs" and "sum_list (map num_gholes Cs) = length ts"
and "length Cs = length ss"
and "GFun f ss = fill_gholes (GMFun f Cs) ts"
moreover then have "∀i < length ss. ss ! i =⇩G⇩f (Cs ! i, partition_gholes ts Cs ! i)"
by (auto simp del: fill_gholes.simps
simp: partition_holes_fill_gholes_conv' length_partition_gholes_nth intro!: eq_gfill.intros)
moreover have "∀i < length ss. P (ss ! i) (Cs ! i) (partition_gholes ts Cs ! i)"
using GFun calculation(5) nth_mem by blast
ultimately have ?case using assms(3)[of Cs ss ts f] by auto}
ultimately show ?case using GFun
by (elim eq_gfill.cases) (auto simp del: fill_gholes.simps,
metis GFun.prems eqgf_GMFunE eqgf_GMHoleE gterm.inject num_gholes.elims)
qed
lemma nempty_ground_mctxt_gmctxt [simp]:
"C ≠ MHole ⟹ ground_mctxt C ⟹ gmctxt_of_mctxt C ≠ GMHole"
by (induct C) auto
lemma mctxt_of_gmctxt_fill_holes [simp]:
assumes "num_gholes C = length ss"
shows "gterm_of_term (fill_holes (mctxt_of_gmctxt C) (map term_of_gterm ss)) = fill_gholes C ss" using assms
by (induct rule: fill_gholes_induct) auto
lemma mctxt_of_gmctxt_terms_fill_holes:
assumes "num_gholes C = length ss"
shows "gterm_of_term (fill_holes (mctxt_of_gmctxt C) ss) = fill_gholes C (map gterm_of_term ss)" using assms
by (induct rule: fill_gholes_induct) auto
lemma ground_gmctxt_of_mctxt_gterm_fill_holes:
assumes "num_holes C = length ss" and "ground_mctxt C"
shows "term_of_gterm (fill_gholes (gmctxt_of_mctxt C) ss) = fill_holes C (map term_of_gterm ss)" using assms
by (induct rule: fill_holes_induct)
(auto simp: comp_def, metis (no_types, lifting) map_eq_conv num_gholes_gmctxt_of_mctxt)
lemma ground_gmctxt_of_gterm_of_term:
assumes "num_holes C = length ss" and "ground_mctxt C"
shows "gterm_of_term (fill_holes C (map term_of_gterm ss)) = fill_gholes (gmctxt_of_mctxt C) ss" using assms
by (induct rule: fill_holes_induct)
(auto simp: comp_def, metis (no_types, lifting) map_eq_conv num_gholes_gmctxt_of_mctxt)
lemma ground_gmctxt_of_mctxt_fill_holes [simp]:
assumes "num_holes C = length ss" and "ground_mctxt C" "∀ s ∈ set ss. ground s"
shows "term_of_gterm (fill_gholes (gmctxt_of_mctxt C) (map gterm_of_term ss)) = fill_holes C ss" using assms
by (induct rule: fill_holes_induct) auto
lemma fill_holes_mctxt_of_gmctxt_to_fill_gholes:
assumes "num_gholes C = length ss"
shows "fill_holes (mctxt_of_gmctxt C) (map term_of_gterm ss) = term_of_gterm (fill_gholes C ss)"
using assms
by (metis ground_gmctxt_of_mctxt_gterm_fill_holes ground_mctxt_of_gmctxt mctxt_of_gmctxt_inv num_holes_mctxt_of_gmctxt)
lemma fill_gholes_gmctxt_of_gterm [simp]:
"fill_gholes (gmctxt_of_gterm s) [] = s"
by (induct s) (auto simp add: map_nth_eq_conv)
lemma fill_gholes_GMHole [simp]:
"length ss = Suc 0 ⟹ fill_gholes GMHole ss = ss ! 0"
by (cases ss) auto
lemma apply_gctxt_fill_gholes:
"C⟨s⟩⇩G = fill_gholes (gmctxt_of_gctxt C) [s]"
by (induct C) (auto simp: partition_holes_fill_gholes_conv'
simp del: fill_gholes.simps intro!: nth_equalityI)
lemma fill_gholes_apply_gctxt:
"num_gholes C = 1 ⟹ fill_gholes C [s] = (gctxt_of_gmctxt C)⟨s⟩⇩G"
by (simp add: apply_gctxt_fill_gholes gmctxt_of_gctxt_gctxt_of_gmctxt)
lemma fill_gholes_replicate [simp]:
"n = length ss ⟹ fill_gholes (GMFun f (replicate n GMHole)) ss = GFun f ss"
unfolding partition_holes_fill_gholes_conv'
by (induct ss arbitrary: n) auto
lemma fill_gholes_gmctxt_replicate_MHole [simp]:
"fill_gholes_gmctxt C (replicate (num_gholes C) GMHole) = C"
proof (induct C)
case (GMFun f Cs)
{fix i assume "i < length Cs"
then have "partition_gholes (replicate (sum_list (map num_gholes Cs)) GMHole) Cs ! i =
replicate (num_gholes (Cs ! i)) GMHole"
using partition_by_nth_nth[of "map num_gholes Cs" "replicate (sum_list (map num_gholes Cs)) MHole"]
by (auto simp: length_partition_by_nth partition_by_nth_nth intro!: nth_equalityI)}
note * = this
show ?case using GMFun[OF nth_mem] by (auto simp: * intro!: nth_equalityI)
qed auto
lemma fill_gholes_gmctxt_GMFun_replicate_length [simp]:
"fill_gholes_gmctxt (GMFun f (replicate (length Cs) GMHole)) Cs = GMFun f Cs"
unfolding partition_holes_fill_gholes_gmctxt_conv'
by (induct Cs) simp_all
lemma fill_gholes_gmctxt_MFun:
assumes lCs: "length Cs = length ts"
and lss: "length ss = length ts"
and rec: "⋀ i. i < length ts ⟹ num_gholes (Cs ! i) = length (ss ! i) ∧
fill_gholes_gmctxt (Cs ! i) (ss ! i) = ts ! i"
shows "fill_gholes_gmctxt (GMFun f Cs) (concat ss) = GMFun f ts"
using assms unfolding fill_gholes_gmctxt.simps gmctxt.simps
by (auto intro!: nth_equalityI)
(metis length_map map_nth_eq_conv partition_by_concat_id)
lemma fill_gholes_gmctxt_nHole [simp]:
"C ≠ GMHole ⟹ num_gholes C = length Ds ⟹ fill_gholes_gmctxt C Ds ≠ GMHole"
using fill_gholes_gmctxt.elims by blast
lemma num_gholes_fill_gholes_gmctxt [simp]:
assumes "num_gholes C = length Ds"
shows "num_gholes (fill_gholes_gmctxt C Ds) = sum_list (map num_gholes Ds)" using assms
proof (induct C arbitrary: Ds)
case GMHole then show ?case
by (cases Ds) simp_all
next
case (GMFun f Cs)
then have *: "map (num_gholes ∘ (λi. fill_gholes_gmctxt (Cs ! i) (partition_gholes Ds Cs ! i))) [0..<length Cs] =
map (λi. sum_list (map num_gholes (partition_gholes Ds Cs ! i))) [0 ..< length Cs]"
and "sum_list (map num_gholes Cs) = length Ds"
by (auto simp add: length_partition_by_nth)
then show ?case
using map_upt_len_conv [of "λx. sum_list (map num_gholes x)" "partition_gholes Ds Cs"]
unfolding partition_holes_fill_holes_mctxt_conv by (simp add: *)
qed
lemma num_gholes_greater0_fill_gholes_gmctxt [intro!]:
assumes "num_gholes C = length Ds"
and "∃ D ∈ set Ds. 0 < num_gholes D"
shows "0 < sum_list (map num_gholes Ds)"
using assms gr_zeroI by force
lemma fill_gholes_gmctxt_fill_gholes:
assumes len_ds: "length Ds = num_gholes C"
and nh: "num_gholes (fill_gholes_gmctxt C Ds) = length ss"
shows "fill_gholes (fill_gholes_gmctxt C Ds) ss =
fill_gholes C [fill_gholes (Ds ! i) (partition_gholes ss Ds ! i). i ← [0 ..< num_gholes C]]"
using assms(1)[symmetric] assms(2)
proof (induct C Ds arbitrary: ss rule: fill_gholes_induct)
case (GMFun f Cs ds ss)
define qs where "qs = map (λi. fill_gholes_gmctxt (Cs ! i) (partition_gholes ds Cs ! i)) [0..<length Cs]"
then have qs: "⋀i. i < length Cs ⟹ fill_gholes_gmctxt (Cs ! i) (partition_gholes ds Cs ! i) = qs ! i"
"length qs = length Cs" by auto
define zs where "zs = map (λi. fill_gholes (ds ! i) (partition_gholes ss ds ! i)) [0..<length ds]"
{fix i assume i: "i < length Cs"
from GMFun(1) have *: "map length (partition_gholes ds Cs) = map num_gholes Cs" by auto
have **: "length ss = sum_list (map sum_list (partition_gholes (map num_gholes ds) Cs))"
using GMFun(1) GMFun(3)[symmetric] num_gholes_fill_gholes_gmctxt[of "GMFun f Cs" ds]
by (auto simp: comp_def map_map_partition_by[symmetric])
have "partition_by (partition_by ss
(map (λi. num_gholes (fill_gholes_gmctxt (Cs ! i) (partition_gholes ds Cs ! i))) [0..<length Cs]) ! i)
(partition_gholes (map num_gholes ds) Cs ! i) = partition_gholes (partition_gholes ss ds) Cs ! i"
using i GMFun(1) GMFun(3) partition_by_partition_by[OF **]
by (auto simp: comp_def num_gholes_fill_gholes_gmctxt length_partition_by_nth
intro!: arg_cong[of _ _ "λx. partition_by (partition_by ss x ! _) _"] nth_equalityI)
then have "map (λj. fill_gholes (partition_gholes ds Cs ! i ! j)
(partition_gholes (partition_gholes ss qs ! i)
(partition_gholes ds Cs ! i) ! j)) [0..<num_gholes (Cs ! i)] =
partition_gholes zs Cs ! i" using GMFun(1,3)
by (auto simp: length_partition_by_nth zs_def qs_def i comp_def partition_by_nth_nth intro: nth_equalityI)}
then show ?case using GMFun
by (simp add: qs_def [symmetric] qs zs_def [symmetric] length_partition_by_nth)
qed auto
lemma fill_gholes_gmctxt_sound:
assumes len_ds: "length Ds = num_gholes C"
and len_sss: "length sss = num_gholes C"
and len_ts: "length ts = num_gholes C"
and insts: "⋀ i. i < length Ds ⟹ ts ! i =⇩G⇩f (Ds ! i, sss ! i)"
shows "fill_gholes C ts =⇩G⇩f (fill_gholes_gmctxt C Ds, concat sss)"
proof (rule eqfI)
note l_nh_i = eqgfE(2)[OF insts]
from len_ds len_sss have concat_sss: "partition_gholes (concat sss) Ds = sss"
by (metis l_nh_i length_map map_nth_eq_conv partition_by_concat_id)
then show nh: "num_gholes (fill_gholes_gmctxt C Ds) = length (concat sss)"
unfolding num_gholes_fill_gholes_gmctxt [OF len_ds [symmetric]] length_concat
by (metis l_nh_i len_ds len_sss nth_map_conv)
have ts: "ts = [fill_gholes (Ds ! i) (partition_gholes (concat sss) Ds ! i) . i ← [0..<num_gholes C]]" (is "_ = ?fhs")
proof (rule nth_equalityI)
show l_fhs: "length ts = length ?fhs" unfolding length_map
by (metis diff_zero len_ts length_upt)
fix i
assume i: "i < length ts"
then have i': "i < length [0..<num_gholes C]"
by (metis diff_zero len_ts length_upt)
show "ts!i = ?fhs ! i"
unfolding nth_map[OF i']
using eqgfE(1)[OF insts[unfolded len_ds, OF i[unfolded len_ts]]]
by (metis concat_sss i' len_ds len_sss map_nth nth_map)
qed
note ts = this
show "fill_gholes C ts = fill_gholes (fill_gholes_gmctxt C Ds) (concat sss)"
unfolding fill_gholes_gmctxt_fill_gholes[OF len_ds nh] ts ..
qed
subsection ‹Semilattice Structures›
lemma inf_gmctxt_idem [simp]:
"(C :: 'f gmctxt) ⊓ C = C"
by (induct C) (auto simp: zip_same_conv_map intro: map_idI)
lemma inf_gmctxt_GMHole2 [simp]:
"C ⊓ GMHole = GMHole"
by (induct C) simp_all
lemma inf_gmctxt_comm [ac_simps]:
"(C :: 'f gmctxt) ⊓ D = D ⊓ C"
by (induct C D rule: inf_gmctxt.induct) (fastforce simp: in_set_conv_nth intro!: nth_equalityI)+
lemma inf_gmctxt_assoc [ac_simps]:
fixes C :: "'f gmctxt"
shows "C ⊓ D ⊓ E = C ⊓ (D ⊓ E)"
apply (induct C D arbitrary: E rule: inf_gmctxt.induct)
apply (auto)
apply (case_tac E, auto)+
apply (fastforce simp: in_set_conv_nth intro!: nth_equalityI)
apply (case_tac E, auto)+
done
instantiation gmctxt :: (type) order
begin
"(C :: 'a gmctxt) ≤ D ⟷ C ⊓ D = C"">definition "(C :: 'a gmctxt) ≤ D ⟷ C ⊓ D = C"
"(C :: 'a gmctxt) < D ⟷ C ≤ D ∧ ¬ D ≤ C"">definition "(C :: 'a gmctxt) < D ⟷ C ≤ D ∧ ¬ D ≤ C"
instance
by (standard, simp_all add: less_eq_gmctxt_def less_gmctxt_def ac_simps, metis inf_gmctxt_assoc)
end
lemma less_eq_gmctxt_prime: "C ≤ D ⟷ less_eq_gmctxt C D"
proof
assume "less_eq_gmctxt C D" then show "C ≤ D"
by (induct C D rule: less_eq_gmctxt.induct) (auto simp: less_eq_gmctxt_def intro: nth_equalityI)
next
assume "C ≤ D" then show "less_eq_gmctxt C D" unfolding less_eq_gmctxt_def
by (induct C D rule: inf_gmctxt.induct)
(auto split: if_splits simp: set_zip intro!: less_eq_gmctxt.intros nth_equalityI elim!: nth_equalityE, metis)
qed
lemmas less_eq_gmctxt_induct = less_eq_gmctxt.induct[folded less_eq_gmctxt_prime, consumes 1]
lemmas less_eq_gmctxt_intros = less_eq_gmctxt.intros[folded less_eq_gmctxt_prime]
lemma less_eq_gmctxt_Hole:
"less_eq_gmctxt C GMHole ⟹ C = GMHole"
using less_eq_gmctxt.cases by blast
lemma num_gholes_at_least1:
"0 < num_gholes C ⟹ 0 < num_gholes (C ⊓ D)"
proof (induct C arbitrary: D)
case (GMFun f Cs)
from GMFun(2) obtain i where wit: "i < length Cs" "0 < num_gholes (Cs ! i)"
by (auto, metis (mono_tags, lifting) in_set_conv_nth length_map map_nth_eq_conv not_less sum_list_nonpos)
note IS = GMFun(1)[OF nth_mem, OF wit]
show ?case
proof (cases D)
case [simp]: (GMFun g Ds)
{assume "f = g" "length Cs = length Ds"
then have "0 < num_gholes (Cs ! i ⊓ Ds ! i)" using IS[of "Ds ! i"]
by auto}
then show ?thesis using wit(1)
by (auto simp: split!: prod.splits)
(smt forall_finite(1) length_map length_zip linorder_neqE_nat map_nth_eq_conv
min.absorb2 nth_mem nth_zip o_apply order_refl split_conv sum_list_eq_0_iff)
qed auto
qed auto
text ‹
@{const sup} is defined on compatible multihole contexts.
Note that compatibility is not transitive.
›
instance gmctxt :: (type) semilattice_inf
apply (standard)
apply (auto simp: less_eq_gmctxt_def inf_gmctxt_assoc [symmetric])
apply (metis inf_gmctxt_comm inf_gmctxt_assoc inf_gmctxt_idem)+
done
lemma sup_gmctxt_idem [simp]:
fixes C :: "'f gmctxt"
shows "C ⊔ C = C"
by (induct C) (auto simp: zip_same_conv_map intro: map_idI)
lemma sup_gmctxt_MHole [simp]: "C ⊔ GMHole = C"
by (induct C) simp_all
lemma sup_gmctxt_comm [ac_simps]:
fixes C :: "'f gmctxt"
shows "C ⊔ D = D ⊔ C"
by (induct C D rule: sup_gmctxt.induct) (fastforce simp: in_set_conv_nth intro!: nth_equalityI)+
lemma comp_gmctxt_refl:
"(C, C) ∈ comp_gmctxt"
by (induct C) auto
lemma comp_gmctxt_sym:
assumes "(C, D) ∈ comp_gmctxt"
shows "(D, C) ∈ comp_gmctxt"
using assms by (induct) auto
lemma sup_gmctxt_assoc [ac_simps]:
assumes "(C, D) ∈ comp_gmctxt" and "(D, E) ∈ comp_gmctxt"
shows "C ⊔ D ⊔ E = C ⊔ (D ⊔ E)"
using assms by (induct C D arbitrary: E) (auto elim!: comp_gmctxt.cases intro!: nth_equalityI)
text ‹
No instantiation to @{class semilattice_sup} possible, since @{const sup} is only
partially defined on terms (e.g., it is not associative in general).
›
interpretation gmctxt_order_bot: order_bot GMHole "(≤)" "(<)"
by (standard) (simp add: less_eq_gmctxt_def)
lemma sup_gmctxt_ge1 [simp]:
assumes "(C, D) ∈ comp_gmctxt"
shows "C ≤ C ⊔ D"
using assms by (induct C D) (auto simp: less_eq_gmctxt_def intro: nth_equalityI)
lemma sup_gmctxt_ge2 [simp]:
assumes "(C, D) ∈ comp_gmctxt"
shows "D ≤ C ⊔ D"
using assms by (induct) (auto simp: less_eq_gmctxt_def intro: nth_equalityI)
lemma sup_gmctxt_least:
assumes "(D, E) ∈ comp_gmctxt"
and "D ≤ C" and "E ≤ C"
shows "D ⊔ E ≤ C"
using assms
apply (induct arbitrary: C)
apply (auto simp: less_eq_gmctxt_def elim!: inf_gmctxt.elims intro!: nth_equalityI)
apply (metis (erased, lifting) length_map nth_map nth_zip split_conv)
apply (case_tac "fb = gb ∧ length Csb = length Dsb", simp_all)+
done
lemma sup_gmctxt_args_MHole2 [simp]:
"sup_gmctxt_args C GMHole = replicate (num_gholes C) GMHole"
by (cases C) simp_all
lemma num_gholes_sup_gmctxt_args:
assumes "(C, D) ∈ comp_gmctxt"
shows "num_gholes C = length (sup_gmctxt_args C D)"
using assms by (induct) (auto simp: length_concat intro!: arg_cong [of _ _ sum_list] nth_equalityI)
lemma sup_gmctxt_sup_gmctxt_args:
assumes "(C, D) ∈ comp_gmctxt"
shows "fill_gholes_gmctxt C (sup_gmctxt_args C D) = C ⊔ D" using assms
proof (induct)
note fill_gholes_gmctxt.simps [simp del]
case (GMFun f g Cs Ds)
then show ?case
proof (cases "f = g ∧ length Cs = length Ds")
case True
with GMFun have "∀i < length Cs.
fill_gholes_gmctxt (Cs ! i) (sup_gmctxt_args (Cs ! i) (Ds ! i)) = Cs ! i ⊔ Ds ! i"
and *: "∀i < length Cs. (Cs ! i, Ds ! i) ∈ comp_gmctxt" by (force simp: set_zip)+
moreover have "partition_gholes (concat (map (case_prod sup_gmctxt_args) (zip Cs Ds)))
Cs = map (case_prod sup_gmctxt_args) (zip Cs Ds)"
using True and * by (intro partition_by_concat_id) (auto simp: num_gholes_sup_gmctxt_args)
ultimately show ?thesis
using * and True by (auto simp: partition_holes_fill_gholes_gmctxt_conv intro!: nth_equalityI)
qed auto
qed auto
lemma eqgf_comp_gmctxt:
assumes "s =⇩G⇩f (C, ss)" and "s =⇩G⇩f (D, ts)"
shows "(C, D) ∈ comp_gmctxt" using assms
proof (induct s arbitrary: C D ss ts)
case (GFun f ss C D us vs)
{ fix Cs and Ds
assume *: "C = GMFun f Cs" "D = GMFun f Ds" and **: "length Cs = length Ds"
have ?case
proof (unfold *, intro comp_gmctxt.GMFun [OF refl **] allI impI)
fix i
assume "i < length Ds" then show "(Cs ! i, Ds ! i) ∈ comp_gmctxt"
using GFun by (auto simp: * ** elim!: eqgf_GMFunE) (metis nth_mem)
qed}
from GFun.prems this show ?case
by (cases C D rule: gmctxt.exhaust [case_product gmctxt.exhaust])
(auto simp: eq_gfill.simps dest: map_eq_imp_length_eq intro: comp_mctxt.intros)
qed
lemma eqgf_less_eq [simp]:
assumes "s =⇩G⇩f (C, ss)"
shows "C ≤ gmctxt_of_gterm s" using assms
by (induct rule: eq_gfill_induct) (auto simp: less_eq_gmctxt_prime)
lemma less_eq_comp_gmctxt [simp]:
"C ≤ D ⟹ (C, D) ∈ comp_gmctxt"
by (induct rule: less_eq_gmctxt_induct) auto
lemma gmctxt_less_eq_sup:
"(C :: 'f gmctxt) ≤ D ⟹ C ⊔ D = D"
by (induct rule: less_eq_gmctxt_induct) (auto intro: nth_equalityI)
lemma fill_gholes_gmctxt_less_eq:
assumes "num_gholes C = length Ds"
shows "C ≤ fill_gholes_gmctxt C Ds" using assms
proof (induct C arbitrary: Ds)
case (GMFun f Cs)
show ?case using GMFun(1)[OF nth_mem] GMFun(2)
unfolding partition_holes_fill_gholes_gmctxt_conv'
by (intro less_eq_gmctxt_intros) (auto simp: length_partition_by_nth)
qed simp
lemma less_eq_to_sup_mctxt_args [elim]:
assumes "C ≤ D"
obtains Ds where "num_gholes C = length Ds" "D = fill_gholes_gmctxt C Ds"
using assms gmctxt_less_eq_sup[OF assms]
using sup_gmctxt_sup_gmctxt_args[OF less_eq_comp_gmctxt[OF assms]]
using less_eq_comp_gmctxt num_gholes_sup_gmctxt_args
by force
lemma fill_gholes_gmctxt_sup_mctxt_args [simp]:
assumes "num_gholes C = length Ds"
shows "sup_gmctxt_args C (fill_gholes_gmctxt C Ds) = Ds" using assms
proof (induct C arbitrary: Ds)
case GMHole then show ?case
by (cases Ds) auto
next
case (GMFun f Cs)
have "map2 sup_gmctxt_args Cs (map2 fill_gholes_gmctxt Cs (partition_gholes Ds Cs)) = partition_gholes Ds Cs"
using GMFun(1)[OF nth_mem] GMFun(2)
by (auto simp: length_partition_by_nth intro!: nth_equalityI)
then show ?case using GMFun(1)[OF nth_mem] GMFun(2)
unfolding partition_holes_fill_gholes_gmctxt_conv'
using concat_partition_by[of "map num_gholes Cs" Ds]
by auto
qed
lemma map2_fill_gholes_gmctxt_id [simp]:
assumes "⋀ i. i < length Ds ⟹ num_gholes (Ds ! i) = 0"
shows "map2 fill_gholes_gmctxt Ds (replicate (length Ds) []) = Ds"
using assms fill_gholes_gmctxt_no_holes[of "Ds ! i" for i]
by (auto simp: map_nth_eq_conv)
lemma fill_gholes_gmctxt_GMFun_replicate_append [simp]:
assumes "length Cs = n" and "⋀ t. t ∈ set Ds ⟹ num_gholes t = 0"
shows "fill_gholes_gmctxt (GMFun f ((replicate n GMHole) @ Ds)) Cs = GMFun f (Cs @ Ds)" using assms
proof (induct n arbitrary: Cs)
case 0 note [simp] = 0(1)
have "i < length Ds ⟹ num_gholes (Ds ! i) = 0" for i using 0 by fastforce
then show ?case using 0 unfolding partition_holes_fill_gholes_gmctxt_conv'
by (cases Cs) auto
next
case (Suc n) then show ?case unfolding partition_holes_fill_gholes_gmctxt_conv'
by (simp add: Cons_nth_drop_Suc take_Suc_conv_app_nth)
qed
subsection ‹Hole positions lemmas›
lemma finite_ghole_poss:
"finite (ghole_poss C)"
by (induct C) auto
lemma ghole_poss_simp [simp]:
"ghole_poss (GMFun f cs) = {i # p | i p. i < length cs ∧ p ∈ ghole_poss (cs ! i)}" by auto
declare ghole_poss.simps(2)[simp del]
lemma num_gholes_zero_ghole_poss:
"num_gholes D = 0 ⟹ ghole_poss D = {}"
by (induct D) auto
lemma ghole_poss_num_gholes_zero:
"ghole_poss D = {} ⟹ num_gholes D = 0"
proof (induct D)
case (GMFun f Ds)
then show ?case
by (simp, metis Collect_empty_eq Collect_mem_eq in_set_idx)
qed simp
lemma num_ghloes_nzero_ghole_poss_nempty:
"num_gholes D ≠ 0 ⟹ ghole_poss D ≠ {}"
by (induct D) (auto simp: in_set_conv_nth, fastforce)
lemma ghole_poss_epsE [elim]:
"ghole_poss D = {[]} ⟹ D = GMHole"
by (induct D) auto
lemma ghole_poss_gmctxt_of_gterm [simp]:
"ghole_poss (gmctxt_of_gterm t) = {}"
by (induct t) auto
lemma ghole_poss_subseteq_args [simp]:
assumes "ghole_poss (GMFun f Ds) ⊆ ghole_poss (GMFun g Cs)"
shows "∀ i < min (length Ds) (length Cs). ghole_poss (Ds ! i) ⊆ ghole_poss (Cs ! i)" using assms
by auto
lemma factor_ghole_pos_by_prefix:
assumes "C ≤ D" "p ∈ ghole_poss D"
obtains q where "q ≤⇩p p" "q ∈ ghole_poss C"
using assms
by (induct C D arbitrary: p thesis rule: less_eq_gmctxt_induct)
(auto, metis less_eq_pos_simps(4))
lemma prefix_and_fewer_gholes_implies_equal_gmctxt:
"C ≤ D ⟹ ghole_poss C ⊆ ghole_poss D ⟹ C = D"
proof (induct C D rule: less_eq_gmctxt_induct)
case (1 D) then show ?case by (cases D) auto
next
case (2 Cs Ds f)
have "i < length Ds ⟹ ghole_poss (Cs ! i) ⊆ ghole_poss (Ds ! i)" for i using 2(1,4) by auto
then show ?case using 2 by (auto intro!: nth_equalityI)
qed
lemma set_sup_gmctxt_args_split:
"length Cs = length Ds ⟹ set (sup_gmctxt_args (GMFun f Cs) (GMFun f Ds)) =
(⋃ i ∈ {0..< length Ds}. set (sup_gmctxt_args (Cs ! i) (Ds ! i)))"
by (auto simp: atLeast0LessThan in_set_zip)
(metis length_map map_fst_zip nth_mem nth_zip)
lemma gmctxt_closing_trans:
"gmctxt_closing C D ⟹ gmctxt_closing D E ⟹ gmctxt_closing C E"
unfolding gmctxt_closing_def using less_eq_gmctxt_prime
by (metis (full_types) order_trans)
lemma gmctxt_closing_sup_args_ghole_or_gterm:
assumes "gmctxt_closing C D"
shows "∀ E ∈ set (sup_gmctxt_args C D). E = GMHole ∨ num_gholes E = 0"
using assms unfolding gmctxt_closing_def
proof -
from assms have "C ≤ D" "ghole_poss D ⊆ ghole_poss C" unfolding gmctxt_closing_def
by (auto simp: less_eq_gmctxt_prime)
then show ?thesis
proof (induct rule: less_eq_gmctxt_induct)
case (1 D)
then show ?case
by (cases D) (auto simp: in_set_conv_nth intro!: ghole_poss_num_gholes_zero, blast)
next
case (2 cs ds f) note IS = this
show ?case using IS set_sup_gmctxt_args_split[OF IS(1)]
by auto
qed
qed
lemma inv_imples_ghole_poss_subseteq:
"C ≤ D ⟹ ∀ E ∈ set (sup_gmctxt_args C D). E = GMHole ∨ num_gholes E = 0 ⟹ ghole_poss D ⊆ ghole_poss C"
proof (induct rule: less_eq_gmctxt_induct)
case (1 D) then show ?case
by (cases D) (auto simp: num_gholes_zero_ghole_poss)
next
case (2 cs ds f)
then show ?case using set_sup_gmctxt_args_split[OF 2(1)]
by auto (metis (no_types, lifting) fst_conv in_set_zip snd_conv subsetD)
qed
lemma fill_gholes_gmctxt_ghole_poss_subseteq:
assumes "num_gholes C = length Ds" "∀ i < length Ds. Ds ! i = GMHole ∨ num_gholes (Ds ! i) = 0"
shows "ghole_poss (fill_gholes_gmctxt C Ds) ⊆ ghole_poss C" using assms
proof (induct rule: fill_gholes_induct)
case (GMFun f Cs xs)
then show ?case unfolding partition_holes_fill_gholes_gmctxt_conv'
by auto (metis (no_types, lifting) length_map length_partition_by_nth partition_by_nth_nth(1, 2) subsetD)
qed (auto simp: num_gholes_zero_ghole_poss)
lemma ghole_poss_not_in_poss_gmctxt:
assumes "p ∈ ghole_poss C"
shows "p ∉ poss_gmctxt C" using assms
by (induct C arbitrary: p) auto
lemma comp_gmctxt_inf_ghole_poss_cases:
assumes "(C, D) ∈ comp_gmctxt" "p ∈ ghole_poss (C ⊓ D)"
shows "p ∈ ghole_poss C ∧ p ∈ ghole_poss D ∨
p ∈ ghole_poss C ∧ p ∈ poss_gmctxt D ∨
p ∈ ghole_poss D ∧ p ∈ poss_gmctxt C" using assms
proof (induct arbitrary: p)
case (GMHole1 D) then show ?case
by (cases D) auto
next
case (GMHole2 C) then show ?case
by (cases C) auto
next
case (GMFun f g Cs Ds)
then show ?case
by (auto simp: atLeast0LessThan) blast+
qed
subsection ‹Lemmas about ghole_poss_list and connection to ghole_poss›
lemma length_ghole_poss_list_num_gholes:
"num_gholes C = length (ghole_poss_list C)"
by (induct C) (auto simp: length_concat intro: nth_sum_listI)
lemma ghole_poss_list_distict:
"distinct (ghole_poss_list C)"
proof (induct C)
case (GMFun f Cs)
then show ?case proof (induct Cs rule: rev_induct)
case (snoc x xs)
then have "distinct (ghole_poss_list (GMFun f xs))" "distinct (ghole_poss_list x)" by auto
then show ?case using snoc by (auto simp add: map_cons_presv_distinct dest: set_zip_leftD)
qed auto
qed auto
lemma ghole_poss_ghole_poss_list_conv:
"ghole_poss C = set (ghole_poss_list C)"
proof (induct C)
case (GMFun f Cs) note IS = GMFun[OF nth_mem]
{fix p assume "p ∈ ghole_poss (GMFun f Cs)"
then obtain i ps where w: "p = i # ps" "i < length Cs"
"ps ∈ ghole_poss (Cs ! i)" by auto
then have "(i, Cs ! i) ∈ set (zip [0..<length Cs] Cs)"
by (force simp: in_set_zip)
then have "p ∈ set (ghole_poss_list (GMFun f Cs))" using IS[of i] w
by auto}
then show ?case using IS
by (auto simp: in_set_zip)
qed auto
lemma card_ghole_poss_num_gholes:
"card (ghole_poss C) = num_gholes C"
unfolding ghole_poss_ghole_poss_list_conv
unfolding length_ghole_poss_list_num_gholes
using ghole_poss_list_distict
using distinct_card by blast
subsection ‹Subterms at position of multihole contexts›
lemma subgm_at_hole_poss [simp]:
"p ∈ ghole_poss C ⟹ subgm_at C p = GMHole"
by (induct C arbitrary: p) auto
lemma subgm_at_mctxt_of_term:
"p ∈ gposs t ⟹ subgm_at (gmctxt_of_gterm t) p = gmctxt_of_gterm (gsubt_at t p)"
by (induct t arbitrary: p) auto
lemma num_gholes_subgm_at:
assumes "p ∈ poss_gmctxt C"
shows "num_gholes (subgm_at C p) = ghole_num_at_pos p C" using assms
by (induct C arbitrary: p) auto
lemma gmctxt_subtgm_at_fill_args_empty_pos [simp]:
assumes "num_gholes C = length ts"
shows "gmctxt_subtgm_at_fill_args [] C ts = ts"
using assms by (auto simp: gmctxt_subtgm_at_fill_args_def)
lemma ghole_num_bef_at_pos_num_gholes_less_eq:
assumes "p ∈ poss_gmctxt C"
shows "ghole_num_bef_pos p C + ghole_num_at_pos p C ≤ num_gholes C" using assms
proof (induct C arbitrary: p)
case (GMFun f Cs)
show ?case
proof (cases p)
case (Cons i ps)
have *: "num_gholes (GMFun f Cs) = sum_list (map num_gholes (take i Cs)) + num_gholes (Cs ! i) + sum_list (map num_gholes (drop (Suc i) Cs))"
using GMFun(2) unfolding Cons
by (auto simp flip: take_map take_drop)
(metis ab_semigroup_add_class.add_ac(1) id_take_nth_drop map_append_Cons sum_list.Cons sum_list.append take_map)
from Cons have
"(sum_list (map num_gholes (take i Cs)) + (ghole_num_bef_pos ps (Cs ! i) + ghole_num_at_pos ps (Cs ! i)))
+ sum_list (map num_gholes (drop (Suc i) Cs)) ≤
(sum_list (map num_gholes (take i Cs)) + num_gholes (Cs ! i)) + sum_list (map num_gholes (drop (Suc i) Cs))"
using GMFun(1)[OF nth_mem, of i ps] GMFun(2)
by auto
from add_le_imp_le_right[OF this] show ?thesis using GMFun(2) *
unfolding Cons
by simp
qed auto
qed auto
lemma ghole_num_at_pos_fill_args_length:
assumes "p ∈ poss_gmctxt C" "num_gholes C = length ts"
shows "ghole_num_at_pos p C = length (gmctxt_subtgm_at_fill_args p C ts)"
using ghole_num_bef_at_pos_num_gholes_less_eq[OF assms(1)] assms(2)
by (auto simp: gmctxt_subtgm_at_fill_args_def)
lemma ghole_poss_nth_subt_at:
assumes "t =⇩G⇩f (C, ts)" and "p ∈ ghole_poss C"
shows "ghole_num_bef_pos p C < length ts ∧ gsubt_at t p = ts ! ghole_num_bef_pos p C" using assms
proof (induct arbitrary: p rule: eq_gfill_induct)
case (GMFun f ss Cs ts)
let ?ts = "partition_gholes ts Cs"
from GMFun obtain i and q where [simp]: "p = i # q"
and "i < length ss" and "q ∈ ghole_poss (Cs ! i)" by auto
with GMFun.hyps have "ss ! i =⇩G⇩f (Cs ! i, ?ts ! i)"
and j: "ghole_num_bef_pos q (Cs ! i) < length (?ts ! i)" (is "?j < length _")
and *: "?ts ! i ! ghole_num_bef_pos q (Cs ! i) = gsubt_at (ss ! i) q"
by auto
let ?k = "sum_list (map length (take i ?ts)) + ?j"
have "i < length ?ts" using ‹i < length ss› and GMFun by auto
with partition_by_nth_nth_old [OF this j] and GMFun and concat_nth_length [OF this j]
have "?ts ! i ! ?j = ts ! ?k" and "?k < length ts" by (auto)
moreover with * have "ts ! ?k = gsubt_at (GFun f ss) p" using ‹i < length ss› by simp
ultimately show ?case using GMFun.hyps(2) by (auto simp: take_map [symmetric])
qed auto
lemma poss_gmctxt_fill_gholes_split:
assumes "t =⇩G⇩f (C, ts)" and "p ∈ poss_gmctxt C"
shows "gsubt_at t p =⇩G⇩f (subgm_at C p , gmctxt_subtgm_at_fill_args p C ts)"
using assms
proof (induct arbitrary: p rule: eq_gfill_induct)
case (GMFun f ss Cs ts)
let ?ts = "partition_gholes ts Cs"
from GMFun have "⋀ i. i < length Cs ⟹ ss ! i =⇩G⇩f (Cs ! i, ?ts ! i)" by auto
show ?case
proof (cases p)
case Nil
then have "GFun f ss =⇩G⇩f (GMFun f Cs, concat ?ts)" using GMFun
by (intro eqgf_GMFunI) (auto simp del: fill_gholes.simps)
then show ?thesis using GMFun unfolding Nil
by simp
next
case (Cons i q)
then have "ghole_num_at_pos q (Cs ! i) ≤ num_gholes (Cs ! i) - ghole_num_bef_pos q (Cs ! i)"
using GMFun(1, 2, 4) ghole_num_bef_at_pos_num_gholes_less_eq[of q "Cs ! i"]
by auto
then show ?thesis using GMFun
by (auto simp: Cons add.commute gmctxt_subtgm_at_fill_args_def partition_by_nth drop_take take_map min_def split!: if_splits)
qed
qed auto
lemma fill_gholes_ghole_poss:
assumes "t =⇩G⇩f (C, ts)" and "i < length ts"
shows "gsubt_at t (ghole_poss_list C ! i) = ts ! i" using assms
proof (induct arbitrary: i rule: eq_gfill_induct)
case (GMFun f ss Cs ts)
have *: "length (concat (poss_rec ghole_poss_list Cs)) = num_gholes (GMFun f Cs)"
using GMFun(1, 2, 4)
unfolding length_ghole_poss_list_num_gholes[of "GMFun f Cs", symmetric, unfolded ghole_poss_list.simps]
by auto
from GMFun have b: "i < length (concat (partition_gholes ts Cs))" by simp
then have ts: "ts ! i = (λ (j, k). partition_gholes ts Cs ! j ! k) (concat_index_split (0, i) (partition_gholes ts Cs))"
by (metis GMFun.hyps(2) concat_index_split_sound concat_partition_by)
obtain o_idx i_idx where csp: "concat_index_split (0, i) (partition_gholes ts Cs) = (o_idx, i_idx)"
using old.prod.exhaust by blast
have idx: "o_idx < length Cs" "i_idx < length (partition_gholes ts Cs ! o_idx)"
using concat_index_split_sound_bounds[OF b csp] by auto
have "concat_index_split (0, i) (poss_rec ghole_poss_list Cs) = (o_idx, i_idx)"
using GMFun(1, 2, 4) * unfolding csp[symmetric]
by (intro concat_index_split_unique, unfold *)
(auto, simp add: length_ghole_poss_list_num_gholes length_partition_gholes_nth)
then have gp: "ghole_poss_list (GMFun f Cs) ! i = poss_rec ghole_poss_list Cs ! o_idx ! i_idx"
by (simp add: "*" GMFun.hyps(2) GMFun.prems concat_index_split_less_length_concat(4))
from idx GMFun have r: "o_idx < length (zip [0..<length ss] Cs)" by auto
then show ?case using GMFun idx unfolding ts csp gp
by (auto simp: nth_map[OF r] length_ghole_poss_list_num_gholes length_partition_gholes_nth split: prod.splits)
qed auto
subsection ‹Unfill holes lemmas›
lemma length_unfill_gholes [simp]:
assumes "C ≤ gmctxt_of_gterm t"
shows "length (unfill_gholes C t) = num_gholes C"
using assms
proof (induct C t rule: unfill_gholes.induct)
case (2 f Cs g ts) with 2(1)[OF _ nth_mem] 2(2) show ?case
by (auto simp: less_eq_gmctxt_def length_concat
intro!: cong[of sum_list, OF refl] nth_equalityI elim!: nth_equalityE)
qed (auto simp: less_eq_mctxt_def)
lemma fill_gholes_arbitrary:
assumes lCs: "length Cs = length ts"
and lss: "length ss = length ts"
and rec: "⋀ i. i < length ts ⟹ num_gholes (Cs ! i) = length (ss ! i) ∧ f (Cs ! i) (ss ! i) = ts ! i"
shows "map (λi. f (Cs ! i) (partition_gholes (concat ss) Cs ! i)) [0 ..< length Cs] = ts"
proof -
have "sum_list (map num_gholes Cs) = length (concat ss)" using assms
by (auto simp: length_concat map_nth_eq_conv intro: arg_cong[of _ _ "sum_list"])
moreover have "partition_gholes (concat ss) Cs = ss"
using assms by (auto intro: partition_by_concat_id)
ultimately show ?thesis using assms by (auto intro: nth_equalityI)
qed
lemma fill_unfill_gholes:
assumes "C ≤ gmctxt_of_gterm t"
shows "fill_gholes C (unfill_gholes C t) = t"
using assms
proof (induct C t rule: unfill_gholes.induct)
case (2 f Cs g ts) with 2(1)[OF _ nth_mem] 2(2) show ?case
by (auto simp: less_eq_gmctxt_def unfill_gholes_conv intro!: fill_gholes_arbitrary elim!: nth_equalityE)
qed (auto simp: less_eq_mctxt_def split: if_splits)
subsubsection ‹signature induced by a mctxt/gmctxt›
lemma funas_gmctxt_of_mctxt [simp]:
"ground_mctxt C ⟹ funas_gmctxt (gmctxt_of_mctxt C) = funas_mctxt C"
by (induct C) (auto simp: funas_gterm_gterm_of_term)
lemma funas_mctxt_of_gmctxt_conv:
"funas_mctxt (mctxt_of_gmctxt C) = funas_gmctxt C"
by (induct C) (auto simp flip: funas_gterm_gterm_of_term)
lemma funas_gterm_ctxt_apply [simp]:
assumes "num_gholes C = length ss"
shows "funas_gterm (fill_gholes C ss) = funas_gmctxt C ∪ ⋃ (set (map funas_gterm ss))" using assms
proof (induct rule: fill_gholes_induct)
case (GMFun f Cs ss)
show ?case using GMFun partition_gholes_subseteq[OF GMFun(1)]
by (auto simp add: Un_Union_image simp del: map_partition_by_nth)
qed simp
lemma funas_gmctxt_gmctxt_of_gterm [simp]:
"funas_gmctxt (gmctxt_of_gterm s) = funas_gterm s"
by (induct s) auto
lemma funas_gmctxt_replicate_GMHole [simp]:
"funas_gmctxt (GMFun f (replicate n GMHole)) = {(f, n)}"
by auto
lemma funas_gmctxt_gmctxt_of_gctxt [simp]:
"funas_gmctxt (gmctxt_of_gctxt C) = funas_gctxt C"
by (induct C) auto
lemma funas_gmctxt_fill_gholes_gmctxt [simp]:
assumes "num_gholes C = length Ds"
shows "funas_gmctxt (fill_gholes_gmctxt C Ds) = funas_gmctxt C ∪ ⋃(set (map funas_gmctxt Ds))"
(is "?f C Ds = ?g C Ds") using assms
proof (induct C arbitrary: Ds)
case GMHole then show ?case by (cases Ds) simp_all
next
case (GMFun f Cs)
then have num_gholes: "sum_list (map num_gholes Cs) = length Ds" by simp
let ?ys = "partition_gholes Ds Cs"
have "⋀i. i < length Cs ⟹ ?f (Cs ! i) (?ys ! i) = ?g (Cs ! i) (?ys ! i)"
by (simp add: GMFun.hyps length_partition_by_nth num_gholes)
then have "(⋃i ∈ {0 ..< length Cs}. ?f (Cs ! i) (?ys ! i)) =
(⋃i ∈ {0 ..< length Cs}. ?g (Cs ! i) (?ys ! i))" by simp
then show ?case
using num_gholes unfolding partition_holes_fill_holes_mctxt_conv
by (simp add: UN_Un_distrib UN_upt_len_conv [of _ _ "λx. ⋃(set x)"] UN_set_partition_by_map)
qed
lemma funas_supremum:
"C ≤ D ⟹ funas_gmctxt D = funas_gmctxt C ∪ ⋃ (set (map funas_gmctxt (sup_gmctxt_args C D)))"
using fill_gholes_gmctxt_sup_mctxt_args[of C]
by (auto simp: fill_gholes_gmctxt_sup_mctxt_args[of C] elim!: less_eq_to_sup_mctxt_args[of C D])
lemma funas_gctxt_gctxt_of_gmctxt [simp]:
"num_gholes D = Suc 0 ⟹ funas_gctxt (gctxt_of_gmctxt D) = funas_gmctxt D"
by (metis One_nat_def funas_gmctxt_gmctxt_of_gctxt gmctxt_of_gctxt_gctxt_of_gmctxt)
lemma funas_gterm_gterm_of_gmctxt [simp]:
"num_gholes C = 0 ⟹ funas_gterm (gterm_of_gmctxt C) = funas_gmctxt C"
by (metis funas_gmctxt_gmctxt_of_gterm no_gholes_gmctxt_of_gterm_gterm_of_gmctxt_id)
lemma less_sup_gmctxt_args_funas_gmctxt:
"C ≤ D ⟹ funas_gmctxt C ⊆ ℱ ⟹ ∀ Ds ∈ set (sup_gmctxt_args C D). funas_gmctxt Ds ⊆ ℱ ⟹ funas_gmctxt D ⊆ ℱ"
using funas_supremum[of C D] by auto
lemma funas_gmctxt_poss_gmctxt_subgm_at_funas:
assumes "funas_gmctxt C ⊆ ℱ" "p ∈ poss_gmctxt C"
shows "funas_gmctxt (subgm_at C p) ⊆ ℱ"
using assms
proof (induct C arbitrary: p)
case (GMFun f Cs)
then show ?case
by (auto, blast) (metis SUP_le_iff nth_mem subsetD)
qed auto
lemma inf_funas_gmctxt_subset1:
"funas_gmctxt (C ⊓ D) ⊆ funas_gmctxt C"
using funas_supremum[of C "C ⊓ D"]
by (metis funas_supremum inf_le1 le_sup_iff order_refl)
lemma inf_funas_gmctxt_subset2:
"funas_gmctxt (C ⊓ D) ⊆ funas_gmctxt D"
using funas_supremum[of D "C ⊓ D"]
by (metis funas_supremum inf_le2 le_sup_iff order_refl)
end