Added skip_mono flag and inductive_flags type.
authorberghofe
Thu Apr 03 17:54:19 2008 +0200 (2008-04-03)
changeset 26534a2cb4de2a1aa
parent 26533 aeef55a3d1d5
child 26535 66bca8a4079c
Added skip_mono flag and inductive_flags type.
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/inductive_set_package.ML
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Thu Apr 03 17:52:51 2008 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Thu Apr 03 17:54:19 2008 +0200
     1.3 @@ -37,19 +37,16 @@
     1.4      Proof.context -> thm list list * local_theory
     1.5    val inductive_cases_i: ((bstring * Attrib.src list) * term list) list ->
     1.6      Proof.context -> thm list list * local_theory
     1.7 +  type inductive_flags
     1.8    val add_inductive_i:
     1.9 -    {quiet_mode: bool, verbose: bool, kind: string, alt_name: bstring,
    1.10 -      coind: bool, no_elim: bool, no_ind: bool} ->
    1.11 -    ((string * typ) * mixfix) list ->
    1.12 +    inductive_flags -> ((string * typ) * mixfix) list ->
    1.13      (string * typ) list -> ((bstring * Attrib.src list) * term) list -> thm list ->
    1.14        local_theory -> inductive_result * local_theory
    1.15    val add_inductive: bool -> bool -> (string * string option * mixfix) list ->
    1.16      (string * string option * mixfix) list ->
    1.17      ((bstring * Attrib.src list) * string) list -> (Facts.ref * Attrib.src list) list ->
    1.18      local_theory -> inductive_result * local_theory
    1.19 -  val add_inductive_global: string ->
    1.20 -    {quiet_mode: bool, verbose: bool, kind: string, alt_name: bstring,
    1.21 -      coind: bool, no_elim: bool, no_ind: bool} ->
    1.22 +  val add_inductive_global: string -> inductive_flags ->
    1.23      ((string * typ) * mixfix) list -> (string * typ) list ->
    1.24      ((bstring * Attrib.src list) * term) list -> thm list -> theory -> inductive_result * theory
    1.25    val arities_of: thm -> (string * int) list
    1.26 @@ -70,9 +67,7 @@
    1.27      thm -> local_theory -> thm list * thm list * thm * local_theory
    1.28    val add_ind_def: add_ind_def
    1.29    val gen_add_inductive_i: add_ind_def ->
    1.30 -    {quiet_mode: bool, verbose: bool, kind: string, alt_name: bstring,
    1.31 -      coind: bool, no_elim: bool, no_ind: bool} ->
    1.32 -    ((string * typ) * mixfix) list ->
    1.33 +    inductive_flags -> ((string * typ) * mixfix) list ->
    1.34      (string * typ) list -> ((bstring * Attrib.src list) * term) list -> thm list ->
    1.35        local_theory -> inductive_result * local_theory
    1.36    val gen_add_inductive: add_ind_def ->
    1.37 @@ -315,11 +310,12 @@
    1.38  
    1.39  (** proofs for (co)inductive predicates **)
    1.40  
    1.41 -(* prove monotonicity -- NOT subject to quick_and_dirty! *)
    1.42 +(* prove monotonicity *)
    1.43  
    1.44 -fun prove_mono quiet_mode predT fp_fun monos ctxt =
    1.45 - (message quiet_mode "  Proving monotonicity ...";
    1.46 -  Goal.prove ctxt [] []   (*NO quick_and_dirty here!*)
    1.47 +fun prove_mono quiet_mode skip_mono predT fp_fun monos ctxt =
    1.48 + (message (quiet_mode orelse skip_mono andalso !quick_and_dirty)
    1.49 +    "  Proving monotonicity ...";
    1.50 +  (if skip_mono then SkipProof.prove else Goal.prove) ctxt [] []
    1.51      (HOLogic.mk_Trueprop
    1.52        (Const (@{const_name Orderings.mono}, (predT --> predT) --> HOLogic.boolT) $ fp_fun))
    1.53      (fn _ => EVERY [rtac @{thm monoI} 1,
    1.54 @@ -586,7 +582,7 @@
    1.55  
    1.56  (** specification of (co)inductive predicates **)
    1.57  
    1.58 -fun mk_ind_def quiet_mode alt_name coind cs intr_ts monos params cnames_syn ctxt =
    1.59 +fun mk_ind_def quiet_mode skip_mono alt_name coind cs intr_ts monos params cnames_syn ctxt =
    1.60    let
    1.61      val fp_name = if coind then @{const_name Inductive.gfp} else @{const_name Inductive.lfp};
    1.62  
    1.63 @@ -664,7 +660,7 @@
    1.64      val (consts_defs, ctxt'') = fold_map (LocalTheory.define Thm.internalK) specs ctxt';
    1.65      val preds = (case cs of [_] => [rec_const] | _ => map #1 consts_defs);
    1.66  
    1.67 -    val mono = prove_mono quiet_mode predT fp_fun monos ctxt''
    1.68 +    val mono = prove_mono quiet_mode skip_mono predT fp_fun monos ctxt''
    1.69  
    1.70    in (ctxt'', rec_name, mono, fp_def', map (#2 o #2) consts_defs,
    1.71      list_comb (rec_const, params), preds, argTs, bs, xs)
    1.72 @@ -715,14 +711,17 @@
    1.73        end
    1.74    in (intrs', elims', induct', ctxt3) end;
    1.75  
    1.76 -type add_ind_def =
    1.77 +type inductive_flags =
    1.78    {quiet_mode: bool, verbose: bool, kind: string, alt_name: bstring,
    1.79 -    coind: bool, no_elim: bool, no_ind: bool} ->
    1.80 +   coind: bool, no_elim: bool, no_ind: bool, skip_mono: bool}
    1.81 +
    1.82 +type add_ind_def =
    1.83 +  inductive_flags ->
    1.84    term list -> ((string * Attrib.src list) * term) list -> thm list ->
    1.85    term list -> (string * mixfix) list ->
    1.86    local_theory -> inductive_result * local_theory
    1.87  
    1.88 -fun add_ind_def {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind}
    1.89 +fun add_ind_def {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono}
    1.90      cs intros monos params cnames_syn ctxt =
    1.91    let
    1.92      val _ = null cnames_syn andalso error "No inductive predicates given";
    1.93 @@ -735,7 +734,8 @@
    1.94        apfst split_list (split_list (map (check_rule ctxt cs params) intros));
    1.95  
    1.96      val (ctxt1, rec_name, mono, fp_def, rec_preds_defs, rec_const, preds,
    1.97 -      argTs, bs, xs) = mk_ind_def quiet_mode alt_name coind cs intr_ts monos params cnames_syn ctxt;
    1.98 +      argTs, bs, xs) = mk_ind_def quiet_mode skip_mono alt_name coind cs intr_ts
    1.99 +        monos params cnames_syn ctxt;
   1.100  
   1.101      val (intrs, unfold) = prove_intrs quiet_mode coind mono fp_def (length bs + length xs)
   1.102        params intr_ts rec_preds_defs ctxt1;
   1.103 @@ -774,7 +774,7 @@
   1.104  (* external interfaces *)
   1.105  
   1.106  fun gen_add_inductive_i mk_def
   1.107 -    (flags as {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind})
   1.108 +    (flags as {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono})
   1.109      cnames_syn pnames spec monos lthy =
   1.110    let
   1.111      val thy = ProofContext.theory_of lthy;
   1.112 @@ -839,7 +839,7 @@
   1.113      val intrs = map (apsnd the_single) specs;
   1.114      val monos = Attrib.eval_thms lthy raw_monos;
   1.115      val flags = {quiet_mode = false, verbose = verbose, kind = Thm.theoremK, alt_name = "",
   1.116 -      coind = coind, no_elim = false, no_ind = false};
   1.117 +      coind = coind, no_elim = false, no_ind = false, skip_mono = false};
   1.118    in
   1.119      lthy
   1.120      |> LocalTheory.set_group (serial_string ())
     2.1 --- a/src/HOL/Tools/inductive_set_package.ML	Thu Apr 03 17:52:51 2008 +0200
     2.2 +++ b/src/HOL/Tools/inductive_set_package.ML	Thu Apr 03 17:54:19 2008 +0200
     2.3 @@ -12,8 +12,7 @@
     2.4    val to_pred_att: thm list -> attribute
     2.5    val pred_set_conv_att: attribute
     2.6    val add_inductive_i:
     2.7 -    {quiet_mode: bool, verbose: bool, kind: string, alt_name: bstring,
     2.8 -      coind: bool, no_elim: bool, no_ind: bool} ->
     2.9 +    InductivePackage.inductive_flags ->
    2.10      ((string * typ) * mixfix) list ->
    2.11      (string * typ) list -> ((bstring * Attrib.src list) * term) list -> thm list ->
    2.12        local_theory -> InductivePackage.inductive_result * local_theory
    2.13 @@ -402,7 +401,7 @@
    2.14  
    2.15  (**** definition of inductive sets ****)
    2.16  
    2.17 -fun add_ind_set_def {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind}
    2.18 +fun add_ind_set_def {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono}
    2.19      cs intros monos params cnames_syn ctxt =
    2.20    let
    2.21      val thy = ProofContext.theory_of ctxt;
    2.22 @@ -466,7 +465,7 @@
    2.23      val monos' = map (to_pred [] (Context.Proof ctxt)) monos;
    2.24      val ({preds, intrs, elims, raw_induct, ...}, ctxt1) =
    2.25        InductivePackage.add_ind_def {quiet_mode = quiet_mode, verbose = verbose, kind = kind,
    2.26 -          alt_name = "", coind = coind, no_elim = no_elim, no_ind = no_ind}
    2.27 +          alt_name = "", coind = coind, no_elim = no_elim, no_ind = no_ind, skip_mono = skip_mono}
    2.28          cs' intros' monos' params1 cnames_syn' ctxt;
    2.29  
    2.30      (* define inductive sets using previously defined predicates *)