Theory Regular_Tree_Relations.Tree_Automata_Impl

theory Tree_Automata_Impl
  imports Tree_Automata_Abstract_Impl
   "HOL-Library.List_Lexorder"
   "HOL-Library.AList_Mapping"
   Tree_Automata_Class_Instances_Impl
   Containers.Containers
begin

definition map_val_of_list :: "('b  'a)  ('b  'c list)  'b list  ('a, 'c list) mapping" where
  "map_val_of_list ek ev xs = foldr (λx m. Mapping.update (ek x) (ev x @ case_option Nil id (Mapping.lookup m (ek x))) m) xs Mapping.empty"

abbreviation "map_of_list ek ev xs  map_val_of_list ek (λ x. [ev x]) xs"

lemma map_val_of_list_tabulate_conv:
  "map_val_of_list ek ev xs = Mapping.tabulate (sort (remdups (map ek xs))) (λ k. concat (map ev (filter (λ x. k = ek x) xs)))"
  unfolding map_val_of_list_def
proof (induct xs)
  case (Cons x xs) then show ?case
    by (intro mapping_eqI) (auto simp: lookup_combine lookup_update' lookup_empty lookup_tabulate image_iff)
qed (simp add: empty_Mapping tabulate_Mapping)

lemmas map_val_of_list_simp = map_val_of_list_tabulate_conv lookup_tabulate
subsection ‹Setup for the list implementation of reachable states›

definition reach_infer0_cont where
  "reach_infer0_cont Δ =
     map r_rhs (filter (λ r. case r of TA_rule f ps p  ps = []) (sorted_list_of_fset Δ))"

definition reach_infer1_cont :: "('q :: linorder, 'f :: linorder) ta_rule fset  ('q × 'q) fset  'q  'q fset  'q list" where
  "reach_infer1_cont Δ Δε =
    (let rules = sorted_list_of_fset Δ in
     let eps   = sorted_list_of_fset Δε in
     let mapp_r = map_val_of_list fst snd (concat (map (λ r. map (λ q. (q, [r])) (r_lhs_states r)) rules)) in
     let mapp_e = map_of_list fst snd eps in
    (λ p bs.
    (map r_rhs (filter (λ r. case r of TA_rule f qs q 
      fset_of_list qs |⊆| finsert p bs) (case_option Nil id (Mapping.lookup mapp_r p)))) @
      case_option Nil id (Mapping.lookup mapp_e p)))"

locale reach_rules_fset =
  fixes Δ :: "('q :: linorder, 'f :: linorder) ta_rule fset" and Δε :: "('q × 'q) fset"
begin

sublocale reach_horn "TA Δ Δε" .

lemma infer1:
  "infer1 p (fset bs) = set (reach_infer1_cont Δ Δε p bs)"
  unfolding reach_infer1 reach_infer1_cont_def set_append Un_assoc[symmetric] Let_def
  unfolding sorted_list_of_fset_simps union_fset
  apply (intro arg_cong2[of _ _ _ _ "(∪)"])
  subgoal
    apply (auto simp: fset_of_list_elem less_eq_fset.rep_eq fset_of_list.rep_eq image_iff
      map_val_of_list_simp split!: ta_rule.splits)
    apply (metis list.set_intros(1) ta_rule.sel(2, 3))
    apply (metis in_set_simps(2) ta_rule.exhaust_sel)
    done
  subgoal
    apply (simp add: image_def Bex_def map_val_of_list_simp)
    done
  done

sublocale l: horn_fset "reach_rules (TA Δ Δε)" "reach_infer0_cont Δ" "reach_infer1_cont Δ Δε"
  apply (unfold_locales)
  unfolding reach_infer0 reach_infer0_cont_def
  subgoal
    apply (auto simp: image_iff ta_rule.case_eq_if Bex_def fset_of_list_elem)
    apply force
    apply (metis ta_rule.collapse)+
    done
  subgoal using infer1
    apply blast
    done
  done

lemmas infer = l.infer0 l.infer1
lemmas saturate_impl_sound = l.saturate_impl_sound
lemmas saturate_impl_complete = l.saturate_impl_complete

end

definition "reach_cont_impl Δ Δε =
   horn_fset_impl.saturate_impl (reach_infer0_cont Δ) (reach_infer1_cont Δ Δε)"

lemma reach_fset_impl_sound:
  "reach_cont_impl Δ Δε = Some xs  fset xs = ta_reach (TA Δ Δε)"
  using reach_rules_fset.saturate_impl_sound unfolding reach_cont_impl_def
  unfolding reach_horn.reach_sound .

lemma reach_fset_impl_complete:
  "reach_cont_impl Δ Δε  None"
proof -
  have "finite (ta_reach (TA Δ Δε))"
    unfolding ta_reach_reachable by simp
  then show ?thesis unfolding reach_cont_impl_def
    by (intro reach_rules_fset.saturate_impl_complete)
      (auto simp: reach_horn.reach_sound)
qed

lemma reach_impl [code]:
  "ta_reachable (TA Δ Δε) = the (reach_cont_impl Δ Δε)"
  using reach_fset_impl_sound[of Δ Δε]
  by (auto simp add: ta_reach_reachable reach_fset_impl_complete fset_of_list_elem)

subsection ‹Setup for list implementation of productive states›
definition productive_infer1_cont :: "('q :: linorder, 'f :: linorder) ta_rule fset  ('q × 'q) fset  'q  'q fset  'q list" where
  "productive_infer1_cont Δ Δε =
    (let rules = sorted_list_of_fset Δ in
     let eps   = sorted_list_of_fset Δε in
     let mapp_r = map_of_list (λ r. r_rhs r) r_lhs_states rules in
     let mapp_e = map_of_list snd fst eps in
    (λ p bs.
     (case_option Nil id (Mapping.lookup mapp_e p)) @
     concat (case_option Nil id (Mapping.lookup mapp_r p))))"

locale productive_rules_fset =
  fixes Δ :: "('q :: linorder, 'f :: linorder) ta_rule fset" and Δε :: "('q × 'q) fset" and P :: "'q fset"
begin

sublocale productive_horn "TA Δ Δε" P .

lemma infer1:
  "infer1 p (fset bs) = set (productive_infer1_cont Δ Δε p bs)"
  unfolding productive_infer1 productive_infer1_cont_def set_append Un_assoc[symmetric]
  unfolding union_fset sorted_list_of_fset_simps Let_def set_append
  apply (intro arg_cong2[of _ _ _ _ "(∪)"])
  subgoal
    by (simp add: image_def Bex_def map_val_of_list_simp)
  subgoal
    apply (auto simp: map_val_of_list_simp image_iff)
    apply (metis ta_rule.sel(2, 3))
    apply (metis ta_rule.collapse)
    done
  done

sublocale l: horn_fset "productive_rules P (TA Δ Δε)" "sorted_list_of_fset P" "productive_infer1_cont Δ Δε"
  apply (unfold_locales)
  using infer1 productive_infer0 fset_of_list.rep_eq
  by fastforce+

lemmas infer = l.infer0 l.infer1
lemmas saturate_impl_sound = l.saturate_impl_sound
lemmas saturate_impl_complete = l.saturate_impl_complete

end

definition "productive_cont_impl P Δ Δε =
   horn_fset_impl.saturate_impl (sorted_list_of_fset P) (productive_infer1_cont Δ Δε)"

lemma productive_cont_impl_sound:
  "productive_cont_impl P Δ Δε = Some xs  fset xs = ta_productive_ind P (TA Δ Δε)"
  using productive_rules_fset.saturate_impl_sound unfolding productive_cont_impl_def
  unfolding productive_horn.productive_sound .

lemma productive_cont_impl_complete:
  "productive_cont_impl P Δ Δε  None"
proof -
  have "finite (ta_productive_ind  P (TA Δ Δε))"
    unfolding ta_productive_ind by simp
  then show ?thesis unfolding productive_cont_impl_def
    by (intro productive_rules_fset.saturate_impl_complete)
      (auto simp: productive_horn.productive_sound)
qed

lemma productive_impl [code]:
  "ta_productive P (TA Δ Δε) = the (productive_cont_impl P Δ Δε)"
  using productive_cont_impl_complete[of P Δ] productive_cont_impl_sound[of P Δ]
  by (auto simp add: ta_productive_ind fset_of_list_elem)

subsection ‹Setup for the implementation of power set construction states›


abbreviation "r_statesl r  length (r_lhs_states r)"

definition ps_reachable_states_list where
  "ps_reachable_states_list mapp_r mapp_e f ps =
   (let R = filter (λ r. list_all2 (|∈|) (r_lhs_states r) ps)
      (case_option Nil id (Mapping.lookup mapp_r (f, length ps))) in
    let S = map r_rhs R in
    S @ concat (map (case_option Nil id  Mapping.lookup mapp_e) S))"

lemma ps_reachable_states_list_sound:
  assumes "length ps = n"
  and mapp_r: "case_option Nil id (Mapping.lookup mapp_r (f, n)) =
     filter (λr. r_root r = f  r_statesl r = n) (sorted_list_of_fset Δ)"
  and mapp_e: "p. case_option Nil id (Mapping.lookup mapp_e p) =
     map snd (filter (λ q. fst q = p) (sorted_list_of_fset (Δε|+|)))"
  shows "fset_of_list (ps_reachable_states_list mapp_r mapp_e f (map ex ps)) =
   ps_reachable_states (TA Δ Δε) f (map ex ps)" (is "?Ls = ?Rs")
proof -
  have *: "length ps = n" "length (map ex ps) = n" using assms by auto
  {fix q assume "q |∈| ?Ls"
    then obtain qs p where "TA_rule f qs p |∈| Δ" "length ps = length qs"
       "list_all2 (|∈|) qs (map ex ps)" "p = q  (p, q) |∈| Δε|+|"
      unfolding ps_reachable_states_list_def Let_def comp_def assms(1, 2, 3) *
      by (force simp add: fset_of_list_elem image_iff fBex_def) 
    then have "q |∈| ?Rs"
      by (force simp add: ps_reachable_states_fmember image_iff)}
  moreover
    {fix q assume "q |∈| ?Rs"
       then obtain qs p where "TA_rule f qs p |∈| Δ" "length ps = length qs"
         "list_all2 (|∈|) qs (map ex ps)" "p = q  (p, q) |∈| Δε|+|"
         by (auto simp add: ps_reachable_states_fmember list_all2_iff)
       then have "q |∈| ?Ls"
         unfolding ps_reachable_states_list_def Let_def * comp_def assms(2, 3)
         by (force simp add: fset_of_list_elem image_iff)}
  ultimately show ?thesis by blast
qed


lemma rule_target_statesI:
  " r |∈| Δ. r_rhs r = q  q |∈| rule_target_states Δ"
  by auto

definition ps_states_infer0_cont :: "('q :: linorder, 'f :: linorder) ta_rule fset 
   ('q × 'q) fset  'q FSet_Lex_Wrapper list" where
   "ps_states_infer0_cont Δ Δε =
     (let sig = filter (λ r. r_lhs_states r = []) (sorted_list_of_fset Δ) in
        filter (λ p. ex p  {||}) (map (λ r. Wrapp (ps_reachable_states (TA Δ Δε) (r_root r) [])) sig))"

definition ps_states_infer1_cont :: "('q :: linorder , 'f :: linorder) ta_rule fset  ('q × 'q) fset 
   'q FSet_Lex_Wrapper  'q FSet_Lex_Wrapper fset  'q FSet_Lex_Wrapper list" where
  "ps_states_infer1_cont Δ Δε =
    (let sig = remdups (map (λ r. (r_root r, r_statesl r)) (filter (λ r. r_lhs_states r  []) (sorted_list_of_fset Δ))) in
     let arities = remdups (map snd sig) in
     let etr   = sorted_list_of_fset (Δε|+|) in
     let mapp_r = map_of_list (λ r. (r_root r, r_statesl r)) id (sorted_list_of_fset Δ) in
     let mapp_e = map_of_list fst snd etr in
    (λ p bs.
      (let states = sorted_list_of_fset (finsert p bs) in
       let arity_to_states_map = Mapping.tabulate arities (λ n. list_of_permutation_element_n p n states) in
       let res = map (λ (f, n).
         map (λ s. let rules = the (Mapping.lookup mapp_r (f, n)) in
            Wrapp (fset_of_list (ps_reachable_states_list mapp_r mapp_e f (map ex s))))
           (the (Mapping.lookup arity_to_states_map n)))
          sig in
      filter (λ p. ex p  {||}) (concat res))))"

locale ps_states_fset =
  fixes Δ :: "('q :: linorder, 'f :: linorder) ta_rule fset" and Δε :: "('q × 'q) fset"
begin

sublocale ps_states_horn "TA Δ Δε" .

lemma infer0: "infer0 = set (ps_states_infer0_cont Δ Δε)"
  unfolding ps_states_horn.ps_construction_infer0
  unfolding ps_states_infer0_cont_def Let_def
  using ps_reachable_states_fmember
  by (auto simp add: image_def Ball_def Bex_def)
     (metis list_all2_Nil2 ps_reachable_states_fmember ta.sel(1) ta_rule.sel(1, 2))

lemma r_lhs_states_nConst:
  "r_lhs_states r  []  r_statesl r  0" for r by auto


lemma filter_empty_conv':
  "[] = filter P xs  (xset xs. ¬ P x)"
  by (metis filter_empty_conv)

lemma infer1:
  "infer1 p (fset bs) = set (ps_states_infer1_cont Δ Δε p bs)" (is "?Ls = ?Rs")
proof -
  let ?mapp_r = "map_of_list (λr. (r_root r, r_statesl r)) (λx. x) (sorted_list_of_fset Δ)"
  let ?mapp_e = "map_of_list fst snd (sorted_list_of_fset (Δε|+|))"
  have mapr: "case_option Nil id (Mapping.lookup ?mapp_r (f, n)) =
     filter (λr. r_root r = f  r_statesl r = n) (sorted_list_of_fset Δ)" for f n
    by (auto simp: map_val_of_list_simp image_iff filter_empty_conv' intro: filter_cong)
  have epsr: "p. case_option Nil id (Mapping.lookup ?mapp_e p) =
     map snd (filter (λ q. fst q = p) (sorted_list_of_fset (Δε|+|)))"
    by (auto simp: map_val_of_list_simp image_iff filter_empty_conv) metis
  have *: "p  set qs  x |∈| ps_reachable_states (TA Δ Δε) f (map ex qs) 
    ( ps q. TA_rule f ps q |∈| Δ  length ps = length qs)" for x f qs
    by (auto simp: ps_reachable_states_fmember list_all2_conv_all_nth)
  {fix q assume "q  ?Ls"
    then obtain f qss where sp: "q = Wrapp (ps_reachable_states (TA Δ Δε) f (map ex qss))"
      "ps_reachable_states (TA Δ Δε) f (map ex qss)  {||}" "p  set qss" "set qss  insert p (fset bs)"
      by (auto simp add: ps_construction_infer1 ps_reachable_states_fmember)
    from sp(2, 3) obtain ps p' where r: "TA_rule f ps p' |∈| Δ" "length ps = length qss" using *
      by blast
    then have mem: "qss  set (list_of_permutation_element_n p (length ps) (sorted_list_of_fset (finsert p bs)))" using sp(2-)
      by (auto simp: list_of_permutation_element_n_iff)
         (meson in_set_idx insertE set_list_subset_eq_nth_conv)
    then have "q  ?Rs" using sp r
      unfolding ps_construction_infer1 ps_states_infer1_cont_def Let_def
      apply (simp add: lookup_tabulate ps_reachable_states_fmember image_iff)
      apply (rule_tac x = "f ps  p'" in exI)
      apply (auto simp: Bex_def ps_reachable_states_list_sound[OF _ mapr epsr] intro: exI[of _ qss])
      done}
  moreover
  {fix q assume ass: "q  ?Rs"
    then obtain r qss where "r |∈| Δ" "r_lhs_states r  []" "qss  set (list_of_permutation_element_n p (r_statesl r) (sorted_list_of_fset (finsert p bs)))"
      "q = Wrapp (ps_reachable_states (TA Δ Δε) (r_root r) (map ex qss))"
      unfolding ps_states_infer1_cont_def Let_def
      by (auto simp add: lookup_tabulate ps_reachable_states_fmember image_iff
         ps_reachable_states_list_sound[OF _ mapr epsr] split: if_splits)
    moreover have "q  Wrapp {||}" using ass
      by (auto simp: ps_states_infer1_cont_def Let_def)
    ultimately have "q  ?Ls" unfolding ps_construction_infer1
      apply (auto simp: list_of_permutation_element_n_iff intro!: exI[of _ "r_root r"] exI[of _ qss])
      apply (metis in_set_idx)
      done}
  ultimately show ?thesis by blast
qed


sublocale l: horn_fset "ps_states_rules (TA Δ Δε)" "ps_states_infer0_cont Δ Δε" "ps_states_infer1_cont Δ Δε"
  apply (unfold_locales)
  using infer0 infer1
  by fastforce+

lemmas infer = l.infer0 l.infer1
lemmas saturate_impl_sound = l.saturate_impl_sound
lemmas saturate_impl_complete = l.saturate_impl_complete


end

definition "ps_states_fset_impl Δ Δε =
   horn_fset_impl.saturate_impl (ps_states_infer0_cont Δ Δε) (ps_states_infer1_cont Δ Δε)"

lemma ps_states_fset_impl_sound:
  assumes "ps_states_fset_impl Δ Δε = Some xs"
  shows "xs = ps_states (TA Δ Δε)"
  using ps_states_fset.saturate_impl_sound[OF assms[unfolded ps_states_fset_impl_def]]
  using ps_states_horn.ps_states_sound[of "TA Δ Δε"]
  by (auto simp: fset_of_list_elem ps_states.rep_eq fset_of_list.rep_eq)

lemma ps_states_fset_impl_complete:
  "ps_states_fset_impl Δ Δε  None"
proof -
  let ?R = "ps_states (TA Δ Δε)"
  let ?S = "horn.saturate (ps_states_rules (TA Δ Δε))"
  have "?S  fset ?R"
    using ps_states_horn.ps_states_sound
    by (simp add: ps_states_horn.ps_states_sound ps_states.rep_eq)
  from finite_subset[OF this] show ?thesis
  unfolding ps_states_fset_impl_def
  by (intro ps_states_fset.saturate_impl_complete) simp
qed

lemma ps_ta_impl [code]:
  "ps_ta (TA Δ Δε) =
    (let xs = the (ps_states_fset_impl Δ Δε) in
      TA (ps_rules (TA Δ Δε) xs) {||})"
  using ps_states_fset_impl_complete
  using ps_states_fset_impl_sound
  unfolding ps_ta_def Let_def
  by (metis option.exhaust_sel)

lemma ps_reg_impl [code]:
  "ps_reg (Reg Q (TA Δ Δε)) =
    (let xs = the (ps_states_fset_impl Δ Δε) in
     Reg (ffilter (λ S. Q |∩| ex S  {||}) xs)
         (TA (ps_rules (TA Δ Δε) xs) {||}))"
  using ps_states_fset_impl_complete[of Δ Δε]
  using ps_states_fset_impl_sound[of Δ Δε]
  unfolding ps_reg_def ps_ta_Qf_def Let_def
  unfolding ps_ta_def Let_def
  using eq_ffilter by auto

lemma prod_ta_zip [code]:
  "prod_ta_rules (𝒜 :: ('q1 :: linorder, 'f :: linorder) ta) ( :: ('q2 :: linorder, 'f :: linorder) ta) =
   (let sig = sorted_list_of_fset (ta_sig 𝒜 |∩| ta_sig ) in
    let mapA = map_of_list (λr. (r_root r, r_statesl r)) id (sorted_list_of_fset (rules 𝒜)) in
    let mapB = map_of_list (λr. (r_root r, r_statesl r)) id (sorted_list_of_fset (rules )) in
    let merge = (λ (ra, rb). TA_rule (r_root ra) (zip (r_lhs_states ra) (r_lhs_states rb)) (r_rhs ra, r_rhs rb)) in
      fset_of_list (
      concat (map (λ (f, n). map merge
        (List.product (the (Mapping.lookup mapA (f, n))) (the (Mapping.lookup mapB (f, n))))) sig)))"
 (is "?Ls = ?Rs")
proof -
  have [simp]: "distinct (sorted_list_of_fset (ta_sig 𝒜))"  "distinct (sorted_list_of_fset (ta_sig ))"
    by (simp_all add: distinct_sorted_list_of_fset)
  have *: "sort (remdups (map (λr. (r_root r, r_statesl r)) (sorted_list_of_fset (rules 𝒜)))) = sorted_list_of_fset (ta_sig 𝒜)"
   "sort (remdups (map (λr. (r_root r, r_statesl r)) (sorted_list_of_fset (rules )))) = sorted_list_of_fset (ta_sig )"
     by (auto simp: ta_sig_def sorted_list_of_fset_fimage_dist)
  {fix r assume ass: "r |∈| ?Ls"
    then obtain f qs q where [simp]: "r = f qs  q" by auto
    then have "(f, length qs) |∈| ta_sig 𝒜 |∩| ta_sig " using ass by auto
    then have "r |∈| ?Rs" using ass unfolding map_val_of_list_tabulate_conv *
      by (auto simp: Let_def fset_of_list_elem image_iff case_prod_beta lookup_tabulate intro!: bexI[of _ "(f, length qs)"])
         (metis (no_types, lifting) length_map ta_rule.sel(1 - 3) zip_map_fst_snd)}
    moreover
    {fix r assume ass: "r |∈| ?Rs" then have "r |∈| ?Ls" unfolding map_val_of_list_tabulate_conv *
        by (auto simp: fset_of_list_elem finite_Collect_prod_ta_rules lookup_tabulate)
           (metis ta_rule.collapse)}
  ultimately show ?thesis by blast
qed

(*
export_code ta_der in Haskell
export_code ta_reachable in Haskell
export_code ta_productive in Haskell
export_code trim_ta in Haskell
export_code ta_restrict in Haskell
export_code ps_reachable_states in Haskell
export_code prod_ta_rules in Haskell
export_code ps_ta in Haskell
export_code ps_reg in Haskell
export_code reg_intersect in Haskell
*)

end