# HG changeset patch
# User blanchet
# Date 1285799377 -7200
# Node ID 25a339e1ff9bf0be8a7a2448f99eb773a7f1618c
# Parent  699a20afc5bd54ca69dffb9a05135d4f1a3595ee
move functions closer to where they're used

diff -r 699a20afc5bd -r 25a339e1ff9b src/HOL/Tools/Sledgehammer/metis_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/metis_reconstruct.ML	Thu Sep 30 00:12:11 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_reconstruct.ML	Thu Sep 30 00:29:37 2010 +0200
@@ -352,6 +352,21 @@
           get (n+1) xs
   in get 1 end
 
+(* Permute a rule's premises to move the i-th premise to the last position. *)
+fun make_last i th =
+  let val n = nprems_of th
+  in  if 1 <= i andalso i <= n
+      then Thm.permute_prems (i-1) 1 th
+      else raise THM("select_literal", i, [th])
+  end;
+
+(* Maps a rule that ends "... ==> P ==> False" to "... ==> ~P" while suppressing
+   double-negations. *)
+val negate_head = rewrite_rule [@{thm atomize_not}, not_not RS eq_reflection]
+
+(* Maps the clause  [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P *)
+val select_literal = negate_head oo make_last
+
 fun resolve_inf ctxt mode old_skolems thpairs atm th1 th2 =
   let
     val thy = ProofContext.theory_of ctxt
@@ -378,8 +393,7 @@
               handle Empty => raise Fail "Failed to find literal in th2"
         val _ = trace_msg (fn () => "  index_th2: " ^ Int.toString index_th2)
     in
-      resolve_inc_tyvars thy (Meson.select_literal index_th1 i_th1) index_th2
-                         i_th2
+      resolve_inc_tyvars thy (select_literal index_th1 i_th1) index_th2 i_th2
     end
   end;
 
@@ -502,7 +516,17 @@
   | (_, Metis_Proof.Equality (f_lit, f_p, f_r)) =>
     equality_inf ctxt mode old_skolems f_lit f_p f_r
 
-fun is_real_literal (_, (c, _)) = not (String.isPrefix class_prefix c)
+fun flexflex_first_order th =
+  case Thm.tpairs_of th of
+      [] => th
+    | pairs =>
+        let val thy = theory_of_thm th
+            val (_, tenv) =
+              fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty)
+            val t_pairs = map Meson.term_pair_of (Vartab.dest tenv)
+            val th' = Thm.instantiate ([], map (pairself (cterm_of thy)) t_pairs) th
+        in  th'  end
+        handle THM _ => th;
 
 fun replay_one_inference ctxt mode old_skolems (fol_th, inf) thpairs =
   let
@@ -510,7 +534,7 @@
     val _ = trace_msg (fn () => "METIS THM: " ^ Metis_Thm.toString fol_th)
     val _ = trace_msg (fn () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf)
     val th = step ctxt mode old_skolems thpairs (fol_th, inf)
-             |> Meson.flexflex_first_order
+             |> flexflex_first_order
     val _ = trace_msg (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
     val _ = trace_msg (fn () => "=============================================")
   in (fol_th, th) :: thpairs end
diff -r 699a20afc5bd -r 25a339e1ff9b src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Thu Sep 30 00:12:11 2010 +0200
+++ b/src/HOL/Tools/meson.ML	Thu Sep 30 00:29:37 2010 +0200
@@ -9,7 +9,6 @@
 sig
   val trace: bool Unsynchronized.ref
   val term_pair_of: indexname * (typ * 'a) -> term * 'a
-  val flexflex_first_order: thm -> thm
   val size_of_subgoals: thm -> int
   val has_too_many_clauses: Proof.context -> term -> bool
   val make_cnf: thm list -> thm -> Proof.context -> thm list * Proof.context
@@ -37,9 +36,6 @@
   val make_meta_clause: thm -> thm
   val make_meta_clauses: thm list -> thm list
   val meson_tac: Proof.context -> thm list -> int -> tactic
-  val negate_head: thm -> thm
-  val select_literal: int -> thm -> thm
-  val skolemize_tac: Proof.context -> int -> tactic
   val setup: theory -> theory
 end
 
@@ -110,18 +106,6 @@
     SOME th => th
   | NONE => raise THM ("first_order_resolve", 0, [thA, thB]))
 
-fun flexflex_first_order th =
-  case Thm.tpairs_of th of
-      [] => th
-    | pairs =>
-        let val thy = theory_of_thm th
-            val (_, tenv) =
-              fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty)
-            val t_pairs = map term_pair_of (Vartab.dest tenv)
-            val th' = Thm.instantiate ([], map (pairself (cterm_of thy)) t_pairs) th
-        in  th'  end
-        handle THM _ => th;
-
 (*Forward proof while preserving bound variables names*)
 fun rename_bvs_RS th rl =
   let val th' = th RS rl
@@ -694,37 +678,4 @@
     name_thms "MClause#"
       (distinct Thm.eq_thm_prop (map make_meta_clause ths));
 
-(*Permute a rule's premises to move the i-th premise to the last position.*)
-fun make_last i th =
-  let val n = nprems_of th
-  in  if 1 <= i andalso i <= n
-      then Thm.permute_prems (i-1) 1 th
-      else raise THM("select_literal", i, [th])
-  end;
-
-(*Maps a rule that ends "... ==> P ==> False" to "... ==> ~P" while suppressing
-  double-negations.*)
-val negate_head = rewrite_rule [@{thm atomize_not}, not_not RS eq_reflection];
-
-(*Maps the clause  [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P*)
-fun select_literal i cl = negate_head (make_last i cl);
-
-
-(*Top-level Skolemization. Allows part of the conversion to clauses to be
-  expressed as a tactic (or Isar method).  Each assumption of the selected
-  goal is converted to NNF and then its existential quantifiers are pulled
-  to the front. Finally, all existential quantifiers are eliminated,
-  leaving !!-quantified variables. Perhaps Safe_tac should follow, but it
-  might generate many subgoals.*)
-
-fun skolemize_tac ctxt = SUBGOAL (fn (goal, i) =>
-  let val ts = Logic.strip_assums_hyp goal
-  in
-    EVERY'
-     [Misc_Legacy.METAHYPS (fn hyps =>
-        (cut_facts_tac (skolemize_nnf_list ctxt hyps) 1
-          THEN REPEAT (etac exE 1))),
-      REPEAT_DETERM_N (length ts) o (etac thin_rl)] i
-  end);
-
 end;