author | haftmann |
Mon, 05 Jul 2010 15:12:20 +0200 | |
changeset 37715 | 44b27ea94a16 |
parent 35762 | af3ff2ba4c54 |
permissions | -rw-r--r-- |
24584 | 1 |
(* Title: FOLP/ex/Prolog.ML |
1459 | 2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
0 | 3 |
Copyright 1992 University of Cambridge |
4 |
||
5 |
For ex/prolog.thy. First-Order Logic: PROLOG examples |
|
6 |
*) |
|
7 |
||
8 |
open Prolog; |
|
9 |
||
5061 | 10 |
Goal "app(a:b:c:Nil, d:e:Nil, ?x)"; |
0 | 11 |
by (resolve_tac [appNil,appCons] 1); |
12 |
by (resolve_tac [appNil,appCons] 1); |
|
13 |
by (resolve_tac [appNil,appCons] 1); |
|
14 |
by (resolve_tac [appNil,appCons] 1); |
|
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
24584
diff
changeset
|
15 |
result(); |
0 | 16 |
|
5061 | 17 |
Goal "app(?x, c:d:Nil, a:b:c:d:Nil)"; |
0 | 18 |
by (REPEAT (resolve_tac [appNil,appCons] 1)); |
19 |
result(); |
|
20 |
||
21 |
||
5061 | 22 |
Goal "app(?x, ?y, a:b:c:d:Nil)"; |
0 | 23 |
by (REPEAT (resolve_tac [appNil,appCons] 1)); |
24 |
back(); |
|
25 |
back(); |
|
26 |
back(); |
|
27 |
back(); |
|
28 |
result(); |
|
29 |
||
30 |
||
31 |
(*app([x1,...,xn], y, ?z) requires (n+1) inferences*) |
|
32 |
(*rev([x1,...,xn], ?y) requires (n+1)(n+2)/2 inferences*) |
|
33 |
||
5061 | 34 |
Goal "rev(a:b:c:d:Nil, ?x)"; |
0 | 35 |
val rules = [appNil,appCons,revNil,revCons]; |
36 |
by (REPEAT (resolve_tac rules 1)); |
|
37 |
result(); |
|
38 |
||
5061 | 39 |
Goal "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:Nil, ?w)"; |
0 | 40 |
by (REPEAT (resolve_tac rules 1)); |
41 |
result(); |
|
42 |
||
5061 | 43 |
Goal "rev(?x, a:b:c:Nil)"; |
0 | 44 |
by (REPEAT (resolve_tac rules 1)); (*does not solve it directly!*) |
45 |
back(); |
|
46 |
back(); |
|
47 |
||
48 |
(*backtracking version*) |
|
49 |
val prolog_tac = DEPTH_FIRST (has_fewer_prems 1) (resolve_tac rules 1); |
|
50 |
||
51 |
choplev 0; |
|
52 |
by prolog_tac; |
|
53 |
result(); |
|
54 |
||
5061 | 55 |
Goal "rev(a:?x:c:?y:Nil, d:?z:b:?u)"; |
0 | 56 |
by prolog_tac; |
57 |
result(); |
|
58 |
||
59 |
(*rev([a..p], ?w) requires 153 inferences *) |
|
5061 | 60 |
Goal "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:o:p:Nil, ?w)"; |
0 | 61 |
by (DEPTH_SOLVE (resolve_tac ([refl,conjI]@rules) 1)); |
62 |
(*Poly/ML: 4 secs >> 38 lips*) |
|
63 |
result(); |
|
64 |
||
65 |
(*?x has 16, ?y has 32; rev(?y,?w) requires 561 (rather large) inferences; |
|
66 |
total inferences = 2 + 1 + 17 + 561 = 581*) |
|
5061 | 67 |
Goal |
0 | 68 |
"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)"; |
69 |
by (DEPTH_SOLVE (resolve_tac ([refl,conjI]@rules) 1)); |
|
70 |
(*Poly/ML: 29 secs >> 20 lips*) |
|
71 |
result(); |
|
72 |
||
73 |
writeln"Reached end of file."; |