author | wenzelm |
Mon, 28 Sep 2020 22:22:56 +0200 | |
changeset 72323 | e36f94e2eb6b |
parent 69989 | bcba61d92558 |
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 |
||
63167 | 7 |
section \<open> |
43197 | 8 |
Example that Exercises Metis's (and Hence Sledgehammer's) Type Encodings |
63167 | 9 |
\<close> |
43197 | 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 |
||
50705
0e943b33d907
use new skolemizer for reconstructing skolemization steps in Isar proofs (because the old skolemizer messes up the order of the Skolem arguments)
blanchet
parents:
48664
diff
changeset
|
15 |
declare [[metis_new_skolem]] |
43197 | 16 |
|
63167 | 17 |
text \<open>Setup for testing Metis exhaustively\<close> |
43162 | 18 |
|
19 |
lemma fork: "P \<Longrightarrow> P \<Longrightarrow> P" by assumption |
|
20 |
||
63167 | 21 |
ML \<open> |
43626
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43212
diff
changeset
|
22 |
val type_encs = |
43208 | 23 |
["erased", |
43989 | 24 |
"poly_guards", |
44768 | 25 |
"poly_guards?", |
26 |
"poly_guards??", |
|
48146 | 27 |
"poly_guards@", |
43208 | 28 |
"poly_tags", |
44768 | 29 |
"poly_tags?", |
30 |
"poly_tags??", |
|
48146 | 31 |
"poly_tags@", |
43208 | 32 |
"poly_args", |
48092 | 33 |
"poly_args?", |
44494
a77901b3774e
rationalized option names -- mono becomes raw_mono and mangled becomes mono
blanchet
parents:
44412
diff
changeset
|
34 |
"raw_mono_guards", |
44768 | 35 |
"raw_mono_guards?", |
36 |
"raw_mono_guards??", |
|
48146 | 37 |
"raw_mono_guards@", |
44494
a77901b3774e
rationalized option names -- mono becomes raw_mono and mangled becomes mono
blanchet
parents:
44412
diff
changeset
|
38 |
"raw_mono_tags", |
44768 | 39 |
"raw_mono_tags?", |
40 |
"raw_mono_tags??", |
|
48146 | 41 |
"raw_mono_tags@", |
44494
a77901b3774e
rationalized option names -- mono becomes raw_mono and mangled becomes mono
blanchet
parents:
44412
diff
changeset
|
42 |
"raw_mono_args", |
48092 | 43 |
"raw_mono_args?", |
43989 | 44 |
"mono_guards", |
44768 | 45 |
"mono_guards?", |
46 |
"mono_guards??", |
|
43208 | 47 |
"mono_tags", |
48 |
"mono_tags?", |
|
44768 | 49 |
"mono_tags??", |
50 |
"mono_args"] |
|
43162 | 51 |
|
43212 | 52 |
fun metis_exhaust_tac ctxt ths = |
43162 | 53 |
let |
43172 | 54 |
fun tac [] st = all_tac st |
43626
a867ebb12209
renamed "type_sys" to "type_enc", which is more accurate
blanchet
parents:
43212
diff
changeset
|
55 |
| tac (type_enc :: type_encs) st = |
69989 | 56 |
st |> ((if null type_encs then all_tac else resolve_tac ctxt @{thms fork} 1) |
46369 | 57 |
THEN Metis_Tactic.metis_tac [type_enc] |
58 |
ATP_Problem_Generate.combsN ctxt ths 1 |
|
43172 | 59 |
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
|
60 |
THEN tac type_encs) |
46436 | 61 |
in tac type_encs end |
63167 | 62 |
\<close> |
43162 | 63 |
|
63167 | 64 |
method_setup metis_exhaust = \<open> |
43162 | 65 |
Attrib.thms >> |
46436 | 66 |
(fn ths => fn ctxt => SIMPLE_METHOD (metis_exhaust_tac ctxt ths)) |
63167 | 67 |
\<close> "exhaustively run Metis with all type encodings" |
43162 | 68 |
|
63167 | 69 |
text \<open>Miscellaneous tests\<close> |
43162 | 70 |
|
71 |
lemma "x = y \<Longrightarrow> y = x" |
|
43212 | 72 |
by metis_exhaust |
43162 | 73 |
|
48098
dd611ab202a8
tweak Metis example to avoid glitch in proof reconstruction with a few guard-based, type-argument-less encodings
blanchet
parents:
48092
diff
changeset
|
74 |
lemma "[a] = [Suc 0] \<Longrightarrow> a = 1" |
dd611ab202a8
tweak Metis example to avoid glitch in proof reconstruction with a few guard-based, type-argument-less encodings
blanchet
parents:
48092
diff
changeset
|
75 |
by (metis_exhaust last.simps One_nat_def) |
43162 | 76 |
|
77 |
lemma "map Suc [0] = [Suc 0]" |
|
55465 | 78 |
by (metis_exhaust list.map) |
43162 | 79 |
|
80 |
lemma "map Suc [1 + 1] = [Suc 2]" |
|
55465 | 81 |
by (metis_exhaust list.map nat_1_add_1) |
43162 | 82 |
|
83 |
lemma "map Suc [2] = [Suc (1 + 1)]" |
|
55465 | 84 |
by (metis_exhaust list.map nat_1_add_1) |
43162 | 85 |
|
86 |
definition "null xs = (xs = [])" |
|
87 |
||
88 |
lemma "P (null xs) \<Longrightarrow> null xs \<Longrightarrow> xs = []" |
|
43212 | 89 |
by (metis_exhaust null_def) |
43162 | 90 |
|
61076 | 91 |
lemma "(0::nat) + 0 = 0" |
45502
6246bef495ff
avoid theorem references like 'semiring_norm(111)'
huffman
parents:
44815
diff
changeset
|
92 |
by (metis_exhaust add_0_left) |
43162 | 93 |
|
94 |
end |