theory NF_Impl
imports NF TR.Tree_Automata
begin
fun mergeP_impl where
"mergeP_impl Bot t = True"
| "mergeP_impl t Bot = True"
| "mergeP_impl (BFun f ss) (BFun g ts) =
(if f = g ∧ length ss = length ts then list_all (λ (x, y). mergeP_impl x y) (zip ss ts) else False)"
lemma [simp]: "mergeP_impl s Bot = True" by (cases s) auto
lemma [simp]: "mergeP_impl s t ⟷ (s, t) ∈ mergeP" (is "?LS = ?RS")
proof
show "?LS ⟹ ?RS"
by (induct rule: mergeP_impl.induct, auto split: if_splits intro!: step)
(smt length_zip list_all_length mergeP.step min_less_iff_conj nth_mem nth_zip old.prod.case)
next
show "?RS ⟹ ?LS" by (induct rule: mergeP.induct, auto simp add: list_all_length)
qed
fun bless_eq_impl where
"bless_eq_impl Bot t = True"
| "bless_eq_impl (BFun f ss) (BFun g ts) =
(if f = g ∧ length ss = length ts then list_all (λ (x, y). bless_eq_impl x y) (zip ss ts) else False)"
| "bless_eq_impl _ _ = False"
lemma [simp]: "bless_eq_impl s t ⟷ (s, t) ∈ bless_eq" (is "?RS = ?LS")
proof
show "?LS ⟹ ?RS" by (induct rule: bless_eq.induct, auto simp add: list_all_length)
next
show "?RS ⟹ ?LS"
by (induct rule: bless_eq_impl.induct, auto split: if_splits intro!: step)
(metis (full_types) length_zip list_all_length min_less_iff_conj nth_mem nth_zip old.prod.case)
qed
"psubt_bot_impl R ≡ remdups (map term_to_bot_term (concat (map supt_list R)))"">definition "psubt_bot_impl R ≡ remdups (map term_to_bot_term (concat (map supt_list R)))"
lemma psubt_bot_impl[simp]: "set (psubt_bot_impl R) = psubt_lhs_bot (set R)"
by (induct R, auto simp: psubt_bot_impl_def)
"states_impl R = List.insert Bot (map the (removeAll None">definition "states_impl R = List.insert Bot (map the (removeAll None
(closure_impl (lift_f_total mergeP_impl (↑)) (map Some (psubt_bot_impl R)))))"
lemma states_impl [simp]: "set (states_impl R) = states (set R)"
proof -
have [simp]: "lift_f_total mergeP_impl (↑) = lift_f_total (λ x y. mergeP_impl x y) (↑)" by blast
show ?thesis unfolding states_impl_def states_def
using lift_total.cl.closure_impl
by (simp add: lift_total.cl.pred_closure_lift_closure)
qed
lemma fstates_code[code]:
"fstates (fset_of_list R) = fset_of_list (states_impl R)"
by (auto simp: fmember.rep_eq fstates.rep_eq fset_of_list.rep_eq)
abbreviation check_intance_lhs where
"check_intance_lhs qs f R ≡ list_all (λ u. ¬ bless_eq_impl u (BFun f qs)) R"
definition min_elem where
"min_elem s ss = (let ts = filter (λ x. bless_eq_impl x s) ss in
foldr (↑) ts Bot)"
lemma bound_impl [simp, code]:
"bound_max s (set ss) = min_elem s ss"
proof -
have [simp]: "{y. lift_total.lifted_less_eq y (Some s) ∧ y ∈ Some ` set ss} = Some ` {x ∈ set ss. x ≤⇩b s}"
by auto
then show ?thesis
using lift_total.supremum_impl[of "filter (λ x. bless_eq_impl x s) ss"]
using lift_total.supremum_smaller_exists_unique[of "set ss" s]
by (auto simp: min_elem_def Let_def lift_total.lift_ord.smaller_subset_def)
qed
definition nf_rule_impl where
"nf_rule_impl S R SR h = (let (f, n) = h in
let states = list_of_permutation_n S n in
let nlhs_inst = filter (λ qs. check_intance_lhs qs f R) states in
map (λ qs. TA_rule f qs (min_elem (BFun f qs) SR)) nlhs_inst)"
abbreviation nf_rules_impl where
"nf_rules_impl R ℱ ≡ concat (map (nf_rule_impl (states_impl R) (map term_to_bot_term R) (psubt_bot_impl R)) ℱ)"
lemma nf_rules_in_impl:
assumes "TA_rule f qs q |∈| nf_rules (fset_of_list R) (fset_of_list ℱ)"
shows "TA_rule f qs q |∈| fset_of_list (nf_rules_impl R ℱ)"
proof -
have funas: "(f, length qs) ∈ set ℱ" and st: "fset_of_list qs |⊆| fstates (fset_of_list R)"
and nlhs: "¬(∃ s ∈ (set R). s⇧⊥ ≤⇩b BFun f qs)"
and min: "q = bound_max (BFun f qs) (psubt_lhs_bot (set R))"
using assms by (auto simp add: nf_rules_fmember simp flip: fset_of_list_elem fmember.rep_eq)
then have st_impl: "qs |∈| fset_of_list (list_of_permutation_n (states_impl R) (length qs))"
using list_fun_sym_eq_set
by (auto simp add: fset_of_list_elem list_fun_sym_eq_set_cons_l subset_code(1)
fset_of_list.rep_eq less_eq_fset.rep_eq fstates.rep_eq)
from nlhs have nlhs_impl: "check_intance_lhs qs f (map term_to_bot_term R)"
by (auto simp: list.pred_set)
have min_impl: "q = min_elem (BFun f qs) (psubt_bot_impl R)"
using bound_impl min
by (auto simp flip: psubt_bot_impl)
then show ?thesis using funas nlhs_impl funas st_impl unfolding nf_rule_impl_def
by (auto simp: fset_of_list_elem)
qed
lemma nf_rules_impl_in_rules:
assumes "TA_rule f qs q |∈| fset_of_list (nf_rules_impl R ℱ)"
shows "TA_rule f qs q |∈| nf_rules (fset_of_list R) (fset_of_list ℱ)"
proof -
have funas: "(f, length qs) ∈ set ℱ"
and st_impl: "qs |∈| fset_of_list (list_of_permutation_n (states_impl R) (length qs))"
and nlhs_impl: "check_intance_lhs qs f (map term_to_bot_term R)"
and min: "q = min_elem (BFun f qs) (psubt_bot_impl R)" using assms
by (auto simp add: list_fun_length_n nf_rule_impl_def fset_of_list_elem)
from st_impl have st: "fset_of_list qs |⊆| fstates (fset_of_list R)"
using list_fun_sym_eq_set[of "states_impl R" "length qs"] in_set_idx
by (force simp: fset_of_list_elem fstates.rep_eq fmember.rep_eq fset_of_list.rep_eq)
from nlhs_impl have nlhs: "¬(∃ l ∈ (set R). l⇧⊥ ≤⇩b BFun f qs)"
by auto (metis (no_types, lifting) Ball_set_list_all in_set_idx length_map nth_map nth_mem)
have "q = bound_max (BFun f qs) (psubt_lhs_bot (set R))"
using bound_impl min
by (auto simp flip: psubt_bot_impl)
then show ?thesis using funas st nlhs
by (auto simp add: nf_rules_fmember fset_of_list_elem fset_of_list.rep_eq)
qed
lemma rule_set_eq:
shows "nf_rules (fset_of_list R) (fset_of_list ℱ) = fset_of_list (nf_rules_impl R ℱ)" (is "?Ls = ?Rs")
proof -
{fix r assume "r |∈| ?Ls" then have "r |∈| ?Rs"
using nf_rules_in_impl[where ?R = R and ?ℱ = ℱ]
by (cases r) auto}
moreover
{fix r assume "r |∈| ?Rs" then have "r |∈| ?Ls"
using nf_rules_impl_in_rules[where ?R = R and ?ℱ = ℱ]
by (cases r) auto}
ultimately show ?thesis by blast
qed
lemma nf_ta_code [code]:
"nf_ta (fset_of_list R) (fset_of_list ℱ) = TA (fset_of_list (nf_rules_impl R ℱ)) {||}"
unfolding nf_ta_def
by (intro TA_equalityI) (auto simp add: rule_set_eq)
end