added fork_mono flag, which is usually enabled in batch-mode only;
authorwenzelm
Wed Jan 07 23:52:18 2009 +0100 (2009-01-07)
changeset 2938879eb3649ca9e
parent 29387 d23fdfa46b6a
child 29389 0a49f940d729
added fork_mono flag, which is usually enabled in batch-mode only;
mono rule: unnamed LocalTheory.node ensures proper joining of pending proofs;
src/HOL/Tools/inductive_package.ML
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Wed Jan 07 20:27:55 2009 +0100
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Wed Jan 07 23:52:18 2009 +0100
     1.3 @@ -46,7 +46,7 @@
     1.4      (Binding.T * string option * mixfix) list ->
     1.5      (Attrib.binding * string) list ->
     1.6      (Facts.ref * Attrib.src list) list ->
     1.7 -    local_theory -> inductive_result * local_theory
     1.8 +    bool -> local_theory -> inductive_result * local_theory
     1.9    val add_inductive_global: string -> inductive_flags ->
    1.10      ((Binding.T * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list ->
    1.11      thm list -> theory -> inductive_result * theory
    1.12 @@ -74,9 +74,9 @@
    1.13      (Binding.T * string option * mixfix) list ->
    1.14      (Binding.T * string option * mixfix) list ->
    1.15      (Attrib.binding * string) list -> (Facts.ref * Attrib.src list) list ->
    1.16 -    local_theory -> inductive_result * local_theory
    1.17 +    bool -> local_theory -> inductive_result * local_theory
    1.18    val gen_ind_decl: add_ind_def -> bool ->
    1.19 -    OuterParse.token list -> (local_theory -> local_theory) * OuterParse.token list
    1.20 +    OuterParse.token list -> (bool -> local_theory -> local_theory) * OuterParse.token list
    1.21  end;
    1.22  
    1.23  structure InductivePackage: INDUCTIVE_PACKAGE =
    1.24 @@ -312,10 +312,11 @@
    1.25  
    1.26  (* prove monotonicity *)
    1.27  
    1.28 -fun prove_mono quiet_mode skip_mono predT fp_fun monos ctxt =
    1.29 - (message (quiet_mode orelse skip_mono andalso !quick_and_dirty)
    1.30 +fun prove_mono quiet_mode skip_mono fork_mono predT fp_fun monos ctxt =
    1.31 + (message (quiet_mode orelse skip_mono andalso !quick_and_dirty orelse fork_mono)
    1.32      "  Proving monotonicity ...";
    1.33 -  (if skip_mono then SkipProof.prove else Goal.prove) ctxt [] []
    1.34 +  (if skip_mono then SkipProof.prove else if fork_mono then Goal.prove_future else Goal.prove) ctxt
    1.35 +    [] []
    1.36      (HOLogic.mk_Trueprop
    1.37        (Const (@{const_name Orderings.mono}, (predT --> predT) --> HOLogic.boolT) $ fp_fun))
    1.38      (fn _ => EVERY [rtac @{thm monoI} 1,
    1.39 @@ -582,7 +583,7 @@
    1.40  
    1.41  (** specification of (co)inductive predicates **)
    1.42  
    1.43 -fun mk_ind_def quiet_mode skip_mono alt_name coind cs intr_ts monos params cnames_syn ctxt =
    1.44 +fun mk_ind_def quiet_mode skip_mono fork_mono alt_name coind cs intr_ts monos params cnames_syn ctxt =
    1.45    let
    1.46      val fp_name = if coind then @{const_name Inductive.gfp} else @{const_name Inductive.lfp};
    1.47  
    1.48 @@ -662,9 +663,11 @@
    1.49      val (consts_defs, ctxt'') = fold_map (LocalTheory.define Thm.internalK) specs ctxt';
    1.50      val preds = (case cs of [_] => [rec_const] | _ => map #1 consts_defs);
    1.51  
    1.52 -    val mono = prove_mono quiet_mode skip_mono predT fp_fun monos ctxt''
    1.53 +    val mono = prove_mono quiet_mode skip_mono fork_mono predT fp_fun monos ctxt'';
    1.54 +    val ((_, [mono']), ctxt''') =
    1.55 +      LocalTheory.note Thm.internalK (Attrib.empty_binding, [mono]) ctxt'';
    1.56  
    1.57 -  in (ctxt'', rec_name, mono, fp_def', map (#2 o #2) consts_defs,
    1.58 +  in (ctxt''', rec_name, mono', fp_def', map (#2 o #2) consts_defs,
    1.59      list_comb (rec_const, params), preds, argTs, bs, xs)
    1.60    end;
    1.61  
    1.62 @@ -718,7 +721,7 @@
    1.63  
    1.64  type inductive_flags =
    1.65    {quiet_mode: bool, verbose: bool, kind: string, alt_name: Binding.T,
    1.66 -   coind: bool, no_elim: bool, no_ind: bool, skip_mono: bool}
    1.67 +   coind: bool, no_elim: bool, no_ind: bool, skip_mono: bool, fork_mono: bool}
    1.68  
    1.69  type add_ind_def =
    1.70    inductive_flags ->
    1.71 @@ -726,7 +729,7 @@
    1.72    term list -> (Binding.T * mixfix) list ->
    1.73    local_theory -> inductive_result * local_theory
    1.74  
    1.75 -fun add_ind_def {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono}
    1.76 +fun add_ind_def {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono}
    1.77      cs intros monos params cnames_syn ctxt =
    1.78    let
    1.79      val _ = null cnames_syn andalso error "No inductive predicates given";
    1.80 @@ -739,7 +742,7 @@
    1.81        apfst split_list (split_list (map (check_rule ctxt cs params) intros));
    1.82  
    1.83      val (ctxt1, rec_name, mono, fp_def, rec_preds_defs, rec_const, preds,
    1.84 -      argTs, bs, xs) = mk_ind_def quiet_mode skip_mono alt_name coind cs intr_ts
    1.85 +      argTs, bs, xs) = mk_ind_def quiet_mode skip_mono fork_mono alt_name coind cs intr_ts
    1.86          monos params cnames_syn ctxt;
    1.87  
    1.88      val (intrs, unfold) = prove_intrs quiet_mode coind mono fp_def (length bs + length xs)
    1.89 @@ -780,7 +783,7 @@
    1.90  (* external interfaces *)
    1.91  
    1.92  fun gen_add_inductive_i mk_def
    1.93 -    (flags as {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono})
    1.94 +    (flags as {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono})
    1.95      cnames_syn pnames spec monos lthy =
    1.96    let
    1.97      val thy = ProofContext.theory_of lthy;
    1.98 @@ -836,7 +839,7 @@
    1.99      ||> fold (snd oo LocalTheory.abbrev Syntax.mode_default) abbrevs
   1.100    end;
   1.101  
   1.102 -fun gen_add_inductive mk_def verbose coind cnames_syn pnames_syn intro_srcs raw_monos lthy =
   1.103 +fun gen_add_inductive mk_def verbose coind cnames_syn pnames_syn intro_srcs raw_monos int lthy =
   1.104    let
   1.105      val ((vars, specs), _) = lthy |> ProofContext.set_mode ProofContext.mode_abbrev
   1.106        |> Specification.read_specification
   1.107 @@ -845,7 +848,8 @@
   1.108      val intrs = map (apsnd the_single) specs;
   1.109      val monos = Attrib.eval_thms lthy raw_monos;
   1.110      val flags = {quiet_mode = false, verbose = verbose, kind = Thm.theoremK,
   1.111 -      alt_name = Binding.empty, coind = coind, no_elim = false, no_ind = false, skip_mono = false};
   1.112 +      alt_name = Binding.empty, coind = coind, no_elim = false, no_ind = false,
   1.113 +      skip_mono = false, fork_mono = not int};
   1.114    in
   1.115      lthy
   1.116      |> LocalTheory.set_group (serial_string ())
   1.117 @@ -956,12 +960,12 @@
   1.118    Scan.optional (P.$$$ "where" |-- P.!!! SpecParse.specification) [] --
   1.119    Scan.optional (P.$$$ "monos" |-- P.!!! SpecParse.xthms1) []
   1.120    >> (fn (((preds, params), specs), monos) =>
   1.121 -      (snd o gen_add_inductive mk_def true coind preds params (flatten_specification specs) monos));
   1.122 +      (snd oo gen_add_inductive mk_def true coind preds params (flatten_specification specs) monos));
   1.123  
   1.124  val ind_decl = gen_ind_decl add_ind_def;
   1.125  
   1.126 -val _ = OuterSyntax.local_theory "inductive" "define inductive predicates" K.thy_decl (ind_decl false);
   1.127 -val _ = OuterSyntax.local_theory "coinductive" "define coinductive predicates" K.thy_decl (ind_decl true);
   1.128 +val _ = OuterSyntax.local_theory' "inductive" "define inductive predicates" K.thy_decl (ind_decl false);
   1.129 +val _ = OuterSyntax.local_theory' "coinductive" "define coinductive predicates" K.thy_decl (ind_decl true);
   1.130  
   1.131  val _ =
   1.132    OuterSyntax.local_theory "inductive_cases"