# HG changeset patch
# User wenzelm
# Date 924277626 -7200
# Node ID 583add9799c37bd51e07fd58e446b3eca6ed63f9
# Parent  931fc1daa8b1b987db7e8b1180c3dc1e78fa2865
may specify induction predicates as well;

diff -r 931fc1daa8b1 -r 583add9799c3 src/HOL/Tools/induct_method.ML
--- a/src/HOL/Tools/induct_method.ML	Fri Apr 16 17:46:02 1999 +0200
+++ b/src/HOL/Tools/induct_method.ML	Fri Apr 16 17:47:06 1999 +0200
@@ -3,10 +3,6 @@
     Author:     Markus Wenzel, TU Muenchen
 
 Proof by induction on types / set / functions.
-
-TODO:
-  - induct vs. coinduct (!?);
-  - use of 'function' (!?);
 *)
 
 signature INDUCT_METHOD =
@@ -31,39 +27,52 @@
     --| Args.$$$ ":";
 
 
+(* induct_rule *)
+
+fun kind_rule Type = (#induction oo DatatypePackage.datatype_info, 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);
+
+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;
+
+
 (* induct_tac *)
 
-fun induct_rule thy Type name = #induction (DatatypePackage.datatype_info thy name)
-  | induct_rule thy Set name = #induct (#2 (InductivePackage.get_inductive thy name))
-  | induct_rule thy Function name = #induct (RecdefPackage.get_recdef thy name);
-
-
-fun induct_tac thy xs opt_kind_name i state =
+fun induct_tac thy insts opt_kind_name i state =
   let
     val (kind, name) =
       (case opt_kind_name of Some kind_name => kind_name | None =>
-        (case try (#1 o Term.dest_Type o Term.type_of o hd) xs of
+        (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);
 
-    fun inst_rule () =
-      let
-        val cert = Thm.cterm_of (Sign.merge (pairself Thm.sign_of_thm (state, rule)));
-        fun rule_var (_ $ x) = cert x
-          | rule_var _ = raise THM ("Malformed induction rule", 0, [rule]);
-        val rule_preds = DatatypeAux.dest_conj (HOLogic.dest_Trueprop (Thm.concl_of rule));
-      in Drule.cterm_instantiate (map rule_var rule_preds ~~ map cert xs) rule end;
-  in Tactic.rtac (if null xs then rule else inst_rule ()) i state end;
+
+    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)]
+      | prep_inst _ = raise THM ("Malformed induction rule", 0, [rule]);
+
+    val prep_insts = flat o map2 prep_inst;
+
+    val inst_rule =
+      if null insts then rule
+      else Drule.cterm_instantiate (prep_insts
+        (DatatypeAux.dest_conj (HOLogic.dest_Trueprop (Thm.concl_of rule)), insts)) rule;
+  in Tactic.rtac inst_rule i state end;
 
 
 (* induct_method *)
 
 val term = Scan.unless (Scan.lift kind) Args.local_term;
+val inst = term -- term >> (apfst Some) || term >> pair None;
 
 fun induct ctxt =
-  Scan.repeat term -- Scan.option (Scan.lift (kind -- Args.name))
-  >> (fn (xs, k) => Method.METHOD0 (FIRSTGOAL (induct_tac (ProofContext.theory_of ctxt) xs k)));
+  Args.and_list inst -- Scan.option (Scan.lift (kind -- Args.name))
+  >> (fn (is, k) => Method.METHOD0 (FIRSTGOAL (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");