Theory IL_TemporalOperators

(*  Title:      IL_Operator.thy
    Date:       Oct 2006
    Author:     David Trachtenherz
*)

section ‹Temporal logic operators on natural intervals›

theory IL_TemporalOperators
imports IL_IntervalOperators
begin

text ‹Bool : some additional properties›

instantiation bool :: "{ord, zero, one, plus, times, order}"
begin

definition Zero_bool_def [simp]: "0 ≡ False"
definition One_bool_def [simp]: "1 ≡ True"
definition add_bool_def: "a + b ≡ a ∨ b"
definition mult_bool_def: "a * b ≡ a ∧ b"

instance ..

end

value "False < True"
value "True < True"
value "True ≤ True"

lemmas bool_op_rel_defs =
  add_bool_def 
  mult_bool_def
  less_bool_def
  le_bool_def

instance bool :: wellorder
apply (rule wf_wellorderI)
 apply (rule_tac t="{(x, y). x < y}" and s="{(False, True)}" in subst)
  apply fastforce
 apply (unfold wf_def, blast)
apply intro_classes
done

instance bool :: comm_semiring_1
apply intro_classes
apply (unfold bool_op_rel_defs Zero_bool_def One_bool_def)
apply blast+
done


subsection ‹Basic definitions›

lemma UNIV_nat: "ℕ = (UNIV::nat set)"
by (simp add: Nats_def)

text ‹Universal temporal operator: Always/Globally›
definition iAll :: "iT ⇒ (Time ⇒ bool) ⇒ bool"      ― ‹Always›
  where "iAll I P ≡ ∀t∈I. P t"

text ‹Existential temporal operator: Eventually/Finally›
definition iEx :: "iT ⇒ (Time ⇒ bool) ⇒ bool"      ― ‹Eventually›
  where "iEx I P ≡ ∃t∈I. P t"


syntax
  "_iAll" :: "Time ⇒ iT ⇒ (Time ⇒ bool) ⇒ bool" ("(3□ _ _./ _)" [0, 0, 10] 10)
  "_iEx" ::  "Time ⇒ iT ⇒ (Time ⇒ bool) ⇒ bool" ("(3◇ _ _./ _)" [0, 0, 10] 10)
translations
  "□ t I. P" ⇌ "CONST iAll I (λt. P)"
  "◇ t I. P" ⇌ "CONST iEx I (λt. P)"

text ‹Future temporal operator: Next›
definition iNext :: "Time ⇒ iT ⇒ (Time ⇒ bool) ⇒ bool"      ― ‹Next›
  where "iNext t0 I P ≡ P (inext t0 I)"

text ‹Past temporal operator: Last/Previous›
definition iLast :: "Time ⇒ iT ⇒ (Time ⇒ bool) ⇒ bool"      ― ‹Last›
  where "iLast t0 I P ≡ P (iprev t0 I)"

syntax
  "_iNext" :: "Time ⇒ Time ⇒ iT ⇒ (Time ⇒ bool) ⇒ bool" ("(3○ _ _ _./ _)" [0, 0, 10] 10)
  "_iLast" :: "Time ⇒ Time ⇒ iT ⇒ (Time ⇒ bool) ⇒ bool" ("(3⊖ _ _ _./ _)" [0, 0, 10] 10)
translations
  "○ t t0 I. P" ⇌ "CONST iNext t0 I (λt. P)"
  "⊖ t t0 I. P" ⇌ "CONST iLast t0 I (λt. P)"

lemma "○ t 10 [0…]. (t + 10 > 10)"
by (simp add: iNext_def iT_inext_if)

text ‹The following versions of Next and Last operator differ in the cases
  where no next/previous element exists or specified time point is not in interval:
  the weak versions return @{term True} and the strong versions return @{term False}.›

definition iNextWeak :: "Time ⇒ iT ⇒ (Time ⇒ bool) ⇒ bool"      ― ‹Weak Next›
  where "iNextWeak t0 I P  ≡ (□ t {inext t0 I} ↓> t0. P t)"

definition iNextStrong :: "Time ⇒ iT ⇒ (Time ⇒ bool) ⇒ bool"      ― ‹Strong Next›
  where "iNextStrong t0 I P ≡ (◇ t {inext t0 I} ↓> t0. P t)"

definition iLastWeak :: "Time ⇒ iT ⇒ (Time ⇒ bool) ⇒ bool"      ― ‹Weak Last›
  where "iLastWeak t0 I P   ≡ (□ t {iprev t0 I} ↓< t0. P t)"

definition iLastStrong :: "Time ⇒ iT ⇒ (Time ⇒ bool) ⇒ bool"      ― ‹Strong Last›
  where "iLastStrong t0 I P ≡ (◇ t {iprev t0 I} ↓< t0. P t)"

syntax
  "_iNextWeak"   :: "Time ⇒ Time ⇒ iT ⇒ (Time ⇒ bool) ⇒ bool" ("(3○⇩W _ _ _./ _)" [0, 0, 10] 10)
  "_iNextStrong" :: "Time ⇒ Time ⇒ iT ⇒ (Time ⇒ bool) ⇒ bool" ("(3○⇩S _ _ _./ _)" [0, 0, 10] 10)
  "_iLastWeak"   :: "Time ⇒ Time ⇒ iT ⇒ (Time ⇒ bool) ⇒ bool" ("(3⊖⇩W _ _ _./ _)" [0, 0, 10] 10)
  "_iLastStrong" :: "Time ⇒ Time ⇒ iT ⇒ (Time ⇒ bool) ⇒ bool" ("(3⊖⇩S _ _ _./ _)" [0, 0, 10] 10)
translations
  "○⇩W t t0 I. P" ⇌ "CONST iNextWeak t0 I (λt. P)"
  "○⇩S t t0 I. P" ⇌ "CONST iNextStrong t0 I (λt. P)"
  "⊖⇩W t t0 I. P" ⇌ "CONST iLastWeak t0 I (λt. P)"
  "⊖⇩S t t0 I. P" ⇌ "CONST iLastStrong t0 I (λt. P)"


text ‹Some examples for Next and Last operator›

lemma "○ t 5 [0…,10]. ([0::int,10,20,30,40,50,60,70,80,90] ! t < 80)"
by (simp add: iNext_def iIN_inext)

lemma "⊖ t 5 [0…,10]. ([0::int,10,20,30,40,50,60,70,80,90] ! t < 80)"
by (simp add: iLast_def iIN_iprev)


text ‹Temporal Until operator›
definition iUntil :: "iT ⇒ (Time ⇒ bool) ⇒ (Time ⇒ bool) ⇒ bool"      ― ‹Until›
  where "iUntil I P Q ≡ ◇ t I. Q t ∧ (□ t' (I ↓< t). P t')"

text ‹Temporal Since operator (past operator corresponding to Until)›
definition iSince :: "iT ⇒ (Time ⇒ bool) ⇒ (Time ⇒ bool) ⇒ bool"      ― ‹Since›
  where "iSince I P Q ≡ ◇ t I. Q t ∧ (□ t' (I ↓> t). P t')"

syntax
  "_iUntil" ::  "Time ⇒ Time ⇒ iT ⇒ (Time ⇒ bool) ⇒ (Time ⇒ bool) ⇒ bool" 
    ("(_./ _ (3𝒰 _ _)./ _)" [10, 0, 0, 0, 10] 10)
  "_iSince" ::  "Time ⇒ Time ⇒ iT ⇒ (Time ⇒ bool) ⇒ (Time ⇒ bool) ⇒ bool" 
    ("(_./ _ (3𝒮 _ _)./ _)" [10, 0, 0, 0, 10] 10)
translations
  "P. t 𝒰 t' I. Q" ⇌ "CONST iUntil I (λt. P) (λt'. Q)"
  "P. t 𝒮 t' I. Q" ⇌ "CONST iSince I (λt. P) (λt'. Q)"

definition iWeakUntil :: "iT ⇒ (Time ⇒ bool) ⇒ (Time ⇒ bool) ⇒ bool"      ― ‹Weak Until/Wating-for/Unless›
  where "iWeakUntil I P Q ≡ (□ t I. P t) ∨ (◇ t I. Q t ∧ (□ t' (I ↓< t). P t'))"

definition iWeakSince :: "iT ⇒ (Time ⇒ bool) ⇒ (Time ⇒ bool) ⇒ bool"      ― ‹Weak Since/Back-to›
  where "iWeakSince I P Q ≡ (□ t I. P t) ∨ (◇ t I. Q t ∧ (□ t' (I ↓> t). P t'))"

syntax
  "_iWeakUntil" ::  "Time ⇒ Time ⇒ iT ⇒ (Time ⇒ bool) ⇒ (Time ⇒ bool) ⇒ bool" 
    ("(_./ _ (3𝒲 _ _)./ _)" [10, 0, 0, 0, 10] 10)
  "_iWeakSince" ::  "Time ⇒ Time ⇒ iT ⇒ (Time ⇒ bool) ⇒ (Time ⇒ bool) ⇒ bool" 
    ("(_./ _ (3ℬ _ _)./ _)" [10, 0, 0, 0, 10] 10)
translations
  "P. t 𝒲 t' I. Q" ⇌ "CONST iWeakUntil I (λt. P) (λt'. Q)"
  "P. t ℬ t' I. Q" ⇌ "CONST iWeakSince I (λt. P) (λt'. Q)"


definition iRelease :: "iT ⇒ (Time ⇒ bool) ⇒ (Time ⇒ bool) ⇒ bool"      ― ‹Release›
  where "iRelease I P Q ≡ (□ t I. Q t) ∨ (◇ t I. P t ∧ (□ t' (I ↓≤ t). Q t'))"

definition iTrigger :: "iT ⇒ (Time ⇒ bool) ⇒ (Time ⇒ bool) ⇒ bool"      ― ‹Trigger›
  where "iTrigger I P Q ≡ (□ t I. Q t) ∨ (◇ t I. P t ∧ (□ t' (I ↓≥ t). Q t'))"

syntax
  "_iRelease" ::  "Time ⇒ Time ⇒ iT ⇒ (Time ⇒ bool) ⇒ (Time ⇒ bool) ⇒ bool" 
    ("(_./ _ (3ℛ _ _)./ _)" [10, 0, 0, 0, 10] 10)
  "_iTrigger" ::  "Time ⇒ Time ⇒ iT ⇒ (Time ⇒ bool) ⇒ (Time ⇒ bool) ⇒ bool" 
    ("(_./ _ (3𝒯 _ _)./ _)" [10, 0, 0, 0, 10] 10)
translations
  "P. t ℛ t' I. Q" ⇌ "CONST iRelease I (λt. P) (λt'. Q)"
  "P. t 𝒯 t' I. Q" ⇌ "CONST iTrigger I (λt. P) (λt'. Q)"


lemmas iTL_Next_defs =
  iNext_def iLast_def
  iNextWeak_def iLastWeak_def
  iNextStrong_def iLastStrong_def
lemmas iTL_defs = 
  iAll_def iEx_def
  iUntil_def iSince_def
  iWeakUntil_def iWeakSince_def
  iRelease_def iTrigger_def
  iTL_Next_defs
(* Like in Set.thy *)
(* To avoid eta-contraction of body: *)
print_translation ‹
 [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax iAll} @{syntax_const "_iAll"},
  Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax iEx} @{syntax_const "_iEx"}]
›

print_translation ‹
let
  fun btr' syn [i,Abs abs,Abs abs'] =
    let
      val (t,P) = Syntax_Trans.atomic_abs_tr' abs;
      val (t',Q) = Syntax_Trans.atomic_abs_tr' abs'
    in Syntax.const syn $ P $ t $ t' $ i $ Q end
in
 [(@{const_syntax "iUntil"}, K (btr' "_iUntil")),
  (@{const_syntax "iSince"}, K (btr' "_iSince"))]
end
›

print_translation ‹
let
  fun btr' syn [i,Abs abs,Abs abs'] =
    let
      val (t,P) = Syntax_Trans.atomic_abs_tr' abs;
      val (t',Q) = Syntax_Trans.atomic_abs_tr' abs'
    in Syntax.const syn $ P $ t $ t' $ i $ Q end
in
 [(@{const_syntax "iWeakUntil"}, K (btr' "_iWeakUntil")),
  (@{const_syntax "iWeakSince"}, K (btr' "_iWeakSince"))]
end
›

print_translation ‹
let
  fun btr' syn [i,Abs abs,Abs abs'] =
    let
      val (t,P) = Syntax_Trans.atomic_abs_tr' abs;
      val (t',Q) = Syntax_Trans.atomic_abs_tr' abs'
    in Syntax.const syn $ P $ t $ t' $ i $ Q end
in
 [(@{const_syntax "iRelease"}, K (btr' "_iRelease")),
  (@{const_syntax "iTrigger"}, K (btr' "_iTrigger"))]
end
›


subsection ‹Basic lemmata for temporal operators›

subsubsection ‹Intro/elim rules›

lemma 
  iexI[intro]:      "⟦ P t; t ∈ I ⟧ ⟹ ◇ t I. P t" and
  rev_iexI[intro?]: "⟦ t ∈ I; P t ⟧ ⟹ ◇ t I. P t" and
  iexE[elim!]:      "⟦ ◇ t I. P t; ⋀t. ⟦ t ∈ I; P t ⟧ ⟹ Q ⟧ ⟹ Q"
by (unfold iEx_def, blast+)

lemma
  iallI[intro!]: "(⋀t. t ∈ I ⟹ P t) ⟹ □ t I. P t" and
  ispec[dest?]: "⟦ □ t I. P t; t ∈ I ⟧ ⟹ P t" and
  iallE[elim]: "⟦ □ t I. P t; P t ⟹ Q; t ∉ I ⟹ Q ⟧ ⟹ Q"
by (unfold iAll_def, blast+)

lemma
  iuntilI[intro]: "
    ⟦ Q t; (⋀t'. t' ∈ I ↓< t⟹ P t'); t ∈ I ⟧ ⟹ P t'. t' 𝒰 t I. Q t" and
  rev_iuntilI[intro?]: "
    ⟦ t ∈ I; Q t; (⋀t'. t' ∈ I ↓< t⟹ P t') ⟧ ⟹ P t'. t' 𝒰 t I. Q t"
by (unfold iUntil_def, blast+)

lemma
  iuntilE[elim]: "
    ⟦ P' t'. t' 𝒰 t I. P t; ⋀t. ⟦ t ∈ I; P t ⟧ ⟹ Q ⟧ ⟹ Q"
by (unfold iUntil_def, blast)

lemma
  isinceI[intro]: "
    ⟦ Q t; (⋀t'. t' ∈ I ↓> t⟹ P t'); t ∈ I ⟧ ⟹ P t'. t' 𝒮 t I. Q t" and
  rev_isinceI[intro?]: "
    ⟦ t ∈ I; Q t; (⋀t'. t' ∈ I ↓> t⟹ P t') ⟧ ⟹ P t'. t' 𝒮 t I. Q t"
by (unfold iSince_def, blast+)
lemma
  isinceE[elim]: "
    ⟦ P' t'. t' 𝒮 t I. P t; ⋀t. ⟦ t ∈ I; P t ⟧ ⟹ Q ⟧ ⟹ Q"
by (unfold iSince_def, blast)


subsubsection ‹Rewrite rules for trivial simplification›

lemma iall_triv[simp]: "(□ t I. P) = ((∃t. t ∈ I) ⟶ P)"
by (simp add: iAll_def)

lemma iex_triv[simp]: "(◇ t I. P) = ((∃t. t ∈ I) ∧ P)"
by (simp add: iEx_def)

lemma iex_conjL1: "
  (◇ t1 I1. (P1 t1 ∧ (◇ t2 I2. P2 t1 t2))) = 
  (◇ t1 I1. ◇ t2 I2. P1 t1 ∧ P2 t1 t2)"
by blast

lemma iex_conjR1: "
  (◇ t1 I1. ((◇ t2 I2. P2 t1 t2) ∧ P1 t1)) =
  (◇ t1 I1. ◇ t2 I2. P2 t1 t2 ∧ P1 t1)"
by blast

lemma iex_conjL2: "
  (◇ t1 I1. (P1 t1 ∧ (◇ t2 (I2 t1). P2 t1 t2))) = 
  (◇ t1 I1. ◇ t2 (I2 t1). P1 t1 ∧ P2 t1 t2)"
by blast

lemma iex_conjR2: "
  (◇ t1 I1. ((◇ t2 (I2 t1). P2 t1 t2) ∧ P1 t1)) = 
  (◇ t1 I1. ◇ t2 (I2 t1). P2 t1 t2 ∧ P1 t1)"
by blast

lemma iex_commute: "
  (◇ t1 I1. ◇ t2 I2. P t1 t2) = 
  (◇ t2 I2. ◇ t1 I1. P t1 t2)"
by blast

lemma iall_conjL1: "
  I2 ≠ {} ⟹
  (□ t1 I1. (P1 t1 ∧ (□ t2 I2. P2 t1 t2))) = 
  (□ t1 I1. □ t2 I2. P1 t1 ∧ P2 t1 t2)"
by blast

lemma iall_conjR1: "
  I2 ≠ {} ⟹
  (□ t1 I1. ((□ t2 I2. P2 t1 t2) ∧ P1 t1)) =
  (□ t1 I1. □ t2 I2. P2 t1 t2 ∧ P1 t1)"
by blast

lemma iall_conjL2: "
  □ t1 I1. I2 t1 ≠ {} ⟹
  (□ t1 I1. (P1 t1 ∧ (□ t2 (I2 t1). P2 t1 t2))) = 
  (□ t1 I1. □ t2 (I2 t1). P1 t1 ∧ P2 t1 t2)"
by blast

lemma iall_conjR2: "
  □ t1 I1. I2 t1 ≠ {} ⟹
  (□ t1 I1. ((□ t2 (I2 t1). P2 t1 t2) ∧ P1 t1)) = 
  (□ t1 I1. □ t2 (I2 t1). P2 t1 t2 ∧ P1 t1)"
by blast

lemma iall_commute: "
  (□ t1 I1. □ t2 I2. P t1 t2) = 
  (□ t2 I2. □ t1 I1. P t1 t2)"
by blast

lemma iall_conj_distrib: "
  (□ t I. P t ∧ Q t) = ((□ t I. P t) ∧ (□ t I. Q t))"
by blast

lemma iex_disj_distrib: "
  (◇ t I. P t ∨ Q t) = ((◇ t I. P t) ∨ (◇ t I. Q t))"
by blast

lemma iall_conj_distrib2: "
  (□ t1 I1. □ t2 (I2 t1). P t1 t2 ∧ Q t1 t2) = 
  ((□ t1 I1. □ t2 (I2 t1). P t1 t2) ∧ (□ t1 I1. □ t2 (I2 t1). Q t1 t2))"
by blast

lemma iex_disj_distrib2: "
  (◇ t1 I1. ◇ t2 (I2 t1). P t1 t2 ∨ Q t1 t2) = 
  ((◇ t1 I1. ◇ t2 (I2 t1). P t1 t2) ∨ (◇ t1 I1. ◇ t2 (I2 t1). Q t1 t2))"
by blast

lemma iUntil_disj_distrib: "
  (P t1. t1 𝒰 t2 I. (Q1 t2 ∨ Q2 t2)) = ((P t1. t1 𝒰 t2 I. Q1 t2) ∨ (P t1. t1 𝒰 t2 I. Q2 t2))"
unfolding iUntil_def by blast

lemma iSince_disj_distrib: "
  (P t1. t1 𝒮 t2 I. (Q1 t2 ∨ Q2 t2)) = ((P t1. t1 𝒮 t2 I. Q1 t2) ∨ (P t1. t1 𝒮 t2 I. Q2 t2))"
unfolding iSince_def by blast

lemma 
  iNext_iff: "(○ t t0 I. P t) = (□ t […0] ⊕ (inext t0 I). P t)" and
  iLast_iff: "(⊖ t t0 I. P t) = (□ t […0] ⊕ (iprev t0 I). P t)"
by (fastforce simp: iTL_Next_defs iT_add iIN_0)+

lemma 
  iNext_iEx_iff: "(○ t t0 I. P t) = (◇ t […0] ⊕ (inext t0 I). P t)" and
  iLast_iEx_iff: "(⊖ t t0 I. P t) = (◇ t […0] ⊕ (iprev t0 I). P t)"
by (fastforce simp: iTL_Next_defs iT_add iIN_0)+


lemma inext_singleton_cut_greater_not_empty_iff: "
  ({inext t0 I} ↓> t0 ≠ {}) = (I ↓> t0 ≠ {} ∧ t0 ∈ I)"
apply (simp add: cut_greater_singleton)
apply (case_tac "t0 ∈ I")
 prefer 2
 apply (simp add: not_in_inext_fix)
apply simp
apply (case_tac "I ↓> t0 = {}")
 apply (simp add: cut_greater_empty_iff inext_all_le_fix)
apply (simp add: cut_greater_not_empty_iff inext_mono2)
done

lemma iprev_singleton_cut_less_not_empty_iff: "
  ({iprev t0 I} ↓< t0 ≠ {}) = (I ↓< t0 ≠ {} ∧ t0 ∈ I)"
apply (simp add: cut_less_singleton)
apply (case_tac "t0 ∈ I")
 prefer 2
 apply (simp add: not_in_iprev_fix)
apply simp
apply (case_tac "I ↓< t0 = {}")
 apply (simp add: cut_less_empty_iff iprev_all_ge_fix)
apply (simp add: cut_less_not_empty_iff iprev_mono2)
done

lemma inext_singleton_cut_greater_empty_iff: "
  ({inext t0 I} ↓> t0 = {}) = (I ↓> t0 = {} ∨ t0 ∉ I)"
apply (subst Not_eq_iff[symmetric])
apply (simp add: inext_singleton_cut_greater_not_empty_iff)
done

lemma iprev_singleton_cut_less_empty_iff: "
  ({iprev t0 I} ↓< t0 = {}) = (I ↓< t0 = {} ∨ t0 ∉ I)"
apply (subst Not_eq_iff[symmetric])
apply (simp add: iprev_singleton_cut_less_not_empty_iff)
done

lemma iNextWeak_iff : "(○⇩W t t0 I. P t) = ((○ t t0 I. P t) ∨ (I ↓> t0 = {}) ∨ t0 ∉ I)"
apply (unfold iTL_defs)
apply (simp add: inext_singleton_cut_greater_empty_iff[symmetric] cut_greater_singleton)
done

lemma iNextStrong_iff : "(○⇩S t t0 I. P t) = ((○ t t0 I. P t) ∧ (I ↓> t0 ≠ {}) ∧ t0 ∈ I)"
apply (unfold iTL_defs)
apply (simp add: inext_singleton_cut_greater_not_empty_iff[symmetric] cut_greater_singleton)
done

lemma iLastWeak_iff : "(⊖⇩W t t0 I. P t) = ((⊖ t t0 I. P t) ∨ (I ↓< t0 = {}) ∨ t0 ∉ I)"
apply (unfold iTL_defs)
apply (simp add: iprev_singleton_cut_less_empty_iff[symmetric] cut_less_singleton)
done

lemma iLastStrong_iff : "(⊖⇩S t t0 I. P t) = ((⊖ t t0 I. P t) ∧ (I ↓< t0 ≠ {}) ∧ t0 ∈ I)"
apply (unfold iTL_defs)
apply (simp add: iprev_singleton_cut_less_not_empty_iff[symmetric] cut_less_singleton)
done

lemmas iTL_Next_iff =
  iNext_iff iLast_iff
  iNextWeak_iff iNextStrong_iff
  iLastWeak_iff iLastStrong_iff


lemma 
  iNext_iff_singleton       : "(○ t t0 I. P t) = (□ t {inext t0 I}. P t)" and
  iLast_iff_singleton       : "(⊖ t t0 I. P t) = (□ t {iprev t0 I}. P t)"
by (fastforce simp: iTL_Next_defs iT_add iIN_0)+
lemmas iNextLast_iff_singleton = iNext_iff_singleton iLast_iff_singleton

lemma 
  iNext_iEx_iff_singleton   : "(○ t t0 I. P t) = (◇ t {inext t0 I}. P t)" and
  iLast_iEx_iff_singleton   : "(⊖ t t0 I. P t) = (◇ t {iprev t0 I}. P t)"
by (fastforce simp: iTL_Next_defs iT_add iIN_0)+


lemma 
  iNextWeak_iAll_conv:  "(○⇩W t t0 I. P t) = (□ t ({inext t0 I} ↓> t0). P t)" and
  iNextStrong_iEx_conv: "(○⇩S t t0 I. P t) = (◇ t ({inext t0 I} ↓> t0). P t)" and
  iLastWeak_iAll_conv:  "(⊖⇩W t t0 I. P t) = (□ t ({iprev t0 I} ↓< t0). P t)" and
  iLastStrong_iEx_conv: "(⊖⇩S t t0 I. P t) = (◇ t ({iprev t0 I} ↓< t0). P t)"
by (simp_all add: iTL_Next_defs)


lemma 
  iAll_True[simp]: "□ t I. True" and
  iAll_False[simp]: "(□ t I. False) = (I = {})" and
  iEx_True[simp]: "(◇ t I. True) = (I ≠ {})" and
  iEx_False[simp]: "¬ (◇ t I. False)" 
by blast+

lemma empty_iff_iAll_False:   "(I = {}) = (□ t I. False)" by blast
lemma not_empty_iff_iEx_True: "(I ≠ {}) = (◇ t I. True)" by blast

lemma 
  iNext_True: "○ t t0 I. True" and
  iNextWeak_True: "(○⇩W t t0 I. True)" and
  iNext_False: "¬ (○ t t0 I. False)" and
  iNextStrong_False: "¬ (○⇩S t t0 I. False)"
by (simp_all add: iTL_defs)

lemma
  iNextStrong_True: "(○⇩S t t0 I. True) = (I ↓> t0 ≠ {} ∧ t0 ∈ I)" and
  iNextWeak_False: "(¬ (○⇩W t t0 I. False)) = (I ↓> t0 ≠ {} ∧ t0 ∈ I)"
by (simp_all add: iTL_defs ex_in_conv inext_singleton_cut_greater_not_empty_iff)


lemma 
  iLast_True:        "⊖ t t0 I. True" and
  iLastWeak_True:    "(⊖⇩W t t0 I. True)" and
  iLast_False:       "¬ (⊖ t t0 I. False)" and
  iLastStrong_False: "¬ (⊖⇩S t t0 I. False)"
by (simp_all add: iTL_defs)

lemma
  iLastStrong_True:  "(⊖⇩S t t0 I. True) = (I ↓< t0 ≠ {} ∧ t0 ∈ I)" and
  iLastWeak_False:   "(¬ (⊖⇩W t t0 I. False)) = (I ↓< t0 ≠ {} ∧ t0 ∈ I)"
by (simp_all add: iTL_defs ex_in_conv iprev_singleton_cut_less_not_empty_iff)

lemma iUntil_True_left[simp]: "(True. t' 𝒰 t I. Q t) = (◇ t I. Q t)" 
by blast

lemma iUntil_True[simp]: "(P t'. t' 𝒰 t I. True) = (I ≠ {})"
apply (unfold iTL_defs)
apply (rule iffI)
 apply blast
apply (rule_tac x="iMin I" in bexI)
apply (simp add: cut_less_Min_empty iMinI_ex2)+
done

lemma iUntil_False_left[simp]: "(False. t' 𝒰 t I. Q t) = (I ≠ {} ∧ Q (iMin I))"
apply (case_tac "I = {}", blast)
apply (simp add: iTL_defs)
apply (rule iffI)
 apply clarsimp
 apply (drule iMin_equality)
  apply (simp add: cut_less_empty_iff)
 apply simp
apply (rule_tac x="iMin I" in bexI)
 apply (simp add: cut_less_Min_empty)
apply (simp add: iMinI_ex2)
done

lemma iUntil_False[simp]: "¬ (P t'. t' 𝒰 t I. False)" 
by blast

lemma iSince_True_left[simp]: "(True. t' 𝒮 t I. Q t) = (◇ t I. Q t)" 
by blast

lemma iSince_True_if: "
  (P t'. t' 𝒮 t I. True) = 
  (if finite I then I ≠ {} else ◇ t1 I. □ t2 (I ↓> t1). P t2)"
apply (clarsimp simp: iTL_defs)
apply (rule iffI)
 apply clarsimp
apply (rule_tac x="Max I" in bexI)
 apply (simp add: cut_greater_Max_empty)
apply simp
done

corollary iSince_True_finite[simp]: "finite I ⟹ (P t'. t' 𝒮 t I. True) = (I ≠ {})"
by (simp add: iSince_True_if)

lemma iSince_False_left[simp]: "(False. t' 𝒮 t I. Q t) = (finite I ∧ I ≠ {} ∧ Q (Max I))"
apply (simp add: iTL_defs)
apply (case_tac "I = {}", simp)
apply (case_tac "infinite I")
 apply (simp add: nat_cut_greater_infinite_not_empty)
apply (rule iffI)
 apply clarsimp
 apply (drule Max_equality)
   apply simp
  apply (simp add: cut_greater_empty_iff)
 apply simp
apply (rule_tac x="Max I" in bexI)
 apply (simp add: cut_greater_Max_empty)
apply simp
done

lemma iSince_False[simp]: "¬ (P t'. t' 𝒮 t I. False)"
by blast

lemma iWeakUntil_True_left[simp]: "True. t' 𝒲 t I. Q t"
by (simp add: iWeakUntil_def)

lemma iWeakUntil_True[simp]: "P t'. t' 𝒲 t I. True"
apply (simp add: iTL_defs)
apply (case_tac "I = {}", simp)
apply (rule disjI2)
apply (rule_tac x="iMin I" in bexI)
 apply (simp add: cut_less_Min_empty)
apply (simp add: iMinI_ex2)
done

lemma iWeakUntil_False_left[simp]: "(False. t' 𝒲 t I. Q t) = (I = {} ∨ Q (iMin I))"
apply (simp add: iTL_defs)
apply (case_tac "I = {}", simp)
apply (rule iffI)
 apply (clarsimp simp: cut_less_empty_iff)
 apply (frule iMin_equality)
 apply simp+
apply (rule_tac x="iMin I" in bexI)
 apply (simp add: cut_less_Min_empty)
apply (simp add: iMinI_ex2)
done

lemma iWeakUntil_False[simp]: "(P t'. t' 𝒲 t I. False) = (□ t I. P t)"
by (simp add: iWeakUntil_def)

lemma iWeakSince_True_left[simp]: "True. t' ℬ t I. Q t"
by (simp add: iTL_defs)

lemma iWeakSince_True_disj: "
  (P t'. t' ℬ t I. True) = 
  (I = {} ∨ (◇ t1 I. □ t2 (I ↓> t1). P t2))"
unfolding iTL_defs by blast

lemma iWeakSince_True_finite[simp]: "finite I ⟹ (P t'. t' ℬ t I. True)"
apply (simp add: iTL_defs)
apply (case_tac "I = {}", simp)
apply (rule disjI2)
apply (rule_tac x="Max I" in bexI)
 apply (simp add: cut_greater_Max_empty)
apply simp
done

lemma iWeakSince_False_left[simp]: "(False. t' ℬ t I. Q t) = (I = {} ∨ (finite I ∧ Q (Max I)))"
apply (simp add: iTL_defs)
apply (case_tac "I = {}", simp)
apply (case_tac "infinite I")
 apply (simp add: nat_cut_greater_infinite_not_empty)
apply (rule iffI)
 apply clarsimp
 apply (drule Max_equality)
   apply simp
  apply (simp add: cut_greater_empty_iff)
 apply simp
apply simp
apply (rule_tac x="Max I" in bexI)
 apply (simp add: cut_greater_Max_empty)
apply simp
done

lemma iWeakSince_False[simp]: "(P t'. t' ℬ t I. False) = (□ t I. P t)"
by (simp add: iWeakSince_def)

lemma iRelease_True_left[simp]: "(True. t' ℛ t I. Q t) = (I = {} ∨ Q (iMin I))"
apply (simp add: iTL_defs)
apply (case_tac "I = {}", simp)
apply (rule iffI)
 apply (erule disjE)
  apply (blast intro: iMinI2_ex2)
 apply clarsimp
 apply (drule_tac x="iMin I" in bspec)
  apply (blast intro: iMinI_ex2)
 apply simp
apply (rule disjI2)
apply (rule_tac x="iMin I" in bexI)
 apply fastforce
apply (simp add: iMinI_ex2)
done

lemma iRelease_True[simp]: "P t'. t' ℛ t I. True"
by (simp add: iTL_defs)

lemma iRelease_False_left[simp]: "(False. t' ℛ t I. Q t) = (□ t I. Q t)"
by (simp add: iTL_defs)

lemma iRelease_False[simp]: "(P t'. t' ℛ t I. False) = (I = {})"
unfolding iTL_defs by blast

lemma iTrigger_True_left[simp]: "(True. t' 𝒯 t I. Q t) = (I = {} ∨ (◇ t1 I. □ t2 (I ↓≥ t1). Q t2))"
unfolding iTL_defs by blast

lemma iTrigger_True[simp]: "P t'. t' 𝒯 t I. True"
by (simp add: iTL_defs)

lemma iTrigger_False_left[simp]: "(False. t' 𝒯 t I. Q t) = (□ t I. Q t)"
by (simp add: iTL_defs)

lemma iTrigger_False[simp]: "(P t'. t' 𝒯 t I. False) = (I = {})"
unfolding iTL_defs by blast

lemma 
  iUntil_TrueTrue[simp]: "(True. t' 𝒰 t I. True) = (I ≠ {})" and
  iSince_TrueTrue[simp]: "(True. t' 𝒮 t I. True) = (I ≠ {})" and
  iWeakUntil_TrueTrue[simp]: "True. t' 𝒲 t I. True" and
  iWeakSince_TrueTrue[simp]: "True. t' ℬ t I. True" and
  iRelease_TrueTrue[simp]: "True. t' ℛ t I. True" and
  iTrigger_TrueTrue[simp]: "True. t' 𝒯 t I. True"
by (simp_all add: iTL_defs ex_in_conv)


subsubsection ‹Empty sets and singletons›

lemma iAll_empty[simp]: "□ t {}. P t" by blast
lemma iEx_empty[simp]: "¬ (◇ t {}. P t)" by blast

lemma iUntil_empty[simp]: "¬ (P t0. t0 𝒰 t1 {}. Q t1)" by blast
lemma iSince_empty[simp]: "¬ (P t0. t0 𝒮 t1 {}. Q t1)" by blast
lemma iWeakUntil_empty[simp]: "P t0. t0 𝒲 t1 {}. Q t1" by (simp add: iWeakUntil_def)
lemma iWeakSince_empty[simp]: "P t0. t0 ℬ t1 {}. Q t1" by (simp add: iWeakSince_def)

lemma iRelease_empty[simp]: "P t0. t0 ℛ t1 {}. Q t1" by (simp add: iRelease_def)
lemma iTrigger_empty[simp]: "P t0. t0 𝒯 t1 {}. Q t1" by (simp add: iTrigger_def)

lemmas iTL_empty =
  iAll_empty iEx_empty
  iUntil_empty iSince_empty
  iWeakUntil_empty iWeakSince_empty
  iRelease_empty iTrigger_empty

lemma iAll_singleton[simp]: "(□ t' {t}. P t') = P t" by blast
lemma iEx_singleton[simp]: "(◇ t' {t}. P t') = P t" by blast

lemma iUntil_singleton[simp]: "(P t0. t0 𝒰 t1 {t}. Q t1) = Q t"
by (simp add: iUntil_def cut_less_singleton)

lemma iSince_singleton[simp]: "(P t0. t0 𝒮 t1 {t}. Q t1) = Q t"
by (simp add: iSince_def cut_greater_singleton)

lemma iWeakUntil_singleton[simp]: "(P t0. t0 𝒲 t1 {t}. Q t1) = (P t ∨ Q t)"
by (simp add: iWeakUntil_def cut_less_singleton)

lemma iWeakSince_singleton[simp]: "(P t0. t0 ℬ t1 {t}. Q t1) = (P t ∨ Q t)"
by (simp add: iWeakSince_def cut_greater_singleton)

lemma iRelease_singleton[simp]: "(P t0. t0 ℛ t1 {t}. Q t1) = Q t"
unfolding iRelease_def by blast

lemma iTrigger_singleton[simp]: "(P t0. t0 𝒯 t1 {t}. Q t1) = Q t"
unfolding iTrigger_def by blast

lemmas iTL_singleton =
  iAll_singleton iEx_singleton
  iUntil_singleton iSince_singleton
  iWeakUntil_singleton iWeakSince_singleton
  iRelease_singleton iTrigger_singleton


subsubsection ‹Conversions between temporal operators›

lemma iAll_iEx_conv: "(□ t I. P t) = (¬ (◇ t I. ¬ P t))" by blast
lemma iEx_iAll_conv: "(◇ t I. P t) = (¬ (□ t I. ¬ P t))" by blast

lemma not_iAll[simp]: "(¬ (□ t I. P t)) = (◇ t I. ¬ P t)" by blast
lemma not_iEx[simp]: "(¬ (◇ t I. P t)) = (□ t I. ¬ P t)" by blast

lemma iUntil_iEx_conv: "(True. t' 𝒰 t I. P t) = (◇ t I. P t)" by blast
lemma iSince_iEx_conv: "(True. t' 𝒮 t I. P t) = (◇ t I. P t)" by blast

lemma iRelease_iAll_conv: "(False. t' ℛ t I. P t) = (□ t I. P t)"
by (simp add: iRelease_def)

lemma iTrigger_iAll_conv: "(False. t' 𝒯 t I. P t) = (□ t I. P t)"
by (simp add: iTrigger_def)

lemma iWeakUntil_iUntil_conv: "(P t'. t' 𝒲 t I. Q t) = ((P t'. t' 𝒰 t I. Q t) ∨ (□ t I. P t))"
unfolding iWeakUntil_def iUntil_def by blast

lemma iWeakSince_iSince_conv: "(P t'. t' ℬ t I. Q t) = ((P t'. t' 𝒮 t I. Q t) ∨ (□ t I. P t))"
unfolding iWeakSince_def iSince_def by blast

lemma iUntil_iWeakUntil_conv: "(P t'. t' 𝒰 t I. Q t) = ((P t'. t' 𝒲 t I. Q t) ∧ (◇ t I. Q t))"
by (subst iWeakUntil_iUntil_conv, blast)

lemma iSince_iWeakSince_conv: "(P t'. t' 𝒮 t I. Q t) = ((P t'. t' ℬ t I. Q t) ∧ (◇ t I. Q t))"
by (subst iWeakSince_iSince_conv, blast)


lemma iRelease_iWeakUntil_conv: "(P t'. t' ℛ t I. Q t) = (Q t'. t' 𝒲 t I. (Q t ∧ P t))"
apply (unfold iRelease_def iWeakUntil_def)
apply (simp add: cut_le_less_conv_if)
apply blast
done

lemma iRelease_iUntil_conv: "(P t'. t' ℛ t I. Q t) = ((□ t I. Q t) ∨ (Q t'. t' 𝒰 t I. (Q t ∧ P t)))"
by (fastforce simp: iRelease_iWeakUntil_conv iWeakUntil_iUntil_conv)

lemma iTrigger_iWeakSince_conv: "(P t'. t' 𝒯 t I. Q t) = (Q t'. t' ℬ t I. (Q t ∧ P t))"
apply (unfold iTrigger_def iWeakSince_def)
apply (simp add: cut_ge_greater_conv_if)
apply blast
done

lemma iTrigger_iSince_conv: "(P t'. t' 𝒯 t I. Q t) = ((□ t I. Q t) ∨ (Q t'. t' 𝒮 t I. (Q t ∧ P t)))"
by (fastforce simp: iTrigger_iWeakSince_conv iWeakSince_iSince_conv)

lemma iRelease_not_iUntil_conv: "(P t'. t' ℛ t I. Q t) = (¬ (¬ P t'. t' 𝒰 t I. ¬ Q t))"
apply (simp only: iUntil_def iRelease_def not_iAll not_iEx de_Morgan_conj not_not)
apply (case_tac "□ t I. Q t", blast)
apply (simp (no_asm_simp))
apply clarsimp
apply (rule iffI)
 apply (elim iexE, intro iallI, rename_tac t1 t2)
 apply (case_tac "t2 ≤ t1", blast)
 apply (simp add: linorder_not_le, blast)
apply (frule_tac t=t in ispec, assumption)
apply clarsimp
apply (rule_tac t="iMin {t ∈ I. P t}" in iexI)
 prefer 2
 apply (blast intro: subsetD[OF _ iMinI_ex])
apply (rule conjI)
 apply (blast intro: iMinI2)
apply (clarsimp simp: cut_le_mem_iff, rename_tac t1 t2)
apply (drule_tac t=t2 in ispec, assumption)
apply (clarsimp simp: cut_less_mem_iff)
apply (frule_tac x=t' in order_less_le_trans, assumption)
apply (drule not_less_iMin)
apply simp
done
lemma iUntil_not_iRelease_conv: "(P t'. t' 𝒰 t I. Q t) = (¬ (¬ P t'. t' ℛ t I. ¬ Q t))"
by (simp add: iRelease_not_iUntil_conv)

text ‹The Trigger operator \isasymT is a past operator,
  so that it is used for time intervals,
  that are bounded by a current time point, and thus are finite.
  For an infinite interval
  the stated relation to the Since operator \isasymS would not be fulfilled.›
lemma iTrigger_not_iSince_conv: "finite I ⟹ (P t'. t' 𝒯 t I. Q t) = (¬ (¬ P t'. t' 𝒮 t I. ¬ Q t))"
apply (unfold iTrigger_def iSince_def)
apply (case_tac "□ t I. Q t", blast)
apply (simp (no_asm_simp))
apply clarsimp
apply (rule iffI)
 apply (elim iexE conjE, rule iallI, rename_tac t1 t2)
 apply (case_tac "t2 ≥ t1", blast)
 apply (simp add: linorder_not_le, blast)
apply (frule_tac t=t in ispec, assumption)
 apply (erule disjE, blast)
apply (erule iexE)
apply (subgoal_tac "finite {t ∈ I. P t}")
 prefer 2
 apply (blast intro: subset_finite_imp_finite)
apply (rule_tac t="Max {t ∈ I. P t}" in iexI)
 prefer 2
 apply (blast intro: subsetD[OF _ MaxI])
apply (rule conjI)
 apply (blast intro: MaxI2)
apply (clarsimp simp: cut_ge_mem_iff, rename_tac t1 t2)
apply (drule_tac t=t2 in ispec, assumption)
apply (clarsimp simp: cut_greater_mem_iff, rename_tac t')
apply (frule_tac z=t' in order_le_less_trans, assumption)
apply (drule_tac A="{t ∈ I. P t}" in not_greater_Max[rotated 1])
apply simp+
done

lemma iSince_not_iTrigger_conv: "finite I ⟹ (P t'. t' 𝒮 t I. Q t) = (¬ (¬ P t'. t' 𝒯 t I. ¬ Q t))"
by (simp add: iTrigger_not_iSince_conv)


lemma not_iUntil: "
  (¬ (P t1. t1 𝒰 t2 I. Q t2)) =
  (□ t I. (Q t ⟶ (◇ t' (I ↓< t). ¬ P t')))"
unfolding iTL_defs by blast

lemma not_iSince: "
  (¬ (P t1. t1 𝒮 t2 I. Q t2)) =
  (□ t I. (Q t ⟶ (◇ t' (I ↓> t). ¬ P t')))"
unfolding iTL_defs by blast


lemma iWeakUntil_conj_iUntil_conv: "
  (P t1. t1 𝒲 t2 I. (P t2 ∧ Q t2)) = (¬ (¬ Q t1. t1 𝒰 t2 I. ¬ P t2))"
by (simp add: iRelease_not_iUntil_conv[symmetric] iRelease_iWeakUntil_conv)

lemma iUntil_disj_iUntil_conv: "
  (P t1 ∨ Q t1. t1 𝒰 t2 I. Q t2) = 
  (P t1. t1 𝒰 t2 I. Q t2)"
apply (unfold iUntil_def)
apply (rule iffI)
 prefer 2
 apply blast
apply (clarsimp, rename_tac t1)
apply (rule_tac t="iMin {t ∈ I. Q t}" in iexI)
 apply (subgoal_tac "Q (iMin {t ∈ I. Q t})")
  prefer 2
  apply (blast intro: iMinI2)
 apply (clarsimp, rename_tac t2)
 apply (frule Collect_not_less_iMin, simp)
 apply (subgoal_tac "t2 < t1")
  prefer 2
  apply (rule order_less_le_trans, assumption)
  apply (simp add: Collect_iMin_le)
 apply blast
apply (rule subsetD[OF _ iMinI])
apply blast+
done

lemma iWeakUntil_disj_iWeakUntil_conv: "
  (P t1 ∨ Q t1. t1 𝒲 t2 I. Q t2) = 
  (P t1. t1 𝒲 t2 I. Q t2)"
apply (simp only: iWeakUntil_iUntil_conv iUntil_disj_iUntil_conv)
apply (case_tac "P t1. t1 𝒰 t2 I. Q t2", simp+)
apply (case_tac "□ t I. P t", blast)
apply (simp add: not_iUntil)
apply (clarsimp, rename_tac t1)
apply (case_tac "¬ Q t1", blast)
apply (subgoal_tac "iMin {t ∈ I. Q t} ∈ I")
 prefer 2
 apply (blast intro: subsetD[OF _ iMinI])
apply (frule_tac t="iMin {t ∈ I. Q t}" in ispec, assumption)
apply (drule mp)
 apply (blast intro: iMinI2)
apply (clarsimp, rename_tac t2)
apply (subgoal_tac "¬ Q t2")
 prefer 2
 apply (drule Collect_not_less_iMin)
 apply (simp add: cut_less_mem_iff)
apply blast
done

lemma iWeakUntil_iUntil_conj_conv: "
  (P t1. t1 𝒲 t2 I. Q t2) = 
  (¬ (¬ Q t1. t1 𝒰 t2 I. (¬ P t2 ∧ ¬ Q t2)))"
apply (subst iWeakUntil_disj_iWeakUntil_conv[symmetric])
apply (subst de_Morgan_disj[symmetric])
apply (subst iWeakUntil_conj_iUntil_conv[symmetric])
apply (simp add: conj_disj_distribR conj_disj_absorb)
done


text ‹Negation and temporal operators›
 
lemma 
  not_iNext[simp]: "(¬ (○ t t0 I. P t)) = (○ t t0 I. ¬ P t)" and
  not_iNextWeak[simp]: "(¬ (○⇩W t t0 I. P t)) = (○⇩S t t0 I. ¬ P t)" and
  not_iNextStrong[simp]: "(¬ (○⇩S t t0 I. P t)) = (○⇩W t t0 I. ¬ P t)" and
  not_iLast[simp]: "(¬ (⊖ t t0 I. P t)) = (⊖ t t0 I. ¬ P t)" and
  not_iLastWeak[simp]: "(¬ (⊖⇩W t t0 I. P t)) = (⊖⇩S t t0 I. ¬ P t)" and
  not_iLastStrong[simp]: "(¬ (⊖⇩S t t0 I. P t)) = (⊖⇩W t t0 I. ¬ P t)"
by (simp_all add: iTL_Next_defs)

lemma not_iWeakUntil: "
  (¬ (P t1. t1 𝒲 t2 I. Q t2)) =
  ((□ t I. (Q t ⟶ (◇ t' (I ↓< t). ¬ P t'))) ∧ (◇ t I. ¬ P t))"
by (simp add: iWeakUntil_iUntil_conv not_iUntil)
lemma not_iWeakSince: "
  (¬ (P t1. t1 ℬ t2 I. Q t2)) =
  ((□ t I. (Q t ⟶ (◇ t' (I ↓> t). ¬ P t'))) ∧ (◇ t I. ¬ P t))"
by (simp add: iWeakSince_iSince_conv not_iSince)

lemma not_iRelease: "
  (¬ (P t'. t' ℛ t I. Q t)) = 
  ((◇ t I. ¬ Q t) ∧ (□ t I. P t ⟶ (◇ t I ↓≤ t. ¬ Q t)))"
by (simp add: iRelease_def)

lemma not_iRelease_iUntil_conv: "
  (¬ (P t'. t' ℛ t I. Q t)) = (¬ P t'. t' 𝒰 t I. ¬ Q t)"
by (simp add: iUntil_not_iRelease_conv)

lemma not_iTrigger: "
  (¬ (P t'. t' 𝒯 t I. Q t)) = 
  ((◇ t I. ¬ Q t) ∧ (□ t I. ¬ P t ∨ (◇ t I ↓≥ t. ¬ Q t)))"
by (simp add: iTrigger_def)

lemma not_iTrigger_iSince_conv: "
  finite I ⟹ (¬ (P t'. t' 𝒯 t I. Q t)) = (¬ P t'. t' 𝒮 t I. ¬ Q t)"
by (simp add: iSince_not_iTrigger_conv)


subsubsection ‹Some implication results›

lemma all_imp_iall: "∀x. P x ⟹ □ t I. P t" by blast
lemma bex_imp_lex:  "◇ t I. P t ⟹ ∃x. P x" by blast

lemma iAll_imp_iEx: "I ≠ {} ⟹ □ t I. P t ⟹ ◇ t I. P t" by blast
lemma i_set_iAll_imp_iEx: "I ∈ i_set ⟹ □ t I. P t ⟹ ◇ t I. P t"
by (rule iAll_imp_iEx, rule i_set_imp_not_empty)

lemmas iT_iAll_imp_iEx = iT_not_empty[THEN iAll_imp_iEx]

lemma iUntil_imp_iEx: "P t1. t1 𝒰 t2 I. Q t2 ⟹ ◇ t I. Q t"
unfolding iTL_defs  by blast

lemma iSince_imp_iEx: "P t1. t1 𝒮 t2 I. Q t2 ⟹ ◇ t I. Q t"
unfolding iTL_defs  by blast

lemma iall_subset_imp_iall: "⟦ □ t B. P t; A ⊆ B ⟧ ⟹ □ t A. P t"
by blast

lemma iex_subset_imp_iex: "⟦ ◇ t A. P t; A ⊆ B ⟧ ⟹ ◇ t B. P t"
by blast

lemma iall_mp: "⟦ □ t I. P t ⟶ Q t; □ t I. P t ⟧ ⟹ □ t I. Q t" by blast
lemma iex_mp: "⟦ □ t I. P t ⟶ Q t; ◇ t I. P t ⟧ ⟹ ◇ t I. Q t" by blast


lemma iUntil_imp: "
  ⟦ P1 t1. t1 𝒰 t2 I. Q t2; □ t I. P1 t ⟶ P2 t ⟧ ⟹ P2 t1. t1 𝒰 t2 I. Q t2"
unfolding iTL_defs  by blast

lemma iSince_imp: "
  ⟦ P1 t1. t1 𝒮 t2 I. Q t2; □ t I. P1 t ⟶ P2 t ⟧ ⟹ P2 t1. t1 𝒮 t2 I. Q t2"
unfolding iTL_defs  by blast

lemma iWeakUntil_imp: "
  ⟦ P1 t1. t1 𝒲 t2 I. Q t2; □ t I. P1 t ⟶ P2 t ⟧ ⟹ P2 t1. t1 𝒲 t2 I. Q t2"
unfolding iTL_defs  by blast

lemma iWeakSince_imp: "
  ⟦ P1 t1. t1 ℬ t2 I. Q t2; □ t I. P1 t ⟶ P2 t ⟧ ⟹ P2 t1. t1 ℬ t2 I. Q t2"
unfolding iTL_defs  by blast

lemma iRelease_imp: "
  ⟦ P1 t1. t1 ℛ t2 I. Q t2; □ t I. P1 t ⟶ P2 t ⟧ ⟹ P2 t1. t1 ℛ t2 I. Q t2"
unfolding iTL_defs  by blast

lemma iTrigger_imp: "
  ⟦ P1 t1. t1 𝒯 t2 I. Q t2; □ t I. P1 t ⟶ P2 t ⟧ ⟹ P2 t1. t1 𝒯 t2 I. Q t2"
unfolding iTL_defs  by blast


lemma iMin_imp_iUntil: "
  ⟦ I ≠ {}; Q (iMin I) ⟧ ⟹ P t'. t' 𝒰 t I. Q t"
apply (unfold iUntil_def)
apply (rule_tac t="iMin I" in iexI)
 apply (simp add: cut_less_Min_empty)
apply (blast intro: iMinI_ex2)
done

lemma Max_imp_iSince: "
  ⟦ finite I; I ≠ {}; Q (Max I) ⟧ ⟹ P t'. t' 𝒮 t I. Q t"
apply (unfold iSince_def)
apply (rule_tac t="Max I" in iexI)
 apply (simp add: cut_greater_Max_empty)
apply (blast intro: Max_in)
done


subsubsection ‹Congruence rules for temporal operators' predicates›

lemma iAll_cong: "□ t I. f t = g t ⟹ (□ t I. P (f t) t) = (□ t I. P (g t) t)"
unfolding iTL_defs by simp

lemma iEx_cong: "□ t I. f t = g t ⟹ (◇ t I. P (f t) t) = (◇ t I. P (g t) t)"
unfolding iTL_defs by simp

lemma iUntil_cong1: "
  □ t I. f t = g t ⟹ 
  (P (f t1) t1. t1 𝒰 t2 I. Q t2) = (P (g t1) t1. t1 𝒰 t2 I. Q t2)"
apply (unfold iUntil_def)
apply (rule iEx_cong)
apply (rule iallI)
apply (rule_tac f="λx. (Q t ∧ x)" in arg_cong, rename_tac t)
apply (rule iAll_cong[OF iall_subset_imp_iall[OF _ cut_less_subset]])
apply (rule iallI, rename_tac t')
apply (drule_tac t=t' in ispec)
apply simp+
done

lemma iUntil_cong2: "
  □ t I. f t = g t ⟹ 
  (P t1. t1 𝒰 t2 I. Q (f t2) t2) = (P t1. t1 𝒰 t2 I. Q (g t2) t2)"
apply (unfold iUntil_def)
apply (rule iEx_cong)
apply (rule iallI, rename_tac t)
apply (drule_tac t=t in ispec)
apply simp+
done

lemma iSince_cong1: "
  □ t I. f t = g t ⟹ 
  (P (f t1) t1. t1 𝒮 t2 I. Q t2) = (P (g t1) t1. t1 𝒮 t2 I. Q t2)"
apply (unfold iSince_def)
apply (rule iEx_cong)
apply (rule iallI, rename_tac t)
apply (rule_tac f="λx. (Q t ∧ x)" in arg_cong)
apply (rule iAll_cong[OF iall_subset_imp_iall[OF _ cut_greater_subset]])
apply (rule iallI, rename_tac t')
apply (drule_tac t=t' in ispec)
apply simp+
done

lemma iSince_cong2: "
  □ t I. f t = g t ⟹ 
  (P t1. t1 𝒮 t2 I. Q (f t2) t2) = (P t1. t1 𝒮 t2 I. Q (g t2) t2)"
apply (unfold iSince_def)
apply (rule iEx_cong)
apply (rule iallI, rename_tac t)
apply (drule_tac t=t in ispec)
apply simp+
done


lemma bex_subst: "
  ∀x∈A. P x ⟶ (Q x = Q' x) ⟹
  (∃x∈A. P x ∧ Q x) = (∃x∈A. P x ∧ Q' x)" 
by blast

lemma iEx_subst: "
  □ t I. P t ⟶ (Q t = Q' t) ⟹
  (◇ t I. P t ∧ Q t) = (◇ t I. P t ∧ Q' t)"
by blast


subsubsection ‹Temporal operators with set unions/intersections and subsets›

lemma iAll_subset: "⟦ A ⊆ B; □ t B. P t ⟧ ⟹ □ t A. P t"
by (rule iall_subset_imp_iall)

lemma iEx_subset: "⟦ A ⊆ B; ◇ t A. P t ⟧ ⟹ ◇ t B. P t"
by (rule iex_subset_imp_iex)

lemma iUntil_append: "
  ⟦ finite A; Max A ≤ iMin B ⟧ ⟹
  P t1. t1 𝒰 t2 A. Q t2 ⟹ P t1. t1 𝒰 t2 (A ∪ B). Q t2"
apply (case_tac "A = {}", simp)
apply (unfold iUntil_def)
apply (rule iEx_subset[OF Un_upper1])
apply (rule_tac f="λt. A ↓< t" and g="λt. (A ∪ B) ↓< t" in subst[OF iEx_cong, rule_format])
 apply (clarsimp simp: cut_less_Un, rename_tac t t')
 apply (cut_tac t=t and I=B in cut_less_Min_empty)
 apply simp+
done

lemma iSince_prepend: "
  ⟦ finite A; Max A ≤ iMin B ⟧ ⟹
  P t1. t1 𝒮 t2 B. Q t2 ⟹ P t1. t1 𝒮 t2 (A ∪ B). Q t2"
apply (case_tac "B = {}", simp)
apply (unfold iSince_def)
apply (rule iEx_subset[OF Un_upper2])
apply (rule_tac f="λt. B ↓> t" and g="λt. (A ∪ B) ↓> t" in subst[OF iEx_cong, rule_format])
 apply (clarsimp simp: cut_greater_Un, rename_tac t t')
 apply (cut_tac t=t and I=A in cut_greater_Max_empty)
 apply (simp add: iMin_ge_iff)+
done

lemma 
  iAll_union: "⟦ □ t A. P t; □ t B. P t ⟧ ⟹ □ t (A ∪ B). P t" and
  iAll_union_conv: "(□ t A ∪ B. P t) = ((□ t A. P t) ∧ (□ t B. P t))"
by blast+

lemma 
  iEx_union: "(◇ t A. P t) ∨ (◇ t B. P t) ⟹ ◇ t (A ∪ B). P t" and
  iEx_union_conv: "(◇ t (A ∪ B). P t) = ((◇ t A. P t) ∨ (◇ t B. P t))" 
by blast+

lemma iAll_inter: "(□ t A. P t) ∨ (□ t B. P t) ⟹ □ t (A ∩ B). P t" by blast

lemma not_iEx_inter: "
  ∃A B P. (◇ t A. P t) ∧ (◇ t B. P t) ∧ ¬ (◇ t (A ∩ B). P t)"
by (rule_tac x="{0}" in exI, rule_tac x="{Suc 0}" in exI, blast)

lemma 
  iAll_insert: "⟦ P t; □ t I. P t ⟧ ⟹ □ t' (insert t I). P t'" and
  iAll_insert_conv: "(□ t' (insert t I). P t') = (P t ∧ (□ t' I. P t'))"
by blast+

lemma 
  iEx_insert: "⟦ P t ∨ (◇ t I. P t) ⟧ ⟹ ◇ t' (insert t I). P t'" and
  iEx_insert_conv: "(◇ t' (insert t I). P t') = (P t ∨ (◇ t' I. P t'))"
by blast+


subsection ‹Further results for temporal operators›

lemma Collect_minI_iEx: "◇ t I. P t ⟹ ◇ t I. P t ∧ (□ t' (I ↓< t). ¬ P t')"
by (unfold iAll_def iEx_def, rule Collect_minI_ex_cut)

lemma iUntil_disj_conv1: "
  I ≠ {} ⟹
  (P t'. t' 𝒰 t I. Q t) = (Q (iMin I) ∨ (P t'. t' 𝒰 t I. Q t ∧ iMin I < t))"
apply (case_tac "Q (iMin I)")
 apply (simp add: iMin_imp_iUntil)
apply (unfold iUntil_def, blast)
done

lemma iSince_disj_conv1: "
  ⟦ finite I; I ≠ {} ⟧ ⟹
  (P t'. t' 𝒮 t I. Q t) = (Q (Max I) ∨ (P t'. t' 𝒮 t I. Q t ∧ t < Max I))"
apply (case_tac "Q (Max I)")
 apply (simp add: Max_imp_iSince)
apply (unfold iSince_def, blast)
done

lemma iUntil_next: "
  I ≠ {} ⟹
  (P t'. t' 𝒰 t I. Q t) = 
  (Q (iMin I) ∨ (P (iMin I) ∧ (P t'. t' 𝒰 t (I ↓> (iMin I)). Q t)))"
apply (case_tac "Q (iMin I)")
 apply (simp add: iMin_imp_iUntil)
apply (simp add: iUntil_def)
apply (frule iMinI_ex2)
apply blast
done

lemma iSince_prev: "⟦ finite I; I ≠ {} ⟧ ⟹
  (P t'. t' 𝒮 t I. Q t) = 
  (Q (Max I) ∨ (P (Max I) ∧ (P t'. t' 𝒮 t (I ↓< Max I). Q t)))"
apply (case_tac "Q (Max I)")
 apply (simp add: Max_imp_iSince)
apply (simp add: iSince_def)
apply (frule Max_in, assumption)
apply blast
done

lemma iNext_induct_rule: "
  ⟦ P (iMin I); □ t I. (P t ⟶ (○ t' t I. P t')); t ∈ I ⟧ ⟹ P t"
apply (rule inext_induct[of _ I])
  apply simp
 apply (drule_tac t=n in ispec, assumption)
 apply (simp add: iNext_def)
apply assumption
done

lemma iNext_induct: "
  ⟦ P (iMin I); □ t I. (P t ⟶ (○ t' t I. P t')) ⟧ ⟹ □ t I. P t"
by (rule iallI, rule iNext_induct_rule)

lemma iLast_induct_rule: "
  ⟦ P (Max I); □ t I. (P t ⟶ (⊖ t' t I. P t')); finite I; t ∈ I ⟧ ⟹ P t"
apply (rule iprev_induct[of _ I])
  apply assumption
 apply (drule_tac t=n in ispec, assumption)
 apply (simp add: iLast_def)
apply assumption+
done

lemma iLast_induct: "
  ⟦ P (Max I); □ t I. (P t ⟶ (⊖ t' t I. P t')); finite I ⟧ ⟹ □ t I. P t"
by (rule iallI, rule iLast_induct_rule)


lemma iUntil_conj_not: "((P t1 ∧ ¬ Q t1). t1 𝒰 t2 I. Q t2) = (P t1. t1 𝒰 t2 I. Q t2)"
apply (unfold iUntil_def)
apply (rule iffI)
 apply blast
apply (clarsimp, rename_tac t)
apply (rule_tac t="iMin {x ∈ I. Q x}" in iexI)
 apply (rule conjI)
  apply (blast intro: iMinI2)
 apply (clarsimp simp: cut_less_mem_iff, rename_tac t1)
 apply (subgoal_tac "iMin {x ∈ I. Q x} ≤ t")
  prefer 2
  apply (simp add: iMin_le)
 apply (frule order_less_le_trans, assumption)
 apply (drule_tac t=t1 in ispec, simp add: cut_less_mem_iff)
 apply (rule ccontr, simp)
 apply (subgoal_tac "t1 ∈ {x ∈ I. Q x}")
  prefer 2
  apply blast
 apply (drule_tac k=t1 and I="{x ∈ I. Q x}" in iMin_le)
 apply simp
apply (blast intro: subsetD[OF _ iMinI])
done

lemma iWeakUntil_conj_not: "((P t1 ∧ ¬ Q t1). t1 𝒲 t2 I. Q t2) = (P t1. t1 𝒲 t2 I. Q t2)"
by (simp only: iWeakUntil_iUntil_conv iUntil_conj_not, blast)

lemma iSince_conj_not: "finite I ⟹
  ((P t1 ∧ ¬ Q t1). t1 𝒮 t2 I. Q t2) = (P t1. t1 𝒮 t2 I. Q t2)"
apply (simp only: iSince_def)
apply (case_tac "I = {}", simp)
apply (rule iffI)  
 apply blast
apply (clarsimp, rename_tac t)
apply (subgoal_tac "finite {x ∈ I. Q x}")
 prefer 2
 apply fastforce
apply (rule_tac t="Max {x ∈ I. Q x}" in iexI)
 apply (rule conjI)
  apply (blast intro: MaxI2)
 apply (clarsimp simp: cut_greater_mem_iff, rename_tac t1)
 apply (subgoal_tac "t ≤ Max {x ∈ I. Q x}")
  prefer 2
  apply simp
 apply (frule order_le_less_trans, assumption)
 apply (drule_tac t=t1 in ispec, simp add: cut_greater_mem_iff)
 apply (rule ccontr, simp)
 apply (subgoal_tac "t1 ∈ {x ∈ I. Q x}")
  prefer 2
  apply blast
 apply (drule  not_greater_Max[rotated 1], simp+)
apply (rule subsetD[OF _ MaxI], fastforce+)
done

lemma iWeakSince_conj_not: "finite I ⟹
  ((P t1 ∧ ¬ Q t1). t1 ℬ t2 I. Q t2) = (P t1. t1 ℬ t2 I. Q t2)"
by (simp only: iWeakSince_iSince_conv iSince_conj_not, blast)


lemma iNextStrong_imp_iNextWeak: "(○⇩S t t0 I. P t) ⟶ (○⇩W t t0 I. P t)"
unfolding iTL_Next_defs by blast
lemma iLastStrong_imp_iLastWeak: "(⊖⇩S t t0 I. P t) ⟶ (⊖⇩W t t0 I. P t)"
unfolding iTL_Next_defs by blast

lemma infin_imp_iNextWeak_iNextStrong_eq_iNext: "
  ⟦ infinite I; t0 ∈ I ⟧ ⟹ 
  ((○⇩W t t0 I. P t) = (○ t t0 I. P t)) ∧ ((○⇩S t t0 I. P t) = (○ t t0 I. P t))"
by (simp add: iTL_Next_iff nat_cut_greater_infinite_not_empty)

lemma infin_imp_iNextWeak_eq_iNext: "⟦ infinite I; t0 ∈ I ⟧ ⟹ (○⇩W t t0 I. P t) = (○ t t0 I. P t)"
by (simp add: infin_imp_iNextWeak_iNextStrong_eq_iNext)
lemma infin_imp_iNextStrong_eq_iNext: "⟦ infinite I; t0 ∈ I ⟧ ⟹ (○⇩S t t0 I. P t) = (○ t t0 I. P t)"
by (simp add: infin_imp_iNextWeak_iNextStrong_eq_iNext)
lemma infin_imp_iNextStrong_eq_iNextWeak: "⟦ infinite I; t0 ∈ I ⟧ ⟹ (○⇩S t t0 I. P t) = (○⇩W t t0 I. P t)"
by (simp add: infin_imp_iNextWeak_eq_iNext infin_imp_iNextStrong_eq_iNext)

lemma 
  not_in_iNext_eq: "t0 ∉ I ⟹ (○ t t0 I. P t) = (P t0)" and
  not_in_iLast_eq: "t0 ∉ I ⟹ (⊖ t t0 I. P t) = (P t0)"
by (simp_all add: iTL_defs not_in_inext_fix not_in_iprev_fix)

lemma 
  not_in_iNextWeak_eq: "t0 ∉ I ⟹ (○⇩W t t0 I. P t)" and
  not_in_iLastWeak_eq: "t0 ∉ I ⟹ (⊖⇩W t t0 I. P t)"
by (simp_all add: iNextWeak_iff iLastWeak_iff)

lemma 
  not_in_iNextStrong_eq: "t0 ∉ I ⟹ ¬ (○⇩S t t0 I. P t)" and
  not_in_iLastStrong_eq: "t0 ∉ I ⟹ ¬ (⊖⇩S t t0 I. P t)"
by (simp_all add: iNextStrong_iff iLastStrong_iff)

lemma 
  iNext_UNIV: "(○ t t0 UNIV. P t) = P (Suc t0)" and
  iNextWeak_UNIV: "(○⇩W t t0 UNIV. P t) = P (Suc t0)" and
  iNextStrong_UNIV: "(○⇩S t t0 UNIV. P t) = P (Suc t0)"
by (simp_all add: iTL_Next_defs inext_UNIV cut_greater_singleton)

lemma 
  iLast_UNIV: "(⊖ t t0 UNIV. P t) = P (t0 - Suc 0)" and
  iLastWeak_UNIV: "(⊖⇩W t t0 UNIV. P t) = (if 0 < t0 then P (t0 - Suc 0) else True)" and
  iLastStrong_UNIV: "(⊖⇩S t t0 UNIV. P t) = (if 0 < t0 then P (t0 - Suc 0) else False)"
by (simp_all add: iTL_Next_defs iprev_UNIV cut_less_singleton)

lemmas iTL_Next_UNIV = 
  iNext_UNIV iNextWeak_UNIV iNextStrong_UNIV
  iLast_UNIV iLastWeak_UNIV iLastStrong_UNIV

lemma inext_nth_iNext_Suc: "(○ t (I → n) I. P t) = P (I → Suc n)"
by (simp add: iNext_def)

lemma iprev_nth_iLast_Suc: "(⊖ t (I ← n) I. P t) = P (I ← Suc n)"
by (simp add: iLast_def)


subsection ‹Temporal operators and arithmetic interval operators›

text ‹
  Shifting intervals through addition and subtraction of constants. 
  Mirroring intervals through subtraction of intervals from constants. 
  Expanding and compressing intervals through multiplication and division by constants.›

text ‹Always operator›
lemma iT_Plus_iAll_conv: "(□ t I ⊕ k. P t) = (□ t I. P (t + k))"
apply (unfold iAll_def Ball_def)
apply (rule iffI)
 apply (clarify, rename_tac x)
 apply (drule_tac x="x + k" in spec)
 apply (simp add: iT_Plus_mem_iff2)
apply (clarify, rename_tac x)
apply (drule_tac x="x - k" in spec)
apply (simp add: iT_Plus_mem_iff)
done

lemma iT_Mult_iAll_conv: "(□ t I ⊗ k. P t) = (□ t I. P (t * k))"
apply (unfold iAll_def Ball_def)
apply (case_tac "I = {}")
 apply (simp add: iT_Mult_empty)
apply (case_tac "k = 0")
 apply (force simp: iT_Mult_0 iTILL_0)
apply (rule iffI)
 apply (clarify, rename_tac x)
 apply (drule_tac x="x * k" in spec)
 apply (simp add: iT_Mult_mem_iff2)
apply (clarify, rename_tac x)
apply (drule_tac x="x div k" in spec)
apply (simp add: iT_Mult_mem_iff mod_0_div_mult_cancel)
done

lemma iT_Plus_neg_iAll_conv: "(□ t I ⊕- k. P t) = (□ t (I ↓≥ k). P (t - k))"
apply (unfold iAll_def Ball_def)
apply (rule iffI)
 apply (clarify, rename_tac x)
 apply (drule_tac x="x - k" in spec)
 apply (simp add: iT_Plus_neg_mem_iff2)
apply (clarify, rename_tac x)
apply (drule_tac x="x + k" in spec)
apply (simp add: iT_Plus_neg_mem_iff cut_ge_mem_iff)
done

lemma iT_Minus_iAll_conv: "(□ t k ⊖ I. P t) = (□ t (I ↓≤ k). P (k - t))"
apply (unfold iAll_def Ball_def)
apply (rule iffI)
 apply (clarify, rename_tac x)
 apply (drule_tac x="k - x" in spec)
 apply (simp add: iT_Minus_mem_iff)
apply (clarify, rename_tac x)
apply (drule_tac x="k - x" in spec)
apply (simp add: iT_Minus_mem_iff cut_le_mem_iff)
done

lemma iT_Div_iAll_conv: "(□ t I ⊘ k. P t) = (□ t I. P (t div k))"
apply (case_tac "I = {}")
 apply (simp add: iT_Div_empty)
apply (case_tac "k = 0")
 apply (force simp: iT_Div_0 iTILL_0)
apply (unfold iAll_def Ball_def)
apply (rule iffI)
 apply (clarify, rename_tac x)
 apply (drule_tac x="x div k" in spec)
 apply (simp add: iT_Div_imp_mem)
apply (blast dest: iT_Div_mem_iff[THEN iffD1])
done

lemmas iT_arith_iAll_conv = 
  iT_Plus_iAll_conv
  iT_Mult_iAll_conv
  iT_Plus_neg_iAll_conv
  iT_Minus_iAll_conv
  iT_Div_iAll_conv

text ‹Eventually operator›
lemma 
  iT_Plus_iEx_conv: "(◇ t I ⊕ k. P t) = (◇ t I. P (t + k))" and
  iT_Mult_iEx_conv: "(◇ t I ⊗ k. P t) = (◇ t I. P (t * k))" and
  iT_Plus_neg_iEx_conv: "(◇ t I ⊕- k. P t) = (◇ t (I ↓≥ k). P (t - k))" and
  iT_Minus_iEx_conv: "(◇ t k ⊖ I. P t) = (◇ t (I ↓≤ k). P (k - t))" and
  iT_Div_iEx_conv: "(◇ t I ⊘ k. P t) = (◇ t I. P (t div k))"
by (simp_all only: iEx_iAll_conv iT_arith_iAll_conv)


text ‹Until and Since operators›

lemma iT_Plus_iUntil_conv: "(P t1. t1 𝒰 t2 (I ⊕ k). Q t2) = (P (t1 + k). t1 𝒰 t2 I. Q (t2 + k))"
by (simp add: iUntil_def iT_Plus_iAll_conv iT_Plus_iEx_conv iT_Plus_cut_less2)

lemma iT_Mult_iUntil_conv: "(P t1. t1 𝒰 t2 (I ⊗ k). Q t2) = (P (t1 * k). t1 𝒰 t2 I. Q (t2 * k))"
apply (case_tac "I = {}")
 apply (simp add: iT_Mult_empty)
apply (case_tac "k = 0")
 apply (force simp add: iT_Mult_0 iTILL_0)
apply (simp add: iUntil_def iT_Mult_iAll_conv iT_Mult_iEx_conv iT_Mult_cut_less2)
done

lemma iT_Plus_neg_iUntil_conv: "(P t1. t1 𝒰 t2 (I ⊕- k). Q t2) = (P (t1 - k). t1 𝒰 t2 (I ↓≥ k). Q (t2 - k))"
apply (simp add: iUntil_def iT_Plus_neg_iAll_conv iT_Plus_neg_iEx_conv iT_Plus_neg_cut_less2)
apply (simp add: i_cut_commute_disj)
done

lemma iT_Minus_iUntil_conv: "(P t1. t1 𝒰 t2 (k ⊖ I). Q t2) = (P (k - t1). t1 𝒮 t2 (I ↓≤ k). Q (k - t2))"
apply (simp add: iUntil_def iSince_def iT_Minus_iAll_conv iT_Minus_iEx_conv iT_Minus_cut_less2)
apply (simp add: i_cut_commute_disj)
done

lemma iT_Div_iUntil_conv: "(P t1. t1 𝒰 t2 (I ⊘ k). Q t2) = (P (t1 div k). t1 𝒰 t2 I. Q (t2 div k))"
apply (case_tac "I = {}")
 apply (simp add: iT_Div_empty)
apply (case_tac "k = 0")
 apply (force simp add: iT_Div_0 iTILL_0)
apply (simp add: iUntil_def iT_Div_iAll_conv iT_Div_iEx_conv iT_Div_cut_less2)
apply (rule iffI)
 apply (clarsimp, rename_tac t)
 apply (subgoal_tac "I ↓≥ (t - t mod k) ≠ {}")
  prefer 2
  apply (simp add: cut_ge_not_empty_iff)
  apply (rule_tac x=t in bexI)
  apply simp+
 apply (case_tac "t mod k = 0")
  apply (rule_tac t=t in iexI)
  apply simp+
 apply (rule_tac t="iMin (I ↓≥ (t - t mod k))" in iexI)
  apply (subgoal_tac "
    t - t mod k ≤ iMin (I ↓≥ (t - t mod k)) ∧
    iMin (I ↓≥ (t - t mod k)) ≤ t")
   prefer 2
   apply (rule conjI)
    apply (blast intro: cut_ge_Min_greater)
   apply (simp add: iMin_le cut_ge_mem_iff)
  apply clarify
  apply (rule_tac t="iMin (I ↓≥ (t - t mod k)) div k" and s="t div k" in subst)
   apply (rule order_antisym)
    apply (drule_tac m="t - t mod k" and k=k in div_le_mono)
    apply (simp add: sub_mod_div_eq_div)
   apply (rule div_le_mono, assumption)
  apply (clarsimp, rename_tac t1)
  apply (subgoal_tac "t1 ∈ I ↓< (t - t mod k) ∪ I ↓≥ (t - t mod k)")
   prefer 2
   apply (simp add: cut_less_cut_ge_ident)
  apply (subgoal_tac "t1 ∉ I ↓≥ (t - t mod k)")
   prefer 2
   apply (blast dest: not_less_iMin)
  apply blast
 apply (blast intro: subsetD[OF _ iMinI_ex2])
apply (clarsimp, rename_tac t)
apply (rule_tac t=t in iexI)
 apply simp
 apply (rule_tac B="I ↓< t" in iAll_subset)
 apply (simp add: cut_less_mono)
apply simp+
done


text ‹Until and Since operators can be converted into each other through substraction of intervals from constants›

lemma iUntil_iSince_conv: "
  ⟦ finite I; Max I ≤ k ⟧ ⟹ 
  (P t1. t1 𝒰 t2 I. Q t2) = (P (k - t1). t1 𝒮 t2 (k ⊖ I). Q (k - t2))"
apply (case_tac "I = {}")
 apply (simp add: iT_Minus_empty)
apply (frule le_trans[OF iMin_le_Max], assumption+)
apply (subgoal_tac "Max (k ⊖ I) ≤ k")
 prefer 2
 apply (simp add: iT_Minus_Max)
apply (subgoal_tac "iMin (k ⊖ I) ≤ k")
 prefer 2
 apply (rule order_trans[OF iMin_le_Max])
 apply (simp add: iT_Minus_finite iT_Minus_empty_iff del: Max_le_iff)+
apply (rule_tac t="P t1. t1 𝒰 t2 I. Q t2" and s="P t1. t1 𝒰 t2 (k ⊖ (k ⊖ I)). Q t2" in subst)
 apply (simp add: iT_Minus_Minus_eq)
apply (simp add: iT_Minus_iUntil_conv cut_le_Max_all iT_Minus_finite)
done

lemma iSince_iUntil_conv: "
  ⟦ finite I; Max I ≤ k ⟧ ⟹ 
  (P t1. t1 𝒮 t2 I. Q t2) = (P (k - t1). t1 𝒰 t2 (k ⊖ I). Q (k - t2))"
apply (case_tac "I = {}")
 apply (simp add: iT_Minus_empty)
apply (simp (no_asm_simp) add: iT_Minus_iUntil_conv)
apply (simp (no_asm_simp) add: cut_le_Max_all)
apply (unfold iSince_def)
apply (rule iffI)
 apply (clarsimp, rename_tac t)
 apply (rule_tac t=t in iexI)
  apply (frule_tac x=t in bspec, assumption)
  apply (clarsimp, rename_tac t1)
  apply (drule_tac t=t1 in ispec)
   apply (simp add: cut_greater_mem_iff)
  apply simp+
apply (clarsimp, rename_tac t)
apply (rule_tac t=t in iexI)
 apply (clarsimp, rename_tac t')
 apply (drule_tac t=t' in ispec)
  apply (simp add: cut_greater_mem_iff)
 apply simp+
done


lemma iT_Plus_iSince_conv: "(P t1. t1 𝒮 t2 (I ⊕ k). Q t2) = (P (t1 + k). t1 𝒮 t2 I. Q (t2 + k))"
by (simp add: iSince_def iT_Plus_iAll_conv iT_Plus_iEx_conv iT_Plus_cut_greater2)

lemma iT_Mult_iSince_conv: "0 < k ⟹ (P t1. t1 𝒮 t2 (I ⊗ k). Q t2) = (P (t1 * k). t1 𝒮 t2 I. Q (t2 * k))"
by (simp add: iSince_def iT_Mult_iAll_conv iT_Mult_iEx_conv iT_Mult_cut_greater2)

lemma iT_Plus_neg_iSince_conv: "(P t1. t1 𝒮 t2 (I ⊕- k). Q t2) = (P (t1 - k). t1 𝒮 t2 (I ↓≥ k). Q (t2 - k))"
apply (simp add: iSince_def iT_Plus_neg_iAll_conv iT_Plus_neg_iEx_conv)
apply (rule iffI)
 apply (clarsimp, rename_tac t)
 apply (simp add: iT_Plus_neg_cut_greater2)
 apply (rule_tac t=t in iexI)
  apply (clarsimp, rename_tac t')
  apply (drule_tac t="t' - k" in ispec)
   apply (simp add: iT_Plus_neg_mem_iff2 cut_greater_mem_iff)
  apply simp
 apply blast
apply (clarsimp, rename_tac t)
apply (rule_tac t=t in iexI)
 apply (clarsimp, rename_tac t')
 apply (drule_tac t="t' + k" in ispec)
  apply (simp add: iT_Plus_neg_mem_iff i_cut_mem_iff)
 apply simp
apply blast
done
lemma iT_Minus_iSince_conv: "
  (P t1. t1 𝒮 t2 (k ⊖ I). Q t2) = (P (k - t1). t1 𝒰 t2 (I ↓≤ k). Q (k - t2))"
apply (case_tac "I = {}")
 apply (simp add: iT_Minus_empty cut_le_empty)
apply (case_tac "I ↓≤ k = {}")
 apply (simp add: iT_Minus_image_conv)
apply (subst iT_Minus_cut_eq[OF order_refl, symmetric])
apply (subst iSince_iUntil_conv[where k=k])
  apply (rule iT_Minus_finite)
 apply (subst iT_Minus_Max)
   apply simp
  apply (rule cut_le_bound, rule iMinI_ex2, simp)
 apply simp
apply (simp add: iT_Minus_Minus_cut_eq)
done

lemma iT_Div_iSince_conv: "
  0 < k ⟹ (P t1. t1 𝒮 t2 (I ⊘ k). Q t2) = (P (t1 div k). t1 𝒮 t2 I. Q (t2 div k))"
apply (case_tac "I = {}")
 apply (simp add: iT_Div_empty)
apply (simp add: iSince_def iT_Div_iAll_conv iT_Div_iEx_conv)
apply (simp add: iT_Div_cut_greater)
apply (subgoal_tac "∀t. t ≤ t div k * k + (k - Suc 0)")
 prefer 2
 apply clarsimp
 apply (simp add: div_mult_cancel add.commute[of _ k])
 apply (simp add: le_add_diff Suc_mod_le_divisor)
apply (rule iffI)
 apply (clarsimp, rename_tac t)
 apply (drule_tac x=t in spec)
 apply (subgoal_tac "I ↓≤ (t div k * k + (k - Suc 0)) ≠ {}")
  prefer 2
  apply (simp add: cut_le_not_empty_iff)
  apply (rule_tac x=t in bexI, assumption+)
 apply (subgoal_tac "t ≤ Max (I ↓≤ (t div k * k + (k - Suc 0)))")
  prefer 2
  apply (simp add: nat_cut_le_finite cut_le_mem_iff)
 apply (subgoal_tac "Max (I ↓≤ (t div k * k + (k - Suc 0))) ≤ t div k * k + (k - Suc 0)")
  prefer 2
  apply (simp add: nat_cut_le_finite cut_le_mem_iff)
 apply (subgoal_tac "Max (I ↓≤ (t div k * k + (k - Suc 0))) div k = t div k")
  prefer 2
  apply (rule order_antisym)
   apply (rule_tac t="t div k" and s="(t div k * k + (k - Suc 0)) div k" in subst)
    apply (simp only: div_add1_eq1_mod_0_left[OF mod_mult_self2_is_0])
    apply simp
   apply (rule div_le_mono)
   apply (simp only: div_add1_eq1_mod_0_left[OF mod_mult_self2_is_0])
   apply simp
  apply (rule div_le_mono, assumption)
 apply (rule_tac t="Max (I ↓≤ (t div k * k + (k - Suc 0)))" in iexI)
  apply (clarsimp, rename_tac t1)
  apply (subgoal_tac "t1 ∈ I")
   prefer 2
   apply assumption
  apply (subgoal_tac "t div k * k + (k - Suc 0) < t1")
   prefer 2
   apply (rule ccontr)
   apply (drule not_greater_Max[OF nat_cut_le_finite])
   apply (simp add: i_cut_mem_iff)
  apply (drule_tac t="t1 div k" in ispec)
   apply (simp add: iT_Div_imp_mem cut_greater_mem_iff)
  apply assumption
 apply (blast intro: subsetD[OF _ Max_in[OF nat_cut_le_finite]])
apply (clarsimp, rename_tac t)
apply (drule_tac x=t in spec)
apply (rule_tac t=t in iexI)
 apply (clarsimp simp: iT_Div_mem_iff, rename_tac t1 t2)
 apply (drule_tac t=t2 in ispec)
  apply (simp add: cut_greater_mem_iff)
 apply simp+
done


text ‹Weak Until and Weak Since operators›

lemma iT_Plus_iWeakUntil_conv: "(P t1. t1 𝒲 t2 (I ⊕ k). Q t2) = (P (t1 + k). t1 𝒲 t2 I. Q (t2 + k))"
by (simp add: iWeakUntil_iUntil_conv iT_Plus_iUntil_conv iT_Plus_iAll_conv)

lemma iT_Mult_iWeakUntil_conv: "(P t1. t1 𝒲 t2 (I ⊗ k). Q t2) = (P (t1 * k). t1 𝒲 t2 I. Q (t2 * k))"
by (simp add: iWeakUntil_iUntil_conv iT_Mult_iUntil_conv iT_Mult_iAll_conv)

lemma iT_Plus_neg_iWeakUntil_conv: "(P t1. t1 𝒲 t2 (I ⊕- k). Q t2) = (P (t1 - k). t1 𝒲 t2 (I ↓≥ k). Q (t2 - k))"
by (simp add: iWeakUntil_iUntil_conv iT_Plus_neg_iUntil_conv iT_Plus_neg_iAll_conv)

lemma iT_Minus_iWeakUntil_conv: "(P t1. t1 𝒲 t2 (k ⊖ I). Q t2) = (P (k - t1). t1 ℬ t2 (I ↓≤ k). Q (k - t2))"
by (simp add: iWeakUntil_iUntil_conv iWeakSince_iSince_conv iT_Minus_iUntil_conv iT_Minus_iAll_conv)

lemma iT_Div_iWeakUntil_conv: "(P t1. t1 𝒲 t2 (I ⊘ k). Q t2) = (P (t1 div k). t1 𝒲 t2 I. Q (t2 div k))"
by (simp add: iWeakUntil_iUntil_conv iT_Div_iUntil_conv iT_Div_iAll_conv)


lemma iT_Plus_iWeakSince_conv: "(P t1. t1 ℬ t2 (I ⊕ k). Q t2) = (P (t1 + k). t1 ℬ t2 I. Q (t2 + k))"
by (simp add: iWeakSince_iSince_conv iT_Plus_iSince_conv iT_Plus_iAll_conv)

lemma iT_Mult_iWeakSince_conv: "0 < k ⟹ (P t1. t1 ℬ t2 (I ⊗ k). Q t2) = (P (t1 * k). t1 ℬ t2 I. Q (t2 * k))"
by (simp add: iWeakSince_iSince_conv iT_Mult_iSince_conv iT_Mult_iAll_conv)

lemma iT_Plus_neg_iWeakSince_conv: "(P t1. t1 ℬ t2 (I ⊕- k). Q t2) = (P (t1 - k). t1 ℬ t2 (I ↓≥ k). Q (t2 - k))"
by (simp add: iWeakSince_iSince_conv iT_Plus_neg_iSince_conv iT_Plus_neg_iAll_conv)

lemma iT_Minus_iWeakSince_conv: "
  (P t1. t1 ℬ t2 (k ⊖ I). Q t2) = (P (k - t1). t1 𝒲 t2 (I ↓≤ k). Q (k - t2))"
by (simp add: iWeakSince_iSince_conv iT_Minus_iSince_conv iT_Minus_iAll_conv iWeakUntil_iUntil_conv)

lemma iT_Div_iWeakSince_conv: "
  0 < k ⟹ (P t1. t1 ℬ t2 (I ⊘ k). Q t2) = (P (t1 div k). t1 ℬ t2 I. Q (t2 div k))"
by (simp add: iWeakSince_iSince_conv iT_Div_iSince_conv iT_Div_iAll_conv)


text ‹Release and Trigger operators›

lemma iT_Plus_iRelease_conv: "(P t1. t1 ℛ t2 (I ⊕ k). Q t2) = (P (t1 + k). t1 ℛ t2 I. Q (t2 + k))"
by (simp add: iRelease_iWeakUntil_conv iT_Plus_iWeakUntil_conv)

lemma iT_Mult_iRelease_conv: "(P t1. t1 ℛ t2 (I ⊗ k). Q t2) = (P (t1 * k). t1 ℛ t2 I. Q (t2 * k))"
by (simp add: iRelease_iWeakUntil_conv iT_Mult_iWeakUntil_conv)

lemma iT_Plus_neg_iRelease_conv: "(P t1. t1 ℛ t2 (I ⊕- k). Q t2) = (P (t1 - k). t1 ℛ t2 (I ↓≥ k). Q (t2 - k))"
by (simp add: iRelease_iWeakUntil_conv iT_Plus_neg_iWeakUntil_conv)

lemma iT_Minus_iRelease_conv: "(P t1. t1 ℛ t2 (k ⊖ I). Q t2) = (P (k - t1). t1 𝒯 t2 (I ↓≤ k). Q (k - t2))"
by (simp add: iRelease_iWeakUntil_conv iT_Minus_iWeakUntil_conv 
  iTrigger_iSince_conv iWeakSince_iSince_conv disj_commute)

lemma iT_Div_iRelease_conv: "(P t1. t1 ℛ t2 (I ⊘ k). Q t2) = (P (t1 div k). t1 ℛ t2 I. Q (t2 div k))"
by (simp add: iRelease_iWeakUntil_conv iT_Div_iWeakUntil_conv)


lemma iT_Plus_iTrigger_conv: "(P t1. t1 𝒯 t2 (I ⊕ k). Q t2) = (P (t1 + k). t1 𝒯 t2 I. Q (t2 + k))"
by (simp add: iTrigger_iWeakSince_conv iT_Plus_iWeakSince_conv)

lemma iT_Mult_iTrigger_conv: "0 < k ⟹ (P t1. t1 𝒯 t2 (I ⊗ k). Q t2) = (P (t1 * k). t1 𝒯 t2 I. Q (t2 * k))"
by (simp add: iTrigger_iWeakSince_conv iT_Mult_iWeakSince_conv)

lemma iT_Plus_neg_iTrigger_conv: "(P t1. t1 𝒯 t2 (I ⊕- k). Q t2) = (P (t1 - k). t1 𝒯 t2 (I ↓≥ k). Q (t2 - k))"
by (simp add: iTrigger_iWeakSince_conv iT_Plus_neg_iWeakSince_conv)

lemma iT_Minus_iTrigger_conv: "
  (P t1. t1 𝒯 t2 (k ⊖ I). Q t2) = (P (k - t1). t1 ℛ t2 (I ↓≤ k). Q (k - t2))"
by (fastforce simp add: iTrigger_iWeakSince_conv iT_Minus_iWeakSince_conv iRelease_iUntil_conv iWeakUntil_iUntil_conv)

lemma iT_Div_iTrigger_conv: "
  0 < k ⟹ (P t1. t1 𝒯 t2 (I ⊘ k). Q t2) = (P (t1 div k). t1 𝒯 t2 I. Q (t2 div k))"
by (simp add: iTrigger_iWeakSince_conv iT_Div_iWeakSince_conv)

end