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 {*
|
|
25 |
open ATP_Translate
|
|
26 |
|
|
27 |
val polymorphisms = [Polymorphic, Monomorphic, Mangled_Monomorphic]
|
|
28 |
val levels =
|
|
29 |
[All_Types, Nonmonotonic_Types, Finite_Types, Const_Arg_Types, No_Types]
|
|
30 |
val heaviness = [Heavyweight, Lightweight]
|
|
31 |
val type_syss =
|
|
32 |
(levels |> map Simple_Types) @
|
|
33 |
(map_product pair levels heaviness
|
43196
|
34 |
(* The following two families of type systems are too incomplete for our
|
|
35 |
tests. *)
|
|
36 |
|> remove (op =) (Nonmonotonic_Types, Heavyweight)
|
|
37 |
|> remove (op =) (Finite_Types, Heavyweight)
|
43162
|
38 |
|> map_product pair polymorphisms
|
|
39 |
|> map_product (fn constr => fn (poly, (level, heaviness)) =>
|
|
40 |
constr (poly, level, heaviness))
|
|
41 |
[Preds, Tags])
|
|
42 |
|
43205
|
43 |
fun new_metis_exhaust_tac ctxt ths =
|
43162
|
44 |
let
|
43172
|
45 |
fun tac [] st = all_tac st
|
|
46 |
| tac (type_sys :: type_syss) st =
|
|
47 |
st (* |> tap (fn _ => tracing (PolyML.makestring type_sys)) *)
|
|
48 |
|> ((if null type_syss then all_tac else rtac @{thm fork} 1)
|
43205
|
49 |
THEN Metis_Tactics.new_metis_tac [type_sys] ctxt ths 1
|
43172
|
50 |
THEN COND (has_fewer_prems 2) all_tac no_tac
|
|
51 |
THEN tac type_syss)
|
43162
|
52 |
in tac end
|
|
53 |
*}
|
|
54 |
|
43205
|
55 |
method_setup new_metis_exhaust = {*
|
43162
|
56 |
Attrib.thms >>
|
43205
|
57 |
(fn ths => fn ctxt => SIMPLE_METHOD (new_metis_exhaust_tac ctxt ths type_syss))
|
43162
|
58 |
*} "exhaustively run the new Metis with all type encodings"
|
|
59 |
|
|
60 |
|
43197
|
61 |
text {* Miscellaneous tests *}
|
43162
|
62 |
|
|
63 |
lemma "x = y \<Longrightarrow> y = x"
|
43205
|
64 |
by new_metis_exhaust
|
43162
|
65 |
|
|
66 |
lemma "[a] = [1 + 1] \<Longrightarrow> a = 1 + (1::int)"
|
43205
|
67 |
by (new_metis_exhaust last.simps)
|
43162
|
68 |
|
|
69 |
lemma "map Suc [0] = [Suc 0]"
|
43205
|
70 |
by (new_metis_exhaust map.simps)
|
43162
|
71 |
|
|
72 |
lemma "map Suc [1 + 1] = [Suc 2]"
|
43205
|
73 |
by (new_metis_exhaust map.simps nat_1_add_1)
|
43162
|
74 |
|
|
75 |
lemma "map Suc [2] = [Suc (1 + 1)]"
|
43205
|
76 |
by (new_metis_exhaust map.simps nat_1_add_1)
|
43162
|
77 |
|
|
78 |
definition "null xs = (xs = [])"
|
|
79 |
|
|
80 |
lemma "P (null xs) \<Longrightarrow> null xs \<Longrightarrow> xs = []"
|
43205
|
81 |
by (new_metis_exhaust null_def)
|
43162
|
82 |
|
|
83 |
lemma "(0::nat) + 0 = 0"
|
43205
|
84 |
by (new_metis_exhaust arithmetic_simps(38))
|
43162
|
85 |
|
|
86 |
end
|