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