renamed Sledgehammer option
authorblanchet
Tue Nov 06 15:15:33 2012 +0100 (2012-11-06)
changeset 500206b9611abcd4c
parent 50019 930a10e674ef
child 50021 d96a3f468203
renamed Sledgehammer option
NEWS
src/Doc/Sledgehammer/document/root.tex
src/HOL/Metis_Examples/Big_O.thy
src/HOL/Metis_Examples/Sets.thy
src/HOL/Metis_Examples/Trans_Closure.thy
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
     1.1 --- a/NEWS	Tue Nov 06 15:12:31 2012 +0100
     1.2 +++ b/NEWS	Tue Nov 06 15:15:33 2012 +0100
     1.3 @@ -227,7 +227,7 @@
     1.4    - Renamed "kill_provers" subcommand to "kill"
     1.5    - Renamed options:
     1.6        isar_proof ~> isar_proofs
     1.7 -      isar_shrink_factor ~> isar_shrinkage
     1.8 +      isar_shrink_factor ~> isar_shrink
     1.9        max_relevant ~> max_facts
    1.10        relevance_thresholds ~> fact_thresholds
    1.11  
     2.1 --- a/src/Doc/Sledgehammer/document/root.tex	Tue Nov 06 15:12:31 2012 +0100
     2.2 +++ b/src/Doc/Sledgehammer/document/root.tex	Tue Nov 06 15:15:33 2012 +0100
     2.3 @@ -369,7 +369,7 @@
     2.4  \item[\labelitemi] \textbf{\textit{isar\_proofs}} (\S\ref{output-format}) specifies
     2.5  that Isar proofs should be generated, instead of one-liner \textit{metis} or
     2.6  \textit{smt} proofs. The length of the Isar proofs can be controlled by setting
     2.7 -\textit{isar\_shrinkage} (\S\ref{output-format}).
     2.8 +\textit{isar\_shrink} (\S\ref{output-format}).
     2.9  
    2.10  \item[\labelitemi] \textbf{\textit{timeout}} (\S\ref{timeouts}) controls the
    2.11  provers' time limit. It is set to 30 seconds, but since Sledgehammer runs
    2.12 @@ -508,7 +508,7 @@
    2.13  is highly experimental. Work on a new implementation has begun. There is a large body of
    2.14  research into transforming resolution proofs into natural deduction proofs (such
    2.15  as Isar proofs), which we hope to leverage. In the meantime, a workaround is to
    2.16 -set the \textit{isar\_shrinkage} option (\S\ref{output-format}) to a larger
    2.17 +set the \textit{isar\_shrink} option (\S\ref{output-format}) to a larger
    2.18  value or to try several provers and keep the nicest-looking proof.
    2.19  
    2.20  \point{How can I tell whether a suggested proof is sound?}
    2.21 @@ -1299,7 +1299,7 @@
    2.22  fails; however, they are usually faster and sometimes more robust than
    2.23  \textit{metis} proofs.
    2.24  
    2.25 -\opdefault{isar\_shrinkage}{int}{\upshape 10}
    2.26 +\opdefault{isar\_shrink}{int}{\upshape 10}
    2.27  Specifies the granularity of the generated Isar proofs if \textit{isar\_proofs}
    2.28  is enabled. A value of $n$ indicates that each Isar proof step should correspond
    2.29  to a group of up to $n$ consecutive proof steps in the ATP proof.
     3.1 --- a/src/HOL/Metis_Examples/Big_O.thy	Tue Nov 06 15:12:31 2012 +0100
     3.2 +++ b/src/HOL/Metis_Examples/Big_O.thy	Tue Nov 06 15:15:33 2012 +0100
     3.3 @@ -29,7 +29,7 @@
     3.4  
     3.5  (*** Now various verions with an increasing shrink factor ***)
     3.6  
     3.7 -sledgehammer_params [isar_proofs, isar_shrinkage = 1]
     3.8 +sledgehammer_params [isar_proofs, isar_shrink = 1]
     3.9  
    3.10  lemma
    3.11    "(\<exists>c\<Colon>'a\<Colon>linordered_idom.
    3.12 @@ -60,7 +60,7 @@
    3.13    thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis F4)
    3.14  qed
    3.15  
    3.16 -sledgehammer_params [isar_proofs, isar_shrinkage = 2]
    3.17 +sledgehammer_params [isar_proofs, isar_shrink = 2]
    3.18  
    3.19  lemma
    3.20    "(\<exists>c\<Colon>'a\<Colon>linordered_idom.
    3.21 @@ -83,7 +83,7 @@
    3.22    thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis F2)
    3.23  qed
    3.24  
    3.25 -sledgehammer_params [isar_proofs, isar_shrinkage = 3]
    3.26 +sledgehammer_params [isar_proofs, isar_shrink = 3]
    3.27  
    3.28  lemma
    3.29    "(\<exists>c\<Colon>'a\<Colon>linordered_idom.
    3.30 @@ -103,7 +103,7 @@
    3.31    thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis A1 abs_ge_zero)
    3.32  qed
    3.33  
    3.34 -sledgehammer_params [isar_proofs, isar_shrinkage = 4]
    3.35 +sledgehammer_params [isar_proofs, isar_shrink = 4]
    3.36  
    3.37  lemma
    3.38    "(\<exists>c\<Colon>'a\<Colon>linordered_idom.
    3.39 @@ -123,7 +123,7 @@
    3.40    thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis abs_mult)
    3.41  qed
    3.42  
    3.43 -sledgehammer_params [isar_proofs, isar_shrinkage = 1]
    3.44 +sledgehammer_params [isar_proofs, isar_shrink = 1]
    3.45  
    3.46  lemma bigo_alt_def: "O(f) = {h. \<exists>c. (0 < c \<and> (\<forall>x. abs (h x) <= c * abs (f x)))}"
    3.47  by (auto simp add: bigo_def bigo_pos_const)
     4.1 --- a/src/HOL/Metis_Examples/Sets.thy	Tue Nov 06 15:12:31 2012 +0100
     4.2 +++ b/src/HOL/Metis_Examples/Sets.thy	Tue Nov 06 15:15:33 2012 +0100
     4.3 @@ -21,7 +21,7 @@
     4.4  lemma "P(n::nat) ==> ~P(0) ==> n ~= 0"
     4.5  by metis
     4.6  
     4.7 -sledgehammer_params [isar_proofs, isar_shrinkage = 1]
     4.8 +sledgehammer_params [isar_proofs, isar_shrink = 1]
     4.9  
    4.10  (*multiple versions of this example*)
    4.11  lemma (*equal_union: *)
    4.12 @@ -70,7 +70,7 @@
    4.13    ultimately show "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by metis
    4.14  qed
    4.15  
    4.16 -sledgehammer_params [isar_proofs, isar_shrinkage = 2]
    4.17 +sledgehammer_params [isar_proofs, isar_shrink = 2]
    4.18  
    4.19  lemma (*equal_union: *)
    4.20     "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
    4.21 @@ -107,7 +107,7 @@
    4.22    ultimately show "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by metis
    4.23  qed
    4.24  
    4.25 -sledgehammer_params [isar_proofs, isar_shrinkage = 3]
    4.26 +sledgehammer_params [isar_proofs, isar_shrink = 3]
    4.27  
    4.28  lemma (*equal_union: *)
    4.29     "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
    4.30 @@ -124,7 +124,7 @@
    4.31    ultimately show "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_commute Un_upper2)
    4.32  qed
    4.33  
    4.34 -sledgehammer_params [isar_proofs, isar_shrinkage = 4]
    4.35 +sledgehammer_params [isar_proofs, isar_shrink = 4]
    4.36  
    4.37  lemma (*equal_union: *)
    4.38     "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
    4.39 @@ -140,7 +140,7 @@
    4.40    ultimately show "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_subset_iff Un_upper2)
    4.41  qed
    4.42  
    4.43 -sledgehammer_params [isar_proofs, isar_shrinkage = 1]
    4.44 +sledgehammer_params [isar_proofs, isar_shrink = 1]
    4.45  
    4.46  lemma (*equal_union: *)
    4.47     "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
     5.1 --- a/src/HOL/Metis_Examples/Trans_Closure.thy	Tue Nov 06 15:12:31 2012 +0100
     5.2 +++ b/src/HOL/Metis_Examples/Trans_Closure.thy	Tue Nov 06 15:15:33 2012 +0100
     5.3 @@ -44,7 +44,7 @@
     5.4  
     5.5  lemma "\<lbrakk>f c = Intg x; \<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x; (a, b) \<in> R\<^sup>*; (b,c) \<in> R\<^sup>*\<rbrakk>
     5.6         \<Longrightarrow> \<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*"
     5.7 -(* sledgehammer [isar_proofs, isar_shrinkage = 2] *)
     5.8 +(* sledgehammer [isar_proofs, isar_shrink = 2] *)
     5.9  proof -
    5.10    assume A1: "f c = Intg x"
    5.11    assume A2: "\<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x"
     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Nov 06 15:12:31 2012 +0100
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Nov 06 15:15:33 2012 +0100
     6.3 @@ -95,7 +95,7 @@
     6.4     ("max_mono_iters", "smart"),
     6.5     ("max_new_mono_instances", "smart"),
     6.6     ("isar_proofs", "false"),
     6.7 -   ("isar_shrinkage", "10"),
     6.8 +   ("isar_shrink", "10"),
     6.9     ("slice", "true"),
    6.10     ("minimize", "smart"),
    6.11     ("preplay_timeout", "3")]
    6.12 @@ -119,7 +119,7 @@
    6.13  val params_for_minimize =
    6.14    ["debug", "verbose", "overlord", "type_enc", "strict", "lam_trans",
    6.15     "uncurried_aliases", "max_mono_iters", "max_new_mono_instances",
    6.16 -   "isar_proofs", "isar_shrinkage", "timeout", "preplay_timeout"]
    6.17 +   "isar_proofs", "isar_shrink", "timeout", "preplay_timeout"]
    6.18  
    6.19  val property_dependent_params = ["provers", "timeout"]
    6.20  
    6.21 @@ -316,7 +316,7 @@
    6.22      val max_new_mono_instances =
    6.23        lookup_option lookup_int "max_new_mono_instances"
    6.24      val isar_proofs = lookup_bool "isar_proofs"
    6.25 -    val isar_shrinkage = Real.max (1.0, lookup_real "isar_shrinkage")
    6.26 +    val isar_shrink = Real.max (1.0, lookup_real "isar_shrink")
    6.27      val slice = mode <> Auto_Try andalso lookup_bool "slice"
    6.28      val minimize =
    6.29        if mode = Auto_Try then NONE else lookup_option lookup_bool "minimize"
    6.30 @@ -333,7 +333,7 @@
    6.31       learn = learn, fact_filter = fact_filter, max_facts = max_facts,
    6.32       fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
    6.33       max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs,
    6.34 -     isar_shrinkage = isar_shrinkage, slice = slice, minimize = minimize,
    6.35 +     isar_shrink = isar_shrink, slice = slice, minimize = minimize,
    6.36       timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
    6.37    end
    6.38  
     7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Tue Nov 06 15:12:31 2012 +0100
     7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Tue Nov 06 15:15:33 2012 +0100
     7.3 @@ -54,7 +54,7 @@
     7.4  
     7.5  fun test_facts ({debug, verbose, overlord, provers, max_mono_iters,
     7.6                   max_new_mono_instances, type_enc, strict, lam_trans,
     7.7 -                 uncurried_aliases, isar_proofs, isar_shrinkage,
     7.8 +                 uncurried_aliases, isar_proofs, isar_shrink,
     7.9                   preplay_timeout, ...} : params)
    7.10                 silent (prover : prover) timeout i n state facts =
    7.11    let
    7.12 @@ -73,7 +73,7 @@
    7.13         learn = false, fact_filter = NONE, max_facts = SOME (length facts),
    7.14         fact_thresholds = (1.01, 1.01), max_mono_iters = max_mono_iters,
    7.15         max_new_mono_instances = max_new_mono_instances,
    7.16 -       isar_proofs = isar_proofs, isar_shrinkage = isar_shrinkage,
    7.17 +       isar_proofs = isar_proofs, isar_shrink = isar_shrink,
    7.18         slice = false, minimize = SOME false, timeout = timeout,
    7.19         preplay_timeout = preplay_timeout, expect = ""}
    7.20      val problem =
    7.21 @@ -237,7 +237,7 @@
    7.22          ({debug, verbose, overlord, blocking, provers, type_enc, strict,
    7.23           lam_trans, uncurried_aliases, learn, fact_filter, max_facts,
    7.24           fact_thresholds, max_mono_iters, max_new_mono_instances, isar_proofs,
    7.25 -         isar_shrinkage, slice, minimize, timeout, preplay_timeout, expect}
    7.26 +         isar_shrink, slice, minimize, timeout, preplay_timeout, expect}
    7.27           : params) =
    7.28    let
    7.29      fun lookup_override name default_value =
    7.30 @@ -255,7 +255,7 @@
    7.31       learn = learn, fact_filter = fact_filter, max_facts = max_facts,
    7.32       fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
    7.33       max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs,
    7.34 -     isar_shrinkage = isar_shrinkage, slice = slice, minimize = minimize,
    7.35 +     isar_shrink = isar_shrink, slice = slice, minimize = minimize,
    7.36       timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
    7.37    end
    7.38  
     8.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Nov 06 15:12:31 2012 +0100
     8.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Nov 06 15:15:33 2012 +0100
     8.3 @@ -34,7 +34,7 @@
     8.4       max_mono_iters : int option,
     8.5       max_new_mono_instances : int option,
     8.6       isar_proofs : bool,
     8.7 -     isar_shrinkage : real,
     8.8 +     isar_shrink : real,
     8.9       slice : bool,
    8.10       minimize : bool option,
    8.11       timeout : Time.time,
    8.12 @@ -327,7 +327,7 @@
    8.13     max_mono_iters : int option,
    8.14     max_new_mono_instances : int option,
    8.15     isar_proofs : bool,
    8.16 -   isar_shrinkage : real,
    8.17 +   isar_shrink : real,
    8.18     slice : bool,
    8.19     minimize : bool option,
    8.20     timeout : Time.time,
    8.21 @@ -642,7 +642,7 @@
    8.22            best_max_mono_iters, best_max_new_mono_instances, ...} : atp_config)
    8.23          (params as {debug, verbose, overlord, type_enc, strict, lam_trans,
    8.24                      uncurried_aliases, max_facts, max_mono_iters,
    8.25 -                    max_new_mono_instances, isar_proofs, isar_shrinkage,
    8.26 +                    max_new_mono_instances, isar_proofs, isar_shrink,
    8.27                      slice, timeout, preplay_timeout, ...})
    8.28          minimize_command
    8.29          ({state, goal, subgoal, subgoal_count, facts, ...} : prover_problem) =
    8.30 @@ -888,7 +888,7 @@
    8.31                    else
    8.32                      ()
    8.33                  val isar_params =
    8.34 -                  (debug, verbose, preplay_timeout, isar_shrinkage,
    8.35 +                  (debug, verbose, preplay_timeout, isar_shrink,
    8.36                     pool, fact_names, sym_tab, atp_proof, goal)
    8.37                  val one_line_params =
    8.38                    (preplay, proof_banner mode name, used_facts,
     9.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Tue Nov 06 15:12:31 2012 +0100
     9.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Tue Nov 06 15:15:33 2012 +0100
     9.3 @@ -748,8 +748,8 @@
     9.4    type key = label
     9.5    val ord = label_ord)
     9.6  
     9.7 -fun shrink_proof debug ctxt type_enc lam_trans preplay
     9.8 -                 preplay_timeout isar_shrinkage proof =
     9.9 +fun shrink_proof debug ctxt type_enc lam_trans preplay preplay_timeout
    9.10 +                 isar_shrink proof =
    9.11    let
    9.12      (* clean vector interface *)
    9.13      fun get i v = Vector.sub (v, i)
    9.14 @@ -770,7 +770,7 @@
    9.15      (* proof vector *)
    9.16      val proof_vect = proof |> map SOME |> Vector.fromList
    9.17      val n = Vector.length proof_vect
    9.18 -    val n_target = Real.fromInt n / isar_shrinkage |> Real.round
    9.19 +    val n_target = Real.fromInt n / isar_shrink |> Real.round
    9.20  
    9.21      (* table for mapping from label to proof position *)
    9.22      fun update_table (i, Prove (_, label, _, _)) =
    9.23 @@ -932,8 +932,8 @@
    9.24    * (string * stature) list vector * int Symtab.table * string proof * thm
    9.25  
    9.26  fun isar_proof_text ctxt isar_proofs
    9.27 -    (debug, verbose, preplay_timeout, isar_shrinkage,
    9.28 -     pool, fact_names, sym_tab, atp_proof, goal)
    9.29 +    (debug, verbose, preplay_timeout, isar_shrink, pool, fact_names, sym_tab,
    9.30 +     atp_proof, goal)
    9.31      (one_line_params as (_, _, _, _, subgoal, subgoal_count)) =
    9.32    let
    9.33      val (params, hyp_ts, concl_t) = strip_subgoal ctxt goal subgoal
    9.34 @@ -1030,8 +1030,7 @@
    9.35            |> map (do_inf true)
    9.36            |> append assms
    9.37            |> shrink_proof debug ctxt type_enc lam_trans preplay
    9.38 -                 preplay_timeout
    9.39 -                 (if isar_proofs then isar_shrinkage else 1000.0)
    9.40 +                 preplay_timeout (if isar_proofs then isar_shrink else 1000.0)
    9.41         (* ||> reorder_proof_to_minimize_jumps (* ? *) *)
    9.42            ||> chain_direct_proof
    9.43            ||> kill_useless_labels_in_proof