Theory DRA_Implementation

(*
    Author:   Benedikt Seidl
    License:  BSD
*)

section ‹Implementation of the DRA Construction›

theory DRA_Implementation
imports
  DRA_Construction
  LTL.Rewriting
  Transition_Systems_and_Automata.DRA_Translate
begin

subsection ‹Generating the Explicit Automaton›

text ‹
  We convert the implicit automaton to its explicit representation
  and afterwards proof the final correctness theorem and the overall
  size bound.
›

definition dra_to_drai :: "('a, 'b) dra ⇒ 'a list ⇒ ('a, 'b) drai"
where
  "dra_to_drai 𝔄 Σ = drai Σ (initial 𝔄) (transition 𝔄) (condition 𝔄)"

lemma dra_to_drai_language:
  "set Σ = alphabet 𝔄 ⟹ language (drai_dra (dra_to_drai 𝔄 Σ)) = language 𝔄"
  by (simp add: dra_to_drai_def drai_dra_def)

definition drai_to_draei :: "nat ⇒ ('a, 'b :: hashable) drai ⇒ ('a, nat) draei"
where
  "drai_to_draei hms = to_draei_impl (=) bounded_hashcode_nat hms"


lemma dra_to_drai_rel:
  assumes
    "(Σ, alphabet A) ∈ ⟨Id⟩ list_set_rel"
  shows
    "(dra_to_drai A Σ, A) ∈ ⟨Id, Id⟩drai_dra_rel"
proof -
  have "(A, A) ∈ ⟨Id, Id⟩dra_rel"
    by simp

  then have "(dra_to_drai A Σ, dra (alphabet A) (initial A) (transition A) (condition A)) ∈ ⟨Id, Id⟩drai_dra_rel"
    unfolding dra_to_drai_def using assms by parametricity

  then show ?thesis
    by simp
qed

lemma draei_language_rel:
  fixes
    A :: "('label, 'state :: hashable) dra"
  assumes
    "(Σ, alphabet A) ∈ ⟨Id⟩ list_set_rel"
  and
    "finite (DRA.nodes A)"
  and
    "is_valid_def_hm_size TYPE('state) hms"
  shows
    "DRA.language (drae_dra (draei_drae (drai_to_draei hms (dra_to_drai A Σ)))) = DRA.language A"
proof -
  have "(dra_to_drai A Σ, A) ∈ ⟨Id, Id⟩drai_dra_rel"
    using dra_to_drai_rel assms by fast

  then have "(drai_to_draei hms (dra_to_drai A Σ), to_draei A) ∈ ⟨Id_on (dra.alphabet A), rel (dra_to_drai A Σ) A (=) bounded_hashcode_nat hms⟩ draei_dra_rel"
    unfolding drai_to_draei_def
    using to_draei_impl_refine[unfolded autoref_tag_defs]
    by parametricity (simp_all add: assms is_bounded_hashcode_def bounded_hashcode_nat_bounds)

  then have "(DRA.language ((drae_dra ∘ draei_drae) (drai_to_draei hms (dra_to_drai A Σ))), DRA.language (id (to_draei A))) ∈ ⟨⟨Id_on (dra.alphabet A)⟩ stream_rel⟩ set_rel"
    by parametricity

  then show ?thesis
    by (simp add: to_draei_def)
qed


subsection ‹Defining the Alphabet›

fun atoms_ltlc_list :: "'a ltlc ⇒ 'a list"
where
  "atoms_ltlc_list true⇩c = []"
| "atoms_ltlc_list false⇩c = []"
| "atoms_ltlc_list prop⇩c(q) = [q]"
| "atoms_ltlc_list (not⇩c φ) = atoms_ltlc_list φ"
| "atoms_ltlc_list (φ and⇩c ψ) = List.union (atoms_ltlc_list φ) (atoms_ltlc_list ψ)"
| "atoms_ltlc_list (φ or⇩c ψ) = List.union (atoms_ltlc_list φ) (atoms_ltlc_list ψ)"
| "atoms_ltlc_list (φ implies⇩c ψ) = List.union (atoms_ltlc_list φ) (atoms_ltlc_list ψ)"
| "atoms_ltlc_list (X⇩c φ) = atoms_ltlc_list φ"
| "atoms_ltlc_list (F⇩c φ) = atoms_ltlc_list φ"
| "atoms_ltlc_list (G⇩c φ) = atoms_ltlc_list φ"
| "atoms_ltlc_list (φ U⇩c ψ) = List.union (atoms_ltlc_list φ) (atoms_ltlc_list ψ)"
| "atoms_ltlc_list (φ R⇩c ψ) = List.union (atoms_ltlc_list φ) (atoms_ltlc_list ψ)"
| "atoms_ltlc_list (φ W⇩c ψ) = List.union (atoms_ltlc_list φ) (atoms_ltlc_list ψ)"
| "atoms_ltlc_list (φ M⇩c ψ) = List.union (atoms_ltlc_list φ) (atoms_ltlc_list ψ)"

lemma atoms_ltlc_list_set:
  "set (atoms_ltlc_list φ) = atoms_ltlc φ"
  by (induction φ) simp_all

lemma atoms_ltlc_list_distinct:
  "distinct (atoms_ltlc_list φ)"
  by (induction φ) simp_all

definition ltl_alphabet :: "'a list ⇒ 'a set list"
where
  "ltl_alphabet AP = map set (subseqs AP)"


subsection ‹The Final Constant›

text ‹
  We require the quotient type to be hashable in order to efficiently explore the automaton.
›

locale dra_implementation = dra_construction_size _ _ _ Abs
  for
    Abs :: "'a ltln ⇒ 'ltlq :: hashable"
begin

definition ltln_to_draei :: "'a list ⇒ 'a ltln ⇒ ('a set, nat) draei"
where
  "ltln_to_draei AP φ = drai_to_draei (Suc (size φ)) (dra_to_drai (ltl_to_dra_alphabet φ (set AP)) (ltl_alphabet AP))"

definition ltlc_to_draei :: "'a ltlc ⇒ ('a set, nat) draei"
where
  "ltlc_to_draei φ = ltln_to_draei (atoms_ltlc_list φ) (simplify Slow (ltlc_to_ltln φ))"


lemma ltl_to_dra_alphabet_rel:
  "distinct AP ⟹ (ltl_alphabet AP, alphabet (ltl_to_dra_alphabet ψ (set AP))) ∈ ⟨Id⟩ list_set_rel"
  unfolding ltl_to_dra_alphabet_alphabet ltl_alphabet_def
  by (simp add: list_set_rel_def in_br_conv subseqs_powset distinct_set_subseqs)

lemma ltlc_to_ltln_simplify_atoms:
  "atoms_ltln (simplify Slow (ltlc_to_ltln φ)) ⊆ atoms_ltlc φ"
  using ltlc_to_ltln_atoms simplify_atoms by fast

lemma valid_def_hm_size:
  "is_valid_def_hm_size TYPE('state) (Suc (size φ))" for φ :: "'a ltln"
  unfolding is_valid_def_hm_size_def
  using ltln.size_neq by auto

theorem final_correctness:
  "to_omega ` language (drae_dra (draei_drae (ltlc_to_draei φ)))
    = language_ltlc φ ∩ {w. range w ⊆ Pow (atoms_ltlc φ)}"
  unfolding ltlc_to_draei_def ltln_to_draei_def
  unfolding draei_language_rel[OF ltl_to_dra_alphabet_rel[OF atoms_ltlc_list_distinct] ltl_to_dra_alphabet_nodes_finite valid_def_hm_size]
  unfolding atoms_ltlc_list_set
  unfolding ltl_to_dra_alphabet_language[OF ltlc_to_ltln_simplify_atoms]
  unfolding ltlc_to_ltln_atoms language_ltln_def language_ltlc_def ltlc_to_ltln_semantics simplify_correct ..

end

end