- Datatype package now also supports arbitrarily branching datatypes
authorberghofe
Fri Jul 16 12:14:04 1999 +0200 (1999-07-16)
changeset 701585be09eb136c
parent 7014 11ee650edcd2
child 7016 df54b5365477
- 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.
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_rep_proofs.ML
     1.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Fri Jul 16 12:09:48 1999 +0200
     1.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Fri Jul 16 12:14:04 1999 +0200
     1.3 @@ -25,13 +25,10 @@
     1.4    val prove_primrec_thms : bool -> string list -> (int * (string * DatatypeAux.dtyp list *
     1.5      (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
     1.6        DatatypeAux.datatype_info Symtab.table -> thm list list -> thm list list ->
     1.7 -        thm -> theory -> theory * string list * thm list
     1.8 +        simpset -> thm -> theory -> theory * string list * thm list
     1.9    val prove_case_thms : bool -> string list -> (int * (string * DatatypeAux.dtyp list *
    1.10      (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
    1.11        string list -> thm list -> theory -> theory * string list * thm list list
    1.12 -  val prove_distinctness_thms : bool -> string list -> (int * (string * DatatypeAux.dtyp list *
    1.13 -    (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
    1.14 -      thm list list -> thm list list -> theory -> theory * thm list list
    1.15    val prove_split_thms : string list -> (int * (string * DatatypeAux.dtyp list *
    1.16      (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
    1.17        thm list list -> thm list list -> thm list -> thm list list -> theory ->
    1.18 @@ -97,10 +94,14 @@
    1.19  (*************************** primrec combinators ******************************)
    1.20  
    1.21  fun prove_primrec_thms flat_names new_type_names descr sorts
    1.22 -    (dt_info : datatype_info Symtab.table) constr_inject dist_rewrites induct thy =
    1.23 +    (dt_info : datatype_info Symtab.table) constr_inject dist_rewrites dist_ss induct thy =
    1.24    let
    1.25      val _ = message "Constructing primrec combinators ...";
    1.26  
    1.27 +    val fun_rel_comp_name = Sign.intern_const (sign_of Relation.thy) "fun_rel_comp";
    1.28 +    val [fun_rel_comp_def, o_def] =
    1.29 +      map (get_thm Relation.thy) ["fun_rel_comp_def", "o_def"];
    1.30 +
    1.31      val big_name = space_implode "_" new_type_names;
    1.32      val thy0 = add_path flat_names big_name thy;
    1.33  
    1.34 @@ -123,9 +124,14 @@
    1.35      val reccomb_fn_Ts = flat (map (fn (i, (_, _, constrs)) =>
    1.36        map (fn (_, cargs) =>
    1.37          let
    1.38 -          val recs = filter is_rec_type cargs;
    1.39 -          val argTs = (map (typ_of_dtyp descr' sorts) cargs) @
    1.40 -            (map (fn r => nth_elem (dest_DtRec r, rec_result_Ts)) recs)
    1.41 +          val Ts = map (typ_of_dtyp descr' sorts) cargs;
    1.42 +          val recs = filter (is_rec_type o fst) (cargs ~~ Ts);
    1.43 +
    1.44 +          fun mk_argT (DtRec k, _) = nth_elem (k, rec_result_Ts)
    1.45 +            | mk_argT (DtType ("fun", [_, DtRec k]), Type ("fun", [T, _])) =
    1.46 +               T --> nth_elem (k, rec_result_Ts);
    1.47 +
    1.48 +          val argTs = Ts @ map mk_argT recs
    1.49          in argTs ---> nth_elem (i, rec_result_Ts)
    1.50          end) constrs) descr');
    1.51  
    1.52 @@ -141,22 +147,27 @@
    1.53  
    1.54      fun make_rec_intr T set_name ((rec_intr_ts, l), (cname, cargs)) =
    1.55        let
    1.56 -        fun mk_prem (dt, (j, k, prems, t1s, t2s)) =
    1.57 -          let
    1.58 -            val T = typ_of_dtyp descr' sorts dt;
    1.59 -            val free1 = mk_Free "x" T j
    1.60 -          in (case dt of
    1.61 -             DtRec m =>
    1.62 +        fun mk_prem ((dt, U), (j, k, prems, t1s, t2s)) =
    1.63 +          let val free1 = mk_Free "x" U j
    1.64 +          in (case (dt, U) of
    1.65 +             (DtRec m, _) =>
    1.66                 let val free2 = mk_Free "y" (nth_elem (m, rec_result_Ts)) k
    1.67                 in (j + 1, k + 1, (HOLogic.mk_Trueprop (HOLogic.mk_mem
    1.68                   (HOLogic.mk_prod (free1, free2), nth_elem (m, rec_sets))))::prems,
    1.69                     free1::t1s, free2::t2s)
    1.70                 end
    1.71 +           | (DtType ("fun", [_, DtRec m]), U' as Type ("fun", [T', _])) =>
    1.72 +               let val free2 = mk_Free "y" (T' --> nth_elem (m, rec_result_Ts)) k
    1.73 +               in (j + 1, k + 1, (HOLogic.mk_Trueprop (HOLogic.mk_mem (free2,
    1.74 +                 Const (fun_rel_comp_name, [U', snd (strip_type (nth_elem (m, rec_set_Ts)))] --->
    1.75 +                   HOLogic.mk_setT (T' --> nth_elem (m, rec_result_Ts))) $
    1.76 +                     free1 $ nth_elem (m, rec_sets))))::prems, free1::t1s, free2::t2s)
    1.77 +               end
    1.78             | _ => (j + 1, k, prems, free1::t1s, t2s))
    1.79            end;
    1.80  
    1.81          val Ts = map (typ_of_dtyp descr' sorts) cargs;
    1.82 -        val (_, _, prems, t1s, t2s) = foldr mk_prem (cargs, (1, 1, [], [], []))
    1.83 +        val (_, _, prems, t1s, t2s) = foldr mk_prem (cargs ~~ Ts, (1, 1, [], [], []))
    1.84  
    1.85        in (rec_intr_ts @ [Logic.list_implies (prems, HOLogic.mk_Trueprop (HOLogic.mk_mem
    1.86          (HOLogic.mk_prod (list_comb (Const (cname, Ts ---> T), t1s),
    1.87 @@ -170,7 +181,7 @@
    1.88      val (thy1, {intrs = rec_intrs, elims = rec_elims, ...}) =
    1.89        setmp InductivePackage.quiet_mode (!quiet_mode)
    1.90          (InductivePackage.add_inductive_i false true big_rec_name' false false true
    1.91 -           rec_sets [] (map (fn x => (("", x), [])) rec_intr_ts) [] []) thy0;
    1.92 +           rec_sets [] (map (fn x => (("", x), [])) rec_intr_ts) [fun_rel_comp_mono] []) thy0;
    1.93  
    1.94      (* prove uniqueness and termination of primrec combinators *)
    1.95  
    1.96 @@ -181,9 +192,7 @@
    1.97          val distinct_tac = (etac Pair_inject 1) THEN
    1.98            (if i < length newTs then
    1.99               full_simp_tac (HOL_ss addsimps (nth_elem (i, dist_rewrites))) 1
   1.100 -           else full_simp_tac (HOL_ss addsimps
   1.101 -             ((#distinct (the (Symtab.lookup (dt_info, tname)))) @
   1.102 -               [Suc_Suc_eq, Suc_not_Zero, Zero_not_Suc])) 1);
   1.103 +           else full_simp_tac dist_ss 1);
   1.104  
   1.105          val inject = map (fn r => r RS iffD1)
   1.106            (if i < length newTs then nth_elem (i, constr_inject)
   1.107 @@ -194,6 +203,7 @@
   1.108              val k = length (filter is_rec_type cargs)
   1.109  
   1.110            in (EVERY [DETERM tac,
   1.111 +                REPEAT (dtac fun_rel_comp_unique 1),
   1.112                  REPEAT (etac ex1E 1), rtac ex1I 1,
   1.113                  DEPTH_SOLVE_1 (ares_tac [intr] 1),
   1.114                  REPEAT_DETERM_N k (etac thin 1),
   1.115 @@ -252,10 +262,9 @@
   1.116          (Sign.base_name name, reccomb_fn_Ts @ [T] ---> T', NoSyn))
   1.117            (reccomb_names ~~ recTs ~~ rec_result_Ts)) |>
   1.118        Theory.add_defs_i (map (fn ((((name, comb), set), T), T') =>
   1.119 -        ((Sign.base_name name) ^ "_def", Logic.mk_equals
   1.120 -          (comb $ Free ("x", T),
   1.121 +        ((Sign.base_name name) ^ "_def", Logic.mk_equals (comb, absfree ("x", T,
   1.122             Const ("Eps", (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
   1.123 -             HOLogic.mk_mem (HOLogic.mk_prod (Free ("x", T), Free ("y", T')), set)))))
   1.124 +             HOLogic.mk_mem (HOLogic.mk_prod (Free ("x", T), Free ("y", T')), set))))))
   1.125                 (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts)) |>
   1.126        parent_path flat_names;
   1.127  
   1.128 @@ -270,7 +279,8 @@
   1.129          [rtac select1_equality 1,
   1.130           resolve_tac rec_unique_thms 1,
   1.131           resolve_tac rec_intrs 1,
   1.132 -         REPEAT (resolve_tac rec_total_thms 1)]))
   1.133 +         rewrite_goals_tac [o_def, fun_rel_comp_def],
   1.134 +         REPEAT ((rtac CollectI 1 THEN rtac allI 1) ORELSE resolve_tac rec_total_thms 1)]))
   1.135             (DatatypeProp.make_primrecs new_type_names descr sorts thy2)
   1.136  
   1.137    in
   1.138 @@ -294,10 +304,13 @@
   1.139      val newTs = take (length (hd descr), recTs);
   1.140      val T' = TFree (variant used "'t", HOLogic.termS);
   1.141  
   1.142 +    fun mk_dummyT (DtRec _) = T'
   1.143 +      | mk_dummyT (DtType ("fun", [T, _])) = typ_of_dtyp descr' sorts T --> T'
   1.144 +
   1.145      val case_dummy_fns = map (fn (_, (_, _, constrs)) => map (fn (_, cargs) =>
   1.146        let
   1.147          val Ts = map (typ_of_dtyp descr' sorts) cargs;
   1.148 -        val Ts' = replicate (length (filter is_rec_type cargs)) T'
   1.149 +        val Ts' = map mk_dummyT (filter is_rec_type cargs)
   1.150        in Const ("arbitrary", Ts @ Ts' ---> T')
   1.151        end) constrs) descr';
   1.152  
   1.153 @@ -312,7 +325,7 @@
   1.154            val (fns1, fns2) = ListPair.unzip (map (fn ((_, cargs), j) =>
   1.155              let
   1.156                val Ts = map (typ_of_dtyp descr' sorts) cargs;
   1.157 -              val Ts' = Ts @ (replicate (length (filter is_rec_type cargs)) T');
   1.158 +              val Ts' = Ts @ map mk_dummyT (filter is_rec_type cargs);
   1.159                val frees' = map (uncurry (mk_Free "x")) (Ts' ~~ (1 upto length Ts'));
   1.160                val frees = take (length cargs, frees');
   1.161                val free = mk_Free "f" (Ts ---> T') j
   1.162 @@ -350,80 +363,6 @@
   1.163      (store_thmss "cases" new_type_names case_thms thy3, case_names, case_thms)
   1.164    end;
   1.165  
   1.166 -(************************ distinctness of constructors ************************)
   1.167 -
   1.168 -fun prove_distinctness_thms flat_names new_type_names descr sorts dist_rewrites case_thms thy =
   1.169 -  let
   1.170 -    val thy1 = add_path flat_names (space_implode "_" new_type_names) thy;
   1.171 -
   1.172 -    val descr' = flat descr;
   1.173 -    val recTs = get_rec_types descr' sorts;
   1.174 -    val newTs = take (length (hd descr), recTs);
   1.175 -
   1.176 -    (*--------------------------------------------------------------------*)
   1.177 -    (* define t_ord - functions for proving distinctness of constructors: *)
   1.178 -    (*  t_ord C_i ... = i                                                 *)
   1.179 -    (*--------------------------------------------------------------------*)
   1.180 -
   1.181 -    fun define_ord ((thy, ord_defs), (((_, (_, _, constrs)), T), tname)) =
   1.182 -      if length constrs < DatatypeProp.dtK then (thy, ord_defs)
   1.183 -      else
   1.184 -        let
   1.185 -          val Tss = map ((map (typ_of_dtyp descr' sorts)) o snd) constrs;
   1.186 -          val ts = map HOLogic.mk_nat (0 upto length constrs - 1);
   1.187 -          val mk_abs = foldr (fn (T, t') => Abs ("x", T, t'));
   1.188 -          val fs = map mk_abs (Tss ~~ ts);
   1.189 -          val fTs = map (fn Ts => Ts ---> HOLogic.natT) Tss;
   1.190 -          val ord_name = Sign.full_name (Theory.sign_of thy) (tname ^ "_ord");
   1.191 -          val case_name = Sign.intern_const (Theory.sign_of thy) (tname ^ "_case");
   1.192 -          val ordT = T --> HOLogic.natT;
   1.193 -          val caseT = fTs ---> ordT;
   1.194 -          val defpair = (tname ^ "_ord_def", Logic.mk_equals
   1.195 -            (Const (ord_name, ordT), list_comb (Const (case_name, caseT), fs)));
   1.196 -          val thy' = thy |>
   1.197 -            Theory.add_consts_i [(tname ^ "_ord", ordT, NoSyn)] |>
   1.198 -            Theory.add_defs_i [defpair];
   1.199 -          val def = get_def thy' (tname ^ "_ord")
   1.200 -
   1.201 -        in (thy', ord_defs @ [def]) end;
   1.202 -
   1.203 -    val (thy2, ord_defs) =
   1.204 -      foldl define_ord ((thy1, []), (hd descr) ~~ newTs ~~ new_type_names);
   1.205 -
   1.206 -    (**** number of constructors < dtK ****)
   1.207 -
   1.208 -    fun prove_distinct_thms _ [] = []
   1.209 -      | prove_distinct_thms dist_rewrites' (t::_::ts) =
   1.210 -          let
   1.211 -            val dist_thm = prove_goalw_cterm [] (cterm_of (Theory.sign_of thy2) t) (fn _ =>
   1.212 -              [simp_tac (HOL_ss addsimps dist_rewrites') 1])
   1.213 -          in dist_thm::(standard (dist_thm RS not_sym))::
   1.214 -            (prove_distinct_thms dist_rewrites' ts)
   1.215 -          end;
   1.216 -
   1.217 -    val distinct_thms = map (fn ((((_, (_, _, constrs)), ts),
   1.218 -      dist_rewrites'), case_thms) =>
   1.219 -        if length constrs < DatatypeProp.dtK then
   1.220 -          prove_distinct_thms dist_rewrites' ts
   1.221 -        else 
   1.222 -          let
   1.223 -            val t::ts' = rev ts;
   1.224 -            val (_ $ (_ $ (_ $ (f $ _) $ _))) = hd (Logic.strip_imp_prems t);
   1.225 -            val cert = cterm_of (Theory.sign_of thy2);
   1.226 -            val distinct_lemma' = cterm_instantiate
   1.227 -              [(cert distinct_f, cert f)] distinct_lemma;
   1.228 -            val rewrites = ord_defs @ (map mk_meta_eq case_thms)
   1.229 -          in
   1.230 -            (map (fn t => prove_goalw_cterm rewrites (cert t)
   1.231 -              (fn _ => [rtac refl 1])) (rev ts')) @ [standard distinct_lemma']
   1.232 -          end) ((hd descr) ~~ (DatatypeProp.make_distincts new_type_names
   1.233 -            descr sorts thy2) ~~ dist_rewrites ~~ case_thms)
   1.234 -
   1.235 -  in
   1.236 -    (thy2 |> parent_path flat_names |>
   1.237 -             store_thmss "distinct" new_type_names distinct_thms,
   1.238 -     distinct_thms)
   1.239 -  end;
   1.240  
   1.241  (******************************* case splitting *******************************)
   1.242  
   1.243 @@ -465,6 +404,11 @@
   1.244  (******************************* size functions *******************************)
   1.245  
   1.246  fun prove_size_thms flat_names new_type_names descr sorts reccomb_names primrec_thms thy =
   1.247 +  if exists (fn (_, (_, _, constrs)) => exists (fn (_, cargs) => exists
   1.248 +    (fn (DtType ("fun", [_, DtRec _])) => true | _ => false) cargs) constrs) (flat descr)
   1.249 +  then
   1.250 +    (thy, [])
   1.251 +  else
   1.252    let
   1.253      val _ = message "Proving equations for size function ...";
   1.254  
   1.255 @@ -475,7 +419,7 @@
   1.256      val recTs = get_rec_types descr' sorts;
   1.257  
   1.258      val big_size_name = space_implode "_" new_type_names ^ "_size";
   1.259 -    val size_name = Sign.intern_const (Theory.sign_of (the (get_thy "Arith" thy1))) "size";
   1.260 +    val size_name = Sign.intern_const (Theory.sign_of (theory "Arith")) "size";
   1.261      val size_names = replicate (length (hd descr)) size_name @
   1.262        map (Sign.full_name (Theory.sign_of thy1))
   1.263          (if length (flat (tl descr)) = 1 then [big_size_name] else
     2.1 --- a/src/HOL/Tools/datatype_aux.ML	Fri Jul 16 12:09:48 1999 +0200
     2.2 +++ b/src/HOL/Tools/datatype_aux.ML	Fri Jul 16 12:14:04 1999 +0200
     2.3 @@ -13,8 +13,6 @@
     2.4    
     2.5    val foldl1 : ('a * 'a -> 'a) -> 'a list -> 'a
     2.6  
     2.7 -  val get_thy : string -> theory -> theory option
     2.8 -
     2.9    val add_path : bool -> string -> theory -> theory
    2.10    val parent_path : bool -> theory -> theory
    2.11  
    2.12 @@ -28,6 +26,10 @@
    2.13    val indtac : thm -> int -> tactic
    2.14    val exh_tac : (string -> thm) -> int -> tactic
    2.15  
    2.16 +  datatype simproc_dist = QuickAndDirty
    2.17 +                        | FewConstrs of thm list
    2.18 +                        | ManyConstrs of thm * simpset;
    2.19 +
    2.20    datatype dtyp =
    2.21        DtTFree of string
    2.22      | DtType of string * (dtyp list)
    2.23 @@ -35,6 +37,7 @@
    2.24  
    2.25    type datatype_info
    2.26  
    2.27 +  exception Datatype
    2.28    val dtyp_of_typ : (string * string list) list -> typ -> dtyp
    2.29    val mk_Free : string -> typ -> int -> term
    2.30    val is_rec_type : dtyp -> bool
    2.31 @@ -46,14 +49,16 @@
    2.32    val dest_conj : term -> term list
    2.33    val get_nonrec_types : (int * (string * dtyp list *
    2.34      (string * dtyp list) list)) list -> (string * sort) list -> typ list
    2.35 +  val get_branching_types : (int * (string * dtyp list *
    2.36 +    (string * dtyp list) list)) list -> (string * sort) list -> typ list
    2.37    val get_rec_types : (int * (string * dtyp list *
    2.38      (string * dtyp list) list)) list -> (string * sort) list -> typ list
    2.39    val check_nonempty : (int * (string * dtyp list *
    2.40      (string * dtyp list) list)) list list -> unit
    2.41    val unfold_datatypes : 
    2.42 -    datatype_info Symtab.table ->
    2.43 -      (int * (string * dtyp list *
    2.44 -        (string * dtyp list) list)) list -> int ->
    2.45 +    Sign.sg -> (int * (string * dtyp list * (string * dtyp list) list)) list ->
    2.46 +      (string * sort) list -> datatype_info Symtab.table ->
    2.47 +        (int * (string * dtyp list * (string * dtyp list) list)) list -> int ->
    2.48            (int * (string * dtyp list *
    2.49              (string * dtyp list) list)) list list * int
    2.50  end;
    2.51 @@ -67,9 +72,6 @@
    2.52  (* FIXME: move to library ? *)
    2.53  fun foldl1 f (x::xs) = foldl f (x, xs);
    2.54  
    2.55 -fun get_thy name thy = find_first
    2.56 -  (equal name o Sign.name_of o Theory.sign_of) (Theory.ancestors_of thy);
    2.57 -
    2.58  fun add_path flat_names s = if flat_names then I else Theory.add_path s;
    2.59  fun parent_path flat_names = if flat_names then I else Theory.parent_path;
    2.60  
    2.61 @@ -92,7 +94,7 @@
    2.62  (* split theorem thm_1 & ... & thm_n into n theorems *)
    2.63  
    2.64  fun split_conj_thm th =
    2.65 -  ((th RS conjunct1)::(split_conj_thm (th RS conjunct2))) handle _ => [th];
    2.66 +  ((th RS conjunct1)::(split_conj_thm (th RS conjunct2))) handle THM _ => [th];
    2.67  
    2.68  val mk_conj = foldr1 (HOLogic.mk_binop "op &");
    2.69  val mk_disj = foldr1 (HOLogic.mk_binop "op |");
    2.70 @@ -138,6 +140,12 @@
    2.71    in compose_tac (false, exhaustion', nprems_of exhaustion) i state
    2.72    end;
    2.73  
    2.74 +(* handling of distinctness theorems *)
    2.75 +
    2.76 +datatype simproc_dist = QuickAndDirty
    2.77 +                      | FewConstrs of thm list
    2.78 +                      | ManyConstrs of thm * simpset;
    2.79 +
    2.80  (********************** Internal description of datatypes *********************)
    2.81  
    2.82  datatype dtyp =
    2.83 @@ -157,7 +165,7 @@
    2.84     case_rewrites : thm list,
    2.85     induction : thm,
    2.86     exhaustion : thm,
    2.87 -   distinct : thm list,
    2.88 +   distinct : simproc_dist,
    2.89     inject : thm list,
    2.90     nchotomy : thm,
    2.91     case_cong : thm};
    2.92 @@ -172,8 +180,13 @@
    2.93        DtType (name, map (subst_DtTFree i substs) ts)
    2.94    | subst_DtTFree i _ (DtRec j) = DtRec (i + j);
    2.95  
    2.96 -fun dest_DtTFree (DtTFree a) = a;
    2.97 -fun dest_DtRec (DtRec i) = i;
    2.98 +exception Datatype;
    2.99 +
   2.100 +fun dest_DtTFree (DtTFree a) = a
   2.101 +  | dest_DtTFree _ = raise Datatype;
   2.102 +
   2.103 +fun dest_DtRec (DtRec i) = i
   2.104 +  | dest_DtRec _ = raise Datatype;
   2.105  
   2.106  fun is_rec_type (DtType (_, dts)) = exists is_rec_type dts
   2.107    | is_rec_type (DtRec _) = true
   2.108 @@ -201,6 +214,7 @@
   2.109  
   2.110  fun get_nonrec_types descr sorts =
   2.111    let fun add (Ts, T as DtTFree _) = T ins Ts
   2.112 +        | add (Ts, T as DtType ("fun", [_, DtRec _])) = Ts
   2.113          | add (Ts, T as DtType _) = T ins Ts
   2.114          | add (Ts, _) = Ts
   2.115    in map (typ_of_dtyp descr sorts) (foldl (fn (Ts, (_, (_, _, constrs))) =>
   2.116 @@ -213,6 +227,16 @@
   2.117  fun get_rec_types descr sorts = map (fn (_ , (s, ds, _)) =>
   2.118    Type (s, map (typ_of_dtyp descr sorts) ds)) descr;
   2.119  
   2.120 +(* get all branching types *)
   2.121 +
   2.122 +fun get_branching_types descr sorts = 
   2.123 +  let fun add (Ts, DtType ("fun", [T, DtRec _])) = T ins Ts
   2.124 +        | add (Ts, _) = Ts
   2.125 +  in map (typ_of_dtyp descr sorts) (foldl (fn (Ts, (_, (_, _, constrs))) =>
   2.126 +    foldl (fn (Ts', (_, cargs)) =>
   2.127 +      foldl add (Ts', cargs)) (Ts, constrs)) ([], descr))
   2.128 +  end;
   2.129 +
   2.130  (* nonemptiness check for datatypes *)
   2.131  
   2.132  fun check_nonempty descr =
   2.133 @@ -223,6 +247,7 @@
   2.134          val (_, _, constrs) = the (assoc (descr', i));
   2.135          fun arg_nonempty (DtRec i) = if i mem is then false
   2.136                else is_nonempty_dt (i::is) i
   2.137 +          | arg_nonempty (DtType ("fun", [_, T])) = arg_nonempty T
   2.138            | arg_nonempty _ = true;
   2.139        in exists ((forall arg_nonempty) o snd) constrs
   2.140        end
   2.141 @@ -234,16 +259,19 @@
   2.142  (* all types of the form DtType (dt_name, [..., DtRec _, ...]) *)
   2.143  (* need to be unfolded                                         *)
   2.144  
   2.145 -fun unfold_datatypes (dt_info : datatype_info Symtab.table) descr i =
   2.146 +fun unfold_datatypes sign orig_descr sorts (dt_info : datatype_info Symtab.table) descr i =
   2.147    let
   2.148 -    fun get_dt_descr i tname dts =
   2.149 +    fun typ_error T msg = error ("Non-admissible type expression\n" ^
   2.150 +      Sign.string_of_typ sign (typ_of_dtyp (orig_descr @ descr) sorts T) ^ "\n" ^ msg);
   2.151 +
   2.152 +    fun get_dt_descr T i tname dts =
   2.153        (case Symtab.lookup (dt_info, tname) of
   2.154 -         None => error (tname ^ " is not a datatype - can't use it in\
   2.155 -           \ indirect recursion")
   2.156 +         None => typ_error T (tname ^ " is not a datatype - can't use it in\
   2.157 +           \ nested recursion")
   2.158         | (Some {index, descr, ...}) =>
   2.159             let val (_, vars, _) = the (assoc (descr, index));
   2.160 -               val subst = ((map dest_DtTFree vars) ~~ dts) handle _ =>
   2.161 -                 error ("Type constructor " ^ tname ^ " used with wrong\
   2.162 +               val subst = ((map dest_DtTFree vars) ~~ dts) handle LIST _ =>
   2.163 +                 typ_error T ("Type constructor " ^ tname ^ " used with wrong\
   2.164                    \ number of arguments")
   2.165             in (i + index, map (fn (j, (tn, args, cs)) => (i + j,
   2.166               (tn, map (subst_DtTFree i subst) args,
   2.167 @@ -254,9 +282,18 @@
   2.168  
   2.169      fun unfold_arg ((i, Ts, descrs), T as (DtType (tname, dts))) =
   2.170            if is_rec_type T then
   2.171 -            let val (index, descr) = get_dt_descr i tname dts;
   2.172 -                val (descr', i') = unfold_datatypes dt_info descr (i + length descr)
   2.173 -            in (i', Ts @ [DtRec index], descrs @ descr') end
   2.174 +            if tname = "fun" then
   2.175 +              if is_rec_type (hd dts) then
   2.176 +                typ_error T "Non-strictly positive recursive occurrence of type"
   2.177 +              else
   2.178 +                (case hd (tl dts) of
   2.179 +                   DtType ("fun", _) => typ_error T "Curried function types not allowed"
   2.180 +                 | T' => let val (i', [T''], descrs') = unfold_arg ((i, [], descrs), T')
   2.181 +                         in (i', Ts @ [DtType (tname, [hd dts, T''])], descrs') end)
   2.182 +            else
   2.183 +              let val (index, descr) = get_dt_descr T i tname dts;
   2.184 +                  val (descr', i') = unfold_datatypes sign orig_descr sorts dt_info descr (i + length descr)
   2.185 +              in (i', Ts @ [DtRec index], descrs @ descr') end
   2.186            else (i, Ts @ [T], descrs)
   2.187        | unfold_arg ((i, Ts, descrs), T) = (i, Ts @ [T], descrs);
   2.188  
     3.1 --- a/src/HOL/Tools/datatype_package.ML	Fri Jul 16 12:09:48 1999 +0200
     3.2 +++ b/src/HOL/Tools/datatype_package.ML	Fri Jul 16 12:14:04 1999 +0200
     3.3 @@ -11,6 +11,7 @@
     3.4    val mutual_induct_tac : string list -> int -> tactic
     3.5    val induct_tac : string -> int -> tactic
     3.6    val exhaust_tac : string -> int -> tactic
     3.7 +  val distinct_simproc : simproc
     3.8  end;
     3.9  
    3.10  signature DATATYPE_PACKAGE =
    3.11 @@ -63,9 +64,12 @@
    3.12         simps : thm list}
    3.13    val get_datatypes : theory -> DatatypeAux.datatype_info Symtab.table
    3.14    val print_datatypes : theory -> unit
    3.15 -  val datatype_info_sg : Sign.sg -> string -> DatatypeAux.datatype_info
    3.16 -  val datatype_info : theory -> string -> DatatypeAux.datatype_info
    3.17 +  val datatype_info_sg : Sign.sg -> string -> DatatypeAux.datatype_info option
    3.18 +  val datatype_info : theory -> string -> DatatypeAux.datatype_info option
    3.19 +  val datatype_info_sg_err : Sign.sg -> string -> DatatypeAux.datatype_info
    3.20 +  val datatype_info_err : theory -> string -> DatatypeAux.datatype_info
    3.21    val constrs_of : theory -> string -> term list option
    3.22 +  val constrs_of_sg : Sign.sg -> string -> term list option
    3.23    val case_const_of : theory -> string -> term option
    3.24    val setup: (theory -> theory) list
    3.25  end;
    3.26 @@ -104,28 +108,31 @@
    3.27  
    3.28  (** theory information about datatypes **)
    3.29  
    3.30 -fun datatype_info_sg sg name =
    3.31 -  (case Symtab.lookup (get_datatypes_sg sg, name) of
    3.32 -    Some info => info
    3.33 -  | None => error ("Unknown datatype " ^ quote name));
    3.34 +fun datatype_info_sg sg name = Symtab.lookup (get_datatypes_sg sg, name);
    3.35 +
    3.36 +fun datatype_info_sg_err sg name = (case datatype_info_sg sg name of
    3.37 +      Some info => info
    3.38 +    | None => error ("Unknown datatype " ^ quote name));
    3.39  
    3.40  val datatype_info = datatype_info_sg o Theory.sign_of;
    3.41  
    3.42 -fun constrs_of thy tname =
    3.43 -  let
    3.44 -    val {index, descr, ...} = datatype_info thy tname;
    3.45 -    val (_, _, constrs) = the (assoc (descr, index))
    3.46 -  in
    3.47 -    Some (map (fn (cname, _) =>
    3.48 -      Const (cname, the (Sign.const_type (Theory.sign_of thy) cname))) constrs)
    3.49 -  end handle _ => None;
    3.50 +fun datatype_info_err thy name = (case datatype_info thy name of
    3.51 +      Some info => info
    3.52 +    | None => error ("Unknown datatype " ^ quote name));
    3.53  
    3.54 -fun case_const_of thy tname =
    3.55 -  let
    3.56 -    val {case_name, ...} = datatype_info thy tname;
    3.57 -  in
    3.58 -    Some (Const (case_name, the (Sign.const_type (Theory.sign_of thy) case_name)))
    3.59 -  end handle _ => None;
    3.60 +fun constrs_of_sg sg tname = (case datatype_info_sg sg tname of
    3.61 +   Some {index, descr, ...} =>
    3.62 +     let val (_, _, constrs) = the (assoc (descr, index))
    3.63 +     in Some (map (fn (cname, _) => Const (cname, the (Sign.const_type sg cname))) constrs)
    3.64 +     end
    3.65 + | _ => None);
    3.66 +
    3.67 +val constrs_of = constrs_of_sg o Theory.sign_of;
    3.68 +
    3.69 +fun case_const_of thy tname = (case datatype_info thy tname of
    3.70 +   Some {case_name, ...} => Some (Const (case_name, the (Sign.const_type
    3.71 +     (Theory.sign_of thy) case_name)))
    3.72 + | _ => None);
    3.73  
    3.74  fun find_tname var Bi =
    3.75    let val frees = map dest_Free (term_frees Bi)
    3.76 @@ -168,7 +175,7 @@
    3.77      val (_, _, Bi, _) = dest_state (state, i);
    3.78      val {sign, ...} = rep_thm state;
    3.79      val tn = find_tname (hd vars) Bi;
    3.80 -    val {induction, ...} = datatype_info_sg sign tn;
    3.81 +    val {induction, ...} = datatype_info_sg_err sign tn;
    3.82      val ind_vnames = map (fn (_ $ Var (ixn, _)) =>
    3.83        implode (tl (explode (Syntax.string_of_vname ixn))))
    3.84          (dest_conj (HOLogic.dest_Trueprop (concl_of induction)));
    3.85 @@ -186,7 +193,7 @@
    3.86    let
    3.87      val {sign, ...} = rep_thm state;
    3.88      val tn = infer_tname state sign i aterm;
    3.89 -    val {exhaustion, ...} = datatype_info_sg sign tn;
    3.90 +    val {exhaustion, ...} = datatype_info_sg_err sign tn;
    3.91      val _ $ Var (ixn, _) $ _ = HOLogic.dest_Trueprop
    3.92        (hd (Logic.strip_assums_hyp (hd (prems_of exhaustion))));
    3.93      val exh_vname = implode (tl (explode (Syntax.string_of_vname ixn)))
    3.94 @@ -195,6 +202,61 @@
    3.95    end;
    3.96  
    3.97  
    3.98 +(**** simplification procedure for showing distinctness of constructors ****)
    3.99 +
   3.100 +(* oracle *)
   3.101 +
   3.102 +val distinctN = "constr_distinct";
   3.103 +
   3.104 +exception ConstrDistinct of term;
   3.105 +
   3.106 +
   3.107 +fun distinct_proc sg _ (t as Const ("op =", _) $ t1 $ t2) =
   3.108 +  (case (pairself strip_comb (t1, t2)) of
   3.109 +     ((Const (cname1, _), xs), (Const (cname2, _), ys)) =>
   3.110 +         (case (fastype_of t1, fastype_of t2) of
   3.111 +            (Type (tname1, _), Type (tname2, _)) =>
   3.112 +                if tname1 = tname2 andalso not (cname1 = cname2) then
   3.113 +                   (case (constrs_of_sg sg tname1) of
   3.114 +                      Some constrs => let val cnames = map (fst o dest_Const) constrs
   3.115 +                        in if cname1 mem cnames andalso cname2 mem cnames then
   3.116 +                             let val eq_t = Logic.mk_equals (t, Const ("False", HOLogic.boolT));
   3.117 +                                 val eq_ct = cterm_of sg eq_t;
   3.118 +                                 val Datatype_thy = theory "Datatype";
   3.119 +                                 val [In0_inject, In1_inject, In0_not_In1, In1_not_In0] =
   3.120 +                                   map (get_thm Datatype_thy)
   3.121 +                                     ["In0_inject", "In1_inject", "In0_not_In1", "In1_not_In0"]
   3.122 +                             in (case (#distinct (datatype_info_sg_err sg tname1)) of
   3.123 +                                 QuickAndDirty => Some (Thm.invoke_oracle
   3.124 +                                   Datatype_thy distinctN (sg, ConstrDistinct eq_t))
   3.125 +                               | FewConstrs thms => Some (prove_goalw_cterm [] eq_ct (K
   3.126 +                                   [rtac eq_reflection 1, rtac iffI 1, rtac notE 1,
   3.127 +                                    atac 2, resolve_tac thms 1, etac FalseE 1]))
   3.128 +                               | ManyConstrs (thm, ss) => Some (prove_goalw_cterm [] eq_ct (K
   3.129 +                                   [rtac eq_reflection 1, rtac iffI 1, dtac thm 1,
   3.130 +                                    full_simp_tac ss 1,
   3.131 +                                    REPEAT (dresolve_tac [In0_inject, In1_inject] 1),
   3.132 +                                    eresolve_tac [In0_not_In1 RS notE, In1_not_In0 RS notE] 1,
   3.133 +                                    etac FalseE 1])))
   3.134 +                             end
   3.135 +                           else None
   3.136 +                        end
   3.137 +                    | None => None)
   3.138 +                else None
   3.139 +          | _ => None)
   3.140 +   | _ => None)
   3.141 +  | distinct_proc sg _ _ = None;
   3.142 +
   3.143 +val distinct_pats = [Thm.read_cterm (Theory.sign_of HOL.thy) ("s = t", HOLogic.termTVar)];
   3.144 +val distinct_simproc = mk_simproc "distinct_simproc" distinct_pats distinct_proc;
   3.145 +
   3.146 +val dist_ss = HOL_ss addsimprocs [distinct_simproc];
   3.147 +
   3.148 +val simproc_setup =
   3.149 +  [Theory.add_oracle (distinctN, fn (_, ConstrDistinct t) => t),
   3.150 +   fn thy => (simpset_ref_of thy := simpset_of thy addsimprocs [distinct_simproc]; thy)];
   3.151 +
   3.152 +
   3.153  (* prepare types *)
   3.154  
   3.155  fun read_typ sign ((Ts, sorts), str) =
   3.156 @@ -240,7 +302,7 @@
   3.157  
   3.158  fun clasimp addDistinct ([], _) = clasimp
   3.159    | clasimp addDistinct (thms::thmss, (_, (_, _, constrs))::descr) =
   3.160 -      if length constrs < DatatypeProp.dtK then
   3.161 +      if length constrs < !DatatypeProp.dtK then
   3.162          clasimp addIffs thms addDistinct (thmss, descr)
   3.163        else
   3.164          clasimp addsimps2 thms addDistinct (thmss, descr);
   3.165 @@ -275,6 +337,9 @@
   3.166      val used = foldr add_typ_tfree_names (recTs, []);
   3.167      val newTs = take (length (hd descr), recTs);
   3.168  
   3.169 +    val no_size = exists (fn (_, (_, _, constrs)) => exists (fn (_, cargs) => exists
   3.170 +      (fn (DtType ("fun", [_, DtRec _])) => true | _ => false) cargs) constrs) descr';
   3.171 +
   3.172      (**** declare new types and constants ****)
   3.173  
   3.174      val tyvars = map (fn (_, (_, Ts, _)) => map dest_DtTFree Ts) (hd descr);
   3.175 @@ -290,9 +355,14 @@
   3.176      val reccomb_fn_Ts = flat (map (fn (i, (_, _, constrs)) =>
   3.177        map (fn (_, cargs) =>
   3.178          let
   3.179 -          val recs = filter is_rec_type cargs;
   3.180 -          val argTs = (map (typ_of_dtyp descr' sorts) cargs) @
   3.181 -            (map (fn r => nth_elem (dest_DtRec r, rec_result_Ts)) recs)
   3.182 +          val Ts = map (typ_of_dtyp descr' sorts) cargs;
   3.183 +          val recs = filter (is_rec_type o fst) (cargs ~~ Ts);
   3.184 +
   3.185 +          fun mk_argT (DtRec k, _) = nth_elem (k, rec_result_Ts)
   3.186 +            | mk_argT (DtType ("fun", [_, DtRec k]), Type ("fun", [T, _])) =
   3.187 +               T --> nth_elem (k, rec_result_Ts);
   3.188 +
   3.189 +          val argTs = Ts @ map mk_argT recs
   3.190          in argTs ---> nth_elem (i, rec_result_Ts)
   3.191          end) constrs) descr');
   3.192  
   3.193 @@ -341,19 +411,11 @@
   3.194  
   3.195      val thy2 = thy2' |>
   3.196  
   3.197 -      (** t_ord functions **)
   3.198 -
   3.199 -      Theory.add_consts_i
   3.200 -        (foldr (fn ((((_, (_, _, constrs)), tname), T), decls) =>
   3.201 -          if length constrs < DatatypeProp.dtK then decls
   3.202 -          else (tname ^ "_ord", T --> HOLogic.natT, NoSyn)::decls)
   3.203 -            ((hd descr) ~~ new_type_names ~~ newTs, [])) |>
   3.204 -
   3.205        (** size functions **)
   3.206  
   3.207 -      Theory.add_consts_i (map (fn (s, T) =>
   3.208 +      (if no_size then I else Theory.add_consts_i (map (fn (s, T) =>
   3.209          (Sign.base_name s, T --> HOLogic.natT, NoSyn))
   3.210 -          (size_names ~~ drop (length (hd descr), recTs))) |>
   3.211 +          (size_names ~~ drop (length (hd descr), recTs)))) |>
   3.212  
   3.213        (** constructors **)
   3.214  
   3.215 @@ -370,19 +432,19 @@
   3.216      (**** introduction of axioms ****)
   3.217  
   3.218      val rec_axs = DatatypeProp.make_primrecs new_type_names descr sorts thy2;
   3.219 -    val size_axs = DatatypeProp.make_size new_type_names descr sorts thy2;
   3.220 +    val size_axs = if no_size then [] else DatatypeProp.make_size new_type_names descr sorts thy2;
   3.221  
   3.222      val (thy3, inject) = thy2 |>
   3.223        Theory.add_path (space_implode "_" new_type_names) |>
   3.224        PureThy.add_axioms_i [(("induct", DatatypeProp.make_ind descr sorts), [])] |>
   3.225        PureThy.add_axiomss_i [(("recs", rec_axs), [])] |>
   3.226 -      PureThy.add_axiomss_i [(("size", size_axs), [])] |>
   3.227 +      (if no_size then I else PureThy.add_axiomss_i [(("size", size_axs), [])]) |>
   3.228        Theory.parent_path |>
   3.229        add_and_get_axiomss "inject" new_type_names
   3.230          (DatatypeProp.make_injs descr sorts);
   3.231      val induct = get_axiom thy3 "induct";
   3.232      val rec_thms = get_thms thy3 "recs";
   3.233 -    val size_thms = get_thms thy3 "size";
   3.234 +    val size_thms = if no_size then [] else get_thms thy3 "size";
   3.235      val (thy4, distinct) = add_and_get_axiomss "distinct" new_type_names
   3.236        (DatatypeProp.make_distincts new_type_names descr sorts thy3) thy3;
   3.237      val (thy5, exhaustion) = add_and_get_axioms "exhaust" new_type_names
   3.238 @@ -401,7 +463,8 @@
   3.239      
   3.240      val dt_infos = map (make_dt_info descr' induct reccomb_names' rec_thms)
   3.241        ((0 upto length (hd descr) - 1) ~~ (hd descr) ~~ case_names' ~~ case_thms ~~
   3.242 -        exhaustion ~~ distinct ~~ inject ~~ nchotomys ~~ case_congs);
   3.243 +        exhaustion ~~ replicate (length (hd descr)) QuickAndDirty ~~ inject ~~
   3.244 +          nchotomys ~~ case_congs);
   3.245  
   3.246      val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms;
   3.247  
   3.248 @@ -413,7 +476,7 @@
   3.249  
   3.250      val _ = store_clasimp thy11 ((claset_of thy11, simpset_of thy11)
   3.251        addsimps2 flat case_thms addsimps2 size_thms addsimps2 rec_thms
   3.252 -      addIffs flat inject addDistinct (distinct, hd descr));
   3.253 +      addIffs flat (inject @ distinct));
   3.254  
   3.255    in
   3.256      (thy11,
   3.257 @@ -435,18 +498,16 @@
   3.258    let
   3.259      val _ = message ("Proofs for datatype(s) " ^ commas_quote new_type_names);
   3.260  
   3.261 -    val (thy2, inject, dist_rewrites, induct) = thy |>
   3.262 +    val (thy2, inject, distinct, dist_rewrites, simproc_dists, induct) = thy |>
   3.263        DatatypeRepProofs.representation_proofs flat_names dt_info new_type_names descr sorts
   3.264          types_syntax constr_syntax;
   3.265  
   3.266      val (thy3, casedist_thms) =
   3.267        DatatypeAbsProofs.prove_casedist_thms new_type_names descr sorts induct thy2;
   3.268      val (thy4, reccomb_names, rec_thms) = DatatypeAbsProofs.prove_primrec_thms
   3.269 -      flat_names new_type_names descr sorts dt_info inject dist_rewrites induct thy3;
   3.270 -    val (thy5, case_names, case_thms) = DatatypeAbsProofs.prove_case_thms
   3.271 +      flat_names new_type_names descr sorts dt_info inject dist_rewrites dist_ss induct thy3;
   3.272 +    val (thy6, case_names, case_thms) = DatatypeAbsProofs.prove_case_thms
   3.273        flat_names new_type_names descr sorts reccomb_names rec_thms thy4;
   3.274 -    val (thy6, distinct) = DatatypeAbsProofs.prove_distinctness_thms
   3.275 -      flat_names new_type_names descr sorts dist_rewrites case_thms thy5;
   3.276      val (thy7, split_thms) = DatatypeAbsProofs.prove_split_thms new_type_names
   3.277        descr sorts inject dist_rewrites casedist_thms case_thms thy6;
   3.278      val (thy8, nchotomys) = DatatypeAbsProofs.prove_nchotomys new_type_names
   3.279 @@ -458,7 +519,7 @@
   3.280  
   3.281      val dt_infos = map (make_dt_info (flat descr) induct reccomb_names rec_thms)
   3.282        ((0 upto length (hd descr) - 1) ~~ (hd descr) ~~ case_names ~~ case_thms ~~
   3.283 -        casedist_thms ~~ distinct ~~ inject ~~ nchotomys ~~ case_congs);
   3.284 +        casedist_thms ~~ simproc_dists ~~ inject ~~ nchotomys ~~ case_congs);
   3.285  
   3.286      val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms;
   3.287  
   3.288 @@ -470,7 +531,7 @@
   3.289  
   3.290      val _ = store_clasimp thy11 ((claset_of thy11, simpset_of thy11)
   3.291        addsimps2 flat case_thms addsimps2 size_thms addsimps2 rec_thms
   3.292 -      addIffs flat inject addDistinct (distinct, hd descr));
   3.293 +      addIffs flat (inject @ distinct));
   3.294  
   3.295    in
   3.296      (thy11,
   3.297 @@ -505,7 +566,7 @@
   3.298        Sign.string_of_term sign t);
   3.299  
   3.300      fun get_typ (t as _ $ Var (_, Type (tname, Ts))) =
   3.301 -          ((tname, map dest_TFree Ts) handle _ => err t)
   3.302 +          ((tname, map dest_TFree Ts) handle TERM _ => err t)
   3.303        | get_typ t = err t;
   3.304  
   3.305      val dtnames = map get_typ (dest_conj (HOLogic.dest_Trueprop (concl_of induction')));
   3.306 @@ -535,7 +596,7 @@
   3.307      val (thy2, casedist_thms) = thy1 |>
   3.308        DatatypeAbsProofs.prove_casedist_thms new_type_names [descr] sorts induction;
   3.309      val (thy3, reccomb_names, rec_thms) = DatatypeAbsProofs.prove_primrec_thms
   3.310 -      false new_type_names [descr] sorts dt_info inject distinct induction thy2;
   3.311 +      false new_type_names [descr] sorts dt_info inject distinct dist_ss induction thy2;
   3.312      val (thy4, case_names, case_thms) = DatatypeAbsProofs.prove_case_thms false
   3.313        new_type_names [descr] sorts reccomb_names rec_thms thy3;
   3.314      val (thy5, split_thms) = DatatypeAbsProofs.prove_split_thms
   3.315 @@ -552,7 +613,7 @@
   3.316  
   3.317      val dt_infos = map (make_dt_info descr induction reccomb_names rec_thms)
   3.318        ((0 upto length descr - 1) ~~ descr ~~ case_names ~~ case_thms ~~
   3.319 -        casedist_thms ~~ distinct ~~ inject ~~ nchotomys ~~ case_congs);
   3.320 +        casedist_thms ~~ map FewConstrs distinct ~~ inject ~~ nchotomys ~~ case_congs);
   3.321  
   3.322      val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms;
   3.323  
   3.324 @@ -564,7 +625,7 @@
   3.325  
   3.326      val _ = store_clasimp thy9 ((claset_of thy9, simpset_of thy9)
   3.327        addsimps2 flat case_thms addsimps2 size_thms addsimps2 rec_thms
   3.328 -      addIffs flat inject addDistinct (distinct, descr));
   3.329 +      addIffs flat (inject @ distinct));
   3.330  
   3.331    in
   3.332      (thy9,
   3.333 @@ -641,10 +702,10 @@
   3.334        end;
   3.335  
   3.336      val (dts', constr_syntax, sorts', i) = foldl prep_dt_spec (([], [], [], 0), dts);
   3.337 +    val sorts = sorts' @ (map (rpair (Sign.defaultS sign)) (tyvars \\ map fst sorts'));
   3.338      val dt_info = get_datatypes thy;
   3.339 -    val (descr, _) = unfold_datatypes dt_info dts' i;
   3.340 +    val (descr, _) = unfold_datatypes sign dts' sorts dt_info dts' i;
   3.341      val _ = check_nonempty descr;
   3.342 -    val sorts = sorts' @ (map (rpair (Sign.defaultS sign)) (tyvars \\ map fst sorts'));
   3.343  
   3.344    in
   3.345      (if (!quick_and_dirty) then add_datatype_axm else add_datatype_def)
   3.346 @@ -659,7 +720,7 @@
   3.347  
   3.348  (* setup theory *)
   3.349  
   3.350 -val setup = [DatatypesData.init];
   3.351 +val setup = [DatatypesData.init] @ simproc_setup;
   3.352  
   3.353  
   3.354  (* outer syntax *)
     4.1 --- a/src/HOL/Tools/datatype_prop.ML	Fri Jul 16 12:09:48 1999 +0200
     4.2 +++ b/src/HOL/Tools/datatype_prop.ML	Fri Jul 16 12:14:04 1999 +0200
     4.3 @@ -8,7 +8,7 @@
     4.4  
     4.5  signature DATATYPE_PROP =
     4.6  sig
     4.7 -  val dtK : int
     4.8 +  val dtK : int ref
     4.9    val make_injs : (int * (string * DatatypeAux.dtyp list *
    4.10      (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
    4.11        term list list
    4.12 @@ -46,7 +46,7 @@
    4.13  open DatatypeAux;
    4.14  
    4.15  (*the kind of distinctiveness axioms depends on number of constructors*)
    4.16 -val dtK = 7;
    4.17 +val dtK = ref 7;
    4.18  
    4.19  fun make_tnames Ts =
    4.20    let
    4.21 @@ -110,14 +110,19 @@
    4.22  
    4.23      fun make_ind_prem k T (cname, cargs) =
    4.24        let
    4.25 +        fun mk_prem ((DtRec k, s), T) = HOLogic.mk_Trueprop
    4.26 +              (make_pred k T $ Free (s, T))
    4.27 +          | mk_prem ((DtType ("fun", [_, DtRec k]), s), T' as Type ("fun", [T, U])) =
    4.28 +              HOLogic.mk_Trueprop (HOLogic.all_const T $
    4.29 +                Abs ("x", T, make_pred k U $ (Free (s, T') $ Bound 0)));
    4.30 +
    4.31          val recs = filter is_rec_type cargs;
    4.32          val Ts = map (typ_of_dtyp descr' sorts) cargs;
    4.33          val recTs' = map (typ_of_dtyp descr' sorts) recs;
    4.34          val tnames = variantlist (make_tnames Ts, pnames);
    4.35          val rec_tnames = map fst (filter (is_rec_type o snd) (tnames ~~ cargs));
    4.36          val frees = tnames ~~ Ts;
    4.37 -        val prems = map (fn ((r, s), T) => HOLogic.mk_Trueprop
    4.38 -          (make_pred (dest_DtRec r) T $ Free (s, T))) (recs ~~ rec_tnames ~~ recTs');
    4.39 +        val prems = map mk_prem (recs ~~ rec_tnames ~~ recTs');
    4.40  
    4.41        in list_all_free (frees, Logic.list_implies (prems,
    4.42          HOLogic.mk_Trueprop (make_pred k T $ 
    4.43 @@ -162,6 +167,8 @@
    4.44  
    4.45  fun make_primrecs new_type_names descr sorts thy =
    4.46    let
    4.47 +    val o_name = Sign.intern_const (sign_of Fun.thy) "op o";
    4.48 +
    4.49      val sign = Theory.sign_of thy;
    4.50  
    4.51      val descr' = flat descr;
    4.52 @@ -174,9 +181,14 @@
    4.53      val reccomb_fn_Ts = flat (map (fn (i, (_, _, constrs)) =>
    4.54        map (fn (_, cargs) =>
    4.55          let
    4.56 -          val recs = filter is_rec_type cargs;
    4.57 -          val argTs = (map (typ_of_dtyp descr' sorts) cargs) @
    4.58 -            (map (fn r => nth_elem (dest_DtRec r, rec_result_Ts)) recs)
    4.59 +          val Ts = map (typ_of_dtyp descr' sorts) cargs;
    4.60 +          val recs = filter (is_rec_type o fst) (cargs ~~ Ts);
    4.61 +
    4.62 +          fun mk_argT (DtRec k, _) = nth_elem (k, rec_result_Ts)
    4.63 +            | mk_argT (DtType ("fun", [_, DtRec k]), Type ("fun", [T, _])) =
    4.64 +               T --> nth_elem (k, rec_result_Ts);
    4.65 +
    4.66 +          val argTs = Ts @ map mk_argT recs
    4.67          in argTs ---> nth_elem (i, rec_result_Ts)
    4.68          end) constrs) descr');
    4.69  
    4.70 @@ -201,7 +213,14 @@
    4.71          val rec_tnames = map fst (filter (is_rec_type o snd) (tnames ~~ cargs));
    4.72          val frees = map Free (tnames ~~ Ts);
    4.73          val frees' = map Free (rec_tnames ~~ recTs');
    4.74 -        val reccombs' = map (fn (DtRec i) => nth_elem (i, reccombs)) recs
    4.75 +
    4.76 +        fun mk_reccomb (DtRec i, _) = nth_elem (i, reccombs)
    4.77 +          | mk_reccomb (DtType ("fun", [_, DtRec i]), Type ("fun", [T, U])) =
    4.78 +              let val T' = nth_elem (i, rec_result_Ts)
    4.79 +              in Const (o_name, [U --> T', T --> U, T] ---> T') $ nth_elem (i, reccombs)
    4.80 +              end;
    4.81 +
    4.82 +        val reccombs' = map mk_reccomb (recs ~~ recTs')
    4.83  
    4.84        in (ts @ [HOLogic.mk_Trueprop (HOLogic.mk_eq
    4.85          (comb_t $ list_comb (Const (cname, Ts ---> T), frees),
    4.86 @@ -292,35 +311,12 @@
    4.87            in (make_distincts' constrs) @ (make_distincts_1 T constrs)
    4.88            end;
    4.89  
    4.90 -    (**** number of constructors >= dtK : t_ord C_i ... = i ****)
    4.91 -
    4.92 -    fun make_distincts_2 T tname i constrs =
    4.93 -      let
    4.94 -        val ord_name = Sign.intern_const (Theory.sign_of thy) (tname ^ "_ord");
    4.95 -        val ord_t = Const (ord_name, T --> HOLogic.natT)
    4.96 -
    4.97 -      in (case constrs of
    4.98 -          [] => [Logic.mk_implies (HOLogic.mk_Trueprop (Not $ HOLogic.mk_eq
    4.99 -             (ord_t $ Free ("x", T), ord_t $ Free ("y", T))),
   4.100 -               HOLogic.mk_Trueprop (Not $ HOLogic.mk_eq
   4.101 -                 (Free ("x", T), Free ("y", T))))]
   4.102 -        | ((cname, cargs)::constrs) =>
   4.103 -            let
   4.104 -              val Ts = map (typ_of_dtyp descr' sorts) cargs;
   4.105 -              val frees = map Free ((make_tnames Ts) ~~ Ts);
   4.106 -            in
   4.107 -              (HOLogic.mk_Trueprop (HOLogic.mk_eq (ord_t $
   4.108 -                list_comb (Const (cname, Ts ---> T), frees), HOLogic.mk_nat i)))::
   4.109 -                  (make_distincts_2 T tname (i + 1) constrs)
   4.110 -            end)
   4.111 -      end;
   4.112 -
   4.113    in map (fn (((_, (_, _, constrs)), T), tname) =>
   4.114 -      if length constrs < dtK then make_distincts_1 T constrs
   4.115 -      else make_distincts_2 T tname 0 constrs)
   4.116 +      if length constrs < !dtK then make_distincts_1 T constrs else [])
   4.117          ((hd descr) ~~ newTs ~~ new_type_names)
   4.118    end;
   4.119  
   4.120 +
   4.121  (*************************** the "split" - equations **************************)
   4.122  
   4.123  fun make_splits new_type_names descr sorts thy =
   4.124 @@ -403,7 +399,7 @@
   4.125      val recTs = get_rec_types descr' sorts;
   4.126  
   4.127      val big_size_name = space_implode "_" new_type_names ^ "_size";
   4.128 -    val size_name = Sign.intern_const (Theory.sign_of (the (get_thy "Arith" thy))) "size";
   4.129 +    val size_name = Sign.intern_const (Theory.sign_of (theory "Arith")) "size";
   4.130      val size_names = replicate (length (hd descr)) size_name @
   4.131        map (Sign.intern_const (Theory.sign_of thy))
   4.132          (if length (flat (tl descr)) = 1 then [big_size_name] else
     5.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Fri Jul 16 12:09:48 1999 +0200
     5.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Fri Jul 16 12:14:04 1999 +0200
     5.3 @@ -12,13 +12,16 @@
     5.4  
     5.5  *)
     5.6  
     5.7 +val foo = ref [TrueI];
     5.8 +
     5.9  signature DATATYPE_REP_PROOFS =
    5.10  sig
    5.11    val representation_proofs : bool -> DatatypeAux.datatype_info Symtab.table ->
    5.12      string list -> (int * (string * DatatypeAux.dtyp list *
    5.13        (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
    5.14          (string * mixfix) list -> (string * mixfix) list list -> theory ->
    5.15 -          theory * thm list list * thm list list * thm
    5.16 +          theory * thm list list * thm list list * thm list list *
    5.17 +            DatatypeAux.simproc_dist list * thm
    5.18  end;
    5.19  
    5.20  structure DatatypeRepProofs : DATATYPE_REP_PROOFS =
    5.21 @@ -43,15 +46,22 @@
    5.22  fun representation_proofs flat_names (dt_info : datatype_info Symtab.table)
    5.23        new_type_names descr sorts types_syntax constr_syntax thy =
    5.24    let
    5.25 -    val Univ_thy = the (get_thy "Univ" thy);
    5.26 -    val node_name = Sign.intern_tycon (Theory.sign_of Univ_thy) "node";
    5.27 -    val [In0_name, In1_name, Scons_name, Leaf_name, Numb_name] =
    5.28 -      map (Sign.intern_const (Theory.sign_of Univ_thy))
    5.29 -        ["In0", "In1", "Scons", "Leaf", "Numb"];
    5.30 +    val Datatype_thy = theory "Datatype";
    5.31 +    val node_name = Sign.intern_tycon (Theory.sign_of Datatype_thy) "node";
    5.32 +    val [In0_name, In1_name, Scons_name, Leaf_name, Numb_name, Lim_name,
    5.33 +      Funs_name, o_name] =
    5.34 +      map (Sign.intern_const (Theory.sign_of Datatype_thy))
    5.35 +        ["In0", "In1", "Scons", "Leaf", "Numb", "Lim", "Funs", "op o"];
    5.36 +
    5.37      val [In0_inject, In1_inject, Scons_inject, Leaf_inject, In0_eq, In1_eq,
    5.38 -      In0_not_In1, In1_not_In0] = map (get_thm Univ_thy)
    5.39 -        ["In0_inject", "In1_inject", "Scons_inject", "Leaf_inject", "In0_eq",
    5.40 -         "In1_eq", "In0_not_In1", "In1_not_In0"];
    5.41 +         In0_not_In1, In1_not_In0, Funs_mono, FunsI, Lim_inject,
    5.42 +         Funs_inv, FunsD, Funs_rangeE, Funs_nonempty] = map (get_thm Datatype_thy)
    5.43 +        ["In0_inject", "In1_inject", "Scons_inject", "Leaf_inject", "In0_eq", "In1_eq",
    5.44 +         "In0_not_In1", "In1_not_In0", "Funs_mono", "FunsI", "Lim_inject",
    5.45 +         "Funs_inv", "FunsD", "Funs_rangeE", "Funs_nonempty"];
    5.46 +
    5.47 +    val Funs_IntE = (Int_lower2 RS Funs_mono RS
    5.48 +      (Int_lower1 RS Funs_mono RS Int_greatest) RS subsetD) RS IntE;
    5.49  
    5.50      val descr' = flat descr;
    5.51  
    5.52 @@ -65,19 +75,23 @@
    5.53  
    5.54      val tyvars = map (fn (_, (_, Ts, _)) => map dest_DtTFree Ts) (hd descr);
    5.55      val leafTs' = get_nonrec_types descr' sorts;
    5.56 -    val unneeded_vars = hd tyvars \\ foldr add_typ_tfree_names (leafTs', []);
    5.57 +    val branchTs = get_branching_types descr' sorts;
    5.58 +    val branchT = if null branchTs then HOLogic.unitT
    5.59 +      else fold_bal (fn (T, U) => Type ("+", [T, U])) branchTs;
    5.60 +    val unneeded_vars = hd tyvars \\ foldr add_typ_tfree_names (leafTs' @ branchTs, []);
    5.61      val leafTs = leafTs' @ (map (fn n => TFree (n, the (assoc (sorts, n)))) unneeded_vars);
    5.62      val recTs = get_rec_types descr' sorts;
    5.63      val newTs = take (length (hd descr), recTs);
    5.64      val oldTs = drop (length (hd descr), recTs);
    5.65      val sumT = if null leafTs then HOLogic.unitT
    5.66        else fold_bal (fn (T, U) => Type ("+", [T, U])) leafTs;
    5.67 -    val Univ_elT = HOLogic.mk_setT (Type (node_name, [sumT]));
    5.68 +    val Univ_elT = HOLogic.mk_setT (Type (node_name, [sumT, branchT]));
    5.69      val UnivT = HOLogic.mk_setT Univ_elT;
    5.70  
    5.71      val In0 = Const (In0_name, Univ_elT --> Univ_elT);
    5.72      val In1 = Const (In1_name, Univ_elT --> Univ_elT);
    5.73      val Leaf = Const (Leaf_name, sumT --> Univ_elT);
    5.74 +    val Lim = Const (Lim_name, (branchT --> Univ_elT) --> Univ_elT);
    5.75  
    5.76      (* make injections needed for embedding types in leaves *)
    5.77  
    5.78 @@ -103,6 +117,25 @@
    5.79        else
    5.80          foldr1 (HOLogic.mk_binop Scons_name) ts);
    5.81  
    5.82 +    (* function spaces *)
    5.83 +
    5.84 +    fun mk_fun_inj T' x =
    5.85 +      let
    5.86 +        fun mk_inj T n i =
    5.87 +          if n = 1 then x else
    5.88 +          let
    5.89 +            val n2 = n div 2;
    5.90 +            val Type (_, [T1, T2]) = T;
    5.91 +            val sum_case = Const ("sum_case", [T1 --> Univ_elT, T2 --> Univ_elT, T] ---> Univ_elT)
    5.92 +          in
    5.93 +            if i <= n2 then
    5.94 +              sum_case $ (mk_inj T1 n2 i) $ Const ("arbitrary", T2 --> Univ_elT)
    5.95 +            else
    5.96 +              sum_case $ Const ("arbitrary", T1 --> Univ_elT) $ mk_inj T2 (n - n2) (i - n2)
    5.97 +          end
    5.98 +      in mk_inj branchT (length branchTs) (1 + find_index_eq T' branchTs)
    5.99 +      end;
   5.100 +
   5.101      (************** generate introduction rules for representing set **********)
   5.102  
   5.103      val _ = message "Constructing representing sets ...";
   5.104 @@ -116,6 +149,14 @@
   5.105                in (j + 1, (HOLogic.mk_mem (free_t,
   5.106                  Const (nth_elem (k, rep_set_names), UnivT)))::prems, free_t::ts)
   5.107                end
   5.108 +          | mk_prem (DtType ("fun", [T, DtRec k]), (j, prems, ts)) =
   5.109 +              let val T' = typ_of_dtyp descr' sorts T;
   5.110 +                  val free_t = mk_Free "x" (T' --> Univ_elT) j
   5.111 +              in (j + 1, (HOLogic.mk_mem (free_t,
   5.112 +                Const (Funs_name, UnivT --> HOLogic.mk_setT (T' --> Univ_elT)) $
   5.113 +                  Const (nth_elem (k, rep_set_names), UnivT)))::prems,
   5.114 +                    Lim $ mk_fun_inj T' free_t::ts)
   5.115 +              end
   5.116            | mk_prem (dt, (j, prems, ts)) =
   5.117                let val T = typ_of_dtyp descr' sorts dt
   5.118                in (j + 1, prems, (Leaf $ mk_inj T (mk_Free "x" T j))::ts)
   5.119 @@ -136,16 +177,17 @@
   5.120      val (thy2, {raw_induct = rep_induct, intrs = rep_intrs, ...}) =
   5.121        setmp InductivePackage.quiet_mode (!quiet_mode)
   5.122          (InductivePackage.add_inductive_i false true big_rec_name false true false
   5.123 -           consts [] (map (fn x => (("", x), [])) intr_ts) [] []) thy1;
   5.124 +           consts [] (map (fn x => (("", x), [])) intr_ts) [Funs_mono] []) thy1;
   5.125  
   5.126      (********************************* typedef ********************************)
   5.127  
   5.128      val thy3 = add_path flat_names big_name (foldl (fn (thy, ((((name, mx), tvs), c), name')) =>
   5.129        setmp TypedefPackage.quiet_mode true
   5.130          (TypedefPackage.add_typedef_i_no_def name' (name, tvs, mx) c [] []
   5.131 -          (Some (QUIET_BREADTH_FIRST (has_fewer_prems 1) (resolve_tac rep_intrs 1)))) thy)
   5.132 -            (parent_path flat_names thy2, types_syntax ~~ tyvars ~~ (take (length newTs, consts)) ~~
   5.133 -              new_type_names));
   5.134 +          (Some (QUIET_BREADTH_FIRST (has_fewer_prems 1)
   5.135 +            (resolve_tac (Funs_nonempty::rep_intrs) 1)))) thy)
   5.136 +              (parent_path flat_names thy2, types_syntax ~~ tyvars ~~
   5.137 +                (take (length newTs, consts)) ~~ new_type_names));
   5.138  
   5.139      (*********************** definition of constructors ***********************)
   5.140  
   5.141 @@ -171,6 +213,13 @@
   5.142            in (case dt of
   5.143                DtRec m => (j + 1, free_t::l_args, (Const (nth_elem (m, all_rep_names),
   5.144                  T --> Univ_elT) $ free_t)::r_args)
   5.145 +            | DtType ("fun", [T', DtRec m]) =>
   5.146 +                let val ([T''], T''') = strip_type T
   5.147 +                in (j + 1, free_t::l_args, (Lim $ mk_fun_inj T''
   5.148 +                  (Const (o_name, [T''' --> Univ_elT, T, T''] ---> Univ_elT) $
   5.149 +                    Const (nth_elem (m, all_rep_names), T''' --> Univ_elT) $ free_t))::r_args)
   5.150 +                end
   5.151 +
   5.152              | _ => (j + 1, free_t::l_args, (Leaf $ mk_inj T free_t)::r_args))
   5.153            end;
   5.154  
   5.155 @@ -200,8 +249,8 @@
   5.156          val sg = Theory.sign_of thy;
   5.157          val rep_const = cterm_of sg
   5.158            (Const (Sign.intern_const sg ("Rep_" ^ tname), T --> Univ_elT));
   5.159 -        val cong' = cterm_instantiate [(cterm_of sg cong_f, rep_const)] arg_cong;
   5.160 -        val dist = cterm_instantiate [(cterm_of sg distinct_f, rep_const)] distinct_lemma;
   5.161 +        val cong' = standard (cterm_instantiate [(cterm_of sg cong_f, rep_const)] arg_cong);
   5.162 +        val dist = standard (cterm_instantiate [(cterm_of sg distinct_f, rep_const)] distinct_lemma);
   5.163          val (thy', defs', eqns', _) = foldl ((make_constr_def tname T) (length constrs))
   5.164            ((add_path flat_names tname thy, defs, [], 1), constrs ~~ constr_syntax)
   5.165        in
   5.166 @@ -282,23 +331,34 @@
   5.167          val rep_const = Const (rep_name, T --> Univ_elT);
   5.168          val constr = Const (cname, argTs ---> T);
   5.169  
   5.170 -        fun process_arg ks' ((i2, i2', ts), dt) =
   5.171 +        fun process_arg ks' ((i2, i2', ts, Ts), dt) =
   5.172            let val T' = typ_of_dtyp descr' sorts dt
   5.173            in (case dt of
   5.174                DtRec j => if j mem ks' then
   5.175 -                  (i2 + 1, i2' + 1, ts @ [mk_Free "y" Univ_elT i2'])
   5.176 +                  (i2 + 1, i2' + 1, ts @ [mk_Free "y" Univ_elT i2'], Ts @ [Univ_elT])
   5.177                  else
   5.178                    (i2 + 1, i2', ts @ [Const (nth_elem (j, all_rep_names),
   5.179 -                    T' --> Univ_elT) $ mk_Free "x" T' i2])
   5.180 -            | _ => (i2 + 1, i2', ts @ [Leaf $ mk_inj T' (mk_Free "x" T' i2)]))
   5.181 +                    T' --> Univ_elT) $ mk_Free "x" T' i2], Ts)
   5.182 +            | (DtType ("fun", [_, DtRec j])) =>
   5.183 +                let val ([T''], T''') = strip_type T'
   5.184 +                in if j mem ks' then
   5.185 +                    (i2 + 1, i2' + 1, ts @ [Lim $ mk_fun_inj T''
   5.186 +                      (mk_Free "y" (T'' --> Univ_elT) i2')], Ts @ [T'' --> Univ_elT])
   5.187 +                  else
   5.188 +                    (i2 + 1, i2', ts @ [Lim $ mk_fun_inj T''
   5.189 +                      (Const (o_name, [T''' --> Univ_elT, T', T''] ---> Univ_elT) $
   5.190 +                        Const (nth_elem (j, all_rep_names), T''' --> Univ_elT) $
   5.191 +                          mk_Free "x" T' i2)], Ts)
   5.192 +                end
   5.193 +            | _ => (i2 + 1, i2', ts @ [Leaf $ mk_inj T' (mk_Free "x" T' i2)], Ts))
   5.194            end;
   5.195  
   5.196 -        val (i2, i2', ts) = foldl (process_arg ks) ((1, 1, []), cargs);
   5.197 +        val (i2, i2', ts, Ts) = foldl (process_arg ks) ((1, 1, [], []), cargs);
   5.198          val xs = map (uncurry (mk_Free "x")) (argTs ~~ (1 upto (i2 - 1)));
   5.199 -        val ys = map (mk_Free "y" Univ_elT) (1 upto (i2' - 1));
   5.200 +        val ys = map (uncurry (mk_Free "y")) (Ts ~~ (1 upto (i2' - 1)));
   5.201          val f = list_abs_free (map dest_Free (xs @ ys), mk_univ_inj ts n i);
   5.202  
   5.203 -        val (_, _, ts') = foldl (process_arg []) ((1, 1, []), cargs);
   5.204 +        val (_, _, ts', _) = foldl (process_arg []) ((1, 1, [], []), cargs);
   5.205          val eqn = HOLogic.mk_Trueprop (HOLogic.mk_eq
   5.206            (rep_const $ list_comb (constr, xs), mk_univ_inj ts' n i))
   5.207  
   5.208 @@ -340,6 +400,21 @@
   5.209  
   5.210      (* prove isomorphism properties *)
   5.211  
   5.212 +    fun mk_funs_inv thm =
   5.213 +      let
   5.214 +        val [_, t] = prems_of Funs_inv;
   5.215 +        val [_ $ (_ $ _ $ R)] = Logic.strip_assums_hyp t;
   5.216 +        val _ $ (_ $ (r $ (a $ _)) $ _) = Logic.strip_assums_concl t;
   5.217 +        val [_ $ (_ $ _ $ R')] = prems_of thm;
   5.218 +        val _ $ (_ $ (r' $ (a' $ _)) $ _) = concl_of thm;
   5.219 +        val inv' = cterm_instantiate (map 
   5.220 +          ((pairself (cterm_of (sign_of_thm thm))) o
   5.221 +           (apsnd (map_term_types (incr_tvar 1))))
   5.222 +             [(R, R'), (r, r'), (a, a')]) Funs_inv
   5.223 +      in
   5.224 +        rule_by_tactic (atac 2) (thm RSN (2, inv'))
   5.225 +      end;
   5.226 +
   5.227      (* prove  x : dt_rep_set_i --> x : range dt_Rep_i *)
   5.228  
   5.229      fun mk_iso_t (((set_name, iso_name), i), T) =
   5.230 @@ -355,8 +430,6 @@
   5.231      val iso_t = HOLogic.mk_Trueprop (mk_conj (map mk_iso_t
   5.232        (rep_set_names ~~ all_rep_names ~~ (0 upto (length descr' - 1)) ~~ recTs)));
   5.233  
   5.234 -    val newT_Abs_inverse_thms = map (fn (iso, _, _) => iso RS subst) newT_iso_axms;
   5.235 -
   5.236      (* all the theorems are proved by one single simultaneous induction *)
   5.237  
   5.238      val iso_thms = if length descr = 1 then [] else
   5.239 @@ -365,14 +438,19 @@
   5.240             [indtac rep_induct 1,
   5.241              REPEAT (rtac TrueI 1),
   5.242              REPEAT (EVERY
   5.243 -              [REPEAT (etac rangeE 1),
   5.244 -               REPEAT (eresolve_tac newT_Abs_inverse_thms 1),
   5.245 +              [rewrite_goals_tac [mk_meta_eq Collect_mem_eq],
   5.246 +               REPEAT (etac Funs_IntE 1),
   5.247 +               REPEAT (eresolve_tac [rangeE, Funs_rangeE] 1),
   5.248 +               REPEAT (eresolve_tac (map (fn (iso, _, _) => iso RS subst) newT_iso_axms @
   5.249 +                 map (fn (iso, _, _) => mk_funs_inv iso RS subst) newT_iso_axms) 1),
   5.250                 TRY (hyp_subst_tac 1),
   5.251                 rtac (sym RS range_eqI) 1,
   5.252                 resolve_tac iso_char_thms 1])])));
   5.253  
   5.254 -    val Abs_inverse_thms = newT_Abs_inverse_thms @ (map (fn r =>
   5.255 -      r RS mp RS f_inv_f RS subst) iso_thms);
   5.256 +    val Abs_inverse_thms' = (map #1 newT_iso_axms) @ map (fn r => r RS mp RS f_inv_f) iso_thms;
   5.257 +
   5.258 +    val Abs_inverse_thms = map (fn r => r RS subst) (Abs_inverse_thms' @
   5.259 +      map mk_funs_inv Abs_inverse_thms');
   5.260  
   5.261      (* prove  inj dt_Rep_i  and  dt_Rep_i x : dt_rep_set_i *)
   5.262  
   5.263 @@ -395,7 +473,7 @@
   5.264          val (ind_concl1, ind_concl2) = ListPair.unzip (map mk_ind_concl ds);
   5.265  
   5.266          val rewrites = map mk_meta_eq iso_char_thms;
   5.267 -        val inj_thms' = map (fn r => r RS injD) inj_thms;
   5.268 +        val inj_thms' = flat (map (fn r => [r RS injD, r RS inj_o]) inj_thms);
   5.269  
   5.270          val inj_thm = prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5)
   5.271            (HOLogic.mk_Trueprop (mk_conj ind_concl1))) (fn _ =>
   5.272 @@ -411,8 +489,9 @@
   5.273                     ORELSE (EVERY
   5.274                       [REPEAT (etac Scons_inject 1),
   5.275                        REPEAT (dresolve_tac
   5.276 -                        (inj_thms' @ [Leaf_inject, Inl_inject, Inr_inject]) 1),
   5.277 -                      REPEAT (EVERY [etac allE 1, dtac mp 1, atac 1]),
   5.278 +                        (inj_thms' @ [Leaf_inject, Lim_inject, Inl_inject, Inr_inject]) 1),
   5.279 +                      REPEAT ((EVERY [etac allE 1, dtac mp 1, atac 1]) ORELSE
   5.280 +                              (dtac inj_fun_lemma 1 THEN atac 1)),
   5.281                        TRY (hyp_subst_tac 1),
   5.282                        rtac refl 1])])])]);
   5.283  
   5.284 @@ -425,11 +504,11 @@
   5.285  	       (HOLogic.mk_Trueprop (mk_conj ind_concl2)))
   5.286  	      (fn _ =>
   5.287  	       [indtac induction 1,
   5.288 -		rewrite_goals_tac rewrites,
   5.289 +		rewrite_goals_tac (o_def :: rewrites),
   5.290  		REPEAT (EVERY
   5.291  			[resolve_tac rep_intrs 1,
   5.292 -			 REPEAT ((atac 1) ORELSE
   5.293 -				 (resolve_tac elem_thms 1))])]);
   5.294 +			 REPEAT (FIRST [atac 1, etac spec 1,
   5.295 +				 resolve_tac (FunsI :: elem_thms) 1])])]);
   5.296  
   5.297        in (inj_thms @ inj_thms'', elem_thms @ (split_conj_thm elem_thm))
   5.298        end;
   5.299 @@ -446,19 +525,18 @@
   5.300      fun prove_constr_rep_thm eqn =
   5.301        let
   5.302          val inj_thms = map (fn (r, _) => r RS inj_onD) newT_iso_inj_thms;
   5.303 -        val rewrites = constr_defs @ (map (mk_meta_eq o #2) newT_iso_axms)
   5.304 +        val rewrites = o_def :: constr_defs @ (map (mk_meta_eq o #2) newT_iso_axms)
   5.305        in prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5) eqn) (fn _ =>
   5.306          [resolve_tac inj_thms 1,
   5.307           rewrite_goals_tac rewrites,
   5.308           rtac refl 1,
   5.309           resolve_tac rep_intrs 2,
   5.310 -         REPEAT (resolve_tac iso_elem_thms 1)])
   5.311 +         REPEAT (resolve_tac (FunsI :: iso_elem_thms) 1)])
   5.312        end;
   5.313  
   5.314      (*--------------------------------------------------------------*)
   5.315      (* constr_rep_thms and rep_congs are used to prove distinctness *)
   5.316 -    (* of constructors internally.                                  *)
   5.317 -    (* the external version uses dt_case which is not defined yet   *)
   5.318 +    (* of constructors.                                             *)
   5.319      (*--------------------------------------------------------------*)
   5.320  
   5.321      val constr_rep_thms = map (map prove_constr_rep_thm) constr_rep_eqns;
   5.322 @@ -467,27 +545,45 @@
   5.323        dist_lemma::(rep_thms @ [In0_eq, In1_eq, In0_not_In1, In1_not_In0]))
   5.324          (constr_rep_thms ~~ dist_lemmas);
   5.325  
   5.326 +    fun prove_distinct_thms (_, []) = []
   5.327 +      | prove_distinct_thms (dist_rewrites', t::_::ts) =
   5.328 +          let
   5.329 +            val dist_thm = prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5) t) (fn _ =>
   5.330 +              [simp_tac (HOL_ss addsimps dist_rewrites') 1])
   5.331 +          in dist_thm::(standard (dist_thm RS not_sym))::
   5.332 +            (prove_distinct_thms (dist_rewrites', ts))
   5.333 +          end;
   5.334 +
   5.335 +    val distinct_thms = map prove_distinct_thms (dist_rewrites ~~
   5.336 +      DatatypeProp.make_distincts new_type_names descr sorts thy5);
   5.337 +
   5.338 +    val simproc_dists = map (fn ((((_, (_, _, constrs)), rep_thms), congr), dists) =>
   5.339 +      if length constrs < !DatatypeProp.dtK then FewConstrs dists
   5.340 +      else ManyConstrs (congr, HOL_basic_ss addsimps rep_thms)) (hd descr ~~
   5.341 +        constr_rep_thms ~~ rep_congs ~~ distinct_thms);
   5.342 +
   5.343      (* prove injectivity of constructors *)
   5.344  
   5.345      fun prove_constr_inj_thm rep_thms t =
   5.346 -      let val inj_thms = Scons_inject::(map make_elim
   5.347 +      let val inj_thms = Scons_inject::sum_case_inject::(map make_elim
   5.348          ((map (fn r => r RS injD) iso_inj_thms) @
   5.349 -          [In0_inject, In1_inject, Leaf_inject, Inl_inject, Inr_inject]))
   5.350 +          [In0_inject, In1_inject, Leaf_inject, Inl_inject, Inr_inject, Lim_inject]))
   5.351        in prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5) t) (fn _ =>
   5.352          [rtac iffI 1,
   5.353           REPEAT (etac conjE 2), hyp_subst_tac 2, rtac refl 2,
   5.354           dresolve_tac rep_congs 1, dtac box_equals 1,
   5.355 -         REPEAT (resolve_tac rep_thms 1),
   5.356 +         REPEAT (resolve_tac rep_thms 1), rewrite_goals_tac [o_def],
   5.357           REPEAT (eresolve_tac inj_thms 1),
   5.358 -         hyp_subst_tac 1,
   5.359 -         REPEAT (resolve_tac [conjI, refl] 1)])
   5.360 +         REPEAT (ares_tac [conjI] 1 ORELSE (EVERY [rtac ext 1, dtac fun_cong 1,
   5.361 +                  eresolve_tac inj_thms 1, atac 1]))])
   5.362        end;
   5.363  
   5.364      val constr_inject = map (fn (ts, thms) => map (prove_constr_inj_thm thms) ts)
   5.365        ((DatatypeProp.make_injs descr sorts) ~~ constr_rep_thms);
   5.366  
   5.367 -    val thy6 = store_thmss "inject" new_type_names
   5.368 -      constr_inject (parent_path flat_names thy5);
   5.369 +    val thy6 = thy5 |> parent_path flat_names |>
   5.370 +      store_thmss "inject" new_type_names constr_inject |>
   5.371 +      store_thmss "distinct" new_type_names distinct_thms;
   5.372  
   5.373      (*************************** induction theorem ****************************)
   5.374  
   5.375 @@ -538,17 +634,18 @@
   5.376        (DatatypeProp.make_ind descr sorts)) (fn prems =>
   5.377          [rtac indrule_lemma' 1, indtac rep_induct 1,
   5.378           EVERY (map (fn (prem, r) => (EVERY
   5.379 -           [REPEAT (eresolve_tac Abs_inverse_thms 1),
   5.380 +           [REPEAT (eresolve_tac (Funs_IntE::Abs_inverse_thms) 1),
   5.381              simp_tac (HOL_basic_ss addsimps ((symmetric r)::Rep_inverse_thms')) 1,
   5.382 -            DEPTH_SOLVE_1 (ares_tac [prem] 1)]))
   5.383 -              (prems ~~ (constr_defs @ (map mk_meta_eq iso_char_thms))))]);
   5.384 +            DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE (EVERY [rewrite_goals_tac [o_def],
   5.385 +              rtac allI 1, dtac FunsD 1, etac CollectD 1]))]))
   5.386 +                (prems ~~ (constr_defs @ (map mk_meta_eq iso_char_thms))))]);
   5.387  
   5.388      val thy7 = thy6 |>
   5.389        Theory.add_path big_name |>
   5.390        PureThy.add_thms [(("induct", dt_induct), [])] |>
   5.391        Theory.parent_path;
   5.392  
   5.393 -  in (thy7, constr_inject, dist_rewrites, dt_induct)
   5.394 +  in (thy7, constr_inject, distinct_thms, dist_rewrites, simproc_dists, dt_induct)
   5.395    end;
   5.396  
   5.397  end;