Theory TA_Clousure_Const

section ‹(Multihole)Context closure of recognized tree languages›

theory TA_Clousure_Const
  imports Tree_Automata_Derivation_Split
begin


subsection ‹Tree Automata closure constructions›
declare ta_union_def [simp]
subsubsection ‹Reflexive closure over a given signature›

definition "reflcl_rules ℱ q ≡ (λ (f, n). TA_rule f (replicate n q) q) |`| ℱ"
definition "refl_ta ℱ q = TA (reflcl_rules ℱ q) {||}"

definition gen_reflcl_automaton :: "('f × nat) fset ⇒ ('q, 'f) ta ⇒ 'q ⇒ ('q, 'f) ta" where
  "gen_reflcl_automaton ℱ 𝒜 q = ta_union 𝒜 (refl_ta ℱ q)"

definition "reflcl_automaton ℱ 𝒜 = (let ℬ = fmap_states_ta Some 𝒜 in
   gen_reflcl_automaton ℱ ℬ None)"

definition "reflcl_reg ℱ 𝒜 = Reg (finsert None (Some |`| fin 𝒜)) (reflcl_automaton ℱ (ta 𝒜))"

subsubsection ‹Multihole context closure over a given signature›

definition "refl_over_states_ta Q ℱ 𝒜 q = TA (reflcl_rules ℱ q) ((λ p. (p, q)) |`| (Q |∩| 𝒬 𝒜))"

definition gen_parallel_closure_automaton :: "'q fset ⇒ ('f × nat) fset ⇒ ('q, 'f) ta ⇒ 'q ⇒ ('q, 'f) ta" where
  "gen_parallel_closure_automaton Q ℱ 𝒜 q = ta_union 𝒜 (refl_over_states_ta Q ℱ 𝒜 q)"

definition parallel_closure_reg where
  "parallel_closure_reg ℱ 𝒜 = (let ℬ = fmap_states_reg Some 𝒜 in
   Reg {|None|} (gen_parallel_closure_automaton (fin ℬ) ℱ (ta ℬ) None))"

subsubsection ‹Context closure of regular tree language›

definition "semantic_path_rules ℱ q⇩c q⇩i q⇩f ≡ 
  |⋃| ((λ (f, n). fset_of_list (map (λ i. TA_rule f ((replicate n q⇩c)[i := q⇩i]) q⇩f) [0..< n])) |`| ℱ)"

definition "reflcl_over_single_ta Q ℱ q⇩c q⇩f ≡
  TA (reflcl_rules ℱ q⇩c |∪| semantic_path_rules ℱ q⇩c q⇩f q⇩f) ((λ p. (p, q⇩f)) |`| Q)"

definition "gen_ctxt_closure_automaton Q ℱ 𝒜 q⇩c q⇩f = ta_union 𝒜 (reflcl_over_single_ta Q ℱ q⇩c q⇩f)"

definition "gen_ctxt_closure_reg ℱ 𝒜 q⇩c q⇩f =
   Reg {|q⇩f|} (gen_ctxt_closure_automaton (fin 𝒜) ℱ (ta 𝒜) q⇩c q⇩f)"

definition "ctxt_closure_reg ℱ 𝒜 =
  (let ℬ = fmap_states_reg Inl (reg_Restr_Q⇩f 𝒜) in
  gen_ctxt_closure_reg ℱ ℬ (Inr False) (Inr True))"


subsubsection ‹Not empty context closure of regular tree language›

datatype cl_states = cl_state | tr_state | fin_state | fin_clstate

definition "reflcl_over_nhole_ctxt_ta Q ℱ q⇩c q⇩i q⇩f ≡
  TA (reflcl_rules ℱ q⇩c |∪| semantic_path_rules ℱ q⇩c q⇩i q⇩f |∪| semantic_path_rules ℱ q⇩c q⇩f q⇩f) ((λ p. (p, q⇩i)) |`| Q)"

definition "gen_nhole_ctxt_closure_automaton Q ℱ 𝒜 q⇩c q⇩i q⇩f =
   ta_union 𝒜 (reflcl_over_nhole_ctxt_ta Q ℱ q⇩c q⇩i q⇩f)"

definition "gen_nhole_ctxt_closure_reg ℱ 𝒜 q⇩c q⇩i q⇩f =
    Reg {|q⇩f|} (gen_nhole_ctxt_closure_automaton (fin 𝒜) ℱ (ta 𝒜) q⇩c q⇩i q⇩f)"

definition "nhole_ctxt_closure_reg ℱ 𝒜 =
  (let ℬ = fmap_states_reg Inl (reg_Restr_Q⇩f 𝒜) in
  (gen_nhole_ctxt_closure_reg ℱ ℬ (Inr cl_state) (Inr tr_state) (Inr fin_state)))"

subsubsection ‹Non empty multihole context closure of regular tree language›

abbreviation "add_eps 𝒜 e ≡ TA (rules 𝒜) (eps 𝒜 |∪| e)"
definition "reflcl_over_nhole_mctxt_ta Q ℱ q⇩c q⇩i q⇩f ≡
  add_eps (reflcl_over_nhole_ctxt_ta Q ℱ q⇩c q⇩i q⇩f) {|(q⇩i, q⇩c)|}"

definition "gen_nhole_mctxt_closure_automaton Q ℱ 𝒜 q⇩c q⇩i q⇩f =
   ta_union 𝒜 (reflcl_over_nhole_mctxt_ta Q ℱ q⇩c q⇩i q⇩f)"

definition "gen_nhole_mctxt_closure_reg ℱ 𝒜 q⇩c q⇩i q⇩f = 
   Reg {|q⇩f|} (gen_nhole_mctxt_closure_automaton (fin 𝒜) ℱ (ta 𝒜) q⇩c q⇩i q⇩f)"

definition "nhole_mctxt_closure_reg ℱ 𝒜 =
  (let ℬ = fmap_states_reg Inl (reg_Restr_Q⇩f 𝒜) in
  (gen_nhole_mctxt_closure_reg ℱ ℬ (Inr cl_state) (Inr tr_state) (Inr fin_state)))"

subsubsection ‹Not empty multihole context closure of regular tree language›

definition "gen_mctxt_closure_reg ℱ 𝒜 q⇩c q⇩i q⇩f =
   Reg {|q⇩f, q⇩i|} (gen_nhole_mctxt_closure_automaton (fin 𝒜) ℱ (ta 𝒜) q⇩c q⇩i q⇩f)"

definition "mctxt_closure_reg ℱ 𝒜 =
  (let ℬ = fmap_states_reg Inl (reg_Restr_Q⇩f 𝒜) in
  (gen_mctxt_closure_reg ℱ ℬ (Inr cl_state) (Inr tr_state) (Inr fin_state)))"


subsubsection ‹Multihole context closure of regular tree language›

definition "nhole_mctxt_reflcl_reg ℱ 𝒜 =
  reg_union (nhole_mctxt_closure_reg ℱ 𝒜) (Reg {|fin_clstate|} (refl_ta ℱ (fin_clstate)))"

subsubsection ‹Lemmas about @{const ta_der'}›

lemma ta_det'_ground_id:
  "t |∈| ta_der' 𝒜 s ⟹ ground t ⟹ t = s"
  by (induct s arbitrary: t) (auto simp add: ta_der'.simps nth_equalityI)

lemma ta_det'_vars_term_id:
  "t |∈| ta_der' 𝒜 s ⟹ vars_term t ∩ fset (𝒬 𝒜) = {} ⟹ t = s"
proof (induct s arbitrary: t)
  case (Fun f ss)
  from Fun(2-) obtain ts where [simp]: "t = Fun f ts" and len: "length ts = length ss"
    by (cases t) (auto dest: rule_statesD eps_dest_all)
  from Fun(1)[OF nth_mem, of i "ts ! i" for i] show ?case using Fun(2-) len
    by (auto simp add: ta_der'.simps Union_disjoint
        dest: rule_statesD eps_dest_all intro!: nth_equalityI)
qed (auto simp add: ta_der'.simps dest: rule_statesD eps_dest_all)

lemma fresh_states_ta_der'_pres:
  assumes st: "q ∈ vars_term s" "q |∉| 𝒬 𝒜"
    and reach: "t |∈| ta_der' 𝒜 s"
  shows "q ∈ vars_term t" using reach st(1)
proof (induct s arbitrary: t)
  case (Var x)
  then show ?case using assms(2)
    by (cases t) (auto simp: ta_der'.simps dest: eps_trancl_statesD)
next
  case (Fun f ss)
  from Fun(3) obtain i where w: "i < length ss" "q ∈ vars_term (ss ! i)" by (auto simp: in_set_conv_nth)
  have "i < length (args t) ∧ q ∈ vars_term (args t ! i)" using Fun(2) w assms(2) Fun(1)[OF nth_mem[OF w(1)] _ w(2)]
    using rule_statesD(3) ta_der_to_ta_der'
    by (auto simp: ta_der'.simps dest: rule_statesD(3)) fastforce+
  then show ?case by (cases t) auto
qed

lemma ta_der'_states:
  "t |∈| ta_der' 𝒜 s ⟹ vars_term t ⊆ vars_term s ∪ fset (𝒬 𝒜)"
proof (induct s arbitrary: t)
  case (Var x) then show ?case
    by (auto simp: ta_der'.simps dest: eps_dest_all)
next
  case (Fun f ts) then show ?case
    by (auto simp: ta_der'.simps rule_statesD dest: eps_dest_all)
       (metis (no_types, opaque_lifting) Un_iff in_set_conv_nth subsetD)
qed

lemma ta_der'_gterm_states:
  "t |∈| ta_der' 𝒜 (term_of_gterm s) ⟹ vars_term t ⊆ fset (𝒬 𝒜)"
  using ta_der'_states[of t 𝒜 "term_of_gterm s"]
  by auto

lemma ta_der'_Var_funas:
  "Var q |∈| ta_der' 𝒜 s ⟹ funas_term s ⊆ fset (ta_sig 𝒜)"
  by (auto simp: less_eq_fset.rep_eq ffunas_term.rep_eq dest!: ta_der_term_sig ta_der'_to_ta_der)


lemma ta_sig_fsubsetI:
  assumes "⋀ r. r |∈| rules 𝒜 ⟹ (r_root r, length (r_lhs_states r)) |∈| ℱ"
  shows "ta_sig 𝒜 |⊆| ℱ" using assms
  by (auto simp: ta_sig_def)

subsubsection ‹Signature induced by @{const refl_ta} and @{const refl_over_states_ta}›

lemma refl_ta_sig [simp]:
  "ta_sig (refl_ta ℱ q) = ℱ"
  "ta_sig (refl_over_states_ta  Q ℱ 𝒜 q ) = ℱ"
  by (auto simp: ta_sig_def refl_ta_def reflcl_rules_def refl_over_states_ta_def image_iff Bex_def)

subsubsection ‹Correctness of @{const refl_ta}, @{const gen_reflcl_automaton}, and @{const reflcl_automaton}›

lemma refl_ta_eps [simp]: "eps (refl_ta ℱ q) = {||}"
  by (auto simp: refl_ta_def)

lemma refl_ta_sound:
  "s ∈ 𝒯⇩G (fset ℱ) ⟹ q |∈| ta_der (refl_ta ℱ q) (term_of_gterm s)"
  by (induct rule: 𝒯⇩G.induct) (auto simp: refl_ta_def reflcl_rules_def
      image_iff Bex_def)

lemma reflcl_rules_args:
  "length ps = n ⟹ f ps → p |∈| reflcl_rules ℱ q ⟹ ps = replicate n q"
  by (auto simp: reflcl_rules_def)

lemma 𝒬_refl_ta:
  "𝒬 (refl_ta ℱ q) |⊆| {|q|}"
  by (auto simp: 𝒬_def refl_ta_def rule_states_def reflcl_rules_def fset_of_list_elem)

lemma refl_ta_complete1:
  "Var p |∈| ta_der' (refl_ta ℱ q) s ⟹ p ≠ q ⟹ s = Var p"
  by (cases s) (auto simp: ta_der'.simps refl_ta_def reflcl_rules_def)

lemma refl_ta_complete2:
  "Var q |∈| ta_der' (refl_ta ℱ q) s ⟹ funas_term s ⊆ fset ℱ ∧ vars_term s ⊆ {q}"
  unfolding ta_der_to_ta_der'[symmetric]
  using ta_der_term_sig[of q "refl_ta ℱ q" s] ta_der_states'[of q "refl_ta ℱ q" s]
  using fsubsetD[OF 𝒬_refl_ta[of ℱ q]]
  by (auto simp: ffunas_term.rep_eq)
     (metis Term.term.simps(17) fresh_states_ta_der'_pres singletonD ta_der_to_ta_der')

lemma gen_reflcl_lang:
  assumes "q |∉| 𝒬 𝒜"
  shows "gta_lang (finsert q Q) (gen_reflcl_automaton ℱ 𝒜 q) = gta_lang Q 𝒜 ∪ 𝒯⇩G (fset ℱ)"
    (is "?Ls = ?Rs")
proof -
  let ?A = "gen_reflcl_automaton ℱ 𝒜 q"
  interpret sq: derivation_split ?A "𝒜" "refl_ta ℱ q"
    using assms unfolding derivation_split_def
    by (auto simp: gen_reflcl_automaton_def refl_ta_def reflcl_rules_def 𝒬_def)
  show ?thesis
  proof
    {fix s assume "s ∈ ?Ls" then obtain p u where
        seq: "u |∈| ta_der' 𝒜 (term_of_gterm s)" "Var p |∈| ta_der' (refl_ta ℱ q) u" and
        fin: "p |∈| finsert q Q"
        by (auto simp: ta_der_to_ta_der' elim!: gta_langE dest!: sq.ta_der'_split)
      have "vars_term u ⊆ {q} ⟹ u = term_of_gterm s" using assms
        by (intro ta_det'_vars_term_id[OF seq(1)]) auto
      then have "s ∈ ?Rs" using assms fin seq funas_term_of_gterm_conv
        using refl_ta_complete1[OF seq(2)]
        by (cases "p = q") (auto simp: ta_der_to_ta_der' 𝒯⇩G_funas_gterm_conv dest!: refl_ta_complete2)}
    then show "?Ls ⊆ gta_lang Q 𝒜 ∪ 𝒯⇩G (fset ℱ)" by blast
  next
    show "gta_lang Q 𝒜 ∪ 𝒯⇩G (fset ℱ) ⊆ ?Ls"
      using sq.ta_der_monos unfolding gta_lang_def gta_der_def
      by (auto dest: refl_ta_sound)
  qed
qed

lemma reflcl_lang:
  "gta_lang (finsert None (Some |`| Q)) (reflcl_automaton ℱ 𝒜) = gta_lang Q 𝒜 ∪ 𝒯⇩G (fset ℱ)"
proof -
  have st: "None |∉| 𝒬 (fmap_states_ta Some 𝒜)" by auto
  have "gta_lang Q 𝒜 = gta_lang (Some |`| Q) (fmap_states_ta Some 𝒜)"
    by (simp add: finj_Some fmap_states_ta_lang2)
  then show ?thesis
    unfolding reflcl_automaton_def Let_def gen_reflcl_lang[OF st, of "Some |`| Q" ℱ]
    by simp
qed

lemma ℒ_reflcl_reg:
  "ℒ (reflcl_reg ℱ 𝒜) = ℒ 𝒜 ∪  𝒯⇩G (fset ℱ)"
  by (simp add: ℒ_def reflcl_lang reflcl_reg_def )

subsubsection ‹Correctness of @{const gen_parallel_closure_automaton} and @{const parallel_closure_reg}›

lemma set_list_subset_nth_conv:
  "set xs ⊆ A ⟹ i < length xs ⟹ xs ! i ∈ A"
  by (metis in_set_conv_nth subset_code(1))

lemma ground_gmctxt_of_mctxt_fill_holes':
  "num_holes C = length ss ⟹ ground_mctxt C ⟹ ∀s∈set ss. ground s ⟹
   fill_gholes (gmctxt_of_mctxt C) (map gterm_of_term ss) = gterm_of_term (fill_holes C ss)"
  using ground_gmctxt_of_mctxt_fill_holes
  by (metis term_of_gterm_inv)


lemma refl_over_states_ta_eps_trancl [simp]:
  "(eps (refl_over_states_ta Q ℱ 𝒜 q))|⇧+| = eps (refl_over_states_ta Q ℱ 𝒜 q)"
proof (intro fequalityI fsubsetI)
  fix x assume "x |∈| (eps (refl_over_states_ta Q ℱ 𝒜 q))|⇧+|"
  hence "(fst x, snd x) |∈| (eps (refl_over_states_ta Q ℱ 𝒜 q))|⇧+|"
    by (metis prod.exhaust_sel)
  thus "x |∈| eps (refl_over_states_ta Q ℱ 𝒜 q)"
    by (rule ftranclE) (auto simp add: refl_over_states_ta_def image_iff Bex_def dest: ftranclD)
next
  fix x assume "x |∈| eps (refl_over_states_ta Q ℱ 𝒜 q)"
  thus "x |∈| (eps (refl_over_states_ta Q ℱ 𝒜 q))|⇧+|"
    by (metis fr_into_trancl prod.exhaust_sel)
qed

lemma refl_over_states_ta_epsD:
  "(p, q) |∈| (eps (refl_over_states_ta Q ℱ 𝒜 q)) ⟹ p |∈| Q"
  by (auto simp: refl_over_states_ta_def)

lemma refl_over_states_ta_vars_term:
  "q |∈| ta_der (refl_over_states_ta Q ℱ 𝒜 q) u ⟹ vars_term u ⊆ insert q (fset Q)"
proof (induct u)
  case (Fun f ts)
  from Fun(2) reflcl_rules_args[of _ "length ts" f _ ℱ q]
  have "i < length ts ⟹ q |∈| ta_der (refl_over_states_ta Q ℱ 𝒜 q) (ts ! i)" for i
    by (fastforce simp: refl_over_states_ta_def)
  then have "i < length ts ⟹ x ∈ vars_term (ts ! i) ⟹ x = q ∨ x |∈| Q" for i x
    using Fun(1)[OF nth_mem, of i]
    by (meson insert_iff subsetD)
  then show ?case by (fastforce simp: in_set_conv_nth)
qed (auto dest: refl_over_states_ta_epsD)

lemmas refl_over_states_ta_vars_term' =
  refl_over_states_ta_vars_term[unfolded ta_der_to_ta_der' ta_der'_target_args_vars_term_conv,
    THEN set_list_subset_nth_conv, unfolded finsert.rep_eq[symmetric]]

lemma refl_over_states_ta_sound:
  "funas_term u ⊆ fset ℱ ⟹ vars_term u ⊆ insert q (fset (Q |∩| 𝒬 𝒜)) ⟹ q |∈| ta_der (refl_over_states_ta Q ℱ 𝒜 q) u"
proof (induct u)
  case (Fun f ts)
  have reach: "i < length ts ⟹ q |∈| ta_der (refl_over_states_ta Q ℱ 𝒜 q) (ts ! i)" for i
    using Fun(2-) by (intro Fun(1)[OF nth_mem]) (auto simp: SUP_le_iff)
  from Fun(2) have "TA_rule f (replicate (length ts) q) q |∈| rules (refl_over_states_ta Q ℱ 𝒜 q)"
    by (auto simp: refl_over_states_ta_def reflcl_rules_def fimage_iff fBex_def)
  then show ?case using reach
    by force
qed (auto simp: refl_over_states_ta_def)


lemma gen_parallelcl_lang:
  fixes 𝒜 :: "('q, 'f) ta"
  assumes "q |∉| 𝒬 𝒜"
  shows "gta_lang {|q|} (gen_parallel_closure_automaton Q ℱ 𝒜 q) =
    {fill_gholes C ss | C ss. num_gholes C = length ss ∧ funas_gmctxt C ⊆ (fset ℱ) ∧ (∀ i < length ss. ss ! i ∈ gta_lang Q 𝒜)}"
    (is "?Ls = ?Rs")
proof -
  let ?A = "gen_parallel_closure_automaton Q ℱ 𝒜 q" let ?B = "refl_over_states_ta Q ℱ 𝒜 q"
  interpret sq: derivation_split "?A" "𝒜" "?B"
    using assms unfolding derivation_split_def
    by (auto simp: gen_parallel_closure_automaton_def refl_over_states_ta_def 𝒬_def reflcl_rules_def)
  {fix s assume "s ∈ ?Ls" then obtain u where
      seq: "u |∈| ta_der' 𝒜 (term_of_gterm s)" "Var q |∈| ta_der'?B u" and
      fin: "q |∈| finsert q Q"
      by (auto simp: ta_der_to_ta_der' elim!: gta_langE dest!: sq.ta_der'_split)
    let ?w = "λ i. ta_der'_source_args u (term_of_gterm s) ! i"
    have "s ∈ ?Rs" using seq(1) ta_der'_Var_funas[OF seq(2)] fin
      using ground_ta_der_statesD[of "?w i" "ta_der'_target_args u ! i" 𝒜 for i] assms
      using refl_over_states_ta_vars_term'[OF seq(2)]
      using ta_der'_ground_mctxt_structure[OF seq(1)]
      by (force simp: ground_gmctxt_of_mctxt_fill_holes' ta_der'_source_args_term_of_gterm
          intro!: exI[of _ "gmctxt_of_mctxt (ta_der'_target_mctxt u)"]
          exI[of _ "map gterm_of_term (ta_der'_source_args u (term_of_gterm s))"]
          gta_langI[of "ta_der'_target_args u ! i" Q 𝒜
            "gterm_of_term (?w i)" for i])}
  then have ls: "?Ls ⊆ ?Rs" by blast
  {fix t assume "t ∈ ?Rs"
    then obtain C ss where len: "num_gholes C = length ss" and
      gr_fun: "funas_gmctxt C ⊆ fset ℱ" and
      reachA: "∀ i < length ss. ss ! i ∈ gta_lang Q 𝒜" and
      const: "t = fill_gholes C ss" by auto
    from reachA obtain qs where "length ss = length qs" "∀ i < length qs. qs ! i |∈| Q |∩| 𝒬 𝒜"
      "∀ i < length qs. qs ! i |∈| ta_der 𝒜 ((map term_of_gterm ss) ! i)"
      using Ex_list_of_length_P[of "length ss" "λ q i. q |∈| ta_der 𝒜 (term_of_gterm (ss ! i)) ∧ q |∈| Q"]
      by (metis (full_types) finterI gta_langE gterm_ta_der_states length_map map_nth_eq_conv)
    then have "q |∈| ta_der ?A (fill_holes (mctxt_of_gmctxt C) (map term_of_gterm ss))"
      using reachA len gr_fun
      apply (intro sq.mctxt_const_to_ta_der[of "mctxt_of_gmctxt C" "map term_of_gterm ss" qs q])
      subgoal by auto
      subgoal by auto
      subgoal by auto
      subgoal 
        apply (intro refl_over_states_ta_sound)
        subgoal by (subst funas_mctxt_fill_holes, auto simp: funas_mctxt_of_gmctxt_conv)
        subgoal by (auto dest!: in_set_idx)
        done
      done
    then have "t ∈ ?Ls" unfolding const
      by (simp add: fill_holes_mctxt_of_gmctxt_to_fill_gholes gta_langI len)}
  then show ?thesis using ls by blast
qed

lemma parallelcl_gmctxt_lang:
  fixes 𝒜 :: "('q, 'f) reg"
  shows "ℒ (parallel_closure_reg ℱ 𝒜) =
    {fill_gholes C ss |
      C ss. num_gholes C = length ss ∧ funas_gmctxt C ⊆ fset ℱ ∧ (∀ i < length ss. ss ! i ∈ ℒ 𝒜)}"
proof -
  have *: "gta_lang (fin (fmap_states_reg Some 𝒜)) (fmap_states_ta Some (ta 𝒜)) = gta_lang (fin 𝒜) (ta 𝒜)"
    by (simp add: finj_Some fmap_states_reg_def fmap_states_ta_lang2)
  have " None |∉| 𝒬 (fmap_states_ta Some (ta 𝒜))" by auto
  from gen_parallelcl_lang[OF this, of "fin (fmap_states_reg Some 𝒜)" ℱ] show ?thesis
    unfolding ℒ_def parallel_closure_reg_def Let_def * fmap_states_reg_def
    by (simp add: finj_Some fmap_states_ta_lang2)
qed

lemma parallelcl_mctxt_lang:
  shows "ℒ (parallel_closure_reg ℱ 𝒜) =
    {(gterm_of_term :: ('f, 'q option) term ⇒ 'f gterm) (fill_holes C (map term_of_gterm ss)) |
      C ss. num_holes C = length ss ∧ ground_mctxt C ∧ funas_mctxt C ⊆ fset ℱ ∧ (∀ i < length ss. ss ! i ∈ ℒ 𝒜)}"
  by (auto simp: parallelcl_gmctxt_lang) (metis funas_gmctxt_of_mctxt num_gholes_gmctxt_of_mctxt
      ground_gmctxt_of_gterm_of_term funas_mctxt_of_gmctxt_conv
      ground_mctxt_of_gmctxt mctxt_of_gmctxt_fill_holes num_holes_mctxt_of_gmctxt)+ 

subsubsection ‹Correctness of @{const gen_ctxt_closure_reg} and @{const ctxt_closure_reg}›

lemma semantic_path_rules_rhs:
  "r |∈| semantic_path_rules Q q⇩c q⇩i q⇩f ⟹ r_rhs r = q⇩f"
  by (auto simp: semantic_path_rules_def)

lemma reflcl_over_single_ta_transl [simp]:
  "(eps (reflcl_over_single_ta Q ℱ q⇩c q⇩f))|⇧+| = eps (reflcl_over_single_ta Q ℱ q⇩c q⇩f)"
proof (intro fequalityI fsubsetI)
  fix x assume "x |∈| (eps (reflcl_over_single_ta Q ℱ q⇩c q⇩f))|⇧+|"
  hence "(fst x, snd x) |∈| (eps (reflcl_over_single_ta Q ℱ q⇩c q⇩f))|⇧+|"
    by simp
  thus "x |∈| eps (reflcl_over_single_ta Q ℱ q⇩c q⇩f)"
    by (smt (verit, ccfv_threshold) fimageE ftranclD ftranclE prod.collapse
        reflcl_over_single_ta_def snd_conv ta.sel(2))
next
  show "⋀x. x |∈| eps (reflcl_over_single_ta Q ℱ q⇩c q⇩f) ⟹
    x |∈| (eps (reflcl_over_single_ta Q ℱ q⇩c q⇩f))|⇧+|"
    by auto
qed

lemma reflcl_over_single_ta_epsD:
  "(p, q⇩f) |∈| eps (reflcl_over_single_ta Q ℱ q⇩c q⇩f) ⟹ p |∈| Q"
  "(p, q) |∈| eps (reflcl_over_single_ta Q ℱ q⇩c q⇩f) ⟹ q = q⇩f"
  by (auto simp: reflcl_over_single_ta_def)

lemma reflcl_over_single_ta_rules_split:
  "r |∈| rules (reflcl_over_single_ta Q ℱ q⇩c q⇩f) ⟹
     r |∈| reflcl_rules ℱ q⇩c ∨ r |∈| semantic_path_rules ℱ q⇩c q⇩f q⇩f"
  by (auto simp: reflcl_over_single_ta_def)

lemma reflcl_over_single_ta_rules_semantic_path_rulesI:
  "r |∈| semantic_path_rules ℱ q⇩c q⇩f q⇩f ⟹ r |∈| rules (reflcl_over_single_ta Q ℱ q⇩c q⇩f)"
  by (auto simp: reflcl_over_single_ta_def)

lemma semantic_path_rules_fmember [intro]:
  "TA_rule f qs q |∈| semantic_path_rules ℱ q⇩c q⇩i q⇩f ⟷ (∃ n i. (f, n) |∈| ℱ ∧ i < n ∧ q = q⇩f ∧
    (qs = (replicate n q⇩c)[i := q⇩i]))" (is "?Ls ⟷ ?Rs")
  by (force simp: semantic_path_rules_def fBex_def fimage_iff fset_of_list_elem)

lemma semantic_path_rules_fmemberD:
  "r |∈| semantic_path_rules ℱ q⇩c q⇩i q⇩f ⟹ (∃ n i. (r_root r, n) |∈| ℱ ∧ i < n ∧ r_rhs r = q⇩f ∧
    (r_lhs_states r = (replicate n q⇩c)[i := q⇩i]))"
  by (cases r) (simp add: semantic_path_rules_fmember) 


lemma reflcl_over_single_ta_vars_term_q⇩c:
  "q⇩c ≠ q⇩f ⟹ q⇩c |∈| ta_der (reflcl_over_single_ta Q ℱ q⇩c q⇩f) u ⟹
    vars_term_list u = replicate (length (vars_term_list u)) q⇩c"
proof (induct u)
  case (Fun f ts)
  have "i < length ts ⟹ q⇩c |∈| ta_der (reflcl_over_single_ta Q ℱ q⇩c q⇩f) (ts ! i)" for i using Fun(2, 3)
    by (auto dest!: reflcl_over_single_ta_rules_split reflcl_over_single_ta_epsD
        reflcl_rules_args semantic_path_rules_rhs)
  then have "i < length (concat (map vars_term_list ts)) ⟹ concat (map vars_term_list ts) ! i = q⇩c" for i
    using Fun(1)[OF nth_mem Fun(2)]
    by (metis (no_types, lifting) length_map nth_concat_split nth_map nth_replicate)
  then show ?case using Fun(1)[OF nth_mem Fun(2)]
    by (metis in_set_conv_nth replicate_length_same
        vars_term_list.simps(2))
qed (auto dest: reflcl_over_single_ta_epsD simp: vars_term_list.simps)

lemma reflcl_over_single_ta_vars_term:
  "q⇩c |∉| Q ⟹ q⇩c ≠ q⇩f ⟹ q⇩f |∈| ta_der (reflcl_over_single_ta Q ℱ q⇩c q⇩f) u ⟹
   length (vars_term_list u) = n ⟹ (∃ i q. i < n ∧ q |∈| finsert q⇩f Q ∧ vars_term_list u = (replicate n q⇩c)[i := q])"
proof (induct u arbitrary: n)
  case (Var x) then show ?case
    by (intro exI[of _ 0] exI[of _ x]) (auto dest: reflcl_over_single_ta_epsD(1) simp: vars_term_list.simps)
next
  case (Fun f ts)
  from Fun(2, 3, 4) obtain qs where rule: "TA_rule f qs q⇩f |∈| semantic_path_rules ℱ q⇩c q⇩f q⇩f"
    "length qs = length ts" "∀ i < length ts. qs ! i |∈| ta_der (reflcl_over_single_ta Q ℱ q⇩c q⇩f) (ts ! i)"
    using semantic_path_rules_rhs reflcl_over_single_ta_epsD
    by (fastforce simp: reflcl_rules_def dest!: reflcl_over_single_ta_rules_split)
  from rule(1, 2) obtain i where states: "i < length ts" "qs = (replicate (length ts) q⇩c)[i := q⇩f]"
    by (auto simp: semantic_path_rules_fmember)
  then have qc: "j < length ts ⟹ j ≠ i ⟹ vars_term_list (ts ! j) = replicate (length (vars_term_list (ts ! j))) q⇩c" for j
    using reflcl_over_single_ta_vars_term_q⇩c[OF Fun(3)] rule
    by force
  from Fun(1)[OF nth_mem, of i] Fun(2, 3) rule states obtain k q where
    qf: "k <  length (vars_term_list (ts ! i))" "q |∈| finsert q⇩f Q"
    "vars_term_list (ts ! i) = (replicate (length (vars_term_list (ts ! i))) q⇩c)[k := q]"
    by (auto simp: nth_list_update split: if_splits)
  let ?l = "sum_list (map length (take i (map vars_term_list ts))) + k"
  show ?case using qc qf rule(2) Fun(5) states(1)
    apply (intro exI[of _ ?l] exI[of _ q])
    apply (auto simp: vars_term_list.simps concat_nth_length nth_list_update elim!: nth_concat_split' intro!: nth_equalityI)
       apply (metis length_replicate nth_list_update_eq nth_list_update_neq nth_replicate)+
    done
qed

lemma refl_ta_reflcl_over_single_ta_mono:
  "q |∈| ta_der (refl_ta ℱ q) t ⟹ q |∈| ta_der (reflcl_over_single_ta Q ℱ q q⇩f) t"
  by (intro ta_der_el_mono[where ?ℬ = "reflcl_over_single_ta Q ℱ q q⇩f"])
    (auto simp: refl_ta_def reflcl_over_single_ta_def)

lemma reflcl_over_single_ta_sound:
  assumes "funas_gctxt C ⊆ fset ℱ" "q |∈| Q"
  shows "q⇩f |∈| ta_der (reflcl_over_single_ta Q ℱ q⇩c q⇩f) (ctxt_of_gctxt C)⟨Var q⟩" using assms(1)
proof (induct C)
  case GHole then show ?case using assms(2)
    by (auto simp add: reflcl_over_single_ta_def)
next
  case (GMore f ss C ts)
  let ?i = "length ss" let ?n = "Suc (length ss + length ts)"
  from GMore have "(f, ?n) |∈| ℱ" by auto
  then have "f ((replicate ?n q⇩c)[?i := q⇩f]) → q⇩f |∈| rules (reflcl_over_single_ta Q ℱ q⇩c q⇩f)"
    using semantic_path_rules_fmember[of f "(replicate ?n q⇩c)[?i := q⇩f]" q⇩f ℱ q⇩c q⇩f q⇩f]
    using less_add_Suc1
    by (intro reflcl_over_single_ta_rules_semantic_path_rulesI) blast
  moreover from GMore(2) have "i < length ss ⟹ q⇩c |∈| ta_der (reflcl_over_single_ta Q ℱ q⇩c q⇩f) (term_of_gterm (ss ! i))" for i
    by (intro refl_ta_reflcl_over_single_ta_mono refl_ta_sound) (auto simp: SUP_le_iff 𝒯⇩G_funas_gterm_conv)
  moreover from GMore(2) have "i < length ts ⟹ q⇩c |∈| ta_der (reflcl_over_single_ta Q ℱ q⇩c q⇩f) (term_of_gterm (ts ! i))" for i
    by (intro refl_ta_reflcl_over_single_ta_mono refl_ta_sound) (auto simp: SUP_le_iff 𝒯⇩G_funas_gterm_conv)
  moreover from GMore have "q⇩f |∈| ta_der (reflcl_over_single_ta Q ℱ q⇩c q⇩f) (ctxt_of_gctxt C)⟨Var q⟩" by auto
  ultimately show ?case
    by (auto simp: nth_append_Cons simp del: replicate.simps intro!: exI[of _ "(replicate ?n q⇩c)[?i := q⇩f]"] exI[of _ q⇩f])
qed

lemma reflcl_over_single_ta_sig: "ta_sig (reflcl_over_single_ta Q ℱ q⇩c q⇩f) |⊆| ℱ"
  by (intro ta_sig_fsubsetI)
    (auto simp: reflcl_rules_def dest!: semantic_path_rules_fmemberD reflcl_over_single_ta_rules_split)

lemma gen_gctxtcl_lang:
  assumes "q⇩c |∉| 𝒬 𝒜" and "q⇩f |∉| 𝒬 𝒜" and "q⇩c |∉| Q" and "q⇩c ≠ q⇩f"
  shows "gta_lang {|q⇩f|} (gen_ctxt_closure_automaton Q ℱ 𝒜 q⇩c q⇩f) =
    {C⟨s⟩⇩G | C s. funas_gctxt C ⊆ fset ℱ ∧ s ∈ gta_lang Q 𝒜}"
    (is "?Ls = ?Rs")
proof -
  let ?A = "gen_ctxt_closure_automaton Q ℱ 𝒜 q⇩c q⇩f" let ?B = "reflcl_over_single_ta Q ℱ q⇩c q⇩f"
  interpret sq: derivation_split ?A 𝒜 ?B
    using assms unfolding derivation_split_def
    by (auto simp: gen_ctxt_closure_automaton_def reflcl_over_single_ta_def 𝒬_def reflcl_rules_def
        dest!: semantic_path_rules_rhs)
  {fix s assume "s ∈ ?Ls" then obtain u where
      seq: "u |∈| ta_der' 𝒜 (term_of_gterm s)" "Var q⇩f |∈| ta_der'?B u" using sq.ta_der'_split
      by (force simp: ta_der_to_ta_der' elim!: gta_langE)
    have "q⇩c ∉ vars_term u" "q⇩f ∉ vars_term u"
      using subsetD[OF ta_der'_gterm_states[OF seq(1)]] assms(1, 2)
      by (auto simp flip: set_vars_term_list)
    then obtain q where vars: "vars_term_list u = [q]" and fin: "q |∈| Q" unfolding set_vars_term_list[symmetric]
      using reflcl_over_single_ta_vars_term[unfolded ta_der_to_ta_der', OF assms(3, 4) seq(2), of "length (vars_term_list u)"]
      by (metis (no_types, lifting) finsertE in_set_conv_nth length_0_conv length_Suc_conv
          length_replicate lessI less_Suc_eq_0_disj nth_Cons_0 nth_list_update nth_replicate zero_less_Suc)
    have "s ∈ ?Rs" using fin ta_der'_ground_ctxt_structure[OF seq(1) vars]
      using ta_der'_Var_funas[OF seq(2), THEN subset_trans, OF reflcl_over_single_ta_sig[unfolded less_eq_fset.rep_eq]]
      by (auto intro!: exI[of _ "ta_der'_gctxt u"] exI[of _ "ta_der'_source_gctxt_arg u s"])
        (metis Un_iff funas_term_ctxt_apply funas_ctxt_of_gctxt_conv subset_eq) 
  }
  then have ls: "?Ls ⊆ ?Rs" by blast
  {fix t assume "t ∈ ?Rs"
    then obtain C s where gr_fun: "funas_gctxt C ⊆ fset ℱ" and reachA: "s ∈ gta_lang Q 𝒜" and
      const: "t = C⟨s⟩⇩G" by auto
    from reachA obtain q where der_A: "q |∈| Q |∩| 𝒬 𝒜" "q |∈| ta_der 𝒜 (term_of_gterm s)"
      by auto
    have "q⇩f |∈| ta_der ?B (ctxt_of_gctxt C)⟨Var q⟩" using gr_fun der_A(1)
      using reflcl_over_single_ta_sound[OF gr_fun]
      by force
    then have "t ∈ ?Ls" unfolding const
      by (meson der_A(2) finsertI1 gta_langI sq.gctxt_const_to_ta_der)}
  then show ?thesis using ls by blast
qed

lemma gen_gctxt_closure_sound:
  fixes 𝒜 :: "('q, 'f) reg"
  assumes "q⇩c |∉| 𝒬⇩r 𝒜" and "q⇩f |∉| 𝒬⇩r 𝒜" and "q⇩c |∉| fin 𝒜" and "q⇩c ≠ q⇩f"
  shows "ℒ (gen_ctxt_closure_reg ℱ 𝒜 q⇩c q⇩f) = {C⟨s⟩⇩G | C s. funas_gctxt C ⊆ fset ℱ ∧ s ∈ ℒ 𝒜}"
  using gen_gctxtcl_lang[OF assms] unfolding ℒ_def
  by (simp add: gen_ctxt_closure_reg_def)

lemma gen_ctxt_closure_sound:
  fixes 𝒜 :: "('q, 'f) reg"
  assumes "q⇩c |∉| 𝒬⇩r 𝒜" and "q⇩f |∉| 𝒬⇩r 𝒜" and "q⇩c |∉| fin 𝒜" and "q⇩c ≠ q⇩f"
  shows "ℒ (gen_ctxt_closure_reg ℱ 𝒜 q⇩c q⇩f) =
    {(gterm_of_term :: ('f, 'q) term ⇒ 'f gterm) C⟨term_of_gterm s⟩ | C s. ground_ctxt C ∧ funas_ctxt C ⊆ fset ℱ ∧ s ∈ ℒ 𝒜}"
  unfolding gen_gctxt_closure_sound[OF assms]
  by (metis (no_types, opaque_lifting) ctxt_of_gctxt_apply funas_ctxt_of_gctxt_conv gctxt_of_ctxt_inv ground_ctxt_of_gctxt)

lemma gctxt_closure_lang:
  shows "ℒ (ctxt_closure_reg ℱ 𝒜) =
    { C⟨s⟩⇩G | C s. funas_gctxt C ⊆ fset ℱ ∧ s ∈ ℒ 𝒜}"
proof -
  let ?B = "fmap_states_reg Inl (reg_Restr_Q⇩f 𝒜)"
  have ts: "Inr False |∉| 𝒬⇩r ?B" "Inr True |∉| 𝒬⇩r ?B" "Inr False |∉| fin (fmap_states_reg Inl (reg_Restr_Q⇩f 𝒜))"
    by (auto simp: fmap_states_reg_def fmap_states_ta_def' 𝒬_def rule_states_def) 
  from gen_gctxt_closure_sound[OF ts] show ?thesis 
    by (simp add: ctxt_closure_reg_def)
qed

lemma ctxt_closure_lang:
  shows "ℒ (ctxt_closure_reg ℱ 𝒜) =
    {(gterm_of_term :: ('f, 'q + bool) term ⇒ 'f gterm) C⟨term_of_gterm s⟩ |
      C s. ground_ctxt C ∧ funas_ctxt C ⊆ fset ℱ ∧ s ∈ ℒ 𝒜}"
  unfolding gctxt_closure_lang
  by (metis (mono_tags, opaque_lifting) ctxt_of_gctxt_inv funas_gctxt_of_ctxt
      ground_ctxt_of_gctxt ground_gctxt_of_ctxt_apply_gterm term_of_gterm_inv)


subsubsection ‹Correctness of @{const gen_nhole_ctxt_closure_automaton} and @{const nhole_ctxt_closure_reg}›

lemma reflcl_over_nhole_ctxt_ta_vars_term_q⇩c:
  "q⇩c ≠ q⇩f ⟹ q⇩c ≠ q⇩i ⟹ q⇩c |∈| ta_der (reflcl_over_nhole_ctxt_ta Q ℱ q⇩c q⇩i q⇩f) u ⟹
    vars_term_list u = replicate (length (vars_term_list u)) q⇩c"
proof (induct u)
  case (Fun f ts)
  have "i < length ts ⟹ q⇩c |∈| ta_der (reflcl_over_nhole_ctxt_ta Q ℱ q⇩c q⇩i q⇩f) (ts ! i)" for i using Fun(2, 3, 4)
    by (auto simp: reflcl_over_nhole_ctxt_ta_def dest!: ftranclD2 reflcl_rules_args semantic_path_rules_rhs)
  then have "i < length (concat (map vars_term_list ts)) ⟹ concat (map vars_term_list ts) ! i = q⇩c" for i
    using Fun(1)[OF nth_mem Fun(2, 3)]
    by (metis (no_types, lifting) length_map map_nth_eq_conv nth_concat_split' nth_replicate)
  then show ?case using Fun(1)[OF nth_mem Fun(2)]
    by (auto intro: nth_equalityI simp: vars_term_list.simps)
qed (auto simp: reflcl_over_nhole_ctxt_ta_def dest: ftranclD2 simp: vars_term_list.simps)

lemma reflcl_over_nhole_ctxt_ta_vars_term_Var:
  assumes disj: "q⇩c |∉| Q" "q⇩f |∉| Q" "q⇩c ≠ q⇩f" "q⇩i ≠ q⇩f" "q⇩c ≠ q⇩i"
    and reach: "q⇩i |∈| ta_der (reflcl_over_nhole_ctxt_ta Q ℱ q⇩c q⇩i q⇩f) u"
  shows "(∃ q. q |∈| finsert q⇩i Q ∧  u = Var q)" using assms
  by (cases u) (fastforce simp: reflcl_over_nhole_ctxt_ta_def reflcl_rules_def dest: ftranclD semantic_path_rules_rhs)+

lemma reflcl_over_nhole_ctxt_ta_vars_term:
  assumes disj: "q⇩c |∉| Q" "q⇩f |∉| Q" "q⇩c ≠ q⇩f" "q⇩i ≠ q⇩f" "q⇩c ≠ q⇩i"
    and reach: "q⇩f |∈| ta_der (reflcl_over_nhole_ctxt_ta Q ℱ q⇩c q⇩i q⇩f) u"
  shows "(∃ i q. i < length (vars_term_list u) ∧ q |∈| {|q⇩i, q⇩f|} |∪| Q ∧ vars_term_list u = (replicate (length (vars_term_list u)) q⇩c)[i := q])"
  using assms
proof (induct u)
  case (Var q) then show ?case
    by (intro exI[of _ 0] exI[of _ q]) (auto simp: reflcl_over_nhole_ctxt_ta_def vars_term_list.simps dest: ftranclD2)
next
  case (Fun f ts)
  from Fun(2 - 7) obtain q qs where rule: "TA_rule f qs q⇩f |∈| semantic_path_rules ℱ q⇩c q q⇩f" "q = q⇩i ∨ q = q⇩f"
    "length qs = length ts" "∀ i < length ts. qs ! i |∈| ta_der (reflcl_over_nhole_ctxt_ta Q ℱ q⇩c q⇩i q⇩f) (ts ! i)"
    by (auto simp: reflcl_over_nhole_ctxt_ta_def reflcl_rules_def dest: ftranclD2)
  from rule(1- 3) obtain i where states: "i < length ts" "qs = (replicate (length ts) q⇩c)[i := q]"
    by (auto simp: semantic_path_rules_fmember)
  then have qc: "j < length ts ⟹ j ≠ i ⟹ vars_term_list (ts ! j) = replicate (length (vars_term_list (ts ! j))) q⇩c" for j
    using reflcl_over_nhole_ctxt_ta_vars_term_q⇩c[OF Fun(4, 6)] rule
    by force
  from rule states have "q |∈| ta_der (reflcl_over_nhole_ctxt_ta Q ℱ q⇩c q⇩i q⇩f) (ts ! i)"
    by auto
  from this Fun(1)[OF nth_mem, of i, OF _ Fun(2 - 6)] rule(2) states(1) obtain k q' where
    qf: "k < length (vars_term_list (ts ! i))" "q' |∈| {|q⇩i, q⇩f|} |∪| Q "
    "vars_term_list (ts ! i) = (replicate (length (vars_term_list (ts ! i))) q⇩c)[k :=  q']"
    using reflcl_over_nhole_ctxt_ta_vars_term_Var[OF Fun(2 - 6), of ℱ "ts ! i"]
    by (auto simp: nth_list_update vars_term_list.simps split: if_splits) blast
  let ?l = "sum_list (map length (take i (map vars_term_list ts))) + k"
  show ?case using qc qf rule(3) states(1)
    apply (intro exI[of _ ?l] exI[of _  q'])
    apply (auto 0 0 simp: vars_term_list.simps concat_nth_length nth_list_update elim!: nth_concat_split' intro!: nth_equalityI)
         apply (metis length_replicate nth_list_update_eq nth_list_update_neq nth_replicate)+
    done
qed

lemma reflcl_over_nhole_ctxt_ta_mono:
  "q |∈| ta_der (refl_ta ℱ q) t ⟹ q |∈| ta_der (reflcl_over_nhole_ctxt_ta Q ℱ q q⇩i q⇩f) t"
  by (intro ta_der_el_mono[where ?ℬ = "reflcl_over_nhole_ctxt_ta Q ℱ q q⇩i q⇩f"])
    (auto simp: refl_ta_def reflcl_over_nhole_ctxt_ta_def)


lemma reflcl_over_nhole_ctxt_ta_sound:
  assumes "funas_gctxt C ⊆ fset ℱ" "C ≠ GHole" "q |∈| Q" 
  shows "q⇩f |∈| ta_der (reflcl_over_nhole_ctxt_ta Q ℱ q⇩c q⇩i q⇩f) (ctxt_of_gctxt C)⟨Var q⟩" using assms(1, 2)
proof (induct C)
  case GHole then show ?case using assms(2)
    by (auto simp add: reflcl_over_single_ta_def)
next
  case (GMore f ss C ts) note IH = this
  let ?i = "length ss" let ?n = "Suc (length ss + length ts)"
  from GMore have funas: "(f, ?n) |∈| ℱ" by auto
  from GMore(2) have args_ss: "i < length ss ⟹ q⇩c |∈| ta_der (reflcl_over_nhole_ctxt_ta Q ℱ q⇩c q⇩i q⇩f) (term_of_gterm (ss ! i))" for i
    by (intro reflcl_over_nhole_ctxt_ta_mono refl_ta_sound) (auto simp: SUP_le_iff 𝒯⇩G_funas_gterm_conv)
  from GMore(2) have args_ts: "i < length ts ⟹ q⇩c |∈| ta_der (reflcl_over_nhole_ctxt_ta Q ℱ q⇩c q⇩i q⇩f) (term_of_gterm (ts ! i))" for i
    by (intro reflcl_over_nhole_ctxt_ta_mono refl_ta_sound) (auto simp: SUP_le_iff 𝒯⇩G_funas_gterm_conv)
  note args = this
  show ?case
  proof (cases C)
    case [simp]: GHole
    from funas have "f ((replicate ?n q⇩c)[?i := q⇩i]) → q⇩f |∈| rules (reflcl_over_nhole_ctxt_ta Q ℱ q⇩c q⇩i q⇩f)"
      using semantic_path_rules_fmember[of f "(replicate ?n q⇩c)[?i := q⇩i]" q⇩f ℱ q⇩c q⇩i q⇩f]
      unfolding reflcl_over_nhole_ctxt_ta_def
      by (metis funionCI less_add_Suc1 ta.sel(1))
    moreover have "q⇩i |∈| ta_der (reflcl_over_nhole_ctxt_ta Q ℱ q⇩c q⇩i q⇩f) (ctxt_of_gctxt C)⟨Var q⟩"
      using assms(3) by (auto simp: reflcl_over_nhole_ctxt_ta_def)
    ultimately show ?thesis using args_ss args_ts
      by (auto simp: nth_append_Cons simp del: replicate.simps intro!: exI[of _ "(replicate ?n q⇩c)[?i := q⇩i]"] exI[of _ q⇩f])
  next
    case (GMore x21 x22 x23 x24)
    then have "q⇩f |∈| ta_der (reflcl_over_nhole_ctxt_ta Q ℱ q⇩c q⇩i q⇩f) (ctxt_of_gctxt C)⟨Var q⟩"
      using IH(1, 2) by auto
    moreover from funas have "f ((replicate ?n q⇩c)[?i := q⇩f]) → q⇩f |∈| rules (reflcl_over_nhole_ctxt_ta Q ℱ q⇩c q⇩i q⇩f)"
      using semantic_path_rules_fmember[of f "(replicate ?n q⇩c)[?i := q⇩f]" q⇩f ℱ q⇩c q⇩f q⇩f]
      unfolding reflcl_over_nhole_ctxt_ta_def
      by (metis funionI2 less_add_Suc1 ta.sel(1))
    ultimately show ?thesis using args_ss args_ts
      by (auto simp: nth_append_Cons simp del: replicate.simps intro!: exI[of _ "(replicate ?n q⇩c)[?i := q⇩f]"] exI[of _ q⇩f])
  qed
qed

lemma reflcl_over_nhole_ctxt_ta_sig: "ta_sig (reflcl_over_nhole_ctxt_ta Q ℱ q⇩c q⇩i q⇩f) |⊆| ℱ"
  by (intro ta_sig_fsubsetI)
    (auto simp: reflcl_over_nhole_ctxt_ta_def reflcl_rules_def dest!: semantic_path_rules_fmemberD)

lemma gen_nhole_gctxt_closure_lang:
  assumes "q⇩c |∉| 𝒬 𝒜" "q⇩i |∉| 𝒬 𝒜" "q⇩f |∉| 𝒬 𝒜"
    and "q⇩c |∉| Q" "q⇩f |∉| Q"
    and "q⇩c ≠ q⇩i" "q⇩c ≠ q⇩f" "q⇩i ≠ q⇩f"
  shows "gta_lang {|q⇩f|} (gen_nhole_ctxt_closure_automaton Q ℱ 𝒜 q⇩c q⇩i q⇩f) =
    {C⟨s⟩⇩G | C s. C ≠ GHole ∧ funas_gctxt C ⊆ fset ℱ ∧ s ∈ gta_lang Q 𝒜}"
    (is "?Ls = ?Rs")
proof -
  let ?A = "gen_nhole_ctxt_closure_automaton Q ℱ 𝒜 q⇩c q⇩i q⇩f" let ?B = "reflcl_over_nhole_ctxt_ta Q ℱ q⇩c q⇩i q⇩f"
  interpret sq: derivation_split ?A 𝒜 ?B
    using assms unfolding derivation_split_def
    by (auto simp: gen_nhole_ctxt_closure_automaton_def reflcl_over_nhole_ctxt_ta_def 𝒬_def reflcl_rules_def
        dest!: semantic_path_rules_rhs)
  {fix s assume "s ∈ ?Ls" then obtain u where
      seq: "u |∈| ta_der' 𝒜 (term_of_gterm s)" "Var q⇩f |∈| ta_der'?B u" using sq.ta_der'_split
      by (force simp: ta_der_to_ta_der' elim!: gta_langE)
    have "q⇩c ∉ vars_term u" "q⇩i ∉ vars_term u" "q⇩f ∉ vars_term u"
      using subsetD[OF ta_der'_gterm_states[OF seq(1)]] assms(1 - 3)
      by (auto simp flip: set_vars_term_list)
    then obtain q where vars: "vars_term_list u = [q]" and fin: "q |∈| Q"
      unfolding set_vars_term_list[symmetric]
      using reflcl_over_nhole_ctxt_ta_vars_term[unfolded ta_der_to_ta_der', OF assms(4, 5, 7 - 8, 6) seq(2)]
      by (metis (no_types, opaque_lifting) finsert_iff funion_commute funion_finsert_right
          length_greater_0_conv lessI list.size(3) list_update_code(2) not0_implies_Suc
          nth_list_update_neq nth_mem nth_replicate replicate_Suc replicate_empty sup_bot.right_neutral)
    from seq(2) have "ta_der'_gctxt u ≠ GHole" using ta_der'_ground_ctxt_structure(1)[OF seq(1) vars]
      using fin assms(4, 5, 8) by (auto simp: reflcl_over_nhole_ctxt_ta_def dest!: ftranclD2)
    then have "s ∈ ?Rs" using fin ta_der'_ground_ctxt_structure[OF seq(1) vars] seq(2)
      using ta_der'_Var_funas[OF seq(2), THEN subset_trans, OF reflcl_over_nhole_ctxt_ta_sig[unfolded less_eq_fset.rep_eq]]
      by (auto intro!: exI[of _ "ta_der'_gctxt u"] exI[of _ "ta_der'_source_gctxt_arg u s"])
        (metis Un_iff funas_term_ctxt_apply funas_ctxt_of_gctxt_conv in_mono)}
  then have ls: "?Ls ⊆ ?Rs" by blast
  {fix t assume "t ∈ ?Rs"
    then obtain C s where gr_fun: "funas_gctxt C ⊆ fset ℱ" "C ≠ GHole" and reachA: "s ∈ gta_lang Q 𝒜" and
      const: "t = C⟨s⟩⇩G" by auto
    from reachA obtain q where der_A: "q |∈| Q |∩| 𝒬 𝒜" "q |∈| ta_der 𝒜 (term_of_gterm s)"
      by auto
    have "q⇩f |∈| ta_der ?B (ctxt_of_gctxt C)⟨Var q⟩" using gr_fun der_A(1)
      using reflcl_over_nhole_ctxt_ta_sound[OF gr_fun]
      by force
    then have "t ∈ ?Ls" unfolding const
      by (meson der_A(2) finsertI1 gta_langI sq.gctxt_const_to_ta_der)}
  then show ?thesis using ls by blast
qed

lemma gen_nhole_gctxt_closure_sound:
  assumes "q⇩c |∉| 𝒬⇩r 𝒜" "q⇩i |∉| 𝒬⇩r 𝒜" "q⇩f |∉| 𝒬⇩r 𝒜"
    and "q⇩c |∉| (fin 𝒜)" "q⇩f |∉| (fin 𝒜)"
    and "q⇩c ≠ q⇩i" "q⇩c ≠ q⇩f" "q⇩i ≠ q⇩f"
  shows "ℒ (gen_nhole_ctxt_closure_reg ℱ 𝒜 q⇩c q⇩i q⇩f) =
    { C⟨s⟩⇩G | C s. C ≠ GHole ∧ funas_gctxt C ⊆ fset ℱ ∧ s ∈ ℒ 𝒜}"
  using gen_nhole_gctxt_closure_lang[OF assms] unfolding ℒ_def
  by (auto simp: gen_nhole_ctxt_closure_reg_def)


lemma nhole_ctxtcl_lang:
  "ℒ (nhole_ctxt_closure_reg ℱ 𝒜) =
    { C⟨s⟩⇩G | C s. C ≠ GHole ∧ funas_gctxt C ⊆ fset ℱ ∧ s ∈ ℒ 𝒜}"
proof -
  let ?B = "fmap_states_reg (Inl :: 'b ⇒ 'b + cl_states) (reg_Restr_Q⇩f 𝒜)"
  have ts: "Inr cl_state |∉| 𝒬⇩r ?B" "Inr tr_state |∉| 𝒬⇩r ?B" "Inr fin_state |∉| 𝒬⇩r ?B"
    by (auto simp: fmap_states_reg_def)
  then have "Inr cl_state |∉| fin (fmap_states_reg Inl (reg_Restr_Q⇩f 𝒜))"
    "Inr fin_state |∉| fin (fmap_states_reg Inl (reg_Restr_Q⇩f 𝒜))"
    using finj_Inl_Inr(1) fmap_states_reg_Restr_Q⇩f_fin by blast+
  from gen_nhole_gctxt_closure_sound[OF ts this] show ?thesis
    by (simp add: nhole_ctxt_closure_reg_def Let_def)
qed


subsubsection ‹Correctness of @{const gen_nhole_mctxt_closure_automaton}›

lemmas reflcl_over_nhole_mctxt_ta_simp = reflcl_over_nhole_mctxt_ta_def reflcl_over_nhole_ctxt_ta_def

lemma reflcl_rules_rhsD:
  "f ps → q |∈| reflcl_rules ℱ q⇩c ⟹ q = q⇩c"
  by (auto simp: reflcl_rules_def)

lemma reflcl_over_nhole_mctxt_ta_vars_term:
  assumes "q |∈| ta_der (reflcl_over_nhole_mctxt_ta Q ℱ q⇩c q⇩i q⇩f) t"
   and "q⇩c |∉| Q" "q ≠ q⇩c" "q⇩f ≠ q⇩c" "q⇩i ≠ q⇩c"
  shows "vars_term t ≠ {}" using assms
proof (induction t arbitrary: q)
  case (Fun f ts)
  let ?A = "reflcl_over_nhole_mctxt_ta Q ℱ q⇩c q⇩i q⇩f"
  from Fun(2) obtain p ps where rule: "TA_rule f ps p |∈| rules ?A"
    "length ps = length ts" "∀ i < length ts. ps ! i |∈| ta_der ?A (ts ! i)"
    "p = q ∨ (p, q) |∈| (eps ?A)|⇧+|"
    by force
  from rule(1, 4) Fun(3-) have "p ≠ q⇩c"
    by (auto simp: reflcl_over_nhole_mctxt_ta_simp dest: ftranclD)
  then have "∃ i < length ts. ps ! i ≠ q⇩c" using rule(1, 2) Fun(4-)
    using semantic_path_rules_fmemberD
    by (force simp: reflcl_over_nhole_mctxt_ta_simp dest: reflcl_rules_rhsD)
  then show ?case using Fun(1)[OF nth_mem _ Fun(3) _ Fun(5, 6)] rule(2, 3)
    by fastforce
qed auto

lemma reflcl_over_nhole_mctxt_ta_Fun:
  assumes "q⇩f |∈| ta_der (reflcl_over_nhole_mctxt_ta Q ℱ q⇩c q⇩i q⇩f) t" "t ≠ Var q⇩f"
    and  "q⇩f ≠ q⇩c" "q⇩f ≠ q⇩i"
  shows "is_Fun t" using assms
  by (cases t) (auto simp: reflcl_over_nhole_mctxt_ta_simp dest: ftranclD2)

lemma rule_states_reflcl_rulesD:
  "p |∈| rule_states (reflcl_rules ℱ q) ⟹ p = q"
  by (auto simp: reflcl_rules_def rule_states_def fset_of_list_elem)

lemma rule_states_semantic_path_rulesD:
  "p |∈| rule_states (semantic_path_rules ℱ q⇩c q⇩i q⇩f) ⟹ p = q⇩c ∨ p = q⇩i ∨ p = q⇩f"
  by (auto simp: rule_states_def dest!: semantic_path_rules_fmemberD)
    (metis in_fset_conv_nth length_list_update length_replicate nth_list_update nth_replicate)

lemma 𝒬_reflcl_over_nhole_mctxt_ta:
  "𝒬 (reflcl_over_nhole_mctxt_ta Q ℱ q⇩c q⇩i q⇩f) |⊆| Q |∪| {|q⇩c, q⇩i, q⇩f|}"
  by (auto 0 0 simp: eps_states_def reflcl_over_nhole_mctxt_ta_simp 𝒬_def
      dest!: rule_states_reflcl_rulesD rule_states_semantic_path_rulesD)

lemma reflcl_over_nhole_mctxt_ta_vars_term_subset_eq:
  assumes "q |∈| ta_der (reflcl_over_nhole_mctxt_ta Q ℱ q⇩c q⇩i q⇩f) t" "q = q⇩f ∨ q = q⇩i"
  shows "vars_term t ⊆ {q⇩c, q⇩i, q⇩f} ∪ fset Q"
  using fresh_states_ta_der'_pres[OF _ _ assms(1)[unfolded ta_der_to_ta_der']] assms(2)
  using fsubsetD[OF 𝒬_reflcl_over_nhole_mctxt_ta[of Q ℱ q⇩c q⇩i q⇩f]]
  by auto

lemma sig_reflcl_over_nhole_mctxt_ta [simp]:
  "ta_sig (reflcl_over_nhole_mctxt_ta Q ℱ q⇩c q⇩i q⇩f) = ℱ"
  by (force simp: reflcl_over_nhole_mctxt_ta_simp reflcl_rules_def
      dest!: semantic_path_rules_fmemberD intro!: ta_sig_fsubsetI)

lemma reflcl_over_nhole_mctxt_ta_aux_sound:
  assumes "funas_term t ⊆ fset ℱ" "vars_term t ⊆ fset Q"
  shows "q⇩c |∈| ta_der (reflcl_over_nhole_mctxt_ta Q ℱ q⇩c q⇩i q⇩f) t" using assms
proof (induct t)
  case (Var x)
  then show ?case
    by (auto simp: reflcl_over_nhole_mctxt_ta_simp fimage_iff)
     (meson finsertI1 finsertI2 fr_into_trancl ftrancl_into_trancl rev_fimage_eqI)
next
  case (Fun f ts)
  from Fun(2) have "TA_rule f (replicate (length ts) q⇩c) q⇩c |∈| rules (reflcl_over_nhole_mctxt_ta Q ℱ q⇩c q⇩i q⇩f)"
    by (auto simp: reflcl_over_nhole_mctxt_ta_simp reflcl_rules_def fimage_iff fBall_def
             split: prod.splits)
  then show ?case using Fun(1)[OF nth_mem] Fun(2-)
    by (auto simp: SUP_le_iff) (metis length_replicate nth_replicate)
qed

lemma reflcl_over_nhole_mctxt_ta_sound:
  assumes "funas_term t ⊆ fset ℱ" "vars_term t ⊆ fset Q" "vars_term t ≠ {}"
  shows "(is_Var t ⟶ q⇩i |∈| ta_der (reflcl_over_nhole_mctxt_ta Q ℱ q⇩c q⇩i q⇩f) t) ∧
    (is_Fun t ⟶ q⇩f |∈| ta_der (reflcl_over_nhole_mctxt_ta Q ℱ q⇩c q⇩i q⇩f) t)" using assms
proof (induct t)
  case (Fun f ts)
  let ?A = "reflcl_over_nhole_mctxt_ta Q ℱ q⇩c q⇩i q⇩f"
  from Fun(4) obtain i where vars: "i < length ts" "vars_term (ts ! i) ≠ {}"
    by (metis SUP_le_iff in_set_conv_nth subset_empty term.set(4))
  consider (v) "is_Var (ts ! i)" | (f) "is_Fun (ts ! i)" by blast
  then show ?case
  proof cases
    case v
    from v Fun(1)[OF nth_mem[OF vars(1)]] have "q⇩i |∈| ta_der ?A (ts ! i)"
      using vars Fun(2-) by (auto simp: SUP_le_iff)
    moreover have "f (replicate (length ts) q⇩c)[i := q⇩i] → q⇩f |∈| rules ?A"
      using Fun(2) vars(1)
      by (auto simp: reflcl_over_nhole_mctxt_ta_simp semantic_path_rules_fmember)
    moreover have "j < length ts ⟹ q⇩c |∈| ta_der ?A (ts ! j)" for j using Fun(2-)
      by (intro reflcl_over_nhole_mctxt_ta_aux_sound) (auto simp: SUP_le_iff)
    ultimately show ?thesis using vars
      by auto (metis length_list_update length_replicate nth_list_update nth_replicate)
  next
    case f
    from f Fun(1)[OF nth_mem[OF vars(1)]] have "q⇩f |∈| ta_der ?A (ts ! i)"
      using vars Fun(2-) by (auto simp: SUP_le_iff)
    moreover have "f (replicate (length ts) q⇩c)[i := q⇩f] → q⇩f |∈| rules ?A"
      using Fun(2) vars(1)
      by (auto simp: reflcl_over_nhole_mctxt_ta_simp semantic_path_rules_fmember)
    moreover have "j < length ts ⟹ q⇩c |∈| ta_der ?A (ts ! j)" for j using Fun(2-)
      by (intro reflcl_over_nhole_mctxt_ta_aux_sound) (auto simp: SUP_le_iff)
    ultimately show ?thesis using vars
      by auto (metis length_list_update length_replicate nth_list_update nth_replicate) 
  qed
qed (auto simp: reflcl_over_nhole_mctxt_ta_simp dest!: ftranclD2)


lemma gen_nhole_gmctxt_closure_lang:
  assumes "q⇩c |∉| 𝒬 𝒜" and "q⇩i |∉| 𝒬 𝒜" "q⇩f |∉| 𝒬 𝒜"
    and "q⇩c |∉| Q" "q⇩f ≠ q⇩c" "q⇩f ≠ q⇩i" "q⇩i ≠ q⇩c"
  shows "gta_lang {|q⇩f|} (gen_nhole_mctxt_closure_automaton Q ℱ 𝒜 q⇩c q⇩i q⇩f) =
    { fill_gholes C ss |
      C ss. 0 < num_gholes C ∧ num_gholes C = length ss ∧ C ≠ GMHole ∧
      funas_gmctxt C ⊆ fset ℱ ∧ (∀ i < length ss. ss ! i ∈ gta_lang Q 𝒜)}"
    (is "?Ls = ?Rs")
proof -
  let ?A = "gen_nhole_mctxt_closure_automaton Q ℱ 𝒜 q⇩c q⇩i q⇩f" let ?B = "reflcl_over_nhole_mctxt_ta Q ℱ q⇩c q⇩i q⇩f"
  interpret sq: derivation_split "?A" "𝒜" "?B"
    using assms unfolding derivation_split_def
    by (auto simp: gen_nhole_mctxt_closure_automaton_def reflcl_over_nhole_mctxt_ta_def
        reflcl_over_nhole_ctxt_ta_def 𝒬_def reflcl_rules_def dest!: semantic_path_rules_rhs)
  {fix s assume "s ∈ ?Ls" then obtain u where
      seq: "u |∈| ta_der' 𝒜 (term_of_gterm s)" "Var q⇩f |∈| ta_der'?B u"
      by (auto simp: ta_der_to_ta_der' elim!: gta_langE dest!: sq.ta_der'_split)
    note der = seq(2)[unfolded ta_der_to_ta_der'[symmetric]]
    have "vars_term u ⊆ fset Q" "vars_term u ≠ {}"
      using ta_der'_gterm_states[OF seq(1)] assms(1 - 3)
      using reflcl_over_nhole_mctxt_ta_vars_term[OF der assms(4) assms(5) assms(5) assms(7)]
      using reflcl_over_nhole_mctxt_ta_vars_term_subset_eq[OF der]
      by (metis Un_insert_left insert_is_Un subset_iff subset_insert)+
    then have vars: "¬ ground u" "i < length (ta_der'_target_args u) ⟹ ta_der'_target_args u ! i |∈| Q" for i
      by (auto simp: ta_der'_target_args_def split_vars_vars_term_list
          set_list_subset_nth_conv simp flip: set_vars_term_list)
    have hole: "ta_der'_target_mctxt u ≠ MHole" using vars assms(3-)
      using reflcl_over_nhole_mctxt_ta_Fun[OF der]
      using ta_der'_mctxt_structure(1, 3)[OF seq(1)]
      by auto
        (metis One_nat_def fill_holes_MHole gterm_ta_der_states
          length_map nth_map seq(1) ta_der_to_ta_der' term.disc(1)
          zero_less_Suc)
    let ?w = "λ i. ta_der'_source_args u (term_of_gterm s) ! i"
    have "s ∈ ?Rs" using seq(1) ta_der'_Var_funas[OF seq(2)]
      using ground_ta_der_statesD[of "?w i" "ta_der'_target_args u ! i" 𝒜 for i] assms vars
      using ta_der'_ground_mctxt_structure[OF seq(1)] hole
      by (force simp: ground_gmctxt_of_mctxt_fill_holes' ta_der'_source_args_term_of_gterm
          intro!: exI[of _ "gmctxt_of_mctxt (ta_der'_target_mctxt u)"]
          exI[of _ "map gterm_of_term (ta_der'_source_args u (term_of_gterm s))"]
          gta_langI[of "ta_der'_target_args u ! i" Q 𝒜
            "gterm_of_term (?w i)" for i])}
  then have ls: "?Ls ⊆ ?Rs" by blast
  {fix t assume "t ∈ ?Rs"
    then obtain C ss where len: "0 < num_gholes C" "num_gholes C = length ss" "C ≠ GMHole" and
      gr_fun: "funas_gmctxt C ⊆ fset ℱ" and
      reachA: "∀ i < length ss. ss ! i ∈ gta_lang Q 𝒜" and
      const: "t = fill_gholes C ss" by auto
    from reachA obtain qs where states: "length ss = length qs" "∀ i < length qs. qs ! i |∈| Q |∩| 𝒬 𝒜"
      "∀ i < length qs. qs ! i |∈| ta_der 𝒜 ((map term_of_gterm ss) ! i)"
      using Ex_list_of_length_P[of "length ss" "λ q i. q |∈| ta_der 𝒜 (term_of_gterm (ss ! i)) ∧ q |∈| Q"]
      by (metis (full_types) finterI gta_langE gterm_ta_der_states length_map map_nth_eq_conv)
    have [simp]: "is_Fun (fill_holes (mctxt_of_gmctxt C) (map Var qs)) ⟷ True"
      "is_Var (fill_holes (mctxt_of_gmctxt C) (map Var qs)) ⟷ False"
      using len(3) by (cases C, auto)+
    have "q⇩f |∈| ta_der ?A (fill_holes (mctxt_of_gmctxt C) (map term_of_gterm ss))"
      using reachA len gr_fun states
      apply (intro sq.mctxt_const_to_ta_der[of "mctxt_of_gmctxt C" "map term_of_gterm ss" qs q⇩f])
      subgoal by auto
      subgoal by auto
      subgoal by auto
      subgoal apply (intro reflcl_over_nhole_mctxt_ta_sound[of "fill_holes (mctxt_of_gmctxt C) (map Var qs)", simplified])
        subgoal by (subst funas_mctxt_fill_holes, auto simp: funas_mctxt_of_gmctxt_conv)
        subgoal by (auto dest!: in_set_idx)
        subgoal by (auto dest!: in_set_idx)
        done
      done
    then have "t ∈ ?Ls" unfolding const
      by (simp add: fill_holes_mctxt_of_gmctxt_to_fill_gholes gta_langI len)}
  then show ?thesis using ls by blast
qed

lemma nhole_gmctxt_closure_lang:
  "ℒ (nhole_mctxt_closure_reg ℱ 𝒜) =
    { fill_gholes C ss | C ss. num_gholes C = length ss ∧ 0 < num_gholes C ∧ C ≠ GMHole ∧
      funas_gmctxt C ⊆ fset ℱ ∧ (∀ i < length ss. ss ! i ∈ ℒ 𝒜)}"
  (is "?Ls = ?Rs")
proof -
  let ?B = "fmap_states_reg (Inl :: 'b ⇒ 'b + cl_states) (reg_Restr_Q⇩f 𝒜)"
  have ts: "Inr cl_state |∉| 𝒬⇩r ?B" "Inr tr_state |∉| 𝒬⇩r ?B" "Inr fin_state |∉| 𝒬⇩r ?B"
    "Inr cl_state |∉| fin ?B"
    by (auto simp: fmap_states_reg_def)
  have [simp]: "gta_lang (fin (fmap_states_reg Inl (reg_Restr_Q⇩f 𝒜))) (ta (fmap_states_reg Inl (reg_Restr_Q⇩f 𝒜)))
    = gta_lang (fin 𝒜) (ta 𝒜)"
    by (metis ℒ_def ℒ_fmap_states_reg_Inl_Inr(1) reg_Rest_fin_states) 
  from gen_nhole_gmctxt_closure_lang[OF ts] show ?thesis 
    by (auto simp add: nhole_mctxt_closure_reg_def gen_nhole_mctxt_closure_reg_def Let_def ℒ_def)
qed

subsubsection ‹Correctness of @{const gen_mctxt_closure_reg} and @{const mctxt_closure_reg}›

lemma gen_gmctxt_closure_lang:
  assumes "q⇩c |∉| 𝒬 𝒜" and "q⇩i |∉| 𝒬 𝒜" "q⇩f |∉| 𝒬 𝒜"
    and disj: "q⇩c |∉| Q" "q⇩f ≠ q⇩c" "q⇩f ≠ q⇩i" "q⇩i ≠ q⇩c"
  shows "gta_lang {|q⇩f, q⇩i|} (gen_nhole_mctxt_closure_automaton Q ℱ 𝒜 q⇩c q⇩i q⇩f) =
    { fill_gholes C ss |
      C ss. 0 < num_gholes C ∧ num_gholes C = length ss ∧
      funas_gmctxt C ⊆ fset ℱ ∧ (∀ i < length ss. ss ! i ∈ gta_lang Q 𝒜)}"
    (is "?Ls = ?Rs")
proof -
  let ?A = "gen_nhole_mctxt_closure_automaton Q ℱ 𝒜 q⇩c q⇩i q⇩f" let ?B = "reflcl_over_nhole_mctxt_ta Q ℱ q⇩c q⇩i q⇩f"
  interpret sq: derivation_split "?A" "𝒜" "?B"
    using assms unfolding derivation_split_def
    by (auto simp: gen_nhole_mctxt_closure_automaton_def reflcl_over_nhole_mctxt_ta_def
        reflcl_over_nhole_ctxt_ta_def 𝒬_def reflcl_rules_def dest!: semantic_path_rules_rhs)
  {fix s assume "s ∈ ?Ls" then obtain u q where
      seq: "u |∈| ta_der' 𝒜 (term_of_gterm s)" "Var q |∈| ta_der'?B u" "q = q⇩f ∨ q = q⇩i"
      by (auto simp: ta_der_to_ta_der' elim!: gta_langE dest!: sq.ta_der'_split)
    have "vars_term u ⊆ fset Q" "vars_term u ≠ {}"
      using ta_der'_gterm_states[OF seq(1)] assms seq(3)
      using reflcl_over_nhole_mctxt_ta_vars_term[OF seq(2)[unfolded ta_der_to_ta_der'[symmetric]] disj(1) _ disj(2, 4)]
      using reflcl_over_nhole_mctxt_ta_vars_term_subset_eq[OF seq(2)[unfolded ta_der_to_ta_der'[symmetric]] seq(3)]
      by (metis Un_insert_left subsetD subset_insert sup_bot_left)+
    then have vars: "¬ ground u" "i < length (ta_der'_target_args u) ⟹ ta_der'_target_args u ! i |∈| Q" for i
      by (auto simp: ta_der'_target_args_def split_vars_vars_term_list
          set_list_subset_nth_conv simp flip: set_vars_term_list)
    let ?w = "λ i. ta_der'_source_args u (term_of_gterm s) ! i"
    have "s ∈ ?Rs" using seq(1) ta_der'_Var_funas[OF seq(2)]
      using ground_ta_der_statesD[of "?w i" "ta_der'_target_args u ! i" 𝒜 for i] assms vars
      using ta_der'_ground_mctxt_structure[OF seq(1)]
      by (force simp: ground_gmctxt_of_mctxt_fill_holes' ta_der'_source_args_term_of_gterm
          intro!: exI[of _ "gmctxt_of_mctxt (ta_der'_target_mctxt u)"]
          exI[of _ "map gterm_of_term (ta_der'_source_args u (term_of_gterm s))"]
          gta_langI[of "ta_der'_target_args u ! i" Q 𝒜
            "gterm_of_term (?w i)" for i])}
  then have "?Ls ⊆ ?Rs" by blast
  moreover
  {fix t assume "t ∈ ?Rs"
    then obtain C ss where len: "0 < num_gholes C" "num_gholes C = length ss" and
      gr_fun: "funas_gmctxt C ⊆ fset ℱ" and
      reachA: "∀ i < length ss. ss ! i ∈ gta_lang Q 𝒜" and
      const: "t = fill_gholes C ss" by auto
    from const have const': "term_of_gterm t = fill_holes (mctxt_of_gmctxt C) (map term_of_gterm ss)"
      by (simp add: fill_holes_mctxt_of_gmctxt_to_fill_gholes len(2))
    from reachA obtain qs where states: "length ss = length qs" "∀ i < length qs. qs ! i |∈| Q |∩| 𝒬 𝒜"
      "∀ i < length qs. qs ! i |∈| ta_der 𝒜 ((map term_of_gterm ss) ! i)"
      using Ex_list_of_length_P[of "length ss" "λ q i. q |∈| ta_der 𝒜 (term_of_gterm (ss ! i)) ∧ q |∈| Q"]
      by (metis (full_types) finterI gta_langE gterm_ta_der_states length_map map_nth_eq_conv)
    have "C = GMHole ⟹ is_Var (fill_holes (mctxt_of_gmctxt C) (map Var qs)) = True" using len states(1)
      by (metis One_nat_def fill_holes_MHole is_VarI length_map
          mctxt_of_gmctxt.simps(1) nth_map num_gholes.simps(1))
    then have hole: "C = GMHole ⟹ q⇩i |∈| ta_der ?A (fill_holes (mctxt_of_gmctxt C) (map term_of_gterm ss))"
      using reachA len gr_fun states len
      using reflcl_over_nhole_mctxt_ta_sound[of "fill_holes (mctxt_of_gmctxt C) (map Var qs)"]
      by (intro sq.mctxt_const_to_ta_der[of "mctxt_of_gmctxt C" "map term_of_gterm ss" qs q⇩i])
         (auto simp: funas_mctxt_of_gmctxt_conv set_list_subset_eq_nth_conv
          dest!: in_set_idx)
    have "C ≠ GMHole ⟹ is_Fun (fill_holes (mctxt_of_gmctxt C) (map Var qs)) = True"
      by (cases C) auto
    then have "C ≠ GMHole ⟹ q⇩f |∈| ta_der ?A (fill_holes (mctxt_of_gmctxt C) (map term_of_gterm ss))"
      using reachA len gr_fun states
      apply (intro sq.mctxt_const_to_ta_der[of "mctxt_of_gmctxt C" "map term_of_gterm ss" qs q⇩f])
      subgoal by auto
      subgoal by auto
      subgoal by auto
      subgoal 
        apply (intro reflcl_over_nhole_mctxt_ta_sound[of "fill_holes (mctxt_of_gmctxt C) (map Var qs)", 
              THEN conjunct2, rule_format])
        subgoal by (subst funas_mctxt_fill_holes, auto simp: funas_mctxt_of_gmctxt_conv)
        subgoal by (auto dest!: in_set_idx)
        subgoal by (auto dest!: in_set_idx)
        subgoal by auto
        done
      done
    then have "t ∈ ?Ls" using hole const' unfolding gta_lang_def gta_der_def
      by (metis (mono_tags, lifting) fempty_iff finsert_iff finterI mem_Collect_eq)}
  ultimately show ?thesis
    by (meson subsetI subset_antisym) 
qed


lemma gmctxt_closure_lang:
  "ℒ (mctxt_closure_reg ℱ 𝒜) =
    { fill_gholes C ss | C ss. num_gholes C = length ss ∧ 0 < num_gholes C ∧
      funas_gmctxt C ⊆ fset ℱ ∧ (∀ i < length ss. ss ! i ∈ ℒ 𝒜)}"
  (is "?Ls = ?Rs")
proof -
  let ?B = "fmap_states_reg (Inl :: 'b ⇒ 'b + cl_states) (reg_Restr_Q⇩f 𝒜)"
  have ts: "Inr cl_state |∉| 𝒬⇩r ?B" "Inr tr_state |∉| 𝒬⇩r ?B" "Inr fin_state |∉| 𝒬⇩r ?B"
    "Inr cl_state |∉| fin ?B"
    by (auto simp: fmap_states_reg_def)
  have [simp]: "gta_lang (fin (fmap_states_reg Inl (reg_Restr_Q⇩f 𝒜))) (ta (fmap_states_reg Inl (reg_Restr_Q⇩f 𝒜)))
    = gta_lang (fin 𝒜) (ta 𝒜)"
    by (metis ℒ_def ℒ_fmap_states_reg_Inl_Inr(1) reg_Rest_fin_states) 
  from gen_gmctxt_closure_lang[OF ts] show ?thesis
    by (auto simp add: mctxt_closure_reg_def gen_mctxt_closure_reg_def Let_def ℒ_def)
qed


subsubsection ‹Correctness of @{const nhole_mctxt_reflcl_reg}›

lemma nhole_mctxt_reflcl_lang:
  "ℒ (nhole_mctxt_reflcl_reg ℱ 𝒜) = ℒ (nhole_mctxt_closure_reg ℱ 𝒜) ∪ 𝒯⇩G (fset ℱ)"
proof -
  let ?refl = "Reg {|fin_clstate|} (refl_ta ℱ (fin_clstate))"
  {fix t assume "t ∈ ℒ ?refl" then have "t ∈ 𝒯⇩G (fset ℱ)"
      using reg_funas by fastforce}
  moreover
  {fix t assume "t ∈ 𝒯⇩G (fset ℱ)" then have "t ∈ ℒ ?refl"
      by (simp add: ℒ_def gta_langI refl_ta_sound)}
  ultimately have *: "ℒ ?refl = 𝒯⇩G (fset ℱ)"
    by blast
  show ?thesis unfolding nhole_mctxt_reflcl_reg_def ℒ_union * by simp
qed
declare ta_union_def [simp del]
end