# 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
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
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)
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β©"
"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

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

lemma rule_statesD:
"r |β| Ξβ©A βΉ p |β| fset_of_list (r_lhs_states r) βΉ p |β| π¬β©A"
"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:
by (auto simp: eps_dest_all π¬β©B_def rev_image_eqI elim: ftranclE)

lemma transcl_eps_simp:
proof -
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:
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!]

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)"
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|β§+|"
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
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β©"