61 back |
61 back |
62 done |
62 done |
63 |
63 |
64 (*backtracking version*) |
64 (*backtracking version*) |
65 ML {* |
65 ML {* |
66 val prolog_tac = DEPTH_FIRST (has_fewer_prems 1) (resolve_tac (@{thms rules}) 1) |
66 fun prolog_tac ctxt = |
|
67 DEPTH_FIRST (has_fewer_prems 1) (resolve_tac ctxt @{thms rules} 1) |
67 *} |
68 *} |
68 |
69 |
69 schematic_lemma "rev(?x, a:b:c:Nil)" |
70 schematic_lemma "rev(?x, a:b:c:Nil)" |
70 apply (tactic prolog_tac) |
71 apply (tactic \<open>prolog_tac @{context}\<close>) |
71 done |
72 done |
72 |
73 |
73 schematic_lemma "rev(a:?x:c:?y:Nil, d:?z:b:?u)" |
74 schematic_lemma "rev(a:?x:c:?y:Nil, d:?z:b:?u)" |
74 apply (tactic prolog_tac) |
75 apply (tactic \<open>prolog_tac @{context}\<close>) |
75 done |
76 done |
76 |
77 |
77 (*rev([a..p], ?w) requires 153 inferences *) |
78 (*rev([a..p], ?w) requires 153 inferences *) |
78 schematic_lemma "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:o:p:Nil, ?w)" |
79 schematic_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 ([@{thm refl}, @{thm conjI}] @ @{thms rules}) 1) *}) |
80 apply (tactic {* |
|
81 DEPTH_SOLVE (resolve_tac @{context} ([@{thm refl}, @{thm conjI}] @ @{thms rules}) 1) *}) |
80 done |
82 done |
81 |
83 |
82 (*?x has 16, ?y has 32; rev(?y,?w) requires 561 (rather large) inferences |
84 (*?x has 16, ?y has 32; rev(?y,?w) requires 561 (rather large) inferences |
83 total inferences = 2 + 1 + 17 + 561 = 581*) |
85 total inferences = 2 + 1 + 17 + 561 = 581*) |
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)" |
86 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)" |
85 apply (tactic {* DEPTH_SOLVE (resolve_tac ([@{thm refl}, @{thm conjI}] @ @{thms rules}) 1) *}) |
87 apply (tactic {* |
|
88 DEPTH_SOLVE (resolve_tac @{context} ([@{thm refl}, @{thm conjI}] @ @{thms rules}) 1) *}) |
86 done |
89 done |
87 |
90 |
88 end |
91 end |