src/HOL/Nominal/nominal_datatype.ML
changeset 31936 9466169dc8e0
parent 31784 bd3486c57ba3
child 32010 cb1a1c94b4cd
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Fri Jul 03 16:51:08 2009 +0200
     1.3 @@ -0,0 +1,2094 @@
     1.4 +(*  Title:      HOL/Nominal/nominal_datatype.ML
     1.5 +    Author:     Stefan Berghofer and Christian Urban, TU Muenchen
     1.6 +
     1.7 +Nominal datatype package for Isabelle/HOL.
     1.8 +*)
     1.9 +
    1.10 +signature NOMINAL_DATATYPE =
    1.11 +sig
    1.12 +  val add_nominal_datatype : Datatype.config -> string list ->
    1.13 +    (string list * bstring * mixfix *
    1.14 +      (bstring * string list * mixfix) list) list -> theory -> theory
    1.15 +  type descr
    1.16 +  type nominal_datatype_info
    1.17 +  val get_nominal_datatypes : theory -> nominal_datatype_info Symtab.table
    1.18 +  val get_nominal_datatype : theory -> string -> nominal_datatype_info option
    1.19 +  val mk_perm: typ list -> term -> term -> term
    1.20 +  val perm_of_pair: term * term -> term
    1.21 +  val mk_not_sym: thm list -> thm list
    1.22 +  val perm_simproc: simproc
    1.23 +  val fresh_const: typ -> typ -> term
    1.24 +  val fresh_star_const: typ -> typ -> term
    1.25 +end
    1.26 +
    1.27 +structure NominalDatatype : NOMINAL_DATATYPE =
    1.28 +struct
    1.29 +
    1.30 +val finite_emptyI = thm "finite.emptyI";
    1.31 +val finite_Diff = thm "finite_Diff";
    1.32 +val finite_Un = thm "finite_Un";
    1.33 +val Un_iff = thm "Un_iff";
    1.34 +val In0_eq = thm "In0_eq";
    1.35 +val In1_eq = thm "In1_eq";
    1.36 +val In0_not_In1 = thm "In0_not_In1";
    1.37 +val In1_not_In0 = thm "In1_not_In0";
    1.38 +val Un_assoc = thm "Un_assoc";
    1.39 +val Collect_disj_eq = thm "Collect_disj_eq";
    1.40 +val empty_def = thm "empty_def";
    1.41 +val empty_iff = thm "empty_iff";
    1.42 +
    1.43 +open DatatypeAux;
    1.44 +open NominalAtoms;
    1.45 +
    1.46 +(** FIXME: Datatype should export this function **)
    1.47 +
    1.48 +local
    1.49 +
    1.50 +fun dt_recs (DtTFree _) = []
    1.51 +  | dt_recs (DtType (_, dts)) = List.concat (map dt_recs dts)
    1.52 +  | dt_recs (DtRec i) = [i];
    1.53 +
    1.54 +fun dt_cases (descr: descr) (_, args, constrs) =
    1.55 +  let
    1.56 +    fun the_bname i = Long_Name.base_name (#1 (valOf (AList.lookup (op =) descr i)));
    1.57 +    val bnames = map the_bname (distinct op = (List.concat (map dt_recs args)));
    1.58 +  in map (fn (c, _) => space_implode "_" (Long_Name.base_name c :: bnames)) constrs end;
    1.59 +
    1.60 +
    1.61 +fun induct_cases descr =
    1.62 +  DatatypeProp.indexify_names (List.concat (map (dt_cases descr) (map #2 descr)));
    1.63 +
    1.64 +fun exhaust_cases descr i = dt_cases descr (valOf (AList.lookup (op =) descr i));
    1.65 +
    1.66 +in
    1.67 +
    1.68 +fun mk_case_names_induct descr = RuleCases.case_names (induct_cases descr);
    1.69 +
    1.70 +fun mk_case_names_exhausts descr new =
    1.71 +  map (RuleCases.case_names o exhaust_cases descr o #1)
    1.72 +    (List.filter (fn ((_, (name, _, _))) => name mem_string new) descr);
    1.73 +
    1.74 +end;
    1.75 +
    1.76 +(* theory data *)
    1.77 +
    1.78 +type descr = (int * (string * dtyp list * (string * (dtyp list * dtyp) list) list)) list;
    1.79 +
    1.80 +type nominal_datatype_info =
    1.81 +  {index : int,
    1.82 +   descr : descr,
    1.83 +   sorts : (string * sort) list,
    1.84 +   rec_names : string list,
    1.85 +   rec_rewrites : thm list,
    1.86 +   induction : thm,
    1.87 +   distinct : thm list,
    1.88 +   inject : thm list};
    1.89 +
    1.90 +structure NominalDatatypesData = TheoryDataFun
    1.91 +(
    1.92 +  type T = nominal_datatype_info Symtab.table;
    1.93 +  val empty = Symtab.empty;
    1.94 +  val copy = I;
    1.95 +  val extend = I;
    1.96 +  fun merge _ tabs : T = Symtab.merge (K true) tabs;
    1.97 +);
    1.98 +
    1.99 +val get_nominal_datatypes = NominalDatatypesData.get;
   1.100 +val put_nominal_datatypes = NominalDatatypesData.put;
   1.101 +val map_nominal_datatypes = NominalDatatypesData.map;
   1.102 +val get_nominal_datatype = Symtab.lookup o get_nominal_datatypes;
   1.103 +
   1.104 +
   1.105 +(**** make datatype info ****)
   1.106 +
   1.107 +fun make_dt_info descr sorts induct reccomb_names rec_thms
   1.108 +    (((i, (_, (tname, _, _))), distinct), inject) =
   1.109 +  (tname,
   1.110 +   {index = i,
   1.111 +    descr = descr,
   1.112 +    sorts = sorts,
   1.113 +    rec_names = reccomb_names,
   1.114 +    rec_rewrites = rec_thms,
   1.115 +    induction = induct,
   1.116 +    distinct = distinct,
   1.117 +    inject = inject});
   1.118 +
   1.119 +(*******************************)
   1.120 +
   1.121 +val (_ $ (_ $ (_ $ (distinct_f $ _) $ _))) = hd (prems_of distinct_lemma);
   1.122 +
   1.123 +
   1.124 +(** simplification procedure for sorting permutations **)
   1.125 +
   1.126 +val dj_cp = thm "dj_cp";
   1.127 +
   1.128 +fun dest_permT (Type ("fun", [Type ("List.list", [Type ("*", [T, _])]),
   1.129 +      Type ("fun", [_, U])])) = (T, U);
   1.130 +
   1.131 +fun permTs_of (Const ("Nominal.perm", T) $ t $ u) = fst (dest_permT T) :: permTs_of u
   1.132 +  | permTs_of _ = [];
   1.133 +
   1.134 +fun perm_simproc' thy ss (Const ("Nominal.perm", T) $ t $ (u as Const ("Nominal.perm", U) $ r $ s)) =
   1.135 +      let
   1.136 +        val (aT as Type (a, []), S) = dest_permT T;
   1.137 +        val (bT as Type (b, []), _) = dest_permT U
   1.138 +      in if aT mem permTs_of u andalso aT <> bT then
   1.139 +          let
   1.140 +            val cp = cp_inst_of thy a b;
   1.141 +            val dj = dj_thm_of thy b a;
   1.142 +            val dj_cp' = [cp, dj] MRS dj_cp;
   1.143 +            val cert = SOME o cterm_of thy
   1.144 +          in
   1.145 +            SOME (mk_meta_eq (Drule.instantiate' [SOME (ctyp_of thy S)]
   1.146 +              [cert t, cert r, cert s] dj_cp'))
   1.147 +          end
   1.148 +        else NONE
   1.149 +      end
   1.150 +  | perm_simproc' thy ss _ = NONE;
   1.151 +
   1.152 +val perm_simproc =
   1.153 +  Simplifier.simproc (the_context ()) "perm_simp" ["pi1 \<bullet> (pi2 \<bullet> x)"] perm_simproc';
   1.154 +
   1.155 +val meta_spec = thm "meta_spec";
   1.156 +
   1.157 +fun projections rule =
   1.158 +  ProjectRule.projections (ProofContext.init (Thm.theory_of_thm rule)) rule
   1.159 +  |> map (standard #> RuleCases.save rule);
   1.160 +
   1.161 +val supp_prod = thm "supp_prod";
   1.162 +val fresh_prod = thm "fresh_prod";
   1.163 +val supports_fresh = thm "supports_fresh";
   1.164 +val supports_def = thm "Nominal.supports_def";
   1.165 +val fresh_def = thm "fresh_def";
   1.166 +val supp_def = thm "supp_def";
   1.167 +val rev_simps = thms "rev.simps";
   1.168 +val app_simps = thms "append.simps";
   1.169 +val at_fin_set_supp = thm "at_fin_set_supp";
   1.170 +val at_fin_set_fresh = thm "at_fin_set_fresh";
   1.171 +val abs_fun_eq1 = thm "abs_fun_eq1";
   1.172 +
   1.173 +val collect_simp = rewrite_rule [mk_meta_eq mem_Collect_eq];
   1.174 +
   1.175 +fun mk_perm Ts t u =
   1.176 +  let
   1.177 +    val T = fastype_of1 (Ts, t);
   1.178 +    val U = fastype_of1 (Ts, u)
   1.179 +  in Const ("Nominal.perm", T --> U --> U) $ t $ u end;
   1.180 +
   1.181 +fun perm_of_pair (x, y) =
   1.182 +  let
   1.183 +    val T = fastype_of x;
   1.184 +    val pT = mk_permT T
   1.185 +  in Const ("List.list.Cons", HOLogic.mk_prodT (T, T) --> pT --> pT) $
   1.186 +    HOLogic.mk_prod (x, y) $ Const ("List.list.Nil", pT)
   1.187 +  end;
   1.188 +
   1.189 +fun mk_not_sym ths = maps (fn th => case prop_of th of
   1.190 +    _ $ (Const ("Not", _) $ (Const ("op =", _) $ _ $ _)) => [th, th RS not_sym]
   1.191 +  | _ => [th]) ths;
   1.192 +
   1.193 +fun fresh_const T U = Const ("Nominal.fresh", T --> U --> HOLogic.boolT);
   1.194 +fun fresh_star_const T U =
   1.195 +  Const ("Nominal.fresh_star", HOLogic.mk_setT T --> U --> HOLogic.boolT);
   1.196 +
   1.197 +fun gen_add_nominal_datatype prep_typ config new_type_names dts thy =
   1.198 +  let
   1.199 +    (* this theory is used just for parsing *)
   1.200 +
   1.201 +    val tmp_thy = thy |>
   1.202 +      Theory.copy |>
   1.203 +      Sign.add_types (map (fn (tvs, tname, mx, _) =>
   1.204 +        (Binding.name tname, length tvs, mx)) dts);
   1.205 +
   1.206 +    val atoms = atoms_of thy;
   1.207 +
   1.208 +    fun prep_constr ((constrs, sorts), (cname, cargs, mx)) =
   1.209 +      let val (cargs', sorts') = Library.foldl (prep_typ tmp_thy) (([], sorts), cargs)
   1.210 +      in (constrs @ [(cname, cargs', mx)], sorts') end
   1.211 +
   1.212 +    fun prep_dt_spec ((dts, sorts), (tvs, tname, mx, constrs)) =
   1.213 +      let val (constrs', sorts') = Library.foldl prep_constr (([], sorts), constrs)
   1.214 +      in (dts @ [(tvs, tname, mx, constrs')], sorts') end
   1.215 +
   1.216 +    val (dts', sorts) = Library.foldl prep_dt_spec (([], []), dts);
   1.217 +    val tyvars = map (map (fn s =>
   1.218 +      (s, the (AList.lookup (op =) sorts s))) o #1) dts';
   1.219 +
   1.220 +    fun inter_sort thy S S' = Type.inter_sort (Sign.tsig_of thy) (S, S');
   1.221 +    fun augment_sort_typ thy S =
   1.222 +      let val S = Sign.certify_sort thy S
   1.223 +      in map_type_tfree (fn (s, S') => TFree (s,
   1.224 +        if member (op = o apsnd fst) sorts s then inter_sort thy S S' else S'))
   1.225 +      end;
   1.226 +    fun augment_sort thy S = map_types (augment_sort_typ thy S);
   1.227 +
   1.228 +    val types_syntax = map (fn (tvs, tname, mx, constrs) => (tname, mx)) dts';
   1.229 +    val constr_syntax = map (fn (tvs, tname, mx, constrs) =>
   1.230 +      map (fn (cname, cargs, mx) => (cname, mx)) constrs) dts';
   1.231 +
   1.232 +    val ps = map (fn (_, n, _, _) =>
   1.233 +      (Sign.full_bname tmp_thy n, Sign.full_bname tmp_thy (n ^ "_Rep"))) dts;
   1.234 +    val rps = map Library.swap ps;
   1.235 +
   1.236 +    fun replace_types (Type ("Nominal.ABS", [T, U])) =
   1.237 +          Type ("fun", [T, Type ("Nominal.noption", [replace_types U])])
   1.238 +      | replace_types (Type (s, Ts)) =
   1.239 +          Type (getOpt (AList.lookup op = ps s, s), map replace_types Ts)
   1.240 +      | replace_types T = T;
   1.241 +
   1.242 +    val dts'' = map (fn (tvs, tname, mx, constrs) => (tvs, Binding.name (tname ^ "_Rep"), NoSyn,
   1.243 +      map (fn (cname, cargs, mx) => (Binding.name (cname ^ "_Rep"),
   1.244 +        map replace_types cargs, NoSyn)) constrs)) dts';
   1.245 +
   1.246 +    val new_type_names' = map (fn n => n ^ "_Rep") new_type_names;
   1.247 +
   1.248 +    val (full_new_type_names',thy1) =
   1.249 +      Datatype.add_datatype config new_type_names' dts'' thy;
   1.250 +
   1.251 +    val {descr, induction, ...} =
   1.252 +      Datatype.the_info thy1 (hd full_new_type_names');
   1.253 +    fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
   1.254 +
   1.255 +    val big_name = space_implode "_" new_type_names;
   1.256 +
   1.257 +
   1.258 +    (**** define permutation functions ****)
   1.259 +
   1.260 +    val permT = mk_permT (TFree ("'x", HOLogic.typeS));
   1.261 +    val pi = Free ("pi", permT);
   1.262 +    val perm_types = map (fn (i, _) =>
   1.263 +      let val T = nth_dtyp i
   1.264 +      in permT --> T --> T end) descr;
   1.265 +    val perm_names' = DatatypeProp.indexify_names (map (fn (i, _) =>
   1.266 +      "perm_" ^ name_of_typ (nth_dtyp i)) descr);
   1.267 +    val perm_names = replicate (length new_type_names) "Nominal.perm" @
   1.268 +      map (Sign.full_bname thy1) (List.drop (perm_names', length new_type_names));
   1.269 +    val perm_names_types = perm_names ~~ perm_types;
   1.270 +    val perm_names_types' = perm_names' ~~ perm_types;
   1.271 +
   1.272 +    val perm_eqs = maps (fn (i, (_, _, constrs)) =>
   1.273 +      let val T = nth_dtyp i
   1.274 +      in map (fn (cname, dts) =>
   1.275 +        let
   1.276 +          val Ts = map (typ_of_dtyp descr sorts) dts;
   1.277 +          val names = Name.variant_list ["pi"] (DatatypeProp.make_tnames Ts);
   1.278 +          val args = map Free (names ~~ Ts);
   1.279 +          val c = Const (cname, Ts ---> T);
   1.280 +          fun perm_arg (dt, x) =
   1.281 +            let val T = type_of x
   1.282 +            in if is_rec_type dt then
   1.283 +                let val (Us, _) = strip_type T
   1.284 +                in list_abs (map (pair "x") Us,
   1.285 +                  Free (nth perm_names_types' (body_index dt)) $ pi $
   1.286 +                    list_comb (x, map (fn (i, U) =>
   1.287 +                      Const ("Nominal.perm", permT --> U --> U) $
   1.288 +                        (Const ("List.rev", permT --> permT) $ pi) $
   1.289 +                        Bound i) ((length Us - 1 downto 0) ~~ Us)))
   1.290 +                end
   1.291 +              else Const ("Nominal.perm", permT --> T --> T) $ pi $ x
   1.292 +            end;
   1.293 +        in
   1.294 +          (Attrib.empty_binding, HOLogic.mk_Trueprop (HOLogic.mk_eq
   1.295 +            (Free (nth perm_names_types' i) $
   1.296 +               Free ("pi", mk_permT (TFree ("'x", HOLogic.typeS))) $
   1.297 +               list_comb (c, args),
   1.298 +             list_comb (c, map perm_arg (dts ~~ args)))))
   1.299 +        end) constrs
   1.300 +      end) descr;
   1.301 +
   1.302 +    val (perm_simps, thy2) =
   1.303 +      Primrec.add_primrec_overloaded
   1.304 +        (map (fn (s, sT) => (s, sT, false))
   1.305 +           (List.take (perm_names' ~~ perm_names_types, length new_type_names)))
   1.306 +        (map (fn s => (Binding.name s, NONE, NoSyn)) perm_names') perm_eqs thy1;
   1.307 +
   1.308 +    (**** prove that permutation functions introduced by unfolding are ****)
   1.309 +    (**** equivalent to already existing permutation functions         ****)
   1.310 +
   1.311 +    val _ = warning ("length descr: " ^ string_of_int (length descr));
   1.312 +    val _ = warning ("length new_type_names: " ^ string_of_int (length new_type_names));
   1.313 +
   1.314 +    val perm_indnames = DatatypeProp.make_tnames (map body_type perm_types);
   1.315 +    val perm_fun_def = PureThy.get_thm thy2 "perm_fun_def";
   1.316 +
   1.317 +    val unfolded_perm_eq_thms =
   1.318 +      if length descr = length new_type_names then []
   1.319 +      else map standard (List.drop (split_conj_thm
   1.320 +        (Goal.prove_global thy2 [] []
   1.321 +          (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
   1.322 +            (map (fn (c as (s, T), x) =>
   1.323 +               let val [T1, T2] = binder_types T
   1.324 +               in HOLogic.mk_eq (Const c $ pi $ Free (x, T2),
   1.325 +                 Const ("Nominal.perm", T) $ pi $ Free (x, T2))
   1.326 +               end)
   1.327 +             (perm_names_types ~~ perm_indnames))))
   1.328 +          (fn _ => EVERY [indtac induction perm_indnames 1,
   1.329 +            ALLGOALS (asm_full_simp_tac
   1.330 +              (simpset_of thy2 addsimps [perm_fun_def]))])),
   1.331 +        length new_type_names));
   1.332 +
   1.333 +    (**** prove [] \<bullet> t = t ****)
   1.334 +
   1.335 +    val _ = warning "perm_empty_thms";
   1.336 +
   1.337 +    val perm_empty_thms = List.concat (map (fn a =>
   1.338 +      let val permT = mk_permT (Type (a, []))
   1.339 +      in map standard (List.take (split_conj_thm
   1.340 +        (Goal.prove_global thy2 [] []
   1.341 +          (augment_sort thy2 [pt_class_of thy2 a]
   1.342 +            (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
   1.343 +              (map (fn ((s, T), x) => HOLogic.mk_eq
   1.344 +                  (Const (s, permT --> T --> T) $
   1.345 +                     Const ("List.list.Nil", permT) $ Free (x, T),
   1.346 +                   Free (x, T)))
   1.347 +               (perm_names ~~
   1.348 +                map body_type perm_types ~~ perm_indnames)))))
   1.349 +          (fn _ => EVERY [indtac induction perm_indnames 1,
   1.350 +            ALLGOALS (asm_full_simp_tac (simpset_of thy2))])),
   1.351 +        length new_type_names))
   1.352 +      end)
   1.353 +      atoms);
   1.354 +
   1.355 +    (**** prove (pi1 @ pi2) \<bullet> t = pi1 \<bullet> (pi2 \<bullet> t) ****)
   1.356 +
   1.357 +    val _ = warning "perm_append_thms";
   1.358 +
   1.359 +    (*FIXME: these should be looked up statically*)
   1.360 +    val at_pt_inst = PureThy.get_thm thy2 "at_pt_inst";
   1.361 +    val pt2 = PureThy.get_thm thy2 "pt2";
   1.362 +
   1.363 +    val perm_append_thms = List.concat (map (fn a =>
   1.364 +      let
   1.365 +        val permT = mk_permT (Type (a, []));
   1.366 +        val pi1 = Free ("pi1", permT);
   1.367 +        val pi2 = Free ("pi2", permT);
   1.368 +        val pt_inst = pt_inst_of thy2 a;
   1.369 +        val pt2' = pt_inst RS pt2;
   1.370 +        val pt2_ax = PureThy.get_thm thy2 (Long_Name.map_base_name (fn s => "pt_" ^ s ^ "2") a);
   1.371 +      in List.take (map standard (split_conj_thm
   1.372 +        (Goal.prove_global thy2 [] []
   1.373 +           (augment_sort thy2 [pt_class_of thy2 a]
   1.374 +             (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
   1.375 +                (map (fn ((s, T), x) =>
   1.376 +                    let val perm = Const (s, permT --> T --> T)
   1.377 +                    in HOLogic.mk_eq
   1.378 +                      (perm $ (Const ("List.append", permT --> permT --> permT) $
   1.379 +                         pi1 $ pi2) $ Free (x, T),
   1.380 +                       perm $ pi1 $ (perm $ pi2 $ Free (x, T)))
   1.381 +                    end)
   1.382 +                  (perm_names ~~
   1.383 +                   map body_type perm_types ~~ perm_indnames)))))
   1.384 +           (fn _ => EVERY [indtac induction perm_indnames 1,
   1.385 +              ALLGOALS (asm_full_simp_tac (simpset_of thy2 addsimps [pt2', pt2_ax]))]))),
   1.386 +         length new_type_names)
   1.387 +      end) atoms);
   1.388 +
   1.389 +    (**** prove pi1 ~ pi2 ==> pi1 \<bullet> t = pi2 \<bullet> t ****)
   1.390 +
   1.391 +    val _ = warning "perm_eq_thms";
   1.392 +
   1.393 +    val pt3 = PureThy.get_thm thy2 "pt3";
   1.394 +    val pt3_rev = PureThy.get_thm thy2 "pt3_rev";
   1.395 +
   1.396 +    val perm_eq_thms = List.concat (map (fn a =>
   1.397 +      let
   1.398 +        val permT = mk_permT (Type (a, []));
   1.399 +        val pi1 = Free ("pi1", permT);
   1.400 +        val pi2 = Free ("pi2", permT);
   1.401 +        val at_inst = at_inst_of thy2 a;
   1.402 +        val pt_inst = pt_inst_of thy2 a;
   1.403 +        val pt3' = pt_inst RS pt3;
   1.404 +        val pt3_rev' = at_inst RS (pt_inst RS pt3_rev);
   1.405 +        val pt3_ax = PureThy.get_thm thy2 (Long_Name.map_base_name (fn s => "pt_" ^ s ^ "3") a);
   1.406 +      in List.take (map standard (split_conj_thm
   1.407 +        (Goal.prove_global thy2 [] []
   1.408 +          (augment_sort thy2 [pt_class_of thy2 a] (Logic.mk_implies
   1.409 +             (HOLogic.mk_Trueprop (Const ("Nominal.prm_eq",
   1.410 +                permT --> permT --> HOLogic.boolT) $ pi1 $ pi2),
   1.411 +              HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
   1.412 +                (map (fn ((s, T), x) =>
   1.413 +                    let val perm = Const (s, permT --> T --> T)
   1.414 +                    in HOLogic.mk_eq
   1.415 +                      (perm $ pi1 $ Free (x, T),
   1.416 +                       perm $ pi2 $ Free (x, T))
   1.417 +                    end)
   1.418 +                  (perm_names ~~
   1.419 +                   map body_type perm_types ~~ perm_indnames))))))
   1.420 +           (fn _ => EVERY [indtac induction perm_indnames 1,
   1.421 +              ALLGOALS (asm_full_simp_tac (simpset_of thy2 addsimps [pt3', pt3_rev', pt3_ax]))]))),
   1.422 +         length new_type_names)
   1.423 +      end) atoms);
   1.424 +
   1.425 +    (**** prove pi1 \<bullet> (pi2 \<bullet> t) = (pi1 \<bullet> pi2) \<bullet> (pi1 \<bullet> t) ****)
   1.426 +
   1.427 +    val cp1 = PureThy.get_thm thy2 "cp1";
   1.428 +    val dj_cp = PureThy.get_thm thy2 "dj_cp";
   1.429 +    val pt_perm_compose = PureThy.get_thm thy2 "pt_perm_compose";
   1.430 +    val pt_perm_compose_rev = PureThy.get_thm thy2 "pt_perm_compose_rev";
   1.431 +    val dj_perm_perm_forget = PureThy.get_thm thy2 "dj_perm_perm_forget";
   1.432 +
   1.433 +    fun composition_instance name1 name2 thy =
   1.434 +      let
   1.435 +        val cp_class = cp_class_of thy name1 name2;
   1.436 +        val pt_class =
   1.437 +          if name1 = name2 then [pt_class_of thy name1]
   1.438 +          else [];
   1.439 +        val permT1 = mk_permT (Type (name1, []));
   1.440 +        val permT2 = mk_permT (Type (name2, []));
   1.441 +        val Ts = map body_type perm_types;
   1.442 +        val cp_inst = cp_inst_of thy name1 name2;
   1.443 +        val simps = simpset_of thy addsimps (perm_fun_def ::
   1.444 +          (if name1 <> name2 then
   1.445 +             let val dj = dj_thm_of thy name2 name1
   1.446 +             in [dj RS (cp_inst RS dj_cp), dj RS dj_perm_perm_forget] end
   1.447 +           else
   1.448 +             let
   1.449 +               val at_inst = at_inst_of thy name1;
   1.450 +               val pt_inst = pt_inst_of thy name1;
   1.451 +             in
   1.452 +               [cp_inst RS cp1 RS sym,
   1.453 +                at_inst RS (pt_inst RS pt_perm_compose) RS sym,
   1.454 +                at_inst RS (pt_inst RS pt_perm_compose_rev) RS sym]
   1.455 +            end))
   1.456 +        val sort = Sign.certify_sort thy (cp_class :: pt_class);
   1.457 +        val thms = split_conj_thm (Goal.prove_global thy [] []
   1.458 +          (augment_sort thy sort
   1.459 +            (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
   1.460 +              (map (fn ((s, T), x) =>
   1.461 +                  let
   1.462 +                    val pi1 = Free ("pi1", permT1);
   1.463 +                    val pi2 = Free ("pi2", permT2);
   1.464 +                    val perm1 = Const (s, permT1 --> T --> T);
   1.465 +                    val perm2 = Const (s, permT2 --> T --> T);
   1.466 +                    val perm3 = Const ("Nominal.perm", permT1 --> permT2 --> permT2)
   1.467 +                  in HOLogic.mk_eq
   1.468 +                    (perm1 $ pi1 $ (perm2 $ pi2 $ Free (x, T)),
   1.469 +                     perm2 $ (perm3 $ pi1 $ pi2) $ (perm1 $ pi1 $ Free (x, T)))
   1.470 +                  end)
   1.471 +                (perm_names ~~ Ts ~~ perm_indnames)))))
   1.472 +          (fn _ => EVERY [indtac induction perm_indnames 1,
   1.473 +             ALLGOALS (asm_full_simp_tac simps)]))
   1.474 +      in
   1.475 +        fold (fn (s, tvs) => fn thy => AxClass.prove_arity
   1.476 +            (s, map (inter_sort thy sort o snd) tvs, [cp_class])
   1.477 +            (Class.intro_classes_tac [] THEN ALLGOALS (resolve_tac thms)) thy)
   1.478 +          (full_new_type_names' ~~ tyvars) thy
   1.479 +      end;
   1.480 +
   1.481 +    val (perm_thmss,thy3) = thy2 |>
   1.482 +      fold (fn name1 => fold (composition_instance name1) atoms) atoms |>
   1.483 +      fold (fn atom => fn thy =>
   1.484 +        let val pt_name = pt_class_of thy atom
   1.485 +        in
   1.486 +          fold (fn (s, tvs) => fn thy => AxClass.prove_arity
   1.487 +              (s, map (inter_sort thy [pt_name] o snd) tvs, [pt_name])
   1.488 +              (EVERY
   1.489 +                [Class.intro_classes_tac [],
   1.490 +                 resolve_tac perm_empty_thms 1,
   1.491 +                 resolve_tac perm_append_thms 1,
   1.492 +                 resolve_tac perm_eq_thms 1, assume_tac 1]) thy)
   1.493 +            (full_new_type_names' ~~ tyvars) thy
   1.494 +        end) atoms |>
   1.495 +      PureThy.add_thmss
   1.496 +        [((Binding.name (space_implode "_" new_type_names ^ "_unfolded_perm_eq"),
   1.497 +          unfolded_perm_eq_thms), [Simplifier.simp_add]),
   1.498 +         ((Binding.name (space_implode "_" new_type_names ^ "_perm_empty"),
   1.499 +          perm_empty_thms), [Simplifier.simp_add]),
   1.500 +         ((Binding.name (space_implode "_" new_type_names ^ "_perm_append"),
   1.501 +          perm_append_thms), [Simplifier.simp_add]),
   1.502 +         ((Binding.name (space_implode "_" new_type_names ^ "_perm_eq"),
   1.503 +          perm_eq_thms), [Simplifier.simp_add])];
   1.504 +
   1.505 +    (**** Define representing sets ****)
   1.506 +
   1.507 +    val _ = warning "representing sets";
   1.508 +
   1.509 +    val rep_set_names = DatatypeProp.indexify_names
   1.510 +      (map (fn (i, _) => name_of_typ (nth_dtyp i) ^ "_set") descr);
   1.511 +    val big_rep_name =
   1.512 +      space_implode "_" (DatatypeProp.indexify_names (List.mapPartial
   1.513 +        (fn (i, ("Nominal.noption", _, _)) => NONE
   1.514 +          | (i, _) => SOME (name_of_typ (nth_dtyp i))) descr)) ^ "_set";
   1.515 +    val _ = warning ("big_rep_name: " ^ big_rep_name);
   1.516 +
   1.517 +    fun strip_option (dtf as DtType ("fun", [dt, DtRec i])) =
   1.518 +          (case AList.lookup op = descr i of
   1.519 +             SOME ("Nominal.noption", _, [(_, [dt']), _]) =>
   1.520 +               apfst (cons dt) (strip_option dt')
   1.521 +           | _ => ([], dtf))
   1.522 +      | strip_option (DtType ("fun", [dt, DtType ("Nominal.noption", [dt'])])) =
   1.523 +          apfst (cons dt) (strip_option dt')
   1.524 +      | strip_option dt = ([], dt);
   1.525 +
   1.526 +    val dt_atomTs = distinct op = (map (typ_of_dtyp descr sorts)
   1.527 +      (List.concat (map (fn (_, (_, _, cs)) => List.concat
   1.528 +        (map (List.concat o map (fst o strip_option) o snd) cs)) descr)));
   1.529 +    val dt_atoms = map (fst o dest_Type) dt_atomTs;
   1.530 +
   1.531 +    fun make_intr s T (cname, cargs) =
   1.532 +      let
   1.533 +        fun mk_prem (dt, (j, j', prems, ts)) =
   1.534 +          let
   1.535 +            val (dts, dt') = strip_option dt;
   1.536 +            val (dts', dt'') = strip_dtyp dt';
   1.537 +            val Ts = map (typ_of_dtyp descr sorts) dts;
   1.538 +            val Us = map (typ_of_dtyp descr sorts) dts';
   1.539 +            val T = typ_of_dtyp descr sorts dt'';
   1.540 +            val free = mk_Free "x" (Us ---> T) j;
   1.541 +            val free' = app_bnds free (length Us);
   1.542 +            fun mk_abs_fun (T, (i, t)) =
   1.543 +              let val U = fastype_of t
   1.544 +              in (i + 1, Const ("Nominal.abs_fun", [T, U, T] --->
   1.545 +                Type ("Nominal.noption", [U])) $ mk_Free "y" T i $ t)
   1.546 +              end
   1.547 +          in (j + 1, j' + length Ts,
   1.548 +            case dt'' of
   1.549 +                DtRec k => list_all (map (pair "x") Us,
   1.550 +                  HOLogic.mk_Trueprop (Free (List.nth (rep_set_names, k),
   1.551 +                    T --> HOLogic.boolT) $ free')) :: prems
   1.552 +              | _ => prems,
   1.553 +            snd (List.foldr mk_abs_fun (j', free) Ts) :: ts)
   1.554 +          end;
   1.555 +
   1.556 +        val (_, _, prems, ts) = List.foldr mk_prem (1, 1, [], []) cargs;
   1.557 +        val concl = HOLogic.mk_Trueprop (Free (s, T --> HOLogic.boolT) $
   1.558 +          list_comb (Const (cname, map fastype_of ts ---> T), ts))
   1.559 +      in Logic.list_implies (prems, concl)
   1.560 +      end;
   1.561 +
   1.562 +    val (intr_ts, (rep_set_names', recTs')) =
   1.563 +      apfst List.concat (apsnd ListPair.unzip (ListPair.unzip (List.mapPartial
   1.564 +        (fn ((_, ("Nominal.noption", _, _)), _) => NONE
   1.565 +          | ((i, (_, _, constrs)), rep_set_name) =>
   1.566 +              let val T = nth_dtyp i
   1.567 +              in SOME (map (make_intr rep_set_name T) constrs,
   1.568 +                (rep_set_name, T))
   1.569 +              end)
   1.570 +                (descr ~~ rep_set_names))));
   1.571 +    val rep_set_names'' = map (Sign.full_bname thy3) rep_set_names';
   1.572 +
   1.573 +    val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy4) =
   1.574 +        Inductive.add_inductive_global (serial_string ())
   1.575 +          {quiet_mode = false, verbose = false, kind = Thm.internalK,
   1.576 +           alt_name = Binding.name big_rep_name, coind = false, no_elim = true, no_ind = false,
   1.577 +           skip_mono = true, fork_mono = false}
   1.578 +          (map (fn (s, T) => ((Binding.name s, T --> HOLogic.boolT), NoSyn))
   1.579 +             (rep_set_names' ~~ recTs'))
   1.580 +          [] (map (fn x => (Attrib.empty_binding, x)) intr_ts) [] thy3;
   1.581 +
   1.582 +    (**** Prove that representing set is closed under permutation ****)
   1.583 +
   1.584 +    val _ = warning "proving closure under permutation...";
   1.585 +
   1.586 +    val abs_perm = PureThy.get_thms thy4 "abs_perm";
   1.587 +
   1.588 +    val perm_indnames' = List.mapPartial
   1.589 +      (fn (x, (_, ("Nominal.noption", _, _))) => NONE | (x, _) => SOME x)
   1.590 +      (perm_indnames ~~ descr);
   1.591 +
   1.592 +    fun mk_perm_closed name = map (fn th => standard (th RS mp))
   1.593 +      (List.take (split_conj_thm (Goal.prove_global thy4 [] []
   1.594 +        (augment_sort thy4
   1.595 +          (pt_class_of thy4 name :: map (cp_class_of thy4 name) (dt_atoms \ name))
   1.596 +          (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map
   1.597 +            (fn ((s, T), x) =>
   1.598 +               let
   1.599 +                 val S = Const (s, T --> HOLogic.boolT);
   1.600 +                 val permT = mk_permT (Type (name, []))
   1.601 +               in HOLogic.mk_imp (S $ Free (x, T),
   1.602 +                 S $ (Const ("Nominal.perm", permT --> T --> T) $
   1.603 +                   Free ("pi", permT) $ Free (x, T)))
   1.604 +               end) (rep_set_names'' ~~ recTs' ~~ perm_indnames')))))
   1.605 +        (fn _ => EVERY
   1.606 +           [indtac rep_induct [] 1,
   1.607 +            ALLGOALS (simp_tac (simpset_of thy4 addsimps
   1.608 +              (symmetric perm_fun_def :: abs_perm))),
   1.609 +            ALLGOALS (resolve_tac rep_intrs THEN_ALL_NEW assume_tac)])),
   1.610 +        length new_type_names));
   1.611 +
   1.612 +    val perm_closed_thmss = map mk_perm_closed atoms;
   1.613 +
   1.614 +    (**** typedef ****)
   1.615 +
   1.616 +    val _ = warning "defining type...";
   1.617 +
   1.618 +    val (typedefs, thy6) =
   1.619 +      thy4
   1.620 +      |> fold_map (fn ((((name, mx), tvs), (cname, U)), name') => fn thy =>
   1.621 +          Typedef.add_typedef false (SOME (Binding.name name'))
   1.622 +            (Binding.name name, map fst tvs, mx)
   1.623 +            (Const ("Collect", (U --> HOLogic.boolT) --> HOLogic.mk_setT U) $
   1.624 +               Const (cname, U --> HOLogic.boolT)) NONE
   1.625 +            (rtac exI 1 THEN rtac CollectI 1 THEN
   1.626 +              QUIET_BREADTH_FIRST (has_fewer_prems 1)
   1.627 +              (resolve_tac rep_intrs 1)) thy |> (fn ((_, r), thy) =>
   1.628 +        let
   1.629 +          val permT = mk_permT
   1.630 +            (TFree (Name.variant (map fst tvs) "'a", HOLogic.typeS));
   1.631 +          val pi = Free ("pi", permT);
   1.632 +          val T = Type (Sign.intern_type thy name, map TFree tvs);
   1.633 +        in apfst (pair r o hd)
   1.634 +          (PureThy.add_defs_unchecked true [((Binding.name ("prm_" ^ name ^ "_def"), Logic.mk_equals
   1.635 +            (Const ("Nominal.perm", permT --> T --> T) $ pi $ Free ("x", T),
   1.636 +             Const (Sign.intern_const thy ("Abs_" ^ name), U --> T) $
   1.637 +               (Const ("Nominal.perm", permT --> U --> U) $ pi $
   1.638 +                 (Const (Sign.intern_const thy ("Rep_" ^ name), T --> U) $
   1.639 +                   Free ("x", T))))), [])] thy)
   1.640 +        end))
   1.641 +          (types_syntax ~~ tyvars ~~
   1.642 +            List.take (rep_set_names'' ~~ recTs', length new_type_names) ~~
   1.643 +            new_type_names);
   1.644 +
   1.645 +    val perm_defs = map snd typedefs;
   1.646 +    val Abs_inverse_thms = map (collect_simp o #Abs_inverse o fst) typedefs;
   1.647 +    val Rep_inverse_thms = map (#Rep_inverse o fst) typedefs;
   1.648 +    val Rep_thms = map (collect_simp o #Rep o fst) typedefs;
   1.649 +
   1.650 +
   1.651 +    (** prove that new types are in class pt_<name> **)
   1.652 +
   1.653 +    val _ = warning "prove that new types are in class pt_<name> ...";
   1.654 +
   1.655 +    fun pt_instance (atom, perm_closed_thms) =
   1.656 +      fold (fn ((((((Abs_inverse, Rep_inverse), Rep),
   1.657 +        perm_def), name), tvs), perm_closed) => fn thy =>
   1.658 +          let
   1.659 +            val pt_class = pt_class_of thy atom;
   1.660 +            val sort = Sign.certify_sort thy
   1.661 +              (pt_class :: map (cp_class_of thy atom) (dt_atoms \ atom))
   1.662 +          in AxClass.prove_arity
   1.663 +            (Sign.intern_type thy name,
   1.664 +              map (inter_sort thy sort o snd) tvs, [pt_class])
   1.665 +            (EVERY [Class.intro_classes_tac [],
   1.666 +              rewrite_goals_tac [perm_def],
   1.667 +              asm_full_simp_tac (simpset_of thy addsimps [Rep_inverse]) 1,
   1.668 +              asm_full_simp_tac (simpset_of thy addsimps
   1.669 +                [Rep RS perm_closed RS Abs_inverse]) 1,
   1.670 +              asm_full_simp_tac (HOL_basic_ss addsimps [PureThy.get_thm thy
   1.671 +                ("pt_" ^ Long_Name.base_name atom ^ "3")]) 1]) thy
   1.672 +          end)
   1.673 +        (Abs_inverse_thms ~~ Rep_inverse_thms ~~ Rep_thms ~~ perm_defs ~~
   1.674 +           new_type_names ~~ tyvars ~~ perm_closed_thms);
   1.675 +
   1.676 +
   1.677 +    (** prove that new types are in class cp_<name1>_<name2> **)
   1.678 +
   1.679 +    val _ = warning "prove that new types are in class cp_<name1>_<name2> ...";
   1.680 +
   1.681 +    fun cp_instance (atom1, perm_closed_thms1) (atom2, perm_closed_thms2) thy =
   1.682 +      let
   1.683 +        val cp_class = cp_class_of thy atom1 atom2;
   1.684 +        val sort = Sign.certify_sort thy
   1.685 +          (pt_class_of thy atom1 :: map (cp_class_of thy atom1) (dt_atoms \ atom1) @
   1.686 +           (if atom1 = atom2 then [cp_class_of thy atom1 atom1] else
   1.687 +            pt_class_of thy atom2 :: map (cp_class_of thy atom2) (dt_atoms \ atom2)));
   1.688 +        val cp1' = cp_inst_of thy atom1 atom2 RS cp1
   1.689 +      in fold (fn ((((((Abs_inverse, Rep),
   1.690 +        perm_def), name), tvs), perm_closed1), perm_closed2) => fn thy =>
   1.691 +          AxClass.prove_arity
   1.692 +            (Sign.intern_type thy name,
   1.693 +              map (inter_sort thy sort o snd) tvs, [cp_class])
   1.694 +            (EVERY [Class.intro_classes_tac [],
   1.695 +              rewrite_goals_tac [perm_def],
   1.696 +              asm_full_simp_tac (simpset_of thy addsimps
   1.697 +                ((Rep RS perm_closed1 RS Abs_inverse) ::
   1.698 +                 (if atom1 = atom2 then []
   1.699 +                  else [Rep RS perm_closed2 RS Abs_inverse]))) 1,
   1.700 +              cong_tac 1,
   1.701 +              rtac refl 1,
   1.702 +              rtac cp1' 1]) thy)
   1.703 +        (Abs_inverse_thms ~~ Rep_thms ~~ perm_defs ~~ new_type_names ~~
   1.704 +           tyvars ~~ perm_closed_thms1 ~~ perm_closed_thms2) thy
   1.705 +      end;
   1.706 +
   1.707 +    val thy7 = fold (fn x => fn thy => thy |>
   1.708 +      pt_instance x |>
   1.709 +      fold (cp_instance x) (atoms ~~ perm_closed_thmss))
   1.710 +        (atoms ~~ perm_closed_thmss) thy6;
   1.711 +
   1.712 +    (**** constructors ****)
   1.713 +
   1.714 +    fun mk_abs_fun (x, t) =
   1.715 +      let
   1.716 +        val T = fastype_of x;
   1.717 +        val U = fastype_of t
   1.718 +      in
   1.719 +        Const ("Nominal.abs_fun", T --> U --> T -->
   1.720 +          Type ("Nominal.noption", [U])) $ x $ t
   1.721 +      end;
   1.722 +
   1.723 +    val (ty_idxs, _) = List.foldl
   1.724 +      (fn ((i, ("Nominal.noption", _, _)), p) => p
   1.725 +        | ((i, _), (ty_idxs, j)) => (ty_idxs @ [(i, j)], j + 1)) ([], 0) descr;
   1.726 +
   1.727 +    fun reindex (DtType (s, dts)) = DtType (s, map reindex dts)
   1.728 +      | reindex (DtRec i) = DtRec (the (AList.lookup op = ty_idxs i))
   1.729 +      | reindex dt = dt;
   1.730 +
   1.731 +    fun strip_suffix i s = implode (List.take (explode s, size s - i));
   1.732 +
   1.733 +    (** strips the "_Rep" in type names *)
   1.734 +    fun strip_nth_name i s =
   1.735 +      let val xs = Long_Name.explode s;
   1.736 +      in Long_Name.implode (Library.nth_map (length xs - i) (strip_suffix 4) xs) end;
   1.737 +
   1.738 +    val (descr'', ndescr) = ListPair.unzip (map_filter
   1.739 +      (fn (i, ("Nominal.noption", _, _)) => NONE
   1.740 +        | (i, (s, dts, constrs)) =>
   1.741 +             let
   1.742 +               val SOME index = AList.lookup op = ty_idxs i;
   1.743 +               val (constrs2, constrs1) =
   1.744 +                 map_split (fn (cname, cargs) =>
   1.745 +                   apsnd (pair (strip_nth_name 2 (strip_nth_name 1 cname)))
   1.746 +                   (fold_map (fn dt => fn dts =>
   1.747 +                     let val (dts', dt') = strip_option dt
   1.748 +                     in ((length dts, length dts'), dts @ dts' @ [reindex dt']) end)
   1.749 +                       cargs [])) constrs
   1.750 +             in SOME ((index, (strip_nth_name 1 s,  map reindex dts, constrs1)),
   1.751 +               (index, constrs2))
   1.752 +             end) descr);
   1.753 +
   1.754 +    val (descr1, descr2) = chop (length new_type_names) descr'';
   1.755 +    val descr' = [descr1, descr2];
   1.756 +
   1.757 +    fun partition_cargs idxs xs = map (fn (i, j) =>
   1.758 +      (List.take (List.drop (xs, i), j), List.nth (xs, i + j))) idxs;
   1.759 +
   1.760 +    val pdescr = map (fn ((i, (s, dts, constrs)), (_, idxss)) => (i, (s, dts,
   1.761 +      map (fn ((cname, cargs), idxs) => (cname, partition_cargs idxs cargs))
   1.762 +        (constrs ~~ idxss)))) (descr'' ~~ ndescr);
   1.763 +
   1.764 +    fun nth_dtyp' i = typ_of_dtyp descr'' sorts (DtRec i);
   1.765 +
   1.766 +    val rep_names = map (fn s =>
   1.767 +      Sign.intern_const thy7 ("Rep_" ^ s)) new_type_names;
   1.768 +    val abs_names = map (fn s =>
   1.769 +      Sign.intern_const thy7 ("Abs_" ^ s)) new_type_names;
   1.770 +
   1.771 +    val recTs = get_rec_types descr'' sorts;
   1.772 +    val newTs' = Library.take (length new_type_names, recTs');
   1.773 +    val newTs = Library.take (length new_type_names, recTs);
   1.774 +
   1.775 +    val full_new_type_names = map (Sign.full_bname thy) new_type_names;
   1.776 +
   1.777 +    fun make_constr_def tname T T' ((thy, defs, eqns),
   1.778 +        (((cname_rep, _), (cname, cargs)), (cname', mx))) =
   1.779 +      let
   1.780 +        fun constr_arg ((dts, dt), (j, l_args, r_args)) =
   1.781 +          let
   1.782 +            val xs = map (fn (dt, i) => mk_Free "x" (typ_of_dtyp descr'' sorts dt) i)
   1.783 +              (dts ~~ (j upto j + length dts - 1))
   1.784 +            val x = mk_Free "x" (typ_of_dtyp descr'' sorts dt) (j + length dts)
   1.785 +          in
   1.786 +            (j + length dts + 1,
   1.787 +             xs @ x :: l_args,
   1.788 +             List.foldr mk_abs_fun
   1.789 +               (case dt of
   1.790 +                  DtRec k => if k < length new_type_names then
   1.791 +                      Const (List.nth (rep_names, k), typ_of_dtyp descr'' sorts dt -->
   1.792 +                        typ_of_dtyp descr sorts dt) $ x
   1.793 +                    else error "nested recursion not (yet) supported"
   1.794 +                | _ => x) xs :: r_args)
   1.795 +          end
   1.796 +
   1.797 +        val (_, l_args, r_args) = List.foldr constr_arg (1, [], []) cargs;
   1.798 +        val abs_name = Sign.intern_const thy ("Abs_" ^ tname);
   1.799 +        val rep_name = Sign.intern_const thy ("Rep_" ^ tname);
   1.800 +        val constrT = map fastype_of l_args ---> T;
   1.801 +        val lhs = list_comb (Const (cname, constrT), l_args);
   1.802 +        val rhs = list_comb (Const (cname_rep, map fastype_of r_args ---> T'), r_args);
   1.803 +        val def = Logic.mk_equals (lhs, Const (abs_name, T' --> T) $ rhs);
   1.804 +        val eqn = HOLogic.mk_Trueprop (HOLogic.mk_eq
   1.805 +          (Const (rep_name, T --> T') $ lhs, rhs));
   1.806 +        val def_name = (Long_Name.base_name cname) ^ "_def";
   1.807 +        val ([def_thm], thy') = thy |>
   1.808 +          Sign.add_consts_i [(Binding.name cname', constrT, mx)] |>
   1.809 +          (PureThy.add_defs false o map Thm.no_attributes) [(Binding.name def_name, def)]
   1.810 +      in (thy', defs @ [def_thm], eqns @ [eqn]) end;
   1.811 +
   1.812 +    fun dt_constr_defs ((thy, defs, eqns, dist_lemmas), ((((((_, (_, _, constrs)),
   1.813 +        (_, (_, _, constrs'))), tname), T), T'), constr_syntax)) =
   1.814 +      let
   1.815 +        val rep_const = cterm_of thy
   1.816 +          (Const (Sign.intern_const thy ("Rep_" ^ tname), T --> T'));
   1.817 +        val dist = standard (cterm_instantiate [(cterm_of thy distinct_f, rep_const)] distinct_lemma);
   1.818 +        val (thy', defs', eqns') = Library.foldl (make_constr_def tname T T')
   1.819 +          ((Sign.add_path tname thy, defs, []), constrs ~~ constrs' ~~ constr_syntax)
   1.820 +      in
   1.821 +        (parent_path (#flat_names config) thy', defs', eqns @ [eqns'], dist_lemmas @ [dist])
   1.822 +      end;
   1.823 +
   1.824 +    val (thy8, constr_defs, constr_rep_eqns, dist_lemmas) = Library.foldl dt_constr_defs
   1.825 +      ((thy7, [], [], []), List.take (descr, length new_type_names) ~~
   1.826 +        List.take (pdescr, length new_type_names) ~~
   1.827 +        new_type_names ~~ newTs ~~ newTs' ~~ constr_syntax);
   1.828 +
   1.829 +    val abs_inject_thms = map (collect_simp o #Abs_inject o fst) typedefs
   1.830 +    val rep_inject_thms = map (#Rep_inject o fst) typedefs
   1.831 +
   1.832 +    (* prove theorem  Rep_i (Constr_j ...) = Constr'_j ...  *)
   1.833 +
   1.834 +    fun prove_constr_rep_thm eqn =
   1.835 +      let
   1.836 +        val inj_thms = map (fn r => r RS iffD1) abs_inject_thms;
   1.837 +        val rewrites = constr_defs @ map mk_meta_eq Rep_inverse_thms
   1.838 +      in Goal.prove_global thy8 [] [] eqn (fn _ => EVERY
   1.839 +        [resolve_tac inj_thms 1,
   1.840 +         rewrite_goals_tac rewrites,
   1.841 +         rtac refl 3,
   1.842 +         resolve_tac rep_intrs 2,
   1.843 +         REPEAT (resolve_tac Rep_thms 1)])
   1.844 +      end;
   1.845 +
   1.846 +    val constr_rep_thmss = map (map prove_constr_rep_thm) constr_rep_eqns;
   1.847 +
   1.848 +    (* prove theorem  pi \<bullet> Rep_i x = Rep_i (pi \<bullet> x) *)
   1.849 +
   1.850 +    fun prove_perm_rep_perm (atom, perm_closed_thms) = map (fn th =>
   1.851 +      let
   1.852 +        val _ $ (_ $ (Rep $ x)) = Logic.unvarify (prop_of th);
   1.853 +        val Type ("fun", [T, U]) = fastype_of Rep;
   1.854 +        val permT = mk_permT (Type (atom, []));
   1.855 +        val pi = Free ("pi", permT);
   1.856 +      in
   1.857 +        Goal.prove_global thy8 [] []
   1.858 +          (augment_sort thy8
   1.859 +            (pt_class_of thy8 atom :: map (cp_class_of thy8 atom) (dt_atoms \ atom))
   1.860 +            (HOLogic.mk_Trueprop (HOLogic.mk_eq
   1.861 +              (Const ("Nominal.perm", permT --> U --> U) $ pi $ (Rep $ x),
   1.862 +               Rep $ (Const ("Nominal.perm", permT --> T --> T) $ pi $ x)))))
   1.863 +          (fn _ => simp_tac (HOL_basic_ss addsimps (perm_defs @ Abs_inverse_thms @
   1.864 +            perm_closed_thms @ Rep_thms)) 1)
   1.865 +      end) Rep_thms;
   1.866 +
   1.867 +    val perm_rep_perm_thms = List.concat (map prove_perm_rep_perm
   1.868 +      (atoms ~~ perm_closed_thmss));
   1.869 +
   1.870 +    (* prove distinctness theorems *)
   1.871 +
   1.872 +    val distinct_props = DatatypeProp.make_distincts descr' sorts;
   1.873 +    val dist_rewrites = map2 (fn rep_thms => fn dist_lemma =>
   1.874 +      dist_lemma :: rep_thms @ [In0_eq, In1_eq, In0_not_In1, In1_not_In0])
   1.875 +        constr_rep_thmss dist_lemmas;
   1.876 +
   1.877 +    fun prove_distinct_thms _ (_, []) = []
   1.878 +      | prove_distinct_thms (p as (rep_thms, dist_lemma)) (k, t :: ts) =
   1.879 +          let
   1.880 +            val dist_thm = Goal.prove_global thy8 [] [] t (fn _ =>
   1.881 +              simp_tac (simpset_of thy8 addsimps (dist_lemma :: rep_thms)) 1)
   1.882 +          in dist_thm :: standard (dist_thm RS not_sym) ::
   1.883 +            prove_distinct_thms p (k, ts)
   1.884 +          end;
   1.885 +
   1.886 +    val distinct_thms = map2 prove_distinct_thms
   1.887 +      (constr_rep_thmss ~~ dist_lemmas) distinct_props;
   1.888 +
   1.889 +    (** prove equations for permutation functions **)
   1.890 +
   1.891 +    val perm_simps' = map (fn (((i, (_, _, constrs)), tname), constr_rep_thms) =>
   1.892 +      let val T = nth_dtyp' i
   1.893 +      in List.concat (map (fn (atom, perm_closed_thms) =>
   1.894 +          map (fn ((cname, dts), constr_rep_thm) =>
   1.895 +        let
   1.896 +          val cname = Sign.intern_const thy8
   1.897 +            (Long_Name.append tname (Long_Name.base_name cname));
   1.898 +          val permT = mk_permT (Type (atom, []));
   1.899 +          val pi = Free ("pi", permT);
   1.900 +
   1.901 +          fun perm t =
   1.902 +            let val T = fastype_of t
   1.903 +            in Const ("Nominal.perm", permT --> T --> T) $ pi $ t end;
   1.904 +
   1.905 +          fun constr_arg ((dts, dt), (j, l_args, r_args)) =
   1.906 +            let
   1.907 +              val Ts = map (typ_of_dtyp descr'' sorts) dts;
   1.908 +              val xs = map (fn (T, i) => mk_Free "x" T i)
   1.909 +                (Ts ~~ (j upto j + length dts - 1))
   1.910 +              val x = mk_Free "x" (typ_of_dtyp descr'' sorts dt) (j + length dts)
   1.911 +            in
   1.912 +              (j + length dts + 1,
   1.913 +               xs @ x :: l_args,
   1.914 +               map perm (xs @ [x]) @ r_args)
   1.915 +            end
   1.916 +
   1.917 +          val (_, l_args, r_args) = List.foldr constr_arg (1, [], []) dts;
   1.918 +          val c = Const (cname, map fastype_of l_args ---> T)
   1.919 +        in
   1.920 +          Goal.prove_global thy8 [] []
   1.921 +            (augment_sort thy8
   1.922 +              (pt_class_of thy8 atom :: map (cp_class_of thy8 atom) (dt_atoms \ atom))
   1.923 +              (HOLogic.mk_Trueprop (HOLogic.mk_eq
   1.924 +                (perm (list_comb (c, l_args)), list_comb (c, r_args)))))
   1.925 +            (fn _ => EVERY
   1.926 +              [simp_tac (simpset_of thy8 addsimps (constr_rep_thm :: perm_defs)) 1,
   1.927 +               simp_tac (HOL_basic_ss addsimps (Rep_thms @ Abs_inverse_thms @
   1.928 +                 constr_defs @ perm_closed_thms)) 1,
   1.929 +               TRY (simp_tac (HOL_basic_ss addsimps
   1.930 +                 (symmetric perm_fun_def :: abs_perm)) 1),
   1.931 +               TRY (simp_tac (HOL_basic_ss addsimps
   1.932 +                 (perm_fun_def :: perm_defs @ Rep_thms @ Abs_inverse_thms @
   1.933 +                    perm_closed_thms)) 1)])
   1.934 +        end) (constrs ~~ constr_rep_thms)) (atoms ~~ perm_closed_thmss))
   1.935 +      end) (List.take (pdescr, length new_type_names) ~~ new_type_names ~~ constr_rep_thmss);
   1.936 +
   1.937 +    (** prove injectivity of constructors **)
   1.938 +
   1.939 +    val rep_inject_thms' = map (fn th => th RS sym) rep_inject_thms;
   1.940 +    val alpha = PureThy.get_thms thy8 "alpha";
   1.941 +    val abs_fresh = PureThy.get_thms thy8 "abs_fresh";
   1.942 +
   1.943 +    val pt_cp_sort =
   1.944 +      map (pt_class_of thy8) dt_atoms @
   1.945 +      maps (fn s => map (cp_class_of thy8 s) (dt_atoms \ s)) dt_atoms;
   1.946 +
   1.947 +    val inject_thms = map (fn (((i, (_, _, constrs)), tname), constr_rep_thms) =>
   1.948 +      let val T = nth_dtyp' i
   1.949 +      in List.mapPartial (fn ((cname, dts), constr_rep_thm) =>
   1.950 +        if null dts then NONE else SOME
   1.951 +        let
   1.952 +          val cname = Sign.intern_const thy8
   1.953 +            (Long_Name.append tname (Long_Name.base_name cname));
   1.954 +
   1.955 +          fun make_inj ((dts, dt), (j, args1, args2, eqs)) =
   1.956 +            let
   1.957 +              val Ts_idx = map (typ_of_dtyp descr'' sorts) dts ~~ (j upto j + length dts - 1);
   1.958 +              val xs = map (fn (T, i) => mk_Free "x" T i) Ts_idx;
   1.959 +              val ys = map (fn (T, i) => mk_Free "y" T i) Ts_idx;
   1.960 +              val x = mk_Free "x" (typ_of_dtyp descr'' sorts dt) (j + length dts);
   1.961 +              val y = mk_Free "y" (typ_of_dtyp descr'' sorts dt) (j + length dts)
   1.962 +            in
   1.963 +              (j + length dts + 1,
   1.964 +               xs @ (x :: args1), ys @ (y :: args2),
   1.965 +               HOLogic.mk_eq
   1.966 +                 (List.foldr mk_abs_fun x xs, List.foldr mk_abs_fun y ys) :: eqs)
   1.967 +            end;
   1.968 +
   1.969 +          val (_, args1, args2, eqs) = List.foldr make_inj (1, [], [], []) dts;
   1.970 +          val Ts = map fastype_of args1;
   1.971 +          val c = Const (cname, Ts ---> T)
   1.972 +        in
   1.973 +          Goal.prove_global thy8 [] []
   1.974 +            (augment_sort thy8 pt_cp_sort
   1.975 +              (HOLogic.mk_Trueprop (HOLogic.mk_eq
   1.976 +                (HOLogic.mk_eq (list_comb (c, args1), list_comb (c, args2)),
   1.977 +                 foldr1 HOLogic.mk_conj eqs))))
   1.978 +            (fn _ => EVERY
   1.979 +               [asm_full_simp_tac (simpset_of thy8 addsimps (constr_rep_thm ::
   1.980 +                  rep_inject_thms')) 1,
   1.981 +                TRY (asm_full_simp_tac (HOL_basic_ss addsimps (fresh_def :: supp_def ::
   1.982 +                  alpha @ abs_perm @ abs_fresh @ rep_inject_thms @
   1.983 +                  perm_rep_perm_thms)) 1)])
   1.984 +        end) (constrs ~~ constr_rep_thms)
   1.985 +      end) (List.take (pdescr, length new_type_names) ~~ new_type_names ~~ constr_rep_thmss);
   1.986 +
   1.987 +    (** equations for support and freshness **)
   1.988 +
   1.989 +    val (supp_thms, fresh_thms) = ListPair.unzip (map ListPair.unzip
   1.990 +      (map (fn ((((i, (_, _, constrs)), tname), inject_thms'), perm_thms') =>
   1.991 +      let val T = nth_dtyp' i
   1.992 +      in List.concat (map (fn (cname, dts) => map (fn atom =>
   1.993 +        let
   1.994 +          val cname = Sign.intern_const thy8
   1.995 +            (Long_Name.append tname (Long_Name.base_name cname));
   1.996 +          val atomT = Type (atom, []);
   1.997 +
   1.998 +          fun process_constr ((dts, dt), (j, args1, args2)) =
   1.999 +            let
  1.1000 +              val Ts_idx = map (typ_of_dtyp descr'' sorts) dts ~~ (j upto j + length dts - 1);
  1.1001 +              val xs = map (fn (T, i) => mk_Free "x" T i) Ts_idx;
  1.1002 +              val x = mk_Free "x" (typ_of_dtyp descr'' sorts dt) (j + length dts)
  1.1003 +            in
  1.1004 +              (j + length dts + 1,
  1.1005 +               xs @ (x :: args1), List.foldr mk_abs_fun x xs :: args2)
  1.1006 +            end;
  1.1007 +
  1.1008 +          val (_, args1, args2) = List.foldr process_constr (1, [], []) dts;
  1.1009 +          val Ts = map fastype_of args1;
  1.1010 +          val c = list_comb (Const (cname, Ts ---> T), args1);
  1.1011 +          fun supp t =
  1.1012 +            Const ("Nominal.supp", fastype_of t --> HOLogic.mk_setT atomT) $ t;
  1.1013 +          fun fresh t = fresh_const atomT (fastype_of t) $ Free ("a", atomT) $ t;
  1.1014 +          val supp_thm = Goal.prove_global thy8 [] []
  1.1015 +            (augment_sort thy8 pt_cp_sort
  1.1016 +              (HOLogic.mk_Trueprop (HOLogic.mk_eq
  1.1017 +                (supp c,
  1.1018 +                 if null dts then HOLogic.mk_set atomT []
  1.1019 +                 else foldr1 (HOLogic.mk_binop @{const_name Un}) (map supp args2)))))
  1.1020 +            (fn _ =>
  1.1021 +              simp_tac (HOL_basic_ss addsimps (supp_def ::
  1.1022 +                 Un_assoc :: de_Morgan_conj :: Collect_disj_eq :: finite_Un ::
  1.1023 +                 symmetric empty_def :: finite_emptyI :: simp_thms @
  1.1024 +                 abs_perm @ abs_fresh @ inject_thms' @ perm_thms')) 1)
  1.1025 +        in
  1.1026 +          (supp_thm,
  1.1027 +           Goal.prove_global thy8 [] [] (augment_sort thy8 pt_cp_sort
  1.1028 +             (HOLogic.mk_Trueprop (HOLogic.mk_eq
  1.1029 +               (fresh c,
  1.1030 +                if null dts then HOLogic.true_const
  1.1031 +                else foldr1 HOLogic.mk_conj (map fresh args2)))))
  1.1032 +             (fn _ =>
  1.1033 +               simp_tac (HOL_ss addsimps [Un_iff, empty_iff, fresh_def, supp_thm]) 1))
  1.1034 +        end) atoms) constrs)
  1.1035 +      end) (List.take (pdescr, length new_type_names) ~~ new_type_names ~~ inject_thms ~~ perm_simps')));
  1.1036 +
  1.1037 +    (**** weak induction theorem ****)
  1.1038 +
  1.1039 +    fun mk_indrule_lemma ((prems, concls), (((i, _), T), U)) =
  1.1040 +      let
  1.1041 +        val Rep_t = Const (List.nth (rep_names, i), T --> U) $
  1.1042 +          mk_Free "x" T i;
  1.1043 +
  1.1044 +        val Abs_t =  Const (List.nth (abs_names, i), U --> T)
  1.1045 +
  1.1046 +      in (prems @ [HOLogic.imp $
  1.1047 +            (Const (List.nth (rep_set_names'', i), U --> HOLogic.boolT) $ Rep_t) $
  1.1048 +              (mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ (Abs_t $ Rep_t))],
  1.1049 +          concls @ [mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ mk_Free "x" T i])
  1.1050 +      end;
  1.1051 +
  1.1052 +    val (indrule_lemma_prems, indrule_lemma_concls) =
  1.1053 +      Library.foldl mk_indrule_lemma (([], []), (descr'' ~~ recTs ~~ recTs'));
  1.1054 +
  1.1055 +    val indrule_lemma = Goal.prove_global thy8 [] []
  1.1056 +      (Logic.mk_implies
  1.1057 +        (HOLogic.mk_Trueprop (mk_conj indrule_lemma_prems),
  1.1058 +         HOLogic.mk_Trueprop (mk_conj indrule_lemma_concls))) (fn _ => EVERY
  1.1059 +           [REPEAT (etac conjE 1),
  1.1060 +            REPEAT (EVERY
  1.1061 +              [TRY (rtac conjI 1), full_simp_tac (HOL_basic_ss addsimps Rep_inverse_thms) 1,
  1.1062 +               etac mp 1, resolve_tac Rep_thms 1])]);
  1.1063 +
  1.1064 +    val Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of indrule_lemma)));
  1.1065 +    val frees = if length Ps = 1 then [Free ("P", snd (dest_Var (hd Ps)))] else
  1.1066 +      map (Free o apfst fst o dest_Var) Ps;
  1.1067 +    val indrule_lemma' = cterm_instantiate
  1.1068 +      (map (cterm_of thy8) Ps ~~ map (cterm_of thy8) frees) indrule_lemma;
  1.1069 +
  1.1070 +    val Abs_inverse_thms' = map (fn r => r RS subst) Abs_inverse_thms;
  1.1071 +
  1.1072 +    val dt_induct_prop = DatatypeProp.make_ind descr' sorts;
  1.1073 +    val dt_induct = Goal.prove_global thy8 []
  1.1074 +      (Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop)
  1.1075 +      (fn {prems, ...} => EVERY
  1.1076 +        [rtac indrule_lemma' 1,
  1.1077 +         (indtac rep_induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
  1.1078 +         EVERY (map (fn (prem, r) => (EVERY
  1.1079 +           [REPEAT (eresolve_tac Abs_inverse_thms' 1),
  1.1080 +            simp_tac (HOL_basic_ss addsimps [symmetric r]) 1,
  1.1081 +            DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE etac allE 1)]))
  1.1082 +                (prems ~~ constr_defs))]);
  1.1083 +
  1.1084 +    val case_names_induct = mk_case_names_induct descr'';
  1.1085 +
  1.1086 +    (**** prove that new datatypes have finite support ****)
  1.1087 +
  1.1088 +    val _ = warning "proving finite support for the new datatype";
  1.1089 +
  1.1090 +    val indnames = DatatypeProp.make_tnames recTs;
  1.1091 +
  1.1092 +    val abs_supp = PureThy.get_thms thy8 "abs_supp";
  1.1093 +    val supp_atm = PureThy.get_thms thy8 "supp_atm";
  1.1094 +
  1.1095 +    val finite_supp_thms = map (fn atom =>
  1.1096 +      let val atomT = Type (atom, [])
  1.1097 +      in map standard (List.take
  1.1098 +        (split_conj_thm (Goal.prove_global thy8 [] []
  1.1099 +           (augment_sort thy8 (fs_class_of thy8 atom :: pt_cp_sort)
  1.1100 +             (HOLogic.mk_Trueprop
  1.1101 +               (foldr1 HOLogic.mk_conj (map (fn (s, T) =>
  1.1102 +                 Const ("Finite_Set.finite", HOLogic.mk_setT atomT --> HOLogic.boolT) $
  1.1103 +                   (Const ("Nominal.supp", T --> HOLogic.mk_setT atomT) $ Free (s, T)))
  1.1104 +                   (indnames ~~ recTs)))))
  1.1105 +           (fn _ => indtac dt_induct indnames 1 THEN
  1.1106 +            ALLGOALS (asm_full_simp_tac (simpset_of thy8 addsimps
  1.1107 +              (abs_supp @ supp_atm @
  1.1108 +               PureThy.get_thms thy8 ("fs_" ^ Long_Name.base_name atom ^ "1") @
  1.1109 +               List.concat supp_thms))))),
  1.1110 +         length new_type_names))
  1.1111 +      end) atoms;
  1.1112 +
  1.1113 +    val simp_atts = replicate (length new_type_names) [Simplifier.simp_add];
  1.1114 +
  1.1115 +	(* Function to add both the simp and eqvt attributes *)
  1.1116 +        (* These two attributes are duplicated on all the types in the mutual nominal datatypes *)
  1.1117 +
  1.1118 +    val simp_eqvt_atts = replicate (length new_type_names) [Simplifier.simp_add, NominalThmDecls.eqvt_add];
  1.1119 + 
  1.1120 +    val (_, thy9) = thy8 |>
  1.1121 +      Sign.add_path big_name |>
  1.1122 +      PureThy.add_thms [((Binding.name "induct", dt_induct), [case_names_induct])] ||>>
  1.1123 +      PureThy.add_thmss [((Binding.name "inducts", projections dt_induct), [case_names_induct])] ||>
  1.1124 +      Sign.parent_path ||>>
  1.1125 +      DatatypeAux.store_thmss_atts "distinct" new_type_names simp_atts distinct_thms ||>>
  1.1126 +      DatatypeAux.store_thmss "constr_rep" new_type_names constr_rep_thmss ||>>
  1.1127 +      DatatypeAux.store_thmss_atts "perm" new_type_names simp_eqvt_atts perm_simps' ||>>
  1.1128 +      DatatypeAux.store_thmss "inject" new_type_names inject_thms ||>>
  1.1129 +      DatatypeAux.store_thmss "supp" new_type_names supp_thms ||>>
  1.1130 +      DatatypeAux.store_thmss_atts "fresh" new_type_names simp_atts fresh_thms ||>
  1.1131 +      fold (fn (atom, ths) => fn thy =>
  1.1132 +        let
  1.1133 +          val class = fs_class_of thy atom;
  1.1134 +          val sort = Sign.certify_sort thy (class :: pt_cp_sort)
  1.1135 +        in fold (fn Type (s, Ts) => AxClass.prove_arity
  1.1136 +          (s, map (inter_sort thy sort o snd o dest_TFree) Ts, [class])
  1.1137 +          (Class.intro_classes_tac [] THEN resolve_tac ths 1)) newTs thy
  1.1138 +        end) (atoms ~~ finite_supp_thms);
  1.1139 +
  1.1140 +    (**** strong induction theorem ****)
  1.1141 +
  1.1142 +    val pnames = if length descr'' = 1 then ["P"]
  1.1143 +      else map (fn i => "P" ^ string_of_int i) (1 upto length descr'');
  1.1144 +    val ind_sort = if null dt_atomTs then HOLogic.typeS
  1.1145 +      else Sign.certify_sort thy9 (map (fs_class_of thy9) dt_atoms);
  1.1146 +    val fsT = TFree ("'n", ind_sort);
  1.1147 +    val fsT' = TFree ("'n", HOLogic.typeS);
  1.1148 +
  1.1149 +    val fresh_fs = map (fn (s, T) => (T, Free (s, fsT' --> HOLogic.mk_setT T)))
  1.1150 +      (DatatypeProp.indexify_names (replicate (length dt_atomTs) "f") ~~ dt_atomTs);
  1.1151 +
  1.1152 +    fun make_pred fsT i T =
  1.1153 +      Free (List.nth (pnames, i), fsT --> T --> HOLogic.boolT);
  1.1154 +
  1.1155 +    fun mk_fresh1 xs [] = []
  1.1156 +      | mk_fresh1 xs ((y as (_, T)) :: ys) = map (fn x => HOLogic.mk_Trueprop
  1.1157 +            (HOLogic.mk_not (HOLogic.mk_eq (Free y, Free x))))
  1.1158 +              (filter (fn (_, U) => T = U) (rev xs)) @
  1.1159 +          mk_fresh1 (y :: xs) ys;
  1.1160 +
  1.1161 +    fun mk_fresh2 xss [] = []
  1.1162 +      | mk_fresh2 xss ((p as (ys, _)) :: yss) = List.concat (map (fn y as (_, T) =>
  1.1163 +            map (fn (_, x as (_, U)) => HOLogic.mk_Trueprop
  1.1164 +              (fresh_const T U $ Free y $ Free x)) (rev xss @ yss)) ys) @
  1.1165 +          mk_fresh2 (p :: xss) yss;
  1.1166 +
  1.1167 +    fun make_ind_prem fsT f k T ((cname, cargs), idxs) =
  1.1168 +      let
  1.1169 +        val recs = List.filter is_rec_type cargs;
  1.1170 +        val Ts = map (typ_of_dtyp descr'' sorts) cargs;
  1.1171 +        val recTs' = map (typ_of_dtyp descr'' sorts) recs;
  1.1172 +        val tnames = Name.variant_list pnames (DatatypeProp.make_tnames Ts);
  1.1173 +        val rec_tnames = map fst (List.filter (is_rec_type o snd) (tnames ~~ cargs));
  1.1174 +        val frees = tnames ~~ Ts;
  1.1175 +        val frees' = partition_cargs idxs frees;
  1.1176 +        val z = (Name.variant tnames "z", fsT);
  1.1177 +
  1.1178 +        fun mk_prem ((dt, s), T) =
  1.1179 +          let
  1.1180 +            val (Us, U) = strip_type T;
  1.1181 +            val l = length Us
  1.1182 +          in list_all (z :: map (pair "x") Us, HOLogic.mk_Trueprop
  1.1183 +            (make_pred fsT (body_index dt) U $ Bound l $ app_bnds (Free (s, T)) l))
  1.1184 +          end;
  1.1185 +
  1.1186 +        val prems = map mk_prem (recs ~~ rec_tnames ~~ recTs');
  1.1187 +        val prems' = map (fn p as (_, T) => HOLogic.mk_Trueprop
  1.1188 +            (f T (Free p) (Free z))) (List.concat (map fst frees')) @
  1.1189 +          mk_fresh1 [] (List.concat (map fst frees')) @
  1.1190 +          mk_fresh2 [] frees'
  1.1191 +
  1.1192 +      in list_all_free (frees @ [z], Logic.list_implies (prems' @ prems,
  1.1193 +        HOLogic.mk_Trueprop (make_pred fsT k T $ Free z $
  1.1194 +          list_comb (Const (cname, Ts ---> T), map Free frees))))
  1.1195 +      end;
  1.1196 +
  1.1197 +    val ind_prems = List.concat (map (fn (((i, (_, _, constrs)), (_, idxss)), T) =>
  1.1198 +      map (make_ind_prem fsT (fn T => fn t => fn u =>
  1.1199 +        fresh_const T fsT $ t $ u) i T)
  1.1200 +          (constrs ~~ idxss)) (descr'' ~~ ndescr ~~ recTs));
  1.1201 +    val tnames = DatatypeProp.make_tnames recTs;
  1.1202 +    val zs = Name.variant_list tnames (replicate (length descr'') "z");
  1.1203 +    val ind_concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop "op &")
  1.1204 +      (map (fn ((((i, _), T), tname), z) =>
  1.1205 +        make_pred fsT i T $ Free (z, fsT) $ Free (tname, T))
  1.1206 +        (descr'' ~~ recTs ~~ tnames ~~ zs)));
  1.1207 +    val induct = Logic.list_implies (ind_prems, ind_concl);
  1.1208 +
  1.1209 +    val ind_prems' =
  1.1210 +      map (fn (_, f as Free (_, T)) => list_all_free ([("x", fsT')],
  1.1211 +        HOLogic.mk_Trueprop (Const ("Finite_Set.finite",
  1.1212 +          (snd (split_last (binder_types T)) --> HOLogic.boolT) -->
  1.1213 +            HOLogic.boolT) $ (f $ Free ("x", fsT'))))) fresh_fs @
  1.1214 +      List.concat (map (fn (((i, (_, _, constrs)), (_, idxss)), T) =>
  1.1215 +        map (make_ind_prem fsT' (fn T => fn t => fn u => HOLogic.Not $
  1.1216 +          HOLogic.mk_mem (t, the (AList.lookup op = fresh_fs T) $ u)) i T)
  1.1217 +            (constrs ~~ idxss)) (descr'' ~~ ndescr ~~ recTs));
  1.1218 +    val ind_concl' = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop "op &")
  1.1219 +      (map (fn ((((i, _), T), tname), z) =>
  1.1220 +        make_pred fsT' i T $ Free (z, fsT') $ Free (tname, T))
  1.1221 +        (descr'' ~~ recTs ~~ tnames ~~ zs)));
  1.1222 +    val induct' = Logic.list_implies (ind_prems', ind_concl');
  1.1223 +
  1.1224 +    val aux_ind_vars =
  1.1225 +      (DatatypeProp.indexify_names (replicate (length dt_atomTs) "pi") ~~
  1.1226 +       map mk_permT dt_atomTs) @ [("z", fsT')];
  1.1227 +    val aux_ind_Ts = rev (map snd aux_ind_vars);
  1.1228 +    val aux_ind_concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop "op &")
  1.1229 +      (map (fn (((i, _), T), tname) =>
  1.1230 +        HOLogic.list_all (aux_ind_vars, make_pred fsT' i T $ Bound 0 $
  1.1231 +          fold_rev (mk_perm aux_ind_Ts) (map Bound (length dt_atomTs downto 1))
  1.1232 +            (Free (tname, T))))
  1.1233 +        (descr'' ~~ recTs ~~ tnames)));
  1.1234 +
  1.1235 +    val fin_set_supp = map (fn s =>
  1.1236 +      at_inst_of thy9 s RS at_fin_set_supp) dt_atoms;
  1.1237 +    val fin_set_fresh = map (fn s =>
  1.1238 +      at_inst_of thy9 s RS at_fin_set_fresh) dt_atoms;
  1.1239 +    val pt1_atoms = map (fn Type (s, _) =>
  1.1240 +      PureThy.get_thm thy9 ("pt_" ^ Long_Name.base_name s ^ "1")) dt_atomTs;
  1.1241 +    val pt2_atoms = map (fn Type (s, _) =>
  1.1242 +      PureThy.get_thm thy9 ("pt_" ^ Long_Name.base_name s ^ "2") RS sym) dt_atomTs;
  1.1243 +    val exists_fresh' = PureThy.get_thms thy9 "exists_fresh'";
  1.1244 +    val fs_atoms = PureThy.get_thms thy9 "fin_supp";
  1.1245 +    val abs_supp = PureThy.get_thms thy9 "abs_supp";
  1.1246 +    val perm_fresh_fresh = PureThy.get_thms thy9 "perm_fresh_fresh";
  1.1247 +    val calc_atm = PureThy.get_thms thy9 "calc_atm";
  1.1248 +    val fresh_atm = PureThy.get_thms thy9 "fresh_atm";
  1.1249 +    val fresh_left = PureThy.get_thms thy9 "fresh_left";
  1.1250 +    val perm_swap = PureThy.get_thms thy9 "perm_swap";
  1.1251 +
  1.1252 +    fun obtain_fresh_name' ths ts T (freshs1, freshs2, ctxt) =
  1.1253 +      let
  1.1254 +        val p = foldr1 HOLogic.mk_prod (ts @ freshs1);
  1.1255 +        val ex = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop
  1.1256 +            (HOLogic.exists_const T $ Abs ("x", T,
  1.1257 +              fresh_const T (fastype_of p) $
  1.1258 +                Bound 0 $ p)))
  1.1259 +          (fn _ => EVERY
  1.1260 +            [resolve_tac exists_fresh' 1,
  1.1261 +             simp_tac (HOL_ss addsimps (supp_prod :: finite_Un :: fs_atoms @
  1.1262 +               fin_set_supp @ ths)) 1]);
  1.1263 +        val (([cx], ths), ctxt') = Obtain.result
  1.1264 +          (fn _ => EVERY
  1.1265 +            [etac exE 1,
  1.1266 +             full_simp_tac (HOL_ss addsimps (fresh_prod :: fresh_atm)) 1,
  1.1267 +             REPEAT (etac conjE 1)])
  1.1268 +          [ex] ctxt
  1.1269 +      in (freshs1 @ [term_of cx], freshs2 @ ths, ctxt') end;
  1.1270 +
  1.1271 +    fun fresh_fresh_inst thy a b =
  1.1272 +      let
  1.1273 +        val T = fastype_of a;
  1.1274 +        val SOME th = find_first (fn th => case prop_of th of
  1.1275 +            _ $ (_ $ (Const (_, Type (_, [U, _])) $ _ $ _)) $ _ => U = T
  1.1276 +          | _ => false) perm_fresh_fresh
  1.1277 +      in
  1.1278 +        Drule.instantiate' []
  1.1279 +          [SOME (cterm_of thy a), NONE, SOME (cterm_of thy b)] th
  1.1280 +      end;
  1.1281 +
  1.1282 +    val fs_cp_sort =
  1.1283 +      map (fs_class_of thy9) dt_atoms @
  1.1284 +      maps (fn s => map (cp_class_of thy9 s) (dt_atoms \ s)) dt_atoms;
  1.1285 +
  1.1286 +    (**********************************************************************
  1.1287 +      The subgoals occurring in the proof of induct_aux have the
  1.1288 +      following parameters:
  1.1289 +
  1.1290 +        x_1 ... x_k p_1 ... p_m z
  1.1291 +
  1.1292 +      where
  1.1293 +
  1.1294 +        x_i : constructor arguments (introduced by weak induction rule)
  1.1295 +        p_i : permutations (one for each atom type in the data type)
  1.1296 +        z   : freshness context
  1.1297 +    ***********************************************************************)
  1.1298 +
  1.1299 +    val _ = warning "proving strong induction theorem ...";
  1.1300 +
  1.1301 +    val induct_aux = Goal.prove_global thy9 []
  1.1302 +        (map (augment_sort thy9 fs_cp_sort) ind_prems')
  1.1303 +        (augment_sort thy9 fs_cp_sort ind_concl') (fn {prems, context} =>
  1.1304 +      let
  1.1305 +        val (prems1, prems2) = chop (length dt_atomTs) prems;
  1.1306 +        val ind_ss2 = HOL_ss addsimps
  1.1307 +          finite_Diff :: abs_fresh @ abs_supp @ fs_atoms;
  1.1308 +        val ind_ss1 = ind_ss2 addsimps fresh_left @ calc_atm @
  1.1309 +          fresh_atm @ rev_simps @ app_simps;
  1.1310 +        val ind_ss3 = HOL_ss addsimps abs_fun_eq1 ::
  1.1311 +          abs_perm @ calc_atm @ perm_swap;
  1.1312 +        val ind_ss4 = HOL_basic_ss addsimps fresh_left @ prems1 @
  1.1313 +          fin_set_fresh @ calc_atm;
  1.1314 +        val ind_ss5 = HOL_basic_ss addsimps pt1_atoms;
  1.1315 +        val ind_ss6 = HOL_basic_ss addsimps flat perm_simps';
  1.1316 +        val th = Goal.prove context [] []
  1.1317 +          (augment_sort thy9 fs_cp_sort aux_ind_concl)
  1.1318 +          (fn {context = context1, ...} =>
  1.1319 +             EVERY (indtac dt_induct tnames 1 ::
  1.1320 +               maps (fn ((_, (_, _, constrs)), (_, constrs')) =>
  1.1321 +                 map (fn ((cname, cargs), is) =>
  1.1322 +                   REPEAT (rtac allI 1) THEN
  1.1323 +                   SUBPROOF (fn {prems = iprems, params, concl,
  1.1324 +                       context = context2, ...} =>
  1.1325 +                     let
  1.1326 +                       val concl' = term_of concl;
  1.1327 +                       val _ $ (_ $ _ $ u) = concl';
  1.1328 +                       val U = fastype_of u;
  1.1329 +                       val (xs, params') =
  1.1330 +                         chop (length cargs) (map term_of params);
  1.1331 +                       val Ts = map fastype_of xs;
  1.1332 +                       val cnstr = Const (cname, Ts ---> U);
  1.1333 +                       val (pis, z) = split_last params';
  1.1334 +                       val mk_pi = fold_rev (mk_perm []) pis;
  1.1335 +                       val xs' = partition_cargs is xs;
  1.1336 +                       val xs'' = map (fn (ts, u) => (map mk_pi ts, mk_pi u)) xs';
  1.1337 +                       val ts = maps (fn (ts, u) => ts @ [u]) xs'';
  1.1338 +                       val (freshs1, freshs2, context3) = fold (fn t =>
  1.1339 +                         let val T = fastype_of t
  1.1340 +                         in obtain_fresh_name' prems1
  1.1341 +                           (the (AList.lookup op = fresh_fs T) $ z :: ts) T
  1.1342 +                         end) (maps fst xs') ([], [], context2);
  1.1343 +                       val freshs1' = unflat (map fst xs') freshs1;
  1.1344 +                       val freshs2' = map (Simplifier.simplify ind_ss4)
  1.1345 +                         (mk_not_sym freshs2);
  1.1346 +                       val ind_ss1' = ind_ss1 addsimps freshs2';
  1.1347 +                       val ind_ss3' = ind_ss3 addsimps freshs2';
  1.1348 +                       val rename_eq =
  1.1349 +                         if forall (null o fst) xs' then []
  1.1350 +                         else [Goal.prove context3 [] []
  1.1351 +                           (HOLogic.mk_Trueprop (HOLogic.mk_eq
  1.1352 +                             (list_comb (cnstr, ts),
  1.1353 +                              list_comb (cnstr, maps (fn ((bs, t), cs) =>
  1.1354 +                                cs @ [fold_rev (mk_perm []) (map perm_of_pair
  1.1355 +                                  (bs ~~ cs)) t]) (xs'' ~~ freshs1')))))
  1.1356 +                           (fn _ => EVERY
  1.1357 +                              (simp_tac (HOL_ss addsimps flat inject_thms) 1 ::
  1.1358 +                               REPEAT (FIRSTGOAL (rtac conjI)) ::
  1.1359 +                               maps (fn ((bs, t), cs) =>
  1.1360 +                                 if null bs then []
  1.1361 +                                 else rtac sym 1 :: maps (fn (b, c) =>
  1.1362 +                                   [rtac trans 1, rtac sym 1,
  1.1363 +                                    rtac (fresh_fresh_inst thy9 b c) 1,
  1.1364 +                                    simp_tac ind_ss1' 1,
  1.1365 +                                    simp_tac ind_ss2 1,
  1.1366 +                                    simp_tac ind_ss3' 1]) (bs ~~ cs))
  1.1367 +                                 (xs'' ~~ freshs1')))];
  1.1368 +                       val th = Goal.prove context3 [] [] concl' (fn _ => EVERY
  1.1369 +                         [simp_tac (ind_ss6 addsimps rename_eq) 1,
  1.1370 +                          cut_facts_tac iprems 1,
  1.1371 +                          (resolve_tac prems THEN_ALL_NEW
  1.1372 +                            SUBGOAL (fn (t, i) => case Logic.strip_assums_concl t of
  1.1373 +                                _ $ (Const ("Nominal.fresh", _) $ _ $ _) =>
  1.1374 +                                  simp_tac ind_ss1' i
  1.1375 +                              | _ $ (Const ("Not", _) $ _) =>
  1.1376 +                                  resolve_tac freshs2' i
  1.1377 +                              | _ => asm_simp_tac (HOL_basic_ss addsimps
  1.1378 +                                  pt2_atoms addsimprocs [perm_simproc]) i)) 1])
  1.1379 +                       val final = ProofContext.export context3 context2 [th]
  1.1380 +                     in
  1.1381 +                       resolve_tac final 1
  1.1382 +                     end) context1 1) (constrs ~~ constrs')) (descr'' ~~ ndescr)))
  1.1383 +      in
  1.1384 +        EVERY
  1.1385 +          [cut_facts_tac [th] 1,
  1.1386 +           REPEAT (eresolve_tac [conjE, @{thm allE_Nil}] 1),
  1.1387 +           REPEAT (etac allE 1),
  1.1388 +           REPEAT (TRY (rtac conjI 1) THEN asm_full_simp_tac ind_ss5 1)]
  1.1389 +      end);
  1.1390 +
  1.1391 +    val induct_aux' = Thm.instantiate ([],
  1.1392 +      map (fn (s, v as Var (_, T)) =>
  1.1393 +        (cterm_of thy9 v, cterm_of thy9 (Free (s, T))))
  1.1394 +          (pnames ~~ map head_of (HOLogic.dest_conj
  1.1395 +             (HOLogic.dest_Trueprop (concl_of induct_aux)))) @
  1.1396 +      map (fn (_, f) =>
  1.1397 +        let val f' = Logic.varify f
  1.1398 +        in (cterm_of thy9 f',
  1.1399 +          cterm_of thy9 (Const ("Nominal.supp", fastype_of f')))
  1.1400 +        end) fresh_fs) induct_aux;
  1.1401 +
  1.1402 +    val induct = Goal.prove_global thy9 []
  1.1403 +      (map (augment_sort thy9 fs_cp_sort) ind_prems)
  1.1404 +      (augment_sort thy9 fs_cp_sort ind_concl)
  1.1405 +      (fn {prems, ...} => EVERY
  1.1406 +         [rtac induct_aux' 1,
  1.1407 +          REPEAT (resolve_tac fs_atoms 1),
  1.1408 +          REPEAT ((resolve_tac prems THEN_ALL_NEW
  1.1409 +            (etac meta_spec ORELSE' full_simp_tac (HOL_basic_ss addsimps [fresh_def]))) 1)])
  1.1410 +
  1.1411 +    val (_, thy10) = thy9 |>
  1.1412 +      Sign.add_path big_name |>
  1.1413 +      PureThy.add_thms [((Binding.name "strong_induct'", induct_aux), [])] ||>>
  1.1414 +      PureThy.add_thms [((Binding.name "strong_induct", induct), [case_names_induct])] ||>>
  1.1415 +      PureThy.add_thmss [((Binding.name "strong_inducts", projections induct), [case_names_induct])];
  1.1416 +
  1.1417 +    (**** recursion combinator ****)
  1.1418 +
  1.1419 +    val _ = warning "defining recursion combinator ...";
  1.1420 +
  1.1421 +    val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
  1.1422 +
  1.1423 +    val (rec_result_Ts', rec_fn_Ts') = DatatypeProp.make_primrec_Ts descr' sorts used;
  1.1424 +
  1.1425 +    val rec_sort = if null dt_atomTs then HOLogic.typeS else
  1.1426 +      Sign.certify_sort thy10 pt_cp_sort;
  1.1427 +
  1.1428 +    val rec_result_Ts = map (fn TFree (s, _) => TFree (s, rec_sort)) rec_result_Ts';
  1.1429 +    val rec_fn_Ts = map (typ_subst_atomic (rec_result_Ts' ~~ rec_result_Ts)) rec_fn_Ts';
  1.1430 +
  1.1431 +    val rec_set_Ts = map (fn (T1, T2) =>
  1.1432 +      rec_fn_Ts @ [T1, T2] ---> HOLogic.boolT) (recTs ~~ rec_result_Ts);
  1.1433 +
  1.1434 +    val big_rec_name = big_name ^ "_rec_set";
  1.1435 +    val rec_set_names' =
  1.1436 +      if length descr'' = 1 then [big_rec_name] else
  1.1437 +        map ((curry (op ^) (big_rec_name ^ "_")) o string_of_int)
  1.1438 +          (1 upto (length descr''));
  1.1439 +    val rec_set_names =  map (Sign.full_bname thy10) rec_set_names';
  1.1440 +
  1.1441 +    val rec_fns = map (uncurry (mk_Free "f"))
  1.1442 +      (rec_fn_Ts ~~ (1 upto (length rec_fn_Ts)));
  1.1443 +    val rec_sets' = map (fn c => list_comb (Free c, rec_fns))
  1.1444 +      (rec_set_names' ~~ rec_set_Ts);
  1.1445 +    val rec_sets = map (fn c => list_comb (Const c, rec_fns))
  1.1446 +      (rec_set_names ~~ rec_set_Ts);
  1.1447 +
  1.1448 +    (* introduction rules for graph of recursion function *)
  1.1449 +
  1.1450 +    val rec_preds = map (fn (a, T) =>
  1.1451 +      Free (a, T --> HOLogic.boolT)) (pnames ~~ rec_result_Ts);
  1.1452 +
  1.1453 +    fun mk_fresh3 rs [] = []
  1.1454 +      | mk_fresh3 rs ((p as (ys, z)) :: yss) = List.concat (map (fn y as (_, T) =>
  1.1455 +            List.mapPartial (fn ((_, (_, x)), r as (_, U)) => if z = x then NONE
  1.1456 +              else SOME (HOLogic.mk_Trueprop
  1.1457 +                (fresh_const T U $ Free y $ Free r))) rs) ys) @
  1.1458 +          mk_fresh3 rs yss;
  1.1459 +
  1.1460 +    (* FIXME: avoid collisions with other variable names? *)
  1.1461 +    val rec_ctxt = Free ("z", fsT');
  1.1462 +
  1.1463 +    fun make_rec_intr T p rec_set ((rec_intr_ts, rec_prems, rec_prems',
  1.1464 +          rec_eq_prems, l), ((cname, cargs), idxs)) =
  1.1465 +      let
  1.1466 +        val Ts = map (typ_of_dtyp descr'' sorts) cargs;
  1.1467 +        val frees = map (fn i => "x" ^ string_of_int i) (1 upto length Ts) ~~ Ts;
  1.1468 +        val frees' = partition_cargs idxs frees;
  1.1469 +        val binders = List.concat (map fst frees');
  1.1470 +        val atomTs = distinct op = (maps (map snd o fst) frees');
  1.1471 +        val recs = List.mapPartial
  1.1472 +          (fn ((_, DtRec i), p) => SOME (i, p) | _ => NONE)
  1.1473 +          (partition_cargs idxs cargs ~~ frees');
  1.1474 +        val frees'' = map (fn i => "y" ^ string_of_int i) (1 upto length recs) ~~
  1.1475 +          map (fn (i, _) => List.nth (rec_result_Ts, i)) recs;
  1.1476 +        val prems1 = map (fn ((i, (_, x)), y) => HOLogic.mk_Trueprop
  1.1477 +          (List.nth (rec_sets', i) $ Free x $ Free y)) (recs ~~ frees'');
  1.1478 +        val prems2 =
  1.1479 +          map (fn f => map (fn p as (_, T) => HOLogic.mk_Trueprop
  1.1480 +            (fresh_const T (fastype_of f) $ Free p $ f)) binders) rec_fns;
  1.1481 +        val prems3 = mk_fresh1 [] binders @ mk_fresh2 [] frees';
  1.1482 +        val prems4 = map (fn ((i, _), y) =>
  1.1483 +          HOLogic.mk_Trueprop (List.nth (rec_preds, i) $ Free y)) (recs ~~ frees'');
  1.1484 +        val prems5 = mk_fresh3 (recs ~~ frees'') frees';
  1.1485 +        val prems6 = maps (fn aT => map (fn y as (_, T) => HOLogic.mk_Trueprop
  1.1486 +          (Const ("Finite_Set.finite", HOLogic.mk_setT aT --> HOLogic.boolT) $
  1.1487 +             (Const ("Nominal.supp", T --> HOLogic.mk_setT aT) $ Free y)))
  1.1488 +               frees'') atomTs;
  1.1489 +        val prems7 = map (fn x as (_, T) => HOLogic.mk_Trueprop
  1.1490 +          (fresh_const T fsT' $ Free x $ rec_ctxt)) binders;
  1.1491 +        val result = list_comb (List.nth (rec_fns, l), map Free (frees @ frees''));
  1.1492 +        val result_freshs = map (fn p as (_, T) =>
  1.1493 +          fresh_const T (fastype_of result) $ Free p $ result) binders;
  1.1494 +        val P = HOLogic.mk_Trueprop (p $ result)
  1.1495 +      in
  1.1496 +        (rec_intr_ts @ [Logic.list_implies (List.concat prems2 @ prems3 @ prems1,
  1.1497 +           HOLogic.mk_Trueprop (rec_set $
  1.1498 +             list_comb (Const (cname, Ts ---> T), map Free frees) $ result))],
  1.1499 +         rec_prems @ [list_all_free (frees @ frees'', Logic.list_implies (prems4, P))],
  1.1500 +         rec_prems' @ map (fn fr => list_all_free (frees @ frees'',
  1.1501 +           Logic.list_implies (List.nth (prems2, l) @ prems3 @ prems5 @ prems7 @ prems6 @ [P],
  1.1502 +             HOLogic.mk_Trueprop fr))) result_freshs,
  1.1503 +         rec_eq_prems @ [List.concat prems2 @ prems3],
  1.1504 +         l + 1)
  1.1505 +      end;
  1.1506 +
  1.1507 +    val (rec_intr_ts, rec_prems, rec_prems', rec_eq_prems, _) =
  1.1508 +      Library.foldl (fn (x, ((((d, d'), T), p), rec_set)) =>
  1.1509 +        Library.foldl (make_rec_intr T p rec_set) (x, #3 (snd d) ~~ snd d'))
  1.1510 +          (([], [], [], [], 0), descr'' ~~ ndescr ~~ recTs ~~ rec_preds ~~ rec_sets');
  1.1511 +
  1.1512 +    val ({intrs = rec_intrs, elims = rec_elims, raw_induct = rec_induct, ...}, thy11) =
  1.1513 +      thy10 |>
  1.1514 +        Inductive.add_inductive_global (serial_string ())
  1.1515 +          {quiet_mode = #quiet config, verbose = false, kind = Thm.internalK,
  1.1516 +           alt_name = Binding.name big_rec_name, coind = false, no_elim = false, no_ind = false,
  1.1517 +           skip_mono = true, fork_mono = false}
  1.1518 +          (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
  1.1519 +          (map dest_Free rec_fns)
  1.1520 +          (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) [] ||>
  1.1521 +      PureThy.hide_fact true (Long_Name.append (Sign.full_bname thy10 big_rec_name) "induct");
  1.1522 +
  1.1523 +    (** equivariance **)
  1.1524 +
  1.1525 +    val fresh_bij = PureThy.get_thms thy11 "fresh_bij";
  1.1526 +    val perm_bij = PureThy.get_thms thy11 "perm_bij";
  1.1527 +
  1.1528 +    val (rec_equiv_thms, rec_equiv_thms') = ListPair.unzip (map (fn aT =>
  1.1529 +      let
  1.1530 +        val permT = mk_permT aT;
  1.1531 +        val pi = Free ("pi", permT);
  1.1532 +        val rec_fns_pi = map (mk_perm [] pi o uncurry (mk_Free "f"))
  1.1533 +          (rec_fn_Ts ~~ (1 upto (length rec_fn_Ts)));
  1.1534 +        val rec_sets_pi = map (fn c => list_comb (Const c, rec_fns_pi))
  1.1535 +          (rec_set_names ~~ rec_set_Ts);
  1.1536 +        val ps = map (fn ((((T, U), R), R'), i) =>
  1.1537 +          let
  1.1538 +            val x = Free ("x" ^ string_of_int i, T);
  1.1539 +            val y = Free ("y" ^ string_of_int i, U)
  1.1540 +          in
  1.1541 +            (R $ x $ y, R' $ mk_perm [] pi x $ mk_perm [] pi y)
  1.1542 +          end) (recTs ~~ rec_result_Ts ~~ rec_sets ~~ rec_sets_pi ~~ (1 upto length recTs));
  1.1543 +        val ths = map (fn th => standard (th RS mp)) (split_conj_thm
  1.1544 +          (Goal.prove_global thy11 [] []
  1.1545 +            (augment_sort thy1 pt_cp_sort
  1.1546 +              (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map HOLogic.mk_imp ps))))
  1.1547 +            (fn _ => rtac rec_induct 1 THEN REPEAT
  1.1548 +               (simp_tac (Simplifier.theory_context thy11 HOL_basic_ss
  1.1549 +                  addsimps flat perm_simps'
  1.1550 +                  addsimprocs [NominalPermeq.perm_simproc_app]) 1 THEN
  1.1551 +                (resolve_tac rec_intrs THEN_ALL_NEW
  1.1552 +                 asm_simp_tac (HOL_ss addsimps (fresh_bij @ perm_bij))) 1))))
  1.1553 +        val ths' = map (fn ((P, Q), th) =>
  1.1554 +          Goal.prove_global thy11 [] []
  1.1555 +            (augment_sort thy1 pt_cp_sort
  1.1556 +              (Logic.mk_implies (HOLogic.mk_Trueprop Q, HOLogic.mk_Trueprop P)))
  1.1557 +            (fn _ => dtac (Thm.instantiate ([],
  1.1558 +                 [(cterm_of thy11 (Var (("pi", 0), permT)),
  1.1559 +                   cterm_of thy11 (Const ("List.rev", permT --> permT) $ pi))]) th) 1 THEN
  1.1560 +               NominalPermeq.perm_simp_tac HOL_ss 1)) (ps ~~ ths)
  1.1561 +      in (ths, ths') end) dt_atomTs);
  1.1562 +
  1.1563 +    (** finite support **)
  1.1564 +
  1.1565 +    val rec_fin_supp_thms = map (fn aT =>
  1.1566 +      let
  1.1567 +        val name = Long_Name.base_name (fst (dest_Type aT));
  1.1568 +        val fs_name = PureThy.get_thm thy11 ("fs_" ^ name ^ "1");
  1.1569 +        val aset = HOLogic.mk_setT aT;
  1.1570 +        val finite = Const ("Finite_Set.finite", aset --> HOLogic.boolT);
  1.1571 +        val fins = map (fn (f, T) => HOLogic.mk_Trueprop
  1.1572 +          (finite $ (Const ("Nominal.supp", T --> aset) $ f)))
  1.1573 +            (rec_fns ~~ rec_fn_Ts)
  1.1574 +      in
  1.1575 +        map (fn th => standard (th RS mp)) (split_conj_thm
  1.1576 +          (Goal.prove_global thy11 []
  1.1577 +            (map (augment_sort thy11 fs_cp_sort) fins)
  1.1578 +            (augment_sort thy11 fs_cp_sort
  1.1579 +              (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
  1.1580 +                (map (fn (((T, U), R), i) =>
  1.1581 +                   let
  1.1582 +                     val x = Free ("x" ^ string_of_int i, T);
  1.1583 +                     val y = Free ("y" ^ string_of_int i, U)
  1.1584 +                   in
  1.1585 +                     HOLogic.mk_imp (R $ x $ y,
  1.1586 +                       finite $ (Const ("Nominal.supp", U --> aset) $ y))
  1.1587 +                   end) (recTs ~~ rec_result_Ts ~~ rec_sets ~~
  1.1588 +                     (1 upto length recTs))))))
  1.1589 +            (fn {prems = fins, ...} =>
  1.1590 +              (rtac rec_induct THEN_ALL_NEW cut_facts_tac fins) 1 THEN REPEAT
  1.1591 +               (NominalPermeq.finite_guess_tac (HOL_ss addsimps [fs_name]) 1))))
  1.1592 +      end) dt_atomTs;
  1.1593 +
  1.1594 +    (** freshness **)
  1.1595 +
  1.1596 +    val finite_premss = map (fn aT =>
  1.1597 +      map (fn (f, T) => HOLogic.mk_Trueprop
  1.1598 +        (Const ("Finite_Set.finite", HOLogic.mk_setT aT --> HOLogic.boolT) $
  1.1599 +           (Const ("Nominal.supp", T --> HOLogic.mk_setT aT) $ f)))
  1.1600 +           (rec_fns ~~ rec_fn_Ts)) dt_atomTs;
  1.1601 +
  1.1602 +    val rec_fns' = map (augment_sort thy11 fs_cp_sort) rec_fns;
  1.1603 +
  1.1604 +    val rec_fresh_thms = map (fn ((aT, eqvt_ths), finite_prems) =>
  1.1605 +      let
  1.1606 +        val name = Long_Name.base_name (fst (dest_Type aT));
  1.1607 +        val fs_name = PureThy.get_thm thy11 ("fs_" ^ name ^ "1");
  1.1608 +        val a = Free ("a", aT);
  1.1609 +        val freshs = map (fn (f, fT) => HOLogic.mk_Trueprop
  1.1610 +          (fresh_const aT fT $ a $ f)) (rec_fns ~~ rec_fn_Ts)
  1.1611 +      in
  1.1612 +        map (fn (((T, U), R), eqvt_th) =>
  1.1613 +          let
  1.1614 +            val x = Free ("x", augment_sort_typ thy11 fs_cp_sort T);
  1.1615 +            val y = Free ("y", U);
  1.1616 +            val y' = Free ("y'", U)
  1.1617 +          in
  1.1618 +            standard (Goal.prove (ProofContext.init thy11) []
  1.1619 +              (map (augment_sort thy11 fs_cp_sort)
  1.1620 +                (finite_prems @
  1.1621 +                   [HOLogic.mk_Trueprop (R $ x $ y),
  1.1622 +                    HOLogic.mk_Trueprop (HOLogic.mk_all ("y'", U,
  1.1623 +                      HOLogic.mk_imp (R $ x $ y', HOLogic.mk_eq (y', y)))),
  1.1624 +                    HOLogic.mk_Trueprop (fresh_const aT T $ a $ x)] @
  1.1625 +                 freshs))
  1.1626 +              (HOLogic.mk_Trueprop (fresh_const aT U $ a $ y))
  1.1627 +              (fn {prems, context} =>
  1.1628 +                 let
  1.1629 +                   val (finite_prems, rec_prem :: unique_prem ::
  1.1630 +                     fresh_prems) = chop (length finite_prems) prems;
  1.1631 +                   val unique_prem' = unique_prem RS spec RS mp;
  1.1632 +                   val unique = [unique_prem', unique_prem' RS sym] MRS trans;
  1.1633 +                   val _ $ (_ $ (_ $ S $ _)) $ _ = prop_of supports_fresh;
  1.1634 +                   val tuple = foldr1 HOLogic.mk_prod (x :: rec_fns')
  1.1635 +                 in EVERY
  1.1636 +                   [rtac (Drule.cterm_instantiate
  1.1637 +                      [(cterm_of thy11 S,
  1.1638 +                        cterm_of thy11 (Const ("Nominal.supp",
  1.1639 +                          fastype_of tuple --> HOLogic.mk_setT aT) $ tuple))]
  1.1640 +                      supports_fresh) 1,
  1.1641 +                    simp_tac (HOL_basic_ss addsimps
  1.1642 +                      [supports_def, symmetric fresh_def, fresh_prod]) 1,
  1.1643 +                    REPEAT_DETERM (resolve_tac [allI, impI] 1),
  1.1644 +                    REPEAT_DETERM (etac conjE 1),
  1.1645 +                    rtac unique 1,
  1.1646 +                    SUBPROOF (fn {prems = prems', params = [a, b], ...} => EVERY
  1.1647 +                      [cut_facts_tac [rec_prem] 1,
  1.1648 +                       rtac (Thm.instantiate ([],
  1.1649 +                         [(cterm_of thy11 (Var (("pi", 0), mk_permT aT)),
  1.1650 +                           cterm_of thy11 (perm_of_pair (term_of a, term_of b)))]) eqvt_th) 1,
  1.1651 +                       asm_simp_tac (HOL_ss addsimps
  1.1652 +                         (prems' @ perm_swap @ perm_fresh_fresh)) 1]) context 1,
  1.1653 +                    rtac rec_prem 1,
  1.1654 +                    simp_tac (HOL_ss addsimps (fs_name ::
  1.1655 +                      supp_prod :: finite_Un :: finite_prems)) 1,
  1.1656 +                    simp_tac (HOL_ss addsimps (symmetric fresh_def ::
  1.1657 +                      fresh_prod :: fresh_prems)) 1]
  1.1658 +                 end))
  1.1659 +          end) (recTs ~~ rec_result_Ts ~~ rec_sets ~~ eqvt_ths)
  1.1660 +      end) (dt_atomTs ~~ rec_equiv_thms' ~~ finite_premss);
  1.1661 +
  1.1662 +    (** uniqueness **)
  1.1663 +
  1.1664 +    val fun_tuple = foldr1 HOLogic.mk_prod (rec_ctxt :: rec_fns);
  1.1665 +    val fun_tupleT = fastype_of fun_tuple;
  1.1666 +    val rec_unique_frees =
  1.1667 +      DatatypeProp.indexify_names (replicate (length recTs) "x") ~~ recTs;
  1.1668 +    val rec_unique_frees'' = map (fn (s, T) => (s ^ "'", T)) rec_unique_frees;
  1.1669 +    val rec_unique_frees' =
  1.1670 +      DatatypeProp.indexify_names (replicate (length recTs) "y") ~~ rec_result_Ts;
  1.1671 +    val rec_unique_concls = map (fn ((x, U), R) =>
  1.1672 +        Const ("Ex1", (U --> HOLogic.boolT) --> HOLogic.boolT) $
  1.1673 +          Abs ("y", U, R $ Free x $ Bound 0))
  1.1674 +      (rec_unique_frees ~~ rec_result_Ts ~~ rec_sets);
  1.1675 +
  1.1676 +    val induct_aux_rec = Drule.cterm_instantiate
  1.1677 +      (map (pairself (cterm_of thy11) o apsnd (augment_sort thy11 fs_cp_sort))
  1.1678 +         (map (fn (aT, f) => (Logic.varify f, Abs ("z", HOLogic.unitT,
  1.1679 +            Const ("Nominal.supp", fun_tupleT --> HOLogic.mk_setT aT) $ fun_tuple)))
  1.1680 +              fresh_fs @
  1.1681 +          map (fn (((P, T), (x, U)), Q) =>
  1.1682 +           (Var ((P, 0), Logic.varifyT (fsT' --> T --> HOLogic.boolT)),
  1.1683 +            Abs ("z", HOLogic.unitT, absfree (x, U, Q))))
  1.1684 +              (pnames ~~ recTs ~~ rec_unique_frees ~~ rec_unique_concls) @
  1.1685 +          map (fn (s, T) => (Var ((s, 0), Logic.varifyT T), Free (s, T)))
  1.1686 +            rec_unique_frees)) induct_aux;
  1.1687 +
  1.1688 +    fun obtain_fresh_name vs ths rec_fin_supp T (freshs1, freshs2, ctxt) =
  1.1689 +      let
  1.1690 +        val p = foldr1 HOLogic.mk_prod (vs @ freshs1);
  1.1691 +        val ex = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop
  1.1692 +            (HOLogic.exists_const T $ Abs ("x", T,
  1.1693 +              fresh_const T (fastype_of p) $ Bound 0 $ p)))
  1.1694 +          (fn _ => EVERY
  1.1695 +            [cut_facts_tac ths 1,
  1.1696 +             REPEAT_DETERM (dresolve_tac (the (AList.lookup op = rec_fin_supp T)) 1),
  1.1697 +             resolve_tac exists_fresh' 1,
  1.1698 +             asm_simp_tac (HOL_ss addsimps (supp_prod :: finite_Un :: fs_atoms)) 1]);
  1.1699 +        val (([cx], ths), ctxt') = Obtain.result
  1.1700 +          (fn _ => EVERY
  1.1701 +            [etac exE 1,
  1.1702 +             full_simp_tac (HOL_ss addsimps (fresh_prod :: fresh_atm)) 1,
  1.1703 +             REPEAT (etac conjE 1)])
  1.1704 +          [ex] ctxt
  1.1705 +      in (freshs1 @ [term_of cx], freshs2 @ ths, ctxt') end;
  1.1706 +
  1.1707 +    val finite_ctxt_prems = map (fn aT =>
  1.1708 +      HOLogic.mk_Trueprop
  1.1709 +        (Const ("Finite_Set.finite", HOLogic.mk_setT aT --> HOLogic.boolT) $
  1.1710 +           (Const ("Nominal.supp", fsT' --> HOLogic.mk_setT aT) $ rec_ctxt))) dt_atomTs;
  1.1711 +
  1.1712 +    val rec_unique_thms = split_conj_thm (Goal.prove
  1.1713 +      (ProofContext.init thy11) (map fst rec_unique_frees)
  1.1714 +      (map (augment_sort thy11 fs_cp_sort)
  1.1715 +        (List.concat finite_premss @ finite_ctxt_prems @ rec_prems @ rec_prems'))
  1.1716 +      (augment_sort thy11 fs_cp_sort
  1.1717 +        (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj rec_unique_concls)))
  1.1718 +      (fn {prems, context} =>
  1.1719 +         let
  1.1720 +           val k = length rec_fns;
  1.1721 +           val (finite_thss, ths1) = fold_map (fn T => fn xs =>
  1.1722 +             apfst (pair T) (chop k xs)) dt_atomTs prems;
  1.1723 +           val (finite_ctxt_ths, ths2) = chop (length dt_atomTs) ths1;
  1.1724 +           val (P_ind_ths, fcbs) = chop k ths2;
  1.1725 +           val P_ths = map (fn th => th RS mp) (split_conj_thm
  1.1726 +             (Goal.prove context
  1.1727 +               (map fst (rec_unique_frees'' @ rec_unique_frees')) []
  1.1728 +               (augment_sort thy11 fs_cp_sort
  1.1729 +                 (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
  1.1730 +                    (map (fn (((x, y), S), P) => HOLogic.mk_imp
  1.1731 +                      (S $ Free x $ Free y, P $ (Free y)))
  1.1732 +                        (rec_unique_frees'' ~~ rec_unique_frees' ~~
  1.1733 +                           rec_sets ~~ rec_preds)))))
  1.1734 +               (fn _ =>
  1.1735 +                  rtac rec_induct 1 THEN
  1.1736 +                  REPEAT ((resolve_tac P_ind_ths THEN_ALL_NEW assume_tac) 1))));
  1.1737 +           val rec_fin_supp_thms' = map
  1.1738 +             (fn (ths, (T, fin_ths)) => (T, map (curry op MRS fin_ths) ths))
  1.1739 +             (rec_fin_supp_thms ~~ finite_thss);
  1.1740 +         in EVERY
  1.1741 +           ([rtac induct_aux_rec 1] @
  1.1742 +            maps (fn ((_, finite_ths), finite_th) =>
  1.1743 +              [cut_facts_tac (finite_th :: finite_ths) 1,
  1.1744 +               asm_simp_tac (HOL_ss addsimps [supp_prod, finite_Un]) 1])
  1.1745 +                (finite_thss ~~ finite_ctxt_ths) @
  1.1746 +            maps (fn ((_, idxss), elim) => maps (fn idxs =>
  1.1747 +              [full_simp_tac (HOL_ss addsimps [symmetric fresh_def, supp_prod, Un_iff]) 1,
  1.1748 +               REPEAT_DETERM (eresolve_tac [conjE, ex1E] 1),
  1.1749 +               rtac ex1I 1,
  1.1750 +               (resolve_tac rec_intrs THEN_ALL_NEW atac) 1,
  1.1751 +               rotate_tac ~1 1,
  1.1752 +               ((DETERM o etac elim) THEN_ALL_NEW full_simp_tac
  1.1753 +                  (HOL_ss addsimps List.concat distinct_thms)) 1] @
  1.1754 +               (if null idxs then [] else [hyp_subst_tac 1,
  1.1755 +                SUBPROOF (fn {asms, concl, prems = prems', params, context = context', ...} =>
  1.1756 +                  let
  1.1757 +                    val SOME prem = find_first (can (HOLogic.dest_eq o
  1.1758 +                      HOLogic.dest_Trueprop o prop_of)) prems';
  1.1759 +                    val _ $ (_ $ lhs $ rhs) = prop_of prem;
  1.1760 +                    val _ $ (_ $ lhs' $ rhs') = term_of concl;
  1.1761 +                    val rT = fastype_of lhs';
  1.1762 +                    val (c, cargsl) = strip_comb lhs;
  1.1763 +                    val cargsl' = partition_cargs idxs cargsl;
  1.1764 +                    val boundsl = List.concat (map fst cargsl');
  1.1765 +                    val (_, cargsr) = strip_comb rhs;
  1.1766 +                    val cargsr' = partition_cargs idxs cargsr;
  1.1767 +                    val boundsr = List.concat (map fst cargsr');
  1.1768 +                    val (params1, _ :: params2) =
  1.1769 +                      chop (length params div 2) (map term_of params);
  1.1770 +                    val params' = params1 @ params2;
  1.1771 +                    val rec_prems = filter (fn th => case prop_of th of
  1.1772 +                        _ $ p => (case head_of p of
  1.1773 +                          Const (s, _) => s mem rec_set_names
  1.1774 +                        | _ => false)
  1.1775 +                      | _ => false) prems';
  1.1776 +                    val fresh_prems = filter (fn th => case prop_of th of
  1.1777 +                        _ $ (Const ("Nominal.fresh", _) $ _ $ _) => true
  1.1778 +                      | _ $ (Const ("Not", _) $ _) => true
  1.1779 +                      | _ => false) prems';
  1.1780 +                    val Ts = map fastype_of boundsl;
  1.1781 +
  1.1782 +                    val _ = warning "step 1: obtaining fresh names";
  1.1783 +                    val (freshs1, freshs2, context'') = fold
  1.1784 +                      (obtain_fresh_name (rec_ctxt :: rec_fns' @ params')
  1.1785 +                         (List.concat (map snd finite_thss) @
  1.1786 +                            finite_ctxt_ths @ rec_prems)
  1.1787 +                         rec_fin_supp_thms')
  1.1788 +                      Ts ([], [], context');
  1.1789 +                    val pi1 = map perm_of_pair (boundsl ~~ freshs1);
  1.1790 +                    val rpi1 = rev pi1;
  1.1791 +                    val pi2 = map perm_of_pair (boundsr ~~ freshs1);
  1.1792 +                    val rpi2 = rev pi2;
  1.1793 +
  1.1794 +                    val fresh_prems' = mk_not_sym fresh_prems;
  1.1795 +                    val freshs2' = mk_not_sym freshs2;
  1.1796 +
  1.1797 +                    (** as, bs, cs # K as ts, K bs us **)
  1.1798 +                    val _ = warning "step 2: as, bs, cs # K as ts, K bs us";
  1.1799 +                    val prove_fresh_ss = HOL_ss addsimps
  1.1800 +                      (finite_Diff :: List.concat fresh_thms @
  1.1801 +                       fs_atoms @ abs_fresh @ abs_supp @ fresh_atm);
  1.1802 +                    (* FIXME: avoid asm_full_simp_tac ? *)
  1.1803 +                    fun prove_fresh ths y x = Goal.prove context'' [] []
  1.1804 +                      (HOLogic.mk_Trueprop (fresh_const
  1.1805 +                         (fastype_of x) (fastype_of y) $ x $ y))
  1.1806 +                      (fn _ => cut_facts_tac ths 1 THEN asm_full_simp_tac prove_fresh_ss 1);
  1.1807 +                    val constr_fresh_thms =
  1.1808 +                      map (prove_fresh fresh_prems lhs) boundsl @
  1.1809 +                      map (prove_fresh fresh_prems rhs) boundsr @
  1.1810 +                      map (prove_fresh freshs2 lhs) freshs1 @
  1.1811 +                      map (prove_fresh freshs2 rhs) freshs1;
  1.1812 +
  1.1813 +                    (** pi1 o (K as ts) = pi2 o (K bs us) **)
  1.1814 +                    val _ = warning "step 3: pi1 o (K as ts) = pi2 o (K bs us)";
  1.1815 +                    val pi1_pi2_eq = Goal.prove context'' [] []
  1.1816 +                      (HOLogic.mk_Trueprop (HOLogic.mk_eq
  1.1817 +                        (fold_rev (mk_perm []) pi1 lhs, fold_rev (mk_perm []) pi2 rhs)))
  1.1818 +                      (fn _ => EVERY
  1.1819 +                         [cut_facts_tac constr_fresh_thms 1,
  1.1820 +                          asm_simp_tac (HOL_basic_ss addsimps perm_fresh_fresh) 1,
  1.1821 +                          rtac prem 1]);
  1.1822 +
  1.1823 +                    (** pi1 o ts = pi2 o us **)
  1.1824 +                    val _ = warning "step 4: pi1 o ts = pi2 o us";
  1.1825 +                    val pi1_pi2_eqs = map (fn (t, u) =>
  1.1826 +                      Goal.prove context'' [] []
  1.1827 +                        (HOLogic.mk_Trueprop (HOLogic.mk_eq
  1.1828 +                          (fold_rev (mk_perm []) pi1 t, fold_rev (mk_perm []) pi2 u)))
  1.1829 +                        (fn _ => EVERY
  1.1830 +                           [cut_facts_tac [pi1_pi2_eq] 1,
  1.1831 +                            asm_full_simp_tac (HOL_ss addsimps
  1.1832 +                              (calc_atm @ List.concat perm_simps' @
  1.1833 +                               fresh_prems' @ freshs2' @ abs_perm @
  1.1834 +                               alpha @ List.concat inject_thms)) 1]))
  1.1835 +                        (map snd cargsl' ~~ map snd cargsr');
  1.1836 +
  1.1837 +                    (** pi1^-1 o pi2 o us = ts **)
  1.1838 +                    val _ = warning "step 5: pi1^-1 o pi2 o us = ts";
  1.1839 +                    val rpi1_pi2_eqs = map (fn ((t, u), eq) =>
  1.1840 +                      Goal.prove context'' [] []
  1.1841 +                        (HOLogic.mk_Trueprop (HOLogic.mk_eq
  1.1842 +                          (fold_rev (mk_perm []) (rpi1 @ pi2) u, t)))
  1.1843 +                        (fn _ => simp_tac (HOL_ss addsimps
  1.1844 +                           ((eq RS sym) :: perm_swap)) 1))
  1.1845 +                        (map snd cargsl' ~~ map snd cargsr' ~~ pi1_pi2_eqs);
  1.1846 +
  1.1847 +                    val (rec_prems1, rec_prems2) =
  1.1848 +                      chop (length rec_prems div 2) rec_prems;
  1.1849 +
  1.1850 +                    (** (ts, pi1^-1 o pi2 o vs) in rec_set **)
  1.1851 +                    val _ = warning "step 6: (ts, pi1^-1 o pi2 o vs) in rec_set";
  1.1852 +                    val rec_prems' = map (fn th =>
  1.1853 +                      let
  1.1854 +                        val _ $ (S $ x $ y) = prop_of th;
  1.1855 +                        val Const (s, _) = head_of S;
  1.1856 +                        val k = find_index (equal s) rec_set_names;
  1.1857 +                        val pi = rpi1 @ pi2;
  1.1858 +                        fun mk_pi z = fold_rev (mk_perm []) pi z;
  1.1859 +                        fun eqvt_tac p =
  1.1860 +                          let
  1.1861 +                            val U as Type (_, [Type (_, [T, _])]) = fastype_of p;
  1.1862 +                            val l = find_index (equal T) dt_atomTs;
  1.1863 +                            val th = List.nth (List.nth (rec_equiv_thms', l), k);
  1.1864 +                            val th' = Thm.instantiate ([],
  1.1865 +                              [(cterm_of thy11 (Var (("pi", 0), U)),
  1.1866 +                                cterm_of thy11 p)]) th;
  1.1867 +                          in rtac th' 1 end;
  1.1868 +                        val th' = Goal.prove context'' [] []
  1.1869 +                          (HOLogic.mk_Trueprop (S $ mk_pi x $ mk_pi y))
  1.1870 +                          (fn _ => EVERY
  1.1871 +                             (map eqvt_tac pi @
  1.1872 +                              [simp_tac (HOL_ss addsimps (fresh_prems' @ freshs2' @
  1.1873 +                                 perm_swap @ perm_fresh_fresh)) 1,
  1.1874 +                               rtac th 1]))
  1.1875 +                      in
  1.1876 +                        Simplifier.simplify
  1.1877 +                          (HOL_basic_ss addsimps rpi1_pi2_eqs) th'
  1.1878 +                      end) rec_prems2;
  1.1879 +
  1.1880 +                    val ihs = filter (fn th => case prop_of th of
  1.1881 +                      _ $ (Const ("All", _) $ _) => true | _ => false) prems';
  1.1882 +
  1.1883 +                    (** pi1 o rs = pi2 o vs , rs = pi1^-1 o pi2 o vs **)
  1.1884 +                    val _ = warning "step 7: pi1 o rs = pi2 o vs , rs = pi1^-1 o pi2 o vs";
  1.1885 +                    val rec_eqns = map (fn (th, ih) =>
  1.1886 +                      let
  1.1887 +                        val th' = th RS (ih RS spec RS mp) RS sym;
  1.1888 +                        val _ $ (_ $ lhs $ rhs) = prop_of th';
  1.1889 +                        fun strip_perm (_ $ _ $ t) = strip_perm t
  1.1890 +                          | strip_perm t = t;
  1.1891 +                      in
  1.1892 +                        Goal.prove context'' [] []
  1.1893 +                           (HOLogic.mk_Trueprop (HOLogic.mk_eq
  1.1894 +                              (fold_rev (mk_perm []) pi1 lhs,
  1.1895 +                               fold_rev (mk_perm []) pi2 (strip_perm rhs))))
  1.1896 +                           (fn _ => simp_tac (HOL_basic_ss addsimps
  1.1897 +                              (th' :: perm_swap)) 1)
  1.1898 +                      end) (rec_prems' ~~ ihs);
  1.1899 +
  1.1900 +                    (** as # rs **)
  1.1901 +                    val _ = warning "step 8: as # rs";
  1.1902 +                    val rec_freshs = List.concat
  1.1903 +                      (map (fn (rec_prem, ih) =>
  1.1904 +                        let
  1.1905 +                          val _ $ (S $ x $ (y as Free (_, T))) =
  1.1906 +                            prop_of rec_prem;
  1.1907 +                          val k = find_index (equal S) rec_sets;
  1.1908 +                          val atoms = List.concat (List.mapPartial (fn (bs, z) =>
  1.1909 +                            if z = x then NONE else SOME bs) cargsl')
  1.1910 +                        in
  1.1911 +                          map (fn a as Free (_, aT) =>
  1.1912 +                            let val l = find_index (equal aT) dt_atomTs;
  1.1913 +                            in
  1.1914 +                              Goal.prove context'' [] []
  1.1915 +                                (HOLogic.mk_Trueprop (fresh_const aT T $ a $ y))
  1.1916 +                                (fn _ => EVERY
  1.1917 +                                   (rtac (List.nth (List.nth (rec_fresh_thms, l), k)) 1 ::
  1.1918 +                                    map (fn th => rtac th 1)
  1.1919 +                                      (snd (List.nth (finite_thss, l))) @
  1.1920 +                                    [rtac rec_prem 1, rtac ih 1,
  1.1921 +                                     REPEAT_DETERM (resolve_tac fresh_prems 1)]))
  1.1922 +                            end) atoms
  1.1923 +                        end) (rec_prems1 ~~ ihs));
  1.1924 +
  1.1925 +                    (** as # fK as ts rs , bs # fK bs us vs **)
  1.1926 +                    val _ = warning "step 9: as # fK as ts rs , bs # fK bs us vs";
  1.1927 +                    fun prove_fresh_result (a as Free (_, aT)) =
  1.1928 +                      Goal.prove context'' [] []
  1.1929 +                        (HOLogic.mk_Trueprop (fresh_const aT rT $ a $ rhs'))
  1.1930 +                        (fn _ => EVERY
  1.1931 +                           [resolve_tac fcbs 1,
  1.1932 +                            REPEAT_DETERM (resolve_tac
  1.1933 +                              (fresh_prems @ rec_freshs) 1),
  1.1934 +                            REPEAT_DETERM (resolve_tac (maps snd rec_fin_supp_thms') 1
  1.1935 +                              THEN resolve_tac rec_prems 1),
  1.1936 +                            resolve_tac P_ind_ths 1,
  1.1937 +                            REPEAT_DETERM (resolve_tac (P_ths @ rec_prems) 1)]);
  1.1938 +
  1.1939 +                    val fresh_results'' = map prove_fresh_result boundsl;
  1.1940 +
  1.1941 +                    fun prove_fresh_result'' ((a as Free (_, aT), b), th) =
  1.1942 +                      let val th' = Goal.prove context'' [] []
  1.1943 +                        (HOLogic.mk_Trueprop (fresh_const aT rT $
  1.1944 +                            fold_rev (mk_perm []) (rpi2 @ pi1) a $
  1.1945 +                            fold_rev (mk_perm []) (rpi2 @ pi1) rhs'))
  1.1946 +                        (fn _ => simp_tac (HOL_ss addsimps fresh_bij) 1 THEN
  1.1947 +                           rtac th 1)
  1.1948 +                      in
  1.1949 +                        Goal.prove context'' [] []
  1.1950 +                          (HOLogic.mk_Trueprop (fresh_const aT rT $ b $ lhs'))
  1.1951 +                          (fn _ => EVERY
  1.1952 +                             [cut_facts_tac [th'] 1,
  1.1953 +                              full_simp_tac (Simplifier.theory_context thy11 HOL_ss
  1.1954 +                                addsimps rec_eqns @ pi1_pi2_eqs @ perm_swap
  1.1955 +                                addsimprocs [NominalPermeq.perm_simproc_app]) 1,
  1.1956 +                              full_simp_tac (HOL_ss addsimps (calc_atm @
  1.1957 +                                fresh_prems' @ freshs2' @ perm_fresh_fresh)) 1])
  1.1958 +                      end;
  1.1959 +
  1.1960 +                    val fresh_results = fresh_results'' @ map prove_fresh_result''
  1.1961 +                      (boundsl ~~ boundsr ~~ fresh_results'');
  1.1962 +
  1.1963 +                    (** cs # fK as ts rs , cs # fK bs us vs **)
  1.1964 +                    val _ = warning "step 10: cs # fK as ts rs , cs # fK bs us vs";
  1.1965 +                    fun prove_fresh_result' recs t (a as Free (_, aT)) =
  1.1966 +                      Goal.prove context'' [] []
  1.1967 +                        (HOLogic.mk_Trueprop (fresh_const aT rT $ a $ t))
  1.1968 +                        (fn _ => EVERY
  1.1969 +                          [cut_facts_tac recs 1,
  1.1970 +                           REPEAT_DETERM (dresolve_tac
  1.1971 +                             (the (AList.lookup op = rec_fin_supp_thms' aT)) 1),
  1.1972 +                           NominalPermeq.fresh_guess_tac
  1.1973 +                             (HOL_ss addsimps (freshs2 @
  1.1974 +                                fs_atoms @ fresh_atm @
  1.1975 +                                List.concat (map snd finite_thss))) 1]);
  1.1976 +
  1.1977 +                    val fresh_results' =
  1.1978 +                      map (prove_fresh_result' rec_prems1 rhs') freshs1 @
  1.1979 +                      map (prove_fresh_result' rec_prems2 lhs') freshs1;
  1.1980 +
  1.1981 +                    (** pi1 o (fK as ts rs) = pi2 o (fK bs us vs) **)
  1.1982 +                    val _ = warning "step 11: pi1 o (fK as ts rs) = pi2 o (fK bs us vs)";
  1.1983 +                    val pi1_pi2_result = Goal.prove context'' [] []
  1.1984 +                      (HOLogic.mk_Trueprop (HOLogic.mk_eq
  1.1985 +                        (fold_rev (mk_perm []) pi1 rhs', fold_rev (mk_perm []) pi2 lhs')))
  1.1986 +                      (fn _ => simp_tac (Simplifier.context context'' HOL_ss
  1.1987 +                           addsimps pi1_pi2_eqs @ rec_eqns
  1.1988 +                           addsimprocs [NominalPermeq.perm_simproc_app]) 1 THEN
  1.1989 +                         TRY (simp_tac (HOL_ss addsimps
  1.1990 +                           (fresh_prems' @ freshs2' @ calc_atm @ perm_fresh_fresh)) 1));
  1.1991 +
  1.1992 +                    val _ = warning "final result";
  1.1993 +                    val final = Goal.prove context'' [] [] (term_of concl)
  1.1994 +                      (fn _ => cut_facts_tac [pi1_pi2_result RS sym] 1 THEN
  1.1995 +                        full_simp_tac (HOL_basic_ss addsimps perm_fresh_fresh @
  1.1996 +                          fresh_results @ fresh_results') 1);
  1.1997 +                    val final' = ProofContext.export context'' context' [final];
  1.1998 +                    val _ = warning "finished!"
  1.1999 +                  in
  1.2000 +                    resolve_tac final' 1
  1.2001 +                  end) context 1])) idxss) (ndescr ~~ rec_elims))
  1.2002 +         end));
  1.2003 +
  1.2004 +    val rec_total_thms = map (fn r => r RS theI') rec_unique_thms;
  1.2005 +
  1.2006 +    (* define primrec combinators *)
  1.2007 +
  1.2008 +    val big_reccomb_name = (space_implode "_" new_type_names) ^ "_rec";
  1.2009 +    val reccomb_names = map (Sign.full_bname thy11)
  1.2010 +      (if length descr'' = 1 then [big_reccomb_name] else
  1.2011 +        (map ((curry (op ^) (big_reccomb_name ^ "_")) o string_of_int)
  1.2012 +          (1 upto (length descr''))));
  1.2013 +    val reccombs = map (fn ((name, T), T') => list_comb
  1.2014 +      (Const (name, rec_fn_Ts @ [T] ---> T'), rec_fns))
  1.2015 +        (reccomb_names ~~ recTs ~~ rec_result_Ts);
  1.2016 +
  1.2017 +    val (reccomb_defs, thy12) =
  1.2018 +      thy11
  1.2019 +      |> Sign.add_consts_i (map (fn ((name, T), T') =>
  1.2020 +          (Binding.name (Long_Name.base_name name), rec_fn_Ts @ [T] ---> T', NoSyn))
  1.2021 +          (reccomb_names ~~ recTs ~~ rec_result_Ts))
  1.2022 +      |> (PureThy.add_defs false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') =>
  1.2023 +          (Binding.name (Long_Name.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T,
  1.2024 +           Const ("The", (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
  1.2025 +             set $ Free ("x", T) $ Free ("y", T'))))))
  1.2026 +               (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts));
  1.2027 +
  1.2028 +    (* prove characteristic equations for primrec combinators *)
  1.2029 +
  1.2030 +    val rec_thms = map (fn (prems, concl) =>
  1.2031 +      let
  1.2032 +        val _ $ (_ $ (_ $ x) $ _) = concl;
  1.2033 +        val (_, cargs) = strip_comb x;
  1.2034 +        val ps = map (fn (x as Free (_, T), i) =>
  1.2035 +          (Free ("x" ^ string_of_int i, T), x)) (cargs ~~ (1 upto length cargs));
  1.2036 +        val concl' = subst_atomic_types (rec_result_Ts' ~~ rec_result_Ts) concl;
  1.2037 +        val prems' = List.concat finite_premss @ finite_ctxt_prems @
  1.2038 +          rec_prems @ rec_prems' @ map (subst_atomic ps) prems;
  1.2039 +        fun solve rules prems = resolve_tac rules THEN_ALL_NEW
  1.2040 +          (resolve_tac prems THEN_ALL_NEW atac)
  1.2041 +      in
  1.2042 +        Goal.prove_global thy12 []
  1.2043 +          (map (augment_sort thy12 fs_cp_sort) prems')
  1.2044 +          (augment_sort thy12 fs_cp_sort concl')
  1.2045 +          (fn {prems, ...} => EVERY
  1.2046 +            [rewrite_goals_tac reccomb_defs,
  1.2047 +             rtac the1_equality 1,
  1.2048 +             solve rec_unique_thms prems 1,
  1.2049 +             resolve_tac rec_intrs 1,
  1.2050 +             REPEAT (solve (prems @ rec_total_thms) prems 1)])
  1.2051 +      end) (rec_eq_prems ~~
  1.2052 +        DatatypeProp.make_primrecs new_type_names descr' sorts thy12);
  1.2053 +
  1.2054 +    val dt_infos = map (make_dt_info pdescr sorts induct reccomb_names rec_thms)
  1.2055 +      ((0 upto length descr1 - 1) ~~ descr1 ~~ distinct_thms ~~ inject_thms);
  1.2056 +
  1.2057 +    (* FIXME: theorems are stored in database for testing only *)
  1.2058 +    val (_, thy13) = thy12 |>
  1.2059 +      PureThy.add_thmss
  1.2060 +        [((Binding.name "rec_equiv", List.concat rec_equiv_thms), []),
  1.2061 +         ((Binding.name "rec_equiv'", List.concat rec_equiv_thms'), []),
  1.2062 +         ((Binding.name "rec_fin_supp", List.concat rec_fin_supp_thms), []),
  1.2063 +         ((Binding.name "rec_fresh", List.concat rec_fresh_thms), []),
  1.2064 +         ((Binding.name "rec_unique", map standard rec_unique_thms), []),
  1.2065 +         ((Binding.name "recs", rec_thms), [])] ||>
  1.2066 +      Sign.parent_path ||>
  1.2067 +      map_nominal_datatypes (fold Symtab.update dt_infos);
  1.2068 +
  1.2069 +  in
  1.2070 +    thy13
  1.2071 +  end;
  1.2072 +
  1.2073 +val add_nominal_datatype = gen_add_nominal_datatype Datatype.read_typ;
  1.2074 +
  1.2075 +
  1.2076 +(* FIXME: The following stuff should be exported by Datatype *)
  1.2077 +
  1.2078 +local structure P = OuterParse and K = OuterKeyword in
  1.2079 +
  1.2080 +val datatype_decl =
  1.2081 +  Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.name -- P.opt_infix --
  1.2082 +    (P.$$$ "=" |-- P.enum1 "|" (P.name -- Scan.repeat P.typ -- P.opt_mixfix));
  1.2083 +
  1.2084 +fun mk_datatype args =
  1.2085 +  let
  1.2086 +    val names = map (fn ((((NONE, _), t), _), _) => t | ((((SOME t, _), _), _), _) => t) args;
  1.2087 +    val specs = map (fn ((((_, vs), t), mx), cons) =>
  1.2088 +      (vs, t, mx, map (fn ((x, y), z) => (x, y, z)) cons)) args;
  1.2089 +  in add_nominal_datatype Datatype.default_config names specs end;
  1.2090 +
  1.2091 +val _ =
  1.2092 +  OuterSyntax.command "nominal_datatype" "define inductive datatypes" K.thy_decl
  1.2093 +    (P.and_list1 datatype_decl >> (Toplevel.theory o mk_datatype));
  1.2094 +
  1.2095 +end;
  1.2096 +
  1.2097 +end