# Theory DRA_Construction

```(*
Author:   Benedikt Seidl
*)

section ‹Constructing DRAs for LTL Formulas›

theory DRA_Construction
imports
Transition_Functions

"../Quotient_Type"
"../Omega_Words_Fun_Stream"

"HOL-Library.Log_Nat"

"../Logical_Characterization/Master_Theorem"
"../Logical_Characterization/Restricted_Master_Theorem"

Transition_Systems_and_Automata.DBA_Combine
Transition_Systems_and_Automata.DCA_Combine
Transition_Systems_and_Automata.DRA_Combine
begin

― ‹We use prefix and suffix on infinite words.›
hide_const Sublist.prefix Sublist.suffix

locale dra_construction = transition_functions eq normalise + quotient eq Rep Abs
for
eq :: "'a ltln ⇒ 'a ltln ⇒ bool" (infix "∼" 75)
and
normalise :: "'a ltln ⇒ 'a ltln"
and
Rep :: "'ltlq ⇒ 'a ltln"
and
Abs :: "'a ltln ⇒ 'ltlq"
begin

subsection ‹Lifting Setup›

abbreviation true⇩n_lifted :: "'ltlq" ("↑true⇩n") where
"↑true⇩n ≡ Abs true⇩n"

abbreviation false⇩n_lifted :: "'ltlq" ("↑false⇩n") where
"↑false⇩n ≡ Abs false⇩n"

abbreviation af_letter_lifted :: "'a set ⇒ 'ltlq ⇒ 'ltlq" ("↑afletter") where
"↑afletter ν φ ≡ Abs (af_letter (Rep φ) ν)"

abbreviation af_lifted :: "'ltlq ⇒ 'a set list ⇒ 'ltlq" ("↑af") where
"↑af φ w ≡ fold ↑afletter w φ"

abbreviation GF_advice_lifted :: "'ltlq ⇒ 'a ltln set ⇒ 'ltlq" ("_↑[_]⇩ν" [90,60] 89) where
"φ↑[X]⇩ν ≡ Abs ((Rep φ)[X]⇩ν)"

lemma af_letter_lifted_semantics:
"↑afletter ν (Abs φ) = Abs (af_letter φ ν)"
by (metis Rep_Abs_eq af_letter_congruent Abs_eq)

lemma af_lifted_semantics:
"↑af (Abs φ) w = Abs (af φ w)"
by (induction w rule: rev_induct) (auto simp: Abs_eq, insert Rep_Abs_eq af_letter_congruent eq_sym, blast)

lemma af_lifted_range:
"range (↑af (Abs φ)) ⊆ {Abs ψ | ψ. nested_prop_atoms ψ ⊆ nested_prop_atoms φ}"
using af_lifted_semantics af_nested_prop_atoms by blast

definition af_letter⇩F_lifted :: "'a ltln ⇒ 'a set ⇒ 'ltlq ⇒ 'ltlq" ("↑afletter⇩F")
where
"↑afletter⇩F φ ν ψ ≡ Abs (af_letter⇩F φ (Rep ψ) ν)"

definition af_letter⇩G_lifted :: "'a ltln ⇒ 'a set ⇒ 'ltlq ⇒ 'ltlq" ("↑afletter⇩G")
where
"↑afletter⇩G φ ν ψ ≡ Abs (af_letter⇩G φ (Rep ψ) ν)"

lemma af_letter⇩F_lifted_semantics:
"↑afletter⇩F φ ν (Abs ψ) = Abs (af_letter⇩F φ ψ ν)"
by (metis af_letter⇩F_lifted_def Rep_inverse af_letter⇩F_def af_letter_congruent Abs_eq)

lemma af_letter⇩G_lifted_semantics:
"↑afletter⇩G φ ν (Abs ψ) = Abs (af_letter⇩G φ ψ ν)"
by (metis af_letter⇩G_lifted_def Rep_inverse af_letter⇩G_def af_letter_congruent Abs_eq)

abbreviation af⇩F_lifted :: "'a ltln ⇒ 'ltlq ⇒ 'a set list ⇒ 'ltlq" ("↑af⇩F")
where
"↑af⇩F φ ψ w ≡ fold (↑afletter⇩F φ) w ψ"

abbreviation af⇩G_lifted :: "'a ltln ⇒ 'ltlq ⇒ 'a set list ⇒ 'ltlq" ("↑af⇩G")
where
"↑af⇩G φ ψ w ≡ fold (↑afletter⇩G φ) w ψ"

lemma af⇩F_lifted_semantics:
"↑af⇩F φ (Abs ψ) w = Abs (af⇩F φ ψ w)"
by (induction w rule: rev_induct) (auto simp: af_letter⇩F_lifted_semantics)

lemma af⇩G_lifted_semantics:
"↑af⇩G φ (Abs ψ) w = Abs (af⇩G φ ψ w)"
by (induction w rule: rev_induct) (auto simp: af_letter⇩G_lifted_semantics)

definition af_letter⇩ν_lifted :: "'a ltln set ⇒ 'a set ⇒ 'ltlq × 'ltlq ⇒ 'ltlq × 'ltlq" ("↑afletter⇩ν")
where
"↑afletter⇩ν X ν p ≡
(Abs (fst (af_letter⇩ν X (Rep (fst p), Rep (snd p)) ν)),
Abs (snd (af_letter⇩ν X (Rep (fst p), Rep (snd p)) ν)))"

abbreviation af⇩ν_lifted :: "'a ltln set ⇒ 'ltlq × 'ltlq ⇒ 'a set list ⇒ 'ltlq × 'ltlq" ("↑af⇩ν")
where
"↑af⇩ν X p w ≡ fold (↑afletter⇩ν X) w p"

lemma af_letter⇩ν_lifted_semantics:
"↑afletter⇩ν X ν (Abs x, Abs y) = (Abs (fst (af_letter⇩ν X (x, y) ν)), Abs (snd (af_letter⇩ν X (x, y) ν)))"
by (simp add: af_letter⇩ν_def af_letter⇩ν_lifted_def) (insert GF_advice_congruent Rep_Abs_eq Rep_inverse af_letter_lifted_semantics eq_trans Abs_eq, blast)

lemma af⇩ν_lifted_semantics:
"↑af⇩ν X (Abs ξ, Abs ζ) w = (Abs (fst (af⇩ν X (ξ, ζ) w)), Abs (snd (af⇩ν X (ξ, ζ) w)))"
apply (induction w rule: rev_induct)
apply (auto simp: af_letter⇩ν_lifted_def af_letter⇩ν_lifted_semantics af_letter_lifted_semantics)
by (metis (no_types, opaque_lifting) af_letter⇩ν_lifted_def af⇩ν_fst af_letter⇩ν_lifted_semantics eq_fst_iff prod.sel(2))

subsection ‹Büchi automata for basic languages›

definition 𝔄⇩μ :: "'a ltln ⇒ ('a set, 'ltlq) dba" where
"𝔄⇩μ φ = dba UNIV (Abs φ) ↑afletter (λψ. ψ = ↑true⇩n)"

definition 𝔄⇩μ_GF :: "'a ltln ⇒ ('a set, 'ltlq) dba" where
"𝔄⇩μ_GF φ = dba UNIV (Abs (F⇩n φ)) (↑afletter⇩F φ) (λψ. ψ = ↑true⇩n)"

definition 𝔄⇩ν :: "'a ltln ⇒ ('a set, 'ltlq) dca" where
"𝔄⇩ν φ = dca UNIV (Abs φ) ↑afletter (λψ. ψ = ↑false⇩n)"

definition 𝔄⇩ν_FG :: "'a ltln ⇒ ('a set, 'ltlq) dca" where
"𝔄⇩ν_FG φ = dca UNIV (Abs (G⇩n φ)) (↑afletter⇩G φ) (λψ. ψ = ↑false⇩n)"

lemma dba_run:
"DBA.run (dba UNIV p δ α) (to_stream w) p" unfolding dba.run_alt_def by simp

lemma dca_run:
"DCA.run (dca UNIV p δ α) (to_stream w) p" unfolding dca.run_alt_def by simp

lemma 𝔄⇩μ_language:
"φ ∈ μLTL ⟹ to_stream w ∈ DBA.language (𝔄⇩μ φ) ⟷ w ⊨⇩n φ"
proof -
assume "φ ∈ μLTL"

then have "w ⊨⇩n φ ⟷ (∀n. ∃k≥n. af φ (w[0 → k]) ∼ true⇩n)"
by (meson af_μLTL af_prefix_true le_cases)

also have "… ⟷ (∀n. ∃k≥n. af φ (w[0 → Suc k]) ∼ true⇩n)"
by (meson af_prefix_true le_SucI order_refl)

also have "… ⟷ infs (λψ. ψ = ↑true⇩n) (DBA.trace (𝔄⇩μ φ) (to_stream w) (Abs φ))"
by (simp add: infs_snth 𝔄⇩μ_def DBA.transition_def af_lifted_semantics Abs_eq[symmetric] af_letter_lifted_semantics)

also have "… ⟷ to_stream w ∈ DBA.language (𝔄⇩μ φ)"
unfolding 𝔄⇩μ_def dba.initial_def dba.accepting_def by (auto simp: dba_run)

finally show ?thesis
by simp
qed

lemma 𝔄⇩μ_GF_language:
"φ ∈ μLTL ⟹ to_stream w ∈ DBA.language (𝔄⇩μ_GF φ) ⟷ w ⊨⇩n G⇩n (F⇩n φ)"
proof -
assume "φ ∈ μLTL"

then have "w ⊨⇩n G⇩n (F⇩n φ) ⟷ (∀n. ∃k. af (F⇩n φ) (w[n → k]) ∼⇩L true⇩n)"
using ltl_lang_equivalence.af_μLTL_GF by blast

also have "… ⟷ (∀n. ∃k>n. af⇩F φ (F⇩n φ) (w[0 → k]) ∼ true⇩n)"
using af⇩F_semantics_ltr af⇩F_semantics_rtl
using ‹φ ∈ μLTL› af_μLTL_GF calculation by blast

also have "… ⟷ (∀n. ∃k≥n. af⇩F φ (F⇩n φ) (w[0 → Suc k]) ∼ true⇩n)"

also have "… ⟷ infs (λψ. ψ = ↑true⇩n) (DBA.trace (𝔄⇩μ_GF φ) (to_stream w) (Abs (F⇩n φ)))"
by (simp add: infs_snth 𝔄⇩μ_GF_def DBA.transition_def af⇩F_lifted_semantics Abs_eq[symmetric] af_letter⇩F_lifted_semantics)

also have "… ⟷ to_stream w ∈ DBA.language (𝔄⇩μ_GF φ)"
unfolding 𝔄⇩μ_GF_def dba.initial_def dba.accepting_def by (auto simp: dba_run)

finally show ?thesis
by simp
qed

lemma 𝔄⇩ν_language:
"φ ∈ νLTL ⟹ to_stream w ∈ DCA.language (𝔄⇩ν φ) ⟷ w ⊨⇩n φ"
proof -
assume "φ ∈ νLTL"

then have "w ⊨⇩n φ ⟷ (∃n. ∀k≥n. ¬ af φ (w[0 → k]) ∼ false⇩n)"
by (meson af_νLTL af_prefix_false le_cases order_refl)

also have "… ⟷ (∃n. ∀k≥n. ¬ af φ (w[0 → Suc k]) ∼ false⇩n)"
by (meson af_prefix_false le_SucI order_refl)

also have "… ⟷ fins (λψ. ψ = ↑false⇩n) (DCA.trace (𝔄⇩ν φ) (to_stream w) (Abs φ))"
by (simp add: infs_snth 𝔄⇩ν_def DBA.transition_def af_lifted_semantics Abs_eq[symmetric] af_letter_lifted_semantics)

also have "… ⟷ to_stream w ∈ DCA.language (𝔄⇩ν φ)"
unfolding 𝔄⇩ν_def dca.initial_def dca.rejecting_def by (auto simp: dca_run)

finally show ?thesis
by simp
qed

lemma 𝔄⇩ν_FG_language:
"φ ∈ νLTL ⟹ to_stream w ∈ DCA.language (𝔄⇩ν_FG φ) ⟷ w ⊨⇩n F⇩n (G⇩n φ)"
proof -
assume "φ ∈ νLTL"

then have "w ⊨⇩n F⇩n (G⇩n φ) ⟷ (∃k. ∀j. ¬ af (G⇩n φ) (w[k → j]) ∼⇩L false⇩n)"
using ltl_lang_equivalence.af_νLTL_FG by blast

also have "… ⟷ (∃n. ∀k>n. ¬ af⇩G φ (G⇩n φ) (w[0 → k]) ∼ false⇩n)"
using af⇩G_semantics_ltr af⇩G_semantics_rtl
using ‹φ ∈ νLTL› af_νLTL_FG calculation by blast

also have "… ⟷ (∃n. ∀k≥n. ¬ af⇩G φ (G⇩n φ) (w[0 → Suc k]) ∼ false⇩n)"

also have "… ⟷ fins (λψ. ψ = ↑false⇩n) (DCA.trace (𝔄⇩ν_FG φ) (to_stream w) (Abs (G⇩n φ)))"
by (simp add: infs_snth 𝔄⇩ν_FG_def DBA.transition_def af⇩G_lifted_semantics Abs_eq[symmetric] af_letter⇩G_lifted_semantics)

also have "… ⟷ to_stream w ∈ DCA.language (𝔄⇩ν_FG φ)"
unfolding 𝔄⇩ν_FG_def dca.initial_def dca.rejecting_def by (auto simp: dca_run)

finally show ?thesis
by simp
qed

subsection ‹A DCA checking the GF-advice Function›

definition ℭ :: "'a ltln ⇒ 'a ltln set ⇒ ('a set, 'ltlq × 'ltlq) dca" where
"ℭ φ X = dca UNIV (Abs φ, Abs ((normalise φ)[X]⇩ν)) (↑afletter⇩ν X) (λp. snd p = ↑false⇩n)"

lemma ℭ_language:
"to_stream w ∈ DCA.language (ℭ φ X) ⟷ (∃i. suffix i w ⊨⇩n af φ (prefix i w)[X]⇩ν)"
proof -

have "(∃i. suffix i w ⊨⇩n af φ (prefix i w)[X]⇩ν)
⟷ (∃m. ∀k≥m. ¬ snd (af⇩ν X (φ, (normalise φ)[X]⇩ν) (prefix (Suc k) w)) ∼ false⇩n)"
using af⇩ν_semantics_ltr af⇩ν_semantics_rtl by blast

also have "… ⟷ fins (λp. snd p = ↑false⇩n) (DCA.trace (ℭ φ X) (to_stream w) (Abs φ, Abs ((normalise φ)[X]⇩ν)))"
by(simp add: infs_snth ℭ_def DCA.transition_def af⇩ν_lifted_semantics af_letter⇩ν_lifted_semantics Abs_eq)

also have "… ⟷ to_stream w ∈ DCA.language (ℭ φ X)"
by (simp add: ℭ_def dca.initial_def dca.rejecting_def dca.language_def dca_run)

finally show ?thesis
by blast
qed

subsection ‹A DRA for each combination of sets X and Y›

lemma dba_language:
"(⋀w. to_stream w ∈ DBA.language 𝔄 ⟷ w ⊨⇩n φ) ⟹ DBA.language 𝔄 = {w. to_omega w ⊨⇩n φ}"
by (metis (mono_tags, lifting) Collect_cong dba.language_def mem_Collect_eq to_stream_to_omega)

lemma dca_language:
"(⋀w. to_stream w ∈ DCA.language 𝔄 ⟷ w ⊨⇩n φ) ⟹ DCA.language 𝔄 = {w. to_omega w ⊨⇩n φ}"
by (metis (mono_tags, lifting) Collect_cong dca.language_def mem_Collect_eq to_stream_to_omega)

definition 𝔄⇩1 :: "'a ltln ⇒ 'a ltln list ⇒ ('a set, 'ltlq × 'ltlq) dca" where
"𝔄⇩1 φ xs = ℭ φ (set xs)"

lemma 𝔄⇩1_language:
"to_omega ` DCA.language (𝔄⇩1 φ xs) = L⇩1 φ (set xs)"
by (simp add: 𝔄⇩1_def L⇩1_def set_eq_iff ℭ_language)

lemma 𝔄⇩1_alphabet:
"DCA.alphabet (𝔄⇩1 φ xs) = UNIV"
unfolding 𝔄⇩1_def ℭ_def by simp

definition 𝔄⇩2 :: "'a ltln list ⇒ 'a ltln list ⇒ ('a set, 'ltlq list degen) dba" where
"𝔄⇩2 xs ys = DBA_Combine.intersect_list (map (λψ. 𝔄⇩μ_GF (ψ[set ys]⇩μ)) xs)"

lemma 𝔄⇩2_language:
"to_omega ` DBA.language (𝔄⇩2 xs ys) = L⇩2 (set xs) (set ys)"

lemma 𝔄⇩2_alphabet:
"DBA.alphabet (𝔄⇩2 xs ys) = UNIV"

definition 𝔄⇩3 :: "'a ltln list ⇒ 'a ltln list ⇒ ('a set, 'ltlq list) dca" where
"𝔄⇩3 xs ys = DCA_Combine.intersect_list (map (λψ. 𝔄⇩ν_FG (ψ[set xs]⇩ν)) ys)"

lemma 𝔄⇩3_language:
"to_omega ` DCA.language (𝔄⇩3 xs ys) = L⇩3 (set xs) (set ys)"

lemma 𝔄⇩3_alphabet:
"DCA.alphabet (𝔄⇩3 xs ys) = UNIV"

definition "𝔄' φ xs ys = intersect_bc (𝔄⇩2 xs ys) (DCA_Combine.intersect (𝔄⇩1 φ xs) (𝔄⇩3 xs ys))"

lemma 𝔄'_language:
"to_omega ` DRA.language (𝔄' φ xs ys) = (L⇩1 φ (set xs) ∩ L⇩2 (set xs) (set ys) ∩ L⇩3 (set xs) (set ys))"
by (simp add: 𝔄'_def 𝔄⇩1_language 𝔄⇩2_language 𝔄⇩3_language) fastforce

lemma 𝔄'_alphabet:
"DRA.alphabet (𝔄' φ xs ys) = UNIV"
by (simp add: 𝔄'_def 𝔄⇩1_alphabet 𝔄⇩2_alphabet 𝔄⇩3_alphabet)

subsection ‹A DRA for @{term "L(φ)"}›

text ‹
This is the final constant constructing a deterministic Rabin automaton
using the pure version of the  @{thm master_theorem}.
›

definition "ltl_to_dra φ = DRA_Combine.union_list (map (λ(xs, ys). 𝔄' φ xs ys) (advice_sets φ))"

lemma ltl_to_dra_language:
"to_omega ` DRA.language (ltl_to_dra φ) = language_ltln φ"
proof -
have "(⋂(a, b)∈set (advice_sets φ). dra.alphabet (𝔄' φ a b)) =
(⋃(a, b)∈set (advice_sets φ). dra.alphabet (𝔄' φ a b))"
then have *: "DRA.language (DRA_Combine.union_list (map (λ(x, y). 𝔄' φ x y) (advice_sets φ))) =
⋃ (DRA.language ` set (map (λ(x, y). 𝔄' φ x y) (advice_sets φ)))"
have "language_ltln φ = ⋃ {(L⇩1 φ X ∩ L⇩2 X Y ∩ L⇩3 X Y) | X Y. X ⊆ subformulas⇩μ φ ∧ Y ⊆ subformulas⇩ν φ}"
unfolding master_theorem_language by auto
also have "… = ⋃ {L⇩1 φ (set xs) ∩ L⇩2 (set xs) (set ys) ∩ L⇩3 (set xs) (set ys) | xs ys. (xs, ys) ∈ set (advice_sets φ)}"
unfolding advice_sets_subformulas by (metis (no_types, lifting))
also have "… = ⋃ {to_omega ` DRA.language (𝔄' φ xs ys) | xs ys. (xs, ys) ∈ set (advice_sets φ)}"
finally show ?thesis
using * by (auto simp add: ltl_to_dra_def)
qed

lemma ltl_to_dra_alphabet:
"alphabet (ltl_to_dra φ) = UNIV"
by (auto simp: ltl_to_dra_def 𝔄'_alphabet)

subsection ‹A DRA for @{term "L(φ)"} with Restricted Advice Sets›

text ‹
The following constant uses the @{thm master_theorem_restricted} to reduce
the size of the resulting automaton.
›

definition "ltl_to_dra_restricted φ = DRA_Combine.union_list (map (λ(xs, ys). 𝔄' φ xs ys) (restricted_advice_sets φ))"

lemma ltl_to_dra_restricted_language:
"to_omega ` DRA.language (ltl_to_dra_restricted φ) = language_ltln φ"
proof -
have "(⋂(a, b)∈set (restricted_advice_sets φ). dra.alphabet (𝔄' φ a b)) =
(⋃(a, b)∈set (restricted_advice_sets φ). dra.alphabet (𝔄' φ a b))"
then have *: "DRA.language (DRA_Combine.union_list (map (λ(x, y). 𝔄' φ x y) (restricted_advice_sets φ))) =
⋃ (DRA.language ` set (map (λ(x, y). 𝔄' φ x y) (restricted_advice_sets φ)))"
have "language_ltln φ = ⋃ {(L⇩1 φ X ∩ L⇩2 X Y ∩ L⇩3 X Y) | X Y. X ⊆ subformulas⇩μ φ ∩ restricted_subformulas φ ∧ Y ⊆ subformulas⇩ν φ ∩ restricted_subformulas φ}"
unfolding master_theorem_restricted_language by auto
also have "… = ⋃ {L⇩1 φ (set xs) ∩ L⇩2 (set xs) (set ys) ∩ L⇩3 (set xs) (set ys) | xs ys. (xs, ys) ∈ set (restricted_advice_sets φ)}"
unfolding restricted_advice_sets_subformulas by (metis (no_types, lifting))
also have "… = ⋃ {to_omega ` DRA.language (𝔄' φ xs ys) | xs ys. (xs, ys) ∈ set (restricted_advice_sets φ)}"
finally show ?thesis
using * by (auto simp add: ltl_to_dra_restricted_def)
qed

lemma ltl_to_dra_restricted_alphabet:
"alphabet (ltl_to_dra_restricted φ) = UNIV"
by (auto simp: ltl_to_dra_restricted_def 𝔄'_alphabet)

subsection ‹A DRA for @{term "L(φ)"} with a finite alphabet›

text ‹
Until this point, we use @{term UNIV} as the alphabet in all places.
To explore the automaton, however, we need a way to fix the alphabet
to some finite set.
›

definition dra_set_alphabet :: "('a set, 'b) dra ⇒ 'a set set ⇒ ('a set, 'b) dra"
where
"dra_set_alphabet 𝔄 Σ = dra Σ (initial 𝔄) (transition 𝔄) (condition 𝔄)"

lemma dra_set_alphabet_language:
"Σ ⊆ alphabet 𝔄 ⟹ language (dra_set_alphabet 𝔄 Σ) = language 𝔄 ∩ {s. sset s ⊆ Σ}"
by (auto simp add: dra_set_alphabet_def dra.language_def set_eq_iff dra.run_alt_def streams_iff_sset)

lemma dra_set_alphabet_alphabet[simp]:
"alphabet (dra_set_alphabet 𝔄 Σ) = Σ"
unfolding dra_set_alphabet_def by simp

lemma dra_set_alphabet_nodes:
"Σ ⊆ alphabet 𝔄 ⟹ DRA.nodes (dra_set_alphabet 𝔄 Σ) ⊆ DRA.nodes 𝔄"
unfolding dra_set_alphabet_def dra.nodes_alt_def dra.reachable_alt_def dra.path_alt_def
by auto

definition "ltl_to_dra_alphabet φ Ap = dra_set_alphabet (ltl_to_dra_restricted φ) (Pow Ap)"

lemma ltl_to_dra_alphabet_language:
assumes
"atoms_ltln φ ⊆ Ap"
shows
"to_omega ` language (ltl_to_dra_alphabet φ Ap) = language_ltln φ ∩ {w. range w ⊆ Pow Ap}"
proof -
have 1: "Pow Ap ⊆ alphabet (ltl_to_dra_restricted φ)"
unfolding ltl_to_dra_restricted_alphabet by simp

show ?thesis
unfolding ltl_to_dra_alphabet_def dra_set_alphabet_language[OF 1]
by (simp add: ltl_to_dra_restricted_language sset_range) force
qed

lemma ltl_to_dra_alphabet_alphabet[simp]:
"alphabet (ltl_to_dra_alphabet φ Ap) = Pow Ap"
unfolding ltl_to_dra_alphabet_def by simp

lemma ltl_to_dra_alphabet_nodes:
"DRA.nodes (ltl_to_dra_alphabet φ Ap) ⊆ DRA.nodes (ltl_to_dra_restricted φ)"
unfolding ltl_to_dra_alphabet_def
by (rule dra_set_alphabet_nodes) (simp add: ltl_to_dra_restricted_alphabet)

end

subsection ‹Verified Bounds for Number of Nodes›

text ‹
Using two additional assumptions, we can show a double-exponential size bound
for the constructed automaton.
›

(* TODO add to HOL/Groups_List.thy *)
lemma list_prod_mono:
"f ≤ g ⟹ (∏x←xs. f x) ≤ (∏x←xs. g x)" for f g :: "'a ⇒ nat"
by (induction xs) (auto simp: le_funD mult_le_mono)

(* TODO add to HOL/Groups_List.thy *)
lemma list_prod_const:
"(⋀x. x ∈ set xs ⟹ f x ≤ c) ⟹ (∏x←xs. f x) ≤ c ^ length xs" for f :: "'a ⇒ nat"
by (induction xs) (auto simp: mult_le_mono)

(* TODO add to HOL/Finite_Set.thy *)
lemma card_insert_Suc:
"card (insert x S) ≤ Suc (card S)"
by (metis Suc_n_not_le_n card.infinite card_insert_if finite_insert linear)

(* TODO add to HOL/Power.thy *)
lemma nat_power_le_imp_le:
"0 < a ⟹ a ≤ b ⟹ x ^ a ≤ x ^ b" for x :: nat
by (metis leD linorder_le_less_linear nat_power_less_imp_less neq0_conv power_eq_0_iff)

(* TODO add to HOL/Power.thy *)
lemma const_less_power:
"n < x ^ n" if "x > 1"
using that by (induction n) (auto simp: less_trans_Suc)

(* TODO add to HOL-Library/Log_Nat.thy *)
lemma floorlog_le_const:
"floorlog x n ≤ n"
by (induction n) (simp add: floorlog_eq_zero_iff, metis Suc_lessI floorlog_le_iff le_SucI power_inject_exp)

locale dra_construction_size = dra_construction + transition_functions_size +
assumes
equiv_finite: "finite P ⟹ finite {Abs ψ | ψ. prop_atoms ψ ⊆ P}"
assumes
equiv_card: "finite P ⟹ card {Abs ψ | ψ. prop_atoms ψ ⊆ P} ≤ 2 ^ 2 ^ card P"
begin

lemma af⇩F_lifted_range:
"nested_prop_atoms ψ ⊆ nested_prop_atoms (F⇩n φ) ⟹ range (↑af⇩F φ (Abs ψ)) ⊆  {Abs ψ | ψ. nested_prop_atoms ψ ⊆ nested_prop_atoms (F⇩n φ)}"
using af⇩F_lifted_semantics af⇩F_nested_prop_atoms by blast

lemma af⇩G_lifted_range:
"nested_prop_atoms ψ ⊆ nested_prop_atoms (G⇩n φ) ⟹ range (↑af⇩G φ (Abs ψ)) ⊆  {Abs ψ | ψ. nested_prop_atoms ψ ⊆ nested_prop_atoms (G⇩n φ)}"
using af⇩G_lifted_semantics af⇩G_nested_prop_atoms by blast

lemma 𝔄⇩μ_nodes:
"DBA.nodes (𝔄⇩μ φ) ⊆ {Abs ψ | ψ. nested_prop_atoms ψ ⊆ nested_prop_atoms φ}"
unfolding 𝔄⇩μ_def
using af_lifted_semantics af_nested_prop_atoms by fastforce

lemma 𝔄⇩μ_GF_nodes:
"DBA.nodes (𝔄⇩μ_GF φ) ⊆ {Abs ψ | ψ. nested_prop_atoms ψ ⊆ nested_prop_atoms (F⇩n φ)}"
unfolding 𝔄⇩μ_GF_def dba.nodes_alt_def dba.reachable_alt_def
using af⇩F_nested_prop_atoms[of "F⇩n φ"] by (auto simp: af⇩F_lifted_semantics)

lemma 𝔄⇩ν_nodes:
"DCA.nodes (𝔄⇩ν φ) ⊆ {Abs ψ | ψ. nested_prop_atoms ψ ⊆ nested_prop_atoms φ}"
unfolding 𝔄⇩ν_def
using af_lifted_semantics af_nested_prop_atoms by fastforce

lemma 𝔄⇩ν_FG_nodes:
"DCA.nodes (𝔄⇩ν_FG φ) ⊆ {Abs ψ | ψ. nested_prop_atoms ψ ⊆ nested_prop_atoms (G⇩n φ)}"
unfolding 𝔄⇩ν_FG_def dca.nodes_alt_def dca.reachable_alt_def
using af⇩G_nested_prop_atoms[of "G⇩n φ"] by (auto simp: af⇩G_lifted_semantics)

lemma ℭ_nodes_normalise:
"DCA.nodes (ℭ φ X) ⊆ {Abs ψ | ψ. nested_prop_atoms ψ ⊆ nested_prop_atoms φ} × {Abs ψ | ψ. nested_prop_atoms ψ ⊆ nested_prop_atoms⇩ν (normalise φ) X}"
unfolding ℭ_def dca.nodes_alt_def dca.reachable_alt_def
apply (auto simp add: af⇩ν_lifted_semantics af_letter⇩ν_lifted_semantics)
using af⇩ν_fst_nested_prop_atoms apply force
by (metis GF_advice_nested_prop_atoms⇩ν af⇩ν_snd_nested_prop_atoms Abs_eq af⇩ν_lifted_semantics fst_conv normalise_eq snd_conv sup.absorb_iff1)

lemma ℭ_nodes:
"DCA.nodes (ℭ φ X) ⊆ {Abs ψ | ψ. nested_prop_atoms ψ ⊆ nested_prop_atoms φ} × {Abs ψ | ψ. nested_prop_atoms ψ ⊆ nested_prop_atoms⇩ν φ X}"
unfolding ℭ_def dca.nodes_alt_def dca.reachable_alt_def
apply (auto simp add: af⇩ν_lifted_semantics af_letter⇩ν_lifted_semantics)
using af⇩ν_fst_nested_prop_atoms apply force
by (metis (no_types, opaque_lifting) GF_advice_nested_prop_atoms⇩ν af⇩ν_snd_nested_prop_atoms fst_eqD nested_prop_atoms⇩ν_subset normalise_nested_propos order_refl order_trans snd_eqD sup.order_iff)

lemma equiv_subset:
"{Abs ψ |ψ. nested_prop_atoms ψ ⊆ P} ⊆ {Abs ψ |ψ. prop_atoms ψ ⊆ P}"
using prop_atoms_nested_prop_atoms by blast

lemma equiv_finite':
"finite P ⟹ finite {Abs ψ | ψ. nested_prop_atoms ψ ⊆ P}"
using equiv_finite equiv_subset finite_subset by fast

lemma equiv_card':
"finite P ⟹ card {Abs ψ | ψ. nested_prop_atoms ψ ⊆ P} ≤ 2 ^ 2 ^ card P"
by (metis (mono_tags, lifting) equiv_card equiv_subset equiv_finite card_mono le_trans)

lemma nested_prop_atoms_finite:
"finite {Abs ψ | ψ. nested_prop_atoms ψ ⊆ nested_prop_atoms φ}"
using equiv_finite'[OF Equivalence_Relations.nested_prop_atoms_finite] .

lemma nested_prop_atoms_card:
"card {Abs ψ | ψ. nested_prop_atoms ψ ⊆ nested_prop_atoms φ} ≤ 2 ^ 2 ^ card (nested_prop_atoms φ)"
using equiv_card'[OF Equivalence_Relations.nested_prop_atoms_finite] .

lemma nested_prop_atoms⇩ν_finite:
"finite {Abs ψ | ψ. nested_prop_atoms ψ ⊆ nested_prop_atoms⇩ν φ X}"
using equiv_finite'[OF nested_prop_atoms⇩ν_finite] by fast

lemma nested_prop_atoms⇩ν_card:
"card {Abs ψ | ψ. nested_prop_atoms ψ ⊆ nested_prop_atoms⇩ν φ X} ≤ 2 ^ 2 ^ card (nested_prop_atoms φ)" (is "?lhs ≤ ?rhs")
proof -
have "finite {Abs ψ | ψ. prop_atoms ψ ⊆ nested_prop_atoms⇩ν φ X}"

then have "?lhs ≤ card {Abs ψ | ψ. prop_atoms ψ ⊆ (nested_prop_atoms⇩ν φ X)}"
using card_mono equiv_subset by blast

also have "… ≤ 2 ^ 2 ^ card (nested_prop_atoms⇩ν φ X)"

also have "… ≤ ?rhs"
using nested_prop_atoms⇩ν_card by auto

finally show ?thesis .
qed

lemma 𝔄⇩μ_GF_nodes_finite:
"finite (DBA.nodes (𝔄⇩μ_GF φ))"
using finite_subset[OF 𝔄⇩μ_GF_nodes nested_prop_atoms_finite] .

lemma 𝔄⇩ν_FG_nodes_finite:
"finite (DCA.nodes (𝔄⇩ν_FG φ))"
using finite_subset[OF 𝔄⇩ν_FG_nodes nested_prop_atoms_finite] .

lemma 𝔄⇩μ_GF_nodes_card:
"card (DBA.nodes (𝔄⇩μ_GF φ)) ≤ 2 ^ 2 ^ card (nested_prop_atoms (F⇩n φ))"
using le_trans[OF card_mono[OF nested_prop_atoms_finite 𝔄⇩μ_GF_nodes] nested_prop_atoms_card] .

lemma 𝔄⇩ν_FG_nodes_card:
"card (DCA.nodes (𝔄⇩ν_FG φ)) ≤ 2 ^ 2 ^ card (nested_prop_atoms (G⇩n φ))"
using le_trans[OF card_mono[OF nested_prop_atoms_finite 𝔄⇩ν_FG_nodes] nested_prop_atoms_card] .

lemma 𝔄⇩2_nodes_finite_helper:
"list_all (finite ∘ DBA.nodes) (map (λψ. 𝔄⇩μ_GF (ψ[set ys]⇩μ)) xs)"
by (auto simp: list.pred_map list_all_iff 𝔄⇩μ_GF_nodes_finite)

lemma 𝔄⇩2_nodes_finite:
"finite (DBA.nodes (𝔄⇩2 xs ys))"
unfolding 𝔄⇩2_def using DBA_Combine.intersect_list_nodes_finite 𝔄⇩2_nodes_finite_helper .

lemma 𝔄⇩3_nodes_finite_helper:
"list_all (finite ∘ DCA.nodes) (map (λψ. 𝔄⇩ν_FG (ψ[set xs]⇩ν)) ys)"
by (auto simp: list.pred_map list_all_iff 𝔄⇩ν_FG_nodes_finite)

lemma 𝔄⇩3_nodes_finite:
"finite (DCA.nodes (𝔄⇩3 xs ys))"
unfolding 𝔄⇩3_def using DCA_Combine.intersect_list_nodes_finite 𝔄⇩3_nodes_finite_helper .

lemma 𝔄⇩2_nodes_card:
assumes
"length xs ≤ n"
and
"⋀ψ. ψ ∈ set xs ⟹ card (nested_prop_atoms ψ) ≤ n"
shows
"card (DBA.nodes (𝔄⇩2 xs ys)) ≤ 2 ^ 2 ^ (n + floorlog 2 n + 2)"
proof -
have 1: "⋀ψ. ψ ∈ set xs ⟹ card (nested_prop_atoms (F⇩n ψ[set ys]⇩μ)) ≤ Suc n"
proof -
fix ψ
assume "ψ ∈ set xs"

have "card (nested_prop_atoms (F⇩n (ψ[set ys]⇩μ)))
≤ Suc (card (nested_prop_atoms (ψ[set ys]⇩μ)))"

also have "… ≤ Suc (card (nested_prop_atoms ψ))"

also have "… ≤ Suc n"
by (simp add: assms(2) ‹ψ ∈ set xs›)

finally show "card (nested_prop_atoms (F⇩n (ψ[set ys]⇩μ))) ≤ Suc n" .
qed

have "(∏ψ←xs. card (DBA.nodes (𝔄⇩μ_GF (ψ[set ys]⇩μ))))
≤ (∏ψ←xs. 2 ^ 2 ^ card (nested_prop_atoms (F⇩n (ψ[set ys]⇩μ))))"
by (rule list_prod_mono) (insert 𝔄⇩μ_GF_nodes_card le_fun_def, blast)

also have "… ≤ (2 ^ 2 ^ Suc n) ^ length xs"
by (rule list_prod_const) (metis 1 Suc_leI nat_power_le_imp_le nat_power_eq_Suc_0_iff neq0_conv pos2 zero_less_power)

also have "… ≤ (2 ^ 2 ^ Suc n) ^ n"
using assms(1) nat_power_le_imp_le by fastforce

also have "… = 2 ^ (n * 2 ^ Suc n)"
by (metis Groups.mult_ac(2) power_mult)

also have "… ≤ 2 ^ (2 ^ floorlog 2 n * 2 ^ Suc n)"
by (cases "n = 0") (auto simp: floorlog_bounds less_imp_le_nat)

also have "… = 2 ^ 2 ^ (Suc n + floorlog 2 n)"

finally have 2: "(∏ψ←xs. card (DBA.nodes (𝔄⇩μ_GF (ψ[set ys]⇩μ)))) ≤ 2 ^ 2 ^ (Suc n + floorlog 2 n)" .

have "card (DBA.nodes (𝔄⇩2 xs ys)) ≤ max 1 (length xs) * (∏ψ←xs. card (DBA.nodes (𝔄⇩μ_GF (ψ[set ys]⇩μ))))"
using DBA_Combine.intersect_list_nodes_card[OF 𝔄⇩2_nodes_finite_helper]
by (auto simp: 𝔄⇩2_def comp_def)

also have "… ≤ max 1 n * 2 ^ 2 ^ (Suc n + floorlog 2 n)"
using assms(1) 2 by (simp add: mult_le_mono)

also have "… ≤ 2 ^ (floorlog 2 n) * 2 ^ 2 ^ (Suc n + floorlog 2 n)"
by (cases "n = 0") (auto simp: floorlog_bounds less_imp_le_nat)

also have "… = 2 ^ (floorlog 2 n + 2 ^ (Suc n + floorlog 2 n))"

also have "… ≤ 2 ^ (n + 2 ^ (Suc n + floorlog 2 n))"

also have "… ≤ 2 ^ 2 ^ (n + floorlog 2 n + 2)"

finally show ?thesis .
qed

lemma 𝔄⇩3_nodes_card:
assumes
"length ys ≤ n"
and
"⋀ψ. ψ ∈ set ys ⟹ card (nested_prop_atoms ψ) ≤ n"
shows
"card (DCA.nodes (𝔄⇩3 xs ys)) ≤ 2 ^ 2 ^ (n + floorlog 2 n + 1)"
proof -
have 1: "⋀ψ. ψ ∈ set ys ⟹ card (DCA.nodes (𝔄⇩ν_FG (ψ[set xs]⇩ν))) ≤ 2 ^ 2 ^ Suc n"
proof -
fix ψ
assume "ψ ∈ set ys"

have "card (nested_prop_atoms (G⇩n ψ[set xs]⇩ν))
≤ Suc (card (nested_prop_atoms (ψ[set xs]⇩ν)))"

also have "… ≤ Suc (card (nested_prop_atoms ψ))"

also have "… ≤ Suc n"
by (simp add: assms(2) ‹ψ ∈ set ys›)

finally have 2: "card (nested_prop_atoms (G⇩n ψ[set xs]⇩ν)) ≤ Suc n" .

then show "?thesis ψ"
by (intro le_trans[OF 𝔄⇩ν_FG_nodes_card]) (meson one_le_numeral power_increasing)
qed

have "card (DCA.nodes (𝔄⇩3 xs ys)) ≤ (∏ψ←ys. card (DCA.nodes (𝔄⇩ν_FG (ψ[set xs]⇩ν))))"
unfolding 𝔄⇩3_def using DCA_Combine.intersect_list_nodes_card[OF 𝔄⇩3_nodes_finite_helper]
by (auto simp: comp_def)

also have "… ≤ (2 ^ 2 ^ Suc n) ^ length ys"
by (rule list_prod_const) (rule 1)

also have "… ≤ (2 ^ 2 ^ Suc n) ^ n"

also have "… ≤ 2 ^ (n * 2 ^ Suc n)"
by (metis le_refl mult.commute power_mult)

also have "… ≤ 2 ^ (2 ^ floorlog 2 n * 2 ^ Suc n)"
by (cases ‹n > 0›) (simp_all add: floorlog_bounds less_imp_le_nat)

also have "… = 2 ^ 2 ^ (n + floorlog 2 n + 1)"

finally show ?thesis .
qed

lemma 𝔄⇩1_nodes_finite:
"finite (DCA.nodes (𝔄⇩1 φ xs))"
unfolding 𝔄⇩1_def
by (metis (no_types, lifting) finite_subset ℭ_nodes finite_SigmaI nested_prop_atoms⇩ν_finite nested_prop_atoms_finite)

lemma 𝔄⇩1_nodes_card:
assumes
"card (subfrmlsn φ) ≤ n"
shows
"card (DCA.nodes (𝔄⇩1 φ xs)) ≤ 2 ^ 2 ^ (n + 1)"
proof -
let ?fst = "{Abs ψ | ψ. nested_prop_atoms ψ ⊆ nested_prop_atoms φ}"
let ?snd = "{Abs ψ | ψ. nested_prop_atoms ψ ⊆ nested_prop_atoms⇩ν φ (set xs)}"

have 1: "card (nested_prop_atoms φ) ≤ n"
by (meson card_mono[OF subfrmlsn_finite nested_prop_atoms_subfrmlsn] assms le_trans)

have "card (DCA.nodes (𝔄⇩1 φ xs)) ≤ card (?fst × ?snd)"
unfolding 𝔄⇩1_def
by (rule card_mono) (simp_all add: ℭ_nodes nested_prop_atoms⇩ν_finite nested_prop_atoms_finite)

also have "… = card ?fst * card ?snd"
using nested_prop_atoms⇩ν_finite card_cartesian_product by blast

also have "… ≤ 2 ^ 2 ^ card (nested_prop_atoms φ) * 2 ^ 2 ^ card (nested_prop_atoms φ)"
using nested_prop_atoms⇩ν_card nested_prop_atoms_card mult_le_mono by blast

also have "… = 2 ^ 2 ^ (card (nested_prop_atoms φ) + 1)"

also have "… ≤ 2 ^ 2 ^ (n + 1)"
using assms 1 by simp

finally show ?thesis .
qed

lemma 𝔄'_nodes_finite:
"finite (DRA.nodes (𝔄' φ xs ys))"
unfolding 𝔄'_def
using intersect_nodes_finite intersect_bc_nodes_finite
using 𝔄⇩1_nodes_finite 𝔄⇩2_nodes_finite 𝔄⇩3_nodes_finite
by fast

lemma 𝔄'_nodes_card:
assumes
"length xs ≤ n"
and
"⋀ψ. ψ ∈ set xs ⟹ card (nested_prop_atoms ψ) ≤ n"
and
"length ys ≤ n"
and
"⋀ψ. ψ ∈ set ys ⟹ card (nested_prop_atoms ψ) ≤ n"
and
"card (subfrmlsn φ) ≤ n"
shows
"card (DRA.nodes (𝔄' φ xs ys)) ≤ 2 ^ 2 ^ (n + floorlog 2 n + 4)"
proof -
have "n + 1 ≤ n + floorlog 2 n + 2"
by auto

then have 1: "(2::nat) ^ (n + 1) ≤ 2 ^ (n + floorlog 2 n + 2)"
using one_le_numeral power_increasing by blast

have "card (DRA.nodes (𝔄' φ xs ys)) ≤ card (DCA.nodes (𝔄⇩1 φ xs)) * card (DBA.nodes (𝔄⇩2 xs ys)) * card (DCA.nodes (𝔄⇩3 xs ys))" (is "?lhs ≤ ?rhs")
proof (unfold 𝔄'_def)
have "card (DBA.nodes (𝔄⇩2 xs ys)) * card (DCA.nodes (DCA_Combine.intersect (𝔄⇩1 φ xs) (𝔄⇩3 xs ys))) ≤ ?rhs"
by (simp add: intersect_nodes_card[OF 𝔄⇩1_nodes_finite 𝔄⇩3_nodes_finite])
then show "card (DRA.nodes (intersect_bc (𝔄⇩2 xs ys) (DCA_Combine.intersect (𝔄⇩1 φ xs) (𝔄⇩3 xs ys)))) ≤ ?rhs"
by (meson intersect_bc_nodes_card[OF 𝔄⇩2_nodes_finite intersect_nodes_finite[OF 𝔄⇩1_nodes_finite 𝔄⇩3_nodes_finite]] basic_trans_rules(23))
qed

also have "… ≤ 2 ^ 2 ^ (n + 1) * 2 ^ 2 ^ (n + floorlog 2 n + 2) * 2 ^ 2 ^ (n + floorlog 2 n + 1)"
using 𝔄⇩1_nodes_card[OF assms(5)] 𝔄⇩2_nodes_card[OF assms(1,2)] 𝔄⇩3_nodes_card[OF assms(3,4)]
by (metis mult_le_mono)

also have "… = 2 ^ (2 ^ (n + 1) + 2 ^ (n + floorlog 2 n + 2) + 2 ^ (n + floorlog 2 n + 1))"

also have "… ≤ 2 ^ (4 * 2 ^ (n + floorlog 2 n + 2))"
using 1 by auto

finally show ?thesis
qed

lemma subformula_nested_prop_atoms_subfrmlsn:
"ψ ∈ subfrmlsn φ ⟹ nested_prop_atoms ψ ⊆ subfrmlsn φ"
using nested_prop_atoms_subfrmlsn subfrmlsn_subset by blast

lemma ltl_to_dra_nodes_finite:
"finite (DRA.nodes (ltl_to_dra φ))"
unfolding ltl_to_dra_def
apply (rule DRA_Combine.union_list_nodes_finite)
apply (simp add: list.pred_set split_def 𝔄'_nodes_finite)
done

lemma ltl_to_dra_restricted_nodes_finite:
"finite (DRA.nodes (ltl_to_dra_restricted φ))"
unfolding ltl_to_dra_restricted_def
apply (rule DRA_Combine.union_list_nodes_finite)
apply (simp add: list.pred_set split_def 𝔄'_nodes_finite)
done

lemma ltl_to_dra_alphabet_nodes_finite:
"finite (DRA.nodes (ltl_to_dra_alphabet φ AP))"
using ltl_to_dra_alphabet_nodes ltl_to_dra_restricted_nodes_finite finite_subset by fast

lemma ltl_to_dra_nodes_card:
assumes
"card (subfrmlsn φ) ≤ n"
shows
"card (DRA.nodes (ltl_to_dra φ)) ≤ 2 ^ 2 ^ (2 * n + floorlog 2 n + 4)"
proof -
let ?map = "map (λ(x, y). 𝔄' φ x y) (advice_sets φ)"

have 1: "⋀x::nat. x > 0 ⟹ x ^ length (advice_sets φ) ≤ x ^ 2 ^ card (subfrmlsn φ)"

have "card (DRA.nodes (ltl_to_dra φ)) ≤ prod_list (map (card ∘ DRA.nodes) ?map)"
unfolding ltl_to_dra_def
apply (rule DRA_Combine.union_list_nodes_card)
unfolding list.pred_set using 𝔄'_nodes_finite by auto

also have "… = (∏(x, y)←advice_sets φ. card (DRA.nodes (𝔄' φ x y)))"
by (induction "advice_sets φ") (auto, metis (no_types, lifting) comp_apply split_def)

also have "… ≤ (2 ^ 2 ^ (n + floorlog 2 n + 4)) ^ length (advice_sets φ)"
proof (rule list_prod_const, unfold split_def, rule 𝔄'_nodes_card)
show "⋀x. x ∈ set (advice_sets φ) ⟹ length (fst x) ≤ n"

show "⋀x ψ. ⟦x ∈ set (advice_sets φ); ψ ∈ set (fst x)⟧ ⟹ card (nested_prop_atoms ψ) ≤ n"
by (metis (no_types, lifting) card_mono subfrmlsn_finite subset_iff sup.absorb_iff2 sup.coboundedI1 surjective_pairing)

show "⋀x. x ∈ set (advice_sets φ) ⟹ length (snd x) ≤ n"

show "⋀x ψ. ⟦x ∈ set (advice_sets φ); ψ ∈ set (snd x)⟧ ⟹ card (nested_prop_atoms ψ) ≤ n"
by (metis (no_types, lifting) card_mono subfrmlsn_finite subset_iff sup.absorb_iff2 sup.coboundedI1 surjective_pairing)
qed (insert assms, blast)

also have "… ≤ (2 ^ 2 ^ (n + floorlog 2 n + 4)) ^ (2 ^ card (subfrmlsn φ))"

also have "… ≤ (2 ^ 2 ^ (n + floorlog 2 n + 4)) ^ (2 ^ n)"

also have "… = 2 ^ (2 ^ n * 2 ^ (n + floorlog 2 n + 4))"
by (simp add: ac_simps power_mult [symmetric])

also have "… = 2 ^ 2 ^ (2 * n + floorlog 2 n + 4)"

finally show ?thesis .
qed

text ‹We verify the size bound of the automaton to be double exponential.›

theorem ltl_to_dra_size:
"card (DRA.nodes (ltl_to_dra φ)) ≤ 2 ^ 2 ^ (2 * size φ + floorlog 2 (size φ) + 4)"
using ltl_to_dra_nodes_card subfrmlsn_card by blast

end

end
```