1 (* Title: HOL/Prolog/Test.ML |
|
2 ID: $Id$ |
|
3 Author: David von Oheimb (based on a lecture on Lambda Prolog by Nadathur) |
|
4 *) |
|
5 |
|
6 val prog_Test = prog_HOHH@[append, reverse, mappred, mapfun, age, eq, bag_appl]; |
|
7 fun pgoal s = (case Goal s of _ => by (prolog_tac prog_Test)); |
|
8 val p = ptac prog_Test 1; |
|
9 |
|
10 pgoal "append ?x ?y [a,b,c,d]"; |
|
11 back(); |
|
12 back(); |
|
13 back(); |
|
14 back(); |
|
15 |
|
16 pgoal "append [a,b] y ?L"; |
|
17 pgoal "!y. append [a,b] y (?L y)"; |
|
18 |
|
19 pgoal "reverse [] ?L"; |
|
20 |
|
21 pgoal "reverse [23] ?L"; |
|
22 pgoal "reverse [23,24,?x] ?L"; |
|
23 pgoal "reverse ?L [23,24,?x]"; |
|
24 |
|
25 pgoal "mappred age ?x [23,24]"; |
|
26 back(); |
|
27 |
|
28 pgoal "mappred (%x y. ? z. age z y) ?x [23,24]"; |
|
29 |
|
30 pgoal "mappred ?P [bob,sue] [24,23]"; |
|
31 |
|
32 pgoal "mapfun f [bob,bob,sue] [?x,?y,?z]"; |
|
33 |
|
34 pgoal "mapfun (%x. h x 25) [bob,sue] ?L"; |
|
35 |
|
36 pgoal "mapfun ?F [24,25] [h bob 24,h bob 25]"; |
|
37 |
|
38 pgoal "mapfun ?F [24] [h 24 24]"; |
|
39 back(); |
|
40 back(); |
|
41 back(); |
|
42 |
|
43 |
|
44 (* |
|
45 goal (the_context ()) "f a = ?g a a & ?g = x"; |
|
46 by (rtac conjI 1); |
|
47 by (rtac refl 1); |
|
48 back(); |
|
49 back(); |
|
50 *) |
|
51 |
|
52 pgoal "True"; |
|
53 |
|
54 pgoal "age ?x 24 & age ?y 23"; |
|
55 back(); |
|
56 |
|
57 pgoal "age ?x 24 | age ?x 23"; |
|
58 back(); |
|
59 back(); |
|
60 |
|
61 pgoal "? x y. age x y"; |
|
62 |
|
63 pgoal "!x y. append [] x x"; |
|
64 |
|
65 pgoal "age sue 24 .. age bob 23 => age ?x ?y"; |
|
66 back(); |
|
67 back(); |
|
68 back(); |
|
69 back(); |
|
70 |
|
71 (*set trace_DEPTH_FIRST;*) |
|
72 pgoal "age bob 25 :- age bob 24 => age bob 25"; |
|
73 (*reset trace_DEPTH_FIRST;*) |
|
74 |
|
75 pgoal "(!x. age x 25 :- age x 23) => age ?x 25 & age ?y 25"; |
|
76 back(); |
|
77 back(); |
|
78 back(); |
|
79 |
|
80 pgoal "!x. ? y. eq x y"; |
|
81 |
|
82 pgoal "? P. P & eq P ?x"; |
|
83 (* |
|
84 back(); |
|
85 back(); |
|
86 back(); |
|
87 back(); |
|
88 back(); |
|
89 back(); |
|
90 back(); |
|
91 back(); |
|
92 *) |
|
93 |
|
94 pgoal "? P. eq P (True & True) & P"; |
|
95 |
|
96 pgoal "? P. eq P op | & P k True"; |
|
97 |
|
98 pgoal "? P. eq P (Q => True) & P"; |
|
99 |
|
100 (* P flexible: *) |
|
101 pgoal "(!P k l. P k l :- eq P Q) => Q a b"; |
|
102 (* |
|
103 loops: |
|
104 pgoal "(!P k l. P k l :- eq P (%x y. x | y)) => a | b"; |
|
105 *) |
|
106 |
|
107 (* implication and disjunction in atom: *) |
|
108 goal (the_context ()) "? Q. (!p q. R(q :- p) => R(Q p q)) & Q (t | s) (s | t)"; |
|
109 by (fast_tac HOL_cs 1); |
|
110 |
|
111 (* disjunction in atom: *) |
|
112 goal (the_context ()) "(!P. g P :- (P => b | a)) => g(a | b)"; |
|
113 by (step_tac HOL_cs 1); |
|
114 by (step_tac HOL_cs 1); |
|
115 by (step_tac HOL_cs 1); |
|
116 by (fast_tac HOL_cs 2); |
|
117 by (fast_tac HOL_cs 1); |
|
118 (* |
|
119 hangs: |
|
120 goal (the_context ()) "(!P. g P :- (P => b | a)) => g(a | b)"; |
|
121 by (fast_tac HOL_cs 1); |
|
122 *) |
|
123 |
|
124 pgoal "!Emp Stk.(\ |
|
125 \ empty (Emp::'b) .. \ |
|
126 \ (!(X::nat) S. add X (S::'b) (Stk X S)) .. \ |
|
127 \ (!(X::nat) S. remove X ((Stk X S)::'b) S))\ |
|
128 \ => bag_appl 23 24 ?X ?Y"; |
|
129 |
|
130 pgoal "!Qu. ( \ |
|
131 \ (!L. empty (Qu L L)) .. \ |
|
132 \ (!(X::nat) L K. add X (Qu L (X#K)) (Qu L K)) ..\ |
|
133 \ (!(X::nat) L K. remove X (Qu (X#L) K) (Qu L K)))\ |
|
134 \ => bag_appl 23 24 ?X ?Y"; |
|
135 |
|
136 pgoal "D & (!y. E) :- (!x. True & True) :- True => D"; |
|
137 |
|
138 pgoal "P x .. P y => P ?X"; |
|
139 back(); |
|
140 (* |
|
141 back(); |
|
142 -> problem with DEPTH_SOLVE: |
|
143 Exception- THM ("dest_state", 1, ["P x & P y --> P y"]) raised |
|
144 Exception raised at run-time |
|
145 *) |
|