Reimplemented parts of datatype package dealing with datatypes involving
authorberghofe
Thu Oct 10 14:26:50 2002 +0200 (2002-10-10)
changeset 1364163d1790a43ed
parent 13640 993576f4de30
child 13642 a3d97348ceb6
Reimplemented parts of datatype package dealing with datatypes involving
function types. Now also supports functions with more than one argument.
src/HOL/Tools/datatype_abs_proofs.ML
src/HOL/Tools/datatype_aux.ML
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/datatype_prop.ML
src/HOL/Tools/datatype_realizer.ML
src/HOL/Tools/datatype_rep_proofs.ML
src/HOL/Tools/primrec_package.ML
     1.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Thu Oct 10 14:23:47 2002 +0200
     1.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Thu Oct 10 14:26:50 2002 +0200
     1.3 @@ -18,31 +18,29 @@
     1.4  
     1.5  signature DATATYPE_ABS_PROOFS =
     1.6  sig
     1.7 -  val prove_casedist_thms : string list -> (int * (string * DatatypeAux.dtyp list *
     1.8 -    (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
     1.9 -      thm -> theory attribute list -> theory -> theory * thm list
    1.10 -  val prove_primrec_thms : bool -> string list -> (int * (string * DatatypeAux.dtyp list *
    1.11 -    (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
    1.12 +  val prove_casedist_thms : string list ->
    1.13 +    DatatypeAux.descr list -> (string * sort) list -> thm ->
    1.14 +    theory attribute list -> theory -> theory * thm list
    1.15 +  val prove_primrec_thms : bool -> string list ->
    1.16 +    DatatypeAux.descr list -> (string * sort) list ->
    1.17        DatatypeAux.datatype_info Symtab.table -> thm list list -> thm list list ->
    1.18          simpset -> thm -> theory -> theory * (string list * thm list)
    1.19 -  val prove_case_thms : bool -> string list -> (int * (string * DatatypeAux.dtyp list *
    1.20 -    (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
    1.21 +  val prove_case_thms : bool -> string list ->
    1.22 +    DatatypeAux.descr list -> (string * sort) list ->
    1.23        string list -> thm list -> theory -> theory * (thm list list * string list)
    1.24 -  val prove_split_thms : string list -> (int * (string * DatatypeAux.dtyp list *
    1.25 -    (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
    1.26 +  val prove_split_thms : string list ->
    1.27 +    DatatypeAux.descr list -> (string * sort) list ->
    1.28        thm list list -> thm list list -> thm list -> thm list list -> theory ->
    1.29          theory * (thm * thm) list
    1.30 -  val prove_size_thms : bool -> string list -> (int * (string * DatatypeAux.dtyp list *
    1.31 -    (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
    1.32 +  val prove_size_thms : bool -> string list ->
    1.33 +    DatatypeAux.descr list -> (string * sort) list ->
    1.34        string list -> thm list -> theory -> theory * thm list
    1.35 -  val prove_nchotomys : string list -> (int * (string * DatatypeAux.dtyp list *
    1.36 -    (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
    1.37 -      thm list -> theory -> theory * thm list
    1.38 -  val prove_weak_case_congs : string list -> (int * (string * DatatypeAux.dtyp list *
    1.39 -    (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
    1.40 -      theory -> theory * thm list
    1.41 -  val prove_case_congs : string list -> (int * (string * DatatypeAux.dtyp list *
    1.42 -    (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
    1.43 +  val prove_nchotomys : string list -> DatatypeAux.descr list ->
    1.44 +    (string * sort) list -> thm list -> theory -> theory * thm list
    1.45 +  val prove_weak_case_congs : string list -> DatatypeAux.descr list ->
    1.46 +    (string * sort) list -> theory -> theory * thm list
    1.47 +  val prove_case_congs : string list ->
    1.48 +    DatatypeAux.descr list -> (string * sort) list ->
    1.49        thm list -> thm list list -> theory -> theory * thm list
    1.50  end;
    1.51  
    1.52 @@ -51,10 +49,6 @@
    1.53  
    1.54  open DatatypeAux;
    1.55  
    1.56 -val thin = read_instantiate_sg (Theory.sign_of Set.thy) [("V", "?X : ?Y")] thin_rl;
    1.57 -
    1.58 -val (_ $ (_ $ (_ $ (distinct_f $ _) $ _))) = hd (prems_of distinct_lemma);
    1.59 -
    1.60  (************************ case distinction theorems ***************************)
    1.61  
    1.62  fun prove_casedist_thms new_type_names descr sorts induct case_names_exhausts thy =
    1.63 @@ -99,8 +93,6 @@
    1.64    let
    1.65      val _ = message "Constructing primrec combinators ...";
    1.66  
    1.67 -    val fun_rel_comp_name = "Relation.fun_rel_comp";
    1.68 -
    1.69      val big_name = space_implode "_" new_type_names;
    1.70      val thy0 = add_path flat_names big_name thy;
    1.71  
    1.72 @@ -126,9 +118,8 @@
    1.73            val Ts = map (typ_of_dtyp descr' sorts) cargs;
    1.74            val recs = filter (is_rec_type o fst) (cargs ~~ Ts);
    1.75  
    1.76 -          fun mk_argT (DtRec k, _) = nth_elem (k, rec_result_Ts)
    1.77 -            | mk_argT (DtType ("fun", [_, DtRec k]), Type ("fun", [T, _])) =
    1.78 -               T --> nth_elem (k, rec_result_Ts);
    1.79 +          fun mk_argT (dt, T) =
    1.80 +            binder_types T ---> nth_elem (body_index dt, rec_result_Ts);
    1.81  
    1.82            val argTs = Ts @ map mk_argT recs
    1.83          in argTs ---> nth_elem (i, rec_result_Ts)
    1.84 @@ -148,20 +139,17 @@
    1.85        let
    1.86          fun mk_prem ((dt, U), (j, k, prems, t1s, t2s)) =
    1.87            let val free1 = mk_Free "x" U j
    1.88 -          in (case (dt, U) of
    1.89 -             (DtRec m, _) =>
    1.90 -               let val free2 = mk_Free "y" (nth_elem (m, rec_result_Ts)) k
    1.91 -               in (j + 1, k + 1, (HOLogic.mk_Trueprop (HOLogic.mk_mem
    1.92 -                 (HOLogic.mk_prod (free1, free2), nth_elem (m, rec_sets))))::prems,
    1.93 +          in (case (strip_dtyp dt, strip_type U) of
    1.94 +             ((_, DtRec m), (Us, _)) =>
    1.95 +               let
    1.96 +                 val free2 = mk_Free "y" (Us ---> nth_elem (m, rec_result_Ts)) k;
    1.97 +                 val i = length Us
    1.98 +               in (j + 1, k + 1, HOLogic.mk_Trueprop (HOLogic.list_all
    1.99 +                     (map (pair "x") Us, HOLogic.mk_mem (HOLogic.mk_prod
   1.100 +                       (app_bnds free1 i, app_bnds free2 i),
   1.101 +                         nth_elem (m, rec_sets)))) :: prems,
   1.102                     free1::t1s, free2::t2s)
   1.103                 end
   1.104 -           | (DtType ("fun", [_, DtRec m]), U' as Type ("fun", [T', _])) =>
   1.105 -               let val free2 = mk_Free "y" (T' --> nth_elem (m, rec_result_Ts)) k
   1.106 -               in (j + 1, k + 1, (HOLogic.mk_Trueprop (HOLogic.mk_mem (free2,
   1.107 -                 Const (fun_rel_comp_name, [U', snd (strip_type (nth_elem (m, rec_set_Ts)))] --->
   1.108 -                   HOLogic.mk_setT (T' --> nth_elem (m, rec_result_Ts))) $
   1.109 -                     free1 $ nth_elem (m, rec_sets))))::prems, free1::t1s, free2::t2s)
   1.110 -               end
   1.111             | _ => (j + 1, k, prems, free1::t1s, t2s))
   1.112            end;
   1.113  
   1.114 @@ -180,7 +168,7 @@
   1.115      val (thy1, {intrs = rec_intrs, elims = rec_elims, ...}) =
   1.116        setmp InductivePackage.quiet_mode (!quiet_mode)
   1.117          (InductivePackage.add_inductive_i false true big_rec_name' false false true
   1.118 -           rec_sets (map (fn x => (("", x), [])) rec_intr_ts) [fun_rel_comp_mono]) thy0;
   1.119 +           rec_sets (map (fn x => (("", x), [])) rec_intr_ts) []) thy0;
   1.120  
   1.121      (* prove uniqueness and termination of primrec combinators *)
   1.122  
   1.123 @@ -202,16 +190,14 @@
   1.124              val k = length (filter is_rec_type cargs)
   1.125  
   1.126            in (EVERY [DETERM tac,
   1.127 -                REPEAT (dtac fun_rel_comp_unique 1),
   1.128                  REPEAT (etac ex1E 1), rtac ex1I 1,
   1.129                  DEPTH_SOLVE_1 (ares_tac [intr] 1),
   1.130 -                REPEAT_DETERM_N k (etac thin 1),
   1.131 +                REPEAT_DETERM_N k (etac thin_rl 1 THEN rotate_tac 1 1),
   1.132                  etac elim 1,
   1.133                  REPEAT_DETERM_N j distinct_tac,
   1.134                  etac Pair_inject 1, TRY (dresolve_tac inject 1),
   1.135                  REPEAT (etac conjE 1), hyp_subst_tac 1,
   1.136 -                REPEAT (etac allE 1),
   1.137 -                REPEAT (dtac mp 1 THEN atac 1),
   1.138 +                REPEAT (EVERY [etac allE 1, dtac mp 1, atac 1]),
   1.139                  TRY (hyp_subst_tac 1),
   1.140                  rtac refl 1,
   1.141                  REPEAT_DETERM_N (n - j - 1) distinct_tac],
   1.142 @@ -236,7 +222,8 @@
   1.143          val induct' = cterm_instantiate ((map cert induct_Ps) ~~
   1.144            (map cert insts)) induct;
   1.145          val (tac, _) = foldl mk_unique_tac
   1.146 -          (((rtac induct' THEN_ALL_NEW ObjectLogic.atomize_tac) 1, rec_intrs),
   1.147 +          (((rtac induct' THEN_ALL_NEW ObjectLogic.atomize_tac) 1
   1.148 +              THEN rewtac (mk_meta_eq choice_eq), rec_intrs),
   1.149              descr' ~~ rec_elims ~~ recTs ~~ rec_result_Ts);
   1.150  
   1.151        in split_conj_thm (prove_goalw_cterm []
   1.152 @@ -277,8 +264,7 @@
   1.153          [rtac the1_equality 1,
   1.154           resolve_tac rec_unique_thms 1,
   1.155           resolve_tac rec_intrs 1,
   1.156 -         rewrite_goals_tac [o_def, fun_rel_comp_def],
   1.157 -         REPEAT ((rtac CollectI 1 THEN rtac allI 1) ORELSE resolve_tac rec_total_thms 1)]))
   1.158 +         REPEAT (rtac allI 1 ORELSE resolve_tac rec_total_thms 1)]))
   1.159             (DatatypeProp.make_primrecs new_type_names descr sorts thy2)
   1.160  
   1.161    in
   1.162 @@ -302,8 +288,7 @@
   1.163      val newTs = take (length (hd descr), recTs);
   1.164      val T' = TFree (variant used "'t", HOLogic.typeS);
   1.165  
   1.166 -    fun mk_dummyT (DtRec _) = T'
   1.167 -      | mk_dummyT (DtType ("fun", [T, _])) = typ_of_dtyp descr' sorts T --> T'
   1.168 +    fun mk_dummyT dt = binder_types (typ_of_dtyp descr' sorts dt) ---> T';
   1.169  
   1.170      val case_dummy_fns = map (fn (_, (_, _, constrs)) => map (fn (_, cargs) =>
   1.171        let
   1.172 @@ -401,8 +386,9 @@
   1.173  (******************************* size functions *******************************)
   1.174  
   1.175  fun prove_size_thms flat_names new_type_names descr sorts reccomb_names primrec_thms thy =
   1.176 -  if exists (fn (_, (_, _, constrs)) => exists (fn (_, cargs) => exists
   1.177 -    (fn (DtType ("fun", [_, DtRec _])) => true | _ => false) cargs) constrs) (flat descr)
   1.178 +  if exists (fn (_, (_, _, constrs)) => exists (fn (_, cargs) => exists (fn dt =>
   1.179 +    is_rec_type dt andalso not (null (fst (strip_dtyp dt)))) cargs) constrs)
   1.180 +      (flat descr)
   1.181    then
   1.182      (thy, [])
   1.183    else
     2.1 --- a/src/HOL/Tools/datatype_aux.ML	Thu Oct 10 14:23:47 2002 +0200
     2.2 +++ b/src/HOL/Tools/datatype_aux.ML	Thu Oct 10 14:26:50 2002 +0200
     2.3 @@ -25,6 +25,9 @@
     2.4    val mk_conj : term list -> term
     2.5    val mk_disj : term list -> term
     2.6  
     2.7 +  val app_bnds : term -> int -> term
     2.8 +
     2.9 +  val cong_tac : int -> tactic
    2.10    val indtac : thm -> int -> tactic
    2.11    val exh_tac : (string -> thm) -> int -> tactic
    2.12  
    2.13 @@ -44,25 +47,21 @@
    2.14    val dtyp_of_typ : (string * string list) list -> typ -> dtyp
    2.15    val mk_Free : string -> typ -> int -> term
    2.16    val is_rec_type : dtyp -> bool
    2.17 -  val typ_of_dtyp : (int * (string * dtyp list *
    2.18 -    (string * dtyp list) list)) list -> (string * sort) list -> dtyp -> typ
    2.19 +  val typ_of_dtyp : descr -> (string * sort) list -> dtyp -> typ
    2.20    val dest_DtTFree : dtyp -> string
    2.21    val dest_DtRec : dtyp -> int
    2.22 +  val strip_dtyp : dtyp -> dtyp list * dtyp
    2.23 +  val body_index : dtyp -> int
    2.24 +  val mk_fun_dtyp : dtyp list -> dtyp -> dtyp
    2.25    val dest_TFree : typ -> string
    2.26 -  val get_nonrec_types : (int * (string * dtyp list *
    2.27 -    (string * dtyp list) list)) list -> (string * sort) list -> typ list
    2.28 -  val get_branching_types : (int * (string * dtyp list *
    2.29 -    (string * dtyp list) list)) list -> (string * sort) list -> typ list
    2.30 -  val get_rec_types : (int * (string * dtyp list *
    2.31 -    (string * dtyp list) list)) list -> (string * sort) list -> typ list
    2.32 -  val check_nonempty : (int * (string * dtyp list *
    2.33 -    (string * dtyp list) list)) list list -> unit
    2.34 +  val get_nonrec_types : descr -> (string * sort) list -> typ list
    2.35 +  val get_branching_types : descr -> (string * sort) list -> typ list
    2.36 +  val get_arities : descr -> int list
    2.37 +  val get_rec_types : descr -> (string * sort) list -> typ list
    2.38 +  val check_nonempty : descr list -> unit
    2.39    val unfold_datatypes : 
    2.40 -    Sign.sg -> (int * (string * dtyp list * (string * dtyp list) list)) list ->
    2.41 -      (string * sort) list -> datatype_info Symtab.table ->
    2.42 -        (int * (string * dtyp list * (string * dtyp list) list)) list -> int ->
    2.43 -          (int * (string * dtyp list *
    2.44 -            (string * dtyp list) list)) list list * int
    2.45 +    Sign.sg -> descr -> (string * sort) list -> datatype_info Symtab.table ->
    2.46 +      descr -> int -> descr list * int
    2.47  end;
    2.48  
    2.49  structure DatatypeAux : DATATYPE_AUX =
    2.50 @@ -105,6 +104,23 @@
    2.51  val mk_conj = foldr1 (HOLogic.mk_binop "op &");
    2.52  val mk_disj = foldr1 (HOLogic.mk_binop "op |");
    2.53  
    2.54 +fun app_bnds t i = list_comb (t, map Bound (i - 1 downto 0));
    2.55 +
    2.56 +
    2.57 +fun cong_tac i st = (case Logic.strip_assums_concl
    2.58 +  (nth_elem (i - 1, prems_of st)) of
    2.59 +    _ $ (_ $ (f $ x) $ (g $ y)) =>
    2.60 +      let
    2.61 +        val cong' = lift_rule (st, i) cong;
    2.62 +        val _ $ (_ $ (f' $ x') $ (g' $ y')) =
    2.63 +          Logic.strip_assums_concl (prop_of cong');
    2.64 +        val insts = map (pairself (cterm_of (#sign (rep_thm st))) o
    2.65 +          apsnd (curry list_abs (Logic.strip_params (concl_of cong'))) o
    2.66 +            apfst head_of) [(f', f), (g', g), (x', x), (y', y)]
    2.67 +      in compose_tac (false, cterm_instantiate insts cong', 2) i st
    2.68 +        handle THM _ => no_tac st
    2.69 +      end
    2.70 +  | _ => no_tac st);
    2.71  
    2.72  (* instantiate induction rule *)
    2.73  
    2.74 @@ -198,6 +214,14 @@
    2.75    | is_rec_type (DtRec _) = true
    2.76    | is_rec_type _ = false;
    2.77  
    2.78 +fun strip_dtyp (DtType ("fun", [T, U])) = apfst (cons T) (strip_dtyp U)
    2.79 +  | strip_dtyp T = ([], T);
    2.80 +
    2.81 +val body_index = dest_DtRec o snd o strip_dtyp;
    2.82 +
    2.83 +fun mk_fun_dtyp [] U = U
    2.84 +  | mk_fun_dtyp (T :: Ts) U = DtType ("fun", [T, mk_fun_dtyp Ts U]);
    2.85 +
    2.86  fun dest_TFree (TFree (n, _)) = n;
    2.87  
    2.88  fun name_of_typ (Type (s, Ts)) = space_implode "_"
    2.89 @@ -223,14 +247,9 @@
    2.90  (* find all non-recursive types in datatype description *)
    2.91  
    2.92  fun get_nonrec_types descr sorts =
    2.93 -  let fun add (Ts, T as DtTFree _) = T ins Ts
    2.94 -        | add (Ts, T as DtType ("fun", [_, DtRec _])) = Ts
    2.95 -        | add (Ts, T as DtType _) = T ins Ts
    2.96 -        | add (Ts, _) = Ts
    2.97 -  in map (typ_of_dtyp descr sorts) (foldl (fn (Ts, (_, (_, _, constrs))) =>
    2.98 +  map (typ_of_dtyp descr sorts) (foldl (fn (Ts, (_, (_, _, constrs))) =>
    2.99      foldl (fn (Ts', (_, cargs)) =>
   2.100 -      foldl add (Ts', cargs)) (Ts, constrs)) ([], descr))
   2.101 -  end;
   2.102 +      filter_out is_rec_type cargs union Ts') (Ts, constrs)) ([], descr));
   2.103  
   2.104  (* get all recursive types in datatype description *)
   2.105  
   2.106 @@ -239,13 +258,14 @@
   2.107  
   2.108  (* get all branching types *)
   2.109  
   2.110 -fun get_branching_types descr sorts = 
   2.111 -  let fun add (Ts, DtType ("fun", [T, DtRec _])) = T ins Ts
   2.112 -        | add (Ts, _) = Ts
   2.113 -  in map (typ_of_dtyp descr sorts) (foldl (fn (Ts, (_, (_, _, constrs))) =>
   2.114 -    foldl (fn (Ts', (_, cargs)) =>
   2.115 -      foldl add (Ts', cargs)) (Ts, constrs)) ([], descr))
   2.116 -  end;
   2.117 +fun get_branching_types descr sorts =
   2.118 +  map (typ_of_dtyp descr sorts) (foldl (fn (Ts, (_, (_, _, constrs))) =>
   2.119 +    foldl (fn (Ts', (_, cargs)) => foldr op union (map (fst o strip_dtyp)
   2.120 +      cargs, Ts')) (Ts, constrs)) ([], descr));
   2.121 +
   2.122 +fun get_arities descr = foldl (fn (is, (_, (_, _, constrs))) =>
   2.123 +  foldl (fn (is', (_, cargs)) => map (length o fst o strip_dtyp)
   2.124 +    (filter is_rec_type cargs) union is') (is, constrs)) ([], descr);
   2.125  
   2.126  (* nonemptiness check for datatypes *)
   2.127  
   2.128 @@ -255,11 +275,10 @@
   2.129      fun is_nonempty_dt is i =
   2.130        let
   2.131          val (_, _, constrs) = the (assoc (descr', i));
   2.132 -        fun arg_nonempty (DtRec i) = if i mem is then false
   2.133 +        fun arg_nonempty (_, DtRec i) = if i mem is then false
   2.134                else is_nonempty_dt (i::is) i
   2.135 -          | arg_nonempty (DtType ("fun", [_, T])) = arg_nonempty T
   2.136            | arg_nonempty _ = true;
   2.137 -      in exists ((forall arg_nonempty) o snd) constrs
   2.138 +      in exists ((forall (arg_nonempty o strip_dtyp)) o snd) constrs
   2.139        end
   2.140    in assert_all (fn (i, _) => is_nonempty_dt [i] i) (hd descr)
   2.141      (fn (_, (s, _, _)) => "Nonemptiness check failed for datatype " ^ s)
   2.142 @@ -290,22 +309,21 @@
   2.143  
   2.144      (* unfold a single constructor argument *)
   2.145  
   2.146 -    fun unfold_arg ((i, Ts, descrs), T as (DtType (tname, dts))) =
   2.147 -          if is_rec_type T then
   2.148 -            if tname = "fun" then
   2.149 -              if is_rec_type (hd dts) then
   2.150 -                typ_error T "Non-strictly positive recursive occurrence of type"
   2.151 -              else
   2.152 -                (case hd (tl dts) of
   2.153 -                   DtType ("fun", _) => typ_error T "Curried function types not allowed"
   2.154 -                 | T' => let val (i', [T''], descrs') = unfold_arg ((i, [], descrs), T')
   2.155 -                         in (i', Ts @ [DtType (tname, [hd dts, T''])], descrs') end)
   2.156 -            else
   2.157 -              let val (index, descr) = get_dt_descr T i tname dts;
   2.158 -                  val (descr', i') = unfold_datatypes sign orig_descr sorts dt_info descr (i + length descr)
   2.159 -              in (i', Ts @ [DtRec index], descrs @ descr') end
   2.160 -          else (i, Ts @ [T], descrs)
   2.161 -      | unfold_arg ((i, Ts, descrs), T) = (i, Ts @ [T], descrs);
   2.162 +    fun unfold_arg ((i, Ts, descrs), T) =
   2.163 +      if is_rec_type T then
   2.164 +        let val (Us, U) = strip_dtyp T
   2.165 +        in if exists is_rec_type Us then
   2.166 +            typ_error T "Non-strictly positive recursive occurrence of type"
   2.167 +          else (case U of
   2.168 +              DtType (tname, dts) =>  
   2.169 +                let
   2.170 +                  val (index, descr) = get_dt_descr T i tname dts;
   2.171 +                  val (descr', i') = unfold_datatypes sign orig_descr sorts
   2.172 +                    dt_info descr (i + length descr)
   2.173 +                in (i', Ts @ [mk_fun_dtyp Us (DtRec index)], descrs @ descr') end
   2.174 +            | _ => (i, Ts @ [T], descrs))
   2.175 +        end
   2.176 +      else (i, Ts @ [T], descrs);
   2.177  
   2.178      (* unfold a constructor *)
   2.179  
     3.1 --- a/src/HOL/Tools/datatype_package.ML	Thu Oct 10 14:23:47 2002 +0200
     3.2 +++ b/src/HOL/Tools/datatype_package.ML	Thu Oct 10 14:26:50 2002 +0200
     3.3 @@ -450,7 +450,8 @@
     3.4      val newTs = take (length (hd descr), recTs);
     3.5  
     3.6      val no_size = exists (fn (_, (_, _, constrs)) => exists (fn (_, cargs) => exists
     3.7 -      (fn (DtType ("fun", [_, DtRec _])) => true | _ => false) cargs) constrs) descr';
     3.8 +      (fn dt => is_rec_type dt andalso not (null (fst (strip_dtyp dt))))
     3.9 +        cargs) constrs) descr';
    3.10  
    3.11      (**** declare new types and constants ****)
    3.12  
    3.13 @@ -470,9 +471,8 @@
    3.14            val Ts = map (typ_of_dtyp descr' sorts) cargs;
    3.15            val recs = filter (is_rec_type o fst) (cargs ~~ Ts);
    3.16  
    3.17 -          fun mk_argT (DtRec k, _) = nth_elem (k, rec_result_Ts)
    3.18 -            | mk_argT (DtType ("fun", [_, DtRec k]), Type ("fun", [T, _])) =
    3.19 -               T --> nth_elem (k, rec_result_Ts);
    3.20 +          fun mk_argT (dt, T) =
    3.21 +            binder_types T ---> nth_elem (body_index dt, rec_result_Ts);
    3.22  
    3.23            val argTs = Ts @ map mk_argT recs
    3.24          in argTs ---> nth_elem (i, rec_result_Ts)
     4.1 --- a/src/HOL/Tools/datatype_prop.ML	Thu Oct 10 14:23:47 2002 +0200
     4.2 +++ b/src/HOL/Tools/datatype_prop.ML	Thu Oct 10 14:26:50 2002 +0200
     4.3 @@ -11,38 +11,27 @@
     4.4    val dtK : int ref
     4.5    val indexify_names: string list -> string list
     4.6    val make_tnames: typ list -> string list
     4.7 -  val make_injs : (int * (string * DatatypeAux.dtyp list *
     4.8 -    (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
     4.9 -      term list list
    4.10 -  val make_ind : (int * (string * DatatypeAux.dtyp list *
    4.11 -    (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list -> term
    4.12 -  val make_casedists : (int * (string * DatatypeAux.dtyp list *
    4.13 -    (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list -> term list
    4.14 -  val make_primrecs : string list -> (int * (string * DatatypeAux.dtyp list *
    4.15 -    (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
    4.16 -      theory -> term list
    4.17 -  val make_cases : string list -> (int * (string * DatatypeAux.dtyp list *
    4.18 -    (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
    4.19 -      theory -> term list list
    4.20 -  val make_distincts : string list -> (int * (string * DatatypeAux.dtyp list *
    4.21 -    (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
    4.22 -      theory -> term list list
    4.23 -  val make_splits : string list -> (int * (string * DatatypeAux.dtyp list *
    4.24 -    (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
    4.25 -      theory -> (term * term) list
    4.26 -  val make_case_trrules : string list -> (int * (string * DatatypeAux.dtyp list *
    4.27 -    (string * DatatypeAux.dtyp list) list)) list list -> ast Syntax.trrule list
    4.28 -  val make_size : (int * (string * DatatypeAux.dtyp list *
    4.29 -    (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
    4.30 -      theory -> term list
    4.31 -  val make_weak_case_congs : string list -> (int * (string * DatatypeAux.dtyp list *
    4.32 -    (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
    4.33 -      theory -> term list
    4.34 -  val make_case_congs : string list -> (int * (string * DatatypeAux.dtyp list *
    4.35 -    (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
    4.36 -      theory -> term list
    4.37 -  val make_nchotomys : (int * (string * DatatypeAux.dtyp list *
    4.38 -    (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list -> term list
    4.39 +  val make_injs : DatatypeAux.descr list -> (string * sort) list -> term list list
    4.40 +  val make_ind : DatatypeAux.descr list -> (string * sort) list -> term
    4.41 +  val make_casedists : DatatypeAux.descr list -> (string * sort) list -> term list
    4.42 +  val make_primrecs : string list -> DatatypeAux.descr list ->
    4.43 +    (string * sort) list -> theory -> term list
    4.44 +  val make_cases : string list -> DatatypeAux.descr list ->
    4.45 +    (string * sort) list -> theory -> term list list
    4.46 +  val make_distincts : string list -> DatatypeAux.descr list ->
    4.47 +    (string * sort) list -> theory -> term list list
    4.48 +  val make_splits : string list -> DatatypeAux.descr list ->
    4.49 +    (string * sort) list -> theory -> (term * term) list
    4.50 +  val make_case_trrules : string list -> DatatypeAux.descr list ->
    4.51 +    ast Syntax.trrule list
    4.52 +  val make_size : DatatypeAux.descr list -> (string * sort) list ->
    4.53 +    theory -> term list
    4.54 +  val make_weak_case_congs : string list -> DatatypeAux.descr list ->
    4.55 +    (string * sort) list -> theory -> term list
    4.56 +  val make_case_congs : string list -> DatatypeAux.descr list ->
    4.57 +    (string * sort) list -> theory -> term list
    4.58 +  val make_nchotomys : DatatypeAux.descr list ->
    4.59 +    (string * sort) list -> term list
    4.60  end;
    4.61  
    4.62  structure DatatypeProp : DATATYPE_PROP =
    4.63 @@ -111,11 +100,11 @@
    4.64  
    4.65      fun make_ind_prem k T (cname, cargs) =
    4.66        let
    4.67 -        fun mk_prem ((DtRec k, s), T) = HOLogic.mk_Trueprop
    4.68 -              (make_pred k T $ Free (s, T))
    4.69 -          | mk_prem ((DtType ("fun", [_, DtRec k]), s), T' as Type ("fun", [T, U])) =
    4.70 -              all T $ Abs ("x", T, HOLogic.mk_Trueprop
    4.71 -                (make_pred k U $ (Free (s, T') $ Bound 0)));
    4.72 +        fun mk_prem ((dt, s), T) =
    4.73 +          let val (Us, U) = strip_type T
    4.74 +          in list_all (map (pair "x") Us, HOLogic.mk_Trueprop
    4.75 +            (make_pred (body_index dt) U $ app_bnds (Free (s, T)) (length Us)))
    4.76 +          end;
    4.77  
    4.78          val recs = filter is_rec_type cargs;
    4.79          val Ts = map (typ_of_dtyp descr' sorts) cargs;
    4.80 @@ -168,8 +157,6 @@
    4.81  
    4.82  fun make_primrecs new_type_names descr sorts thy =
    4.83    let
    4.84 -    val o_name = "Fun.comp";
    4.85 -
    4.86      val sign = Theory.sign_of thy;
    4.87  
    4.88      val descr' = flat descr;
    4.89 @@ -185,9 +172,8 @@
    4.90            val Ts = map (typ_of_dtyp descr' sorts) cargs;
    4.91            val recs = filter (is_rec_type o fst) (cargs ~~ Ts);
    4.92  
    4.93 -          fun mk_argT (DtRec k, _) = nth_elem (k, rec_result_Ts)
    4.94 -            | mk_argT (DtType ("fun", [_, DtRec k]), Type ("fun", [T, _])) =
    4.95 -               T --> nth_elem (k, rec_result_Ts);
    4.96 +          fun mk_argT (dt, T) =
    4.97 +            binder_types T ---> nth_elem (body_index dt, rec_result_Ts);
    4.98  
    4.99            val argTs = Ts @ map mk_argT recs
   4.100          in argTs ---> nth_elem (i, rec_result_Ts)
   4.101 @@ -215,17 +201,17 @@
   4.102          val frees = map Free (tnames ~~ Ts);
   4.103          val frees' = map Free (rec_tnames ~~ recTs');
   4.104  
   4.105 -        fun mk_reccomb (DtRec i, _) = nth_elem (i, reccombs)
   4.106 -          | mk_reccomb (DtType ("fun", [_, DtRec i]), Type ("fun", [T, U])) =
   4.107 -              let val T' = nth_elem (i, rec_result_Ts)
   4.108 -              in Const (o_name, [U --> T', T --> U, T] ---> T') $ nth_elem (i, reccombs)
   4.109 -              end;
   4.110 +        fun mk_reccomb ((dt, T), t) =
   4.111 +          let val (Us, U) = strip_type T
   4.112 +          in list_abs (map (pair "x") Us,
   4.113 +            nth_elem (body_index dt, reccombs) $ app_bnds t (length Us))
   4.114 +          end;
   4.115  
   4.116 -        val reccombs' = map mk_reccomb (recs ~~ recTs')
   4.117 +        val reccombs' = map mk_reccomb (recs ~~ recTs' ~~ frees')
   4.118  
   4.119        in (ts @ [HOLogic.mk_Trueprop (HOLogic.mk_eq
   4.120          (comb_t $ list_comb (Const (cname, Ts ---> T), frees),
   4.121 -         list_comb (f, frees @ (map (op $) (reccombs' ~~ frees')))))], fs)
   4.122 +         list_comb (f, frees @ reccombs')))], fs)
   4.123        end
   4.124  
   4.125    in fst (foldl (fn (x, ((dt, T), comb_t)) =>
     5.1 --- a/src/HOL/Tools/datatype_realizer.ML	Thu Oct 10 14:23:47 2002 +0200
     5.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Thu Oct 10 14:26:50 2002 +0200
     5.3 @@ -88,23 +88,18 @@
     5.4                  in (HOLogic.mk_Trueprop (make_pred i rT T (list_comb (f, vs'))
     5.5                    (list_comb (Const (cname, Ts ---> T), map Free frees))), f')
     5.6                  end
     5.7 -            | mk_prems vs (((DtRec k, s), T) :: ds) = 
     5.8 +            | mk_prems vs (((dt, s), T) :: ds) = 
     5.9                  let
    5.10 +                  val k = body_index dt;
    5.11 +                  val (Us, U) = strip_type T;
    5.12 +                  val i = length Us;
    5.13                    val rT = nth_elem (k, rec_result_Ts);
    5.14 -                  val r = Free ("r" ^ s, rT);
    5.15 +                  val r = Free ("r" ^ s, Us ---> rT);
    5.16                    val (p, f) = mk_prems (vs @ [r]) ds
    5.17 -                in (mk_all k ("r" ^ s) rT (Logic.mk_implies
    5.18 -                  (HOLogic.mk_Trueprop (make_pred k rT T r (Free (s, T))), p)), f)
    5.19 -                end
    5.20 -            | mk_prems vs (((DtType ("fun", [_, DtRec k]), s),
    5.21 -                  T' as Type ("fun", [T, U])) :: ds) =
    5.22 -                let
    5.23 -                  val rT = nth_elem (k, rec_result_Ts);
    5.24 -                  val r = Free ("r" ^ s, T --> rT);
    5.25 -                  val (p, f) = mk_prems (vs @ [r]) ds
    5.26 -                in (mk_all k ("r" ^ s) (T --> rT) (Logic.mk_implies
    5.27 -                  (all T $ Abs ("x", T, HOLogic.mk_Trueprop (make_pred k rT U
    5.28 -                    (r $ Bound 0) (Free (s, T') $ Bound 0))), p)), f)
    5.29 +                in (mk_all k ("r" ^ s) (Us ---> rT) (Logic.mk_implies
    5.30 +                  (list_all (map (pair "x") Us, HOLogic.mk_Trueprop
    5.31 +                    (make_pred k rT U (app_bnds r i)
    5.32 +                      (app_bnds (Free (s, T)) i))), p)), f)
    5.33                  end
    5.34  
    5.35          in (j + 1,
     6.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Thu Oct 10 14:23:47 2002 +0200
     6.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Thu Oct 10 14:26:50 2002 +0200
     6.3 @@ -15,11 +15,10 @@
     6.4  signature DATATYPE_REP_PROOFS =
     6.5  sig
     6.6    val representation_proofs : bool -> DatatypeAux.datatype_info Symtab.table ->
     6.7 -    string list -> (int * (string * DatatypeAux.dtyp list *
     6.8 -      (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
     6.9 -        (string * mixfix) list -> (string * mixfix) list list -> theory attribute
    6.10 -          -> theory -> theory * thm list list * thm list list * thm list list *
    6.11 -            DatatypeAux.simproc_dist list * thm
    6.12 +    string list -> DatatypeAux.descr list -> (string * sort) list ->
    6.13 +      (string * mixfix) list -> (string * mixfix) list list -> theory attribute
    6.14 +        -> theory -> theory * thm list list * thm list list * thm list list *
    6.15 +          DatatypeAux.simproc_dist list * thm
    6.16  end;
    6.17  
    6.18  structure DatatypeRepProofs : DATATYPE_REP_PROOFS =
    6.19 @@ -54,19 +53,15 @@
    6.20      val Leaf_name = "Datatype_Universe.Leaf";
    6.21      val Numb_name = "Datatype_Universe.Numb";
    6.22      val Lim_name = "Datatype_Universe.Lim";
    6.23 -    val Funs_name = "Datatype_Universe.Funs";
    6.24 -    val o_name = "Fun.comp";
    6.25 -    val sum_case_name = "Datatype.sum.sum_case";
    6.26 +    val Suml_name = "Datatype.Suml";
    6.27 +    val Sumr_name = "Datatype.Sumr";
    6.28  
    6.29 -    val [In0_inject, In1_inject, Scons_inject, Leaf_inject, In0_eq, In1_eq,
    6.30 -         In0_not_In1, In1_not_In0, Funs_mono, FunsI, Lim_inject,
    6.31 -         Funs_inv, FunsD, Funs_rangeE, Funs_nonempty, sum_case_inject] = map (get_thm Datatype_thy)
    6.32 -        ["In0_inject", "In1_inject", "Scons_inject", "Leaf_inject", "In0_eq", "In1_eq",
    6.33 -         "In0_not_In1", "In1_not_In0", "Funs_mono", "FunsI", "Lim_inject",
    6.34 -         "Funs_inv", "FunsD", "Funs_rangeE", "Funs_nonempty", "sum_case_inject"];
    6.35 -
    6.36 -    val Funs_IntE = (Int_lower2 RS Funs_mono RS
    6.37 -      (Int_lower1 RS Funs_mono RS Int_greatest) RS subsetD) RS IntE;
    6.38 +    val [In0_inject, In1_inject, Scons_inject, Leaf_inject,
    6.39 +         In0_eq, In1_eq, In0_not_In1, In1_not_In0,
    6.40 +         Lim_inject, Suml_inject, Sumr_inject] = map (get_thm Datatype_thy)
    6.41 +        ["In0_inject", "In1_inject", "Scons_inject", "Leaf_inject",
    6.42 +         "In0_eq", "In1_eq", "In0_not_In1", "In1_not_In0",
    6.43 +         "Lim_inject", "Suml_inject", "Sumr_inject"];
    6.44  
    6.45      val descr' = flat descr;
    6.46  
    6.47 @@ -83,6 +78,7 @@
    6.48      val branchTs = get_branching_types descr' sorts;
    6.49      val branchT = if null branchTs then HOLogic.unitT
    6.50        else fold_bal (fn (T, U) => Type ("+", [T, U])) branchTs;
    6.51 +    val arities = get_arities descr' \ 0;
    6.52      val unneeded_vars = hd tyvars \\ foldr add_typ_tfree_names (leafTs' @ branchTs, []);
    6.53      val leafTs = leafTs' @ (map (fn n => TFree (n, the (assoc (sorts, n)))) unneeded_vars);
    6.54      val recTs = get_rec_types descr' sorts;
    6.55 @@ -131,16 +127,16 @@
    6.56            let
    6.57              val n2 = n div 2;
    6.58              val Type (_, [T1, T2]) = T;
    6.59 -            val sum_case = Const (sum_case_name, [T1 --> Univ_elT, T2 --> Univ_elT, T] ---> Univ_elT)
    6.60 +            fun mkT U = (U --> Univ_elT) --> T --> Univ_elT
    6.61            in
    6.62 -            if i <= n2 then
    6.63 -              sum_case $ (mk_inj T1 n2 i) $ Const ("arbitrary", T2 --> Univ_elT)
    6.64 -            else
    6.65 -              sum_case $ Const ("arbitrary", T1 --> Univ_elT) $ mk_inj T2 (n - n2) (i - n2)
    6.66 +            if i <= n2 then Const (Suml_name, mkT T1) $ mk_inj T1 n2 i
    6.67 +            else Const (Sumr_name, mkT T2) $ mk_inj T2 (n - n2) (i - n2)
    6.68            end
    6.69        in mk_inj branchT (length branchTs) (1 + find_index_eq T' branchTs)
    6.70        end;
    6.71  
    6.72 +    val mk_lim = foldr (fn (T, t) => Lim $ mk_fun_inj T (Abs ("x", T, t)));
    6.73 +
    6.74      (************** generate introduction rules for representing set **********)
    6.75  
    6.76      val _ = message "Constructing representing sets ...";
    6.77 @@ -149,28 +145,26 @@
    6.78  
    6.79      fun make_intr s n (i, (_, cargs)) =
    6.80        let
    6.81 -        fun mk_prem (DtRec k, (j, prems, ts)) =
    6.82 -              let val free_t = mk_Free "x" Univ_elT j
    6.83 -              in (j + 1, (HOLogic.mk_mem (free_t,
    6.84 -                Const (nth_elem (k, rep_set_names), UnivT)))::prems, free_t::ts)
    6.85 +        fun mk_prem (dt, (j, prems, ts)) = (case strip_dtyp dt of
    6.86 +            (dts, DtRec k) =>
    6.87 +              let
    6.88 +                val Ts = map (typ_of_dtyp descr' sorts) dts;
    6.89 +                val free_t =
    6.90 +                  app_bnds (mk_Free "x" (Ts ---> Univ_elT) j) (length Ts)
    6.91 +              in (j + 1, list_all (map (pair "x") Ts,
    6.92 +                  HOLogic.mk_Trueprop (HOLogic.mk_mem (free_t,
    6.93 +                    Const (nth_elem (k, rep_set_names), UnivT)))) :: prems,
    6.94 +                mk_lim (Ts, free_t) :: ts)
    6.95                end
    6.96 -          | mk_prem (DtType ("fun", [T, DtRec k]), (j, prems, ts)) =
    6.97 -              let val T' = typ_of_dtyp descr' sorts T;
    6.98 -                  val free_t = mk_Free "x" (T' --> Univ_elT) j
    6.99 -              in (j + 1, (HOLogic.mk_mem (free_t,
   6.100 -                Const (Funs_name, UnivT --> HOLogic.mk_setT (T' --> Univ_elT)) $
   6.101 -                  Const (nth_elem (k, rep_set_names), UnivT)))::prems,
   6.102 -                    Lim $ mk_fun_inj T' free_t::ts)
   6.103 -              end
   6.104 -          | mk_prem (dt, (j, prems, ts)) =
   6.105 +          | _ =>
   6.106                let val T = typ_of_dtyp descr' sorts dt
   6.107                in (j + 1, prems, (Leaf $ mk_inj T (mk_Free "x" T j))::ts)
   6.108 -              end;
   6.109 +              end);
   6.110  
   6.111          val (_, prems, ts) = foldr mk_prem (cargs, (1, [], []));
   6.112          val concl = HOLogic.mk_Trueprop (HOLogic.mk_mem
   6.113            (mk_univ_inj ts n i, Const (s, UnivT)))
   6.114 -      in Logic.list_implies (map HOLogic.mk_Trueprop prems, concl)
   6.115 +      in Logic.list_implies (prems, concl)
   6.116        end;
   6.117  
   6.118      val consts = map (fn s => Const (s, UnivT)) rep_set_names;
   6.119 @@ -182,7 +176,7 @@
   6.120      val (thy2, {raw_induct = rep_induct, intrs = rep_intrs, ...}) =
   6.121        setmp InductivePackage.quiet_mode (!quiet_mode)
   6.122          (InductivePackage.add_inductive_i false true big_rec_name false true false
   6.123 -           consts (map (fn x => (("", x), [])) intr_ts) [Funs_mono]) thy1;
   6.124 +           consts (map (fn x => (("", x), [])) intr_ts) []) thy1;
   6.125  
   6.126      (********************************* typedef ********************************)
   6.127  
   6.128 @@ -191,7 +185,7 @@
   6.129          (TypedefPackage.add_typedef_i false (Some name') (name, tvs, mx) c None
   6.130            (rtac exI 1 THEN
   6.131              QUIET_BREADTH_FIRST (has_fewer_prems 1)
   6.132 -            (resolve_tac (Funs_nonempty::rep_intrs) 1))) thy |> #1)
   6.133 +            (resolve_tac rep_intrs 1))) thy |> #1)
   6.134                (parent_path flat_names thy2, types_syntax ~~ tyvars ~~
   6.135                  (take (length newTs, consts)) ~~ new_type_names));
   6.136  
   6.137 @@ -216,16 +210,10 @@
   6.138          fun constr_arg (dt, (j, l_args, r_args)) =
   6.139            let val T = typ_of_dtyp descr' sorts dt;
   6.140                val free_t = mk_Free "x" T j
   6.141 -          in (case dt of
   6.142 -              DtRec m => (j + 1, free_t::l_args, (Const (nth_elem (m, all_rep_names),
   6.143 -                T --> Univ_elT) $ free_t)::r_args)
   6.144 -            | DtType ("fun", [T', DtRec m]) =>
   6.145 -                let val ([T''], T''') = strip_type T
   6.146 -                in (j + 1, free_t::l_args, (Lim $ mk_fun_inj T''
   6.147 -                  (Const (o_name, [T''' --> Univ_elT, T, T''] ---> Univ_elT) $
   6.148 -                    Const (nth_elem (m, all_rep_names), T''' --> Univ_elT) $ free_t))::r_args)
   6.149 -                end
   6.150 -
   6.151 +          in (case (strip_dtyp dt, strip_type T) of
   6.152 +              ((_, DtRec m), (Us, U)) => (j + 1, free_t :: l_args, mk_lim (Us,
   6.153 +                Const (nth_elem (m, all_rep_names), U --> Univ_elT) $
   6.154 +                  app_bnds free_t (length Us)) :: r_args)
   6.155              | _ => (j + 1, free_t::l_args, (Leaf $ mk_inj T free_t)::r_args))
   6.156            end;
   6.157  
   6.158 @@ -321,11 +309,11 @@
   6.159      (* isomorphisms are defined using primrec-combinators:                 *)
   6.160      (* generate appropriate functions for instantiating primrec-combinator *)
   6.161      (*                                                                     *)
   6.162 -    (*   e.g.  dt_Rep_i = list_rec ... (%h t y. In1 ((Leaf h) $ y))        *)
   6.163 +    (*   e.g.  dt_Rep_i = list_rec ... (%h t y. In1 (Scons (Leaf h) y))    *)
   6.164      (*                                                                     *)
   6.165      (* also generate characteristic equations for isomorphisms             *)
   6.166      (*                                                                     *)
   6.167 -    (*   e.g.  dt_Rep_i (cons h t) = In1 ((dt_Rep_j h) $ (dt_Rep_i t))     *)
   6.168 +    (*   e.g.  dt_Rep_i (cons h t) = In1 (Scons (dt_Rep_j h) (dt_Rep_i t)) *)
   6.169      (*---------------------------------------------------------------------*)
   6.170  
   6.171      fun make_iso_def k ks n ((fs, eqns, i), (cname, cargs)) =
   6.172 @@ -337,24 +325,18 @@
   6.173          val constr = Const (cname, argTs ---> T);
   6.174  
   6.175          fun process_arg ks' ((i2, i2', ts, Ts), dt) =
   6.176 -          let val T' = typ_of_dtyp descr' sorts dt
   6.177 -          in (case dt of
   6.178 -              DtRec j => if j mem ks' then
   6.179 -                  (i2 + 1, i2' + 1, ts @ [mk_Free "y" Univ_elT i2'], Ts @ [Univ_elT])
   6.180 +          let
   6.181 +            val T' = typ_of_dtyp descr' sorts dt;
   6.182 +            val (Us, U) = strip_type T'
   6.183 +          in (case strip_dtyp dt of
   6.184 +              (_, DtRec j) => if j mem ks' then
   6.185 +                  (i2 + 1, i2' + 1, ts @ [mk_lim (Us, app_bnds
   6.186 +                     (mk_Free "y" (Us ---> Univ_elT) i2') (length Us))],
   6.187 +                   Ts @ [Us ---> Univ_elT])
   6.188                  else
   6.189 -                  (i2 + 1, i2', ts @ [Const (nth_elem (j, all_rep_names),
   6.190 -                    T' --> Univ_elT) $ mk_Free "x" T' i2], Ts)
   6.191 -            | (DtType ("fun", [_, DtRec j])) =>
   6.192 -                let val ([T''], T''') = strip_type T'
   6.193 -                in if j mem ks' then
   6.194 -                    (i2 + 1, i2' + 1, ts @ [Lim $ mk_fun_inj T''
   6.195 -                      (mk_Free "y" (T'' --> Univ_elT) i2')], Ts @ [T'' --> Univ_elT])
   6.196 -                  else
   6.197 -                    (i2 + 1, i2', ts @ [Lim $ mk_fun_inj T''
   6.198 -                      (Const (o_name, [T''' --> Univ_elT, T', T''] ---> Univ_elT) $
   6.199 -                        Const (nth_elem (j, all_rep_names), T''' --> Univ_elT) $
   6.200 -                          mk_Free "x" T' i2)], Ts)
   6.201 -                end
   6.202 +                  (i2 + 1, i2', ts @ [mk_lim (Us,
   6.203 +                     Const (nth_elem (j, all_rep_names), U --> Univ_elT) $
   6.204 +                       app_bnds (mk_Free "x" T' i2) (length Us))], Ts)
   6.205              | _ => (i2 + 1, i2', ts @ [Leaf $ mk_inj T' (mk_Free "x" T' i2)], Ts))
   6.206            end;
   6.207  
   6.208 @@ -406,18 +388,25 @@
   6.209  
   6.210      fun mk_funs_inv thm =
   6.211        let
   6.212 -        val [_, t] = prems_of Funs_inv;
   6.213 -        val [_ $ (_ $ _ $ R)] = Logic.strip_assums_hyp t;
   6.214 -        val _ $ (_ $ (r $ (a $ _)) $ _) = Logic.strip_assums_concl t;
   6.215 -        val [_ $ (_ $ _ $ R')] = prems_of thm;
   6.216 -        val _ $ (_ $ (r' $ (a' $ _)) $ _) = concl_of thm;
   6.217 -        val inv' = cterm_instantiate (map 
   6.218 -          ((pairself (cterm_of (sign_of_thm thm))) o
   6.219 -           (apsnd (map_term_types (incr_tvar 1))))
   6.220 -             [(R, R'), (r, r'), (a, a')]) Funs_inv
   6.221 -      in
   6.222 -        rule_by_tactic (atac 2) (thm RSN (2, inv'))
   6.223 -      end;
   6.224 +        val {sign, prop, ...} = rep_thm thm;
   6.225 +        val (_ $ (_ $ (Const (_, Type (_, [U, _])) $ _ $ S)) $
   6.226 +          (_ $ (_ $ (r $ (a $ _)) $ _)), _) = Type.freeze_thaw prop;
   6.227 +        val used = add_term_tfree_names (a, []);
   6.228 +
   6.229 +        fun mk_thm i =
   6.230 +          let
   6.231 +            val Ts = map (TFree o rpair HOLogic.typeS)
   6.232 +              (variantlist (replicate i "'t", used));
   6.233 +            val f = Free ("f", Ts ---> U)
   6.234 +          in prove_goalw_cterm [] (cterm_of sign (Logic.mk_implies
   6.235 +            (HOLogic.mk_Trueprop (HOLogic.list_all
   6.236 +               (map (pair "x") Ts, HOLogic.mk_mem (app_bnds f i, S))),
   6.237 +             HOLogic.mk_Trueprop (HOLogic.mk_eq (list_abs (map (pair "x") Ts,
   6.238 +               r $ (a $ app_bnds f i)), f))))) (fn prems =>
   6.239 +                 [cut_facts_tac prems 1, REPEAT (rtac ext 1),
   6.240 +                  REPEAT (etac allE 1), rtac thm 1, atac 1])
   6.241 +          end
   6.242 +      in map (fn r => r RS subst) (thm :: map mk_thm arities) end;
   6.243  
   6.244      (* prove  inj dt_Rep_i  and  dt_Rep_i x : dt_rep_set_i *)
   6.245  
   6.246 @@ -440,8 +429,8 @@
   6.247          val (ind_concl1, ind_concl2) = ListPair.unzip (map mk_ind_concl ds);
   6.248  
   6.249          val rewrites = map mk_meta_eq iso_char_thms;
   6.250 -        val inj_thms' = flat (map (fn r => [r RS injD, r RS inj_o])
   6.251 -          (map snd newT_iso_inj_thms @ inj_thms));
   6.252 +        val inj_thms' = map (fn r => r RS injD)
   6.253 +          (map snd newT_iso_inj_thms @ inj_thms);
   6.254  
   6.255          val inj_thm = prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5)
   6.256            (HOLogic.mk_Trueprop (mk_conj ind_concl1))) (fn _ =>
   6.257 @@ -455,13 +444,15 @@
   6.258                     REPEAT (dresolve_tac [In0_inject, In1_inject] 1),
   6.259                     (eresolve_tac [In0_not_In1 RS notE, In1_not_In0 RS notE] 1)
   6.260                     ORELSE (EVERY
   6.261 -                     [REPEAT (eresolve_tac (Scons_inject :: sum_case_inject ::
   6.262 -                        map make_elim (inj_thms' @
   6.263 -                          [Leaf_inject, Lim_inject, Inl_inject, Inr_inject])) 1),
   6.264 -                      REPEAT ((EVERY [etac allE 1, dtac mp 1, atac 1]) ORELSE
   6.265 -                              (dtac inj_fun_lemma 1 THEN atac 1)),
   6.266 -                      REPEAT (hyp_subst_tac 1),
   6.267 -                      rtac refl 1])])])]);
   6.268 +                     [REPEAT (eresolve_tac (Scons_inject ::
   6.269 +                        map make_elim [Leaf_inject, Inl_inject, Inr_inject]) 1),
   6.270 +                      REPEAT (cong_tac 1), rtac refl 1,
   6.271 +                      REPEAT (atac 1 ORELSE (EVERY
   6.272 +                        [REPEAT (rtac ext 1),
   6.273 +                         REPEAT (eresolve_tac (mp :: allE ::
   6.274 +                           map make_elim (Suml_inject :: Sumr_inject ::
   6.275 +                             Lim_inject :: fun_cong :: inj_thms')) 1),
   6.276 +                         atac 1]))])])])]);
   6.277  
   6.278          val inj_thms'' = map (fn r => r RS datatype_injI)
   6.279                               (split_conj_thm inj_thm);
   6.280 @@ -472,11 +463,9 @@
   6.281  	       (HOLogic.mk_Trueprop (mk_conj ind_concl2)))
   6.282  	      (fn _ =>
   6.283  	       [(indtac induction THEN_ALL_NEW ObjectLogic.atomize_tac) 1,
   6.284 -		rewrite_goals_tac (o_def :: rewrites),
   6.285 -		REPEAT (EVERY
   6.286 -			[resolve_tac rep_intrs 1,
   6.287 -			 REPEAT (FIRST [atac 1, etac spec 1,
   6.288 -				 resolve_tac (FunsI :: elem_thms) 1])])]);
   6.289 +		rewrite_goals_tac rewrites,
   6.290 +		REPEAT ((resolve_tac rep_intrs THEN_ALL_NEW
   6.291 +                  ((REPEAT o etac allE) THEN' ares_tac elem_thms)) 1)]);
   6.292  
   6.293        in (inj_thms'' @ inj_thms, elem_thms @ (split_conj_thm elem_thm))
   6.294        end;
   6.295 @@ -502,18 +491,20 @@
   6.296  
   6.297      (* all the theorems are proved by one single simultaneous induction *)
   6.298  
   6.299 +    val range_eqs = map (fn r => mk_meta_eq (r RS range_ex1_eq))
   6.300 +      iso_inj_thms_unfolded;
   6.301 +
   6.302      val iso_thms = if length descr = 1 then [] else
   6.303        drop (length newTs, split_conj_thm
   6.304          (prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5) iso_t) (fn _ =>
   6.305 -           [indtac rep_induct 1,
   6.306 +           [(indtac rep_induct THEN_ALL_NEW ObjectLogic.atomize_tac) 1,
   6.307              REPEAT (rtac TrueI 1),
   6.308 +            rewrite_goals_tac (mk_meta_eq choice_eq ::
   6.309 +              symmetric (mk_meta_eq expand_fun_eq) :: range_eqs),
   6.310 +            rewrite_goals_tac (map symmetric range_eqs),
   6.311              REPEAT (EVERY
   6.312 -              [rewrite_goals_tac [mk_meta_eq Collect_mem_eq],
   6.313 -               REPEAT (etac Funs_IntE 1),
   6.314 -               REPEAT (eresolve_tac (rangeE ::
   6.315 -                 map (fn r => r RS Funs_rangeE) iso_inj_thms_unfolded) 1),
   6.316 -               REPEAT (eresolve_tac (map (fn (iso, _, _) => iso RS subst) newT_iso_axms @
   6.317 -                 map (fn (iso, _, _) => mk_funs_inv iso RS subst) newT_iso_axms) 1),
   6.318 +              [REPEAT (eresolve_tac ([rangeE, ex1_implies_ex RS exE] @
   6.319 +                 flat (map (mk_funs_inv o #1) newT_iso_axms)) 1),
   6.320                 TRY (hyp_subst_tac 1),
   6.321                 rtac (sym RS range_eqI) 1,
   6.322                 resolve_tac iso_char_thms 1])])));
   6.323 @@ -523,8 +514,7 @@
   6.324        map2 (fn (r_inj, r) => f_myinv_f OF [r_inj, r RS mp])
   6.325          (iso_inj_thms_unfolded, iso_thms);
   6.326  
   6.327 -    val Abs_inverse_thms = map (fn r => r RS subst) (Abs_inverse_thms' @
   6.328 -      map mk_funs_inv Abs_inverse_thms');
   6.329 +    val Abs_inverse_thms = flat (map mk_funs_inv Abs_inverse_thms');
   6.330  
   6.331      (******************* freeness theorems for constructors *******************)
   6.332  
   6.333 @@ -541,7 +531,7 @@
   6.334           rewrite_goals_tac rewrites,
   6.335           rtac refl 1,
   6.336           resolve_tac rep_intrs 2,
   6.337 -         REPEAT (resolve_tac (FunsI :: iso_elem_thms) 1)])
   6.338 +         REPEAT (resolve_tac iso_elem_thms 1)])
   6.339        end;
   6.340  
   6.341      (*--------------------------------------------------------------*)
   6.342 @@ -575,17 +565,19 @@
   6.343      (* prove injectivity of constructors *)
   6.344  
   6.345      fun prove_constr_inj_thm rep_thms t =
   6.346 -      let val inj_thms = Scons_inject::sum_case_inject::(map make_elim
   6.347 +      let val inj_thms = Scons_inject :: (map make_elim
   6.348          ((map (fn r => r RS injD) iso_inj_thms) @
   6.349 -          [In0_inject, In1_inject, Leaf_inject, Inl_inject, Inr_inject, Lim_inject]))
   6.350 +          [In0_inject, In1_inject, Leaf_inject, Inl_inject, Inr_inject,
   6.351 +           Lim_inject, Suml_inject, Sumr_inject]))
   6.352        in prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5) t) (fn _ =>
   6.353          [rtac iffI 1,
   6.354           REPEAT (etac conjE 2), hyp_subst_tac 2, rtac refl 2,
   6.355           dresolve_tac rep_congs 1, dtac box_equals 1,
   6.356 -         REPEAT (resolve_tac rep_thms 1), rewtac o_def,
   6.357 +         REPEAT (resolve_tac rep_thms 1),
   6.358           REPEAT (eresolve_tac inj_thms 1),
   6.359 -         REPEAT (ares_tac [conjI] 1 ORELSE (EVERY [rtac ext 1, dtac fun_cong 1,
   6.360 -                  eresolve_tac inj_thms 1, atac 1]))])
   6.361 +         REPEAT (ares_tac [conjI] 1 ORELSE (EVERY [REPEAT (rtac ext 1),
   6.362 +           REPEAT (eresolve_tac (make_elim fun_cong :: inj_thms) 1),
   6.363 +           atac 1]))])
   6.364        end;
   6.365  
   6.366      val constr_inject = map (fn (ts, thms) => map (prove_constr_inj_thm thms) ts)
   6.367 @@ -641,12 +633,12 @@
   6.368  
   6.369      val dt_induct = prove_goalw_cterm [] (cert
   6.370        (DatatypeProp.make_ind descr sorts)) (fn prems =>
   6.371 -        [rtac indrule_lemma' 1, indtac rep_induct 1,
   6.372 +        [rtac indrule_lemma' 1,
   6.373 +         (indtac rep_induct THEN_ALL_NEW ObjectLogic.atomize_tac) 1,
   6.374           EVERY (map (fn (prem, r) => (EVERY
   6.375 -           [REPEAT (eresolve_tac (Funs_IntE::Abs_inverse_thms) 1),
   6.376 +           [REPEAT (eresolve_tac Abs_inverse_thms 1),
   6.377              simp_tac (HOL_basic_ss addsimps ((symmetric r)::Rep_inverse_thms')) 1,
   6.378 -            DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE (EVERY [rewtac o_def,
   6.379 -              dtac FunsD 1, etac CollectD 1]))]))
   6.380 +            DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE etac allE 1)]))
   6.381                  (prems ~~ (constr_defs @ (map mk_meta_eq iso_char_thms))))]);
   6.382  
   6.383      val (thy7, [dt_induct']) = thy6 |>
     7.1 --- a/src/HOL/Tools/primrec_package.ML	Thu Oct 10 14:23:47 2002 +0200
     7.2 +++ b/src/HOL/Tools/primrec_package.ML	Thu Oct 10 14:26:50 2002 +0200
     7.3 @@ -141,16 +141,13 @@
     7.4                (fnames', fnss', (Const ("arbitrary", dummyT))::fns))
     7.5          | Some (ls, cargs', rs, rhs, eq) =>
     7.6              let
     7.7 -              fun rec_index (DtRec k) = k
     7.8 -                | rec_index (DtType ("fun", [_, DtRec k])) = k;
     7.9 -
    7.10                val recs = filter (is_rec_type o snd) (cargs' ~~ cargs);
    7.11                val rargs = map fst recs;
    7.12                val subs = map (rpair dummyT o fst) 
    7.13  		             (rev (rename_wrt_term rhs rargs));
    7.14                val ((fnames'', fnss''), rhs') = 
    7.15  		  (subst (map (fn ((x, y), z) =>
    7.16 -			       (Free x, (rec_index y, Free z)))
    7.17 +			       (Free x, (body_index y, Free z)))
    7.18  			  (recs ~~ subs))
    7.19  		   ((fnames', fnss'), rhs))
    7.20                    handle RecError s => primrec_eq_err sign s eq
    7.21 @@ -257,7 +254,7 @@
    7.22        (if eq_set (names1, names2) then (PureThy.add_defs_i false o map Thm.no_attributes) defs'
    7.23         else primrec_err ("functions " ^ commas_quote names2 ^
    7.24           "\nare not mutually recursive"));
    7.25 -    val rewrites = o_def :: (map mk_meta_eq rec_rewrites) @ defs_thms';
    7.26 +    val rewrites = (map mk_meta_eq rec_rewrites) @ defs_thms';
    7.27      val _ = message ("Proving equations for primrec function(s) " ^ commas_quote names1 ^ " ...");
    7.28      val simps = map (fn (_, t) => prove_goalw_cterm rewrites (cterm_of (Theory.sign_of thy') t)
    7.29          (fn _ => [rtac refl 1])) eqns;