# HG changeset patch
# User wenzelm
# Date 951861980 -3600
# Node ID 74639e19eca09aeb74345ba4a19dcb7d821bd776
# Parent  c9b4f1c4781694606420fdb19088ef9b8295f16e
add_cases_induct: project_rules accomodates mutual induction;

diff -r c9b4f1c47816 -r 74639e19eca0 src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Tue Feb 29 20:51:43 2000 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Tue Feb 29 23:06:20 2000 +0100
@@ -18,7 +18,7 @@
 current theory!
 
   Introduction rules have the form
-  [| ti:M(Sj), ..., P(x), ... |] ==> t: Sk |]
+  [| ti:M(Sj), ..., P(x), ... |] ==> t: Sk
   where M is some monotone operator (usually the identity)
   P(x) is any side condition on the free variables
   ti, t are any terms
@@ -382,6 +382,40 @@
 
 
 
+(** prepare cases and induct rules **)
+
+(*
+  transform mutual rule:
+    HH ==> (x1:A1 --> P1 x1) & ... & (xn:An --> Pn xn)
+  into i-th projection:
+    xi:Ai ==> HH ==> Pi xi
+*)
+
+fun project_rules [name] rule = [(name, rule)]
+  | project_rules names mutual_rule =
+      let
+        val n = length names;
+        fun proj i =
+          (if i < n then (fn th => th RS conjunct1) else I)
+            (Library.funpow (i - 1) (fn th => th RS conjunct2) mutual_rule)
+            RS mp |> Thm.permute_prems 0 ~1 |> Drule.standard;
+      in names ~~ map proj (1 upto n) end;
+
+fun add_cases_induct no_elim no_ind names elims induct =
+  let
+    val cases_specs =
+      if no_elim then []
+      else map2 (fn (name, elim) => (("", elim), [InductMethod.cases_set_global name]))
+        (names, elims);
+
+    val induct_specs =
+      if no_ind then []
+      else map (fn (name, th) => (("", th), [InductMethod.induct_set_global name]))
+        (project_rules names induct);
+  in PureThy.add_thms (cases_specs @ induct_specs) end;
+
+
+
 (*** proofs for (co)inductive sets ***)
 
 (** prove monotonicity **)
@@ -744,18 +778,6 @@
 
 (** introduction of (co)inductive sets **)
 
-fun add_cases_induct no_elim no_ind names elims induct =
-  let
-    val cases_specs =
-      if no_elim then []
-      else map2 (fn (name, elim) => (("", elim), [InductMethod.cases_set_global name]))
-        (names, elims);
-    val induct_specs =
-      if no_ind then []
-      else map (fn name => (("", induct), [InductMethod.induct_set_global name])) names;
-  in PureThy.add_thms (cases_specs @ induct_specs) end;
-
-
 fun add_inductive_i verbose declare_consts alt_name coind no_elim no_ind cs
     atts intros monos con_defs thy =
   let