# HG changeset patch
# User blanchet
# Date 1409263046 -7200
# Node ID 4ae52c60603a0ec01c0b84658a83869ea06b2de2
# Parent  ecf5826ba23449f06b06287f3826cd9b6103b611
renamed 'skolem' to 'moura' (to suggest Z3-style skolemization); reintroduced 'fastforce' to the mix of tested proof methods

diff -r ecf5826ba234 -r 4ae52c60603a src/HOL/Hilbert_Choice.thy
--- a/src/HOL/Hilbert_Choice.thy	Thu Aug 28 23:48:46 2014 +0200
+++ b/src/HOL/Hilbert_Choice.thy	Thu Aug 28 23:57:26 2014 +0200
@@ -114,14 +114,14 @@
 subsection {* A skolemization tactic and proof method *}
 
 ML {*
-fun skolem_tac ctxt =
+fun moura_tac ctxt =
   Atomize_Elim.atomize_elim_tac ctxt THEN'
   SELECT_GOAL (Clasimp.auto_tac (ctxt addSIs @{thms choice bchoice}) THEN ALLGOALS (blast_tac ctxt));
 *}
 
-method_setup skolem = {*
- Scan.succeed (SIMPLE_METHOD' o skolem_tac)
-*} "solve skolemization goals"
+method_setup moura = {*
+ Scan.succeed (SIMPLE_METHOD' o moura_tac)
+*} "solve skolemization goals, especially those arising from Z3 proofs"
 
 
 subsection {*Function Inverse*}
diff -r ecf5826ba234 -r 4ae52c60603a src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Aug 28 23:48:46 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Aug 28 23:57:26 2014 +0200
@@ -128,7 +128,7 @@
   * (term, string) atp_step list * thm
 
 val basic_systematic_methods = [Metis_Method (NONE, NONE), Meson_Method, Blast_Method, SATx_Method]
-val basic_simp_based_methods = [Auto_Method, Simp_Method, Force_Method]
+val basic_simp_based_methods = [Auto_Method, Simp_Method, Fastforce_Method, Force_Method]
 val basic_arith_methods = [Linarith_Method, Presburger_Method, Algebra_Method]
 
 val arith_methods = basic_arith_methods @ basic_simp_based_methods @ basic_systematic_methods
@@ -137,7 +137,7 @@
   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 = basic_simp_based_methods @ basic_systematic_methods @ basic_arith_methods
-fun skolem_methods_of z3 = (basic_systematic_methods, [Skolem_Method]) |> z3 ? swap |> op @
+fun skolem_methods_of z3 = basic_systematic_methods |> z3 ? cons Moura_Method
 
 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)) =
diff -r ecf5826ba234 -r 4ae52c60603a src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Thu Aug 28 23:48:46 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Thu Aug 28 23:57:26 2014 +0200
@@ -18,8 +18,9 @@
     Simp_Method |
     Simp_Size_Method |
     Auto_Method |
+    Fastforce_Method |
     Force_Method |
-    Skolem_Method |
+    Moura_Method |
     Linarith_Method |
     Presburger_Method |
     Algebra_Method
@@ -57,8 +58,9 @@
   Simp_Method |
   Simp_Size_Method |
   Auto_Method |
+  Fastforce_Method |
   Force_Method |
-  Skolem_Method |
+  Moura_Method |
   Linarith_Method |
   Presburger_Method |
   Algebra_Method
@@ -94,8 +96,9 @@
       | 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"
+      | Fastforce_Method => "fastforce"
       | Force_Method => "force"
-      | Skolem_Method => "skolem"
+      | Moura_Method => "moura"
       | Linarith_Method => "linarith"
       | Presburger_Method => "presburger"
       | Algebra_Method => "algebra")
@@ -122,14 +125,15 @@
       SATx_Method => SAT.satx_tac ctxt
     | Blast_Method => blast_tac ctxt
     | Auto_Method => SELECT_GOAL (Clasimp.auto_tac ctxt)
+    | Fastforce_Method => Clasimp.fast_force_tac ctxt
     | Force_Method => Clasimp.force_tac ctxt
-    | Skolem_Method => skolem_tac ctxt
+    | Moura_Method => moura_tac 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, Skolem_Method]
+val simp_based_methods = [Simp_Method, Simp_Size_Method, Auto_Method, Force_Method, Moura_Method]
 
 fun thms_influence_proof_method ctxt meth ths =
   not (member (op =) simp_based_methods meth) orelse
diff -r ecf5826ba234 -r 4ae52c60603a src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Thu Aug 28 23:48:46 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Thu Aug 28 23:57:26 2014 +0200
@@ -162,7 +162,7 @@
 fun bunches_of_proof_methods try0 smt_proofs needs_full_types desperate_lam_trans =
   (if try0 then
     [[Simp_Method, Auto_Method, Blast_Method, Linarith_Method],
-     [Meson_Method, Force_Method, Presburger_Method]]
+     [Meson_Method, Fastforce_Method, Force_Method, Presburger_Method]]
    else
      []) @
   [[Metis_Method (if needs_full_types then SOME full_typesN else NONE, NONE)],