author | blanchet |
Fri, 01 Jul 2011 15:53:38 +0200 | |
changeset 43629 | 030610b1e5a8 |
parent 43626 | a867ebb12209 |
child 43989 | eb763b3ff9ed |
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 |
|
43162 | 12 |
imports Main |
13 |
begin |
|
14 |
||
43197 | 15 |
declare [[metis_new_skolemizer]] |
16 |
||
17 |
sledgehammer_params [prover = e, blocking, timeout = 10, preplay_timeout = 0] |
|
18 |
||
19 |
||
43162 | 20 |
text {* Setup for testing Metis exhaustively *} |
21 |
||
22 |
lemma fork: "P \<Longrightarrow> P \<Longrightarrow> P" by assumption |
|
23 |
||
24 |
ML {* |
|
43208 | 25 |
(* The commented-out type systems are too incomplete for our exhaustive |
26 |
tests. *) |
|
43626
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43212
diff
changeset
|
27 |
val type_encs = |
43208 | 28 |
["erased", |
29 |
"poly_preds", |
|
30 |
"poly_preds_heavy", |
|
31 |
"poly_tags", |
|
32 |
"poly_tags_heavy", |
|
33 |
"poly_args", |
|
34 |
"mono_preds", |
|
35 |
"mono_preds_heavy", |
|
36 |
"mono_tags", |
|
37 |
"mono_tags_heavy", |
|
38 |
"mono_args", |
|
39 |
"mangled_preds", |
|
40 |
"mangled_preds_heavy", |
|
41 |
"mangled_tags", |
|
42 |
"mangled_tags_heavy", |
|
43 |
"mangled_args", |
|
44 |
"simple", |
|
45 |
"poly_preds?", |
|
43629 | 46 |
"poly_preds_heavy?", |
47 |
"poly_tags?", |
|
43208 | 48 |
(* "poly_tags_heavy?", *) |
49 |
"mono_preds?", |
|
50 |
"mono_preds_heavy?", |
|
51 |
"mono_tags?", |
|
52 |
"mono_tags_heavy?", |
|
53 |
"mangled_preds?", |
|
54 |
"mangled_preds_heavy?", |
|
55 |
"mangled_tags?", |
|
56 |
"mangled_tags_heavy?", |
|
57 |
"simple?", |
|
58 |
"poly_preds!", |
|
43629 | 59 |
"poly_preds_heavy!", |
43208 | 60 |
(* "poly_tags!", *) |
43629 | 61 |
"poly_tags_heavy!", |
43208 | 62 |
"mono_preds!", |
63 |
"mono_preds_heavy!", |
|
64 |
"mono_tags!", |
|
65 |
"mono_tags_heavy!", |
|
66 |
"mangled_preds!", |
|
67 |
"mangled_preds_heavy!", |
|
68 |
"mangled_tags!", |
|
69 |
"mangled_tags_heavy!", |
|
70 |
"simple!"] |
|
43162 | 71 |
|
43212 | 72 |
fun metis_exhaust_tac ctxt ths = |
43162 | 73 |
let |
43172 | 74 |
fun tac [] st = all_tac st |
43626
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43212
diff
changeset
|
75 |
| tac (type_enc :: type_encs) st = |
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43212
diff
changeset
|
76 |
st (* |> tap (fn _ => tracing (PolyML.makestring type_enc)) *) |
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43212
diff
changeset
|
77 |
|> ((if null type_encs then all_tac else rtac @{thm fork} 1) |
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43212
diff
changeset
|
78 |
THEN Metis_Tactics.metis_tac [type_enc] ctxt ths 1 |
43172 | 79 |
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
|
80 |
THEN tac type_encs) |
43162 | 81 |
in tac end |
82 |
*} |
|
83 |
||
43212 | 84 |
method_setup metis_exhaust = {* |
43162 | 85 |
Attrib.thms >> |
43626
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43212
diff
changeset
|
86 |
(fn ths => fn ctxt => SIMPLE_METHOD (metis_exhaust_tac ctxt ths type_encs)) |
43162 | 87 |
*} "exhaustively run the new Metis with all type encodings" |
88 |
||
89 |
||
43197 | 90 |
text {* Miscellaneous tests *} |
43162 | 91 |
|
92 |
lemma "x = y \<Longrightarrow> y = x" |
|
43212 | 93 |
by metis_exhaust |
43162 | 94 |
|
95 |
lemma "[a] = [1 + 1] \<Longrightarrow> a = 1 + (1::int)" |
|
43212 | 96 |
by (metis_exhaust last.simps) |
43162 | 97 |
|
98 |
lemma "map Suc [0] = [Suc 0]" |
|
43212 | 99 |
by (metis_exhaust map.simps) |
43162 | 100 |
|
101 |
lemma "map Suc [1 + 1] = [Suc 2]" |
|
43212 | 102 |
by (metis_exhaust map.simps nat_1_add_1) |
43162 | 103 |
|
104 |
lemma "map Suc [2] = [Suc (1 + 1)]" |
|
43212 | 105 |
by (metis_exhaust map.simps nat_1_add_1) |
43162 | 106 |
|
107 |
definition "null xs = (xs = [])" |
|
108 |
||
109 |
lemma "P (null xs) \<Longrightarrow> null xs \<Longrightarrow> xs = []" |
|
43212 | 110 |
by (metis_exhaust null_def) |
43162 | 111 |
|
112 |
lemma "(0::nat) + 0 = 0" |
|
43212 | 113 |
by (metis_exhaust arithmetic_simps(38)) |
43162 | 114 |
|
115 |
end |