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_𝒬
      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