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 (* TODO: these cannot be applied successively to simplify infs due to introduction of ∘ avoid or add extra simplification rules for infs *) 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