author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 47048  3347c853d8e2 
child 48091  64025f5405a4 
permissions  rwrr 
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 