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)
      by (auto simp: 𝒯G_equivalent_def)}
  moreover
  {fix t assume "t ∈ ?Rs"
    then have f: "funas_gterm t βŠ† fset β„±" "βˆ€ q. q |∈| ta_der π’œ (term_of_gterm t) ⟢ q |βˆ‰| Q"
      by (auto simp: 𝒯G_equivalent_def)
    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
      by (auto simp: 𝒯G_equivalent_def filter_ta_sig_def
                 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 β„±"
      by (auto simp: 𝒯G_equivalent_def)
    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:
  "β„’ (filter_ta_reg β„± π’œ) = β„’ π’œ ∩ 𝒯G (fset β„±)"
  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