src/HOLCF/IOA/meta_theory/Seq.thy
author mueller
Wed Apr 30 11:20:15 1997 +0200 (1997-04-30)
changeset 3071 981258186b71
child 3275 3f53f2c876f4
permissions -rw-r--r--
New meta theory for IOA based on HOLCF.
mueller@3071
     1
(*  Title:      HOLCF/IOA/meta_theory/Seq.thy
mueller@3071
     2
    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
mueller@3071
    10
Seq = HOLCF + 
mueller@3071
    11
mueller@3071
    12
domain 'a seq = nil | "##" (HD::'a) (lazy TL::'a seq)  (cinfixr 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@3071
    32
mueller@3071
    33
syntax
mueller@3071
    34
   "@@"		:: "'a seq => 'a seq => 'a seq"	(infixr 65)
mueller@3071
    35
   "Finite"     :: "'a seq => bool"
mueller@3071
    36
mueller@3071
    37
translations
mueller@3071
    38
   "xs @@ ys" == "sconc`xs`ys"
mueller@3071
    39
   "Finite x" == "x:sfinite"
mueller@3071
    40
   "~(Finite x)" =="x~:sfinite"
mueller@3071
    41
mueller@3071
    42
defs 
mueller@3071
    43
mueller@3071
    44
mueller@3071
    45
mueller@3071
    46
(* f not possible at lhs, as "pattern matching" only for % x arguments,
mueller@3071
    47
   f cannot be written at rhs in front, as fix_eq3 does not apply later *)
mueller@3071
    48
smap_def
mueller@3071
    49
  "smap == (fix`(LAM h f tr. case tr of 
mueller@3071
    50
      nil   => nil
mueller@3071
    51
    | x##xs => f`x ## h`f`xs))"
mueller@3071
    52
mueller@3071
    53
sfilter_def       
mueller@3071
    54
  "sfilter == (fix`(LAM h P t. case t of 
mueller@3071
    55
	   nil => nil
mueller@3071
    56
	 | x##xs => If P`x                                 
mueller@3071
    57
                    then x##(h`P`xs)
mueller@3071
    58
                    else     h`P`xs
mueller@3071
    59
                    fi))" 
mueller@3071
    60
sforall_def
mueller@3071
    61
  "sforall P t == (sforall2`P`t ~=FF)" 
mueller@3071
    62
mueller@3071
    63
mueller@3071
    64
sforall2_def
mueller@3071
    65
  "sforall2 == (fix`(LAM h P t. case t of 
mueller@3071
    66
	   nil => TT
mueller@3071
    67
	 | x##xs => P`x andalso h`P`xs))"
mueller@3071
    68
  
mueller@3071
    69
sconc_def
mueller@3071
    70
  "sconc == (fix`(LAM h t1 t2. case t1 of 
mueller@3071
    71
               nil       => t2
mueller@3071
    72
             | x##xs => x##(h`xs`t2)))"
mueller@3071
    73
mueller@3071
    74
slast_def
mueller@3071
    75
  "slast == (fix`(LAM h t. case t of 
mueller@3071
    76
	   nil => UU
mueller@3071
    77
	 | x##xs => (If is_nil`xs                              
mueller@3071
    78
                          then x
mueller@3071
    79
                         else h`xs fi)))"
mueller@3071
    80
mueller@3071
    81
stakewhile_def      
mueller@3071
    82
  "stakewhile == (fix`(LAM h P t. case t of 
mueller@3071
    83
	   nil => nil
mueller@3071
    84
	 | x##xs => If P`x                                 
mueller@3071
    85
                    then x##(h`P`xs)
mueller@3071
    86
                    else nil
mueller@3071
    87
                    fi))" 
mueller@3071
    88
sdropwhile_def
mueller@3071
    89
  "sdropwhile == (fix`(LAM h P t. case t of 
mueller@3071
    90
	   nil => nil
mueller@3071
    91
	 | x##xs => If P`x                                 
mueller@3071
    92
                    then h`P`xs
mueller@3071
    93
                    else t
mueller@3071
    94
                    fi))" 
mueller@3071
    95
sflat_def
mueller@3071
    96
  "sflat == (fix`(LAM h t. case t of 
mueller@3071
    97
	   nil => nil
mueller@3071
    98
	 | x##xs => x @@ (h`xs)))"
mueller@3071
    99
mueller@3071
   100
szip_def
mueller@3071
   101
  "szip == (fix`(LAM h t1 t2. case t1 of 
mueller@3071
   102
               nil   => nil
mueller@3071
   103
             | x##xs => (case t2 of 
mueller@3071
   104
                          nil => UU 
mueller@3071
   105
                        | y##ys => <x,y>##(h`xs`ys))))"
mueller@3071
   106
mueller@3071
   107
mueller@3071
   108
proj_def 
mueller@3071
   109
 "nproj == (%n tr.HD`(iterate n TL tr))"   
mueller@3071
   110
mueller@3071
   111
Partial_def
mueller@3071
   112
  "Partial x  == (seq_finite x) & ~(Finite x)"
mueller@3071
   113
mueller@3071
   114
Infinite_def
mueller@3071
   115
  "Infinite x == ~(seq_finite x)"
mueller@3071
   116
mueller@3071
   117
mueller@3071
   118
inductive "sfinite" 
mueller@3071
   119
   intrs  
mueller@3071
   120
    sfinite_0  "nil:sfinite"
mueller@3071
   121
    sfinite_n  "[|tr:sfinite;a~=UU|] ==> (a##tr) : sfinite"
mueller@3071
   122
mueller@3071
   123
mueller@3071
   124
end