characterization of until in terms of strong until (and vice versa), contributed by Michael Foster
authortraytel
Wed Nov 06 09:25:53 2019 +0100 (8 days ago ago)
changeset 712581d19e844fa4d
parent 71257 9b531e611d66
child 71260 b3956a37c994
characterization of until in terms of strong until (and vice versa), contributed by Michael Foster
src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy
     1.1 --- a/src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy	Tue Nov 05 22:56:06 2019 +0100
     1.2 +++ b/src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy	Wed Nov 06 09:25:53 2019 +0100
     1.3 @@ -787,4 +787,44 @@
     1.4      by (induction rule: ev_induct_strong) (auto intro: suntil.intros)
     1.5  qed (auto simp: ev_suntil)
     1.6  
     1.7 +section \<open>Weak vs. strong until (contributed by Michael Foster, University of Sheffield)\<close>
     1.8 +
     1.9 +lemma suntil_implies_until: "(\<phi> suntil \<psi>) \<omega> \<Longrightarrow> (\<phi> until \<psi>) \<omega>"
    1.10 +  by (induct rule: suntil_induct_strong) (auto intro: UNTIL.intros)
    1.11 +
    1.12 +lemma alw_implies_until: "alw \<phi> \<omega> \<Longrightarrow> (\<phi> until \<psi>) \<omega>"
    1.13 +  unfolding until_false[symmetric] by (auto elim: until_mono)
    1.14 +
    1.15 +lemma until_ev_suntil: "(\<phi> until \<psi>) \<omega> \<Longrightarrow> ev \<psi> \<omega> \<Longrightarrow> (\<phi> suntil \<psi>) \<omega>"
    1.16 +proof (rotate_tac, induction rule: ev.induct)
    1.17 +  case (base xs)
    1.18 +  then show ?case
    1.19 +    by (simp add: suntil.base)
    1.20 +next
    1.21 +  case (step xs)
    1.22 +  then show ?case
    1.23 +    by (metis UNTIL.cases suntil.base suntil.step)
    1.24 +qed
    1.25 +
    1.26 +lemma suntil_as_until: "(\<phi> suntil \<psi>) \<omega> = ((\<phi> until \<psi>) \<omega> \<and> ev \<psi> \<omega>)"
    1.27 +  using ev_suntil suntil_implies_until until_ev_suntil by blast
    1.28 +
    1.29 +lemma until_not_relesased_now: "(\<phi> until \<psi>) \<omega> \<Longrightarrow> \<not> \<psi> \<omega> \<Longrightarrow> \<phi> \<omega>"
    1.30 +  using UNTIL.cases by auto
    1.31 +
    1.32 +lemma until_must_release_ev: "(\<phi> until \<psi>) \<omega> \<Longrightarrow> ev (not \<phi>) \<omega> \<Longrightarrow> ev \<psi> \<omega>"
    1.33 +proof (rotate_tac, induction rule: ev.induct)
    1.34 +  case (base xs)
    1.35 +  then show ?case
    1.36 +    using until_not_relesased_now by blast
    1.37 +next
    1.38 +  case (step xs)
    1.39 +  then show ?case
    1.40 +    using UNTIL.cases by blast
    1.41 +qed
    1.42 +
    1.43 +lemma until_as_suntil: "(\<phi> until \<psi>) \<omega> = ((\<phi> suntil \<psi>) or (alw \<phi>)) \<omega>"
    1.44 +  using alw_implies_until not_alw_iff suntil_implies_until until_ev_suntil until_must_release_ev
    1.45 +  by blast
    1.46 +
    1.47  end