add_cases_induct: project_rules accomodates mutual induction;
authorwenzelm
Tue Feb 29 23:06:20 2000 +0100 (2000-02-29)
changeset 831674639e19eca0
parent 8315 c9b4f1c47816
child 8317 a959dfeeacc6
add_cases_induct: project_rules accomodates mutual induction;
src/HOL/Tools/inductive_package.ML
     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