Theory Tree_Automata_Derivation_Split

theory Tree_Automata_Derivation_Split
  imports Regular_Tree_Relations.Tree_Automata
    Ground_MCtxt
begin

lemma ta_der'_inf_mctxt:
  assumes "t |∈| ta_der' π’œ s"
  shows "fst (split_vars t) ≀ (mctxt_of_term s)" using assms
proof (induct s arbitrary: t)
  case (Fun f ts) then show ?case
    by (cases t) (auto simp: comp_def less_eq_mctxt_prime intro: less_eq_mctxt'.intros)
qed (auto simp: ta_der'.simps)

lemma ta_der'_poss_subt_at_ta_der':
  assumes "t |∈| ta_der' π’œ s" and "p ∈ poss t"
  shows "t |_ p |∈| ta_der' π’œ (s |_ p)" using assms
  by (induct s arbitrary: t p) (auto simp: ta_der'.simps, blast+)

lemma ta_der'_varposs_to_ta_der:
  assumes "t |∈| ta_der' π’œ s" and "p ∈ varposs t"
  shows "the_Var (t |_ p) |∈| ta_der π’œ (s |_ p)" using assms
  by (induct s arbitrary: t p) (auto simp: ta_der'.simps, blast+)

definition "ta_der'_target_mctxt t ≑ fst (split_vars t)"
definition "ta_der'_target_args t ≑  snd (split_vars t)"
definition "ta_der'_source_args t s ≑ unfill_holes (fst (split_vars t)) s"

lemmas ta_der'_mctxt_simps = ta_der'_target_mctxt_def ta_der'_target_args_def ta_der'_source_args_def

lemma ta_der'_target_mctxt_funas [simp]:
  "funas_mctxt (ta_der'_target_mctxt u) = funas_term u"
  by (auto simp: ta_der'_target_mctxt_def)

lemma ta_der'_target_mctxt_ground [simp]:
  "ground_mctxt (ta_der'_target_mctxt t)"
  by (auto simp: ta_der'_target_mctxt_def)

lemma ta_der'_source_args_ground:
  "t |∈| ta_der' π’œ s ⟹ ground s ⟹ βˆ€ u ∈ set (ta_der'_source_args t s). ground u"
  by (metis fill_unfill_holes ground_fill_holes length_unfill_holes ta_der'_inf_mctxt ta_der'_mctxt_simps)

lemma ta_der'_source_args_term_of_gterm:
  "t |∈| ta_der' π’œ (term_of_gterm s) ⟹ βˆ€ u ∈ set (ta_der'_source_args t (term_of_gterm s)). ground u"
  by (intro ta_der'_source_args_ground) auto

lemma ta_der'_source_args_length: 
  "t |∈| ta_der' π’œ s ⟹ num_holes (ta_der'_target_mctxt t) = length (ta_der'_source_args t s)"
  by (auto simp: ta_der'_mctxt_simps ta_der'_inf_mctxt)

lemma ta_der'_target_args_length: 
  "num_holes (ta_der'_target_mctxt t) = length (ta_der'_target_args t)"
  by (auto simp: ta_der'_mctxt_simps split_vars_num_holes)

lemma ta_der'_target_args_vars_term_conv:
  "vars_term t = set (ta_der'_target_args t)"
  by (auto simp: ta_der'_target_args_def split_vars_vars_term_list)

lemma ta_der'_target_args_vars_term_list_conv:
  "ta_der'_target_args t = vars_term_list t"
  by (auto simp: ta_der'_target_args_def split_vars_vars_term_list)


lemma mctxt_args_ta_der':
  assumes "num_holes C = length qs" "num_holes C = length ss" 
    and "βˆ€ i < length ss. qs ! i |∈| ta_der π’œ (ss ! i)"
  shows "(fill_holes C (map Var qs)) |∈| ta_der' π’œ (fill_holes C ss)" using assms
proof (induct rule: fill_holes_induct2)
  case MHole then show ?case
    by (cases ss; cases qs) (auto simp: ta_der_to_ta_der')
next
  case (MFun f ts) then show ?case
    by (simp add: partition_by_nth_nth(1, 2))
qed auto

― β€ΉSplitting derivation into multihole context containing the remaining function symbols and
  the states, where each state is reached via the automataβ€Ί
lemma ta_der'_mctxt_structure:
  assumes "t |∈| ta_der' π’œ s"
  shows "t = fill_holes (ta_der'_target_mctxt t) (map Var (ta_der'_target_args t))" (is "?G1")
    "s = fill_holes (ta_der'_target_mctxt t) (ta_der'_source_args t s)" (is "?G2")
    "num_holes (ta_der'_target_mctxt t) = length (ta_der'_source_args t s) ∧
     length (ta_der'_source_args t s) = length (ta_der'_target_args t)" (is "?G3")
    "i < length (ta_der'_source_args t s) ⟹ ta_der'_target_args t ! i |∈| ta_der π’œ (ta_der'_source_args t s ! i)"
proof -
  let ?C = "ta_der'_target_mctxt t" let ?ss = "ta_der'_source_args t s"
  let ?qs = "ta_der'_target_args t"
  have t_split: "?G1" by (auto simp: ta_der'_mctxt_simps split_vars_fill_holes)
  have s_split: "?G2" by (auto simp: ta_der'_mctxt_simps ta_der'_inf_mctxt[OF assms]
     intro!: fill_unfill_holes[symmetric])
  have len: "num_holes ?C = length ?ss" "length ?ss = length ?qs" using assms
    by (auto simp: ta_der'_mctxt_simps split_vars_num_holes ta_der'_inf_mctxt)
  have "i < length (ta_der'_target_args t) ⟹
       ta_der'_target_args t ! i |∈| ta_der π’œ (ta_der'_source_args t s ! i)" for i
    using ta_der'_poss_subt_at_ta_der'[OF assms, of "varposs_list t ! i"]
    unfolding ta_der'_mctxt_simps split_vars_vars_term_list length_map 
    by (auto simp: unfill_holes_to_subst_at_hole_poss[OF ta_der'_inf_mctxt[OF assms]]
       simp flip: varposs_list_to_var_term_list[of i t, unfolded varposs_list_var_terms_length])
       (metis assms hole_poss_split_vars_varposs_list nth_map nth_mem
        ta_der'_varposs_to_ta_der ta_der_to_ta_der' varposs_eq_varposs_list varposs_list_var_terms_length)
  then show ?G1 ?G2 ?G3 "i < length (ta_der'_source_args t s) ⟹
       ta_der'_target_args t ! i |∈| ta_der π’œ (ta_der'_source_args t s ! i)" using len t_split s_split
    by (simp_all add: ta_der'_mctxt_simps)
qed

lemma ta_der'_ground_mctxt_structure:
  assumes "t |∈| ta_der' π’œ (term_of_gterm s)"
  shows "t = fill_holes (ta_der'_target_mctxt t) (map Var (ta_der'_target_args t))"
    "term_of_gterm s = fill_holes (ta_der'_target_mctxt t) (ta_der'_source_args t (term_of_gterm s))"
    "num_holes (ta_der'_target_mctxt t) =  length (ta_der'_source_args t (term_of_gterm s)) ∧
     length (ta_der'_source_args t (term_of_gterm s)) = length (ta_der'_target_args t)"
    "i < length (ta_der'_target_args t) ⟹ ta_der'_target_args t ! i |∈| ta_der π’œ (ta_der'_source_args t (term_of_gterm s) ! i)"
  using ta_der'_mctxt_structure[OF assms]
  by force+


― β€ΉSplitting derivation into context containing the remaining function symbols and stateβ€Ί

definition "ta_der'_gctxt t ≑ gctxt_of_gmctxt (gmctxt_of_mctxt (fst (split_vars t)))"
abbreviation "ta_der'_ctxt t ≑ ctxt_of_gctxt (ta_der'_gctxt t)"
definition "ta_der'_source_ctxt_arg t s ≑ hd (unfill_holes (fst (split_vars t)) s)"

abbreviation "ta_der'_source_gctxt_arg t s ≑ gterm_of_term (ta_der'_source_ctxt_arg t (term_of_gterm s))"

lemma ta_der'_ctxt_structure:
  assumes "t |∈| ta_der' π’œ s" "vars_term_list t = [q]"
  shows "t = (ta_der'_ctxt t)⟨Var q⟩" (is "?G1")
    "s = (ta_der'_ctxt t)⟨ta_der'_source_ctxt_arg t s⟩" (is "?G2")
    "ground_ctxt (ta_der'_ctxt t)" (is "?G3")
    "q |∈| ta_der π’œ (ta_der'_source_ctxt_arg t s)" (is "?G4")
proof -
  have *: "length xs = Suc 0 ⟹ xs = [hd xs]" for xs
    by (metis length_0_conv length_Suc_conv list.sel(1))
  have [simp]: "length (snd (split_vars t)) = Suc 0" using assms(2) ta_der'_inf_mctxt[OF assms(1)]
    by (auto simp: split_vars_vars_term_list)
  have [simp]: "num_gholes (gmctxt_of_mctxt (fst (split_vars t))) = Suc 0" using assms(2)
    by (simp add: split_vars_num_holes split_vars_vars_term_list)
  have [simp]: "ta_der'_source_args t s = [ta_der'_source_ctxt_arg t s]"
    using assms(2) ta_der'_inf_mctxt[OF assms(1)]
    by (auto simp: ta_der'_source_args_def ta_der'_source_ctxt_arg_def split_vars_num_holes intro!: *)
  have t_split: ?G1 using assms(2)
    by (auto simp: ta_der'_gctxt_def split_vars_fill_holes
      split_vars_vars_term_list simp flip: ctxt_of_gctxt_gctxt_of_gmctxt_apply)
  have s_split: ?G2 using ta_der'_mctxt_structure[OF assms(1)] assms(2)
    by (auto simp: ta_der'_gctxt_def ta_der'_target_mctxt_def
          simp flip: ctxt_of_gctxt_gctxt_of_gmctxt_apply)
  from ta_der'_mctxt_structure[OF assms(1)] have ?G4
    by (auto simp: ta_der'_target_args_def assms(2) split_vars_vars_term_list)
  moreover have ?G3 unfolding ta_der'_gctxt_def by auto
  ultimately show ?G1 ?G2 ?G3 ?G4 using t_split s_split
    by force+
qed


lemma ta_der'_ground_ctxt_structure:
  assumes "t |∈| ta_der' π’œ (term_of_gterm s)" "vars_term_list t = [q]"
  shows "t = (ta_der'_ctxt t)⟨Var q⟩"
    "s = (ta_der'_gctxt t)⟨ta_der'_source_gctxt_arg t s⟩G"
    "ground (ta_der'_source_ctxt_arg t (term_of_gterm s))"
    "q |∈| ta_der π’œ (ta_der'_source_ctxt_arg t (term_of_gterm s))"
  using ta_der'_ctxt_structure[OF assms] term_of_gterm_ctxt_apply
  by force+

subsection β€ΉSufficient condition for splitting the reachability relation induced by a tree automatonβ€Ί

locale derivation_split =
  fixes A :: "('q, 'f) ta" and π’œ and ℬ
  assumes rule_split: "rules A = rules π’œ |βˆͺ| rules ℬ"
    and eps_split: "eps A = eps π’œ |βˆͺ| eps ℬ"
    and B_target_states: "rule_target_states (rules ℬ) |βˆͺ| (snd |`| (eps ℬ)) |∩|
      (rule_arg_states (rules π’œ) |βˆͺ| (fst |`| (eps π’œ))) = {||}"
begin

abbreviation "Ξ”A ≑ rules π’œ"
abbreviation "Ξ”β„°A ≑ eps π’œ"
abbreviation "Ξ”B ≑ rules ℬ"
abbreviation "Ξ”β„°B ≑ eps ℬ"

abbreviation "𝒬A ≑ 𝒬 π’œ"
definition "𝒬B ≑ rule_target_states Ξ”B |βˆͺ| (snd |`| Ξ”β„°B)"
lemmas B_target_states' = B_target_states[folded 𝒬B_def]

lemma states_split [simp]: "𝒬 A = 𝒬 π’œ |βˆͺ| 𝒬 ℬ"
  by (auto simp add: 𝒬_def rule_split eps_split)

lemma A_args_states_not_B:
  "TA_rule f qs q |∈| Ξ”A ⟹ p |∈| fset_of_list qs ⟹ p |βˆ‰| 𝒬B"
  using B_target_states
  by (force simp add: 𝒬B_def)

lemma rule_statesD:
  "r |∈| Ξ”A ⟹ r_rhs r |∈| 𝒬A"
  "r |∈| Ξ”B ⟹ r_rhs r |∈| 𝒬B"
  "r |∈| Ξ”A ⟹ p |∈| fset_of_list (r_lhs_states r) ⟹ p |∈| 𝒬A"
  "TA_rule f qs q |∈| Ξ”A ⟹ q |∈| 𝒬A"
  "TA_rule f qs q |∈| Ξ”B ⟹ q |∈| 𝒬B"
  "TA_rule f qs q |∈| Ξ”A ⟹ p |∈| fset_of_list qs ⟹ p |∈| 𝒬A"
  by (auto simp: rule_statesD 𝒬B_def rev_image_eqI)

lemma eps_states_dest:
  "(p, q) |∈| Ξ”β„°A ⟹ p |∈| 𝒬A"
  "(p, q) |∈| Ξ”β„°A ⟹ q |∈| 𝒬A"
  "(p, q) |∈| Ξ”β„°A|+| ⟹ p |∈| 𝒬A"
  "(p, q) |∈| Ξ”β„°A|+| ⟹ q |∈| 𝒬A"
  "(p, q) |∈| Ξ”β„°B ⟹ q |∈| 𝒬B"
  "(p, q) |∈| Ξ”β„°B|+| ⟹ q |∈| 𝒬B"
  by (auto simp: eps_dest_all 𝒬B_def rev_image_eqI elim: ftranclE)

lemma transcl_eps_simp:
  "(eps A)|+| = Ξ”β„°A|+| |βˆͺ| Ξ”β„°B|+| |βˆͺ| (Ξ”β„°A|+| |O| Ξ”β„°B|+|)"
proof -
  have "Ξ”β„°B |O| Ξ”β„°A = {||}" using B_target_states'
    by (metis eps_states_dest(5) ex_fin_conv fimageI finterI frelcompE fst_conv inf_sup_distrib1 sup_eq_bot_iff)
  from ftrancl_Un2_separatorE[OF this] show ?thesis
    unfolding eps_split by auto
qed

lemma B_rule_eps_A_False:
  "f qs β†’ q |∈| Ξ”B ⟹ (q, p) |∈| Ξ”β„°A|+| ⟹ False"
  using B_target_states unfolding 𝒬B_def
  by (metis B_target_states' equalsffemptyD fimage_eqI finter_iff fst_conv ftranclD funion_iff local.rule_statesD(5))

lemma to_A_rule_set:
  assumes "TA_rule f qs q |∈| rules A" and "q = p ∨ (q, p) |∈| (eps A)|+|" and "p |βˆ‰| 𝒬B"
  shows "TA_rule f qs q |∈| Ξ”A" "q = p ∨ (q, p) |∈| Ξ”β„°A|+|" using assms
  unfolding transcl_eps_simp rule_split
  by (auto dest: rule_statesD eps_states_dest dest: B_rule_eps_A_False)

lemma to_B_rule_set:
  assumes "TA_rule f qs q |∈| rules A" and "q |βˆ‰| 𝒬A"
  shows "TA_rule f qs q |∈| Ξ”B" using assms
  unfolding transcl_eps_simp rule_split
  by (auto dest: rule_statesD eps_states_dest)


declare fsubsetI[rule del]
lemma ta_der_monos:
  "ta_der π’œ t |βŠ†| ta_der A t" "ta_der ℬ t |βŠ†| ta_der A t"
  by (auto simp: sup.coboundedI1 rule_split eps_split intro!: ta_der_mono)
declare fsubsetI[intro!]


lemma ta_der_from_Ξ”A:
  assumes "q |∈| ta_der A (term_of_gterm t)" and "q |βˆ‰| 𝒬B"
  shows "q |∈| ta_der π’œ (term_of_gterm t)" using assms
proof (induct rule: ta_der_gterm_induct)
  case (GFun f ts ps p q)
  have "i < length ts ⟹ ps ! i |βˆ‰| 𝒬B" for i using GFun A_args_states_not_B
    by (metis fnth_mem to_A_rule_set(1))
  then show ?case using GFun(2, 5) to_A_rule_set[OF GFun(1, 3, 6)]
    by (auto simp: transcl_eps_simp)
qed

lemma ta_state:
  assumes "q |∈| ta_der A (term_of_gterm s)"
  shows "q |∈| 𝒬A ∨ q |∈| 𝒬B" using assms
  by (cases s) (auto simp: rule_split transcl_eps_simp dest: rule_statesD eps_states_dest)

(* Main lemmas *)

lemma ta_der_split:
  assumes "q |∈| ta_der A (term_of_gterm s)" and "q |∈| 𝒬B"
  shows "βˆƒ t. t |∈| ta_der' π’œ (term_of_gterm s) ∧ q |∈| ta_der ℬ t"
    (is "βˆƒt . ?P s q t") using assms
proof (induct rule: ta_der_gterm_induct)
  case (GFun f ts ps p q)
  {fix i assume ass: "i < length ts"
    then have "βˆƒ t. t |∈| ta_der' π’œ (term_of_gterm (ts ! i)) ∧ ps ! i |∈| ta_der ℬ t"
    proof (cases "ps ! i |βˆ‰| 𝒬B")
      case True then show ?thesis
        using ta_state GFun(2, 4) ta_der_from_Ξ”A[of "ps ! i" "ts ! i"] ass
        by (intro exI[of _ "Var (ps ! i)"]) (auto simp: ta_der_to_ta_der' 𝒬B_def)
    next
      case False
      then have "ps ! i |∈| 𝒬B" using ta_state[OF GFun(4)[OF ass]]
        by auto 
      from GFun(5)[OF ass this] show ?thesis .
    qed}
  then obtain h where IH:
    "βˆ€ i < length ts. h i |∈| ta_der' π’œ (term_of_gterm (ts ! i))"
    "βˆ€ i < length ts. ps ! i |∈| ta_der ℬ (h i)"
    using GFun(1 - 4) choice_nat[of "length ts" "Ξ» t i. ?P (ts ! i) (ps ! i) t"]
    by blast
  from GFun(1) consider (A) "f ps β†’ p |∈| Ξ”A" | (B) "f ps β†’ p |∈| Ξ”B" by (auto simp: rule_split)
  then show ?case
  proof cases
    case A then obtain q' where eps_sp: "p = q' ∨ (p, q') |∈| Ξ”β„°A|+|"
      "q' = q ∨ (q', q) |∈| Ξ”β„°B|+|" using GFun(3, 6)
      by (auto simp: transcl_eps_simp dest: eps_states_dest)
    from GFun(4)[THEN ta_der_from_Ξ”A] A GFun(2, 4)
    have reach_fst: "p |∈| ta_der π’œ (term_of_gterm (GFun f ts))"
      using A_args_states_not_B by auto
    then have "q' |∈| ta_der π’œ (term_of_gterm (GFun f ts))" using eps_sp
      by (meson ta_der_trancl_eps)
    then show ?thesis using eps_sp(2)
      by (intro exI[of _ "Var q'"]) (auto simp flip: ta_der_to_ta_der' simp del: ta_der'_simps)
  next
    case B
    then have "p = q ∨ (p, q) |∈| Ξ”β„°B|+|" using GFun(3)
      by (auto simp: transcl_eps_simp dest: B_rule_eps_A_False)
    then show ?thesis using GFun(2, 4, 6) IH B
      by (auto intro!: exI[of _ "Fun f (map h [0 ..< length ts])"] exI[of _ ps])
  qed
qed


lemma ta_der'_split:
  assumes "t |∈| ta_der' A (term_of_gterm s)"
  shows "βˆƒ u. u |∈| ta_der' π’œ (term_of_gterm s) ∧ t |∈| ta_der' ℬ u"
    (is "βˆƒ u. ?P s t u") using assms
proof (induct s arbitrary: t)
  case (GFun f ts) show ?case
  proof (cases t)
    case [simp]: (Var q)
    have "q |∈| ta_der A (term_of_gterm (GFun f ts))" using GFun(2)
      by (auto simp flip: ta_der_to_ta_der')
    from ta_der_split[OF this] ta_der_from_Ξ”A[OF this] ta_state[OF this]
    show ?thesis unfolding Var
      by (metis ta_der'_refl ta_der_to_ta_der')
  next
    case [simp]: (Fun g ss)
    obtain h where IH:
      "βˆ€ i < length ts. h i |∈| ta_der' π’œ (term_of_gterm (ts ! i))"
      "βˆ€ i < length ts. ss ! i |∈| ta_der' ℬ (h i)"
      using GFun choice_nat[of "length ts" "Ξ» t i. ?P (ts ! i) (ss ! i) t"]
      by auto
    then show ?thesis using GFun(2)
      by (auto intro!: exI[of _ "Fun f (map h [0..<length ts])"])
  qed
qed

(* TODO rewrite using ta_der'_mctxt_structure *)
lemma ta_der_to_mcxtx:
  assumes "q |∈| ta_der A (term_of_gterm s)" and "q |∈| 𝒬B"
  shows "βˆƒ C ss qs. length qs = length ss ∧ num_holes C = length ss ∧
    (βˆ€ i < length ss. qs ! i |∈| ta_der π’œ (term_of_gterm (ss ! i))) ∧
    q |∈| ta_der ℬ (fill_holes C (map Var qs)) ∧
    ground_mctxt C ∧ fill_holes C (map term_of_gterm ss) = term_of_gterm s"
    (is "βˆƒC ss qs. ?P s q C ss qs")
proof -
  from ta_der_split[OF assms] obtain t where
    wit: "t |∈| ta_der' π’œ (term_of_gterm s)" "q |∈| ta_der ℬ t" by auto
  let ?C = "fst (split_vars t)" let ?ss = "map (gsubt_at s) (varposs_list t)"
  let ?qs = "snd (split_vars t)"
  have poss [simp]:"i < length (varposs_list t) ⟹ varposs_list t ! i ∈ gposs s" for i
    by (metis nth_mem ta_der'_poss[OF wit(1)] poss_gposs_conv subset_eq varposs_eq_varposs_list
        varposs_imp_poss varposs_list_var_terms_length)
  have len: "num_holes ?C = length ?ss" "length ?ss = length ?qs"
    by (simp_all add: split_vars_num_holes split_vars_vars_term_list varposs_list_var_terms_length)
  from unfill_holes_to_subst_at_hole_poss[OF ta_der'_inf_mctxt[OF wit(1)]]
  have "unfill_holes (fst (split_vars t)) (term_of_gterm s) = map (term_of_gterm ∘ gsubt_at s) (varposs_list t)"
    by (auto simp: comp_def hole_poss_split_vars_varposs_list
        dest: in_set_idx intro!: nth_equalityI term_of_gterm_gsubt)
  from fill_unfill_holes[OF ta_der'_inf_mctxt[OF wit(1)]] this
  have rep: "fill_holes ?C (map term_of_gterm ?ss) = term_of_gterm s"
    by simp
  have reach_int: "i < length ?ss ⟹ ?qs ! i |∈| ta_der π’œ (term_of_gterm (?ss ! i))" for i
    using wit(1) ta_der'_varposs_to_ta_der
    unfolding split_vars_vars_term_list length_map
    unfolding varposs_list_to_var_term_list[symmetric]
    by (metis nth_map nth_mem poss term_of_gterm_gsubt varposs_eq_varposs_list)
  have reach_end: "q |∈| ta_der ℬ (fill_holes ?C (map Var ?qs))" using wit
    using split_vars_fill_holes[of ?C t "map Var ?qs"]
    by auto
  show ?thesis using len rep reach_end reach_int
    by (metis split_vars_ground')
qed

lemma ta_der_to_gmcxtx:
  assumes "q |∈| ta_der A (term_of_gterm s)" and "q |∈| 𝒬B"
  shows "βˆƒ C ss qs qs'. length qs' = length qs ∧ length qs = length ss ∧ num_gholes C = length ss ∧
    (βˆ€ i < length ss. qs ! i |∈| ta_der π’œ (term_of_gterm (ss ! i))) ∧
    q |∈| ta_der ℬ (fill_holes (mctxt_of_gmctxt C) (map Var qs')) ∧
    fill_gholes C ss = s"
  using ta_der_to_mcxtx[OF assms]
  by (metis gmctxt_of_mctxt_inv ground_gmctxt_of_gterm_of_term num_gholes_gmctxt_of_mctxt term_of_gterm_inv)

(* Reconstuction *)

lemma mctxt_const_to_ta_der:
  assumes "num_holes C = length ss" "length ss = length qs"
    and "βˆ€ i < length qs. qs ! i |∈| ta_der π’œ (ss ! i)"
    and "q |∈| ta_der ℬ (fill_holes C (map Var qs))"
  shows "q |∈| ta_der A (fill_holes C ss)"
proof -
  have mid: "fill_holes C (map Var qs) |∈| ta_der' A (fill_holes C ss)"
    using assms(1 - 3) ta_der_monos(1)
    by (intro mctxt_args_ta_der') auto
  then show ?thesis using assms(1, 2) ta_der_monos(2)[THEN fsubsetD, OF assms(4)]
    using ta_der'_trans
    by (simp add: ta_der'_ta_der)
qed

lemma ctxt_const_to_ta_der:
  assumes "q |∈| ta_der π’œ s"
    and "p |∈| ta_der ℬ C⟨Var q⟩"
  shows "p |∈| ta_der A C⟨s⟩" using assms
  by (meson fin_mono ta_der_ctxt ta_der_monos(1) ta_der_monos(2))

lemma gctxt_const_to_ta_der:
  assumes "q |∈| ta_der π’œ (term_of_gterm s)"
    and "p |∈| ta_der ℬ (ctxt_of_gctxt C)⟨Var q⟩"
  shows "p |∈| ta_der A (term_of_gterm C⟨s⟩G)" using assms
  by (metis ctxt_const_to_ta_der ctxt_of_gctxt_inv ground_ctxt_of_gctxt ground_gctxt_of_ctxt_apply_gterm)

end
end