(* 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