# Theory Regular_Tree_Relations.Tree_Automata_Det

```theory Tree_Automata_Det
imports
Tree_Automata
begin

subsection ‹Powerset Construction for Tree Automata›

text ‹
The idea to treat states and transitions separately is from arXiv:1511.03595. Some parts of
the implementation are also based on that paper. (The Algorithm corresponds roughly to the one
in "Step 5")
›

text ‹Abstract Definitions and Correctness Proof›

definition ps_reachable_statesp where
"ps_reachable_statesp 𝒜 f ps = (λ q'. ∃ qs q. TA_rule f qs q |∈| rules 𝒜 ∧ list_all2 (|∈|) qs ps ∧
(q = q' ∨ (q,q') |∈| (eps 𝒜)|⇧+|))"

lemma ps_reachable_statespE:
assumes "ps_reachable_statesp 𝒜 f qs q"
obtains ps p where "TA_rule f ps p |∈| rules 𝒜" "list_all2 (|∈|) ps qs" "(p = q ∨ (p, q) |∈| (eps 𝒜)|⇧+|)"
using assms unfolding ps_reachable_statesp_def
by auto

lemma ps_reachable_statesp_𝒬:
"ps_reachable_statesp 𝒜 f ps q ⟹ q |∈| 𝒬 𝒜"
by (auto simp: ps_reachable_statesp_def simp flip: dest: rule_statesD eps_trancl_statesD)

lemma finite_Collect_ps_statep [simp]:
"finite (Collect (ps_reachable_statesp 𝒜 f ps))" (is "finite ?S")
by (intro finite_subset[of ?S "fset (𝒬 𝒜)"])
(auto simp: ps_reachable_statesp_𝒬)
lemmas finite_Collect_ps_statep_unfolded [simp] = finite_Collect_ps_statep[unfolded ps_reachable_statesp_def, simplified]

definition "ps_reachable_states 𝒜 f ps ≡ fCollect (ps_reachable_statesp 𝒜 f ps)"

lemmas ps_reachable_states_simp = ps_reachable_statesp_def ps_reachable_states_def

lemma ps_reachable_states_fmember:
"q' |∈| ps_reachable_states 𝒜 f ps ⟷ (∃ qs q. TA_rule f qs q |∈| rules 𝒜 ∧
list_all2 (|∈|) qs ps ∧ (q = q' ∨ (q, q') |∈| (eps 𝒜)|⇧+|))"
by (auto simp: ps_reachable_states_simp)

lemma ps_reachable_statesI:
assumes "TA_rule f ps p |∈| rules 𝒜" "list_all2 (|∈|) ps qs" "(p = q ∨ (p, q) |∈| (eps 𝒜)|⇧+|)"
shows "p |∈| ps_reachable_states 𝒜 f qs"
using assms unfolding ps_reachable_states_simp
by auto

lemma ps_reachable_states_sig:
"ps_reachable_states 𝒜 f ps ≠ {||} ⟹ (f, length ps) |∈| ta_sig 𝒜"
by (auto simp: ps_reachable_states_simp ta_sig_def image_iff intro!: bexI dest!: list_all2_lengthD)

text ‹
A set of "powerset states" is complete if it is sufficient to capture all (non)deterministic
derivations.
›

definition ps_states_complete_it :: "('a, 'b) ta ⇒ 'a FSet_Lex_Wrapper fset ⇒ 'a FSet_Lex_Wrapper fset ⇒ bool"
where "ps_states_complete_it 𝒜 Q Qnext ≡
∀f ps. fset_of_list ps |⊆| Q ∧ ps_reachable_states 𝒜 f (map ex ps) ≠ {||} ⟶ Wrapp (ps_reachable_states 𝒜 f (map ex ps)) |∈| Qnext"

lemma ps_states_complete_itD:
"ps_states_complete_it 𝒜 Q Qnext ⟹ fset_of_list ps |⊆| Q ⟹
ps_reachable_states 𝒜 f (map ex ps) ≠ {||} ⟹ Wrapp (ps_reachable_states 𝒜 f (map ex ps)) |∈| Qnext"
unfolding ps_states_complete_it_def by blast

abbreviation "ps_states_complete 𝒜 Q ≡ ps_states_complete_it 𝒜 Q Q"

text ‹The least complete set of states›
inductive_set ps_states_set for 𝒜 where
"∀ p ∈ set ps. p ∈ ps_states_set 𝒜 ⟹ ps_reachable_states 𝒜 f (map ex ps) ≠ {||} ⟹
Wrapp (ps_reachable_states 𝒜 f (map ex ps)) ∈ ps_states_set 𝒜"

lemma ps_states_Pow:
"ps_states_set 𝒜 ⊆ fset (Wrapp |`| fPow (𝒬 𝒜))"
proof -
{fix q assume "q ∈ ps_states_set 𝒜" then have "q ∈ fset (Wrapp |`| fPow (𝒬 𝒜))"
by induct (auto simp: ps_reachable_statesp_𝒬 ps_reachable_states_def image_iff)}
then show ?thesis by blast
qed

context
includes fset.lifting
begin
lift_definition ps_states  :: "('a, 'b) ta ⇒ 'a FSet_Lex_Wrapper fset" is ps_states_set
by (auto intro: finite_subset[OF ps_states_Pow])

lemma ps_states: "ps_states 𝒜 |⊆| Wrapp |`| fPow (𝒬 𝒜)" using ps_states_Pow
by (simp add: ps_states_Pow less_eq_fset.rep_eq ps_states.rep_eq)

lemmas ps_states_cases = ps_states_set.cases[Transfer.transferred]
lemmas ps_states_induct = ps_states_set.induct[Transfer.transferred]
lemmas ps_states_simps = ps_states_set.simps[Transfer.transferred]
lemmas ps_states_intros= ps_states_set.intros[Transfer.transferred]
end

lemma ps_states_complete:
"ps_states_complete 𝒜 (ps_states 𝒜)"
unfolding ps_states_complete_it_def
by (auto intro: ps_states_intros)

lemma ps_states_least_complete:
assumes "ps_states_complete_it 𝒜 Q Qnext" "Qnext |⊆| Q"
shows "ps_states 𝒜 |⊆| Q"
proof standard
fix q assume ass: "q |∈| ps_states 𝒜" then show "q |∈| Q"
using ps_states_complete_itD[OF assms(1)] fsubsetD[OF assms(2)]
by (induct rule: ps_states_induct[of _ 𝒜]) (fastforce intro: ass)+
qed

definition ps_rulesp :: "('a, 'b) ta ⇒ 'a FSet_Lex_Wrapper fset ⇒ ('a FSet_Lex_Wrapper, 'b) ta_rule ⇒ bool" where
"ps_rulesp 𝒜 Q = (λ r. ∃ f ps p. r = TA_rule f ps (Wrapp p) ∧ fset_of_list ps |⊆| Q ∧
p = ps_reachable_states 𝒜 f (map ex ps) ∧ p ≠ {||})"

definition "ps_rules" where
"ps_rules 𝒜 Q ≡ fCollect (ps_rulesp 𝒜 Q)"

lemma finite_ps_rulesp [simp]:
"finite (Collect (ps_rulesp 𝒜 Q))" (is "finite ?S")
proof -
let ?Q = "fset (Wrapp |`| fPow (𝒬 𝒜) |∪| Q)" let ?sig = "fset (ta_sig 𝒜)"
define args where "args ≡ ⋃ (f,n) ∈ ?sig. {qs| qs. set qs ⊆ ?Q ∧ length qs = n}"
define bound where "bound ≡ ⋃(f,_) ∈ ?sig. ⋃q ∈ ?Q. ⋃qs ∈ args. {TA_rule f qs q}"
have finite: "finite ?Q" "finite ?sig" by (auto intro: finite_subset)
then have "finite args" using finite_lists_length_eq[OF ‹finite ?Q›]
by (force simp: args_def)
with finite have "finite bound" unfolding bound_def by (auto simp only: finite_UN)
moreover have "Collect (ps_rulesp 𝒜 Q) ⊆ bound"
proof standard
fix r assume *: "r ∈ Collect (ps_rulesp 𝒜 Q)"
obtain f ps p where r[simp]: "r = TA_rule f ps p" by (cases r)
from * obtain qs q where "TA_rule f qs q |∈| rules 𝒜" and len: "length ps = length qs"
unfolding ps_rulesp_def ps_reachable_states_simp
using list_all2_lengthD by fastforce
from this have sym: "(f, length qs) ∈ ?sig"
by auto
moreover from * have "set ps ⊆ ?Q" unfolding ps_rulesp_def
by (auto simp flip: fset_of_list_elem simp: ps_reachable_statesp_def)
ultimately have ps: "ps ∈ args"
by (auto simp only: args_def UN_iff intro!: bexI[of _ "(f, length qs)"] len)
from * have "p ∈ ?Q" unfolding ps_rulesp_def ps_reachable_states_def
using ps_reachable_statesp_𝒬
with ps sym show "r ∈ bound"
by (auto simp only: r bound_def UN_iff intro!: bexI[of _ "(f, length qs)"] bexI[of _ "p"] bexI[of _ "ps"])
qed
ultimately show ?thesis by (blast intro: finite_subset)
qed

lemmas finite_ps_rulesp_unfolded = finite_ps_rulesp[unfolded ps_rulesp_def, simplified]

lemmas ps_rulesI [intro!] = fCollect_memberI[OF finite_ps_rulesp]

lemma ps_rules_states:
"rule_states (fCollect (ps_rulesp 𝒜 Q)) |⊆| (Wrapp |`| fPow (𝒬 𝒜) |∪| Q)"
by (auto simp: ps_rulesp_def rule_states_def ps_reachable_states_def ps_reachable_statesp_𝒬) blast

definition ps_ta :: "('q, 'f) ta ⇒ ('q FSet_Lex_Wrapper, 'f) ta" where
"ps_ta 𝒜 = (let Q = ps_states 𝒜 in
TA (ps_rules 𝒜 Q) {||})"

definition ps_ta_Q⇩f :: "'q fset ⇒ ('q, 'f) ta ⇒ 'q FSet_Lex_Wrapper fset" where
"ps_ta_Q⇩f Q 𝒜 = (let Q' = ps_states 𝒜 in
ffilter (λ S. Q |∩| (ex S) ≠ {||}) Q')"

lemma ps_rules_sound:
assumes "p |∈| ta_der (ps_ta 𝒜) (term_of_gterm t)"
shows "ex p |⊆| ta_der 𝒜 (term_of_gterm t)" using assms
proof (induction rule: ta_der_gterm_induct)
case (GFun f ts ps p q)
then have IH: "∀i < length ts. ex (ps ! i) |⊆| gta_der 𝒜 (ts ! i)" unfolding gta_der_def by auto
show ?case
proof standard
fix r assume "r |∈| ex q"
with GFun(1 - 3) obtain qs q' where "TA_rule f qs q' |∈| rules 𝒜"
"q' = r ∨ (q', r) |∈| (eps 𝒜)|⇧+|" "list_all2 (|∈|) qs (map ex ps)"
by (auto simp: Let_def ps_ta_def ps_rulesp_def ps_reachable_states_simp ps_rules_def)
then show "r |∈| ta_der 𝒜 (term_of_gterm (GFun f ts))"
using GFun(2) IH unfolding gta_der_def
by (force dest!: fsubsetD intro!: exI[of _ q'] exI[of _ qs] simp: list_all2_conv_all_nth)
qed
qed

lemma ps_ta_nt_empty_set:
"TA_rule f qs (Wrapp {||}) |∈| rules (ps_ta 𝒜) ⟹ False"
by (auto simp: ps_ta_def ps_rulesp_def ps_rules_def)

lemma ps_rules_not_empty_reach:
assumes "Wrapp {||} |∈| ta_der (ps_ta 𝒜) (term_of_gterm t)"
shows False using assms
proof (induction t)
case (GFun f ts)
then show ?case using ps_ta_nt_empty_set[of f _ 𝒜]
by (auto simp: ps_ta_def)
qed

lemma ps_rules_complete:
assumes "q |∈| ta_der 𝒜 (term_of_gterm t)"
shows "∃p. q |∈| ex p ∧ p |∈| ta_der (ps_ta 𝒜) (term_of_gterm t) ∧ p |∈| ps_states 𝒜" using assms
proof (induction  rule: ta_der_gterm_induct)
let ?P = "λt q p. q |∈| ex p ∧ p |∈| ta_der (ps_ta 𝒜) (term_of_gterm t) ∧ p |∈| ps_states 𝒜"
case (GFun f ts ps p q)
then have "∀i. ∃p. i < length ts ⟶ ?P (ts ! i) (ps ! i) p" by auto
with choice[OF this] obtain psf where ps: "∀i < length ts. ?P (ts ! i) (ps ! i) (psf i)" by auto
define qs where "qs = map psf [0 ..< length ts]"
let ?p = "ps_reachable_states 𝒜 f (map ex qs)"
from ps have in_Q: "fset_of_list qs |⊆| ps_states 𝒜"
by (auto simp: qs_def fset_of_list_elem)
from ps GFun(2) have all: "list_all2 (|∈|) ps (map ex qs)"
by (auto simp: list_all2_conv_all_nth qs_def)
then have in_p: "q |∈| ?p" using GFun(1, 3)
unfolding ps_reachable_statesp_def ps_reachable_states_def by auto
then have rule: "TA_rule f qs (Wrapp ?p) |∈| ps_rules 𝒜 (ps_states 𝒜)" using in_Q unfolding ps_rules_def
by (intro ps_rulesI) (auto simp: ps_rulesp_def)
from in_Q in_p have "Wrapp ?p |∈| (ps_states 𝒜)"
by (auto intro!: ps_states_complete[unfolded ps_states_complete_it_def, rule_format])
with in_p ps rule show ?case
by (auto intro!: exI[of _ "Wrapp ?p"] exI[of _ qs] simp: ps_ta_def qs_def)
qed

lemma ps_ta_eps[simp]: "eps (ps_ta 𝒜) = {||}" by (auto simp: Let_def ps_ta_def)

lemma ps_ta_det[iff]: "ta_det (ps_ta 𝒜)" by (auto simp: Let_def ps_ta_def ta_det_def ps_rulesp_def ps_rules_def)

lemma ps_gta_lang:
"gta_lang (ps_ta_Q⇩f Q 𝒜) (ps_ta 𝒜) = gta_lang Q 𝒜" (is "?R = ?L")
proof standard
show "?L ⊆ ?R" proof standard
fix t assume "t ∈ ?L"
then obtain q where q_res: "q |∈| ta_der 𝒜 (term_of_gterm t)" and q_final: "q |∈| Q"
by auto
from ps_rules_complete[OF q_res] obtain p where
"p |∈| ps_states 𝒜" "q |∈| ex p" "p |∈| ta_der (ps_ta 𝒜) (term_of_gterm t)"
by auto
moreover with q_final have "p |∈| ps_ta_Q⇩f Q 𝒜"
by (auto simp: ps_ta_Q⇩f_def)
ultimately show "t ∈ ?R" by auto
qed
show "?R ⊆ ?L" proof standard
fix t assume "t ∈ ?R"
then obtain p where
p_res: "p |∈| ta_der (ps_ta 𝒜) (term_of_gterm t)" and p_final: "p |∈| ps_ta_Q⇩f Q 𝒜"
by (auto simp: ta_lang_def)
from ps_rules_sound[OF p_res] have "ex p |⊆| ta_der 𝒜 (term_of_gterm t)"
by auto
moreover from p_final obtain q where "q |∈| ex p" "q |∈| Q" by (auto simp:  ps_ta_Q⇩f_def)
ultimately show "t ∈ ?L" by auto
qed
qed

definition ps_reg where
"ps_reg R = Reg (ps_ta_Q⇩f (fin R) (ta R)) (ps_ta (ta R))"

lemma ℒ_ps_reg:
"ℒ (ps_reg R) = ℒ R"
by (auto simp: ℒ_def ps_gta_lang ps_reg_def)

lemma ps_ta_states: "𝒬 (ps_ta 𝒜) |⊆| Wrapp |`| fPow (𝒬 𝒜)"
using ps_rules_states ps_states unfolding ps_ta_def 𝒬_def
by (auto simp: Let_def ps_rules_def) force

lemma ps_ta_states': "ex |`| 𝒬 (ps_ta 𝒜) |⊆| fPow (𝒬 𝒜)"
using ps_ta_states[of 𝒜]
by fastforce

end
```