second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions

--- a/src/HOL/Tools/Sledgehammer/meson_clausifier.ML	Wed Sep 29 22:23:27 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/meson_clausifier.ML	Wed Sep 29 23:06:02 2010 +0200
@@ -8,11 +8,12 @@
 signature MESON_CLAUSIFIER =
 sig
   val new_skolemizer : bool Config.T
+  val new_skolem_var_prefix : string
   val extensionalize_theorem : thm -> thm
   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 -> thm -> thm list
+  val cnf_axiom : theory -> thm -> thm option * thm list
   val meson_general_tac : Proof.context -> thm list -> int -> tactic
   val setup: theory -> theory
 end;
@@ -23,6 +24,8 @@
 val (new_skolemizer, new_skolemizer_setup) =
   Attrib.config_bool "meson_new_skolemizer" (K false)
 
+val new_skolem_var_prefix = "SK?" (* purposedly won't parse *)
+
 (**** Transformation of Elimination Rules into First-Order Formulas****)
 
 val cfalse = cterm_of @{theory HOL} HOLogic.false_const;
@@ -220,17 +223,6 @@
     |> Thm.varifyT_global
   end
 
-(* Converts an Isabelle theorem (intro, elim or simp format, even higher-order)
-   into NNF. *)
-fun nnf_axiom th ctxt0 =
-  let
-    val th1 = th |> transform_elim_theorem |> zero_var_indexes
-    val ((_, [th2]), ctxt) = Variable.import true [th1] ctxt0
-    val th3 = th2 |> Conv.fconv_rule Object_Logic.atomize
-                  |> extensionalize_theorem
-                  |> Meson.make_nnf ctxt
-  in (th3, ctxt) end
-
 fun to_definitional_cnf_with_quantifiers thy th =
   let
     val eqth = cnf.make_cnfx_thm thy (HOLogic.dest_Trueprop (prop_of th))
@@ -238,35 +230,120 @@
     val eqth = eqth RS @{thm TruepropI}
   in Thm.equal_elim eqth th end
 
-(* Convert a theorem to CNF, with Skolem functions as additional premises. *)
+val kill_quantifiers =
+  let
+    fun conv pos ct =
+      ct |> (case term_of ct of
+               Const (s, _) $ Abs (s', _, _) =>
+               if s = @{const_name all} orelse s = @{const_name All} orelse
+                  s = @{const_name Ex} then
+                 Thm.dest_comb #> snd
+                 #> Thm.dest_abs (SOME (s' |> pos = (s = @{const_name Ex})
+                                            ? prefix new_skolem_var_prefix))
+                 #> snd #> conv pos
+               else
+                 Conv.all_conv
+             | Const (s, _) $ _ $ _ =>
+               if s = @{const_name "==>"} orelse
+                  s = @{const_name HOL.implies} then
+                 Conv.combination_conv (Conv.arg_conv (conv (not pos)))
+                                       (conv pos)
+               else if s = @{const_name HOL.conj} orelse
+                       s = @{const_name HOL.disj} then
+                 Conv.combination_conv (Conv.arg_conv (conv pos)) (conv pos)
+               else
+                 Conv.all_conv
+             | Const (s, _) $ _ =>
+               if s = @{const_name Trueprop} then
+                 Conv.arg_conv (conv pos)
+               else if s = @{const_name Not} then
+                 Conv.arg_conv (conv (not pos))
+               else
+                 Conv.all_conv
+             | _ => Conv.all_conv)
+  in
+    conv true #> Drule.export_without_context
+    #> cprop_of #> Thm.dest_equals #> snd
+  end
+
+val pull_out_quant_ss =
+  MetaSimplifier.clear_ss HOL_basic_ss
+      addsimps @{thms all_simps[symmetric]}
+
+(* Converts an Isabelle theorem into NNF. *)
+fun nnf_axiom new_skolemizer th ctxt =
+  let
+    val thy = ProofContext.theory_of ctxt
+    val th =
+      th |> transform_elim_theorem
+         |> zero_var_indexes
+         |> new_skolemizer ? forall_intr_vars
+    val (th, ctxt) = Variable.import true [th] ctxt |>> snd |>> the_single
+    val th = th |> Conv.fconv_rule Object_Logic.atomize
+                |> extensionalize_theorem
+                |> Meson.make_nnf ctxt
+  in
+    if new_skolemizer then
+      let
+        val th' = th |> Meson.skolemize ctxt
+                     |> simplify pull_out_quant_ss
+                     |> Drule.eta_contraction_rule
+        val t = th' |> cprop_of |> kill_quantifiers |> term_of
+      in
+        if exists_subterm (fn Var ((s, _), _) =>
+                              String.isPrefix new_skolem_var_prefix s
+                            | _ => false) t then
+          let
+            val (ct, ctxt) =
+              Variable.import_terms true [t] ctxt
+              |>> the_single |>> cterm_of thy
+          in (SOME (th', ct), ct |> Thm.assume, ctxt) end
+       else
+          (NONE, th, ctxt)
+      end
+    else
+      (NONE, th, ctxt)
+  end
+
+(* Convert a theorem to CNF, with additional premises due to skolemization. *)
 fun cnf_axiom thy th =
   let
     val ctxt0 = Variable.global_thm_context th
-    val (nnf_th, ctxt) = nnf_axiom th ctxt0
+    val new_skolemizer = Config.get ctxt0 new_skolemizer
+    val (opt, nnf_th, ctxt) = nnf_axiom new_skolemizer th ctxt0
     fun aux th =
-      Meson.make_cnf (map (old_skolem_theorem_from_def thy)
-                          (old_skolem_defs th)) th ctxt
+      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)
            | p => p)
+    val export = Variable.export ctxt ctxt0
   in
-    cnf_ths |> map introduce_combinators_in_theorem
-            |> Variable.export ctxt ctxt0
-            |> Meson.finish_cnf
-            |> map Thm.close_derivation
+    (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))
+             |> export
+             |> Meson.finish_cnf
+             |> map Thm.close_derivation)
   end
-  handle THM _ => []
+  handle THM _ => (NONE, [])
 
 fun meson_general_tac ctxt ths =
   let
     val thy = ProofContext.theory_of ctxt
     val ctxt0 = Classical.put_claset HOL_cs ctxt
-  in Meson.meson_tac ctxt0 (maps (cnf_axiom thy) ths) end
+  in Meson.meson_tac ctxt0 (maps (snd o cnf_axiom thy) ths) end
 
 val setup =
-  Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt =>
-    SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ctxt ths)))
-    "MESON resolution proof procedure";
+  new_skolemizer_setup
+  #> Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt =>
+       SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ctxt ths)))
+       "MESON resolution proof procedure"
 
 end;

--- a/src/HOL/Tools/Sledgehammer/metis_reconstruct.ML	Wed Sep 29 22:23:27 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_reconstruct.ML	Wed Sep 29 23:06:02 2010 +0200
@@ -13,6 +13,7 @@
 
   val trace : bool Unsynchronized.ref
   val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a
+  val untyped_aconv : term -> term -> bool
   val replay_one_inference :
     Proof.context -> mode -> (string * term) list
     -> Metis_Thm.thm * Metis_Proof.inference -> (Metis_Thm.thm * thm) list

--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Wed Sep 29 22:23:27 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Wed Sep 29 23:06:02 2010 +0200
@@ -51,6 +51,98 @@
    models = []}
 val resolution_params = {active = active_params, waiting = waiting_params}
 
+(* In principle, it should be sufficient to apply "assume_tac" to unify the
+   conclusion with one of the premises. However, in practice, this fails
+   horribly because of the mildly higher-order nature of the unification
+   problems. Typical constraints are of the form "?x a b =?= b", where "a" and
+   "b" are goal parameters. *)
+fun unify_one_prem_with_concl thy i th =
+  let
+    val goal = Logic.get_goal (prop_of th) i |> Envir.beta_eta_contract
+    val prems = Logic.strip_assums_hyp goal
+    val concl = Logic.strip_assums_concl goal
+    fun add_types Tp instT =
+      if exists (curry (op =) Tp) instT then instT
+      else Tp :: map (apsnd (typ_subst_atomic [Tp])) instT
+    fun unify_types (T, U) =
+      if T = U then
+        I
+      else case (T, U) of
+        (TVar _, _) => add_types (T, U)
+      | (_, TVar _) => add_types (U, T)
+      | (Type (s, Ts), Type (t, Us)) =>
+        if s = t andalso length Ts = length Us then fold unify_types (Ts ~~ Us)
+        else raise TYPE ("unify_types", [T, U], [])
+      | _ => raise TYPE ("unify_types", [T, U], [])
+    fun pair_untyped_aconv (t1, t2) (u1, u2) =
+      untyped_aconv t1 u1 andalso untyped_aconv t2 u2
+    fun add_terms tp inst =
+      if exists (pair_untyped_aconv tp) inst then inst
+      else tp :: map (apsnd (subst_atomic [tp])) inst
+    fun is_flex t =
+      case strip_comb t of
+        (Var _, args) => forall (is_Bound orf is_Var orf is_Free) args
+      | _ => false
+    fun unify_flex flex rigid =
+      case strip_comb flex of
+        (Var (z as (_, T)), args) =>
+        add_terms (Var z,
+          (* FIXME: reindex bound variables *)
+          fold_rev (curry absdummy) (take (length args) (binder_types T)) rigid)
+      | _ => raise TERM ("unify_flex: expected flex", [flex])
+    fun unify_potential_flex comb atom =
+      if is_flex comb then unify_flex comb atom
+      else if is_Var atom then add_terms (atom, comb)
+      else raise TERM ("unify_terms", [comb, atom])
+    fun unify_terms (t, u) =
+      case (t, u) of
+        (t1 $ t2, u1 $ u2) =>
+        if is_flex t then unify_flex t u
+        else if is_flex u then unify_flex u t
+        else fold unify_terms [(t1, u1), (t2, u2)]
+      | (_ $ _, _) => unify_potential_flex t u
+      | (_, _ $ _) => unify_potential_flex u t
+      | (Var _, _) => add_terms (t, u)
+      | (_, Var _) => add_terms (u, t)
+      | _ => if untyped_aconv t u then I else raise TERM ("unify_terms", [t, u])
+    fun unify_prem prem =
+      let
+        val inst = [] |> unify_terms (prem, concl)
+        val instT = fold (unify_types o pairself fastype_of) inst []
+        val inst = inst |> map (pairself (subst_atomic_types instT))
+        val cinstT = instT |> map (pairself (ctyp_of thy))
+        val cinst = inst |> map (pairself (cterm_of thy))
+      in th |> Thm.instantiate (cinstT, []) |> Thm.instantiate ([], cinst) end
+  in
+    case prems of
+      [prem] => unify_prem prem
+    | _ =>
+      case fold (fn prem => fn th as SOME _ => th
+                             | NONE => try unify_prem prem) prems NONE of
+        SOME th => th
+      | NONE => raise Fail "unify_one_prem_with_concl"
+  end
+
+(* Attempts to derive the theorem "False" from a theorem of the form
+   "P1 ==> ... ==> Pn ==> False", where the "Pi"s are to be discharged using the
+   specified axioms. The axioms have leading "All" and "Ex" quantifiers, which
+   must be eliminated first. *)
+fun discharge_skolem_premises ctxt axioms premises_imp_false =
+  if prop_of premises_imp_false aconv @{prop False} then
+    premises_imp_false
+  else
+    let val thy = ProofContext.theory_of ctxt in
+      Goal.prove ctxt [] [] @{prop False}
+          (K (cut_rules_tac axioms 1
+              THEN TRY (REPEAT_ALL_NEW (etac @{thm exE}) 1)
+(* FIXME: THEN etac @{lemma "P ==> (P ==> P ==> Q) ==> Q" by fast} 1 *)
+              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)
+                        THEN assume_tac 1)))
+    end
+
 (* Main function to start Metis proof and reconstruction *)
 fun FOL_SOLVE mode ctxt cls ths0 =
   let val thy = ProofContext.theory_of ctxt
@@ -58,7 +150,8 @@
       val th_cls_pairs =
         map (fn th => (Thm.get_name_hint th, Meson_Clausifier.cnf_axiom thy th))
             ths0
-      val thss = map #2 th_cls_pairs
+      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")
       val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) cls
       val _ = trace_msg (fn () => "THEOREM CLAUSES")
@@ -68,7 +161,7 @@
       val _ = if null tfrees then ()
               else (trace_msg (fn () => "TFREE CLAUSES");
                     app (fn TyLitFree ((s, _), (s', _)) =>
-                            trace_msg (fn _ => s ^ "(" ^ s' ^ ")")) tfrees)
+                            trace_msg (fn () => s ^ "(" ^ s' ^ ")")) tfrees)
       val _ = trace_msg (fn () => "CLAUSES GIVEN TO METIS")
       val thms = map #1 axioms
       val _ = app (fn th => trace_msg (fn () => Metis_Thm.toString th)) thms
@@ -91,7 +184,7 @@
                 and used = map_filter (used_axioms axioms) proof
                 val _ = trace_msg (fn () => "METIS COMPLETED...clauses actually used:")
                 val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) used
-                val unused = th_cls_pairs |> map_filter (fn (name, cls) =>
+                val unused = th_cls_pairs |> map_filter (fn (name, (_, cls)) =>
                   if have_common_thm used cls then NONE else SOME name)
             in
                 if not (null cls) andalso not (have_common_thm used cls) then
@@ -106,7 +199,7 @@
                 case result of
                     (_,ith)::_ =>
                         (trace_msg (fn () => "Success: " ^ Display.string_of_thm ctxt ith);
-                         [ith])
+                         [discharge_skolem_premises ctxt dischargers ith])
                   | _ => (trace_msg (fn () => "Metis: No result"); [])
             end
         | Metis_Resolution.Satisfiable _ =>

--- a/src/HOL/Tools/Sledgehammer/metis_translate.ML	Wed Sep 29 22:23:27 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_translate.ML	Wed Sep 29 23:06:02 2010 +0200
@@ -95,8 +95,6 @@
 val type_const_prefix = "tc_";
 val class_prefix = "class_";
 
-val new_skolem_var_prefix = "SK?" (* purposedly won't parse *)
-
 val skolem_prefix = "Sledgehammer" ^ Long_Name.separator ^ "Sko"
 val old_skolem_prefix = skolem_prefix ^ "o"
 val new_skolem_prefix = skolem_prefix ^ "n"
@@ -427,7 +425,7 @@
     let
       val (tp, ts) = combtype_of T
       val v' =
-        if String.isPrefix new_skolem_var_prefix s then
+        if String.isPrefix Meson_Clausifier.new_skolem_var_prefix s then
           let
             val tys = T |> strip_type |> swap |> op ::
             val s' = new_skolem_name th_no s (length tys)