Theory Regular_Tree_Relations.Tree_Automata_Abstract_Impl

theory Tree_Automata_Abstract_Impl
  imports Tree_Automata_Det Horn_Fset
begin

section ‹Computing state derivation›

lemma ta_der_Var_code [code]:
  "ta_der 𝒜 (Var q) = finsert q ((eps 𝒜)|⇧+| |``| {|q|})"
  by (auto)

lemma ta_der_Fun_code [code]:
  "ta_der 𝒜 (Fun f ts) =
     (let args = map (ta_der 𝒜) ts in
      let P = (λ r. case r of TA_rule g ps p ⇒ f = g ∧ list_all2 fmember ps args) in
      let S = r_rhs |`| ffilter P (rules 𝒜) in
         S |∪| (eps 𝒜)|⇧+| |``| S)" (is "?Ls = ?Rs")
proof
  {fix q assume "q |∈| ?Ls" then have "q |∈| ?Rs"
      apply (simp add: Let_def fImage_iff fBex_def image_iff)
      by (smt (verit, ccfv_threshold) IntI length_map list_all2_conv_all_nth mem_Collect_eq nth_map
          ta_rule.case ta_rule.sel(3))
    }
  then show "?Ls |⊆| ?Rs" by blast
next
  {fix q assume "q |∈| ?Rs" then have "q |∈| ?Ls"
      apply (auto simp: Let_def ffmember_filter fimage_iff fBex_def list_all2_conv_all_nth fImage_iff
                  split!: ta_rule.splits)
      apply (metis ta_rule.collapse)
      apply blast
      done}
  then show "?Rs |⊆| ?Ls" by blast
qed

definition eps_free_automata where
  "eps_free_automata epscl 𝒜 =
  (let ruleps = (λ r. finsert (r_rhs r) (epscl |``| {|r_rhs r|})) in
   let rules = (λ r. (λ q. TA_rule (r_root r) (r_lhs_states r) q) |`| (ruleps r)) |`| (rules 𝒜) in
   TA ( |⋃| rules) {||})"

lemma eps_free [code]:
  "eps_free 𝒜 = eps_free_automata ((eps 𝒜)|⇧+|) 𝒜"
  apply (intro TA_equalityI)
   apply (auto simp: eps_free_def eps_free_rulep_def eps_free_automata_def)
  using fBex_def apply fastforce
  apply (metis ta_rule.exhaust_sel)+
  done


lemma eps_of_eps_free_automata [simp]:
  "eps (eps_free_automata S 𝒜) = {||}"
  by (auto simp add: eps_free_automata_def)

lemma eps_free_automata_empty [simp]:
  "eps 𝒜 = {||} ⟹ eps_free_automata {||} 𝒜 = 𝒜"
  by (auto simp add: eps_free_automata_def intro!: TA_equalityI)

section ‹Computing the restriction of tree automata to state set›

lemma ta_restrict [code]:
  "ta_restrict 𝒜 Q =
     (let rules =  ffilter (λ r. case r of TA_rule f ps p ⇒ fset_of_list ps |⊆| Q ∧ p |∈| Q) (rules 𝒜) in
      let eps = ffilter (λ r. case r of (p, q) ⇒ p |∈| Q ∧ q |∈| Q) (eps 𝒜) in
      TA rules eps)"
  by (auto simp: Let_def ta_restrict_def split!: ta_rule.splits intro: finite_subset[OF _ finite_Collect_ta_rule])


section ‹Computing the epsilon transition for the product automaton›

lemma prod_eps[code_unfold]:
  "fCollect (prod_epsLp 𝒜 ℬ) = (λ ((p, q), r). ((p, r), (q, r))) |`| (eps 𝒜 |×| 𝒬 ℬ)"
  "fCollect (prod_epsRp 𝒜 ℬ) = (λ ((p, q), r). ((r, p), (r, q))) |`| (eps ℬ |×| 𝒬 𝒜)"
  by (auto simp: finite_prod_epsLp prod_epsLp_def finite_prod_epsRp prod_epsRp_def image_iff
      fSigma.rep_eq) force+

section ‹Computing reachability›

inductive_set ta_reach for 𝒜 where
   rule [intro]: "f qs → q |∈| rules 𝒜 ⟹ ∀ i < length qs. qs ! i ∈ ta_reach 𝒜 ⟹ q ∈ ta_reach 𝒜"
 |  eps [intro]: "q ∈ ta_reach 𝒜 ⟹ (q, r) |∈| eps 𝒜 ⟹ r ∈ ta_reach 𝒜"


lemma ta_reach_eps_transI:
  assumes "(p, q) |∈| (eps 𝒜)|⇧+|" "p ∈ ta_reach 𝒜"
  shows "q ∈ ta_reach 𝒜" using assms
  by (induct rule: ftrancl_induct) auto

lemma ta_reach_ground_term_der:
  assumes "q ∈ ta_reach 𝒜"
  shows "∃ t. ground t ∧ q |∈| ta_der 𝒜 t" using assms
proof (induct)
  case (rule f qs q)
  then obtain ts where "length ts = length qs"
    "∀ i < length qs. ground (ts ! i)"
    "∀ i < length qs. qs ! i |∈| ta_der 𝒜 (ts ! i)"
    using Ex_list_of_length_P[of "length qs" "λ t i. ground t ∧ qs ! i |∈| ta_der 𝒜 t"]
    by auto
  then show ?case using rule(1)
    by (auto dest!: in_set_idx intro!: exI[of _ "Fun f ts"]) blast
qed (auto, meson ta_der_eps)

lemma ground_term_der_ta_reach:
  assumes "ground t" "q |∈| ta_der 𝒜 t"
  shows "q ∈ ta_reach 𝒜" using assms(2, 1)
  by (induct rule: ta_der_induct) (auto simp add: rule ta_reach_eps_transI)

lemma ta_reach_reachable:
  "ta_reach 𝒜 = fset (ta_reachable 𝒜)"
  using ta_reach_ground_term_der[of _ 𝒜]
  using ground_term_der_ta_reach[of _ _ 𝒜]
  unfolding ta_reachable_def
  by auto


subsection ‹Horn setup for reachable states›
definition "reach_rules 𝒜 =
  {qs →⇩h q | f qs q. TA_rule f qs q |∈| rules 𝒜} ∪
  {[q] →⇩h r | q r. (q, r) |∈| eps 𝒜}"

locale reach_horn =
  fixes 𝒜 :: "('q, 'f) ta"
begin

sublocale horn "reach_rules 𝒜" .

lemma reach_infer0: "infer0 = {q | f q. TA_rule f [] q |∈| rules 𝒜}"
  by (auto simp: horn.infer0_def reach_rules_def)

lemma reach_infer1:
  "infer1 p X = {r | f qs r. TA_rule f qs r |∈| rules 𝒜 ∧ p ∈ set qs ∧ set qs ⊆ insert p X} ∪
   {r | r. (p, r) |∈| eps 𝒜}"
  unfolding reach_rules_def
  by (auto simp: horn.infer1_def simp flip: ex_simps(1))

lemma reach_sound:
  "ta_reach 𝒜 = saturate"
proof (intro set_eqI iffI, goal_cases lr rl)
  case (lr x) obtain p where x: "p = ta_reach 𝒜" by auto
  show ?case using lr unfolding x
  proof (induct)
    case (rule f qs q)
    then show ?case
      by (intro infer[of qs q]) (auto simp: reach_rules_def dest: in_set_idx)
  next
    case (eps q r)
    then show ?case
      by (intro infer[of "[q]" r]) (auto simp: reach_rules_def)
  qed
next
  case (rl x)
  then show ?case
    by (induct) (auto simp: reach_rules_def)
qed
end

subsection ‹Computing productivity›

text ‹First, use an alternative definition of productivity›

inductive_set ta_productive_ind :: "'q fset ⇒ ('q,'f) ta ⇒ 'q set" for P and 𝒜 :: "('q,'f) ta" where
  basic [intro]: "q |∈| P ⟹ q ∈ ta_productive_ind P 𝒜"
| eps [intro]: "(p, q) |∈| (eps 𝒜)|⇧+| ⟹ q ∈ ta_productive_ind P 𝒜 ⟹ p ∈ ta_productive_ind P 𝒜"
| rule: "TA_rule f qs q |∈| rules 𝒜 ⟹ q ∈ ta_productive_ind P 𝒜 ⟹ q' ∈ set qs ⟹ q' ∈ ta_productive_ind P 𝒜"

lemma ta_productive_ind:
  "ta_productive_ind P 𝒜 = fset (ta_productive P 𝒜)" (is "?LS = ?RS")
proof -
  {fix q assume "q ∈ ?LS" then have "q ∈ ?RS"
      by (induct) (auto dest: ta_prod_epsD intro: ta_productive_setI,
         metis (full_types) in_set_conv_nth rule_reachable_ctxt_exist ta_productiveI')}
  moreover
  {fix q assume "q ∈ ?RS" note * = this
    from ta_productiveE[OF *] obtain r C where
      reach : "r |∈| ta_der 𝒜 C⟨Var q⟩" and f: "r |∈| P" by auto
    from f have "r ∈ ta_productive_ind P 𝒜" "r |∈| ta_productive P 𝒜"
      by (auto intro: ta_productive_setI)
    then have "q ∈ ?LS" using reach
    proof (induct C arbitrary: q r)
      case (More f ss C ts)
      from iffD1 ta_der_Fun[THEN iffD1, OF More(4)[unfolded ctxt_apply_term.simps]] obtain ps p where
        inv: "f ps → p |∈| rules 𝒜" "p = r ∨ (p, r) |∈| (eps 𝒜)|⇧+|" "length ps = length (ss @ C⟨Var q⟩ # ts)"
             "ps ! length ss |∈| ta_der 𝒜 C⟨Var q⟩"
        by (auto simp: nth_append_Cons split: if_splits)
      then have "p ∈ ta_productive_ind P 𝒜 ⟹ p |∈| ta_der 𝒜 C⟨Var q⟩ ⟹ q ∈ ta_productive_ind P 𝒜" for p
        using More(1) calculation by auto
      note [intro!] = this[of "ps ! length ss"]
      show ?case using More(2) inv
        by (auto simp: nth_append_Cons ta_productive_ind.rule)
           (metis less_add_Suc1 nth_mem ta_productive_ind.simps)
    qed (auto intro: ta_productive_setI)
  }
  ultimately show ?thesis by auto
qed


subsubsection ‹Horn setup for productive states›

definition "productive_rules P 𝒜 = {[] →⇩h q | q. q |∈| P} ∪
  {[r] →⇩h q | q r. (q, r) |∈| eps 𝒜} ∪
  {[q] →⇩h r | f qs q r. TA_rule f qs q |∈| rules 𝒜 ∧ r ∈ set qs}"

locale productive_horn =
  fixes 𝒜 :: "('q, 'f) ta" and P :: "'q fset"
begin

sublocale horn "productive_rules P 𝒜" .

lemma productive_infer0: "infer0 = fset P"
  by (auto simp: productive_rules_def horn.infer0_def)

lemma productive_infer1:
  "infer1 p X = {r | r. (r, p) |∈| eps 𝒜} ∪
    {r | f qs r. TA_rule f qs p |∈| rules 𝒜 ∧ r ∈ set qs}"
  unfolding productive_rules_def horn_infer1_union
  by (auto simp add: horn.infer1_def)
     (metis insertCI list.set(1) list.simps(15) singletonD subsetI)

lemma productive_sound:
  "ta_productive_ind P 𝒜 = saturate"
proof (intro set_eqI iffI, goal_cases lr rl)
  case (lr p) then show ?case using lr
  proof (induct)
    case (basic q)
    then show ?case
      by (intro infer[of "[]" q]) (auto simp: productive_rules_def)
  next
    case (eps p q) then show ?case
    proof (induct rule: ftrancl_induct)
      case (Base p q)
      then show ?case using infer[of "[q]" p]
        by (auto simp: productive_rules_def)
    next
      case (Step p q r)
      then show ?case using infer[of "[r]" q]
        by (auto simp: productive_rules_def)
    qed
  next
    case (rule f qs q p)
    then show ?case
      by (intro infer[of "[q]" p]) (auto simp: productive_rules_def)
  qed
next
  case (rl p)
  then show ?case
    by (induct) (auto simp: productive_rules_def ta_productive_ind.rule)
qed
end

subsection ‹Horn setup for power set construction states›

lemma prod_list_exists:
  assumes "fst p ∈ set qs" "set qs ⊆ insert (fst p) (fst ` X)"
  obtains as where "p ∈ set as" "map fst as = qs" "set as ⊆ insert p X"
proof -
  from assms have "qs ∈ lists (fst ` (insert p X))" by blast
  then obtain ts where ts: "map fst ts = qs" "ts ∈ lists (insert p X)"
    by (metis image_iff lists_image)
  then obtain i where mem: "i < length qs" "qs ! i = fst p" using assms(1)
    by (metis in_set_idx)
  from ts have p: "ts[i := p] ∈ lists (insert p X)"
    using set_update_subset_insert by fastforce
  then have "p ∈ set (ts[i := p])" "map fst (ts[i := p]) = qs" "set (ts[i := p]) ⊆ insert p X"
    using mem ts(1)
    by (auto simp add: nth_list_update set_update_memI intro!: nth_equalityI)
  then show ?thesis using that
    by blast
qed

definition "ps_states_rules 𝒜 = {rs →⇩h (Wrapp q) | rs f q.
    q = ps_reachable_states 𝒜 f (map ex rs) ∧ q ≠ {||}}"

locale ps_states_horn =
  fixes 𝒜 :: "('q, 'f) ta"
begin

sublocale horn "ps_states_rules 𝒜" .

lemma ps_construction_infer0: "infer0 =
  {Wrapp q | f q. q = ps_reachable_states 𝒜 f [] ∧ q ≠ {||}}"
    by (auto simp: ps_states_rules_def horn.infer0_def)

lemma ps_construction_infer1:
  "infer1 p X = {Wrapp q | f qs q. q = ps_reachable_states 𝒜 f (map ex qs) ∧ q ≠ {||} ∧
   p ∈ set qs ∧ set qs ⊆ insert p X}"
  unfolding ps_states_rules_def horn_infer1_union
  by (auto simp add: horn.infer1_def ps_reachable_states_def comp_def elim!: prod_list_exists) 

lemma ps_states_sound:
  "ps_states_set 𝒜 = saturate"
proof (intro set_eqI iffI, goal_cases lr rl)
  case (lr p) then show ?case using lr
  proof (induct)
    case (1 ps f)
    then have "ps →⇩h (Wrapp (ps_reachable_states 𝒜 f (map ex ps))) ∈ ps_states_rules 𝒜"
      by (auto simp: ps_states_rules_def)
    then show ?case using horn.saturate.simps 1
      by fastforce
  qed
next
  case (rl p)
  then obtain q where "q ∈ saturate" "q = p" by blast
  then show ?case
    by (induct arbitrary: p)
       (auto simp: ps_states_rules_def intro!: ps_states_set.intros)
qed

end

definition ps_reachable_states_cont where
  "ps_reachable_states_cont Δ Δ⇩ε f ps =
   (let R = ffilter (λ r. case r of TA_rule g qs q ⇒ f = g ∧ list_all2 (|∈|) qs ps) Δ in
    let S = r_rhs |`| R in
    S |∪| Δ⇩ε|⇧+| |``| S)"

lemma ps_reachable_states [code]:
  "ps_reachable_states (TA Δ Δ⇩ε) f ps = ps_reachable_states_cont Δ Δ⇩ε f ps"
  by (auto simp: ps_reachable_states_fmember ps_reachable_states_cont_def Let_def fimage_iff fBex_def
           split!: ta_rule.splits) force+

definition ps_rules_cont where
 "ps_rules_cont 𝒜 Q =
   (let sig = ta_sig 𝒜 in
    let qss = (λ (f, n). (f, n, fset_of_list (List.n_lists n (sorted_list_of_fset Q)))) |`| sig in
    let res = (λ (f, n, Qs). (λ qs. TA_rule f qs (Wrapp (ps_reachable_states 𝒜 f (map ex qs)))) |`| Qs) |`| qss in
      ffilter (λ r. ex (r_rhs r) ≠ {||}) ( |⋃| res))"

lemma ps_rules [code]:
  "ps_rules 𝒜 Q = ps_rules_cont 𝒜 Q"
  using ps_reachable_states_sig finite_ps_rulesp_unfolded[of Q 𝒜]
  unfolding ps_rules_cont_def
  apply (auto simp: fset_of_list_elem ps_rules_def fin_mono ps_rulesp_def
    image_iff set_n_lists split!: prod.splits dest!: in_set_idx)
  by fastforce+

end