--- a/src/HOLCF/FOCUS/Stream_adm.thy Tue Sep 06 20:53:27 2005 +0200
+++ b/src/HOLCF/FOCUS/Stream_adm.thy Tue Sep 06 21:51:17 2005 +0200
@@ -1,28 +1,29 @@
-(* Title: HOLCF/ex/Stream_adm.thy
+(* Title: HOLCF/ex/Stream_adm.thy
ID: $Id$
- Author: David von Oheimb, TU Muenchen
-
-Admissibility for streams
+ Author: David von Oheimb, TU Muenchen
*)
-Stream_adm = Stream + Continuity +
-
-consts
-
- stream_monoP,
- stream_antiP :: "(('a stream) set \\<Rightarrow> ('a stream) set) \\<Rightarrow> bool"
+header {* Admissibility for streams *}
-defs
-
- stream_monoP_def "stream_monoP F \\<equiv> \\<exists>Q i. \\<forall>P s. Fin i \\<le> #s \\<longrightarrow>
- (s \\<in> F P) = (stream_take i\\<cdot>s \\<in> Q \\<and> iterate i rt s \\<in> P)"
- stream_antiP_def "stream_antiP F \\<equiv> \\<forall>P x. \\<exists>Q i.
- (#x < Fin i \\<longrightarrow> (\\<forall>y. x \\<sqsubseteq> y \\<longrightarrow> y \\<in> F P \\<longrightarrow> x \\<in> F P)) \\<and>
- (Fin i <= #x \\<longrightarrow> (\\<forall>y. x \\<sqsubseteq> y \\<longrightarrow>
- (y \\<in> F P) = (stream_take i\\<cdot>y \\<in> Q \\<and> iterate i rt y \\<in> P)))"
+theory Stream_adm
+imports Stream Continuity
+begin
constdefs
+
+ stream_monoP :: "(('a stream) set \<Rightarrow> ('a stream) set) \<Rightarrow> bool"
+ "stream_monoP F \<equiv> \<exists>Q i. \<forall>P s. Fin i \<le> #s \<longrightarrow>
+ (s \<in> F P) = (stream_take i\<cdot>s \<in> Q \<and> iterate i rt s \<in> P)"
+
+ stream_antiP :: "(('a stream) set \<Rightarrow> ('a stream) set) \<Rightarrow> bool"
+ "stream_antiP F \<equiv> \<forall>P x. \<exists>Q i.
+ (#x < Fin i \<longrightarrow> (\<forall>y. x \<sqsubseteq> y \<longrightarrow> y \<in> F P \<longrightarrow> x \<in> F P)) \<and>
+ (Fin i <= #x \<longrightarrow> (\<forall>y. x \<sqsubseteq> y \<longrightarrow>
+ (y \<in> F P) = (stream_take i\<cdot>y \<in> Q \<and> iterate i rt y \<in> P)))"
+
antitonP :: "'a set => bool"
- "antitonP P \\<equiv> \\<forall>x y. x \\<sqsubseteq> y \\<longrightarrow> y\\<in>P \\<longrightarrow> x\\<in>P"
-
+ "antitonP P \<equiv> \<forall>x y. x \<sqsubseteq> y \<longrightarrow> y\<in>P \<longrightarrow> x\<in>P"
+
+ML {* use_legacy_bindings (the_context ()) *}
+
end