Theory Code_Export
section ‹Code export to Standard ML›
theory Code_Export
imports
"LTL_to_DRA/DRA_Instantiation"
LTL.Code_Equations
"HOL-Library.Code_Target_Numeral"
begin
subsection ‹Hashing Sets›
global_interpretation comp_fun_commute "plus o cube o hashcode :: ('a :: hashable) ⇒ hashcode ⇒ hashcode"
by unfold_locales (auto simp: cube_def)
lemma [code]:
"hashcode (set xs) = fold (plus o cube o hashcode) (remdups xs) (uint32_of_nat (length (remdups xs)))"
by (simp add: fold_set_fold_remdups length_remdups_card_conv)
lemma [code]:
"hashcode (abs_ltln⇩P φ) = hashcode (min_dnf φ)"
by simp
lemma min_dnf_rep_abs[simp]:
"min_dnf (Unf (rep_ltln⇩Q (abs_ltln⇩Q φ))) = min_dnf (Unf φ)"
using Quotient3_ltln⇩Q ltl_prop_equiv_min_dnf ltl_prop_unfold_equiv_def rep_abs_rsp by fastforce
lemma [code]:
"hashcode (abs_ltln⇩Q φ) = hashcode (min_dnf (Unf φ))"
by simp
subsection ‹LTL to DRA›
declare ltl_to_dra⇩P.af_letter⇩F_lifted_semantics [code]
declare ltl_to_dra⇩P.af_letter⇩G_lifted_semantics [code]
declare ltl_to_dra⇩P.af_letter⇩ν_lifted_semantics [code]
declare ltl_to_dra⇩Q.af_letter⇩F_lifted_semantics [code]
declare ltl_to_dra⇩Q.af_letter⇩G_lifted_semantics [code]
declare ltl_to_dra⇩Q.af_letter⇩ν_lifted_semantics [code]
definition atoms_ltlc_list_literals :: "String.literal ltlc ⇒ String.literal list"
where
"atoms_ltlc_list_literals = atoms_ltlc_list"
definition ltlc_to_draei_literals :: "equiv ⇒ String.literal ltlc ⇒ (String.literal set, nat) draei"
where
"ltlc_to_draei_literals = ltlc_to_draei"
definition sort_transitions :: "(nat × String.literal set × nat) list ⇒ (nat × String.literal set × nat) list"
where
"sort_transitions = sort_key fst"
export_code True_ltlc Iff_ltlc ltlc_to_draei_literals Prop PropUnfold
alphabetei initialei transitionei conditionei
integer_of_nat atoms_ltlc_list_literals sort_transitions set
in SML module_name LTL file_prefix LTL_to_DRA
subsection ‹LTL to NBA›
subsection ‹LTL to LDBA›
end