author wenzelm Tue Feb 29 23:06:20 2000 +0100 (2000-02-29) changeset 8316 74639e19eca0 parent 8315 c9b4f1c47816 child 8317 a959dfeeacc6
```     1.1 --- a/src/HOL/Tools/inductive_package.ML	Tue Feb 29 20:51:43 2000 +0100
1.2 +++ b/src/HOL/Tools/inductive_package.ML	Tue Feb 29 23:06:20 2000 +0100
1.3 @@ -18,7 +18,7 @@
1.4  current theory!
1.5
1.6    Introduction rules have the form
1.7 -  [| ti:M(Sj), ..., P(x), ... |] ==> t: Sk |]
1.8 +  [| ti:M(Sj), ..., P(x), ... |] ==> t: Sk
1.9    where M is some monotone operator (usually the identity)
1.10    P(x) is any side condition on the free variables
1.11    ti, t are any terms
1.12 @@ -382,6 +382,40 @@
1.13
1.14
1.15
1.16 +(** prepare cases and induct rules **)
1.17 +
1.18 +(*
1.19 +  transform mutual rule:
1.20 +    HH ==> (x1:A1 --> P1 x1) & ... & (xn:An --> Pn xn)
1.21 +  into i-th projection:
1.22 +    xi:Ai ==> HH ==> Pi xi
1.23 +*)
1.24 +
1.25 +fun project_rules [name] rule = [(name, rule)]
1.26 +  | project_rules names mutual_rule =
1.27 +      let
1.28 +        val n = length names;
1.29 +        fun proj i =
1.30 +          (if i < n then (fn th => th RS conjunct1) else I)
1.31 +            (Library.funpow (i - 1) (fn th => th RS conjunct2) mutual_rule)
1.32 +            RS mp |> Thm.permute_prems 0 ~1 |> Drule.standard;
1.33 +      in names ~~ map proj (1 upto n) end;
1.34 +
1.35 +fun add_cases_induct no_elim no_ind names elims induct =
1.36 +  let
1.37 +    val cases_specs =
1.38 +      if no_elim then []
1.39 +      else map2 (fn (name, elim) => (("", elim), [InductMethod.cases_set_global name]))
1.40 +        (names, elims);
1.41 +
1.42 +    val induct_specs =
1.43 +      if no_ind then []
1.44 +      else map (fn (name, th) => (("", th), [InductMethod.induct_set_global name]))
1.45 +        (project_rules names induct);
1.46 +  in PureThy.add_thms (cases_specs @ induct_specs) end;
1.47 +
1.48 +
1.49 +
1.50  (*** proofs for (co)inductive sets ***)
1.51
1.52  (** prove monotonicity **)
1.53 @@ -744,18 +778,6 @@
1.54
1.55  (** introduction of (co)inductive sets **)
1.56
1.57 -fun add_cases_induct no_elim no_ind names elims induct =
1.58 -  let
1.59 -    val cases_specs =
1.60 -      if no_elim then []
1.61 -      else map2 (fn (name, elim) => (("", elim), [InductMethod.cases_set_global name]))
1.62 -        (names, elims);
1.63 -    val induct_specs =
1.64 -      if no_ind then []
1.65 -      else map (fn name => (("", induct), [InductMethod.induct_set_global name])) names;
1.66 -  in PureThy.add_thms (cases_specs @ induct_specs) end;
1.67 -
1.68 -
1.69  fun add_inductive_i verbose declare_consts alt_name coind no_elim no_ind cs
1.70      atts intros monos con_defs thy =
1.71    let
```