# HG changeset patch # User wenzelm # Date 1231526493 -3600 # Node ID 747c95f7bb7e69603d65b06bbd645dffb2e12c8a # Parent 43a12fc76f4897e9e9b46a6a6d04ecbd396da21c# Parent 7c68688f6eed1afca6fafff9f82d01747afe3809 merged diff -r 43a12fc76f48 -r 747c95f7bb7e src/HOL/Nominal/nominal_package.ML --- a/src/HOL/Nominal/nominal_package.ML Fri Jan 09 09:49:01 2009 -0800 +++ b/src/HOL/Nominal/nominal_package.ML Fri Jan 09 19:41:33 2009 +0100 @@ -571,7 +571,7 @@ InductivePackage.add_inductive_global (serial_string ()) {quiet_mode = false, verbose = false, kind = Thm.internalK, alt_name = Binding.name big_rep_name, coind = false, no_elim = true, no_ind = false, - skip_mono = true} + skip_mono = true, fork_mono = false} (map (fn (s, T) => ((Binding.name s, T --> HOLogic.boolT), NoSyn)) (rep_set_names' ~~ recTs')) [] (map (fn x => (Attrib.empty_binding, x)) intr_ts) [] thy3; @@ -1509,7 +1509,7 @@ InductivePackage.add_inductive_global (serial_string ()) {quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK, alt_name = Binding.name big_rec_name, coind = false, no_elim = false, no_ind = false, - skip_mono = true} + skip_mono = true, fork_mono = false} (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts)) (map dest_Free rec_fns) (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) [] ||> diff -r 43a12fc76f48 -r 747c95f7bb7e src/HOL/Tools/datatype_abs_proofs.ML --- a/src/HOL/Tools/datatype_abs_proofs.ML Fri Jan 09 09:49:01 2009 -0800 +++ b/src/HOL/Tools/datatype_abs_proofs.ML Fri Jan 09 19:41:33 2009 +0100 @@ -155,7 +155,7 @@ InductivePackage.add_inductive_global (serial_string ()) {quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK, alt_name = Binding.name big_rec_name', coind = false, no_elim = false, no_ind = true, - skip_mono = true} + skip_mono = true, fork_mono = false} (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts)) (map dest_Free rec_fns) (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) [] thy0; diff -r 43a12fc76f48 -r 747c95f7bb7e src/HOL/Tools/datatype_rep_proofs.ML --- a/src/HOL/Tools/datatype_rep_proofs.ML Fri Jan 09 09:49:01 2009 -0800 +++ b/src/HOL/Tools/datatype_rep_proofs.ML Fri Jan 09 19:41:33 2009 +0100 @@ -183,7 +183,7 @@ InductivePackage.add_inductive_global (serial_string ()) {quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK, alt_name = Binding.name big_rec_name, coind = false, no_elim = true, no_ind = false, - skip_mono = true} + skip_mono = true, fork_mono = false} (map (fn s => ((Binding.name s, UnivT'), NoSyn)) rep_set_names') [] (map (fn x => (Attrib.empty_binding, x)) intr_ts) [] thy1; diff -r 43a12fc76f48 -r 747c95f7bb7e src/HOL/Tools/function_package/inductive_wrap.ML --- a/src/HOL/Tools/function_package/inductive_wrap.ML Fri Jan 09 09:49:01 2009 -0800 +++ b/src/HOL/Tools/function_package/inductive_wrap.ML Fri Jan 09 19:41:33 2009 +0100 @@ -48,7 +48,8 @@ coind = false, no_elim = false, no_ind = false, - skip_mono = true} + skip_mono = true, + fork_mono = false} [((Binding.name R, T), NoSyn)] (* the relation *) [] (* no parameters *) (map (fn t => (Attrib.empty_binding, t)) defs) (* the intros *) diff -r 43a12fc76f48 -r 747c95f7bb7e src/HOL/Tools/inductive_package.ML --- a/src/HOL/Tools/inductive_package.ML Fri Jan 09 09:49:01 2009 -0800 +++ b/src/HOL/Tools/inductive_package.ML Fri Jan 09 19:41:33 2009 +0100 @@ -46,7 +46,7 @@ (Binding.T * string option * mixfix) list -> (Attrib.binding * string) list -> (Facts.ref * Attrib.src list) list -> - local_theory -> inductive_result * local_theory + bool -> local_theory -> inductive_result * local_theory val add_inductive_global: string -> inductive_flags -> ((Binding.T * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list -> thm list -> theory -> inductive_result * theory @@ -74,9 +74,9 @@ (Binding.T * string option * mixfix) list -> (Binding.T * string option * mixfix) list -> (Attrib.binding * string) list -> (Facts.ref * Attrib.src list) list -> - local_theory -> inductive_result * local_theory + bool -> local_theory -> inductive_result * local_theory val gen_ind_decl: add_ind_def -> bool -> - OuterParse.token list -> (local_theory -> local_theory) * OuterParse.token list + OuterParse.token list -> (bool -> local_theory -> local_theory) * OuterParse.token list end; structure InductivePackage: INDUCTIVE_PACKAGE = @@ -312,10 +312,11 @@ (* prove monotonicity *) -fun prove_mono quiet_mode skip_mono predT fp_fun monos ctxt = - (message (quiet_mode orelse skip_mono andalso !quick_and_dirty) +fun prove_mono quiet_mode skip_mono fork_mono predT fp_fun monos ctxt = + (message (quiet_mode orelse skip_mono andalso !quick_and_dirty orelse fork_mono) " Proving monotonicity ..."; - (if skip_mono then SkipProof.prove else Goal.prove) ctxt [] [] + (if skip_mono then SkipProof.prove else if fork_mono then Goal.prove_future else Goal.prove) ctxt + [] [] (HOLogic.mk_Trueprop (Const (@{const_name Orderings.mono}, (predT --> predT) --> HOLogic.boolT) $ fp_fun)) (fn _ => EVERY [rtac @{thm monoI} 1, @@ -582,7 +583,7 @@ (** specification of (co)inductive predicates **) -fun mk_ind_def quiet_mode skip_mono alt_name coind cs intr_ts monos params cnames_syn ctxt = +fun mk_ind_def quiet_mode skip_mono fork_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}; @@ -662,9 +663,11 @@ 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 skip_mono predT fp_fun monos ctxt'' + val mono = prove_mono quiet_mode skip_mono fork_mono predT fp_fun monos ctxt''; + val ((_, [mono']), ctxt''') = + LocalTheory.note Thm.internalK (Attrib.empty_binding, [mono]) ctxt''; - in (ctxt'', rec_name, mono, fp_def', map (#2 o #2) consts_defs, + in (ctxt''', rec_name, mono', fp_def', map (#2 o #2) consts_defs, list_comb (rec_const, params), preds, argTs, bs, xs) end; @@ -718,7 +721,7 @@ type inductive_flags = {quiet_mode: bool, verbose: bool, kind: string, alt_name: Binding.T, - coind: bool, no_elim: bool, no_ind: bool, skip_mono: bool} + coind: bool, no_elim: bool, no_ind: bool, skip_mono: bool, fork_mono: bool} type add_ind_def = inductive_flags -> @@ -726,7 +729,7 @@ term list -> (Binding.T * mixfix) list -> local_theory -> inductive_result * local_theory -fun add_ind_def {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono} +fun add_ind_def {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono} cs intros monos params cnames_syn ctxt = let val _ = null cnames_syn andalso error "No inductive predicates given"; @@ -739,7 +742,7 @@ 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 skip_mono alt_name coind cs intr_ts + argTs, bs, xs) = mk_ind_def quiet_mode skip_mono fork_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) @@ -780,7 +783,7 @@ (* external interfaces *) fun gen_add_inductive_i mk_def - (flags as {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono}) + (flags as {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono}) cnames_syn pnames spec monos lthy = let val thy = ProofContext.theory_of lthy; @@ -836,7 +839,7 @@ ||> fold (snd oo LocalTheory.abbrev Syntax.mode_default) abbrevs end; -fun gen_add_inductive mk_def verbose coind cnames_syn pnames_syn intro_srcs raw_monos lthy = +fun gen_add_inductive mk_def verbose coind cnames_syn pnames_syn intro_srcs raw_monos int lthy = let val ((vars, specs), _) = lthy |> ProofContext.set_mode ProofContext.mode_abbrev |> Specification.read_specification @@ -845,7 +848,8 @@ 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 = Binding.empty, coind = coind, no_elim = false, no_ind = false, skip_mono = false}; + alt_name = Binding.empty, coind = coind, no_elim = false, no_ind = false, + skip_mono = false, fork_mono = not int}; in lthy |> LocalTheory.set_group (serial_string ()) @@ -956,12 +960,12 @@ Scan.optional (P.$$$ "where" |-- P.!!! SpecParse.specification) [] -- Scan.optional (P.$$$ "monos" |-- P.!!! SpecParse.xthms1) [] >> (fn (((preds, params), specs), monos) => - (snd o gen_add_inductive mk_def true coind preds params (flatten_specification specs) monos)); + (snd oo gen_add_inductive mk_def true coind preds params (flatten_specification specs) monos)); val ind_decl = gen_ind_decl add_ind_def; -val _ = OuterSyntax.local_theory "inductive" "define inductive predicates" K.thy_decl (ind_decl false); -val _ = OuterSyntax.local_theory "coinductive" "define coinductive predicates" K.thy_decl (ind_decl true); +val _ = OuterSyntax.local_theory' "inductive" "define inductive predicates" K.thy_decl (ind_decl false); +val _ = OuterSyntax.local_theory' "coinductive" "define coinductive predicates" K.thy_decl (ind_decl true); val _ = OuterSyntax.local_theory "inductive_cases" diff -r 43a12fc76f48 -r 747c95f7bb7e src/HOL/Tools/inductive_realizer.ML --- a/src/HOL/Tools/inductive_realizer.ML Fri Jan 09 09:49:01 2009 -0800 +++ b/src/HOL/Tools/inductive_realizer.ML Fri Jan 09 19:41:33 2009 +0100 @@ -347,7 +347,7 @@ val (ind_info, thy3') = thy2 |> InductivePackage.add_inductive_global (serial_string ()) {quiet_mode = false, verbose = false, kind = Thm.theoremK, alt_name = Binding.empty, - coind = false, no_elim = false, no_ind = false, skip_mono = false} + coind = false, no_elim = false, no_ind = false, skip_mono = false, fork_mono = false} rlzpreds rlzparams (map (fn (rintr, intr) => ((Binding.name (Sign.base_name (name_of_thm intr)), []), subst_atomic rlzpreds' (Logic.unvarify rintr))) diff -r 43a12fc76f48 -r 747c95f7bb7e src/HOL/Tools/inductive_set_package.ML --- a/src/HOL/Tools/inductive_set_package.ML Fri Jan 09 09:49:01 2009 -0800 +++ b/src/HOL/Tools/inductive_set_package.ML Fri Jan 09 19:41:33 2009 +0100 @@ -20,7 +20,7 @@ (Binding.T * string option * mixfix) list -> (Binding.T * string option * mixfix) list -> (Attrib.binding * string) list -> (Facts.ref * Attrib.src list) list -> - local_theory -> InductivePackage.inductive_result * local_theory + bool -> local_theory -> InductivePackage.inductive_result * local_theory val codegen_preproc: theory -> thm list -> thm list val setup: theory -> theory end; @@ -403,7 +403,8 @@ (**** definition of inductive sets ****) -fun add_ind_set_def {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono} +fun add_ind_set_def + {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono} cs intros monos params cnames_syn ctxt = let val thy = ProofContext.theory_of ctxt; @@ -468,7 +469,8 @@ val ({preds, intrs, elims, raw_induct, ...}, ctxt1) = InductivePackage.add_ind_def {quiet_mode = quiet_mode, verbose = verbose, kind = kind, alt_name = Binding.empty, - coind = coind, no_elim = no_elim, no_ind = no_ind, skip_mono = skip_mono} + coind = coind, no_elim = no_elim, no_ind = no_ind, + skip_mono = skip_mono, fork_mono = fork_mono} cs' intros' monos' params1 cnames_syn' ctxt; (* define inductive sets using previously defined predicates *) @@ -550,10 +552,10 @@ val ind_set_decl = InductivePackage.gen_ind_decl add_ind_set_def; val _ = - OuterSyntax.local_theory "inductive_set" "define inductive sets" K.thy_decl (ind_set_decl false); + OuterSyntax.local_theory' "inductive_set" "define inductive sets" K.thy_decl (ind_set_decl false); val _ = - OuterSyntax.local_theory "coinductive_set" "define coinductive sets" K.thy_decl (ind_set_decl true); + OuterSyntax.local_theory' "coinductive_set" "define coinductive sets" K.thy_decl (ind_set_decl true); end;