Theory Sequence_LTL
section ‹Linear Temporal Logic on Streams›
theory Sequence_LTL
imports
"Sequence"
"HOL-Library.Linear_Temporal_Logic_on_Streams"
begin
subsection ‹Basics›
text ‹Avoid destroying the constant @{const holds} prematurely.›
lemmas [simp del] = holds.simps holds_eq1 holds_eq2 not_holds_eq
lemma ev_smap[iff]: "ev P (smap f w) ⟷ ev (P ∘ smap f) w" using ev_smap unfolding comp_apply by this
lemma alw_smap[iff]: "alw P (smap f w) ⟷ alw (P ∘ smap f) w" using alw_smap unfolding comp_apply by this
lemma holds_smap[iff]: "holds P (smap f w) ⟷ holds (P ∘ f) w" unfolding holds.simps by simp
lemmas [iff] = ev_sconst alw_sconst hld_smap'
lemmas [iff] = alw_ev_stl
lemma alw_ev_sdrop[iff]: "alw (ev P) (sdrop n w) ⟷ alw (ev P) w"
using alw_ev_sdrop alw_sdrop by blast
lemma alw_ev_scons[iff]: "alw (ev P) (a ## w) ⟷ alw (ev P) w" by (metis alw_ev_stl stream.sel(2))
lemma alw_ev_shift[iff]: "alw (ev P) (u @- v) ⟷ alw (ev P) v" by (induct u) (auto)
lemmas [simp del, iff] = ev_alw_stl
lemma ev_alw_sdrop[iff]: "ev (alw P) (sdrop n w) ⟷ ev (alw P) w"
using alwD alw_alw alw_sdrop ev_alw_imp_alw_ev not_ev_iff by metis
lemma ev_alw_scons[iff]: "ev (alw P) (a ## w) ⟷ ev (alw P) w" by (metis ev_alw_stl stream.sel(2))
lemma ev_alw_shift[iff]: "ev (alw P) (u @- v) ⟷ ev (alw P) v" by (induct u) (auto)
lemma holds_sconst[iff]: "holds P (sconst a) ⟷ P a" unfolding holds.simps by simp
lemma HLD_sconst[iff]: "HLD A (sconst a) ⟷ a ∈ A" unfolding HLD_def holds.simps by simp
lemma ev_alt_def: "ev φ w ⟷ (∃ u v. w = u @- v ∧ φ v)"
using ev.base ev_shift ev_imp_shift by metis
lemma ev_stl_alt_def: "ev φ (stl w) ⟷ (∃ u v. w = u @- v ∧ u ≠ [] ∧ φ v)"
unfolding ev_alt_def by (cases w) (force simp: scons_eq)
lemma ev_HLD_sset: "ev (HLD A) w ⟷ sset w ∩ A ≠ {}" unfolding HLD_def ev_holds_sset by auto
lemma alw_ev_coinduct[case_names alw_ev, consumes 1]:
assumes "R w"
assumes "⋀ w. R w ⟹ ev φ w ∧ ev R (stl w)"
shows "alw (ev φ) w"
proof -
have "ev R w" using assms(1) by rule
then show ?thesis using assms(2) by (coinduct) (metis alw_sdrop not_ev_iff sdrop_stl sdrop_wait)
qed
subsection ‹Infinite Occurrence›
abbreviation "infs P w ≡ alw (ev (holds P)) w"
abbreviation "fins P w ≡ ¬ infs P w"
lemma infs_suffix: "infs P w ⟷ (∀ u v. w = u @- v ⟶ Bex (sset v) P)"
using alwD alw_iff_sdrop alw_shift ev_holds_sset stake_sdrop by (metis (mono_tags, opaque_lifting))
lemma infs_snth: "infs P w ⟷ (∀ n. ∃ k ≥ n. P (w !! k))"
by (auto simp: alw_iff_sdrop ev_iff_sdrop holds.simps intro: le_add1 dest: le_Suc_ex)
lemma infs_infm: "infs P w ⟷ (∃⇩∞ i. P (w !! i))"
unfolding infs_snth INFM_nat_le by rule
lemma infs_coinduct[case_names infs, coinduct pred: infs]:
assumes "R w"
assumes "⋀ w. R w ⟹ Bex (sset w) P ∧ ev R (stl w)"
shows "infs P w"
using assms by (coinduct rule: alw_ev_coinduct) (auto simp: ev_holds_sset)
lemma infs_coinduct_shift[case_names infs, consumes 1]:
assumes "R w"
assumes "⋀ w. R w ⟹ ∃ u v. w = u @- v ∧ Bex (set u) P ∧ R v"
shows "infs P w"
using assms by (coinduct) (force simp: ev_stl_alt_def)
lemma infs_flat_coinduct[case_names infs_flat, consumes 1]:
assumes "R w"
assumes "⋀ u v. R (u ## v) ⟹ Bex (set u) P ∧ R v"
shows "infs P (flat w)"
using assms by (coinduction arbitrary: w rule: infs_coinduct_shift)
(metis empty_iff flat_Stream list.set(1) stream.exhaust)
lemma infs_sscan_coinduct[case_names infs_sscan, consumes 1]:
assumes "R w a"
assumes "⋀ w a. R w a ⟹ P a ∧ (∃ u v. w = u @- v ∧ u ≠ [] ∧ R v (fold f u a))"
shows "infs P (a ## sscan f w a)"
using assms(1)
proof (coinduction arbitrary: w a rule: infs_coinduct_shift)
case (infs w a)
obtain u v where 1: "P a" "w = u @- v" "u ≠ []" "R v (fold f u a)" using infs assms(2) by blast
show ?case
proof (intro exI conjI bexI)
have "sscan f w a = scan f u a @- sscan f v (fold f u a)" unfolding 1(2) by simp
also have "scan f u a = butlast (scan f u a) @ [fold f u a]"
using 1(3) by (metis last_ConsR scan_eq_nil scan_last snoc_eq_iff_butlast)
also have "a ## … @- sscan f v (fold f u a) =
(a # butlast (scan f u a)) @- fold f u a ## sscan f v (fold f u a)" by simp
finally show "a ## sscan f w a = (a # butlast (scan f u a)) @- fold f u a ## sscan f v (fold f u a)" by this
show "P a" using 1(1) by this
show "a ∈ set (a # butlast (scan f u a))" by simp
show "R v (fold f u a)" using 1(4) by this
qed rule
qed
lemma infs_mono: "(⋀ a. a ∈ sset w ⟹ P a ⟹ Q a) ⟹ infs P w ⟹ infs Q w"
unfolding infs_snth by force
lemma infs_mono_strong: "stream_all2 (λ a b. P a ⟶ Q b) u v ⟹ infs P u ⟹ infs Q v"
unfolding stream_rel_snth infs_snth by blast
lemma infs_all: "Ball (sset w) P ⟹ infs P w" unfolding infs_snth by auto
lemma infs_any: "infs P w ⟹ Bex (sset w) P" unfolding ev_holds_sset by auto
lemma infs_bot[iff]: "infs bot w ⟷ False" using infs_any by auto
lemma infs_top[iff]: "infs top w ⟷ True" by (simp add: infs_all)
lemma infs_disj[iff]: "infs (λ a. P a ∨ Q a) w ⟷ infs P w ∨ infs Q w"
unfolding infs_snth using le_trans le_cases by metis
lemma infs_bex[iff]:
assumes "finite S"
shows "infs (λ a. ∃ x ∈ S. P x a) w ⟷ (∃ x ∈ S. infs (P x) w)"
using assms infs_any by induct auto
lemma infs_bex_le_nat[iff]: "infs (λ a. ∃ k < n :: nat. P k a) w ⟷ (∃ k < n. infs (P k) w)"
proof -
have "infs (λ a. ∃ k < n. P k a) w ⟷ infs (λ a. ∃ k ∈ {k. k < n}. P k a) w" by simp
also have "… ⟷ (∃ k ∈ {k. k < n}. infs (P k) w)" by blast
also have "… ⟷ (∃ k < n. infs (P k) w)" by simp
finally show ?thesis by this
qed
lemma infs_cycle[iff]:
assumes "w ≠ []"
shows "infs P (cycle w) ⟷ Bex (set w) P"
proof
show "infs P (cycle w) ⟹ Bex (set w) P"
using assms by (auto simp: ev_holds_sset dest: alwD)
show "Bex (set w) P ⟹ infs P (cycle w)"
using assms by (coinduction rule: infs_coinduct_shift) (blast dest: cycle_decomp)
qed
end