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

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 𝒜)"
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
by (intro sq.mctxt_const_to_ta_der[of "mctxt_of_gmctxt C" "map term_of_gterm ss" qs q])
(auto simp: funas_mctxt_of_gmctxt_conv
dest!: in_set_idx intro!: refl_over_states_ta_sound)
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
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 (auto intro: nth_equalityI)
qed (auto dest: reflcl_over_single_ta_epsD)

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))
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: 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)
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]
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_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

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
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)
qed (auto simp: reflcl_over_nhole_ctxt_ta_def dest: ftranclD2)

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 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 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: 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)
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
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
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_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
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 fill_holes_MHole gterm_ta_der_states length_map lessI map_nth_eq_conv seq(1) ta_der_to_ta_der' term.disc(1))
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
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⇩f])
(auto simp: funas_mctxt_of_gmctxt_conv set_list_subset_eq_nth_conv
dest!: in_set_idx)
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)"
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 fill_holes_MHole length_map mctxt_of_gmctxt.simps(1) nth_map num_gholes.simps(1) term.disc(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
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⇩f])
(auto simp: funas_mctxt_of_gmctxt_conv set_list_subset_eq_nth_conv
dest!: in_set_idx)
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```