# Theory DRA_Instantiation

```(*
Author:   Benedikt Seidl
*)

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)"
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)"
qed

end

instantiation ltln⇩P:: (hashable) hashable
begin

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

instance
proof
from def_hashmap_size[where ?'a = "'a"]
show "1 < def_hashmap_size TYPE('a ltln⇩P)"
qed

end

instantiation ltln⇩Q :: (hashable) hashable
begin

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

instance
proof
from def_hashmap_size[where ?'a = "'a"]
show "1 < def_hashmap_size TYPE('a ltln⇩Q)"
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_dra⇩P: dra_implementation "(∼⇩P)" id rep_ltln⇩P abs_ltln⇩P
defines ltl_to_dra⇩P = ltl_to_dra⇩P.ltl_to_dra
and ltl_to_dra_restricted⇩P = ltl_to_dra⇩P.ltl_to_dra_restricted
and ltl_to_dra_alphabet⇩P = ltl_to_dra⇩P.ltl_to_dra_alphabet
and 𝔄'⇩P = ltl_to_dra⇩P.𝔄'
and 𝔄⇩1⇩P = ltl_to_dra⇩P.𝔄⇩1
and 𝔄⇩2⇩P = ltl_to_dra⇩P.𝔄⇩2
and 𝔄⇩3⇩P = ltl_to_dra⇩P.𝔄⇩3
and 𝔄⇩ν_FG⇩P = ltl_to_dra⇩P.𝔄⇩ν_FG
and 𝔄⇩μ_GF⇩P = ltl_to_dra⇩P.𝔄⇩μ_GF
and af_letter⇩G⇩P = ltl_to_dra⇩P.af_letter⇩G
and af_letter⇩F⇩P = ltl_to_dra⇩P.af_letter⇩F
and af_letter⇩G_lifted⇩P = ltl_to_dra⇩P.af_letter⇩G_lifted
and af_letter⇩F_lifted⇩P = ltl_to_dra⇩P.af_letter⇩F_lifted
and af_letter⇩ν_lifted⇩P = ltl_to_dra⇩P.af_letter⇩ν_lifted
and ℭ⇩P = ltl_to_dra⇩P.ℭ
and af_letter⇩ν⇩P = ltl_to_dra⇩P.af_letter⇩ν
and ltln_to_draei⇩P = ltl_to_dra⇩P.ltln_to_draei
and ltlc_to_draei⇩P = ltl_to_dra⇩P.ltlc_to_draei
by unfold_locales (meson Quotient_abs_rep Quotient_ltln⇩P, simp_all add: Quotient_abs_rep Quotient_ltln⇩P ltln⇩P.abs_eq_iff prop_equiv_card prop_equiv_finite)

thm ltl_to_dra⇩P.ltl_to_dra_language
thm ltl_to_dra⇩P.ltl_to_dra_size
thm ltl_to_dra⇩P.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_dra⇩Q: dra_implementation "(∼⇩Q)" Unf rep_ltln⇩Q abs_ltln⇩Q
defines ltl_to_dra⇩Q = ltl_to_dra⇩Q.ltl_to_dra
and ltl_to_dra_restricted⇩Q = ltl_to_dra⇩Q.ltl_to_dra_restricted
and ltl_to_dra_alphabet⇩Q = ltl_to_dra⇩Q.ltl_to_dra_alphabet
and 𝔄'⇩Q = ltl_to_dra⇩Q.𝔄'
and 𝔄⇩1⇩Q = ltl_to_dra⇩Q.𝔄⇩1
and 𝔄⇩2⇩Q = ltl_to_dra⇩Q.𝔄⇩2
and 𝔄⇩3⇩Q = ltl_to_dra⇩Q.𝔄⇩3
and 𝔄⇩ν_FG⇩Q = ltl_to_dra⇩Q.𝔄⇩ν_FG
and 𝔄⇩μ_GF⇩Q = ltl_to_dra⇩Q.𝔄⇩μ_GF
and af_letter⇩G⇩Q = ltl_to_dra⇩Q.af_letter⇩G
and af_letter⇩F⇩Q = ltl_to_dra⇩Q.af_letter⇩F
and af_letter⇩G_lifted⇩Q = ltl_to_dra⇩Q.af_letter⇩G_lifted
and af_letter⇩F_lifted⇩Q = ltl_to_dra⇩Q.af_letter⇩F_lifted
and af_letter⇩ν_lifted⇩Q = ltl_to_dra⇩Q.af_letter⇩ν_lifted
and ℭ⇩Q = ltl_to_dra⇩Q.ℭ
and af_letter⇩ν⇩Q = ltl_to_dra⇩Q.af_letter⇩ν
and ltln_to_draei⇩Q = ltl_to_dra⇩Q.ltln_to_draei
and ltlc_to_draei⇩Q = ltl_to_dra⇩Q.ltlc_to_draei
by unfold_locales (meson Quotient_abs_rep Quotient_ltln⇩Q, simp_all add: Quotient_abs_rep Quotient_ltln⇩Q ltln⇩Q.abs_eq_iff nested_prop_atoms_Unf prop_unfold_equiv_finite prop_unfold_equiv_card)

thm ltl_to_dra⇩Q.ltl_to_dra_language
thm ltl_to_dra⇩Q.ltl_to_dra_size
thm ltl_to_dra⇩Q.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_draei⇩P"
| "ltlc_to_draei PropUnfold = ltlc_to_draei⇩Q"

end
```