src/HOL/Tools/induct_method.ML

 struct
 
 
 (* 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
   in ind_rule thy (intern (Theory.sign_of thy) name) end;
 

       (case opt_kind_name of Some kind_name => kind_name | None =>
         (case try (#1 o Term.dest_Type o Term.type_of o #2 o hd) insts of
           Some name => (Type, name)
         | 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)]
       | prep_inst ((_ $ x), (None, y)) = [(cert x, cert y)]

 fun induct ctxt =
   Args.and_list inst -- Scan.option (Scan.lift (kind -- Args.name))
   >> (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 *)
 
 val setup = [Method.add_methods [induct_method]];