24 "[x, xs]" == "x#[xs]" |
24 "[x, xs]" == "x#[xs]" |
25 "[x]" == "x#[]" |
25 "[x]" == "x#[]" |
26 |
26 |
27 typedecl person |
27 typedecl person |
28 |
28 |
29 consts |
29 axiomatization |
30 append :: "['a list, 'a list, 'a list] => bool" |
30 append :: "['a list, 'a list, 'a list] => bool" and |
31 reverse :: "['a list, 'a list] => bool" |
31 reverse :: "['a list, 'a list] => bool" and |
32 |
32 |
33 mappred :: "[('a => 'b => bool), 'a list, 'b list] => bool" |
33 mappred :: "[('a => 'b => bool), 'a list, 'b list] => bool" and |
34 mapfun :: "[('a => 'b), 'a list, 'b list] => bool" |
34 mapfun :: "[('a => 'b), 'a list, 'b list] => bool" and |
35 |
35 |
36 bob :: person |
36 bob :: person and |
37 sue :: person |
37 sue :: person and |
38 ned :: person |
38 ned :: person and |
39 |
39 |
40 nat23 :: nat ("23") |
40 nat23 :: nat ("23") and |
41 nat24 :: nat ("24") |
41 nat24 :: nat ("24") and |
42 nat25 :: nat ("25") |
42 nat25 :: nat ("25") and |
43 |
43 |
44 age :: "[person, nat] => bool" |
44 age :: "[person, nat] => bool" and |
45 |
45 |
46 eq :: "['a, 'a] => bool" |
46 eq :: "['a, 'a] => bool" and |
47 |
47 |
48 empty :: "['b] => bool" |
48 empty :: "['b] => bool" and |
49 add :: "['a, 'b, 'b] => bool" |
49 add :: "['a, 'b, 'b] => bool" and |
50 remove :: "['a, 'b, 'b] => bool" |
50 remove :: "['a, 'b, 'b] => bool" and |
51 bag_appl:: "['a, 'a, 'a, 'a] => bool" |
51 bag_appl:: "['a, 'a, 'a, 'a] => bool" |
52 |
52 where |
53 axioms |
53 append: "\<And>x xs ys zs. append [] xs xs .. |
54 append: "append [] xs xs .. |
54 append (x#xs) ys (x#zs) :- append xs ys zs" and |
55 append (x#xs) ys (x#zs) :- append xs ys zs" |
55 reverse: "\<And>L1 L2. reverse L1 L2 :- (!rev_aux. |
56 reverse: "reverse L1 L2 :- (!rev_aux. |
|
57 (!L. rev_aux [] L L ).. |
56 (!L. rev_aux [] L L ).. |
58 (!X L1 L2 L3. rev_aux (X#L1) L2 L3 :- rev_aux L1 L2 (X#L3)) |
57 (!X L1 L2 L3. rev_aux (X#L1) L2 L3 :- rev_aux L1 L2 (X#L3)) |
59 => rev_aux L1 L2 [])" |
58 => rev_aux L1 L2 [])" and |
60 |
59 |
61 mappred: "mappred P [] [] .. |
60 mappred: "\<And>x xs y ys P. mappred P [] [] .. |
62 mappred P (x#xs) (y#ys) :- P x y & mappred P xs ys" |
61 mappred P (x#xs) (y#ys) :- P x y & mappred P xs ys" and |
63 mapfun: "mapfun f [] [] .. |
62 mapfun: "\<And>x xs ys f. mapfun f [] [] .. |
64 mapfun f (x#xs) (f x#ys) :- mapfun f xs ys" |
63 mapfun f (x#xs) (f x#ys) :- mapfun f xs ys" and |
65 |
64 |
66 age: "age bob 24 .. |
65 age: "age bob 24 .. |
67 age sue 23 .. |
66 age sue 23 .. |
68 age ned 23" |
67 age ned 23" and |
69 |
68 |
70 eq: "eq x x" |
69 eq: "\<And>x. eq x x" and |
71 |
70 |
72 (* actual definitions of empty and add is hidden -> yields abstract data type *) |
71 (* actual definitions of empty and add is hidden -> yields abstract data type *) |
73 |
72 |
74 bag_appl: "bag_appl A B X Y:- (? S1 S2 S3 S4 S5. |
73 bag_appl: "\<And>A B X Y. bag_appl A B X Y:- (? S1 S2 S3 S4 S5. |
75 empty S1 & |
74 empty S1 & |
76 add A S1 S2 & |
75 add A S1 S2 & |
77 add B S2 S3 & |
76 add B S2 S3 & |
78 remove X S3 S4 & |
77 remove X S3 S4 & |
79 remove Y S4 S5 & |
78 remove Y S4 S5 & |