1 (* Title: FOL/ex/prolog.ML |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1992 University of Cambridge |
|
5 |
|
6 For ex/prolog.thy. First-Order Logic: PROLOG examples |
|
7 *) |
|
8 |
|
9 open Prolog; |
|
10 |
|
11 goal Prolog.thy "app(a:b:c:Nil, d:e:Nil, ?x)"; |
|
12 by (resolve_tac [appNil,appCons] 1); |
|
13 by (resolve_tac [appNil,appCons] 1); |
|
14 by (resolve_tac [appNil,appCons] 1); |
|
15 by (resolve_tac [appNil,appCons] 1); |
|
16 prth (result()); |
|
17 |
|
18 goal Prolog.thy "app(?x, c:d:Nil, a:b:c:d:Nil)"; |
|
19 by (REPEAT (resolve_tac [appNil,appCons] 1)); |
|
20 result(); |
|
21 |
|
22 |
|
23 goal Prolog.thy "app(?x, ?y, a:b:c:d:Nil)"; |
|
24 by (REPEAT (resolve_tac [appNil,appCons] 1)); |
|
25 back(); |
|
26 back(); |
|
27 back(); |
|
28 back(); |
|
29 result(); |
|
30 |
|
31 |
|
32 (*app([x1,...,xn], y, ?z) requires (n+1) inferences*) |
|
33 (*rev([x1,...,xn], ?y) requires (n+1)(n+2)/2 inferences*) |
|
34 |
|
35 goal Prolog.thy "rev(a:b:c:d:Nil, ?x)"; |
|
36 val rules = [appNil,appCons,revNil,revCons]; |
|
37 by (REPEAT (resolve_tac rules 1)); |
|
38 result(); |
|
39 |
|
40 goal Prolog.thy "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:Nil, ?w)"; |
|
41 by (REPEAT (resolve_tac rules 1)); |
|
42 result(); |
|
43 |
|
44 goal Prolog.thy "rev(?x, a:b:c:Nil)"; |
|
45 by (REPEAT (resolve_tac rules 1)); (*does not solve it directly!*) |
|
46 back(); |
|
47 back(); |
|
48 |
|
49 (*backtracking version*) |
|
50 val prolog_tac = DEPTH_FIRST (has_fewer_prems 1) (resolve_tac rules 1); |
|
51 |
|
52 choplev 0; |
|
53 by prolog_tac; |
|
54 result(); |
|
55 |
|
56 goal Prolog.thy "rev(a:?x:c:?y:Nil, d:?z:b:?u)"; |
|
57 by prolog_tac; |
|
58 result(); |
|
59 |
|
60 (*rev([a..p], ?w) requires 153 inferences *) |
|
61 goal Prolog.thy "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:o:p:Nil, ?w)"; |
|
62 by (DEPTH_SOLVE (resolve_tac ([refl,conjI]@rules) 1)); |
|
63 (*Poly/ML: 4 secs >> 38 lips*) |
|
64 result(); |
|
65 |
|
66 (*?x has 16, ?y has 32; rev(?y,?w) requires 561 (rather large) inferences; |
|
67 total inferences = 2 + 1 + 17 + 561 = 581*) |
|
68 goal Prolog.thy |
|
69 "a:b:c:d:e:f:g:h:i:j:k:l:m:n:o:p:Nil = ?x & app(?x,?x,?y) & rev(?y,?w)"; |
|
70 by (DEPTH_SOLVE (resolve_tac ([refl,conjI]@rules) 1)); |
|
71 (*Poly/ML: 29 secs >> 20 lips*) |
|
72 result(); |
|
73 |
|
74 writeln"Reached end of file."; |
|