# Theory Regular_Tree_Relations.Tree_Automata_Complement

```theory Tree_Automata_Complement
imports Tree_Automata_Det
begin

subsection βΉComplement closure of regular languagesβΊ

definition partially_completely_defined_on where
"partially_completely_defined_on π β± β·
(β t. funas_gterm t β fset β± β· (β q. q |β| ta_der π (term_of_gterm t)))"

definition sig_ta where
"sig_ta β± = TA ((Ξ» (f, n). TA_rule f (replicate n ()) ()) |`| β±) {||}"

lemma sig_ta_rules_fmember:
"TA_rule f qs q |β| rules (sig_ta β±) β· (β n. (f, n) |β| β± β§ qs = replicate n () β§ q = ())"
by (auto simp: sig_ta_def fimage_iff fBex_def)

lemma sig_ta_completely_defined:
"partially_completely_defined_on (sig_ta β±) β±"
proof -
{fix t assume "funas_gterm t β fset β±"
then have "() |β| ta_der (sig_ta β±) (term_of_gterm t)"
proof (induct t)
case (GFun f ts)
then show ?case
by (auto simp: sig_ta_rules_fmember SUP_le_iff
intro!: exI[of _ "replicate (length ts) ()"])
qed}
moreover
{fix t q assume "q |β| ta_der (sig_ta β±) (term_of_gterm t)"
then have "funas_gterm t β fset β±"
proof (induct rule: ta_der_gterm_induct)
case (GFun f ts ps p q)
from GFun(1 - 4) GFun(5)[THEN subsetD] show ?case
by (auto simp: sig_ta_rules_fmember dest!: in_set_idx)
qed}
ultimately show ?thesis
unfolding partially_completely_defined_on_def
by blast
qed

lemma ta_der_fsubset_sig_ta_completely:
assumes "ta_subset (sig_ta β±) π" "ta_sig π |β| β±"
shows "partially_completely_defined_on π β±"
proof -
have "ta_der (sig_ta β±) t |β| ta_der π t" for t
using assms by (simp add: ta_der_mono')
then show ?thesis using sig_ta_completely_defined assms(2)
by (auto simp: partially_completely_defined_on_def)
(metis ffunas_gterm.rep_eq fin_mono ta_der_gterm_sig)
qed

lemma completely_definied_ps_taI:
"partially_completely_defined_on π β± βΉ partially_completely_defined_on (ps_ta π) β±"
unfolding partially_completely_defined_on_def
using ps_rules_not_empty_reach[of π]
using fsubsetD[OF ps_rules_sound[of _ π]] ps_rules_complete[of _ π]
by (metis FSet_Lex_Wrapper.collapse fsubsetI fsubset_fempty)

lemma completely_definied_ta_union1I:
"partially_completely_defined_on π β± βΉ ta_sig β¬ |β| β± βΉ π¬ π |β©| π¬ β¬ = {||} βΉ
partially_completely_defined_on (ta_union π β¬) β±"
unfolding partially_completely_defined_on_def
using ta_union_der_disj_states'[of π β¬]
by (auto simp: ta_union_der_disj_states)
(metis ffunas_gterm.rep_eq fsubset_trans less_eq_fset.rep_eq ta_der_gterm_sig)

lemma completely_definied_fmaps_statesI:
"partially_completely_defined_on π β± βΉ finj_on f (π¬ π) βΉ partially_completely_defined_on (fmap_states_ta f π) β±"
unfolding partially_completely_defined_on_def
using fsubsetD[OF ta_der_fmap_states_ta_mono2, of f π]
using ta_der_to_fmap_states_der[of _ π _ f]
by (auto simp: fimage_iff fBex_def) fastforce+

lemma det_completely_defined_complement:
assumes "partially_completely_defined_on π β±" "ta_det π"
shows "gta_lang (π¬ π |-| Q) π = π―β©G (fset β±) - gta_lang Q π" (is "?Ls = ?Rs")
proof -
{fix t assume "t β ?Ls"
then obtain p where p: "p |β| π¬ π" "p |β| Q" "p |β| ta_der π (term_of_gterm t)"
by auto
from ta_detE[OF assms(2) p(3)] have "β q. q |β| ta_der π (term_of_gterm t) βΆ q = p"
by blast
moreover have "funas_gterm t β fset β±"
using p(3) assms(1) unfolding partially_completely_defined_on_def
by (auto simp: less_eq_fset.rep_eq ffunas_gterm.rep_eq)
ultimately have "t β ?Rs" using p(2)
moreover
{fix t assume "t β ?Rs"
then have f: "funas_gterm t β fset β±" "β q. q |β| ta_der π (term_of_gterm t) βΆ q |β| Q"
from f(1) obtain p where "p |β| ta_der π (term_of_gterm t)" using assms(1)
by (force simp: partially_completely_defined_on_def)
then have "t β ?Ls" using f(2)
by (auto simp: gterm_ta_der_states intro: gta_langI[of p])}
ultimately show ?thesis by blast
qed

lemma ta_der_gterm_sig_fset:
"q |β| ta_der π (term_of_gterm t) βΉ funas_gterm t β fset (ta_sig π)"
using ta_der_gterm_sig
by (metis ffunas_gterm.rep_eq less_eq_fset.rep_eq)

definition filter_ta_sig where
"filter_ta_sig β± π = TA (ffilter (Ξ» r. (r_root r, length (r_lhs_states r)) |β| β±) (rules π)) (eps π)"

definition filter_ta_reg where
"filter_ta_reg β± R = Reg (fin R) (filter_ta_sig β± (ta R))"

lemma filter_ta_sig:
"ta_sig (filter_ta_sig β± π) |β| β±"
by (auto simp: ta_sig_def filter_ta_sig_def)

lemma filter_ta_sig_lang:
"gta_lang Q (filter_ta_sig β± π) = gta_lang Q π β© π―β©G (fset β±)" (is "?Ls = ?Rs")
proof -
let ?A = "filter_ta_sig β± π"
{fix t assume "t β ?Ls"
then obtain q where q: "q |β| Q" "q |β| ta_der ?A (term_of_gterm t)"
by auto
then have "funas_gterm t β fset β±"
using subset_trans[OF ta_der_gterm_sig_fset[OF q(2)] filter_ta_sig[unfolded less_eq_fset.rep_eq]]
by blast
then have "t β ?Rs" using q
intro!: gta_langI[of q] ta_der_el_mono[where ?q = q and β¬ = π and π = ?A])}
moreover
{fix t assume ass: "t β ?Rs"
then have funas: "funas_gterm t β fset β±"
from ass obtain p where p: "p |β| Q" "p |β| ta_der π (term_of_gterm t)"
by auto
from this(2) funas have "p |β| ta_der ?A (term_of_gterm t)"
proof (induct rule: ta_der_gterm_induct)
case (GFun f ts ps p q)
then show ?case
by (auto simp: filter_ta_sig_def SUP_le_iff intro!: exI[of _ ps] exI[of _ p])
qed
then have "t β ?Ls" using p(1) by auto}
ultimately show ?thesis by blast
qed

lemma β_filter_ta_reg:
using filter_ta_sig_lang
by (auto simp: β_def filter_ta_reg_def)

definition sig_ta_reg where
"sig_ta_reg β± = Reg {||} (sig_ta β±)"

lemma β_sig_ta_reg:
"β (sig_ta_reg β±) = {}"
by (auto simp: β_def sig_ta_reg_def)

definition complement_reg where
"complement_reg R β± = (let π = ps_reg (reg_union (sig_ta_reg β±) R) in
Reg (π¬β©r π |-| fin π) (ta π))"

lemma β_complement_reg:
assumes "ta_sig (ta π) |β| β±"
shows "β (complement_reg π β±) = π―β©G (fset β±) - β π"
proof -
have "β (complement_reg π β±) = π―β©G (fset β±) - β (ps_reg (reg_union (sig_ta_reg β±) π))"
unfolding β_def complement_reg_def using assms
by (auto simp: complement_reg_def Let_def ps_reg_def reg_union_def sig_ta_reg_def
sig_ta_completely_defined finj_Inl_Inr
intro!: det_completely_defined_complement completely_definied_ps_taI
completely_definied_ta_union1I completely_definied_fmaps_statesI)
then show ?thesis
by (auto simp: β_ps_reg β_union β_sig_ta_reg)
qed

lemma β_complement_filter_reg:
"β (complement_reg (filter_ta_reg β± π) β±) = π―β©G (fset β±) - β π"
proof -
have *: "ta_sig (ta (filter_ta_reg β± π)) |β| β±"
by (auto simp: filter_ta_reg_def filter_ta_sig)
show ?thesis unfolding β_complement_reg[OF *] β_filter_ta_reg
by blast
qed

definition difference_reg where
"difference_reg R L = (let F = ta_sig (ta R) in
reg_intersect R (trim_reg (complement_reg (filter_ta_reg F L) F)))"

lemma β_difference_reg:
"β (difference_reg R L) = β R - β L" (is "?Ls = ?Rs")
unfolding difference_reg_def Let_def β_trim β_intersect β_complement_filter_reg
using reg_funas by blast

end```