--- a/src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy Sat Nov 14 18:37:49 2015 +0100
+++ b/src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy Sun Nov 15 12:39:51 2015 +0100
@@ -64,6 +64,10 @@
abbreviation HLD_nxt (infixr "\<cdot>" 65) where
"s \<cdot> P \<equiv> HLD s aand nxt P"
+context
+ notes [[inductive_defs]]
+begin
+
inductive ev for \<phi> where
base: "\<phi> xs \<Longrightarrow> ev \<phi> xs"
|
@@ -78,6 +82,8 @@
|
step: "\<lbrakk>\<phi> xs; (\<phi> until \<psi>) (stl xs)\<rbrakk> \<Longrightarrow> (\<phi> until \<psi>) xs"
+end
+
lemma holds_mono:
assumes holds: "holds P xs" and 0: "\<And> x. P x \<Longrightarrow> Q x"
shows "holds Q xs"
@@ -587,12 +593,18 @@
text \<open>Strong until\<close>
+context
+ notes [[inductive_defs]]
+begin
+
inductive suntil (infix "suntil" 60) for \<phi> \<psi> where
base: "\<psi> \<omega> \<Longrightarrow> (\<phi> suntil \<psi>) \<omega>"
| step: "\<phi> \<omega> \<Longrightarrow> (\<phi> suntil \<psi>) (stl \<omega>) \<Longrightarrow> (\<phi> suntil \<psi>) \<omega>"
inductive_simps suntil_Stream: "(\<phi> suntil \<psi>) (x ## s)"
+end
+
lemma suntil_induct_strong[consumes 1, case_names base step]:
"(\<phi> suntil \<psi>) x \<Longrightarrow>
(\<And>\<omega>. \<psi> \<omega> \<Longrightarrow> P \<omega>) \<Longrightarrow>