# HG changeset patch # User wenzelm # Date 966269694 -7200 # Node ID 65ee72db023611c4decd8165feefab9fde8a91ea # Parent 938a99cc55f7016fe2eeddba518c3e2f20c36223 raplaced "intrs" by "intrs" (new-style only); improved new-style interface to mk_cases; diff -r 938a99cc55f7 -r 65ee72db0236 src/HOL/Tools/inductive_package.ML --- a/src/HOL/Tools/inductive_package.ML Mon Aug 14 18:13:42 2000 +0200 +++ b/src/HOL/Tools/inductive_package.ML Mon Aug 14 18:14:54 2000 +0200 @@ -3,7 +3,7 @@ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Stefan Berghofer, TU Muenchen Copyright 1994 University of Cambridge - 1998 TU Muenchen + 1998 TU Muenchen (Co)Inductive Definition module for HOL. @@ -49,9 +49,9 @@ (xstring * Args.src list) list -> theory -> theory * {defs: thm list, elims: thm list, raw_induct: thm, induct: thm, intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm} - val inductive_cases: (((bstring * Args.src list) * xstring) * string list) * Comment.text + val inductive_cases: ((bstring * Args.src list) * string list) * Comment.text -> theory -> theory - val inductive_cases_i: (((bstring * theory attribute list) * string) * term list) * Comment.text + val inductive_cases_i: ((bstring * theory attribute list) * term list) * Comment.text -> theory -> theory val setup: (theory -> theory) list end; @@ -59,6 +59,7 @@ structure InductivePackage: INDUCTIVE_PACKAGE = struct + (*** theory data ***) (* data kind 'HOL/inductive' *) @@ -92,6 +93,11 @@ fun get_inductive thy name = Symtab.lookup (fst (InductiveData.get thy), name); +fun the_inductive thy name = + (case get_inductive thy name of + None => error ("Unknown (co)inductive set " ^ quote name) + | Some info => info); + fun put_inductives names info thy = let fun upd ((tab, monos), name) = (Symtab.update_new ((name, info), tab), monos); @@ -291,7 +297,7 @@ in map mk_elim (cs ~~ cTs) end; - + (** premises and conclusions of induction rules **) @@ -331,7 +337,7 @@ fun mk_prem (s, prems) = (case subst s of (_, Some (t, u)) => t :: u :: prems | (t, _) => t :: prems); - + val Const ("op :", _) $ t $ u = HOLogic.dest_Trueprop (Logic.strip_imp_concl r) @@ -472,47 +478,48 @@ (** derivation of simplified elimination rules **) (*Applies freeness of the given constructors, which *must* be unfolded by - the given defs. Cannot simply use the local con_defs because con_defs=[] + the given defs. Cannot simply use the local con_defs because con_defs=[] for inference systems. *) (*cprop should have the form t:Si where Si is an inductive set*) -fun mk_cases_i solved elims ss cprop = + +val mk_cases_err = "mk_cases: proposition not of form 't : S_i'"; + +fun mk_cases_i elims ss cprop = let val prem = Thm.assume cprop; - val tac = TRYALL (InductMethod.simp_case_tac solved ss) THEN prune_params_tac; + val tac = ALLGOALS (InductMethod.simp_case_tac false ss) THEN prune_params_tac; fun mk_elim rl = Drule.standard (Tactic.rule_by_tactic tac (prem RS rl)); in (case get_first (try mk_elim) elims of Some r => r | None => error (Pretty.string_of (Pretty.block - [Pretty.str "mk_cases: proposition not of form 't : S_i'", Pretty.fbrk, - Display.pretty_cterm cprop]))) + [Pretty.str mk_cases_err, Pretty.fbrk, Display.pretty_cterm cprop]))) end; fun mk_cases elims s = - mk_cases_i false elims (simpset()) (Thm.read_cterm (Thm.sign_of_thm (hd elims)) (s, propT)); + mk_cases_i elims (simpset()) (Thm.read_cterm (Thm.sign_of_thm (hd elims)) (s, propT)); + +fun smart_mk_cases thy ss cprop = + let + val c = #1 (Term.dest_Const (Term.head_of (#2 (HOLogic.dest_mem (HOLogic.dest_Trueprop + (Logic.strip_imp_concl (Thm.term_of cprop))))))) handle TERM _ => error mk_cases_err; + val (_, {elims, ...}) = the_inductive thy c; + in mk_cases_i elims ss cprop end; (* inductive_cases(_i) *) fun gen_inductive_cases prep_att prep_const prep_prop - ((((name, raw_atts), raw_set), raw_props), comment) thy = - let val sign = Theory.sign_of thy; - in (case get_inductive thy (prep_const sign raw_set) of - None => error ("Unknown (co)inductive set " ^ quote name) - | Some (_, {elims, ...}) => - let - val atts = map (prep_att thy) raw_atts; - val cprops = map - (Thm.cterm_of sign o prep_prop (ProofContext.init thy)) raw_props; - val thms = map - (mk_cases_i true elims (Simplifier.simpset_of thy)) cprops; - in - thy |> IsarThy.have_theorems_i - [(((name, atts), map Thm.no_attributes thms), comment)] - end) - end; + (((name, raw_atts), raw_props), comment) thy = + let + val ss = Simplifier.simpset_of thy; + val sign = Theory.sign_of thy; + val cprops = map (Thm.cterm_of sign o prep_prop (ProofContext.init thy)) raw_props; + val atts = map (prep_att thy) raw_atts; + val thms = map (smart_mk_cases thy ss) cprops; + in thy |> IsarThy.have_theorems_i [(((name, atts), map Thm.no_attributes thms), comment)] end; val inductive_cases = gen_inductive_cases Attrib.global_attribute Sign.intern_const ProofContext.read_prop; @@ -520,6 +527,18 @@ val inductive_cases_i = gen_inductive_cases (K I) (K I) ProofContext.cert_prop; +(* mk_cases_meth *) + +fun mk_cases_meth (ctxt, raw_props) = + let + val thy = ProofContext.theory_of ctxt; + val ss = Simplifier.get_local_simpset ctxt; + val cprops = map (Thm.cterm_of (Theory.sign_of thy) o ProofContext.read_prop ctxt) raw_props; + in Method.erule (map (smart_mk_cases thy ss) cprops) end; + +val mk_cases_args = Method.syntax (Scan.lift (Scan.repeat1 Args.name)); + + (** prove induction rule **) @@ -662,7 +681,7 @@ val mono = prove_mono setT fp_fun monos thy' in - (thy', mono, fp_def, rec_sets_defs, rec_const, sumT) + (thy', mono, fp_def, rec_sets_defs, rec_const, sumT) end; fun add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs @@ -693,7 +712,7 @@ val (thy'', [intrs']) = thy' - |> PureThy.add_thmss [(("intrs", intrs), atts)] + |> PureThy.add_thmss [(("intros", intrs), atts)] |>> (#1 o PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts)) |>> (if no_elim then I else #1 o PureThy.add_thmss [(("elims", elims), [])]) |>> (if no_ind then I else #1 o PureThy.add_thms @@ -728,16 +747,14 @@ val (elim_ts, elim_cases) = Library.split_list (mk_elims cs cTs params intr_ts intr_names); val (_, ind_prems, mutual_ind_concl) = mk_indrule cs cTs params intr_ts; val ind_t = Logic.list_implies (ind_prems, mutual_ind_concl); - - val thy'' = + + val (thy'', [intrs, raw_elims]) = thy' - |> (#1 o PureThy.add_axiomss_i [(("intrs", intr_ts), atts), (("raw_elims", elim_ts), [])]) - |> (if coind then I else + |> PureThy.add_axiomss_i [(("intros", intr_ts), atts), (("raw_elims", elim_ts), [])] + |>> (if coind then I else #1 o PureThy.add_axioms_i [(("raw_induct", ind_t), [apsnd (standard o split_rule)])]); - val intrs = PureThy.get_thms thy'' "intrs"; - val elims = map2 (fn (th, cases) => RuleCases.name cases th) - (PureThy.get_thms thy'' "raw_elims", elim_cases); + val elims = map2 (fn (th, cases) => RuleCases.name cases th) (raw_elims, elim_cases); val raw_induct = if coind then Drule.asm_rl else PureThy.get_thm thy'' "raw_induct"; val induct = if coind orelse length cs > 1 then raw_induct else standard (raw_induct RSN (2, rev_mp)); @@ -828,6 +845,8 @@ val setup = [InductiveData.init, + Method.add_methods [("mk_cases_tac", mk_cases_meth oo mk_cases_args, + "dynamic case analysis on sets")], Attrib.add_attributes [("mono", mono_attr, "monotonicity rule")]]; @@ -840,7 +859,7 @@ fun ind_decl coind = (Scan.repeat1 P.term --| P.marg_comment) -- - (P.$$$ "intrs" |-- + (P.$$$ "intros" |-- P.!!! (P.opt_attribs -- Scan.repeat1 (P.opt_thm_name ":" -- P.prop --| P.marg_comment))) -- Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1 --| P.marg_comment) [] -- Scan.optional (P.$$$ "con_defs" |-- P.!!! P.xthms1 --| P.marg_comment) [] @@ -854,14 +873,14 @@ val ind_cases = - P.opt_thm_name "=" -- P.xname --| P.$$$ ":" -- Scan.repeat1 P.prop -- P.marg_comment + P.opt_thm_name "=" -- Scan.repeat1 P.prop -- P.marg_comment >> (Toplevel.theory o inductive_cases); val inductive_casesP = - OuterSyntax.command "inductive_cases" "create simplified instances of elimination rules" - K.thy_decl ind_cases; + OuterSyntax.improper_command "inductive_cases" + "create simplified instances of elimination rules (improper)" K.thy_script ind_cases; -val _ = OuterSyntax.add_keywords ["intrs", "monos", "con_defs"]; +val _ = OuterSyntax.add_keywords ["intros", "monos", "con_defs", "of"]; val _ = OuterSyntax.add_parsers [inductiveP, coinductiveP, inductive_casesP]; end;