author | wenzelm |
Tue, 09 Dec 2014 19:39:40 +0100 | |
changeset 59119 | c90c02940964 |
parent 58889 | 5b7a9633cfa8 |
child 59498 | 50b60f501b05 |
permissions | -rw-r--r-- |
31974 | 1 |
(* Title: FOL/ex/Prolog.thy |
1473 | 2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
0 | 3 |
Copyright 1992 University of Cambridge |
4 |
*) |
|
5 |
||
58889 | 6 |
section {* First-Order Logic: PROLOG examples *} |
17245 | 7 |
|
8 |
theory Prolog |
|
9 |
imports FOL |
|
10 |
begin |
|
11 |
||
12 |
typedecl 'a list |
|
55380
4de48353034e
prefer vacuous definitional type classes over axiomatic ones;
wenzelm
parents:
41779
diff
changeset
|
13 |
instance list :: ("term") "term" .. |
41779 | 14 |
|
15 |
axiomatization |
|
16 |
Nil :: "'a list" and |
|
17 |
Cons :: "['a, 'a list]=> 'a list" (infixr ":" 60) and |
|
18 |
app :: "['a list, 'a list, 'a list] => o" and |
|
17245 | 19 |
rev :: "['a list, 'a list] => o" |
41779 | 20 |
where |
21 |
appNil: "app(Nil,ys,ys)" and |
|
22 |
appCons: "app(xs,ys,zs) ==> app(x:xs, ys, x:zs)" and |
|
23 |
revNil: "rev(Nil,Nil)" and |
|
17245 | 24 |
revCons: "[| rev(xs,ys); app(ys, x:Nil, zs) |] ==> rev(x:xs, zs)" |
25 |
||
36319 | 26 |
schematic_lemma "app(a:b:c:Nil, d:e:Nil, ?x)" |
19819 | 27 |
apply (rule appNil appCons) |
28 |
apply (rule appNil appCons) |
|
29 |
apply (rule appNil appCons) |
|
30 |
apply (rule appNil appCons) |
|
31 |
done |
|
32 |
||
36319 | 33 |
schematic_lemma "app(?x, c:d:Nil, a:b:c:d:Nil)" |
19819 | 34 |
apply (rule appNil appCons)+ |
35 |
done |
|
36 |
||
36319 | 37 |
schematic_lemma "app(?x, ?y, a:b:c:d:Nil)" |
19819 | 38 |
apply (rule appNil appCons)+ |
39 |
back |
|
40 |
back |
|
41 |
back |
|
42 |
back |
|
43 |
done |
|
44 |
||
45 |
(*app([x1,...,xn], y, ?z) requires (n+1) inferences*) |
|
46 |
(*rev([x1,...,xn], ?y) requires (n+1)(n+2)/2 inferences*) |
|
47 |
||
48 |
lemmas rules = appNil appCons revNil revCons |
|
49 |
||
36319 | 50 |
schematic_lemma "rev(a:b:c:d:Nil, ?x)" |
19819 | 51 |
apply (rule rules)+ |
52 |
done |
|
53 |
||
36319 | 54 |
schematic_lemma "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:Nil, ?w)" |
19819 | 55 |
apply (rule rules)+ |
56 |
done |
|
57 |
||
36319 | 58 |
schematic_lemma "rev(?x, a:b:c:Nil)" |
19819 | 59 |
apply (rule rules)+ -- {* does not solve it directly! *} |
60 |
back |
|
61 |
back |
|
62 |
done |
|
63 |
||
64 |
(*backtracking version*) |
|
65 |
ML {* |
|
26287 | 66 |
val prolog_tac = DEPTH_FIRST (has_fewer_prems 1) (resolve_tac (@{thms rules}) 1) |
19819 | 67 |
*} |
68 |
||
36319 | 69 |
schematic_lemma "rev(?x, a:b:c:Nil)" |
19819 | 70 |
apply (tactic prolog_tac) |
71 |
done |
|
72 |
||
36319 | 73 |
schematic_lemma "rev(a:?x:c:?y:Nil, d:?z:b:?u)" |
19819 | 74 |
apply (tactic prolog_tac) |
75 |
done |
|
76 |
||
77 |
(*rev([a..p], ?w) requires 153 inferences *) |
|
36319 | 78 |
schematic_lemma "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:o:p:Nil, ?w)" |
26287 | 79 |
apply (tactic {* DEPTH_SOLVE (resolve_tac ([@{thm refl}, @{thm conjI}] @ @{thms rules}) 1) *}) |
19819 | 80 |
done |
81 |
||
82 |
(*?x has 16, ?y has 32; rev(?y,?w) requires 561 (rather large) inferences |
|
83 |
total inferences = 2 + 1 + 17 + 561 = 581*) |
|
36319 | 84 |
schematic_lemma "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)" |
26287 | 85 |
apply (tactic {* DEPTH_SOLVE (resolve_tac ([@{thm refl}, @{thm conjI}] @ @{thms rules}) 1) *}) |
19819 | 86 |
done |
17245 | 87 |
|
0 | 88 |
end |