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 ⟷ (∀x∈set 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_Q⇩f_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
end