characterization of until in terms of strong until (and vice versa), contributed by Michael Foster

--- a/src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy	Tue Nov 05 22:56:06 2019 +0100
+++ b/src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy	Wed Nov 06 09:25:53 2019 +0100
@@ -787,4 +787,44 @@
     by (induction rule: ev_induct_strong) (auto intro: suntil.intros)
 qed (auto simp: ev_suntil)
 
+section \<open>Weak vs. strong until (contributed by Michael Foster, University of Sheffield)\<close>
+
+lemma suntil_implies_until: "(\<phi> suntil \<psi>) \<omega> \<Longrightarrow> (\<phi> until \<psi>) \<omega>"
+  by (induct rule: suntil_induct_strong) (auto intro: UNTIL.intros)
+
+lemma alw_implies_until: "alw \<phi> \<omega> \<Longrightarrow> (\<phi> until \<psi>) \<omega>"
+  unfolding until_false[symmetric] by (auto elim: until_mono)
+
+lemma until_ev_suntil: "(\<phi> until \<psi>) \<omega> \<Longrightarrow> ev \<psi> \<omega> \<Longrightarrow> (\<phi> suntil \<psi>) \<omega>"
+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: "(\<phi> suntil \<psi>) \<omega> = ((\<phi> until \<psi>) \<omega> \<and> ev \<psi> \<omega>)"
+  using ev_suntil suntil_implies_until until_ev_suntil by blast
+
+lemma until_not_relesased_now: "(\<phi> until \<psi>) \<omega> \<Longrightarrow> \<not> \<psi> \<omega> \<Longrightarrow> \<phi> \<omega>"
+  using UNTIL.cases by auto
+
+lemma until_must_release_ev: "(\<phi> until \<psi>) \<omega> \<Longrightarrow> ev (not \<phi>) \<omega> \<Longrightarrow> ev \<psi> \<omega>"
+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: "(\<phi> until \<psi>) \<omega> = ((\<phi> suntil \<psi>) or (alw \<phi>)) \<omega>"
+  using alw_implies_until not_alw_iff suntil_implies_until until_ev_suntil until_must_release_ev
+  by blast
+
 end