Theory DRA_Construction

(*
    Author:   Benedikt Seidl
    License:  BSD
*)

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 truen_lifted :: "'ltlq" ("↑truen") where
  "↑truen ≡ Abs truen"

abbreviation falsen_lifted :: "'ltlq" ("↑falsen") where
  "↑falsen ≡ Abs falsen"

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_letterF_lifted :: "'a ltln ⇒ 'a set ⇒ 'ltlq ⇒ 'ltlq" ("↑afletterF")
where
  "↑afletterF φ ν ψ ≡ Abs (af_letterF φ (Rep ψ) ν)"

definition af_letterG_lifted :: "'a ltln ⇒ 'a set ⇒ 'ltlq ⇒ 'ltlq" ("↑afletterG")
where
  "↑afletterG φ ν ψ ≡ Abs (af_letterG φ (Rep ψ) ν)"

lemma af_letterF_lifted_semantics:
  "↑afletterF φ ν (Abs ψ) = Abs (af_letterF φ ψ ν)"
  by (metis af_letterF_lifted_def Rep_inverse af_letterF_def af_letter_congruent Abs_eq)

lemma af_letterG_lifted_semantics:
  "↑afletterG φ ν (Abs ψ) = Abs (af_letterG φ ψ ν)"
  by (metis af_letterG_lifted_def Rep_inverse af_letterG_def af_letter_congruent Abs_eq)

abbreviation afF_lifted :: "'a ltln ⇒ 'ltlq ⇒ 'a set list ⇒ 'ltlq" ("↑afF")
where
  "↑afF φ ψ w ≡ fold (↑afletterF φ) w ψ"

abbreviation afG_lifted :: "'a ltln ⇒ 'ltlq ⇒ 'a set list ⇒ 'ltlq" ("↑afG")
where
  "↑afG φ ψ w ≡ fold (↑afletterG φ) w ψ"

lemma afF_lifted_semantics:
  "↑afF φ (Abs ψ) w = Abs (afF φ ψ w)"
  by (induction w rule: rev_induct) (auto simp: af_letterF_lifted_semantics)

lemma afG_lifted_semantics:
  "↑afG φ (Abs ψ) w = Abs (afG φ ψ w)"
  by (induction w rule: rev_induct) (auto simp: af_letterG_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 (λψ. ψ = ↑truen)"

definition 𝔄μ_GF :: "'a ltln ⇒ ('a set, 'ltlq) dba" where
  "𝔄μ_GF φ = dba UNIV (Abs (Fn φ)) (↑afletterF φ) (λψ. ψ = ↑truen)"

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

definition 𝔄ν_FG :: "'a ltln ⇒ ('a set, 'ltlq) dca" where
  "𝔄ν_FG φ = dca UNIV (Abs (Gn φ)) (↑afletterG φ) (λψ. ψ = ↑falsen)"


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]) ∼ truen)"
    by (meson af_μLTL af_prefix_true le_cases)

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

  also have "… ⟷ infs (λψ. ψ = ↑truen) (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 Gn (Fn φ)"
proof -
  assume "φ ∈ μLTL"

  then have "w ⊨n Gn (Fn φ) ⟷ (∀n. ∃k. af (Fn φ) (w[n → k]) ∼L truen)"
    using ltl_lang_equivalence.af_μLTL_GF by blast

  also have "… ⟷ (∀n. ∃k>n. afF φ (Fn φ) (w[0 → k]) ∼ truen)"
    using afF_semantics_ltr afF_semantics_rtl
    using ‹φ ∈ μLTL› af_μLTL_GF calculation by blast

  also have "… ⟷ (∀n. ∃k≥n. afF φ (Fn φ) (w[0 → Suc k]) ∼ truen)"
    by (metis less_Suc_eq_le less_imp_Suc_add)

  also have "… ⟷ infs (λψ. ψ = ↑truen) (DBA.trace (𝔄μ_GF φ) (to_stream w) (Abs (Fn φ)))"
    by (simp add: infs_snth 𝔄μ_GF_def DBA.transition_def afF_lifted_semantics Abs_eq[symmetric] af_letterF_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]) ∼ falsen)"
    by (meson af_νLTL af_prefix_false le_cases order_refl)

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

  also have "… ⟷ fins (λψ. ψ = ↑falsen) (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 Fn (Gn φ)"
proof -
  assume "φ ∈ νLTL"

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

  also have "… ⟷ (∃n. ∀k>n. ¬ afG φ (Gn φ) (w[0 → k]) ∼ falsen)"
    using afG_semantics_ltr afG_semantics_rtl
    using ‹φ ∈ νLTL› af_νLTL_FG calculation by blast

  also have "… ⟷ (∃n. ∀k≥n. ¬ afG φ (Gn φ) (w[0 → Suc k]) ∼ falsen)"
    by (metis less_Suc_eq_le less_imp_Suc_add)

  also have "… ⟷ fins (λψ. ψ = ↑falsen) (DCA.trace (𝔄ν_FG φ) (to_stream w) (Abs (Gn φ)))"
    by (simp add: infs_snth 𝔄ν_FG_def DBA.transition_def afG_lifted_semantics Abs_eq[symmetric] af_letterG_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 = ↑falsen)"

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)) ∼ falsen)"
    using afν_semantics_ltr afν_semantics_rtl by blast

  also have "… ⟷ fins (λp. snd p = ↑falsen) (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) = L1 φ (set xs)"
  by (simp add: 𝔄1_def L1_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) = L2 (set xs) (set ys)"
  by (simp add: 𝔄2_def L2_def set_eq_iff dba_language[OF 𝔄μ_GF_language[OF FG_advice_μLTL(1)]])

lemma 𝔄2_alphabet:
  "DBA.alphabet (𝔄2 xs ys) = UNIV"
  by (simp add: 𝔄2_def 𝔄μ_GF_def)


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) = L3 (set xs) (set ys)"
  by (simp add: 𝔄3_def L3_def set_eq_iff dca_language[OF 𝔄ν_FG_language[OF GF_advice_νLTL(1)]])

lemma 𝔄3_alphabet:
  "DCA.alphabet (𝔄3 xs ys) = UNIV"
  by (simp add: 𝔄3_def 𝔄ν_FG_def)


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

lemma 𝔄'_language:
  "to_omega ` DRA.language (𝔄' φ xs ys) = (L1 φ (set xs) ∩ L2 (set xs) (set ys) ∩ L3 (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))"
    using advice_sets_not_empty by (simp add: 𝔄'_alphabet)
  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 φ)))"
    by (simp add: split_def)
  have "language_ltln φ = ⋃ {(L1 φ X ∩ L2 X Y ∩ L3 X Y) | X Y. X ⊆ subformulasμ φ ∧ Y ⊆ subformulasν φ}"
    unfolding master_theorem_language by auto
  also have "… = ⋃ {L1 φ (set xs) ∩ L2 (set xs) (set ys) ∩ L3 (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 φ)}"
    by (simp add: 𝔄'_language)
  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))"
    using restricted_advice_sets_not_empty by (simp add: 𝔄'_alphabet)
  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 φ)))"
    by (simp add: split_def)
  have "language_ltln φ = ⋃ {(L1 φ X ∩ L2 X Y ∩ L3 X Y) | X Y. X ⊆ subformulasμ φ ∩ restricted_subformulas φ ∧ Y ⊆ subformulasν φ ∩ restricted_subformulas φ}"
    unfolding master_theorem_restricted_language by auto
  also have "… = ⋃ {L1 φ (set xs) ∩ L2 (set xs) (set ys) ∩ L3 (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 φ)}"
    by (simp add: 𝔄'_language)
  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 afF_lifted_range:
  "nested_prop_atoms ψ ⊆ nested_prop_atoms (Fn φ) ⟹ range (↑afF φ (Abs ψ)) ⊆  {Abs ψ | ψ. nested_prop_atoms ψ ⊆ nested_prop_atoms (Fn φ)}"
  using afF_lifted_semantics afF_nested_prop_atoms by blast

lemma afG_lifted_range:
  "nested_prop_atoms ψ ⊆ nested_prop_atoms (Gn φ) ⟹ range (↑afG φ (Abs ψ)) ⊆  {Abs ψ | ψ. nested_prop_atoms ψ ⊆ nested_prop_atoms (Gn φ)}"
  using afG_lifted_semantics afG_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 (Fn φ)}"
  unfolding 𝔄μ_GF_def dba.nodes_alt_def dba.reachable_alt_def
  using afF_nested_prop_atoms[of "Fn φ"] by (auto simp: afF_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 (Gn φ)}"
  unfolding 𝔄ν_FG_def dca.nodes_alt_def dca.reachable_alt_def
  using afG_nested_prop_atoms[of "Gn φ"] by (auto simp: afG_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}"
    by (simp add: nested_prop_atomsν_finite Advice.nested_prop_atomsν_finite equiv_finite)

  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)"
    using equiv_card[OF Advice.nested_prop_atomsν_finite] by fast

  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 (Fn φ))"
  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 (Gn φ))"
  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 (Fn ψ[set ys]μ)) ≤ Suc n"
  proof -
    fix ψ
    assume "ψ ∈ set xs"

    have "card (nested_prop_atoms (Fn (ψ[set ys]μ)))
          ≤ Suc (card (nested_prop_atoms (ψ[set ys]μ)))"
      by (simp add: card_insert_Suc)

    also have "… ≤ Suc (card (nested_prop_atoms ψ))"
      by (simp add: FG_advice_nested_prop_atoms_card)

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

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

  have "(∏ψ←xs. card (DBA.nodes (𝔄μ_GF (ψ[set ys]μ))))
        ≤ (∏ψ←xs. 2 ^ 2 ^ card (nested_prop_atoms (Fn (ψ[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)"
    by (simp add: power_add)

  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))"
    by (simp add: power_add)

  also have "… ≤ 2 ^ (n + 2 ^ (Suc n + floorlog 2 n))"
    by (simp add: floorlog_le_const)

  also have "… ≤ 2 ^ 2 ^ (n + floorlog 2 n + 2)"
    by simp (metis const_less_power Suc_1 add_Suc_right add_leE lessI less_imp_le_nat power_Suc)

  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 (Gn ψ[set xs]ν))
          ≤ Suc (card (nested_prop_atoms (ψ[set xs]ν)))"
      by (simp add: card_insert_Suc)

    also have "… ≤ Suc (card (nested_prop_atoms ψ))"
      by (simp add: GF_advice_nested_prop_atoms_card)

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

    finally have 2: "card (nested_prop_atoms (Gn ψ[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"
    by (simp add: assms(1) power_increasing)

  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)"
    by (simp add: power_add)

  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)"
    by (simp add: semiring_normalization_rules(36))

  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))"
    by (metis power_add)

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

  finally show ?thesis
    by (simp add: numeral.simps(2) power_add)
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: split_def 𝔄'_alphabet advice_sets_not_empty)
  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: split_def 𝔄'_alphabet advice_sets_not_empty)
  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 φ)"
    by (metis advice_sets_length linorder_not_less nat_power_less_imp_less)

  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"
      using advice_sets_element_length assms by fastforce

    show "⋀x ψ. ⟦x ∈ set (advice_sets φ); ψ ∈ set (fst x)⟧ ⟹ card (nested_prop_atoms ψ) ≤ n"
      using advice_sets_element_subfrmlsn(1) assms subformula_nested_prop_atoms_subfrmlsn subformulasμ_subfrmlsn
      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"
      using advice_sets_element_length assms by fastforce

    show "⋀x ψ. ⟦x ∈ set (advice_sets φ); ψ ∈ set (snd x)⟧ ⟹ card (nested_prop_atoms ψ) ≤ n"
      using advice_sets_element_subfrmlsn(2) assms subformula_nested_prop_atoms_subfrmlsn subformulasν_subfrmlsn
      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 φ))"
    by (simp add: 1)

  also have "… ≤ (2 ^ 2 ^ (n + floorlog 2 n + 4)) ^ (2 ^ n)"
    by (simp add: assms power_increasing)

  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)"
    by (simp add: power_add) (simp add: mult_2 power_add)

  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