Theory Ground_MCtxt

theory Ground_MCtxt
  imports
   Multihole_Context
   Regular_Tree_Relations.Ground_Terms
   Regular_Tree_Relations.Ground_Ctxt
begin

subsection ‹Ground multihole context›

datatype (gfuns_mctxt: 'f) gmctxt = GMHole | GMFun 'f "'f gmctxt list"

subsubsection ‹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 = Suc 0"
| "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 term_of_gmctxt :: "'f gmctxt ⇒ ('f, 'v) term" where
  "term_of_gmctxt (GMFun f Cs) = Fun f (map term_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 = length (takeWhile (λ 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 where
  "funas_gmctxt (GMFun f Cs) = {(f, length Cs)} ∪ ⋃(funas_gmctxt ` set Cs)" |
  "funas_gmctxt _ = {}"

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]))"

subsubsection ‹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]))"

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

subsubsection ‹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)"

subsubsection ‹Conversions from and to ground multihole contexts›

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) = Suc 0"
  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

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)

lemma no_gholes_term_of_gterm_gterm_of_gmctxt [simp]:
  "num_gholes C = 0 ⟹ term_of_gterm (gterm_of_gmctxt C) = term_of_gmctxt C"
  by (induct C) (auto simp: comp_def intro: nth_equalityI)

lemma no_gholes_term_of_mctxt_mctxt_of_gmctxt [simp]:
  "num_gholes C = 0 ⟹ term_of_mctxt (mctxt_of_gmctxt C) = term_of_gmctxt C"
  by (induct C) (auto simp: comp_def intro: nth_equalityI)

lemma nthWhile_gmctxt_of_gctxt [simp]:
  "length (takeWhile (λ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 ⟹ length (takeWhile (λ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 = Suc 0 ⟹ gmctxt_of_gctxt (gctxt_of_gmctxt C) = C"
proof (induct C)
  case (GMFun f Cs)
  then obtain i where nth: "i < length Cs" "i = length (takeWhile (λC. num_gholes C = 0) Cs)"
    using sum_list_nthWhile_length by auto
  then have "0 < num_gholes (Cs ! i)" unfolding nth(2) using nth_length_takeWhile
    by auto
  from nth(1) this have num: "num_gholes (Cs ! i) = Suc 0" 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 = Suc 0))"
  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)

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

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


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)

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 = Suc 0 ⟹ fill_gholes C [s] = (gctxt_of_gmctxt C)⟨s⟩⇩G"
  by (simp add: apply_gctxt_fill_gholes gmctxt_of_gctxt_gctxt_of_gmctxt)


lemma ctxt_of_gctxt_gctxt_of_gmctxt_apply:
  "num_gholes C = Suc 0 ⟹ fill_holes (mctxt_of_gmctxt C) [s] = (ctxt_of_gctxt (gctxt_of_gmctxt C))⟨s⟩"
proof (induct C)
  case (GMFun f Cs)
  obtain i where split: "i < length Cs" "num_gholes (Cs ! i) = Suc 0"
    "∀ j < length Cs. j ≠ i ⟶ num_gholes (Cs ! j) = 0" using GMFun(2)
    by auto
  then have [simp]: "sum_list (take i (map num_gholes Cs)) = 0"
    by (auto simp: sum_list_eq_0_iff dest: set_take_nth)
  from split have [simp]: "j < length Cs ⟹ j ≠ i ⟹
     fill_holes (mctxt_of_gmctxt (Cs ! j)) [] = term_of_mctxt (mctxt_of_gmctxt (Cs ! j))" for j
    by (intro fill_holes_term_of_mctxt) auto
  from split have [simp]: "gctxt_of_gmctxt (GMFun f Cs) =
    GMore f (map gterm_of_gmctxt (take i Cs)) (gctxt_of_gmctxt (Cs ! i)) (map gterm_of_gmctxt (drop (Suc i) Cs))"
     using nth_length_takeWhile GMFun(2) sum_list_nthWhile_length by (auto simp: Let_def)
  show ?case using GMFun(1)[OF nth_mem[OF split(1)] split(2)] split
    by (auto simp: min_def nth_append_Cons partition_by_nth simp del: gctxt_of_gmctxt.simps intro!: nth_equalityI)
qed auto


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

subsubsection ‹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

definition "(C :: 'a gmctxt) ≤ D ⟷ C ⊓ 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 (verit, del_insts) length_map length_zip map_nth_eq_conv min_less_iff_conj not_gr0 nth_mem nth_zip o_apply prod.simps(2) 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)
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

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 position_less_eq_Cons)

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

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

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 Cons_nth_drop_Suc add.assoc append_take_drop_id drop_map length_map nth_map sum_list.Cons sum_list.append)
    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

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

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 split: if_splits)

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