# HG changeset patch # User wenzelm # Date 936720633 -7200 # Node ID 930e5947562d7d8c4b7651b01bbf9d41ab5242fe # Parent 85cf7fa5b138bf0e6521adbdd428d25a8b789966 rule option; diff -r 85cf7fa5b138 -r 930e5947562d src/HOL/Tools/induct_method.ML --- a/src/HOL/Tools/induct_method.ML Tue Sep 07 18:10:03 1999 +0200 +++ b/src/HOL/Tools/induct_method.ML Tue Sep 07 18:10:33 1999 +0200 @@ -16,22 +16,23 @@ (* type induct_kind *) -datatype induct_kind = Type | Set | Function; +datatype induct_kind = Type | Set | Function | Rule; -val typeN = "type"; -val setN = "set"; -val functionN = "function"; +val kind_name = + Args.$$$ "type" >> K Type || + Args.$$$ "set" >> K Set || + Args.$$$ "function" >> K Function || + Args.$$$ "rule" >> K Rule; -val kind = - (Args.$$$ typeN >> K Type || Args.$$$ setN >> K Set || Args.$$$ functionN >> K Function) - --| Args.$$$ ":"; +val kind = kind_name --| Args.$$$ ":"; (* induct_rule *) fun kind_rule Type = (#induction oo DatatypePackage.datatype_info_err, Sign.intern_tycon) | kind_rule Set = ((#induct o #2) oo InductivePackage.get_inductive, Sign.intern_const) - | kind_rule Function = (#induct oo RecdefPackage.get_recdef, Sign.intern_const); + | kind_rule Function = (#induct oo RecdefPackage.get_recdef, Sign.intern_const) + | kind_rule Rule = (PureThy.get_thm, K I); fun induct_rule thy kind name = let val (ind_rule, intern) = kind_rule kind @@ -49,7 +50,6 @@ | None => error "Unable to figure out induction rule")); val rule = Drule.incr_indexes_wrt [] [] [] [state] (induct_rule thy kind name); - val cert = Thm.cterm_of (Sign.merge (pairself Thm.sign_of_thm (state, rule))); fun prep_inst ((P $ x), (Some Q, y)) = [(cert P, cert Q), (cert x, cert y)] @@ -75,7 +75,7 @@ >> (fn (is, k) => Method.METHOD (FIRSTGOAL o induct_tac (ProofContext.theory_of ctxt) is k)); fun induct_meth src ctxt = #2 (Method.syntax (induct ctxt) ctxt src); -val induct_method = ("induct", induct_meth, "induction on types / sets / functions"); +val induct_method = ("induct", induct_meth, "induction on types, sets, functions etc."); (* theory setup *)