1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jul 12 21:14:54 2013 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jul 12 22:41:25 2013 +0200
     1.3 @@ -102,6 +102,8 @@
     1.4     ("isar_compress", "10"),
     1.5     ("isar_compress_degree", "2"), (* TODO: document; right value?? *)
     1.6     ("merge_timeout_slack", "1.2"), (* TODO: document *)
     1.7 +   ("isar_try0", "true"), (* TODO: document *)
     1.8 +   ("isar_minimize", "true"), (* TODO: document *)
     1.9     ("slice", "true"),
    1.10     ("minimize", "smart"),
    1.11     ("preplay_timeout", "3"),
    1.12 @@ -123,13 +125,16 @@
    1.13     ("no_isar_proofs", "isar_proofs"),
    1.14     ("dont_slice", "slice"),
    1.15     ("dont_minimize", "minimize"),
    1.16 +   ("dont_try0_isar", "isar_try0"),
    1.17 +   ("dont_minimize_isar", "isar_minimize"),
    1.18     ("no_preplay_trace", "preplay_trace")] (* TODO: document *)
    1.19  
    1.20  val params_for_minimize =
    1.21    ["debug", "verbose", "overlord", "type_enc", "strict", "lam_trans",
    1.22     "uncurried_aliases", "max_mono_iters", "max_new_mono_instances",
    1.23     "learn", "isar_proofs", "isar_compress", "timeout", "preplay_timeout"]
    1.24 -(* TODO: add isar_compress_degree, merge_timeout_slack,  preplay_trace? *)
    1.25 +(* TODO: add isar_compress_degree, merge_timeout_slack,  preplay_trace,
    1.26 +   isar_try0, isar_minimize? *)
    1.27  
    1.28  val property_dependent_params = ["provers", "timeout"]
    1.29  
    1.30 @@ -313,6 +318,8 @@
    1.31      val isar_compress = Real.max (1.0, lookup_real "isar_compress")
    1.32      val isar_compress_degree = Int.max (1, lookup_int "isar_compress_degree")
    1.33      val merge_timeout_slack = Real.max (1.0, lookup_real "merge_timeout_slack")
    1.34 +    val isar_try0 = lookup_bool "isar_try0"
    1.35 +    val isar_minimize = lookup_bool "isar_minimize"
    1.36      val slice = mode <> Auto_Try andalso lookup_bool "slice"
    1.37      val minimize =
    1.38        if mode = Auto_Try then NONE else lookup_option lookup_bool "minimize"
    1.39 @@ -330,7 +337,8 @@
    1.40       fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
    1.41       max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs,
    1.42       isar_compress = isar_compress, isar_compress_degree = isar_compress_degree,
    1.43 -     merge_timeout_slack = merge_timeout_slack, slice = slice,
    1.44 +     merge_timeout_slack = merge_timeout_slack, isar_try0 = isar_try0,
    1.45 +     isar_minimize = isar_minimize, slice = slice,
    1.46       minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout,
    1.47       preplay_trace = preplay_trace, expect = expect}
    1.48    end

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Fri Jul 12 21:14:54 2013 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Fri Jul 12 22:41:25 2013 +0200
     2.3 @@ -59,6 +59,7 @@
     2.4                   max_new_mono_instances, type_enc, strict, lam_trans,
     2.5                   uncurried_aliases, isar_proofs, isar_compress,
     2.6                   isar_compress_degree, merge_timeout_slack,
     2.7 +                 isar_try0, isar_minimize,
     2.8                   preplay_timeout, preplay_trace, ...} : params)
     2.9                 silent (prover : prover) timeout i n state facts =
    2.10    let
    2.11 @@ -83,6 +84,7 @@
    2.12         isar_proofs = isar_proofs, isar_compress = isar_compress,
    2.13         isar_compress_degree = isar_compress_degree,
    2.14         merge_timeout_slack = merge_timeout_slack,
    2.15 +       isar_try0 = isar_try0, isar_minimize = isar_minimize,
    2.16         slice = false, minimize = SOME false, timeout = timeout,
    2.17         preplay_timeout = preplay_timeout, preplay_trace = preplay_trace,
    2.18         expect = ""}
    2.19 @@ -255,7 +257,8 @@
    2.20          ({debug, verbose, overlord, blocking, provers, type_enc, strict,
    2.21           lam_trans, uncurried_aliases, learn, fact_filter, max_facts,
    2.22           fact_thresholds, max_mono_iters, max_new_mono_instances, isar_proofs,
    2.23 -         isar_compress, isar_compress_degree, merge_timeout_slack, slice,
    2.24 +         isar_compress, isar_compress_degree, merge_timeout_slack, isar_try0,
    2.25 +         isar_minimize, slice,
    2.26           minimize, timeout, preplay_timeout, preplay_trace, expect} : params) =
    2.27    let
    2.28      fun lookup_override name default_value =
    2.29 @@ -274,7 +277,8 @@
    2.30       fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
    2.31       max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs,
    2.32       isar_compress = isar_compress, isar_compress_degree = isar_compress_degree,
    2.33 -     merge_timeout_slack = merge_timeout_slack, slice = slice,
    2.34 +     merge_timeout_slack = merge_timeout_slack,
    2.35 +     isar_try0 = isar_try0, isar_minimize = isar_minimize, slice = slice,
    2.36       minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout,
    2.37       preplay_trace = preplay_trace, expect = expect}
    2.38    end

     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML	Fri Jul 12 21:14:54 2013 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML	Fri Jul 12 22:41:25 2013 +0200
     3.3 @@ -10,7 +10,7 @@
     3.4    type preplay_interface = Sledgehammer_Preplay.preplay_interface
     3.5    type isar_proof = Sledgehammer_Proof.isar_proof
     3.6    val minimize_dependencies_and_remove_unrefed_steps :
     3.7 -    preplay_interface -> isar_proof -> isar_proof
     3.8 +    bool -> preplay_interface -> isar_proof -> isar_proof
     3.9  end
    3.10  
    3.11  
    3.12 @@ -50,7 +50,8 @@
    3.13        mk_step_lfs_gfs min_lfs min_gfs
    3.14      end)
    3.15  
    3.16 -fun minimize_dependencies_and_remove_unrefed_steps preplay_interface proof =
    3.17 +fun minimize_dependencies_and_remove_unrefed_steps
    3.18 +  isar_minimize preplay_interface proof =
    3.19    let
    3.20      fun cons_to xs x = x :: xs
    3.21  
    3.22 @@ -85,7 +86,8 @@
    3.23              (refed, accu)
    3.24  
    3.25      and do_refed_step step =
    3.26 -      min_deps_of_step preplay_interface step
    3.27 +      step
    3.28 +      |> isar_minimize ? min_deps_of_step preplay_interface
    3.29        |> do_refed_step'
    3.30  
    3.31      and do_refed_step' (Let _) = raise Fail "Sledgehammer_Minimize_Isar"

     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri Jul 12 21:14:54 2013 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri Jul 12 22:41:25 2013 +0200
     4.3 @@ -38,6 +38,8 @@
     4.4       isar_compress : real,
     4.5       isar_compress_degree : int,
     4.6       merge_timeout_slack : real,
     4.7 +     isar_try0 : bool,
     4.8 +     isar_minimize : bool,
     4.9       slice : bool,
    4.10       minimize : bool option,
    4.11       timeout : Time.time option,
    4.12 @@ -351,6 +353,8 @@
    4.13     isar_compress : real,
    4.14     isar_compress_degree : int,
    4.15     merge_timeout_slack : real,
    4.16 +   isar_try0 : bool,
    4.17 +   isar_minimize : bool,
    4.18     slice : bool,
    4.19     minimize : bool option,
    4.20     timeout : Time.time option,
    4.21 @@ -684,6 +688,7 @@
    4.22                      uncurried_aliases, fact_filter, max_facts, max_mono_iters,
    4.23                      max_new_mono_instances, isar_proofs, isar_compress,
    4.24                      isar_compress_degree, merge_timeout_slack,
    4.25 +                    isar_try0, isar_minimize,
    4.26                      slice, timeout, preplay_timeout, preplay_trace, ...})
    4.27          minimize_command
    4.28          ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
    4.29 @@ -959,6 +964,7 @@
    4.30                  val isar_params =
    4.31                    (debug, verbose, preplay_timeout, preplay_trace, isar_compress,
    4.32                     isar_compress_degree, merge_timeout_slack,
    4.33 +                   isar_try0,isar_minimize,
    4.34                     pool, fact_names, lifted, sym_tab, atp_proof, goal)
    4.35                  val one_line_params =
    4.36                    (preplay, proof_banner mode name, used_facts,

     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Fri Jul 12 21:14:54 2013 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Fri Jul 12 22:41:25 2013 +0200
     5.3 @@ -12,7 +12,7 @@
     5.4    type one_line_params = Sledgehammer_Print.one_line_params
     5.5  
     5.6    type isar_params =
     5.7 -    bool * bool * Time.time option * bool * real * int * real
     5.8 +    bool * bool * Time.time option * bool * real * int * real * bool * bool
     5.9      * string Symtab.table * (string * stature) list vector
    5.10      * (string * term) list * int Symtab.table * string proof * thm
    5.11  
    5.12 @@ -409,14 +409,14 @@
    5.13    in chain_proof end
    5.14  
    5.15  type isar_params =
    5.16 -  bool * bool * Time.time option * bool * real * int * real
    5.17 +  bool * bool * Time.time option * bool * real * int * real * bool * bool
    5.18    * string Symtab.table * (string * stature) list vector
    5.19    * (string * term) list * int Symtab.table * string proof * thm
    5.20  
    5.21  fun isar_proof_text ctxt isar_proofs
    5.22      (debug, verbose, preplay_timeout, preplay_trace, isar_compress,
    5.23 -     isar_compress_degree, merge_timeout_slack, pool, fact_names, lifted,
    5.24 -     sym_tab, atp_proof, goal)
    5.25 +     isar_compress_degree, merge_timeout_slack, isar_try0, isar_minimize, pool,
    5.26 +     fact_names, lifted, sym_tab, atp_proof, goal)
    5.27      (one_line_params as (_, _, _, _, subgoal, subgoal_count)) =
    5.28    let
    5.29      val (params, hyp_ts, concl_t) = strip_subgoal goal subgoal ctxt
    5.30 @@ -594,8 +594,9 @@
    5.31                 (if isar_proofs = SOME true then isar_compress else 1000.0)
    5.32                 (if isar_proofs = SOME true then isar_compress_degree else 100)
    5.33                 merge_timeout_slack preplay_interface
    5.34 -          |> try0 preplay_timeout preplay_interface
    5.35 -          |> minimize_dependencies_and_remove_unrefed_steps preplay_interface
    5.36 +          |> isar_try0 ? try0 preplay_timeout preplay_interface
    5.37 +          |> minimize_dependencies_and_remove_unrefed_steps isar_minimize
    5.38 +               preplay_interface
    5.39            |> `overall_preplay_stats
    5.40            ||> clean_up_labels_in_proof
    5.41          val isar_text = string_of_proof ctxt type_enc lam_trans subgoal