# HG changeset patch
# User blanchet
# Date 1406897037 -7200
# Node ID a68b8db8691d005b753f1f6e0cf6b5a78421df68
# Parent  0af2d5dfb0ace63b6c8f448cd321810093244b73
added appropriate method for skolemization of Z3 steps to the mix

diff -r 0af2d5dfb0ac -r a68b8db8691d src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Aug 01 14:43:57 2014 +0200
@@ -116,15 +116,16 @@
   * (term, string) atp_step list * thm
 
 val basic_systematic_methods = [Metis_Method (NONE, NONE), Meson_Method, Blast_Method, SATx_Method]
-val simp_based_methods = [Auto_Method, Simp_Method, Force_Method]
+val basic_simp_based_methods = [Auto_Method, Simp_Method, Force_Method]
 val basic_arith_methods = [Linarith_Method, Presburger_Method, Algebra_Method]
 
-val arith_methods = basic_arith_methods @ simp_based_methods @ basic_systematic_methods
+val arith_methods = basic_arith_methods @ basic_simp_based_methods @ basic_systematic_methods
 val datatype_methods = [Simp_Method, Simp_Size_Method]
-val systematic_methods0 = basic_systematic_methods @ basic_arith_methods @ simp_based_methods @
+val systematic_methods =
+  basic_systematic_methods @ basic_arith_methods @ basic_simp_based_methods @
   [Metis_Method (SOME full_typesN, NONE), Metis_Method (SOME no_typesN, NONE)]
-val rewrite_methods = simp_based_methods @ basic_systematic_methods @ basic_arith_methods
-val skolem_methods = basic_systematic_methods
+val rewrite_methods = basic_simp_based_methods @ basic_systematic_methods @ basic_arith_methods
+val skolem_methods = Auto_Choice_Method :: basic_systematic_methods
 
 fun isar_proof_text ctxt debug isar_proofs smt_proofs isar_params
     (one_line_params as ((used_facts, (_, one_line_play)), banner, subgoal, subgoal_count)) =
@@ -136,7 +137,7 @@
         val (verbose, alt_metis_args, preplay_timeout, compress, try0, minimize, atp_proof, goal) =
           isar_params ()
 
-        val systematic_methods = insert (op =) (Metis_Method alt_metis_args) systematic_methods0
+        val systematic_methods' = insert (op =) (Metis_Method alt_metis_args) systematic_methods
 
         fun massage_methods (meths as meth :: _) =
           if not try0 then [meth]
@@ -228,7 +229,7 @@
             accum
             |> (if tainted = [] then
                   cons (Prove (if outer then [Show] else [], [], no_label, concl_t, [],
-                    (the_list predecessor, []), massage_methods systematic_methods, ""))
+                    (the_list predecessor, []), massage_methods systematic_methods', ""))
                 else
                   I)
             |> rev
@@ -244,7 +245,7 @@
                 (if skolem then skolem_methods
                  else if is_arith_rule rule then arith_methods
                  else if is_datatype_rule rule then datatype_methods
-                 else systematic_methods)
+                 else systematic_methods')
                 |> massage_methods
 
               fun prove sub facts = Prove (maybe_show outer c [], [], l, t, sub, facts, meths, "")
@@ -275,7 +276,7 @@
               val step =
                 Prove (maybe_show outer c [], [], l, t,
                   map isar_case (filter_out (null o snd) cases),
-                  (the_list predecessor, []), massage_methods systematic_methods, "")
+                  (the_list predecessor, []), massage_methods systematic_methods', "")
             in
               isar_steps outer (SOME l) (step :: accum) infs
             end
diff -r 0af2d5dfb0ac -r a68b8db8691d src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Fri Aug 01 14:43:57 2014 +0200
@@ -18,6 +18,7 @@
     Simp_Method |
     Simp_Size_Method |
     Auto_Method |
+    Auto_Choice_Method |
     Force_Method |
     Linarith_Method |
     Presburger_Method |
@@ -56,6 +57,7 @@
   Simp_Method |
   Simp_Size_Method |
   Auto_Method |
+  Auto_Choice_Method |
   Force_Method |
   Linarith_Method |
   Presburger_Method |
@@ -92,6 +94,7 @@
       | Simp_Method => if null ss then "simp" else "simp add:"
       | Simp_Size_Method => "simp add: " ^ short_thm_name ctxt @{thm size_ne_size_imp_ne}
       | Auto_Method => "auto"
+      | Auto_Choice_Method => "atomize_elim, auto intro!: " ^ short_thm_name ctxt @{thm choice}
       | Force_Method => "force"
       | Linarith_Method => "linarith"
       | Presburger_Method => "presburger"
@@ -124,14 +127,18 @@
     (case meth of
       SATx_Method => SAT.satx_tac ctxt
     | Blast_Method => blast_tac ctxt
-    | Auto_Method => K (Clasimp.auto_tac (silence_methods ctxt))
-    | Force_Method => Clasimp.force_tac (silence_methods ctxt)
+    | Auto_Method => SELECT_GOAL (Clasimp.auto_tac (silence_methods ctxt))
+    | Auto_Choice_Method =>
+      AtomizeElim.atomize_elim_tac ctxt THEN'
+      SELECT_GOAL (Clasimp.auto_tac (silence_methods ctxt addSIs @{thms choice}))
+    | Force_Method => SELECT_GOAL (Clasimp.auto_tac (silence_methods ctxt))
     | Linarith_Method =>
       let val ctxt = Config.put Lin_Arith.verbose false ctxt in Lin_Arith.tac ctxt end
     | Presburger_Method => Cooper.tac true [] [] ctxt
     | Algebra_Method => Groebner.algebra_tac [] [] ctxt))
 
-val simp_based_methods = [Simp_Method, Simp_Size_Method, Auto_Method, Force_Method]
+val simp_based_methods =
+  [Simp_Method, Simp_Size_Method, Auto_Method, Auto_Choice_Method, Force_Method]
 
 fun thms_influence_proof_method ctxt meth ths =
   not (member (op =) simp_based_methods meth) orelse