Theory Normal_Form_Complexity

(*
    Author:   Salomon Sickert
    License:  BSD
*)

section ‹Size Bounds›

text ‹We prove an exponential upper bound for the normalisation procedure. Moreover, we show that 
  the number of proper subformulas, which correspond to states very-weak alternating automata 
  (A1W), is only linear for each disjunct.›

theory Normal_Form_Complexity imports
  Normal_Form
begin

subsection ‹Inequalities and Identities›

lemma inequality_1: 
  "y > 0 ⟹ y + 3 ≤ (2 :: nat) ^ (y + 1)"
  by (induction y) (simp, fastforce)

lemma inequality_2: 
  "x > 0 ⟹ y > 0 ⟹ ((2 :: nat) ^ (x + 1)) + (2 ^ (y + 1)) ≤ (2 ^ (x + y + 1))"
  by (induction x; simp; induction y; simp; fastforce)

lemma size_gr_0: 
  "size (φ :: 'a ltln) > 0" 
  by (cases φ) simp_all

lemma sum_associative:
  "finite X ⟹ (∑x ∈ X. f x + c) = (∑x ∈ X. f x) + card X * c"
  by (induction rule: finite_induct) simp_all

subsection ‹Length›

text ‹We prove that the length (size) of the resulting formula in normal form is at most exponential.›

lemma flatten_sigma_1_length: 
  "size (φ[N]Σ1) ≤ size φ"
  by (induction φ) simp_all

lemma flatten_pi_1_length: 
  "size (φ[M]Π1) ≤ size φ"
  by (induction φ) simp_all

lemma flatten_sigma_2_length: 
  "size (φ[M]Σ2) ≤ 2 ^ (size φ + 1)"
proof (induction φ)
  case (And_ltln φ1 φ2)
  hence "size (φ1 andn φ2)[M]Σ2  ≤ (2 ^ (size φ1 + 1)) + (2 ^ (size φ2 + 1)) + 1"
    by simp
  also
  have "… ≤ 2 ^ (size φ1 + size φ2 + 1) + 1 "
    using inequality_2[OF size_gr_0 size_gr_0] by simp
  also
  have "… ≤ 2 ^ (size (φ1 andn φ2) + 1)"
    by simp
  finally
  show ?case.
next
  case (Or_ltln φ1 φ2)
  hence "size (φ1 orn φ2)[M]Σ2  ≤ (2 ^ (size φ1 + 1)) + (2 ^ (size φ2 + 1)) + 1"
    by simp
  also
  have "… ≤ 2 ^ (size φ1 + size φ2 + 1) + 1 "
    using inequality_2[OF size_gr_0 size_gr_0] by simp
  also
  have "… ≤ 2 ^ (size (φ1 orn φ2) + 1)"
    by simp
  finally
  show ?case.
next
  case (Next_ltln φ)
  then show ?case 
    using le_Suc_eq by fastforce
next
  case (WeakUntil_ltln φ1 φ2)
  hence "size (φ1 Wn φ2)[M]Σ2 ≤ 2 ^ (size φ1 + 1) + 2 ^ (size φ2 + 1) + size φ1 + 4"
    by (simp, simp add: add.commute add_mono flatten_pi_1_length)
  also
  have "… ≤ 2 ^ (size φ2 + 1) + 2 * 2 ^ (size φ1 + 1) + 1"
    using inequality_1[OF size_gr_0, of φ1] by simp
  also
  have "… ≤ 2 * (2 ^ (size φ1 + 1) + 2 ^ (size φ2 + 1))"
    by simp
  also
  have "… ≤ 2 * 2 ^ (size φ1 + size φ2 + 1)"
    using inequality_2[OF size_gr_0 size_gr_0] mult_le_mono2 by blast 
  also
  have "… = 2 ^ (size (φ1 Wn φ2) + 1)"
    by simp
  finally
  show ?case.
next
  case (StrongRelease_ltln φ1 φ2)
  hence "size (φ1 Mn φ2)[M]Σ2  ≤ (2 ^ (size φ1 + 1)) + (2 ^ (size φ2 + 1)) + 1"
    by simp
  also
  have "… ≤ 2 ^ (size φ1 + size φ2 + 1) + 1 "
    using inequality_2[OF size_gr_0 size_gr_0] by simp
  also
  have "… ≤ 2 ^ (size (φ1 Mn φ2) + 1)"
    by simp
  finally
  show ?case.
next
  case (Until_ltln φ1 φ2)
  hence "size (φ1 Un φ2)[M]Σ2  ≤ (2 ^ (size φ1 + 1)) + (2 ^ (size φ2 + 1)) + 1"
    by simp
  also
  have "… ≤ 2 ^ (size φ1 + size φ2 + 1) + 1 "
    using inequality_2[OF size_gr_0 size_gr_0] by simp
  also
  have "… ≤ 2 ^ (size (φ1 Un φ2) + 1)"
    by simp
  finally
  show ?case.
next
  case (Release_ltln φ1 φ2)
  hence "size (φ1 Rn φ2)[M]Σ2 ≤ 2 ^ (size φ1 + 1) + 2 ^ (size φ2 + 1) + size φ2 + 4"
    by (simp, simp add: add.commute add_mono flatten_pi_1_length)
  also
  have "… ≤ 2 ^ (size φ1 + 1) + 2 * 2 ^ (size φ2 + 1) + 1"
    using inequality_1[OF size_gr_0, of φ2] by simp
  also
  have "… ≤ 2 * (2 ^ (size φ1 + 1) + 2 ^ (size φ2 + 1))"
    by simp
  also
  have "… ≤ 2 * 2 ^ (size φ1 + size φ2 + 1)"
    using inequality_2[OF size_gr_0 size_gr_0] mult_le_mono2 by blast 
  also
  have "… = 2 ^ (size (φ1 Rn φ2) + 1)"
    by simp
  finally
  show ?case .
qed auto

lemma flatten_pi_2_length: 
  "size (φ[N]Π2) ≤ 2 ^ (size φ + 1)"
proof (induction φ)
  case (And_ltln φ1 φ2)
  hence "size (φ1 andn φ2)[N]Π2  ≤ (2 ^ (size φ1 + 1)) + (2 ^ (size φ2 + 1)) + 1"
    by simp
  also
  have "… ≤ 2 ^ (size φ1 + size φ2 + 1) + 1 "
    using inequality_2[OF size_gr_0 size_gr_0] by simp
  also
  have "… ≤ 2 ^ (size (φ1 andn φ2) + 1)"
    by simp
  finally
  show ?case.
next
  case (Or_ltln φ1 φ2)
  hence "size (φ1 orn φ2)[N]Π2  ≤ (2 ^ (size φ1 + 1)) + (2 ^ (size φ2 + 1)) + 1"
    by simp
  also
  have "… ≤ 2 ^ (size φ1 + size φ2 + 1) + 1 "
    using inequality_2[OF size_gr_0 size_gr_0] by simp
  also
  have "… ≤ 2 ^ (size (φ1 orn φ2) + 1)"
    by simp
  finally
  show ?case.
next
  case (Next_ltln φ)
  then show ?case 
    using le_Suc_eq by fastforce
next
  case (Until_ltln φ1 φ2)
  hence "size (φ1 Un φ2)[N]Π2 ≤ 2 ^ (size φ1 + 1) + 2 ^ (size φ2 + 1) + size φ2 + 4"
    by (simp, simp add: add.commute add_mono flatten_sigma_1_length)
  also
  have "… ≤ 2 ^ (size φ1 + 1) + 2 * 2 ^ (size φ2 + 1) + 1"
    using inequality_1[OF size_gr_0, of φ2] by simp
  also
  have "… ≤ 2 * (2 ^ (size φ1 + 1) + 2 ^ (size φ2 + 1))"
    by simp
  also
  have "… ≤ 2 * 2 ^ (size φ1 + size φ2 + 1)"
    using inequality_2[OF size_gr_0 size_gr_0] mult_le_mono2 by blast 
  also
  have "… = 2 ^ (size (φ1 Un φ2) + 1)"
    by simp
  finally
  show ?case.
next
  case (Release_ltln φ1 φ2)
  hence "size (φ1 Rn φ2)[N]Π2  ≤ (2 ^ (size φ1 + 1)) + (2 ^ (size φ2 + 1)) + 1"
    by simp
  also
  have "… ≤ 2 ^ (size φ1 + size φ2 + 1) + 1 "
    using inequality_2[OF size_gr_0 size_gr_0] by simp
  also
  have "… ≤ 2 ^ (size (φ1 Rn φ2) + 1)"
    by simp
  finally
  show ?case.
next
  case (WeakUntil_ltln φ1 φ2)
  hence "size (φ1 Wn φ2)[N]Π2  ≤ (2 ^ (size φ1 + 1)) + (2 ^ (size φ2 + 1)) + 1"
    by simp
  also
  have "… ≤ 2 ^ (size φ1 + size φ2 + 1) + 1 "
    using inequality_2[OF size_gr_0 size_gr_0] by simp
  also
  have "… ≤ 2 ^ (size (φ1 Wn φ2) + 1)"
    by simp
  finally
  show ?case.
next
  case (StrongRelease_ltln φ1 φ2)
  hence "size (φ1 Mn φ2)[N]Π2 ≤ 2 ^ (size φ1 + 1) + 2 ^ (size φ2 + 1) + size φ1 + 4"
    by (simp, simp add: add.commute add_mono flatten_sigma_1_length)
  also
  have "… ≤ 2 ^ (size φ2 + 1) + 2 * 2 ^ (size φ1 + 1) + 1"
    using inequality_1[OF size_gr_0, of φ1] by simp
  also
  have "… ≤ 2 * (2 ^ (size φ1 + 1) + 2 ^ (size φ2 + 1))"
    by simp
  also
  have "… ≤ 2 * 2 ^ (size φ1 + size φ2 + 1)"
    using inequality_2[OF size_gr_0 size_gr_0] mult_le_mono2 by blast 
  also
  have "… = 2 ^ (size (φ1 Mn φ2) + 1)"
    by simp
  finally
  show ?case .
qed auto

definition "normal_form_length_upper_bound"
  where "normal_form_length_upper_bound φ
    ≡ (2 :: nat) ^ (size φ) * (2 ^ (size φ + 1) + 2 * (size φ + 2) ^ 2)"

definition "normal_form_disjunct_with_flatten_pi_2_length"
  where "normal_form_disjunct_with_flatten_pi_2_length φ M N
    ≡ size (φ[N]Π2) + (∑ψ ∈ M. size (ψ[N]Σ1) + 2) + (∑ψ ∈ N. size (ψ[M]Π1) + 2)" 

definition "normal_form_with_flatten_pi_2_length"
  where "normal_form_with_flatten_pi_2_length φ 
    ≡ ∑(M, N) ∈ {(M, N) | M N. M ⊆ subformulasμ φ ∧ N ⊆ subformulasν φ}. normal_form_disjunct_with_flatten_pi_2_length φ M N"

definition "normal_form_disjunct_with_flatten_sigma_2_length"
  where "normal_form_disjunct_with_flatten_sigma_2_length φ M N 
    ≡ size (φ[M]Σ2) + (∑ψ ∈ M. size (ψ[N]Σ1) + 2) + (∑ψ ∈ N. size (ψ[M]Π1) + 2)" 

definition "normal_form_with_flatten_sigma_2_length"
  where "normal_form_with_flatten_sigma_2_length φ 
    ≡ ∑(M, N) ∈ {(M, N) | M N. M ⊆ subformulasμ φ ∧ N ⊆ subformulasν φ}. normal_form_disjunct_with_flatten_sigma_2_length φ M N"

lemma normal_form_disjunct_length_upper_bound:
  assumes 
    "M ⊆ subformulasμ φ" 
    "N ⊆ subformulasν φ"
  shows 
    "normal_form_disjunct_with_flatten_sigma_2_length φ M N ≤ 2 ^ (size φ + 1) + 2 * (size φ + 2) ^ 2" (is "?thesis1")
    "normal_form_disjunct_with_flatten_pi_2_length φ M N ≤ 2 ^ (size φ + 1) + 2 * (size φ + 2) ^ 2" (is "?thesis2")
proof -
  let ?n = "size φ"
  let ?b = "2 ^ (?n + 1) + ?n * (?n + 2) + ?n * (?n + 2)"

  have finite_M: "finite M" and card_M: "card M ≤ ?n"
    by (metis assms(1) finite_subset subformulasμ_finite)
       (meson assms(1) card_mono order_trans subformulasμ_subfrmlsn subfrmlsn_card subfrmlsn_finite) 

  have finite_N: "finite N" and card_N: "card N ≤ ?n"
    by (metis assms(2) finite_subset subformulasν_finite)
       (meson assms(2) card_mono order_trans subformulasν_subfrmlsn subfrmlsn_card subfrmlsn_finite) 

  have size_M: "⋀ψ. ψ ∈ M ⟹ size ψ ≤ size φ"
    and size_N: "⋀ψ. ψ ∈ N ⟹ size ψ ≤ size φ"
    by (metis assms(1) eq_iff in_mono less_imp_le subformulasμ_subfrmlsn subfrmlsn_size)
       (metis assms(2) eq_iff in_mono less_imp_le subformulasν_subfrmlsn subfrmlsn_size)

  hence size_M': "⋀ψ. ψ ∈ M ⟹ size (ψ[N]Σ1) ≤ size φ"
    and size_N': "⋀ψ. ψ ∈ N ⟹ size (ψ[M]Π1) ≤ size φ"
    using flatten_sigma_1_length flatten_pi_1_length order_trans by blast+

  have "(∑ψ ∈ M. size (ψ[N]Σ1)) ≤ ?n * ?n"
    and "(∑ψ ∈ N. size (ψ[M]Π1)) ≤ ?n * ?n"
    using sum_bounded_above[of M, OF size_M'] sum_bounded_above[of N, OF size_N']
    using mult_le_mono[OF card_M] mult_le_mono[OF card_N] by fastforce+
     
  hence "(∑ψ ∈ M. (size (ψ[N]Σ1) + 2)) ≤ ?n * (?n + 2)"
    and "(∑ψ ∈ N. (size (ψ[M]Π1) + 2)) ≤ ?n * (?n + 2)"
    unfolding sum_associative[OF finite_M] sum_associative[OF finite_N]
    using card_M card_N by simp_all

  hence "normal_form_disjunct_with_flatten_sigma_2_length φ M N ≤ ?b"
    and "normal_form_disjunct_with_flatten_pi_2_length φ M N ≤ ?b"
    unfolding normal_form_disjunct_with_flatten_sigma_2_length_def normal_form_disjunct_with_flatten_pi_2_length_def 
    by (metis (no_types, lifting) flatten_sigma_2_length flatten_pi_2_length add_le_mono)+

  thus ?thesis1 and ?thesis2
    by (simp_all add: power2_eq_square)
qed

theorem normal_form_length_upper_bound:
  "normal_form_with_flatten_sigma_2_length φ ≤ normal_form_length_upper_bound φ" (is "?thesis1")
  "normal_form_with_flatten_pi_2_length φ ≤ normal_form_length_upper_bound φ" (is "?thesis2")
proof -
  let ?n = "size φ"
  let ?b = "2 ^ (size φ + 1) + 2 * (size φ + 2) ^ 2"

  have "{(M, N) | M N. M ⊆ subformulasμ φ ∧ N ⊆ subformulasν φ} = {M. M ⊆ subformulasμ φ} × {N. N ⊆ subformulasν φ}" (is "?choices = _")
    by simp
  
  moreover
  
  have "card {M. M ⊆ subformulasμ φ} = (2 :: nat) ^ (card (subformulasμ φ))"
    and "card {N. N ⊆ subformulasν φ} = (2 :: nat) ^ (card (subformulasν φ))"
    using card_Pow unfolding Pow_def using subformulasμ_finite subformulasν_finite by auto
  
  ultimately
  
  have "card ?choices ≤ 2 ^ (card (subfrmlsn φ))" (is "?f ≤ _")
    by (metis subformulasμν_card card_cartesian_product subformulasμν_subfrmlsn subfrmlsn_finite Suc_1 card_mono lessI power_add power_increasing_iff)
  
  moreover
  
  have "(2 :: nat) ^ (card (subfrmlsn φ)) ≤ 2 ^ ?n"
    using power_increasing[of _ _ "2 :: nat"] by (simp add: subfrmlsn_card)
  
  ultimately
  
  have bar: "of_nat (card ?choices) ≤ (2 :: nat) ^ ?n"
    using of_nat_id by presburger

  moreover

  have "normal_form_with_flatten_sigma_2_length φ ≤ of_nat (card ?choices) * ?b"
    unfolding normal_form_with_flatten_sigma_2_length_def
    by (rule sum_bounded_above) (insert normal_form_disjunct_length_upper_bound, auto)

  moreover

  have "normal_form_with_flatten_pi_2_length φ ≤ of_nat (card ?choices) * ?b"
    unfolding normal_form_with_flatten_pi_2_length_def
    by (rule sum_bounded_above) (insert normal_form_disjunct_length_upper_bound, auto)

  ultimately

  show ?thesis1 and ?thesis2
    unfolding normal_form_length_upper_bound_def 
    using mult_le_mono1 order_trans by blast+
qed

subsection ‹Proper Subformulas›

text ‹We prove that the number of (proper) subformulas (sf) in a disjunct is linear and not exponential.›

fun sf :: "'a ltln ⇒ 'a ltln set"
where
  "sf (φ andn ψ) = sf φ ∪ sf ψ"
| "sf (φ orn ψ) = sf φ ∪ sf ψ"
| "sf (Xn φ) = {Xn φ} ∪ sf φ"
| "sf (φ Un ψ) = {φ Un ψ} ∪ sf φ ∪ sf ψ"
| "sf (φ Rn ψ) = {φ Rn ψ} ∪ sf φ ∪ sf ψ"
| "sf (φ Wn ψ) = {φ Wn ψ} ∪ sf φ ∪ sf ψ"
| "sf (φ Mn ψ) = {φ Mn ψ} ∪ sf φ ∪ sf ψ"
| "sf φ = {}"

lemma sf_finite: 
  "finite (sf φ)"
  by (induction φ) auto

lemma sf_subset_subfrmlsn: 
  "sf φ ⊆ subfrmlsn φ"
  by (induction φ) auto

lemma sf_size:
  "ψ ∈ sf φ ⟹ size ψ ≤ size φ"
  by (induction φ) auto

lemma sf_sf_subset: 
  "ψ ∈ sf φ ⟹ sf ψ ⊆ sf φ"
  by (induction φ) auto

lemma subfrmlsn_sf_subset: 
  "ψ ∈ subfrmlsn φ ⟹ sf ψ ⊆ sf φ"
  by (induction φ) auto

lemma sf_subset_insert:
  assumes "sf φ ⊆ insert φ X"
  assumes "ψ ∈ subfrmlsn φ"
  assumes "φ ≠ ψ" 
  shows "sf ψ ⊆ X" 
proof -
  have "sf ψ ⊆ sf φ - {φ}"
    using assms(2,3) subfrmlsn_sf_subset sf_size subfrmlsn_size by fastforce
  thus "?thesis"
    using assms(1) by auto
qed

lemma flatten_pi_1_sf_subset: 
  "sf (φ[M]Π1) ⊆ (⋃φ∈sf φ. sf (φ[M]Π1))"
  by (induction φ) auto

lemma flatten_sigma_1_sf_subset: 
  "sf (φ[M]Σ1) ⊆ (⋃φ∈sf φ. sf (φ[M]Σ1))"
  by (induction φ) auto

lemma flatten_sigma_2_sf_subset: 
  "sf (φ[M]Σ2) ⊆ (⋃ψ∈sf φ. sf (ψ[M]Σ2))"
  by (induction φ) auto

lemma sf_set1: 
  "sf (φ[M]Σ2) ∪ sf (φ[M]Π1) ⊆ (⋃ψ ∈ (sf φ). (sf (ψ[M]Σ2) ∪ sf (ψ[M]Π1)))"
  by (induction φ) auto

(* TODO: could be moved *)
lemma ltln_not_idempotent [simp]:
  "φ andn ψ ≠ φ" "ψ andn φ ≠ φ" "φ ≠ φ andn ψ" "φ ≠ ψ andn φ"
  "φ orn ψ ≠ φ" "ψ orn φ ≠ φ" "φ ≠ φ orn ψ" "φ ≠ ψ orn φ"
  "Xn φ ≠ φ" "φ ≠ Xn φ"
  "φ Un ψ ≠ φ" "φ ≠ φ Un ψ" "ψ Un φ ≠ φ" "φ ≠ ψ Un φ"
  "φ Rn ψ ≠ φ" "φ ≠ φ Rn ψ" "ψ Rn φ ≠ φ" "φ ≠ ψ Rn φ"
  "φ Wn ψ ≠ φ" "φ ≠ φ Wn ψ" "ψ Wn φ ≠ φ" "φ ≠ ψ Wn φ"
  "φ Mn ψ ≠ φ" "φ ≠ φ Mn ψ" "ψ Mn φ ≠ φ" "φ ≠ ψ Mn φ"
  by (induction φ; force)+

lemma flatten_card_sf_induct:
  assumes "finite X"
  assumes "⋀x. x ∈ X ⟹ sf x ⊆ X"
  shows "card (⋃φ∈X. sf (φ[N]Σ1)) ≤ card X 
   ∧ card (⋃φ∈X. sf (φ[M]Π1)) ≤ card X 
   ∧ card (⋃φ∈X. sf (φ[M]Σ2) ∪ sf (φ[M]Π1)) ≤ 3 * card X"
  using assms(2)
proof (induction rule: finite_ranking_induct[where f = size, OF ‹finite X›])
  case (2 ψ X)
    {
      assume "ψ ∉ X"
      hence "⋀χ. χ ∈ X ⟹ sf χ ⊆ X"
        using 2(2,4) sf_subset_subfrmlsn subfrmlsn_size by fastforce
      hence "card (⋃φ∈X. sf (φ[N]Σ1)) ≤ card X"
        and "card (⋃φ∈X. sf (φ[M]Π1)) ≤ card X"        
        and "card (⋃φ∈X. sf (φ[M]Σ2) ∪ sf (φ[M]Π1)) ≤ 3 * card X"
        using 2(3) by simp+
      
      moreover

      let ?lower1 = "⋃φ ∈ insert ψ X. sf (φ[N]Σ1)"
      let ?upper1 = "(⋃φ ∈ X. sf (φ[N]Σ1)) ∪ {ψ[N]Σ1}"

      let ?lower2 = "⋃φ ∈ insert ψ X. sf (φ[M]Π1)"
      let ?upper2 = "(⋃φ ∈ X. sf (φ[M]Π1)) ∪ {ψ[M]Π1}"

      let ?lower3 = "⋃φ ∈ insert ψ X. sf (φ[M]Σ2) ∪ sf (φ[M]Π1)"
      let ?upper3_cases = "{ψ[M]Σ2, ψ[M]Π1} ∪ (case ψ of (φ1 Wn φ2) ⇒ {Gn (φ1[M]Π1)} | (φ1 Rn φ2) ⇒ {Gn (φ2[M]Π1)} | _ ⇒ {})"
      let ?upper3 = "(⋃φ ∈ X. sf (φ[M]Σ2) ∪ sf (φ[M]Π1)) ∪ ?upper3_cases"

      have finite_upper1: "finite (?upper1)"
        and finite_upper2: "finite (?upper2)" 
        and finite_upper3: "finite (?upper3)" 
        using 2(1) sf_finite by auto (cases ψ, auto)

      have "⋀x y. card {x, y} ≤ 3"
        and "⋀x y z. card {x, y, z} ≤ 3"
        by (simp add: card_insert_if le_less)+
      hence card_leq_3: "card (?upper3_cases) ≤ 3"
        by (cases ψ) (simp_all, fast)

      note card_subset_split_rule = le_trans[OF card_mono card_Un_le]

      have sf_in_X: "sf ψ ⊆ insert ψ X"
        using 2 by blast

      have "?lower1 ⊆ ?upper1 ∧ ?lower2 ⊆ ?upper2 ∧ ?lower3 ⊆ ?upper3" 
      proof (cases ψ)
        case (And_ltln ψ1 ψ2)
        have *: "sf ψ1 ⊆ X" "sf ψ2 ⊆ X" 
          by (rule sf_subset_insert[OF sf_in_X, unfolded And_ltln]; simp)+

        have "(sf (ψ[M]Σ2)) ⊆ (⋃φ ∈ X. sf (φ[M]Σ2))"
          and "(sf (ψ[M]Π1)) ⊆ (⋃φ ∈ X. sf (φ[M]Π1))"
          and "(sf (ψ[N]Σ1)) ⊆ (⋃φ ∈ X. sf (φ[N]Σ1))"
          subgoal
            using flatten_sigma_2_sf_subset[of _ M] * by (force simp: And_ltln)
          subgoal
            using flatten_pi_1_sf_subset[of _ M] * by (force simp: And_ltln)
          subgoal 
            using flatten_sigma_1_sf_subset * by (force simp: And_ltln)
          done
        
        thus ?thesis 
          by blast
      next
        case (Or_ltln ψ1 ψ2)
        have *: "sf ψ1 ⊆ X" "sf ψ2 ⊆ X"
          by (rule sf_subset_insert[OF sf_in_X, unfolded Or_ltln]; simp)+

        have "(sf (ψ[M]Σ2)) ⊆ (⋃φ ∈ X. sf (φ[M]Σ2))"
          and "(sf (ψ[M]Π1)) ⊆ (⋃φ ∈ X. sf (φ[M]Π1))"
          and "(sf (ψ[N]Σ1)) ⊆ (⋃φ ∈ X. sf (φ[N]Σ1))"
          subgoal
            using flatten_sigma_2_sf_subset[of _ M] * by (force simp: Or_ltln)
          subgoal
            using flatten_pi_1_sf_subset[of _ M] * by (force simp: Or_ltln)
          subgoal 
            using flatten_sigma_1_sf_subset * by (force simp: Or_ltln)
          done
          
        thus ?thesis 
          by blast
      next
        case (Next_ltln ψ1)
        have *: "sf ψ1 ⊆ X" 
          by (rule sf_subset_insert[OF sf_in_X, unfolded Next_ltln]) simp_all
  
        have "(sf (ψ[M]Σ2)) ⊆ (⋃φ ∈ X. sf (φ[M]Σ2)) ∪ {ψ[M]Σ2}"
          and "(sf (ψ[M]Π1)) ⊆ (⋃φ ∈ X. sf (φ[M]Π1)) ∪ {ψ[M]Π1}"
          and "(sf (ψ[N]Σ1)) ⊆ (⋃φ ∈ X. sf (φ[N]Σ1)) ∪ {ψ[N]Σ1}"
          subgoal
            using flatten_sigma_2_sf_subset[of _ M] * by (force simp: Next_ltln)
          subgoal
            using flatten_pi_1_sf_subset[of _ M] * by (force simp: Next_ltln)
          subgoal 
            using flatten_sigma_1_sf_subset * by (force simp: Next_ltln)
          done
        
        thus ?thesis
          by blast
      next
        case (Until_ltln ψ1 ψ2)
        have *: "sf ψ1 ⊆ X" "sf ψ2 ⊆ X"
          by (rule sf_subset_insert[OF sf_in_X, unfolded Until_ltln]; simp)+
  
        hence "(sf (ψ[M]Σ2)) ⊆ (⋃φ ∈ X. sf (φ[M]Σ2)) ∪ {ψ[M]Σ2}"
          and "(sf (ψ[M]Π1)) ⊆ (⋃φ ∈ X. sf (φ[M]Π1)) ∪ {ψ[M]Π1}"
          and "(sf (ψ[N]Σ1)) ⊆ (⋃φ ∈ X. sf (φ[N]Σ1)) ∪ {ψ[N]Σ1}"
          subgoal
            using flatten_sigma_2_sf_subset[of _ M] * by (force simp: Until_ltln)
          subgoal
            using flatten_pi_1_sf_subset[of _ M] * by (force simp: Until_ltln)
          subgoal 
            using flatten_sigma_1_sf_subset * by (force simp: Until_ltln)
          done
  
        thus ?thesis
          by blast
      next
        case (Release_ltln ψ1 ψ2)
        have *: "sf ψ1 ⊆ X" "sf ψ2 ⊆ X"
          by (rule sf_subset_insert[OF sf_in_X, unfolded Release_ltln]; simp)+
  
        have "(sf (ψ[M]Σ2)) ⊆ (⋃φ ∈ X. sf (φ[M]Σ2)) ∪ {ψ[M]Σ2, Gn ψ2[M]Π1} ∪ sf (ψ2[M]Π1)"
          and "(sf (ψ[M]Π1)) ⊆ (⋃φ ∈ X. sf (φ[M]Π1)) ∪ {ψ[M]Π1}"
          and "(sf (ψ[N]Σ1)) ⊆ (⋃φ ∈ X. sf (φ[N]Σ1)) ∪ {ψ[N]Σ1}"
          subgoal
            using flatten_sigma_2_sf_subset[of _ M] * by (force simp: Release_ltln)
          subgoal
            using flatten_pi_1_sf_subset[of _ M] * by (force simp: Release_ltln)
          subgoal 
            using flatten_sigma_1_sf_subset * by (force simp: Release_ltln)
          done
  
        moreover 
        have "sf (ψ2[M]Π1) ⊆ (⋃φ∈X. sf φ[M]Σ2 ∪ sf (φ[M]Π1)) ∪ {ψ[M]Π1}" 
          using ‹(sf (ψ[M]Π1)) ⊆ (⋃φ ∈ X. sf (φ[M]Π1)) ∪ {ψ[M]Π1}› 
          by (auto simp: Release_ltln)
          
        ultimately
        show ?thesis
          by (simp add: Release_ltln) blast 
      next
        case (WeakUntil_ltln ψ1 ψ2)
        have *: "sf ψ1 ⊆ X" "sf ψ2 ⊆ X"
          by (rule sf_subset_insert[OF sf_in_X, unfolded WeakUntil_ltln]; simp)+
  
        have "(sf (ψ[M]Σ2)) ⊆ (⋃φ ∈ X. sf (φ[M]Σ2)) ∪ {ψ[M]Σ2, Gn ψ1[M]Π1} ∪ sf (ψ1[M]Π1)"
          and "(sf (ψ[M]Π1)) ⊆ (⋃φ ∈ X. sf (φ[M]Π1)) ∪ {ψ[M]Π1}"
          and "(sf (ψ[N]Σ1)) ⊆ (⋃φ ∈ X. sf (φ[N]Σ1)) ∪ {ψ[N]Σ1}"
          subgoal
            using flatten_sigma_2_sf_subset[of _ M] * by (force simp: WeakUntil_ltln)
          subgoal
            using flatten_pi_1_sf_subset[of _ M] * by (force simp: WeakUntil_ltln)
          subgoal 
            using flatten_sigma_1_sf_subset * by (force simp: WeakUntil_ltln)
          done
  
        moreover 
        have "sf (ψ1[M]Π1) ⊆ (⋃φ∈X. sf φ[M]Σ2 ∪ sf (φ[M]Π1)) ∪ {ψ[M]Π1}" 
          using ‹(sf (ψ[M]Π1)) ⊆ (⋃φ ∈ X. sf (φ[M]Π1)) ∪ {ψ[M]Π1}› 
          by (auto simp: WeakUntil_ltln)
          
        ultimately
        show ?thesis
          by (simp add: WeakUntil_ltln) blast 
      next 
        case (StrongRelease_ltln ψ1 ψ2)
        have *: "sf ψ1 ⊆ X" "sf ψ2 ⊆ X"
          by (rule sf_subset_insert[OF sf_in_X, unfolded StrongRelease_ltln]; simp)+
          
        hence "(sf (ψ[M]Σ2)) ⊆ (⋃φ ∈ X. sf (φ[M]Σ2)) ∪ {ψ[M]Σ2}"
          and "(sf (ψ[M]Π1)) ⊆ (⋃φ ∈ X. sf (φ[M]Π1)) ∪ {ψ[M]Π1}"
          and "(sf (ψ[N]Σ1)) ⊆ (⋃φ ∈ X. sf (φ[N]Σ1)) ∪ {ψ[N]Σ1}"
          subgoal
            using flatten_sigma_2_sf_subset[of _ M] * by (force simp: StrongRelease_ltln)
          subgoal
            using flatten_pi_1_sf_subset[of _ M] * by (force simp: StrongRelease_ltln)
          subgoal 
            using flatten_sigma_1_sf_subset * by (force simp: StrongRelease_ltln)
          done
          
        thus ?thesis 
          by blast
      qed auto

      hence "card ?lower1 ≤ card (⋃φ ∈ X. sf (φ[N]Σ1)) + 1"
        and "card ?lower2 ≤ card (⋃φ ∈ X. sf (φ[M]Π1)) + 1"
        and "card ?lower3 ≤ card (⋃φ ∈ X. sf (φ[M]Σ2) ∪ sf (φ[M]Π1)) + 3" 
        using card_subset_split_rule[OF finite_upper1, of ?lower1] 
        using card_subset_split_rule[OF finite_upper2, of ?lower2]
        using card_subset_split_rule[OF finite_upper3, of ?lower3]
        using card_leq_3 by simp+
  
      moreover
      have "card (insert ψ X) = card X + 1"
        using ‹ψ ∉ X› ‹finite X› by simp
      ultimately
      have ?case
        by linarith
    }
  moreover
  have "ψ ∈ X ⟹ ?case"
    using 2 by (simp add: insert_absorb)
  ultimately
  show ?case 
    by meson
qed simp
      
theorem flatten_card_sf: 
  "card (⋃ψ ∈ sf φ. sf (ψ[M]Σ1)) ≤ card (sf φ)" (is "?t1") 
  "card (⋃ψ ∈ sf φ. sf (ψ[M]Π1)) ≤ card (sf φ)" (is "?t2")
  "card (sf (φ[M]Σ2) ∪ sf (φ[M]Π1)) ≤ 3 * card (sf φ)" (is "?t3")
proof -
  have "card (⋃ψ ∈ sf φ. sf ψ[M]Σ2 ∪ sf (ψ[M]Π1)) ≤ 3 * card (sf φ)"
    using flatten_card_sf_induct[OF sf_finite sf_sf_subset] by auto
  moreover
  have "card (sf φ[M]Σ2 ∪ sf (φ[M]Π1)) ≤ card (⋃ψ ∈ sf φ. sf ψ[M]Σ2 ∪ sf (ψ[M]Π1))"
    using card_mono[OF _ sf_set1] sf_finite by blast
  ultimately
  show ?t1 ?t2 ?t3
    using flatten_card_sf_induct[OF sf_finite sf_sf_subset] by auto
qed

corollary flatten_sigma_2_card_sf: 
  "card (sf (φ[M]Σ2)) ≤ 3 * (card (sf φ))"
  by (metis sf_finite order.trans[OF _ flatten_card_sf(3), of "card (sf (φ[M]Σ2))", OF card_mono] finite_UnI Un_upper1)

end