Theory Normal_Form

(*
    Author:   Salomon Sickert
    License:  BSD
*)

section ‹A Normal Form for Linear Temporal Logic›

theory Normal_Form imports
  LTL_Master_Theorem.Master_Theorem
begin

subsection ‹LTL Equivalences›

text ‹Several valid laws of LTL relating strong and weak operators that are useful later.›

lemma ltln_strong_weak_2:
  "w ⊨n φ Un ψ ⟷ w ⊨n (φ andn Fn ψ) Wn ψ" (is "?thesis1")
  "w ⊨n φ Mn ψ ⟷ w ⊨n φ Rn (ψ andn Fn φ)" (is "?thesis2")
proof -
  have "∃j. suffix (i + j) w ⊨n ψ"
    if "suffix j w ⊨n ψ" and "∀j≤i. ¬ suffix j w ⊨n ψ" for i j
  proof
    from that have "j > i"
      by (cases "j > i") auto
    thus "suffix (i + (j - i)) w ⊨n ψ"
      using that by auto
  qed
  thus ?thesis1
    unfolding ltln_strong_weak by auto
next 
  have "∃j. suffix (i + j) w ⊨n φ"
    if "suffix j w ⊨n φ" and "∀j<i. ¬ suffix j w ⊨n φ" for i j
  proof
    from that have "j ≥ i"
      by (cases "j ≥ i") auto
    thus "suffix (i + (j - i)) w ⊨n φ"
      using that by auto
  qed
  thus ?thesis2
    unfolding ltln_strong_weak by auto
qed

lemma ltln_weak_strong_2:
  "w ⊨n φ Wn ψ ⟷ w ⊨n φ Un (ψ orn Gn φ)" (is "?thesis1")
  "w ⊨n φ Rn ψ ⟷ w ⊨n (φ orn Gn ψ) Mn ψ" (is "?thesis2")
proof -
  have "suffix j w ⊨n φ"
    if "⋀j. j < i ⟹ suffix j w ⊨n φ" and "⋀j. suffix (i + j) w ⊨n φ" for i j
    using that(1)[of j] that(2)[of "j - i"] by (cases "j < i") simp_all
  thus ?thesis1
    unfolding ltln_weak_strong unfolding semantics_ltln.simps suffix_suffix by blast
next
  have "suffix j w ⊨n ψ"
    if "⋀j. j ≤ i ⟹ suffix j w ⊨n ψ" and "⋀j. suffix (i + j) w ⊨n ψ" for i j
    using that(1)[of j] that(2)[of "j - i"] by (cases "j ≤ i") simp_all
  thus ?thesis2
    unfolding ltln_weak_strong unfolding semantics_ltln.simps suffix_suffix by blast
qed

subsection ‹$\evalnu{\psi}{M}$, $\evalmu{\psi}{N}$, $\flatten{\psi}{M}$, and $\flattentwo{\psi}{N}$›

text ‹The following four functions use "promise sets", named $M$ or $N$, to rewrite arbitrary 
  formulas into formulas from the class $\Sigma_1$-, $\Sigma_2$-, $\Pi_1$-, and $\Pi_2$, 
  respectively. In general the obtained formulas are not  equivalent, but under some conditions 
  (as outlined below) they are.›

no_notation FG_advice (‹_[_]μ› [90,60] 89)
no_notation GF_advice (‹_[_]ν› [90,60] 89)

notation FG_advice (‹_[_]Σ1› [90,60] 89)
notation GF_advice (‹_[_]Π1› [90,60] 89)

fun flatten_sigma_2:: "'a ltln ⇒ 'a ltln set ⇒ 'a ltln" (‹_[_]Σ2›)
where
  "(φ Un ψ)[M]Σ2 = (φ[M]Σ2) Un (ψ[M]Σ2)"
| "(φ Wn ψ)[M]Σ2 = (φ[M]Σ2) Un ((ψ[M]Σ2) orn (Gn φ[M]Π1))"
| "(φ Mn ψ)[M]Σ2 = (φ[M]Σ2) Mn (ψ[M]Σ2)"
| "(φ Rn ψ)[M]Σ2 = ((φ[M]Σ2) orn (Gn ψ[M]Π1)) Mn (ψ[M]Σ2)"
| "(φ andn ψ)[M]Σ2 = (φ[M]Σ2) andn (ψ[M]Σ2)"
| "(φ orn ψ)[M]Σ2 = (φ[M]Σ2) orn (ψ[M]Σ2)"
| "(Xn φ)[M]Σ2 = Xn (φ[M]Σ2)"
| "φ[M]Σ2 = φ"

fun flatten_pi_2 :: "'a ltln ⇒ 'a ltln set ⇒ 'a ltln" (‹_[_]Π2›)
where
  "(φ Wn ψ)[N]Π2 = (φ[N]Π2) Wn (ψ[N]Π2)"
| "(φ Un ψ)[N]Π2 = (φ[N]Π2 andn (Fn ψ[N]Σ1)) Wn (ψ[N]Π2)"
| "(φ Rn ψ)[N]Π2 = (φ[N]Π2) Rn (ψ[N]Π2)"
| "(φ Mn ψ)[N]Π2 = (φ[N]Π2) Rn ((ψ[N]Π2) andn (Fn φ[N]Σ1))"
| "(φ andn ψ)[N]Π2 = (φ[N]Π2) andn (ψ[N]Π2)"
| "(φ orn ψ)[N]Π2 = (φ[N]Π2) orn (ψ[N]Π2)"
| "(Xn φ)[N]Π2 = Xn (φ[N]Π2)"
| "φ[N]Π2 = φ"

lemma GF_advice_restriction:
  "φ[𝒢ℱ (φ Wn ψ) w]Π1 = φ[𝒢ℱ φ w]Π1"
  "ψ[𝒢ℱ (φ Rn ψ) w]Π1 = ψ[𝒢ℱ ψ w]Π1"
  by (metis (no_types, lifting) 𝒢ℱ_semantics' inf_commute inf_left_commute inf_sup_absorb subformulasμ.simps(6) GF_advice_inter_subformulas) 
     (metis (no_types, lifting) GF_advice_inter 𝒢ℱ.simps(5) 𝒢ℱ_semantics' 𝒢ℱ_subformulasμ inf.commute sup.boundedE)

lemma FG_advice_restriction: 
  "ψ[ℱ𝒢 (φ Un ψ) w]Σ1 = ψ[ℱ𝒢 ψ w]Σ1"
  "φ[ℱ𝒢 (φ Mn ψ) w]Σ1 = φ[ℱ𝒢 φ w]Σ1"  
  by (metis (no_types, lifting) FG_advice_inter ℱ𝒢.simps(4) ℱ𝒢_semantics' ℱ𝒢_subformulasν inf.commute sup.boundedE) 
     (metis (no_types, lifting) FG_advice_inter ℱ𝒢.simps(7) ℱ𝒢_semantics' ℱ𝒢_subformulasν inf.right_idem inf_commute sup.cobounded1) 

lemma flatten_sigma_2_intersection:
  "M ∩ subformulasμ φ ⊆ S ⟹ φ[M ∩ S]Σ2 = φ[M]Σ2"
  by (induction φ) (simp; blast intro: GF_advice_inter)+

lemma flatten_sigma_2_intersection_eq:
  "M ∩ subformulasμ φ = M' ⟹ φ[M']Σ2 = φ[M]Σ2"
  using flatten_sigma_2_intersection by auto

lemma flatten_sigma_2_monotone: 
  "w ⊨n φ[M]Σ2 ⟹ M ⊆ M' ⟹ w ⊨n φ[M']Σ2"
  by (induction φ arbitrary: w)
     (simp; blast dest: GF_advice_monotone)+

lemma flatten_pi_2_intersection:
  "N ∩ subformulasν φ ⊆ S ⟹ φ[N ∩ S]Π2 = φ[N]Π2"
  by (induction φ) (simp; blast intro: FG_advice_inter)+

lemma flatten_pi_2_intersection_eq:
  "N ∩ subformulasν φ = N' ⟹ φ[N']Π2 = φ[N]Π2"
  using flatten_pi_2_intersection by auto

lemma flatten_pi_2_monotone: 
  "w ⊨n φ[N]Π2 ⟹ N ⊆ N' ⟹ w ⊨n φ[N']Π2"
  by (induction φ arbitrary: w)
     (simp; blast dest: FG_advice_monotone)+

lemma ltln_weak_strong_stable_words_1:
  "w ⊨n (φ Wn ψ) ⟷ w ⊨n φ Un (ψ orn (Gn φ[𝒢ℱ φ w]Π1))" (is "?lhs ⟷ ?rhs") 
proof 
  assume ?lhs
  
  moreover

  {
    assume assm: "w ⊨n Gn φ"
    moreover
    obtain i where "⋀j. ℱ φ (suffix i w) ⊆ 𝒢ℱ φ w"
      by (metis MOST_nat_le 𝒢ℱ_suffix μ_stable_def order_refl suffix_μ_stable)
    hence "⋀j. ℱ φ (suffix i (suffix j w)) ⊆ 𝒢ℱ φ w"
      by (metis ℱ_suffix 𝒢ℱ_ℱ_subset 𝒢ℱ_suffix semiring_normalization_rules(24) subset_Un_eq suffix_suffix sup.orderE)
    ultimately
    have "suffix i w ⊨n Gn (φ[𝒢ℱ φ w]Π1)"
      using GF_advice_a1[OF ‹⋀j. ℱ φ (suffix i (suffix j w)) ⊆ 𝒢ℱ φ w›]
      by (simp add: add.commute)
    hence "?rhs"
      using assm by auto 
  }

  moreover

  have "w ⊨n φ Un ψ ⟹ ?rhs"
    by auto
  
  ultimately

  show ?rhs
    using ltln_weak_to_strong(1) by blast
next
  assume ?rhs
  thus ?lhs
    unfolding ltln_weak_strong_2 unfolding semantics_ltln.simps
    by (metis 𝒢ℱ_suffix order_refl GF_advice_a2)
qed

lemma ltln_weak_strong_stable_words_2:
  "w ⊨n (φ Rn ψ) ⟷ w ⊨n (φ orn (Gn ψ[𝒢ℱ ψ w]Π1)) Mn ψ" (is "?lhs ⟷ ?rhs") 
proof 
  assume ?lhs
  
  moreover

  {
    assume assm: "w ⊨n Gn ψ"
    moreover
    obtain i where "⋀j. ℱ ψ (suffix i w) ⊆ 𝒢ℱ ψ w"
      by (metis MOST_nat_le 𝒢ℱ_suffix μ_stable_def order_refl suffix_μ_stable)
    hence "⋀j. ℱ ψ (suffix i (suffix j w)) ⊆ 𝒢ℱ ψ w"
      by (metis ℱ_suffix 𝒢ℱ_ℱ_subset 𝒢ℱ_suffix semiring_normalization_rules(24) subset_Un_eq suffix_suffix sup.orderE)
    ultimately
    have "suffix i w ⊨n Gn (ψ[𝒢ℱ ψ w]Π1)"
      using GF_advice_a1[OF ‹⋀j. ℱ ψ (suffix i (suffix j w)) ⊆ 𝒢ℱ ψ w›]
      by (simp add: add.commute)
    hence "?rhs"
      using assm by auto 
  }

  moreover

  have "w ⊨n φ Mn ψ ⟹ ?rhs"
    by auto
  
  ultimately

  show ?rhs
    using ltln_weak_to_strong by blast
next
  assume ?rhs
  thus ?lhs
    unfolding ltln_weak_strong_2 unfolding semantics_ltln.simps
    by (metis GF_advice_a2 𝒢ℱ_suffix order_refl)
qed

lemma ltln_weak_strong_stable_words:
  "w ⊨n (φ Wn ψ) ⟷ w ⊨n φ Un (ψ orn (Gn φ[𝒢ℱ (φ Wn ψ) w]Π1))"
  "w ⊨n (φ Rn ψ) ⟷ w ⊨n (φ orn (Gn ψ[𝒢ℱ (φ Rn ψ) w]Π1)) Mn ψ"
  unfolding ltln_weak_strong_stable_words_1 ltln_weak_strong_stable_words_2 GF_advice_restriction by simp+

lemma flatten_sigma_2_IH_lifting: 
  assumes "ψ ∈ subfrmlsn φ"
  assumes "suffix i w ⊨n ψ[𝒢ℱ ψ (suffix i w)]Σ2 = suffix i w ⊨n ψ"
  shows "suffix i w ⊨n ψ[𝒢ℱ φ w]Σ2 = suffix i w ⊨n ψ" 
  by (metis (no_types, lifting) inf.absorb_iff2 inf_assoc inf_commute assms(2) 𝒢ℱ_suffix flatten_sigma_2_intersection_eq[of "𝒢ℱ φ w" ψ "𝒢ℱ ψ w"] 𝒢ℱ_semantics' subformulasμ_subset[OF assms(1)])
  
lemma flatten_sigma_2_correct:
  "w ⊨n φ[𝒢ℱ φ w]Σ2 ⟷ w ⊨n φ"
proof (induction φ arbitrary: w)
  case (And_ltln φ1 φ2)
  then show ?case 
    using flatten_sigma_2_IH_lifting[of _ "φ1 andn φ2" 0] by simp
next
  case (Or_ltln φ1 φ2)
  then show ?case 
    using flatten_sigma_2_IH_lifting[of _ "φ1 orn φ2" 0] by simp
next
  case (Next_ltln φ)
  then show ?case 
    using flatten_sigma_2_IH_lifting[of _ "Xn φ" 1] by fastforce
next
  case (Until_ltln φ1 φ2)
  then show ?case
    using flatten_sigma_2_IH_lifting[of _ "φ1 Un φ2"] by fastforce
next
  case (Release_ltln φ1 φ2)
  then show ?case
    unfolding ltln_weak_strong_stable_words
    using flatten_sigma_2_IH_lifting[of _ "φ1 Rn φ2"] by fastforce
next
  case (WeakUntil_ltln φ1 φ2)
  then show ?case
    unfolding ltln_weak_strong_stable_words
    using flatten_sigma_2_IH_lifting[of _ "φ1 Wn φ2"] by fastforce
next
case (StrongRelease_ltln φ1 φ2)
  then show ?case
    using flatten_sigma_2_IH_lifting[of _ "φ1 Mn φ2"] by fastforce
qed auto

lemma ltln_strong_weak_stable_words_1:
  "w ⊨n φ Un ψ ⟷ w ⊨n (φ andn (Fn ψ[ℱ𝒢 ψ w]Σ1)) Wn ψ" (is "?lhs ⟷ ?rhs") 
proof 
  assume ?rhs

  moreover

  obtain i where "ν_stable ψ (suffix i w)"
    by (metis MOST_nat less_Suc_eq suffix_ν_stable)
  hence "∀ψ ∈ ℱ𝒢 ψ w. suffix i w ⊨n Gn ψ"
    using ℱ𝒢_suffix 𝒢_elim ν_stable_def by blast

  {
    assume assm: "w ⊨n Gn (φ andn (Fn ψ[ℱ𝒢 ψ w]Σ1))"
    hence "suffix i w ⊨n (Fn ψ)[ℱ𝒢 ψ w]Σ1"
      by simp
    hence "suffix i w ⊨n Fn ψ"
      by (blast dest: FG_advice_b2_helper[OF ‹∀ψ ∈ ℱ𝒢 ψ w. suffix i w ⊨n Gn ψ›])
    hence "w ⊨n φ Un ψ"
      using assm by auto
  }

  ultimately
  
  show ?lhs
    by (meson ltln_weak_to_strong(1) semantics_ltln.simps(5) until_and_left_distrib)
next 
  assume ?lhs 

  moreover

  have "⋀i. suffix i w ⊨n ψ ⟹ suffix i w ⊨n ψ[ℱ𝒢 ψ w]Σ1"
    using ℱ𝒢_suffix by (blast intro: FG_advice_b1)

  ultimately

  show "?rhs"
    unfolding ltln_strong_weak_2 by fastforce
qed

lemma ltln_strong_weak_stable_words_2:
  "w ⊨n φ Mn ψ ⟷ w ⊨n φ Rn (ψ andn (Fn φ[ℱ𝒢 φ w]Σ1))" (is "?lhs ⟷ ?rhs") 
proof 
  assume ?rhs

  moreover

  obtain i where "ν_stable φ (suffix i w)"
    by (metis MOST_nat less_Suc_eq suffix_ν_stable)
  hence "∀ψ ∈ ℱ𝒢 φ w. suffix i w ⊨n Gn ψ"
    using ℱ𝒢_suffix 𝒢_elim ν_stable_def by blast

  {
    assume assm: "w ⊨n Gn (ψ andn (Fn φ[ℱ𝒢 φ w]Σ1))"
    hence "suffix i w ⊨n (Fn φ)[ℱ𝒢 φ w]Σ1"
      by simp
    hence "suffix i w ⊨n Fn φ"
      by (blast dest: FG_advice_b2_helper[OF ‹∀ψ ∈ ℱ𝒢 φ w. suffix i w ⊨n Gn ψ›])
    hence "w ⊨n φ Mn ψ"
      using assm by auto
  }

  ultimately
  
  show ?lhs
    using ltln_weak_to_strong(3) semantics_ltln.simps(5) strong_release_and_right_distrib by blast
next 
  assume ?lhs 

  moreover

  have "⋀i. suffix i w ⊨n φ ⟹ suffix i w ⊨n φ[ℱ𝒢 φ w]Σ1"
    using ℱ𝒢_suffix by (blast intro: FG_advice_b1)

  ultimately

  show "?rhs"
    unfolding ltln_strong_weak_2 by fastforce
qed

lemma ltln_strong_weak_stable_words:
  "w ⊨n φ Un ψ ⟷ w ⊨n (φ andn (Fn ψ[ℱ𝒢 (φ Un ψ) w]Σ1)) Wn ψ"
  "w ⊨n φ Mn ψ ⟷ w ⊨n φ Rn (ψ andn (Fn φ[ℱ𝒢 (φ Mn ψ) w]Σ1))"
  unfolding ltln_strong_weak_stable_words_1 ltln_strong_weak_stable_words_2 FG_advice_restriction by simp+

lemma flatten_pi_2_IH_lifting: 
  assumes "ψ ∈ subfrmlsn φ"
  assumes "suffix i w ⊨n ψ[ℱ𝒢 ψ (suffix i w)]Π2 = suffix i w ⊨n ψ"
  shows "suffix i w ⊨n ψ[ℱ𝒢 φ w]Π2 = suffix i w ⊨n ψ" 
  by (metis (no_types, lifting) inf.absorb_iff2 inf_assoc inf_commute assms(2) ℱ𝒢_suffix flatten_pi_2_intersection_eq[of "ℱ𝒢 φ w" ψ "ℱ𝒢 ψ w"] ℱ𝒢_semantics' subformulasν_subset[OF assms(1)])

lemma flatten_pi_2_correct:
  "w ⊨n φ[ℱ𝒢 φ w]Π2 ⟷ w ⊨n φ"
proof (induction φ arbitrary: w)
  case (And_ltln φ1 φ2)
  then show ?case 
    using flatten_pi_2_IH_lifting[of _ "φ1 andn φ2" 0] by simp
next
  case (Or_ltln φ1 φ2)
  then show ?case 
    using flatten_pi_2_IH_lifting[of _ "φ1 orn φ2" 0] by simp
next
  case (Next_ltln φ)
  then show ?case 
    using flatten_pi_2_IH_lifting[of _ "Xn φ" 1] by fastforce
next
  case (Until_ltln φ1 φ2)
  then show ?case
    unfolding ltln_strong_weak_stable_words
    using flatten_pi_2_IH_lifting[of _ "φ1 Un φ2"] by fastforce
next
  case (Release_ltln φ1 φ2)
  then show ?case
    using flatten_pi_2_IH_lifting[of _ "φ1 Rn φ2"] by fastforce
next
  case (WeakUntil_ltln φ1 φ2)
  then show ?case
    using flatten_pi_2_IH_lifting[of _ "φ1 Wn φ2"] by fastforce
next
case (StrongRelease_ltln φ1 φ2)
  then show ?case
    unfolding ltln_strong_weak_stable_words
    using flatten_pi_2_IH_lifting[of _ "φ1 Mn φ2"] by fastforce
qed auto

subsection ‹Main Theorem›

text ‹Using the four previously defined functions we obtain our normal form.›

theorem normal_form_with_flatten_sigma_2:
  "w ⊨n φ ⟷ 
    (∃M ⊆ subformulasμ φ. ∃N ⊆ subformulasν φ.
      w ⊨n φ[M]Σ2 ∧ (∀ψ ∈ M. w ⊨n Gn (Fn ψ[N]Σ1)) ∧ (∀ψ ∈ N. w ⊨n Fn (Gn ψ[M]Π1)))" (is "?lhs ⟷ ?rhs")
proof
  assume ?lhs
  then have "w ⊨n φ[𝒢ℱ φ w]Σ2"
    using flatten_sigma_2_correct by blast
  then show ?rhs
    using 𝒢ℱ_subformulasμ ℱ𝒢_subformulasν 𝒢ℱ_implies_GF ℱ𝒢_implies_FG by metis 
next
  assume ?rhs
  then obtain M N where "w ⊨n φ[M]Σ2" and "M ⊆ 𝒢ℱ φ w" and "N ⊆ ℱ𝒢 φ w"
    using X_𝒢ℱ_Y_ℱ𝒢 by blast
  then have "w ⊨n φ[𝒢ℱ φ w]Σ2"
    using flatten_sigma_2_monotone by blast
  then show ?lhs
    using flatten_sigma_2_correct by blast
qed

theorem normal_form_with_flatten_pi_2:
  "w ⊨n φ ⟷ 
    (∃M ⊆ subformulasμ φ. ∃N ⊆ subformulasν φ.
      w ⊨n φ[N]Π2 ∧ (∀ψ ∈ M. w ⊨n Gn (Fn ψ[N]Σ1)) ∧ (∀ψ ∈ N. w ⊨n Fn (Gn ψ[M]Π1)))" (is "?lhs ⟷ ?rhs")
proof
  assume ?lhs
  then have "w ⊨n φ[ℱ𝒢 φ w]Π2"
    using flatten_pi_2_correct by blast
  then show ?rhs
    using 𝒢ℱ_subformulasμ ℱ𝒢_subformulasν 𝒢ℱ_implies_GF ℱ𝒢_implies_FG by metis 
next
  assume ?rhs
  then obtain M N where "w ⊨n φ[N]Π2" and "M ⊆ 𝒢ℱ φ w" and "N ⊆ ℱ𝒢 φ w"
    using X_𝒢ℱ_Y_ℱ𝒢 by metis
  then have "w ⊨n φ[ℱ𝒢 φ w]Π2"
    using flatten_pi_2_monotone by metis
  then show ?lhs
    using flatten_pi_2_correct by blast
qed

end