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