# HG changeset patch
# User blanchet
# Date 1285865977 -7200
# Node ID 35ae5cf8c96a5ef0c6242ccf1755109bc18f0beb
# Parent  25a339e1ff9bf0be8a7a2448f99eb773a7f1618c
encode number of skolem assumptions in them, for more efficient retrieval later

diff -r 25a339e1ff9b -r 35ae5cf8c96a src/HOL/Sledgehammer.thy
--- a/src/HOL/Sledgehammer.thy	Thu Sep 30 00:29:37 2010 +0200
+++ b/src/HOL/Sledgehammer.thy	Thu Sep 30 18:59:37 2010 +0200
@@ -60,6 +60,12 @@
 lemma equal_imp_equal [no_atp]: "X = Y ==> X = Y"
 by auto
 
+lemma skolem_COMBK_iff: "P \<longleftrightarrow> skolem (COMBK P (i\<Colon>nat))"
+unfolding skolem_def COMBK_def by (rule refl)
+
+lemmas skolem_COMBK_I = iffD1 [OF skolem_COMBK_iff]
+lemmas skolem_COMBK_D = iffD2 [OF skolem_COMBK_iff]
+
 text{*Theorems for translation to combinators*}
 
 lemma abs_S [no_atp]: "\<lambda>x. (f x) (g x) \<equiv> COMBS f g"
diff -r 25a339e1ff9b -r 35ae5cf8c96a src/HOL/Tools/Sledgehammer/meson_clausify.ML
--- a/src/HOL/Tools/Sledgehammer/meson_clausify.ML	Thu Sep 30 00:29:37 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/meson_clausify.ML	Thu Sep 30 18:59:37 2010 +0200
@@ -12,7 +12,7 @@
   val introduce_combinators_in_cterm : cterm -> thm
   val introduce_combinators_in_theorem : thm -> thm
   val to_definitional_cnf_with_quantifiers : theory -> thm -> thm
-  val cnf_axiom : theory -> bool -> thm -> thm option * thm list
+  val cnf_axiom : theory -> bool -> int -> thm -> thm option * thm list
   val meson_general_tac : Proof.context -> thm list -> int -> tactic
   val setup: theory -> theory
 end;
@@ -293,7 +293,7 @@
             val (ct, ctxt) =
               Variable.import_terms true [t] ctxt
               |>> the_single |>> cterm_of thy
-          in (SOME (th', ct), ct |> Thm.assume, ctxt) end
+          in (SOME (th', ct), Thm.assume ct, ctxt) end
        else
           (NONE, th, ctxt)
       end
@@ -302,27 +302,32 @@
   end
 
 (* Convert a theorem to CNF, with additional premises due to skolemization. *)
-fun cnf_axiom thy new_skolemizer th =
+fun cnf_axiom thy new_skolemizer ax_no th =
   let
     val ctxt0 = Variable.global_thm_context th
     val (opt, nnf_th, ctxt) = nnf_axiom new_skolemizer th ctxt0
-    fun aux th =
+    fun clausify th =
       Meson.make_cnf (if new_skolemizer then
                         []
                       else
                         map (old_skolem_theorem_from_def thy)
                             (old_skolem_defs th)) th ctxt
     val (cnf_ths, ctxt) =
-      aux nnf_th
-      |> (fn ([], _) => aux (to_definitional_cnf_with_quantifiers thy nnf_th)
+      clausify nnf_th
+      |> (fn ([], _) =>
+             clausify (to_definitional_cnf_with_quantifiers thy nnf_th)
            | p => p)
     val export = Variable.export ctxt ctxt0
+    fun intr_imp ct th =
+      Thm.instantiate ([], map (pairself (cterm_of @{theory}))
+                               [(Var (("i", 1), @{typ nat}),
+                                 HOLogic.mk_number @{typ nat} ax_no)])
+                      @{thm skolem_COMBK_D}
+      RS Thm.implies_intr ct th
   in
     (opt |> Option.map (singleton export o fst),
      cnf_ths |> map (introduce_combinators_in_theorem
-                     #> (case opt of
-                           SOME (_, ct) => Thm.implies_intr ct
-                         | NONE => I))
+                     #> (case opt of SOME (_, ct) => intr_imp ct | NONE => I))
              |> export
              |> Meson.finish_cnf
              |> map Thm.close_derivation)
@@ -333,7 +338,7 @@
   let
     val thy = ProofContext.theory_of ctxt
     val ctxt0 = Classical.put_claset HOL_cs ctxt
-  in Meson.meson_tac ctxt0 (maps (snd o cnf_axiom thy false) ths) end
+  in Meson.meson_tac ctxt0 (maps (snd o cnf_axiom thy false 0) ths) end
 
 val setup =
   Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt =>
diff -r 25a339e1ff9b -r 35ae5cf8c96a src/HOL/Tools/Sledgehammer/metis_tactics.ML
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Thu Sep 30 00:29:37 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Thu Sep 30 18:59:37 2010 +0200
@@ -147,7 +147,8 @@
               THEN TRY (REPEAT_ALL_NEW (etac @{thm allE}) 1)
               THEN match_tac [premises_imp_false] 1
               THEN DETERM_UNTIL_SOLVED
-                       (PRIMITIVE (unify_one_prem_with_concl thy 1)
+                       (rtac @{thm skolem_COMBK_I} 1
+                        THEN PRIMITIVE (unify_one_prem_with_concl thy 1)
                         THEN assume_tac 1)))
     end
 
@@ -157,8 +158,10 @@
       val type_lits = Config.get ctxt type_lits
       val new_skolemizer = Config.get ctxt new_skolemizer
       val th_cls_pairs =
-        map (fn th => (Thm.get_name_hint th,
-                       Meson_Clausify.cnf_axiom thy new_skolemizer th)) ths0
+        map2 (fn j => fn th =>
+                (Thm.get_name_hint th,
+                 Meson_Clausify.cnf_axiom thy new_skolemizer j th))
+             (0 upto length ths0 - 1) ths0
       val thss = map (snd o snd) th_cls_pairs
       val dischargers = map_filter (fst o snd) th_cls_pairs
       val _ = trace_msg (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")