src/HOLCF/IOA/meta_theory/Sequence.thy
author nipkow
Tue Jan 09 15:36:30 2001 +0100 (2001-01-09)
changeset 10835 f4745d77e620
parent 7229 6773ba0c36d5
child 12028 52aa183c15bb
permissions -rw-r--r--
` -> $
     1 (*  Title:      HOLCF/IOA/meta_theory/Sequence.thy
     2     ID:         $Id$
     3     Author:     Olaf M"uller
     4     Copyright   1996  TU Muenchen
     5 
     6 Sequences over flat domains with lifted elements
     7 
     8 *)  
     9 
    10 Sequence = Seq + 
    11 
    12 default term
    13 
    14 types 'a Seq = ('a::term lift)seq
    15 
    16 consts
    17 
    18   Consq            ::"'a            => 'a Seq -> 'a Seq"
    19   Filter           ::"('a => bool)  => 'a Seq -> 'a Seq"
    20   Map              ::"('a => 'b)    => 'a Seq -> 'b Seq"
    21   Forall           ::"('a => bool)  => 'a Seq => bool"
    22   Last             ::"'a Seq        -> 'a lift"
    23   Dropwhile,
    24   Takewhile        ::"('a => bool)  => 'a Seq -> 'a Seq" 
    25   Zip              ::"'a Seq        -> 'b Seq -> ('a * 'b) Seq"
    26   Flat             ::"('a Seq) seq   -> 'a Seq"
    27 
    28   Filter2          ::"('a => bool)  => 'a Seq -> 'a Seq"
    29 
    30 syntax
    31 
    32  "@Consq"         ::"'a => 'a Seq => 'a Seq"       ("(_/>>_)"  [66,65] 65)
    33  (* list Enumeration *)
    34   "_totlist"      :: args => 'a Seq                          ("[(_)!]")
    35   "_partlist"     :: args => 'a Seq                          ("[(_)?]")
    36 
    37 
    38 syntax (symbols)
    39 
    40  "@Consq"     ::"'a => 'a Seq => 'a Seq"       ("(_\\<leadsto>_)"  [66,65] 65)
    41  
    42 
    43 translations
    44 
    45   "a>>s"         == "Consq a$s"
    46   "[x, xs!]"     == "x>>[xs!]"
    47   "[x!]"         == "x>>nil"
    48   "[x, xs?]"     == "x>>[xs?]"
    49   "[x?]"         == "x>>UU" 
    50 
    51 defs
    52 
    53 
    54 Consq_def     "Consq a == LAM s. Def a ## s"
    55 
    56 Filter_def    "Filter P == sfilter$(flift2 P)"
    57 
    58 Map_def       "Map f  == smap$(flift2 f)"
    59 
    60 Forall_def    "Forall P == sforall (flift2 P)"
    61 
    62 Last_def      "Last == slast"
    63 
    64 Dropwhile_def "Dropwhile P == sdropwhile$(flift2 P)"
    65 
    66 Takewhile_def "Takewhile P == stakewhile$(flift2 P)"
    67 
    68 Flat_def      "Flat == sflat"
    69 
    70 Zip_def
    71   "Zip == (fix$(LAM h t1 t2. case t1 of 
    72                nil   => nil
    73              | x##xs => (case t2 of 
    74                           nil => UU 
    75                         | y##ys => (case x of 
    76                                       Undef  => UU
    77                                     | Def a => (case y of 
    78                                                   Undef => UU
    79                                                 | Def b => Def (a,b)##(h$xs$ys))))))"
    80 
    81 Filter2_def    "Filter2 P == (fix$(LAM h t. case t of 
    82             nil => nil
    83 	  | x##xs => (case x of Undef => UU | Def y => (if P y                                 
    84                      then x##(h$xs)
    85                      else     h$xs))))" 
    86 
    87 rules
    88 
    89 
    90 (* for test purposes should be deleted FIX !! *)
    91 adm_all    "adm f"
    92 
    93 
    94 end