1.1 --- a/src/HOL/Tools/inductive_package.ML	Mon Jan 29 10:28:00 2001 +0100
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Mon Jan 29 13:26:04 2001 +0100
     1.3 @@ -33,6 +33,7 @@
     1.4  sig
     1.5    val quiet_mode: bool ref
     1.6    val unify_consts: Sign.sg -> term list -> term list -> term list * term list
     1.7 +  val split_rule_vars: term list -> thm -> thm
     1.8    val get_inductive: theory -> string -> ({names: string list, coind: bool} *
     1.9      {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
    1.10       intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}) option
    1.11 @@ -228,6 +229,54 @@
    1.12        Abs ("y", cT, mk_inj cs sumT c (Bound 0)) $ t
    1.13    end;
    1.14  
    1.15 +(** proper splitting **)
    1.16 +
    1.17 +fun prod_factors p (Const ("Pair", _) $ t $ u) =
    1.18 +      p :: prod_factors (1::p) t @ prod_factors (2::p) u
    1.19 +  | prod_factors p _ = [];
    1.20 +
    1.21 +fun mg_prod_factors ts (fs, t $ u) = if t mem ts then
    1.22 +        let val f = prod_factors [] u
    1.23 +        in overwrite (fs, (t, f inter if_none (assoc (fs, t)) f)) end
    1.24 +      else mg_prod_factors ts (mg_prod_factors ts (fs, t), u)
    1.25 +  | mg_prod_factors ts (fs, Abs (_, _, t)) = mg_prod_factors ts (fs, t)
    1.26 +  | mg_prod_factors ts (fs, _) = fs;
    1.27 +
    1.28 +fun prodT_factors p ps (T as Type ("*", [T1, T2])) =
    1.29 +      if p mem ps then prodT_factors (1::p) ps T1 @ prodT_factors (2::p) ps T2
    1.30 +      else [T]
    1.31 +  | prodT_factors _ _ T = [T];
    1.32 +
    1.33 +fun ap_split p ps (Type ("*", [T1, T2])) T3 u =
    1.34 +      if p mem ps then HOLogic.split_const (T1, T2, T3) $
    1.35 +        Abs ("v", T1, ap_split (2::p) ps T2 T3 (ap_split (1::p) ps T1
    1.36 +          (prodT_factors (2::p) ps T2 ---> T3) (incr_boundvars 1 u) $ Bound 0))
    1.37 +      else u
    1.38 +  | ap_split _ _ _ _ u =  u;
    1.39 +
    1.40 +fun mk_tuple p ps (Type ("*", [T1, T2])) (tms as t::_) =
    1.41 +      if p mem ps then HOLogic.mk_prod (mk_tuple (1::p) ps T1 tms, 
    1.42 +        mk_tuple (2::p) ps T2 (drop (length (prodT_factors (1::p) ps T1), tms)))
    1.43 +      else t
    1.44 +  | mk_tuple _ _ _ (t::_) = t;
    1.45 +
    1.46 +fun split_rule_var' ((t as Var (v, Type ("fun", [T1, T2])), ps), rl) =
    1.47 +      let val T' = prodT_factors [] ps T1 ---> T2
    1.48 +          val newt = ap_split [] ps T1 T2 (Var (v, T'))
    1.49 +          val cterm = Thm.cterm_of (#sign (rep_thm rl))
    1.50 +      in
    1.51 +          instantiate ([], [(cterm t, cterm newt)]) rl
    1.52 +      end
    1.53 +  | split_rule_var' (_, rl) = rl;
    1.54 +
    1.55 +val remove_split = rewrite_rule [split_conv RS eq_reflection];
    1.56 +
    1.57 +fun split_rule_vars vs rl = standard (remove_split (foldr split_rule_var'
    1.58 +  (mg_prod_factors vs ([], #prop (rep_thm rl)), rl)));
    1.59 +
    1.60 +fun split_rule vs rl = standard (remove_split (foldr split_rule_var'
    1.61 +  (mapfilter (fn (t as Var ((a, _), _)) =>
    1.62 +    apsome (pair t) (assoc (vs, a))) (term_vars (#prop (rep_thm rl))), rl)));
    1.63  
    1.64  
    1.65  (** process rules **)
    1.66 @@ -361,15 +410,17 @@
    1.67        end;
    1.68  
    1.69      val ind_prems = map mk_ind_prem intr_ts;
    1.70 +    val factors = foldl (mg_prod_factors preds) ([], ind_prems);
    1.71  
    1.72      (* make conclusions for induction rules *)
    1.73  
    1.74      fun mk_ind_concl ((c, P), (ts, x)) =
    1.75        let val T = HOLogic.dest_setT (fastype_of c);
    1.76 -          val Ts = HOLogic.prodT_factors T;
    1.77 +          val ps = if_none (assoc (factors, P)) [];
    1.78 +          val Ts = prodT_factors [] ps T;
    1.79            val (frees, x') = foldr (fn (T', (fs, s)) =>
    1.80              ((Free (s, T'))::fs, bump_string s)) (Ts, ([], x));
    1.81 -          val tuple = HOLogic.mk_tuple T frees;
    1.82 +          val tuple = mk_tuple [] ps T frees;
    1.83        in ((HOLogic.mk_binop "op -->"
    1.84          (HOLogic.mk_mem (tuple, c), P $ tuple))::ts, x')
    1.85        end;
    1.86 @@ -377,7 +428,8 @@
    1.87      val mutual_ind_concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
    1.88          (fst (foldr mk_ind_concl (cs ~~ preds, ([], "xa")))))
    1.89  
    1.90 -  in (preds, ind_prems, mutual_ind_concl)
    1.91 +  in (preds, ind_prems, mutual_ind_concl,
    1.92 +    map (apfst (fst o dest_Free)) factors)
    1.93    end;
    1.94  
    1.95  
    1.96 @@ -558,7 +610,8 @@
    1.97          None => []
    1.98        | Some thy' => map mk_meta_eq (PureThy.get_thms thy' "sum.cases"));
    1.99  
   1.100 -    val (preds, ind_prems, mutual_ind_concl) = mk_indrule cs cTs params intr_ts;
   1.101 +    val (preds, ind_prems, mutual_ind_concl, factors) =
   1.102 +      mk_indrule cs cTs params intr_ts;
   1.103  
   1.104      (* make predicate for instantiation of abstract induction rule *)
   1.105  
   1.106 @@ -611,7 +664,7 @@
   1.107              rewrite_goals_tac sum_case_rewrites,
   1.108              atac 1])])
   1.109  
   1.110 -  in standard (split_rule (induct RS lemma)) end;
   1.111 +  in standard (split_rule factors (induct RS lemma)) end;
   1.112  
   1.113  
   1.114