Theory DRA_Instantiation

(*
    Author:   Benedikt Seidl
    License:  BSD
*)

section ‹Instantiation of the LTL to DRA construction›

theory DRA_Instantiation
imports
  DRA_Implementation
  LTL.Equivalence_Relations
  LTL.Disjunctive_Normal_Form
  "../Logical_Characterization/Extra_Equivalence_Relations"
  "HOL-Library.Log_Nat"
  Deriving.Derive
begin

subsection ‹Hash Functions for Quotient Types›

derive hashable ltln

definition "cube a = a * a * a"


instantiation set :: (hashable) hashable
begin

definition [simp]: "hashcode (x :: 'a set) = Finite_Set.fold (plus o cube o hashcode) (uint32_of_nat (card x)) x"
definition "def_hashmap_size = (λ_ :: 'a set itself. 2 * def_hashmap_size TYPE('a))"

instance
proof
  from def_hashmap_size[where ?'a = "'a"]
  show "1 < def_hashmap_size TYPE('a set)"
    by (simp add: def_hashmap_size_set_def)
qed

end


instantiation fset :: (hashable) hashable
begin

definition [simp]: "hashcode (x :: 'a fset) = hashcode (fset x)"
definition "def_hashmap_size = (λ_ :: 'a fset itself. 2 * def_hashmap_size TYPE('a))"

instance
proof
  from def_hashmap_size[where ?'a = "'a"]
  show "1 < def_hashmap_size TYPE('a fset)"
    by (simp add: def_hashmap_size_fset_def)
qed

end


instantiation ltlnP:: (hashable) hashable
begin

definition [simp]: "hashcode (φ :: 'a ltlnP) = hashcode (min_dnf (rep_ltlnP φ))"
definition "def_hashmap_size = (λ_ :: 'a ltlnP itself. def_hashmap_size TYPE('a ltln))"

instance
proof
  from def_hashmap_size[where ?'a = "'a"]
  show "1 < def_hashmap_size TYPE('a ltlnP)"
    by (simp add: def_hashmap_size_ltlnP_def def_hashmap_size_ltln_def)
qed

end


instantiation ltlnQ :: (hashable) hashable
begin

definition [simp]: "hashcode (φ :: 'a ltlnQ) = hashcode (min_dnf (Unf (rep_ltlnQ φ)))"
definition "def_hashmap_size = (λ_ :: 'a ltlnQ itself. def_hashmap_size TYPE('a ltln))"

instance
proof
  from def_hashmap_size[where ?'a = "'a"]
  show "1 < def_hashmap_size TYPE('a ltlnQ)"
    by (simp add: def_hashmap_size_ltlnQ_def def_hashmap_size_ltln_def)
qed

end


subsection ‹Interpretations with Equivalence Relations›

text ‹
  We instantiate the construction locale with propositional equivalence
  and obtain a function converting a formula into an abstract automaton.
›

global_interpretation ltl_to_draP: dra_implementation "(∼P)" id rep_ltlnP abs_ltlnP
  defines ltl_to_draP = ltl_to_draP.ltl_to_dra
    and ltl_to_dra_restrictedP = ltl_to_draP.ltl_to_dra_restricted
    and ltl_to_dra_alphabetP = ltl_to_draP.ltl_to_dra_alphabet
    and 𝔄'P = ltl_to_draP.𝔄'
    and 𝔄1P = ltl_to_draP.𝔄1
    and 𝔄2P = ltl_to_draP.𝔄2
    and 𝔄3P = ltl_to_draP.𝔄3
    and 𝔄ν_FGP = ltl_to_draP.𝔄ν_FG
    and 𝔄μ_GFP = ltl_to_draP.𝔄μ_GF
    and af_letterGP = ltl_to_draP.af_letterG
    and af_letterFP = ltl_to_draP.af_letterF
    and af_letterG_liftedP = ltl_to_draP.af_letterG_lifted
    and af_letterF_liftedP = ltl_to_draP.af_letterF_lifted
    and af_letterν_liftedP = ltl_to_draP.af_letterν_lifted
    and ℭP = ltl_to_draP.ℭ
    and af_letterνP = ltl_to_draP.af_letterν
    and ltln_to_draeiP = ltl_to_draP.ltln_to_draei
    and ltlc_to_draeiP = ltl_to_draP.ltlc_to_draei
  by unfold_locales (meson Quotient_abs_rep Quotient_ltlnP, simp_all add: Quotient_abs_rep Quotient_ltlnP ltlnP.abs_eq_iff prop_equiv_card prop_equiv_finite)

thm ltl_to_draP.ltl_to_dra_language
thm ltl_to_draP.ltl_to_dra_size
thm ltl_to_draP.final_correctness

text ‹
  Similarly, we instantiate the locale with a different equivalence relation and obtain another
  constant for translation of LTL to deterministic Rabin automata.
›

global_interpretation ltl_to_draQ: dra_implementation "(∼Q)" Unf rep_ltlnQ abs_ltlnQ
  defines ltl_to_draQ = ltl_to_draQ.ltl_to_dra
    and ltl_to_dra_restrictedQ = ltl_to_draQ.ltl_to_dra_restricted
    and ltl_to_dra_alphabetQ = ltl_to_draQ.ltl_to_dra_alphabet
    and 𝔄'Q = ltl_to_draQ.𝔄'
    and 𝔄1Q = ltl_to_draQ.𝔄1
    and 𝔄2Q = ltl_to_draQ.𝔄2
    and 𝔄3Q = ltl_to_draQ.𝔄3
    and 𝔄ν_FGQ = ltl_to_draQ.𝔄ν_FG
    and 𝔄μ_GFQ = ltl_to_draQ.𝔄μ_GF
    and af_letterGQ = ltl_to_draQ.af_letterG
    and af_letterFQ = ltl_to_draQ.af_letterF
    and af_letterG_liftedQ = ltl_to_draQ.af_letterG_lifted
    and af_letterF_liftedQ = ltl_to_draQ.af_letterF_lifted
    and af_letterν_liftedQ = ltl_to_draQ.af_letterν_lifted
    and ℭQ = ltl_to_draQ.ℭ
    and af_letterνQ = ltl_to_draQ.af_letterν
    and ltln_to_draeiQ = ltl_to_draQ.ltln_to_draei
    and ltlc_to_draeiQ = ltl_to_draQ.ltlc_to_draei
  by unfold_locales (meson Quotient_abs_rep Quotient_ltlnQ, simp_all add: Quotient_abs_rep Quotient_ltlnQ ltlnQ.abs_eq_iff nested_prop_atoms_Unf prop_unfold_equiv_finite prop_unfold_equiv_card)

thm ltl_to_draQ.ltl_to_dra_language
thm ltl_to_draQ.ltl_to_dra_size
thm ltl_to_draQ.final_correctness


text ‹
  We allow the user to choose one of the two equivalence relations.
›

datatype equiv = Prop | PropUnfold

fun ltlc_to_draei :: "equiv ⇒ ('a :: hashable) ltlc ⇒ ('a set, nat) draei"
where
  "ltlc_to_draei Prop = ltlc_to_draeiP"
| "ltlc_to_draei PropUnfold = ltlc_to_draeiQ"

end