src/HOLCF/FOCUS/Stream_adm.thy
author oheimb
Thu May 31 16:53:00 2001 +0200 (2001-05-31)
changeset 11350 4c55b020d6ee
child 11355 778c369559d9
permissions -rw-r--r--
added FOCUS including the One-Element Buffer by Manfred Broy
oheimb@11350
     1
(*  Title: 	HOLCF/ex/Stream_adm.thy
oheimb@11350
     2
    ID:         $ $
oheimb@11350
     3
    Author: 	David von Oheimb, TU Muenchen
oheimb@11350
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
oheimb@11350
     5
oheimb@11350
     6
Admissibility for streams
oheimb@11350
     7
*)
oheimb@11350
     8
oheimb@11350
     9
Stream_adm = Stream + Continuity +
oheimb@11350
    10
oheimb@11350
    11
consts
oheimb@11350
    12
oheimb@11350
    13
  stream_monoP,
oheimb@11350
    14
  stream_antiP	:: "(('a stream) set \\<Rightarrow> ('a stream) set) \\<Rightarrow> bool"
oheimb@11350
    15
oheimb@11350
    16
defs
oheimb@11350
    17
oheimb@11350
    18
  stream_monoP_def "stream_monoP F \\<equiv> \\<exists>Q i. \\<forall>P s. Fin i \\<le> #s \\<longrightarrow> 
oheimb@11350
    19
			s \\<in> F P = (stream_take i\\<cdot>s \\<in> Q \\<and> iterate i rt s \\<in> P)"
oheimb@11350
    20
  stream_antiP_def "stream_antiP F \\<equiv> \\<forall>P x. \\<exists>Q i. 
oheimb@11350
    21
		(#x  < Fin i \\<longrightarrow> (\\<forall>y. x \\<sqsubseteq> y \\<longrightarrow> y \\<in> F P \\<longrightarrow> x \\<in> F P)) \\<and>
oheimb@11350
    22
		(Fin i <= #x \\<longrightarrow> (\\<forall>y. x \\<sqsubseteq> y \\<longrightarrow> 
oheimb@11350
    23
		y \\<in> F P = (stream_take i\\<cdot>y \\<in> Q \\<and> iterate i rt y \\<in> P)))"
oheimb@11350
    24
oheimb@11350
    25
constdefs
oheimb@11350
    26
  antitonP :: "'a set => bool"
oheimb@11350
    27
 "antitonP P \\<equiv> \\<forall>x y. x \\<sqsubseteq> y \\<longrightarrow> y\\<in>P \\<longrightarrow> x\\<in>P"
oheimb@11350
    28
  
oheimb@11350
    29
end