3071
|
1 |
(* Title: HOLCF/IOA/meta_theory/Sequence.thy
|
3275
|
2 |
ID: $Id$
|
3071
|
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 |
|
3952
|
16 |
consts
|
3071
|
17 |
|
|
18 |
Cons ::"'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 |
"@Cons" ::"'a => 'a Seq => 'a Seq" ("(_>>_)" [66,65] 65)
|
|
33 |
|
|
34 |
syntax (symbols)
|
|
35 |
|
|
36 |
"@Cons" ::"'a => 'a Seq => 'a Seq" ("(_\\<leadsto>_)" [66,65] 65)
|
|
37 |
|
|
38 |
|
|
39 |
translations
|
|
40 |
|
|
41 |
"a>>s" == "Cons a`s"
|
|
42 |
|
|
43 |
defs
|
|
44 |
|
|
45 |
|
|
46 |
Cons_def "Cons a == LAM s. Def a ## s"
|
|
47 |
|
|
48 |
Filter_def "Filter P == sfilter`(flift2 P)"
|
|
49 |
|
|
50 |
Map_def "Map f == smap`(flift2 f)"
|
|
51 |
|
|
52 |
Forall_def "Forall P == sforall (flift2 P)"
|
|
53 |
|
|
54 |
Last_def "Last == slast"
|
|
55 |
|
|
56 |
Dropwhile_def "Dropwhile P == sdropwhile`(flift2 P)"
|
|
57 |
|
|
58 |
Takewhile_def "Takewhile P == stakewhile`(flift2 P)"
|
|
59 |
|
|
60 |
Flat_def "Flat == sflat"
|
|
61 |
|
|
62 |
Zip_def
|
|
63 |
"Zip == (fix`(LAM h t1 t2. case t1 of
|
|
64 |
nil => nil
|
|
65 |
| x##xs => (case t2 of
|
|
66 |
nil => UU
|
|
67 |
| y##ys => (case x of
|
|
68 |
Undef => UU
|
|
69 |
| Def a => (case y of
|
|
70 |
Undef => UU
|
|
71 |
| Def b => Def (a,b)##(h`xs`ys))))))"
|
|
72 |
|
|
73 |
Filter2_def "Filter2 P == (fix`(LAM h t. case t of
|
|
74 |
nil => nil
|
|
75 |
| x##xs => (case x of Undef => UU | Def y => (if P y
|
|
76 |
then x##(h`xs)
|
|
77 |
else h`xs))))"
|
|
78 |
|
|
79 |
rules
|
|
80 |
|
|
81 |
|
|
82 |
(* for test purposes should be deleted FIX !! *)
|
|
83 |
adm_all "adm f"
|
|
84 |
|
|
85 |
|
|
86 |
end |