1.1 --- a/NEWS	Thu Dec 01 13:34:12 2011 +0100
     1.2 +++ b/NEWS	Thu Dec 01 13:34:13 2011 +0100
     1.3 @@ -148,6 +148,7 @@
     1.4  
     1.5  * Sledgehammer:
     1.6    - Added "lam_trans" option.
     1.7 +  - Renamed "slicing" ("no_slicing") option to "slice" ("dont_slice").
     1.8  
     1.9  * Metis:
    1.10    - Added possibility to specify lambda translations scheme as a

     2.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Dec 01 13:34:12 2011 +0100
     2.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Dec 01 13:34:13 2011 +0100
     2.3 @@ -10,7 +10,7 @@
     2.4  val keepK = "keep"
     2.5  val type_encK = "type_enc"
     2.6  val soundK = "sound"
     2.7 -val slicingK = "slicing"
     2.8 +val sliceK = "slice"
     2.9  val lam_transK = "lam_trans"
    2.10  val e_weight_methodK = "e_weight_method"
    2.11  val force_sosK = "force_sos"
    2.12 @@ -361,7 +361,7 @@
    2.13    SH_FAIL of int * int |
    2.14    SH_ERROR
    2.15  
    2.16 -fun run_sh prover_name prover type_enc sound max_relevant slicing lam_trans
    2.17 +fun run_sh prover_name prover type_enc sound max_relevant slice lam_trans
    2.18          e_weight_method force_sos hard_timeout timeout dir pos st =
    2.19    let
    2.20      val {context = ctxt, facts = chained_ths, goal} = Proof.goal st
    2.21 @@ -381,7 +381,7 @@
    2.22                         e_weight_method |> the_default I)
    2.23                   #> (Option.map (Config.put ATP_Systems.force_sos)
    2.24                         force_sos |> the_default I))
    2.25 -    val params as {relevance_thresholds, max_relevant, slicing, ...} =
    2.26 +    val params as {relevance_thresholds, max_relevant, slice, ...} =
    2.27        Sledgehammer_Isar.default_params ctxt
    2.28            [("verbose", "true"),
    2.29             ("type_enc", type_enc),
    2.30 @@ -389,11 +389,11 @@
    2.31             ("lam_trans", lam_trans |> the_default "smart"),
    2.32             ("preplay_timeout", preplay_timeout),
    2.33             ("max_relevant", max_relevant),
    2.34 -           ("slicing", slicing),
    2.35 +           ("slice", slice),
    2.36             ("timeout", string_of_int timeout),
    2.37             ("preplay_timeout", preplay_timeout)]
    2.38      val default_max_relevant =
    2.39 -      Sledgehammer_Provers.default_max_relevant_for_prover ctxt slicing
    2.40 +      Sledgehammer_Provers.default_max_relevant_for_prover ctxt slice
    2.41          prover_name
    2.42      val is_appropriate_prop =
    2.43        Sledgehammer_Provers.is_appropriate_prop_for_prover ctxt prover_name
    2.44 @@ -469,7 +469,7 @@
    2.45      val type_enc = AList.lookup (op =) args type_encK |> the_default "smart"
    2.46      val sound = AList.lookup (op =) args soundK |> the_default "false"
    2.47      val max_relevant = AList.lookup (op =) args max_relevantK |> the_default "smart"
    2.48 -    val slicing = AList.lookup (op =) args slicingK |> the_default "true"
    2.49 +    val slice = AList.lookup (op =) args sliceK |> the_default "true"
    2.50      val lam_trans = AList.lookup (op =) args lam_transK
    2.51      val e_weight_method = AList.lookup (op =) args e_weight_methodK
    2.52      val force_sos = AList.lookup (op =) args force_sosK
    2.53 @@ -480,7 +480,7 @@
    2.54         minimizer has a chance to do its magic *)
    2.55      val hard_timeout = SOME (2 * timeout)
    2.56      val (msg, result) =
    2.57 -      run_sh prover_name prover type_enc sound max_relevant slicing lam_trans
    2.58 +      run_sh prover_name prover type_enc sound max_relevant slice lam_trans
    2.59          e_weight_method force_sos hard_timeout timeout dir pos st
    2.60    in
    2.61      case result of
    2.62 @@ -555,7 +555,7 @@
    2.63     ("max_relevant", "0"),
    2.64     ("type_enc", type_enc),
    2.65     ("sound", "true"),
    2.66 -   ("slicing", "false"),
    2.67 +   ("slice", "false"),
    2.68     ("timeout", timeout |> Time.toSeconds |> string_of_int)]
    2.69  
    2.70  fun run_reconstructor trivial full m name reconstructor named_thms id

     3.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Thu Dec 01 13:34:12 2011 +0100
     3.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Thu Dec 01 13:34:13 2011 +0100
     3.3 @@ -113,10 +113,10 @@
     3.4           val {context = ctxt, facts = chained_ths, goal} = Proof.goal pre
     3.5           val prover = AList.lookup (op =) args "prover"
     3.6                        |> the_default default_prover
     3.7 -         val {relevance_thresholds, max_relevant, slicing, ...} =
     3.8 +         val {relevance_thresholds, max_relevant, slice, ...} =
     3.9             Sledgehammer_Isar.default_params ctxt args
    3.10           val default_max_relevant =
    3.11 -           Sledgehammer_Provers.default_max_relevant_for_prover ctxt slicing
    3.12 +           Sledgehammer_Provers.default_max_relevant_for_prover ctxt slice
    3.13                                                                  prover
    3.14           val is_appropriate_prop =
    3.15             Sledgehammer_Provers.is_appropriate_prop_for_prover ctxt

     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Dec 01 13:34:12 2011 +0100
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Dec 01 13:34:13 2011 +0100
     4.3 @@ -95,7 +95,7 @@
     4.4     ("max_new_mono_instances", "200"),
     4.5     ("isar_proof", "false"),
     4.6     ("isar_shrink_factor", "1"),
     4.7 -   ("slicing", "true"),
     4.8 +   ("slice", "true"),
     4.9     ("preplay_timeout", "4")]
    4.10  
    4.11  val alias_params =
    4.12 @@ -107,7 +107,7 @@
    4.13     ("non_blocking", "blocking"),
    4.14     ("unsound", "sound"),
    4.15     ("no_isar_proof", "isar_proof"),
    4.16 -   ("no_slicing", "slicing")]
    4.17 +   ("dont_slice", "slice")]
    4.18  
    4.19  val params_for_minimize =
    4.20    ["debug", "verbose", "overlord", "type_enc", "sound", "lam_trans",
    4.21 @@ -289,7 +289,7 @@
    4.22      val max_new_mono_instances = lookup_int "max_new_mono_instances"
    4.23      val isar_proof = lookup_bool "isar_proof"
    4.24      val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor")
    4.25 -    val slicing = mode <> Auto_Try andalso lookup_bool "slicing"
    4.26 +    val slice = mode <> Auto_Try andalso lookup_bool "slice"
    4.27      val timeout =
    4.28        (if mode = Auto_Try then NONE else lookup_time "timeout") |> the_timeout
    4.29      val preplay_timeout =
    4.30 @@ -302,8 +302,8 @@
    4.31       lam_trans = lam_trans, relevance_thresholds = relevance_thresholds,
    4.32       max_relevant = max_relevant, max_mono_iters = max_mono_iters,
    4.33       max_new_mono_instances = max_new_mono_instances,  isar_proof = isar_proof,
    4.34 -     isar_shrink_factor = isar_shrink_factor, slicing = slicing,
    4.35 -     timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
    4.36 +     isar_shrink_factor = isar_shrink_factor, slice = slice, timeout = timeout,
    4.37 +     preplay_timeout = preplay_timeout, expect = expect}
    4.38    end
    4.39  
    4.40  fun get_params mode = extract_params mode o default_raw_params

     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu Dec 01 13:34:12 2011 +0100
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu Dec 01 13:34:13 2011 +0100
     5.3 @@ -65,7 +65,7 @@
     5.4         lam_trans = lam_trans, relevance_thresholds = (1.01, 1.01),
     5.5         max_relevant = SOME (length facts), max_mono_iters = max_mono_iters,
     5.6         max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
     5.7 -       isar_shrink_factor = isar_shrink_factor, slicing = false,
     5.8 +       isar_shrink_factor = isar_shrink_factor, slice = false,
     5.9         timeout = timeout, preplay_timeout = preplay_timeout, expect = ""}
    5.10      val problem =
    5.11        {state = state, goal = goal, subgoal = i, subgoal_count = n,

     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Dec 01 13:34:12 2011 +0100
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Dec 01 13:34:13 2011 +0100
     6.3 @@ -33,7 +33,7 @@
     6.4       max_new_mono_instances: int,
     6.5       isar_proof: bool,
     6.6       isar_shrink_factor: int,
     6.7 -     slicing: bool,
     6.8 +     slice: bool,
     6.9       timeout: Time.time,
    6.10       preplay_timeout: Time.time,
    6.11       expect: string}
    6.12 @@ -163,18 +163,18 @@
    6.13    is_reconstructor orf is_smt_prover ctxt orf
    6.14    is_atp_installed (Proof_Context.theory_of ctxt)
    6.15  
    6.16 -fun get_slices slicing slices =
    6.17 -  (0 upto length slices - 1) ~~ slices |> not slicing ? (List.last #> single)
    6.18 +fun get_slices slice slices =
    6.19 +  (0 upto length slices - 1) ~~ slices |> not slice ? (List.last #> single)
    6.20  
    6.21  val reconstructor_default_max_relevant = 20
    6.22  
    6.23 -fun default_max_relevant_for_prover ctxt slicing name =
    6.24 +fun default_max_relevant_for_prover ctxt slice name =
    6.25    let val thy = Proof_Context.theory_of ctxt in
    6.26      if is_reconstructor name then
    6.27        reconstructor_default_max_relevant
    6.28      else if is_atp thy name then
    6.29        fold (Integer.max o #1 o snd o snd o snd)
    6.30 -           (get_slices slicing (#best_slices (get_atp thy name) ctxt)) 0
    6.31 +           (get_slices slice (#best_slices (get_atp thy name) ctxt)) 0
    6.32      else (* is_smt_prover ctxt name *)
    6.33        SMT_Solver.default_max_relevant ctxt name
    6.34    end
    6.35 @@ -296,7 +296,7 @@
    6.36     max_new_mono_instances: int,
    6.37     isar_proof: bool,
    6.38     isar_shrink_factor: int,
    6.39 -   slicing: bool,
    6.40 +   slice: bool,
    6.41     timeout: Time.time,
    6.42     preplay_timeout: Time.time,
    6.43     expect: string}
    6.44 @@ -578,7 +578,7 @@
    6.45            conj_sym_kind, prem_kind, best_slices, ...} : atp_config)
    6.46          (params as {debug, verbose, overlord, type_enc, sound, lam_trans,
    6.47                      max_relevant, max_mono_iters, max_new_mono_instances,
    6.48 -                    isar_proof, isar_shrink_factor, slicing, timeout,
    6.49 +                    isar_proof, isar_shrink_factor, slice, timeout,
    6.50                      preplay_timeout, ...})
    6.51          minimize_command
    6.52          ({state, goal, subgoal, subgoal_count, facts, ...} : prover_problem) =
    6.53 @@ -624,7 +624,7 @@
    6.54            let
    6.55              (* If slicing is disabled, we expand the last slice to fill the
    6.56                 entire time available. *)
    6.57 -            val actual_slices = get_slices slicing (best_slices ctxt)
    6.58 +            val actual_slices = get_slices slice (best_slices ctxt)
    6.59              val num_actual_slices = length actual_slices
    6.60              fun monomorphize_facts facts =
    6.61                let
    6.62 @@ -873,10 +873,10 @@
    6.63  
    6.64  fun smt_filter_loop ctxt name
    6.65                      ({debug, verbose, overlord, max_mono_iters,
    6.66 -                      max_new_mono_instances, timeout, slicing, ...} : params)
    6.67 +                      max_new_mono_instances, timeout, slice, ...} : params)
    6.68                      state i smt_filter =
    6.69    let
    6.70 -    val max_slices = if slicing then Config.get ctxt smt_max_slices else 1
    6.71 +    val max_slices = if slice then Config.get ctxt smt_max_slices else 1
    6.72      val repair_context =
    6.73        select_smt_solver name
    6.74        #> Config.put SMT_Config.verbose debug

     7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Thu Dec 01 13:34:12 2011 +0100
     7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Thu Dec 01 13:34:13 2011 +0100
     7.3 @@ -75,8 +75,8 @@
     7.4  fun adjust_reconstructor_params override_params
     7.5          ({debug, verbose, overlord, blocking, provers, type_enc, sound,
     7.6           lam_trans, relevance_thresholds, max_relevant, max_mono_iters,
     7.7 -         max_new_mono_instances, isar_proof, isar_shrink_factor, slicing,
     7.8 -         timeout, preplay_timeout, expect} : params) =
     7.9 +         max_new_mono_instances, isar_proof, isar_shrink_factor, slice, timeout,
    7.10 +         preplay_timeout, expect} : params) =
    7.11    let
    7.12      fun lookup_override name default_value =
    7.13        case AList.lookup (op =) override_params name of
    7.14 @@ -93,8 +93,8 @@
    7.15       relevance_thresholds = relevance_thresholds,
    7.16       max_mono_iters = max_mono_iters,
    7.17       max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
    7.18 -     isar_shrink_factor = isar_shrink_factor, slicing = slicing,
    7.19 -     timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
    7.20 +     isar_shrink_factor = isar_shrink_factor, slice = slice, timeout = timeout,
    7.21 +     preplay_timeout = preplay_timeout, expect = expect}
    7.22    end
    7.23  
    7.24  fun minimize ctxt mode name (params as {debug, verbose, isar_proof, ...})
    7.25 @@ -172,7 +172,7 @@
    7.26  fun is_induction_fact (Untranslated_Fact ((_, Induction), _)) = true
    7.27    | is_induction_fact _ = false
    7.28  
    7.29 -fun launch_prover (params as {debug, verbose, blocking, max_relevant, slicing,
    7.30 +fun launch_prover (params as {debug, verbose, blocking, max_relevant, slice,
    7.31                                timeout, expect, ...})
    7.32          mode minimize_command only
    7.33          {state, goal, subgoal, subgoal_count, facts, smt_filter} name =
    7.34 @@ -183,7 +183,7 @@
    7.35      val death_time = Time.+ (birth_time, hard_timeout)
    7.36      val max_relevant =
    7.37        max_relevant
    7.38 -      |> the_default (default_max_relevant_for_prover ctxt slicing name)
    7.39 +      |> the_default (default_max_relevant_for_prover ctxt slice name)
    7.40      val num_facts = length facts |> not only ? Integer.min max_relevant
    7.41      fun desc () =
    7.42        prover_description ctxt params name num_facts subgoal subgoal_count goal
    7.43 @@ -277,7 +277,7 @@
    7.44  val auto_try_max_relevant_divisor = 2 (* FUDGE *)
    7.45  
    7.46  fun run_sledgehammer (params as {debug, verbose, blocking, provers,
    7.47 -                                 relevance_thresholds, max_relevant, slicing,
    7.48 +                                 relevance_thresholds, max_relevant, slice,
    7.49                                   timeout, ...})
    7.50          mode i (relevance_override as {only, ...}) minimize_command state =
    7.51    if null provers then
    7.52 @@ -338,7 +338,7 @@
    7.53                SOME n => n
    7.54              | NONE =>
    7.55                0 |> fold (Integer.max
    7.56 -                         o default_max_relevant_for_prover ctxt slicing)
    7.57 +                         o default_max_relevant_for_prover ctxt slice)
    7.58                          provers
    7.59                  |> mode = Auto_Try
    7.60                     ? (fn n => n div auto_try_max_relevant_divisor)

     8.1 --- a/src/HOL/ex/sledgehammer_tactics.ML	Thu Dec 01 13:34:12 2011 +0100
     8.2 +++ b/src/HOL/ex/sledgehammer_tactics.ML	Thu Dec 01 13:34:13 2011 +0100
     8.3 @@ -25,13 +25,13 @@
     8.4  fun run_atp override_params relevance_override i n ctxt goal =
     8.5    let
     8.6      val chained_ths = [] (* a tactic has no chained ths *)
     8.7 -    val params as {provers, relevance_thresholds, max_relevant, slicing, ...} =
     8.8 +    val params as {provers, relevance_thresholds, max_relevant, slice, ...} =
     8.9        Sledgehammer_Isar.default_params ctxt override_params
    8.10      val name = hd provers
    8.11      val prover =
    8.12        Sledgehammer_Provers.get_prover ctxt Sledgehammer_Provers.Normal name
    8.13      val default_max_relevant =
    8.14 -      Sledgehammer_Provers.default_max_relevant_for_prover ctxt slicing name
    8.15 +      Sledgehammer_Provers.default_max_relevant_for_prover ctxt slice name
    8.16      val is_built_in_const =
    8.17        Sledgehammer_Provers.is_built_in_const_for_prover ctxt name
    8.18      val relevance_fudge =