# 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 =
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)"

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)"

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)"

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

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)"

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

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 (case_tac "t0 ∈ I")
prefer 2
apply simp
apply (case_tac "I ↓> t0 = {}")
done

lemma iprev_singleton_cut_less_not_empty_iff: "
({iprev t0 I} ↓< t0 ≠ {}) = (I ↓< t0 ≠ {} ∧ t0 ∈ I)"
apply (case_tac "t0 ∈ I")
prefer 2
apply simp
apply (case_tac "I ↓< t0 = {}")
done

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

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

lemma iNextWeak_iff : "(○⇩W t t0 I. P t) = ((○ t t0 I. P t) ∨ (I ↓> t0 = {}) ∨ t0 ∉ I)"
apply (unfold iTL_defs)
done

lemma iNextStrong_iff : "(○⇩S t t0 I. P t) = ((○ t t0 I. P t) ∧ (I ↓> t0 ≠ {}) ∧ t0 ∈ I)"
apply (unfold iTL_defs)
done

lemma iLastWeak_iff : "(⊖⇩W t t0 I. P t) = ((⊖ t t0 I. P t) ∨ (I ↓< t0 = {}) ∨ t0 ∉ I)"
apply (unfold iTL_defs)
done

lemma iLastStrong_iff : "(⊖⇩S t t0 I. P t) = ((⊖ t t0 I. P t) ∧ (I ↓< t0 ≠ {}) ∧ t0 ∈ I)"
apply (unfold iTL_defs)
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)"

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)"

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)"

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)
done

lemma iUntil_False_left[simp]: "(False. t' 𝒰 t I. Q t) = (I ≠ {} ∧ Q (iMin I))"
apply (case_tac "I = {}", blast)
apply (rule iffI)
apply clarsimp
apply (drule iMin_equality)
apply simp
apply (rule_tac x="iMin I" in bexI)
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
done

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

lemma iSince_False_left[simp]: "(False. t' 𝒮 t I. Q t) = (finite I ∧ I ≠ {} ∧ Q (Max I))"
apply (case_tac "I = {}", simp)
apply (case_tac "infinite I")
apply (rule iffI)
apply clarsimp
apply (drule Max_equality)
apply simp
apply simp
apply (rule_tac x="Max I" in bexI)
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"

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

lemma iWeakUntil_False_left[simp]: "(False. t' 𝒲 t I. Q t) = (I = {} ∨ Q (iMin I))"
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)
done

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

lemma iWeakSince_True_left[simp]: "True. t' ℬ t I. Q t"

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 (case_tac "I = {}", simp)
apply (rule disjI2)
apply (rule_tac x="Max I" in bexI)
apply simp
done

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

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

lemma iRelease_True_left[simp]: "(True. t' ℛ t I. Q t) = (I = {} ∨ Q (iMin I))"
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
done

lemma iRelease_True[simp]: "P t'. t' ℛ t I. True"

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

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"

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

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"

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"

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

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

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

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)"

lemma iTrigger_iAll_conv: "(False. t' 𝒯 t I. P t) = (□ t I. P t)"

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 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 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 (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))"

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 (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))"

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))"

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 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 (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 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])
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)"

lemma not_iWeakUntil: "
(¬ (P t1. t1 𝒲 t2 I. Q t2)) =
((□ t I. (Q t ⟶ (◇ t' (I ↓< t). ¬ P t'))) ∧ (◇ t I. ¬ P t))"
lemma not_iWeakSince: "
(¬ (P t1. t1 ℬ t2 I. Q t2)) =
((□ t I. (Q t ⟶ (◇ t' (I ↓> t). ¬ P t'))) ∧ (◇ t I. ¬ P t))"

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

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

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

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

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 (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 (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)
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 (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 (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 (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 (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 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 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 (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))"

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

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)"

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)"

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)"

lemma iprev_nth_iLast_Suc: "(⊖ t (I ← n) I. P t) = P (I ← Suc n)"

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 (clarify, rename_tac x)
apply (drule_tac x="x - k" in spec)
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 (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 (clarify, rename_tac x)
apply (drule_tac x="x div k" in spec)
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 (clarify, rename_tac x)
apply (drule_tac x="x + k" in spec)
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 (clarify, rename_tac x)
apply (drule_tac x="k - x" in spec)
done

lemma iT_Div_iAll_conv: "(□ t I ⊘ k. P t) = (□ t I. P (t div k))"
apply (case_tac "I = {}")
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 (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 (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)
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)
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 (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 (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 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 (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 (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+
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 (frule le_trans[OF iMin_le_Max], assumption+)
apply (subgoal_tac "Max (k ⊖ I) ≤ k")
prefer 2
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_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 (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+
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+
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 (rule_tac t=t in iexI)
apply (clarsimp, rename_tac t')
apply (drule_tac t="t' - k" in ispec)