separate directory for datatype package
authorhaftmann
Wed Jun 10 15:04:33 2009 +0200 (2009-06-10)
changeset 31604eb2f9d709296
parent 31603 fa30cd74d7d6
child 31605 92d7a5094e23
separate directory for datatype package
src/HOL/Fun.thy
src/HOL/Inductive.thy
src/HOL/IsaMakefile
src/HOL/Product_Type.thy
src/HOL/Tools/datatype_package/datatype_abs_proofs.ML
src/HOL/Tools/datatype_package/datatype_case.ML
src/HOL/Tools/datatype_package/datatype_codegen.ML
src/HOL/Tools/datatype_package/datatype_package.ML
src/HOL/Tools/datatype_package/datatype_prop.ML
src/HOL/Tools/datatype_package/datatype_realizer.ML
src/HOL/Tools/datatype_package/datatype_rep_proofs.ML
     1.1 --- a/src/HOL/Fun.thy	Wed Jun 10 15:04:32 2009 +0200
     1.2 +++ b/src/HOL/Fun.thy	Wed Jun 10 15:04:33 2009 +0200
     1.3 @@ -133,7 +133,7 @@
     1.4    shows "inj f"
     1.5    using assms unfolding inj_on_def by auto
     1.6  
     1.7 -text{*For Proofs in @{text "Tools/datatype_rep_proofs"}*}
     1.8 +text{*For Proofs in @{text "Tools/datatype_package/datatype_rep_proofs"}*}
     1.9  lemma datatype_injI:
    1.10      "(!! x. ALL y. f(x) = f(y) --> x=y) ==> inj(f)"
    1.11  by (simp add: inj_on_def)
     2.1 --- a/src/HOL/Inductive.thy	Wed Jun 10 15:04:32 2009 +0200
     2.2 +++ b/src/HOL/Inductive.thy	Wed Jun 10 15:04:33 2009 +0200
     2.3 @@ -10,15 +10,15 @@
     2.4    ("Tools/inductive_package.ML")
     2.5    "Tools/dseq.ML"
     2.6    ("Tools/inductive_codegen.ML")
     2.7 -  ("Tools/datatype_aux.ML")
     2.8 -  ("Tools/datatype_prop.ML")
     2.9 -  ("Tools/datatype_rep_proofs.ML")
    2.10 -  ("Tools/datatype_abs_proofs.ML")
    2.11 -  ("Tools/datatype_case.ML")
    2.12 -  ("Tools/datatype_package.ML")
    2.13 +  ("Tools/datatype_package/datatype_aux.ML")
    2.14 +  ("Tools/datatype_package/datatype_prop.ML")
    2.15 +  ("Tools/datatype_package/datatype_rep_proofs.ML")
    2.16 +  ("Tools/datatype_package/datatype_abs_proofs.ML")
    2.17 +  ("Tools/datatype_package/datatype_case.ML")
    2.18 +  ("Tools/datatype_package/datatype_package.ML")
    2.19    ("Tools/old_primrec_package.ML")
    2.20    ("Tools/primrec_package.ML")
    2.21 -  ("Tools/datatype_codegen.ML")
    2.22 +  ("Tools/datatype_package/datatype_codegen.ML")
    2.23  begin
    2.24  
    2.25  subsection {* Least and greatest fixed points *}
    2.26 @@ -335,17 +335,18 @@
    2.27  
    2.28  text {* Package setup. *}
    2.29  
    2.30 -use "Tools/datatype_aux.ML"
    2.31 -use "Tools/datatype_prop.ML"
    2.32 -use "Tools/datatype_rep_proofs.ML"
    2.33 -use "Tools/datatype_abs_proofs.ML"
    2.34 -use "Tools/datatype_case.ML"
    2.35 -use "Tools/datatype_package.ML"
    2.36 +use "Tools/datatype_package/datatype_aux.ML"
    2.37 +use "Tools/datatype_package/datatype_prop.ML"
    2.38 +use "Tools/datatype_package/datatype_rep_proofs.ML"
    2.39 +use "Tools/datatype_package/datatype_abs_proofs.ML"
    2.40 +use "Tools/datatype_package/datatype_case.ML"
    2.41 +use "Tools/datatype_package/datatype_package.ML"
    2.42  setup DatatypePackage.setup
    2.43 +
    2.44  use "Tools/old_primrec_package.ML"
    2.45  use "Tools/primrec_package.ML"
    2.46  
    2.47 -use "Tools/datatype_codegen.ML"
    2.48 +use "Tools/datatype_package/datatype_codegen.ML"
    2.49  setup DatatypeCodegen.setup
    2.50  
    2.51  use "Tools/inductive_codegen.ML"
     3.1 --- a/src/HOL/IsaMakefile	Wed Jun 10 15:04:32 2009 +0200
     3.2 +++ b/src/HOL/IsaMakefile	Wed Jun 10 15:04:33 2009 +0200
     3.3 @@ -141,14 +141,14 @@
     3.4    Sum_Type.thy \
     3.5    Tools/arith_data.ML \
     3.6    Tools/cnf_funcs.ML \
     3.7 -  Tools/datatype_abs_proofs.ML \
     3.8 -  Tools/datatype_aux.ML \
     3.9 -  Tools/datatype_case.ML \
    3.10 -  Tools/datatype_codegen.ML \
    3.11 -  Tools/datatype_package.ML \
    3.12 -  Tools/datatype_prop.ML \
    3.13 -  Tools/datatype_realizer.ML \
    3.14 -  Tools/datatype_rep_proofs.ML \
    3.15 +  Tools/datatype_package/datatype_abs_proofs.ML \
    3.16 +  Tools/datatype_package/datatype_aux.ML \
    3.17 +  Tools/datatype_package/datatype_case.ML \
    3.18 +  Tools/datatype_package/datatype_codegen.ML \
    3.19 +  Tools/datatype_package/datatype_package.ML \
    3.20 +  Tools/datatype_package/datatype_prop.ML \
    3.21 +  Tools/datatype_package/datatype_realizer.ML \
    3.22 +  Tools/datatype_package/datatype_rep_proofs.ML \
    3.23    Tools/dseq.ML \
    3.24    Tools/function_package/auto_term.ML \
    3.25    Tools/function_package/context_tree.ML \
     4.1 --- a/src/HOL/Product_Type.thy	Wed Jun 10 15:04:32 2009 +0200
     4.2 +++ b/src/HOL/Product_Type.thy	Wed Jun 10 15:04:33 2009 +0200
     4.3 @@ -12,7 +12,7 @@
     4.4    ("Tools/split_rule.ML")
     4.5    ("Tools/inductive_set_package.ML")
     4.6    ("Tools/inductive_realizer.ML")
     4.7 -  ("Tools/datatype_realizer.ML")
     4.8 +  ("Tools/datatype_package/datatype_realizer.ML")
     4.9  begin
    4.10  
    4.11  subsection {* @{typ bool} is a datatype *}
    4.12 @@ -1155,7 +1155,7 @@
    4.13  use "Tools/inductive_set_package.ML"
    4.14  setup InductiveSetPackage.setup
    4.15  
    4.16 -use "Tools/datatype_realizer.ML"
    4.17 +use "Tools/datatype_package/datatype_realizer.ML"
    4.18  setup DatatypeRealizer.setup
    4.19  
    4.20  end
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Tools/datatype_package/datatype_abs_proofs.ML	Wed Jun 10 15:04:33 2009 +0200
     5.3 @@ -0,0 +1,446 @@
     5.4 +(*  Title:      HOL/Tools/datatype_abs_proofs.ML
     5.5 +    Author:     Stefan Berghofer, TU Muenchen
     5.6 +
     5.7 +Proofs and defintions independent of concrete representation
     5.8 +of datatypes  (i.e. requiring only abstract properties such as
     5.9 +injectivity / distinctness of constructors and induction)
    5.10 +
    5.11 + - case distinction (exhaustion) theorems
    5.12 + - characteristic equations for primrec combinators
    5.13 + - characteristic equations for case combinators
    5.14 + - equations for splitting "P (case ...)" expressions
    5.15 + - "nchotomy" and "case_cong" theorems for TFL
    5.16 +*)
    5.17 +
    5.18 +signature DATATYPE_ABS_PROOFS =
    5.19 +sig
    5.20 +  val prove_casedist_thms : string list ->
    5.21 +    DatatypeAux.descr list -> (string * sort) list -> thm ->
    5.22 +    attribute list -> theory -> thm list * theory
    5.23 +  val prove_primrec_thms : bool -> string list ->
    5.24 +    DatatypeAux.descr list -> (string * sort) list ->
    5.25 +      DatatypeAux.datatype_info Symtab.table -> thm list list -> thm list list ->
    5.26 +        simpset -> thm -> theory -> (string list * thm list) * theory
    5.27 +  val prove_case_thms : bool -> string list ->
    5.28 +    DatatypeAux.descr list -> (string * sort) list ->
    5.29 +      string list -> thm list -> theory -> (thm list list * string list) * theory
    5.30 +  val prove_split_thms : string list ->
    5.31 +    DatatypeAux.descr list -> (string * sort) list ->
    5.32 +      thm list list -> thm list list -> thm list -> thm list list -> theory ->
    5.33 +        (thm * thm) list * theory
    5.34 +  val prove_nchotomys : string list -> DatatypeAux.descr list ->
    5.35 +    (string * sort) list -> thm list -> theory -> thm list * theory
    5.36 +  val prove_weak_case_congs : string list -> DatatypeAux.descr list ->
    5.37 +    (string * sort) list -> theory -> thm list * theory
    5.38 +  val prove_case_congs : string list ->
    5.39 +    DatatypeAux.descr list -> (string * sort) list ->
    5.40 +      thm list -> thm list list -> theory -> thm list * theory
    5.41 +end;
    5.42 +
    5.43 +structure DatatypeAbsProofs: DATATYPE_ABS_PROOFS =
    5.44 +struct
    5.45 +
    5.46 +open DatatypeAux;
    5.47 +
    5.48 +(************************ case distinction theorems ***************************)
    5.49 +
    5.50 +fun prove_casedist_thms new_type_names descr sorts induct case_names_exhausts thy =
    5.51 +  let
    5.52 +    val _ = message "Proving case distinction theorems ...";
    5.53 +
    5.54 +    val descr' = List.concat descr;
    5.55 +    val recTs = get_rec_types descr' sorts;
    5.56 +    val newTs = Library.take (length (hd descr), recTs);
    5.57 +
    5.58 +    val {maxidx, ...} = rep_thm induct;
    5.59 +    val induct_Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct)));
    5.60 +
    5.61 +    fun prove_casedist_thm ((i, t), T) =
    5.62 +      let
    5.63 +        val dummyPs = map (fn (Var (_, Type (_, [T', T'']))) =>
    5.64 +          Abs ("z", T', Const ("True", T''))) induct_Ps;
    5.65 +        val P = Abs ("z", T, HOLogic.imp $ HOLogic.mk_eq (Var (("a", maxidx+1), T), Bound 0) $
    5.66 +          Var (("P", 0), HOLogic.boolT))
    5.67 +        val insts = Library.take (i, dummyPs) @ (P::(Library.drop (i + 1, dummyPs)));
    5.68 +        val cert = cterm_of thy;
    5.69 +        val insts' = (map cert induct_Ps) ~~ (map cert insts);
    5.70 +        val induct' = refl RS ((List.nth
    5.71 +          (split_conj_thm (cterm_instantiate insts' induct), i)) RSN (2, rev_mp))
    5.72 +
    5.73 +      in
    5.74 +        SkipProof.prove_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
    5.75 +          (fn {prems, ...} => EVERY
    5.76 +            [rtac induct' 1,
    5.77 +             REPEAT (rtac TrueI 1),
    5.78 +             REPEAT ((rtac impI 1) THEN (eresolve_tac prems 1)),
    5.79 +             REPEAT (rtac TrueI 1)])
    5.80 +      end;
    5.81 +
    5.82 +    val casedist_thms = map prove_casedist_thm ((0 upto (length newTs - 1)) ~~
    5.83 +      (DatatypeProp.make_casedists descr sorts) ~~ newTs)
    5.84 +  in
    5.85 +    thy
    5.86 +    |> store_thms_atts "exhaust" new_type_names (map single case_names_exhausts) casedist_thms
    5.87 +  end;
    5.88 +
    5.89 +
    5.90 +(*************************** primrec combinators ******************************)
    5.91 +
    5.92 +fun prove_primrec_thms flat_names new_type_names descr sorts
    5.93 +    (dt_info : datatype_info Symtab.table) constr_inject dist_rewrites dist_ss induct thy =
    5.94 +  let
    5.95 +    val _ = message "Constructing primrec combinators ...";
    5.96 +
    5.97 +    val big_name = space_implode "_" new_type_names;
    5.98 +    val thy0 = add_path flat_names big_name thy;
    5.99 +
   5.100 +    val descr' = List.concat descr;
   5.101 +    val recTs = get_rec_types descr' sorts;
   5.102 +    val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
   5.103 +    val newTs = Library.take (length (hd descr), recTs);
   5.104 +
   5.105 +    val induct_Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct)));
   5.106 +
   5.107 +    val big_rec_name' = big_name ^ "_rec_set";
   5.108 +    val rec_set_names' =
   5.109 +      if length descr' = 1 then [big_rec_name'] else
   5.110 +        map ((curry (op ^) (big_rec_name' ^ "_")) o string_of_int)
   5.111 +          (1 upto (length descr'));
   5.112 +    val rec_set_names = map (Sign.full_bname thy0) rec_set_names';
   5.113 +
   5.114 +    val (rec_result_Ts, reccomb_fn_Ts) = DatatypeProp.make_primrec_Ts descr sorts used;
   5.115 +
   5.116 +    val rec_set_Ts = map (fn (T1, T2) =>
   5.117 +      reccomb_fn_Ts @ [T1, T2] ---> HOLogic.boolT) (recTs ~~ rec_result_Ts);
   5.118 +
   5.119 +    val rec_fns = map (uncurry (mk_Free "f"))
   5.120 +      (reccomb_fn_Ts ~~ (1 upto (length reccomb_fn_Ts)));
   5.121 +    val rec_sets' = map (fn c => list_comb (Free c, rec_fns))
   5.122 +      (rec_set_names' ~~ rec_set_Ts);
   5.123 +    val rec_sets = map (fn c => list_comb (Const c, rec_fns))
   5.124 +      (rec_set_names ~~ rec_set_Ts);
   5.125 +
   5.126 +    (* introduction rules for graph of primrec function *)
   5.127 +
   5.128 +    fun make_rec_intr T rec_set ((rec_intr_ts, l), (cname, cargs)) =
   5.129 +      let
   5.130 +        fun mk_prem ((dt, U), (j, k, prems, t1s, t2s)) =
   5.131 +          let val free1 = mk_Free "x" U j
   5.132 +          in (case (strip_dtyp dt, strip_type U) of
   5.133 +             ((_, DtRec m), (Us, _)) =>
   5.134 +               let
   5.135 +                 val free2 = mk_Free "y" (Us ---> List.nth (rec_result_Ts, m)) k;
   5.136 +                 val i = length Us
   5.137 +               in (j + 1, k + 1, HOLogic.mk_Trueprop (HOLogic.list_all
   5.138 +                     (map (pair "x") Us, List.nth (rec_sets', m) $
   5.139 +                       app_bnds free1 i $ app_bnds free2 i)) :: prems,
   5.140 +                   free1::t1s, free2::t2s)
   5.141 +               end
   5.142 +           | _ => (j + 1, k, prems, free1::t1s, t2s))
   5.143 +          end;
   5.144 +
   5.145 +        val Ts = map (typ_of_dtyp descr' sorts) cargs;
   5.146 +        val (_, _, prems, t1s, t2s) = List.foldr mk_prem (1, 1, [], [], []) (cargs ~~ Ts)
   5.147 +
   5.148 +      in (rec_intr_ts @ [Logic.list_implies (prems, HOLogic.mk_Trueprop
   5.149 +        (rec_set $ list_comb (Const (cname, Ts ---> T), t1s) $
   5.150 +          list_comb (List.nth (rec_fns, l), t1s @ t2s)))], l + 1)
   5.151 +      end;
   5.152 +
   5.153 +    val (rec_intr_ts, _) = Library.foldl (fn (x, ((d, T), set_name)) =>
   5.154 +      Library.foldl (make_rec_intr T set_name) (x, #3 (snd d)))
   5.155 +        (([], 0), descr' ~~ recTs ~~ rec_sets');
   5.156 +
   5.157 +    val ({intrs = rec_intrs, elims = rec_elims, ...}, thy1) =
   5.158 +        InductivePackage.add_inductive_global (serial_string ())
   5.159 +          {quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK,
   5.160 +            alt_name = Binding.name big_rec_name', coind = false, no_elim = false, no_ind = true,
   5.161 +            skip_mono = true, fork_mono = false}
   5.162 +          (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
   5.163 +          (map dest_Free rec_fns)
   5.164 +          (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) [] thy0;
   5.165 +
   5.166 +    (* prove uniqueness and termination of primrec combinators *)
   5.167 +
   5.168 +    val _ = message "Proving termination and uniqueness of primrec functions ...";
   5.169 +
   5.170 +    fun mk_unique_tac ((tac, intrs), ((((i, (tname, _, constrs)), elim), T), T')) =
   5.171 +      let
   5.172 +        val distinct_tac =
   5.173 +          (if i < length newTs then
   5.174 +             full_simp_tac (HOL_ss addsimps (List.nth (dist_rewrites, i))) 1
   5.175 +           else full_simp_tac dist_ss 1);
   5.176 +
   5.177 +        val inject = map (fn r => r RS iffD1)
   5.178 +          (if i < length newTs then List.nth (constr_inject, i)
   5.179 +            else #inject (the (Symtab.lookup dt_info tname)));
   5.180 +
   5.181 +        fun mk_unique_constr_tac n ((tac, intr::intrs, j), (cname, cargs)) =
   5.182 +          let
   5.183 +            val k = length (List.filter is_rec_type cargs)
   5.184 +
   5.185 +          in (EVERY [DETERM tac,
   5.186 +                REPEAT (etac ex1E 1), rtac ex1I 1,
   5.187 +                DEPTH_SOLVE_1 (ares_tac [intr] 1),
   5.188 +                REPEAT_DETERM_N k (etac thin_rl 1 THEN rotate_tac 1 1),
   5.189 +                etac elim 1,
   5.190 +                REPEAT_DETERM_N j distinct_tac,
   5.191 +                TRY (dresolve_tac inject 1),
   5.192 +                REPEAT (etac conjE 1), hyp_subst_tac 1,
   5.193 +                REPEAT (EVERY [etac allE 1, dtac mp 1, atac 1]),
   5.194 +                TRY (hyp_subst_tac 1),
   5.195 +                rtac refl 1,
   5.196 +                REPEAT_DETERM_N (n - j - 1) distinct_tac],
   5.197 +              intrs, j + 1)
   5.198 +          end;
   5.199 +
   5.200 +        val (tac', intrs', _) = Library.foldl (mk_unique_constr_tac (length constrs))
   5.201 +          ((tac, intrs, 0), constrs);
   5.202 +
   5.203 +      in (tac', intrs') end;
   5.204 +
   5.205 +    val rec_unique_thms =
   5.206 +      let
   5.207 +        val rec_unique_ts = map (fn (((set_t, T1), T2), i) =>
   5.208 +          Const ("Ex1", (T2 --> HOLogic.boolT) --> HOLogic.boolT) $
   5.209 +            absfree ("y", T2, set_t $ mk_Free "x" T1 i $ Free ("y", T2)))
   5.210 +              (rec_sets ~~ recTs ~~ rec_result_Ts ~~ (1 upto length recTs));
   5.211 +        val cert = cterm_of thy1
   5.212 +        val insts = map (fn ((i, T), t) => absfree ("x" ^ (string_of_int i), T, t))
   5.213 +          ((1 upto length recTs) ~~ recTs ~~ rec_unique_ts);
   5.214 +        val induct' = cterm_instantiate ((map cert induct_Ps) ~~
   5.215 +          (map cert insts)) induct;
   5.216 +        val (tac, _) = Library.foldl mk_unique_tac
   5.217 +          (((rtac induct' THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1
   5.218 +              THEN rewrite_goals_tac [mk_meta_eq choice_eq], rec_intrs),
   5.219 +            descr' ~~ rec_elims ~~ recTs ~~ rec_result_Ts);
   5.220 +
   5.221 +      in split_conj_thm (SkipProof.prove_global thy1 [] []
   5.222 +        (HOLogic.mk_Trueprop (mk_conj rec_unique_ts)) (K tac))
   5.223 +      end;
   5.224 +
   5.225 +    val rec_total_thms = map (fn r => r RS theI') rec_unique_thms;
   5.226 +
   5.227 +    (* define primrec combinators *)
   5.228 +
   5.229 +    val big_reccomb_name = (space_implode "_" new_type_names) ^ "_rec";
   5.230 +    val reccomb_names = map (Sign.full_bname thy1)
   5.231 +      (if length descr' = 1 then [big_reccomb_name] else
   5.232 +        (map ((curry (op ^) (big_reccomb_name ^ "_")) o string_of_int)
   5.233 +          (1 upto (length descr'))));
   5.234 +    val reccombs = map (fn ((name, T), T') => list_comb
   5.235 +      (Const (name, reccomb_fn_Ts @ [T] ---> T'), rec_fns))
   5.236 +        (reccomb_names ~~ recTs ~~ rec_result_Ts);
   5.237 +
   5.238 +    val (reccomb_defs, thy2) =
   5.239 +      thy1
   5.240 +      |> Sign.add_consts_i (map (fn ((name, T), T') =>
   5.241 +          (Binding.name (Long_Name.base_name name), reccomb_fn_Ts @ [T] ---> T', NoSyn))
   5.242 +          (reccomb_names ~~ recTs ~~ rec_result_Ts))
   5.243 +      |> (PureThy.add_defs false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') =>
   5.244 +          (Binding.name (Long_Name.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T,
   5.245 +           Const ("The", (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
   5.246 +             set $ Free ("x", T) $ Free ("y", T'))))))
   5.247 +               (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts))
   5.248 +      ||> parent_path flat_names
   5.249 +      ||> Theory.checkpoint;
   5.250 +
   5.251 +
   5.252 +    (* prove characteristic equations for primrec combinators *)
   5.253 +
   5.254 +    val _ = message "Proving characteristic theorems for primrec combinators ..."
   5.255 +
   5.256 +    val rec_thms = map (fn t => SkipProof.prove_global thy2 [] [] t
   5.257 +      (fn _ => EVERY
   5.258 +        [rewrite_goals_tac reccomb_defs,
   5.259 +         rtac the1_equality 1,
   5.260 +         resolve_tac rec_unique_thms 1,
   5.261 +         resolve_tac rec_intrs 1,
   5.262 +         REPEAT (rtac allI 1 ORELSE resolve_tac rec_total_thms 1)]))
   5.263 +           (DatatypeProp.make_primrecs new_type_names descr sorts thy2)
   5.264 +
   5.265 +  in
   5.266 +    thy2
   5.267 +    |> Sign.add_path (space_implode "_" new_type_names)
   5.268 +    |> PureThy.add_thmss [((Binding.name "recs", rec_thms),
   5.269 +         [Nitpick_Const_Simp_Thms.add])]
   5.270 +    ||> Sign.parent_path
   5.271 +    ||> Theory.checkpoint
   5.272 +    |-> (fn thms => pair (reccomb_names, Library.flat thms))
   5.273 +  end;
   5.274 +
   5.275 +
   5.276 +(***************************** case combinators *******************************)
   5.277 +
   5.278 +fun prove_case_thms flat_names new_type_names descr sorts reccomb_names primrec_thms thy =
   5.279 +  let
   5.280 +    val _ = message "Proving characteristic theorems for case combinators ...";
   5.281 +
   5.282 +    val thy1 = add_path flat_names (space_implode "_" new_type_names) thy;
   5.283 +
   5.284 +    val descr' = List.concat descr;
   5.285 +    val recTs = get_rec_types descr' sorts;
   5.286 +    val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
   5.287 +    val newTs = Library.take (length (hd descr), recTs);
   5.288 +    val T' = TFree (Name.variant used "'t", HOLogic.typeS);
   5.289 +
   5.290 +    fun mk_dummyT dt = binder_types (typ_of_dtyp descr' sorts dt) ---> T';
   5.291 +
   5.292 +    val case_dummy_fns = map (fn (_, (_, _, constrs)) => map (fn (_, cargs) =>
   5.293 +      let
   5.294 +        val Ts = map (typ_of_dtyp descr' sorts) cargs;
   5.295 +        val Ts' = map mk_dummyT (List.filter is_rec_type cargs)
   5.296 +      in Const (@{const_name undefined}, Ts @ Ts' ---> T')
   5.297 +      end) constrs) descr';
   5.298 +
   5.299 +    val case_names = map (fn s => Sign.full_bname thy1 (s ^ "_case")) new_type_names;
   5.300 +
   5.301 +    (* define case combinators via primrec combinators *)
   5.302 +
   5.303 +    val (case_defs, thy2) = Library.foldl (fn ((defs, thy),
   5.304 +      ((((i, (_, _, constrs)), T), name), recname)) =>
   5.305 +        let
   5.306 +          val (fns1, fns2) = ListPair.unzip (map (fn ((_, cargs), j) =>
   5.307 +            let
   5.308 +              val Ts = map (typ_of_dtyp descr' sorts) cargs;
   5.309 +              val Ts' = Ts @ map mk_dummyT (List.filter is_rec_type cargs);
   5.310 +              val frees' = map (uncurry (mk_Free "x")) (Ts' ~~ (1 upto length Ts'));
   5.311 +              val frees = Library.take (length cargs, frees');
   5.312 +              val free = mk_Free "f" (Ts ---> T') j
   5.313 +            in
   5.314 +             (free, list_abs_free (map dest_Free frees',
   5.315 +               list_comb (free, frees)))
   5.316 +            end) (constrs ~~ (1 upto length constrs)));
   5.317 +
   5.318 +          val caseT = (map (snd o dest_Free) fns1) @ [T] ---> T';
   5.319 +          val fns = (List.concat (Library.take (i, case_dummy_fns))) @
   5.320 +            fns2 @ (List.concat (Library.drop (i + 1, case_dummy_fns)));
   5.321 +          val reccomb = Const (recname, (map fastype_of fns) @ [T] ---> T');
   5.322 +          val decl = ((Binding.name (Long_Name.base_name name), caseT), NoSyn);
   5.323 +          val def = (Binding.name (Long_Name.base_name name ^ "_def"),
   5.324 +            Logic.mk_equals (list_comb (Const (name, caseT), fns1),
   5.325 +              list_comb (reccomb, (List.concat (Library.take (i, case_dummy_fns))) @
   5.326 +                fns2 @ (List.concat (Library.drop (i + 1, case_dummy_fns))) )));
   5.327 +          val ([def_thm], thy') =
   5.328 +            thy
   5.329 +            |> Sign.declare_const [] decl |> snd
   5.330 +            |> (PureThy.add_defs false o map Thm.no_attributes) [def];
   5.331 +
   5.332 +        in (defs @ [def_thm], thy')
   5.333 +        end) (([], thy1), (hd descr) ~~ newTs ~~ case_names ~~
   5.334 +          (Library.take (length newTs, reccomb_names)))
   5.335 +      ||> Theory.checkpoint;
   5.336 +
   5.337 +    val case_thms = map (map (fn t => SkipProof.prove_global thy2 [] [] t
   5.338 +      (fn _ => EVERY [rewrite_goals_tac (case_defs @ map mk_meta_eq primrec_thms), rtac refl 1])))
   5.339 +          (DatatypeProp.make_cases new_type_names descr sorts thy2)
   5.340 +  in
   5.341 +    thy2
   5.342 +    |> Context.the_theory o fold (fold Nitpick_Const_Simp_Thms.add_thm) case_thms
   5.343 +       o Context.Theory
   5.344 +    |> parent_path flat_names
   5.345 +    |> store_thmss "cases" new_type_names case_thms
   5.346 +    |-> (fn thmss => pair (thmss, case_names))
   5.347 +  end;
   5.348 +
   5.349 +
   5.350 +(******************************* case splitting *******************************)
   5.351 +
   5.352 +fun prove_split_thms new_type_names descr sorts constr_inject dist_rewrites
   5.353 +    casedist_thms case_thms thy =
   5.354 +  let
   5.355 +    val _ = message "Proving equations for case splitting ...";
   5.356 +
   5.357 +    val descr' = List.concat descr;
   5.358 +    val recTs = get_rec_types descr' sorts;
   5.359 +    val newTs = Library.take (length (hd descr), recTs);
   5.360 +
   5.361 +    fun prove_split_thms ((((((t1, t2), inject), dist_rewrites'),
   5.362 +        exhaustion), case_thms'), T) =
   5.363 +      let
   5.364 +        val cert = cterm_of thy;
   5.365 +        val _ $ (_ $ lhs $ _) = hd (Logic.strip_assums_hyp (hd (prems_of exhaustion)));
   5.366 +        val exhaustion' = cterm_instantiate
   5.367 +          [(cert lhs, cert (Free ("x", T)))] exhaustion;
   5.368 +        val tacf = K (EVERY [rtac exhaustion' 1, ALLGOALS (asm_simp_tac
   5.369 +          (HOL_ss addsimps (dist_rewrites' @ inject @ case_thms')))])
   5.370 +      in
   5.371 +        (SkipProof.prove_global thy [] [] t1 tacf,
   5.372 +         SkipProof.prove_global thy [] [] t2 tacf)
   5.373 +      end;
   5.374 +
   5.375 +    val split_thm_pairs = map prove_split_thms
   5.376 +      ((DatatypeProp.make_splits new_type_names descr sorts thy) ~~ constr_inject ~~
   5.377 +        dist_rewrites ~~ casedist_thms ~~ case_thms ~~ newTs);
   5.378 +
   5.379 +    val (split_thms, split_asm_thms) = ListPair.unzip split_thm_pairs
   5.380 +
   5.381 +  in
   5.382 +    thy
   5.383 +    |> store_thms "split" new_type_names split_thms
   5.384 +    ||>> store_thms "split_asm" new_type_names split_asm_thms
   5.385 +    |-> (fn (thms1, thms2) => pair (thms1 ~~ thms2))
   5.386 +  end;
   5.387 +
   5.388 +fun prove_weak_case_congs new_type_names descr sorts thy =
   5.389 +  let
   5.390 +    fun prove_weak_case_cong t =
   5.391 +       SkipProof.prove_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
   5.392 +         (fn {prems, ...} => EVERY [rtac ((hd prems) RS arg_cong) 1])
   5.393 +
   5.394 +    val weak_case_congs = map prove_weak_case_cong (DatatypeProp.make_weak_case_congs
   5.395 +      new_type_names descr sorts thy)
   5.396 +
   5.397 +  in thy |> store_thms "weak_case_cong" new_type_names weak_case_congs end;
   5.398 +
   5.399 +(************************* additional theorems for TFL ************************)
   5.400 +
   5.401 +fun prove_nchotomys new_type_names descr sorts casedist_thms thy =
   5.402 +  let
   5.403 +    val _ = message "Proving additional theorems for TFL ...";
   5.404 +
   5.405 +    fun prove_nchotomy (t, exhaustion) =
   5.406 +      let
   5.407 +        (* For goal i, select the correct disjunct to attack, then prove it *)
   5.408 +        fun tac i 0 = EVERY [TRY (rtac disjI1 i),
   5.409 +              hyp_subst_tac i, REPEAT (rtac exI i), rtac refl i]
   5.410 +          | tac i n = rtac disjI2 i THEN tac i (n - 1)
   5.411 +      in 
   5.412 +        SkipProof.prove_global thy [] [] t (fn _ =>
   5.413 +          EVERY [rtac allI 1,
   5.414 +           exh_tac (K exhaustion) 1,
   5.415 +           ALLGOALS (fn i => tac i (i-1))])
   5.416 +      end;
   5.417 +
   5.418 +    val nchotomys =
   5.419 +      map prove_nchotomy (DatatypeProp.make_nchotomys descr sorts ~~ casedist_thms)
   5.420 +
   5.421 +  in thy |> store_thms "nchotomy" new_type_names nchotomys end;
   5.422 +
   5.423 +fun prove_case_congs new_type_names descr sorts nchotomys case_thms thy =
   5.424 +  let
   5.425 +    fun prove_case_cong ((t, nchotomy), case_rewrites) =
   5.426 +      let
   5.427 +        val (Const ("==>", _) $ tm $ _) = t;
   5.428 +        val (Const ("Trueprop", _) $ (Const ("op =", _) $ _ $ Ma)) = tm;
   5.429 +        val cert = cterm_of thy;
   5.430 +        val nchotomy' = nchotomy RS spec;
   5.431 +        val [v] = Term.add_vars (concl_of nchotomy') [];
   5.432 +        val nchotomy'' = cterm_instantiate [(cert (Var v), cert Ma)] nchotomy'
   5.433 +      in
   5.434 +        SkipProof.prove_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
   5.435 +          (fn {prems, ...} => 
   5.436 +            let val simplify = asm_simp_tac (HOL_ss addsimps (prems @ case_rewrites))
   5.437 +            in EVERY [simp_tac (HOL_ss addsimps [hd prems]) 1,
   5.438 +                cut_facts_tac [nchotomy''] 1,
   5.439 +                REPEAT (etac disjE 1 THEN REPEAT (etac exE 1) THEN simplify 1),
   5.440 +                REPEAT (etac exE 1) THEN simplify 1 (* Get last disjunct *)]
   5.441 +            end)
   5.442 +      end;
   5.443 +
   5.444 +    val case_congs = map prove_case_cong (DatatypeProp.make_case_congs
   5.445 +      new_type_names descr sorts thy ~~ nchotomys ~~ case_thms)
   5.446 +
   5.447 +  in thy |> store_thms "case_cong" new_type_names case_congs end;
   5.448 +
   5.449 +end;
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Tools/datatype_package/datatype_case.ML	Wed Jun 10 15:04:33 2009 +0200
     6.3 @@ -0,0 +1,469 @@
     6.4 +(*  Title:      HOL/Tools/datatype_case.ML
     6.5 +    Author:     Konrad Slind, Cambridge University Computer Laboratory
     6.6 +    Author:     Stefan Berghofer, TU Muenchen
     6.7 +
     6.8 +Nested case expressions on datatypes.
     6.9 +*)
    6.10 +
    6.11 +signature DATATYPE_CASE =
    6.12 +sig
    6.13 +  val make_case: (string -> DatatypeAux.datatype_info option) ->
    6.14 +    Proof.context -> bool -> string list -> term -> (term * term) list ->
    6.15 +    term * (term * (int * bool)) list
    6.16 +  val dest_case: (string -> DatatypeAux.datatype_info option) -> bool ->
    6.17 +    string list -> term -> (term * (term * term) list) option
    6.18 +  val strip_case: (string -> DatatypeAux.datatype_info option) -> bool ->
    6.19 +    term -> (term * (term * term) list) option
    6.20 +  val case_tr: bool -> (theory -> string -> DatatypeAux.datatype_info option)
    6.21 +    -> Proof.context -> term list -> term
    6.22 +  val case_tr': (theory -> string -> DatatypeAux.datatype_info option) ->
    6.23 +    string -> Proof.context -> term list -> term
    6.24 +end;
    6.25 +
    6.26 +structure DatatypeCase : DATATYPE_CASE =
    6.27 +struct
    6.28 +
    6.29 +exception CASE_ERROR of string * int;
    6.30 +
    6.31 +fun match_type thy pat ob = Sign.typ_match thy (pat, ob) Vartab.empty;
    6.32 +
    6.33 +(*---------------------------------------------------------------------------
    6.34 + * Get information about datatypes
    6.35 + *---------------------------------------------------------------------------*)
    6.36 +
    6.37 +fun ty_info (tab : string -> DatatypeAux.datatype_info option) s =
    6.38 +  case tab s of
    6.39 +    SOME {descr, case_name, index, sorts, ...} =>
    6.40 +      let
    6.41 +        val (_, (tname, dts, constrs)) = nth descr index;
    6.42 +        val mk_ty = DatatypeAux.typ_of_dtyp descr sorts;
    6.43 +        val T = Type (tname, map mk_ty dts)
    6.44 +      in
    6.45 +        SOME {case_name = case_name,
    6.46 +          constructors = map (fn (cname, dts') =>
    6.47 +            Const (cname, Logic.varifyT (map mk_ty dts' ---> T))) constrs}
    6.48 +      end
    6.49 +  | NONE => NONE;
    6.50 +
    6.51 +
    6.52 +(*---------------------------------------------------------------------------
    6.53 + * Each pattern carries with it a tag (i,b) where
    6.54 + * i is the clause it came from and
    6.55 + * b=true indicates that clause was given by the user
    6.56 + * (or is an instantiation of a user supplied pattern)
    6.57 + * b=false --> i = ~1
    6.58 + *---------------------------------------------------------------------------*)
    6.59 +
    6.60 +fun pattern_subst theta (tm, x) = (subst_free theta tm, x);
    6.61 +
    6.62 +fun row_of_pat x = fst (snd x);
    6.63 +
    6.64 +fun add_row_used ((prfx, pats), (tm, tag)) =
    6.65 +  fold Term.add_free_names (tm :: pats @ prfx);
    6.66 +
    6.67 +(* try to preserve names given by user *)
    6.68 +fun default_names names ts =
    6.69 +  map (fn ("", Free (name', _)) => name' | (name, _) => name) (names ~~ ts);
    6.70 +
    6.71 +fun strip_constraints (Const ("_constrain", _) $ t $ tT) =
    6.72 +      strip_constraints t ||> cons tT
    6.73 +  | strip_constraints t = (t, []);
    6.74 +
    6.75 +fun mk_fun_constrain tT t = Syntax.const "_constrain" $ t $
    6.76 +  (Syntax.free "fun" $ tT $ Syntax.free "dummy");
    6.77 +
    6.78 +
    6.79 +(*---------------------------------------------------------------------------
    6.80 + * Produce an instance of a constructor, plus genvars for its arguments.
    6.81 + *---------------------------------------------------------------------------*)
    6.82 +fun fresh_constr ty_match ty_inst colty used c =
    6.83 +  let
    6.84 +    val (_, Ty) = dest_Const c
    6.85 +    val Ts = binder_types Ty;
    6.86 +    val names = Name.variant_list used
    6.87 +      (DatatypeProp.make_tnames (map Logic.unvarifyT Ts));
    6.88 +    val ty = body_type Ty;
    6.89 +    val ty_theta = ty_match ty colty handle Type.TYPE_MATCH =>
    6.90 +      raise CASE_ERROR ("type mismatch", ~1)
    6.91 +    val c' = ty_inst ty_theta c
    6.92 +    val gvars = map (ty_inst ty_theta o Free) (names ~~ Ts)
    6.93 +  in (c', gvars)
    6.94 +  end;
    6.95 +
    6.96 +
    6.97 +(*---------------------------------------------------------------------------
    6.98 + * Goes through a list of rows and picks out the ones beginning with a
    6.99 + * pattern with constructor = name.
   6.100 + *---------------------------------------------------------------------------*)
   6.101 +fun mk_group (name, T) rows =
   6.102 +  let val k = length (binder_types T)
   6.103 +  in fold (fn (row as ((prfx, p :: rst), rhs as (_, (i, _)))) =>
   6.104 +    fn ((in_group, not_in_group), (names, cnstrts)) => (case strip_comb p of
   6.105 +        (Const (name', _), args) =>
   6.106 +          if name = name' then
   6.107 +            if length args = k then
   6.108 +              let val (args', cnstrts') = split_list (map strip_constraints args)
   6.109 +              in
   6.110 +                ((((prfx, args' @ rst), rhs) :: in_group, not_in_group),
   6.111 +                 (default_names names args', map2 append cnstrts cnstrts'))
   6.112 +              end
   6.113 +            else raise CASE_ERROR
   6.114 +              ("Wrong number of arguments for constructor " ^ name, i)
   6.115 +          else ((in_group, row :: not_in_group), (names, cnstrts))
   6.116 +      | _ => raise CASE_ERROR ("Not a constructor pattern", i)))
   6.117 +    rows (([], []), (replicate k "", replicate k [])) |>> pairself rev
   6.118 +  end;
   6.119 +
   6.120 +(*---------------------------------------------------------------------------
   6.121 + * Partition the rows. Not efficient: we should use hashing.
   6.122 + *---------------------------------------------------------------------------*)
   6.123 +fun partition _ _ _ _ _ _ _ [] = raise CASE_ERROR ("partition: no rows", ~1)
   6.124 +  | partition ty_match ty_inst type_of used constructors colty res_ty
   6.125 +        (rows as (((prfx, _ :: rstp), _) :: _)) =
   6.126 +      let
   6.127 +        fun part {constrs = [], rows = [], A} = rev A
   6.128 +          | part {constrs = [], rows = (_, (_, (i, _))) :: _, A} =
   6.129 +              raise CASE_ERROR ("Not a constructor pattern", i)
   6.130 +          | part {constrs = c :: crst, rows, A} =
   6.131 +              let
   6.132 +                val ((in_group, not_in_group), (names, cnstrts)) =
   6.133 +                  mk_group (dest_Const c) rows;
   6.134 +                val used' = fold add_row_used in_group used;
   6.135 +                val (c', gvars) = fresh_constr ty_match ty_inst colty used' c;
   6.136 +                val in_group' =
   6.137 +                  if null in_group  (* Constructor not given *)
   6.138 +                  then
   6.139 +                    let
   6.140 +                      val Ts = map type_of rstp;
   6.141 +                      val xs = Name.variant_list
   6.142 +                        (fold Term.add_free_names gvars used')
   6.143 +                        (replicate (length rstp) "x")
   6.144 +                    in
   6.145 +                      [((prfx, gvars @ map Free (xs ~~ Ts)),
   6.146 +                        (Const ("HOL.undefined", res_ty), (~1, false)))]
   6.147 +                    end
   6.148 +                  else in_group
   6.149 +              in
   6.150 +                part{constrs = crst,
   6.151 +                  rows = not_in_group,
   6.152 +                  A = {constructor = c',
   6.153 +                    new_formals = gvars,
   6.154 +                    names = names,
   6.155 +                    constraints = cnstrts,
   6.156 +                    group = in_group'} :: A}
   6.157 +              end
   6.158 +      in part {constrs = constructors, rows = rows, A = []}
   6.159 +      end;
   6.160 +
   6.161 +(*---------------------------------------------------------------------------
   6.162 + * Misc. routines used in mk_case
   6.163 + *---------------------------------------------------------------------------*)
   6.164 +
   6.165 +fun mk_pat ((c, c'), l) =
   6.166 +  let
   6.167 +    val L = length (binder_types (fastype_of c))
   6.168 +    fun build (prfx, tag, plist) =
   6.169 +      let val (args, plist') = chop L plist
   6.170 +      in (prfx, tag, list_comb (c', args) :: plist') end
   6.171 +  in map build l end;
   6.172 +
   6.173 +fun v_to_prfx (prfx, v::pats) = (v::prfx,pats)
   6.174 +  | v_to_prfx _ = raise CASE_ERROR ("mk_case: v_to_prfx", ~1);
   6.175 +
   6.176 +fun v_to_pats (v::prfx,tag, pats) = (prfx, tag, v::pats)
   6.177 +  | v_to_pats _ = raise CASE_ERROR ("mk_case: v_to_pats", ~1);
   6.178 +
   6.179 +
   6.180 +(*----------------------------------------------------------------------------
   6.181 + * Translation of pattern terms into nested case expressions.
   6.182 + *
   6.183 + * This performs the translation and also builds the full set of patterns.
   6.184 + * Thus it supports the construction of induction theorems even when an
   6.185 + * incomplete set of patterns is given.
   6.186 + *---------------------------------------------------------------------------*)
   6.187 +
   6.188 +fun mk_case tab ctxt ty_match ty_inst type_of used range_ty =
   6.189 +  let
   6.190 +    val name = Name.variant used "a";
   6.191 +    fun expand constructors used ty ((_, []), _) =
   6.192 +          raise CASE_ERROR ("mk_case: expand_var_row", ~1)
   6.193 +      | expand constructors used ty (row as ((prfx, p :: rst), rhs)) =
   6.194 +          if is_Free p then
   6.195 +            let
   6.196 +              val used' = add_row_used row used;
   6.197 +              fun expnd c =
   6.198 +                let val capp =
   6.199 +                  list_comb (fresh_constr ty_match ty_inst ty used' c)
   6.200 +                in ((prfx, capp :: rst), pattern_subst [(p, capp)] rhs)
   6.201 +                end
   6.202 +            in map expnd constructors end
   6.203 +          else [row]
   6.204 +    fun mk {rows = [], ...} = raise CASE_ERROR ("no rows", ~1)
   6.205 +      | mk {path = [], rows = ((prfx, []), (tm, tag)) :: _} =  (* Done *)
   6.206 +          ([(prfx, tag, [])], tm)
   6.207 +      | mk {path, rows as ((row as ((_, [Free _]), _)) :: _ :: _)} =
   6.208 +          mk {path = path, rows = [row]}
   6.209 +      | mk {path = u :: rstp, rows as ((_, _ :: _), _) :: _} =
   6.210 +          let val col0 = map (fn ((_, p :: _), (_, (i, _))) => (p, i)) rows
   6.211 +          in case Option.map (apfst head_of)
   6.212 +            (find_first (not o is_Free o fst) col0) of
   6.213 +              NONE =>
   6.214 +                let
   6.215 +                  val rows' = map (fn ((v, _), row) => row ||>
   6.216 +                    pattern_subst [(v, u)] |>> v_to_prfx) (col0 ~~ rows);
   6.217 +                  val (pref_patl, tm) = mk {path = rstp, rows = rows'}
   6.218 +                in (map v_to_pats pref_patl, tm) end
   6.219 +            | SOME (Const (cname, cT), i) => (case ty_info tab cname of
   6.220 +                NONE => raise CASE_ERROR ("Not a datatype constructor: " ^ cname, i)
   6.221 +              | SOME {case_name, constructors} =>
   6.222 +                let
   6.223 +                  val pty = body_type cT;
   6.224 +                  val used' = fold Term.add_free_names rstp used;
   6.225 +                  val nrows = maps (expand constructors used' pty) rows;
   6.226 +                  val subproblems = partition ty_match ty_inst type_of used'
   6.227 +                    constructors pty range_ty nrows;
   6.228 +                  val new_formals = map #new_formals subproblems
   6.229 +                  val constructors' = map #constructor subproblems
   6.230 +                  val news = map (fn {new_formals, group, ...} =>
   6.231 +                    {path = new_formals @ rstp, rows = group}) subproblems;
   6.232 +                  val (pat_rect, dtrees) = split_list (map mk news);
   6.233 +                  val case_functions = map2
   6.234 +                    (fn {new_formals, names, constraints, ...} =>
   6.235 +                       fold_rev (fn ((x as Free (_, T), s), cnstrts) => fn t =>
   6.236 +                         Abs (if s = "" then name else s, T,
   6.237 +                           abstract_over (x, t)) |>
   6.238 +                         fold mk_fun_constrain cnstrts)
   6.239 +                           (new_formals ~~ names ~~ constraints))
   6.240 +                    subproblems dtrees;
   6.241 +                  val types = map type_of (case_functions @ [u]);
   6.242 +                  val case_const = Const (case_name, types ---> range_ty)
   6.243 +                  val tree = list_comb (case_const, case_functions @ [u])
   6.244 +                  val pat_rect1 = flat (map mk_pat
   6.245 +                    (constructors ~~ constructors' ~~ pat_rect))
   6.246 +                in (pat_rect1, tree)
   6.247 +                end)
   6.248 +            | SOME (t, i) => raise CASE_ERROR ("Not a datatype constructor: " ^
   6.249 +                Syntax.string_of_term ctxt t, i)
   6.250 +          end
   6.251 +      | mk _ = raise CASE_ERROR ("Malformed row matrix", ~1)
   6.252 +  in mk
   6.253 +  end;
   6.254 +
   6.255 +fun case_error s = error ("Error in case expression:\n" ^ s);
   6.256 +
   6.257 +(* Repeated variable occurrences in a pattern are not allowed. *)
   6.258 +fun no_repeat_vars ctxt pat = fold_aterms
   6.259 +  (fn x as Free (s, _) => (fn xs =>
   6.260 +        if member op aconv xs x then
   6.261 +          case_error (quote s ^ " occurs repeatedly in the pattern " ^
   6.262 +            quote (Syntax.string_of_term ctxt pat))
   6.263 +        else x :: xs)
   6.264 +    | _ => I) pat [];
   6.265 +
   6.266 +fun gen_make_case ty_match ty_inst type_of tab ctxt err used x clauses =
   6.267 +  let
   6.268 +    fun string_of_clause (pat, rhs) = Syntax.string_of_term ctxt
   6.269 +      (Syntax.const "_case1" $ pat $ rhs);
   6.270 +    val _ = map (no_repeat_vars ctxt o fst) clauses;
   6.271 +    val rows = map_index (fn (i, (pat, rhs)) =>
   6.272 +      (([], [pat]), (rhs, (i, true)))) clauses;
   6.273 +    val rangeT = (case distinct op = (map (type_of o snd) clauses) of
   6.274 +        [] => case_error "no clauses given"
   6.275 +      | [T] => T
   6.276 +      | _ => case_error "all cases must have the same result type");
   6.277 +    val used' = fold add_row_used rows used;
   6.278 +    val (patts, case_tm) = mk_case tab ctxt ty_match ty_inst type_of
   6.279 +        used' rangeT {path = [x], rows = rows}
   6.280 +      handle CASE_ERROR (msg, i) => case_error (msg ^
   6.281 +        (if i < 0 then ""
   6.282 +         else "\nIn clause\n" ^ string_of_clause (nth clauses i)));
   6.283 +    val patts1 = map
   6.284 +      (fn (_, tag, [pat]) => (pat, tag)
   6.285 +        | _ => case_error "error in pattern-match translation") patts;
   6.286 +    val patts2 = Library.sort (Library.int_ord o Library.pairself row_of_pat) patts1
   6.287 +    val finals = map row_of_pat patts2
   6.288 +    val originals = map (row_of_pat o #2) rows
   6.289 +    val _ = case originals \\ finals of
   6.290 +        [] => ()
   6.291 +      | is => (if err then case_error else warning)
   6.292 +          ("The following clauses are redundant (covered by preceding clauses):\n" ^
   6.293 +           cat_lines (map (string_of_clause o nth clauses) is));
   6.294 +  in
   6.295 +    (case_tm, patts2)
   6.296 +  end;
   6.297 +
   6.298 +fun make_case tab ctxt = gen_make_case
   6.299 +  (match_type (ProofContext.theory_of ctxt)) Envir.subst_TVars fastype_of tab ctxt;
   6.300 +val make_case_untyped = gen_make_case (K (K Vartab.empty))
   6.301 +  (K (Term.map_types (K dummyT))) (K dummyT);
   6.302 +
   6.303 +
   6.304 +(* parse translation *)
   6.305 +
   6.306 +fun case_tr err tab_of ctxt [t, u] =
   6.307 +    let
   6.308 +      val thy = ProofContext.theory_of ctxt;
   6.309 +      (* replace occurrences of dummy_pattern by distinct variables *)
   6.310 +      (* internalize constant names                                 *)
   6.311 +      fun prep_pat ((c as Const ("_constrain", _)) $ t $ tT) used =
   6.312 +            let val (t', used') = prep_pat t used
   6.313 +            in (c $ t' $ tT, used') end
   6.314 +        | prep_pat (Const ("dummy_pattern", T)) used =
   6.315 +            let val x = Name.variant used "x"
   6.316 +            in (Free (x, T), x :: used) end
   6.317 +        | prep_pat (Const (s, T)) used =
   6.318 +            (case try (unprefix Syntax.constN) s of
   6.319 +               SOME c => (Const (c, T), used)
   6.320 +             | NONE => (Const (Sign.intern_const thy s, T), used))
   6.321 +        | prep_pat (v as Free (s, T)) used =
   6.322 +            let val s' = Sign.intern_const thy s
   6.323 +            in
   6.324 +              if Sign.declared_const thy s' then
   6.325 +                (Const (s', T), used)
   6.326 +              else (v, used)
   6.327 +            end
   6.328 +        | prep_pat (t $ u) used =
   6.329 +            let
   6.330 +              val (t', used') = prep_pat t used;
   6.331 +              val (u', used'') = prep_pat u used'
   6.332 +            in
   6.333 +              (t' $ u', used'')
   6.334 +            end
   6.335 +        | prep_pat t used = case_error ("Bad pattern: " ^ Syntax.string_of_term ctxt t);
   6.336 +      fun dest_case1 (t as Const ("_case1", _) $ l $ r) =
   6.337 +            let val (l', cnstrts) = strip_constraints l
   6.338 +            in ((fst (prep_pat l' (Term.add_free_names t [])), r), cnstrts)
   6.339 +            end
   6.340 +        | dest_case1 t = case_error "dest_case1";
   6.341 +      fun dest_case2 (Const ("_case2", _) $ t $ u) = t :: dest_case2 u
   6.342 +        | dest_case2 t = [t];
   6.343 +      val (cases, cnstrts) = split_list (map dest_case1 (dest_case2 u));
   6.344 +      val (case_tm, _) = make_case_untyped (tab_of thy) ctxt err []
   6.345 +        (fold (fn tT => fn t => Syntax.const "_constrain" $ t $ tT)
   6.346 +           (flat cnstrts) t) cases;
   6.347 +    in case_tm end
   6.348 +  | case_tr _ _ _ ts = case_error "case_tr";
   6.349 +
   6.350 +
   6.351 +(*---------------------------------------------------------------------------
   6.352 + * Pretty printing of nested case expressions
   6.353 + *---------------------------------------------------------------------------*)
   6.354 +
   6.355 +(* destruct one level of pattern matching *)
   6.356 +
   6.357 +fun gen_dest_case name_of type_of tab d used t =
   6.358 +  case apfst name_of (strip_comb t) of
   6.359 +    (SOME cname, ts as _ :: _) =>
   6.360 +      let
   6.361 +        val (fs, x) = split_last ts;
   6.362 +        fun strip_abs i t =
   6.363 +          let
   6.364 +            val zs = strip_abs_vars t;
   6.365 +            val _ = if length zs < i then raise CASE_ERROR ("", 0) else ();
   6.366 +            val (xs, ys) = chop i zs;
   6.367 +            val u = list_abs (ys, strip_abs_body t);
   6.368 +            val xs' = map Free (Name.variant_list (OldTerm.add_term_names (u, used))
   6.369 +              (map fst xs) ~~ map snd xs)
   6.370 +          in (xs', subst_bounds (rev xs', u)) end;
   6.371 +        fun is_dependent i t =
   6.372 +          let val k = length (strip_abs_vars t) - i
   6.373 +          in k < 0 orelse exists (fn j => j >= k)
   6.374 +            (loose_bnos (strip_abs_body t))
   6.375 +          end;
   6.376 +        fun count_cases (_, _, true) = I
   6.377 +          | count_cases (c, (_, body), false) =
   6.378 +              AList.map_default op aconv (body, []) (cons c);
   6.379 +        val is_undefined = name_of #> equal (SOME "HOL.undefined");
   6.380 +        fun mk_case (c, (xs, body), _) = (list_comb (c, xs), body)
   6.381 +      in case ty_info tab cname of
   6.382 +          SOME {constructors, case_name} =>
   6.383 +            if length fs = length constructors then
   6.384 +              let
   6.385 +                val cases = map (fn (Const (s, U), t) =>
   6.386 +                  let
   6.387 +                    val k = length (binder_types U);
   6.388 +                    val p as (xs, _) = strip_abs k t
   6.389 +                  in
   6.390 +                    (Const (s, map type_of xs ---> type_of x),
   6.391 +                     p, is_dependent k t)
   6.392 +                  end) (constructors ~~ fs);
   6.393 +                val cases' = sort (int_ord o swap o pairself (length o snd))
   6.394 +                  (fold_rev count_cases cases []);
   6.395 +                val R = type_of t;
   6.396 +                val dummy = if d then Const ("dummy_pattern", R)
   6.397 +                  else Free (Name.variant used "x", R)
   6.398 +              in
   6.399 +                SOME (x, map mk_case (case find_first (is_undefined o fst) cases' of
   6.400 +                  SOME (_, cs) =>
   6.401 +                  if length cs = length constructors then [hd cases]
   6.402 +                  else filter_out (fn (_, (_, body), _) => is_undefined body) cases
   6.403 +                | NONE => case cases' of
   6.404 +                  [] => cases
   6.405 +                | (default, cs) :: _ =>
   6.406 +                  if length cs = 1 then cases
   6.407 +                  else if length cs = length constructors then
   6.408 +                    [hd cases, (dummy, ([], default), false)]
   6.409 +                  else
   6.410 +                    filter_out (fn (c, _, _) => member op aconv cs c) cases @
   6.411 +                    [(dummy, ([], default), false)]))
   6.412 +              end handle CASE_ERROR _ => NONE
   6.413 +            else NONE
   6.414 +        | _ => NONE
   6.415 +      end
   6.416 +  | _ => NONE;
   6.417 +
   6.418 +val dest_case = gen_dest_case (try (dest_Const #> fst)) fastype_of;
   6.419 +val dest_case' = gen_dest_case
   6.420 +  (try (dest_Const #> fst #> unprefix Syntax.constN)) (K dummyT);
   6.421 +
   6.422 +
   6.423 +(* destruct nested patterns *)
   6.424 +
   6.425 +fun strip_case'' dest (pat, rhs) =
   6.426 +  case dest (Term.add_free_names pat []) rhs of
   6.427 +    SOME (exp as Free _, clauses) =>
   6.428 +      if member op aconv (OldTerm.term_frees pat) exp andalso
   6.429 +        not (exists (fn (_, rhs') =>
   6.430 +          member op aconv (OldTerm.term_frees rhs') exp) clauses)
   6.431 +      then
   6.432 +        maps (strip_case'' dest) (map (fn (pat', rhs') =>
   6.433 +          (subst_free [(exp, pat')] pat, rhs')) clauses)
   6.434 +      else [(pat, rhs)]
   6.435 +  | _ => [(pat, rhs)];
   6.436 +
   6.437 +fun gen_strip_case dest t = case dest [] t of
   6.438 +    SOME (x, clauses) =>
   6.439 +      SOME (x, maps (strip_case'' dest) clauses)
   6.440 +  | NONE => NONE;
   6.441 +
   6.442 +val strip_case = gen_strip_case oo dest_case;
   6.443 +val strip_case' = gen_strip_case oo dest_case';
   6.444 +
   6.445 +
   6.446 +(* print translation *)
   6.447 +
   6.448 +fun case_tr' tab_of cname ctxt ts =
   6.449 +  let
   6.450 +    val thy = ProofContext.theory_of ctxt;
   6.451 +    val consts = ProofContext.consts_of ctxt;
   6.452 +    fun mk_clause (pat, rhs) =
   6.453 +      let val xs = Term.add_frees pat []
   6.454 +      in
   6.455 +        Syntax.const "_case1" $
   6.456 +          map_aterms
   6.457 +            (fn Free p => Syntax.mark_boundT p
   6.458 +              | Const (s, _) => Const (Consts.extern_early consts s, dummyT)
   6.459 +              | t => t) pat $
   6.460 +          map_aterms
   6.461 +            (fn x as Free (s, T) =>
   6.462 +                  if member (op =) xs (s, T) then Syntax.mark_bound s else x
   6.463 +              | t => t) rhs
   6.464 +      end
   6.465 +  in case strip_case' (tab_of thy) true (list_comb (Syntax.const cname, ts)) of
   6.466 +      SOME (x, clauses) => Syntax.const "_case_syntax" $ x $
   6.467 +        foldr1 (fn (t, u) => Syntax.const "_case2" $ t $ u)
   6.468 +          (map mk_clause clauses)
   6.469 +    | NONE => raise Match
   6.470 +  end;
   6.471 +
   6.472 +end;
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/Tools/datatype_package/datatype_codegen.ML	Wed Jun 10 15:04:33 2009 +0200
     7.3 @@ -0,0 +1,451 @@
     7.4 +(*  Title:      HOL/Tools/datatype_codegen.ML
     7.5 +    Author:     Stefan Berghofer and Florian Haftmann, TU Muenchen
     7.6 +
     7.7 +Code generator facilities for inductive datatypes.
     7.8 +*)
     7.9 +
    7.10 +signature DATATYPE_CODEGEN =
    7.11 +sig
    7.12 +  val find_shortest_path: DatatypeAux.descr -> int -> (string * int) option
    7.13 +  val mk_eq_eqns: theory -> string -> (thm * bool) list
    7.14 +  val mk_case_cert: theory -> string -> thm
    7.15 +  val setup: theory -> theory
    7.16 +end;
    7.17 +
    7.18 +structure DatatypeCodegen : DATATYPE_CODEGEN =
    7.19 +struct
    7.20 +
    7.21 +(** SML code generator **)
    7.22 +
    7.23 +open Codegen;
    7.24 +
    7.25 +(**** datatype definition ****)
    7.26 +
    7.27 +(* find shortest path to constructor with no recursive arguments *)
    7.28 +
    7.29 +fun find_nonempty (descr: DatatypeAux.descr) is i =
    7.30 +  let
    7.31 +    val (_, _, constrs) = the (AList.lookup (op =) descr i);
    7.32 +    fun arg_nonempty (_, DatatypeAux.DtRec i) = if member (op =) is i
    7.33 +          then NONE
    7.34 +          else Option.map (curry op + 1 o snd) (find_nonempty descr (i::is) i)
    7.35 +      | arg_nonempty _ = SOME 0;
    7.36 +    fun max xs = Library.foldl
    7.37 +      (fn (NONE, _) => NONE
    7.38 +        | (SOME i, SOME j) => SOME (Int.max (i, j))
    7.39 +        | (_, NONE) => NONE) (SOME 0, xs);
    7.40 +    val xs = sort (int_ord o pairself snd)
    7.41 +      (map_filter (fn (s, dts) => Option.map (pair s)
    7.42 +        (max (map (arg_nonempty o DatatypeAux.strip_dtyp) dts))) constrs)
    7.43 +  in case xs of [] => NONE | x :: _ => SOME x end;
    7.44 +
    7.45 +fun find_shortest_path descr i = find_nonempty descr [i] i;
    7.46 +
    7.47 +fun add_dt_defs thy defs dep module (descr: DatatypeAux.descr) sorts gr =
    7.48 +  let
    7.49 +    val descr' = List.filter (can (map DatatypeAux.dest_DtTFree o #2 o snd)) descr;
    7.50 +    val rtnames = map (#1 o snd) (List.filter (fn (_, (_, _, cs)) =>
    7.51 +      exists (exists DatatypeAux.is_rec_type o snd) cs) descr');
    7.52 +
    7.53 +    val (_, (tname, _, _)) :: _ = descr';
    7.54 +    val node_id = tname ^ " (type)";
    7.55 +    val module' = if_library (thyname_of_type thy tname) module;
    7.56 +
    7.57 +    fun mk_dtdef prfx [] gr = ([], gr)
    7.58 +      | mk_dtdef prfx ((_, (tname, dts, cs))::xs) gr =
    7.59 +          let
    7.60 +            val tvs = map DatatypeAux.dest_DtTFree dts;
    7.61 +            val cs' = map (apsnd (map (DatatypeAux.typ_of_dtyp descr sorts))) cs;
    7.62 +            val ((_, type_id), gr') = mk_type_id module' tname gr;
    7.63 +            val (ps, gr'') = gr' |>
    7.64 +              fold_map (fn (cname, cargs) =>
    7.65 +                fold_map (invoke_tycodegen thy defs node_id module' false)
    7.66 +                  cargs ##>>
    7.67 +                mk_const_id module' cname) cs';
    7.68 +            val (rest, gr''') = mk_dtdef "and " xs gr''
    7.69 +          in
    7.70 +            (Pretty.block (str prfx ::
    7.71 +               (if null tvs then [] else
    7.72 +                  [mk_tuple (map str tvs), str " "]) @
    7.73 +               [str (type_id ^ " ="), Pretty.brk 1] @
    7.74 +               List.concat (separate [Pretty.brk 1, str "| "]
    7.75 +                 (map (fn (ps', (_, cname)) => [Pretty.block
    7.76 +                   (str cname ::
    7.77 +                    (if null ps' then [] else
    7.78 +                     List.concat ([str " of", Pretty.brk 1] ::
    7.79 +                       separate [str " *", Pretty.brk 1]
    7.80 +                         (map single ps'))))]) ps))) :: rest, gr''')
    7.81 +          end;
    7.82 +
    7.83 +    fun mk_constr_term cname Ts T ps =
    7.84 +      List.concat (separate [str " $", Pretty.brk 1]
    7.85 +        ([str ("Const (\"" ^ cname ^ "\","), Pretty.brk 1,
    7.86 +          mk_type false (Ts ---> T), str ")"] :: ps));
    7.87 +
    7.88 +    fun mk_term_of_def gr prfx [] = []
    7.89 +      | mk_term_of_def gr prfx ((_, (tname, dts, cs)) :: xs) =
    7.90 +          let
    7.91 +            val cs' = map (apsnd (map (DatatypeAux.typ_of_dtyp descr sorts))) cs;
    7.92 +            val dts' = map (DatatypeAux.typ_of_dtyp descr sorts) dts;
    7.93 +            val T = Type (tname, dts');
    7.94 +            val rest = mk_term_of_def gr "and " xs;
    7.95 +            val (eqs, _) = fold_map (fn (cname, Ts) => fn prfx =>
    7.96 +              let val args = map (fn i =>
    7.97 +                str ("x" ^ string_of_int i)) (1 upto length Ts)
    7.98 +              in (Pretty.blk (4,
    7.99 +                [str prfx, mk_term_of gr module' false T, Pretty.brk 1,
   7.100 +                 if null Ts then str (snd (get_const_id gr cname))
   7.101 +                 else parens (Pretty.block
   7.102 +                   [str (snd (get_const_id gr cname)),
   7.103 +                    Pretty.brk 1, mk_tuple args]),
   7.104 +                 str " =", Pretty.brk 1] @
   7.105 +                 mk_constr_term cname Ts T
   7.106 +                   (map2 (fn x => fn U => [Pretty.block [mk_term_of gr module' false U,
   7.107 +                      Pretty.brk 1, x]]) args Ts)), "  | ")
   7.108 +              end) cs' prfx
   7.109 +          in eqs @ rest end;
   7.110 +
   7.111 +    fun mk_gen_of_def gr prfx [] = []
   7.112 +      | mk_gen_of_def gr prfx ((i, (tname, dts, cs)) :: xs) =
   7.113 +          let
   7.114 +            val tvs = map DatatypeAux.dest_DtTFree dts;
   7.115 +            val Us = map (DatatypeAux.typ_of_dtyp descr sorts) dts;
   7.116 +            val T = Type (tname, Us);
   7.117 +            val (cs1, cs2) =
   7.118 +              List.partition (exists DatatypeAux.is_rec_type o snd) cs;
   7.119 +            val SOME (cname, _) = find_shortest_path descr i;
   7.120 +
   7.121 +            fun mk_delay p = Pretty.block
   7.122 +              [str "fn () =>", Pretty.brk 1, p];
   7.123 +
   7.124 +            fun mk_force p = Pretty.block [p, Pretty.brk 1, str "()"];
   7.125 +
   7.126 +            fun mk_constr s b (cname, dts) =
   7.127 +              let
   7.128 +                val gs = map (fn dt => mk_app false (mk_gen gr module' false rtnames s
   7.129 +                    (DatatypeAux.typ_of_dtyp descr sorts dt))
   7.130 +                  [str (if b andalso DatatypeAux.is_rec_type dt then "0"
   7.131 +                     else "j")]) dts;
   7.132 +                val Ts = map (DatatypeAux.typ_of_dtyp descr sorts) dts;
   7.133 +                val xs = map str
   7.134 +                  (DatatypeProp.indexify_names (replicate (length dts) "x"));
   7.135 +                val ts = map str
   7.136 +                  (DatatypeProp.indexify_names (replicate (length dts) "t"));
   7.137 +                val (_, id) = get_const_id gr cname
   7.138 +              in
   7.139 +                mk_let
   7.140 +                  (map2 (fn p => fn q => mk_tuple [p, q]) xs ts ~~ gs)
   7.141 +                  (mk_tuple
   7.142 +                    [case xs of
   7.143 +                       _ :: _ :: _ => Pretty.block
   7.144 +                         [str id, Pretty.brk 1, mk_tuple xs]
   7.145 +                     | _ => mk_app false (str id) xs,
   7.146 +                     mk_delay (Pretty.block (mk_constr_term cname Ts T
   7.147 +                       (map (single o mk_force) ts)))])
   7.148 +              end;
   7.149 +
   7.150 +            fun mk_choice [c] = mk_constr "(i-1)" false c
   7.151 +              | mk_choice cs = Pretty.block [str "one_of",
   7.152 +                  Pretty.brk 1, Pretty.blk (1, str "[" ::
   7.153 +                  List.concat (separate [str ",", Pretty.fbrk]
   7.154 +                    (map (single o mk_delay o mk_constr "(i-1)" false) cs)) @
   7.155 +                  [str "]"]), Pretty.brk 1, str "()"];
   7.156 +
   7.157 +            val gs = maps (fn s =>
   7.158 +              let val s' = strip_tname s
   7.159 +              in [str (s' ^ "G"), str (s' ^ "T")] end) tvs;
   7.160 +            val gen_name = "gen_" ^ snd (get_type_id gr tname)
   7.161 +
   7.162 +          in
   7.163 +            Pretty.blk (4, separate (Pretty.brk 1) 
   7.164 +                (str (prfx ^ gen_name ^
   7.165 +                   (if null cs1 then "" else "'")) :: gs @
   7.166 +                 (if null cs1 then [] else [str "i"]) @
   7.167 +                 [str "j"]) @
   7.168 +              [str " =", Pretty.brk 1] @
   7.169 +              (if not (null cs1) andalso not (null cs2)
   7.170 +               then [str "frequency", Pretty.brk 1,
   7.171 +                 Pretty.blk (1, [str "[",
   7.172 +                   mk_tuple [str "i", mk_delay (mk_choice cs1)],
   7.173 +                   str ",", Pretty.fbrk,
   7.174 +                   mk_tuple [str "1", mk_delay (mk_choice cs2)],
   7.175 +                   str "]"]), Pretty.brk 1, str "()"]
   7.176 +               else if null cs2 then
   7.177 +                 [Pretty.block [str "(case", Pretty.brk 1,
   7.178 +                   str "i", Pretty.brk 1, str "of",
   7.179 +                   Pretty.brk 1, str "0 =>", Pretty.brk 1,
   7.180 +                   mk_constr "0" true (cname, valOf (AList.lookup (op =) cs cname)),
   7.181 +                   Pretty.brk 1, str "| _ =>", Pretty.brk 1,
   7.182 +                   mk_choice cs1, str ")"]]
   7.183 +               else [mk_choice cs2])) ::
   7.184 +            (if null cs1 then []
   7.185 +             else [Pretty.blk (4, separate (Pretty.brk 1) 
   7.186 +                 (str ("and " ^ gen_name) :: gs @ [str "i"]) @
   7.187 +               [str " =", Pretty.brk 1] @
   7.188 +               separate (Pretty.brk 1) (str (gen_name ^ "'") :: gs @
   7.189 +                 [str "i", str "i"]))]) @
   7.190 +            mk_gen_of_def gr "and " xs
   7.191 +          end
   7.192 +
   7.193 +  in
   7.194 +    (module', (add_edge_acyclic (node_id, dep) gr
   7.195 +        handle Graph.CYCLES _ => gr) handle Graph.UNDEF _ =>
   7.196 +         let
   7.197 +           val gr1 = add_edge (node_id, dep)
   7.198 +             (new_node (node_id, (NONE, "", "")) gr);
   7.199 +           val (dtdef, gr2) = mk_dtdef "datatype " descr' gr1 ;
   7.200 +         in
   7.201 +           map_node node_id (K (NONE, module',
   7.202 +             string_of (Pretty.blk (0, separate Pretty.fbrk dtdef @
   7.203 +               [str ";"])) ^ "\n\n" ^
   7.204 +             (if "term_of" mem !mode then
   7.205 +                string_of (Pretty.blk (0, separate Pretty.fbrk
   7.206 +                  (mk_term_of_def gr2 "fun " descr') @ [str ";"])) ^ "\n\n"
   7.207 +              else "") ^
   7.208 +             (if "test" mem !mode then
   7.209 +                string_of (Pretty.blk (0, separate Pretty.fbrk
   7.210 +                  (mk_gen_of_def gr2 "fun " descr') @ [str ";"])) ^ "\n\n"
   7.211 +              else ""))) gr2
   7.212 +         end)
   7.213 +  end;
   7.214 +
   7.215 +
   7.216 +(**** case expressions ****)
   7.217 +
   7.218 +fun pretty_case thy defs dep module brack constrs (c as Const (_, T)) ts gr =
   7.219 +  let val i = length constrs
   7.220 +  in if length ts <= i then
   7.221 +       invoke_codegen thy defs dep module brack (eta_expand c ts (i+1)) gr
   7.222 +    else
   7.223 +      let
   7.224 +        val ts1 = Library.take (i, ts);
   7.225 +        val t :: ts2 = Library.drop (i, ts);
   7.226 +        val names = List.foldr OldTerm.add_term_names
   7.227 +          (map (fst o fst o dest_Var) (List.foldr OldTerm.add_term_vars [] ts1)) ts1;
   7.228 +        val (Ts, dT) = split_last (Library.take (i+1, fst (strip_type T)));
   7.229 +
   7.230 +        fun pcase [] [] [] gr = ([], gr)
   7.231 +          | pcase ((cname, cargs)::cs) (t::ts) (U::Us) gr =
   7.232 +              let
   7.233 +                val j = length cargs;
   7.234 +                val xs = Name.variant_list names (replicate j "x");
   7.235 +                val Us' = Library.take (j, fst (strip_type U));
   7.236 +                val frees = map Free (xs ~~ Us');
   7.237 +                val (cp, gr0) = invoke_codegen thy defs dep module false
   7.238 +                  (list_comb (Const (cname, Us' ---> dT), frees)) gr;
   7.239 +                val t' = Envir.beta_norm (list_comb (t, frees));
   7.240 +                val (p, gr1) = invoke_codegen thy defs dep module false t' gr0;
   7.241 +                val (ps, gr2) = pcase cs ts Us gr1;
   7.242 +              in
   7.243 +                ([Pretty.block [cp, str " =>", Pretty.brk 1, p]] :: ps, gr2)
   7.244 +              end;
   7.245 +
   7.246 +        val (ps1, gr1) = pcase constrs ts1 Ts gr ;
   7.247 +        val ps = List.concat (separate [Pretty.brk 1, str "| "] ps1);
   7.248 +        val (p, gr2) = invoke_codegen thy defs dep module false t gr1;
   7.249 +        val (ps2, gr3) = fold_map (invoke_codegen thy defs dep module true) ts2 gr2;
   7.250 +      in ((if not (null ts2) andalso brack then parens else I)
   7.251 +        (Pretty.block (separate (Pretty.brk 1)
   7.252 +          (Pretty.block ([str "(case ", p, str " of",
   7.253 +             Pretty.brk 1] @ ps @ [str ")"]) :: ps2))), gr3)
   7.254 +      end
   7.255 +  end;
   7.256 +
   7.257 +
   7.258 +(**** constructors ****)
   7.259 +
   7.260 +fun pretty_constr thy defs dep module brack args (c as Const (s, T)) ts gr =
   7.261 +  let val i = length args
   7.262 +  in if i > 1 andalso length ts < i then
   7.263 +      invoke_codegen thy defs dep module brack (eta_expand c ts i) gr
   7.264 +     else
   7.265 +       let
   7.266 +         val id = mk_qual_id module (get_const_id gr s);
   7.267 +         val (ps, gr') = fold_map
   7.268 +           (invoke_codegen thy defs dep module (i = 1)) ts gr;
   7.269 +       in (case args of
   7.270 +          _ :: _ :: _ => (if brack then parens else I)
   7.271 +            (Pretty.block [str id, Pretty.brk 1, mk_tuple ps])
   7.272 +        | _ => (mk_app brack (str id) ps), gr')
   7.273 +       end
   7.274 +  end;
   7.275 +
   7.276 +
   7.277 +(**** code generators for terms and types ****)
   7.278 +
   7.279 +fun datatype_codegen thy defs dep module brack t gr = (case strip_comb t of
   7.280 +   (c as Const (s, T), ts) =>
   7.281 +     (case DatatypePackage.datatype_of_case thy s of
   7.282 +        SOME {index, descr, ...} =>
   7.283 +          if is_some (get_assoc_code thy (s, T)) then NONE else
   7.284 +          SOME (pretty_case thy defs dep module brack
   7.285 +            (#3 (the (AList.lookup op = descr index))) c ts gr )
   7.286 +      | NONE => case (DatatypePackage.datatype_of_constr thy s, strip_type T) of
   7.287 +        (SOME {index, descr, ...}, (_, U as Type (tyname, _))) =>
   7.288 +          if is_some (get_assoc_code thy (s, T)) then NONE else
   7.289 +          let
   7.290 +            val SOME (tyname', _, constrs) = AList.lookup op = descr index;
   7.291 +            val SOME args = AList.lookup op = constrs s
   7.292 +          in
   7.293 +            if tyname <> tyname' then NONE
   7.294 +            else SOME (pretty_constr thy defs
   7.295 +              dep module brack args c ts (snd (invoke_tycodegen thy defs dep module false U gr)))
   7.296 +          end
   7.297 +      | _ => NONE)
   7.298 + | _ => NONE);
   7.299 +
   7.300 +fun datatype_tycodegen thy defs dep module brack (Type (s, Ts)) gr =
   7.301 +      (case DatatypePackage.get_datatype thy s of
   7.302 +         NONE => NONE
   7.303 +       | SOME {descr, sorts, ...} =>
   7.304 +           if is_some (get_assoc_type thy s) then NONE else
   7.305 +           let
   7.306 +             val (ps, gr') = fold_map
   7.307 +               (invoke_tycodegen thy defs dep module false) Ts gr;
   7.308 +             val (module', gr'') = add_dt_defs thy defs dep module descr sorts gr' ;
   7.309 +             val (tyid, gr''') = mk_type_id module' s gr''
   7.310 +           in SOME (Pretty.block ((if null Ts then [] else
   7.311 +               [mk_tuple ps, str " "]) @
   7.312 +               [str (mk_qual_id module tyid)]), gr''')
   7.313 +           end)
   7.314 +  | datatype_tycodegen _ _ _ _ _ _ _ = NONE;
   7.315 +
   7.316 +
   7.317 +(** generic code generator **)
   7.318 +
   7.319 +(* case certificates *)
   7.320 +
   7.321 +fun mk_case_cert thy tyco =
   7.322 +  let
   7.323 +    val raw_thms =
   7.324 +      (#case_rewrites o DatatypePackage.the_datatype thy) tyco;
   7.325 +    val thms as hd_thm :: _ = raw_thms
   7.326 +      |> Conjunction.intr_balanced
   7.327 +      |> Thm.unvarify
   7.328 +      |> Conjunction.elim_balanced (length raw_thms)
   7.329 +      |> map Simpdata.mk_meta_eq
   7.330 +      |> map Drule.zero_var_indexes
   7.331 +    val params = fold_aterms (fn (Free (v, _)) => insert (op =) v
   7.332 +      | _ => I) (Thm.prop_of hd_thm) [];
   7.333 +    val rhs = hd_thm
   7.334 +      |> Thm.prop_of
   7.335 +      |> Logic.dest_equals
   7.336 +      |> fst
   7.337 +      |> Term.strip_comb
   7.338 +      |> apsnd (fst o split_last)
   7.339 +      |> list_comb;
   7.340 +    val lhs = Free (Name.variant params "case", Term.fastype_of rhs);
   7.341 +    val asm = (Thm.cterm_of thy o Logic.mk_equals) (lhs, rhs);
   7.342 +  in
   7.343 +    thms
   7.344 +    |> Conjunction.intr_balanced
   7.345 +    |> MetaSimplifier.rewrite_rule [(Thm.symmetric o Thm.assume) asm]
   7.346 +    |> Thm.implies_intr asm
   7.347 +    |> Thm.generalize ([], params) 0
   7.348 +    |> AxClass.unoverload thy
   7.349 +    |> Thm.varifyT
   7.350 +  end;
   7.351 +
   7.352 +
   7.353 +(* equality *)
   7.354 +
   7.355 +fun mk_eq_eqns thy dtco =
   7.356 +  let
   7.357 +    val (vs, cos) = DatatypePackage.the_datatype_spec thy dtco;
   7.358 +    val { descr, index, inject = inject_thms, ... } = DatatypePackage.the_datatype thy dtco;
   7.359 +    val ty = Type (dtco, map TFree vs);
   7.360 +    fun mk_eq (t1, t2) = Const (@{const_name eq_class.eq}, ty --> ty --> HOLogic.boolT)
   7.361 +      $ t1 $ t2;
   7.362 +    fun true_eq t12 = HOLogic.mk_eq (mk_eq t12, HOLogic.true_const);
   7.363 +    fun false_eq t12 = HOLogic.mk_eq (mk_eq t12, HOLogic.false_const);
   7.364 +    val triv_injects = map_filter
   7.365 +     (fn (c, []) => SOME (HOLogic.mk_Trueprop (true_eq (Const (c, ty), Const (c, ty))))
   7.366 +       | _ => NONE) cos;
   7.367 +    fun prep_inject (trueprop $ (equiv $ (_ $ t1 $ t2) $ rhs)) =
   7.368 +      trueprop $ (equiv $ mk_eq (t1, t2) $ rhs);
   7.369 +    val injects = map prep_inject (nth (DatatypeProp.make_injs [descr] vs) index);
   7.370 +    fun prep_distinct (trueprop $ (not $ (_ $ t1 $ t2))) =
   7.371 +      [trueprop $ false_eq (t1, t2), trueprop $ false_eq (t2, t1)];
   7.372 +    val distincts = maps prep_distinct (snd (nth (DatatypeProp.make_distincts [descr] vs) index));
   7.373 +    val refl = HOLogic.mk_Trueprop (true_eq (Free ("x", ty), Free ("x", ty)));
   7.374 +    val simpset = Simplifier.context (ProofContext.init thy) (HOL_basic_ss
   7.375 +      addsimps (map Simpdata.mk_eq (@{thm eq} :: @{thm eq_True} :: inject_thms))
   7.376 +      addsimprocs [DatatypePackage.distinct_simproc]);
   7.377 +    fun prove prop = Goal.prove_global thy [] [] prop (K (ALLGOALS (simp_tac simpset)))
   7.378 +      |> Simpdata.mk_eq;
   7.379 +  in map (rpair true o prove) (triv_injects @ injects @ distincts) @ [(prove refl, false)] end;
   7.380 +
   7.381 +fun add_equality vs dtcos thy =
   7.382 +  let
   7.383 +    fun add_def dtco lthy =
   7.384 +      let
   7.385 +        val ty = Type (dtco, map TFree vs);
   7.386 +        fun mk_side const_name = Const (const_name, ty --> ty --> HOLogic.boolT)
   7.387 +          $ Free ("x", ty) $ Free ("y", ty);
   7.388 +        val def = HOLogic.mk_Trueprop (HOLogic.mk_eq
   7.389 +          (mk_side @{const_name eq_class.eq}, mk_side @{const_name "op ="}));
   7.390 +        val def' = Syntax.check_term lthy def;
   7.391 +        val ((_, (_, thm)), lthy') = Specification.definition
   7.392 +          (NONE, (Attrib.empty_binding, def')) lthy;
   7.393 +        val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy);
   7.394 +        val thm' = singleton (ProofContext.export lthy' ctxt_thy) thm;
   7.395 +      in (thm', lthy') end;
   7.396 +    fun tac thms = Class.intro_classes_tac []
   7.397 +      THEN ALLGOALS (ProofContext.fact_tac thms);
   7.398 +    fun add_eq_thms dtco thy =
   7.399 +      let
   7.400 +        val const = AxClass.param_of_inst thy (@{const_name eq_class.eq}, dtco);
   7.401 +        val thy_ref = Theory.check_thy thy;
   7.402 +        fun mk_thms () = rev ((mk_eq_eqns (Theory.deref thy_ref) dtco));
   7.403 +      in
   7.404 +        Code.add_eqnl (const, Lazy.lazy mk_thms) thy
   7.405 +      end;
   7.406 +  in
   7.407 +    thy
   7.408 +    |> TheoryTarget.instantiation (dtcos, vs, [HOLogic.class_eq])
   7.409 +    |> fold_map add_def dtcos
   7.410 +    |-> (fn def_thms => Class.prove_instantiation_exit_result (map o Morphism.thm)
   7.411 +         (fn _ => fn def_thms => tac def_thms) def_thms)
   7.412 +    |-> (fn def_thms => fold Code.del_eqn def_thms)
   7.413 +    |> fold add_eq_thms dtcos
   7.414 +  end;
   7.415 +
   7.416 +
   7.417 +(* liberal addition of code data for datatypes *)
   7.418 +
   7.419 +fun mk_constr_consts thy vs dtco cos =
   7.420 +  let
   7.421 +    val cs = map (fn (c, tys) => (c, tys ---> Type (dtco, map TFree vs))) cos;
   7.422 +    val cs' = map (fn c_ty as (_, ty) => (AxClass.unoverload_const thy c_ty, ty)) cs;
   7.423 +  in if is_some (try (Code.constrset_of_consts thy) cs')
   7.424 +    then SOME cs
   7.425 +    else NONE
   7.426 +  end;
   7.427 +
   7.428 +fun add_all_code dtcos thy =
   7.429 +  let
   7.430 +    val (vs :: _, coss) = (split_list o map (DatatypePackage.the_datatype_spec thy)) dtcos;
   7.431 +    val any_css = map2 (mk_constr_consts thy vs) dtcos coss;
   7.432 +    val css = if exists is_none any_css then []
   7.433 +      else map_filter I any_css;
   7.434 +    val case_rewrites = maps (#case_rewrites o DatatypePackage.the_datatype thy) dtcos;
   7.435 +    val certs = map (mk_case_cert thy) dtcos;
   7.436 +  in
   7.437 +    if null css then thy
   7.438 +    else thy
   7.439 +      |> fold Code.add_datatype css
   7.440 +      |> fold_rev Code.add_default_eqn case_rewrites
   7.441 +      |> fold Code.add_case certs
   7.442 +      |> add_equality vs dtcos
   7.443 +   end;
   7.444 +
   7.445 +
   7.446 +
   7.447 +(** theory setup **)
   7.448 +
   7.449 +val setup = 
   7.450 +  add_codegen "datatype" datatype_codegen
   7.451 +  #> add_tycodegen "datatype" datatype_tycodegen
   7.452 +  #> DatatypePackage.interpretation add_all_code
   7.453 +
   7.454 +end;
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/Tools/datatype_package/datatype_package.ML	Wed Jun 10 15:04:33 2009 +0200
     8.3 @@ -0,0 +1,712 @@
     8.4 +(*  Title:      HOL/Tools/datatype_package.ML
     8.5 +    Author:     Stefan Berghofer, TU Muenchen
     8.6 +
     8.7 +Datatype package for Isabelle/HOL.
     8.8 +*)
     8.9 +
    8.10 +signature DATATYPE_PACKAGE =
    8.11 +sig
    8.12 +  type datatype_info = DatatypeAux.datatype_info
    8.13 +  type descr = DatatypeAux.descr
    8.14 +  val get_datatypes : theory -> datatype_info Symtab.table
    8.15 +  val get_datatype : theory -> string -> datatype_info option
    8.16 +  val the_datatype : theory -> string -> datatype_info
    8.17 +  val datatype_of_constr : theory -> string -> datatype_info option
    8.18 +  val datatype_of_case : theory -> string -> datatype_info option
    8.19 +  val the_datatype_spec : theory -> string -> (string * sort) list * (string * typ list) list
    8.20 +  val the_datatype_descr : theory -> string list
    8.21 +    -> descr * (string * sort) list * string list
    8.22 +      * (string list * string list) * (typ list * typ list)
    8.23 +  val get_datatype_constrs : theory -> string -> (string * typ) list option
    8.24 +  val distinct_simproc : simproc
    8.25 +  val make_case :  Proof.context -> bool -> string list -> term ->
    8.26 +    (term * term) list -> term * (term * (int * bool)) list
    8.27 +  val strip_case : Proof.context -> bool -> term -> (term * (term * term) list) option
    8.28 +  val read_typ: theory ->
    8.29 +    (typ list * (string * sort) list) * string -> typ list * (string * sort) list
    8.30 +  val interpretation : (string list -> theory -> theory) -> theory -> theory
    8.31 +  val rep_datatype : ({distinct : thm list list,
    8.32 +       inject : thm list list,
    8.33 +       exhaustion : thm list,
    8.34 +       rec_thms : thm list,
    8.35 +       case_thms : thm list list,
    8.36 +       split_thms : (thm * thm) list,
    8.37 +       induction : thm,
    8.38 +       simps : thm list} -> Proof.context -> Proof.context) -> string list option -> term list
    8.39 +    -> theory -> Proof.state;
    8.40 +  val rep_datatype_cmd : string list option -> string list -> theory -> Proof.state;
    8.41 +  val add_datatype : bool -> bool -> string list -> (string list * binding * mixfix *
    8.42 +    (binding * typ list * mixfix) list) list -> theory ->
    8.43 +      {distinct : thm list list,
    8.44 +       inject : thm list list,
    8.45 +       exhaustion : thm list,
    8.46 +       rec_thms : thm list,
    8.47 +       case_thms : thm list list,
    8.48 +       split_thms : (thm * thm) list,
    8.49 +       induction : thm,
    8.50 +       simps : thm list} * theory
    8.51 +  val add_datatype_cmd : bool -> string list -> (string list * binding * mixfix *
    8.52 +    (binding * string list * mixfix) list) list -> theory ->
    8.53 +      {distinct : thm list list,
    8.54 +       inject : thm list list,
    8.55 +       exhaustion : thm list,
    8.56 +       rec_thms : thm list,
    8.57 +       case_thms : thm list list,
    8.58 +       split_thms : (thm * thm) list,
    8.59 +       induction : thm,
    8.60 +       simps : thm list} * theory
    8.61 +  val setup: theory -> theory
    8.62 +  val quiet_mode : bool ref
    8.63 +  val print_datatypes : theory -> unit
    8.64 +end;
    8.65 +
    8.66 +structure DatatypePackage : DATATYPE_PACKAGE =
    8.67 +struct
    8.68 +
    8.69 +open DatatypeAux;
    8.70 +
    8.71 +val quiet_mode = quiet_mode;
    8.72 +
    8.73 +
    8.74 +(* theory data *)
    8.75 +
    8.76 +structure DatatypesData = TheoryDataFun
    8.77 +(
    8.78 +  type T =
    8.79 +    {types: datatype_info Symtab.table,
    8.80 +     constrs: datatype_info Symtab.table,
    8.81 +     cases: datatype_info Symtab.table};
    8.82 +
    8.83 +  val empty =
    8.84 +    {types = Symtab.empty, constrs = Symtab.empty, cases = Symtab.empty};
    8.85 +  val copy = I;
    8.86 +  val extend = I;
    8.87 +  fun merge _
    8.88 +    ({types = types1, constrs = constrs1, cases = cases1},
    8.89 +     {types = types2, constrs = constrs2, cases = cases2}) =
    8.90 +    {types = Symtab.merge (K true) (types1, types2),
    8.91 +     constrs = Symtab.merge (K true) (constrs1, constrs2),
    8.92 +     cases = Symtab.merge (K true) (cases1, cases2)};
    8.93 +);
    8.94 +
    8.95 +val get_datatypes = #types o DatatypesData.get;
    8.96 +val map_datatypes = DatatypesData.map;
    8.97 +
    8.98 +fun print_datatypes thy =
    8.99 +  Pretty.writeln (Pretty.strs ("datatypes:" ::
   8.100 +    map #1 (NameSpace.extern_table (Sign.type_space thy, get_datatypes thy))));
   8.101 +
   8.102 +
   8.103 +(** theory information about datatypes **)
   8.104 +
   8.105 +fun put_dt_infos (dt_infos : (string * datatype_info) list) =
   8.106 +  map_datatypes (fn {types, constrs, cases} =>
   8.107 +    {types = fold Symtab.update dt_infos types,
   8.108 +     constrs = fold Symtab.default (*conservative wrt. overloaded constructors*)
   8.109 +       (maps (fn (_, info as {descr, index, ...}) => map (rpair info o fst)
   8.110 +          (#3 (the (AList.lookup op = descr index)))) dt_infos) constrs,
   8.111 +     cases = fold Symtab.update
   8.112 +       (map (fn (_, info as {case_name, ...}) => (case_name, info)) dt_infos)
   8.113 +       cases});
   8.114 +
   8.115 +val get_datatype = Symtab.lookup o get_datatypes;
   8.116 +
   8.117 +fun the_datatype thy name = (case get_datatype thy name of
   8.118 +      SOME info => info
   8.119 +    | NONE => error ("Unknown datatype " ^ quote name));
   8.120 +
   8.121 +val datatype_of_constr = Symtab.lookup o #constrs o DatatypesData.get;
   8.122 +val datatype_of_case = Symtab.lookup o #cases o DatatypesData.get;
   8.123 +
   8.124 +fun get_datatype_descr thy dtco =
   8.125 +  get_datatype thy dtco
   8.126 +  |> Option.map (fn info as { descr, index, ... } =>
   8.127 +       (info, (((fn SOME (_, dtys, cos) => (dtys, cos)) o AList.lookup (op =) descr) index)));
   8.128 +
   8.129 +fun the_datatype_spec thy dtco =
   8.130 +  let
   8.131 +    val info as { descr, index, sorts = raw_sorts, ... } = the_datatype thy dtco;
   8.132 +    val SOME (_, dtys, raw_cos) = AList.lookup (op =) descr index;
   8.133 +    val sorts = map ((fn v => (v, (the o AList.lookup (op =) raw_sorts) v))
   8.134 +      o DatatypeAux.dest_DtTFree) dtys;
   8.135 +    val cos = map
   8.136 +      (fn (co, tys) => (co, map (DatatypeAux.typ_of_dtyp descr sorts) tys)) raw_cos;
   8.137 +  in (sorts, cos) end;
   8.138 +
   8.139 +fun the_datatype_descr thy (raw_tycos as raw_tyco :: _) =
   8.140 +  let
   8.141 +    val info = the_datatype thy raw_tyco;
   8.142 +    val descr = #descr info;
   8.143 +
   8.144 +    val SOME (_, dtys, raw_cos) = AList.lookup (op =) descr (#index info);
   8.145 +    val vs = map ((fn v => (v, (the o AList.lookup (op =) (#sorts info)) v))
   8.146 +      o dest_DtTFree) dtys;
   8.147 +
   8.148 +    fun is_DtTFree (DtTFree _) = true
   8.149 +      | is_DtTFree _ = false
   8.150 +    val k = find_index (fn (_, (_, dTs, _)) => not (forall is_DtTFree dTs)) descr;
   8.151 +    val protoTs as (dataTs, _) = chop k descr
   8.152 +      |> (pairself o map) (fn (_, (tyco, dTs, _)) => (tyco, map (typ_of_dtyp descr vs) dTs));
   8.153 +    
   8.154 +    val tycos = map fst dataTs;
   8.155 +    val _ = if gen_eq_set (op =) (tycos, raw_tycos) then ()
   8.156 +      else error ("Type constructors " ^ commas (map quote raw_tycos)
   8.157 +        ^ "do not belong exhaustively to one mutual recursive datatype");
   8.158 +
   8.159 +    val (Ts, Us) = (pairself o map) Type protoTs;
   8.160 +
   8.161 +    val names = map Long_Name.base_name (the_default tycos (#alt_names info));
   8.162 +    val (auxnames, _) = Name.make_context names
   8.163 +      |> fold_map (yield_singleton Name.variants o name_of_typ) Us
   8.164 +
   8.165 +  in (descr, vs, tycos, (names, auxnames), (Ts, Us)) end;
   8.166 +
   8.167 +fun get_datatype_constrs thy dtco =
   8.168 +  case try (the_datatype_spec thy) dtco
   8.169 +   of SOME (sorts, cos) =>
   8.170 +        let
   8.171 +          fun subst (v, sort) = TVar ((v, 0), sort);
   8.172 +          fun subst_ty (TFree v) = subst v
   8.173 +            | subst_ty ty = ty;
   8.174 +          val dty = Type (dtco, map subst sorts);
   8.175 +          fun mk_co (co, tys) = (co, map (Term.map_atyps subst_ty) tys ---> dty);
   8.176 +        in SOME (map mk_co cos) end
   8.177 +    | NONE => NONE;
   8.178 +
   8.179 +
   8.180 +(** induct method setup **)
   8.181 +
   8.182 +(* case names *)
   8.183 +
   8.184 +local
   8.185 +
   8.186 +fun dt_recs (DtTFree _) = []
   8.187 +  | dt_recs (DtType (_, dts)) = maps dt_recs dts
   8.188 +  | dt_recs (DtRec i) = [i];
   8.189 +
   8.190 +fun dt_cases (descr: descr) (_, args, constrs) =
   8.191 +  let
   8.192 +    fun the_bname i = Long_Name.base_name (#1 (the (AList.lookup (op =) descr i)));
   8.193 +    val bnames = map the_bname (distinct (op =) (maps dt_recs args));
   8.194 +  in map (fn (c, _) => space_implode "_" (Long_Name.base_name c :: bnames)) constrs end;
   8.195 +
   8.196 +
   8.197 +fun induct_cases descr =
   8.198 +  DatatypeProp.indexify_names (maps (dt_cases descr) (map #2 descr));
   8.199 +
   8.200 +fun exhaust_cases descr i = dt_cases descr (the (AList.lookup (op =) descr i));
   8.201 +
   8.202 +in
   8.203 +
   8.204 +fun mk_case_names_induct descr = RuleCases.case_names (induct_cases descr);
   8.205 +
   8.206 +fun mk_case_names_exhausts descr new =
   8.207 +  map (RuleCases.case_names o exhaust_cases descr o #1)
   8.208 +    (filter (fn ((_, (name, _, _))) => member (op =) new name) descr);
   8.209 +
   8.210 +end;
   8.211 +
   8.212 +fun add_rules simps case_thms rec_thms inject distinct
   8.213 +                  weak_case_congs cong_att =
   8.214 +  PureThy.add_thmss [((Binding.name "simps", simps), []),
   8.215 +    ((Binding.empty, flat case_thms @
   8.216 +          flat distinct @ rec_thms), [Simplifier.simp_add]),
   8.217 +    ((Binding.empty, rec_thms), [Code.add_default_eqn_attribute]),
   8.218 +    ((Binding.empty, flat inject), [iff_add]),
   8.219 +    ((Binding.empty, map (fn th => th RS notE) (flat distinct)), [Classical.safe_elim NONE]),
   8.220 +    ((Binding.empty, weak_case_congs), [cong_att])]
   8.221 +  #> snd;
   8.222 +
   8.223 +
   8.224 +(* add_cases_induct *)
   8.225 +
   8.226 +fun add_cases_induct infos induction thy =
   8.227 +  let
   8.228 +    val inducts = ProjectRule.projections (ProofContext.init thy) induction;
   8.229 +
   8.230 +    fun named_rules (name, {index, exhaustion, ...}: datatype_info) =
   8.231 +      [((Binding.empty, nth inducts index), [Induct.induct_type name]),
   8.232 +       ((Binding.empty, exhaustion), [Induct.cases_type name])];
   8.233 +    fun unnamed_rule i =
   8.234 +      ((Binding.empty, nth inducts i), [Thm.kind_internal, Induct.induct_type ""]);
   8.235 +  in
   8.236 +    thy |> PureThy.add_thms
   8.237 +      (maps named_rules infos @
   8.238 +        map unnamed_rule (length infos upto length inducts - 1)) |> snd
   8.239 +    |> PureThy.add_thmss [((Binding.name "inducts", inducts), [])] |> snd
   8.240 +  end;
   8.241 +
   8.242 +
   8.243 +
   8.244 +(**** simplification procedure for showing distinctness of constructors ****)
   8.245 +
   8.246 +fun stripT (i, Type ("fun", [_, T])) = stripT (i + 1, T)
   8.247 +  | stripT p = p;
   8.248 +
   8.249 +fun stripC (i, f $ x) = stripC (i + 1, f)
   8.250 +  | stripC p = p;
   8.251 +
   8.252 +val distinctN = "constr_distinct";
   8.253 +
   8.254 +fun distinct_rule thy ss tname eq_t = case #distinct (the_datatype thy tname) of
   8.255 +    FewConstrs thms => Goal.prove (Simplifier.the_context ss) [] [] eq_t (K
   8.256 +      (EVERY [rtac eq_reflection 1, rtac iffI 1, rtac notE 1,
   8.257 +        atac 2, resolve_tac thms 1, etac FalseE 1]))
   8.258 +  | ManyConstrs (thm, simpset) =>
   8.259 +      let
   8.260 +        val [In0_inject, In1_inject, In0_not_In1, In1_not_In0] =
   8.261 +          map (PureThy.get_thm (ThyInfo.the_theory "Datatype" thy))
   8.262 +            ["In0_inject", "In1_inject", "In0_not_In1", "In1_not_In0"];
   8.263 +      in
   8.264 +        Goal.prove (Simplifier.the_context ss) [] [] eq_t (K
   8.265 +        (EVERY [rtac eq_reflection 1, rtac iffI 1, dtac thm 1,
   8.266 +          full_simp_tac (Simplifier.inherit_context ss simpset) 1,
   8.267 +          REPEAT (dresolve_tac [In0_inject, In1_inject] 1),
   8.268 +          eresolve_tac [In0_not_In1 RS notE, In1_not_In0 RS notE] 1,
   8.269 +          etac FalseE 1]))
   8.270 +      end;
   8.271 +
   8.272 +fun distinct_proc thy ss (t as Const ("op =", _) $ t1 $ t2) =
   8.273 +  (case (stripC (0, t1), stripC (0, t2)) of
   8.274 +     ((i, Const (cname1, T1)), (j, Const (cname2, T2))) =>
   8.275 +         (case (stripT (0, T1), stripT (0, T2)) of
   8.276 +            ((i', Type (tname1, _)), (j', Type (tname2, _))) =>
   8.277 +                if tname1 = tname2 andalso not (cname1 = cname2) andalso i = i' andalso j = j' then
   8.278 +                   (case (get_datatype_descr thy) tname1 of
   8.279 +                      SOME (_, (_, constrs)) => let val cnames = map fst constrs
   8.280 +                        in if cname1 mem cnames andalso cname2 mem cnames then
   8.281 +                             SOME (distinct_rule thy ss tname1
   8.282 +                               (Logic.mk_equals (t, Const ("False", HOLogic.boolT))))
   8.283 +                           else NONE
   8.284 +                        end
   8.285 +                    | NONE => NONE)
   8.286 +                else NONE
   8.287 +          | _ => NONE)
   8.288 +   | _ => NONE)
   8.289 +  | distinct_proc _ _ _ = NONE;
   8.290 +
   8.291 +val distinct_simproc =
   8.292 +  Simplifier.simproc @{theory HOL} distinctN ["s = t"] distinct_proc;
   8.293 +
   8.294 +val dist_ss = HOL_ss addsimprocs [distinct_simproc];
   8.295 +
   8.296 +val simproc_setup =
   8.297 +  Simplifier.map_simpset (fn ss => ss addsimprocs [distinct_simproc]);
   8.298 +
   8.299 +
   8.300 +(**** translation rules for case ****)
   8.301 +
   8.302 +fun make_case ctxt = DatatypeCase.make_case
   8.303 +  (datatype_of_constr (ProofContext.theory_of ctxt)) ctxt;
   8.304 +
   8.305 +fun strip_case ctxt = DatatypeCase.strip_case
   8.306 +  (datatype_of_case (ProofContext.theory_of ctxt));
   8.307 +
   8.308 +fun add_case_tr' case_names thy =
   8.309 +  Sign.add_advanced_trfuns ([], [],
   8.310 +    map (fn case_name =>
   8.311 +      let val case_name' = Sign.const_syntax_name thy case_name
   8.312 +      in (case_name', DatatypeCase.case_tr' datatype_of_case case_name')
   8.313 +      end) case_names, []) thy;
   8.314 +
   8.315 +val trfun_setup =
   8.316 +  Sign.add_advanced_trfuns ([],
   8.317 +    [("_case_syntax", DatatypeCase.case_tr true datatype_of_constr)],
   8.318 +    [], []);
   8.319 +
   8.320 +
   8.321 +(* prepare types *)
   8.322 +
   8.323 +fun read_typ thy ((Ts, sorts), str) =
   8.324 +  let
   8.325 +    val ctxt = ProofContext.init thy
   8.326 +      |> fold (Variable.declare_typ o TFree) sorts;
   8.327 +    val T = Syntax.read_typ ctxt str;
   8.328 +  in (Ts @ [T], Term.add_tfreesT T sorts) end;
   8.329 +
   8.330 +fun cert_typ sign ((Ts, sorts), raw_T) =
   8.331 +  let
   8.332 +    val T = Type.no_tvars (Sign.certify_typ sign raw_T) handle
   8.333 +      TYPE (msg, _, _) => error msg;
   8.334 +    val sorts' = Term.add_tfreesT T sorts;
   8.335 +  in (Ts @ [T],
   8.336 +      case duplicates (op =) (map fst sorts') of
   8.337 +         [] => sorts'
   8.338 +       | dups => error ("Inconsistent sort constraints for " ^ commas dups))
   8.339 +  end;
   8.340 +
   8.341 +
   8.342 +(**** make datatype info ****)
   8.343 +
   8.344 +fun make_dt_info alt_names descr sorts induct reccomb_names rec_thms
   8.345 +    (((((((((i, (_, (tname, _, _))), case_name), case_thms),
   8.346 +      exhaustion_thm), distinct_thm), inject), nchotomy), case_cong), weak_case_cong) =
   8.347 +  (tname,
   8.348 +   {index = i,
   8.349 +    alt_names = alt_names,
   8.350 +    descr = descr,
   8.351 +    sorts = sorts,
   8.352 +    rec_names = reccomb_names,
   8.353 +    rec_rewrites = rec_thms,
   8.354 +    case_name = case_name,
   8.355 +    case_rewrites = case_thms,
   8.356 +    induction = induct,
   8.357 +    exhaustion = exhaustion_thm,
   8.358 +    distinct = distinct_thm,
   8.359 +    inject = inject,
   8.360 +    nchotomy = nchotomy,
   8.361 +    case_cong = case_cong,
   8.362 +    weak_case_cong = weak_case_cong});
   8.363 +
   8.364 +structure DatatypeInterpretation = InterpretationFun(type T = string list val eq = op =);
   8.365 +val interpretation = DatatypeInterpretation.interpretation;
   8.366 +
   8.367 +
   8.368 +(******************* definitional introduction of datatypes *******************)
   8.369 +
   8.370 +fun add_datatype_def flat_names new_type_names descr sorts types_syntax constr_syntax dt_info
   8.371 +    case_names_induct case_names_exhausts thy =
   8.372 +  let
   8.373 +    val _ = message ("Proofs for datatype(s) " ^ commas_quote new_type_names);
   8.374 +
   8.375 +    val ((inject, distinct, dist_rewrites, simproc_dists, induct), thy2) = thy |>
   8.376 +      DatatypeRepProofs.representation_proofs flat_names dt_info new_type_names descr sorts
   8.377 +        types_syntax constr_syntax case_names_induct;
   8.378 +
   8.379 +    val (casedist_thms, thy3) = DatatypeAbsProofs.prove_casedist_thms new_type_names descr
   8.380 +      sorts induct case_names_exhausts thy2;
   8.381 +    val ((reccomb_names, rec_thms), thy4) = DatatypeAbsProofs.prove_primrec_thms
   8.382 +      flat_names new_type_names descr sorts dt_info inject dist_rewrites
   8.383 +      (Simplifier.theory_context thy3 dist_ss) induct thy3;
   8.384 +    val ((case_thms, case_names), thy6) = DatatypeAbsProofs.prove_case_thms
   8.385 +      flat_names new_type_names descr sorts reccomb_names rec_thms thy4;
   8.386 +    val (split_thms, thy7) = DatatypeAbsProofs.prove_split_thms new_type_names
   8.387 +      descr sorts inject dist_rewrites casedist_thms case_thms thy6;
   8.388 +    val (nchotomys, thy8) = DatatypeAbsProofs.prove_nchotomys new_type_names
   8.389 +      descr sorts casedist_thms thy7;
   8.390 +    val (case_congs, thy9) = DatatypeAbsProofs.prove_case_congs new_type_names
   8.391 +      descr sorts nchotomys case_thms thy8;
   8.392 +    val (weak_case_congs, thy10) = DatatypeAbsProofs.prove_weak_case_congs new_type_names
   8.393 +      descr sorts thy9;
   8.394 +
   8.395 +    val dt_infos = map
   8.396 +      (make_dt_info (SOME new_type_names) (flat descr) sorts induct reccomb_names rec_thms)
   8.397 +      ((0 upto length (hd descr) - 1) ~~ (hd descr) ~~ case_names ~~ case_thms ~~
   8.398 +        casedist_thms ~~ simproc_dists ~~ inject ~~ nchotomys ~~ case_congs ~~ weak_case_congs);
   8.399 +
   8.400 +    val simps = flat (distinct @ inject @ case_thms) @ rec_thms;
   8.401 +
   8.402 +    val thy12 =
   8.403 +      thy10
   8.404 +      |> add_case_tr' case_names
   8.405 +      |> Sign.add_path (space_implode "_" new_type_names)
   8.406 +      |> add_rules simps case_thms rec_thms inject distinct
   8.407 +          weak_case_congs (Simplifier.attrib (op addcongs))
   8.408 +      |> put_dt_infos dt_infos
   8.409 +      |> add_cases_induct dt_infos induct
   8.410 +      |> Sign.parent_path
   8.411 +      |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms) |> snd
   8.412 +      |> DatatypeInterpretation.data (map fst dt_infos);
   8.413 +  in
   8.414 +    ({distinct = distinct,
   8.415 +      inject = inject,
   8.416 +      exhaustion = casedist_thms,
   8.417 +      rec_thms = rec_thms,
   8.418 +      case_thms = case_thms,
   8.419 +      split_thms = split_thms,
   8.420 +      induction = induct,
   8.421 +      simps = simps}, thy12)
   8.422 +  end;
   8.423 +
   8.424 +
   8.425 +(*********************** declare existing type as datatype *********************)
   8.426 +
   8.427 +fun prove_rep_datatype alt_names new_type_names descr sorts induct inject half_distinct thy =
   8.428 +  let
   8.429 +    val ((_, [induct']), _) =
   8.430 +      Variable.importT_thms [induct] (Variable.thm_context induct);
   8.431 +
   8.432 +    fun err t = error ("Ill-formed predicate in induction rule: " ^
   8.433 +      Syntax.string_of_term_global thy t);
   8.434 +
   8.435 +    fun get_typ (t as _ $ Var (_, Type (tname, Ts))) =
   8.436 +          ((tname, map (fst o dest_TFree) Ts) handle TERM _ => err t)
   8.437 +      | get_typ t = err t;
   8.438 +    val dtnames = map get_typ (HOLogic.dest_conj (HOLogic.dest_Trueprop (Thm.concl_of induct')));
   8.439 +
   8.440 +    val dt_info = get_datatypes thy;
   8.441 +
   8.442 +    val distinct = (map o maps) (fn thm => [thm, thm RS not_sym]) half_distinct;
   8.443 +    val (case_names_induct, case_names_exhausts) =
   8.444 +      (mk_case_names_induct descr, mk_case_names_exhausts descr (map #1 dtnames));
   8.445 +
   8.446 +    val _ = message ("Proofs for datatype(s) " ^ commas_quote new_type_names);
   8.447 +
   8.448 +    val (casedist_thms, thy2) = thy |>
   8.449 +      DatatypeAbsProofs.prove_casedist_thms new_type_names [descr] sorts induct
   8.450 +        case_names_exhausts;
   8.451 +    val ((reccomb_names, rec_thms), thy3) = DatatypeAbsProofs.prove_primrec_thms
   8.452 +      false new_type_names [descr] sorts dt_info inject distinct
   8.453 +      (Simplifier.theory_context thy2 dist_ss) induct thy2;
   8.454 +    val ((case_thms, case_names), thy4) = DatatypeAbsProofs.prove_case_thms false
   8.455 +      new_type_names [descr] sorts reccomb_names rec_thms thy3;
   8.456 +    val (split_thms, thy5) = DatatypeAbsProofs.prove_split_thms
   8.457 +      new_type_names [descr] sorts inject distinct casedist_thms case_thms thy4;
   8.458 +    val (nchotomys, thy6) = DatatypeAbsProofs.prove_nchotomys new_type_names
   8.459 +      [descr] sorts casedist_thms thy5;
   8.460 +    val (case_congs, thy7) = DatatypeAbsProofs.prove_case_congs new_type_names
   8.461 +      [descr] sorts nchotomys case_thms thy6;
   8.462 +    val (weak_case_congs, thy8) = DatatypeAbsProofs.prove_weak_case_congs new_type_names
   8.463 +      [descr] sorts thy7;
   8.464 +
   8.465 +    val ((_, [induct']), thy10) =
   8.466 +      thy8
   8.467 +      |> store_thmss "inject" new_type_names inject
   8.468 +      ||>> store_thmss "distinct" new_type_names distinct
   8.469 +      ||> Sign.add_path (space_implode "_" new_type_names)
   8.470 +      ||>> PureThy.add_thms [((Binding.name "induct", induct), [case_names_induct])];
   8.471 +
   8.472 +    val dt_infos = map (make_dt_info alt_names descr sorts induct' reccomb_names rec_thms)
   8.473 +      ((0 upto length descr - 1) ~~ descr ~~ case_names ~~ case_thms ~~ casedist_thms ~~
   8.474 +        map FewConstrs distinct ~~ inject ~~ nchotomys ~~ case_congs ~~ weak_case_congs);
   8.475 +
   8.476 +    val simps = flat (distinct @ inject @ case_thms) @ rec_thms;
   8.477 +
   8.478 +    val thy11 =
   8.479 +      thy10
   8.480 +      |> add_case_tr' case_names
   8.481 +      |> add_rules simps case_thms rec_thms inject distinct
   8.482 +           weak_case_congs (Simplifier.attrib (op addcongs))
   8.483 +      |> put_dt_infos dt_infos
   8.484 +      |> add_cases_induct dt_infos induct'
   8.485 +      |> Sign.parent_path
   8.486 +      |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)
   8.487 +      |> snd
   8.488 +      |> DatatypeInterpretation.data (map fst dt_infos);
   8.489 +  in
   8.490 +    ({distinct = distinct,
   8.491 +      inject = inject,
   8.492 +      exhaustion = casedist_thms,
   8.493 +      rec_thms = rec_thms,
   8.494 +      case_thms = case_thms,
   8.495 +      split_thms = split_thms,
   8.496 +      induction = induct',
   8.497 +      simps = simps}, thy11)
   8.498 +  end;
   8.499 +
   8.500 +fun gen_rep_datatype prep_term after_qed alt_names raw_ts thy =
   8.501 +  let
   8.502 +    fun constr_of_term (Const (c, T)) = (c, T)
   8.503 +      | constr_of_term t =
   8.504 +          error ("Not a constant: " ^ Syntax.string_of_term_global thy t);
   8.505 +    fun no_constr (c, T) = error ("Bad constructor: "
   8.506 +      ^ Sign.extern_const thy c ^ "::"
   8.507 +      ^ Syntax.string_of_typ_global thy T);
   8.508 +    fun type_of_constr (cT as (_, T)) =
   8.509 +      let
   8.510 +        val frees = OldTerm.typ_tfrees T;
   8.511 +        val (tyco, vs) = ((apsnd o map) (dest_TFree) o dest_Type o snd o strip_type) T
   8.512 +          handle TYPE _ => no_constr cT
   8.513 +        val _ = if has_duplicates (eq_fst (op =)) vs then no_constr cT else ();
   8.514 +        val _ = if length frees <> length vs then no_constr cT else ();
   8.515 +      in (tyco, (vs, cT)) end;
   8.516 +
   8.517 +    val raw_cs = AList.group (op =) (map (type_of_constr o constr_of_term o prep_term thy) raw_ts);
   8.518 +    val _ = case map_filter (fn (tyco, _) =>
   8.519 +        if Symtab.defined (get_datatypes thy) tyco then SOME tyco else NONE) raw_cs
   8.520 +     of [] => ()
   8.521 +      | tycos => error ("Type(s) " ^ commas (map quote tycos)
   8.522 +          ^ " already represented inductivly");
   8.523 +    val raw_vss = maps (map (map snd o fst) o snd) raw_cs;
   8.524 +    val ms = case distinct (op =) (map length raw_vss)
   8.525 +     of [n] => 0 upto n - 1
   8.526 +      | _ => error ("Different types in given constructors");
   8.527 +    fun inter_sort m = map (fn xs => nth xs m) raw_vss
   8.528 +      |> Library.foldr1 (Sorts.inter_sort (Sign.classes_of thy))
   8.529 +    val sorts = map inter_sort ms;
   8.530 +    val vs = Name.names Name.context Name.aT sorts;
   8.531 +
   8.532 +    fun norm_constr (raw_vs, (c, T)) = (c, map_atyps
   8.533 +      (TFree o (the o AList.lookup (op =) (map fst raw_vs ~~ vs)) o fst o dest_TFree) T);
   8.534 +
   8.535 +    val cs = map (apsnd (map norm_constr)) raw_cs;
   8.536 +    val dtyps_of_typ = map (dtyp_of_typ (map (rpair (map fst vs) o fst) cs))
   8.537 +      o fst o strip_type;
   8.538 +    val new_type_names = map Long_Name.base_name (the_default (map fst cs) alt_names);
   8.539 +
   8.540 +    fun mk_spec (i, (tyco, constr)) = (i, (tyco,
   8.541 +      map (DtTFree o fst) vs,
   8.542 +      (map o apsnd) dtyps_of_typ constr))
   8.543 +    val descr = map_index mk_spec cs;
   8.544 +    val injs = DatatypeProp.make_injs [descr] vs;
   8.545 +    val half_distincts = map snd (DatatypeProp.make_distincts [descr] vs);
   8.546 +    val ind = DatatypeProp.make_ind [descr] vs;
   8.547 +    val rules = (map o map o map) Logic.close_form [[[ind]], injs, half_distincts];
   8.548 +
   8.549 +    fun after_qed' raw_thms =
   8.550 +      let
   8.551 +        val [[[induct]], injs, half_distincts] =
   8.552 +          unflat rules (map Drule.zero_var_indexes_list raw_thms);
   8.553 +            (*FIXME somehow dubious*)
   8.554 +      in
   8.555 +        ProofContext.theory_result
   8.556 +          (prove_rep_datatype alt_names new_type_names descr vs induct injs half_distincts)
   8.557 +        #-> after_qed
   8.558 +      end;
   8.559 +  in
   8.560 +    thy
   8.561 +    |> ProofContext.init
   8.562 +    |> Proof.theorem_i NONE after_qed' ((map o map) (rpair []) (flat rules))
   8.563 +  end;
   8.564 +
   8.565 +val rep_datatype = gen_rep_datatype Sign.cert_term;
   8.566 +val rep_datatype_cmd = gen_rep_datatype Syntax.read_term_global (K I);
   8.567 +
   8.568 +
   8.569 +
   8.570 +(******************************** add datatype ********************************)
   8.571 +
   8.572 +fun gen_add_datatype prep_typ err flat_names new_type_names dts thy =
   8.573 +  let
   8.574 +    val _ = Theory.requires thy "Datatype" "datatype definitions";
   8.575 +
   8.576 +    (* this theory is used just for parsing *)
   8.577 +
   8.578 +    val tmp_thy = thy |>
   8.579 +      Theory.copy |>
   8.580 +      Sign.add_types (map (fn (tvs, tname, mx, _) =>
   8.581 +        (tname, length tvs, mx)) dts);
   8.582 +
   8.583 +    val (tyvars, _, _, _)::_ = dts;
   8.584 +    val (new_dts, types_syntax) = ListPair.unzip (map (fn (tvs, tname, mx, _) =>
   8.585 +      let val full_tname = Sign.full_name tmp_thy (Binding.map_name (Syntax.type_name mx) tname)
   8.586 +      in (case duplicates (op =) tvs of
   8.587 +            [] => if eq_set (tyvars, tvs) then ((full_tname, tvs), (tname, mx))
   8.588 +                  else error ("Mutually recursive datatypes must have same type parameters")
   8.589 +          | dups => error ("Duplicate parameter(s) for datatype " ^ quote (Binding.str_of tname) ^
   8.590 +              " : " ^ commas dups))
   8.591 +      end) dts);
   8.592 +
   8.593 +    val _ = (case duplicates (op =) (map fst new_dts) @ duplicates (op =) new_type_names of
   8.594 +      [] => () | dups => error ("Duplicate datatypes: " ^ commas dups));
   8.595 +
   8.596 +    fun prep_dt_spec ((tvs, tname, mx, constrs), tname') (dts', constr_syntax, sorts, i) =
   8.597 +      let
   8.598 +        fun prep_constr (cname, cargs, mx') (constrs, constr_syntax', sorts') =
   8.599 +          let
   8.600 +            val (cargs', sorts'') = Library.foldl (prep_typ tmp_thy) (([], sorts'), cargs);
   8.601 +            val _ = (case fold (curry OldTerm.add_typ_tfree_names) cargs' [] \\ tvs of
   8.602 +                [] => ()
   8.603 +              | vs => error ("Extra type variables on rhs: " ^ commas vs))
   8.604 +          in (constrs @ [((if flat_names then Sign.full_name tmp_thy else
   8.605 +                Sign.full_name_path tmp_thy tname')
   8.606 +                  (Binding.map_name (Syntax.const_name mx') cname),
   8.607 +                   map (dtyp_of_typ new_dts) cargs')],
   8.608 +              constr_syntax' @ [(cname, mx')], sorts'')
   8.609 +          end handle ERROR msg => cat_error msg
   8.610 +           ("The error above occured in constructor " ^ quote (Binding.str_of cname) ^
   8.611 +            " of datatype " ^ quote (Binding.str_of tname));
   8.612 +
   8.613 +        val (constrs', constr_syntax', sorts') =
   8.614 +          fold prep_constr constrs ([], [], sorts)
   8.615 +
   8.616 +      in
   8.617 +        case duplicates (op =) (map fst constrs') of
   8.618 +           [] =>
   8.619 +             (dts' @ [(i, (Sign.full_name tmp_thy (Binding.map_name (Syntax.type_name mx) tname),
   8.620 +                map DtTFree tvs, constrs'))],
   8.621 +              constr_syntax @ [constr_syntax'], sorts', i + 1)
   8.622 +         | dups => error ("Duplicate constructors " ^ commas dups ^
   8.623 +             " in datatype " ^ quote (Binding.str_of tname))
   8.624 +      end;
   8.625 +
   8.626 +    val (dts', constr_syntax, sorts', i) =
   8.627 +      fold prep_dt_spec (dts ~~ new_type_names) ([], [], [], 0);
   8.628 +    val sorts = sorts' @ (map (rpair (Sign.defaultS tmp_thy)) (tyvars \\ map fst sorts'));
   8.629 +    val dt_info = get_datatypes thy;
   8.630 +    val (descr, _) = unfold_datatypes tmp_thy dts' sorts dt_info dts' i;
   8.631 +    val _ = check_nonempty descr handle (exn as Datatype_Empty s) =>
   8.632 +      if err then error ("Nonemptiness check failed for datatype " ^ s)
   8.633 +      else raise exn;
   8.634 +
   8.635 +    val descr' = flat descr;
   8.636 +    val case_names_induct = mk_case_names_induct descr';
   8.637 +    val case_names_exhausts = mk_case_names_exhausts descr' (map #1 new_dts);
   8.638 +  in
   8.639 +    add_datatype_def
   8.640 +      flat_names new_type_names descr sorts types_syntax constr_syntax dt_info
   8.641 +      case_names_induct case_names_exhausts thy
   8.642 +  end;
   8.643 +
   8.644 +val add_datatype = gen_add_datatype cert_typ;
   8.645 +val add_datatype_cmd = gen_add_datatype read_typ true;
   8.646 +
   8.647 +
   8.648 +
   8.649 +(** package setup **)
   8.650 +
   8.651 +(* setup theory *)
   8.652 +
   8.653 +val setup =
   8.654 +  DatatypeRepProofs.distinctness_limit_setup #>
   8.655 +  simproc_setup #>
   8.656 +  trfun_setup #>
   8.657 +  DatatypeInterpretation.init;
   8.658 +
   8.659 +
   8.660 +(* outer syntax *)
   8.661 +
   8.662 +local structure P = OuterParse and K = OuterKeyword in
   8.663 +
   8.664 +val datatype_decl =
   8.665 +  Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.binding -- P.opt_infix --
   8.666 +    (P.$$$ "=" |-- P.enum1 "|" (P.binding -- Scan.repeat P.typ -- P.opt_mixfix));
   8.667 +
   8.668 +fun mk_datatype args =
   8.669 +  let
   8.670 +    val names = map
   8.671 +      (fn ((((NONE, _), t), _), _) => Binding.name_of t | ((((SOME t, _), _), _), _) => t) args;
   8.672 +    val specs = map (fn ((((_, vs), t), mx), cons) =>
   8.673 +      (vs, t, mx, map (fn ((x, y), z) => (x, y, z)) cons)) args;
   8.674 +  in snd o add_datatype_cmd false names specs end;
   8.675 +
   8.676 +val _ =
   8.677 +  OuterSyntax.command "datatype" "define inductive datatypes" K.thy_decl
   8.678 +    (P.and_list1 datatype_decl >> (Toplevel.theory o mk_datatype));
   8.679 +
   8.680 +val _ =
   8.681 +  OuterSyntax.command "rep_datatype" "represent existing types inductively" K.thy_goal
   8.682 +    (Scan.option (P.$$$ "(" |-- Scan.repeat1 P.name --| P.$$$ ")") -- Scan.repeat1 P.term
   8.683 +      >> (fn (alt_names, ts) => Toplevel.print
   8.684 +           o Toplevel.theory_to_proof (rep_datatype_cmd alt_names ts)));
   8.685 +
   8.686 +end;
   8.687 +
   8.688 +
   8.689 +(* document antiquotation *)
   8.690 +
   8.691 +val _ = ThyOutput.antiquotation "datatype" Args.tyname
   8.692 +  (fn {source = src, context = ctxt, ...} => fn dtco =>
   8.693 +    let
   8.694 +      val thy = ProofContext.theory_of ctxt;
   8.695 +      val (vs, cos) = the_datatype_spec thy dtco;
   8.696 +      val ty = Type (dtco, map TFree vs);
   8.697 +      fun pretty_typ_bracket (ty as Type (_, _ :: _)) =
   8.698 +            Pretty.enclose "(" ")" [Syntax.pretty_typ ctxt ty]
   8.699 +        | pretty_typ_bracket ty =
   8.700 +            Syntax.pretty_typ ctxt ty;
   8.701 +      fun pretty_constr (co, tys) =
   8.702 +        (Pretty.block o Pretty.breaks)
   8.703 +          (Syntax.pretty_term ctxt (Const (co, tys ---> ty)) ::
   8.704 +            map pretty_typ_bracket tys);
   8.705 +      val pretty_datatype =
   8.706 +        Pretty.block
   8.707 +          (Pretty.command "datatype" :: Pretty.brk 1 ::
   8.708 +           Syntax.pretty_typ ctxt ty ::
   8.709 +           Pretty.str " =" :: Pretty.brk 1 ::
   8.710 +           flat (separate [Pretty.brk 1, Pretty.str "| "]
   8.711 +             (map (single o pretty_constr) cos)));
   8.712 +    in ThyOutput.output (ThyOutput.maybe_pretty_source (K pretty_datatype) src [()]) end);
   8.713 +
   8.714 +end;
   8.715 +
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/HOL/Tools/datatype_package/datatype_prop.ML	Wed Jun 10 15:04:33 2009 +0200
     9.3 @@ -0,0 +1,435 @@
     9.4 +(*  Title:      HOL/Tools/datatype_prop.ML
     9.5 +    Author:     Stefan Berghofer, TU Muenchen
     9.6 +
     9.7 +Characteristic properties of datatypes.
     9.8 +*)
     9.9 +
    9.10 +signature DATATYPE_PROP =
    9.11 +sig
    9.12 +  val indexify_names: string list -> string list
    9.13 +  val make_tnames: typ list -> string list
    9.14 +  val make_injs : DatatypeAux.descr list -> (string * sort) list -> term list list
    9.15 +  val make_distincts : DatatypeAux.descr list ->
    9.16 +    (string * sort) list -> (int * term list) list (*no symmetric inequalities*)
    9.17 +  val make_ind : DatatypeAux.descr list -> (string * sort) list -> term
    9.18 +  val make_casedists : DatatypeAux.descr list -> (string * sort) list -> term list
    9.19 +  val make_primrec_Ts : DatatypeAux.descr list -> (string * sort) list ->
    9.20 +    string list -> typ list * typ list
    9.21 +  val make_primrecs : string list -> DatatypeAux.descr list ->
    9.22 +    (string * sort) list -> theory -> term list
    9.23 +  val make_cases : string list -> DatatypeAux.descr list ->
    9.24 +    (string * sort) list -> theory -> term list list
    9.25 +  val make_splits : string list -> DatatypeAux.descr list ->
    9.26 +    (string * sort) list -> theory -> (term * term) list
    9.27 +  val make_weak_case_congs : string list -> DatatypeAux.descr list ->
    9.28 +    (string * sort) list -> theory -> term list
    9.29 +  val make_case_congs : string list -> DatatypeAux.descr list ->
    9.30 +    (string * sort) list -> theory -> term list
    9.31 +  val make_nchotomys : DatatypeAux.descr list ->
    9.32 +    (string * sort) list -> term list
    9.33 +end;
    9.34 +
    9.35 +structure DatatypeProp : DATATYPE_PROP =
    9.36 +struct
    9.37 +
    9.38 +open DatatypeAux;
    9.39 +
    9.40 +fun indexify_names names =
    9.41 +  let
    9.42 +    fun index (x :: xs) tab =
    9.43 +      (case AList.lookup (op =) tab x of
    9.44 +        NONE => if member (op =) xs x then (x ^ "1") :: index xs ((x, 2) :: tab) else x :: index xs tab
    9.45 +      | SOME i => (x ^ string_of_int i) :: index xs ((x, i + 1) :: tab))
    9.46 +    | index [] _ = [];
    9.47 +  in index names [] end;
    9.48 +
    9.49 +fun make_tnames Ts =
    9.50 +  let
    9.51 +    fun type_name (TFree (name, _)) = implode (tl (explode name))
    9.52 +      | type_name (Type (name, _)) = 
    9.53 +          let val name' = Long_Name.base_name name
    9.54 +          in if Syntax.is_identifier name' then name' else "x" end;
    9.55 +  in indexify_names (map type_name Ts) end;
    9.56 +
    9.57 +
    9.58 +(************************* injectivity of constructors ************************)
    9.59 +
    9.60 +fun make_injs descr sorts =
    9.61 +  let
    9.62 +    val descr' = flat descr;
    9.63 +    fun make_inj T (cname, cargs) =
    9.64 +      if null cargs then I else
    9.65 +        let
    9.66 +          val Ts = map (typ_of_dtyp descr' sorts) cargs;
    9.67 +          val constr_t = Const (cname, Ts ---> T);
    9.68 +          val tnames = make_tnames Ts;
    9.69 +          val frees = map Free (tnames ~~ Ts);
    9.70 +          val frees' = map Free ((map ((op ^) o (rpair "'")) tnames) ~~ Ts);
    9.71 +        in cons (HOLogic.mk_Trueprop (HOLogic.mk_eq
    9.72 +          (HOLogic.mk_eq (list_comb (constr_t, frees), list_comb (constr_t, frees')),
    9.73 +           foldr1 (HOLogic.mk_binop "op &")
    9.74 +             (map HOLogic.mk_eq (frees ~~ frees')))))
    9.75 +        end;
    9.76 +  in
    9.77 +    map2 (fn d => fn T => fold_rev (make_inj T) (#3 (snd d)) [])
    9.78 +      (hd descr) (Library.take (length (hd descr), get_rec_types descr' sorts))
    9.79 +  end;
    9.80 +
    9.81 +
    9.82 +(************************* distinctness of constructors ***********************)
    9.83 +
    9.84 +fun make_distincts descr sorts =
    9.85 +  let
    9.86 +    val descr' = flat descr;
    9.87 +    val recTs = get_rec_types descr' sorts;
    9.88 +    val newTs = Library.take (length (hd descr), recTs);
    9.89 +
    9.90 +    fun prep_constr (cname, cargs) = (cname, map (typ_of_dtyp descr' sorts) cargs);
    9.91 +
    9.92 +    fun make_distincts' _ [] = []
    9.93 +      | make_distincts' T ((cname, cargs)::constrs) =
    9.94 +          let
    9.95 +            val frees = map Free ((make_tnames cargs) ~~ cargs);
    9.96 +            val t = list_comb (Const (cname, cargs ---> T), frees);
    9.97 +
    9.98 +            fun make_distincts'' (cname', cargs') =
    9.99 +              let
   9.100 +                val frees' = map Free ((map ((op ^) o (rpair "'"))
   9.101 +                  (make_tnames cargs')) ~~ cargs');
   9.102 +                val t' = list_comb (Const (cname', cargs' ---> T), frees')
   9.103 +              in
   9.104 +                HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.mk_eq (t, t'))
   9.105 +              end
   9.106 +
   9.107 +          in map make_distincts'' constrs @ make_distincts' T constrs end;
   9.108 +
   9.109 +  in
   9.110 +    map2 (fn ((_, (_, _, constrs))) => fn T =>
   9.111 +      (length constrs, make_distincts' T (map prep_constr constrs))) (hd descr) newTs
   9.112 +  end;
   9.113 +
   9.114 +
   9.115 +(********************************* induction **********************************)
   9.116 +
   9.117 +fun make_ind descr sorts =
   9.118 +  let
   9.119 +    val descr' = List.concat descr;
   9.120 +    val recTs = get_rec_types descr' sorts;
   9.121 +    val pnames = if length descr' = 1 then ["P"]
   9.122 +      else map (fn i => "P" ^ string_of_int i) (1 upto length descr');
   9.123 +
   9.124 +    fun make_pred i T =
   9.125 +      let val T' = T --> HOLogic.boolT
   9.126 +      in Free (List.nth (pnames, i), T') end;
   9.127 +
   9.128 +    fun make_ind_prem k T (cname, cargs) =
   9.129 +      let
   9.130 +        fun mk_prem ((dt, s), T) =
   9.131 +          let val (Us, U) = strip_type T
   9.132 +          in list_all (map (pair "x") Us, HOLogic.mk_Trueprop
   9.133 +            (make_pred (body_index dt) U $ app_bnds (Free (s, T)) (length Us)))
   9.134 +          end;
   9.135 +
   9.136 +        val recs = List.filter is_rec_type cargs;
   9.137 +        val Ts = map (typ_of_dtyp descr' sorts) cargs;
   9.138 +        val recTs' = map (typ_of_dtyp descr' sorts) recs;
   9.139 +        val tnames = Name.variant_list pnames (make_tnames Ts);
   9.140 +        val rec_tnames = map fst (List.filter (is_rec_type o snd) (tnames ~~ cargs));
   9.141 +        val frees = tnames ~~ Ts;
   9.142 +        val prems = map mk_prem (recs ~~ rec_tnames ~~ recTs');
   9.143 +
   9.144 +      in list_all_free (frees, Logic.list_implies (prems,
   9.145 +        HOLogic.mk_Trueprop (make_pred k T $ 
   9.146 +          list_comb (Const (cname, Ts ---> T), map Free frees))))
   9.147 +      end;
   9.148 +
   9.149 +    val prems = List.concat (map (fn ((i, (_, _, constrs)), T) =>
   9.150 +      map (make_ind_prem i T) constrs) (descr' ~~ recTs));
   9.151 +    val tnames = make_tnames recTs;
   9.152 +    val concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop "op &")
   9.153 +      (map (fn (((i, _), T), tname) => make_pred i T $ Free (tname, T))
   9.154 +        (descr' ~~ recTs ~~ tnames)))
   9.155 +
   9.156 +  in Logic.list_implies (prems, concl) end;
   9.157 +
   9.158 +(******************************* case distinction *****************************)
   9.159 +
   9.160 +fun make_casedists descr sorts =
   9.161 +  let
   9.162 +    val descr' = List.concat descr;
   9.163 +
   9.164 +    fun make_casedist_prem T (cname, cargs) =
   9.165 +      let
   9.166 +        val Ts = map (typ_of_dtyp descr' sorts) cargs;
   9.167 +        val frees = Name.variant_list ["P", "y"] (make_tnames Ts) ~~ Ts;
   9.168 +        val free_ts = map Free frees
   9.169 +      in list_all_free (frees, Logic.mk_implies (HOLogic.mk_Trueprop
   9.170 +        (HOLogic.mk_eq (Free ("y", T), list_comb (Const (cname, Ts ---> T), free_ts))),
   9.171 +          HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT))))
   9.172 +      end;
   9.173 +
   9.174 +    fun make_casedist ((_, (_, _, constrs)), T) =
   9.175 +      let val prems = map (make_casedist_prem T) constrs
   9.176 +      in Logic.list_implies (prems, HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT)))
   9.177 +      end
   9.178 +
   9.179 +  in map make_casedist
   9.180 +    ((hd descr) ~~ Library.take (length (hd descr), get_rec_types descr' sorts))
   9.181 +  end;
   9.182 +
   9.183 +(*************** characteristic equations for primrec combinator **************)
   9.184 +
   9.185 +fun make_primrec_Ts descr sorts used =
   9.186 +  let
   9.187 +    val descr' = List.concat descr;
   9.188 +
   9.189 +    val rec_result_Ts = map TFree (Name.variant_list used (replicate (length descr') "'t") ~~
   9.190 +      replicate (length descr') HOLogic.typeS);
   9.191 +
   9.192 +    val reccomb_fn_Ts = List.concat (map (fn (i, (_, _, constrs)) =>
   9.193 +      map (fn (_, cargs) =>
   9.194 +        let
   9.195 +          val Ts = map (typ_of_dtyp descr' sorts) cargs;
   9.196 +          val recs = List.filter (is_rec_type o fst) (cargs ~~ Ts);
   9.197 +
   9.198 +          fun mk_argT (dt, T) =
   9.199 +            binder_types T ---> List.nth (rec_result_Ts, body_index dt);
   9.200 +
   9.201 +          val argTs = Ts @ map mk_argT recs
   9.202 +        in argTs ---> List.nth (rec_result_Ts, i)
   9.203 +        end) constrs) descr');
   9.204 +
   9.205 +  in (rec_result_Ts, reccomb_fn_Ts) end;
   9.206 +
   9.207 +fun make_primrecs new_type_names descr sorts thy =
   9.208 +  let
   9.209 +    val descr' = List.concat descr;
   9.210 +    val recTs = get_rec_types descr' sorts;
   9.211 +    val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
   9.212 +
   9.213 +    val (rec_result_Ts, reccomb_fn_Ts) = make_primrec_Ts descr sorts used;
   9.214 +
   9.215 +    val rec_fns = map (uncurry (mk_Free "f"))
   9.216 +      (reccomb_fn_Ts ~~ (1 upto (length reccomb_fn_Ts)));
   9.217 +
   9.218 +    val big_reccomb_name = (space_implode "_" new_type_names) ^ "_rec";
   9.219 +    val reccomb_names = map (Sign.intern_const thy)
   9.220 +      (if length descr' = 1 then [big_reccomb_name] else
   9.221 +        (map ((curry (op ^) (big_reccomb_name ^ "_")) o string_of_int)
   9.222 +          (1 upto (length descr'))));
   9.223 +    val reccombs = map (fn ((name, T), T') => list_comb
   9.224 +      (Const (name, reccomb_fn_Ts @ [T] ---> T'), rec_fns))
   9.225 +        (reccomb_names ~~ recTs ~~ rec_result_Ts);
   9.226 +
   9.227 +    fun make_primrec T comb_t ((ts, f::fs), (cname, cargs)) =
   9.228 +      let
   9.229 +        val recs = List.filter is_rec_type cargs;
   9.230 +        val Ts = map (typ_of_dtyp descr' sorts) cargs;
   9.231 +        val recTs' = map (typ_of_dtyp descr' sorts) recs;
   9.232 +        val tnames = make_tnames Ts;
   9.233 +        val rec_tnames = map fst (List.filter (is_rec_type o snd) (tnames ~~ cargs));
   9.234 +        val frees = map Free (tnames ~~ Ts);
   9.235 +        val frees' = map Free (rec_tnames ~~ recTs');
   9.236 +
   9.237 +        fun mk_reccomb ((dt, T), t) =
   9.238 +          let val (Us, U) = strip_type T
   9.239 +          in list_abs (map (pair "x") Us,
   9.240 +            List.nth (reccombs, body_index dt) $ app_bnds t (length Us))
   9.241 +          end;
   9.242 +
   9.243 +        val reccombs' = map mk_reccomb (recs ~~ recTs' ~~ frees')
   9.244 +
   9.245 +      in (ts @ [HOLogic.mk_Trueprop (HOLogic.mk_eq
   9.246 +        (comb_t $ list_comb (Const (cname, Ts ---> T), frees),
   9.247 +         list_comb (f, frees @ reccombs')))], fs)
   9.248 +      end
   9.249 +
   9.250 +  in fst (Library.foldl (fn (x, ((dt, T), comb_t)) =>
   9.251 +    Library.foldl (make_primrec T comb_t) (x, #3 (snd dt)))
   9.252 +      (([], rec_fns), descr' ~~ recTs ~~ reccombs))
   9.253 +  end;
   9.254 +
   9.255 +(****************** make terms of form  t_case f1 ... fn  *********************)
   9.256 +
   9.257 +fun make_case_combs new_type_names descr sorts thy fname =
   9.258 +  let
   9.259 +    val descr' = List.concat descr;
   9.260 +    val recTs = get_rec_types descr' sorts;
   9.261 +    val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
   9.262 +    val newTs = Library.take (length (hd descr), recTs);
   9.263 +    val T' = TFree (Name.variant used "'t", HOLogic.typeS);
   9.264 +
   9.265 +    val case_fn_Ts = map (fn (i, (_, _, constrs)) =>
   9.266 +      map (fn (_, cargs) =>
   9.267 +        let val Ts = map (typ_of_dtyp descr' sorts) cargs
   9.268 +        in Ts ---> T' end) constrs) (hd descr);
   9.269 +
   9.270 +    val case_names = map (fn s =>
   9.271 +      Sign.intern_const thy (s ^ "_case")) new_type_names
   9.272 +  in
   9.273 +    map (fn ((name, Ts), T) => list_comb
   9.274 +      (Const (name, Ts @ [T] ---> T'),
   9.275 +        map (uncurry (mk_Free fname)) (Ts ~~ (1 upto length Ts))))
   9.276 +          (case_names ~~ case_fn_Ts ~~ newTs)
   9.277 +  end;
   9.278 +
   9.279 +(**************** characteristic equations for case combinator ****************)
   9.280 +
   9.281 +fun make_cases new_type_names descr sorts thy =
   9.282 +  let
   9.283 +    val descr' = List.concat descr;
   9.284 +    val recTs = get_rec_types descr' sorts;
   9.285 +    val newTs = Library.take (length (hd descr), recTs);
   9.286 +
   9.287 +    fun make_case T comb_t ((cname, cargs), f) =
   9.288 +      let
   9.289 +        val Ts = map (typ_of_dtyp descr' sorts) cargs;
   9.290 +        val frees = map Free ((make_tnames Ts) ~~ Ts)
   9.291 +      in HOLogic.mk_Trueprop (HOLogic.mk_eq
   9.292 +        (comb_t $ list_comb (Const (cname, Ts ---> T), frees),
   9.293 +         list_comb (f, frees)))
   9.294 +      end
   9.295 +
   9.296 +  in map (fn (((_, (_, _, constrs)), T), comb_t) =>
   9.297 +    map (make_case T comb_t) (constrs ~~ (snd (strip_comb comb_t))))
   9.298 +      ((hd descr) ~~ newTs ~~ (make_case_combs new_type_names descr sorts thy "f"))
   9.299 +  end;
   9.300 +
   9.301 +
   9.302 +(*************************** the "split" - equations **************************)
   9.303 +
   9.304 +fun make_splits new_type_names descr sorts thy =
   9.305 +  let
   9.306 +    val descr' = List.concat descr;
   9.307 +    val recTs = get_rec_types descr' sorts;
   9.308 +    val used' = List.foldr OldTerm.add_typ_tfree_names [] recTs;
   9.309 +    val newTs = Library.take (length (hd descr), recTs);
   9.310 +    val T' = TFree (Name.variant used' "'t", HOLogic.typeS);
   9.311 +    val P = Free ("P", T' --> HOLogic.boolT);
   9.312 +
   9.313 +    fun make_split (((_, (_, _, constrs)), T), comb_t) =
   9.314 +      let
   9.315 +        val (_, fs) = strip_comb comb_t;
   9.316 +        val used = ["P", "x"] @ (map (fst o dest_Free) fs);
   9.317 +
   9.318 +        fun process_constr (((cname, cargs), f), (t1s, t2s)) =
   9.319 +          let
   9.320 +            val Ts = map (typ_of_dtyp descr' sorts) cargs;
   9.321 +            val frees = map Free (Name.variant_list used (make_tnames Ts) ~~ Ts);
   9.322 +            val eqn = HOLogic.mk_eq (Free ("x", T),
   9.323 +              list_comb (Const (cname, Ts ---> T), frees));
   9.324 +            val P' = P $ list_comb (f, frees)
   9.325 +          in ((List.foldr (fn (Free (s, T), t) => HOLogic.mk_all (s, T, t))
   9.326 +                (HOLogic.imp $ eqn $ P') frees)::t1s,
   9.327 +              (List.foldr (fn (Free (s, T), t) => HOLogic.mk_exists (s, T, t))
   9.328 +                (HOLogic.conj $ eqn $ (HOLogic.Not $ P')) frees)::t2s)
   9.329 +          end;
   9.330 +
   9.331 +        val (t1s, t2s) = List.foldr process_constr ([], []) (constrs ~~ fs);
   9.332 +        val lhs = P $ (comb_t $ Free ("x", T))
   9.333 +      in
   9.334 +        (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, mk_conj t1s)),
   9.335 +         HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, HOLogic.Not $ mk_disj t2s)))
   9.336 +      end
   9.337 +
   9.338 +  in map make_split ((hd descr) ~~ newTs ~~
   9.339 +    (make_case_combs new_type_names descr sorts thy "f"))
   9.340 +  end;
   9.341 +
   9.342 +(************************* additional rules for TFL ***************************)
   9.343 +
   9.344 +fun make_weak_case_congs new_type_names descr sorts thy =
   9.345 +  let
   9.346 +    val case_combs = make_case_combs new_type_names descr sorts thy "f";
   9.347 +
   9.348 +    fun mk_case_cong comb =
   9.349 +      let 
   9.350 +        val Type ("fun", [T, _]) = fastype_of comb;
   9.351 +        val M = Free ("M", T);
   9.352 +        val M' = Free ("M'", T);
   9.353 +      in
   9.354 +        Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (M, M')),
   9.355 +          HOLogic.mk_Trueprop (HOLogic.mk_eq (comb $ M, comb $ M')))
   9.356 +      end
   9.357 +  in
   9.358 +    map mk_case_cong case_combs
   9.359 +  end;
   9.360 + 
   9.361 +
   9.362 +(*---------------------------------------------------------------------------
   9.363 + * Structure of case congruence theorem looks like this:
   9.364 + *
   9.365 + *    (M = M') 
   9.366 + *    ==> (!!x1,...,xk. (M' = C1 x1..xk) ==> (f1 x1..xk = g1 x1..xk)) 
   9.367 + *    ==> ... 
   9.368 + *    ==> (!!x1,...,xj. (M' = Cn x1..xj) ==> (fn x1..xj = gn x1..xj)) 
   9.369 + *    ==>
   9.370 + *      (ty_case f1..fn M = ty_case g1..gn M')
   9.371 + *---------------------------------------------------------------------------*)
   9.372 +
   9.373 +fun make_case_congs new_type_names descr sorts thy =
   9.374 +  let
   9.375 +    val case_combs = make_case_combs new_type_names descr sorts thy "f";
   9.376 +    val case_combs' = make_case_combs new_type_names descr sorts thy "g";
   9.377 +
   9.378 +    fun mk_case_cong ((comb, comb'), (_, (_, _, constrs))) =
   9.379 +      let
   9.380 +        val Type ("fun", [T, _]) = fastype_of comb;
   9.381 +        val (_, fs) = strip_comb comb;
   9.382 +        val (_, gs) = strip_comb comb';
   9.383 +        val used = ["M", "M'"] @ map (fst o dest_Free) (fs @ gs);
   9.384 +        val M = Free ("M", T);
   9.385 +        val M' = Free ("M'", T);
   9.386 +
   9.387 +        fun mk_clause ((f, g), (cname, _)) =
   9.388 +          let
   9.389 +            val (Ts, _) = strip_type (fastype_of f);
   9.390 +            val tnames = Name.variant_list used (make_tnames Ts);
   9.391 +            val frees = map Free (tnames ~~ Ts)
   9.392 +          in
   9.393 +            list_all_free (tnames ~~ Ts, Logic.mk_implies
   9.394 +              (HOLogic.mk_Trueprop
   9.395 +                (HOLogic.mk_eq (M', list_comb (Const (cname, Ts ---> T), frees))),
   9.396 +               HOLogic.mk_Trueprop
   9.397 +                (HOLogic.mk_eq (list_comb (f, frees), list_comb (g, frees)))))
   9.398 +          end
   9.399 +
   9.400 +      in
   9.401 +        Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (M, M')) ::
   9.402 +          map mk_clause (fs ~~ gs ~~ constrs),
   9.403 +            HOLogic.mk_Trueprop (HOLogic.mk_eq (comb $ M, comb' $ M')))
   9.404 +      end
   9.405 +
   9.406 +  in
   9.407 +    map mk_case_cong (case_combs ~~ case_combs' ~~ hd descr)
   9.408 +  end;
   9.409 +
   9.410 +(*---------------------------------------------------------------------------
   9.411 + * Structure of exhaustion theorem looks like this:
   9.412 + *
   9.413 + *    !v. (? y1..yi. v = C1 y1..yi) | ... | (? y1..yj. v = Cn y1..yj)
   9.414 + *---------------------------------------------------------------------------*)
   9.415 +
   9.416 +fun make_nchotomys descr sorts =
   9.417 +  let
   9.418 +    val descr' = List.concat descr;
   9.419 +    val recTs = get_rec_types descr' sorts;
   9.420 +    val newTs = Library.take (length (hd descr), recTs);
   9.421 +
   9.422 +    fun mk_eqn T (cname, cargs) =
   9.423 +      let
   9.424 +        val Ts = map (typ_of_dtyp descr' sorts) cargs;
   9.425 +        val tnames = Name.variant_list ["v"] (make_tnames Ts);
   9.426 +        val frees = tnames ~~ Ts
   9.427 +      in
   9.428 +        List.foldr (fn ((s, T'), t) => HOLogic.mk_exists (s, T', t))
   9.429 +          (HOLogic.mk_eq (Free ("v", T),
   9.430 +            list_comb (Const (cname, Ts ---> T), map Free frees))) frees
   9.431 +      end
   9.432 +
   9.433 +  in map (fn ((_, (_, _, constrs)), T) =>
   9.434 +    HOLogic.mk_Trueprop (HOLogic.mk_all ("v", T, mk_disj (map (mk_eqn T) constrs))))
   9.435 +      (hd descr ~~ newTs)
   9.436 +  end;
   9.437 +
   9.438 +end;
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/HOL/Tools/datatype_package/datatype_realizer.ML	Wed Jun 10 15:04:33 2009 +0200
    10.3 @@ -0,0 +1,230 @@
    10.4 +(*  Title:      HOL/Tools/datatype_realizer.ML
    10.5 +    Author:     Stefan Berghofer, TU Muenchen
    10.6 +
    10.7 +Porgram extraction from proofs involving datatypes:
    10.8 +Realizers for induction and case analysis
    10.9 +*)
   10.10 +
   10.11 +signature DATATYPE_REALIZER =
   10.12 +sig
   10.13 +  val add_dt_realizers: string list -> theory -> theory
   10.14 +  val setup: theory -> theory
   10.15 +end;
   10.16 +
   10.17 +structure DatatypeRealizer : DATATYPE_REALIZER =
   10.18 +struct
   10.19 +
   10.20 +open DatatypeAux;
   10.21 +
   10.22 +fun subsets i j = if i <= j then
   10.23 +       let val is = subsets (i+1) j
   10.24 +       in map (fn ks => i::ks) is @ is end
   10.25 +     else [[]];
   10.26 +
   10.27 +fun forall_intr_prf (t, prf) =
   10.28 +  let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
   10.29 +  in Abst (a, SOME T, Proofterm.prf_abstract_over t prf) end;
   10.30 +
   10.31 +fun prf_of thm =
   10.32 +  Reconstruct.reconstruct_proof (Thm.theory_of_thm thm) (Thm.prop_of thm) (Thm.proof_of thm);
   10.33 +
   10.34 +fun prf_subst_vars inst =
   10.35 +  Proofterm.map_proof_terms (subst_vars ([], inst)) I;
   10.36 +
   10.37 +fun is_unit t = snd (strip_type (fastype_of t)) = HOLogic.unitT;
   10.38 +
   10.39 +fun tname_of (Type (s, _)) = s
   10.40 +  | tname_of _ = "";
   10.41 +
   10.42 +fun mk_realizes T = Const ("realizes", T --> HOLogic.boolT --> HOLogic.boolT);
   10.43 +
   10.44 +fun make_ind sorts ({descr, rec_names, rec_rewrites, induction, ...} : datatype_info) is thy =
   10.45 +  let
   10.46 +    val recTs = get_rec_types descr sorts;
   10.47 +    val pnames = if length descr = 1 then ["P"]
   10.48 +      else map (fn i => "P" ^ string_of_int i) (1 upto length descr);
   10.49 +
   10.50 +    val rec_result_Ts = map (fn ((i, _), P) =>
   10.51 +      if i mem is then TFree ("'" ^ P, HOLogic.typeS) else HOLogic.unitT)
   10.52 +        (descr ~~ pnames);
   10.53 +
   10.54 +    fun make_pred i T U r x =
   10.55 +      if i mem is then
   10.56 +        Free (List.nth (pnames, i), T --> U --> HOLogic.boolT) $ r $ x
   10.57 +      else Free (List.nth (pnames, i), U --> HOLogic.boolT) $ x;
   10.58 +
   10.59 +    fun mk_all i s T t =
   10.60 +      if i mem is then list_all_free ([(s, T)], t) else t;
   10.61 +
   10.62 +    val (prems, rec_fns) = split_list (flat (fst (fold_map
   10.63 +      (fn ((i, (_, _, constrs)), T) => fold_map (fn (cname, cargs) => fn j =>
   10.64 +        let
   10.65 +          val Ts = map (typ_of_dtyp descr sorts) cargs;
   10.66 +          val tnames = Name.variant_list pnames (DatatypeProp.make_tnames Ts);
   10.67 +          val recs = filter (is_rec_type o fst o fst) (cargs ~~ tnames ~~ Ts);
   10.68 +          val frees = tnames ~~ Ts;
   10.69 +
   10.70 +          fun mk_prems vs [] = 
   10.71 +                let
   10.72 +                  val rT = nth (rec_result_Ts) i;
   10.73 +                  val vs' = filter_out is_unit vs;
   10.74 +                  val f = mk_Free "f" (map fastype_of vs' ---> rT) j;
   10.75 +                  val f' = Envir.eta_contract (list_abs_free
   10.76 +                    (map dest_Free vs, if i mem is then list_comb (f, vs')
   10.77 +                      else HOLogic.unit));
   10.78 +                in (HOLogic.mk_Trueprop (make_pred i rT T (list_comb (f, vs'))
   10.79 +                  (list_comb (Const (cname, Ts ---> T), map Free frees))), f')
   10.80 +                end
   10.81 +            | mk_prems vs (((dt, s), T) :: ds) = 
   10.82 +                let
   10.83 +                  val k = body_index dt;
   10.84 +                  val (Us, U) = strip_type T;
   10.85 +                  val i = length Us;
   10.86 +                  val rT = nth (rec_result_Ts) k;
   10.87 +                  val r = Free ("r" ^ s, Us ---> rT);
   10.88 +                  val (p, f) = mk_prems (vs @ [r]) ds
   10.89 +                in (mk_all k ("r" ^ s) (Us ---> rT) (Logic.mk_implies
   10.90 +                  (list_all (map (pair "x") Us, HOLogic.mk_Trueprop
   10.91 +                    (make_pred k rT U (app_bnds r i)
   10.92 +                      (app_bnds (Free (s, T)) i))), p)), f)
   10.93 +                end
   10.94 +
   10.95 +        in (apfst (curry list_all_free frees) (mk_prems (map Free frees) recs), j + 1) end)
   10.96 +          constrs) (descr ~~ recTs) 1)));
   10.97 + 
   10.98 +    fun mk_proj j [] t = t
   10.99 +      | mk_proj j (i :: is) t = if null is then t else
  10.100 +          if (j: int) = i then HOLogic.mk_fst t
  10.101 +          else mk_proj j is (HOLogic.mk_snd t);
  10.102 +
  10.103 +    val tnames = DatatypeProp.make_tnames recTs;
  10.104 +    val fTs = map fastype_of rec_fns;
  10.105 +    val ps = map (fn ((((i, _), T), U), s) => Abs ("x", T, make_pred i U T
  10.106 +      (list_comb (Const (s, fTs ---> T --> U), rec_fns) $ Bound 0) (Bound 0)))
  10.107 +        (descr ~~ recTs ~~ rec_result_Ts ~~ rec_names);
  10.108 +    val r = if null is then Extraction.nullt else
  10.109 +      foldr1 HOLogic.mk_prod (List.mapPartial (fn (((((i, _), T), U), s), tname) =>
  10.110 +        if i mem is then SOME
  10.111 +          (list_comb (Const (s, fTs ---> T --> U), rec_fns) $ Free (tname, T))
  10.112 +        else NONE) (descr ~~ recTs ~~ rec_result_Ts ~~ rec_names ~~ tnames));
  10.113 +    val concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop "op &")
  10.114 +      (map (fn ((((i, _), T), U), tname) =>
  10.115 +        make_pred i U T (mk_proj i is r) (Free (tname, T)))
  10.116 +          (descr ~~ recTs ~~ rec_result_Ts ~~ tnames)));
  10.117 +    val cert = cterm_of thy;
  10.118 +    val inst = map (pairself cert) (map head_of (HOLogic.dest_conj
  10.119 +      (HOLogic.dest_Trueprop (concl_of induction))) ~~ ps);
  10.120 +
  10.121 +    val thm = OldGoals.simple_prove_goal_cterm (cert (Logic.list_implies (prems, concl)))
  10.122 +      (fn prems =>
  10.123 +         [rewrite_goals_tac (map mk_meta_eq [fst_conv, snd_conv]),
  10.124 +          rtac (cterm_instantiate inst induction) 1,
  10.125 +          ALLGOALS ObjectLogic.atomize_prems_tac,
  10.126 +          rewrite_goals_tac (@{thm o_def} :: map mk_meta_eq rec_rewrites),
  10.127 +          REPEAT ((resolve_tac prems THEN_ALL_NEW (fn i =>
  10.128 +            REPEAT (etac allE i) THEN atac i)) 1)]);
  10.129 +
  10.130 +    val ind_name = Thm.get_name induction;
  10.131 +    val vs = map (fn i => List.nth (pnames, i)) is;
  10.132 +    val (thm', thy') = thy
  10.133 +      |> Sign.root_path
  10.134 +      |> PureThy.store_thm
  10.135 +        (Binding.qualified_name (space_implode "_" (ind_name :: vs @ ["correctness"])), thm)
  10.136 +      ||> Sign.restore_naming thy;
  10.137 +
  10.138 +    val ivs = rev (Term.add_vars (Logic.varify (DatatypeProp.make_ind [descr] sorts)) []);
  10.139 +    val rvs = rev (Thm.fold_terms Term.add_vars thm' []);
  10.140 +    val ivs1 = map Var (filter_out (fn (_, T) =>
  10.141 +      tname_of (body_type T) mem ["set", "bool"]) ivs);
  10.142 +    val ivs2 = map (fn (ixn, _) => Var (ixn, valOf (AList.lookup (op =) rvs ixn))) ivs;
  10.143 +
  10.144 +    val prf = List.foldr forall_intr_prf
  10.145 +     (List.foldr (fn ((f, p), prf) =>
  10.146 +        (case head_of (strip_abs_body f) of
  10.147 +           Free (s, T) =>
  10.148 +             let val T' = Logic.varifyT T
  10.149 +             in Abst (s, SOME T', Proofterm.prf_abstract_over
  10.150 +               (Var ((s, 0), T')) (AbsP ("H", SOME p, prf)))
  10.151 +             end
  10.152 +         | _ => AbsP ("H", SOME p, prf)))
  10.153 +           (Proofterm.proof_combP
  10.154 +             (prf_of thm', map PBound (length prems - 1 downto 0))) (rec_fns ~~ prems_of thm)) ivs2;
  10.155 +
  10.156 +    val r' = if null is then r else Logic.varify (List.foldr (uncurry lambda)
  10.157 +      r (map Logic.unvarify ivs1 @ filter_out is_unit
  10.158 +          (map (head_of o strip_abs_body) rec_fns)));
  10.159 +
  10.160 +  in Extraction.add_realizers_i [(ind_name, (vs, r', prf))] thy' end;
  10.161 +
  10.162 +
  10.163 +fun make_casedists sorts ({index, descr, case_name, case_rewrites, exhaustion, ...} : datatype_info) thy =
  10.164 +  let
  10.165 +    val cert = cterm_of thy;
  10.166 +    val rT = TFree ("'P", HOLogic.typeS);
  10.167 +    val rT' = TVar (("'P", 0), HOLogic.typeS);
  10.168 +
  10.169 +    fun make_casedist_prem T (cname, cargs) =
  10.170 +      let
  10.171 +        val Ts = map (typ_of_dtyp descr sorts) cargs;
  10.172 +        val frees = Name.variant_list ["P", "y"] (DatatypeProp.make_tnames Ts) ~~ Ts;
  10.173 +        val free_ts = map Free frees;
  10.174 +        val r = Free ("r" ^ Long_Name.base_name cname, Ts ---> rT)
  10.175 +      in (r, list_all_free (frees, Logic.mk_implies (HOLogic.mk_Trueprop
  10.176 +        (HOLogic.mk_eq (Free ("y", T), list_comb (Const (cname, Ts ---> T), free_ts))),
  10.177 +          HOLogic.mk_Trueprop (Free ("P", rT --> HOLogic.boolT) $
  10.178 +            list_comb (r, free_ts)))))
  10.179 +      end;
  10.180 +
  10.181 +    val SOME (_, _, constrs) = AList.lookup (op =) descr index;
  10.182 +    val T = List.nth (get_rec_types descr sorts, index);
  10.183 +    val (rs, prems) = split_list (map (make_casedist_prem T) constrs);
  10.184 +    val r = Const (case_name, map fastype_of rs ---> T --> rT);
  10.185 +
  10.186 +    val y = Var (("y", 0), Logic.legacy_varifyT T);
  10.187 +    val y' = Free ("y", T);
  10.188 +
  10.189 +    val thm = OldGoals.prove_goalw_cterm [] (cert (Logic.list_implies (prems,
  10.190 +      HOLogic.mk_Trueprop (Free ("P", rT --> HOLogic.boolT) $
  10.191 +        list_comb (r, rs @ [y'])))))
  10.192 +      (fn prems =>
  10.193 +         [rtac (cterm_instantiate [(cert y, cert y')] exhaustion) 1,
  10.194 +          ALLGOALS (EVERY'
  10.195 +            [asm_simp_tac (HOL_basic_ss addsimps case_rewrites),
  10.196 +             resolve_tac prems, asm_simp_tac HOL_basic_ss])]);
  10.197 +
  10.198 +    val exh_name = Thm.get_name exhaustion;
  10.199 +    val (thm', thy') = thy
  10.200 +      |> Sign.root_path
  10.201 +      |> PureThy.store_thm (Binding.qualified_name (exh_name ^ "_P_correctness"), thm)
  10.202 +      ||> Sign.restore_naming thy;
  10.203 +
  10.204 +    val P = Var (("P", 0), rT' --> HOLogic.boolT);
  10.205 +    val prf = forall_intr_prf (y, forall_intr_prf (P,
  10.206 +      List.foldr (fn ((p, r), prf) =>
  10.207 +        forall_intr_prf (Logic.legacy_varify r, AbsP ("H", SOME (Logic.varify p),
  10.208 +          prf))) (Proofterm.proof_combP (prf_of thm',
  10.209 +            map PBound (length prems - 1 downto 0))) (prems ~~ rs)));
  10.210 +    val r' = Logic.legacy_varify (Abs ("y", Logic.legacy_varifyT T,
  10.211 +      list_abs (map dest_Free rs, list_comb (r,
  10.212 +        map Bound ((length rs - 1 downto 0) @ [length rs])))));
  10.213 +
  10.214 +  in Extraction.add_realizers_i
  10.215 +    [(exh_name, (["P"], r', prf)),
  10.216 +     (exh_name, ([], Extraction.nullt, prf_of exhaustion))] thy'
  10.217 +  end;
  10.218 +
  10.219 +fun add_dt_realizers names thy =
  10.220 +  if ! Proofterm.proofs < 2 then thy
  10.221 +  else let
  10.222 +    val _ = message "Adding realizers for induction and case analysis ..."
  10.223 +    val infos = map (DatatypePackage.the_datatype thy) names;
  10.224 +    val info :: _ = infos;
  10.225 +  in
  10.226 +    thy
  10.227 +    |> fold_rev (make_ind (#sorts info) info) (subsets 0 (length (#descr info) - 1))
  10.228 +    |> fold_rev (make_casedists (#sorts info)) infos
  10.229 +  end;
  10.230 +
  10.231 +val setup = DatatypePackage.interpretation add_dt_realizers;
  10.232 +
  10.233 +end;
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/HOL/Tools/datatype_package/datatype_rep_proofs.ML	Wed Jun 10 15:04:33 2009 +0200
    11.3 @@ -0,0 +1,642 @@
    11.4 +(*  Title:      HOL/Tools/datatype_rep_proofs.ML
    11.5 +    Author:     Stefan Berghofer, TU Muenchen
    11.6 +
    11.7 +Definitional introduction of datatypes
    11.8 +Proof of characteristic theorems:
    11.9 +
   11.10 + - injectivity of constructors
   11.11 + - distinctness of constructors
   11.12 + - induction theorem
   11.13 +*)
   11.14 +
   11.15 +signature DATATYPE_REP_PROOFS =
   11.16 +sig
   11.17 +  val distinctness_limit : int Config.T
   11.18 +  val distinctness_limit_setup : theory -> theory
   11.19 +  val representation_proofs : bool -> DatatypeAux.datatype_info Symtab.table ->
   11.20 +    string list -> DatatypeAux.descr list -> (string * sort) list ->
   11.21 +      (binding * mixfix) list -> (binding * mixfix) list list -> attribute
   11.22 +        -> theory -> (thm list list * thm list list * thm list list *
   11.23 +          DatatypeAux.simproc_dist list * thm) * theory
   11.24 +end;
   11.25 +
   11.26 +structure DatatypeRepProofs : DATATYPE_REP_PROOFS =
   11.27 +struct
   11.28 +
   11.29 +open DatatypeAux;
   11.30 +
   11.31 +(*the kind of distinctiveness axioms depends on number of constructors*)
   11.32 +val (distinctness_limit, distinctness_limit_setup) =
   11.33 +  Attrib.config_int "datatype_distinctness_limit" 7;
   11.34 +
   11.35 +val (_ $ (_ $ (_ $ (distinct_f $ _) $ _))) = hd (prems_of distinct_lemma);
   11.36 +
   11.37 +val collect_simp = rewrite_rule [mk_meta_eq mem_Collect_eq];
   11.38 +
   11.39 +
   11.40 +(** theory context references **)
   11.41 +
   11.42 +val f_myinv_f = thm "f_myinv_f";
   11.43 +val myinv_f_f = thm "myinv_f_f";
   11.44 +
   11.45 +
   11.46 +fun exh_thm_of (dt_info : datatype_info Symtab.table) tname =
   11.47 +  #exhaustion (the (Symtab.lookup dt_info tname));
   11.48 +
   11.49 +(******************************************************************************)
   11.50 +
   11.51 +fun representation_proofs flat_names (dt_info : datatype_info Symtab.table)
   11.52 +      new_type_names descr sorts types_syntax constr_syntax case_names_induct thy =
   11.53 +  let
   11.54 +    val Datatype_thy = ThyInfo.the_theory "Datatype" thy;
   11.55 +    val node_name = "Datatype.node";
   11.56 +    val In0_name = "Datatype.In0";
   11.57 +    val In1_name = "Datatype.In1";
   11.58 +    val Scons_name = "Datatype.Scons";
   11.59 +    val Leaf_name = "Datatype.Leaf";
   11.60 +    val Numb_name = "Datatype.Numb";
   11.61 +    val Lim_name = "Datatype.Lim";
   11.62 +    val Suml_name = "Datatype.Suml";
   11.63 +    val Sumr_name = "Datatype.Sumr";
   11.64 +
   11.65 +    val [In0_inject, In1_inject, Scons_inject, Leaf_inject,
   11.66 +         In0_eq, In1_eq, In0_not_In1, In1_not_In0,
   11.67 +         Lim_inject, Suml_inject, Sumr_inject] = map (PureThy.get_thm Datatype_thy)
   11.68 +          ["In0_inject", "In1_inject", "Scons_inject", "Leaf_inject",
   11.69 +           "In0_eq", "In1_eq", "In0_not_In1", "In1_not_In0",
   11.70 +           "Lim_inject", "Suml_inject", "Sumr_inject"];
   11.71 +
   11.72 +    val descr' = flat descr;
   11.73 +
   11.74 +    val big_name = space_implode "_" new_type_names;
   11.75 +    val thy1 = add_path flat_names big_name thy;
   11.76 +    val big_rec_name = big_name ^ "_rep_set";
   11.77 +    val rep_set_names' =
   11.78 +      (if length descr' = 1 then [big_rec_name] else
   11.79 +        (map ((curry (op ^) (big_rec_name ^ "_")) o string_of_int)
   11.80 +          (1 upto (length descr'))));
   11.81 +    val rep_set_names = map (Sign.full_bname thy1) rep_set_names';
   11.82 +
   11.83 +    val tyvars = map (fn (_, (_, Ts, _)) => map dest_DtTFree Ts) (hd descr);
   11.84 +    val leafTs' = get_nonrec_types descr' sorts;
   11.85 +    val branchTs = get_branching_types descr' sorts;
   11.86 +    val branchT = if null branchTs then HOLogic.unitT
   11.87 +      else BalancedTree.make (fn (T, U) => Type ("+", [T, U])) branchTs;
   11.88 +    val arities = get_arities descr' \ 0;
   11.89 +    val unneeded_vars = hd tyvars \\ List.foldr OldTerm.add_typ_tfree_names [] (leafTs' @ branchTs);
   11.90 +    val leafTs = leafTs' @ (map (fn n => TFree (n, (the o AList.lookup (op =) sorts) n)) unneeded_vars);
   11.91 +    val recTs = get_rec_types descr' sorts;
   11.92 +    val newTs = Library.take (length (hd descr), recTs);
   11.93 +    val oldTs = Library.drop (length (hd descr), recTs);
   11.94 +    val sumT = if null leafTs then HOLogic.unitT
   11.95 +      else BalancedTree.make (fn (T, U) => Type ("+", [T, U])) leafTs;
   11.96 +    val Univ_elT = HOLogic.mk_setT (Type (node_name, [sumT, branchT]));
   11.97 +    val UnivT = HOLogic.mk_setT Univ_elT;
   11.98 +    val UnivT' = Univ_elT --> HOLogic.boolT;
   11.99 +    val Collect = Const ("Collect", UnivT' --> UnivT);
  11.100 +
  11.101 +    val In0 = Const (In0_name, Univ_elT --> Univ_elT);
  11.102 +    val In1 = Const (In1_name, Univ_elT --> Univ_elT);
  11.103 +    val Leaf = Const (Leaf_name, sumT --> Univ_elT);
  11.104 +    val Lim = Const (Lim_name, (branchT --> Univ_elT) --> Univ_elT);
  11.105 +
  11.106 +    (* make injections needed for embedding types in leaves *)
  11.107 +
  11.108 +    fun mk_inj T' x =
  11.109 +      let
  11.110 +        fun mk_inj' T n i =
  11.111 +          if n = 1 then x else
  11.112 +          let val n2 = n div 2;
  11.113 +              val Type (_, [T1, T2]) = T
  11.114 +          in
  11.115 +            if i <= n2 then
  11.116 +              Const ("Sum_Type.Inl", T1 --> T) $ (mk_inj' T1 n2 i)
  11.117 +            else
  11.118 +              Const ("Sum_Type.Inr", T2 --> T) $ (mk_inj' T2 (n - n2) (i - n2))
  11.119 +          end
  11.120 +      in mk_inj' sumT (length leafTs) (1 + find_index_eq T' leafTs)
  11.121 +      end;
  11.122 +
  11.123 +    (* make injections for constructors *)
  11.124 +
  11.125 +    fun mk_univ_inj ts = BalancedTree.access
  11.126 +      {left = fn t => In0 $ t,
  11.127 +        right = fn t => In1 $ t,
  11.128 +        init =
  11.129 +          if ts = [] then Const (@{const_name undefined}, Univ_elT)
  11.130 +          else foldr1 (HOLogic.mk_binop Scons_name) ts};
  11.131 +
  11.132 +    (* function spaces *)
  11.133 +
  11.134 +    fun mk_fun_inj T' x =
  11.135 +      let
  11.136 +        fun mk_inj T n i =
  11.137 +          if n = 1 then x else
  11.138 +          let
  11.139 +            val n2 = n div 2;
  11.140 +            val Type (_, [T1, T2]) = T;
  11.141 +            fun mkT U = (U --> Univ_elT) --> T --> Univ_elT
  11.142 +          in
  11.143 +            if i <= n2 then Const (Suml_name, mkT T1) $ mk_inj T1 n2 i
  11.144 +            else Const (Sumr_name, mkT T2) $ mk_inj T2 (n - n2) (i - n2)
  11.145 +          end
  11.146 +      in mk_inj branchT (length branchTs) (1 + find_index_eq T' branchTs)
  11.147 +      end;
  11.148 +
  11.149 +    val mk_lim = List.foldr (fn (T, t) => Lim $ mk_fun_inj T (Abs ("x", T, t)));
  11.150 +
  11.151 +    (************** generate introduction rules for representing set **********)
  11.152 +
  11.153 +    val _ = message "Constructing representing sets ...";
  11.154 +
  11.155 +    (* make introduction rule for a single constructor *)
  11.156 +
  11.157 +    fun make_intr s n (i, (_, cargs)) =
  11.158 +      let
  11.159 +        fun mk_prem (dt, (j, prems, ts)) = (case strip_dtyp dt of
  11.160 +            (dts, DtRec k) =>
  11.161 +              let
  11.162 +                val Ts = map (typ_of_dtyp descr' sorts) dts;
  11.163 +                val free_t =
  11.164 +                  app_bnds (mk_Free "x" (Ts ---> Univ_elT) j) (length Ts)
  11.165 +              in (j + 1, list_all (map (pair "x") Ts,
  11.166 +                  HOLogic.mk_Trueprop
  11.167 +                    (Free (List.nth (rep_set_names', k), UnivT') $ free_t)) :: prems,
  11.168 +                mk_lim free_t Ts :: ts)
  11.169 +              end
  11.170 +          | _ =>
  11.171 +              let val T = typ_of_dtyp descr' sorts dt
  11.172 +              in (j + 1, prems, (Leaf $ mk_inj T (mk_Free "x" T j))::ts)
  11.173 +              end);
  11.174 +
  11.175 +        val (_, prems, ts) = List.foldr mk_prem (1, [], []) cargs;
  11.176 +        val concl = HOLogic.mk_Trueprop
  11.177 +          (Free (s, UnivT') $ mk_univ_inj ts n i)
  11.178 +      in Logic.list_implies (prems, concl)
  11.179 +      end;
  11.180 +
  11.181 +    val intr_ts = maps (fn ((_, (_, _, constrs)), rep_set_name) =>
  11.182 +      map (make_intr rep_set_name (length constrs))
  11.183 +        ((1 upto (length constrs)) ~~ constrs)) (descr' ~~ rep_set_names');
  11.184 +
  11.185 +    val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy2) =
  11.186 +        InductivePackage.add_inductive_global (serial_string ())
  11.187 +          {quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK,
  11.188 +           alt_name = Binding.name big_rec_name, coind = false, no_elim = true, no_ind = false,
  11.189 +           skip_mono = true, fork_mono = false}
  11.190 +          (map (fn s => ((Binding.name s, UnivT'), NoSyn)) rep_set_names') []
  11.191 +          (map (fn x => (Attrib.empty_binding, x)) intr_ts) [] thy1;
  11.192 +
  11.193 +    (********************************* typedef ********************************)
  11.194 +
  11.195 +    val (typedefs, thy3) = thy2 |>
  11.196 +      parent_path flat_names |>
  11.197 +      fold_map (fn ((((name, mx), tvs), c), name') =>
  11.198 +          TypedefPackage.add_typedef false (SOME (Binding.name name')) (name, tvs, mx)
  11.199 +            (Collect $ Const (c, UnivT')) NONE
  11.200 +            (rtac exI 1 THEN rtac CollectI 1 THEN
  11.201 +              QUIET_BREADTH_FIRST (has_fewer_prems 1)
  11.202 +              (resolve_tac rep_intrs 1)))
  11.203 +                (types_syntax ~~ tyvars ~~
  11.204 +                  (Library.take (length newTs, rep_set_names)) ~~ new_type_names) ||>
  11.205 +      add_path flat_names big_name;
  11.206 +
  11.207 +    (*********************** definition of constructors ***********************)
  11.208 +
  11.209 +    val big_rep_name = (space_implode "_" new_type_names) ^ "_Rep_";
  11.210 +    val rep_names = map (curry op ^ "Rep_") new_type_names;
  11.211 +    val rep_names' = map (fn i => big_rep_name ^ (string_of_int i))
  11.212 +      (1 upto (length (flat (tl descr))));
  11.213 +    val all_rep_names = map (Sign.intern_const thy3) rep_names @
  11.214 +      map (Sign.full_bname thy3) rep_names';
  11.215 +
  11.216 +    (* isomorphism declarations *)
  11.217 +
  11.218 +    val iso_decls = map (fn (T, s) => (Binding.name s, T --> Univ_elT, NoSyn))
  11.219 +      (oldTs ~~ rep_names');
  11.220 +
  11.221 +    (* constructor definitions *)
  11.222 +
  11.223 +    fun make_constr_def tname T n ((thy, defs, eqns, i), ((cname, cargs), (cname', mx))) =
  11.224 +      let
  11.225 +        fun constr_arg (dt, (j, l_args, r_args)) =
  11.226 +          let val T = typ_of_dtyp descr' sorts dt;
  11.227 +              val free_t = mk_Free "x" T j
  11.228 +          in (case (strip_dtyp dt, strip_type T) of
  11.229 +              ((_, DtRec m), (Us, U)) => (j + 1, free_t :: l_args, mk_lim
  11.230 +                (Const (List.nth (all_rep_names, m), U --> Univ_elT) $
  11.231 +                   app_bnds free_t (length Us)) Us :: r_args)
  11.232 +            | _ => (j + 1, free_t::l_args, (Leaf $ mk_inj T free_t)::r_args))
  11.233 +          end;
  11.234 +
  11.235 +        val (_, l_args, r_args) = List.foldr constr_arg (1, [], []) cargs;
  11.236 +        val constrT = (map (typ_of_dtyp descr' sorts) cargs) ---> T;
  11.237 +        val abs_name = Sign.intern_const thy ("Abs_" ^ tname);
  11.238 +        val rep_name = Sign.intern_const thy ("Rep_" ^ tname);
  11.239 +        val lhs = list_comb (Const (cname, constrT), l_args);
  11.240 +        val rhs = mk_univ_inj r_args n i;
  11.241 +        val def = Logic.mk_equals (lhs, Const (abs_name, Univ_elT --> T) $ rhs);
  11.242 +        val def_name = Long_Name.base_name cname ^ "_def";
  11.243 +        val eqn = HOLogic.mk_Trueprop (HOLogic.mk_eq
  11.244 +          (Const (rep_name, T --> Univ_elT) $ lhs, rhs));
  11.245 +        val ([def_thm], thy') =
  11.246 +          thy
  11.247 +          |> Sign.add_consts_i [(cname', constrT, mx)]
  11.248 +          |> (PureThy.add_defs false o map Thm.no_attributes) [(Binding.name def_name, def)];
  11.249 +
  11.250 +      in (thy', defs @ [def_thm], eqns @ [eqn], i + 1) end;
  11.251 +
  11.252 +    (* constructor definitions for datatype *)
  11.253 +
  11.254 +    fun dt_constr_defs ((thy, defs, eqns, rep_congs, dist_lemmas),
  11.255 +        ((((_, (_, _, constrs)), tname), T), constr_syntax)) =
  11.256 +      let
  11.257 +        val _ $ (_ $ (cong_f $ _) $ _) = concl_of arg_cong;
  11.258 +        val rep_const = cterm_of thy
  11.259 +          (Const (Sign.intern_const thy ("Rep_" ^ tname), T --> Univ_elT));
  11.260 +        val cong' = standard (cterm_instantiate [(cterm_of thy cong_f, rep_const)] arg_cong);
  11.261 +        val dist = standard (cterm_instantiate [(cterm_of thy distinct_f, rep_const)] distinct_lemma);
  11.262 +        val (thy', defs', eqns', _) = Library.foldl ((make_constr_def tname T) (length constrs))
  11.263 +          ((add_path flat_names tname thy, defs, [], 1), constrs ~~ constr_syntax)
  11.264 +      in
  11.265 +        (parent_path flat_names thy', defs', eqns @ [eqns'],
  11.266 +          rep_congs @ [cong'], dist_lemmas @ [dist])
  11.267 +      end;
  11.268 +
  11.269 +    val (thy4, constr_defs, constr_rep_eqns, rep_congs, dist_lemmas) = Library.foldl dt_constr_defs
  11.270 +      ((thy3 |> Sign.add_consts_i iso_decls |> parent_path flat_names, [], [], [], []),
  11.271 +        hd descr ~~ new_type_names ~~ newTs ~~ constr_syntax);
  11.272 +
  11.273 +    (*********** isomorphisms for new types (introduced by typedef) ***********)
  11.274 +
  11.275 +    val _ = message "Proving isomorphism properties ...";
  11.276 +
  11.277 +    val newT_iso_axms = map (fn (_, td) =>
  11.278 +      (collect_simp (#Abs_inverse td), #Rep_inverse td,
  11.279 +       collect_simp (#Rep td))) typedefs;
  11.280 +
  11.281 +    val newT_iso_inj_thms = map (fn (_, td) =>
  11.282 +      (collect_simp (#Abs_inject td) RS iffD1, #Rep_inject td RS iffD1)) typedefs;
  11.283 +
  11.284 +    (********* isomorphisms between existing types and "unfolded" types *******)
  11.285 +
  11.286 +    (*---------------------------------------------------------------------*)
  11.287 +    (* isomorphisms are defined using primrec-combinators:                 *)
  11.288 +    (* generate appropriate functions for instantiating primrec-combinator *)
  11.289 +    (*                                                                     *)
  11.290 +    (*   e.g.  dt_Rep_i = list_rec ... (%h t y. In1 (Scons (Leaf h) y))    *)
  11.291 +    (*                                                                     *)
  11.292 +    (* also generate characteristic equations for isomorphisms             *)
  11.293 +    (*                                                                     *)
  11.294 +    (*   e.g.  dt_Rep_i (cons h t) = In1 (Scons (dt_Rep_j h) (dt_Rep_i t)) *)
  11.295 +    (*---------------------------------------------------------------------*)
  11.296 +
  11.297 +    fun make_iso_def k ks n ((fs, eqns, i), (cname, cargs)) =
  11.298 +      let
  11.299 +        val argTs = map (typ_of_dtyp descr' sorts) cargs;
  11.300 +        val T = List.nth (recTs, k);
  11.301 +        val rep_name = List.nth (all_rep_names, k);
  11.302 +        val rep_const = Const (rep_name, T --> Univ_elT);
  11.303 +        val constr = Const (cname, argTs ---> T);
  11.304 +
  11.305 +        fun process_arg ks' ((i2, i2', ts, Ts), dt) =
  11.306 +          let
  11.307 +            val T' = typ_of_dtyp descr' sorts dt;
  11.308 +            val (Us, U) = strip_type T'
  11.309 +          in (case strip_dtyp dt of
  11.310 +              (_, DtRec j) => if j mem ks' then
  11.311 +                  (i2 + 1, i2' + 1, ts @ [mk_lim (app_bnds
  11.312 +                     (mk_Free "y" (Us ---> Univ_elT) i2') (length Us)) Us],
  11.313 +                   Ts @ [Us ---> Univ_elT])
  11.314 +                else
  11.315 +                  (i2 + 1, i2', ts @ [mk_lim
  11.316 +                     (Const (List.nth (all_rep_names, j), U --> Univ_elT) $
  11.317 +                        app_bnds (mk_Free "x" T' i2) (length Us)) Us], Ts)
  11.318 +            | _ => (i2 + 1, i2', ts @ [Leaf $ mk_inj T' (mk_Free "x" T' i2)], Ts))
  11.319 +          end;
  11.320 +
  11.321 +        val (i2, i2', ts, Ts) = Library.foldl (process_arg ks) ((1, 1, [], []), cargs);
  11.322 +        val xs = map (uncurry (mk_Free "x")) (argTs ~~ (1 upto (i2 - 1)));
  11.323 +        val ys = map (uncurry (mk_Free "y")) (Ts ~~ (1 upto (i2' - 1)));
  11.324 +        val f = list_abs_free (map dest_Free (xs @ ys), mk_univ_inj ts n i);
  11.325 +
  11.326 +        val (_, _, ts', _) = Library.foldl (process_arg []) ((1, 1, [], []), cargs);
  11.327 +        val eqn = HOLogic.mk_Trueprop (HOLogic.mk_eq
  11.328 +          (rep_const $ list_comb (constr, xs), mk_univ_inj ts' n i))
  11.329 +
  11.330 +      in (fs @ [f], eqns @ [eqn], i + 1) end;
  11.331 +
  11.332 +    (* define isomorphisms for all mutually recursive datatypes in list ds *)
  11.333 +
  11.334 +    fun make_iso_defs (ds, (thy, char_thms)) =
  11.335 +      let
  11.336 +        val ks = map fst ds;
  11.337 +        val (_, (tname, _, _)) = hd ds;
  11.338 +        val {rec_rewrites, rec_names, ...} = the (Symtab.lookup dt_info tname);
  11.339 +
  11.340 +        fun process_dt ((fs, eqns, isos), (k, (tname, _, constrs))) =
  11.341 +          let
  11.342 +            val (fs', eqns', _) = Library.foldl (make_iso_def k ks (length constrs))
  11.343 +              ((fs, eqns, 1), constrs);
  11.344 +            val iso = (List.nth (recTs, k), List.nth (all_rep_names, k))
  11.345 +          in (fs', eqns', isos @ [iso]) end;
  11.346 +        
  11.347 +        val (fs, eqns, isos) = Library.foldl process_dt (([], [], []), ds);
  11.348 +        val fTs = map fastype_of fs;
  11.349 +        val defs = map (fn (rec_name, (T, iso_name)) => (Binding.name (Long_Name.base_name iso_name ^ "_def"),
  11.350 +          Logic.mk_equals (Const (iso_name, T --> Univ_elT),
  11.351 +            list_comb (Const (rec_name, fTs @ [T] ---> Univ_elT), fs)))) (rec_names ~~ isos);
  11.352 +        val (def_thms, thy') =
  11.353 +          apsnd Theory.checkpoint ((PureThy.add_defs false o map Thm.no_attributes) defs thy);
  11.354 +
  11.355 +        (* prove characteristic equations *)
  11.356 +
  11.357 +        val rewrites = def_thms @ (map mk_meta_eq rec_rewrites);
  11.358 +        val char_thms' = map (fn eqn => SkipProof.prove_global thy' [] [] eqn
  11.359 +          (fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1])) eqns;
  11.360 +
  11.361 +      in (thy', char_thms' @ char_thms) end;
  11.362 +
  11.363 +    val (thy5, iso_char_thms) = apfst Theory.checkpoint (List.foldr make_iso_defs
  11.364 +      (add_path flat_names big_name thy4, []) (tl descr));
  11.365 +
  11.366 +    (* prove isomorphism properties *)
  11.367 +
  11.368 +    fun mk_funs_inv thy thm =
  11.369 +      let
  11.370 +        val prop = Thm.prop_of thm;
  11.371 +        val _ $ (_ $ ((S as Const (_, Type (_, [U, _]))) $ _ )) $
  11.372 +          (_ $ (_ $ (r $ (a $ _)) $ _)) = Type.freeze prop;
  11.373 +        val used = OldTerm.add_term_tfree_names (a, []);
  11.374 +
  11.375 +        fun mk_thm i =
  11.376 +          let
  11.377 +            val Ts = map (TFree o rpair HOLogic.typeS)
  11.378 +              (Name.variant_list used (replicate i "'t"));
  11.379 +            val f = Free ("f", Ts ---> U)
  11.380 +          in SkipProof.prove_global thy [] [] (Logic.mk_implies
  11.381 +            (HOLogic.mk_Trueprop (HOLogic.list_all
  11.382 +               (map (pair "x") Ts, S $ app_bnds f i)),
  11.383 +             HOLogic.mk_Trueprop (HOLogic.mk_eq (list_abs (map (pair "x") Ts,
  11.384 +               r $ (a $ app_bnds f i)), f))))
  11.385 +            (fn _ => EVERY [REPEAT_DETERM_N i (rtac ext 1),
  11.386 +               REPEAT (etac allE 1), rtac thm 1, atac 1])
  11.387 +          end
  11.388 +      in map (fn r => r RS subst) (thm :: map mk_thm arities) end;
  11.389 +
  11.390 +    (* prove  inj dt_Rep_i  and  dt_Rep_i x : dt_rep_set_i *)
  11.391 +
  11.392 +    val fun_congs = map (fn T => make_elim (Drule.instantiate'
  11.393 +      [SOME (ctyp_of thy5 T)] [] fun_cong)) branchTs;
  11.394 +
  11.395 +    fun prove_iso_thms (ds, (inj_thms, elem_thms)) =
  11.396 +      let
  11.397 +        val (_, (tname, _, _)) = hd ds;
  11.398 +        val {induction, ...} = the (Symtab.lookup dt_info tname);
  11.399 +
  11.400 +        fun mk_ind_concl (i, _) =
  11.401 +          let
  11.402 +            val T = List.nth (recTs, i);
  11.403 +            val Rep_t = Const (List.nth (all_rep_names, i), T --> Univ_elT);
  11.404 +            val rep_set_name = List.nth (rep_set_names, i)
  11.405 +          in (HOLogic.all_const T $ Abs ("y", T, HOLogic.imp $
  11.406 +                HOLogic.mk_eq (Rep_t $ mk_Free "x" T i, Rep_t $ Bound 0) $
  11.407 +                  HOLogic.mk_eq (mk_Free "x" T i, Bound 0)),
  11.408 +              Const (rep_set_name, UnivT') $ (Rep_t $ mk_Free "x" T i))
  11.409 +          end;
  11.410 +
  11.411 +        val (ind_concl1, ind_concl2) = ListPair.unzip (map mk_ind_concl ds);
  11.412 +
  11.413 +        val rewrites = map mk_meta_eq iso_char_thms;
  11.414 +        val inj_thms' = map snd newT_iso_inj_thms @
  11.415 +          map (fn r => r RS @{thm injD}) inj_thms;
  11.416 +
  11.417 +        val inj_thm = SkipProof.prove_global thy5 [] []
  11.418 +          (HOLogic.mk_Trueprop (mk_conj ind_concl1)) (fn _ => EVERY
  11.419 +            [(indtac induction [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
  11.420 +             REPEAT (EVERY
  11.421 +               [rtac allI 1, rtac impI 1,
  11.422 +                exh_tac (exh_thm_of dt_info) 1,
  11.423 +                REPEAT (EVERY
  11.424 +                  [hyp_subst_tac 1,
  11.425 +                   rewrite_goals_tac rewrites,
  11.426 +                   REPEAT (dresolve_tac [In0_inject, In1_inject] 1),
  11.427 +                   (eresolve_tac [In0_not_In1 RS notE, In1_not_In0 RS notE] 1)
  11.428 +                   ORELSE (EVERY
  11.429 +                     [REPEAT (eresolve_tac (Scons_inject ::
  11.430 +                        map make_elim [Leaf_inject, Inl_inject, Inr_inject]) 1),
  11.431 +                      REPEAT (cong_tac 1), rtac refl 1,
  11.432 +                      REPEAT (atac 1 ORELSE (EVERY
  11.433 +                        [REPEAT (rtac ext 1),
  11.434 +                         REPEAT (eresolve_tac (mp :: allE ::
  11.435 +                           map make_elim (Suml_inject :: Sumr_inject ::
  11.436 +                             Lim_inject :: inj_thms') @ fun_congs) 1),
  11.437 +                         atac 1]))])])])]);
  11.438 +
  11.439 +        val inj_thms'' = map (fn r => r RS @{thm datatype_injI})
  11.440 +                             (split_conj_thm inj_thm);
  11.441 +
  11.442 +        val elem_thm = 
  11.443 +            SkipProof.prove_global thy5 [] [] (HOLogic.mk_Trueprop (mk_conj ind_concl2))
  11.444 +              (fn _ =>
  11.445 +               EVERY [(indtac induction [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
  11.446 +                rewrite_goals_tac rewrites,
  11.447 +                REPEAT ((resolve_tac rep_intrs THEN_ALL_NEW
  11.448 +                  ((REPEAT o etac allE) THEN' ares_tac elem_thms)) 1)]);
  11.449 +
  11.450 +      in (inj_thms'' @ inj_thms, elem_thms @ (split_conj_thm elem_thm))
  11.451 +      end;
  11.452 +
  11.453 +    val (iso_inj_thms_unfolded, iso_elem_thms) = List.foldr prove_iso_thms
  11.454 +      ([], map #3 newT_iso_axms) (tl descr);
  11.455 +    val iso_inj_thms = map snd newT_iso_inj_thms @
  11.456 +      map (fn r => r RS @{thm injD}) iso_inj_thms_unfolded;
  11.457 +
  11.458 +    (* prove  dt_rep_set_i x --> x : range dt_Rep_i *)
  11.459 +
  11.460 +    fun mk_iso_t (((set_name, iso_name), i), T) =
  11.461 +      let val isoT = T --> Univ_elT
  11.462 +      in HOLogic.imp $ 
  11.463 +        (Const (set_name, UnivT') $ mk_Free "x" Univ_elT i) $
  11.464 +          (if i < length newTs then Const ("True", HOLogic.boolT)
  11.465 +           else HOLogic.mk_mem (mk_Free "x" Univ_elT i,
  11.466 +             Const ("image", [isoT, HOLogic.mk_setT T] ---> UnivT) $
  11.467 +               Const (iso_name, isoT) $ Const (@{const_name UNIV}, HOLogic.mk_setT T)))
  11.468 +      end;
  11.469 +
  11.470 +    val iso_t = HOLogic.mk_Trueprop (mk_conj (map mk_iso_t
  11.471 +      (rep_set_names ~~ all_rep_names ~~ (0 upto (length descr' - 1)) ~~ recTs)));
  11.472 +
  11.473 +    (* all the theorems are proved by one single simultaneous induction *)
  11.474 +
  11.475 +    val range_eqs = map (fn r => mk_meta_eq (r RS @{thm range_ex1_eq}))
  11.476 +      iso_inj_thms_unfolded;
  11.477 +
  11.478 +    val iso_thms = if length descr = 1 then [] else
  11.479 +      Library.drop (length newTs, split_conj_thm
  11.480 +        (SkipProof.prove_global thy5 [] [] iso_t (fn _ => EVERY
  11.481 +           [(indtac rep_induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
  11.482 +            REPEAT (rtac TrueI 1),
  11.483 +            rewrite_goals_tac (mk_meta_eq choice_eq ::
  11.484 +              symmetric (mk_meta_eq @{thm expand_fun_eq}) :: range_eqs),
  11.485 +            rewrite_goals_tac (map symmetric range_eqs),
  11.486 +            REPEAT (EVERY
  11.487 +              [REPEAT (eresolve_tac ([rangeE, ex1_implies_ex RS exE] @
  11.488 +                 maps (mk_funs_inv thy5 o #1) newT_iso_axms) 1),
  11.489 +               TRY (hyp_subst_tac 1),
  11.490 +               rtac (sym RS range_eqI) 1,
  11.491 +               resolve_tac iso_char_thms 1])])));
  11.492 +
  11.493 +    val Abs_inverse_thms' =
  11.494 +      map #1 newT_iso_axms @
  11.495 +      map2 (fn r_inj => fn r => f_myinv_f OF [r_inj, r RS mp])
  11.496 +        iso_inj_thms_unfolded iso_thms;
  11.497 +
  11.498 +    val Abs_inverse_thms = maps (mk_funs_inv thy5) Abs_inverse_thms';
  11.499 +
  11.500 +    (******************* freeness theorems for constructors *******************)
  11.501 +
  11.502 +    val _ = message "Proving freeness of constructors ...";
  11.503 +
  11.504 +    (* prove theorem  Rep_i (Constr_j ...) = Inj_j ...  *)
  11.505 +    
  11.506 +    fun prove_constr_rep_thm eqn =
  11.507 +      let
  11.508 +        val inj_thms = map fst newT_iso_inj_thms;
  11.509 +        val rewrites = @{thm o_def} :: constr_defs @ (map (mk_meta_eq o #2) newT_iso_axms)
  11.510 +      in SkipProof.prove_global thy5 [] [] eqn (fn _ => EVERY
  11.511 +        [resolve_tac inj_thms 1,
  11.512 +         rewrite_goals_tac rewrites,
  11.513 +         rtac refl 3,
  11.514 +         resolve_tac rep_intrs 2,
  11.515 +         REPEAT (resolve_tac iso_elem_thms 1)])
  11.516 +      end;
  11.517 +
  11.518 +    (*--------------------------------------------------------------*)
  11.519 +    (* constr_rep_thms and rep_congs are used to prove distinctness *)
  11.520 +    (* of constructors.                                             *)
  11.521 +    (*--------------------------------------------------------------*)
  11.522 +
  11.523 +    val constr_rep_thms = map (map prove_constr_rep_thm) constr_rep_eqns;
  11.524 +
  11.525 +    val dist_rewrites = map (fn (rep_thms, dist_lemma) =>
  11.526 +      dist_lemma::(rep_thms @ [In0_eq, In1_eq, In0_not_In1, In1_not_In0]))
  11.527 +        (constr_rep_thms ~~ dist_lemmas);
  11.528 +
  11.529 +    fun prove_distinct_thms _ _ (_, []) = []
  11.530 +      | prove_distinct_thms lim dist_rewrites' (k, ts as _ :: _) =
  11.531 +          if k >= lim then [] else let
  11.532 +            (*number of constructors < distinctness_limit : C_i ... ~= C_j ...*)
  11.533 +            fun prove [] = []
  11.534 +              | prove (t :: ts) =
  11.535 +                  let
  11.536 +                    val dist_thm = SkipProof.prove_global thy5 [] [] t (fn _ =>
  11.537 +                      EVERY [simp_tac (HOL_ss addsimps dist_rewrites') 1])
  11.538 +                  in dist_thm :: standard (dist_thm RS not_sym) :: prove ts end;
  11.539 +          in prove ts end;
  11.540 +
  11.541 +    val distinct_thms = DatatypeProp.make_distincts descr sorts
  11.542 +      |> map2 (prove_distinct_thms
  11.543 +           (Config.get_thy thy5 distinctness_limit)) dist_rewrites;
  11.544 +
  11.545 +    val simproc_dists = map (fn ((((_, (_, _, constrs)), rep_thms), congr), dists) =>
  11.546 +      if length constrs < Config.get_thy thy5 distinctness_limit
  11.547 +      then FewConstrs dists
  11.548 +      else ManyConstrs (congr, HOL_basic_ss addsimps rep_thms)) (hd descr ~~
  11.549 +        constr_rep_thms ~~ rep_congs ~~ distinct_thms);
  11.550 +
  11.551 +    (* prove injectivity of constructors *)
  11.552 +
  11.553 +    fun prove_constr_inj_thm rep_thms t =
  11.554 +      let val inj_thms = Scons_inject :: (map make_elim
  11.555 +        (iso_inj_thms @
  11.556 +          [In0_inject, In1_inject, Leaf_inject, Inl_inject, Inr_inject,
  11.557 +           Lim_inject, Suml_inject, Sumr_inject]))
  11.558 +      in SkipProof.prove_global thy5 [] [] t (fn _ => EVERY
  11.559 +        [rtac iffI 1,
  11.560 +         REPEAT (etac conjE 2), hyp_subst_tac 2, rtac refl 2,
  11.561 +         dresolve_tac rep_congs 1, dtac box_equals 1,
  11.562 +         REPEAT (resolve_tac rep_thms 1),
  11.563 +         REPEAT (eresolve_tac inj_thms 1),
  11.564 +         REPEAT (ares_tac [conjI] 1 ORELSE (EVERY [REPEAT (rtac ext 1),
  11.565 +           REPEAT (eresolve_tac (make_elim fun_cong :: inj_thms) 1),
  11.566 +           atac 1]))])
  11.567 +      end;
  11.568 +
  11.569 +    val constr_inject = map (fn (ts, thms) => map (prove_constr_inj_thm thms) ts)
  11.570 +      ((DatatypeProp.make_injs descr sorts) ~~ constr_rep_thms);
  11.571 +
  11.572 +    val ((constr_inject', distinct_thms'), thy6) =
  11.573 +      thy5
  11.574 +      |> parent_path flat_names
  11.575 +      |> store_thmss "inject" new_type_names constr_inject
  11.576 +      ||>> store_thmss "distinct" new_type_names distinct_thms;
  11.577 +
  11.578 +    (*************************** induction theorem ****************************)
  11.579 +
  11.580 +    val _ = message "Proving induction rule for datatypes ...";
  11.581 +
  11.582 +    val Rep_inverse_thms = (map (fn (_, iso, _) => iso RS subst) newT_iso_axms) @
  11.583 +      (map (fn r => r RS myinv_f_f RS subst) iso_inj_thms_unfolded);
  11.584 +    val Rep_inverse_thms' = map (fn r => r RS myinv_f_f) iso_inj_thms_unfolded;
  11.585 +
  11.586 +    fun mk_indrule_lemma ((prems, concls), ((i, _), T)) =
  11.587 +      let
  11.588 +        val Rep_t = Const (List.nth (all_rep_names, i), T --> Univ_elT) $
  11.589 +          mk_Free "x" T i;
  11.590 +
  11.591 +        val Abs_t = if i < length newTs then
  11.592 +            Const (Sign.intern_const thy6
  11.593 +              ("Abs_" ^ (List.nth (new_type_names, i))), Univ_elT --> T)
  11.594 +          else Const ("Inductive.myinv", [T --> Univ_elT, Univ_elT] ---> T) $
  11.595 +            Const (List.nth (all_rep_names, i), T --> Univ_elT)
  11.596 +
  11.597 +      in (prems @ [HOLogic.imp $
  11.598 +            (Const (List.nth (rep_set_names, i), UnivT') $ Rep_t) $
  11.599 +              (mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ (Abs_t $ Rep_t))],
  11.600 +          concls @ [mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ mk_Free "x" T i])
  11.601 +      end;
  11.602 +
  11.603 +    val (indrule_lemma_prems, indrule_lemma_concls) =
  11.604 +      Library.foldl mk_indrule_lemma (([], []), (descr' ~~ recTs));
  11.605 +
  11.606 +    val cert = cterm_of thy6;
  11.607 +
  11.608 +    val indrule_lemma = SkipProof.prove_global thy6 [] []
  11.609 +      (Logic.mk_implies
  11.610 +        (HOLogic.mk_Trueprop (mk_conj indrule_lemma_prems),
  11.611 +         HOLogic.mk_Trueprop (mk_conj indrule_lemma_concls))) (fn _ => EVERY
  11.612 +           [REPEAT (etac conjE 1),
  11.613 +            REPEAT (EVERY
  11.614 +              [TRY (rtac conjI 1), resolve_tac Rep_inverse_thms 1,
  11.615 +               etac mp 1, resolve_tac iso_elem_thms 1])]);
  11.616 +
  11.617 +    val Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of indrule_lemma)));
  11.618 +    val frees = if length Ps = 1 then [Free ("P", snd (dest_Var (hd Ps)))] else
  11.619 +      map (Free o apfst fst o dest_Var) Ps;
  11.620 +    val indrule_lemma' = cterm_instantiate (map cert Ps ~~ map cert frees) indrule_lemma;
  11.621 +
  11.622 +    val dt_induct_prop = DatatypeProp.make_ind descr sorts;
  11.623 +    val dt_induct = SkipProof.prove_global thy6 []
  11.624 +      (Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop)
  11.625 +      (fn {prems, ...} => EVERY
  11.626 +        [rtac indrule_lemma' 1,
  11.627 +         (indtac rep_induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
  11.628 +         EVERY (map (fn (prem, r) => (EVERY
  11.629 +           [REPEAT (eresolve_tac Abs_inverse_thms 1),
  11.630 +            simp_tac (HOL_basic_ss addsimps ((symmetric r)::Rep_inverse_thms')) 1,
  11.631 +            DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE etac allE 1)]))
  11.632 +                (prems ~~ (constr_defs @ (map mk_meta_eq iso_char_thms))))]);
  11.633 +
  11.634 +    val ([dt_induct'], thy7) =
  11.635 +      thy6
  11.636 +      |> Sign.add_path big_name
  11.637 +      |> PureThy.add_thms [((Binding.name "induct", dt_induct), [case_names_induct])]
  11.638 +      ||> Sign.parent_path
  11.639 +      ||> Theory.checkpoint;
  11.640 +
  11.641 +  in
  11.642 +    ((constr_inject', distinct_thms', dist_rewrites, simproc_dists, dt_induct'), thy7)
  11.643 +  end;
  11.644 +
  11.645 +end;