--- a/src/HOL/Sledgehammer.thy Fri Dec 20 16:22:10 2013 +0100
+++ b/src/HOL/Sledgehammer.thy Fri Dec 20 20:36:38 2013 +0100
@@ -11,6 +11,9 @@
keywords "sledgehammer" :: diag and "sledgehammer_params" :: thy_decl
begin
+lemma size_ne_size_imp_ne: "size x \<noteq> size y \<Longrightarrow> x \<noteq> y"
+by (erule contrapos_nn) (rule arg_cong)
+
ML_file "Tools/Sledgehammer/async_manager.ML"
ML_file "Tools/Sledgehammer/sledgehammer_util.ML"
ML_file "Tools/Sledgehammer/sledgehammer_annotate.ML"
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Fri Dec 20 16:22:10 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Fri Dec 20 20:36:38 2013 +0100
@@ -97,6 +97,8 @@
Method.insert_tac facts THEN'
(case meth of
Simp_Method => Simplifier.asm_full_simp_tac ctxt
+ | Simp_Size_Method =>
+ Simplifier.asm_full_simp_tac (Simplifier.add_simp @{thm size_ne_size_imp_ne} ctxt)
| Auto_Method => K (Clasimp.auto_tac ctxt)
| Fastforce_Method => Clasimp.fast_force_tac ctxt
| Force_Method => Clasimp.force_tac ctxt
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML Fri Dec 20 16:22:10 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML Fri Dec 20 20:36:38 2013 +0100
@@ -159,6 +159,7 @@
fun by_method meth = "by " ^
(case meth of
Simp_Method => "simp"
+ | Simp_Size_Method => "(simp add: size_ne_size_imp_ne)"
| Auto_Method => "auto"
| Fastforce_Method => "fastforce"
| Force_Method => "force"
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Fri Dec 20 16:22:10 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Fri Dec 20 20:36:38 2013 +0100
@@ -20,8 +20,8 @@
Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list *
(facts * proof_method list list)
and proof_method =
- Metis_Method | Metis_New_Skolem_Method | Simp_Method | Auto_Method | Fastforce_Method |
- Force_Method | Arith_Method | Blast_Method | Meson_Method
+ Metis_Method | Metis_New_Skolem_Method | Simp_Method | Simp_Size_Method | Auto_Method |
+ Fastforce_Method | Force_Method | Arith_Method | Blast_Method | Meson_Method
val no_label : label
val no_facts : facts
@@ -69,8 +69,8 @@
Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list *
(facts * proof_method list list)
and proof_method =
- Metis_Method | Metis_New_Skolem_Method | Simp_Method | Auto_Method | Fastforce_Method |
- Force_Method | Arith_Method | Blast_Method | Meson_Method
+ Metis_Method | Metis_New_Skolem_Method | Simp_Method | Simp_Size_Method | Auto_Method |
+ Fastforce_Method | Force_Method | Arith_Method | Blast_Method | Meson_Method
val no_label = ("", ~1)
val no_facts = ([],[])
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Fri Dec 20 16:22:10 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Fri Dec 20 20:36:38 2013 +0100
@@ -197,7 +197,7 @@
val arith_methodss =
[[Arith_Method, Simp_Method, Auto_Method, Fastforce_Method, Blast_Method, Force_Method,
Metis_Method], [Meson_Method]]
-val datatype_methodss = [[Auto_Method, Simp_Method, Blast_Method]]
+val datatype_methodss = [[Simp_Size_Method, Simp_Method]]
val metislike_methodss =
[[Metis_Method, Simp_Method, Auto_Method, Arith_Method, Blast_Method, Fastforce_Method,
Force_Method], [Meson_Method]]