src/HOL/Tools/inductive.ML
changeset 49170 03bee3a6a1b7
parent 47876 0521ee2e504d
child 49324 4f28543ae7fa
     1.1 --- a/src/HOL/Tools/inductive.ML	Wed Sep 05 17:12:40 2012 +0200
     1.2 +++ b/src/HOL/Tools/inductive.ML	Wed Sep 05 19:51:00 2012 +0200
     1.3 @@ -39,7 +39,7 @@
     1.4      thm list list * local_theory
     1.5    type inductive_flags =
     1.6      {quiet_mode: bool, verbose: bool, alt_name: binding, coind: bool,
     1.7 -      no_elim: bool, no_ind: bool, skip_mono: bool, fork_mono: bool}
     1.8 +      no_elim: bool, no_ind: bool, skip_mono: bool}
     1.9    val add_inductive_i:
    1.10      inductive_flags -> ((binding * typ) * mixfix) list ->
    1.11      (string * typ) list -> (Attrib.binding * term) list -> thm list -> local_theory ->
    1.12 @@ -358,10 +358,10 @@
    1.13  
    1.14  (* prove monotonicity *)
    1.15  
    1.16 -fun prove_mono quiet_mode skip_mono fork_mono predT fp_fun monos ctxt =
    1.17 - (message (quiet_mode orelse skip_mono andalso !quick_and_dirty orelse fork_mono)
    1.18 +fun prove_mono quiet_mode skip_mono predT fp_fun monos ctxt =
    1.19 + (message (quiet_mode orelse skip_mono andalso ! quick_and_dirty)
    1.20      "  Proving monotonicity ...";
    1.21 -  (if skip_mono then Skip_Proof.prove else if fork_mono then Goal.prove_future else Goal.prove) ctxt
    1.22 +  (if skip_mono then Skip_Proof.prove else Goal.prove_future) ctxt
    1.23      [] []
    1.24      (HOLogic.mk_Trueprop
    1.25        (Const (@{const_name Orderings.mono}, (predT --> predT) --> HOLogic.boolT) $ fp_fun))
    1.26 @@ -746,8 +746,7 @@
    1.27  
    1.28  (** specification of (co)inductive predicates **)
    1.29  
    1.30 -fun mk_ind_def quiet_mode skip_mono fork_mono alt_name coind
    1.31 -    cs intr_ts monos params cnames_syn lthy =
    1.32 +fun mk_ind_def quiet_mode skip_mono alt_name coind cs intr_ts monos params cnames_syn lthy =
    1.33    let
    1.34      val fp_name = if coind then @{const_name Inductive.gfp} else @{const_name Inductive.lfp};
    1.35  
    1.36 @@ -841,7 +840,7 @@
    1.37      val preds = (case cs of [_] => [rec_const] | _ => map #1 consts_defs);
    1.38  
    1.39      val (_, lthy''') = Variable.add_fixes (map (fst o dest_Free) params) lthy'';
    1.40 -    val mono = prove_mono quiet_mode skip_mono fork_mono predT fp_fun monos lthy''';
    1.41 +    val mono = prove_mono quiet_mode skip_mono predT fp_fun monos lthy''';
    1.42      val (_, lthy'''') =
    1.43        Local_Theory.note (apfst Binding.conceal Attrib.empty_binding,
    1.44          Proof_Context.export lthy''' lthy'' [mono]) lthy'';
    1.45 @@ -912,7 +911,7 @@
    1.46  
    1.47  type inductive_flags =
    1.48    {quiet_mode: bool, verbose: bool, alt_name: binding, coind: bool,
    1.49 -    no_elim: bool, no_ind: bool, skip_mono: bool, fork_mono: bool};
    1.50 +    no_elim: bool, no_ind: bool, skip_mono: bool};
    1.51  
    1.52  type add_ind_def =
    1.53    inductive_flags ->
    1.54 @@ -920,7 +919,7 @@
    1.55    term list -> (binding * mixfix) list ->
    1.56    local_theory -> inductive_result * local_theory;
    1.57  
    1.58 -fun add_ind_def {quiet_mode, verbose, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono}
    1.59 +fun add_ind_def {quiet_mode, verbose, alt_name, coind, no_elim, no_ind, skip_mono}
    1.60      cs intros monos params cnames_syn lthy =
    1.61    let
    1.62      val _ = null cnames_syn andalso error "No inductive predicates given";
    1.63 @@ -933,7 +932,7 @@
    1.64        apfst split_list (split_list (map (check_rule lthy cs params) intros));
    1.65  
    1.66      val (lthy1, lthy2, rec_name, mono, fp_def, rec_preds_defs, rec_const, preds,
    1.67 -      argTs, bs, xs) = mk_ind_def quiet_mode skip_mono fork_mono alt_name coind cs intr_ts
    1.68 +      argTs, bs, xs) = mk_ind_def quiet_mode skip_mono alt_name coind cs intr_ts
    1.69          monos params cnames_syn lthy;
    1.70  
    1.71      val (intrs, unfold) = prove_intrs quiet_mode coind mono fp_def (length bs + length xs)
    1.72 @@ -983,7 +982,7 @@
    1.73  (* external interfaces *)
    1.74  
    1.75  fun gen_add_inductive_i mk_def
    1.76 -    (flags as {quiet_mode, verbose, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono})
    1.77 +    (flags as {quiet_mode, verbose, alt_name, coind, no_elim, no_ind, skip_mono})
    1.78      cnames_syn pnames spec monos lthy =
    1.79    let
    1.80      val thy = Proof_Context.theory_of lthy;
    1.81 @@ -1047,8 +1046,9 @@
    1.82        |> Specification.read_spec (cnames_syn @ pnames_syn) intro_srcs;
    1.83      val (cs, ps) = chop (length cnames_syn) vars;
    1.84      val monos = Attrib.eval_thms lthy raw_monos;
    1.85 -    val flags = {quiet_mode = false, verbose = verbose, alt_name = Binding.empty,
    1.86 -      coind = coind, no_elim = false, no_ind = false, skip_mono = false, fork_mono = not int};
    1.87 +    val flags =
    1.88 +     {quiet_mode = false, verbose = verbose, alt_name = Binding.empty,
    1.89 +      coind = coind, no_elim = false, no_ind = false, skip_mono = false};
    1.90    in
    1.91      lthy
    1.92      |> gen_add_inductive_i mk_def flags cs (map (apfst Binding.name_of o fst) ps) intrs monos