# HG changeset patch
# User blanchet
# Date 1285922391 -7200
# Node ID e26d5344e1b751c53af3b2935a13002b86a98731
# Parent  13b3a2ba9ea774bae8baf2604167729d9b295a14
compute substitutions in new skolemizer

diff -r 13b3a2ba9ea7 -r e26d5344e1b7 src/HOL/Tools/Sledgehammer/meson_clausify.ML
--- a/src/HOL/Tools/Sledgehammer/meson_clausify.ML	Thu Sep 30 20:44:53 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/meson_clausify.ML	Fri Oct 01 10:39:51 2010 +0200
@@ -12,7 +12,9 @@
   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 -> int -> thm -> thm option * thm list
+  val cluster_for_zapped_var_name : string -> int * bool
+  val cnf_axiom :
+    theory -> bool -> int -> thm -> (thm * term) option * thm list
   val meson_general_tac : Proof.context -> thm list -> int -> tactic
   val setup: theory -> theory
 end;
@@ -227,13 +229,17 @@
     val eqth = eqth RS @{thm TruepropI}
   in Thm.equal_elim eqth th end
 
-fun zapped_var_name ax_no (skolem, cluster_no) s =
+fun zapped_var_name ax_no (cluster_no, skolem) s =
   (if skolem then new_skolem_var_prefix else new_nonskolem_var_prefix) ^
   string_of_int ax_no ^ "_" ^ string_of_int cluster_no ^ "_" ^ s
 
+fun cluster_for_zapped_var_name s =
+  (nth (space_explode "_" s) 1 |> Int.fromString |> the,
+   String.isPrefix new_skolem_var_prefix s)
+
 fun zap_quantifiers ax_no =
   let
-    fun conv (cluster as (cluster_skolem, cluster_no)) pos ct =
+    fun conv (cluster as (cluster_no, cluster_skolem)) pos ct =
       ct |> (case term_of ct of
                Const (s, _) $ Abs (s', _, _) =>
                if s = @{const_name all} orelse s = @{const_name All} orelse
@@ -242,7 +248,7 @@
                    val skolem = (pos = (s = @{const_name Ex}))
                    val cluster =
                      if skolem = cluster_skolem then cluster
-                     else (skolem, cluster_no |> cluster_skolem ? Integer.add 1)
+                     else (cluster_no |> cluster_skolem ? Integer.add 1, skolem)
                  in
                    Thm.dest_comb #> snd
                    #> Thm.dest_abs (SOME (zapped_var_name ax_no cluster s'))
@@ -270,7 +276,7 @@
                  Conv.all_conv
              | _ => Conv.all_conv)
   in
-    conv (true, 0) true #> Drule.export_without_context
+    conv (0, true) true #> Drule.export_without_context
     #> cprop_of #> Thm.dest_equals #> snd
   end
 
@@ -329,7 +335,6 @@
       |> (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}),
@@ -337,10 +342,12 @@
                       @{thm skolem_COMBK_D}
       RS Thm.implies_intr ct th
   in
-    (opt |> Option.map (singleton export o fst),
+    (opt |> Option.map (I #>> singleton (Variable.export ctxt ctxt0)
+                        ##> (term_of #> HOLogic.dest_Trueprop
+                             #> singleton (Variable.export_terms ctxt ctxt0))),
      cnf_ths |> map (introduce_combinators_in_theorem
                      #> (case opt of SOME (_, ct) => intr_imp ct | NONE => I))
-             |> export
+             |> Variable.export ctxt ctxt0
              |> Meson.finish_cnf
              |> map Thm.close_derivation)
   end
diff -r 13b3a2ba9ea7 -r e26d5344e1b7 src/HOL/Tools/Sledgehammer/metis_tactics.ML
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Thu Sep 30 20:44:53 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Fri Oct 01 10:39:51 2010 +0200
@@ -59,11 +59,11 @@
    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 =
+fun unify_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
+    val prem = goal |> Logic.strip_assums_hyp |> the_single
+    val concl = goal |> Logic.strip_assums_concl
     fun add_types Tp instT =
       if exists (curry (op =) Tp) instT then instT
       else Tp :: map (apsnd (typ_subst_atomic [Tp])) instT
@@ -108,47 +108,62 @@
       | (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 _ = trace_msg (fn () => cat_lines (map (fn (t, u) =>
-            Syntax.string_of_term @{context} t ^ " |-> " ^
-            Syntax.string_of_term @{context} u) inst))
-        val instT = fold (fn Tp => unify_types (pairself fastype_of Tp)
-                                   handle TERM _ => I) 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
+
+    val inst = [] |> unify_terms (prem, concl)
+    val _ = trace_msg (fn () => cat_lines (map (fn (t, u) =>
+        Syntax.string_of_term @{context} t ^ " |-> " ^
+        Syntax.string_of_term @{context} u) inst))
+    val instT = fold (fn Tp => unify_types (pairself fastype_of Tp)
+                               handle TERM _ => I) 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
+  handle Empty => th (* ### FIXME *)
 
 (* 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
+fun discharge_skolem_premises ctxt axioms prems_imp_false =
+  case prop_of prems_imp_false of
+    @{prop False} => prems_imp_false
+  | prems_imp_false_prop =>
+    let
+      val thy = ProofContext.theory_of ctxt
+      fun match_term p =
+        let
+          val (tyenv, tenv) =
+            Pattern.first_order_match thy p (Vartab.empty, Vartab.empty)
+          val tsubst =
+            tenv |> Vartab.dest
+                 |> sort (prod_ord int_ord bool_ord
+                          o pairself (Meson_Clausify.cluster_for_zapped_var_name
+                                      o fst o fst))
+                 |> map (Meson.term_pair_of
+                         #> pairself (Envir.subst_term_types tyenv))
+        in (tyenv, tsubst) end
+      fun subst_info_for_prem assm_no prem =
+        case prem of
+          _ $ (Const (@{const_name skolem}, _) $ (_ $ t $ num)) =>
+          let val ax_no = num |> HOLogic.dest_number |> snd in
+            (ax_no, (assm_no, match_term (nth axioms ax_no |> snd, t)))
+          end
+        | _ => raise TERM ("discharge_skolem_premises: Malformed premise",
+                           [prem])
+      val prems = Logic.strip_imp_prems prems_imp_false_prop
+      val substs = map2 subst_info_for_prem (0 upto length prems - 1) prems
+    in
       Goal.prove ctxt [] [] @{prop False}
-          (K (cut_rules_tac axioms 1
+          (K (cut_rules_tac (map fst axioms) 1
               THEN TRY (REPEAT_ALL_NEW (etac @{thm exE}) 1)
               (* two copies are better than one (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 match_tac [prems_imp_false] 1
               THEN DETERM_UNTIL_SOLVED
                        (rtac @{thm skolem_COMBK_I} 1
-                        THEN PRIMITIVE (unify_one_prem_with_concl thy 1)
+                        THEN PRIMITIVE (unify_prem_with_concl thy 1)
                         THEN assume_tac 1)))
     end