src/HOL/Tools/Datatype/datatype_abs_proofs.ML
changeset 31775 2b04504fcb69
parent 31737 b3f63611784e
child 31902 862ae16a799d
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Tue Jun 23 12:09:30 2009 +0200
     1.3 @@ -0,0 +1,447 @@
     1.4 +(*  Title:      HOL/Tools/datatype_abs_proofs.ML
     1.5 +    Author:     Stefan Berghofer, TU Muenchen
     1.6 +
     1.7 +Proofs and defintions independent of concrete representation
     1.8 +of datatypes  (i.e. requiring only abstract properties such as
     1.9 +injectivity / distinctness of constructors and induction)
    1.10 +
    1.11 + - case distinction (exhaustion) theorems
    1.12 + - characteristic equations for primrec combinators
    1.13 + - characteristic equations for case combinators
    1.14 + - equations for splitting "P (case ...)" expressions
    1.15 + - "nchotomy" and "case_cong" theorems for TFL
    1.16 +*)
    1.17 +
    1.18 +signature DATATYPE_ABS_PROOFS =
    1.19 +sig
    1.20 +  include DATATYPE_COMMON
    1.21 +  val prove_casedist_thms : config -> string list ->
    1.22 +    descr list -> (string * sort) list -> thm ->
    1.23 +    attribute list -> theory -> thm list * theory
    1.24 +  val prove_primrec_thms : config -> string list ->
    1.25 +    descr list -> (string * sort) list ->
    1.26 +      info Symtab.table -> thm list list -> thm list list ->
    1.27 +        simpset -> thm -> theory -> (string list * thm list) * theory
    1.28 +  val prove_case_thms : config -> string list ->
    1.29 +    descr list -> (string * sort) list ->
    1.30 +      string list -> thm list -> theory -> (thm list list * string list) * theory
    1.31 +  val prove_split_thms : config -> string list ->
    1.32 +    descr list -> (string * sort) list ->
    1.33 +      thm list list -> thm list list -> thm list -> thm list list -> theory ->
    1.34 +        (thm * thm) list * theory
    1.35 +  val prove_nchotomys : config -> string list -> descr list ->
    1.36 +    (string * sort) list -> thm list -> theory -> thm list * theory
    1.37 +  val prove_weak_case_congs : string list -> descr list ->
    1.38 +    (string * sort) list -> theory -> thm list * theory
    1.39 +  val prove_case_congs : string list ->
    1.40 +    descr list -> (string * sort) list ->
    1.41 +      thm list -> thm list list -> theory -> thm list * theory
    1.42 +end;
    1.43 +
    1.44 +structure DatatypeAbsProofs: DATATYPE_ABS_PROOFS =
    1.45 +struct
    1.46 +
    1.47 +open DatatypeAux;
    1.48 +
    1.49 +(************************ case distinction theorems ***************************)
    1.50 +
    1.51 +fun prove_casedist_thms (config : config) new_type_names descr sorts induct case_names_exhausts thy =
    1.52 +  let
    1.53 +    val _ = message config "Proving case distinction theorems ...";
    1.54 +
    1.55 +    val descr' = List.concat descr;
    1.56 +    val recTs = get_rec_types descr' sorts;
    1.57 +    val newTs = Library.take (length (hd descr), recTs);
    1.58 +
    1.59 +    val {maxidx, ...} = rep_thm induct;
    1.60 +    val induct_Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct)));
    1.61 +
    1.62 +    fun prove_casedist_thm ((i, t), T) =
    1.63 +      let
    1.64 +        val dummyPs = map (fn (Var (_, Type (_, [T', T'']))) =>
    1.65 +          Abs ("z", T', Const ("True", T''))) induct_Ps;
    1.66 +        val P = Abs ("z", T, HOLogic.imp $ HOLogic.mk_eq (Var (("a", maxidx+1), T), Bound 0) $
    1.67 +          Var (("P", 0), HOLogic.boolT))
    1.68 +        val insts = Library.take (i, dummyPs) @ (P::(Library.drop (i + 1, dummyPs)));
    1.69 +        val cert = cterm_of thy;
    1.70 +        val insts' = (map cert induct_Ps) ~~ (map cert insts);
    1.71 +        val induct' = refl RS ((List.nth
    1.72 +          (split_conj_thm (cterm_instantiate insts' induct), i)) RSN (2, rev_mp))
    1.73 +
    1.74 +      in
    1.75 +        SkipProof.prove_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
    1.76 +          (fn {prems, ...} => EVERY
    1.77 +            [rtac induct' 1,
    1.78 +             REPEAT (rtac TrueI 1),
    1.79 +             REPEAT ((rtac impI 1) THEN (eresolve_tac prems 1)),
    1.80 +             REPEAT (rtac TrueI 1)])
    1.81 +      end;
    1.82 +
    1.83 +    val casedist_thms = map prove_casedist_thm ((0 upto (length newTs - 1)) ~~
    1.84 +      (DatatypeProp.make_casedists descr sorts) ~~ newTs)
    1.85 +  in
    1.86 +    thy
    1.87 +    |> store_thms_atts "exhaust" new_type_names (map single case_names_exhausts) casedist_thms
    1.88 +  end;
    1.89 +
    1.90 +
    1.91 +(*************************** primrec combinators ******************************)
    1.92 +
    1.93 +fun prove_primrec_thms (config : config) new_type_names descr sorts
    1.94 +    (dt_info : info Symtab.table) constr_inject dist_rewrites dist_ss induct thy =
    1.95 +  let
    1.96 +    val _ = message config "Constructing primrec combinators ...";
    1.97 +
    1.98 +    val big_name = space_implode "_" new_type_names;
    1.99 +    val thy0 = add_path (#flat_names config) big_name thy;
   1.100 +
   1.101 +    val descr' = List.concat descr;
   1.102 +    val recTs = get_rec_types descr' sorts;
   1.103 +    val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
   1.104 +    val newTs = Library.take (length (hd descr), recTs);
   1.105 +
   1.106 +    val induct_Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct)));
   1.107 +
   1.108 +    val big_rec_name' = big_name ^ "_rec_set";
   1.109 +    val rec_set_names' =
   1.110 +      if length descr' = 1 then [big_rec_name'] else
   1.111 +        map ((curry (op ^) (big_rec_name' ^ "_")) o string_of_int)
   1.112 +          (1 upto (length descr'));
   1.113 +    val rec_set_names = map (Sign.full_bname thy0) rec_set_names';
   1.114 +
   1.115 +    val (rec_result_Ts, reccomb_fn_Ts) = DatatypeProp.make_primrec_Ts descr sorts used;
   1.116 +
   1.117 +    val rec_set_Ts = map (fn (T1, T2) =>
   1.118 +      reccomb_fn_Ts @ [T1, T2] ---> HOLogic.boolT) (recTs ~~ rec_result_Ts);
   1.119 +
   1.120 +    val rec_fns = map (uncurry (mk_Free "f"))
   1.121 +      (reccomb_fn_Ts ~~ (1 upto (length reccomb_fn_Ts)));
   1.122 +    val rec_sets' = map (fn c => list_comb (Free c, rec_fns))
   1.123 +      (rec_set_names' ~~ rec_set_Ts);
   1.124 +    val rec_sets = map (fn c => list_comb (Const c, rec_fns))
   1.125 +      (rec_set_names ~~ rec_set_Ts);
   1.126 +
   1.127 +    (* introduction rules for graph of primrec function *)
   1.128 +
   1.129 +    fun make_rec_intr T rec_set ((rec_intr_ts, l), (cname, cargs)) =
   1.130 +      let
   1.131 +        fun mk_prem ((dt, U), (j, k, prems, t1s, t2s)) =
   1.132 +          let val free1 = mk_Free "x" U j
   1.133 +          in (case (strip_dtyp dt, strip_type U) of
   1.134 +             ((_, DtRec m), (Us, _)) =>
   1.135 +               let
   1.136 +                 val free2 = mk_Free "y" (Us ---> List.nth (rec_result_Ts, m)) k;
   1.137 +                 val i = length Us
   1.138 +               in (j + 1, k + 1, HOLogic.mk_Trueprop (HOLogic.list_all
   1.139 +                     (map (pair "x") Us, List.nth (rec_sets', m) $
   1.140 +                       app_bnds free1 i $ app_bnds free2 i)) :: prems,
   1.141 +                   free1::t1s, free2::t2s)
   1.142 +               end
   1.143 +           | _ => (j + 1, k, prems, free1::t1s, t2s))
   1.144 +          end;
   1.145 +
   1.146 +        val Ts = map (typ_of_dtyp descr' sorts) cargs;
   1.147 +        val (_, _, prems, t1s, t2s) = List.foldr mk_prem (1, 1, [], [], []) (cargs ~~ Ts)
   1.148 +
   1.149 +      in (rec_intr_ts @ [Logic.list_implies (prems, HOLogic.mk_Trueprop
   1.150 +        (rec_set $ list_comb (Const (cname, Ts ---> T), t1s) $
   1.151 +          list_comb (List.nth (rec_fns, l), t1s @ t2s)))], l + 1)
   1.152 +      end;
   1.153 +
   1.154 +    val (rec_intr_ts, _) = Library.foldl (fn (x, ((d, T), set_name)) =>
   1.155 +      Library.foldl (make_rec_intr T set_name) (x, #3 (snd d)))
   1.156 +        (([], 0), descr' ~~ recTs ~~ rec_sets');
   1.157 +
   1.158 +    val ({intrs = rec_intrs, elims = rec_elims, ...}, thy1) =
   1.159 +        Inductive.add_inductive_global (serial_string ())
   1.160 +          {quiet_mode = #quiet config, verbose = false, kind = Thm.internalK,
   1.161 +            alt_name = Binding.name big_rec_name', coind = false, no_elim = false, no_ind = true,
   1.162 +            skip_mono = true, fork_mono = false}
   1.163 +          (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
   1.164 +          (map dest_Free rec_fns)
   1.165 +          (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) [] thy0;
   1.166 +
   1.167 +    (* prove uniqueness and termination of primrec combinators *)
   1.168 +
   1.169 +    val _ = message config "Proving termination and uniqueness of primrec functions ...";
   1.170 +
   1.171 +    fun mk_unique_tac ((tac, intrs), ((((i, (tname, _, constrs)), elim), T), T')) =
   1.172 +      let
   1.173 +        val distinct_tac =
   1.174 +          (if i < length newTs then
   1.175 +             full_simp_tac (HOL_ss addsimps (List.nth (dist_rewrites, i))) 1
   1.176 +           else full_simp_tac dist_ss 1);
   1.177 +
   1.178 +        val inject = map (fn r => r RS iffD1)
   1.179 +          (if i < length newTs then List.nth (constr_inject, i)
   1.180 +            else #inject (the (Symtab.lookup dt_info tname)));
   1.181 +
   1.182 +        fun mk_unique_constr_tac n ((tac, intr::intrs, j), (cname, cargs)) =
   1.183 +          let
   1.184 +            val k = length (List.filter is_rec_type cargs)
   1.185 +
   1.186 +          in (EVERY [DETERM tac,
   1.187 +                REPEAT (etac ex1E 1), rtac ex1I 1,
   1.188 +                DEPTH_SOLVE_1 (ares_tac [intr] 1),
   1.189 +                REPEAT_DETERM_N k (etac thin_rl 1 THEN rotate_tac 1 1),
   1.190 +                etac elim 1,
   1.191 +                REPEAT_DETERM_N j distinct_tac,
   1.192 +                TRY (dresolve_tac inject 1),
   1.193 +                REPEAT (etac conjE 1), hyp_subst_tac 1,
   1.194 +                REPEAT (EVERY [etac allE 1, dtac mp 1, atac 1]),
   1.195 +                TRY (hyp_subst_tac 1),
   1.196 +                rtac refl 1,
   1.197 +                REPEAT_DETERM_N (n - j - 1) distinct_tac],
   1.198 +              intrs, j + 1)
   1.199 +          end;
   1.200 +
   1.201 +        val (tac', intrs', _) = Library.foldl (mk_unique_constr_tac (length constrs))
   1.202 +          ((tac, intrs, 0), constrs);
   1.203 +
   1.204 +      in (tac', intrs') end;
   1.205 +
   1.206 +    val rec_unique_thms =
   1.207 +      let
   1.208 +        val rec_unique_ts = map (fn (((set_t, T1), T2), i) =>
   1.209 +          Const ("Ex1", (T2 --> HOLogic.boolT) --> HOLogic.boolT) $
   1.210 +            absfree ("y", T2, set_t $ mk_Free "x" T1 i $ Free ("y", T2)))
   1.211 +              (rec_sets ~~ recTs ~~ rec_result_Ts ~~ (1 upto length recTs));
   1.212 +        val cert = cterm_of thy1
   1.213 +        val insts = map (fn ((i, T), t) => absfree ("x" ^ (string_of_int i), T, t))
   1.214 +          ((1 upto length recTs) ~~ recTs ~~ rec_unique_ts);
   1.215 +        val induct' = cterm_instantiate ((map cert induct_Ps) ~~
   1.216 +          (map cert insts)) induct;
   1.217 +        val (tac, _) = Library.foldl mk_unique_tac
   1.218 +          (((rtac induct' THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1
   1.219 +              THEN rewrite_goals_tac [mk_meta_eq choice_eq], rec_intrs),
   1.220 +            descr' ~~ rec_elims ~~ recTs ~~ rec_result_Ts);
   1.221 +
   1.222 +      in split_conj_thm (SkipProof.prove_global thy1 [] []
   1.223 +        (HOLogic.mk_Trueprop (mk_conj rec_unique_ts)) (K tac))
   1.224 +      end;
   1.225 +
   1.226 +    val rec_total_thms = map (fn r => r RS theI') rec_unique_thms;
   1.227 +
   1.228 +    (* define primrec combinators *)
   1.229 +
   1.230 +    val big_reccomb_name = (space_implode "_" new_type_names) ^ "_rec";
   1.231 +    val reccomb_names = map (Sign.full_bname thy1)
   1.232 +      (if length descr' = 1 then [big_reccomb_name] else
   1.233 +        (map ((curry (op ^) (big_reccomb_name ^ "_")) o string_of_int)
   1.234 +          (1 upto (length descr'))));
   1.235 +    val reccombs = map (fn ((name, T), T') => list_comb
   1.236 +      (Const (name, reccomb_fn_Ts @ [T] ---> T'), rec_fns))
   1.237 +        (reccomb_names ~~ recTs ~~ rec_result_Ts);
   1.238 +
   1.239 +    val (reccomb_defs, thy2) =
   1.240 +      thy1
   1.241 +      |> Sign.add_consts_i (map (fn ((name, T), T') =>
   1.242 +          (Binding.name (Long_Name.base_name name), reccomb_fn_Ts @ [T] ---> T', NoSyn))
   1.243 +          (reccomb_names ~~ recTs ~~ rec_result_Ts))
   1.244 +      |> (PureThy.add_defs false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') =>
   1.245 +          (Binding.name (Long_Name.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T,
   1.246 +           Const ("The", (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
   1.247 +             set $ Free ("x", T) $ Free ("y", T'))))))
   1.248 +               (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts))
   1.249 +      ||> parent_path (#flat_names config) 
   1.250 +      ||> Theory.checkpoint;
   1.251 +
   1.252 +
   1.253 +    (* prove characteristic equations for primrec combinators *)
   1.254 +
   1.255 +    val _ = message config "Proving characteristic theorems for primrec combinators ..."
   1.256 +
   1.257 +    val rec_thms = map (fn t => SkipProof.prove_global thy2 [] [] t
   1.258 +      (fn _ => EVERY
   1.259 +        [rewrite_goals_tac reccomb_defs,
   1.260 +         rtac the1_equality 1,
   1.261 +         resolve_tac rec_unique_thms 1,
   1.262 +         resolve_tac rec_intrs 1,
   1.263 +         REPEAT (rtac allI 1 ORELSE resolve_tac rec_total_thms 1)]))
   1.264 +           (DatatypeProp.make_primrecs new_type_names descr sorts thy2)
   1.265 +
   1.266 +  in
   1.267 +    thy2
   1.268 +    |> Sign.add_path (space_implode "_" new_type_names)
   1.269 +    |> PureThy.add_thmss [((Binding.name "recs", rec_thms),
   1.270 +         [Nitpick_Const_Simp_Thms.add])]
   1.271 +    ||> Sign.parent_path
   1.272 +    ||> Theory.checkpoint
   1.273 +    |-> (fn thms => pair (reccomb_names, Library.flat thms))
   1.274 +  end;
   1.275 +
   1.276 +
   1.277 +(***************************** case combinators *******************************)
   1.278 +
   1.279 +fun prove_case_thms (config : config) new_type_names descr sorts reccomb_names primrec_thms thy =
   1.280 +  let
   1.281 +    val _ = message config "Proving characteristic theorems for case combinators ...";
   1.282 +
   1.283 +    val thy1 = add_path (#flat_names config) (space_implode "_" new_type_names) thy;
   1.284 +
   1.285 +    val descr' = List.concat descr;
   1.286 +    val recTs = get_rec_types descr' sorts;
   1.287 +    val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
   1.288 +    val newTs = Library.take (length (hd descr), recTs);
   1.289 +    val T' = TFree (Name.variant used "'t", HOLogic.typeS);
   1.290 +
   1.291 +    fun mk_dummyT dt = binder_types (typ_of_dtyp descr' sorts dt) ---> T';
   1.292 +
   1.293 +    val case_dummy_fns = map (fn (_, (_, _, constrs)) => map (fn (_, cargs) =>
   1.294 +      let
   1.295 +        val Ts = map (typ_of_dtyp descr' sorts) cargs;
   1.296 +        val Ts' = map mk_dummyT (List.filter is_rec_type cargs)
   1.297 +      in Const (@{const_name undefined}, Ts @ Ts' ---> T')
   1.298 +      end) constrs) descr';
   1.299 +
   1.300 +    val case_names = map (fn s => Sign.full_bname thy1 (s ^ "_case")) new_type_names;
   1.301 +
   1.302 +    (* define case combinators via primrec combinators *)
   1.303 +
   1.304 +    val (case_defs, thy2) = Library.foldl (fn ((defs, thy),
   1.305 +      ((((i, (_, _, constrs)), T), name), recname)) =>
   1.306 +        let
   1.307 +          val (fns1, fns2) = ListPair.unzip (map (fn ((_, cargs), j) =>
   1.308 +            let
   1.309 +              val Ts = map (typ_of_dtyp descr' sorts) cargs;
   1.310 +              val Ts' = Ts @ map mk_dummyT (List.filter is_rec_type cargs);
   1.311 +              val frees' = map (uncurry (mk_Free "x")) (Ts' ~~ (1 upto length Ts'));
   1.312 +              val frees = Library.take (length cargs, frees');
   1.313 +              val free = mk_Free "f" (Ts ---> T') j
   1.314 +            in
   1.315 +             (free, list_abs_free (map dest_Free frees',
   1.316 +               list_comb (free, frees)))
   1.317 +            end) (constrs ~~ (1 upto length constrs)));
   1.318 +
   1.319 +          val caseT = (map (snd o dest_Free) fns1) @ [T] ---> T';
   1.320 +          val fns = (List.concat (Library.take (i, case_dummy_fns))) @
   1.321 +            fns2 @ (List.concat (Library.drop (i + 1, case_dummy_fns)));
   1.322 +          val reccomb = Const (recname, (map fastype_of fns) @ [T] ---> T');
   1.323 +          val decl = ((Binding.name (Long_Name.base_name name), caseT), NoSyn);
   1.324 +          val def = (Binding.name (Long_Name.base_name name ^ "_def"),
   1.325 +            Logic.mk_equals (list_comb (Const (name, caseT), fns1),
   1.326 +              list_comb (reccomb, (List.concat (Library.take (i, case_dummy_fns))) @
   1.327 +                fns2 @ (List.concat (Library.drop (i + 1, case_dummy_fns))) )));
   1.328 +          val ([def_thm], thy') =
   1.329 +            thy
   1.330 +            |> Sign.declare_const [] decl |> snd
   1.331 +            |> (PureThy.add_defs false o map Thm.no_attributes) [def];
   1.332 +
   1.333 +        in (defs @ [def_thm], thy')
   1.334 +        end) (([], thy1), (hd descr) ~~ newTs ~~ case_names ~~
   1.335 +          (Library.take (length newTs, reccomb_names)))
   1.336 +      ||> Theory.checkpoint;
   1.337 +
   1.338 +    val case_thms = map (map (fn t => SkipProof.prove_global thy2 [] [] t
   1.339 +      (fn _ => EVERY [rewrite_goals_tac (case_defs @ map mk_meta_eq primrec_thms), rtac refl 1])))
   1.340 +          (DatatypeProp.make_cases new_type_names descr sorts thy2)
   1.341 +  in
   1.342 +    thy2
   1.343 +    |> Context.the_theory o fold (fold Nitpick_Const_Simp_Thms.add_thm) case_thms
   1.344 +       o Context.Theory
   1.345 +    |> parent_path (#flat_names config)
   1.346 +    |> store_thmss "cases" new_type_names case_thms
   1.347 +    |-> (fn thmss => pair (thmss, case_names))
   1.348 +  end;
   1.349 +
   1.350 +
   1.351 +(******************************* case splitting *******************************)
   1.352 +
   1.353 +fun prove_split_thms (config : config) new_type_names descr sorts constr_inject dist_rewrites
   1.354 +    casedist_thms case_thms thy =
   1.355 +  let
   1.356 +    val _ = message config "Proving equations for case splitting ...";
   1.357 +
   1.358 +    val descr' = flat descr;
   1.359 +    val recTs = get_rec_types descr' sorts;
   1.360 +    val newTs = Library.take (length (hd descr), recTs);
   1.361 +
   1.362 +    fun prove_split_thms ((((((t1, t2), inject), dist_rewrites'),
   1.363 +        exhaustion), case_thms'), T) =
   1.364 +      let
   1.365 +        val cert = cterm_of thy;
   1.366 +        val _ $ (_ $ lhs $ _) = hd (Logic.strip_assums_hyp (hd (prems_of exhaustion)));
   1.367 +        val exhaustion' = cterm_instantiate
   1.368 +          [(cert lhs, cert (Free ("x", T)))] exhaustion;
   1.369 +        val tacf = K (EVERY [rtac exhaustion' 1, ALLGOALS (asm_simp_tac
   1.370 +          (HOL_ss addsimps (dist_rewrites' @ inject @ case_thms')))])
   1.371 +      in
   1.372 +        (SkipProof.prove_global thy [] [] t1 tacf,
   1.373 +         SkipProof.prove_global thy [] [] t2 tacf)
   1.374 +      end;
   1.375 +
   1.376 +    val split_thm_pairs = map prove_split_thms
   1.377 +      ((DatatypeProp.make_splits new_type_names descr sorts thy) ~~ constr_inject ~~
   1.378 +        dist_rewrites ~~ casedist_thms ~~ case_thms ~~ newTs);
   1.379 +
   1.380 +    val (split_thms, split_asm_thms) = ListPair.unzip split_thm_pairs
   1.381 +
   1.382 +  in
   1.383 +    thy
   1.384 +    |> store_thms "split" new_type_names split_thms
   1.385 +    ||>> store_thms "split_asm" new_type_names split_asm_thms
   1.386 +    |-> (fn (thms1, thms2) => pair (thms1 ~~ thms2))
   1.387 +  end;
   1.388 +
   1.389 +fun prove_weak_case_congs new_type_names descr sorts thy =
   1.390 +  let
   1.391 +    fun prove_weak_case_cong t =
   1.392 +       SkipProof.prove_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
   1.393 +         (fn {prems, ...} => EVERY [rtac ((hd prems) RS arg_cong) 1])
   1.394 +
   1.395 +    val weak_case_congs = map prove_weak_case_cong (DatatypeProp.make_weak_case_congs
   1.396 +      new_type_names descr sorts thy)
   1.397 +
   1.398 +  in thy |> store_thms "weak_case_cong" new_type_names weak_case_congs end;
   1.399 +
   1.400 +(************************* additional theorems for TFL ************************)
   1.401 +
   1.402 +fun prove_nchotomys (config : config) new_type_names descr sorts casedist_thms thy =
   1.403 +  let
   1.404 +    val _ = message config "Proving additional theorems for TFL ...";
   1.405 +
   1.406 +    fun prove_nchotomy (t, exhaustion) =
   1.407 +      let
   1.408 +        (* For goal i, select the correct disjunct to attack, then prove it *)
   1.409 +        fun tac i 0 = EVERY [TRY (rtac disjI1 i),
   1.410 +              hyp_subst_tac i, REPEAT (rtac exI i), rtac refl i]
   1.411 +          | tac i n = rtac disjI2 i THEN tac i (n - 1)
   1.412 +      in 
   1.413 +        SkipProof.prove_global thy [] [] t (fn _ =>
   1.414 +          EVERY [rtac allI 1,
   1.415 +           exh_tac (K exhaustion) 1,
   1.416 +           ALLGOALS (fn i => tac i (i-1))])
   1.417 +      end;
   1.418 +
   1.419 +    val nchotomys =
   1.420 +      map prove_nchotomy (DatatypeProp.make_nchotomys descr sorts ~~ casedist_thms)
   1.421 +
   1.422 +  in thy |> store_thms "nchotomy" new_type_names nchotomys end;
   1.423 +
   1.424 +fun prove_case_congs new_type_names descr sorts nchotomys case_thms thy =
   1.425 +  let
   1.426 +    fun prove_case_cong ((t, nchotomy), case_rewrites) =
   1.427 +      let
   1.428 +        val (Const ("==>", _) $ tm $ _) = t;
   1.429 +        val (Const ("Trueprop", _) $ (Const ("op =", _) $ _ $ Ma)) = tm;
   1.430 +        val cert = cterm_of thy;
   1.431 +        val nchotomy' = nchotomy RS spec;
   1.432 +        val [v] = Term.add_vars (concl_of nchotomy') [];
   1.433 +        val nchotomy'' = cterm_instantiate [(cert (Var v), cert Ma)] nchotomy'
   1.434 +      in
   1.435 +        SkipProof.prove_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
   1.436 +          (fn {prems, ...} => 
   1.437 +            let val simplify = asm_simp_tac (HOL_ss addsimps (prems @ case_rewrites))
   1.438 +            in EVERY [simp_tac (HOL_ss addsimps [hd prems]) 1,
   1.439 +                cut_facts_tac [nchotomy''] 1,
   1.440 +                REPEAT (etac disjE 1 THEN REPEAT (etac exE 1) THEN simplify 1),
   1.441 +                REPEAT (etac exE 1) THEN simplify 1 (* Get last disjunct *)]
   1.442 +            end)
   1.443 +      end;
   1.444 +
   1.445 +    val case_congs = map prove_case_cong (DatatypeProp.make_case_congs
   1.446 +      new_type_names descr sorts thy ~~ nchotomys ~~ case_thms)
   1.447 +
   1.448 +  in thy |> store_thms "case_cong" new_type_names case_congs end;
   1.449 +
   1.450 +end;