# HG changeset patch
# User paulson
# Date 1198082448 -3600
# Node ID 4cdf7de81e1b07c86e56f233cffe627eeef1d338
# Parent  43a1f08c5a2957f24f2c4f84686b96787ae80a09
Replaced refs by config params; finer critical section in mets method

diff -r 43a1f08c5a29 -r 4cdf7de81e1b src/HOL/ATP_Linkup.thy
--- a/src/HOL/ATP_Linkup.thy	Wed Dec 19 16:52:26 2007 +0100
+++ b/src/HOL/ATP_Linkup.thy	Wed Dec 19 17:40:48 2007 +0100
@@ -109,6 +109,7 @@
 
 use "Tools/res_atp_methods.ML"
 setup ResAtpMethods.setup      --{*Oracle ATP methods: still useful?*}
+setup ResReconstruct.setup     --{*Config parameters*}
 setup ResAxioms.setup          --{*Sledgehammer*}
 
 subsection {* The Metis prover *}
diff -r 43a1f08c5a29 -r 4cdf7de81e1b src/HOL/MetisExamples/BigO.thy
--- a/src/HOL/MetisExamples/BigO.thy	Wed Dec 19 16:52:26 2007 +0100
+++ b/src/HOL/MetisExamples/BigO.thy	Wed Dec 19 17:40:48 2007 +0100
@@ -31,7 +31,7 @@
 
 (*** Now various verions with an increasing modulus ***)
 
-ML{*ResReconstruct.modulus := 1*}
+declare [[reconstruction_modulus = 1]]
 
 lemma bigo_pos_const: "(EX (c::'a::ordered_idom). 
     ALL x. (abs (h x)) <= (c * (abs (f x))))
@@ -100,6 +100,8 @@
   by (metis abs_le_iff 5 18 14)
 qed
 
+declare [[reconstruction_modulus = 2]]
+
 lemma (*bigo_pos_const:*) "(EX (c::'a::ordered_idom). 
     ALL x. (abs (h x)) <= (c * (abs (f x))))
       = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))"
@@ -107,7 +109,6 @@
   apply (case_tac "c = 0", simp)
   apply (rule_tac x = "1" in exI, simp)
   apply (rule_tac x = "abs c" in exI, auto);
-ML{*ResReconstruct.modulus:=2*}
 proof (neg_clausify)
 fix c x
 have 0: "\<And>(X1\<Colon>'a\<Colon>ordered_idom) X2\<Colon>'a\<Colon>ordered_idom. \<bar>X1 * X2\<bar> = \<bar>X2 * X1\<bar>"
@@ -140,6 +141,8 @@
   by (metis 8 abs_ge_zero abs_mult_pos abs_mult 1 9 3 abs_le_iff)
 qed
 
+declare [[reconstruction_modulus = 3]]
+
 lemma (*bigo_pos_const:*) "(EX (c::'a::ordered_idom). 
     ALL x. (abs (h x)) <= (c * (abs (f x))))
       = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))"
@@ -147,7 +150,6 @@
   apply (case_tac "c = 0", simp)
   apply (rule_tac x = "1" in exI, simp)
   apply (rule_tac x = "abs c" in exI, auto);
-ML{*ResReconstruct.modulus:=3*}
 proof (neg_clausify)
 fix c x
 assume 0: "\<And>x\<Colon>'b\<Colon>type.
@@ -171,7 +173,7 @@
 qed
 
 
-ML{*ResReconstruct.modulus:=1*}
+declare [[reconstruction_modulus = 1]]
 
 lemma (*bigo_pos_const:*) "(EX (c::'a::ordered_idom). 
     ALL x. (abs (h x)) <= (c * (abs (f x))))
@@ -207,8 +209,7 @@
 qed
 
 
-ML{*ResReconstruct.recon_sorts:=true*}
-
+declare [[reconstruction_sorts = true]]
 
 lemma bigo_alt_def: "O(f) = 
     {h. EX c. (0 < c & (ALL x. abs (h x) <= c * abs (f x)))}"
@@ -361,8 +362,8 @@
   apply (rule add_mono)
 ML{*ResAtp.problem_name := "BigO__bigo_plus_eq_simpler"*} 
 (*Found by SPASS; SLOW*)
-apply (metis le_maxI2 linorder_linear linorder_not_le min_max.less_eq_less_sup.sup_absorb1 mult_le_cancel_right xt1(6))
-apply (metis le_maxI2 linorder_not_le mult_le_cancel_right xt1(6))
+apply (metis le_maxI2 linorder_linear linorder_not_le min_max.less_eq_less_sup.sup_absorb1 mult_le_cancel_right order_trans)
+apply (metis le_maxI2 linorder_not_le mult_le_cancel_right order_trans)
 done
 
 ML{*ResAtp.problem_name := "BigO__bigo_bounded_alt"*}
@@ -429,7 +430,7 @@
 lemma "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==> f : O(g)" 
   apply (auto simp add: bigo_def)
   (*Version 1: one-shot proof*) 
-apply (metis Orderings.leD Orderings.leI abs_ge_self abs_le_D1 abs_mult abs_of_nonneg order_le_less xt1(12));
+  apply (metis Orderings.leD Orderings.leI abs_ge_self abs_le_D1 abs_mult abs_of_nonneg order_le_less)
   done
 
 text{*So here is the easier (and more natural) problem using transitivity*}
diff -r 43a1f08c5a29 -r 4cdf7de81e1b src/HOL/MetisExamples/Message.thy
--- a/src/HOL/MetisExamples/Message.thy	Wed Dec 19 16:52:26 2007 +0100
+++ b/src/HOL/MetisExamples/Message.thy	Wed Dec 19 17:40:48 2007 +0100
@@ -206,7 +206,7 @@
 ML{*ResAtp.problem_name := "Message__parts_insert_two"*}
 lemma parts_insert2:
      "parts (insert X (insert Y H)) = parts {X} \<union> parts {Y} \<union> parts H"
-by (metis Un_commute Un_empty_left Un_empty_right Un_insert_left Un_insert_right insert_commute parts_Un)
+by (metis Un_commute Un_empty_left Un_empty_right Un_insert_left Un_insert_right parts_Un)
 
 
 lemma parts_UN_subset1: "(\<Union>x\<in>A. parts(H x)) \<subseteq> parts(\<Union>x\<in>A. H x)"
@@ -244,7 +244,7 @@
 lemma parts_subset_iff [simp]: "(parts G \<subseteq> parts H) = (G \<subseteq> parts H)"
 apply (rule iffI) 
 apply (metis Un_absorb1 Un_subset_iff parts_Un parts_increasing)
-apply (metis parts_Un parts_idem parts_increasing parts_mono)
+apply (metis parts_idem parts_mono)
 done
 
 lemma parts_trans: "[| X\<in> parts G;  G \<subseteq> parts H |] ==> X\<in> parts H"
diff -r 43a1f08c5a29 -r 4cdf7de81e1b src/HOL/MetisExamples/Tarski.thy
--- a/src/HOL/MetisExamples/Tarski.thy	Wed Dec 19 16:52:26 2007 +0100
+++ b/src/HOL/MetisExamples/Tarski.thy	Wed Dec 19 17:40:48 2007 +0100
@@ -574,7 +574,7 @@
   qed
 qed
 
-lemma (in CLF) lubH_is_fixp:
+lemma (in CLF) (*lubH_is_fixp:*)
      "H = {x. (x, f x) \<in> r & x \<in> A} ==> lub H cl \<in> fix f A"
 apply (simp add: fix_def)
 apply (rule conjI)
diff -r 43a1f08c5a29 -r 4cdf7de81e1b src/HOL/MetisExamples/set.thy
--- a/src/HOL/MetisExamples/set.thy	Wed Dec 19 16:52:26 2007 +0100
+++ b/src/HOL/MetisExamples/set.thy	Wed Dec 19 17:40:48 2007 +0100
@@ -20,7 +20,7 @@
 lemma "P(n::nat) ==> ~P(0) ==> n ~= 0"
 by metis
 
-ML{*ResReconstruct.modulus := 1*}
+declare [[reconstruction_modulus = 1]]
 
 (*multiple versions of this example*)
 lemma (*equal_union: *)
@@ -90,8 +90,7 @@
   by (metis 31 29)
 qed
 
-
-ML{*ResReconstruct.modulus := 2*}
+declare [[reconstruction_modulus = 2]]
 
 lemma (*equal_union: *)
    "(X = Y \<union> Z) =
@@ -134,7 +133,7 @@
   by (metis 18 17)
 qed
 
-ML{*ResReconstruct.modulus := 3*}
+declare [[reconstruction_modulus = 3]]
 
 lemma (*equal_union: *)
    "(X = Y \<union> Z) =
@@ -169,7 +168,7 @@
 
 (*Example included in TPHOLs paper*)
 
-ML{*ResReconstruct.modulus := 4*}
+declare [[reconstruction_modulus = 4]]
 
 lemma (*equal_union: *)
    "(X = Y \<union> Z) =
diff -r 43a1f08c5a29 -r 4cdf7de81e1b src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Wed Dec 19 16:52:26 2007 +0100
+++ b/src/HOL/Tools/meson.ML	Wed Dec 19 17:40:48 2007 +0100
@@ -528,7 +528,7 @@
 fun skolemize_nnf_list [] = []
   | skolemize_nnf_list (th::ths) = 
       skolemize (make_nnf th) :: skolemize_nnf_list ths
-      handle THM _ =>
+      handle THM _ => (*RS can fail if Unify.search_bound is too small*)
        (warning ("Failed to Skolemize " ^ string_of_thm th);
         skolemize_nnf_list ths);
 
diff -r 43a1f08c5a29 -r 4cdf7de81e1b src/HOL/Tools/metis_tools.ML
--- a/src/HOL/Tools/metis_tools.ML	Wed Dec 19 16:52:26 2007 +0100
+++ b/src/HOL/Tools/metis_tools.ML	Wed Dec 19 17:40:48 2007 +0100
@@ -586,7 +586,7 @@
                 else Output.debug (fn () => "goal is higher-order")
         val _ = Output.debug (fn () => "START METIS PROVE PROCESS")
     in
-        case refute thms of
+        case NAMED_CRITICAL "refute" (fn () => refute thms) of
             Metis.Resolution.Contradiction mth =>
               let val _ = Output.debug (fn () => "METIS RECONSTRUCTION START: " ^
                             Metis.Thm.toString mth)
diff -r 43a1f08c5a29 -r 4cdf7de81e1b src/HOL/Tools/res_reconstruct.ML
--- a/src/HOL/Tools/res_reconstruct.ML	Wed Dec 19 16:52:26 2007 +0100
+++ b/src/HOL/Tools/res_reconstruct.ML	Wed Dec 19 17:40:48 2007 +0100
@@ -9,8 +9,6 @@
 signature RES_RECONSTRUCT =
 sig
   datatype atp = E | SPASS | Vampire
-  val modulus:     int ref
-  val recon_sorts: bool ref
   val chained_hint: string
   val checkEProofFound:
 	TextIO.instream * TextIO.outstream * Posix.Process.pid *
@@ -29,6 +27,7 @@
   val num_typargs: Context.theory -> string -> int
   val make_tvar: string -> typ
   val strip_prefix: string -> string -> string option
+  val setup: Context.theory -> Context.theory
 end;
 
 structure ResReconstruct : RES_RECONSTRUCT =
@@ -39,11 +38,15 @@
 fun trace s = if !Output.debugging then File.append (File.tmp_path trace_path) s
               else ();
 
-datatype atp = E | SPASS | Vampire;
+(*For generating structured proofs: keep every nth proof line*)
+val (modulus, modulus_setup) = Attrib.config_int "reconstruction_modulus" 1;
 
-val recon_sorts = ref true;
+(*Indicates whether to include sort information in generated proofs*)
+val (recon_sorts, recon_sorts_setup) = Attrib.config_bool "reconstruction_sorts" true;
 
-val modulus = ref 1;    (*keep every nth proof line*)
+val setup = modulus_setup #> recon_sorts_setup;
+
+datatype atp = E | SPASS | Vampire;
 
 (**** PARSING OF TSTP FORMAT ****)
 
@@ -358,7 +361,7 @@
             "\"\n  by (metis " ^ space_implode " " deps ^ ")\n"
       fun dolines [(lname, t, deps)] = [doline "show " (lname, t, deps)]
         | dolines ((lname, t, deps)::lines) = doline "have " (lname, t, deps) :: dolines lines
-  in setmp show_sorts (!recon_sorts) dolines end;
+  in setmp show_sorts (Config.get ctxt recon_sorts) dolines end;
 
 fun notequal t (_,t',_) = not (t aconv t');
 
@@ -408,13 +411,13 @@
   counts the number of proof lines processed so far.
   Deleted lines are replaced by their own dependencies. Note that the "add_nonnull_prfline"
   phase may delete some dependencies, hence this phase comes later.*)
-fun add_wanted_prfline ((lno, t, []), (nlines, lines)) =
+fun add_wanted_prfline ctxt ((lno, t, []), (nlines, lines)) =
       (nlines, (lno, t, []) :: lines)   (*conjecture clauses must be kept*)
-  | add_wanted_prfline ((lno, t, deps), (nlines, lines)) =
+  | add_wanted_prfline ctxt ((lno, t, deps), (nlines, lines)) =
       if eq_types t orelse not (null (term_tvars t)) orelse
          exists bad_free (term_frees t) orelse
          (not (null lines) andalso   (*final line can't be deleted for these reasons*)
-          (length deps < 2 orelse nlines mod !modulus <> 0))   
+          (length deps < 2 orelse nlines mod (Config.get ctxt modulus) <> 0))   
       then (nlines+1, map (replace_deps (lno, deps)) lines) (*Delete line*)
       else (nlines+1, (lno, t, deps) :: lines);
 
@@ -442,7 +445,7 @@
       val nonnull_lines =
               foldr add_nonnull_prfline []
                     (foldr add_prfline [] (decode_tstp_list ctxt tuples))
-      val (_,lines) = foldr add_wanted_prfline (0,[]) nonnull_lines
+      val (_,lines) = foldr (add_wanted_prfline ctxt) (0,[]) nonnull_lines
       val (ccls,fixes) = ResAxioms.neg_conjecture_clauses th sgno
       val ccls = map forall_intr_vars ccls
   in