theory Tree_Automata_Complement imports Tree_Automata_Det begin definition completely_defined_on where "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: "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 simp flip: fmember.rep_eq 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 ℱ" apply (induct rule: ta_der_gterm_induct) apply (auto simp: sig_ta_rules_fmember simp flip: fmember.rep_eq) by (metis in_mono in_set_idx notin_fset)} ultimately show ?thesis unfolding completely_defined_on_def by blast qed lemma ta_der_fsubset_sig_ta_completely: assumes "ta_subset (sig_ta ℱ) 𝒜" "ta_sig 𝒜 |⊆| ℱ" shows "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: completely_defined_on_def) (metis ffunas_gterm.rep_eq fin_mono notin_fset ta_der_gterm_sig) qed lemma completely_definied_ps_taI: "completely_defined_on 𝒜 ℱ ⟹ completely_defined_on (ps_ta 𝒜) ℱ" unfolding completely_defined_on_def using ps_rules_not_empty_reach[of 𝒜] using fsubsetD[OF ps_rules_sound[of _ 𝒜]] ps_rules_complete[of _ 𝒜] by auto fastforce+ lemma completely_definied_ta_union1I: "completely_defined_on 𝒜 ℱ ⟹ ta_sig ℬ |⊆| ℱ ⟹ 𝒬 𝒜 |∩| 𝒬 ℬ = {||} ⟹ completely_defined_on (ta_union 𝒜 ℬ) ℱ" unfolding 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: "completely_defined_on 𝒜 ℱ ⟹ finj_on f (𝒬 𝒜) ⟹ completely_defined_on (fmap_states_ta f 𝒜) ℱ" unfolding 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 "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 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: 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 𝒜)" 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 simp flip: fmember.rep_eq intro!: exI[of _ ps] exI[of _ p]) qed then have "t ∈ ?Ls" using p(1) by auto} ultimately show ?thesis by blast qed 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 𝒜))" declare equalityI [rule del] 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_lang ℒ_union ℒ_sig_ta_reg) qed declare equalityI [intro!] end