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