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