Meson.first_order_resolve: avoid handle _;
proper context for various Meson and Metis rules and tactics
unified meson_tac/meson_claset_tac;

--- a/src/HOL/Tools/meson.ML	Wed Jul 29 00:09:14 2009 +0200
+++ b/src/HOL/Tools/meson.ML	Wed Jul 29 19:35:10 2009 +0200
@@ -14,30 +14,29 @@
   val too_many_clauses: Proof.context option -> term -> bool
   val make_cnf: thm list -> thm -> Proof.context -> thm list * Proof.context
   val finish_cnf: thm list -> thm list
-  val make_nnf: thm -> thm
-  val skolemize: thm -> thm
+  val make_nnf: Proof.context -> thm -> thm
+  val skolemize: Proof.context -> thm -> thm
   val is_fol_term: theory -> term -> bool
   val make_clauses: thm list -> thm list
   val make_horns: thm list -> thm list
   val best_prolog_tac: (thm -> int) -> thm list -> tactic
   val depth_prolog_tac: thm list -> tactic
   val gocls: thm list -> thm list
-  val skolemize_prems_tac: thm list -> int -> tactic
-  val MESON: (thm list -> thm list) -> (thm list -> tactic) -> int -> tactic
-  val best_meson_tac: (thm -> int) -> int -> tactic
-  val safe_best_meson_tac: claset -> int -> tactic
-  val depth_meson_tac: int -> tactic
+  val skolemize_prems_tac: Proof.context -> thm list -> int -> tactic
+  val MESON: (thm list -> thm list) -> (thm list -> tactic) -> Proof.context -> int -> tactic
+  val best_meson_tac: (thm -> int) -> Proof.context -> int -> tactic
+  val safe_best_meson_tac: Proof.context -> int -> tactic
+  val depth_meson_tac: Proof.context -> int -> tactic
   val prolog_step_tac': thm list -> int -> tactic
   val iter_deepen_prolog_tac: thm list -> tactic
-  val iter_deepen_meson_tac: thm list -> int -> tactic
+  val iter_deepen_meson_tac: Proof.context -> thm list -> int -> tactic
   val make_meta_clause: thm -> thm
   val make_meta_clauses: thm list -> thm list
-  val meson_claset_tac: thm list -> claset -> int -> tactic
-  val meson_tac: claset -> int -> tactic
+  val meson_tac: Proof.context -> thm list -> int -> tactic
   val negate_head: thm -> thm
   val select_literal: int -> thm -> thm
-  val skolemize_tac: int -> tactic
-  val setup: Context.theory -> Context.theory
+  val skolemize_tac: Proof.context -> int -> tactic
+  val setup: theory -> theory
 end
 
 structure Meson: MESON =
@@ -89,13 +88,16 @@
 
 (*FIXME: currently does not "rename variables apart"*)
 fun first_order_resolve thA thB =
-  let val thy = theory_of_thm thA
-      val tmA = concl_of thA
-      val Const("==>",_) $ tmB $ _ = prop_of thB
-      val (tyenv, tenv) = Pattern.first_order_match thy (tmB, tmA) (Vartab.empty, Vartab.empty)
-      val ct_pairs = map (pairself (cterm_of thy) o term_pair_of) (Vartab.dest tenv)
-  in  thA RS (cterm_instantiate ct_pairs thB)  end
-  handle _ => raise THM ("first_order_resolve", 0, [thA,thB]);  (* FIXME avoid handle _ *)
+  (case
+    try (fn () =>
+      let val thy = theory_of_thm thA
+          val tmA = concl_of thA
+          val Const("==>",_) $ tmB $ _ = prop_of thB
+          val (tyenv, tenv) = Pattern.first_order_match thy (tmB, tmA) (Vartab.empty, Vartab.empty)
+          val ct_pairs = map (pairself (cterm_of thy) o term_pair_of) (Vartab.dest tenv)
+      in  thA RS (cterm_instantiate ct_pairs thB)  end) () of
+    SOME th => th
+  | NONE => raise THM ("first_order_resolve", 0, [thA, thB]));
 
 fun flexflex_first_order th =
   case (tpairs_of th) of
@@ -124,13 +126,13 @@
   e.g. from conj_forward, should have the form
     "[| P' ==> ?P; Q' ==> ?Q |] ==> ?P & ?Q"
   and the effect should be to instantiate ?P and ?Q with normalized versions of P' and Q'.*)
-fun forward_res nf st =
+fun forward_res ctxt nf st =
   let fun forward_tacf [prem] = rtac (nf prem) 1
         | forward_tacf prems =
             error (cat_lines
               ("Bad proof state in forward_res, please inform [e-mail]:" ::
-                Display.string_of_thm_without_context st ::
-                "Premises:" :: map Display.string_of_thm_without_context prems))
+                Display.string_of_thm ctxt st ::
+                "Premises:" :: map (Display.string_of_thm ctxt) prems))
   in
     case Seq.pull (ALLGOALS (OldGoals.METAHYPS forward_tacf) st)
     of SOME(th,_) => th
@@ -223,7 +225,7 @@
 (*** Removal of duplicate literals ***)
 
 (*Forward proof, passing extra assumptions as theorems to the tactic*)
-fun forward_res2 nf hyps st =
+fun forward_res2 ctxt nf hyps st =
   case Seq.pull
         (REPEAT
          (OldGoals.METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1)
@@ -233,16 +235,16 @@
 
 (*Remove duplicates in P|Q by assuming ~P in Q
   rls (initially []) accumulates assumptions of the form P==>False*)
-fun nodups_aux rls th = nodups_aux rls (th RS disj_assoc)
+fun nodups_aux ctxt rls th = nodups_aux ctxt rls (th RS disj_assoc)
     handle THM _ => tryres(th,rls)
-    handle THM _ => tryres(forward_res2 nodups_aux rls (th RS disj_forward2),
+    handle THM _ => tryres(forward_res2 ctxt (nodups_aux ctxt) rls (th RS disj_forward2),
                            [disj_FalseD1, disj_FalseD2, asm_rl])
     handle THM _ => th;
 
 (*Remove duplicate literals, if there are any*)
-fun nodups th =
+fun nodups ctxt th =
   if has_duplicates (op =) (literals (prop_of th))
-    then nodups_aux [] th
+    then nodups_aux ctxt [] th
     else th;
 
 
@@ -321,7 +323,7 @@
       fun cnf_aux (th,ths) =
         if not (can HOLogic.dest_Trueprop (prop_of th)) then ths (*meta-level: ignore*)
         else if not (has_conns ["All","Ex","op &"] (prop_of th))
-        then nodups th :: ths (*no work to do, terminate*)
+        then nodups ctxt th :: ths (*no work to do, terminate*)
         else case head_of (HOLogic.dest_Trueprop (concl_of th)) of
             Const ("op &", _) => (*conjunction*)
                 cnf_aux (th RS conjunct1, cnf_aux (th RS conjunct2, ths))
@@ -335,10 +337,10 @@
               (*Disjunction of P, Q: Create new goal of proving ?P | ?Q and solve it using
                 all combinations of converting P, Q to CNF.*)
               let val tac =
-                  (OldGoals.METAHYPS (resop cnf_nil) 1) THEN
+                  OldGoals.METAHYPS (resop cnf_nil) 1 THEN
                    (fn st' => st' |> OldGoals.METAHYPS (resop cnf_nil) 1)
               in  Seq.list_of (tac (th RS disj_forward)) @ ths  end
-          | _ => nodups th :: ths  (*no work to do*)
+          | _ => nodups ctxt th :: ths  (*no work to do*)
       and cnf_nil th = cnf_aux (th,[])
       val cls = 
 	    if too_many_clauses (SOME ctxt) (concl_of th)
@@ -499,11 +501,11 @@
   | ok4nnf (Const ("Trueprop",_) $ t) = rigid t
   | ok4nnf _ = false;
 
-fun make_nnf1 th =
+fun make_nnf1 ctxt th =
   if ok4nnf (concl_of th)
-  then make_nnf1 (tryres(th, nnf_rls))
+  then make_nnf1 ctxt (tryres(th, nnf_rls))
     handle THM ("tryres", _, _) =>
-        forward_res make_nnf1
+        forward_res ctxt (make_nnf1 ctxt)
            (tryres(th, [conj_forward,disj_forward,all_forward,ex_forward]))
     handle THM ("tryres", _, _) => th
   else th;
@@ -521,32 +523,32 @@
   HOL_basic_ss addsimps nnf_extra_simps
     addsimprocs [defALL_regroup,defEX_regroup, @{simproc neq}, @{simproc let_simp}];
 
-fun make_nnf th = case prems_of th of
+fun make_nnf ctxt th = case prems_of th of
     [] => th |> rewrite_rule (map safe_mk_meta_eq nnf_simps)
              |> simplify nnf_ss
-             |> make_nnf1
+             |> make_nnf1 ctxt
   | _ => raise THM ("make_nnf: premises in argument", 0, [th]);
 
 (*Pull existential quantifiers to front. This accomplishes Skolemization for
   clauses that arise from a subgoal.*)
-fun skolemize1 th =
+fun skolemize1 ctxt th =
   if not (has_conns ["Ex"] (prop_of th)) then th
-  else (skolemize1 (tryres(th, [choice, conj_exD1, conj_exD2,
+  else (skolemize1 ctxt (tryres(th, [choice, conj_exD1, conj_exD2,
                               disj_exD, disj_exD1, disj_exD2])))
     handle THM ("tryres", _, _) =>
-        skolemize1 (forward_res skolemize1
+        skolemize1 ctxt (forward_res ctxt (skolemize1 ctxt)
                    (tryres (th, [conj_forward, disj_forward, all_forward])))
     handle THM ("tryres", _, _) => 
-        forward_res skolemize1 (rename_bvs_RS th ex_forward);
+        forward_res ctxt (skolemize1 ctxt) (rename_bvs_RS th ex_forward);
 
-fun skolemize th = skolemize1 (make_nnf th);
+fun skolemize ctxt th = skolemize1 ctxt (make_nnf ctxt th);
 
-fun skolemize_nnf_list [] = []
-  | skolemize_nnf_list (th::ths) = 
-      skolemize th :: skolemize_nnf_list ths
+fun skolemize_nnf_list _ [] = []
+  | skolemize_nnf_list ctxt (th::ths) =
+      skolemize ctxt th :: skolemize_nnf_list ctxt ths
       handle THM _ => (*RS can fail if Unify.search_bound is too small*)
-       (warning ("Failed to Skolemize " ^ Display.string_of_thm_without_context th);
-        skolemize_nnf_list ths);
+       (warning ("Failed to Skolemize " ^ Display.string_of_thm ctxt th);
+        skolemize_nnf_list ctxt ths);
 
 fun add_clauses (th,cls) =
   let val ctxt0 = Variable.thm_context th
@@ -574,19 +576,19 @@
 (*Return all negative clauses, as possible goal clauses*)
 fun gocls cls = name_thms "Goal#" (map make_goal (neg_clauses cls));
 
-fun skolemize_prems_tac prems =
-    cut_facts_tac (skolemize_nnf_list prems) THEN'
+fun skolemize_prems_tac ctxt prems =
+    cut_facts_tac (skolemize_nnf_list ctxt prems) THEN'
     REPEAT o (etac exE);
 
 (*Basis of all meson-tactics.  Supplies cltac with clauses: HOL disjunctions.
   Function mkcl converts theorems to clauses.*)
-fun MESON mkcl cltac i st =
+fun MESON mkcl cltac ctxt i st =
   SELECT_GOAL
     (EVERY [ObjectLogic.atomize_prems_tac 1,
             rtac ccontr 1,
-            OldGoals.METAHYPS (fn negs =>
-                      EVERY1 [skolemize_prems_tac negs,
-                              OldGoals.METAHYPS (cltac o mkcl)]) 1]) i st
+            FOCUS (fn {context = ctxt', prems = negs, ...} =>
+                      EVERY1 [skolemize_prems_tac ctxt negs,
+                              FOCUS (cltac o mkcl o #prems) ctxt']) ctxt 1]) i st
   handle THM _ => no_tac st;    (*probably from make_meta_clause, not first-order*)
 
 (** Best-first search versions **)
@@ -600,9 +602,9 @@
                          (prolog_step_tac (make_horns cls) 1));
 
 (*First, breaks the goal into independent units*)
-fun safe_best_meson_tac cs =
-     SELECT_GOAL (TRY (safe_tac cs) THEN
-                  TRYALL (best_meson_tac size_of_subgoals));
+fun safe_best_meson_tac ctxt =
+     SELECT_GOAL (TRY (safe_tac (claset_of ctxt)) THEN
+                  TRYALL (best_meson_tac size_of_subgoals ctxt));
 
 (** Depth-first search version **)
 
@@ -627,7 +629,7 @@
 fun iter_deepen_prolog_tac horns =
     ITER_DEEPEN (has_fewer_prems 1) (prolog_step_tac' horns);
 
-fun iter_deepen_meson_tac ths = MESON make_clauses
+fun iter_deepen_meson_tac ctxt ths = ctxt |> MESON make_clauses
   (fn cls =>
     (case (gocls (cls @ ths)) of
       [] => no_tac  (*no goal clauses*)
@@ -636,14 +638,12 @@
           val horns = make_horns (cls @ ths)
           val _ = Output.debug (fn () =>
             cat_lines ("meson method called:" ::
-              map Display.string_of_thm_without_context (cls @ ths) @
-              ["clauses:"] @ map Display.string_of_thm_without_context horns))
+              map (Display.string_of_thm ctxt) (cls @ ths) @
+              ["clauses:"] @ map (Display.string_of_thm ctxt) horns))
         in THEN_ITER_DEEPEN (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' horns) end));
 
-fun meson_claset_tac ths cs =
-  SELECT_GOAL (TRY (safe_tac cs) THEN TRYALL (iter_deepen_meson_tac ths));
-
-val meson_tac = meson_claset_tac [];
+fun meson_tac ctxt ths =
+  SELECT_GOAL (TRY (safe_tac (claset_of ctxt)) THEN TRYALL (iter_deepen_meson_tac ctxt ths));
 
 
 (**** Code to support ordinary resolution, rather than Model Elimination ****)
@@ -695,14 +695,14 @@
   leaving !!-quantified variables. Perhaps Safe_tac should follow, but it
   might generate many subgoals.*)
 
-fun skolemize_tac i st =
-  let val ts = Logic.strip_assums_hyp (List.nth (prems_of st, i-1))
+fun skolemize_tac ctxt = SUBGOAL (fn (goal, i) =>
+  let val ts = Logic.strip_assums_hyp goal
   in
-     EVERY' [OldGoals.METAHYPS
-            (fn hyps => (cut_facts_tac (skolemize_nnf_list hyps) 1
-                         THEN REPEAT (etac exE 1))),
-            REPEAT_DETERM_N (length ts) o (etac thin_rl)] i st
-  end
-  handle Subscript => Seq.empty;
+    EVERY'
+     [OldGoals.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;

--- a/src/HOL/Tools/metis_tools.ML	Wed Jul 29 00:09:14 2009 +0200
+++ b/src/HOL/Tools/metis_tools.ML	Wed Jul 29 19:35:10 2009 +0200
@@ -628,7 +628,8 @@
        if exists_type ResAxioms.type_has_empty_sort (prop_of st0)  
        then (warning "Proof state contains the empty sort"; Seq.empty)
        else 
-	 (Meson.MESON ResAxioms.neg_clausify (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) i
+	 (Meson.MESON ResAxioms.neg_clausify
+	   (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) ctxt i
 	  THEN ResAxioms.expand_defs_tac st0) st0
     end
     handle METIS s => (warning ("Metis: " ^ s); Seq.empty);

--- a/src/HOL/Tools/res_axioms.ML	Wed Jul 29 00:09:14 2009 +0200
+++ b/src/HOL/Tools/res_axioms.ML	Wed Jul 29 19:35:10 2009 +0200
@@ -270,8 +270,10 @@
 (*Converts an Isabelle theorem (intro, elim or simp format, even higher-order) into NNF.*)
 fun to_nnf th ctxt0 =
   let val th1 = th |> transform_elim |> zero_var_indexes
-      val ((_,[th2]),ctxt) = Variable.import true [th1] ctxt0
-      val th3 = th2 |> Conv.fconv_rule ObjectLogic.atomize |> Meson.make_nnf |> strip_lambdas ~1
+      val ((_, [th2]), ctxt) = Variable.import true [th1] ctxt0
+      val th3 = th2
+        |> Conv.fconv_rule ObjectLogic.atomize
+        |> Meson.make_nnf ctxt |> strip_lambdas ~1
   in  (th3, ctxt)  end;
 
 (*Generate Skolem functions for a theorem supplied in nnf*)
@@ -483,33 +485,35 @@
   in Seq.of_list [LocalDefs.expand (filter (is_okdef fixed o Thm.term_of) defs) st] end;
 
 
-fun meson_general_tac ths i st0 =
+fun meson_general_tac ctxt ths i st0 =
   let
-    val thy = Thm.theory_of_thm st0
-  in  (Meson.meson_claset_tac (maps (cnf_axiom thy) ths) HOL_cs i THEN expand_defs_tac st0) st0 end;
+    val thy = ProofContext.theory_of ctxt
+    val ctxt0 = Classical.put_claset HOL_cs ctxt
+  in (Meson.meson_tac ctxt0 (maps (cnf_axiom thy) ths) i THEN expand_defs_tac st0) st0 end;
 
 val meson_method_setup =
-  Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn _ =>
-    SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ths)))
+  Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt =>
+    SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ctxt ths)))
     "MESON resolution proof procedure";
 
 
 (*** Converting a subgoal into negated conjecture clauses. ***)
 
-val neg_skolemize_tac = EVERY' [rtac ccontr, ObjectLogic.atomize_prems_tac, Meson.skolemize_tac];
+fun neg_skolemize_tac ctxt =
+  EVERY' [rtac ccontr, ObjectLogic.atomize_prems_tac, Meson.skolemize_tac ctxt];
 
 val neg_clausify = Meson.make_clauses #> map combinators #> Meson.finish_cnf;
 
 fun neg_conjecture_clauses ctxt st0 n =
   let
-    val st = Seq.hd (neg_skolemize_tac n st0)
+    val st = Seq.hd (neg_skolemize_tac ctxt n st0)
     val ({params, prems, ...}, _) = Subgoal.focus (Variable.set_body false ctxt) n st
   in (neg_clausify prems, map (Term.dest_Free o Thm.term_of o #2) params) end;
 
 (*Conversion of a subgoal to conjecture clauses. Each clause has
   leading !!-bound universal variables, to express generality. *)
 fun neg_clausify_tac ctxt =
-  neg_skolemize_tac THEN'
+  neg_skolemize_tac ctxt THEN'
   SUBGOAL (fn (prop, i) =>
     let val ts = Logic.strip_assums_hyp prop in
       EVERY'

--- a/src/HOL/ex/Classical.thy	Wed Jul 29 00:09:14 2009 +0200
+++ b/src/HOL/ex/Classical.thy	Wed Jul 29 19:35:10 2009 +0200
@@ -429,7 +429,7 @@
 lemma "(\<forall>x y z. R(x,y) & R(y,z) --> R(x,z)) &
        (\<forall>x. \<exists>y. R(x,y)) -->
        ~ (\<forall>x. P x = (\<forall>y. R(x,y) --> ~ P y))"
-by (tactic{*Meson.safe_best_meson_tac @{claset} 1*})
+by (tactic{*Meson.safe_best_meson_tac @{context} 1*})
     --{*In contrast, @{text meson} is SLOW: 7.6s on griffon*}
 
 
@@ -723,7 +723,7 @@
        (\<forall>x y. bird x & snail y \<longrightarrow> ~eats x y) &
        (\<forall>x. (caterpillar x \<or> snail x) \<longrightarrow> (\<exists>y. plant y & eats x y))
        \<longrightarrow> (\<exists>x y. animal x & animal y & (\<exists>z. grain z & eats y z & eats x y))"
-by (tactic{*Meson.safe_best_meson_tac @{claset} 1*})
+by (tactic{*Meson.safe_best_meson_tac @{context} 1*})
     --{*Nearly twice as fast as @{text meson},
         which performs iterative deepening rather than best-first search*}
 

--- a/src/HOL/ex/Meson_Test.thy	Wed Jul 29 00:09:14 2009 +0200
+++ b/src/HOL/ex/Meson_Test.thy	Wed Jul 29 19:35:10 2009 +0200
@@ -31,8 +31,8 @@
 Goal "(\<exists>x. P x) & (\<forall>x. L x --> ~ (M x & R x)) & (\<forall>x. P x --> (M x & L x)) & ((\<forall>x. P x --> Q x) | (\<exists>x. P x & R x)) --> (\<exists>x. Q x & P x)";
 by (rtac ccontr 1);
 val [prem25] = gethyps 1;
-val nnf25 = Meson.make_nnf prem25;
-val xsko25 = Meson.skolemize nnf25;
+val nnf25 = Meson.make_nnf @{context} prem25;
+val xsko25 = Meson.skolemize @{context} nnf25;
 by (cut_facts_tac [xsko25] 1 THEN REPEAT (etac exE 1));
 val [_,sko25] = gethyps 1;
 val clauses25 = Meson.make_clauses [sko25];   (*7 clauses*)
@@ -51,8 +51,8 @@
 Goal "((\<exists>x. p x) = (\<exists>x. q x)) & (\<forall>x. \<forall>y. p x & q y --> (r x = s y)) --> ((\<forall>x. p x --> r x) = (\<forall>x. q x --> s x))";
 by (rtac ccontr 1);
 val [prem26] = gethyps 1;
-val nnf26 = Meson.make_nnf prem26;
-val xsko26 = Meson.skolemize nnf26;
+val nnf26 = Meson.make_nnf @{context} prem26;
+val xsko26 = Meson.skolemize @{context} nnf26;
 by (cut_facts_tac [xsko26] 1 THEN REPEAT (etac exE 1));
 val [_,sko26] = gethyps 1;
 val clauses26 = Meson.make_clauses [sko26];                   (*9 clauses*)
@@ -72,8 +72,8 @@
 Goal "(\<forall>x. \<forall>y. q x y = (\<forall>z. p z x = (p z y::bool))) --> (\<forall>x. (\<forall>y. q x y = (q y x::bool)))";
 by (rtac ccontr 1);
 val [prem43] = gethyps 1;
-val nnf43 = Meson.make_nnf prem43;
-val xsko43 = Meson.skolemize nnf43;
+val nnf43 = Meson.make_nnf @{context} prem43;
+val xsko43 = Meson.skolemize @{context} nnf43;
 by (cut_facts_tac [xsko43] 1 THEN REPEAT (etac exE 1));
 val [_,sko43] = gethyps 1;
 val clauses43 = Meson.make_clauses [sko43];   (*6*)