1.1 --- a/src/HOL/ATP_Linkup.thy	Wed Dec 19 16:52:26 2007 +0100
     1.2 +++ b/src/HOL/ATP_Linkup.thy	Wed Dec 19 17:40:48 2007 +0100
     1.3 @@ -109,6 +109,7 @@
     1.4  
     1.5  use "Tools/res_atp_methods.ML"
     1.6  setup ResAtpMethods.setup      --{*Oracle ATP methods: still useful?*}
     1.7 +setup ResReconstruct.setup     --{*Config parameters*}
     1.8  setup ResAxioms.setup          --{*Sledgehammer*}
     1.9  
    1.10  subsection {* The Metis prover *}

     2.1 --- a/src/HOL/MetisExamples/BigO.thy	Wed Dec 19 16:52:26 2007 +0100
     2.2 +++ b/src/HOL/MetisExamples/BigO.thy	Wed Dec 19 17:40:48 2007 +0100
     2.3 @@ -31,7 +31,7 @@
     2.4  
     2.5  (*** Now various verions with an increasing modulus ***)
     2.6  
     2.7 -ML{*ResReconstruct.modulus := 1*}
     2.8 +declare [[reconstruction_modulus = 1]]
     2.9  
    2.10  lemma bigo_pos_const: "(EX (c::'a::ordered_idom). 
    2.11      ALL x. (abs (h x)) <= (c * (abs (f x))))
    2.12 @@ -100,6 +100,8 @@
    2.13    by (metis abs_le_iff 5 18 14)
    2.14  qed
    2.15  
    2.16 +declare [[reconstruction_modulus = 2]]
    2.17 +
    2.18  lemma (*bigo_pos_const:*) "(EX (c::'a::ordered_idom). 
    2.19      ALL x. (abs (h x)) <= (c * (abs (f x))))
    2.20        = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))"
    2.21 @@ -107,7 +109,6 @@
    2.22    apply (case_tac "c = 0", simp)
    2.23    apply (rule_tac x = "1" in exI, simp)
    2.24    apply (rule_tac x = "abs c" in exI, auto);
    2.25 -ML{*ResReconstruct.modulus:=2*}
    2.26  proof (neg_clausify)
    2.27  fix c x
    2.28  have 0: "\<And>(X1\<Colon>'a\<Colon>ordered_idom) X2\<Colon>'a\<Colon>ordered_idom. \<bar>X1 * X2\<bar> = \<bar>X2 * X1\<bar>"
    2.29 @@ -140,6 +141,8 @@
    2.30    by (metis 8 abs_ge_zero abs_mult_pos abs_mult 1 9 3 abs_le_iff)
    2.31  qed
    2.32  
    2.33 +declare [[reconstruction_modulus = 3]]
    2.34 +
    2.35  lemma (*bigo_pos_const:*) "(EX (c::'a::ordered_idom). 
    2.36      ALL x. (abs (h x)) <= (c * (abs (f x))))
    2.37        = (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))"
    2.38 @@ -147,7 +150,6 @@
    2.39    apply (case_tac "c = 0", simp)
    2.40    apply (rule_tac x = "1" in exI, simp)
    2.41    apply (rule_tac x = "abs c" in exI, auto);
    2.42 -ML{*ResReconstruct.modulus:=3*}
    2.43  proof (neg_clausify)
    2.44  fix c x
    2.45  assume 0: "\<And>x\<Colon>'b\<Colon>type.
    2.46 @@ -171,7 +173,7 @@
    2.47  qed
    2.48  
    2.49  
    2.50 -ML{*ResReconstruct.modulus:=1*}
    2.51 +declare [[reconstruction_modulus = 1]]
    2.52  
    2.53  lemma (*bigo_pos_const:*) "(EX (c::'a::ordered_idom). 
    2.54      ALL x. (abs (h x)) <= (c * (abs (f x))))
    2.55 @@ -207,8 +209,7 @@
    2.56  qed
    2.57  
    2.58  
    2.59 -ML{*ResReconstruct.recon_sorts:=true*}
    2.60 -
    2.61 +declare [[reconstruction_sorts = true]]
    2.62  
    2.63  lemma bigo_alt_def: "O(f) = 
    2.64      {h. EX c. (0 < c & (ALL x. abs (h x) <= c * abs (f x)))}"
    2.65 @@ -361,8 +362,8 @@
    2.66    apply (rule add_mono)
    2.67  ML{*ResAtp.problem_name := "BigO__bigo_plus_eq_simpler"*} 
    2.68  (*Found by SPASS; SLOW*)
    2.69 -apply (metis le_maxI2 linorder_linear linorder_not_le min_max.less_eq_less_sup.sup_absorb1 mult_le_cancel_right xt1(6))
    2.70 -apply (metis le_maxI2 linorder_not_le mult_le_cancel_right xt1(6))
    2.71 +apply (metis le_maxI2 linorder_linear linorder_not_le min_max.less_eq_less_sup.sup_absorb1 mult_le_cancel_right order_trans)
    2.72 +apply (metis le_maxI2 linorder_not_le mult_le_cancel_right order_trans)
    2.73  done
    2.74  
    2.75  ML{*ResAtp.problem_name := "BigO__bigo_bounded_alt"*}
    2.76 @@ -429,7 +430,7 @@
    2.77  lemma "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==> f : O(g)" 
    2.78    apply (auto simp add: bigo_def)
    2.79    (*Version 1: one-shot proof*) 
    2.80 -apply (metis Orderings.leD Orderings.leI abs_ge_self abs_le_D1 abs_mult abs_of_nonneg order_le_less xt1(12));
    2.81 +  apply (metis Orderings.leD Orderings.leI abs_ge_self abs_le_D1 abs_mult abs_of_nonneg order_le_less)
    2.82    done
    2.83  
    2.84  text{*So here is the easier (and more natural) problem using transitivity*}

     3.1 --- a/src/HOL/MetisExamples/Message.thy	Wed Dec 19 16:52:26 2007 +0100
     3.2 +++ b/src/HOL/MetisExamples/Message.thy	Wed Dec 19 17:40:48 2007 +0100
     3.3 @@ -206,7 +206,7 @@
     3.4  ML{*ResAtp.problem_name := "Message__parts_insert_two"*}
     3.5  lemma parts_insert2:
     3.6       "parts (insert X (insert Y H)) = parts {X} \<union> parts {Y} \<union> parts H"
     3.7 -by (metis Un_commute Un_empty_left Un_empty_right Un_insert_left Un_insert_right insert_commute parts_Un)
     3.8 +by (metis Un_commute Un_empty_left Un_empty_right Un_insert_left Un_insert_right parts_Un)
     3.9  
    3.10  
    3.11  lemma parts_UN_subset1: "(\<Union>x\<in>A. parts(H x)) \<subseteq> parts(\<Union>x\<in>A. H x)"
    3.12 @@ -244,7 +244,7 @@
    3.13  lemma parts_subset_iff [simp]: "(parts G \<subseteq> parts H) = (G \<subseteq> parts H)"
    3.14  apply (rule iffI) 
    3.15  apply (metis Un_absorb1 Un_subset_iff parts_Un parts_increasing)
    3.16 -apply (metis parts_Un parts_idem parts_increasing parts_mono)
    3.17 +apply (metis parts_idem parts_mono)
    3.18  done
    3.19  
    3.20  lemma parts_trans: "[| X\<in> parts G;  G \<subseteq> parts H |] ==> X\<in> parts H"

     4.1 --- a/src/HOL/MetisExamples/Tarski.thy	Wed Dec 19 16:52:26 2007 +0100
     4.2 +++ b/src/HOL/MetisExamples/Tarski.thy	Wed Dec 19 17:40:48 2007 +0100
     4.3 @@ -574,7 +574,7 @@
     4.4    qed
     4.5  qed
     4.6  
     4.7 -lemma (in CLF) lubH_is_fixp:
     4.8 +lemma (in CLF) (*lubH_is_fixp:*)
     4.9       "H = {x. (x, f x) \<in> r & x \<in> A} ==> lub H cl \<in> fix f A"
    4.10  apply (simp add: fix_def)
    4.11  apply (rule conjI)

     5.1 --- a/src/HOL/MetisExamples/set.thy	Wed Dec 19 16:52:26 2007 +0100
     5.2 +++ b/src/HOL/MetisExamples/set.thy	Wed Dec 19 17:40:48 2007 +0100
     5.3 @@ -20,7 +20,7 @@
     5.4  lemma "P(n::nat) ==> ~P(0) ==> n ~= 0"
     5.5  by metis
     5.6  
     5.7 -ML{*ResReconstruct.modulus := 1*}
     5.8 +declare [[reconstruction_modulus = 1]]
     5.9  
    5.10  (*multiple versions of this example*)
    5.11  lemma (*equal_union: *)
    5.12 @@ -90,8 +90,7 @@
    5.13    by (metis 31 29)
    5.14  qed
    5.15  
    5.16 -
    5.17 -ML{*ResReconstruct.modulus := 2*}
    5.18 +declare [[reconstruction_modulus = 2]]
    5.19  
    5.20  lemma (*equal_union: *)
    5.21     "(X = Y \<union> Z) =
    5.22 @@ -134,7 +133,7 @@
    5.23    by (metis 18 17)
    5.24  qed
    5.25  
    5.26 -ML{*ResReconstruct.modulus := 3*}
    5.27 +declare [[reconstruction_modulus = 3]]
    5.28  
    5.29  lemma (*equal_union: *)
    5.30     "(X = Y \<union> Z) =
    5.31 @@ -169,7 +168,7 @@
    5.32  
    5.33  (*Example included in TPHOLs paper*)
    5.34  
    5.35 -ML{*ResReconstruct.modulus := 4*}
    5.36 +declare [[reconstruction_modulus = 4]]
    5.37  
    5.38  lemma (*equal_union: *)
    5.39     "(X = Y \<union> Z) =

     6.1 --- a/src/HOL/Tools/meson.ML	Wed Dec 19 16:52:26 2007 +0100
     6.2 +++ b/src/HOL/Tools/meson.ML	Wed Dec 19 17:40:48 2007 +0100
     6.3 @@ -528,7 +528,7 @@
     6.4  fun skolemize_nnf_list [] = []
     6.5    | skolemize_nnf_list (th::ths) = 
     6.6        skolemize (make_nnf th) :: skolemize_nnf_list ths
     6.7 -      handle THM _ =>
     6.8 +      handle THM _ => (*RS can fail if Unify.search_bound is too small*)
     6.9         (warning ("Failed to Skolemize " ^ string_of_thm th);
    6.10          skolemize_nnf_list ths);
    6.11  

     7.1 --- a/src/HOL/Tools/metis_tools.ML	Wed Dec 19 16:52:26 2007 +0100
     7.2 +++ b/src/HOL/Tools/metis_tools.ML	Wed Dec 19 17:40:48 2007 +0100
     7.3 @@ -586,7 +586,7 @@
     7.4                  else Output.debug (fn () => "goal is higher-order")
     7.5          val _ = Output.debug (fn () => "START METIS PROVE PROCESS")
     7.6      in
     7.7 -        case refute thms of
     7.8 +        case NAMED_CRITICAL "refute" (fn () => refute thms) of
     7.9              Metis.Resolution.Contradiction mth =>
    7.10                let val _ = Output.debug (fn () => "METIS RECONSTRUCTION START: " ^
    7.11                              Metis.Thm.toString mth)

     8.1 --- a/src/HOL/Tools/res_reconstruct.ML	Wed Dec 19 16:52:26 2007 +0100
     8.2 +++ b/src/HOL/Tools/res_reconstruct.ML	Wed Dec 19 17:40:48 2007 +0100
     8.3 @@ -9,8 +9,6 @@
     8.4  signature RES_RECONSTRUCT =
     8.5  sig
     8.6    datatype atp = E | SPASS | Vampire
     8.7 -  val modulus:     int ref
     8.8 -  val recon_sorts: bool ref
     8.9    val chained_hint: string
    8.10    val checkEProofFound:
    8.11  	TextIO.instream * TextIO.outstream * Posix.Process.pid *
    8.12 @@ -29,6 +27,7 @@
    8.13    val num_typargs: Context.theory -> string -> int
    8.14    val make_tvar: string -> typ
    8.15    val strip_prefix: string -> string -> string option
    8.16 +  val setup: Context.theory -> Context.theory
    8.17  end;
    8.18  
    8.19  structure ResReconstruct : RES_RECONSTRUCT =
    8.20 @@ -39,12 +38,16 @@
    8.21  fun trace s = if !Output.debugging then File.append (File.tmp_path trace_path) s
    8.22                else ();
    8.23  
    8.24 +(*For generating structured proofs: keep every nth proof line*)
    8.25 +val (modulus, modulus_setup) = Attrib.config_int "reconstruction_modulus" 1;
    8.26 +
    8.27 +(*Indicates whether to include sort information in generated proofs*)
    8.28 +val (recon_sorts, recon_sorts_setup) = Attrib.config_bool "reconstruction_sorts" true;
    8.29 +
    8.30 +val setup = modulus_setup #> recon_sorts_setup;
    8.31 +
    8.32  datatype atp = E | SPASS | Vampire;
    8.33  
    8.34 -val recon_sorts = ref true;
    8.35 -
    8.36 -val modulus = ref 1;    (*keep every nth proof line*)
    8.37 -
    8.38  (**** PARSING OF TSTP FORMAT ****)
    8.39  
    8.40  (*Syntax trees, either termlist or formulae*)
    8.41 @@ -358,7 +361,7 @@
    8.42              "\"\n  by (metis " ^ space_implode " " deps ^ ")\n"
    8.43        fun dolines [(lname, t, deps)] = [doline "show " (lname, t, deps)]
    8.44          | dolines ((lname, t, deps)::lines) = doline "have " (lname, t, deps) :: dolines lines
    8.45 -  in setmp show_sorts (!recon_sorts) dolines end;
    8.46 +  in setmp show_sorts (Config.get ctxt recon_sorts) dolines end;
    8.47  
    8.48  fun notequal t (_,t',_) = not (t aconv t');
    8.49  
    8.50 @@ -408,13 +411,13 @@
    8.51    counts the number of proof lines processed so far.
    8.52    Deleted lines are replaced by their own dependencies. Note that the "add_nonnull_prfline"
    8.53    phase may delete some dependencies, hence this phase comes later.*)
    8.54 -fun add_wanted_prfline ((lno, t, []), (nlines, lines)) =
    8.55 +fun add_wanted_prfline ctxt ((lno, t, []), (nlines, lines)) =
    8.56        (nlines, (lno, t, []) :: lines)   (*conjecture clauses must be kept*)
    8.57 -  | add_wanted_prfline ((lno, t, deps), (nlines, lines)) =
    8.58 +  | add_wanted_prfline ctxt ((lno, t, deps), (nlines, lines)) =
    8.59        if eq_types t orelse not (null (term_tvars t)) orelse
    8.60           exists bad_free (term_frees t) orelse
    8.61           (not (null lines) andalso   (*final line can't be deleted for these reasons*)
    8.62 -          (length deps < 2 orelse nlines mod !modulus <> 0))   
    8.63 +          (length deps < 2 orelse nlines mod (Config.get ctxt modulus) <> 0))   
    8.64        then (nlines+1, map (replace_deps (lno, deps)) lines) (*Delete line*)
    8.65        else (nlines+1, (lno, t, deps) :: lines);
    8.66  
    8.67 @@ -442,7 +445,7 @@
    8.68        val nonnull_lines =
    8.69                foldr add_nonnull_prfline []
    8.70                      (foldr add_prfline [] (decode_tstp_list ctxt tuples))
    8.71 -      val (_,lines) = foldr add_wanted_prfline (0,[]) nonnull_lines
    8.72 +      val (_,lines) = foldr (add_wanted_prfline ctxt) (0,[]) nonnull_lines
    8.73        val (ccls,fixes) = ResAxioms.neg_conjecture_clauses th sgno
    8.74        val ccls = map forall_intr_vars ccls
    8.75    in