src/HOLCF/FOCUS/Fstream.thy
author kleing
Mon Jun 21 10:25:57 2004 +0200 (2004-06-21)
changeset 14981 e73f8140af78
parent 14535 7cb26928e70d
child 15188 9d57263faf9e
permissions -rw-r--r--
Merged in license change from Isabelle2004
oheimb@11350
     1
(*  Title: 	HOLCF/FOCUS/Fstream.thy
wenzelm@11355
     2
    ID:         $Id$
oheimb@11350
     3
    Author: 	David von Oheimb, TU Muenchen
oheimb@11350
     4
oheimb@11350
     5
FOCUS streams (with lifted elements)
oheimb@11350
     6
*)
oheimb@11350
     7
oheimb@11350
     8
(* FOCUS flat streams *)
oheimb@11350
     9
oheimb@14535
    10
Fstream = Streams + 
oheimb@11350
    11
wenzelm@12338
    12
default type
oheimb@11350
    13
oheimb@11350
    14
types 'a fstream = ('a lift) stream
oheimb@11350
    15
oheimb@11350
    16
consts
oheimb@11350
    17
oheimb@11350
    18
  fscons	:: "'a     \\<Rightarrow> 'a fstream \\<rightarrow> 'a fstream"
oheimb@11350
    19
  fsfilter	:: "'a set \\<Rightarrow> 'a fstream \\<rightarrow> 'a fstream"
oheimb@11350
    20
oheimb@11350
    21
syntax
oheimb@11350
    22
oheimb@11350
    23
  "@emptystream":: "'a fstream" 			("<>")
oheimb@11350
    24
  "@fscons"	:: "'a \\<Rightarrow> 'a fstream \\<Rightarrow> 'a fstream"	("(_~>_)"    [66,65] 65)
oheimb@11350
    25
  "@fsfilter"	:: "'a set \\<Rightarrow> 'a fstream \\<Rightarrow> 'a fstream"	("(_'(C')_)" [64,63] 63)
oheimb@11350
    26
oheimb@11350
    27
syntax (xsymbols)
oheimb@11350
    28
oheimb@11350
    29
  "@fscons"	:: "'a \\<Rightarrow> 'a fstream \\<Rightarrow> 'a fstream"	("(_\\<leadsto>_)"
oheimb@11350
    30
								     [66,65] 65)
oheimb@11350
    31
  "@fsfilter"	:: "'a set \\<Rightarrow> 'a fstream \\<Rightarrow> 'a fstream" ("(_\\<copyright>_)"
oheimb@11350
    32
								     [64,63] 63)
oheimb@11350
    33
translations
oheimb@11350
    34
oheimb@11350
    35
  "<>"    => "\\<bottom>"
oheimb@11350
    36
  "a~>s"  == "fscons a\\<cdot>s"
oheimb@11350
    37
  "A(C)s" == "fsfilter A\\<cdot>s"
oheimb@11350
    38
oheimb@11350
    39
defs
oheimb@11350
    40
skalberg@14171
    41
  fscons_def	"fscons a   \\<equiv> \\<Lambda> s. Def a && s"
oheimb@11350
    42
  fsfilter_def  "fsfilter A \\<equiv> sfilter\\<cdot>(flift2 (\\<lambda>x. x\\<in>A))"
oheimb@11350
    43
oheimb@11350
    44
end