--- 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