# HG changeset patch
# User blanchet
# Date 1387568198 -3600
# Node ID 16511f84913ce3fe3ec3b0a42389dcbd15167632
# Parent  5bc637eb60c071133f0d455aadc62f854cd06a80
reconstruct SPASS-Pirate steps of the form 'x ~= C x' (or more complicated)

diff -r 5bc637eb60c0 -r 16511f84913c src/HOL/Sledgehammer.thy
--- 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"
diff -r 5bc637eb60c0 -r 16511f84913c src/HOL/Tools/Sledgehammer/sledgehammer_preplay.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
diff -r 5bc637eb60c0 -r 16511f84913c src/HOL/Tools/Sledgehammer/sledgehammer_print.ML
--- 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"
diff -r 5bc637eb60c0 -r 16511f84913c src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML
--- 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 = ([],[])
diff -r 5bc637eb60c0 -r 16511f84913c src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- 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]]