author | wenzelm |
Sat, 01 Dec 2001 18:52:32 +0100 | |
changeset 12338 | de0f4a63baa5 |
parent 9015 | 8006e9009621 |
child 13208 | 965f95a3abd9 |
permissions | -rw-r--r-- |
9015 | 1 |
(* basic examples *) |
2 |
||
3 |
Test = HOHH + |
|
4 |
||
5 |
types nat |
|
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
9015
diff
changeset
|
6 |
arities nat :: type |
9015 | 7 |
|
8 |
types 'a list |
|
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
9015
diff
changeset
|
9 |
arities list :: (type) type |
9015 | 10 |
|
11 |
consts Nil :: 'a list ("[]") |
|
12 |
Cons :: 'a => 'a list => 'a list (infixr "#" 65) |
|
13 |
||
14 |
syntax |
|
15 |
(* list Enumeration *) |
|
16 |
"@list" :: args => 'a list ("[(_)]") |
|
17 |
||
18 |
translations |
|
19 |
"[x, xs]" == "x#[xs]" |
|
20 |
"[x]" == "x#[]" |
|
21 |
||
22 |
types person |
|
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
9015
diff
changeset
|
23 |
arities person :: type |
9015 | 24 |
|
25 |
consts |
|
26 |
append :: ['a list, 'a list, 'a list] => bool |
|
27 |
reverse :: ['a list, 'a list] => bool |
|
28 |
||
29 |
mappred :: [('a => 'b => bool), 'a list, 'b list] => bool |
|
30 |
mapfun :: [('a => 'b), 'a list, 'b list] => bool |
|
31 |
||
32 |
bob :: person |
|
33 |
sue :: person |
|
34 |
ned :: person |
|
35 |
||
36 |
"23" :: nat ("23") |
|
37 |
"24" :: nat ("24") |
|
38 |
"25" :: nat ("25") |
|
39 |
||
40 |
age :: [person, nat] => bool |
|
41 |
||
42 |
eq :: ['a, 'a] => bool |
|
43 |
||
44 |
empty :: ['b] => bool |
|
45 |
add :: ['a, 'b, 'b] => bool |
|
46 |
remove :: ['a, 'b, 'b] => bool |
|
47 |
bag_appl:: ['a, 'a, 'a, 'a] => bool |
|
48 |
||
49 |
rules append "append [] xs xs .. |
|
50 |
append (x#xs) ys (x#zs) :- append xs ys zs" |
|
51 |
reverse "reverse L1 L2 :- (!rev_aux. |
|
52 |
(!L. rev_aux [] L L ).. |
|
53 |
(!X L1 L2 L3. rev_aux (X#L1) L2 L3 :- rev_aux L1 L2 (X#L3)) |
|
54 |
=> rev_aux L1 L2 [])" |
|
55 |
||
56 |
mappred "mappred P [] [] .. |
|
57 |
mappred P (x#xs) (y#ys) :- P x y & mappred P xs ys" |
|
58 |
mapfun "mapfun f [] [] .. |
|
59 |
mapfun f (x#xs) (f x#ys) :- mapfun f xs ys" |
|
60 |
||
61 |
age "age bob 24 .. |
|
62 |
age sue 23 .. |
|
63 |
age ned 23" |
|
64 |
||
65 |
eq "eq x x" |
|
66 |
||
67 |
(* actual definitions of empty and add is hidden -> yields abstract data type *) |
|
68 |
||
69 |
bag_appl"bag_appl A B X Y:- (? S1 S2 S3 S4 S5. |
|
70 |
empty S1 & |
|
71 |
add A S1 S2 & |
|
72 |
add B S2 S3 & |
|
73 |
remove X S3 S4 & |
|
74 |
remove Y S4 S5 & |
|
75 |
empty S5)" |
|
76 |
end |