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