src/HOLCF/IOA/meta_theory/Sequence.thy

Add icon for interface.

(*  Title:      HOLCF/IOA/meta_theory/Sequence.thy
    ID:         $Id$
    Author:     Olaf Müller

Sequences over flat domains with lifted elements.
*)

theory Sequence
imports Seq
begin

defaultsort type

types 'a Seq = "'a::type lift seq"

consts

  Consq            ::"'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        ::"('a => bool)  => 'a Seq -> 'a Seq"
  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

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


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


translations
  "a>>s"         == "Consq a$s"
  "[x, xs!]"     == "x>>[xs!]"
  "[x!]"         == "x>>nil"
  "[x, xs?]"     == "x>>[xs?]"
  "[x?]"         == "x>>UU"

defs

Consq_def:     "Consq 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
                                      UU  => UU
                                    | Def a => (case y of
                                                  UU => 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 UU => UU | Def y => (if P y
                     then x##(h$xs)
                     else     h$xs))))"

axioms  -- {* for test purposes should be deleted FIX !! *}  (* FIXME *)
  adm_all: "adm f"

ML {* use_legacy_bindings (the_context ()) *}

end