clarified modules that contribute to datatype package;
authorwenzelm
Sat Dec 17 12:42:10 2011 +0100 (2011-12-17)
changeset 459074b41967bd77e
parent 45906 0aaeb5520f2f
child 45908 143d2514347f
clarified modules that contribute to datatype package;
src/HOL/Inductive.thy
src/HOL/IsaMakefile
src/HOL/Tools/Datatype/datatype_abs_proofs.ML
src/HOL/Tools/Datatype/rep_datatype.ML
     1.1 --- a/src/HOL/Inductive.thy	Sat Dec 17 12:10:37 2011 +0100
     1.2 +++ b/src/HOL/Inductive.thy	Sat Dec 17 12:42:10 2011 +0100
     1.3 @@ -11,7 +11,6 @@
     1.4    ("Tools/inductive.ML")
     1.5    ("Tools/Datatype/datatype_aux.ML")
     1.6    ("Tools/Datatype/datatype_prop.ML")
     1.7 -  ("Tools/Datatype/datatype_abs_proofs.ML")
     1.8    ("Tools/Datatype/datatype_data.ML")
     1.9    ("Tools/Datatype/datatype_case.ML")
    1.10    ("Tools/Datatype/rep_datatype.ML")
    1.11 @@ -277,7 +276,6 @@
    1.12  
    1.13  use "Tools/Datatype/datatype_aux.ML"
    1.14  use "Tools/Datatype/datatype_prop.ML"
    1.15 -use "Tools/Datatype/datatype_abs_proofs.ML"
    1.16  use "Tools/Datatype/datatype_data.ML" setup Datatype_Data.setup
    1.17  use "Tools/Datatype/datatype_case.ML" setup Datatype_Case.setup
    1.18  use "Tools/Datatype/rep_datatype.ML"
     2.1 --- a/src/HOL/IsaMakefile	Sat Dec 17 12:10:37 2011 +0100
     2.2 +++ b/src/HOL/IsaMakefile	Sat Dec 17 12:42:10 2011 +0100
     2.3 @@ -211,7 +211,6 @@
     2.4    Tools/ATP/atp_translate.ML \
     2.5    Tools/ATP/atp_util.ML \
     2.6    Tools/Datatype/datatype.ML \
     2.7 -  Tools/Datatype/datatype_abs_proofs.ML \
     2.8    Tools/Datatype/datatype_aux.ML \
     2.9    Tools/Datatype/datatype_case.ML \
    2.10    Tools/Datatype/datatype_codegen.ML \
     3.1 --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Sat Dec 17 12:10:37 2011 +0100
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,457 +0,0 @@
     3.4 -(*  Title:      HOL/Tools/Datatype/datatype_abs_proofs.ML
     3.5 -    Author:     Stefan Berghofer, TU Muenchen
     3.6 -
     3.7 -Datatype package: proofs and definitions independent of concrete
     3.8 -representation of datatypes  (i.e. requiring only abstract
     3.9 -properties: injectivity / distinctness of constructors and induction).
    3.10 -*)
    3.11 -
    3.12 -signature DATATYPE_ABS_PROOFS =
    3.13 -sig
    3.14 -  type config = Datatype_Aux.config
    3.15 -  type descr = Datatype_Aux.descr
    3.16 -  val prove_casedist_thms : config -> string list -> descr list -> thm ->
    3.17 -    attribute list -> theory -> thm list * theory
    3.18 -  val prove_primrec_thms : config -> string list -> descr list ->
    3.19 -    (string -> thm list) -> thm list list -> thm list list * thm list list ->
    3.20 -      thm -> theory -> (string list * thm list) * theory
    3.21 -  val prove_case_thms : config -> string list -> descr list ->
    3.22 -    string list -> thm list -> theory -> (thm list list * string list) * theory
    3.23 -  val prove_split_thms : config -> string list -> string list -> descr list ->
    3.24 -    thm list list -> thm list list -> thm list -> thm list list -> theory ->
    3.25 -    (thm * thm) list * theory
    3.26 -  val prove_nchotomys : config -> string list -> descr list ->
    3.27 -    thm list -> theory -> thm list * theory
    3.28 -  val prove_weak_case_congs : string list -> string list -> descr list -> theory -> thm list * theory
    3.29 -  val prove_case_congs : string list -> string list -> descr list ->
    3.30 -    thm list -> thm list list -> theory -> thm list * theory
    3.31 -end;
    3.32 -
    3.33 -structure Datatype_Abs_Proofs: DATATYPE_ABS_PROOFS =
    3.34 -struct
    3.35 -
    3.36 -type config = Datatype_Aux.config;
    3.37 -type descr = Datatype_Aux.descr;
    3.38 -
    3.39 -
    3.40 -(************************ case distinction theorems ***************************)
    3.41 -
    3.42 -fun prove_casedist_thms (config : config) new_type_names descr induct case_names_exhausts thy =
    3.43 -  let
    3.44 -    val _ = Datatype_Aux.message config "Proving case distinction theorems ...";
    3.45 -
    3.46 -    val descr' = flat descr;
    3.47 -    val recTs = Datatype_Aux.get_rec_types descr';
    3.48 -    val newTs = take (length (hd descr)) recTs;
    3.49 -
    3.50 -    val maxidx = Thm.maxidx_of induct;
    3.51 -    val induct_Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct)));
    3.52 -
    3.53 -    fun prove_casedist_thm (i, (T, t)) =
    3.54 -      let
    3.55 -        val dummyPs = map (fn (Var (_, Type (_, [T', T'']))) =>
    3.56 -          Abs ("z", T', Const (@{const_name True}, T''))) induct_Ps;
    3.57 -        val P =
    3.58 -          Abs ("z", T, HOLogic.imp $ HOLogic.mk_eq (Var (("a", maxidx + 1), T), Bound 0) $
    3.59 -            Var (("P", 0), HOLogic.boolT));
    3.60 -        val insts = take i dummyPs @ (P :: drop (i + 1) dummyPs);
    3.61 -        val cert = cterm_of thy;
    3.62 -        val insts' = map cert induct_Ps ~~ map cert insts;
    3.63 -        val induct' =
    3.64 -          refl RS
    3.65 -            (nth (Datatype_Aux.split_conj_thm (cterm_instantiate insts' induct)) i RSN (2, rev_mp));
    3.66 -      in
    3.67 -        Skip_Proof.prove_global thy []
    3.68 -          (Logic.strip_imp_prems t)
    3.69 -          (Logic.strip_imp_concl t)
    3.70 -          (fn {prems, ...} =>
    3.71 -            EVERY
    3.72 -              [rtac induct' 1,
    3.73 -               REPEAT (rtac TrueI 1),
    3.74 -               REPEAT ((rtac impI 1) THEN (eresolve_tac prems 1)),
    3.75 -               REPEAT (rtac TrueI 1)])
    3.76 -      end;
    3.77 -
    3.78 -    val casedist_thms =
    3.79 -      map_index prove_casedist_thm (newTs ~~ Datatype_Prop.make_casedists descr);
    3.80 -  in
    3.81 -    thy
    3.82 -    |> Datatype_Aux.store_thms_atts "exhaust" new_type_names
    3.83 -        (map single case_names_exhausts) casedist_thms
    3.84 -  end;
    3.85 -
    3.86 -
    3.87 -(*************************** primrec combinators ******************************)
    3.88 -
    3.89 -fun prove_primrec_thms (config : config) new_type_names descr
    3.90 -    injects_of constr_inject (dist_rewrites, other_dist_rewrites) induct thy =
    3.91 -  let
    3.92 -    val _ = Datatype_Aux.message config "Constructing primrec combinators ...";
    3.93 -
    3.94 -    val big_name = space_implode "_" new_type_names;
    3.95 -    val thy0 = Sign.add_path big_name thy;
    3.96 -
    3.97 -    val descr' = flat descr;
    3.98 -    val recTs = Datatype_Aux.get_rec_types descr';
    3.99 -    val used = fold Term.add_tfree_namesT recTs [];
   3.100 -    val newTs = take (length (hd descr)) recTs;
   3.101 -
   3.102 -    val induct_Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct)));
   3.103 -
   3.104 -    val big_rec_name' = big_name ^ "_rec_set";
   3.105 -    val rec_set_names' =
   3.106 -      if length descr' = 1 then [big_rec_name']
   3.107 -      else map (prefix (big_rec_name' ^ "_") o string_of_int) (1 upto length descr');
   3.108 -    val rec_set_names = map (Sign.full_bname thy0) rec_set_names';
   3.109 -
   3.110 -    val (rec_result_Ts, reccomb_fn_Ts) = Datatype_Prop.make_primrec_Ts descr used;
   3.111 -
   3.112 -    val rec_set_Ts =
   3.113 -      map (fn (T1, T2) => (reccomb_fn_Ts @ [T1, T2]) ---> HOLogic.boolT) (recTs ~~ rec_result_Ts);
   3.114 -
   3.115 -    val rec_fns =
   3.116 -      map (uncurry (Datatype_Aux.mk_Free "f")) (reccomb_fn_Ts ~~ (1 upto length reccomb_fn_Ts));
   3.117 -    val rec_sets' =
   3.118 -      map (fn c => list_comb (Free c, rec_fns)) (rec_set_names' ~~ rec_set_Ts);
   3.119 -    val rec_sets =
   3.120 -      map (fn c => list_comb (Const c, rec_fns)) (rec_set_names ~~ rec_set_Ts);
   3.121 -
   3.122 -    (* introduction rules for graph of primrec function *)
   3.123 -
   3.124 -    fun make_rec_intr T rec_set (cname, cargs) (rec_intr_ts, l) =
   3.125 -      let
   3.126 -        fun mk_prem (dt, U) (j, k, prems, t1s, t2s) =
   3.127 -          let val free1 = Datatype_Aux.mk_Free "x" U j in
   3.128 -            (case (Datatype_Aux.strip_dtyp dt, strip_type U) of
   3.129 -              ((_, Datatype_Aux.DtRec m), (Us, _)) =>
   3.130 -                let
   3.131 -                  val free2 = Datatype_Aux.mk_Free "y" (Us ---> nth rec_result_Ts m) k;
   3.132 -                  val i = length Us;
   3.133 -                in
   3.134 -                  (j + 1, k + 1,
   3.135 -                    HOLogic.mk_Trueprop (HOLogic.list_all
   3.136 -                      (map (pair "x") Us, nth rec_sets' m $
   3.137 -                        Datatype_Aux.app_bnds free1 i $ Datatype_Aux.app_bnds free2 i)) :: prems,
   3.138 -                    free1 :: t1s, free2 :: t2s)
   3.139 -                end
   3.140 -            | _ => (j + 1, k, prems, free1 :: t1s, t2s))
   3.141 -          end;
   3.142 -
   3.143 -        val Ts = map (Datatype_Aux.typ_of_dtyp descr') cargs;
   3.144 -        val (_, _, prems, t1s, t2s) = fold_rev mk_prem (cargs ~~ Ts) (1, 1, [], [], []);
   3.145 -
   3.146 -      in
   3.147 -        (rec_intr_ts @
   3.148 -          [Logic.list_implies (prems, HOLogic.mk_Trueprop
   3.149 -            (rec_set $ list_comb (Const (cname, Ts ---> T), t1s) $
   3.150 -              list_comb (nth rec_fns l, t1s @ t2s)))], l + 1)
   3.151 -      end;
   3.152 -
   3.153 -    val (rec_intr_ts, _) =
   3.154 -      fold (fn ((d, T), set_name) =>
   3.155 -        fold (make_rec_intr T set_name) (#3 (snd d))) (descr' ~~ recTs ~~ rec_sets') ([], 0);
   3.156 -
   3.157 -    val ({intrs = rec_intrs, elims = rec_elims, ...}, thy1) =
   3.158 -      thy0
   3.159 -      |> Sign.map_naming Name_Space.conceal
   3.160 -      |> Inductive.add_inductive_global
   3.161 -          {quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name',
   3.162 -            coind = false, no_elim = false, no_ind = true, skip_mono = true, fork_mono = false}
   3.163 -          (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
   3.164 -          (map dest_Free rec_fns)
   3.165 -          (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) []
   3.166 -      ||> Sign.restore_naming thy0
   3.167 -      ||> Theory.checkpoint;
   3.168 -
   3.169 -    (* prove uniqueness and termination of primrec combinators *)
   3.170 -
   3.171 -    val _ = Datatype_Aux.message config "Proving termination and uniqueness of primrec functions ...";
   3.172 -
   3.173 -    fun mk_unique_tac ((((i, (tname, _, constrs)), elim), T), T') (tac, intrs) =
   3.174 -      let
   3.175 -        val distinct_tac =
   3.176 -          if i < length newTs then
   3.177 -            full_simp_tac (HOL_ss addsimps (nth dist_rewrites i)) 1
   3.178 -          else full_simp_tac (HOL_ss addsimps (flat other_dist_rewrites)) 1;
   3.179 -
   3.180 -        val inject =
   3.181 -          map (fn r => r RS iffD1)
   3.182 -            (if i < length newTs then nth constr_inject i else injects_of tname);
   3.183 -
   3.184 -        fun mk_unique_constr_tac n (cname, cargs) (tac, intr :: intrs, j) =
   3.185 -          let
   3.186 -            val k = length (filter Datatype_Aux.is_rec_type cargs);
   3.187 -          in
   3.188 -            (EVERY
   3.189 -              [DETERM tac,
   3.190 -                REPEAT (etac ex1E 1), rtac ex1I 1,
   3.191 -                DEPTH_SOLVE_1 (ares_tac [intr] 1),
   3.192 -                REPEAT_DETERM_N k (etac thin_rl 1 THEN rotate_tac 1 1),
   3.193 -                etac elim 1,
   3.194 -                REPEAT_DETERM_N j distinct_tac,
   3.195 -                TRY (dresolve_tac inject 1),
   3.196 -                REPEAT (etac conjE 1), hyp_subst_tac 1,
   3.197 -                REPEAT (EVERY [etac allE 1, dtac mp 1, atac 1]),
   3.198 -                TRY (hyp_subst_tac 1),
   3.199 -                rtac refl 1,
   3.200 -                REPEAT_DETERM_N (n - j - 1) distinct_tac],
   3.201 -              intrs, j + 1)
   3.202 -          end;
   3.203 -
   3.204 -        val (tac', intrs', _) =
   3.205 -          fold (mk_unique_constr_tac (length constrs)) constrs (tac, intrs, 0);
   3.206 -      in (tac', intrs') end;
   3.207 -
   3.208 -    val rec_unique_thms =
   3.209 -      let
   3.210 -        val rec_unique_ts =
   3.211 -          map (fn (((set_t, T1), T2), i) =>
   3.212 -            Const (@{const_name Ex1}, (T2 --> HOLogic.boolT) --> HOLogic.boolT) $
   3.213 -              absfree ("y", T2) (set_t $ Datatype_Aux.mk_Free "x" T1 i $ Free ("y", T2)))
   3.214 -                (rec_sets ~~ recTs ~~ rec_result_Ts ~~ (1 upto length recTs));
   3.215 -        val cert = cterm_of thy1;
   3.216 -        val insts =
   3.217 -          map (fn ((i, T), t) => absfree ("x" ^ string_of_int i, T) t)
   3.218 -            ((1 upto length recTs) ~~ recTs ~~ rec_unique_ts);
   3.219 -        val induct' = cterm_instantiate (map cert induct_Ps ~~ map cert insts) induct;
   3.220 -        val (tac, _) =
   3.221 -          fold mk_unique_tac (descr' ~~ rec_elims ~~ recTs ~~ rec_result_Ts)
   3.222 -            (((rtac induct' THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1 THEN
   3.223 -                rewrite_goals_tac [mk_meta_eq @{thm choice_eq}], rec_intrs));
   3.224 -      in
   3.225 -        Datatype_Aux.split_conj_thm (Skip_Proof.prove_global thy1 [] []
   3.226 -          (HOLogic.mk_Trueprop (Datatype_Aux.mk_conj rec_unique_ts)) (K tac))
   3.227 -      end;
   3.228 -
   3.229 -    val rec_total_thms = map (fn r => r RS @{thm theI'}) rec_unique_thms;
   3.230 -
   3.231 -    (* define primrec combinators *)
   3.232 -
   3.233 -    val big_reccomb_name = space_implode "_" new_type_names ^ "_rec";
   3.234 -    val reccomb_names =
   3.235 -      map (Sign.full_bname thy1)
   3.236 -        (if length descr' = 1 then [big_reccomb_name]
   3.237 -         else map (prefix (big_reccomb_name ^ "_") o string_of_int) (1 upto length descr'));
   3.238 -    val reccombs =
   3.239 -      map (fn ((name, T), T') => Const (name, reccomb_fn_Ts @ [T] ---> T'))
   3.240 -        (reccomb_names ~~ recTs ~~ rec_result_Ts);
   3.241 -
   3.242 -    val (reccomb_defs, thy2) =
   3.243 -      thy1
   3.244 -      |> Sign.add_consts_i (map (fn ((name, T), T') =>
   3.245 -            (Binding.name (Long_Name.base_name name), reccomb_fn_Ts @ [T] ---> T', NoSyn))
   3.246 -            (reccomb_names ~~ recTs ~~ rec_result_Ts))
   3.247 -      |> (Global_Theory.add_defs false o map Thm.no_attributes)
   3.248 -          (map
   3.249 -            (fn ((((name, comb), set), T), T') =>
   3.250 -              (Binding.name (Long_Name.base_name name ^ "_def"),
   3.251 -                Logic.mk_equals (comb, fold_rev lambda rec_fns (absfree ("x", T)
   3.252 -                 (Const (@{const_name The}, (T' --> HOLogic.boolT) --> T') $ absfree ("y", T')
   3.253 -                   (set $ Free ("x", T) $ Free ("y", T')))))))
   3.254 -            (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts))
   3.255 -      ||> Sign.parent_path
   3.256 -      ||> Theory.checkpoint;
   3.257 -
   3.258 -
   3.259 -    (* prove characteristic equations for primrec combinators *)
   3.260 -
   3.261 -    val _ = Datatype_Aux.message config "Proving characteristic theorems for primrec combinators ...";
   3.262 -
   3.263 -    val rec_thms =
   3.264 -      map (fn t =>
   3.265 -        Skip_Proof.prove_global thy2 [] [] t
   3.266 -          (fn _ => EVERY
   3.267 -            [rewrite_goals_tac reccomb_defs,
   3.268 -             rtac @{thm the1_equality} 1,
   3.269 -             resolve_tac rec_unique_thms 1,
   3.270 -             resolve_tac rec_intrs 1,
   3.271 -             REPEAT (rtac allI 1 ORELSE resolve_tac rec_total_thms 1)]))
   3.272 -       (Datatype_Prop.make_primrecs reccomb_names descr thy2);
   3.273 -  in
   3.274 -    thy2
   3.275 -    |> Sign.add_path (space_implode "_" new_type_names)
   3.276 -    |> Global_Theory.note_thmss ""
   3.277 -      [((Binding.name "recs", [Nitpick_Simps.add]), [(rec_thms, [])])]
   3.278 -    ||> Sign.parent_path
   3.279 -    ||> Theory.checkpoint
   3.280 -    |-> (fn thms => pair (reccomb_names, maps #2 thms))
   3.281 -  end;
   3.282 -
   3.283 -
   3.284 -(***************************** case combinators *******************************)
   3.285 -
   3.286 -fun prove_case_thms (config : config) new_type_names descr reccomb_names primrec_thms thy =
   3.287 -  let
   3.288 -    val _ = Datatype_Aux.message config "Proving characteristic theorems for case combinators ...";
   3.289 -
   3.290 -    val thy1 = Sign.add_path (space_implode "_" new_type_names) thy;
   3.291 -
   3.292 -    val descr' = flat descr;
   3.293 -    val recTs = Datatype_Aux.get_rec_types descr';
   3.294 -    val used = fold Term.add_tfree_namesT recTs [];
   3.295 -    val newTs = take (length (hd descr)) recTs;
   3.296 -    val T' = TFree (singleton (Name.variant_list used) "'t", HOLogic.typeS);
   3.297 -
   3.298 -    fun mk_dummyT dt = binder_types (Datatype_Aux.typ_of_dtyp descr' dt) ---> T';
   3.299 -
   3.300 -    val case_dummy_fns =
   3.301 -      map (fn (_, (_, _, constrs)) => map (fn (_, cargs) =>
   3.302 -        let
   3.303 -          val Ts = map (Datatype_Aux.typ_of_dtyp descr') cargs;
   3.304 -          val Ts' = map mk_dummyT (filter Datatype_Aux.is_rec_type cargs)
   3.305 -        in Const (@{const_name undefined}, Ts @ Ts' ---> T') end) constrs) descr';
   3.306 -
   3.307 -    val case_names = map (fn s => Sign.full_bname thy1 (s ^ "_case")) new_type_names;
   3.308 -
   3.309 -    (* define case combinators via primrec combinators *)
   3.310 -
   3.311 -    val (case_defs, thy2) =
   3.312 -      fold (fn ((((i, (_, _, constrs)), T), name), recname) => fn (defs, thy) =>
   3.313 -          let
   3.314 -            val (fns1, fns2) = split_list (map (fn ((_, cargs), j) =>
   3.315 -              let
   3.316 -                val Ts = map (Datatype_Aux.typ_of_dtyp descr') cargs;
   3.317 -                val Ts' = Ts @ map mk_dummyT (filter Datatype_Aux.is_rec_type cargs);
   3.318 -                val frees' = map2 (Datatype_Aux.mk_Free "x") Ts' (1 upto length Ts');
   3.319 -                val frees = take (length cargs) frees';
   3.320 -                val free = Datatype_Aux.mk_Free "f" (Ts ---> T') j;
   3.321 -              in
   3.322 -                (free, fold_rev (absfree o dest_Free) frees' (list_comb (free, frees)))
   3.323 -              end) (constrs ~~ (1 upto length constrs)));
   3.324 -  
   3.325 -            val caseT = map (snd o dest_Free) fns1 @ [T] ---> T';
   3.326 -            val fns = flat (take i case_dummy_fns) @ fns2 @ flat (drop (i + 1) case_dummy_fns);
   3.327 -            val reccomb = Const (recname, (map fastype_of fns) @ [T] ---> T');
   3.328 -            val decl = ((Binding.name (Long_Name.base_name name), caseT), NoSyn);
   3.329 -            val def =
   3.330 -              (Binding.name (Long_Name.base_name name ^ "_def"),
   3.331 -                Logic.mk_equals (Const (name, caseT),
   3.332 -                  fold_rev lambda fns1
   3.333 -                    (list_comb (reccomb,
   3.334 -                      flat (take i case_dummy_fns) @ fns2 @ flat (drop (i + 1) case_dummy_fns)))));
   3.335 -            val ([def_thm], thy') =
   3.336 -              thy
   3.337 -              |> Sign.declare_const_global decl |> snd
   3.338 -              |> (Global_Theory.add_defs false o map Thm.no_attributes) [def];
   3.339 -  
   3.340 -          in (defs @ [def_thm], thy') end)
   3.341 -        (hd descr ~~ newTs ~~ case_names ~~ take (length newTs) reccomb_names) ([], thy1)
   3.342 -      ||> Theory.checkpoint;
   3.343 -
   3.344 -    val case_thms =
   3.345 -      (map o map) (fn t =>
   3.346 -          Skip_Proof.prove_global thy2 [] [] t
   3.347 -            (fn _ =>
   3.348 -              EVERY [rewrite_goals_tac (case_defs @ map mk_meta_eq primrec_thms), rtac refl 1]))
   3.349 -        (Datatype_Prop.make_cases case_names descr thy2);
   3.350 -  in
   3.351 -    thy2
   3.352 -    |> Context.theory_map ((fold o fold) Nitpick_Simps.add_thm case_thms)
   3.353 -    |> Sign.parent_path
   3.354 -    |> Datatype_Aux.store_thmss "cases" new_type_names case_thms
   3.355 -    |-> (fn thmss => pair (thmss, case_names))
   3.356 -  end;
   3.357 -
   3.358 -
   3.359 -(******************************* case splitting *******************************)
   3.360 -
   3.361 -fun prove_split_thms (config : config)
   3.362 -    new_type_names case_names descr constr_inject dist_rewrites casedist_thms case_thms thy =
   3.363 -  let
   3.364 -    val _ = Datatype_Aux.message config "Proving equations for case splitting ...";
   3.365 -
   3.366 -    val descr' = flat descr;
   3.367 -    val recTs = Datatype_Aux.get_rec_types descr';
   3.368 -    val newTs = take (length (hd descr)) recTs;
   3.369 -
   3.370 -    fun prove_split_thms ((((((t1, t2), inject), dist_rewrites'), exhaustion), case_thms'), T) =
   3.371 -      let
   3.372 -        val cert = cterm_of thy;
   3.373 -        val _ $ (_ $ lhs $ _) = hd (Logic.strip_assums_hyp (hd (prems_of exhaustion)));
   3.374 -        val exhaustion' = cterm_instantiate [(cert lhs, cert (Free ("x", T)))] exhaustion;
   3.375 -        val tac =
   3.376 -          EVERY [rtac exhaustion' 1,
   3.377 -            ALLGOALS (asm_simp_tac (HOL_ss addsimps (dist_rewrites' @ inject @ case_thms')))];
   3.378 -      in
   3.379 -        (Skip_Proof.prove_global thy [] [] t1 (K tac),
   3.380 -         Skip_Proof.prove_global thy [] [] t2 (K tac))
   3.381 -      end;
   3.382 -
   3.383 -    val split_thm_pairs =
   3.384 -      map prove_split_thms
   3.385 -        (Datatype_Prop.make_splits case_names descr thy ~~ constr_inject ~~
   3.386 -          dist_rewrites ~~ casedist_thms ~~ case_thms ~~ newTs);
   3.387 -
   3.388 -    val (split_thms, split_asm_thms) = split_list split_thm_pairs
   3.389 -
   3.390 -  in
   3.391 -    thy
   3.392 -    |> Datatype_Aux.store_thms "split" new_type_names split_thms
   3.393 -    ||>> Datatype_Aux.store_thms "split_asm" new_type_names split_asm_thms
   3.394 -    |-> (fn (thms1, thms2) => pair (thms1 ~~ thms2))
   3.395 -  end;
   3.396 -
   3.397 -fun prove_weak_case_congs new_type_names case_names descr thy =
   3.398 -  let
   3.399 -    fun prove_weak_case_cong t =
   3.400 -     Skip_Proof.prove_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
   3.401 -       (fn {prems, ...} => EVERY [rtac (hd prems RS arg_cong) 1]);
   3.402 -
   3.403 -    val weak_case_congs =
   3.404 -      map prove_weak_case_cong (Datatype_Prop.make_weak_case_congs case_names descr thy);
   3.405 -
   3.406 -  in thy |> Datatype_Aux.store_thms "weak_case_cong" new_type_names weak_case_congs end;
   3.407 -
   3.408 -(************************* additional theorems for TFL ************************)
   3.409 -
   3.410 -fun prove_nchotomys (config : config) new_type_names descr casedist_thms thy =
   3.411 -  let
   3.412 -    val _ = Datatype_Aux.message config "Proving additional theorems for TFL ...";
   3.413 -
   3.414 -    fun prove_nchotomy (t, exhaustion) =
   3.415 -      let
   3.416 -        (* For goal i, select the correct disjunct to attack, then prove it *)
   3.417 -        fun tac i 0 = EVERY [TRY (rtac disjI1 i), hyp_subst_tac i, REPEAT (rtac exI i), rtac refl i]
   3.418 -          | tac i n = rtac disjI2 i THEN tac i (n - 1);
   3.419 -      in
   3.420 -        Skip_Proof.prove_global thy [] [] t
   3.421 -          (fn _ =>
   3.422 -            EVERY [rtac allI 1,
   3.423 -             Datatype_Aux.exh_tac (K exhaustion) 1,
   3.424 -             ALLGOALS (fn i => tac i (i - 1))])
   3.425 -      end;
   3.426 -
   3.427 -    val nchotomys =
   3.428 -      map prove_nchotomy (Datatype_Prop.make_nchotomys descr ~~ casedist_thms);
   3.429 -
   3.430 -  in thy |> Datatype_Aux.store_thms "nchotomy" new_type_names nchotomys end;
   3.431 -
   3.432 -fun prove_case_congs new_type_names case_names descr nchotomys case_thms thy =
   3.433 -  let
   3.434 -    fun prove_case_cong ((t, nchotomy), case_rewrites) =
   3.435 -      let
   3.436 -        val Const ("==>", _) $ tm $ _ = t;
   3.437 -        val Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ Ma) = tm;
   3.438 -        val cert = cterm_of thy;
   3.439 -        val nchotomy' = nchotomy RS spec;
   3.440 -        val [v] = Term.add_vars (concl_of nchotomy') [];
   3.441 -        val nchotomy'' = cterm_instantiate [(cert (Var v), cert Ma)] nchotomy';
   3.442 -      in
   3.443 -        Skip_Proof.prove_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
   3.444 -          (fn {prems, ...} =>
   3.445 -            let val simplify = asm_simp_tac (HOL_ss addsimps (prems @ case_rewrites)) in
   3.446 -              EVERY [
   3.447 -                simp_tac (HOL_ss addsimps [hd prems]) 1,
   3.448 -                cut_facts_tac [nchotomy''] 1,
   3.449 -                REPEAT (etac disjE 1 THEN REPEAT (etac exE 1) THEN simplify 1),
   3.450 -                REPEAT (etac exE 1) THEN simplify 1 (* Get last disjunct *)]
   3.451 -            end)
   3.452 -      end;
   3.453 -
   3.454 -    val case_congs =
   3.455 -      map prove_case_cong
   3.456 -        (Datatype_Prop.make_case_congs case_names descr thy ~~ nchotomys ~~ case_thms);
   3.457 -
   3.458 -  in thy |> Datatype_Aux.store_thms "case_cong" new_type_names case_congs end;
   3.459 -
   3.460 -end;
     4.1 --- a/src/HOL/Tools/Datatype/rep_datatype.ML	Sat Dec 17 12:10:37 2011 +0100
     4.2 +++ b/src/HOL/Tools/Datatype/rep_datatype.ML	Sat Dec 17 12:42:10 2011 +0100
     4.3 @@ -1,7 +1,10 @@
     4.4  (*  Title:      HOL/Tools/Datatype/rep_datatype.ML
     4.5      Author:     Stefan Berghofer, TU Muenchen
     4.6  
     4.7 -Representation of existing types as datatypes.
     4.8 +Representation of existing types as datatypes: proofs and definitions
     4.9 +independent of concrete representation of datatypes (i.e. requiring
    4.10 +only abstract properties: injectivity / distinctness of constructors
    4.11 +and induction).
    4.12  *)
    4.13  
    4.14  signature REP_DATATYPE =
    4.15 @@ -17,6 +20,440 @@
    4.16  structure Rep_Datatype: REP_DATATYPE =
    4.17  struct
    4.18  
    4.19 +type config = Datatype_Aux.config;
    4.20 +type descr = Datatype_Aux.descr;
    4.21 +
    4.22 +
    4.23 +
    4.24 +(** derived definitions and proofs **)
    4.25 +
    4.26 +(* case distinction theorems *)
    4.27 +
    4.28 +fun prove_casedist_thms (config : config) new_type_names descr induct case_names_exhausts thy =
    4.29 +  let
    4.30 +    val _ = Datatype_Aux.message config "Proving case distinction theorems ...";
    4.31 +
    4.32 +    val descr' = flat descr;
    4.33 +    val recTs = Datatype_Aux.get_rec_types descr';
    4.34 +    val newTs = take (length (hd descr)) recTs;
    4.35 +
    4.36 +    val maxidx = Thm.maxidx_of induct;
    4.37 +    val induct_Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct)));
    4.38 +
    4.39 +    fun prove_casedist_thm (i, (T, t)) =
    4.40 +      let
    4.41 +        val dummyPs = map (fn (Var (_, Type (_, [T', T'']))) =>
    4.42 +          Abs ("z", T', Const (@{const_name True}, T''))) induct_Ps;
    4.43 +        val P =
    4.44 +          Abs ("z", T, HOLogic.imp $ HOLogic.mk_eq (Var (("a", maxidx + 1), T), Bound 0) $
    4.45 +            Var (("P", 0), HOLogic.boolT));
    4.46 +        val insts = take i dummyPs @ (P :: drop (i + 1) dummyPs);
    4.47 +        val cert = cterm_of thy;
    4.48 +        val insts' = map cert induct_Ps ~~ map cert insts;
    4.49 +        val induct' =
    4.50 +          refl RS
    4.51 +            (nth (Datatype_Aux.split_conj_thm (cterm_instantiate insts' induct)) i RSN (2, rev_mp));
    4.52 +      in
    4.53 +        Skip_Proof.prove_global thy []
    4.54 +          (Logic.strip_imp_prems t)
    4.55 +          (Logic.strip_imp_concl t)
    4.56 +          (fn {prems, ...} =>
    4.57 +            EVERY
    4.58 +              [rtac induct' 1,
    4.59 +               REPEAT (rtac TrueI 1),
    4.60 +               REPEAT ((rtac impI 1) THEN (eresolve_tac prems 1)),
    4.61 +               REPEAT (rtac TrueI 1)])
    4.62 +      end;
    4.63 +
    4.64 +    val casedist_thms =
    4.65 +      map_index prove_casedist_thm (newTs ~~ Datatype_Prop.make_casedists descr);
    4.66 +  in
    4.67 +    thy
    4.68 +    |> Datatype_Aux.store_thms_atts "exhaust" new_type_names
    4.69 +        (map single case_names_exhausts) casedist_thms
    4.70 +  end;
    4.71 +
    4.72 +
    4.73 +(* primrec combinators *)
    4.74 +
    4.75 +fun prove_primrec_thms (config : config) new_type_names descr
    4.76 +    injects_of constr_inject (dist_rewrites, other_dist_rewrites) induct thy =
    4.77 +  let
    4.78 +    val _ = Datatype_Aux.message config "Constructing primrec combinators ...";
    4.79 +
    4.80 +    val big_name = space_implode "_" new_type_names;
    4.81 +    val thy0 = Sign.add_path big_name thy;
    4.82 +
    4.83 +    val descr' = flat descr;
    4.84 +    val recTs = Datatype_Aux.get_rec_types descr';
    4.85 +    val used = fold Term.add_tfree_namesT recTs [];
    4.86 +    val newTs = take (length (hd descr)) recTs;
    4.87 +
    4.88 +    val induct_Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct)));
    4.89 +
    4.90 +    val big_rec_name' = big_name ^ "_rec_set";
    4.91 +    val rec_set_names' =
    4.92 +      if length descr' = 1 then [big_rec_name']
    4.93 +      else map (prefix (big_rec_name' ^ "_") o string_of_int) (1 upto length descr');
    4.94 +    val rec_set_names = map (Sign.full_bname thy0) rec_set_names';
    4.95 +
    4.96 +    val (rec_result_Ts, reccomb_fn_Ts) = Datatype_Prop.make_primrec_Ts descr used;
    4.97 +
    4.98 +    val rec_set_Ts =
    4.99 +      map (fn (T1, T2) => (reccomb_fn_Ts @ [T1, T2]) ---> HOLogic.boolT) (recTs ~~ rec_result_Ts);
   4.100 +
   4.101 +    val rec_fns =
   4.102 +      map (uncurry (Datatype_Aux.mk_Free "f")) (reccomb_fn_Ts ~~ (1 upto length reccomb_fn_Ts));
   4.103 +    val rec_sets' =
   4.104 +      map (fn c => list_comb (Free c, rec_fns)) (rec_set_names' ~~ rec_set_Ts);
   4.105 +    val rec_sets =
   4.106 +      map (fn c => list_comb (Const c, rec_fns)) (rec_set_names ~~ rec_set_Ts);
   4.107 +
   4.108 +    (* introduction rules for graph of primrec function *)
   4.109 +
   4.110 +    fun make_rec_intr T rec_set (cname, cargs) (rec_intr_ts, l) =
   4.111 +      let
   4.112 +        fun mk_prem (dt, U) (j, k, prems, t1s, t2s) =
   4.113 +          let val free1 = Datatype_Aux.mk_Free "x" U j in
   4.114 +            (case (Datatype_Aux.strip_dtyp dt, strip_type U) of
   4.115 +              ((_, Datatype_Aux.DtRec m), (Us, _)) =>
   4.116 +                let
   4.117 +                  val free2 = Datatype_Aux.mk_Free "y" (Us ---> nth rec_result_Ts m) k;
   4.118 +                  val i = length Us;
   4.119 +                in
   4.120 +                  (j + 1, k + 1,
   4.121 +                    HOLogic.mk_Trueprop (HOLogic.list_all
   4.122 +                      (map (pair "x") Us, nth rec_sets' m $
   4.123 +                        Datatype_Aux.app_bnds free1 i $ Datatype_Aux.app_bnds free2 i)) :: prems,
   4.124 +                    free1 :: t1s, free2 :: t2s)
   4.125 +                end
   4.126 +            | _ => (j + 1, k, prems, free1 :: t1s, t2s))
   4.127 +          end;
   4.128 +
   4.129 +        val Ts = map (Datatype_Aux.typ_of_dtyp descr') cargs;
   4.130 +        val (_, _, prems, t1s, t2s) = fold_rev mk_prem (cargs ~~ Ts) (1, 1, [], [], []);
   4.131 +
   4.132 +      in
   4.133 +        (rec_intr_ts @
   4.134 +          [Logic.list_implies (prems, HOLogic.mk_Trueprop
   4.135 +            (rec_set $ list_comb (Const (cname, Ts ---> T), t1s) $
   4.136 +              list_comb (nth rec_fns l, t1s @ t2s)))], l + 1)
   4.137 +      end;
   4.138 +
   4.139 +    val (rec_intr_ts, _) =
   4.140 +      fold (fn ((d, T), set_name) =>
   4.141 +        fold (make_rec_intr T set_name) (#3 (snd d))) (descr' ~~ recTs ~~ rec_sets') ([], 0);
   4.142 +
   4.143 +    val ({intrs = rec_intrs, elims = rec_elims, ...}, thy1) =
   4.144 +      thy0
   4.145 +      |> Sign.map_naming Name_Space.conceal
   4.146 +      |> Inductive.add_inductive_global
   4.147 +          {quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name',
   4.148 +            coind = false, no_elim = false, no_ind = true, skip_mono = true, fork_mono = false}
   4.149 +          (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
   4.150 +          (map dest_Free rec_fns)
   4.151 +          (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) []
   4.152 +      ||> Sign.restore_naming thy0
   4.153 +      ||> Theory.checkpoint;
   4.154 +
   4.155 +    (* prove uniqueness and termination of primrec combinators *)
   4.156 +
   4.157 +    val _ = Datatype_Aux.message config "Proving termination and uniqueness of primrec functions ...";
   4.158 +
   4.159 +    fun mk_unique_tac ((((i, (tname, _, constrs)), elim), T), T') (tac, intrs) =
   4.160 +      let
   4.161 +        val distinct_tac =
   4.162 +          if i < length newTs then
   4.163 +            full_simp_tac (HOL_ss addsimps (nth dist_rewrites i)) 1
   4.164 +          else full_simp_tac (HOL_ss addsimps (flat other_dist_rewrites)) 1;
   4.165 +
   4.166 +        val inject =
   4.167 +          map (fn r => r RS iffD1)
   4.168 +            (if i < length newTs then nth constr_inject i else injects_of tname);
   4.169 +
   4.170 +        fun mk_unique_constr_tac n (cname, cargs) (tac, intr :: intrs, j) =
   4.171 +          let
   4.172 +            val k = length (filter Datatype_Aux.is_rec_type cargs);
   4.173 +          in
   4.174 +            (EVERY
   4.175 +              [DETERM tac,
   4.176 +                REPEAT (etac ex1E 1), rtac ex1I 1,
   4.177 +                DEPTH_SOLVE_1 (ares_tac [intr] 1),
   4.178 +                REPEAT_DETERM_N k (etac thin_rl 1 THEN rotate_tac 1 1),
   4.179 +                etac elim 1,
   4.180 +                REPEAT_DETERM_N j distinct_tac,
   4.181 +                TRY (dresolve_tac inject 1),
   4.182 +                REPEAT (etac conjE 1), hyp_subst_tac 1,
   4.183 +                REPEAT (EVERY [etac allE 1, dtac mp 1, atac 1]),
   4.184 +                TRY (hyp_subst_tac 1),
   4.185 +                rtac refl 1,
   4.186 +                REPEAT_DETERM_N (n - j - 1) distinct_tac],
   4.187 +              intrs, j + 1)
   4.188 +          end;
   4.189 +
   4.190 +        val (tac', intrs', _) =
   4.191 +          fold (mk_unique_constr_tac (length constrs)) constrs (tac, intrs, 0);
   4.192 +      in (tac', intrs') end;
   4.193 +
   4.194 +    val rec_unique_thms =
   4.195 +      let
   4.196 +        val rec_unique_ts =
   4.197 +          map (fn (((set_t, T1), T2), i) =>
   4.198 +            Const (@{const_name Ex1}, (T2 --> HOLogic.boolT) --> HOLogic.boolT) $
   4.199 +              absfree ("y", T2) (set_t $ Datatype_Aux.mk_Free "x" T1 i $ Free ("y", T2)))
   4.200 +                (rec_sets ~~ recTs ~~ rec_result_Ts ~~ (1 upto length recTs));
   4.201 +        val cert = cterm_of thy1;
   4.202 +        val insts =
   4.203 +          map (fn ((i, T), t) => absfree ("x" ^ string_of_int i, T) t)
   4.204 +            ((1 upto length recTs) ~~ recTs ~~ rec_unique_ts);
   4.205 +        val induct' = cterm_instantiate (map cert induct_Ps ~~ map cert insts) induct;
   4.206 +        val (tac, _) =
   4.207 +          fold mk_unique_tac (descr' ~~ rec_elims ~~ recTs ~~ rec_result_Ts)
   4.208 +            (((rtac induct' THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1 THEN
   4.209 +                rewrite_goals_tac [mk_meta_eq @{thm choice_eq}], rec_intrs));
   4.210 +      in
   4.211 +        Datatype_Aux.split_conj_thm (Skip_Proof.prove_global thy1 [] []
   4.212 +          (HOLogic.mk_Trueprop (Datatype_Aux.mk_conj rec_unique_ts)) (K tac))
   4.213 +      end;
   4.214 +
   4.215 +    val rec_total_thms = map (fn r => r RS @{thm theI'}) rec_unique_thms;
   4.216 +
   4.217 +    (* define primrec combinators *)
   4.218 +
   4.219 +    val big_reccomb_name = space_implode "_" new_type_names ^ "_rec";
   4.220 +    val reccomb_names =
   4.221 +      map (Sign.full_bname thy1)
   4.222 +        (if length descr' = 1 then [big_reccomb_name]
   4.223 +         else map (prefix (big_reccomb_name ^ "_") o string_of_int) (1 upto length descr'));
   4.224 +    val reccombs =
   4.225 +      map (fn ((name, T), T') => Const (name, reccomb_fn_Ts @ [T] ---> T'))
   4.226 +        (reccomb_names ~~ recTs ~~ rec_result_Ts);
   4.227 +
   4.228 +    val (reccomb_defs, thy2) =
   4.229 +      thy1
   4.230 +      |> Sign.add_consts_i (map (fn ((name, T), T') =>
   4.231 +            (Binding.name (Long_Name.base_name name), reccomb_fn_Ts @ [T] ---> T', NoSyn))
   4.232 +            (reccomb_names ~~ recTs ~~ rec_result_Ts))
   4.233 +      |> (Global_Theory.add_defs false o map Thm.no_attributes)
   4.234 +          (map
   4.235 +            (fn ((((name, comb), set), T), T') =>
   4.236 +              (Binding.name (Long_Name.base_name name ^ "_def"),
   4.237 +                Logic.mk_equals (comb, fold_rev lambda rec_fns (absfree ("x", T)
   4.238 +                 (Const (@{const_name The}, (T' --> HOLogic.boolT) --> T') $ absfree ("y", T')
   4.239 +                   (set $ Free ("x", T) $ Free ("y", T')))))))
   4.240 +            (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts))
   4.241 +      ||> Sign.parent_path
   4.242 +      ||> Theory.checkpoint;
   4.243 +
   4.244 +
   4.245 +    (* prove characteristic equations for primrec combinators *)
   4.246 +
   4.247 +    val _ = Datatype_Aux.message config "Proving characteristic theorems for primrec combinators ...";
   4.248 +
   4.249 +    val rec_thms =
   4.250 +      map (fn t =>
   4.251 +        Skip_Proof.prove_global thy2 [] [] t
   4.252 +          (fn _ => EVERY
   4.253 +            [rewrite_goals_tac reccomb_defs,
   4.254 +             rtac @{thm the1_equality} 1,
   4.255 +             resolve_tac rec_unique_thms 1,
   4.256 +             resolve_tac rec_intrs 1,
   4.257 +             REPEAT (rtac allI 1 ORELSE resolve_tac rec_total_thms 1)]))
   4.258 +       (Datatype_Prop.make_primrecs reccomb_names descr thy2);
   4.259 +  in
   4.260 +    thy2
   4.261 +    |> Sign.add_path (space_implode "_" new_type_names)
   4.262 +    |> Global_Theory.note_thmss ""
   4.263 +      [((Binding.name "recs", [Nitpick_Simps.add]), [(rec_thms, [])])]
   4.264 +    ||> Sign.parent_path
   4.265 +    ||> Theory.checkpoint
   4.266 +    |-> (fn thms => pair (reccomb_names, maps #2 thms))
   4.267 +  end;
   4.268 +
   4.269 +
   4.270 +(* case combinators *)
   4.271 +
   4.272 +fun prove_case_thms (config : config) new_type_names descr reccomb_names primrec_thms thy =
   4.273 +  let
   4.274 +    val _ = Datatype_Aux.message config "Proving characteristic theorems for case combinators ...";
   4.275 +
   4.276 +    val thy1 = Sign.add_path (space_implode "_" new_type_names) thy;
   4.277 +
   4.278 +    val descr' = flat descr;
   4.279 +    val recTs = Datatype_Aux.get_rec_types descr';
   4.280 +    val used = fold Term.add_tfree_namesT recTs [];
   4.281 +    val newTs = take (length (hd descr)) recTs;
   4.282 +    val T' = TFree (singleton (Name.variant_list used) "'t", HOLogic.typeS);
   4.283 +
   4.284 +    fun mk_dummyT dt = binder_types (Datatype_Aux.typ_of_dtyp descr' dt) ---> T';
   4.285 +
   4.286 +    val case_dummy_fns =
   4.287 +      map (fn (_, (_, _, constrs)) => map (fn (_, cargs) =>
   4.288 +        let
   4.289 +          val Ts = map (Datatype_Aux.typ_of_dtyp descr') cargs;
   4.290 +          val Ts' = map mk_dummyT (filter Datatype_Aux.is_rec_type cargs)
   4.291 +        in Const (@{const_name undefined}, Ts @ Ts' ---> T') end) constrs) descr';
   4.292 +
   4.293 +    val case_names = map (fn s => Sign.full_bname thy1 (s ^ "_case")) new_type_names;
   4.294 +
   4.295 +    (* define case combinators via primrec combinators *)
   4.296 +
   4.297 +    val (case_defs, thy2) =
   4.298 +      fold (fn ((((i, (_, _, constrs)), T), name), recname) => fn (defs, thy) =>
   4.299 +          let
   4.300 +            val (fns1, fns2) = split_list (map (fn ((_, cargs), j) =>
   4.301 +              let
   4.302 +                val Ts = map (Datatype_Aux.typ_of_dtyp descr') cargs;
   4.303 +                val Ts' = Ts @ map mk_dummyT (filter Datatype_Aux.is_rec_type cargs);
   4.304 +                val frees' = map2 (Datatype_Aux.mk_Free "x") Ts' (1 upto length Ts');
   4.305 +                val frees = take (length cargs) frees';
   4.306 +                val free = Datatype_Aux.mk_Free "f" (Ts ---> T') j;
   4.307 +              in
   4.308 +                (free, fold_rev (absfree o dest_Free) frees' (list_comb (free, frees)))
   4.309 +              end) (constrs ~~ (1 upto length constrs)));
   4.310 +
   4.311 +            val caseT = map (snd o dest_Free) fns1 @ [T] ---> T';
   4.312 +            val fns = flat (take i case_dummy_fns) @ fns2 @ flat (drop (i + 1) case_dummy_fns);
   4.313 +            val reccomb = Const (recname, (map fastype_of fns) @ [T] ---> T');
   4.314 +            val decl = ((Binding.name (Long_Name.base_name name), caseT), NoSyn);
   4.315 +            val def =
   4.316 +              (Binding.name (Long_Name.base_name name ^ "_def"),
   4.317 +                Logic.mk_equals (Const (name, caseT),
   4.318 +                  fold_rev lambda fns1
   4.319 +                    (list_comb (reccomb,
   4.320 +                      flat (take i case_dummy_fns) @ fns2 @ flat (drop (i + 1) case_dummy_fns)))));
   4.321 +            val ([def_thm], thy') =
   4.322 +              thy
   4.323 +              |> Sign.declare_const_global decl |> snd
   4.324 +              |> (Global_Theory.add_defs false o map Thm.no_attributes) [def];
   4.325 +
   4.326 +          in (defs @ [def_thm], thy') end)
   4.327 +        (hd descr ~~ newTs ~~ case_names ~~ take (length newTs) reccomb_names) ([], thy1)
   4.328 +      ||> Theory.checkpoint;
   4.329 +
   4.330 +    val case_thms =
   4.331 +      (map o map) (fn t =>
   4.332 +          Skip_Proof.prove_global thy2 [] [] t
   4.333 +            (fn _ =>
   4.334 +              EVERY [rewrite_goals_tac (case_defs @ map mk_meta_eq primrec_thms), rtac refl 1]))
   4.335 +        (Datatype_Prop.make_cases case_names descr thy2);
   4.336 +  in
   4.337 +    thy2
   4.338 +    |> Context.theory_map ((fold o fold) Nitpick_Simps.add_thm case_thms)
   4.339 +    |> Sign.parent_path
   4.340 +    |> Datatype_Aux.store_thmss "cases" new_type_names case_thms
   4.341 +    |-> (fn thmss => pair (thmss, case_names))
   4.342 +  end;
   4.343 +
   4.344 +
   4.345 +(* case splitting *)
   4.346 +
   4.347 +fun prove_split_thms (config : config)
   4.348 +    new_type_names case_names descr constr_inject dist_rewrites casedist_thms case_thms thy =
   4.349 +  let
   4.350 +    val _ = Datatype_Aux.message config "Proving equations for case splitting ...";
   4.351 +
   4.352 +    val descr' = flat descr;
   4.353 +    val recTs = Datatype_Aux.get_rec_types descr';
   4.354 +    val newTs = take (length (hd descr)) recTs;
   4.355 +
   4.356 +    fun prove_split_thms ((((((t1, t2), inject), dist_rewrites'), exhaustion), case_thms'), T) =
   4.357 +      let
   4.358 +        val cert = cterm_of thy;
   4.359 +        val _ $ (_ $ lhs $ _) = hd (Logic.strip_assums_hyp (hd (prems_of exhaustion)));
   4.360 +        val exhaustion' = cterm_instantiate [(cert lhs, cert (Free ("x", T)))] exhaustion;
   4.361 +        val tac =
   4.362 +          EVERY [rtac exhaustion' 1,
   4.363 +            ALLGOALS (asm_simp_tac (HOL_ss addsimps (dist_rewrites' @ inject @ case_thms')))];
   4.364 +      in
   4.365 +        (Skip_Proof.prove_global thy [] [] t1 (K tac),
   4.366 +         Skip_Proof.prove_global thy [] [] t2 (K tac))
   4.367 +      end;
   4.368 +
   4.369 +    val split_thm_pairs =
   4.370 +      map prove_split_thms
   4.371 +        (Datatype_Prop.make_splits case_names descr thy ~~ constr_inject ~~
   4.372 +          dist_rewrites ~~ casedist_thms ~~ case_thms ~~ newTs);
   4.373 +
   4.374 +    val (split_thms, split_asm_thms) = split_list split_thm_pairs
   4.375 +
   4.376 +  in
   4.377 +    thy
   4.378 +    |> Datatype_Aux.store_thms "split" new_type_names split_thms
   4.379 +    ||>> Datatype_Aux.store_thms "split_asm" new_type_names split_asm_thms
   4.380 +    |-> (fn (thms1, thms2) => pair (thms1 ~~ thms2))
   4.381 +  end;
   4.382 +
   4.383 +fun prove_weak_case_congs new_type_names case_names descr thy =
   4.384 +  let
   4.385 +    fun prove_weak_case_cong t =
   4.386 +     Skip_Proof.prove_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
   4.387 +       (fn {prems, ...} => EVERY [rtac (hd prems RS arg_cong) 1]);
   4.388 +
   4.389 +    val weak_case_congs =
   4.390 +      map prove_weak_case_cong (Datatype_Prop.make_weak_case_congs case_names descr thy);
   4.391 +
   4.392 +  in thy |> Datatype_Aux.store_thms "weak_case_cong" new_type_names weak_case_congs end;
   4.393 +
   4.394 +
   4.395 +(* additional theorems for TFL *)
   4.396 +
   4.397 +fun prove_nchotomys (config : config) new_type_names descr casedist_thms thy =
   4.398 +  let
   4.399 +    val _ = Datatype_Aux.message config "Proving additional theorems for TFL ...";
   4.400 +
   4.401 +    fun prove_nchotomy (t, exhaustion) =
   4.402 +      let
   4.403 +        (* For goal i, select the correct disjunct to attack, then prove it *)
   4.404 +        fun tac i 0 = EVERY [TRY (rtac disjI1 i), hyp_subst_tac i, REPEAT (rtac exI i), rtac refl i]
   4.405 +          | tac i n = rtac disjI2 i THEN tac i (n - 1);
   4.406 +      in
   4.407 +        Skip_Proof.prove_global thy [] [] t
   4.408 +          (fn _ =>
   4.409 +            EVERY [rtac allI 1,
   4.410 +             Datatype_Aux.exh_tac (K exhaustion) 1,
   4.411 +             ALLGOALS (fn i => tac i (i - 1))])
   4.412 +      end;
   4.413 +
   4.414 +    val nchotomys =
   4.415 +      map prove_nchotomy (Datatype_Prop.make_nchotomys descr ~~ casedist_thms);
   4.416 +
   4.417 +  in thy |> Datatype_Aux.store_thms "nchotomy" new_type_names nchotomys end;
   4.418 +
   4.419 +fun prove_case_congs new_type_names case_names descr nchotomys case_thms thy =
   4.420 +  let
   4.421 +    fun prove_case_cong ((t, nchotomy), case_rewrites) =
   4.422 +      let
   4.423 +        val Const ("==>", _) $ tm $ _ = t;
   4.424 +        val Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ Ma) = tm;
   4.425 +        val cert = cterm_of thy;
   4.426 +        val nchotomy' = nchotomy RS spec;
   4.427 +        val [v] = Term.add_vars (concl_of nchotomy') [];
   4.428 +        val nchotomy'' = cterm_instantiate [(cert (Var v), cert Ma)] nchotomy';
   4.429 +      in
   4.430 +        Skip_Proof.prove_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
   4.431 +          (fn {prems, ...} =>
   4.432 +            let val simplify = asm_simp_tac (HOL_ss addsimps (prems @ case_rewrites)) in
   4.433 +              EVERY [
   4.434 +                simp_tac (HOL_ss addsimps [hd prems]) 1,
   4.435 +                cut_facts_tac [nchotomy''] 1,
   4.436 +                REPEAT (etac disjE 1 THEN REPEAT (etac exE 1) THEN simplify 1),
   4.437 +                REPEAT (etac exE 1) THEN simplify 1 (* Get last disjunct *)]
   4.438 +            end)
   4.439 +      end;
   4.440 +
   4.441 +    val case_congs =
   4.442 +      map prove_case_cong
   4.443 +        (Datatype_Prop.make_case_congs case_names descr thy ~~ nchotomys ~~ case_thms);
   4.444 +
   4.445 +  in thy |> Datatype_Aux.store_thms "case_cong" new_type_names case_congs end;
   4.446 +
   4.447 +
   4.448 +
   4.449 +(** derive datatype props **)
   4.450 +
   4.451 +local
   4.452 +
   4.453  fun make_dt_info descr induct inducts rec_names rec_rewrites
   4.454      (index, (((((((((((_, (tname, _, _))), inject), distinct),
   4.455        exhaust), nchotomy), case_name), case_rewrites), case_cong), weak_case_cong),
   4.456 @@ -39,6 +476,8 @@
   4.457      split = split,
   4.458      split_asm = split_asm});
   4.459  
   4.460 +in
   4.461 +
   4.462  fun derive_datatype_props config dt_names descr induct inject distinct thy1 =
   4.463    let
   4.464      val thy2 = thy1 |> Theory.checkpoint;
   4.465 @@ -49,25 +488,23 @@
   4.466          ("Deriving properties for datatype(s) " ^ commas_quote new_type_names);
   4.467  
   4.468      val (exhaust, thy3) = thy2
   4.469 -      |> Datatype_Abs_Proofs.prove_casedist_thms config new_type_names
   4.470 -        descr induct (Datatype_Data.mk_case_names_exhausts flat_descr dt_names);
   4.471 +      |> prove_casedist_thms config new_type_names descr induct
   4.472 +        (Datatype_Data.mk_case_names_exhausts flat_descr dt_names);
   4.473      val (nchotomys, thy4) = thy3
   4.474 -      |> Datatype_Abs_Proofs.prove_nchotomys config new_type_names descr exhaust;
   4.475 +      |> prove_nchotomys config new_type_names descr exhaust;
   4.476      val ((rec_names, rec_rewrites), thy5) = thy4
   4.477 -      |> Datatype_Abs_Proofs.prove_primrec_thms
   4.478 -        config new_type_names descr (#inject o the o Symtab.lookup (Datatype_Data.get_all thy4))
   4.479 -        inject (distinct, Datatype_Data.all_distincts thy2 (Datatype_Aux.get_rec_types flat_descr))
   4.480 -        induct;
   4.481 +      |> prove_primrec_thms config new_type_names descr
   4.482 +        (#inject o the o Symtab.lookup (Datatype_Data.get_all thy4)) inject
   4.483 +        (distinct, Datatype_Data.all_distincts thy2 (Datatype_Aux.get_rec_types flat_descr)) induct;
   4.484      val ((case_rewrites, case_names), thy6) = thy5
   4.485 -      |> Datatype_Abs_Proofs.prove_case_thms config new_type_names descr rec_names rec_rewrites;
   4.486 +      |> prove_case_thms config new_type_names descr rec_names rec_rewrites;
   4.487      val (case_congs, thy7) = thy6
   4.488 -      |> Datatype_Abs_Proofs.prove_case_congs new_type_names case_names descr
   4.489 -        nchotomys case_rewrites;
   4.490 +      |> prove_case_congs new_type_names case_names descr nchotomys case_rewrites;
   4.491      val (weak_case_congs, thy8) = thy7
   4.492 -      |> Datatype_Abs_Proofs.prove_weak_case_congs new_type_names case_names descr;
   4.493 +      |> prove_weak_case_congs new_type_names case_names descr;
   4.494      val (splits, thy9) = thy8
   4.495 -      |> Datatype_Abs_Proofs.prove_split_thms
   4.496 -        config new_type_names case_names descr inject distinct exhaust case_rewrites;
   4.497 +      |> prove_split_thms config new_type_names case_names descr
   4.498 +        inject distinct exhaust case_rewrites;
   4.499  
   4.500      val inducts = Project_Rule.projections (Proof_Context.init_global thy2) induct;
   4.501      val dt_infos =
   4.502 @@ -106,6 +543,8 @@
   4.503      |> pair dt_names
   4.504    end;
   4.505  
   4.506 +end;
   4.507 +
   4.508  
   4.509  
   4.510  (** declare existing type as datatype **)