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_𝒬 by (fastforce simp add: image_iff) 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