# HG changeset patch
# User berghofe
# Date 1207238059 -7200
# Node ID a2cb4de2a1aa74d6b9096bb61f7697a2724f69e1
# Parent  aeef55a3d1d5c9d910a2a42a00bd1f163fd256b8
Added skip_mono flag and inductive_flags type.

diff -r aeef55a3d1d5 -r a2cb4de2a1aa src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Thu Apr 03 17:52:51 2008 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Thu Apr 03 17:54:19 2008 +0200
@@ -37,19 +37,16 @@
     Proof.context -> thm list list * local_theory
   val inductive_cases_i: ((bstring * Attrib.src list) * term list) list ->
     Proof.context -> thm list list * local_theory
+  type inductive_flags
   val add_inductive_i:
-    {quiet_mode: bool, verbose: bool, kind: string, alt_name: bstring,
-      coind: bool, no_elim: bool, no_ind: bool} ->
-    ((string * typ) * mixfix) list ->
+    inductive_flags -> ((string * typ) * mixfix) list ->
     (string * typ) list -> ((bstring * Attrib.src list) * term) list -> thm list ->
       local_theory -> inductive_result * local_theory
   val add_inductive: bool -> bool -> (string * string option * mixfix) list ->
     (string * string option * mixfix) list ->
     ((bstring * Attrib.src list) * string) list -> (Facts.ref * Attrib.src list) list ->
     local_theory -> inductive_result * local_theory
-  val add_inductive_global: string ->
-    {quiet_mode: bool, verbose: bool, kind: string, alt_name: bstring,
-      coind: bool, no_elim: bool, no_ind: bool} ->
+  val add_inductive_global: string -> inductive_flags ->
     ((string * typ) * mixfix) list -> (string * typ) list ->
     ((bstring * Attrib.src list) * term) list -> thm list -> theory -> inductive_result * theory
   val arities_of: thm -> (string * int) list
@@ -70,9 +67,7 @@
     thm -> local_theory -> thm list * thm list * thm * local_theory
   val add_ind_def: add_ind_def
   val gen_add_inductive_i: add_ind_def ->
-    {quiet_mode: bool, verbose: bool, kind: string, alt_name: bstring,
-      coind: bool, no_elim: bool, no_ind: bool} ->
-    ((string * typ) * mixfix) list ->
+    inductive_flags -> ((string * typ) * mixfix) list ->
     (string * typ) list -> ((bstring * Attrib.src list) * term) list -> thm list ->
       local_theory -> inductive_result * local_theory
   val gen_add_inductive: add_ind_def ->
@@ -315,11 +310,12 @@
 
 (** proofs for (co)inductive predicates **)
 
-(* prove monotonicity -- NOT subject to quick_and_dirty! *)
+(* prove monotonicity *)
 
-fun prove_mono quiet_mode predT fp_fun monos ctxt =
- (message quiet_mode "  Proving monotonicity ...";
-  Goal.prove ctxt [] []   (*NO quick_and_dirty here!*)
+fun prove_mono quiet_mode skip_mono predT fp_fun monos ctxt =
+ (message (quiet_mode orelse skip_mono andalso !quick_and_dirty)
+    "  Proving monotonicity ...";
+  (if skip_mono then SkipProof.prove else Goal.prove) ctxt [] []
     (HOLogic.mk_Trueprop
       (Const (@{const_name Orderings.mono}, (predT --> predT) --> HOLogic.boolT) $ fp_fun))
     (fn _ => EVERY [rtac @{thm monoI} 1,
@@ -586,7 +582,7 @@
 
 (** specification of (co)inductive predicates **)
 
-fun mk_ind_def quiet_mode alt_name coind cs intr_ts monos params cnames_syn ctxt =
+fun mk_ind_def quiet_mode skip_mono alt_name coind cs intr_ts monos params cnames_syn ctxt =
   let
     val fp_name = if coind then @{const_name Inductive.gfp} else @{const_name Inductive.lfp};
 
@@ -664,7 +660,7 @@
     val (consts_defs, ctxt'') = fold_map (LocalTheory.define Thm.internalK) specs ctxt';
     val preds = (case cs of [_] => [rec_const] | _ => map #1 consts_defs);
 
-    val mono = prove_mono quiet_mode predT fp_fun monos ctxt''
+    val mono = prove_mono quiet_mode skip_mono predT fp_fun monos ctxt''
 
   in (ctxt'', rec_name, mono, fp_def', map (#2 o #2) consts_defs,
     list_comb (rec_const, params), preds, argTs, bs, xs)
@@ -715,14 +711,17 @@
       end
   in (intrs', elims', induct', ctxt3) end;
 
-type add_ind_def =
+type inductive_flags =
   {quiet_mode: bool, verbose: bool, kind: string, alt_name: bstring,
-    coind: bool, no_elim: bool, no_ind: bool} ->
+   coind: bool, no_elim: bool, no_ind: bool, skip_mono: bool}
+
+type add_ind_def =
+  inductive_flags ->
   term list -> ((string * Attrib.src list) * term) list -> thm list ->
   term list -> (string * mixfix) list ->
   local_theory -> inductive_result * local_theory
 
-fun add_ind_def {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind}
+fun add_ind_def {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono}
     cs intros monos params cnames_syn ctxt =
   let
     val _ = null cnames_syn andalso error "No inductive predicates given";
@@ -735,7 +734,8 @@
       apfst split_list (split_list (map (check_rule ctxt cs params) intros));
 
     val (ctxt1, rec_name, mono, fp_def, rec_preds_defs, rec_const, preds,
-      argTs, bs, xs) = mk_ind_def quiet_mode alt_name coind cs intr_ts monos params cnames_syn ctxt;
+      argTs, bs, xs) = mk_ind_def quiet_mode skip_mono alt_name coind cs intr_ts
+        monos params cnames_syn ctxt;
 
     val (intrs, unfold) = prove_intrs quiet_mode coind mono fp_def (length bs + length xs)
       params intr_ts rec_preds_defs ctxt1;
@@ -774,7 +774,7 @@
 (* external interfaces *)
 
 fun gen_add_inductive_i mk_def
-    (flags as {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind})
+    (flags as {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono})
     cnames_syn pnames spec monos lthy =
   let
     val thy = ProofContext.theory_of lthy;
@@ -839,7 +839,7 @@
     val intrs = map (apsnd the_single) specs;
     val monos = Attrib.eval_thms lthy raw_monos;
     val flags = {quiet_mode = false, verbose = verbose, kind = Thm.theoremK, alt_name = "",
-      coind = coind, no_elim = false, no_ind = false};
+      coind = coind, no_elim = false, no_ind = false, skip_mono = false};
   in
     lthy
     |> LocalTheory.set_group (serial_string ())
diff -r aeef55a3d1d5 -r a2cb4de2a1aa src/HOL/Tools/inductive_set_package.ML
--- a/src/HOL/Tools/inductive_set_package.ML	Thu Apr 03 17:52:51 2008 +0200
+++ b/src/HOL/Tools/inductive_set_package.ML	Thu Apr 03 17:54:19 2008 +0200
@@ -12,8 +12,7 @@
   val to_pred_att: thm list -> attribute
   val pred_set_conv_att: attribute
   val add_inductive_i:
-    {quiet_mode: bool, verbose: bool, kind: string, alt_name: bstring,
-      coind: bool, no_elim: bool, no_ind: bool} ->
+    InductivePackage.inductive_flags ->
     ((string * typ) * mixfix) list ->
     (string * typ) list -> ((bstring * Attrib.src list) * term) list -> thm list ->
       local_theory -> InductivePackage.inductive_result * local_theory
@@ -402,7 +401,7 @@
 
 (**** definition of inductive sets ****)
 
-fun add_ind_set_def {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind}
+fun add_ind_set_def {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono}
     cs intros monos params cnames_syn ctxt =
   let
     val thy = ProofContext.theory_of ctxt;
@@ -466,7 +465,7 @@
     val monos' = map (to_pred [] (Context.Proof ctxt)) monos;
     val ({preds, intrs, elims, raw_induct, ...}, ctxt1) =
       InductivePackage.add_ind_def {quiet_mode = quiet_mode, verbose = verbose, kind = kind,
-          alt_name = "", coind = coind, no_elim = no_elim, no_ind = no_ind}
+          alt_name = "", coind = coind, no_elim = no_elim, no_ind = no_ind, skip_mono = skip_mono}
         cs' intros' monos' params1 cnames_syn' ctxt;
 
     (* define inductive sets using previously defined predicates *)