Theory Code_Export

    Author:   Benedikt Seidl
    License:  BSD

section ‹Code export to Standard ML›

theory Code_Export

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_ltlnP φ) = hashcode (min_dnf φ)"
  by simp

lemma min_dnf_rep_abs[simp]:
  "min_dnf (Unf (rep_ltlnQ (abs_ltlnQ φ))) = min_dnf (Unf φ)"
  using Quotient3_ltlnQ ltl_prop_equiv_min_dnf ltl_prop_unfold_equiv_def rep_abs_rsp by fastforce

lemma [code]:
  "hashcode (abs_ltlnQ φ) = hashcode (min_dnf (Unf φ))"
  by simp

subsection ‹LTL to DRA›

declare ltl_to_draP.af_letterF_lifted_semantics [code]
declare ltl_to_draP.af_letterG_lifted_semantics [code]
declare ltl_to_draP.af_letterν_lifted_semantics [code]

declare ltl_to_draQ.af_letterF_lifted_semantics [code]
declare ltl_to_draQ.af_letterG_lifted_semantics [code]
declare ltl_to_draQ.af_letterν_lifted_semantics [code]

definition atoms_ltlc_list_literals :: "String.literal ltlc  String.literal list"
  "atoms_ltlc_list_literals = atoms_ltlc_list"

definition ltlc_to_draei_literals :: "equiv  String.literal ltlc  (String.literal set, nat) draei"
  "ltlc_to_draei_literals = ltlc_to_draei"

definition sort_transitions :: "(nat × String.literal set × nat) list  (nat × String.literal set × nat) list"
  "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›

(* TODO *)

subsection ‹LTL to LDBA›

(* TODO *)