# HG changeset patch
# User berghofe
# Date 932120044 -7200
# Node ID 85be09eb136c5000314878921984ee18a3eb5e8f
# Parent  11ee650edcd2aba5e411440bb10a56756affdcb1
- Datatype package now also supports arbitrarily branching datatypes
  (using function types).
- Added new simplification procedure for proving distinctness of
  constructors.
- dtK is now a reference.

diff -r 11ee650edcd2 -r 85be09eb136c src/HOL/Tools/datatype_abs_proofs.ML
--- a/src/HOL/Tools/datatype_abs_proofs.ML	Fri Jul 16 12:09:48 1999 +0200
+++ b/src/HOL/Tools/datatype_abs_proofs.ML	Fri Jul 16 12:14:04 1999 +0200
@@ -25,13 +25,10 @@
   val prove_primrec_thms : bool -> string list -> (int * (string * DatatypeAux.dtyp list *
     (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
       DatatypeAux.datatype_info Symtab.table -> thm list list -> thm list list ->
-        thm -> theory -> theory * string list * thm list
+        simpset -> thm -> theory -> theory * string list * thm list
   val prove_case_thms : bool -> string list -> (int * (string * DatatypeAux.dtyp list *
     (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
       string list -> thm list -> theory -> theory * string list * thm list list
-  val prove_distinctness_thms : bool -> string list -> (int * (string * DatatypeAux.dtyp list *
-    (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
-      thm list list -> thm list list -> theory -> theory * thm list list
   val prove_split_thms : string list -> (int * (string * DatatypeAux.dtyp list *
     (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
       thm list list -> thm list list -> thm list -> thm list list -> theory ->
@@ -97,10 +94,14 @@
 (*************************** primrec combinators ******************************)
 
 fun prove_primrec_thms flat_names new_type_names descr sorts
-    (dt_info : datatype_info Symtab.table) constr_inject dist_rewrites induct thy =
+    (dt_info : datatype_info Symtab.table) constr_inject dist_rewrites dist_ss induct thy =
   let
     val _ = message "Constructing primrec combinators ...";
 
+    val fun_rel_comp_name = Sign.intern_const (sign_of Relation.thy) "fun_rel_comp";
+    val [fun_rel_comp_def, o_def] =
+      map (get_thm Relation.thy) ["fun_rel_comp_def", "o_def"];
+
     val big_name = space_implode "_" new_type_names;
     val thy0 = add_path flat_names big_name thy;
 
@@ -123,9 +124,14 @@
     val reccomb_fn_Ts = flat (map (fn (i, (_, _, constrs)) =>
       map (fn (_, cargs) =>
         let
-          val recs = filter is_rec_type cargs;
-          val argTs = (map (typ_of_dtyp descr' sorts) cargs) @
-            (map (fn r => nth_elem (dest_DtRec r, rec_result_Ts)) recs)
+          val Ts = map (typ_of_dtyp descr' sorts) cargs;
+          val recs = filter (is_rec_type o fst) (cargs ~~ Ts);
+
+          fun mk_argT (DtRec k, _) = nth_elem (k, rec_result_Ts)
+            | mk_argT (DtType ("fun", [_, DtRec k]), Type ("fun", [T, _])) =
+               T --> nth_elem (k, rec_result_Ts);
+
+          val argTs = Ts @ map mk_argT recs
         in argTs ---> nth_elem (i, rec_result_Ts)
         end) constrs) descr');
 
@@ -141,22 +147,27 @@
 
     fun make_rec_intr T set_name ((rec_intr_ts, l), (cname, cargs)) =
       let
-        fun mk_prem (dt, (j, k, prems, t1s, t2s)) =
-          let
-            val T = typ_of_dtyp descr' sorts dt;
-            val free1 = mk_Free "x" T j
-          in (case dt of
-             DtRec m =>
+        fun mk_prem ((dt, U), (j, k, prems, t1s, t2s)) =
+          let val free1 = mk_Free "x" U j
+          in (case (dt, U) of
+             (DtRec m, _) =>
                let val free2 = mk_Free "y" (nth_elem (m, rec_result_Ts)) k
                in (j + 1, k + 1, (HOLogic.mk_Trueprop (HOLogic.mk_mem
                  (HOLogic.mk_prod (free1, free2), nth_elem (m, rec_sets))))::prems,
                    free1::t1s, free2::t2s)
                end
+           | (DtType ("fun", [_, DtRec m]), U' as Type ("fun", [T', _])) =>
+               let val free2 = mk_Free "y" (T' --> nth_elem (m, rec_result_Ts)) k
+               in (j + 1, k + 1, (HOLogic.mk_Trueprop (HOLogic.mk_mem (free2,
+                 Const (fun_rel_comp_name, [U', snd (strip_type (nth_elem (m, rec_set_Ts)))] --->
+                   HOLogic.mk_setT (T' --> nth_elem (m, rec_result_Ts))) $
+                     free1 $ nth_elem (m, rec_sets))))::prems, free1::t1s, free2::t2s)
+               end
            | _ => (j + 1, k, prems, free1::t1s, t2s))
           end;
 
         val Ts = map (typ_of_dtyp descr' sorts) cargs;
-        val (_, _, prems, t1s, t2s) = foldr mk_prem (cargs, (1, 1, [], [], []))
+        val (_, _, prems, t1s, t2s) = foldr mk_prem (cargs ~~ Ts, (1, 1, [], [], []))
 
       in (rec_intr_ts @ [Logic.list_implies (prems, HOLogic.mk_Trueprop (HOLogic.mk_mem
         (HOLogic.mk_prod (list_comb (Const (cname, Ts ---> T), t1s),
@@ -170,7 +181,7 @@
     val (thy1, {intrs = rec_intrs, elims = rec_elims, ...}) =
       setmp InductivePackage.quiet_mode (!quiet_mode)
         (InductivePackage.add_inductive_i false true big_rec_name' false false true
-           rec_sets [] (map (fn x => (("", x), [])) rec_intr_ts) [] []) thy0;
+           rec_sets [] (map (fn x => (("", x), [])) rec_intr_ts) [fun_rel_comp_mono] []) thy0;
 
     (* prove uniqueness and termination of primrec combinators *)
 
@@ -181,9 +192,7 @@
         val distinct_tac = (etac Pair_inject 1) THEN
           (if i < length newTs then
              full_simp_tac (HOL_ss addsimps (nth_elem (i, dist_rewrites))) 1
-           else full_simp_tac (HOL_ss addsimps
-             ((#distinct (the (Symtab.lookup (dt_info, tname)))) @
-               [Suc_Suc_eq, Suc_not_Zero, Zero_not_Suc])) 1);
+           else full_simp_tac dist_ss 1);
 
         val inject = map (fn r => r RS iffD1)
           (if i < length newTs then nth_elem (i, constr_inject)
@@ -194,6 +203,7 @@
             val k = length (filter is_rec_type cargs)
 
           in (EVERY [DETERM tac,
+                REPEAT (dtac fun_rel_comp_unique 1),
                 REPEAT (etac ex1E 1), rtac ex1I 1,
                 DEPTH_SOLVE_1 (ares_tac [intr] 1),
                 REPEAT_DETERM_N k (etac thin 1),
@@ -252,10 +262,9 @@
         (Sign.base_name name, reccomb_fn_Ts @ [T] ---> T', NoSyn))
           (reccomb_names ~~ recTs ~~ rec_result_Ts)) |>
       Theory.add_defs_i (map (fn ((((name, comb), set), T), T') =>
-        ((Sign.base_name name) ^ "_def", Logic.mk_equals
-          (comb $ Free ("x", T),
+        ((Sign.base_name name) ^ "_def", Logic.mk_equals (comb, absfree ("x", T,
            Const ("Eps", (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
-             HOLogic.mk_mem (HOLogic.mk_prod (Free ("x", T), Free ("y", T')), set)))))
+             HOLogic.mk_mem (HOLogic.mk_prod (Free ("x", T), Free ("y", T')), set))))))
                (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts)) |>
       parent_path flat_names;
 
@@ -270,7 +279,8 @@
         [rtac select1_equality 1,
          resolve_tac rec_unique_thms 1,
          resolve_tac rec_intrs 1,
-         REPEAT (resolve_tac rec_total_thms 1)]))
+         rewrite_goals_tac [o_def, fun_rel_comp_def],
+         REPEAT ((rtac CollectI 1 THEN rtac allI 1) ORELSE resolve_tac rec_total_thms 1)]))
            (DatatypeProp.make_primrecs new_type_names descr sorts thy2)
 
   in
@@ -294,10 +304,13 @@
     val newTs = take (length (hd descr), recTs);
     val T' = TFree (variant used "'t", HOLogic.termS);
 
+    fun mk_dummyT (DtRec _) = T'
+      | mk_dummyT (DtType ("fun", [T, _])) = typ_of_dtyp descr' sorts T --> T'
+
     val case_dummy_fns = map (fn (_, (_, _, constrs)) => map (fn (_, cargs) =>
       let
         val Ts = map (typ_of_dtyp descr' sorts) cargs;
-        val Ts' = replicate (length (filter is_rec_type cargs)) T'
+        val Ts' = map mk_dummyT (filter is_rec_type cargs)
       in Const ("arbitrary", Ts @ Ts' ---> T')
       end) constrs) descr';
 
@@ -312,7 +325,7 @@
           val (fns1, fns2) = ListPair.unzip (map (fn ((_, cargs), j) =>
             let
               val Ts = map (typ_of_dtyp descr' sorts) cargs;
-              val Ts' = Ts @ (replicate (length (filter is_rec_type cargs)) T');
+              val Ts' = Ts @ map mk_dummyT (filter is_rec_type cargs);
               val frees' = map (uncurry (mk_Free "x")) (Ts' ~~ (1 upto length Ts'));
               val frees = take (length cargs, frees');
               val free = mk_Free "f" (Ts ---> T') j
@@ -350,80 +363,6 @@
     (store_thmss "cases" new_type_names case_thms thy3, case_names, case_thms)
   end;
 
-(************************ distinctness of constructors ************************)
-
-fun prove_distinctness_thms flat_names new_type_names descr sorts dist_rewrites case_thms thy =
-  let
-    val thy1 = add_path flat_names (space_implode "_" new_type_names) thy;
-
-    val descr' = flat descr;
-    val recTs = get_rec_types descr' sorts;
-    val newTs = take (length (hd descr), recTs);
-
-    (*--------------------------------------------------------------------*)
-    (* define t_ord - functions for proving distinctness of constructors: *)
-    (*  t_ord C_i ... = i                                                 *)
-    (*--------------------------------------------------------------------*)
-
-    fun define_ord ((thy, ord_defs), (((_, (_, _, constrs)), T), tname)) =
-      if length constrs < DatatypeProp.dtK then (thy, ord_defs)
-      else
-        let
-          val Tss = map ((map (typ_of_dtyp descr' sorts)) o snd) constrs;
-          val ts = map HOLogic.mk_nat (0 upto length constrs - 1);
-          val mk_abs = foldr (fn (T, t') => Abs ("x", T, t'));
-          val fs = map mk_abs (Tss ~~ ts);
-          val fTs = map (fn Ts => Ts ---> HOLogic.natT) Tss;
-          val ord_name = Sign.full_name (Theory.sign_of thy) (tname ^ "_ord");
-          val case_name = Sign.intern_const (Theory.sign_of thy) (tname ^ "_case");
-          val ordT = T --> HOLogic.natT;
-          val caseT = fTs ---> ordT;
-          val defpair = (tname ^ "_ord_def", Logic.mk_equals
-            (Const (ord_name, ordT), list_comb (Const (case_name, caseT), fs)));
-          val thy' = thy |>
-            Theory.add_consts_i [(tname ^ "_ord", ordT, NoSyn)] |>
-            Theory.add_defs_i [defpair];
-          val def = get_def thy' (tname ^ "_ord")
-
-        in (thy', ord_defs @ [def]) end;
-
-    val (thy2, ord_defs) =
-      foldl define_ord ((thy1, []), (hd descr) ~~ newTs ~~ new_type_names);
-
-    (**** number of constructors < dtK ****)
-
-    fun prove_distinct_thms _ [] = []
-      | prove_distinct_thms dist_rewrites' (t::_::ts) =
-          let
-            val dist_thm = prove_goalw_cterm [] (cterm_of (Theory.sign_of thy2) t) (fn _ =>
-              [simp_tac (HOL_ss addsimps dist_rewrites') 1])
-          in dist_thm::(standard (dist_thm RS not_sym))::
-            (prove_distinct_thms dist_rewrites' ts)
-          end;
-
-    val distinct_thms = map (fn ((((_, (_, _, constrs)), ts),
-      dist_rewrites'), case_thms) =>
-        if length constrs < DatatypeProp.dtK then
-          prove_distinct_thms dist_rewrites' ts
-        else 
-          let
-            val t::ts' = rev ts;
-            val (_ $ (_ $ (_ $ (f $ _) $ _))) = hd (Logic.strip_imp_prems t);
-            val cert = cterm_of (Theory.sign_of thy2);
-            val distinct_lemma' = cterm_instantiate
-              [(cert distinct_f, cert f)] distinct_lemma;
-            val rewrites = ord_defs @ (map mk_meta_eq case_thms)
-          in
-            (map (fn t => prove_goalw_cterm rewrites (cert t)
-              (fn _ => [rtac refl 1])) (rev ts')) @ [standard distinct_lemma']
-          end) ((hd descr) ~~ (DatatypeProp.make_distincts new_type_names
-            descr sorts thy2) ~~ dist_rewrites ~~ case_thms)
-
-  in
-    (thy2 |> parent_path flat_names |>
-             store_thmss "distinct" new_type_names distinct_thms,
-     distinct_thms)
-  end;
 
 (******************************* case splitting *******************************)
 
@@ -465,6 +404,11 @@
 (******************************* size functions *******************************)
 
 fun prove_size_thms flat_names new_type_names descr sorts reccomb_names primrec_thms thy =
+  if exists (fn (_, (_, _, constrs)) => exists (fn (_, cargs) => exists
+    (fn (DtType ("fun", [_, DtRec _])) => true | _ => false) cargs) constrs) (flat descr)
+  then
+    (thy, [])
+  else
   let
     val _ = message "Proving equations for size function ...";
 
@@ -475,7 +419,7 @@
     val recTs = get_rec_types descr' sorts;
 
     val big_size_name = space_implode "_" new_type_names ^ "_size";
-    val size_name = Sign.intern_const (Theory.sign_of (the (get_thy "Arith" thy1))) "size";
+    val size_name = Sign.intern_const (Theory.sign_of (theory "Arith")) "size";
     val size_names = replicate (length (hd descr)) size_name @
       map (Sign.full_name (Theory.sign_of thy1))
         (if length (flat (tl descr)) = 1 then [big_size_name] else
diff -r 11ee650edcd2 -r 85be09eb136c src/HOL/Tools/datatype_aux.ML
--- a/src/HOL/Tools/datatype_aux.ML	Fri Jul 16 12:09:48 1999 +0200
+++ b/src/HOL/Tools/datatype_aux.ML	Fri Jul 16 12:14:04 1999 +0200
@@ -13,8 +13,6 @@
   
   val foldl1 : ('a * 'a -> 'a) -> 'a list -> 'a
 
-  val get_thy : string -> theory -> theory option
-
   val add_path : bool -> string -> theory -> theory
   val parent_path : bool -> theory -> theory
 
@@ -28,6 +26,10 @@
   val indtac : thm -> int -> tactic
   val exh_tac : (string -> thm) -> int -> tactic
 
+  datatype simproc_dist = QuickAndDirty
+                        | FewConstrs of thm list
+                        | ManyConstrs of thm * simpset;
+
   datatype dtyp =
       DtTFree of string
     | DtType of string * (dtyp list)
@@ -35,6 +37,7 @@
 
   type datatype_info
 
+  exception Datatype
   val dtyp_of_typ : (string * string list) list -> typ -> dtyp
   val mk_Free : string -> typ -> int -> term
   val is_rec_type : dtyp -> bool
@@ -46,14 +49,16 @@
   val dest_conj : term -> term list
   val get_nonrec_types : (int * (string * dtyp list *
     (string * dtyp list) list)) list -> (string * sort) list -> typ list
+  val get_branching_types : (int * (string * dtyp list *
+    (string * dtyp list) list)) list -> (string * sort) list -> typ list
   val get_rec_types : (int * (string * dtyp list *
     (string * dtyp list) list)) list -> (string * sort) list -> typ list
   val check_nonempty : (int * (string * dtyp list *
     (string * dtyp list) list)) list list -> unit
   val unfold_datatypes : 
-    datatype_info Symtab.table ->
-      (int * (string * dtyp list *
-        (string * dtyp list) list)) list -> int ->
+    Sign.sg -> (int * (string * dtyp list * (string * dtyp list) list)) list ->
+      (string * sort) list -> datatype_info Symtab.table ->
+        (int * (string * dtyp list * (string * dtyp list) list)) list -> int ->
           (int * (string * dtyp list *
             (string * dtyp list) list)) list list * int
 end;
@@ -67,9 +72,6 @@
 (* FIXME: move to library ? *)
 fun foldl1 f (x::xs) = foldl f (x, xs);
 
-fun get_thy name thy = find_first
-  (equal name o Sign.name_of o Theory.sign_of) (Theory.ancestors_of thy);
-
 fun add_path flat_names s = if flat_names then I else Theory.add_path s;
 fun parent_path flat_names = if flat_names then I else Theory.parent_path;
 
@@ -92,7 +94,7 @@
 (* split theorem thm_1 & ... & thm_n into n theorems *)
 
 fun split_conj_thm th =
-  ((th RS conjunct1)::(split_conj_thm (th RS conjunct2))) handle _ => [th];
+  ((th RS conjunct1)::(split_conj_thm (th RS conjunct2))) handle THM _ => [th];
 
 val mk_conj = foldr1 (HOLogic.mk_binop "op &");
 val mk_disj = foldr1 (HOLogic.mk_binop "op |");
@@ -138,6 +140,12 @@
   in compose_tac (false, exhaustion', nprems_of exhaustion) i state
   end;
 
+(* handling of distinctness theorems *)
+
+datatype simproc_dist = QuickAndDirty
+                      | FewConstrs of thm list
+                      | ManyConstrs of thm * simpset;
+
 (********************** Internal description of datatypes *********************)
 
 datatype dtyp =
@@ -157,7 +165,7 @@
    case_rewrites : thm list,
    induction : thm,
    exhaustion : thm,
-   distinct : thm list,
+   distinct : simproc_dist,
    inject : thm list,
    nchotomy : thm,
    case_cong : thm};
@@ -172,8 +180,13 @@
       DtType (name, map (subst_DtTFree i substs) ts)
   | subst_DtTFree i _ (DtRec j) = DtRec (i + j);
 
-fun dest_DtTFree (DtTFree a) = a;
-fun dest_DtRec (DtRec i) = i;
+exception Datatype;
+
+fun dest_DtTFree (DtTFree a) = a
+  | dest_DtTFree _ = raise Datatype;
+
+fun dest_DtRec (DtRec i) = i
+  | dest_DtRec _ = raise Datatype;
 
 fun is_rec_type (DtType (_, dts)) = exists is_rec_type dts
   | is_rec_type (DtRec _) = true
@@ -201,6 +214,7 @@
 
 fun get_nonrec_types descr sorts =
   let fun add (Ts, T as DtTFree _) = T ins Ts
+        | add (Ts, T as DtType ("fun", [_, DtRec _])) = Ts
         | add (Ts, T as DtType _) = T ins Ts
         | add (Ts, _) = Ts
   in map (typ_of_dtyp descr sorts) (foldl (fn (Ts, (_, (_, _, constrs))) =>
@@ -213,6 +227,16 @@
 fun get_rec_types descr sorts = map (fn (_ , (s, ds, _)) =>
   Type (s, map (typ_of_dtyp descr sorts) ds)) descr;
 
+(* get all branching types *)
+
+fun get_branching_types descr sorts = 
+  let fun add (Ts, DtType ("fun", [T, DtRec _])) = T ins Ts
+        | add (Ts, _) = Ts
+  in map (typ_of_dtyp descr sorts) (foldl (fn (Ts, (_, (_, _, constrs))) =>
+    foldl (fn (Ts', (_, cargs)) =>
+      foldl add (Ts', cargs)) (Ts, constrs)) ([], descr))
+  end;
+
 (* nonemptiness check for datatypes *)
 
 fun check_nonempty descr =
@@ -223,6 +247,7 @@
         val (_, _, constrs) = the (assoc (descr', i));
         fun arg_nonempty (DtRec i) = if i mem is then false
               else is_nonempty_dt (i::is) i
+          | arg_nonempty (DtType ("fun", [_, T])) = arg_nonempty T
           | arg_nonempty _ = true;
       in exists ((forall arg_nonempty) o snd) constrs
       end
@@ -234,16 +259,19 @@
 (* all types of the form DtType (dt_name, [..., DtRec _, ...]) *)
 (* need to be unfolded                                         *)
 
-fun unfold_datatypes (dt_info : datatype_info Symtab.table) descr i =
+fun unfold_datatypes sign orig_descr sorts (dt_info : datatype_info Symtab.table) descr i =
   let
-    fun get_dt_descr i tname dts =
+    fun typ_error T msg = error ("Non-admissible type expression\n" ^
+      Sign.string_of_typ sign (typ_of_dtyp (orig_descr @ descr) sorts T) ^ "\n" ^ msg);
+
+    fun get_dt_descr T i tname dts =
       (case Symtab.lookup (dt_info, tname) of
-         None => error (tname ^ " is not a datatype - can't use it in\
-           \ indirect recursion")
+         None => typ_error T (tname ^ " is not a datatype - can't use it in\
+           \ nested recursion")
        | (Some {index, descr, ...}) =>
            let val (_, vars, _) = the (assoc (descr, index));
-               val subst = ((map dest_DtTFree vars) ~~ dts) handle _ =>
-                 error ("Type constructor " ^ tname ^ " used with wrong\
+               val subst = ((map dest_DtTFree vars) ~~ dts) handle LIST _ =>
+                 typ_error T ("Type constructor " ^ tname ^ " used with wrong\
                   \ number of arguments")
            in (i + index, map (fn (j, (tn, args, cs)) => (i + j,
              (tn, map (subst_DtTFree i subst) args,
@@ -254,9 +282,18 @@
 
     fun unfold_arg ((i, Ts, descrs), T as (DtType (tname, dts))) =
           if is_rec_type T then
-            let val (index, descr) = get_dt_descr i tname dts;
-                val (descr', i') = unfold_datatypes dt_info descr (i + length descr)
-            in (i', Ts @ [DtRec index], descrs @ descr') end
+            if tname = "fun" then
+              if is_rec_type (hd dts) then
+                typ_error T "Non-strictly positive recursive occurrence of type"
+              else
+                (case hd (tl dts) of
+                   DtType ("fun", _) => typ_error T "Curried function types not allowed"
+                 | T' => let val (i', [T''], descrs') = unfold_arg ((i, [], descrs), T')
+                         in (i', Ts @ [DtType (tname, [hd dts, T''])], descrs') end)
+            else
+              let val (index, descr) = get_dt_descr T i tname dts;
+                  val (descr', i') = unfold_datatypes sign orig_descr sorts dt_info descr (i + length descr)
+              in (i', Ts @ [DtRec index], descrs @ descr') end
           else (i, Ts @ [T], descrs)
       | unfold_arg ((i, Ts, descrs), T) = (i, Ts @ [T], descrs);
 
diff -r 11ee650edcd2 -r 85be09eb136c src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Fri Jul 16 12:09:48 1999 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Fri Jul 16 12:14:04 1999 +0200
@@ -11,6 +11,7 @@
   val mutual_induct_tac : string list -> int -> tactic
   val induct_tac : string -> int -> tactic
   val exhaust_tac : string -> int -> tactic
+  val distinct_simproc : simproc
 end;
 
 signature DATATYPE_PACKAGE =
@@ -63,9 +64,12 @@
        simps : thm list}
   val get_datatypes : theory -> DatatypeAux.datatype_info Symtab.table
   val print_datatypes : theory -> unit
-  val datatype_info_sg : Sign.sg -> string -> DatatypeAux.datatype_info
-  val datatype_info : theory -> string -> DatatypeAux.datatype_info
+  val datatype_info_sg : Sign.sg -> string -> DatatypeAux.datatype_info option
+  val datatype_info : theory -> string -> DatatypeAux.datatype_info option
+  val datatype_info_sg_err : Sign.sg -> string -> DatatypeAux.datatype_info
+  val datatype_info_err : theory -> string -> DatatypeAux.datatype_info
   val constrs_of : theory -> string -> term list option
+  val constrs_of_sg : Sign.sg -> string -> term list option
   val case_const_of : theory -> string -> term option
   val setup: (theory -> theory) list
 end;
@@ -104,28 +108,31 @@
 
 (** theory information about datatypes **)
 
-fun datatype_info_sg sg name =
-  (case Symtab.lookup (get_datatypes_sg sg, name) of
-    Some info => info
-  | None => error ("Unknown datatype " ^ quote name));
+fun datatype_info_sg sg name = Symtab.lookup (get_datatypes_sg sg, name);
+
+fun datatype_info_sg_err sg name = (case datatype_info_sg sg name of
+      Some info => info
+    | None => error ("Unknown datatype " ^ quote name));
 
 val datatype_info = datatype_info_sg o Theory.sign_of;
 
-fun constrs_of thy tname =
-  let
-    val {index, descr, ...} = datatype_info thy tname;
-    val (_, _, constrs) = the (assoc (descr, index))
-  in
-    Some (map (fn (cname, _) =>
-      Const (cname, the (Sign.const_type (Theory.sign_of thy) cname))) constrs)
-  end handle _ => None;
+fun datatype_info_err thy name = (case datatype_info thy name of
+      Some info => info
+    | None => error ("Unknown datatype " ^ quote name));
 
-fun case_const_of thy tname =
-  let
-    val {case_name, ...} = datatype_info thy tname;
-  in
-    Some (Const (case_name, the (Sign.const_type (Theory.sign_of thy) case_name)))
-  end handle _ => None;
+fun constrs_of_sg sg tname = (case datatype_info_sg sg tname of
+   Some {index, descr, ...} =>
+     let val (_, _, constrs) = the (assoc (descr, index))
+     in Some (map (fn (cname, _) => Const (cname, the (Sign.const_type sg cname))) constrs)
+     end
+ | _ => None);
+
+val constrs_of = constrs_of_sg o Theory.sign_of;
+
+fun case_const_of thy tname = (case datatype_info thy tname of
+   Some {case_name, ...} => Some (Const (case_name, the (Sign.const_type
+     (Theory.sign_of thy) case_name)))
+ | _ => None);
 
 fun find_tname var Bi =
   let val frees = map dest_Free (term_frees Bi)
@@ -168,7 +175,7 @@
     val (_, _, Bi, _) = dest_state (state, i);
     val {sign, ...} = rep_thm state;
     val tn = find_tname (hd vars) Bi;
-    val {induction, ...} = datatype_info_sg sign tn;
+    val {induction, ...} = datatype_info_sg_err sign tn;
     val ind_vnames = map (fn (_ $ Var (ixn, _)) =>
       implode (tl (explode (Syntax.string_of_vname ixn))))
         (dest_conj (HOLogic.dest_Trueprop (concl_of induction)));
@@ -186,7 +193,7 @@
   let
     val {sign, ...} = rep_thm state;
     val tn = infer_tname state sign i aterm;
-    val {exhaustion, ...} = datatype_info_sg sign tn;
+    val {exhaustion, ...} = datatype_info_sg_err sign tn;
     val _ $ Var (ixn, _) $ _ = HOLogic.dest_Trueprop
       (hd (Logic.strip_assums_hyp (hd (prems_of exhaustion))));
     val exh_vname = implode (tl (explode (Syntax.string_of_vname ixn)))
@@ -195,6 +202,61 @@
   end;
 
 
+(**** simplification procedure for showing distinctness of constructors ****)
+
+(* oracle *)
+
+val distinctN = "constr_distinct";
+
+exception ConstrDistinct of term;
+
+
+fun distinct_proc sg _ (t as Const ("op =", _) $ t1 $ t2) =
+  (case (pairself strip_comb (t1, t2)) of
+     ((Const (cname1, _), xs), (Const (cname2, _), ys)) =>
+         (case (fastype_of t1, fastype_of t2) of
+            (Type (tname1, _), Type (tname2, _)) =>
+                if tname1 = tname2 andalso not (cname1 = cname2) then
+                   (case (constrs_of_sg sg tname1) of
+                      Some constrs => let val cnames = map (fst o dest_Const) constrs
+                        in if cname1 mem cnames andalso cname2 mem cnames then
+                             let val eq_t = Logic.mk_equals (t, Const ("False", HOLogic.boolT));
+                                 val eq_ct = cterm_of sg eq_t;
+                                 val Datatype_thy = theory "Datatype";
+                                 val [In0_inject, In1_inject, In0_not_In1, In1_not_In0] =
+                                   map (get_thm Datatype_thy)
+                                     ["In0_inject", "In1_inject", "In0_not_In1", "In1_not_In0"]
+                             in (case (#distinct (datatype_info_sg_err sg tname1)) of
+                                 QuickAndDirty => Some (Thm.invoke_oracle
+                                   Datatype_thy distinctN (sg, ConstrDistinct eq_t))
+                               | FewConstrs thms => Some (prove_goalw_cterm [] eq_ct (K
+                                   [rtac eq_reflection 1, rtac iffI 1, rtac notE 1,
+                                    atac 2, resolve_tac thms 1, etac FalseE 1]))
+                               | ManyConstrs (thm, ss) => Some (prove_goalw_cterm [] eq_ct (K
+                                   [rtac eq_reflection 1, rtac iffI 1, dtac thm 1,
+                                    full_simp_tac ss 1,
+                                    REPEAT (dresolve_tac [In0_inject, In1_inject] 1),
+                                    eresolve_tac [In0_not_In1 RS notE, In1_not_In0 RS notE] 1,
+                                    etac FalseE 1])))
+                             end
+                           else None
+                        end
+                    | None => None)
+                else None
+          | _ => None)
+   | _ => None)
+  | distinct_proc sg _ _ = None;
+
+val distinct_pats = [Thm.read_cterm (Theory.sign_of HOL.thy) ("s = t", HOLogic.termTVar)];
+val distinct_simproc = mk_simproc "distinct_simproc" distinct_pats distinct_proc;
+
+val dist_ss = HOL_ss addsimprocs [distinct_simproc];
+
+val simproc_setup =
+  [Theory.add_oracle (distinctN, fn (_, ConstrDistinct t) => t),
+   fn thy => (simpset_ref_of thy := simpset_of thy addsimprocs [distinct_simproc]; thy)];
+
+
 (* prepare types *)
 
 fun read_typ sign ((Ts, sorts), str) =
@@ -240,7 +302,7 @@
 
 fun clasimp addDistinct ([], _) = clasimp
   | clasimp addDistinct (thms::thmss, (_, (_, _, constrs))::descr) =
-      if length constrs < DatatypeProp.dtK then
+      if length constrs < !DatatypeProp.dtK then
         clasimp addIffs thms addDistinct (thmss, descr)
       else
         clasimp addsimps2 thms addDistinct (thmss, descr);
@@ -275,6 +337,9 @@
     val used = foldr add_typ_tfree_names (recTs, []);
     val newTs = take (length (hd descr), recTs);
 
+    val no_size = exists (fn (_, (_, _, constrs)) => exists (fn (_, cargs) => exists
+      (fn (DtType ("fun", [_, DtRec _])) => true | _ => false) cargs) constrs) descr';
+
     (**** declare new types and constants ****)
 
     val tyvars = map (fn (_, (_, Ts, _)) => map dest_DtTFree Ts) (hd descr);
@@ -290,9 +355,14 @@
     val reccomb_fn_Ts = flat (map (fn (i, (_, _, constrs)) =>
       map (fn (_, cargs) =>
         let
-          val recs = filter is_rec_type cargs;
-          val argTs = (map (typ_of_dtyp descr' sorts) cargs) @
-            (map (fn r => nth_elem (dest_DtRec r, rec_result_Ts)) recs)
+          val Ts = map (typ_of_dtyp descr' sorts) cargs;
+          val recs = filter (is_rec_type o fst) (cargs ~~ Ts);
+
+          fun mk_argT (DtRec k, _) = nth_elem (k, rec_result_Ts)
+            | mk_argT (DtType ("fun", [_, DtRec k]), Type ("fun", [T, _])) =
+               T --> nth_elem (k, rec_result_Ts);
+
+          val argTs = Ts @ map mk_argT recs
         in argTs ---> nth_elem (i, rec_result_Ts)
         end) constrs) descr');
 
@@ -341,19 +411,11 @@
 
     val thy2 = thy2' |>
 
-      (** t_ord functions **)
-
-      Theory.add_consts_i
-        (foldr (fn ((((_, (_, _, constrs)), tname), T), decls) =>
-          if length constrs < DatatypeProp.dtK then decls
-          else (tname ^ "_ord", T --> HOLogic.natT, NoSyn)::decls)
-            ((hd descr) ~~ new_type_names ~~ newTs, [])) |>
-
       (** size functions **)
 
-      Theory.add_consts_i (map (fn (s, T) =>
+      (if no_size then I else Theory.add_consts_i (map (fn (s, T) =>
         (Sign.base_name s, T --> HOLogic.natT, NoSyn))
-          (size_names ~~ drop (length (hd descr), recTs))) |>
+          (size_names ~~ drop (length (hd descr), recTs)))) |>
 
       (** constructors **)
 
@@ -370,19 +432,19 @@
     (**** introduction of axioms ****)
 
     val rec_axs = DatatypeProp.make_primrecs new_type_names descr sorts thy2;
-    val size_axs = DatatypeProp.make_size new_type_names descr sorts thy2;
+    val size_axs = if no_size then [] else DatatypeProp.make_size new_type_names descr sorts thy2;
 
     val (thy3, inject) = thy2 |>
       Theory.add_path (space_implode "_" new_type_names) |>
       PureThy.add_axioms_i [(("induct", DatatypeProp.make_ind descr sorts), [])] |>
       PureThy.add_axiomss_i [(("recs", rec_axs), [])] |>
-      PureThy.add_axiomss_i [(("size", size_axs), [])] |>
+      (if no_size then I else PureThy.add_axiomss_i [(("size", size_axs), [])]) |>
       Theory.parent_path |>
       add_and_get_axiomss "inject" new_type_names
         (DatatypeProp.make_injs descr sorts);
     val induct = get_axiom thy3 "induct";
     val rec_thms = get_thms thy3 "recs";
-    val size_thms = get_thms thy3 "size";
+    val size_thms = if no_size then [] else get_thms thy3 "size";
     val (thy4, distinct) = add_and_get_axiomss "distinct" new_type_names
       (DatatypeProp.make_distincts new_type_names descr sorts thy3) thy3;
     val (thy5, exhaustion) = add_and_get_axioms "exhaust" new_type_names
@@ -401,7 +463,8 @@
     
     val dt_infos = map (make_dt_info descr' induct reccomb_names' rec_thms)
       ((0 upto length (hd descr) - 1) ~~ (hd descr) ~~ case_names' ~~ case_thms ~~
-        exhaustion ~~ distinct ~~ inject ~~ nchotomys ~~ case_congs);
+        exhaustion ~~ replicate (length (hd descr)) QuickAndDirty ~~ inject ~~
+          nchotomys ~~ case_congs);
 
     val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms;
 
@@ -413,7 +476,7 @@
 
     val _ = store_clasimp thy11 ((claset_of thy11, simpset_of thy11)
       addsimps2 flat case_thms addsimps2 size_thms addsimps2 rec_thms
-      addIffs flat inject addDistinct (distinct, hd descr));
+      addIffs flat (inject @ distinct));
 
   in
     (thy11,
@@ -435,18 +498,16 @@
   let
     val _ = message ("Proofs for datatype(s) " ^ commas_quote new_type_names);
 
-    val (thy2, inject, dist_rewrites, induct) = thy |>
+    val (thy2, inject, distinct, dist_rewrites, simproc_dists, induct) = thy |>
       DatatypeRepProofs.representation_proofs flat_names dt_info new_type_names descr sorts
         types_syntax constr_syntax;
 
     val (thy3, casedist_thms) =
       DatatypeAbsProofs.prove_casedist_thms new_type_names descr sorts induct thy2;
     val (thy4, reccomb_names, rec_thms) = DatatypeAbsProofs.prove_primrec_thms
-      flat_names new_type_names descr sorts dt_info inject dist_rewrites induct thy3;
-    val (thy5, case_names, case_thms) = DatatypeAbsProofs.prove_case_thms
+      flat_names new_type_names descr sorts dt_info inject dist_rewrites dist_ss induct thy3;
+    val (thy6, case_names, case_thms) = DatatypeAbsProofs.prove_case_thms
       flat_names new_type_names descr sorts reccomb_names rec_thms thy4;
-    val (thy6, distinct) = DatatypeAbsProofs.prove_distinctness_thms
-      flat_names new_type_names descr sorts dist_rewrites case_thms thy5;
     val (thy7, split_thms) = DatatypeAbsProofs.prove_split_thms new_type_names
       descr sorts inject dist_rewrites casedist_thms case_thms thy6;
     val (thy8, nchotomys) = DatatypeAbsProofs.prove_nchotomys new_type_names
@@ -458,7 +519,7 @@
 
     val dt_infos = map (make_dt_info (flat descr) induct reccomb_names rec_thms)
       ((0 upto length (hd descr) - 1) ~~ (hd descr) ~~ case_names ~~ case_thms ~~
-        casedist_thms ~~ distinct ~~ inject ~~ nchotomys ~~ case_congs);
+        casedist_thms ~~ simproc_dists ~~ inject ~~ nchotomys ~~ case_congs);
 
     val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms;
 
@@ -470,7 +531,7 @@
 
     val _ = store_clasimp thy11 ((claset_of thy11, simpset_of thy11)
       addsimps2 flat case_thms addsimps2 size_thms addsimps2 rec_thms
-      addIffs flat inject addDistinct (distinct, hd descr));
+      addIffs flat (inject @ distinct));
 
   in
     (thy11,
@@ -505,7 +566,7 @@
       Sign.string_of_term sign t);
 
     fun get_typ (t as _ $ Var (_, Type (tname, Ts))) =
-          ((tname, map dest_TFree Ts) handle _ => err t)
+          ((tname, map dest_TFree Ts) handle TERM _ => err t)
       | get_typ t = err t;
 
     val dtnames = map get_typ (dest_conj (HOLogic.dest_Trueprop (concl_of induction')));
@@ -535,7 +596,7 @@
     val (thy2, casedist_thms) = thy1 |>
       DatatypeAbsProofs.prove_casedist_thms new_type_names [descr] sorts induction;
     val (thy3, reccomb_names, rec_thms) = DatatypeAbsProofs.prove_primrec_thms
-      false new_type_names [descr] sorts dt_info inject distinct induction thy2;
+      false new_type_names [descr] sorts dt_info inject distinct dist_ss induction thy2;
     val (thy4, case_names, case_thms) = DatatypeAbsProofs.prove_case_thms false
       new_type_names [descr] sorts reccomb_names rec_thms thy3;
     val (thy5, split_thms) = DatatypeAbsProofs.prove_split_thms
@@ -552,7 +613,7 @@
 
     val dt_infos = map (make_dt_info descr induction reccomb_names rec_thms)
       ((0 upto length descr - 1) ~~ descr ~~ case_names ~~ case_thms ~~
-        casedist_thms ~~ distinct ~~ inject ~~ nchotomys ~~ case_congs);
+        casedist_thms ~~ map FewConstrs distinct ~~ inject ~~ nchotomys ~~ case_congs);
 
     val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms;
 
@@ -564,7 +625,7 @@
 
     val _ = store_clasimp thy9 ((claset_of thy9, simpset_of thy9)
       addsimps2 flat case_thms addsimps2 size_thms addsimps2 rec_thms
-      addIffs flat inject addDistinct (distinct, descr));
+      addIffs flat (inject @ distinct));
 
   in
     (thy9,
@@ -641,10 +702,10 @@
       end;
 
     val (dts', constr_syntax, sorts', i) = foldl prep_dt_spec (([], [], [], 0), dts);
+    val sorts = sorts' @ (map (rpair (Sign.defaultS sign)) (tyvars \\ map fst sorts'));
     val dt_info = get_datatypes thy;
-    val (descr, _) = unfold_datatypes dt_info dts' i;
+    val (descr, _) = unfold_datatypes sign dts' sorts dt_info dts' i;
     val _ = check_nonempty descr;
-    val sorts = sorts' @ (map (rpair (Sign.defaultS sign)) (tyvars \\ map fst sorts'));
 
   in
     (if (!quick_and_dirty) then add_datatype_axm else add_datatype_def)
@@ -659,7 +720,7 @@
 
 (* setup theory *)
 
-val setup = [DatatypesData.init];
+val setup = [DatatypesData.init] @ simproc_setup;
 
 
 (* outer syntax *)
diff -r 11ee650edcd2 -r 85be09eb136c src/HOL/Tools/datatype_prop.ML
--- a/src/HOL/Tools/datatype_prop.ML	Fri Jul 16 12:09:48 1999 +0200
+++ b/src/HOL/Tools/datatype_prop.ML	Fri Jul 16 12:14:04 1999 +0200
@@ -8,7 +8,7 @@
 
 signature DATATYPE_PROP =
 sig
-  val dtK : int
+  val dtK : int ref
   val make_injs : (int * (string * DatatypeAux.dtyp list *
     (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
       term list list
@@ -46,7 +46,7 @@
 open DatatypeAux;
 
 (*the kind of distinctiveness axioms depends on number of constructors*)
-val dtK = 7;
+val dtK = ref 7;
 
 fun make_tnames Ts =
   let
@@ -110,14 +110,19 @@
 
     fun make_ind_prem k T (cname, cargs) =
       let
+        fun mk_prem ((DtRec k, s), T) = HOLogic.mk_Trueprop
+              (make_pred k T $ Free (s, T))
+          | mk_prem ((DtType ("fun", [_, DtRec k]), s), T' as Type ("fun", [T, U])) =
+              HOLogic.mk_Trueprop (HOLogic.all_const T $
+                Abs ("x", T, make_pred k U $ (Free (s, T') $ Bound 0)));
+
         val recs = filter is_rec_type cargs;
         val Ts = map (typ_of_dtyp descr' sorts) cargs;
         val recTs' = map (typ_of_dtyp descr' sorts) recs;
         val tnames = variantlist (make_tnames Ts, pnames);
         val rec_tnames = map fst (filter (is_rec_type o snd) (tnames ~~ cargs));
         val frees = tnames ~~ Ts;
-        val prems = map (fn ((r, s), T) => HOLogic.mk_Trueprop
-          (make_pred (dest_DtRec r) T $ Free (s, T))) (recs ~~ rec_tnames ~~ recTs');
+        val prems = map mk_prem (recs ~~ rec_tnames ~~ recTs');
 
       in list_all_free (frees, Logic.list_implies (prems,
         HOLogic.mk_Trueprop (make_pred k T $ 
@@ -162,6 +167,8 @@
 
 fun make_primrecs new_type_names descr sorts thy =
   let
+    val o_name = Sign.intern_const (sign_of Fun.thy) "op o";
+
     val sign = Theory.sign_of thy;
 
     val descr' = flat descr;
@@ -174,9 +181,14 @@
     val reccomb_fn_Ts = flat (map (fn (i, (_, _, constrs)) =>
       map (fn (_, cargs) =>
         let
-          val recs = filter is_rec_type cargs;
-          val argTs = (map (typ_of_dtyp descr' sorts) cargs) @
-            (map (fn r => nth_elem (dest_DtRec r, rec_result_Ts)) recs)
+          val Ts = map (typ_of_dtyp descr' sorts) cargs;
+          val recs = filter (is_rec_type o fst) (cargs ~~ Ts);
+
+          fun mk_argT (DtRec k, _) = nth_elem (k, rec_result_Ts)
+            | mk_argT (DtType ("fun", [_, DtRec k]), Type ("fun", [T, _])) =
+               T --> nth_elem (k, rec_result_Ts);
+
+          val argTs = Ts @ map mk_argT recs
         in argTs ---> nth_elem (i, rec_result_Ts)
         end) constrs) descr');
 
@@ -201,7 +213,14 @@
         val rec_tnames = map fst (filter (is_rec_type o snd) (tnames ~~ cargs));
         val frees = map Free (tnames ~~ Ts);
         val frees' = map Free (rec_tnames ~~ recTs');
-        val reccombs' = map (fn (DtRec i) => nth_elem (i, reccombs)) recs
+
+        fun mk_reccomb (DtRec i, _) = nth_elem (i, reccombs)
+          | mk_reccomb (DtType ("fun", [_, DtRec i]), Type ("fun", [T, U])) =
+              let val T' = nth_elem (i, rec_result_Ts)
+              in Const (o_name, [U --> T', T --> U, T] ---> T') $ nth_elem (i, reccombs)
+              end;
+
+        val reccombs' = map mk_reccomb (recs ~~ recTs')
 
       in (ts @ [HOLogic.mk_Trueprop (HOLogic.mk_eq
         (comb_t $ list_comb (Const (cname, Ts ---> T), frees),
@@ -292,35 +311,12 @@
           in (make_distincts' constrs) @ (make_distincts_1 T constrs)
           end;
 
-    (**** number of constructors >= dtK : t_ord C_i ... = i ****)
-
-    fun make_distincts_2 T tname i constrs =
-      let
-        val ord_name = Sign.intern_const (Theory.sign_of thy) (tname ^ "_ord");
-        val ord_t = Const (ord_name, T --> HOLogic.natT)
-
-      in (case constrs of
-          [] => [Logic.mk_implies (HOLogic.mk_Trueprop (Not $ HOLogic.mk_eq
-             (ord_t $ Free ("x", T), ord_t $ Free ("y", T))),
-               HOLogic.mk_Trueprop (Not $ HOLogic.mk_eq
-                 (Free ("x", T), Free ("y", T))))]
-        | ((cname, cargs)::constrs) =>
-            let
-              val Ts = map (typ_of_dtyp descr' sorts) cargs;
-              val frees = map Free ((make_tnames Ts) ~~ Ts);
-            in
-              (HOLogic.mk_Trueprop (HOLogic.mk_eq (ord_t $
-                list_comb (Const (cname, Ts ---> T), frees), HOLogic.mk_nat i)))::
-                  (make_distincts_2 T tname (i + 1) constrs)
-            end)
-      end;
-
   in map (fn (((_, (_, _, constrs)), T), tname) =>
-      if length constrs < dtK then make_distincts_1 T constrs
-      else make_distincts_2 T tname 0 constrs)
+      if length constrs < !dtK then make_distincts_1 T constrs else [])
         ((hd descr) ~~ newTs ~~ new_type_names)
   end;
 
+
 (*************************** the "split" - equations **************************)
 
 fun make_splits new_type_names descr sorts thy =
@@ -403,7 +399,7 @@
     val recTs = get_rec_types descr' sorts;
 
     val big_size_name = space_implode "_" new_type_names ^ "_size";
-    val size_name = Sign.intern_const (Theory.sign_of (the (get_thy "Arith" thy))) "size";
+    val size_name = Sign.intern_const (Theory.sign_of (theory "Arith")) "size";
     val size_names = replicate (length (hd descr)) size_name @
       map (Sign.intern_const (Theory.sign_of thy))
         (if length (flat (tl descr)) = 1 then [big_size_name] else
diff -r 11ee650edcd2 -r 85be09eb136c src/HOL/Tools/datatype_rep_proofs.ML
--- a/src/HOL/Tools/datatype_rep_proofs.ML	Fri Jul 16 12:09:48 1999 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML	Fri Jul 16 12:14:04 1999 +0200
@@ -12,13 +12,16 @@
 
 *)
 
+val foo = ref [TrueI];
+
 signature DATATYPE_REP_PROOFS =
 sig
   val representation_proofs : bool -> DatatypeAux.datatype_info Symtab.table ->
     string list -> (int * (string * DatatypeAux.dtyp list *
       (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
         (string * mixfix) list -> (string * mixfix) list list -> theory ->
-          theory * thm list list * thm list list * thm
+          theory * thm list list * thm list list * thm list list *
+            DatatypeAux.simproc_dist list * thm
 end;
 
 structure DatatypeRepProofs : DATATYPE_REP_PROOFS =
@@ -43,15 +46,22 @@
 fun representation_proofs flat_names (dt_info : datatype_info Symtab.table)
       new_type_names descr sorts types_syntax constr_syntax thy =
   let
-    val Univ_thy = the (get_thy "Univ" thy);
-    val node_name = Sign.intern_tycon (Theory.sign_of Univ_thy) "node";
-    val [In0_name, In1_name, Scons_name, Leaf_name, Numb_name] =
-      map (Sign.intern_const (Theory.sign_of Univ_thy))
-        ["In0", "In1", "Scons", "Leaf", "Numb"];
+    val Datatype_thy = theory "Datatype";
+    val node_name = Sign.intern_tycon (Theory.sign_of Datatype_thy) "node";
+    val [In0_name, In1_name, Scons_name, Leaf_name, Numb_name, Lim_name,
+      Funs_name, o_name] =
+      map (Sign.intern_const (Theory.sign_of Datatype_thy))
+        ["In0", "In1", "Scons", "Leaf", "Numb", "Lim", "Funs", "op o"];
+
     val [In0_inject, In1_inject, Scons_inject, Leaf_inject, In0_eq, In1_eq,
-      In0_not_In1, In1_not_In0] = map (get_thm Univ_thy)
-        ["In0_inject", "In1_inject", "Scons_inject", "Leaf_inject", "In0_eq",
-         "In1_eq", "In0_not_In1", "In1_not_In0"];
+         In0_not_In1, In1_not_In0, Funs_mono, FunsI, Lim_inject,
+         Funs_inv, FunsD, Funs_rangeE, Funs_nonempty] = map (get_thm Datatype_thy)
+        ["In0_inject", "In1_inject", "Scons_inject", "Leaf_inject", "In0_eq", "In1_eq",
+         "In0_not_In1", "In1_not_In0", "Funs_mono", "FunsI", "Lim_inject",
+         "Funs_inv", "FunsD", "Funs_rangeE", "Funs_nonempty"];
+
+    val Funs_IntE = (Int_lower2 RS Funs_mono RS
+      (Int_lower1 RS Funs_mono RS Int_greatest) RS subsetD) RS IntE;
 
     val descr' = flat descr;
 
@@ -65,19 +75,23 @@
 
     val tyvars = map (fn (_, (_, Ts, _)) => map dest_DtTFree Ts) (hd descr);
     val leafTs' = get_nonrec_types descr' sorts;
-    val unneeded_vars = hd tyvars \\ foldr add_typ_tfree_names (leafTs', []);
+    val branchTs = get_branching_types descr' sorts;
+    val branchT = if null branchTs then HOLogic.unitT
+      else fold_bal (fn (T, U) => Type ("+", [T, U])) branchTs;
+    val unneeded_vars = hd tyvars \\ foldr add_typ_tfree_names (leafTs' @ branchTs, []);
     val leafTs = leafTs' @ (map (fn n => TFree (n, the (assoc (sorts, n)))) unneeded_vars);
     val recTs = get_rec_types descr' sorts;
     val newTs = take (length (hd descr), recTs);
     val oldTs = drop (length (hd descr), recTs);
     val sumT = if null leafTs then HOLogic.unitT
       else fold_bal (fn (T, U) => Type ("+", [T, U])) leafTs;
-    val Univ_elT = HOLogic.mk_setT (Type (node_name, [sumT]));
+    val Univ_elT = HOLogic.mk_setT (Type (node_name, [sumT, branchT]));
     val UnivT = HOLogic.mk_setT Univ_elT;
 
     val In0 = Const (In0_name, Univ_elT --> Univ_elT);
     val In1 = Const (In1_name, Univ_elT --> Univ_elT);
     val Leaf = Const (Leaf_name, sumT --> Univ_elT);
+    val Lim = Const (Lim_name, (branchT --> Univ_elT) --> Univ_elT);
 
     (* make injections needed for embedding types in leaves *)
 
@@ -103,6 +117,25 @@
       else
         foldr1 (HOLogic.mk_binop Scons_name) ts);
 
+    (* function spaces *)
+
+    fun mk_fun_inj T' x =
+      let
+        fun mk_inj T n i =
+          if n = 1 then x else
+          let
+            val n2 = n div 2;
+            val Type (_, [T1, T2]) = T;
+            val sum_case = Const ("sum_case", [T1 --> Univ_elT, T2 --> Univ_elT, T] ---> Univ_elT)
+          in
+            if i <= n2 then
+              sum_case $ (mk_inj T1 n2 i) $ Const ("arbitrary", T2 --> Univ_elT)
+            else
+              sum_case $ Const ("arbitrary", T1 --> Univ_elT) $ mk_inj T2 (n - n2) (i - n2)
+          end
+      in mk_inj branchT (length branchTs) (1 + find_index_eq T' branchTs)
+      end;
+
     (************** generate introduction rules for representing set **********)
 
     val _ = message "Constructing representing sets ...";
@@ -116,6 +149,14 @@
               in (j + 1, (HOLogic.mk_mem (free_t,
                 Const (nth_elem (k, rep_set_names), UnivT)))::prems, free_t::ts)
               end
+          | mk_prem (DtType ("fun", [T, DtRec k]), (j, prems, ts)) =
+              let val T' = typ_of_dtyp descr' sorts T;
+                  val free_t = mk_Free "x" (T' --> Univ_elT) j
+              in (j + 1, (HOLogic.mk_mem (free_t,
+                Const (Funs_name, UnivT --> HOLogic.mk_setT (T' --> Univ_elT)) $
+                  Const (nth_elem (k, rep_set_names), UnivT)))::prems,
+                    Lim $ mk_fun_inj T' free_t::ts)
+              end
           | mk_prem (dt, (j, prems, ts)) =
               let val T = typ_of_dtyp descr' sorts dt
               in (j + 1, prems, (Leaf $ mk_inj T (mk_Free "x" T j))::ts)
@@ -136,16 +177,17 @@
     val (thy2, {raw_induct = rep_induct, intrs = rep_intrs, ...}) =
       setmp InductivePackage.quiet_mode (!quiet_mode)
         (InductivePackage.add_inductive_i false true big_rec_name false true false
-           consts [] (map (fn x => (("", x), [])) intr_ts) [] []) thy1;
+           consts [] (map (fn x => (("", x), [])) intr_ts) [Funs_mono] []) thy1;
 
     (********************************* typedef ********************************)
 
     val thy3 = add_path flat_names big_name (foldl (fn (thy, ((((name, mx), tvs), c), name')) =>
       setmp TypedefPackage.quiet_mode true
         (TypedefPackage.add_typedef_i_no_def name' (name, tvs, mx) c [] []
-          (Some (QUIET_BREADTH_FIRST (has_fewer_prems 1) (resolve_tac rep_intrs 1)))) thy)
-            (parent_path flat_names thy2, types_syntax ~~ tyvars ~~ (take (length newTs, consts)) ~~
-              new_type_names));
+          (Some (QUIET_BREADTH_FIRST (has_fewer_prems 1)
+            (resolve_tac (Funs_nonempty::rep_intrs) 1)))) thy)
+              (parent_path flat_names thy2, types_syntax ~~ tyvars ~~
+                (take (length newTs, consts)) ~~ new_type_names));
 
     (*********************** definition of constructors ***********************)
 
@@ -171,6 +213,13 @@
           in (case dt of
               DtRec m => (j + 1, free_t::l_args, (Const (nth_elem (m, all_rep_names),
                 T --> Univ_elT) $ free_t)::r_args)
+            | DtType ("fun", [T', DtRec m]) =>
+                let val ([T''], T''') = strip_type T
+                in (j + 1, free_t::l_args, (Lim $ mk_fun_inj T''
+                  (Const (o_name, [T''' --> Univ_elT, T, T''] ---> Univ_elT) $
+                    Const (nth_elem (m, all_rep_names), T''' --> Univ_elT) $ free_t))::r_args)
+                end
+
             | _ => (j + 1, free_t::l_args, (Leaf $ mk_inj T free_t)::r_args))
           end;
 
@@ -200,8 +249,8 @@
         val sg = Theory.sign_of thy;
         val rep_const = cterm_of sg
           (Const (Sign.intern_const sg ("Rep_" ^ tname), T --> Univ_elT));
-        val cong' = cterm_instantiate [(cterm_of sg cong_f, rep_const)] arg_cong;
-        val dist = cterm_instantiate [(cterm_of sg distinct_f, rep_const)] distinct_lemma;
+        val cong' = standard (cterm_instantiate [(cterm_of sg cong_f, rep_const)] arg_cong);
+        val dist = standard (cterm_instantiate [(cterm_of sg distinct_f, rep_const)] distinct_lemma);
         val (thy', defs', eqns', _) = foldl ((make_constr_def tname T) (length constrs))
           ((add_path flat_names tname thy, defs, [], 1), constrs ~~ constr_syntax)
       in
@@ -282,23 +331,34 @@
         val rep_const = Const (rep_name, T --> Univ_elT);
         val constr = Const (cname, argTs ---> T);
 
-        fun process_arg ks' ((i2, i2', ts), dt) =
+        fun process_arg ks' ((i2, i2', ts, Ts), dt) =
           let val T' = typ_of_dtyp descr' sorts dt
           in (case dt of
               DtRec j => if j mem ks' then
-                  (i2 + 1, i2' + 1, ts @ [mk_Free "y" Univ_elT i2'])
+                  (i2 + 1, i2' + 1, ts @ [mk_Free "y" Univ_elT i2'], Ts @ [Univ_elT])
                 else
                   (i2 + 1, i2', ts @ [Const (nth_elem (j, all_rep_names),
-                    T' --> Univ_elT) $ mk_Free "x" T' i2])
-            | _ => (i2 + 1, i2', ts @ [Leaf $ mk_inj T' (mk_Free "x" T' i2)]))
+                    T' --> Univ_elT) $ mk_Free "x" T' i2], Ts)
+            | (DtType ("fun", [_, DtRec j])) =>
+                let val ([T''], T''') = strip_type T'
+                in if j mem ks' then
+                    (i2 + 1, i2' + 1, ts @ [Lim $ mk_fun_inj T''
+                      (mk_Free "y" (T'' --> Univ_elT) i2')], Ts @ [T'' --> Univ_elT])
+                  else
+                    (i2 + 1, i2', ts @ [Lim $ mk_fun_inj T''
+                      (Const (o_name, [T''' --> Univ_elT, T', T''] ---> Univ_elT) $
+                        Const (nth_elem (j, all_rep_names), T''' --> Univ_elT) $
+                          mk_Free "x" T' i2)], Ts)
+                end
+            | _ => (i2 + 1, i2', ts @ [Leaf $ mk_inj T' (mk_Free "x" T' i2)], Ts))
           end;
 
-        val (i2, i2', ts) = foldl (process_arg ks) ((1, 1, []), cargs);
+        val (i2, i2', ts, Ts) = foldl (process_arg ks) ((1, 1, [], []), cargs);
         val xs = map (uncurry (mk_Free "x")) (argTs ~~ (1 upto (i2 - 1)));
-        val ys = map (mk_Free "y" Univ_elT) (1 upto (i2' - 1));
+        val ys = map (uncurry (mk_Free "y")) (Ts ~~ (1 upto (i2' - 1)));
         val f = list_abs_free (map dest_Free (xs @ ys), mk_univ_inj ts n i);
 
-        val (_, _, ts') = foldl (process_arg []) ((1, 1, []), cargs);
+        val (_, _, ts', _) = foldl (process_arg []) ((1, 1, [], []), cargs);
         val eqn = HOLogic.mk_Trueprop (HOLogic.mk_eq
           (rep_const $ list_comb (constr, xs), mk_univ_inj ts' n i))
 
@@ -340,6 +400,21 @@
 
     (* prove isomorphism properties *)
 
+    fun mk_funs_inv thm =
+      let
+        val [_, t] = prems_of Funs_inv;
+        val [_ $ (_ $ _ $ R)] = Logic.strip_assums_hyp t;
+        val _ $ (_ $ (r $ (a $ _)) $ _) = Logic.strip_assums_concl t;
+        val [_ $ (_ $ _ $ R')] = prems_of thm;
+        val _ $ (_ $ (r' $ (a' $ _)) $ _) = concl_of thm;
+        val inv' = cterm_instantiate (map 
+          ((pairself (cterm_of (sign_of_thm thm))) o
+           (apsnd (map_term_types (incr_tvar 1))))
+             [(R, R'), (r, r'), (a, a')]) Funs_inv
+      in
+        rule_by_tactic (atac 2) (thm RSN (2, inv'))
+      end;
+
     (* prove  x : dt_rep_set_i --> x : range dt_Rep_i *)
 
     fun mk_iso_t (((set_name, iso_name), i), T) =
@@ -355,8 +430,6 @@
     val iso_t = HOLogic.mk_Trueprop (mk_conj (map mk_iso_t
       (rep_set_names ~~ all_rep_names ~~ (0 upto (length descr' - 1)) ~~ recTs)));
 
-    val newT_Abs_inverse_thms = map (fn (iso, _, _) => iso RS subst) newT_iso_axms;
-
     (* all the theorems are proved by one single simultaneous induction *)
 
     val iso_thms = if length descr = 1 then [] else
@@ -365,14 +438,19 @@
            [indtac rep_induct 1,
             REPEAT (rtac TrueI 1),
             REPEAT (EVERY
-              [REPEAT (etac rangeE 1),
-               REPEAT (eresolve_tac newT_Abs_inverse_thms 1),
+              [rewrite_goals_tac [mk_meta_eq Collect_mem_eq],
+               REPEAT (etac Funs_IntE 1),
+               REPEAT (eresolve_tac [rangeE, Funs_rangeE] 1),
+               REPEAT (eresolve_tac (map (fn (iso, _, _) => iso RS subst) newT_iso_axms @
+                 map (fn (iso, _, _) => mk_funs_inv iso RS subst) newT_iso_axms) 1),
                TRY (hyp_subst_tac 1),
                rtac (sym RS range_eqI) 1,
                resolve_tac iso_char_thms 1])])));
 
-    val Abs_inverse_thms = newT_Abs_inverse_thms @ (map (fn r =>
-      r RS mp RS f_inv_f RS subst) iso_thms);
+    val Abs_inverse_thms' = (map #1 newT_iso_axms) @ map (fn r => r RS mp RS f_inv_f) iso_thms;
+
+    val Abs_inverse_thms = map (fn r => r RS subst) (Abs_inverse_thms' @
+      map mk_funs_inv Abs_inverse_thms');
 
     (* prove  inj dt_Rep_i  and  dt_Rep_i x : dt_rep_set_i *)
 
@@ -395,7 +473,7 @@
         val (ind_concl1, ind_concl2) = ListPair.unzip (map mk_ind_concl ds);
 
         val rewrites = map mk_meta_eq iso_char_thms;
-        val inj_thms' = map (fn r => r RS injD) inj_thms;
+        val inj_thms' = flat (map (fn r => [r RS injD, r RS inj_o]) inj_thms);
 
         val inj_thm = prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5)
           (HOLogic.mk_Trueprop (mk_conj ind_concl1))) (fn _ =>
@@ -411,8 +489,9 @@
                    ORELSE (EVERY
                      [REPEAT (etac Scons_inject 1),
                       REPEAT (dresolve_tac
-                        (inj_thms' @ [Leaf_inject, Inl_inject, Inr_inject]) 1),
-                      REPEAT (EVERY [etac allE 1, dtac mp 1, atac 1]),
+                        (inj_thms' @ [Leaf_inject, Lim_inject, Inl_inject, Inr_inject]) 1),
+                      REPEAT ((EVERY [etac allE 1, dtac mp 1, atac 1]) ORELSE
+                              (dtac inj_fun_lemma 1 THEN atac 1)),
                       TRY (hyp_subst_tac 1),
                       rtac refl 1])])])]);
 
@@ -425,11 +504,11 @@
 	       (HOLogic.mk_Trueprop (mk_conj ind_concl2)))
 	      (fn _ =>
 	       [indtac induction 1,
-		rewrite_goals_tac rewrites,
+		rewrite_goals_tac (o_def :: rewrites),
 		REPEAT (EVERY
 			[resolve_tac rep_intrs 1,
-			 REPEAT ((atac 1) ORELSE
-				 (resolve_tac elem_thms 1))])]);
+			 REPEAT (FIRST [atac 1, etac spec 1,
+				 resolve_tac (FunsI :: elem_thms) 1])])]);
 
       in (inj_thms @ inj_thms'', elem_thms @ (split_conj_thm elem_thm))
       end;
@@ -446,19 +525,18 @@
     fun prove_constr_rep_thm eqn =
       let
         val inj_thms = map (fn (r, _) => r RS inj_onD) newT_iso_inj_thms;
-        val rewrites = constr_defs @ (map (mk_meta_eq o #2) newT_iso_axms)
+        val rewrites = o_def :: constr_defs @ (map (mk_meta_eq o #2) newT_iso_axms)
       in prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5) eqn) (fn _ =>
         [resolve_tac inj_thms 1,
          rewrite_goals_tac rewrites,
          rtac refl 1,
          resolve_tac rep_intrs 2,
-         REPEAT (resolve_tac iso_elem_thms 1)])
+         REPEAT (resolve_tac (FunsI :: iso_elem_thms) 1)])
       end;
 
     (*--------------------------------------------------------------*)
     (* constr_rep_thms and rep_congs are used to prove distinctness *)
-    (* of constructors internally.                                  *)
-    (* the external version uses dt_case which is not defined yet   *)
+    (* of constructors.                                             *)
     (*--------------------------------------------------------------*)
 
     val constr_rep_thms = map (map prove_constr_rep_thm) constr_rep_eqns;
@@ -467,27 +545,45 @@
       dist_lemma::(rep_thms @ [In0_eq, In1_eq, In0_not_In1, In1_not_In0]))
         (constr_rep_thms ~~ dist_lemmas);
 
+    fun prove_distinct_thms (_, []) = []
+      | prove_distinct_thms (dist_rewrites', t::_::ts) =
+          let
+            val dist_thm = prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5) t) (fn _ =>
+              [simp_tac (HOL_ss addsimps dist_rewrites') 1])
+          in dist_thm::(standard (dist_thm RS not_sym))::
+            (prove_distinct_thms (dist_rewrites', ts))
+          end;
+
+    val distinct_thms = map prove_distinct_thms (dist_rewrites ~~
+      DatatypeProp.make_distincts new_type_names descr sorts thy5);
+
+    val simproc_dists = map (fn ((((_, (_, _, constrs)), rep_thms), congr), dists) =>
+      if length constrs < !DatatypeProp.dtK then FewConstrs dists
+      else ManyConstrs (congr, HOL_basic_ss addsimps rep_thms)) (hd descr ~~
+        constr_rep_thms ~~ rep_congs ~~ distinct_thms);
+
     (* prove injectivity of constructors *)
 
     fun prove_constr_inj_thm rep_thms t =
-      let val inj_thms = Scons_inject::(map make_elim
+      let val inj_thms = Scons_inject::sum_case_inject::(map make_elim
         ((map (fn r => r RS injD) iso_inj_thms) @
-          [In0_inject, In1_inject, Leaf_inject, Inl_inject, Inr_inject]))
+          [In0_inject, In1_inject, Leaf_inject, Inl_inject, Inr_inject, Lim_inject]))
       in prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5) t) (fn _ =>
         [rtac iffI 1,
          REPEAT (etac conjE 2), hyp_subst_tac 2, rtac refl 2,
          dresolve_tac rep_congs 1, dtac box_equals 1,
-         REPEAT (resolve_tac rep_thms 1),
+         REPEAT (resolve_tac rep_thms 1), rewrite_goals_tac [o_def],
          REPEAT (eresolve_tac inj_thms 1),
-         hyp_subst_tac 1,
-         REPEAT (resolve_tac [conjI, refl] 1)])
+         REPEAT (ares_tac [conjI] 1 ORELSE (EVERY [rtac ext 1, dtac fun_cong 1,
+                  eresolve_tac inj_thms 1, atac 1]))])
       end;
 
     val constr_inject = map (fn (ts, thms) => map (prove_constr_inj_thm thms) ts)
       ((DatatypeProp.make_injs descr sorts) ~~ constr_rep_thms);
 
-    val thy6 = store_thmss "inject" new_type_names
-      constr_inject (parent_path flat_names thy5);
+    val thy6 = thy5 |> parent_path flat_names |>
+      store_thmss "inject" new_type_names constr_inject |>
+      store_thmss "distinct" new_type_names distinct_thms;
 
     (*************************** induction theorem ****************************)
 
@@ -538,17 +634,18 @@
       (DatatypeProp.make_ind descr sorts)) (fn prems =>
         [rtac indrule_lemma' 1, indtac rep_induct 1,
          EVERY (map (fn (prem, r) => (EVERY
-           [REPEAT (eresolve_tac Abs_inverse_thms 1),
+           [REPEAT (eresolve_tac (Funs_IntE::Abs_inverse_thms) 1),
             simp_tac (HOL_basic_ss addsimps ((symmetric r)::Rep_inverse_thms')) 1,
-            DEPTH_SOLVE_1 (ares_tac [prem] 1)]))
-              (prems ~~ (constr_defs @ (map mk_meta_eq iso_char_thms))))]);
+            DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE (EVERY [rewrite_goals_tac [o_def],
+              rtac allI 1, dtac FunsD 1, etac CollectD 1]))]))
+                (prems ~~ (constr_defs @ (map mk_meta_eq iso_char_thms))))]);
 
     val thy7 = thy6 |>
       Theory.add_path big_name |>
       PureThy.add_thms [(("induct", dt_induct), [])] |>
       Theory.parent_path;
 
-  in (thy7, constr_inject, dist_rewrites, dt_induct)
+  in (thy7, constr_inject, distinct_thms, dist_rewrites, simproc_dists, dt_induct)
   end;
 
 end;