21 appNil: "app(Nil,ys,ys)" |
21 appNil: "app(Nil,ys,ys)" |
22 appCons: "app(xs,ys,zs) ==> app(x:xs, ys, x:zs)" |
22 appCons: "app(xs,ys,zs) ==> app(x:xs, ys, x:zs)" |
23 revNil: "rev(Nil,Nil)" |
23 revNil: "rev(Nil,Nil)" |
24 revCons: "[| rev(xs,ys); app(ys, x:Nil, zs) |] ==> rev(x:xs, zs)" |
24 revCons: "[| rev(xs,ys); app(ys, x:Nil, zs) |] ==> rev(x:xs, zs)" |
25 |
25 |
26 ML {* use_legacy_bindings (the_context ()) *} |
26 lemma "app(a:b:c:Nil, d:e:Nil, ?x)" |
|
27 apply (rule appNil appCons) |
|
28 apply (rule appNil appCons) |
|
29 apply (rule appNil appCons) |
|
30 apply (rule appNil appCons) |
|
31 done |
|
32 |
|
33 lemma "app(?x, c:d:Nil, a:b:c:d:Nil)" |
|
34 apply (rule appNil appCons)+ |
|
35 done |
|
36 |
|
37 lemma "app(?x, ?y, a:b:c:d:Nil)" |
|
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 |
|
50 lemma "rev(a:b:c:d:Nil, ?x)" |
|
51 apply (rule rules)+ |
|
52 done |
|
53 |
|
54 lemma "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:Nil, ?w)" |
|
55 apply (rule rules)+ |
|
56 done |
|
57 |
|
58 lemma "rev(?x, a:b:c:Nil)" |
|
59 apply (rule rules)+ -- {* does not solve it directly! *} |
|
60 back |
|
61 back |
|
62 done |
|
63 |
|
64 (*backtracking version*) |
|
65 ML {* |
|
66 val prolog_tac = DEPTH_FIRST (has_fewer_prems 1) (resolve_tac (thms "rules") 1) |
|
67 *} |
|
68 |
|
69 lemma "rev(?x, a:b:c:Nil)" |
|
70 apply (tactic prolog_tac) |
|
71 done |
|
72 |
|
73 lemma "rev(a:?x:c:?y:Nil, d:?z:b:?u)" |
|
74 apply (tactic prolog_tac) |
|
75 done |
|
76 |
|
77 (*rev([a..p], ?w) requires 153 inferences *) |
|
78 lemma "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:o:p:Nil, ?w)" |
|
79 apply (tactic {* DEPTH_SOLVE (resolve_tac ([refl, conjI] @ thms "rules") 1) *}) |
|
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*) |
|
84 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)" |
|
85 apply (tactic {* DEPTH_SOLVE (resolve_tac ([refl, conjI] @ thms "rules") 1) *}) |
|
86 done |
27 |
87 |
28 end |
88 end |