src/HOLCF/IOA/meta_theory/Seq.thy
author nipkow
Tue Jan 09 15:36:30 2001 +0100 (2001-01-09)
changeset 10835 f4745d77e620
parent 5976 44290b71a85f
child 12218 6597093b77e7
permissions -rw-r--r--
` -> $
     1 (*  Title:      HOLCF/IOA/meta_theory/Seq.thy
     2     ID:         $Id$
     3     Author:     Olaf M"uller
     4     Copyright   1996  TU Muenchen
     5 
     6 Partial, Finite and Infinite Sequences (lazy lists), modeled as domain.
     7 *)  
     8 
     9 
    10 Seq = HOLCF + Inductive +
    11 
    12 domain 'a seq = nil | "##" (HD::'a) (lazy TL::'a seq)  (infixr 65) 
    13 
    14 
    15 consts    
    16    sfilter       :: "('a -> tr) -> 'a seq -> 'a seq"  
    17    smap          :: "('a -> 'b) -> 'a seq -> 'b seq"
    18    sforall       :: "('a -> tr) => 'a seq => bool"
    19    sforall2      :: "('a -> tr) -> 'a seq -> tr"
    20    slast         :: "'a seq     -> 'a"
    21    sconc         :: "'a seq     -> 'a seq -> 'a seq"
    22    sdropwhile,
    23    stakewhile    ::"('a -> tr)  -> 'a seq -> 'a seq"  
    24    szip          ::"'a seq      -> 'b seq -> ('a*'b) seq"  
    25    sflat        :: "('a seq) seq  -> 'a seq"
    26 
    27    sfinite       :: "'a seq set"
    28    Partial       ::"'a seq => bool"
    29    Infinite      ::"'a seq => bool"
    30 
    31    nproj        :: "nat => 'a seq => 'a"
    32    sproj        :: "nat => 'a seq => 'a seq"
    33 
    34 syntax
    35    "@@"		:: "'a seq => 'a seq => 'a seq"	(infixr 65)
    36    "Finite"     :: "'a seq => bool"
    37 
    38 translations
    39    "xs @@ ys" == "sconc$xs$ys"
    40    "Finite x" == "x:sfinite"
    41    "~(Finite x)" =="x~:sfinite"
    42 
    43 defs 
    44 
    45 
    46 
    47 (* f not possible at lhs, as "pattern matching" only for % x arguments,
    48    f cannot be written at rhs in front, as fix_eq3 does not apply later *)
    49 smap_def
    50   "smap == (fix$(LAM h f tr. case tr of 
    51       nil   => nil
    52     | x##xs => f$x ## h$f$xs))"
    53 
    54 sfilter_def       
    55   "sfilter == (fix$(LAM h P t. case t of 
    56 	   nil => nil
    57 	 | x##xs => If P$x                                 
    58                     then x##(h$P$xs)
    59                     else     h$P$xs
    60                     fi))" 
    61 sforall_def
    62   "sforall P t == (sforall2$P$t ~=FF)" 
    63 
    64 
    65 sforall2_def
    66   "sforall2 == (fix$(LAM h P t. case t of 
    67 	   nil => TT
    68 	 | x##xs => P$x andalso h$P$xs))"
    69   
    70 sconc_def
    71   "sconc == (fix$(LAM h t1 t2. case t1 of 
    72                nil       => t2
    73              | x##xs => x##(h$xs$t2)))"
    74 
    75 slast_def
    76   "slast == (fix$(LAM h t. case t of 
    77 	   nil => UU
    78 	 | x##xs => (If is_nil$xs                              
    79                           then x
    80                          else h$xs fi)))"
    81 
    82 stakewhile_def      
    83   "stakewhile == (fix$(LAM h P t. case t of 
    84 	   nil => nil
    85 	 | x##xs => If P$x                                 
    86                     then x##(h$P$xs)
    87                     else nil
    88                     fi))" 
    89 sdropwhile_def
    90   "sdropwhile == (fix$(LAM h P t. case t of 
    91 	   nil => nil
    92 	 | x##xs => If P$x                                 
    93                     then h$P$xs
    94                     else t
    95                     fi))" 
    96 sflat_def
    97   "sflat == (fix$(LAM h t. case t of 
    98 	   nil => nil
    99 	 | x##xs => x @@ (h$xs)))"
   100 
   101 szip_def
   102   "szip == (fix$(LAM h t1 t2. case t1 of 
   103                nil   => nil
   104              | x##xs => (case t2 of 
   105                           nil => UU 
   106                         | y##ys => <x,y>##(h$xs$ys))))"
   107 
   108 Partial_def
   109   "Partial x  == (seq_finite x) & ~(Finite x)"
   110 
   111 Infinite_def
   112   "Infinite x == ~(seq_finite x)"
   113 
   114 
   115 inductive "sfinite" 
   116    intrs  
   117     sfinite_0  "nil:sfinite"
   118     sfinite_n  "[|tr:sfinite;a~=UU|] ==> (a##tr) : sfinite"
   119 
   120 
   121 end