Theory Proof_System

(*<*)
theory Proof_System
  imports Formula Partition
begin
(*>*)

section ‹Proof System›

unbundle MFOTL_notation

context begin

inductive SAT and VIO :: "('n, 'd) trace ⇒ ('n, 'd) env ⇒ nat ⇒ ('n, 'd) formula ⇒ bool" for σ where
  STT: "SAT σ v i TT"
| VFF: "VIO σ v i FF"
| SPred: "(r, eval_trms v ts) ∈ Γ σ i ⟹ SAT σ v i (Pred r ts)"
| VPred: "(r, eval_trms v ts) ∉ Γ σ i ⟹ VIO σ v i (Pred r ts)"
| SEq_Const: "v x = c ⟹ SAT σ v i (Eq_Const x c)"
| VEq_Const: "v x ≠ c ⟹ VIO σ v i (Eq_Const x c)"
| SNeg: "VIO σ v i φ ⟹ SAT σ v i (Neg φ)"
| VNeg: "SAT σ v i φ ⟹ VIO σ v i (Neg φ)"
| SOrL: "SAT σ v i φ ⟹ SAT σ v i (Or φ ψ)"
| SOrR: "SAT σ v i ψ ⟹ SAT σ v i (Or φ ψ)"
| VOr: "VIO σ v i φ ⟹ VIO σ v i ψ ⟹ VIO σ v i (Or φ ψ)"
| SAnd: "SAT σ v i φ ⟹ SAT σ v i ψ ⟹ SAT σ v i (And φ ψ)"
| VAndL: "VIO σ v i φ ⟹ VIO σ v i (And φ ψ)"
| VAndR: "VIO σ v i ψ ⟹ VIO σ v i (And φ ψ)"
| SImpL: "VIO σ v i φ ⟹ SAT σ v i (Imp φ ψ)"
| SImpR: "SAT σ v i ψ ⟹ SAT σ v i (Imp φ ψ)"
| VImp: "SAT σ v i φ ⟹ VIO σ v i ψ ⟹ VIO σ v i (Imp φ ψ)"
| SIffSS: "SAT σ v i φ ⟹ SAT σ v i ψ ⟹ SAT σ v i (Iff φ ψ)"
| SIffVV: "VIO σ v i φ ⟹ VIO σ v i ψ ⟹ SAT σ v i (Iff φ ψ)"
| VIffSV: "SAT σ v i φ ⟹ VIO σ v i ψ ⟹ VIO σ v i (Iff φ ψ)"
| VIffVS: "VIO σ v i φ ⟹ SAT σ v i ψ ⟹ VIO σ v i (Iff φ ψ)"
| SExists: "∃z. SAT σ (v (x := z)) i φ ⟹ SAT σ v i (Exists x φ)"
| VExists: "∀z. VIO σ (v (x := z)) i φ ⟹ VIO σ v i (Exists x φ)"
| SForall: "∀z. SAT σ (v (x := z)) i φ ⟹ SAT σ v i (Forall x φ)"
| VForall: "∃z. VIO σ (v (x := z)) i φ ⟹ VIO σ v i (Forall x φ)"
| SPrev: "i > 0 ⟹ mem (Δ σ i) I ⟹ SAT σ v (i-1) φ ⟹ SAT σ v i (❙Y I φ)"
| VPrev: "i > 0 ⟹ VIO σ v (i-1) φ ⟹ VIO σ v i (❙Y I φ)"
| VPrevZ: "i = 0 ⟹ VIO σ v i (❙Y I φ)"
| VPrevOutL: "i > 0 ⟹ (Δ σ i) < (left I) ⟹ VIO σ v i (❙Y I φ)"
| VPrevOutR: "i > 0 ⟹ enat (Δ σ i) > (right I) ⟹ VIO σ v i (❙Y I φ)"
| SNext: "mem (Δ σ (i+1)) I ⟹ SAT σ v (i+1) φ ⟹ SAT σ v i (❙X I φ)"
| VNext: "VIO σ v (i+1) φ ⟹ VIO σ v i (❙X I φ)"
| VNextOutL: "(Δ σ (i+1)) < (left I) ⟹ VIO σ v i (❙X I φ)"
| VNextOutR: "enat (Δ σ (i+1)) > (right I) ⟹ VIO σ v i (❙X I φ)"
| SOnce: "j ≤ i ⟹ mem (δ σ i j) I ⟹ SAT σ v j φ ⟹ SAT σ v i (❙P I φ)"
| VOnceOut: "τ σ i < τ σ 0 + left I ⟹ VIO σ v i (❙P I φ)"
| VOnce: "j = (case right I of ∞ ⇒ 0 
               | enat b ⇒ ETP_p σ i b) ⟹
          (τ σ i) ≥ (τ σ 0) + left I ⟹
          (⋀k. k ∈ {j .. LTP_p σ i I} ⟹ VIO σ v k φ) ⟹ VIO σ v i (❙P I φ)"
| SEventually: "j ≥ i ⟹ mem (δ σ j i) I  ⟹ SAT σ v j φ ⟹ SAT σ v i (❙F I φ)"
| VEventually: "(⋀k. k ∈ (case right I of ∞ ⇒ {ETP_f σ i I ..}
                           | enat b ⇒ {ETP_f σ i I .. LTP_f σ i b}) ⟹ VIO σ v k φ) ⟹ 
                VIO σ v i (❙F I φ)"
| SHistorically: "j = (case right I of ∞ ⇒ 0
                       | enat b ⇒ ETP_p σ i b) ⟹
                 (τ σ i) ≥ (τ σ 0) + left I ⟹
                 (⋀k. k ∈ {j .. LTP_p σ i I} ⟹ SAT σ v k φ) ⟹ SAT σ v i (❙H I φ)"
| SHistoricallyOut: "τ σ i < τ σ 0 + left I ⟹ SAT σ v i (❙H I φ)"
| VHistorically: "j ≤ i ⟹ mem (δ σ i j) I  ⟹ VIO σ v j φ ⟹ VIO σ v i (❙H I φ)"
| SAlways: "(⋀k. k ∈ (case right I of ∞ ⇒ {ETP_f σ i I ..} 
                       | enat b ⇒ {ETP_f σ i I .. LTP_f σ i b}) ⟹ SAT σ v k φ) ⟹
            SAT σ v i (❙G I φ)"
| VAlways: "j ≥ i ⟹ mem (δ σ j i) I  ⟹ VIO σ v j φ ⟹ VIO σ v i (❙G I φ)"
| SSince: "j ≤ i ⟹ mem (δ σ i j) I  ⟹ SAT σ v j ψ ⟹ (⋀k. k ∈ {j <.. i} ⟹ 
           SAT σ v k φ) ⟹ SAT σ v i (φ ❙S I ψ)"
| VSinceOut: "τ σ i < τ σ 0 + left I ⟹ VIO σ v i (φ ❙S I ψ)"
| VSince: "(case right I of ∞ ⇒ True 
            | enat b ⇒ ETP σ ((τ σ i) - b) ≤ j) ⟹ 
           j ≤ i ⟹ (τ σ 0) + left I ≤ (τ σ i) ⟹ VIO σ v j φ ⟹
           (⋀k. k ∈ {j .. (LTP_p σ i I)} ⟹ VIO σ v k ψ) ⟹ VIO σ v i (φ ❙S I ψ)"
| VSinceInf: "j = (case right I of ∞ ⇒ 0 
                   | enat b ⇒ ETP_p σ i b) ⟹
             (τ σ i) ≥ (τ σ 0) + left I ⟹ 
             (⋀k. k ∈ {j .. LTP_p σ i I} ⟹ VIO σ v k ψ) ⟹ VIO σ v i (φ ❙S I ψ)"
| SUntil: "j ≥ i ⟹ mem (δ σ j i) I  ⟹ SAT σ v j ψ ⟹ (⋀k. k ∈ {i ..< j} ⟹ SAT σ v k φ) ⟹ 
           SAT σ v i (φ ❙U I ψ)"
| VUntil: "(case right I of ∞ ⇒ True 
            | enat b ⇒ j < LTP_f σ i b) ⟹ 
           j ≥ i ⟹ VIO σ v j φ ⟹ (⋀k. k ∈ {ETP_f σ i I .. j} ⟹ VIO σ v k ψ) ⟹ 
           VIO σ v i (φ ❙U I ψ)"
| VUntilInf: "(⋀k. k ∈ (case right I of ∞ ⇒ {ETP_f σ i I ..} 
                         | enat b ⇒ {ETP_f σ i I .. LTP_f σ i b}) ⟹ VIO σ v k ψ) ⟹
              VIO σ v i (φ ❙U I ψ)"

subsection ‹Soundness and Completeness›

lemma not_sat_SinceD:
  assumes unsat: "¬ ⟨σ, v, i⟩ ⊨ φ ❙S I ψ" and
    witness: "∃j ≤ i. mem (τ σ i - τ σ j) I ∧ ⟨σ, v, j⟩ ⊨ ψ"
  shows "∃j ≤ i. ETP σ (case right I of ∞ ⇒ 0 | enat n ⇒ τ σ i - n) ≤ j ∧ ¬ ⟨σ, v, j⟩ ⊨ φ
  ∧ (∀k ∈ {j .. (min i (LTP σ (τ σ i - left I)))}. ¬ ⟨σ, v, k⟩ ⊨ ψ)"
proof -
  define A and j where A_def: "A ≡ {j. j ≤ i ∧ mem (τ σ i - τ σ j) I ∧ ⟨σ, v, j⟩ ⊨ ψ}"
    and j_def: "j ≡ Max A"
  from witness have j: "j ≤ i" "⟨σ, v, j⟩ ⊨ ψ" "mem (τ σ i - τ σ j) I"
    using Max_in[of A] unfolding j_def[symmetric] unfolding A_def
    by auto
  moreover
  from j(3) have "ETP σ (case right I of enat n ⇒ τ σ i - n | ∞ ⇒ 0) ≤ j"
    unfolding ETP_def by (intro Least_le) (auto split: enat.splits)
  moreover
  { fix j
    assume j: "τ σ j ≤ τ σ i"
    then obtain k where k: "τ σ i < τ σ k"
      by (meson ex_le_τ gt_ex less_le_trans)
    have "j ≤ ETP σ (Suc (τ σ i))"
      unfolding ETP_def
    proof (intro LeastI2[of _ k "λi. j ≤ i"])
      fix l
      assume "Suc (τ σ i) ≤ τ σ l"
      with j show "j ≤ l"
        by (metis lessI less_τD nless_le order_less_le_trans)
    qed (auto simp: Suc_le_eq k(1))
  } note * = this
  { fix k
    assume "k ∈ {j <.. (min i (LTP σ (τ σ i - left I)))}"
    with j(3) have k: "j < k" "k ≤ i" "k ≤ Max {j. left I + τ σ j ≤ τ σ i}"
      by (auto simp: LTP_def le_diff_conv2 add.commute)
    with j(3) obtain l where "left I + τ σ l ≤ τ σ i" "k ≤ l"
      by (subst (asm) Max_ge_iff) (auto simp: le_diff_conv2 *
          intro!: finite_subset[of _ "{0 .. ETP σ (τ σ i + 1)}"])
    then have "mem (τ σ i - τ σ k) I"
      using k(1,2) j(3)
      by (cases "right I") (auto simp: le_diff_conv le_diff_conv2 add.commute dest: τ_mono
         elim: order_trans[rotated] order_trans)
    with Max_ge[of A k] k have "¬ ⟨σ, v, k⟩ ⊨ ψ"
      unfolding j_def[symmetric] unfolding A_def
      by auto
  }
  ultimately show ?thesis using unsat
    by (auto dest!: spec[of _ j])
qed

lemma not_sat_UntilD:
  assumes unsat: "¬ ⟨σ, v, i⟩ ⊨ φ ❙U I ψ"
    and witness: "∃j ≥ i. mem (δ σ j i) I ∧ ⟨σ, v, j⟩ ⊨ ψ"
  shows "∃j ≥ i. (case right I of ∞ ⇒ True | enat n ⇒ j < LTP σ (τ σ i + n))
  ∧ ¬ (⟨σ, v, j⟩ ⊨ φ) ∧ (∀k ∈ {(max i (ETP σ (τ σ i + left I))) .. j}.
   ¬ ⟨σ, v, k⟩ ⊨ ψ)"
proof -
  from τ_mono have i0: "τ σ 0 ≤ τ σ i" by auto
  from witness obtain jmax where jmax: "jmax ≥ i" "⟨σ, v, jmax⟩ ⊨ ψ"
    "mem (δ σ jmax i) I" by blast
  define A and j where A_def: "A ≡ {j. j ≥ i ∧ j ≤ jmax
  ∧ mem (δ σ j i) I ∧ ⟨σ, v, j⟩ ⊨ ψ}" and j_def: "j ≡ Min A"
  have j: "j ≥ i" "⟨σ, v, j⟩ ⊨ ψ" "mem (δ σ j i) I"
    using A_def j_def jmax Min_in[of A]
    unfolding j_def[symmetric] unfolding A_def
    by fastforce+
  moreover have "case right I of ∞ ⇒ True | enat n ⇒ j ≤ LTP σ (τ σ i + n)"
    using i0 j(1,3)
    by (auto simp: i_LTP_tau trans_le_add1 split: enat.splits)
  moreover
  { fix k
    assume k_def: "k ∈ {(max i (ETP σ (τ σ i + left I))) ..< j}"
    then have ki: "τ σ k ≥ τ σ i + left I" using i_ETP_tau by auto
    with k_def have kj: "k < j" by auto
    then have "τ σ k ≤ τ σ j" by auto
    then have "δ σ k i ≤ δ σ j i" by auto
    with this j(3) have "enat (δ σ k i) ≤ right I"
      by (meson enat_ord_simps(1) order_subst2)
    with this ki j(3) have mem_k: "mem (δ σ k i) I"
      unfolding ETP_def by (auto simp: Least_le)

    with j_def have "j ≤ jmax" using Min_in[of A]
      using jmax A_def
      by (metis (mono_tags, lifting) Collect_empty_eq
          finite_nat_set_iff_bounded_le mem_Collect_eq order_refl)
    with this k_def have kjm: "k ≤ jmax" by auto

    with this mem_k ki Min_le[of A k] k_def have "k ∉ A"
      unfolding j_def[symmetric] unfolding A_def unfolding ETP_def
      using finite_nat_set_iff_bounded_le kj leD by blast
    with this mem_k k_def kjm have "¬ ⟨σ, v, k⟩ ⊨ ψ"
      by (simp add: A_def) }
  ultimately show ?thesis using unsat
    by (auto split: enat.splits dest!: spec[of _ j])
qed

lemma soundness_raw: "(SAT σ v i φ ⟶ ⟨σ, v, i⟩ ⊨ φ) ∧ (VIO σ v i φ ⟶ ¬ ⟨σ, v, i⟩ ⊨ φ)"
proof (induct v i φ rule: SAT_VIO.induct)
  case (VOnceOut i I v φ)
  { fix j
    from τ_mono have j0: "τ σ 0 ≤ τ σ j" by auto
    then have "τ σ i < τ σ j + left I" using VOnceOut by linarith
    then have "δ σ i j < left I"
      using VOnceOut less_τD verit_comp_simplify1(3) by fastforce
    then have "¬ mem (δ σ i j) I" by auto }
  then show ?case
    by auto
next
  case (VOnce j I i v φ)
  { fix k
    assume k_def: "⟨σ, v, k⟩ ⊨ φ ∧ mem (δ σ i k) I ∧ k ≤ i"
    then have k_tau: "τ σ k ≤ τ σ i - left I"
      using diff_le_mono2 by fastforce
    then have k_ltp: "k ≤ LTP σ (τ σ i - left I)"
      using VOnce i_LTP_tau add_le_imp_le_diff
      by blast
    then have "k ∉ {j .. LTP_p σ i I}"
      using k_def VOnce k_tau
      by auto
    then have "k < j" using k_def k_ltp by auto }
  then show ?case
    using VOnce
    by (cases "right I = ∞")
      (auto 0 0 simp: i_ETP_tau i_LTP_tau le_diff_conv2)
next
  case (VEventually I i v φ)
  { fix k n
    assume r: "right I = enat n"
    from this have tin0: "τ σ i + n ≥ τ σ 0"
      by (auto simp add: trans_le_add1)
    define j where "j = LTP σ ((τ σ i) + n)"
    then have j_i: "i ≤ j"
      by (auto simp add: i_LTP_tau trans_le_add1 j_def)
    assume k_def: "⟨σ, v, k⟩ ⊨ φ ∧ mem (δ σ k i) I ∧ i ≤ k"
    then have "τ σ k ≥ τ σ i + left I"
      using le_diff_conv2 by auto
    then have k_etp: "k ≥ ETP σ (τ σ i + left I)"
      using i_ETP_tau by blast
    from this k_def VEventually have "k ∉ {ETP_f σ i I .. j}"
      by (auto simp: r j_def)
    then have "j < k" using r k_def k_etp by auto
    from k_def r have "δ σ k i ≤ n" by auto
    then have "τ σ k ≤ τ σ i + n" by auto
    then have "k ≤ j" using tin0 i_LTP_tau by (auto simp add: j_def) }
  note aux = this
  show ?case
  proof (cases "right I")
    case (enat n)
    show ?thesis
      using VEventually[unfolded enat, simplified] aux
      by (simp add: i_ETP_tau enat)
        (metis τ_mono le_add_diff_inverse nat_add_left_cancel_le)
  next
    case infinity
    show ?thesis
      using VEventually
      by (auto simp: infinity i_ETP_tau le_diff_conv2)
  qed
next
  case (SHistorically j I i v φ)
  { fix k
    assume k_def: "¬ ⟨σ, v, k⟩ ⊨ φ ∧ mem (δ σ i k) I ∧ k ≤ i"
    then have k_tau: "τ σ k ≤ τ σ i - left I"
      using diff_le_mono2 by fastforce
    then have k_ltp: "k ≤ LTP σ (τ σ i - left I)"
      using SHistorically i_LTP_tau add_le_imp_le_diff
      by blast
    then have "k ∉ {j .. LTP_p σ i I}"
      using k_def SHistorically k_tau
      by auto
    then have "k < j" using k_def k_ltp by auto }
  then show ?case
    using SHistorically
    by (cases "right I = ∞")
      (auto 0 0 simp add: le_diff_conv2 i_ETP_tau i_LTP_tau)
next
  case (SHistoricallyOut i I v φ)
  { fix j
    from τ_mono have j0: "τ σ 0 ≤ τ σ j" by auto
    then have "τ σ i < τ σ j + left I" using SHistoricallyOut by linarith
    then have "δ σ i j < left I"
      using SHistoricallyOut less_τD not_le by fastforce
    then have "¬ mem (δ σ i j) I" by auto }
  then show ?case by auto
next
  case (SAlways I i v φ)
  { fix k n
    assume r: "right I = enat n"
    from this SAlways have tin0: "τ σ i + n ≥ τ σ 0"
      by (auto simp add: trans_le_add1)
    define j where "j = LTP σ ((τ σ i) + n)"
    from SAlways have j_i: "i ≤ j"
      by (auto simp add: i_LTP_tau trans_le_add1 j_def)
    assume k_def: "¬ ⟨σ, v, k⟩ ⊨ φ ∧ mem (δ σ k i) I ∧ i ≤ k"
    then have "τ σ k ≥ τ σ i + left I"
      using le_diff_conv2 by auto
    then have k_etp: "k ≥ ETP σ (τ σ i + left I)"
      using SAlways i_ETP_tau by blast
    from this k_def SAlways have "k ∉ {ETP_f σ i I .. j}"
      by (auto simp: r j_def)
    then have "j < k" using SAlways k_def k_etp by simp
    from k_def r have "δ σ k i ≤ n" by simp
    then have "τ σ k ≤ τ σ i + n" by simp
    then have "k ≤ j"
      using tin0 i_LTP_tau  
      by (auto simp add: j_def) }
  note aux = this
  show ?case
  proof (cases "right I")
    case (enat n)
    show ?thesis
      using SAlways[unfolded enat, simplified] aux
      by (simp add: i_ETP_tau le_diff_conv2 enat)
        (metis Groups.ab_semigroup_add_class.add.commute add_le_imp_le_diff)
  next
    case infinity
    show ?thesis
      using SAlways
      by (auto simp: infinity i_ETP_tau le_diff_conv2)
  qed
next
  case (VSinceOut i I v φ ψ)
  { fix j
    from τ_mono have j0: "τ σ 0 ≤ τ σ j" by auto
    then have "τ σ i < τ σ j + left I" using VSinceOut by linarith
    then have "δ σ i j < left I" using VSinceOut j0
      by (metis add.commute gr_zeroI leI less_τD less_diff_conv2 order_less_imp_not_less zero_less_diff)
    then have "¬ mem (δ σ i j) I" by auto }
  then show ?case using VSinceOut by auto
next
  case (VSince I i j v φ ψ)
  { fix k
    assume k_def: "⟨σ, v, k⟩ ⊨ ψ ∧ mem (δ σ i k) I ∧ k ≤ i"
    then have "τ σ k ≤ τ σ i - left I" using diff_le_mono2 by fastforce
    then have k_ltp: "k ≤ LTP σ (τ σ i - left I)"
      using VSince i_LTP_tau add_le_imp_le_diff
      by blast
    then have "k < j" using k_def VSince(7)[of k]
      by force
    then have "j ∈ {k <.. i} ∧ ¬ ⟨σ, v, j⟩ ⊨ φ" using VSince
      by auto }
  then show ?case using VSince
    by force
next
  case (VSinceInf j I i v ψ φ)
  { fix k
    assume k_def: "⟨σ, v, k⟩ ⊨ ψ ∧ mem (δ σ i k) I ∧ k ≤ i"
    then have k_tau: "τ σ k ≤ τ σ i - left I"
      using diff_le_mono2 by fastforce
    then have k_ltp: "k ≤ LTP σ (τ σ i - left I)"
      using VSinceInf i_LTP_tau add_le_imp_le_diff
      by blast
    then have "k ∉ {j .. LTP_p σ i I}"
      using k_def VSinceInf k_tau
      by auto
    then have "k < j" using k_def k_ltp by auto }
  then show ?case
    using VSinceInf
    by (cases "right I = ∞")
      (auto 0 0 simp: i_ETP_tau i_LTP_tau le_diff_conv2)
next
  case (VUntil I j i v φ ψ)
  { fix k
    assume k_def: "⟨σ, v, k⟩ ⊨ ψ ∧ mem (δ σ k i) I ∧ i ≤ k"
    then have "τ σ k ≥ τ σ i + left I"
      using le_diff_conv2 by auto
    then have k_etp: "k ≥ ETP σ (τ σ i + left I)"
      using VUntil i_ETP_tau by blast
    from this k_def VUntil have "k ∉ {ETP_f σ i I .. j}" by auto
    then have "j < k" using k_etp k_def by auto
    then have "j ∈ {i ..< k} ∧ VIO σ v j φ" using VUntil k_def
      by auto }
  then show ?case
    using VUntil by force
next
  case (VUntilInf I i v ψ φ)
  { fix k n
    assume r: "right I = enat n"
    from this VUntilInf have tin0: "τ σ i + n ≥ τ σ 0"
      by (auto simp add: trans_le_add1)
    define j where "j = LTP σ ((τ σ i) + n)"
    from VUntilInf have j_i: "i ≤ j"
      by (auto simp add: i_LTP_tau trans_le_add1 j_def)
    assume k_def: "⟨σ, v, k⟩ ⊨ ψ ∧ mem (δ σ k i) I ∧ i ≤ k"
    then have "τ σ k ≥ τ σ i + left I"
      using le_diff_conv2 by auto
    then have k_etp: "k ≥ ETP σ (τ σ i + left I)"
      using VUntilInf i_ETP_tau by blast
    from this k_def VUntilInf have "k ∉ {ETP_f σ i I .. j}"
      by (auto simp: r j_def)
    then have "j < k" using VUntilInf k_def k_etp by auto
    from k_def r have "δ σ k i ≤ n" by auto
    then have "τ σ k ≤ τ σ i + n" by auto
    then have "k ≤ j"
      using tin0 VUntilInf i_LTP_tau r k_def 
      by (force simp add: j_def) }
  note aux = this
  show ?case
  proof (cases "right I")
    case (enat n)
    show ?thesis
      using VUntilInf[unfolded enat, simplified] aux
      by (simp add: i_ETP_tau enat)
        (metis τ_mono le_add_diff_inverse nat_add_left_cancel_le)
  next
    case infinity
    show ?thesis
      using VUntilInf
      by (auto simp: infinity i_ETP_tau le_diff_conv2)
  qed
qed (auto simp: fun_upd_def split: nat.splits)

lemmas soundness = soundness_raw[THEN conjunct1, THEN mp] soundness_raw[THEN conjunct2, THEN mp]

lemma completeness_raw: "(⟨σ, v, i⟩ ⊨ φ ⟶ SAT σ v i φ) ∧ (¬ ⟨σ, v, i⟩ ⊨ φ ⟶ VIO σ v i φ)"
proof (induct φ arbitrary: v i)
  case (Prev I φ)
  show ?case using Prev
    by (auto intro: SAT_VIO.SPrev SAT_VIO.VPrev SAT_VIO.VPrevOutL SAT_VIO.VPrevOutR SAT_VIO.VPrevZ split: nat.splits)
next
  case (Once I φ)
  { assume "⟨σ, v, i⟩ ⊨ ❙P I φ"
    with Once have "SAT σ v i (❙P I φ)"
      by (auto intro: SAT_VIO.SOnce) }
  moreover
  { assume i_l: "τ σ i < τ σ 0 + left I"
    with Once have "VIO σ v i (❙P I φ)"
      by (auto intro: SAT_VIO.VOnceOut) }
  moreover
  { assume unsat: "¬ ⟨σ, v, i⟩ ⊨ ❙P I φ"
      and i_ge: "τ σ 0 + left I ≤ τ σ i"
    with Once have "VIO σ v i (❙P I φ)"
      by (auto intro!: SAT_VIO.VOnce simp: i_LTP_tau i_ETP_tau
          split: enat.splits) }
  ultimately show ?case
    by force
next
  case (Historically I φ)
  from τ_mono have i0: "τ σ 0 ≤ τ σ i" by auto
  { assume sat: "⟨σ, v, i⟩ ⊨ ❙H I φ"
      and i_ge: "τ σ i ≥ τ σ 0 + left I"
    with Historically have "SAT σ v i (❙H I φ)"
      using le_diff_conv
      by (auto intro!: SAT_VIO.SHistorically simp: i_LTP_tau i_ETP_tau
          split: enat.splits) }
  moreover
  { assume "¬ ⟨σ, v, i⟩ ⊨ ❙H I φ"
    with Historically have "VIO σ v i (❙H I φ)"
      by (auto intro: SAT_VIO.VHistorically) }
  moreover
  { assume i_l: "τ σ i < τ σ 0 + left I"
    with Historically have "SAT σ v i (❙H I φ)"
      by (auto intro: SAT_VIO.SHistoricallyOut) }
  ultimately show ?case
    by force
next
  case (Eventually I φ)
  from τ_mono have i0: "τ σ 0 ≤ τ σ i" by auto
  { assume "⟨σ, v, i⟩ ⊨ ❙F I φ"
    with Eventually have "SAT σ v i (❙F I φ)"
      by (auto intro: SAT_VIO.SEventually) }
  moreover
  { assume unsat: "¬ ⟨σ, v, i⟩ ⊨ ❙F I φ"
    with Eventually have "VIO σ v i (❙F I φ)"
      by (auto intro!: SAT_VIO.VEventually simp: add_increasing2 i0 i_LTP_tau i_ETP_tau
          split: enat.splits) }
  ultimately show ?case by auto
next
  case (Always I φ)
    from τ_mono have i0: "τ σ 0 ≤ τ σ i" by auto
  { assume "¬ ⟨σ, v, i⟩ ⊨ ❙G I φ"
    with Always have "VIO σ v i (❙G I φ)"
      by (auto intro: SAT_VIO.VAlways) }
  moreover
  { assume sat: "⟨σ, v, i⟩ ⊨ ❙G I φ"
    with Always have "SAT σ v i (❙G I φ)"
      by (auto intro!: SAT_VIO.SAlways simp: add_increasing2 i0 i_LTP_tau i_ETP_tau le_diff_conv split: enat.splits)}
  ultimately show ?case by auto
next
  case (Since φ I ψ)
  { assume "⟨σ, v, i⟩ ⊨ φ ❙S I ψ"
    with Since have "SAT σ v i (φ ❙S I ψ)"
      by (auto intro: SAT_VIO.SSince) }
  moreover
  { assume i_l: "τ σ i < τ σ 0 + left I"
    with Since have "VIO σ v i (φ ❙S I ψ)"
      by (auto intro: SAT_VIO.VSinceOut) }
  moreover
  { assume unsat: "¬ ⟨σ, v, i⟩ ⊨ φ ❙S I ψ"
      and nw: "∀j≤i. ¬ mem (δ σ i j) I ∨ ¬ ⟨σ, v, j⟩ ⊨ ψ"
      and i_ge: "τ σ 0 + left I ≤ τ σ i"
    with Since have "VIO σ v i (φ ❙S I ψ)"
      by (auto intro!: SAT_VIO.VSinceInf simp: i_LTP_tau i_ETP_tau
          split: enat.splits)}
  moreover
  { assume unsat: "¬ ⟨σ, v, i⟩ ⊨ φ ❙S I ψ"
      and jw: "∃j≤i. mem (δ σ i j) I ∧ ⟨σ, v, j⟩ ⊨ ψ"
      and i_ge: "τ σ 0 + left I ≤ τ σ i"
    from unsat jw not_sat_SinceD[of σ v i φ I ψ]
    obtain j where j: "j ≤ i"
      "case right I of ∞ ⇒ True | enat n ⇒ ETP σ (τ σ i - n) ≤ j"
      "¬ ⟨σ, v, j⟩ ⊨ φ" "(∀k ∈ {j .. (min i (LTP σ (τ σ i - left I)))}.
      ¬ ⟨σ, v, k⟩ ⊨ ψ)" by (auto split: enat.splits)
    with Since have "VIO σ v i (φ ❙S I ψ)"
      using i_ge unsat jw
      by (auto intro!: SAT_VIO.VSince) }
  ultimately show ?case
    by (force simp del: sat.simps)
next
  case (Until φ I ψ)
  from τ_mono have i0: "τ σ 0 ≤ τ σ i" by auto
  { assume "⟨σ, v, i⟩ ⊨ φ ❙U I ψ"
    with Until have "SAT σ v i (φ ❙U I ψ)"
      by (auto intro: SAT_VIO.SUntil) }
  moreover
  { assume unsat: "¬ ⟨σ, v, i⟩ ⊨ φ ❙U I ψ"
      and witness: "∃j ≥ i. mem (δ σ j i) I ∧ ⟨σ, v, j⟩ ⊨ ψ"
    from this Until not_sat_UntilD[of σ v i φ I ψ] obtain j
      where j: "j ≥ i" "(case right I of ∞ ⇒ True | enat n
      ⇒ j < LTP σ (τ σ i + n))" "¬ (⟨σ, v, j⟩ ⊨ φ)"
        "(∀k ∈ {(max i (ETP σ (τ σ i + left I))) .. j}. ¬ ⟨σ, v, k⟩ ⊨ ψ)"
      by auto
    with Until have "VIO σ v i (φ ❙U I ψ)"
      using unsat witness 
      by (auto intro!: SAT_VIO.VUntil) }
  moreover
  { assume unsat: "¬ ⟨σ, v, i⟩ ⊨ φ ❙U I ψ"
      and no_witness: "∀j ≥ i. ¬ mem (δ σ j i) I ∨ ¬ ⟨σ, v, j⟩ ⊨ ψ"
    with Until have "VIO σ v i (φ ❙U I ψ)"
      by (auto intro!: SAT_VIO.VUntilInf simp: add_increasing2 i0 i_LTP_tau i_ETP_tau
          split: enat.splits)
  }
  ultimately show ?case by auto
qed (auto intro: SAT_VIO.intros)

lemmas completeness = completeness_raw[THEN conjunct1, THEN mp] completeness_raw[THEN conjunct2, THEN mp]

lemma SAT_or_VIO: "SAT σ v i φ ∨ VIO σ v i φ"
  using completeness[of σ v i φ] by auto

end

unbundle MFOTL_no_notation

(*<*)
end
(*>*)