(* Author: Julian Brunner *) (* This is originally a part of the CAVA model checker *) theory Sequence_LTL imports Sequence "HOL-Library.Linear_Temporal_Logic_on_Streams" begin (* basics *) lemmas [iff] = ev_sconst alw_sconst ev_smap alw_smap 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 HLD_sconst[iff]: "HLD A (sconst a) ⟷ a ∈ A" unfolding HLD_def by simp lemma ev_stl: "ev φ (stl w) ⟷ (∃ u v. w = u @- v ∧ u ≠ [] ∧ φ v)" by (metis ev.base ev_shift list.distinct(1) rotate1.simps(2) rotate1_is_Nil_conv sdrop.simps(2) sdrop_wait shift_simps(2) stake_Suc stake_sdrop ) 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 (* acceptance conditions *) abbreviation "infs A w ≡ alw (ev (HLD A)) w" lemma infs_suffix: "infs A w ⟷ (∀ u v. w = u @- v ⟶ sset v ∩ A ≠ {})" using alwD alw_iff_sdrop alw_shift ev_HLD_sset stake_sdrop by metis lemma infs_snth: "infs A w ⟷ (∀ n. ∃ k ≥ n. w !! k ∈ A)" by (auto simp: alw_iff_sdrop ev_iff_sdrop HLD_iff intro: le_add1 dest: le_Suc_ex) lemma infs_infm: "infs A w ⟷ (∃⇩_{∞}i. w !! i ∈ A)" unfolding infs_snth INFM_nat_le by rule lemma infs_coinduct[case_names infs, coinduct pred: infs]: assumes "R w" assumes "⋀ w. R w ⟹ ∃ u v. w = u @- v ∧ set u ∩ A ≠ {} ∧ R v" shows "infs A w" using assms by (coinduct rule: alw_ev_coinduct) (force simp: ev_HLD_sset ev_stl) lemma infs_flat_coinduct[case_names infs_flat, consumes 1]: assumes "R xss" assumes "⋀ xs xss. R (xs ## xss) ⟹ set xs ∩ A ≠ {} ∧ R xss" shows "infs A (flat xss)" using assms by (coinduction arbitrary: xss) (metis empty_set inf_bot_left flat_Stream stream.exhaust) lemma infs_supset[trans]: "infs A w ⟹ sset w ∩ A ⊆ B ⟹ infs B w" unfolding infs_snth by force lemma infsI_sset: "sset w ⊆ A ⟹ infs A w" unfolding infs_snth by force lemma infsD_sset: "infs A w ⟹ sset w ∩ A ≠ {}" unfolding ev_HLD_sset by auto lemma infs_sset[intro!, simp]: "infs (sset w) w" by (auto intro: infsI_sset) lemma infs_UNIV[intro!, simp]: "infs UNIV w" by (auto intro: infsI_sset) lemma infs_union[iff]: "infs (A ∪ B) w ⟷ infs A w ∨ infs B w" unfolding infs_snth by (auto) (meson le_trans nat_le_linear) lemma infs_cycle[iff]: assumes "w ≠ []" shows "infs A (cycle w) ⟷ set w ∩ A ≠ {}" proof show "infs A (cycle w) ⟹ set w ∩ A ≠ {}" using assms by (auto simp: ev_HLD_sset dest: alwD) show "set w ∩ A ≠ {} ⟹ infs A (cycle w)" using assms by (coinduction rule: infs_coinduct) (blast dest: cycle_decomp) qed end