author | blanchet |
Tue, 20 Mar 2012 13:53:09 +0100 | |
changeset 47048 | 3347c853d8e2 |
parent 46733 | 4a03b30e04cb |
child 48091 | 64025f5405a4 |
permissions | -rw-r--r-- |
43197 | 1 |
(* Title: HOL/Metis_Examples/Type_Encodings.thy |
43162 | 2 |
Author: Jasmin Blanchette, TU Muenchen |
3 |
||
43197 | 4 |
Example that exercises Metis's (and hence Sledgehammer's) type encodings. |
43162 | 5 |
*) |
6 |
||
43197 | 7 |
header {* |
8 |
Example that Exercises Metis's (and Hence Sledgehammer's) Type Encodings |
|
9 |
*} |
|
10 |
||
11 |
theory Type_Encodings |
|
44412
c8b847625584
include all encodings in tests, now that the incompleteness of some encodings has been addressed
blanchet
parents:
44408
diff
changeset
|
12 |
imports Main |
43162 | 13 |
begin |
14 |
||
43197 | 15 |
declare [[metis_new_skolemizer]] |
16 |
||
46733
4a03b30e04cb
use SPASS instead of E for Metis examples -- it's seems faster for these small problems
blanchet
parents:
46436
diff
changeset
|
17 |
sledgehammer_params [prover = spass, blocking, timeout = 30, |
4a03b30e04cb
use SPASS instead of E for Metis examples -- it's seems faster for these small problems
blanchet
parents:
46436
diff
changeset
|
18 |
preplay_timeout = 0, dont_minimize] |
43197 | 19 |
|
43162 | 20 |
text {* Setup for testing Metis exhaustively *} |
21 |
||
22 |
lemma fork: "P \<Longrightarrow> P \<Longrightarrow> P" by assumption |
|
23 |
||
24 |
ML {* |
|
43626
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43212
diff
changeset
|
25 |
val type_encs = |
43208 | 26 |
["erased", |
43989 | 27 |
"poly_guards", |
44768 | 28 |
"poly_guards?", |
29 |
"poly_guards??", |
|
47048
3347c853d8e2
take out experimental polymorphic @ encodings from Metis test -- proof reconstruction is fragile for them
blanchet
parents:
46733
diff
changeset
|
30 |
(* "poly_guards@?", *) |
44768 | 31 |
"poly_guards!", |
32 |
"poly_guards!!", |
|
47048
3347c853d8e2
take out experimental polymorphic @ encodings from Metis test -- proof reconstruction is fragile for them
blanchet
parents:
46733
diff
changeset
|
33 |
(* "poly_guards@!", *) |
43208 | 34 |
"poly_tags", |
44768 | 35 |
"poly_tags?", |
36 |
"poly_tags??", |
|
37 |
"poly_tags!", |
|
38 |
"poly_tags!!", |
|
43208 | 39 |
"poly_args", |
44494
a77901b3774e
rationalized option names -- mono becomes raw_mono and mangled becomes mono
blanchet
parents:
44412
diff
changeset
|
40 |
"raw_mono_guards", |
44768 | 41 |
"raw_mono_guards?", |
42 |
"raw_mono_guards??", |
|
44813 | 43 |
"raw_mono_guards@?", |
44768 | 44 |
"raw_mono_guards!", |
45 |
"raw_mono_guards!!", |
|
44813 | 46 |
"raw_mono_guards@!", |
44494
a77901b3774e
rationalized option names -- mono becomes raw_mono and mangled becomes mono
blanchet
parents:
44412
diff
changeset
|
47 |
"raw_mono_tags", |
44768 | 48 |
"raw_mono_tags?", |
49 |
"raw_mono_tags??", |
|
50 |
"raw_mono_tags!", |
|
51 |
"raw_mono_tags!!", |
|
44494
a77901b3774e
rationalized option names -- mono becomes raw_mono and mangled becomes mono
blanchet
parents:
44412
diff
changeset
|
52 |
"raw_mono_args", |
43989 | 53 |
"mono_guards", |
44768 | 54 |
"mono_guards?", |
55 |
"mono_guards??", |
|
56 |
"mono_guards!", |
|
57 |
"mono_guards!!", |
|
43208 | 58 |
"mono_tags", |
59 |
"mono_tags?", |
|
44768 | 60 |
"mono_tags??", |
43208 | 61 |
"mono_tags!", |
44768 | 62 |
"mono_tags!!", |
63 |
"mono_args"] |
|
43162 | 64 |
|
43212 | 65 |
fun metis_exhaust_tac ctxt ths = |
43162 | 66 |
let |
43172 | 67 |
fun tac [] st = all_tac st |
43626
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43212
diff
changeset
|
68 |
| tac (type_enc :: type_encs) st = |
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43212
diff
changeset
|
69 |
st (* |> tap (fn _ => tracing (PolyML.makestring type_enc)) *) |
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43212
diff
changeset
|
70 |
|> ((if null type_encs then all_tac else rtac @{thm fork} 1) |
46369 | 71 |
THEN Metis_Tactic.metis_tac [type_enc] |
72 |
ATP_Problem_Generate.combsN ctxt ths 1 |
|
43172 | 73 |
THEN COND (has_fewer_prems 2) all_tac no_tac |
43626
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43212
diff
changeset
|
74 |
THEN tac type_encs) |
46436 | 75 |
in tac type_encs end |
43162 | 76 |
*} |
77 |
||
43212 | 78 |
method_setup metis_exhaust = {* |
43162 | 79 |
Attrib.thms >> |
46436 | 80 |
(fn ths => fn ctxt => SIMPLE_METHOD (metis_exhaust_tac ctxt ths)) |
81 |
*} "exhaustively run Metis with all type encodings" |
|
43162 | 82 |
|
43197 | 83 |
text {* Miscellaneous tests *} |
43162 | 84 |
|
85 |
lemma "x = y \<Longrightarrow> y = x" |
|
43212 | 86 |
by metis_exhaust |
43162 | 87 |
|
88 |
lemma "[a] = [1 + 1] \<Longrightarrow> a = 1 + (1::int)" |
|
43212 | 89 |
by (metis_exhaust last.simps) |
43162 | 90 |
|
91 |
lemma "map Suc [0] = [Suc 0]" |
|
43212 | 92 |
by (metis_exhaust map.simps) |
43162 | 93 |
|
94 |
lemma "map Suc [1 + 1] = [Suc 2]" |
|
43212 | 95 |
by (metis_exhaust map.simps nat_1_add_1) |
43162 | 96 |
|
97 |
lemma "map Suc [2] = [Suc (1 + 1)]" |
|
43212 | 98 |
by (metis_exhaust map.simps nat_1_add_1) |
43162 | 99 |
|
100 |
definition "null xs = (xs = [])" |
|
101 |
||
102 |
lemma "P (null xs) \<Longrightarrow> null xs \<Longrightarrow> xs = []" |
|
43212 | 103 |
by (metis_exhaust null_def) |
43162 | 104 |
|
105 |
lemma "(0::nat) + 0 = 0" |
|
45502
6246bef495ff
avoid theorem references like 'semiring_norm(111)'
huffman
parents:
44815
diff
changeset
|
106 |
by (metis_exhaust add_0_left) |
43162 | 107 |
|
108 |
end |