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