src/HOL/Tools/datatype_rep_proofs.ML
changeset 13641 63d1790a43ed
parent 13585 db4005b40cc6
child 14981 e73f8140af78
     1.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Thu Oct 10 14:23:47 2002 +0200
     1.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Thu Oct 10 14:26:50 2002 +0200
     1.3 @@ -15,11 +15,10 @@
     1.4  signature DATATYPE_REP_PROOFS =
     1.5  sig
     1.6    val representation_proofs : bool -> DatatypeAux.datatype_info Symtab.table ->
     1.7 -    string list -> (int * (string * DatatypeAux.dtyp list *
     1.8 -      (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
     1.9 -        (string * mixfix) list -> (string * mixfix) list list -> theory attribute
    1.10 -          -> theory -> theory * thm list list * thm list list * thm list list *
    1.11 -            DatatypeAux.simproc_dist list * thm
    1.12 +    string list -> DatatypeAux.descr list -> (string * sort) list ->
    1.13 +      (string * mixfix) list -> (string * mixfix) list list -> theory attribute
    1.14 +        -> theory -> theory * thm list list * thm list list * thm list list *
    1.15 +          DatatypeAux.simproc_dist list * thm
    1.16  end;
    1.17  
    1.18  structure DatatypeRepProofs : DATATYPE_REP_PROOFS =
    1.19 @@ -54,19 +53,15 @@
    1.20      val Leaf_name = "Datatype_Universe.Leaf";
    1.21      val Numb_name = "Datatype_Universe.Numb";
    1.22      val Lim_name = "Datatype_Universe.Lim";
    1.23 -    val Funs_name = "Datatype_Universe.Funs";
    1.24 -    val o_name = "Fun.comp";
    1.25 -    val sum_case_name = "Datatype.sum.sum_case";
    1.26 +    val Suml_name = "Datatype.Suml";
    1.27 +    val Sumr_name = "Datatype.Sumr";
    1.28  
    1.29 -    val [In0_inject, In1_inject, Scons_inject, Leaf_inject, In0_eq, In1_eq,
    1.30 -         In0_not_In1, In1_not_In0, Funs_mono, FunsI, Lim_inject,
    1.31 -         Funs_inv, FunsD, Funs_rangeE, Funs_nonempty, sum_case_inject] = map (get_thm Datatype_thy)
    1.32 -        ["In0_inject", "In1_inject", "Scons_inject", "Leaf_inject", "In0_eq", "In1_eq",
    1.33 -         "In0_not_In1", "In1_not_In0", "Funs_mono", "FunsI", "Lim_inject",
    1.34 -         "Funs_inv", "FunsD", "Funs_rangeE", "Funs_nonempty", "sum_case_inject"];
    1.35 -
    1.36 -    val Funs_IntE = (Int_lower2 RS Funs_mono RS
    1.37 -      (Int_lower1 RS Funs_mono RS Int_greatest) RS subsetD) RS IntE;
    1.38 +    val [In0_inject, In1_inject, Scons_inject, Leaf_inject,
    1.39 +         In0_eq, In1_eq, In0_not_In1, In1_not_In0,
    1.40 +         Lim_inject, Suml_inject, Sumr_inject] = map (get_thm Datatype_thy)
    1.41 +        ["In0_inject", "In1_inject", "Scons_inject", "Leaf_inject",
    1.42 +         "In0_eq", "In1_eq", "In0_not_In1", "In1_not_In0",
    1.43 +         "Lim_inject", "Suml_inject", "Sumr_inject"];
    1.44  
    1.45      val descr' = flat descr;
    1.46  
    1.47 @@ -83,6 +78,7 @@
    1.48      val branchTs = get_branching_types descr' sorts;
    1.49      val branchT = if null branchTs then HOLogic.unitT
    1.50        else fold_bal (fn (T, U) => Type ("+", [T, U])) branchTs;
    1.51 +    val arities = get_arities descr' \ 0;
    1.52      val unneeded_vars = hd tyvars \\ foldr add_typ_tfree_names (leafTs' @ branchTs, []);
    1.53      val leafTs = leafTs' @ (map (fn n => TFree (n, the (assoc (sorts, n)))) unneeded_vars);
    1.54      val recTs = get_rec_types descr' sorts;
    1.55 @@ -131,16 +127,16 @@
    1.56            let
    1.57              val n2 = n div 2;
    1.58              val Type (_, [T1, T2]) = T;
    1.59 -            val sum_case = Const (sum_case_name, [T1 --> Univ_elT, T2 --> Univ_elT, T] ---> Univ_elT)
    1.60 +            fun mkT U = (U --> Univ_elT) --> T --> Univ_elT
    1.61            in
    1.62 -            if i <= n2 then
    1.63 -              sum_case $ (mk_inj T1 n2 i) $ Const ("arbitrary", T2 --> Univ_elT)
    1.64 -            else
    1.65 -              sum_case $ Const ("arbitrary", T1 --> Univ_elT) $ mk_inj T2 (n - n2) (i - n2)
    1.66 +            if i <= n2 then Const (Suml_name, mkT T1) $ mk_inj T1 n2 i
    1.67 +            else Const (Sumr_name, mkT T2) $ mk_inj T2 (n - n2) (i - n2)
    1.68            end
    1.69        in mk_inj branchT (length branchTs) (1 + find_index_eq T' branchTs)
    1.70        end;
    1.71  
    1.72 +    val mk_lim = foldr (fn (T, t) => Lim $ mk_fun_inj T (Abs ("x", T, t)));
    1.73 +
    1.74      (************** generate introduction rules for representing set **********)
    1.75  
    1.76      val _ = message "Constructing representing sets ...";
    1.77 @@ -149,28 +145,26 @@
    1.78  
    1.79      fun make_intr s n (i, (_, cargs)) =
    1.80        let
    1.81 -        fun mk_prem (DtRec k, (j, prems, ts)) =
    1.82 -              let val free_t = mk_Free "x" Univ_elT j
    1.83 -              in (j + 1, (HOLogic.mk_mem (free_t,
    1.84 -                Const (nth_elem (k, rep_set_names), UnivT)))::prems, free_t::ts)
    1.85 +        fun mk_prem (dt, (j, prems, ts)) = (case strip_dtyp dt of
    1.86 +            (dts, DtRec k) =>
    1.87 +              let
    1.88 +                val Ts = map (typ_of_dtyp descr' sorts) dts;
    1.89 +                val free_t =
    1.90 +                  app_bnds (mk_Free "x" (Ts ---> Univ_elT) j) (length Ts)
    1.91 +              in (j + 1, list_all (map (pair "x") Ts,
    1.92 +                  HOLogic.mk_Trueprop (HOLogic.mk_mem (free_t,
    1.93 +                    Const (nth_elem (k, rep_set_names), UnivT)))) :: prems,
    1.94 +                mk_lim (Ts, free_t) :: ts)
    1.95                end
    1.96 -          | mk_prem (DtType ("fun", [T, DtRec k]), (j, prems, ts)) =
    1.97 -              let val T' = typ_of_dtyp descr' sorts T;
    1.98 -                  val free_t = mk_Free "x" (T' --> Univ_elT) j
    1.99 -              in (j + 1, (HOLogic.mk_mem (free_t,
   1.100 -                Const (Funs_name, UnivT --> HOLogic.mk_setT (T' --> Univ_elT)) $
   1.101 -                  Const (nth_elem (k, rep_set_names), UnivT)))::prems,
   1.102 -                    Lim $ mk_fun_inj T' free_t::ts)
   1.103 -              end
   1.104 -          | mk_prem (dt, (j, prems, ts)) =
   1.105 +          | _ =>
   1.106                let val T = typ_of_dtyp descr' sorts dt
   1.107                in (j + 1, prems, (Leaf $ mk_inj T (mk_Free "x" T j))::ts)
   1.108 -              end;
   1.109 +              end);
   1.110  
   1.111          val (_, prems, ts) = foldr mk_prem (cargs, (1, [], []));
   1.112          val concl = HOLogic.mk_Trueprop (HOLogic.mk_mem
   1.113            (mk_univ_inj ts n i, Const (s, UnivT)))
   1.114 -      in Logic.list_implies (map HOLogic.mk_Trueprop prems, concl)
   1.115 +      in Logic.list_implies (prems, concl)
   1.116        end;
   1.117  
   1.118      val consts = map (fn s => Const (s, UnivT)) rep_set_names;
   1.119 @@ -182,7 +176,7 @@
   1.120      val (thy2, {raw_induct = rep_induct, intrs = rep_intrs, ...}) =
   1.121        setmp InductivePackage.quiet_mode (!quiet_mode)
   1.122          (InductivePackage.add_inductive_i false true big_rec_name false true false
   1.123 -           consts (map (fn x => (("", x), [])) intr_ts) [Funs_mono]) thy1;
   1.124 +           consts (map (fn x => (("", x), [])) intr_ts) []) thy1;
   1.125  
   1.126      (********************************* typedef ********************************)
   1.127  
   1.128 @@ -191,7 +185,7 @@
   1.129          (TypedefPackage.add_typedef_i false (Some name') (name, tvs, mx) c None
   1.130            (rtac exI 1 THEN
   1.131              QUIET_BREADTH_FIRST (has_fewer_prems 1)
   1.132 -            (resolve_tac (Funs_nonempty::rep_intrs) 1))) thy |> #1)
   1.133 +            (resolve_tac rep_intrs 1))) thy |> #1)
   1.134                (parent_path flat_names thy2, types_syntax ~~ tyvars ~~
   1.135                  (take (length newTs, consts)) ~~ new_type_names));
   1.136  
   1.137 @@ -216,16 +210,10 @@
   1.138          fun constr_arg (dt, (j, l_args, r_args)) =
   1.139            let val T = typ_of_dtyp descr' sorts dt;
   1.140                val free_t = mk_Free "x" T j
   1.141 -          in (case dt of
   1.142 -              DtRec m => (j + 1, free_t::l_args, (Const (nth_elem (m, all_rep_names),
   1.143 -                T --> Univ_elT) $ free_t)::r_args)
   1.144 -            | DtType ("fun", [T', DtRec m]) =>
   1.145 -                let val ([T''], T''') = strip_type T
   1.146 -                in (j + 1, free_t::l_args, (Lim $ mk_fun_inj T''
   1.147 -                  (Const (o_name, [T''' --> Univ_elT, T, T''] ---> Univ_elT) $
   1.148 -                    Const (nth_elem (m, all_rep_names), T''' --> Univ_elT) $ free_t))::r_args)
   1.149 -                end
   1.150 -
   1.151 +          in (case (strip_dtyp dt, strip_type T) of
   1.152 +              ((_, DtRec m), (Us, U)) => (j + 1, free_t :: l_args, mk_lim (Us,
   1.153 +                Const (nth_elem (m, all_rep_names), U --> Univ_elT) $
   1.154 +                  app_bnds free_t (length Us)) :: r_args)
   1.155              | _ => (j + 1, free_t::l_args, (Leaf $ mk_inj T free_t)::r_args))
   1.156            end;
   1.157  
   1.158 @@ -321,11 +309,11 @@
   1.159      (* isomorphisms are defined using primrec-combinators:                 *)
   1.160      (* generate appropriate functions for instantiating primrec-combinator *)
   1.161      (*                                                                     *)
   1.162 -    (*   e.g.  dt_Rep_i = list_rec ... (%h t y. In1 ((Leaf h) $ y))        *)
   1.163 +    (*   e.g.  dt_Rep_i = list_rec ... (%h t y. In1 (Scons (Leaf h) y))    *)
   1.164      (*                                                                     *)
   1.165      (* also generate characteristic equations for isomorphisms             *)
   1.166      (*                                                                     *)
   1.167 -    (*   e.g.  dt_Rep_i (cons h t) = In1 ((dt_Rep_j h) $ (dt_Rep_i t))     *)
   1.168 +    (*   e.g.  dt_Rep_i (cons h t) = In1 (Scons (dt_Rep_j h) (dt_Rep_i t)) *)
   1.169      (*---------------------------------------------------------------------*)
   1.170  
   1.171      fun make_iso_def k ks n ((fs, eqns, i), (cname, cargs)) =
   1.172 @@ -337,24 +325,18 @@
   1.173          val constr = Const (cname, argTs ---> T);
   1.174  
   1.175          fun process_arg ks' ((i2, i2', ts, Ts), dt) =
   1.176 -          let val T' = typ_of_dtyp descr' sorts dt
   1.177 -          in (case dt of
   1.178 -              DtRec j => if j mem ks' then
   1.179 -                  (i2 + 1, i2' + 1, ts @ [mk_Free "y" Univ_elT i2'], Ts @ [Univ_elT])
   1.180 +          let
   1.181 +            val T' = typ_of_dtyp descr' sorts dt;
   1.182 +            val (Us, U) = strip_type T'
   1.183 +          in (case strip_dtyp dt of
   1.184 +              (_, DtRec j) => if j mem ks' then
   1.185 +                  (i2 + 1, i2' + 1, ts @ [mk_lim (Us, app_bnds
   1.186 +                     (mk_Free "y" (Us ---> Univ_elT) i2') (length Us))],
   1.187 +                   Ts @ [Us ---> Univ_elT])
   1.188                  else
   1.189 -                  (i2 + 1, i2', ts @ [Const (nth_elem (j, all_rep_names),
   1.190 -                    T' --> Univ_elT) $ mk_Free "x" T' i2], Ts)
   1.191 -            | (DtType ("fun", [_, DtRec j])) =>
   1.192 -                let val ([T''], T''') = strip_type T'
   1.193 -                in if j mem ks' then
   1.194 -                    (i2 + 1, i2' + 1, ts @ [Lim $ mk_fun_inj T''
   1.195 -                      (mk_Free "y" (T'' --> Univ_elT) i2')], Ts @ [T'' --> Univ_elT])
   1.196 -                  else
   1.197 -                    (i2 + 1, i2', ts @ [Lim $ mk_fun_inj T''
   1.198 -                      (Const (o_name, [T''' --> Univ_elT, T', T''] ---> Univ_elT) $
   1.199 -                        Const (nth_elem (j, all_rep_names), T''' --> Univ_elT) $
   1.200 -                          mk_Free "x" T' i2)], Ts)
   1.201 -                end
   1.202 +                  (i2 + 1, i2', ts @ [mk_lim (Us,
   1.203 +                     Const (nth_elem (j, all_rep_names), U --> Univ_elT) $
   1.204 +                       app_bnds (mk_Free "x" T' i2) (length Us))], Ts)
   1.205              | _ => (i2 + 1, i2', ts @ [Leaf $ mk_inj T' (mk_Free "x" T' i2)], Ts))
   1.206            end;
   1.207  
   1.208 @@ -406,18 +388,25 @@
   1.209  
   1.210      fun mk_funs_inv thm =
   1.211        let
   1.212 -        val [_, t] = prems_of Funs_inv;
   1.213 -        val [_ $ (_ $ _ $ R)] = Logic.strip_assums_hyp t;
   1.214 -        val _ $ (_ $ (r $ (a $ _)) $ _) = Logic.strip_assums_concl t;
   1.215 -        val [_ $ (_ $ _ $ R')] = prems_of thm;
   1.216 -        val _ $ (_ $ (r' $ (a' $ _)) $ _) = concl_of thm;
   1.217 -        val inv' = cterm_instantiate (map 
   1.218 -          ((pairself (cterm_of (sign_of_thm thm))) o
   1.219 -           (apsnd (map_term_types (incr_tvar 1))))
   1.220 -             [(R, R'), (r, r'), (a, a')]) Funs_inv
   1.221 -      in
   1.222 -        rule_by_tactic (atac 2) (thm RSN (2, inv'))
   1.223 -      end;
   1.224 +        val {sign, prop, ...} = rep_thm thm;
   1.225 +        val (_ $ (_ $ (Const (_, Type (_, [U, _])) $ _ $ S)) $
   1.226 +          (_ $ (_ $ (r $ (a $ _)) $ _)), _) = Type.freeze_thaw prop;
   1.227 +        val used = add_term_tfree_names (a, []);
   1.228 +
   1.229 +        fun mk_thm i =
   1.230 +          let
   1.231 +            val Ts = map (TFree o rpair HOLogic.typeS)
   1.232 +              (variantlist (replicate i "'t", used));
   1.233 +            val f = Free ("f", Ts ---> U)
   1.234 +          in prove_goalw_cterm [] (cterm_of sign (Logic.mk_implies
   1.235 +            (HOLogic.mk_Trueprop (HOLogic.list_all
   1.236 +               (map (pair "x") Ts, HOLogic.mk_mem (app_bnds f i, S))),
   1.237 +             HOLogic.mk_Trueprop (HOLogic.mk_eq (list_abs (map (pair "x") Ts,
   1.238 +               r $ (a $ app_bnds f i)), f))))) (fn prems =>
   1.239 +                 [cut_facts_tac prems 1, REPEAT (rtac ext 1),
   1.240 +                  REPEAT (etac allE 1), rtac thm 1, atac 1])
   1.241 +          end
   1.242 +      in map (fn r => r RS subst) (thm :: map mk_thm arities) end;
   1.243  
   1.244      (* prove  inj dt_Rep_i  and  dt_Rep_i x : dt_rep_set_i *)
   1.245  
   1.246 @@ -440,8 +429,8 @@
   1.247          val (ind_concl1, ind_concl2) = ListPair.unzip (map mk_ind_concl ds);
   1.248  
   1.249          val rewrites = map mk_meta_eq iso_char_thms;
   1.250 -        val inj_thms' = flat (map (fn r => [r RS injD, r RS inj_o])
   1.251 -          (map snd newT_iso_inj_thms @ inj_thms));
   1.252 +        val inj_thms' = map (fn r => r RS injD)
   1.253 +          (map snd newT_iso_inj_thms @ inj_thms);
   1.254  
   1.255          val inj_thm = prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5)
   1.256            (HOLogic.mk_Trueprop (mk_conj ind_concl1))) (fn _ =>
   1.257 @@ -455,13 +444,15 @@
   1.258                     REPEAT (dresolve_tac [In0_inject, In1_inject] 1),
   1.259                     (eresolve_tac [In0_not_In1 RS notE, In1_not_In0 RS notE] 1)
   1.260                     ORELSE (EVERY
   1.261 -                     [REPEAT (eresolve_tac (Scons_inject :: sum_case_inject ::
   1.262 -                        map make_elim (inj_thms' @
   1.263 -                          [Leaf_inject, Lim_inject, Inl_inject, Inr_inject])) 1),
   1.264 -                      REPEAT ((EVERY [etac allE 1, dtac mp 1, atac 1]) ORELSE
   1.265 -                              (dtac inj_fun_lemma 1 THEN atac 1)),
   1.266 -                      REPEAT (hyp_subst_tac 1),
   1.267 -                      rtac refl 1])])])]);
   1.268 +                     [REPEAT (eresolve_tac (Scons_inject ::
   1.269 +                        map make_elim [Leaf_inject, Inl_inject, Inr_inject]) 1),
   1.270 +                      REPEAT (cong_tac 1), rtac refl 1,
   1.271 +                      REPEAT (atac 1 ORELSE (EVERY
   1.272 +                        [REPEAT (rtac ext 1),
   1.273 +                         REPEAT (eresolve_tac (mp :: allE ::
   1.274 +                           map make_elim (Suml_inject :: Sumr_inject ::
   1.275 +                             Lim_inject :: fun_cong :: inj_thms')) 1),
   1.276 +                         atac 1]))])])])]);
   1.277  
   1.278          val inj_thms'' = map (fn r => r RS datatype_injI)
   1.279                               (split_conj_thm inj_thm);
   1.280 @@ -472,11 +463,9 @@
   1.281  	       (HOLogic.mk_Trueprop (mk_conj ind_concl2)))
   1.282  	      (fn _ =>
   1.283  	       [(indtac induction THEN_ALL_NEW ObjectLogic.atomize_tac) 1,
   1.284 -		rewrite_goals_tac (o_def :: rewrites),
   1.285 -		REPEAT (EVERY
   1.286 -			[resolve_tac rep_intrs 1,
   1.287 -			 REPEAT (FIRST [atac 1, etac spec 1,
   1.288 -				 resolve_tac (FunsI :: elem_thms) 1])])]);
   1.289 +		rewrite_goals_tac rewrites,
   1.290 +		REPEAT ((resolve_tac rep_intrs THEN_ALL_NEW
   1.291 +                  ((REPEAT o etac allE) THEN' ares_tac elem_thms)) 1)]);
   1.292  
   1.293        in (inj_thms'' @ inj_thms, elem_thms @ (split_conj_thm elem_thm))
   1.294        end;
   1.295 @@ -502,18 +491,20 @@
   1.296  
   1.297      (* all the theorems are proved by one single simultaneous induction *)
   1.298  
   1.299 +    val range_eqs = map (fn r => mk_meta_eq (r RS range_ex1_eq))
   1.300 +      iso_inj_thms_unfolded;
   1.301 +
   1.302      val iso_thms = if length descr = 1 then [] else
   1.303        drop (length newTs, split_conj_thm
   1.304          (prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5) iso_t) (fn _ =>
   1.305 -           [indtac rep_induct 1,
   1.306 +           [(indtac rep_induct THEN_ALL_NEW ObjectLogic.atomize_tac) 1,
   1.307              REPEAT (rtac TrueI 1),
   1.308 +            rewrite_goals_tac (mk_meta_eq choice_eq ::
   1.309 +              symmetric (mk_meta_eq expand_fun_eq) :: range_eqs),
   1.310 +            rewrite_goals_tac (map symmetric range_eqs),
   1.311              REPEAT (EVERY
   1.312 -              [rewrite_goals_tac [mk_meta_eq Collect_mem_eq],
   1.313 -               REPEAT (etac Funs_IntE 1),
   1.314 -               REPEAT (eresolve_tac (rangeE ::
   1.315 -                 map (fn r => r RS Funs_rangeE) iso_inj_thms_unfolded) 1),
   1.316 -               REPEAT (eresolve_tac (map (fn (iso, _, _) => iso RS subst) newT_iso_axms @
   1.317 -                 map (fn (iso, _, _) => mk_funs_inv iso RS subst) newT_iso_axms) 1),
   1.318 +              [REPEAT (eresolve_tac ([rangeE, ex1_implies_ex RS exE] @
   1.319 +                 flat (map (mk_funs_inv o #1) newT_iso_axms)) 1),
   1.320                 TRY (hyp_subst_tac 1),
   1.321                 rtac (sym RS range_eqI) 1,
   1.322                 resolve_tac iso_char_thms 1])])));
   1.323 @@ -523,8 +514,7 @@
   1.324        map2 (fn (r_inj, r) => f_myinv_f OF [r_inj, r RS mp])
   1.325          (iso_inj_thms_unfolded, iso_thms);
   1.326  
   1.327 -    val Abs_inverse_thms = map (fn r => r RS subst) (Abs_inverse_thms' @
   1.328 -      map mk_funs_inv Abs_inverse_thms');
   1.329 +    val Abs_inverse_thms = flat (map mk_funs_inv Abs_inverse_thms');
   1.330  
   1.331      (******************* freeness theorems for constructors *******************)
   1.332  
   1.333 @@ -541,7 +531,7 @@
   1.334           rewrite_goals_tac rewrites,
   1.335           rtac refl 1,
   1.336           resolve_tac rep_intrs 2,
   1.337 -         REPEAT (resolve_tac (FunsI :: iso_elem_thms) 1)])
   1.338 +         REPEAT (resolve_tac iso_elem_thms 1)])
   1.339        end;
   1.340  
   1.341      (*--------------------------------------------------------------*)
   1.342 @@ -575,17 +565,19 @@
   1.343      (* prove injectivity of constructors *)
   1.344  
   1.345      fun prove_constr_inj_thm rep_thms t =
   1.346 -      let val inj_thms = Scons_inject::sum_case_inject::(map make_elim
   1.347 +      let val inj_thms = Scons_inject :: (map make_elim
   1.348          ((map (fn r => r RS injD) iso_inj_thms) @
   1.349 -          [In0_inject, In1_inject, Leaf_inject, Inl_inject, Inr_inject, Lim_inject]))
   1.350 +          [In0_inject, In1_inject, Leaf_inject, Inl_inject, Inr_inject,
   1.351 +           Lim_inject, Suml_inject, Sumr_inject]))
   1.352        in prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5) t) (fn _ =>
   1.353          [rtac iffI 1,
   1.354           REPEAT (etac conjE 2), hyp_subst_tac 2, rtac refl 2,
   1.355           dresolve_tac rep_congs 1, dtac box_equals 1,
   1.356 -         REPEAT (resolve_tac rep_thms 1), rewtac o_def,
   1.357 +         REPEAT (resolve_tac rep_thms 1),
   1.358           REPEAT (eresolve_tac inj_thms 1),
   1.359 -         REPEAT (ares_tac [conjI] 1 ORELSE (EVERY [rtac ext 1, dtac fun_cong 1,
   1.360 -                  eresolve_tac inj_thms 1, atac 1]))])
   1.361 +         REPEAT (ares_tac [conjI] 1 ORELSE (EVERY [REPEAT (rtac ext 1),
   1.362 +           REPEAT (eresolve_tac (make_elim fun_cong :: inj_thms) 1),
   1.363 +           atac 1]))])
   1.364        end;
   1.365  
   1.366      val constr_inject = map (fn (ts, thms) => map (prove_constr_inj_thm thms) ts)
   1.367 @@ -641,12 +633,12 @@
   1.368  
   1.369      val dt_induct = prove_goalw_cterm [] (cert
   1.370        (DatatypeProp.make_ind descr sorts)) (fn prems =>
   1.371 -        [rtac indrule_lemma' 1, indtac rep_induct 1,
   1.372 +        [rtac indrule_lemma' 1,
   1.373 +         (indtac rep_induct THEN_ALL_NEW ObjectLogic.atomize_tac) 1,
   1.374           EVERY (map (fn (prem, r) => (EVERY
   1.375 -           [REPEAT (eresolve_tac (Funs_IntE::Abs_inverse_thms) 1),
   1.376 +           [REPEAT (eresolve_tac Abs_inverse_thms 1),
   1.377              simp_tac (HOL_basic_ss addsimps ((symmetric r)::Rep_inverse_thms')) 1,
   1.378 -            DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE (EVERY [rewtac o_def,
   1.379 -              dtac FunsD 1, etac CollectD 1]))]))
   1.380 +            DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE etac allE 1)]))
   1.381                  (prems ~~ (constr_defs @ (map mk_meta_eq iso_char_thms))))]);
   1.382  
   1.383      val (thy7, [dt_induct']) = thy6 |>