# HG changeset patch
# User blanchet
# Date 1352211333 -3600
# Node ID 6b9611abcd4ceb56059c5944599c2cf7832b85c8
# Parent  930a10e674ef485f79e2fbece646ca4995ff2b4d
renamed Sledgehammer option

diff -r 930a10e674ef -r 6b9611abcd4c NEWS
--- a/NEWS	Tue Nov 06 15:12:31 2012 +0100
+++ b/NEWS	Tue Nov 06 15:15:33 2012 +0100
@@ -227,7 +227,7 @@
   - Renamed "kill_provers" subcommand to "kill"
   - Renamed options:
       isar_proof ~> isar_proofs
-      isar_shrink_factor ~> isar_shrinkage
+      isar_shrink_factor ~> isar_shrink
       max_relevant ~> max_facts
       relevance_thresholds ~> fact_thresholds
 
diff -r 930a10e674ef -r 6b9611abcd4c src/Doc/Sledgehammer/document/root.tex
--- a/src/Doc/Sledgehammer/document/root.tex	Tue Nov 06 15:12:31 2012 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex	Tue Nov 06 15:15:33 2012 +0100
@@ -369,7 +369,7 @@
 \item[\labelitemi] \textbf{\textit{isar\_proofs}} (\S\ref{output-format}) specifies
 that Isar proofs should be generated, instead of one-liner \textit{metis} or
 \textit{smt} proofs. The length of the Isar proofs can be controlled by setting
-\textit{isar\_shrinkage} (\S\ref{output-format}).
+\textit{isar\_shrink} (\S\ref{output-format}).
 
 \item[\labelitemi] \textbf{\textit{timeout}} (\S\ref{timeouts}) controls the
 provers' time limit. It is set to 30 seconds, but since Sledgehammer runs
@@ -508,7 +508,7 @@
 is highly experimental. Work on a new implementation has begun. There is a large body of
 research into transforming resolution proofs into natural deduction proofs (such
 as Isar proofs), which we hope to leverage. In the meantime, a workaround is to
-set the \textit{isar\_shrinkage} option (\S\ref{output-format}) to a larger
+set the \textit{isar\_shrink} option (\S\ref{output-format}) to a larger
 value or to try several provers and keep the nicest-looking proof.
 
 \point{How can I tell whether a suggested proof is sound?}
@@ -1299,7 +1299,7 @@
 fails; however, they are usually faster and sometimes more robust than
 \textit{metis} proofs.
 
-\opdefault{isar\_shrinkage}{int}{\upshape 10}
+\opdefault{isar\_shrink}{int}{\upshape 10}
 Specifies the granularity of the generated Isar proofs if \textit{isar\_proofs}
 is enabled. A value of $n$ indicates that each Isar proof step should correspond
 to a group of up to $n$ consecutive proof steps in the ATP proof.
diff -r 930a10e674ef -r 6b9611abcd4c src/HOL/Metis_Examples/Big_O.thy
--- a/src/HOL/Metis_Examples/Big_O.thy	Tue Nov 06 15:12:31 2012 +0100
+++ b/src/HOL/Metis_Examples/Big_O.thy	Tue Nov 06 15:15:33 2012 +0100
@@ -29,7 +29,7 @@
 
 (*** Now various verions with an increasing shrink factor ***)
 
-sledgehammer_params [isar_proofs, isar_shrinkage = 1]
+sledgehammer_params [isar_proofs, isar_shrink = 1]
 
 lemma
   "(\<exists>c\<Colon>'a\<Colon>linordered_idom.
@@ -60,7 +60,7 @@
   thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis F4)
 qed
 
-sledgehammer_params [isar_proofs, isar_shrinkage = 2]
+sledgehammer_params [isar_proofs, isar_shrink = 2]
 
 lemma
   "(\<exists>c\<Colon>'a\<Colon>linordered_idom.
@@ -83,7 +83,7 @@
   thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis F2)
 qed
 
-sledgehammer_params [isar_proofs, isar_shrinkage = 3]
+sledgehammer_params [isar_proofs, isar_shrink = 3]
 
 lemma
   "(\<exists>c\<Colon>'a\<Colon>linordered_idom.
@@ -103,7 +103,7 @@
   thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis A1 abs_ge_zero)
 qed
 
-sledgehammer_params [isar_proofs, isar_shrinkage = 4]
+sledgehammer_params [isar_proofs, isar_shrink = 4]
 
 lemma
   "(\<exists>c\<Colon>'a\<Colon>linordered_idom.
@@ -123,7 +123,7 @@
   thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis abs_mult)
 qed
 
-sledgehammer_params [isar_proofs, isar_shrinkage = 1]
+sledgehammer_params [isar_proofs, isar_shrink = 1]
 
 lemma bigo_alt_def: "O(f) = {h. \<exists>c. (0 < c \<and> (\<forall>x. abs (h x) <= c * abs (f x)))}"
 by (auto simp add: bigo_def bigo_pos_const)
diff -r 930a10e674ef -r 6b9611abcd4c src/HOL/Metis_Examples/Sets.thy
--- a/src/HOL/Metis_Examples/Sets.thy	Tue Nov 06 15:12:31 2012 +0100
+++ b/src/HOL/Metis_Examples/Sets.thy	Tue Nov 06 15:15:33 2012 +0100
@@ -21,7 +21,7 @@
 lemma "P(n::nat) ==> ~P(0) ==> n ~= 0"
 by metis
 
-sledgehammer_params [isar_proofs, isar_shrinkage = 1]
+sledgehammer_params [isar_proofs, isar_shrink = 1]
 
 (*multiple versions of this example*)
 lemma (*equal_union: *)
@@ -70,7 +70,7 @@
   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
 qed
 
-sledgehammer_params [isar_proofs, isar_shrinkage = 2]
+sledgehammer_params [isar_proofs, isar_shrink = 2]
 
 lemma (*equal_union: *)
    "(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))"
@@ -107,7 +107,7 @@
   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
 qed
 
-sledgehammer_params [isar_proofs, isar_shrinkage = 3]
+sledgehammer_params [isar_proofs, isar_shrink = 3]
 
 lemma (*equal_union: *)
    "(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))"
@@ -124,7 +124,7 @@
   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)
 qed
 
-sledgehammer_params [isar_proofs, isar_shrinkage = 4]
+sledgehammer_params [isar_proofs, isar_shrink = 4]
 
 lemma (*equal_union: *)
    "(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))"
@@ -140,7 +140,7 @@
   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)
 qed
 
-sledgehammer_params [isar_proofs, isar_shrinkage = 1]
+sledgehammer_params [isar_proofs, isar_shrink = 1]
 
 lemma (*equal_union: *)
    "(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))"
diff -r 930a10e674ef -r 6b9611abcd4c src/HOL/Metis_Examples/Trans_Closure.thy
--- a/src/HOL/Metis_Examples/Trans_Closure.thy	Tue Nov 06 15:12:31 2012 +0100
+++ b/src/HOL/Metis_Examples/Trans_Closure.thy	Tue Nov 06 15:15:33 2012 +0100
@@ -44,7 +44,7 @@
 
 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>
        \<Longrightarrow> \<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*"
-(* sledgehammer [isar_proofs, isar_shrinkage = 2] *)
+(* sledgehammer [isar_proofs, isar_shrink = 2] *)
 proof -
   assume A1: "f c = Intg x"
   assume A2: "\<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x"
diff -r 930a10e674ef -r 6b9611abcd4c src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Nov 06 15:12:31 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Nov 06 15:15:33 2012 +0100
@@ -95,7 +95,7 @@
    ("max_mono_iters", "smart"),
    ("max_new_mono_instances", "smart"),
    ("isar_proofs", "false"),
-   ("isar_shrinkage", "10"),
+   ("isar_shrink", "10"),
    ("slice", "true"),
    ("minimize", "smart"),
    ("preplay_timeout", "3")]
@@ -119,7 +119,7 @@
 val params_for_minimize =
   ["debug", "verbose", "overlord", "type_enc", "strict", "lam_trans",
    "uncurried_aliases", "max_mono_iters", "max_new_mono_instances",
-   "isar_proofs", "isar_shrinkage", "timeout", "preplay_timeout"]
+   "isar_proofs", "isar_shrink", "timeout", "preplay_timeout"]
 
 val property_dependent_params = ["provers", "timeout"]
 
@@ -316,7 +316,7 @@
     val max_new_mono_instances =
       lookup_option lookup_int "max_new_mono_instances"
     val isar_proofs = lookup_bool "isar_proofs"
-    val isar_shrinkage = Real.max (1.0, lookup_real "isar_shrinkage")
+    val isar_shrink = Real.max (1.0, lookup_real "isar_shrink")
     val slice = mode <> Auto_Try andalso lookup_bool "slice"
     val minimize =
       if mode = Auto_Try then NONE else lookup_option lookup_bool "minimize"
@@ -333,7 +333,7 @@
      learn = learn, fact_filter = fact_filter, max_facts = max_facts,
      fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
      max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs,
-     isar_shrinkage = isar_shrinkage, slice = slice, minimize = minimize,
+     isar_shrink = isar_shrink, slice = slice, minimize = minimize,
      timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
   end
 
diff -r 930a10e674ef -r 6b9611abcd4c src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Tue Nov 06 15:12:31 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Tue Nov 06 15:15:33 2012 +0100
@@ -54,7 +54,7 @@
 
 fun test_facts ({debug, verbose, overlord, provers, max_mono_iters,
                  max_new_mono_instances, type_enc, strict, lam_trans,
-                 uncurried_aliases, isar_proofs, isar_shrinkage,
+                 uncurried_aliases, isar_proofs, isar_shrink,
                  preplay_timeout, ...} : params)
                silent (prover : prover) timeout i n state facts =
   let
@@ -73,7 +73,7 @@
        learn = false, fact_filter = NONE, max_facts = SOME (length facts),
        fact_thresholds = (1.01, 1.01), max_mono_iters = max_mono_iters,
        max_new_mono_instances = max_new_mono_instances,
-       isar_proofs = isar_proofs, isar_shrinkage = isar_shrinkage,
+       isar_proofs = isar_proofs, isar_shrink = isar_shrink,
        slice = false, minimize = SOME false, timeout = timeout,
        preplay_timeout = preplay_timeout, expect = ""}
     val problem =
@@ -237,7 +237,7 @@
         ({debug, verbose, overlord, blocking, provers, type_enc, strict,
          lam_trans, uncurried_aliases, learn, fact_filter, max_facts,
          fact_thresholds, max_mono_iters, max_new_mono_instances, isar_proofs,
-         isar_shrinkage, slice, minimize, timeout, preplay_timeout, expect}
+         isar_shrink, slice, minimize, timeout, preplay_timeout, expect}
          : params) =
   let
     fun lookup_override name default_value =
@@ -255,7 +255,7 @@
      learn = learn, fact_filter = fact_filter, max_facts = max_facts,
      fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
      max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs,
-     isar_shrinkage = isar_shrinkage, slice = slice, minimize = minimize,
+     isar_shrink = isar_shrink, slice = slice, minimize = minimize,
      timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
   end
 
diff -r 930a10e674ef -r 6b9611abcd4c src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Nov 06 15:12:31 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Nov 06 15:15:33 2012 +0100
@@ -34,7 +34,7 @@
      max_mono_iters : int option,
      max_new_mono_instances : int option,
      isar_proofs : bool,
-     isar_shrinkage : real,
+     isar_shrink : real,
      slice : bool,
      minimize : bool option,
      timeout : Time.time,
@@ -327,7 +327,7 @@
    max_mono_iters : int option,
    max_new_mono_instances : int option,
    isar_proofs : bool,
-   isar_shrinkage : real,
+   isar_shrink : real,
    slice : bool,
    minimize : bool option,
    timeout : Time.time,
@@ -642,7 +642,7 @@
           best_max_mono_iters, best_max_new_mono_instances, ...} : atp_config)
         (params as {debug, verbose, overlord, type_enc, strict, lam_trans,
                     uncurried_aliases, max_facts, max_mono_iters,
-                    max_new_mono_instances, isar_proofs, isar_shrinkage,
+                    max_new_mono_instances, isar_proofs, isar_shrink,
                     slice, timeout, preplay_timeout, ...})
         minimize_command
         ({state, goal, subgoal, subgoal_count, facts, ...} : prover_problem) =
@@ -888,7 +888,7 @@
                   else
                     ()
                 val isar_params =
-                  (debug, verbose, preplay_timeout, isar_shrinkage,
+                  (debug, verbose, preplay_timeout, isar_shrink,
                    pool, fact_names, sym_tab, atp_proof, goal)
                 val one_line_params =
                   (preplay, proof_banner mode name, used_facts,
diff -r 930a10e674ef -r 6b9611abcd4c src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Tue Nov 06 15:12:31 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Tue Nov 06 15:15:33 2012 +0100
@@ -748,8 +748,8 @@
   type key = label
   val ord = label_ord)
 
-fun shrink_proof debug ctxt type_enc lam_trans preplay
-                 preplay_timeout isar_shrinkage proof =
+fun shrink_proof debug ctxt type_enc lam_trans preplay preplay_timeout
+                 isar_shrink proof =
   let
     (* clean vector interface *)
     fun get i v = Vector.sub (v, i)
@@ -770,7 +770,7 @@
     (* proof vector *)
     val proof_vect = proof |> map SOME |> Vector.fromList
     val n = Vector.length proof_vect
-    val n_target = Real.fromInt n / isar_shrinkage |> Real.round
+    val n_target = Real.fromInt n / isar_shrink |> Real.round
 
     (* table for mapping from label to proof position *)
     fun update_table (i, Prove (_, label, _, _)) =
@@ -932,8 +932,8 @@
   * (string * stature) list vector * int Symtab.table * string proof * thm
 
 fun isar_proof_text ctxt isar_proofs
-    (debug, verbose, preplay_timeout, isar_shrinkage,
-     pool, fact_names, sym_tab, atp_proof, goal)
+    (debug, verbose, preplay_timeout, isar_shrink, pool, fact_names, sym_tab,
+     atp_proof, goal)
     (one_line_params as (_, _, _, _, subgoal, subgoal_count)) =
   let
     val (params, hyp_ts, concl_t) = strip_subgoal ctxt goal subgoal
@@ -1030,8 +1030,7 @@
           |> map (do_inf true)
           |> append assms
           |> shrink_proof debug ctxt type_enc lam_trans preplay
-                 preplay_timeout
-                 (if isar_proofs then isar_shrinkage else 1000.0)
+                 preplay_timeout (if isar_proofs then isar_shrink else 1000.0)
        (* ||> reorder_proof_to_minimize_jumps (* ? *) *)
           ||> chain_direct_proof
           ||> kill_useless_labels_in_proof