# Theory HOL-Library.Linear_Temporal_Logic_on_Streams

```(*  Title:      HOL/Library/Linear_Temporal_Logic_on_Streams.thy
Author:     Andrei Popescu, TU Muenchen
Author:     Dmitriy Traytel, TU Muenchen
*)

section ‹Linear Temporal Logic on Streams›

theory Linear_Temporal_Logic_on_Streams
imports Stream Sublist Extended_Nat Infinite_Set
begin

section‹Preliminaries›

lemma shift_prefix:
assumes "xl @- xs = yl @- ys" and "length xl ≤ length yl"
shows "prefix xl yl"
using assms proof(induct xl arbitrary: yl xs ys)
case (Cons x xl yl xs ys)
thus ?case by (cases yl) auto
qed auto

lemma shift_prefix_cases:
assumes "xl @- xs = yl @- ys"
shows "prefix xl yl ∨ prefix yl xl"
using shift_prefix[OF assms]
by (cases "length xl ≤ length yl") (metis, metis assms nat_le_linear shift_prefix)

section‹Linear temporal logic›

text ‹Propositional connectives:›

abbreviation (input) IMPL (infix "impl" 60)
where "φ impl ψ ≡ λ xs. φ xs ⟶ ψ xs"

abbreviation (input) OR (infix "or" 60)
where "φ or ψ ≡ λ xs. φ xs ∨ ψ xs"

abbreviation (input) AND (infix "aand" 60)
where "φ aand ψ ≡ λ xs. φ xs ∧ ψ xs"

abbreviation (input) not where "not φ ≡ λ xs. ¬ φ xs"

abbreviation (input) "true ≡ λ xs. True"

abbreviation (input) "false ≡ λ xs. False"

lemma impl_not_or: "φ impl ψ = (not φ) or ψ"
by blast

lemma not_or: "not (φ or ψ) = (not φ) aand (not ψ)"
by blast

lemma not_aand: "not (φ aand ψ) = (not φ) or (not ψ)"
by blast

lemma non_not[simp]: "not (not φ) = φ" by simp

text ‹Temporal (LTL) connectives:›

fun holds where "holds P xs ⟷ P (shd xs)"
fun nxt where "nxt φ xs = φ (stl xs)"

definition "HLD s = holds (λx. x ∈ s)"

abbreviation HLD_nxt (infixr "⋅" 65) where
"s ⋅ P ≡ HLD s aand nxt P"

context
notes [[inductive_internals]]
begin

inductive ev for φ where
base: "φ xs ⟹ ev φ xs"
|
step: "ev φ (stl xs) ⟹ ev φ xs"

coinductive alw for φ where
alw: "⟦φ xs; alw φ (stl xs)⟧ ⟹ alw φ xs"

― ‹weak until:›
coinductive UNTIL (infix "until" 60) for φ ψ where
base: "ψ xs ⟹ (φ until ψ) xs"
|
step: "⟦φ xs; (φ until ψ) (stl xs)⟧ ⟹ (φ until ψ) xs"

end

lemma holds_mono:
assumes holds: "holds P xs" and 0: "⋀ x. P x ⟹ Q x"
shows "holds Q xs"
using assms by auto

lemma holds_aand:
"(holds P aand holds Q) steps ⟷ holds (λ step. P step ∧ Q step) steps" by auto

lemma HLD_iff: "HLD s ω ⟷ shd ω ∈ s"
by (simp add: HLD_def)

lemma HLD_Stream[simp]: "HLD X (x ## ω) ⟷ x ∈ X"
by (simp add: HLD_iff)

lemma nxt_mono:
assumes nxt: "nxt φ xs" and 0: "⋀ xs. φ xs ⟹ ψ xs"
shows "nxt ψ xs"
using assms by auto

declare ev.intros[intro]
declare alw.cases[elim]

lemma ev_induct_strong[consumes 1, case_names base step]:
"ev φ x ⟹ (⋀xs. φ xs ⟹ P xs) ⟹ (⋀xs. ev φ (stl xs) ⟹ ¬ φ xs ⟹ P (stl xs) ⟹ P xs) ⟹ P x"
by (induct rule: ev.induct) auto

lemma alw_coinduct[consumes 1, case_names alw stl]:
"X x ⟹ (⋀x. X x ⟹ φ x) ⟹ (⋀x. X x ⟹ ¬ alw φ (stl x) ⟹ X (stl x)) ⟹ alw φ x"
using alw.coinduct[of X x φ] by auto

lemma ev_mono:
assumes ev: "ev φ xs" and 0: "⋀ xs. φ xs ⟹ ψ xs"
shows "ev ψ xs"
using ev by induct (auto simp: 0)

lemma alw_mono:
assumes alw: "alw φ xs" and 0: "⋀ xs. φ xs ⟹ ψ xs"
shows "alw ψ xs"
using alw by coinduct (auto simp: 0)

lemma until_monoL:
assumes until: "(φ1 until ψ) xs" and 0: "⋀ xs. φ1 xs ⟹ φ2 xs"
shows "(φ2 until ψ) xs"
using until by coinduct (auto elim: UNTIL.cases simp: 0)

lemma until_monoR:
assumes until: "(φ until ψ1) xs" and 0: "⋀ xs. ψ1 xs ⟹ ψ2 xs"
shows "(φ until ψ2) xs"
using until by coinduct (auto elim: UNTIL.cases simp: 0)

lemma until_mono:
assumes until: "(φ1 until ψ1) xs" and
0: "⋀ xs. φ1 xs ⟹ φ2 xs" "⋀ xs. ψ1 xs ⟹ ψ2 xs"
shows "(φ2 until ψ2) xs"
using until by coinduct (auto elim: UNTIL.cases simp: 0)

lemma until_false: "φ until false = alw φ"
proof-
{fix xs assume "(φ until false) xs" hence "alw φ xs"
by coinduct (auto elim: UNTIL.cases)
}
moreover
{fix xs assume "alw φ xs" hence "(φ until false) xs"
by coinduct auto
}
ultimately show ?thesis by blast
qed

lemma ev_nxt: "ev φ = (φ or nxt (ev φ))"
by (rule ext) (metis ev.simps nxt.simps)

lemma alw_nxt: "alw φ = (φ aand nxt (alw φ))"
by (rule ext) (metis alw.simps nxt.simps)

lemma ev_ev[simp]: "ev (ev φ) = ev φ"
proof-
{fix xs
assume "ev (ev φ) xs" hence "ev φ xs"
by induct auto
}
thus ?thesis by auto
qed

lemma alw_alw[simp]: "alw (alw φ) = alw φ"
proof-
{fix xs
assume "alw φ xs" hence "alw (alw φ) xs"
by coinduct auto
}
thus ?thesis by auto
qed

lemma ev_shift:
assumes "ev φ xs"
shows "ev φ (xl @- xs)"
using assms by (induct xl) auto

lemma ev_imp_shift:
assumes "ev φ xs"  shows "∃ xl xs2. xs = xl @- xs2 ∧ φ xs2"
using assms by induct (metis shift.simps(1), metis shift.simps(2) stream.collapse)+

lemma alw_ev_shift: "alw φ xs1 ⟹ ev (alw φ) (xl @- xs1)"
by (auto intro: ev_shift)

lemma alw_shift:
assumes "alw φ (xl @- xs)"
shows "alw φ xs"
using assms by (induct xl) auto

lemma ev_ex_nxt:
assumes "ev φ xs"
shows "∃ n. (nxt ^^ n) φ xs"
using assms proof induct
case (base xs) thus ?case by (intro exI[of _ 0]) auto
next
case (step xs)
then obtain n where "(nxt ^^ n) φ (stl xs)" by blast
thus ?case by (intro exI[of _ "Suc n"]) (metis funpow.simps(2) nxt.simps o_def)
qed

lemma alw_sdrop:
assumes "alw φ xs"  shows "alw φ (sdrop n xs)"
by (metis alw_shift assms stake_sdrop)

lemma nxt_sdrop: "(nxt ^^ n) φ xs ⟷ φ (sdrop n xs)"
by (induct n arbitrary: xs) auto

definition "wait φ xs ≡ LEAST n. (nxt ^^ n) φ xs"

lemma nxt_wait:
assumes "ev φ xs"  shows "(nxt ^^ (wait φ xs)) φ xs"
unfolding wait_def using ev_ex_nxt[OF assms] by(rule LeastI_ex)

lemma nxt_wait_least:
assumes ev: "ev φ xs" and nxt: "(nxt ^^ n) φ xs"  shows "wait φ xs ≤ n"
unfolding wait_def using ev_ex_nxt[OF ev] by (metis Least_le nxt)

lemma sdrop_wait:
assumes "ev φ xs"  shows "φ (sdrop (wait φ xs) xs)"
using nxt_wait[OF assms] unfolding nxt_sdrop .

lemma sdrop_wait_least:
assumes ev: "ev φ xs" and nxt: "φ (sdrop n xs)"  shows "wait φ xs ≤ n"
using assms nxt_wait_least unfolding nxt_sdrop by auto

lemma nxt_ev: "(nxt ^^ n) φ xs ⟹ ev φ xs"
by (induct n arbitrary: xs) auto

lemma not_ev: "not (ev φ) = alw (not φ)"
proof(rule ext, safe)
fix xs assume "not (ev φ) xs" thus "alw (not φ) xs"
by (coinduct) auto
next
fix xs assume "ev φ xs" and "alw (not φ) xs" thus False
by (induct) auto
qed

lemma not_alw: "not (alw φ) = ev (not φ)"
proof-
have "not (alw φ) = not (alw (not (not φ)))" by simp
also have "... = ev (not φ)" unfolding not_ev[symmetric] by simp
finally show ?thesis .
qed

lemma not_ev_not[simp]: "not (ev (not φ)) = alw φ"
unfolding not_ev by simp

lemma not_alw_not[simp]: "not (alw (not φ)) = ev φ"
unfolding not_alw by simp

lemma alw_ev_sdrop:
assumes "alw (ev φ) (sdrop m xs)"
shows "alw (ev φ) xs"
using assms
by coinduct (metis alw_nxt ev_shift funpow_swap1 nxt.simps nxt_sdrop stake_sdrop)

lemma ev_alw_imp_alw_ev:
assumes "ev (alw φ) xs"  shows "alw (ev φ) xs"
using assms by induct (metis (full_types) alw_mono ev.base, metis alw alw_nxt ev.step)

lemma alw_aand: "alw (φ aand ψ) = alw φ aand alw ψ"
proof-
{fix xs assume "alw (φ aand ψ) xs" hence "(alw φ aand alw ψ) xs"
by (auto elim: alw_mono)
}
moreover
{fix xs assume "(alw φ aand alw ψ) xs" hence "alw (φ aand ψ) xs"
by coinduct auto
}
ultimately show ?thesis by blast
qed

lemma ev_or: "ev (φ or ψ) = ev φ or ev ψ"
proof-
{fix xs assume "(ev φ or ev ψ) xs" hence "ev (φ or ψ) xs"
by (auto elim: ev_mono)
}
moreover
{fix xs assume "ev (φ or ψ) xs" hence "(ev φ or ev ψ) xs"
by induct auto
}
ultimately show ?thesis by blast
qed

lemma ev_alw_aand:
assumes φ: "ev (alw φ) xs" and ψ: "ev (alw ψ) xs"
shows "ev (alw (φ aand ψ)) xs"
proof-
obtain xl xs1 where xs1: "xs = xl @- xs1" and φφ: "alw φ xs1"
using φ by (metis ev_imp_shift)
moreover obtain yl ys1 where xs2: "xs = yl @- ys1" and ψψ: "alw ψ ys1"
using ψ by (metis ev_imp_shift)
ultimately have 0: "xl @- xs1 = yl @- ys1" by auto
hence "prefix xl yl ∨ prefix yl xl" using shift_prefix_cases by auto
thus ?thesis proof
assume "prefix xl yl"
then obtain yl1 where yl: "yl = xl @ yl1" by (elim prefixE)
have xs1': "xs1 = yl1 @- ys1" using 0 unfolding yl by simp
have "alw φ ys1" using φφ unfolding xs1' by (metis alw_shift)
hence "alw (φ aand ψ) ys1" using ψψ unfolding alw_aand by auto
thus ?thesis unfolding xs2 by (auto intro: alw_ev_shift)
next
assume "prefix yl xl"
then obtain xl1 where xl: "xl = yl @ xl1" by (elim prefixE)
have ys1': "ys1 = xl1 @- xs1" using 0 unfolding xl by simp
have "alw ψ xs1" using ψψ unfolding ys1' by (metis alw_shift)
hence "alw (φ aand ψ) xs1" using φφ unfolding alw_aand by auto
thus ?thesis unfolding xs1 by (auto intro: alw_ev_shift)
qed
qed

lemma ev_alw_alw_impl:
assumes "ev (alw φ) xs" and "alw (alw φ impl ev ψ) xs"
shows "ev ψ xs"
using assms by induct auto

lemma ev_alw_stl[simp]: "ev (alw φ) (stl x) ⟷ ev (alw φ) x"
by (metis (full_types) alw_nxt ev_nxt nxt.simps)

lemma alw_alw_impl_ev:
"alw (alw φ impl ev ψ) = (ev (alw φ) impl alw (ev ψ))" (is "?A = ?B")
proof-
{fix xs assume "?A xs ∧ ev (alw φ) xs" hence "alw (ev ψ) xs"
by coinduct (auto elim: ev_alw_alw_impl)
}
moreover
{fix xs assume "?B xs" hence "?A xs"
by coinduct auto
}
ultimately show ?thesis by blast
qed

lemma ev_alw_impl:
assumes "ev φ xs" and "alw (φ impl ψ) xs"  shows "ev ψ xs"
using assms by induct auto

lemma ev_alw_impl_ev:
assumes "ev φ xs" and "alw (φ impl ev ψ) xs"  shows "ev ψ xs"
using ev_alw_impl[OF assms] by simp

lemma alw_mp:
assumes "alw φ xs" and "alw (φ impl ψ) xs"
shows "alw ψ xs"
proof-
{assume "alw φ xs ∧ alw (φ impl ψ) xs" hence ?thesis
by coinduct auto
}
thus ?thesis using assms by auto
qed

lemma all_imp_alw:
assumes "⋀ xs. φ xs"  shows "alw φ xs"
proof-
{assume "∀ xs. φ xs"
hence ?thesis by coinduct auto
}
thus ?thesis using assms by auto
qed

lemma alw_impl_ev_alw:
assumes "alw (φ impl ev ψ) xs"
shows "alw (ev φ impl ev ψ) xs"
using assms by coinduct (auto dest: ev_alw_impl)

lemma ev_holds_sset:
"ev (holds P) xs ⟷ (∃ x ∈ sset xs. P x)" (is "?L ⟷ ?R")
proof safe
assume ?L thus ?R by induct (metis holds.simps stream.set_sel(1), metis stl_sset)
next
fix x assume "x ∈ sset xs" "P x"
thus ?L by (induct rule: sset_induct) (simp_all add: ev.base ev.step)
qed

text ‹LTL as a program logic:›
lemma alw_invar:
assumes "φ xs" and "alw (φ impl nxt φ) xs"
shows "alw φ xs"
proof-
{assume "φ xs ∧ alw (φ impl nxt φ) xs" hence ?thesis
by coinduct auto
}
thus ?thesis using assms by auto
qed

lemma variance:
assumes 1: "φ xs" and 2: "alw (φ impl (ψ or nxt φ)) xs"
shows "(alw φ or ev ψ) xs"
proof-
{assume "¬ ev ψ xs" hence "alw (not ψ) xs" unfolding not_ev[symmetric] .
moreover have "alw (not ψ impl (φ impl nxt φ)) xs"
using 2 by coinduct auto
ultimately have "alw (φ impl nxt φ) xs" by(auto dest: alw_mp)
with 1 have "alw φ xs" by(rule alw_invar)
}
thus ?thesis by blast
qed

lemma ev_alw_imp_nxt:
assumes e: "ev φ xs" and a: "alw (φ impl (nxt φ)) xs"
shows "ev (alw φ) xs"
proof-
obtain xl xs1 where xs: "xs = xl @- xs1" and φ: "φ xs1"
using e by (metis ev_imp_shift)
have "φ xs1 ∧ alw (φ impl (nxt φ)) xs1" using a φ unfolding xs by (metis alw_shift)
hence "alw φ xs1" by(coinduct xs1 rule: alw.coinduct) auto
thus ?thesis unfolding xs by (auto intro: alw_ev_shift)
qed

inductive ev_at :: "('a stream ⇒ bool) ⇒ nat ⇒ 'a stream ⇒ bool" for P :: "'a stream ⇒ bool" where
base: "P ω ⟹ ev_at P 0 ω"
| step:"¬ P ω ⟹ ev_at P n (stl ω) ⟹ ev_at P (Suc n) ω"

inductive_simps ev_at_0[simp]: "ev_at P 0 ω"
inductive_simps ev_at_Suc[simp]: "ev_at P (Suc n) ω"

lemma ev_at_imp_snth: "ev_at P n ω ⟹ P (sdrop n ω)"
by (induction n arbitrary: ω) auto

lemma ev_at_HLD_imp_snth: "ev_at (HLD X) n ω ⟹ ω !! n ∈ X"
by (auto dest!: ev_at_imp_snth simp: HLD_iff)

lemma ev_at_HLD_single_imp_snth: "ev_at (HLD {x}) n ω ⟹ ω !! n = x"
by (drule ev_at_HLD_imp_snth) simp

lemma ev_at_unique: "ev_at P n ω ⟹ ev_at P m ω ⟹ n = m"
proof (induction arbitrary: m rule: ev_at.induct)
case (base ω) then show ?case
by (simp add: ev_at.simps[of _ _ ω])
next
case (step ω n) from step.prems step.hyps step.IH[of "m - 1"] show ?case
by (auto simp add: ev_at.simps[of _ _ ω])
qed

lemma ev_iff_ev_at: "ev P ω ⟷ (∃n. ev_at P n ω)"
proof
assume "ev P ω" then show "∃n. ev_at P n ω"
by (induction rule: ev_induct_strong) (auto intro: ev_at.intros)
next
assume "∃n. ev_at P n ω"
then obtain n where "ev_at P n ω"
by auto
then show "ev P ω"
by induction auto
qed

lemma ev_at_shift: "ev_at (HLD X) i (stake (Suc i) ω @- ω' :: 's stream) ⟷ ev_at (HLD X) i ω"
by (induction i arbitrary: ω) (auto simp: HLD_iff)

lemma ev_iff_ev_at_unique: "ev P ω ⟷ (∃!n. ev_at P n ω)"
by (auto intro: ev_at_unique simp: ev_iff_ev_at)

lemma alw_HLD_iff_streams: "alw (HLD X) ω ⟷ ω ∈ streams X"
proof
assume "alw (HLD X) ω" then show "ω ∈ streams X"
proof (coinduction arbitrary: ω)
case (streams ω) then show ?case by (cases ω) auto
qed
next
assume "ω ∈ streams X" then show "alw (HLD X) ω"
proof (coinduction arbitrary: ω)
case (alw ω) then show ?case by (cases ω) auto
qed
qed

lemma not_HLD: "not (HLD X) = HLD (- X)"
by (auto simp: HLD_iff)

lemma not_alw_iff: "¬ (alw P ω) ⟷ ev (not P) ω"
using not_alw[of P] by (simp add: fun_eq_iff)

lemma not_ev_iff: "¬ (ev P ω) ⟷ alw (not P) ω"
using not_alw_iff[of "not P" ω, symmetric]  by simp

lemma ev_Stream: "ev P (x ## s) ⟷ P (x ## s) ∨ ev P s"
by (auto elim: ev.cases)

lemma alw_ev_imp_ev_alw:
assumes "alw (ev P) ω" shows "ev (P aand alw (ev P)) ω"
proof -
have "ev P ω" using assms by auto
from this assms show ?thesis
by induct auto
qed

lemma ev_False: "ev (λx. False) ω ⟷ False"
proof
assume "ev (λx. False) ω" then show False
by induct auto
qed auto

lemma alw_False: "alw (λx. False) ω ⟷ False"
by auto

lemma ev_iff_sdrop: "ev P ω ⟷ (∃m. P (sdrop m ω))"
proof safe
assume "ev P ω" then show "∃m. P (sdrop m ω)"
by (induct rule: ev_induct_strong) (auto intro: exI[of _ 0] exI[of _ "Suc n" for n])
next
fix m assume "P (sdrop m ω)" then show "ev P ω"
by (induct m arbitrary: ω) auto
qed

lemma alw_iff_sdrop: "alw P ω ⟷ (∀m. P (sdrop m ω))"
proof safe
fix m assume "alw P ω" then show "P (sdrop m ω)"
by (induct m arbitrary: ω) auto
next
assume "∀m. P (sdrop m ω)" then show "alw P ω"
by (coinduction arbitrary: ω) (auto elim: allE[of _ 0] allE[of _ "Suc n" for n])
qed

lemma infinite_iff_alw_ev: "infinite {m. P (sdrop m ω)} ⟷ alw (ev P) ω"
unfolding infinite_nat_iff_unbounded_le alw_iff_sdrop ev_iff_sdrop
by simp (metis le_Suc_ex le_add1)

lemma alw_inv:
assumes stl: "⋀s. f (stl s) = stl (f s)"
shows "alw P (f s) ⟷ alw (λx. P (f x)) s"
proof
assume "alw P (f s)" then show "alw (λx. P (f x)) s"
by (coinduction arbitrary: s rule: alw_coinduct)
(auto simp: stl)
next
assume "alw (λx. P (f x)) s" then show "alw P (f s)"
by (coinduction arbitrary: s rule: alw_coinduct) (auto simp flip: stl)
qed

lemma ev_inv:
assumes stl: "⋀s. f (stl s) = stl (f s)"
shows "ev P (f s) ⟷ ev (λx. P (f x)) s"
proof
assume "ev P (f s)" then show "ev (λx. P (f x)) s"
by (induction "f s" arbitrary: s) (auto simp: stl)
next
assume "ev (λx. P (f x)) s" then show "ev P (f s)"
by induction (auto simp flip: stl)
qed

lemma alw_smap: "alw P (smap f s) ⟷ alw (λx. P (smap f x)) s"
by (rule alw_inv) simp

lemma ev_smap: "ev P (smap f s) ⟷ ev (λx. P (smap f x)) s"
by (rule ev_inv) simp

lemma alw_cong:
assumes P: "alw P ω" and eq: "⋀ω. P ω ⟹ Q1 ω ⟷ Q2 ω"
shows "alw Q1 ω ⟷ alw Q2 ω"
proof -
from eq have "(alw P aand Q1) = (alw P aand Q2)" by auto
then have "alw (alw P aand Q1) ω = alw (alw P aand Q2) ω" by auto
with P show "alw Q1 ω ⟷ alw Q2 ω"
by (simp add: alw_aand)
qed

lemma ev_cong:
assumes P: "alw P ω" and eq: "⋀ω. P ω ⟹ Q1 ω ⟷ Q2 ω"
shows "ev Q1 ω ⟷ ev Q2 ω"
proof -
from P have "alw (λxs. Q1 xs ⟶ Q2 xs) ω" by (rule alw_mono) (simp add: eq)
moreover from P have "alw (λxs. Q2 xs ⟶ Q1 xs) ω" by (rule alw_mono) (simp add: eq)
moreover note ev_alw_impl[of Q1 ω Q2] ev_alw_impl[of Q2 ω Q1]
ultimately show "ev Q1 ω ⟷ ev Q2 ω"
by auto
qed

lemma alwD: "alw P x ⟹ P x"
by auto

lemma alw_alwD: "alw P ω ⟹ alw (alw P) ω"
by simp

lemma alw_ev_stl: "alw (ev P) (stl ω) ⟷ alw (ev P) ω"
by (auto intro: alw.intros)

lemma holds_Stream: "holds P (x ## s) ⟷ P x"
by simp

lemma holds_eq1[simp]: "holds ((=) x) = HLD {x}"
by rule (auto simp: HLD_iff)

lemma holds_eq2[simp]: "holds (λy. y = x) = HLD {x}"
by rule (auto simp: HLD_iff)

lemma not_holds_eq[simp]: "holds (- (=) x) = not (HLD {x})"
by rule (auto simp: HLD_iff)

text ‹Strong until›

context
notes [[inductive_internals]]
begin

inductive suntil (infix "suntil" 60) for φ ψ where
base: "ψ ω ⟹ (φ suntil ψ) ω"
| step: "φ ω ⟹ (φ suntil ψ) (stl ω) ⟹ (φ suntil ψ) ω"

inductive_simps suntil_Stream: "(φ suntil ψ) (x ## s)"

end

lemma suntil_induct_strong[consumes 1, case_names base step]:
"(φ suntil ψ) x ⟹
(⋀ω. ψ ω ⟹ P ω) ⟹
(⋀ω. φ ω ⟹ ¬ ψ ω ⟹ (φ suntil ψ) (stl ω) ⟹ P (stl ω) ⟹ P ω) ⟹ P x"
using suntil.induct[of φ ψ x P] by blast

lemma ev_suntil: "(φ suntil ψ) ω ⟹ ev ψ ω"
by (induct rule: suntil.induct) auto

lemma suntil_inv:
assumes stl: "⋀s. f (stl s) = stl (f s)"
shows "(P suntil Q) (f s) ⟷ ((λx. P (f x)) suntil (λx. Q (f x))) s"
proof
assume "(P suntil Q) (f s)" then show "((λx. P (f x)) suntil (λx. Q (f x))) s"
by (induction "f s" arbitrary: s) (auto simp: stl intro: suntil.intros)
next
assume "((λx. P (f x)) suntil (λx. Q (f x))) s" then show "(P suntil Q) (f s)"
by induction (auto simp flip: stl intro: suntil.intros)
qed

lemma suntil_smap: "(P suntil Q) (smap f s) ⟷ ((λx. P (smap f x)) suntil (λx. Q (smap f x))) s"
by (rule suntil_inv) simp

lemma hld_smap: "HLD x (smap f s) = holds (λy. f y ∈ x) s"
by (simp add: HLD_def)

lemma suntil_mono:
assumes eq: "⋀ω. P ω ⟹ Q1 ω ⟹ Q2 ω" "⋀ω. P ω ⟹ R1 ω ⟹ R2 ω"
assumes *: "(Q1 suntil R1) ω" "alw P ω" shows "(Q2 suntil R2) ω"
using * by induct (auto intro: eq suntil.intros)

lemma suntil_cong:
"alw P ω ⟹ (⋀ω. P ω ⟹ Q1 ω ⟷ Q2 ω) ⟹ (⋀ω. P ω ⟹ R1 ω ⟷ R2 ω) ⟹
(Q1 suntil R1) ω ⟷ (Q2 suntil R2) ω"
using suntil_mono[of P Q1 Q2 R1 R2 ω] suntil_mono[of P Q2 Q1 R2 R1 ω] by auto

lemma ev_suntil_iff: "ev (P suntil Q) ω ⟷ ev Q ω"
proof
assume "ev (P suntil Q) ω" then show "ev Q ω"
by induct (auto dest: ev_suntil)
next
assume "ev Q ω" then show "ev (P suntil Q) ω"
by induct (auto intro: suntil.intros)
qed

lemma true_suntil: "((λ_. True) suntil P) = ev P"
by (simp add: suntil_def ev_def)

lemma suntil_lfp: "(φ suntil ψ) = lfp (λP s. ψ s ∨ (φ s ∧ P (stl s)))"
by (simp add: suntil_def)

lemma sfilter_P[simp]: "P (shd s) ⟹ sfilter P s = shd s ## sfilter P (stl s)"
using sfilter_Stream[of P "shd s" "stl s"] by simp

lemma sfilter_not_P[simp]: "¬ P (shd s) ⟹ sfilter P s = sfilter P (stl s)"
using sfilter_Stream[of P "shd s" "stl s"] by simp

lemma sfilter_eq:
assumes "ev (holds P) s"
shows "sfilter P s = x ## s' ⟷
P x ∧ (not (holds P) suntil (HLD {x} aand nxt (λs. sfilter P s = s'))) s"
using assms
by (induct rule: ev_induct_strong)
(auto simp add: HLD_iff intro: suntil.intros elim: suntil.cases)

lemma sfilter_streams:
"alw (ev (holds P)) ω ⟹ ω ∈ streams A ⟹ sfilter P ω ∈ streams {x∈A. P x}"
proof (coinduction arbitrary: ω)
case (streams ω)
then have "ev (holds P) ω" by blast
from this streams show ?case
by (induct rule: ev_induct_strong) (auto elim: streamsE)
qed

lemma alw_sfilter:
assumes *: "alw (ev (holds P)) s"
shows "alw Q (sfilter P s) ⟷ alw (λx. Q (sfilter P x)) s"
proof
assume "alw Q (sfilter P s)" with * show "alw (λx. Q (sfilter P x)) s"
proof (coinduction arbitrary: s rule: alw_coinduct)
case (stl s)
then have "ev (holds P) s"
by blast
from this stl show ?case
by (induct rule: ev_induct_strong) auto
qed auto
next
assume "alw (λx. Q (sfilter P x)) s" with * show "alw Q (sfilter P s)"
proof (coinduction arbitrary: s rule: alw_coinduct)
case (stl s)
then have "ev (holds P) s"
by blast
from this stl show ?case
by (induct rule: ev_induct_strong) auto
qed auto
qed

lemma ev_sfilter:
assumes *: "alw (ev (holds P)) s"
shows "ev Q (sfilter P s) ⟷ ev (λx. Q (sfilter P x)) s"
proof
assume "ev Q (sfilter P s)" from this * show "ev (λx. Q (sfilter P x)) s"
proof (induction "sfilter P s" arbitrary: s rule: ev_induct_strong)
case (step s)
then have "ev (holds P) s"
by blast
from this step show ?case
by (induct rule: ev_induct_strong) auto
qed auto
next
assume "ev (λx. Q (sfilter P x)) s" then show "ev Q (sfilter P s)"
proof (induction rule: ev_induct_strong)
case (step s) then show ?case
by (cases "P (shd s)") auto
qed auto
qed

lemma holds_sfilter:
assumes "ev (holds Q) s" shows "holds P (sfilter Q s) ⟷ (not (holds Q) suntil (holds (Q aand P))) s"
proof
assume "holds P (sfilter Q s)" with assms show "(not (holds Q) suntil (holds (Q aand P))) s"
by (induct rule: ev_induct_strong) (auto intro: suntil.intros)
next
assume "(not (holds Q) suntil (holds (Q aand P))) s" then show "holds P (sfilter Q s)"
by induct auto
qed

lemma suntil_aand_nxt:
"(φ suntil (φ aand nxt ψ)) ω ⟷ (φ aand nxt (φ suntil ψ)) ω"
proof
assume "(φ suntil (φ aand nxt ψ)) ω" then show "(φ aand nxt (φ suntil ψ)) ω"
by induction (auto intro: suntil.intros)
next
assume "(φ aand nxt (φ suntil ψ)) ω"
then have "(φ suntil ψ) (stl ω)" "φ ω"
by auto
then show "(φ suntil (φ aand nxt ψ)) ω"
by (induction "stl ω" arbitrary: ω)
(auto elim: suntil.cases intro: suntil.intros)
qed

lemma alw_sconst: "alw P (sconst x) ⟷ P (sconst x)"
proof
assume "P (sconst x)" then show "alw P (sconst x)"
by coinduction auto
qed auto

lemma ev_sconst: "ev P (sconst x) ⟷ P (sconst x)"
proof
assume "ev P (sconst x)" then show "P (sconst x)"
by (induction "sconst x") auto
qed auto

lemma suntil_sconst: "(φ suntil ψ) (sconst x) ⟷ ψ (sconst x)"
proof
assume "(φ suntil ψ) (sconst x)" then show "ψ (sconst x)"
by (induction "sconst x") auto
qed (auto intro: suntil.intros)

lemma hld_smap': "HLD x (smap f s) = HLD (f -` x) s"
by (simp add: HLD_def)

lemma pigeonhole_stream:
assumes "alw (HLD s) ω"
assumes "finite s"
shows "∃x∈s. alw (ev (HLD {x})) ω"
proof -
have "∀i∈UNIV. ∃x∈s. ω !! i = x"
using ‹alw (HLD s) ω› by (simp add: alw_iff_sdrop HLD_iff)
from pigeonhole_infinite_rel[OF infinite_UNIV_nat ‹finite s› this]
show ?thesis
by (simp add: HLD_iff flip: infinite_iff_alw_ev)
qed

lemma ev_eq_suntil: "ev P ω ⟷ (not P suntil P) ω"
proof
assume "ev P ω" then show "((λxs. ¬ P xs) suntil P) ω"
by (induction rule: ev_induct_strong) (auto intro: suntil.intros)
qed (auto simp: ev_suntil)

section ‹Weak vs. strong until (contributed by Michael Foster, University of Sheffield)›

lemma suntil_implies_until: "(φ suntil ψ) ω ⟹ (φ until ψ) ω"
by (induct rule: suntil_induct_strong) (auto intro: UNTIL.intros)

lemma alw_implies_until: "alw φ ω ⟹ (φ until ψ) ω"
unfolding until_false[symmetric] by (auto elim: until_mono)

lemma until_ev_suntil: "(φ until ψ) ω ⟹ ev ψ ω ⟹ (φ suntil ψ) ω"
proof (rotate_tac, induction rule: ev.induct)
case (base xs)
then show ?case
by (simp add: suntil.base)
next
case (step xs)
then show ?case
by (metis UNTIL.cases suntil.base suntil.step)
qed

lemma suntil_as_until: "(φ suntil ψ) ω = ((φ until ψ) ω ∧ ev ψ ω)"
using ev_suntil suntil_implies_until until_ev_suntil by blast

lemma until_not_relesased_now: "(φ until ψ) ω ⟹ ¬ ψ ω ⟹ φ ω"
using UNTIL.cases by auto

lemma until_must_release_ev: "(φ until ψ) ω ⟹ ev (not φ) ω ⟹ ev ψ ω"
proof (rotate_tac, induction rule: ev.induct)
case (base xs)
then show ?case
using until_not_relesased_now by blast
next
case (step xs)
then show ?case
using UNTIL.cases by blast
qed

lemma until_as_suntil: "(φ until ψ) ω = ((φ suntil ψ) or (alw φ)) ω"
using alw_implies_until not_alw_iff suntil_implies_until until_ev_suntil until_must_release_ev
by blast

lemma alw_holds: "alw (holds P) (h##t) = (P h ∧ alw (holds P) t)"
by (metis alw.simps holds_Stream stream.sel(2))

lemma alw_holds2: "alw (holds P) ss = (P (shd ss) ∧ alw (holds P) (stl ss))"
by (meson alw.simps holds.elims(2) holds.elims(3))

lemma alw_eq_sconst: "(alw (HLD {h}) t) = (t = sconst h)"
unfolding sconst_alt alw_HLD_iff_streams streams_iff_sset
using stream.set_sel(1) by force

lemma sdrop_if_suntil: "(p suntil q) ω ⟹ ∃j. q (sdrop j ω) ∧ (∀k < j. p (sdrop k ω))"
proof(induction rule: suntil.induct)
case (base ω)
then show ?case
by force
next
case (step ω)
then obtain j where "q (sdrop j (stl ω))" "∀k<j. p (sdrop k (stl ω))" by blast
with step(1,2) show ?case
using ev_at_imp_snth less_Suc_eq_0_disj by (auto intro!: exI[where x="j+1"])
qed

lemma not_suntil: "(¬ (p suntil q) ω) = (¬ (p until q) ω ∨ alw (not q) ω)"
by (simp add: suntil_as_until alw_iff_sdrop ev_iff_sdrop)

lemma sdrop_until: "q (sdrop j ω) ⟹ ∀k<j. p (sdrop k ω) ⟹ (p until q) ω"
proof(induct j arbitrary: ω)
case 0
then show ?case
by (simp add: UNTIL.base)
next
case (Suc j)
then show ?case
by (metis Suc_mono UNTIL.simps sdrop.simps(1) sdrop.simps(2) zero_less_Suc)
qed

lemma sdrop_suntil: "q (sdrop j ω) ⟹ (∀k < j. p (sdrop k ω)) ⟹ (p suntil q) ω"
by (metis ev_iff_sdrop sdrop_until suntil_as_until)

lemma suntil_iff_sdrop: "(p suntil q) ω = (∃j. q (sdrop j ω) ∧ (∀k < j. p (sdrop k ω)))"
using sdrop_if_suntil sdrop_suntil by blast

end
```