src/HOLCF/IOA/meta_theory/Sequence.thy

tuned checklist;

(*  Title:      HOLCF/IOA/meta_theory/Sequence.thy
    ID:         $Id$
    Author:     Olaf M"uller
    Copyright   1996  TU Muenchen

Sequences over flat domains with lifted elements

*)  

Sequence = Seq + 

default term

types 'a Seq = ('a::term lift)seq

consts

  Cons             ::"'a            => 'a Seq -> 'a Seq"
  Filter           ::"('a => bool)  => 'a Seq -> 'a Seq"
  Map              ::"('a => 'b)    => 'a Seq -> 'b Seq"
  Forall           ::"('a => bool)  => 'a Seq => bool"
  Last             ::"'a Seq        -> 'a lift"
  Dropwhile,
  Takewhile        ::"('a => bool)  => 'a Seq -> 'a Seq" 
  Zip              ::"'a Seq        -> 'b Seq -> ('a * 'b) Seq"
  Flat             ::"('a Seq) seq   -> 'a Seq"

  Filter2          ::"('a => bool)  => 'a Seq -> 'a Seq"

syntax

 "@Cons"     ::"'a => 'a Seq => 'a Seq"       ("(_/>>_)"  [66,65] 65)
 (* list Enumeration *)
  "_totlist"      :: args => 'a Seq                          ("[(_)!]")
  "_partlist"     :: args => 'a Seq                          ("[(_)?]")


syntax (symbols)

 "@Cons"     ::"'a => 'a Seq => 'a Seq"       ("(_\\<leadsto>_)"  [66,65] 65)
 

translations

  "a>>s" == "Cons a`s"
  "[x, xs!]"     == "x>>[xs!]"
  "[x!]"         == "x>>nil"
  "[x, xs?]"     == "x>>[xs?]"
  "[x?]"         == "x>>UU" 

defs


Cons_def      "Cons a == LAM s. Def a ## s"

Filter_def    "Filter P == sfilter`(flift2 P)"

Map_def       "Map f  == smap`(flift2 f)"

Forall_def    "Forall P == sforall (flift2 P)"

Last_def      "Last == slast"

Dropwhile_def "Dropwhile P == sdropwhile`(flift2 P)"

Takewhile_def "Takewhile P == stakewhile`(flift2 P)"

Flat_def      "Flat == sflat"

Zip_def
  "Zip == (fix`(LAM h t1 t2. case t1 of 
               nil   => nil
             | x##xs => (case t2 of 
                          nil => UU 
                        | y##ys => (case x of 
                                      Undef  => UU
                                    | Def a => (case y of 
                                                  Undef => UU
                                                | Def b => Def (a,b)##(h`xs`ys))))))"

Filter2_def    "Filter2 P == (fix`(LAM h t. case t of 
            nil => nil
	  | x##xs => (case x of Undef => UU | Def y => (if P y                                 
                     then x##(h`xs)
                     else     h`xs))))" 

rules


(* for test purposes should be deleted FIX !! *)
adm_all    "adm f"


end