src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
changeset 54701 4ed7454aebde
parent 54691 506312c293f5
child 54740 91f54d386680
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Dec 09 09:44:57 2013 +0100
     1.3 @@ -0,0 +1,981 @@
     1.4 +(*  Title:      HOL/Tools/Ctr_Sugar/ctr_sugar.ML
     1.5 +    Author:     Jasmin Blanchette, TU Muenchen
     1.6 +    Copyright   2012, 2013
     1.7 +
     1.8 +Wrapping existing freely generated type's constructors.
     1.9 +*)
    1.10 +
    1.11 +signature CTR_SUGAR =
    1.12 +sig
    1.13 +  type ctr_sugar =
    1.14 +    {ctrs: term list,
    1.15 +     casex: term,
    1.16 +     discs: term list,
    1.17 +     selss: term list list,
    1.18 +     exhaust: thm,
    1.19 +     nchotomy: thm,
    1.20 +     injects: thm list,
    1.21 +     distincts: thm list,
    1.22 +     case_thms: thm list,
    1.23 +     case_cong: thm,
    1.24 +     weak_case_cong: thm,
    1.25 +     split: thm,
    1.26 +     split_asm: thm,
    1.27 +     disc_thmss: thm list list,
    1.28 +     discIs: thm list,
    1.29 +     sel_thmss: thm list list,
    1.30 +     disc_exhausts: thm list,
    1.31 +     sel_exhausts: thm list,
    1.32 +     collapses: thm list,
    1.33 +     expands: thm list,
    1.34 +     sel_splits: thm list,
    1.35 +     sel_split_asms: thm list,
    1.36 +     case_eq_ifs: thm list};
    1.37 +
    1.38 +  val morph_ctr_sugar: morphism -> ctr_sugar -> ctr_sugar
    1.39 +  val transfer_ctr_sugar: Proof.context -> ctr_sugar -> ctr_sugar
    1.40 +  val ctr_sugar_of: Proof.context -> string -> ctr_sugar option
    1.41 +  val ctr_sugars_of: Proof.context -> ctr_sugar list
    1.42 +  val ctr_sugar_of_case: Proof.context -> string -> ctr_sugar option
    1.43 +  val register_ctr_sugar: string -> ctr_sugar -> local_theory -> local_theory
    1.44 +  val register_ctr_sugar_global: string -> ctr_sugar -> theory -> theory
    1.45 +
    1.46 +  val rep_compat_prefix: string
    1.47 +
    1.48 +  val mk_half_pairss: 'a list * 'a list -> ('a * 'a) list list
    1.49 +  val join_halves: int -> 'a list list -> 'a list list -> 'a list * 'a list list list
    1.50 +
    1.51 +  val mk_ctr: typ list -> term -> term
    1.52 +  val mk_case: typ list -> typ -> term -> term
    1.53 +  val mk_disc_or_sel: typ list -> term -> term
    1.54 +  val name_of_ctr: term -> string
    1.55 +  val name_of_disc: term -> string
    1.56 +  val dest_ctr: Proof.context -> string -> term -> term * term list
    1.57 +  val dest_case: Proof.context -> string -> typ list -> term -> (term list * term list) option
    1.58 +
    1.59 +  val wrap_free_constructors: ({prems: thm list, context: Proof.context} -> tactic) list list ->
    1.60 +    (((bool * (bool * bool)) * term list) * binding) *
    1.61 +      (binding list * (binding list list * (binding * term) list list)) -> local_theory ->
    1.62 +    ctr_sugar * local_theory
    1.63 +  val parse_wrap_free_constructors_options: (bool * (bool * bool)) parser
    1.64 +  val parse_bound_term: (binding * string) parser
    1.65 +end;
    1.66 +
    1.67 +structure Ctr_Sugar : CTR_SUGAR =
    1.68 +struct
    1.69 +
    1.70 +open Ctr_Sugar_Util
    1.71 +open Ctr_Sugar_Tactics
    1.72 +open Ctr_Sugar_Code
    1.73 +
    1.74 +type ctr_sugar =
    1.75 +  {ctrs: term list,
    1.76 +   casex: term,
    1.77 +   discs: term list,
    1.78 +   selss: term list list,
    1.79 +   exhaust: thm,
    1.80 +   nchotomy: thm,
    1.81 +   injects: thm list,
    1.82 +   distincts: thm list,
    1.83 +   case_thms: thm list,
    1.84 +   case_cong: thm,
    1.85 +   weak_case_cong: thm,
    1.86 +   split: thm,
    1.87 +   split_asm: thm,
    1.88 +   disc_thmss: thm list list,
    1.89 +   discIs: thm list,
    1.90 +   sel_thmss: thm list list,
    1.91 +   disc_exhausts: thm list,
    1.92 +   sel_exhausts: thm list,
    1.93 +   collapses: thm list,
    1.94 +   expands: thm list,
    1.95 +   sel_splits: thm list,
    1.96 +   sel_split_asms: thm list,
    1.97 +   case_eq_ifs: thm list};
    1.98 +
    1.99 +fun eq_ctr_sugar ({ctrs = ctrs1, casex = case1, discs = discs1, selss = selss1, ...} : ctr_sugar,
   1.100 +    {ctrs = ctrs2, casex = case2, discs = discs2, selss = selss2, ...} : ctr_sugar) =
   1.101 +  ctrs1 = ctrs2 andalso case1 = case2 andalso discs1 = discs2 andalso selss1 = selss2;
   1.102 +
   1.103 +fun morph_ctr_sugar phi {ctrs, casex, discs, selss, exhaust, nchotomy, injects, distincts,
   1.104 +    case_thms, case_cong, weak_case_cong, split, split_asm, disc_thmss, discIs, sel_thmss,
   1.105 +    disc_exhausts, sel_exhausts, collapses, expands, sel_splits, sel_split_asms, case_eq_ifs} =
   1.106 +  {ctrs = map (Morphism.term phi) ctrs,
   1.107 +   casex = Morphism.term phi casex,
   1.108 +   discs = map (Morphism.term phi) discs,
   1.109 +   selss = map (map (Morphism.term phi)) selss,
   1.110 +   exhaust = Morphism.thm phi exhaust,
   1.111 +   nchotomy = Morphism.thm phi nchotomy,
   1.112 +   injects = map (Morphism.thm phi) injects,
   1.113 +   distincts = map (Morphism.thm phi) distincts,
   1.114 +   case_thms = map (Morphism.thm phi) case_thms,
   1.115 +   case_cong = Morphism.thm phi case_cong,
   1.116 +   weak_case_cong = Morphism.thm phi weak_case_cong,
   1.117 +   split = Morphism.thm phi split,
   1.118 +   split_asm = Morphism.thm phi split_asm,
   1.119 +   disc_thmss = map (map (Morphism.thm phi)) disc_thmss,
   1.120 +   discIs = map (Morphism.thm phi) discIs,
   1.121 +   sel_thmss = map (map (Morphism.thm phi)) sel_thmss,
   1.122 +   disc_exhausts = map (Morphism.thm phi) disc_exhausts,
   1.123 +   sel_exhausts = map (Morphism.thm phi) sel_exhausts,
   1.124 +   collapses = map (Morphism.thm phi) collapses,
   1.125 +   expands = map (Morphism.thm phi) expands,
   1.126 +   sel_splits = map (Morphism.thm phi) sel_splits,
   1.127 +   sel_split_asms = map (Morphism.thm phi) sel_split_asms,
   1.128 +   case_eq_ifs = map (Morphism.thm phi) case_eq_ifs};
   1.129 +
   1.130 +val transfer_ctr_sugar =
   1.131 +  morph_ctr_sugar o Morphism.thm_morphism o Thm.transfer o Proof_Context.theory_of;
   1.132 +
   1.133 +structure Data = Generic_Data
   1.134 +(
   1.135 +  type T = ctr_sugar Symtab.table;
   1.136 +  val empty = Symtab.empty;
   1.137 +  val extend = I;
   1.138 +  val merge = Symtab.merge eq_ctr_sugar;
   1.139 +);
   1.140 +
   1.141 +fun ctr_sugar_of ctxt =
   1.142 +  Symtab.lookup (Data.get (Context.Proof ctxt))
   1.143 +  #> Option.map (transfer_ctr_sugar ctxt);
   1.144 +
   1.145 +fun ctr_sugars_of ctxt =
   1.146 +  Symtab.fold (cons o transfer_ctr_sugar ctxt o snd) (Data.get (Context.Proof ctxt)) [];
   1.147 +
   1.148 +fun ctr_sugar_of_case ctxt s =
   1.149 +  find_first (fn {casex = Const (s', _), ...} => s' = s | _ => false) (ctr_sugars_of ctxt);
   1.150 +
   1.151 +fun register_ctr_sugar key ctr_sugar =
   1.152 +  Local_Theory.declaration {syntax = false, pervasive = true}
   1.153 +    (fn phi => Data.map (Symtab.default (key, morph_ctr_sugar phi ctr_sugar)));
   1.154 +
   1.155 +fun register_ctr_sugar_global key ctr_sugar =
   1.156 +  Context.theory_map (Data.map (Symtab.default (key, ctr_sugar)));
   1.157 +
   1.158 +val rep_compat_prefix = "new";
   1.159 +
   1.160 +val isN = "is_";
   1.161 +val unN = "un_";
   1.162 +fun mk_unN 1 1 suf = unN ^ suf
   1.163 +  | mk_unN _ l suf = unN ^ suf ^ string_of_int l;
   1.164 +
   1.165 +val caseN = "case";
   1.166 +val case_congN = "case_cong";
   1.167 +val case_eq_ifN = "case_eq_if";
   1.168 +val collapseN = "collapse";
   1.169 +val disc_excludeN = "disc_exclude";
   1.170 +val disc_exhaustN = "disc_exhaust";
   1.171 +val discN = "disc";
   1.172 +val discIN = "discI";
   1.173 +val distinctN = "distinct";
   1.174 +val exhaustN = "exhaust";
   1.175 +val expandN = "expand";
   1.176 +val injectN = "inject";
   1.177 +val nchotomyN = "nchotomy";
   1.178 +val selN = "sel";
   1.179 +val sel_exhaustN = "sel_exhaust";
   1.180 +val sel_splitN = "sel_split";
   1.181 +val sel_split_asmN = "sel_split_asm";
   1.182 +val splitN = "split";
   1.183 +val splitsN = "splits";
   1.184 +val split_asmN = "split_asm";
   1.185 +val weak_case_cong_thmsN = "weak_case_cong";
   1.186 +
   1.187 +val cong_attrs = @{attributes [cong]};
   1.188 +val dest_attrs = @{attributes [dest]};
   1.189 +val safe_elim_attrs = @{attributes [elim!]};
   1.190 +val iff_attrs = @{attributes [iff]};
   1.191 +val inductsimp_attrs = @{attributes [induct_simp]};
   1.192 +val nitpicksimp_attrs = @{attributes [nitpick_simp]};
   1.193 +val simp_attrs = @{attributes [simp]};
   1.194 +val code_nitpicksimp_attrs = Code.add_default_eqn_attrib :: nitpicksimp_attrs;
   1.195 +val code_nitpicksimp_simp_attrs = code_nitpicksimp_attrs @ simp_attrs;
   1.196 +
   1.197 +fun unflat_lookup eq xs ys = map (fn xs' => permute_like eq xs xs' ys);
   1.198 +
   1.199 +fun mk_half_pairss' _ ([], []) = []
   1.200 +  | mk_half_pairss' indent (x :: xs, _ :: ys) =
   1.201 +    indent @ fold_rev (cons o single o pair x) ys (mk_half_pairss' ([] :: indent) (xs, ys));
   1.202 +
   1.203 +fun mk_half_pairss p = mk_half_pairss' [[]] p;
   1.204 +
   1.205 +fun join_halves n half_xss other_half_xss =
   1.206 +  let
   1.207 +    val xsss =
   1.208 +      map2 (map2 append) (Library.chop_groups n half_xss)
   1.209 +        (transpose (Library.chop_groups n other_half_xss))
   1.210 +    val xs = splice (flat half_xss) (flat other_half_xss);
   1.211 +  in (xs, xsss) end;
   1.212 +
   1.213 +fun mk_undefined T = Const (@{const_name undefined}, T);
   1.214 +
   1.215 +fun mk_ctr Ts t =
   1.216 +  let val Type (_, Ts0) = body_type (fastype_of t) in
   1.217 +    subst_nonatomic_types (Ts0 ~~ Ts) t
   1.218 +  end;
   1.219 +
   1.220 +fun mk_case Ts T t =
   1.221 +  let val (Type (_, Ts0), body) = strip_type (fastype_of t) |>> List.last in
   1.222 +    subst_nonatomic_types ((body, T) :: (Ts0 ~~ Ts)) t
   1.223 +  end;
   1.224 +
   1.225 +fun mk_disc_or_sel Ts t =
   1.226 +  subst_nonatomic_types (snd (Term.dest_Type (domain_type (fastype_of t))) ~~ Ts) t;
   1.227 +
   1.228 +fun name_of_const what t =
   1.229 +  (case head_of t of
   1.230 +    Const (s, _) => s
   1.231 +  | Free (s, _) => s
   1.232 +  | _ => error ("Cannot extract name of " ^ what));
   1.233 +
   1.234 +val name_of_ctr = name_of_const "constructor";
   1.235 +
   1.236 +val notN = "not_";
   1.237 +val eqN = "eq_";
   1.238 +val neqN = "neq_";
   1.239 +
   1.240 +fun name_of_disc t =
   1.241 +  (case head_of t of
   1.242 +    Abs (_, _, @{const Not} $ (t' $ Bound 0)) =>
   1.243 +    Long_Name.map_base_name (prefix notN) (name_of_disc t')
   1.244 +  | Abs (_, _, Const (@{const_name HOL.eq}, _) $ Bound 0 $ t') =>
   1.245 +    Long_Name.map_base_name (prefix eqN) (name_of_disc t')
   1.246 +  | Abs (_, _, @{const Not} $ (Const (@{const_name HOL.eq}, _) $ Bound 0 $ t')) =>
   1.247 +    Long_Name.map_base_name (prefix neqN) (name_of_disc t')
   1.248 +  | t' => name_of_const "destructor" t');
   1.249 +
   1.250 +val base_name_of_ctr = Long_Name.base_name o name_of_ctr;
   1.251 +
   1.252 +fun dest_ctr ctxt s t =
   1.253 +  let
   1.254 +    val (f, args) = Term.strip_comb t;
   1.255 +  in
   1.256 +    (case ctr_sugar_of ctxt s of
   1.257 +      SOME {ctrs, ...} =>
   1.258 +      (case find_first (can (fo_match ctxt f)) ctrs of
   1.259 +        SOME f' => (f', args)
   1.260 +      | NONE => raise Fail "dest_ctr")
   1.261 +    | NONE => raise Fail "dest_ctr")
   1.262 +  end;
   1.263 +
   1.264 +fun dest_case ctxt s Ts t =
   1.265 +  (case Term.strip_comb t of
   1.266 +    (Const (c, _), args as _ :: _) =>
   1.267 +    (case ctr_sugar_of ctxt s of
   1.268 +      SOME {casex = Const (case_name, _), discs = discs0, selss = selss0, ...} =>
   1.269 +      if case_name = c then
   1.270 +        let val n = length discs0 in
   1.271 +          if n < length args then
   1.272 +            let
   1.273 +              val (branches, obj :: leftovers) = chop n args;
   1.274 +              val discs = map (mk_disc_or_sel Ts) discs0;
   1.275 +              val selss = map (map (mk_disc_or_sel Ts)) selss0;
   1.276 +              val conds = map (rapp obj) discs;
   1.277 +              val branch_argss = map (fn sels => map (rapp obj) sels @ leftovers) selss;
   1.278 +              val branches' = map2 (curry Term.betapplys) branches branch_argss;
   1.279 +            in
   1.280 +              SOME (conds, branches')
   1.281 +            end
   1.282 +          else
   1.283 +            NONE
   1.284 +        end
   1.285 +      else
   1.286 +        NONE
   1.287 +    | _ => NONE)
   1.288 +  | _ => NONE);
   1.289 +
   1.290 +fun eta_expand_arg xs f_xs = fold_rev Term.lambda xs f_xs;
   1.291 +
   1.292 +fun prepare_wrap_free_constructors prep_term ((((no_discs_sels, (no_code, rep_compat)), raw_ctrs),
   1.293 +    raw_case_binding), (raw_disc_bindings, (raw_sel_bindingss, raw_sel_defaultss))) no_defs_lthy =
   1.294 +  let
   1.295 +    (* TODO: sanity checks on arguments *)
   1.296 +
   1.297 +    val n = length raw_ctrs;
   1.298 +    val ks = 1 upto n;
   1.299 +
   1.300 +    val _ = if n > 0 then () else error "No constructors specified";
   1.301 +
   1.302 +    val ctrs0 = map (prep_term no_defs_lthy) raw_ctrs;
   1.303 +    val sel_defaultss =
   1.304 +      pad_list [] n (map (map (apsnd (prep_term no_defs_lthy))) raw_sel_defaultss);
   1.305 +
   1.306 +    val Type (fcT_name, As0) = body_type (fastype_of (hd ctrs0));
   1.307 +    val fc_b_name = Long_Name.base_name fcT_name;
   1.308 +    val fc_b = Binding.name fc_b_name;
   1.309 +
   1.310 +    fun qualify mandatory =
   1.311 +      Binding.qualify mandatory fc_b_name o (rep_compat ? Binding.qualify false rep_compat_prefix);
   1.312 +
   1.313 +    fun dest_TFree_or_TVar (TFree sS) = sS
   1.314 +      | dest_TFree_or_TVar (TVar ((s, _), S)) = (s, S)
   1.315 +      | dest_TFree_or_TVar _ = error "Invalid type argument";
   1.316 +
   1.317 +    val (unsorted_As, B) =
   1.318 +      no_defs_lthy
   1.319 +      |> variant_tfrees (map (fst o dest_TFree_or_TVar) As0)
   1.320 +      ||> the_single o fst o mk_TFrees 1;
   1.321 +
   1.322 +    val As = map2 (resort_tfree o snd o dest_TFree_or_TVar) As0 unsorted_As;
   1.323 +
   1.324 +    val fcT = Type (fcT_name, As);
   1.325 +    val ctrs = map (mk_ctr As) ctrs0;
   1.326 +    val ctr_Tss = map (binder_types o fastype_of) ctrs;
   1.327 +
   1.328 +    val ms = map length ctr_Tss;
   1.329 +
   1.330 +    val raw_disc_bindings' = pad_list Binding.empty n raw_disc_bindings;
   1.331 +
   1.332 +    fun can_definitely_rely_on_disc k = not (Binding.is_empty (nth raw_disc_bindings' (k - 1)));
   1.333 +    fun can_rely_on_disc k =
   1.334 +      can_definitely_rely_on_disc k orelse (k = 1 andalso not (can_definitely_rely_on_disc 2));
   1.335 +    fun should_omit_disc_binding k = n = 1 orelse (n = 2 andalso can_rely_on_disc (3 - k));
   1.336 +
   1.337 +    fun is_disc_binding_valid b =
   1.338 +      not (Binding.is_empty b orelse Binding.eq_name (b, equal_binding));
   1.339 +
   1.340 +    val standard_disc_binding = Binding.name o prefix isN o base_name_of_ctr;
   1.341 +
   1.342 +    val disc_bindings =
   1.343 +      raw_disc_bindings'
   1.344 +      |> map4 (fn k => fn m => fn ctr => fn disc =>
   1.345 +        qualify false
   1.346 +          (if Binding.is_empty disc then
   1.347 +             if should_omit_disc_binding k then disc else standard_disc_binding ctr
   1.348 +           else if Binding.eq_name (disc, equal_binding) then
   1.349 +             if m = 0 then disc
   1.350 +             else error "Cannot use \"=\" syntax for discriminating nonnullary constructor"
   1.351 +           else if Binding.eq_name (disc, standard_binding) then
   1.352 +             standard_disc_binding ctr
   1.353 +           else
   1.354 +             disc)) ks ms ctrs0;
   1.355 +
   1.356 +    fun standard_sel_binding m l = Binding.name o mk_unN m l o base_name_of_ctr;
   1.357 +
   1.358 +    val sel_bindingss =
   1.359 +      pad_list [] n raw_sel_bindingss
   1.360 +      |> map3 (fn ctr => fn m => map2 (fn l => fn sel =>
   1.361 +        qualify false
   1.362 +          (if Binding.is_empty sel orelse Binding.eq_name (sel, standard_binding) then
   1.363 +            standard_sel_binding m l ctr
   1.364 +          else
   1.365 +            sel)) (1 upto m) o pad_list Binding.empty m) ctrs0 ms;
   1.366 +
   1.367 +    val case_Ts = map (fn Ts => Ts ---> B) ctr_Tss;
   1.368 +
   1.369 +    val ((((((((xss, xss'), yss), fs), gs), [u', v']), [w]), (p, p')), names_lthy) = no_defs_lthy |>
   1.370 +      mk_Freess' "x" ctr_Tss
   1.371 +      ||>> mk_Freess "y" ctr_Tss
   1.372 +      ||>> mk_Frees "f" case_Ts
   1.373 +      ||>> mk_Frees "g" case_Ts
   1.374 +      ||>> (apfst (map (rpair fcT)) oo Variable.variant_fixes) [fc_b_name, fc_b_name ^ "'"]
   1.375 +      ||>> mk_Frees "z" [B]
   1.376 +      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "P") HOLogic.boolT;
   1.377 +
   1.378 +    val u = Free u';
   1.379 +    val v = Free v';
   1.380 +    val q = Free (fst p', mk_pred1T B);
   1.381 +
   1.382 +    val xctrs = map2 (curry Term.list_comb) ctrs xss;
   1.383 +    val yctrs = map2 (curry Term.list_comb) ctrs yss;
   1.384 +
   1.385 +    val xfs = map2 (curry Term.list_comb) fs xss;
   1.386 +    val xgs = map2 (curry Term.list_comb) gs xss;
   1.387 +
   1.388 +    (* TODO: Eta-expension is for compatibility with the old datatype package (but it also provides
   1.389 +       nicer names). Consider removing. *)
   1.390 +    val eta_fs = map2 eta_expand_arg xss xfs;
   1.391 +    val eta_gs = map2 eta_expand_arg xss xgs;
   1.392 +
   1.393 +    val case_binding =
   1.394 +      qualify false
   1.395 +        (if Binding.is_empty raw_case_binding orelse
   1.396 +            Binding.eq_name (raw_case_binding, standard_binding) then
   1.397 +           Binding.prefix_name (caseN ^ "_") fc_b
   1.398 +         else
   1.399 +           raw_case_binding);
   1.400 +
   1.401 +    fun mk_case_disj xctr xf xs =
   1.402 +      list_exists_free xs (HOLogic.mk_conj (HOLogic.mk_eq (u, xctr), HOLogic.mk_eq (w, xf)));
   1.403 +
   1.404 +    val case_rhs = fold_rev (fold_rev Term.lambda) [fs, [u]]
   1.405 +      (Const (@{const_name The}, (B --> HOLogic.boolT) --> B) $
   1.406 +         Term.lambda w (Library.foldr1 HOLogic.mk_disj (map3 mk_case_disj xctrs xfs xss)));
   1.407 +
   1.408 +    val ((raw_case, (_, raw_case_def)), (lthy', lthy)) = no_defs_lthy
   1.409 +      |> Local_Theory.define ((case_binding, NoSyn),
   1.410 +        ((Binding.conceal (Thm.def_binding case_binding), []), case_rhs))
   1.411 +      ||> `Local_Theory.restore;
   1.412 +
   1.413 +    val phi = Proof_Context.export_morphism lthy lthy';
   1.414 +
   1.415 +    val case_def = Morphism.thm phi raw_case_def;
   1.416 +
   1.417 +    val case0 = Morphism.term phi raw_case;
   1.418 +    val casex = mk_case As B case0;
   1.419 +
   1.420 +    val fcase = Term.list_comb (casex, fs);
   1.421 +
   1.422 +    val ufcase = fcase $ u;
   1.423 +    val vfcase = fcase $ v;
   1.424 +
   1.425 +    val eta_fcase = Term.list_comb (casex, eta_fs);
   1.426 +    val eta_gcase = Term.list_comb (casex, eta_gs);
   1.427 +
   1.428 +    val eta_ufcase = eta_fcase $ u;
   1.429 +    val eta_vgcase = eta_gcase $ v;
   1.430 +
   1.431 +    fun mk_uu_eq () = HOLogic.mk_eq (u, u);
   1.432 +
   1.433 +    val uv_eq = mk_Trueprop_eq (u, v);
   1.434 +
   1.435 +    val exist_xs_u_eq_ctrs =
   1.436 +      map2 (fn xctr => fn xs => list_exists_free xs (HOLogic.mk_eq (u, xctr))) xctrs xss;
   1.437 +
   1.438 +    val unique_disc_no_def = TrueI; (*arbitrary marker*)
   1.439 +    val alternate_disc_no_def = FalseE; (*arbitrary marker*)
   1.440 +
   1.441 +    fun alternate_disc_lhs get_udisc k =
   1.442 +      HOLogic.mk_not
   1.443 +        (let val b = nth disc_bindings (k - 1) in
   1.444 +           if is_disc_binding_valid b then get_udisc b (k - 1) else nth exist_xs_u_eq_ctrs (k - 1)
   1.445 +         end);
   1.446 +
   1.447 +    val (all_sels_distinct, discs, selss, disc_defs, sel_defs, sel_defss, lthy') =
   1.448 +      if no_discs_sels then
   1.449 +        (true, [], [], [], [], [], lthy)
   1.450 +      else
   1.451 +        let
   1.452 +          fun disc_free b = Free (Binding.name_of b, mk_pred1T fcT);
   1.453 +
   1.454 +          fun disc_spec b exist_xs_u_eq_ctr = mk_Trueprop_eq (disc_free b $ u, exist_xs_u_eq_ctr);
   1.455 +
   1.456 +          fun alternate_disc k =
   1.457 +            Term.lambda u (alternate_disc_lhs (K o rapp u o disc_free) (3 - k));
   1.458 +
   1.459 +          fun mk_sel_case_args b proto_sels T =
   1.460 +            map2 (fn Ts => fn k =>
   1.461 +              (case AList.lookup (op =) proto_sels k of
   1.462 +                NONE =>
   1.463 +                (case AList.lookup Binding.eq_name (rev (nth sel_defaultss (k - 1))) b of
   1.464 +                  NONE => fold_rev (Term.lambda o curry Free Name.uu) Ts (mk_undefined T)
   1.465 +                | SOME t => t |> Type.constraint (Ts ---> T) |> Syntax.check_term lthy)
   1.466 +              | SOME (xs, x) => fold_rev Term.lambda xs x)) ctr_Tss ks;
   1.467 +
   1.468 +          fun sel_spec b proto_sels =
   1.469 +            let
   1.470 +              val _ =
   1.471 +                (case duplicates (op =) (map fst proto_sels) of
   1.472 +                   k :: _ => error ("Duplicate selector name " ^ quote (Binding.name_of b) ^
   1.473 +                     " for constructor " ^
   1.474 +                     quote (Syntax.string_of_term lthy (nth ctrs (k - 1))))
   1.475 +                 | [] => ())
   1.476 +              val T =
   1.477 +                (case distinct (op =) (map (fastype_of o snd o snd) proto_sels) of
   1.478 +                  [T] => T
   1.479 +                | T :: T' :: _ => error ("Inconsistent range type for selector " ^
   1.480 +                    quote (Binding.name_of b) ^ ": " ^ quote (Syntax.string_of_typ lthy T) ^ " vs. "
   1.481 +                    ^ quote (Syntax.string_of_typ lthy T')));
   1.482 +            in
   1.483 +              mk_Trueprop_eq (Free (Binding.name_of b, fcT --> T) $ u,
   1.484 +                Term.list_comb (mk_case As T case0, mk_sel_case_args b proto_sels T) $ u)
   1.485 +            end;
   1.486 +
   1.487 +          val sel_bindings = flat sel_bindingss;
   1.488 +          val uniq_sel_bindings = distinct Binding.eq_name sel_bindings;
   1.489 +          val all_sels_distinct = (length uniq_sel_bindings = length sel_bindings);
   1.490 +
   1.491 +          val sel_binding_index =
   1.492 +            if all_sels_distinct then 1 upto length sel_bindings
   1.493 +            else map (fn b => find_index (curry Binding.eq_name b) uniq_sel_bindings) sel_bindings;
   1.494 +
   1.495 +          val proto_sels = flat (map3 (fn k => fn xs => map (fn x => (k, (xs, x)))) ks xss xss);
   1.496 +          val sel_infos =
   1.497 +            AList.group (op =) (sel_binding_index ~~ proto_sels)
   1.498 +            |> sort (int_ord o pairself fst)
   1.499 +            |> map snd |> curry (op ~~) uniq_sel_bindings;
   1.500 +          val sel_bindings = map fst sel_infos;
   1.501 +
   1.502 +          fun unflat_selss xs = unflat_lookup Binding.eq_name sel_bindings xs sel_bindingss;
   1.503 +
   1.504 +          val (((raw_discs, raw_disc_defs), (raw_sels, raw_sel_defs)), (lthy', lthy)) =
   1.505 +            lthy
   1.506 +            |> apfst split_list o fold_map3 (fn k => fn exist_xs_u_eq_ctr => fn b =>
   1.507 +                if Binding.is_empty b then
   1.508 +                  if n = 1 then pair (Term.lambda u (mk_uu_eq ()), unique_disc_no_def)
   1.509 +                  else pair (alternate_disc k, alternate_disc_no_def)
   1.510 +                else if Binding.eq_name (b, equal_binding) then
   1.511 +                  pair (Term.lambda u exist_xs_u_eq_ctr, refl)
   1.512 +                else
   1.513 +                  Specification.definition (SOME (b, NONE, NoSyn),
   1.514 +                    ((Thm.def_binding b, []), disc_spec b exist_xs_u_eq_ctr)) #>> apsnd snd)
   1.515 +              ks exist_xs_u_eq_ctrs disc_bindings
   1.516 +            ||>> apfst split_list o fold_map (fn (b, proto_sels) =>
   1.517 +              Specification.definition (SOME (b, NONE, NoSyn),
   1.518 +                ((Thm.def_binding b, []), sel_spec b proto_sels)) #>> apsnd snd) sel_infos
   1.519 +            ||> `Local_Theory.restore;
   1.520 +
   1.521 +          val phi = Proof_Context.export_morphism lthy lthy';
   1.522 +
   1.523 +          val disc_defs = map (Morphism.thm phi) raw_disc_defs;
   1.524 +          val sel_defs = map (Morphism.thm phi) raw_sel_defs;
   1.525 +          val sel_defss = unflat_selss sel_defs;
   1.526 +
   1.527 +          val discs0 = map (Morphism.term phi) raw_discs;
   1.528 +          val selss0 = unflat_selss (map (Morphism.term phi) raw_sels);
   1.529 +
   1.530 +          val discs = map (mk_disc_or_sel As) discs0;
   1.531 +          val selss = map (map (mk_disc_or_sel As)) selss0;
   1.532 +        in
   1.533 +          (all_sels_distinct, discs, selss, disc_defs, sel_defs, sel_defss, lthy')
   1.534 +        end;
   1.535 +
   1.536 +    fun mk_imp_p Qs = Logic.list_implies (Qs, HOLogic.mk_Trueprop p);
   1.537 +
   1.538 +    val exhaust_goal =
   1.539 +      let fun mk_prem xctr xs = fold_rev Logic.all xs (mk_imp_p [mk_Trueprop_eq (u, xctr)]) in
   1.540 +        fold_rev Logic.all [p, u] (mk_imp_p (map2 mk_prem xctrs xss))
   1.541 +      end;
   1.542 +
   1.543 +    val inject_goalss =
   1.544 +      let
   1.545 +        fun mk_goal _ _ [] [] = []
   1.546 +          | mk_goal xctr yctr xs ys =
   1.547 +            [fold_rev Logic.all (xs @ ys) (mk_Trueprop_eq (HOLogic.mk_eq (xctr, yctr),
   1.548 +              Library.foldr1 HOLogic.mk_conj (map2 (curry HOLogic.mk_eq) xs ys)))];
   1.549 +      in
   1.550 +        map4 mk_goal xctrs yctrs xss yss
   1.551 +      end;
   1.552 +
   1.553 +    val half_distinct_goalss =
   1.554 +      let
   1.555 +        fun mk_goal ((xs, xc), (xs', xc')) =
   1.556 +          fold_rev Logic.all (xs @ xs')
   1.557 +            (HOLogic.mk_Trueprop (HOLogic.mk_not (HOLogic.mk_eq (xc, xc'))));
   1.558 +      in
   1.559 +        map (map mk_goal) (mk_half_pairss (`I (xss ~~ xctrs)))
   1.560 +      end;
   1.561 +
   1.562 +    val goalss = [exhaust_goal] :: inject_goalss @ half_distinct_goalss;
   1.563 +
   1.564 +    fun after_qed thmss lthy =
   1.565 +      let
   1.566 +        val ([exhaust_thm], (inject_thmss, half_distinct_thmss)) = (hd thmss, chop n (tl thmss));
   1.567 +
   1.568 +        val inject_thms = flat inject_thmss;
   1.569 +
   1.570 +        val rho_As = map (pairself (certifyT lthy)) (map Logic.varifyT_global As ~~ As);
   1.571 +
   1.572 +        fun inst_thm t thm =
   1.573 +          Drule.instantiate' [] [SOME (certify lthy t)]
   1.574 +            (Thm.instantiate (rho_As, []) (Drule.zero_var_indexes thm));
   1.575 +
   1.576 +        val uexhaust_thm = inst_thm u exhaust_thm;
   1.577 +
   1.578 +        val exhaust_cases = map base_name_of_ctr ctrs;
   1.579 +
   1.580 +        val other_half_distinct_thmss = map (map (fn thm => thm RS not_sym)) half_distinct_thmss;
   1.581 +
   1.582 +        val (distinct_thms, (distinct_thmsss', distinct_thmsss)) =
   1.583 +          join_halves n half_distinct_thmss other_half_distinct_thmss ||> `transpose;
   1.584 +
   1.585 +        val nchotomy_thm =
   1.586 +          let
   1.587 +            val goal =
   1.588 +              HOLogic.mk_Trueprop (HOLogic.mk_all (fst u', snd u',
   1.589 +                Library.foldr1 HOLogic.mk_disj exist_xs_u_eq_ctrs));
   1.590 +          in
   1.591 +            Goal.prove_sorry lthy [] [] goal (fn _ => mk_nchotomy_tac n exhaust_thm)
   1.592 +            |> Thm.close_derivation
   1.593 +          end;
   1.594 +
   1.595 +        val case_thms =
   1.596 +          let
   1.597 +            val goals =
   1.598 +              map3 (fn xctr => fn xf => fn xs =>
   1.599 +                fold_rev Logic.all (fs @ xs) (mk_Trueprop_eq (fcase $ xctr, xf))) xctrs xfs xss;
   1.600 +          in
   1.601 +            map4 (fn k => fn goal => fn injects => fn distinctss =>
   1.602 +                Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
   1.603 +                  mk_case_tac ctxt n k case_def injects distinctss)
   1.604 +                |> Thm.close_derivation)
   1.605 +              ks goals inject_thmss distinct_thmsss
   1.606 +          end;
   1.607 +
   1.608 +        val (case_cong_thm, weak_case_cong_thm) =
   1.609 +          let
   1.610 +            fun mk_prem xctr xs xf xg =
   1.611 +              fold_rev Logic.all xs (Logic.mk_implies (mk_Trueprop_eq (v, xctr),
   1.612 +                mk_Trueprop_eq (xf, xg)));
   1.613 +
   1.614 +            val goal =
   1.615 +              Logic.list_implies (uv_eq :: map4 mk_prem xctrs xss xfs xgs,
   1.616 +                 mk_Trueprop_eq (eta_ufcase, eta_vgcase));
   1.617 +            val weak_goal = Logic.mk_implies (uv_eq, mk_Trueprop_eq (ufcase, vfcase));
   1.618 +          in
   1.619 +            (Goal.prove_sorry lthy [] [] goal (fn _ => mk_case_cong_tac lthy uexhaust_thm case_thms),
   1.620 +             Goal.prove_sorry lthy [] [] weak_goal (K (etac arg_cong 1)))
   1.621 +            |> pairself (Thm.close_derivation #> singleton (Proof_Context.export names_lthy lthy))
   1.622 +          end;
   1.623 +
   1.624 +        val split_lhs = q $ ufcase;
   1.625 +
   1.626 +        fun mk_split_conjunct xctr xs f_xs =
   1.627 +          list_all_free xs (HOLogic.mk_imp (HOLogic.mk_eq (u, xctr), q $ f_xs));
   1.628 +        fun mk_split_disjunct xctr xs f_xs =
   1.629 +          list_exists_free xs (HOLogic.mk_conj (HOLogic.mk_eq (u, xctr),
   1.630 +            HOLogic.mk_not (q $ f_xs)));
   1.631 +
   1.632 +        fun mk_split_goal xctrs xss xfs =
   1.633 +          mk_Trueprop_eq (split_lhs, Library.foldr1 HOLogic.mk_conj
   1.634 +            (map3 mk_split_conjunct xctrs xss xfs));
   1.635 +        fun mk_split_asm_goal xctrs xss xfs =
   1.636 +          mk_Trueprop_eq (split_lhs, HOLogic.mk_not (Library.foldr1 HOLogic.mk_disj
   1.637 +            (map3 mk_split_disjunct xctrs xss xfs)));
   1.638 +
   1.639 +        fun prove_split selss goal =
   1.640 +          Goal.prove_sorry lthy [] [] goal (fn _ =>
   1.641 +            mk_split_tac lthy uexhaust_thm case_thms selss inject_thmss distinct_thmsss)
   1.642 +          |> Thm.close_derivation
   1.643 +          |> singleton (Proof_Context.export names_lthy lthy);
   1.644 +
   1.645 +        fun prove_split_asm asm_goal split_thm =
   1.646 +          Goal.prove_sorry lthy [] [] asm_goal (fn {context = ctxt, ...} =>
   1.647 +            mk_split_asm_tac ctxt split_thm)
   1.648 +          |> Thm.close_derivation
   1.649 +          |> singleton (Proof_Context.export names_lthy lthy);
   1.650 +
   1.651 +        val (split_thm, split_asm_thm) =
   1.652 +          let
   1.653 +            val goal = mk_split_goal xctrs xss xfs;
   1.654 +            val asm_goal = mk_split_asm_goal xctrs xss xfs;
   1.655 +
   1.656 +            val thm = prove_split (replicate n []) goal;
   1.657 +            val asm_thm = prove_split_asm asm_goal thm;
   1.658 +          in
   1.659 +            (thm, asm_thm)
   1.660 +          end;
   1.661 +
   1.662 +        val (all_sel_thms, sel_thmss, disc_thmss, nontriv_disc_thms, discI_thms, nontriv_discI_thms,
   1.663 +             disc_exclude_thms, disc_exhaust_thms, sel_exhaust_thms, all_collapse_thms,
   1.664 +             safe_collapse_thms, expand_thms, sel_split_thms, sel_split_asm_thms, case_eq_if_thms) =
   1.665 +          if no_discs_sels then
   1.666 +            ([], [], [], [], [], [], [], [], [], [], [], [], [], [], [])
   1.667 +          else
   1.668 +            let
   1.669 +              val udiscs = map (rapp u) discs;
   1.670 +              val uselss = map (map (rapp u)) selss;
   1.671 +              val usel_ctrs = map2 (curry Term.list_comb) ctrs uselss;
   1.672 +              val usel_fs = map2 (curry Term.list_comb) fs uselss;
   1.673 +
   1.674 +              val vdiscs = map (rapp v) discs;
   1.675 +              val vselss = map (map (rapp v)) selss;
   1.676 +
   1.677 +              fun make_sel_thm xs' case_thm sel_def =
   1.678 +                zero_var_indexes (Drule.gen_all (Drule.rename_bvars' (map (SOME o fst) xs')
   1.679 +                    (Drule.forall_intr_vars (case_thm RS (sel_def RS trans)))));
   1.680 +
   1.681 +              val sel_thmss = map3 (map oo make_sel_thm) xss' case_thms sel_defss;
   1.682 +
   1.683 +              fun has_undefined_rhs thm =
   1.684 +                (case snd (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of thm))) of
   1.685 +                  Const (@{const_name undefined}, _) => true
   1.686 +                | _ => false);
   1.687 +
   1.688 +              val all_sel_thms =
   1.689 +                (if all_sels_distinct andalso forall null sel_defaultss then
   1.690 +                   flat sel_thmss
   1.691 +                 else
   1.692 +                   map_product (fn s => fn (xs', c) => make_sel_thm xs' c s) sel_defs
   1.693 +                     (xss' ~~ case_thms))
   1.694 +                |> filter_out has_undefined_rhs;
   1.695 +
   1.696 +              fun mk_unique_disc_def () =
   1.697 +                let
   1.698 +                  val m = the_single ms;
   1.699 +                  val goal = mk_Trueprop_eq (mk_uu_eq (), the_single exist_xs_u_eq_ctrs);
   1.700 +                in
   1.701 +                  Goal.prove_sorry lthy [] [] goal (fn _ => mk_unique_disc_def_tac m uexhaust_thm)
   1.702 +                  |> Thm.close_derivation
   1.703 +                  |> singleton (Proof_Context.export names_lthy lthy)
   1.704 +                end;
   1.705 +
   1.706 +              fun mk_alternate_disc_def k =
   1.707 +                let
   1.708 +                  val goal =
   1.709 +                    mk_Trueprop_eq (alternate_disc_lhs (K (nth udiscs)) (3 - k),
   1.710 +                      nth exist_xs_u_eq_ctrs (k - 1));
   1.711 +                in
   1.712 +                  Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
   1.713 +                    mk_alternate_disc_def_tac ctxt k (nth disc_defs (2 - k))
   1.714 +                      (nth distinct_thms (2 - k)) uexhaust_thm)
   1.715 +                  |> Thm.close_derivation
   1.716 +                  |> singleton (Proof_Context.export names_lthy lthy)
   1.717 +                end;
   1.718 +
   1.719 +              val has_alternate_disc_def =
   1.720 +                exists (fn def => Thm.eq_thm_prop (def, alternate_disc_no_def)) disc_defs;
   1.721 +
   1.722 +              val disc_defs' =
   1.723 +                map2 (fn k => fn def =>
   1.724 +                  if Thm.eq_thm_prop (def, unique_disc_no_def) then mk_unique_disc_def ()
   1.725 +                  else if Thm.eq_thm_prop (def, alternate_disc_no_def) then mk_alternate_disc_def k
   1.726 +                  else def) ks disc_defs;
   1.727 +
   1.728 +              val discD_thms = map (fn def => def RS iffD1) disc_defs';
   1.729 +              val discI_thms =
   1.730 +                map2 (fn m => fn def => funpow m (fn thm => exI RS thm) (def RS iffD2)) ms
   1.731 +                  disc_defs';
   1.732 +              val not_discI_thms =
   1.733 +                map2 (fn m => fn def => funpow m (fn thm => allI RS thm)
   1.734 +                    (unfold_thms lthy @{thms not_ex} (def RS @{thm ssubst[of _ _ Not]})))
   1.735 +                  ms disc_defs';
   1.736 +
   1.737 +              val (disc_thmss', disc_thmss) =
   1.738 +                let
   1.739 +                  fun mk_thm discI _ [] = refl RS discI
   1.740 +                    | mk_thm _ not_discI [distinct] = distinct RS not_discI;
   1.741 +                  fun mk_thms discI not_discI distinctss = map (mk_thm discI not_discI) distinctss;
   1.742 +                in
   1.743 +                  map3 mk_thms discI_thms not_discI_thms distinct_thmsss' |> `transpose
   1.744 +                end;
   1.745 +
   1.746 +              val nontriv_disc_thms =
   1.747 +                flat (map2 (fn b => if is_disc_binding_valid b then I else K [])
   1.748 +                  disc_bindings disc_thmss);
   1.749 +
   1.750 +              fun is_discI_boring b =
   1.751 +                (n = 1 andalso Binding.is_empty b) orelse Binding.eq_name (b, equal_binding);
   1.752 +
   1.753 +              val nontriv_discI_thms =
   1.754 +                flat (map2 (fn b => if is_discI_boring b then K [] else single) disc_bindings
   1.755 +                  discI_thms);
   1.756 +
   1.757 +              val (disc_exclude_thms, (disc_exclude_thmsss', disc_exclude_thmsss)) =
   1.758 +                let
   1.759 +                  fun mk_goal [] = []
   1.760 +                    | mk_goal [((_, udisc), (_, udisc'))] =
   1.761 +                      [Logic.all u (Logic.mk_implies (HOLogic.mk_Trueprop udisc,
   1.762 +                         HOLogic.mk_Trueprop (HOLogic.mk_not udisc')))];
   1.763 +
   1.764 +                  fun prove tac goal =
   1.765 +                    Goal.prove_sorry lthy [] [] goal (K tac)
   1.766 +                    |> Thm.close_derivation;
   1.767 +
   1.768 +                  val half_pairss = mk_half_pairss (`I (ms ~~ discD_thms ~~ udiscs));
   1.769 +
   1.770 +                  val half_goalss = map mk_goal half_pairss;
   1.771 +                  val half_thmss =
   1.772 +                    map3 (fn [] => K (K []) | [goal] => fn [(((m, discD), _), _)] =>
   1.773 +                        fn disc_thm => [prove (mk_half_disc_exclude_tac lthy m discD disc_thm) goal])
   1.774 +                      half_goalss half_pairss (flat disc_thmss');
   1.775 +
   1.776 +                  val other_half_goalss = map (mk_goal o map swap) half_pairss;
   1.777 +                  val other_half_thmss =
   1.778 +                    map2 (map2 (prove o mk_other_half_disc_exclude_tac)) half_thmss
   1.779 +                      other_half_goalss;
   1.780 +                in
   1.781 +                  join_halves n half_thmss other_half_thmss ||> `transpose
   1.782 +                  |>> has_alternate_disc_def ? K []
   1.783 +                end;
   1.784 +
   1.785 +              val disc_exhaust_thm =
   1.786 +                let
   1.787 +                  fun mk_prem udisc = mk_imp_p [HOLogic.mk_Trueprop udisc];
   1.788 +                  val goal = fold_rev Logic.all [p, u] (mk_imp_p (map mk_prem udiscs));
   1.789 +                in
   1.790 +                  Goal.prove_sorry lthy [] [] goal (fn _ =>
   1.791 +                    mk_disc_exhaust_tac n exhaust_thm discI_thms)
   1.792 +                  |> Thm.close_derivation
   1.793 +                end;
   1.794 +
   1.795 +              val (safe_collapse_thms, all_collapse_thms) =
   1.796 +                let
   1.797 +                  fun mk_goal m udisc usel_ctr =
   1.798 +                    let
   1.799 +                      val prem = HOLogic.mk_Trueprop udisc;
   1.800 +                      val concl = mk_Trueprop_eq ((usel_ctr, u) |> m = 0 ? swap);
   1.801 +                    in
   1.802 +                      (prem aconv concl, Logic.all u (Logic.mk_implies (prem, concl)))
   1.803 +                    end;
   1.804 +                  val (trivs, goals) = map3 mk_goal ms udiscs usel_ctrs |> split_list;
   1.805 +                  val thms =
   1.806 +                    map5 (fn m => fn discD => fn sel_thms => fn triv => fn goal =>
   1.807 +                        Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
   1.808 +                          mk_collapse_tac ctxt m discD sel_thms ORELSE HEADGOAL atac)
   1.809 +                        |> Thm.close_derivation
   1.810 +                        |> not triv ? perhaps (try (fn thm => refl RS thm)))
   1.811 +                      ms discD_thms sel_thmss trivs goals;
   1.812 +                in
   1.813 +                  (map_filter (fn (true, _) => NONE | (false, thm) => SOME thm) (trivs ~~ thms),
   1.814 +                   thms)
   1.815 +                end;
   1.816 +
   1.817 +              val swapped_all_collapse_thms =
   1.818 +                map2 (fn m => fn thm => if m = 0 then thm else thm RS sym) ms all_collapse_thms;
   1.819 +
   1.820 +              val sel_exhaust_thm =
   1.821 +                let
   1.822 +                  fun mk_prem usel_ctr = mk_imp_p [mk_Trueprop_eq (u, usel_ctr)];
   1.823 +                  val goal = fold_rev Logic.all [p, u] (mk_imp_p (map mk_prem usel_ctrs));
   1.824 +                in
   1.825 +                  Goal.prove_sorry lthy [] [] goal (fn _ =>
   1.826 +                    mk_sel_exhaust_tac n disc_exhaust_thm swapped_all_collapse_thms)
   1.827 +                  |> Thm.close_derivation
   1.828 +                end;
   1.829 +
   1.830 +              val expand_thm =
   1.831 +                let
   1.832 +                  fun mk_prems k udisc usels vdisc vsels =
   1.833 +                    (if k = n then [] else [mk_Trueprop_eq (udisc, vdisc)]) @
   1.834 +                    (if null usels then
   1.835 +                       []
   1.836 +                     else
   1.837 +                       [Logic.list_implies
   1.838 +                          (if n = 1 then [] else map HOLogic.mk_Trueprop [udisc, vdisc],
   1.839 +                             HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
   1.840 +                               (map2 (curry HOLogic.mk_eq) usels vsels)))]);
   1.841 +
   1.842 +                  val goal =
   1.843 +                    Library.foldr Logic.list_implies
   1.844 +                      (map5 mk_prems ks udiscs uselss vdiscs vselss, uv_eq);
   1.845 +                  val uncollapse_thms =
   1.846 +                    map2 (fn thm => fn [] => thm | _ => thm RS sym) all_collapse_thms uselss;
   1.847 +                in
   1.848 +                  Goal.prove_sorry lthy [] [] goal (fn _ =>
   1.849 +                    mk_expand_tac lthy n ms (inst_thm u disc_exhaust_thm)
   1.850 +                      (inst_thm v disc_exhaust_thm) uncollapse_thms disc_exclude_thmsss
   1.851 +                      disc_exclude_thmsss')
   1.852 +                  |> Thm.close_derivation
   1.853 +                  |> singleton (Proof_Context.export names_lthy lthy)
   1.854 +                end;
   1.855 +
   1.856 +              val (sel_split_thm, sel_split_asm_thm) =
   1.857 +                let
   1.858 +                  val zss = map (K []) xss;
   1.859 +                  val goal = mk_split_goal usel_ctrs zss usel_fs;
   1.860 +                  val asm_goal = mk_split_asm_goal usel_ctrs zss usel_fs;
   1.861 +
   1.862 +                  val thm = prove_split sel_thmss goal;
   1.863 +                  val asm_thm = prove_split_asm asm_goal thm;
   1.864 +                in
   1.865 +                  (thm, asm_thm)
   1.866 +                end;
   1.867 +
   1.868 +              val case_eq_if_thm =
   1.869 +                let
   1.870 +                  val goal = mk_Trueprop_eq (ufcase, mk_IfN B udiscs usel_fs);
   1.871 +                in
   1.872 +                  Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
   1.873 +                    mk_case_eq_if_tac ctxt n uexhaust_thm case_thms disc_thmss' sel_thmss)
   1.874 +                  |> Thm.close_derivation
   1.875 +                  |> singleton (Proof_Context.export names_lthy lthy)
   1.876 +                end;
   1.877 +            in
   1.878 +              (all_sel_thms, sel_thmss, disc_thmss, nontriv_disc_thms, discI_thms,
   1.879 +               nontriv_discI_thms, disc_exclude_thms, [disc_exhaust_thm], [sel_exhaust_thm],
   1.880 +               all_collapse_thms, safe_collapse_thms, [expand_thm], [sel_split_thm],
   1.881 +               [sel_split_asm_thm], [case_eq_if_thm])
   1.882 +            end;
   1.883 +
   1.884 +        val exhaust_case_names_attr = Attrib.internal (K (Rule_Cases.case_names exhaust_cases));
   1.885 +        val cases_type_attr = Attrib.internal (K (Induct.cases_type fcT_name));
   1.886 +
   1.887 +        val anonymous_notes =
   1.888 +          [(map (fn th => th RS notE) distinct_thms, safe_elim_attrs),
   1.889 +           (map (fn th => th RS @{thm eq_False[THEN iffD2]}
   1.890 +              handle THM _ => th RS @{thm eq_True[THEN iffD2]}) nontriv_disc_thms,
   1.891 +            code_nitpicksimp_attrs)]
   1.892 +          |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
   1.893 +
   1.894 +        val notes =
   1.895 +          [(caseN, case_thms, code_nitpicksimp_simp_attrs),
   1.896 +           (case_congN, [case_cong_thm], []),
   1.897 +           (case_eq_ifN, case_eq_if_thms, []),
   1.898 +           (collapseN, safe_collapse_thms, simp_attrs),
   1.899 +           (discN, nontriv_disc_thms, simp_attrs),
   1.900 +           (discIN, nontriv_discI_thms, []),
   1.901 +           (disc_excludeN, disc_exclude_thms, dest_attrs),
   1.902 +           (disc_exhaustN, disc_exhaust_thms, [exhaust_case_names_attr]),
   1.903 +           (distinctN, distinct_thms, simp_attrs @ inductsimp_attrs),
   1.904 +           (exhaustN, [exhaust_thm], [exhaust_case_names_attr, cases_type_attr]),
   1.905 +           (expandN, expand_thms, []),
   1.906 +           (injectN, inject_thms, iff_attrs @ inductsimp_attrs),
   1.907 +           (nchotomyN, [nchotomy_thm], []),
   1.908 +           (selN, all_sel_thms, code_nitpicksimp_simp_attrs),
   1.909 +           (sel_exhaustN, sel_exhaust_thms, [exhaust_case_names_attr]),
   1.910 +           (sel_splitN, sel_split_thms, []),
   1.911 +           (sel_split_asmN, sel_split_asm_thms, []),
   1.912 +           (splitN, [split_thm], []),
   1.913 +           (split_asmN, [split_asm_thm], []),
   1.914 +           (splitsN, [split_thm, split_asm_thm], []),
   1.915 +           (weak_case_cong_thmsN, [weak_case_cong_thm], cong_attrs)]
   1.916 +          |> filter_out (null o #2)
   1.917 +          |> map (fn (thmN, thms, attrs) =>
   1.918 +            ((qualify true (Binding.name thmN), attrs), [(thms, [])]));
   1.919 +
   1.920 +        val ctr_sugar =
   1.921 +          {ctrs = ctrs, casex = casex, discs = discs, selss = selss, exhaust = exhaust_thm,
   1.922 +           nchotomy = nchotomy_thm, injects = inject_thms, distincts = distinct_thms,
   1.923 +           case_thms = case_thms, case_cong = case_cong_thm, weak_case_cong = weak_case_cong_thm,
   1.924 +           split = split_thm, split_asm = split_asm_thm, disc_thmss = disc_thmss,
   1.925 +           discIs = discI_thms, sel_thmss = sel_thmss, disc_exhausts = disc_exhaust_thms,
   1.926 +           sel_exhausts = sel_exhaust_thms, collapses = all_collapse_thms, expands = expand_thms,
   1.927 +           sel_splits = sel_split_thms, sel_split_asms = sel_split_asm_thms,
   1.928 +           case_eq_ifs = case_eq_if_thms};
   1.929 +      in
   1.930 +        (ctr_sugar,
   1.931 +         lthy
   1.932 +         |> not rep_compat ?
   1.933 +            Local_Theory.declaration {syntax = false, pervasive = true}
   1.934 +              (fn phi => Case_Translation.register
   1.935 +                 (Morphism.term phi casex) (map (Morphism.term phi) ctrs))
   1.936 +         |> Local_Theory.background_theory (fold (fold Code.del_eqn) [disc_defs, sel_defs])
   1.937 +         |> not no_code ?
   1.938 +            Local_Theory.declaration {syntax = false, pervasive = false}
   1.939 +              (fn phi => Context.mapping
   1.940 +                (add_ctr_code fcT_name (map (Morphism.typ phi) As)
   1.941 +                  (map (dest_Const o Morphism.term phi) ctrs) (Morphism.fact phi inject_thms)
   1.942 +                  (Morphism.fact phi distinct_thms) (Morphism.fact phi case_thms))
   1.943 +                I)
   1.944 +         |> Local_Theory.notes (anonymous_notes @ notes) |> snd
   1.945 +         |> register_ctr_sugar fcT_name ctr_sugar)
   1.946 +      end;
   1.947 +  in
   1.948 +    (goalss, after_qed, lthy')
   1.949 +  end;
   1.950 +
   1.951 +fun wrap_free_constructors tacss = (fn (goalss, after_qed, lthy) =>
   1.952 +  map2 (map2 (Thm.close_derivation oo Goal.prove_sorry lthy [] [])) goalss tacss
   1.953 +  |> (fn thms => after_qed thms lthy)) oo prepare_wrap_free_constructors (K I);
   1.954 +
   1.955 +val wrap_free_constructors_cmd = (fn (goalss, after_qed, lthy) =>
   1.956 +  Proof.theorem NONE (snd oo after_qed) (map (map (rpair [])) goalss) lthy) oo
   1.957 +  prepare_wrap_free_constructors Syntax.read_term;
   1.958 +
   1.959 +fun parse_bracket_list parser = @{keyword "["} |-- Parse.list parser --|  @{keyword "]"};
   1.960 +
   1.961 +val parse_bindings = parse_bracket_list parse_binding;
   1.962 +val parse_bindingss = parse_bracket_list parse_bindings;
   1.963 +
   1.964 +val parse_bound_term = (parse_binding --| @{keyword ":"}) -- Parse.term;
   1.965 +val parse_bound_terms = parse_bracket_list parse_bound_term;
   1.966 +val parse_bound_termss = parse_bracket_list parse_bound_terms;
   1.967 +
   1.968 +val parse_wrap_free_constructors_options =
   1.969 +  Scan.optional (@{keyword "("} |-- Parse.list1
   1.970 +        (Parse.reserved "no_discs_sels" >> K 0 || Parse.reserved "no_code" >> K 1 ||
   1.971 +         Parse.reserved "rep_compat" >> K 2) --| @{keyword ")"}
   1.972 +      >> (fn js => (member (op =) js 0, (member (op =) js 1, member (op =) js 2))))
   1.973 +    (false, (false, false));
   1.974 +
   1.975 +val _ =
   1.976 +  Outer_Syntax.local_theory_to_proof @{command_spec "wrap_free_constructors"}
   1.977 +    "wrap an existing freely generated type's constructors"
   1.978 +    ((parse_wrap_free_constructors_options -- (@{keyword "["} |-- Parse.list Parse.term --|
   1.979 +        @{keyword "]"}) --
   1.980 +      parse_binding -- Scan.optional (parse_bindings -- Scan.optional (parse_bindingss --
   1.981 +        Scan.optional parse_bound_termss []) ([], [])) ([], ([], [])))
   1.982 +     >> wrap_free_constructors_cmd);
   1.983 +
   1.984 +end;