1 (* Title: HOL/Nominal/nominal_datatype.ML
2 Author: Stefan Berghofer and Christian Urban, TU Muenchen
4 Nominal datatype package for Isabelle/HOL.
7 signature NOMINAL_DATATYPE =
9 val add_nominal_datatype : Datatype.config -> string list ->
10 (string list * bstring * mixfix *
11 (bstring * string list * mixfix) list) list -> theory -> theory
13 type nominal_datatype_info
14 val get_nominal_datatypes : theory -> nominal_datatype_info Symtab.table
15 val get_nominal_datatype : theory -> string -> nominal_datatype_info option
16 val mk_perm: typ list -> term -> term -> term
17 val perm_of_pair: term * term -> term
18 val mk_not_sym: thm list -> thm list
19 val perm_simproc: simproc
20 val fresh_const: typ -> typ -> term
21 val fresh_star_const: typ -> typ -> term
24 structure NominalDatatype : NOMINAL_DATATYPE =
27 val finite_emptyI = @{thm finite.emptyI};
28 val finite_Diff = @{thm finite_Diff};
29 val finite_Un = @{thm finite_Un};
30 val Un_iff = @{thm Un_iff};
31 val In0_eq = @{thm In0_eq};
32 val In1_eq = @{thm In1_eq};
33 val In0_not_In1 = @{thm In0_not_In1};
34 val In1_not_In0 = @{thm In1_not_In0};
35 val Un_assoc = @{thm Un_assoc};
36 val Collect_disj_eq = @{thm Collect_disj_eq};
37 val Collect_False_empty = @{thm empty_def [THEN sym, THEN eq_reflection]};
38 val empty_iff = @{thm empty_iff};
43 (** FIXME: Datatype should export this function **)
47 fun dt_recs (DtTFree _) = []
48 | dt_recs (DtType (_, dts)) = maps dt_recs dts
49 | dt_recs (DtRec i) = [i];
51 fun dt_cases (descr: descr) (_, args, constrs) =
53 fun the_bname i = Long_Name.base_name (#1 (the (AList.lookup (op =) descr i)));
54 val bnames = map the_bname (distinct op = (maps dt_recs args));
55 in map (fn (c, _) => space_implode "_" (Long_Name.base_name c :: bnames)) constrs end;
58 fun induct_cases descr =
59 Datatype_Prop.indexify_names (maps (dt_cases descr) (map #2 descr));
61 fun exhaust_cases descr i = dt_cases descr (the (AList.lookup (op =) descr i));
65 fun mk_case_names_induct descr = Rule_Cases.case_names (induct_cases descr);
67 fun mk_case_names_exhausts descr new =
68 map (Rule_Cases.case_names o exhaust_cases descr o #1)
69 (filter (fn ((_, (name, _, _))) => member (op =) new name) descr);
75 type descr = (int * (string * dtyp list * (string * (dtyp list * dtyp) list) list)) list;
77 type nominal_datatype_info =
80 sorts : (string * sort) list,
81 rec_names : string list,
82 rec_rewrites : thm list,
87 structure NominalDatatypesData = Theory_Data
89 type T = nominal_datatype_info Symtab.table;
90 val empty = Symtab.empty;
92 fun merge data = Symtab.merge (K true) data;
95 val get_nominal_datatypes = NominalDatatypesData.get;
96 val put_nominal_datatypes = NominalDatatypesData.put;
97 val map_nominal_datatypes = NominalDatatypesData.map;
98 val get_nominal_datatype = Symtab.lookup o get_nominal_datatypes;
101 (**** make datatype info ****)
103 fun make_dt_info descr sorts induct reccomb_names rec_thms
104 (i, (((_, (tname, _, _)), distinct), inject)) =
109 rec_names = reccomb_names,
110 rec_rewrites = rec_thms,
115 (*******************************)
117 val (_ $ (_ $ (_ $ (distinct_f $ _) $ _))) = hd (prems_of distinct_lemma);
120 (** simplification procedure for sorting permutations **)
122 val dj_cp = @{thm dj_cp};
124 fun dest_permT (Type ("fun", [Type ("List.list", [Type (@{type_name Product_Type.prod}, [T, _])]),
125 Type ("fun", [_, U])])) = (T, U);
127 fun permTs_of (Const ("Nominal.perm", T) $ t $ u) = fst (dest_permT T) :: permTs_of u
130 fun perm_simproc' thy ss (Const ("Nominal.perm", T) $ t $ (u as Const ("Nominal.perm", U) $ r $ s)) =
132 val (aT as Type (a, []), S) = dest_permT T;
133 val (bT as Type (b, []), _) = dest_permT U
134 in if member (op =) (permTs_of u) aT andalso aT <> bT then
136 val cp = cp_inst_of thy a b;
137 val dj = dj_thm_of thy b a;
138 val dj_cp' = [cp, dj] MRS dj_cp;
139 val cert = SOME o cterm_of thy
141 SOME (mk_meta_eq (Drule.instantiate' [SOME (ctyp_of thy S)]
142 [cert t, cert r, cert s] dj_cp'))
146 | perm_simproc' thy ss _ = NONE;
149 Simplifier.simproc_global @{theory} "perm_simp" ["pi1 \<bullet> (pi2 \<bullet> x)"] perm_simproc';
151 fun projections rule =
152 Project_Rule.projections (Proof_Context.init_global (Thm.theory_of_thm rule)) rule
153 |> map (Drule.export_without_context #> Rule_Cases.save rule);
155 val supp_prod = @{thm supp_prod};
156 val fresh_prod = @{thm fresh_prod};
157 val supports_fresh = @{thm supports_fresh};
158 val supports_def = @{thm Nominal.supports_def};
159 val fresh_def = @{thm fresh_def};
160 val supp_def = @{thm supp_def};
161 val rev_simps = @{thms rev.simps};
162 val app_simps = @{thms append.simps};
163 val at_fin_set_supp = @{thm at_fin_set_supp};
164 val at_fin_set_fresh = @{thm at_fin_set_fresh};
165 val abs_fun_eq1 = @{thm abs_fun_eq1};
167 val collect_simp = rewrite_rule [mk_meta_eq mem_Collect_eq];
171 val T = fastype_of1 (Ts, t);
172 val U = fastype_of1 (Ts, u)
173 in Const ("Nominal.perm", T --> U --> U) $ t $ u end;
175 fun perm_of_pair (x, y) =
177 val T = fastype_of x;
179 in Const ("List.list.Cons", HOLogic.mk_prodT (T, T) --> pT --> pT) $
180 HOLogic.mk_prod (x, y) $ Const ("List.list.Nil", pT)
183 fun mk_not_sym ths = maps (fn th => case prop_of th of
184 _ $ (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ _)) => [th, th RS not_sym]
187 fun fresh_const T U = Const ("Nominal.fresh", T --> U --> HOLogic.boolT);
188 fun fresh_star_const T U =
189 Const ("Nominal.fresh_star", HOLogic.mk_setT T --> U --> HOLogic.boolT);
191 fun gen_add_nominal_datatype prep_typ config new_type_names dts thy =
193 (* this theory is used just for parsing *)
197 Sign.add_types_global (map (fn (tvs, tname, mx, _) =>
198 (Binding.name tname, length tvs, mx)) dts);
200 val atoms = atoms_of thy;
202 fun prep_constr (cname, cargs, mx) (constrs, sorts) =
203 let val (cargs', sorts') = fold_map (prep_typ tmp_thy) cargs sorts
204 in (constrs @ [(cname, cargs', mx)], sorts') end
206 fun prep_dt_spec (tvs, tname, mx, constrs) (dts, sorts) =
207 let val (constrs', sorts') = fold prep_constr constrs ([], sorts)
208 in (dts @ [(tvs, tname, mx, constrs')], sorts') end
210 val (dts', sorts) = fold prep_dt_spec dts ([], []);
211 val tyvars = map (map (fn s =>
212 (s, the (AList.lookup (op =) sorts s))) o #1) dts';
214 fun inter_sort thy S S' = Sign.inter_sort thy (S, S');
215 fun augment_sort_typ thy S =
216 let val S = Sign.minimize_sort thy (Sign.certify_sort thy S)
217 in map_type_tfree (fn (s, S') => TFree (s,
218 if member (op = o apsnd fst) sorts s then inter_sort thy S S' else S'))
220 fun augment_sort thy S = map_types (augment_sort_typ thy S);
222 val types_syntax = map (fn (tvs, tname, mx, constrs) => (tname, mx)) dts';
223 val constr_syntax = map (fn (tvs, tname, mx, constrs) =>
224 map (fn (cname, cargs, mx) => (cname, mx)) constrs) dts';
226 val ps = map (fn (_, n, _, _) =>
227 (Sign.full_bname tmp_thy n, Sign.full_bname tmp_thy (n ^ "_Rep"))) dts;
228 val rps = map Library.swap ps;
230 fun replace_types (Type ("Nominal.ABS", [T, U])) =
231 Type ("fun", [T, Type ("Nominal.noption", [replace_types U])])
232 | replace_types (Type (s, Ts)) =
233 Type (the_default s (AList.lookup op = ps s), map replace_types Ts)
234 | replace_types T = T;
236 val dts'' = map (fn (tvs, tname, mx, constrs) => (tvs, Binding.name (tname ^ "_Rep"), NoSyn,
237 map (fn (cname, cargs, mx) => (Binding.name (cname ^ "_Rep"),
238 map replace_types cargs, NoSyn)) constrs)) dts';
240 val new_type_names' = map (fn n => n ^ "_Rep") new_type_names;
242 val (full_new_type_names',thy1) =
243 Datatype.add_datatype config new_type_names' dts'' thy;
245 val {descr, induct, ...} =
246 Datatype.the_info thy1 (hd full_new_type_names');
247 fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
249 val big_name = space_implode "_" new_type_names;
252 (**** define permutation functions ****)
254 val permT = mk_permT (TFree ("'x", HOLogic.typeS));
255 val pi = Free ("pi", permT);
256 val perm_types = map (fn (i, _) =>
257 let val T = nth_dtyp i
258 in permT --> T --> T end) descr;
259 val perm_names' = Datatype_Prop.indexify_names (map (fn (i, _) =>
260 "perm_" ^ name_of_typ (nth_dtyp i)) descr);
261 val perm_names = replicate (length new_type_names) "Nominal.perm" @
262 map (Sign.full_bname thy1) (List.drop (perm_names', length new_type_names));
263 val perm_names_types = perm_names ~~ perm_types;
264 val perm_names_types' = perm_names' ~~ perm_types;
266 val perm_eqs = maps (fn (i, (_, _, constrs)) =>
267 let val T = nth_dtyp i
268 in map (fn (cname, dts) =>
270 val Ts = map (typ_of_dtyp descr sorts) dts;
271 val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts);
272 val args = map Free (names ~~ Ts);
273 val c = Const (cname, Ts ---> T);
274 fun perm_arg (dt, x) =
275 let val T = type_of x
276 in if is_rec_type dt then
277 let val Us = binder_types T
278 in list_abs (map (pair "x") Us,
279 Free (nth perm_names_types' (body_index dt)) $ pi $
280 list_comb (x, map (fn (i, U) =>
281 Const ("Nominal.perm", permT --> U --> U) $
282 (Const ("List.rev", permT --> permT) $ pi) $
283 Bound i) ((length Us - 1 downto 0) ~~ Us)))
285 else Const ("Nominal.perm", permT --> T --> T) $ pi $ x
288 (Attrib.empty_binding, HOLogic.mk_Trueprop (HOLogic.mk_eq
289 (Free (nth perm_names_types' i) $
290 Free ("pi", mk_permT (TFree ("'x", HOLogic.typeS))) $
292 list_comb (c, map perm_arg (dts ~~ args)))))
296 val (perm_simps, thy2) =
297 Primrec.add_primrec_overloaded
298 (map (fn (s, sT) => (s, sT, false))
299 (List.take (perm_names' ~~ perm_names_types, length new_type_names)))
300 (map (fn s => (Binding.name s, NONE, NoSyn)) perm_names') perm_eqs thy1;
302 (**** prove that permutation functions introduced by unfolding are ****)
303 (**** equivalent to already existing permutation functions ****)
305 val _ = warning ("length descr: " ^ string_of_int (length descr));
306 val _ = warning ("length new_type_names: " ^ string_of_int (length new_type_names));
308 val perm_indnames = Datatype_Prop.make_tnames (map body_type perm_types);
309 val perm_fun_def = Global_Theory.get_thm thy2 "perm_fun_def";
311 val unfolded_perm_eq_thms =
312 if length descr = length new_type_names then []
313 else map Drule.export_without_context (List.drop (split_conj_thm
314 (Goal.prove_global thy2 [] []
315 (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
316 (map (fn (c as (s, T), x) =>
317 let val [T1, T2] = binder_types T
318 in HOLogic.mk_eq (Const c $ pi $ Free (x, T2),
319 Const ("Nominal.perm", T) $ pi $ Free (x, T2))
321 (perm_names_types ~~ perm_indnames))))
322 (fn _ => EVERY [indtac induct perm_indnames 1,
323 ALLGOALS (asm_full_simp_tac
324 (global_simpset_of thy2 addsimps [perm_fun_def]))])),
325 length new_type_names));
327 (**** prove [] \<bullet> t = t ****)
329 val _ = warning "perm_empty_thms";
331 val perm_empty_thms = maps (fn a =>
332 let val permT = mk_permT (Type (a, []))
333 in map Drule.export_without_context (List.take (split_conj_thm
334 (Goal.prove_global thy2 [] []
335 (augment_sort thy2 [pt_class_of thy2 a]
336 (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
337 (map (fn ((s, T), x) => HOLogic.mk_eq
338 (Const (s, permT --> T --> T) $
339 Const ("List.list.Nil", permT) $ Free (x, T),
342 map body_type perm_types ~~ perm_indnames)))))
343 (fn _ => EVERY [indtac induct perm_indnames 1,
344 ALLGOALS (asm_full_simp_tac (global_simpset_of thy2))])),
345 length new_type_names))
349 (**** prove (pi1 @ pi2) \<bullet> t = pi1 \<bullet> (pi2 \<bullet> t) ****)
351 val _ = warning "perm_append_thms";
353 (*FIXME: these should be looked up statically*)
354 val at_pt_inst = Global_Theory.get_thm thy2 "at_pt_inst";
355 val pt2 = Global_Theory.get_thm thy2 "pt2";
357 val perm_append_thms = maps (fn a =>
359 val permT = mk_permT (Type (a, []));
360 val pi1 = Free ("pi1", permT);
361 val pi2 = Free ("pi2", permT);
362 val pt_inst = pt_inst_of thy2 a;
363 val pt2' = pt_inst RS pt2;
364 val pt2_ax = Global_Theory.get_thm thy2 (Long_Name.map_base_name (fn s => "pt_" ^ s ^ "2") a);
365 in List.take (map Drule.export_without_context (split_conj_thm
366 (Goal.prove_global thy2 [] []
367 (augment_sort thy2 [pt_class_of thy2 a]
368 (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
369 (map (fn ((s, T), x) =>
370 let val perm = Const (s, permT --> T --> T)
372 (perm $ (Const ("List.append", permT --> permT --> permT) $
373 pi1 $ pi2) $ Free (x, T),
374 perm $ pi1 $ (perm $ pi2 $ Free (x, T)))
377 map body_type perm_types ~~ perm_indnames)))))
378 (fn _ => EVERY [indtac induct perm_indnames 1,
379 ALLGOALS (asm_full_simp_tac (global_simpset_of thy2 addsimps [pt2', pt2_ax]))]))),
380 length new_type_names)
383 (**** prove pi1 ~ pi2 ==> pi1 \<bullet> t = pi2 \<bullet> t ****)
385 val _ = warning "perm_eq_thms";
387 val pt3 = Global_Theory.get_thm thy2 "pt3";
388 val pt3_rev = Global_Theory.get_thm thy2 "pt3_rev";
390 val perm_eq_thms = maps (fn a =>
392 val permT = mk_permT (Type (a, []));
393 val pi1 = Free ("pi1", permT);
394 val pi2 = Free ("pi2", permT);
395 val at_inst = at_inst_of thy2 a;
396 val pt_inst = pt_inst_of thy2 a;
397 val pt3' = pt_inst RS pt3;
398 val pt3_rev' = at_inst RS (pt_inst RS pt3_rev);
399 val pt3_ax = Global_Theory.get_thm thy2 (Long_Name.map_base_name (fn s => "pt_" ^ s ^ "3") a);
400 in List.take (map Drule.export_without_context (split_conj_thm
401 (Goal.prove_global thy2 [] []
402 (augment_sort thy2 [pt_class_of thy2 a] (Logic.mk_implies
403 (HOLogic.mk_Trueprop (Const ("Nominal.prm_eq",
404 permT --> permT --> HOLogic.boolT) $ pi1 $ pi2),
405 HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
406 (map (fn ((s, T), x) =>
407 let val perm = Const (s, permT --> T --> T)
409 (perm $ pi1 $ Free (x, T),
410 perm $ pi2 $ Free (x, T))
413 map body_type perm_types ~~ perm_indnames))))))
414 (fn _ => EVERY [indtac induct perm_indnames 1,
415 ALLGOALS (asm_full_simp_tac (global_simpset_of thy2 addsimps [pt3', pt3_rev', pt3_ax]))]))),
416 length new_type_names)
419 (**** prove pi1 \<bullet> (pi2 \<bullet> t) = (pi1 \<bullet> pi2) \<bullet> (pi1 \<bullet> t) ****)
421 val cp1 = Global_Theory.get_thm thy2 "cp1";
422 val dj_cp = Global_Theory.get_thm thy2 "dj_cp";
423 val pt_perm_compose = Global_Theory.get_thm thy2 "pt_perm_compose";
424 val pt_perm_compose_rev = Global_Theory.get_thm thy2 "pt_perm_compose_rev";
425 val dj_perm_perm_forget = Global_Theory.get_thm thy2 "dj_perm_perm_forget";
427 fun composition_instance name1 name2 thy =
429 val cp_class = cp_class_of thy name1 name2;
431 if name1 = name2 then [pt_class_of thy name1]
433 val permT1 = mk_permT (Type (name1, []));
434 val permT2 = mk_permT (Type (name2, []));
435 val Ts = map body_type perm_types;
436 val cp_inst = cp_inst_of thy name1 name2;
437 val simps = global_simpset_of thy addsimps (perm_fun_def ::
438 (if name1 <> name2 then
439 let val dj = dj_thm_of thy name2 name1
440 in [dj RS (cp_inst RS dj_cp), dj RS dj_perm_perm_forget] end
443 val at_inst = at_inst_of thy name1;
444 val pt_inst = pt_inst_of thy name1;
446 [cp_inst RS cp1 RS sym,
447 at_inst RS (pt_inst RS pt_perm_compose) RS sym,
448 at_inst RS (pt_inst RS pt_perm_compose_rev) RS sym]
450 val sort = Sign.minimize_sort thy (Sign.certify_sort thy (cp_class :: pt_class));
451 val thms = split_conj_thm (Goal.prove_global thy [] []
452 (augment_sort thy sort
453 (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
454 (map (fn ((s, T), x) =>
456 val pi1 = Free ("pi1", permT1);
457 val pi2 = Free ("pi2", permT2);
458 val perm1 = Const (s, permT1 --> T --> T);
459 val perm2 = Const (s, permT2 --> T --> T);
460 val perm3 = Const ("Nominal.perm", permT1 --> permT2 --> permT2)
462 (perm1 $ pi1 $ (perm2 $ pi2 $ Free (x, T)),
463 perm2 $ (perm3 $ pi1 $ pi2) $ (perm1 $ pi1 $ Free (x, T)))
465 (perm_names ~~ Ts ~~ perm_indnames)))))
466 (fn _ => EVERY [indtac induct perm_indnames 1,
467 ALLGOALS (asm_full_simp_tac simps)]))
469 fold (fn (s, tvs) => fn thy => AxClass.prove_arity
470 (s, map (inter_sort thy sort o snd) tvs, [cp_class])
471 (Class.intro_classes_tac [] THEN ALLGOALS (resolve_tac thms)) thy)
472 (full_new_type_names' ~~ tyvars) thy
475 val (perm_thmss,thy3) = thy2 |>
476 fold (fn name1 => fold (composition_instance name1) atoms) atoms |>
477 fold (fn atom => fn thy =>
478 let val pt_name = pt_class_of thy atom
480 fold (fn (s, tvs) => fn thy => AxClass.prove_arity
481 (s, map (inter_sort thy [pt_name] o snd) tvs, [pt_name])
483 [Class.intro_classes_tac [],
484 resolve_tac perm_empty_thms 1,
485 resolve_tac perm_append_thms 1,
486 resolve_tac perm_eq_thms 1, assume_tac 1]) thy)
487 (full_new_type_names' ~~ tyvars) thy
489 Global_Theory.add_thmss
490 [((Binding.name (space_implode "_" new_type_names ^ "_unfolded_perm_eq"),
491 unfolded_perm_eq_thms), [Simplifier.simp_add]),
492 ((Binding.name (space_implode "_" new_type_names ^ "_perm_empty"),
493 perm_empty_thms), [Simplifier.simp_add]),
494 ((Binding.name (space_implode "_" new_type_names ^ "_perm_append"),
495 perm_append_thms), [Simplifier.simp_add]),
496 ((Binding.name (space_implode "_" new_type_names ^ "_perm_eq"),
497 perm_eq_thms), [Simplifier.simp_add])];
499 (**** Define representing sets ****)
501 val _ = warning "representing sets";
503 val rep_set_names = Datatype_Prop.indexify_names
504 (map (fn (i, _) => name_of_typ (nth_dtyp i) ^ "_set") descr);
506 space_implode "_" (Datatype_Prop.indexify_names (map_filter
507 (fn (i, ("Nominal.noption", _, _)) => NONE
508 | (i, _) => SOME (name_of_typ (nth_dtyp i))) descr)) ^ "_set";
509 val _ = warning ("big_rep_name: " ^ big_rep_name);
511 fun strip_option (dtf as DtType ("fun", [dt, DtRec i])) =
512 (case AList.lookup op = descr i of
513 SOME ("Nominal.noption", _, [(_, [dt']), _]) =>
514 apfst (cons dt) (strip_option dt')
516 | strip_option (DtType ("fun", [dt, DtType ("Nominal.noption", [dt'])])) =
517 apfst (cons dt) (strip_option dt')
518 | strip_option dt = ([], dt);
520 val dt_atomTs = distinct op = (map (typ_of_dtyp descr sorts)
521 (maps (fn (_, (_, _, cs)) => maps (maps (fst o strip_option) o snd) cs) descr));
522 val dt_atoms = map (fst o dest_Type) dt_atomTs;
524 fun make_intr s T (cname, cargs) =
526 fun mk_prem dt (j, j', prems, ts) =
528 val (dts, dt') = strip_option dt;
529 val (dts', dt'') = strip_dtyp dt';
530 val Ts = map (typ_of_dtyp descr sorts) dts;
531 val Us = map (typ_of_dtyp descr sorts) dts';
532 val T = typ_of_dtyp descr sorts dt'';
533 val free = mk_Free "x" (Us ---> T) j;
534 val free' = app_bnds free (length Us);
535 fun mk_abs_fun T (i, t) =
536 let val U = fastype_of t
537 in (i + 1, Const ("Nominal.abs_fun", [T, U, T] --->
538 Type ("Nominal.noption", [U])) $ mk_Free "y" T i $ t)
540 in (j + 1, j' + length Ts,
542 DtRec k => list_all (map (pair "x") Us,
543 HOLogic.mk_Trueprop (Free (nth rep_set_names k,
544 T --> HOLogic.boolT) $ free')) :: prems
546 snd (fold_rev mk_abs_fun Ts (j', free)) :: ts)
549 val (_, _, prems, ts) = fold_rev mk_prem cargs (1, 1, [], []);
550 val concl = HOLogic.mk_Trueprop (Free (s, T --> HOLogic.boolT) $
551 list_comb (Const (cname, map fastype_of ts ---> T), ts))
552 in Logic.list_implies (prems, concl)
555 val (intr_ts, (rep_set_names', recTs')) =
556 apfst flat (apsnd ListPair.unzip (ListPair.unzip (map_filter
557 (fn ((_, ("Nominal.noption", _, _)), _) => NONE
558 | ((i, (_, _, constrs)), rep_set_name) =>
559 let val T = nth_dtyp i
560 in SOME (map (make_intr rep_set_name T) constrs,
563 (descr ~~ rep_set_names))));
564 val rep_set_names'' = map (Sign.full_bname thy3) rep_set_names';
566 val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy4) =
568 |> Sign.map_naming Name_Space.conceal
569 |> Inductive.add_inductive_global
570 {quiet_mode = false, verbose = false, alt_name = Binding.name big_rep_name,
571 coind = false, no_elim = true, no_ind = false, skip_mono = true, fork_mono = false}
572 (map (fn (s, T) => ((Binding.name s, T --> HOLogic.boolT), NoSyn))
573 (rep_set_names' ~~ recTs'))
574 [] (map (fn x => (Attrib.empty_binding, x)) intr_ts) []
575 ||> Sign.restore_naming thy3;
577 (**** Prove that representing set is closed under permutation ****)
579 val _ = warning "proving closure under permutation...";
581 val abs_perm = Global_Theory.get_thms thy4 "abs_perm";
583 val perm_indnames' = map_filter
584 (fn (x, (_, ("Nominal.noption", _, _))) => NONE | (x, _) => SOME x)
585 (perm_indnames ~~ descr);
587 fun mk_perm_closed name = map (fn th => Drule.export_without_context (th RS mp))
588 (List.take (split_conj_thm (Goal.prove_global thy4 [] []
590 (pt_class_of thy4 name :: map (cp_class_of thy4 name) (remove (op =) name dt_atoms))
591 (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map
594 val S = Const (s, T --> HOLogic.boolT);
595 val permT = mk_permT (Type (name, []))
596 in HOLogic.mk_imp (S $ Free (x, T),
597 S $ (Const ("Nominal.perm", permT --> T --> T) $
598 Free ("pi", permT) $ Free (x, T)))
599 end) (rep_set_names'' ~~ recTs' ~~ perm_indnames')))))
601 [indtac rep_induct [] 1,
602 ALLGOALS (simp_tac (global_simpset_of thy4 addsimps
603 (Thm.symmetric perm_fun_def :: abs_perm))),
604 ALLGOALS (resolve_tac rep_intrs THEN_ALL_NEW assume_tac)])),
605 length new_type_names));
607 val perm_closed_thmss = map mk_perm_closed atoms;
611 val _ = warning "defining type...";
613 val (typedefs, thy6) =
615 |> fold_map (fn ((((name, mx), tvs), (cname, U)), name') => fn thy =>
616 Typedef.add_typedef_global false (SOME (Binding.name name'))
617 (Binding.name name, map (fn (v, _) => (v, dummyS)) tvs, mx) (* FIXME keep constraints!? *)
618 (Const (@{const_name Collect}, (U --> HOLogic.boolT) --> HOLogic.mk_setT U) $
619 Const (cname, U --> HOLogic.boolT)) NONE
620 (rtac exI 1 THEN rtac CollectI 1 THEN
621 QUIET_BREADTH_FIRST (has_fewer_prems 1)
622 (resolve_tac rep_intrs 1)) thy |> (fn ((_, r), thy) =>
625 (TFree (singleton (Name.variant_list (map fst tvs)) "'a", HOLogic.typeS));
626 val pi = Free ("pi", permT);
627 val T = Type (Sign.intern_type thy name, map TFree tvs);
628 in apfst (pair r o hd)
629 (Global_Theory.add_defs_unchecked true [((Binding.name ("prm_" ^ name ^ "_def"), Logic.mk_equals
630 (Const ("Nominal.perm", permT --> T --> T) $ pi $ Free ("x", T),
631 Const (Sign.intern_const thy ("Abs_" ^ name), U --> T) $
632 (Const ("Nominal.perm", permT --> U --> U) $ pi $
633 (Const (Sign.intern_const thy ("Rep_" ^ name), T --> U) $
634 Free ("x", T))))), [])] thy)
636 (types_syntax ~~ tyvars ~~
637 List.take (rep_set_names'' ~~ recTs', length new_type_names) ~~
640 val perm_defs = map snd typedefs;
641 val Abs_inverse_thms = map (collect_simp o #Abs_inverse o snd o fst) typedefs;
642 val Rep_inverse_thms = map (#Rep_inverse o snd o fst) typedefs;
643 val Rep_thms = map (collect_simp o #Rep o snd o fst) typedefs;
646 (** prove that new types are in class pt_<name> **)
648 val _ = warning "prove that new types are in class pt_<name> ...";
650 fun pt_instance (atom, perm_closed_thms) =
651 fold (fn ((((((Abs_inverse, Rep_inverse), Rep),
652 perm_def), name), tvs), perm_closed) => fn thy =>
654 val pt_class = pt_class_of thy atom;
655 val sort = Sign.minimize_sort thy (Sign.certify_sort thy
656 (pt_class :: map (cp_class_of thy atom) (remove (op =) atom dt_atoms)))
657 in AxClass.prove_arity
658 (Sign.intern_type thy name,
659 map (inter_sort thy sort o snd) tvs, [pt_class])
660 (EVERY [Class.intro_classes_tac [],
661 rewrite_goals_tac [perm_def],
662 asm_full_simp_tac (global_simpset_of thy addsimps [Rep_inverse]) 1,
663 asm_full_simp_tac (global_simpset_of thy addsimps
664 [Rep RS perm_closed RS Abs_inverse]) 1,
665 asm_full_simp_tac (HOL_basic_ss addsimps [Global_Theory.get_thm thy
666 ("pt_" ^ Long_Name.base_name atom ^ "3")]) 1]) thy
668 (Abs_inverse_thms ~~ Rep_inverse_thms ~~ Rep_thms ~~ perm_defs ~~
669 new_type_names ~~ tyvars ~~ perm_closed_thms);
672 (** prove that new types are in class cp_<name1>_<name2> **)
674 val _ = warning "prove that new types are in class cp_<name1>_<name2> ...";
676 fun cp_instance (atom1, perm_closed_thms1) (atom2, perm_closed_thms2) thy =
678 val cp_class = cp_class_of thy atom1 atom2;
679 val sort = Sign.minimize_sort thy (Sign.certify_sort thy
680 (pt_class_of thy atom1 :: map (cp_class_of thy atom1) (remove (op =) atom1 dt_atoms) @
681 (if atom1 = atom2 then [cp_class_of thy atom1 atom1] else
682 pt_class_of thy atom2 :: map (cp_class_of thy atom2) (remove (op =) atom2 dt_atoms))));
683 val cp1' = cp_inst_of thy atom1 atom2 RS cp1
684 in fold (fn ((((((Abs_inverse, Rep),
685 perm_def), name), tvs), perm_closed1), perm_closed2) => fn thy =>
687 (Sign.intern_type thy name,
688 map (inter_sort thy sort o snd) tvs, [cp_class])
689 (EVERY [Class.intro_classes_tac [],
690 rewrite_goals_tac [perm_def],
691 asm_full_simp_tac (global_simpset_of thy addsimps
692 ((Rep RS perm_closed1 RS Abs_inverse) ::
693 (if atom1 = atom2 then []
694 else [Rep RS perm_closed2 RS Abs_inverse]))) 1,
698 (Abs_inverse_thms ~~ Rep_thms ~~ perm_defs ~~ new_type_names ~~
699 tyvars ~~ perm_closed_thms1 ~~ perm_closed_thms2) thy
702 val thy7 = fold (fn x => fn thy => thy |>
704 fold (cp_instance x) (atoms ~~ perm_closed_thmss))
705 (atoms ~~ perm_closed_thmss) thy6;
707 (**** constructors ****)
711 val T = fastype_of x;
714 Const ("Nominal.abs_fun", T --> U --> T -->
715 Type ("Nominal.noption", [U])) $ x $ t
718 val (ty_idxs, _) = List.foldl
719 (fn ((i, ("Nominal.noption", _, _)), p) => p
720 | ((i, _), (ty_idxs, j)) => (ty_idxs @ [(i, j)], j + 1)) ([], 0) descr;
722 fun reindex (DtType (s, dts)) = DtType (s, map reindex dts)
723 | reindex (DtRec i) = DtRec (the (AList.lookup op = ty_idxs i))
726 fun strip_suffix i s = implode (List.take (raw_explode s, size s - i)); (* FIXME Symbol.explode (?) *)
728 (** strips the "_Rep" in type names *)
729 fun strip_nth_name i s =
730 let val xs = Long_Name.explode s;
731 in Long_Name.implode (Library.nth_map (length xs - i) (strip_suffix 4) xs) end;
733 val (descr'', ndescr) = ListPair.unzip (map_filter
734 (fn (i, ("Nominal.noption", _, _)) => NONE
735 | (i, (s, dts, constrs)) =>
737 val SOME index = AList.lookup op = ty_idxs i;
738 val (constrs2, constrs1) =
739 map_split (fn (cname, cargs) =>
740 apsnd (pair (strip_nth_name 2 (strip_nth_name 1 cname)))
741 (fold_map (fn dt => fn dts =>
742 let val (dts', dt') = strip_option dt
743 in ((length dts, length dts'), dts @ dts' @ [reindex dt']) end)
745 in SOME ((index, (strip_nth_name 1 s, map reindex dts, constrs1)),
749 val (descr1, descr2) = chop (length new_type_names) descr'';
750 val descr' = [descr1, descr2];
752 fun partition_cargs idxs xs = map (fn (i, j) =>
753 (List.take (List.drop (xs, i), j), nth xs (i + j))) idxs;
755 val pdescr = map (fn ((i, (s, dts, constrs)), (_, idxss)) => (i, (s, dts,
756 map (fn ((cname, cargs), idxs) => (cname, partition_cargs idxs cargs))
757 (constrs ~~ idxss)))) (descr'' ~~ ndescr);
759 fun nth_dtyp' i = typ_of_dtyp descr'' sorts (DtRec i);
761 val rep_names = map (fn s =>
762 Sign.intern_const thy7 ("Rep_" ^ s)) new_type_names;
763 val abs_names = map (fn s =>
764 Sign.intern_const thy7 ("Abs_" ^ s)) new_type_names;
766 val recTs = get_rec_types descr'' sorts;
767 val newTs' = take (length new_type_names) recTs';
768 val newTs = take (length new_type_names) recTs;
770 val full_new_type_names = map (Sign.full_bname thy) new_type_names;
772 fun make_constr_def tname T T' (((cname_rep, _), (cname, cargs)), (cname', mx))
775 fun constr_arg (dts, dt) (j, l_args, r_args) =
777 val xs = map (fn (dt, i) => mk_Free "x" (typ_of_dtyp descr'' sorts dt) i)
778 (dts ~~ (j upto j + length dts - 1))
779 val x = mk_Free "x" (typ_of_dtyp descr'' sorts dt) (j + length dts)
783 fold_rev mk_abs_fun xs
785 DtRec k => if k < length new_type_names then
786 Const (nth rep_names k, typ_of_dtyp descr'' sorts dt -->
787 typ_of_dtyp descr sorts dt) $ x
788 else error "nested recursion not (yet) supported"
792 val (_, l_args, r_args) = fold_rev constr_arg cargs (1, [], []);
793 val abs_name = Sign.intern_const thy ("Abs_" ^ tname);
794 val rep_name = Sign.intern_const thy ("Rep_" ^ tname);
795 val constrT = map fastype_of l_args ---> T;
796 val lhs = list_comb (Const (cname, constrT), l_args);
797 val rhs = list_comb (Const (cname_rep, map fastype_of r_args ---> T'), r_args);
798 val def = Logic.mk_equals (lhs, Const (abs_name, T' --> T) $ rhs);
799 val eqn = HOLogic.mk_Trueprop (HOLogic.mk_eq
800 (Const (rep_name, T --> T') $ lhs, rhs));
801 val def_name = (Long_Name.base_name cname) ^ "_def";
802 val ([def_thm], thy') = thy |>
803 Sign.add_consts_i [(Binding.name cname', constrT, mx)] |>
804 (Global_Theory.add_defs false o map Thm.no_attributes) [(Binding.name def_name, def)]
805 in (thy', defs @ [def_thm], eqns @ [eqn]) end;
807 fun dt_constr_defs ((((((_, (_, _, constrs)),
808 (_, (_, _, constrs'))), tname), T), T'), constr_syntax) (thy, defs, eqns, dist_lemmas) =
810 val rep_const = cterm_of thy
811 (Const (Sign.intern_const thy ("Rep_" ^ tname), T --> T'));
813 Drule.export_without_context
814 (cterm_instantiate [(cterm_of thy distinct_f, rep_const)] distinct_lemma);
815 val (thy', defs', eqns') = fold (make_constr_def tname T T')
816 (constrs ~~ constrs' ~~ constr_syntax) (Sign.add_path tname thy, defs, [])
818 (Sign.parent_path thy', defs', eqns @ [eqns'], dist_lemmas @ [dist])
821 val (thy8, constr_defs, constr_rep_eqns, dist_lemmas) = fold dt_constr_defs
822 (List.take (descr, length new_type_names) ~~
823 List.take (pdescr, length new_type_names) ~~
824 new_type_names ~~ newTs ~~ newTs' ~~ constr_syntax)
827 val abs_inject_thms = map (collect_simp o #Abs_inject o snd o fst) typedefs
828 val rep_inject_thms = map (#Rep_inject o snd o fst) typedefs
830 (* prove theorem Rep_i (Constr_j ...) = Constr'_j ... *)
832 fun prove_constr_rep_thm eqn =
834 val inj_thms = map (fn r => r RS iffD1) abs_inject_thms;
835 val rewrites = constr_defs @ map mk_meta_eq Rep_inverse_thms
836 in Goal.prove_global thy8 [] [] eqn (fn _ => EVERY
837 [resolve_tac inj_thms 1,
838 rewrite_goals_tac rewrites,
840 resolve_tac rep_intrs 2,
841 REPEAT (resolve_tac Rep_thms 1)])
844 val constr_rep_thmss = map (map prove_constr_rep_thm) constr_rep_eqns;
846 (* prove theorem pi \<bullet> Rep_i x = Rep_i (pi \<bullet> x) *)
848 fun prove_perm_rep_perm (atom, perm_closed_thms) = map (fn th =>
850 val _ $ (_ $ (Rep $ x)) = Logic.unvarify_global (prop_of th);
851 val Type ("fun", [T, U]) = fastype_of Rep;
852 val permT = mk_permT (Type (atom, []));
853 val pi = Free ("pi", permT);
855 Goal.prove_global thy8 [] []
857 (pt_class_of thy8 atom :: map (cp_class_of thy8 atom) (remove (op =) atom dt_atoms))
858 (HOLogic.mk_Trueprop (HOLogic.mk_eq
859 (Const ("Nominal.perm", permT --> U --> U) $ pi $ (Rep $ x),
860 Rep $ (Const ("Nominal.perm", permT --> T --> T) $ pi $ x)))))
861 (fn _ => simp_tac (HOL_basic_ss addsimps (perm_defs @ Abs_inverse_thms @
862 perm_closed_thms @ Rep_thms)) 1)
865 val perm_rep_perm_thms = maps prove_perm_rep_perm (atoms ~~ perm_closed_thmss);
867 (* prove distinctness theorems *)
869 val distinct_props = Datatype_Prop.make_distincts descr' sorts;
870 val dist_rewrites = map2 (fn rep_thms => fn dist_lemma =>
871 dist_lemma :: rep_thms @ [In0_eq, In1_eq, In0_not_In1, In1_not_In0])
872 constr_rep_thmss dist_lemmas;
874 fun prove_distinct_thms _ (_, []) = []
875 | prove_distinct_thms (p as (rep_thms, dist_lemma)) (k, t :: ts) =
877 val dist_thm = Goal.prove_global thy8 [] [] t (fn _ =>
878 simp_tac (global_simpset_of thy8 addsimps (dist_lemma :: rep_thms)) 1)
880 dist_thm :: Drule.export_without_context (dist_thm RS not_sym) ::
881 prove_distinct_thms p (k, ts)
884 val distinct_thms = map2 prove_distinct_thms
885 (constr_rep_thmss ~~ dist_lemmas) distinct_props;
887 (** prove equations for permutation functions **)
889 val perm_simps' = map (fn (((i, (_, _, constrs)), tname), constr_rep_thms) =>
890 let val T = nth_dtyp' i
891 in maps (fn (atom, perm_closed_thms) =>
892 map (fn ((cname, dts), constr_rep_thm) =>
894 val cname = Sign.intern_const thy8
895 (Long_Name.append tname (Long_Name.base_name cname));
896 val permT = mk_permT (Type (atom, []));
897 val pi = Free ("pi", permT);
900 let val T = fastype_of t
901 in Const ("Nominal.perm", permT --> T --> T) $ pi $ t end;
903 fun constr_arg (dts, dt) (j, l_args, r_args) =
905 val Ts = map (typ_of_dtyp descr'' sorts) dts;
906 val xs = map (fn (T, i) => mk_Free "x" T i)
907 (Ts ~~ (j upto j + length dts - 1))
908 val x = mk_Free "x" (typ_of_dtyp descr'' sorts dt) (j + length dts)
912 map perm (xs @ [x]) @ r_args)
915 val (_, l_args, r_args) = fold_rev constr_arg dts (1, [], []);
916 val c = Const (cname, map fastype_of l_args ---> T)
918 Goal.prove_global thy8 [] []
920 (pt_class_of thy8 atom :: map (cp_class_of thy8 atom) (remove (op =) atom dt_atoms))
921 (HOLogic.mk_Trueprop (HOLogic.mk_eq
922 (perm (list_comb (c, l_args)), list_comb (c, r_args)))))
924 [simp_tac (global_simpset_of thy8 addsimps (constr_rep_thm :: perm_defs)) 1,
925 simp_tac (HOL_basic_ss addsimps (Rep_thms @ Abs_inverse_thms @
926 constr_defs @ perm_closed_thms)) 1,
927 TRY (simp_tac (HOL_basic_ss addsimps
928 (Thm.symmetric perm_fun_def :: abs_perm)) 1),
929 TRY (simp_tac (HOL_basic_ss addsimps
930 (perm_fun_def :: perm_defs @ Rep_thms @ Abs_inverse_thms @
931 perm_closed_thms)) 1)])
932 end) (constrs ~~ constr_rep_thms)) (atoms ~~ perm_closed_thmss)
933 end) (List.take (pdescr, length new_type_names) ~~ new_type_names ~~ constr_rep_thmss);
935 (** prove injectivity of constructors **)
937 val rep_inject_thms' = map (fn th => th RS sym) rep_inject_thms;
938 val alpha = Global_Theory.get_thms thy8 "alpha";
939 val abs_fresh = Global_Theory.get_thms thy8 "abs_fresh";
942 map (pt_class_of thy8) dt_atoms @
943 maps (fn s => map (cp_class_of thy8 s) (remove (op =) s dt_atoms)) dt_atoms;
945 val inject_thms = map (fn (((i, (_, _, constrs)), tname), constr_rep_thms) =>
946 let val T = nth_dtyp' i
947 in map_filter (fn ((cname, dts), constr_rep_thm) =>
948 if null dts then NONE else SOME
950 val cname = Sign.intern_const thy8
951 (Long_Name.append tname (Long_Name.base_name cname));
953 fun make_inj (dts, dt) (j, args1, args2, eqs) =
955 val Ts_idx = map (typ_of_dtyp descr'' sorts) dts ~~ (j upto j + length dts - 1);
956 val xs = map (fn (T, i) => mk_Free "x" T i) Ts_idx;
957 val ys = map (fn (T, i) => mk_Free "y" T i) Ts_idx;
958 val x = mk_Free "x" (typ_of_dtyp descr'' sorts dt) (j + length dts);
959 val y = mk_Free "y" (typ_of_dtyp descr'' sorts dt) (j + length dts)
962 xs @ (x :: args1), ys @ (y :: args2),
964 (fold_rev mk_abs_fun xs x, fold_rev mk_abs_fun ys y) :: eqs)
967 val (_, args1, args2, eqs) = fold_rev make_inj dts (1, [], [], []);
968 val Ts = map fastype_of args1;
969 val c = Const (cname, Ts ---> T)
971 Goal.prove_global thy8 [] []
972 (augment_sort thy8 pt_cp_sort
973 (HOLogic.mk_Trueprop (HOLogic.mk_eq
974 (HOLogic.mk_eq (list_comb (c, args1), list_comb (c, args2)),
975 foldr1 HOLogic.mk_conj eqs))))
977 [asm_full_simp_tac (global_simpset_of thy8 addsimps (constr_rep_thm ::
978 rep_inject_thms')) 1,
979 TRY (asm_full_simp_tac (HOL_basic_ss addsimps (fresh_def :: supp_def ::
980 alpha @ abs_perm @ abs_fresh @ rep_inject_thms @
981 perm_rep_perm_thms)) 1)])
982 end) (constrs ~~ constr_rep_thms)
983 end) (List.take (pdescr, length new_type_names) ~~ new_type_names ~~ constr_rep_thmss);
985 (** equations for support and freshness **)
987 val (supp_thms, fresh_thms) = ListPair.unzip (map ListPair.unzip
988 (map (fn ((((i, (_, _, constrs)), tname), inject_thms'), perm_thms') =>
989 let val T = nth_dtyp' i
990 in maps (fn (cname, dts) => map (fn atom =>
992 val cname = Sign.intern_const thy8
993 (Long_Name.append tname (Long_Name.base_name cname));
994 val atomT = Type (atom, []);
996 fun process_constr (dts, dt) (j, args1, args2) =
998 val Ts_idx = map (typ_of_dtyp descr'' sorts) dts ~~ (j upto j + length dts - 1);
999 val xs = map (fn (T, i) => mk_Free "x" T i) Ts_idx;
1000 val x = mk_Free "x" (typ_of_dtyp descr'' sorts dt) (j + length dts)
1002 (j + length dts + 1,
1003 xs @ (x :: args1), fold_rev mk_abs_fun xs x :: args2)
1006 val (_, args1, args2) = fold_rev process_constr dts (1, [], []);
1007 val Ts = map fastype_of args1;
1008 val c = list_comb (Const (cname, Ts ---> T), args1);
1010 Const ("Nominal.supp", fastype_of t --> HOLogic.mk_setT atomT) $ t;
1011 fun fresh t = fresh_const atomT (fastype_of t) $ Free ("a", atomT) $ t;
1012 val supp_thm = Goal.prove_global thy8 [] []
1013 (augment_sort thy8 pt_cp_sort
1014 (HOLogic.mk_Trueprop (HOLogic.mk_eq
1016 if null dts then HOLogic.mk_set atomT []
1017 else foldr1 (HOLogic.mk_binop @{const_abbrev union}) (map supp args2)))))
1019 simp_tac (HOL_basic_ss addsimps (supp_def ::
1020 Un_assoc :: de_Morgan_conj :: Collect_disj_eq :: finite_Un ::
1021 Collect_False_empty :: finite_emptyI :: simp_thms @
1022 abs_perm @ abs_fresh @ inject_thms' @ perm_thms')) 1)
1025 Goal.prove_global thy8 [] [] (augment_sort thy8 pt_cp_sort
1026 (HOLogic.mk_Trueprop (HOLogic.mk_eq
1028 if null dts then HOLogic.true_const
1029 else foldr1 HOLogic.mk_conj (map fresh args2)))))
1031 simp_tac (HOL_ss addsimps [Un_iff, empty_iff, fresh_def, supp_thm]) 1))
1033 end) (List.take (pdescr, length new_type_names) ~~ new_type_names ~~ inject_thms ~~ perm_simps')));
1035 (**** weak induction theorem ****)
1037 fun mk_indrule_lemma (((i, _), T), U) (prems, concls) =
1039 val Rep_t = Const (nth rep_names i, T --> U) $ mk_Free "x" T i;
1041 val Abs_t = Const (nth abs_names i, U --> T);
1043 in (prems @ [HOLogic.imp $
1044 (Const (nth rep_set_names'' i, U --> HOLogic.boolT) $ Rep_t) $
1045 (mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ (Abs_t $ Rep_t))],
1046 concls @ [mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ mk_Free "x" T i])
1049 val (indrule_lemma_prems, indrule_lemma_concls) =
1050 fold mk_indrule_lemma (descr'' ~~ recTs ~~ recTs') ([], []);
1052 val indrule_lemma = Goal.prove_global thy8 [] []
1054 (HOLogic.mk_Trueprop (mk_conj indrule_lemma_prems),
1055 HOLogic.mk_Trueprop (mk_conj indrule_lemma_concls))) (fn _ => EVERY
1056 [REPEAT (etac conjE 1),
1058 [TRY (rtac conjI 1), full_simp_tac (HOL_basic_ss addsimps Rep_inverse_thms) 1,
1059 etac mp 1, resolve_tac Rep_thms 1])]);
1061 val Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of indrule_lemma)));
1062 val frees = if length Ps = 1 then [Free ("P", snd (dest_Var (hd Ps)))] else
1063 map (Free o apfst fst o dest_Var) Ps;
1064 val indrule_lemma' = cterm_instantiate
1065 (map (cterm_of thy8) Ps ~~ map (cterm_of thy8) frees) indrule_lemma;
1067 val Abs_inverse_thms' = map (fn r => r RS subst) Abs_inverse_thms;
1069 val dt_induct_prop = Datatype_Prop.make_ind descr' sorts;
1070 val dt_induct = Goal.prove_global thy8 []
1071 (Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop)
1072 (fn {prems, ...} => EVERY
1073 [rtac indrule_lemma' 1,
1074 (indtac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
1075 EVERY (map (fn (prem, r) => (EVERY
1076 [REPEAT (eresolve_tac Abs_inverse_thms' 1),
1077 simp_tac (HOL_basic_ss addsimps [Thm.symmetric r]) 1,
1078 DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE etac allE 1)]))
1079 (prems ~~ constr_defs))]);
1081 val case_names_induct = mk_case_names_induct descr'';
1083 (**** prove that new datatypes have finite support ****)
1085 val _ = warning "proving finite support for the new datatype";
1087 val indnames = Datatype_Prop.make_tnames recTs;
1089 val abs_supp = Global_Theory.get_thms thy8 "abs_supp";
1090 val supp_atm = Global_Theory.get_thms thy8 "supp_atm";
1092 val finite_supp_thms = map (fn atom =>
1093 let val atomT = Type (atom, [])
1094 in map Drule.export_without_context (List.take
1095 (split_conj_thm (Goal.prove_global thy8 [] []
1096 (augment_sort thy8 (fs_class_of thy8 atom :: pt_cp_sort)
1097 (HOLogic.mk_Trueprop
1098 (foldr1 HOLogic.mk_conj (map (fn (s, T) =>
1099 Const ("Finite_Set.finite", HOLogic.mk_setT atomT --> HOLogic.boolT) $
1100 (Const ("Nominal.supp", T --> HOLogic.mk_setT atomT) $ Free (s, T)))
1101 (indnames ~~ recTs)))))
1102 (fn _ => indtac dt_induct indnames 1 THEN
1103 ALLGOALS (asm_full_simp_tac (global_simpset_of thy8 addsimps
1104 (abs_supp @ supp_atm @
1105 Global_Theory.get_thms thy8 ("fs_" ^ Long_Name.base_name atom ^ "1") @
1106 flat supp_thms))))),
1107 length new_type_names))
1110 val simp_atts = replicate (length new_type_names) [Simplifier.simp_add];
1112 (* Function to add both the simp and eqvt attributes *)
1113 (* These two attributes are duplicated on all the types in the mutual nominal datatypes *)
1115 val simp_eqvt_atts = replicate (length new_type_names) [Simplifier.simp_add, NominalThmDecls.eqvt_add];
1117 val (_, thy9) = thy8 |>
1118 Sign.add_path big_name |>
1119 Global_Theory.add_thms [((Binding.name "induct", dt_induct), [case_names_induct])] ||>>
1120 Global_Theory.add_thmss [((Binding.name "inducts", projections dt_induct), [case_names_induct])] ||>
1121 Sign.parent_path ||>>
1122 Datatype_Aux.store_thmss_atts "distinct" new_type_names simp_atts distinct_thms ||>>
1123 Datatype_Aux.store_thmss "constr_rep" new_type_names constr_rep_thmss ||>>
1124 Datatype_Aux.store_thmss_atts "perm" new_type_names simp_eqvt_atts perm_simps' ||>>
1125 Datatype_Aux.store_thmss "inject" new_type_names inject_thms ||>>
1126 Datatype_Aux.store_thmss "supp" new_type_names supp_thms ||>>
1127 Datatype_Aux.store_thmss_atts "fresh" new_type_names simp_atts fresh_thms ||>
1128 fold (fn (atom, ths) => fn thy =>
1130 val class = fs_class_of thy atom;
1131 val sort = Sign.minimize_sort thy (Sign.certify_sort thy (class :: pt_cp_sort));
1132 in fold (fn Type (s, Ts) => AxClass.prove_arity
1133 (s, map (inter_sort thy sort o snd o dest_TFree) Ts, [class])
1134 (Class.intro_classes_tac [] THEN resolve_tac ths 1)) newTs thy
1135 end) (atoms ~~ finite_supp_thms);
1137 (**** strong induction theorem ****)
1139 val pnames = if length descr'' = 1 then ["P"]
1140 else map (fn i => "P" ^ string_of_int i) (1 upto length descr'');
1141 val ind_sort = if null dt_atomTs then HOLogic.typeS
1142 else Sign.minimize_sort thy9 (Sign.certify_sort thy9 (map (fs_class_of thy9) dt_atoms));
1143 val fsT = TFree ("'n", ind_sort);
1144 val fsT' = TFree ("'n", HOLogic.typeS);
1146 val fresh_fs = map (fn (s, T) => (T, Free (s, fsT' --> HOLogic.mk_setT T)))
1147 (Datatype_Prop.indexify_names (replicate (length dt_atomTs) "f") ~~ dt_atomTs);
1149 fun make_pred fsT i T = Free (nth pnames i, fsT --> T --> HOLogic.boolT);
1151 fun mk_fresh1 xs [] = []
1152 | mk_fresh1 xs ((y as (_, T)) :: ys) = map (fn x => HOLogic.mk_Trueprop
1153 (HOLogic.mk_not (HOLogic.mk_eq (Free y, Free x))))
1154 (filter (fn (_, U) => T = U) (rev xs)) @
1155 mk_fresh1 (y :: xs) ys;
1157 fun mk_fresh2 xss [] = []
1158 | mk_fresh2 xss ((p as (ys, _)) :: yss) = maps (fn y as (_, T) =>
1159 map (fn (_, x as (_, U)) => HOLogic.mk_Trueprop
1160 (fresh_const T U $ Free y $ Free x)) (rev xss @ yss)) ys @
1161 mk_fresh2 (p :: xss) yss;
1163 fun make_ind_prem fsT f k T ((cname, cargs), idxs) =
1165 val recs = filter is_rec_type cargs;
1166 val Ts = map (typ_of_dtyp descr'' sorts) cargs;
1167 val recTs' = map (typ_of_dtyp descr'' sorts) recs;
1168 val tnames = Name.variant_list pnames (Datatype_Prop.make_tnames Ts);
1169 val rec_tnames = map fst (filter (is_rec_type o snd) (tnames ~~ cargs));
1170 val frees = tnames ~~ Ts;
1171 val frees' = partition_cargs idxs frees;
1172 val z = (singleton (Name.variant_list tnames) "z", fsT);
1174 fun mk_prem ((dt, s), T) =
1176 val (Us, U) = strip_type T;
1178 in list_all (z :: map (pair "x") Us, HOLogic.mk_Trueprop
1179 (make_pred fsT (body_index dt) U $ Bound l $ app_bnds (Free (s, T)) l))
1182 val prems = map mk_prem (recs ~~ rec_tnames ~~ recTs');
1183 val prems' = map (fn p as (_, T) => HOLogic.mk_Trueprop
1184 (f T (Free p) (Free z))) (maps fst frees') @
1185 mk_fresh1 [] (maps fst frees') @
1188 in list_all_free (frees @ [z], Logic.list_implies (prems' @ prems,
1189 HOLogic.mk_Trueprop (make_pred fsT k T $ Free z $
1190 list_comb (Const (cname, Ts ---> T), map Free frees))))
1193 val ind_prems = maps (fn (((i, (_, _, constrs)), (_, idxss)), T) =>
1194 map (make_ind_prem fsT (fn T => fn t => fn u =>
1195 fresh_const T fsT $ t $ u) i T)
1196 (constrs ~~ idxss)) (descr'' ~~ ndescr ~~ recTs);
1197 val tnames = Datatype_Prop.make_tnames recTs;
1198 val zs = Name.variant_list tnames (replicate (length descr'') "z");
1199 val ind_concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name HOL.conj})
1200 (map (fn ((((i, _), T), tname), z) =>
1201 make_pred fsT i T $ Free (z, fsT) $ Free (tname, T))
1202 (descr'' ~~ recTs ~~ tnames ~~ zs)));
1203 val induct = Logic.list_implies (ind_prems, ind_concl);
1206 map (fn (_, f as Free (_, T)) => list_all_free ([("x", fsT')],
1207 HOLogic.mk_Trueprop (Const ("Finite_Set.finite",
1208 (List.last (binder_types T) --> HOLogic.boolT) -->
1209 HOLogic.boolT) $ (f $ Free ("x", fsT'))))) fresh_fs @
1210 maps (fn (((i, (_, _, constrs)), (_, idxss)), T) =>
1211 map (make_ind_prem fsT' (fn T => fn t => fn u => HOLogic.Not $
1212 HOLogic.mk_mem (t, the (AList.lookup op = fresh_fs T) $ u)) i T)
1213 (constrs ~~ idxss)) (descr'' ~~ ndescr ~~ recTs);
1214 val ind_concl' = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name HOL.conj})
1215 (map (fn ((((i, _), T), tname), z) =>
1216 make_pred fsT' i T $ Free (z, fsT') $ Free (tname, T))
1217 (descr'' ~~ recTs ~~ tnames ~~ zs)));
1218 val induct' = Logic.list_implies (ind_prems', ind_concl');
1221 (Datatype_Prop.indexify_names (replicate (length dt_atomTs) "pi") ~~
1222 map mk_permT dt_atomTs) @ [("z", fsT')];
1223 val aux_ind_Ts = rev (map snd aux_ind_vars);
1224 val aux_ind_concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name HOL.conj})
1225 (map (fn (((i, _), T), tname) =>
1226 HOLogic.list_all (aux_ind_vars, make_pred fsT' i T $ Bound 0 $
1227 fold_rev (mk_perm aux_ind_Ts) (map Bound (length dt_atomTs downto 1))
1229 (descr'' ~~ recTs ~~ tnames)));
1231 val fin_set_supp = map (fn s =>
1232 at_inst_of thy9 s RS at_fin_set_supp) dt_atoms;
1233 val fin_set_fresh = map (fn s =>
1234 at_inst_of thy9 s RS at_fin_set_fresh) dt_atoms;
1235 val pt1_atoms = map (fn Type (s, _) =>
1236 Global_Theory.get_thm thy9 ("pt_" ^ Long_Name.base_name s ^ "1")) dt_atomTs;
1237 val pt2_atoms = map (fn Type (s, _) =>
1238 Global_Theory.get_thm thy9 ("pt_" ^ Long_Name.base_name s ^ "2") RS sym) dt_atomTs;
1239 val exists_fresh' = Global_Theory.get_thms thy9 "exists_fresh'";
1240 val fs_atoms = Global_Theory.get_thms thy9 "fin_supp";
1241 val abs_supp = Global_Theory.get_thms thy9 "abs_supp";
1242 val perm_fresh_fresh = Global_Theory.get_thms thy9 "perm_fresh_fresh";
1243 val calc_atm = Global_Theory.get_thms thy9 "calc_atm";
1244 val fresh_atm = Global_Theory.get_thms thy9 "fresh_atm";
1245 val fresh_left = Global_Theory.get_thms thy9 "fresh_left";
1246 val perm_swap = Global_Theory.get_thms thy9 "perm_swap";
1248 fun obtain_fresh_name' ths ts T (freshs1, freshs2, ctxt) =
1250 val p = foldr1 HOLogic.mk_prod (ts @ freshs1);
1251 val ex = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop
1252 (HOLogic.exists_const T $ Abs ("x", T,
1253 fresh_const T (fastype_of p) $
1256 [resolve_tac exists_fresh' 1,
1257 simp_tac (HOL_ss addsimps (supp_prod :: finite_Un :: fs_atoms @
1258 fin_set_supp @ ths)) 1]);
1259 val (([(_, cx)], ths), ctxt') = Obtain.result
1262 full_simp_tac (HOL_ss addsimps (fresh_prod :: fresh_atm)) 1,
1263 REPEAT (etac conjE 1)])
1265 in (freshs1 @ [term_of cx], freshs2 @ ths, ctxt') end;
1267 fun fresh_fresh_inst thy a b =
1269 val T = fastype_of a;
1270 val SOME th = find_first (fn th => case prop_of th of
1271 _ $ (_ $ (Const (_, Type (_, [U, _])) $ _ $ _)) $ _ => U = T
1272 | _ => false) perm_fresh_fresh
1274 Drule.instantiate' []
1275 [SOME (cterm_of thy a), NONE, SOME (cterm_of thy b)] th
1279 map (fs_class_of thy9) dt_atoms @
1280 maps (fn s => map (cp_class_of thy9 s) (remove (op =) s dt_atoms)) dt_atoms;
1282 (**********************************************************************
1283 The subgoals occurring in the proof of induct_aux have the
1284 following parameters:
1286 x_1 ... x_k p_1 ... p_m z
1290 x_i : constructor arguments (introduced by weak induction rule)
1291 p_i : permutations (one for each atom type in the data type)
1292 z : freshness context
1293 ***********************************************************************)
1295 val _ = warning "proving strong induction theorem ...";
1297 val induct_aux = Goal.prove_global thy9 []
1298 (map (augment_sort thy9 fs_cp_sort) ind_prems')
1299 (augment_sort thy9 fs_cp_sort ind_concl') (fn {prems, context} =>
1301 val (prems1, prems2) = chop (length dt_atomTs) prems;
1302 val ind_ss2 = HOL_ss addsimps
1303 finite_Diff :: abs_fresh @ abs_supp @ fs_atoms;
1304 val ind_ss1 = ind_ss2 addsimps fresh_left @ calc_atm @
1305 fresh_atm @ rev_simps @ app_simps;
1306 val ind_ss3 = HOL_ss addsimps abs_fun_eq1 ::
1307 abs_perm @ calc_atm @ perm_swap;
1308 val ind_ss4 = HOL_basic_ss addsimps fresh_left @ prems1 @
1309 fin_set_fresh @ calc_atm;
1310 val ind_ss5 = HOL_basic_ss addsimps pt1_atoms;
1311 val ind_ss6 = HOL_basic_ss addsimps flat perm_simps';
1312 val th = Goal.prove context [] []
1313 (augment_sort thy9 fs_cp_sort aux_ind_concl)
1314 (fn {context = context1, ...} =>
1315 EVERY (indtac dt_induct tnames 1 ::
1316 maps (fn ((_, (_, _, constrs)), (_, constrs')) =>
1317 map (fn ((cname, cargs), is) =>
1318 REPEAT (rtac allI 1) THEN
1319 SUBPROOF (fn {prems = iprems, params, concl,
1320 context = context2, ...} =>
1322 val concl' = term_of concl;
1323 val _ $ (_ $ _ $ u) = concl';
1324 val U = fastype_of u;
1326 chop (length cargs) (map (term_of o #2) params);
1327 val Ts = map fastype_of xs;
1328 val cnstr = Const (cname, Ts ---> U);
1329 val (pis, z) = split_last params';
1330 val mk_pi = fold_rev (mk_perm []) pis;
1331 val xs' = partition_cargs is xs;
1332 val xs'' = map (fn (ts, u) => (map mk_pi ts, mk_pi u)) xs';
1333 val ts = maps (fn (ts, u) => ts @ [u]) xs'';
1334 val (freshs1, freshs2, context3) = fold (fn t =>
1335 let val T = fastype_of t
1336 in obtain_fresh_name' prems1
1337 (the (AList.lookup op = fresh_fs T) $ z :: ts) T
1338 end) (maps fst xs') ([], [], context2);
1339 val freshs1' = unflat (map fst xs') freshs1;
1340 val freshs2' = map (Simplifier.simplify ind_ss4)
1341 (mk_not_sym freshs2);
1342 val ind_ss1' = ind_ss1 addsimps freshs2';
1343 val ind_ss3' = ind_ss3 addsimps freshs2';
1345 if forall (null o fst) xs' then []
1346 else [Goal.prove context3 [] []
1347 (HOLogic.mk_Trueprop (HOLogic.mk_eq
1348 (list_comb (cnstr, ts),
1349 list_comb (cnstr, maps (fn ((bs, t), cs) =>
1350 cs @ [fold_rev (mk_perm []) (map perm_of_pair
1351 (bs ~~ cs)) t]) (xs'' ~~ freshs1')))))
1353 (simp_tac (HOL_ss addsimps flat inject_thms) 1 ::
1354 REPEAT (FIRSTGOAL (rtac conjI)) ::
1355 maps (fn ((bs, t), cs) =>
1357 else rtac sym 1 :: maps (fn (b, c) =>
1358 [rtac trans 1, rtac sym 1,
1359 rtac (fresh_fresh_inst thy9 b c) 1,
1360 simp_tac ind_ss1' 1,
1362 simp_tac ind_ss3' 1]) (bs ~~ cs))
1363 (xs'' ~~ freshs1')))];
1364 val th = Goal.prove context3 [] [] concl' (fn _ => EVERY
1365 [simp_tac (ind_ss6 addsimps rename_eq) 1,
1366 cut_facts_tac iprems 1,
1367 (resolve_tac prems THEN_ALL_NEW
1368 SUBGOAL (fn (t, i) => case Logic.strip_assums_concl t of
1369 _ $ (Const ("Nominal.fresh", _) $ _ $ _) =>
1371 | _ $ (Const (@{const_name Not}, _) $ _) =>
1372 resolve_tac freshs2' i
1373 | _ => asm_simp_tac (HOL_basic_ss addsimps
1374 pt2_atoms addsimprocs [perm_simproc]) i)) 1])
1375 val final = Proof_Context.export context3 context2 [th]
1378 end) context1 1) (constrs ~~ constrs')) (descr'' ~~ ndescr)))
1381 [cut_facts_tac [th] 1,
1382 REPEAT (eresolve_tac [conjE, @{thm allE_Nil}] 1),
1383 REPEAT (etac allE 1),
1384 REPEAT (TRY (rtac conjI 1) THEN asm_full_simp_tac ind_ss5 1)]
1387 val induct_aux' = Thm.instantiate ([],
1388 map (fn (s, v as Var (_, T)) =>
1389 (cterm_of thy9 v, cterm_of thy9 (Free (s, T))))
1390 (pnames ~~ map head_of (HOLogic.dest_conj
1391 (HOLogic.dest_Trueprop (concl_of induct_aux)))) @
1393 let val f' = Logic.varify_global f
1394 in (cterm_of thy9 f',
1395 cterm_of thy9 (Const ("Nominal.supp", fastype_of f')))
1396 end) fresh_fs) induct_aux;
1398 val induct = Goal.prove_global thy9 []
1399 (map (augment_sort thy9 fs_cp_sort) ind_prems)
1400 (augment_sort thy9 fs_cp_sort ind_concl)
1401 (fn {prems, ...} => EVERY
1402 [rtac induct_aux' 1,
1403 REPEAT (resolve_tac fs_atoms 1),
1404 REPEAT ((resolve_tac prems THEN_ALL_NEW
1405 (etac @{thm meta_spec} ORELSE' full_simp_tac (HOL_basic_ss addsimps [fresh_def]))) 1)])
1407 val (_, thy10) = thy9 |>
1408 Sign.add_path big_name |>
1409 Global_Theory.add_thms [((Binding.name "strong_induct'", induct_aux), [])] ||>>
1410 Global_Theory.add_thms [((Binding.name "strong_induct", induct), [case_names_induct])] ||>>
1411 Global_Theory.add_thmss [((Binding.name "strong_inducts", projections induct), [case_names_induct])];
1413 (**** recursion combinator ****)
1415 val _ = warning "defining recursion combinator ...";
1417 val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
1419 val (rec_result_Ts', rec_fn_Ts') = Datatype_Prop.make_primrec_Ts descr' sorts used;
1421 val rec_sort = if null dt_atomTs then HOLogic.typeS else
1422 Sign.minimize_sort thy10 (Sign.certify_sort thy10 pt_cp_sort);
1424 val rec_result_Ts = map (fn TFree (s, _) => TFree (s, rec_sort)) rec_result_Ts';
1425 val rec_fn_Ts = map (typ_subst_atomic (rec_result_Ts' ~~ rec_result_Ts)) rec_fn_Ts';
1427 val rec_set_Ts = map (fn (T1, T2) =>
1428 rec_fn_Ts @ [T1, T2] ---> HOLogic.boolT) (recTs ~~ rec_result_Ts);
1430 val big_rec_name = big_name ^ "_rec_set";
1431 val rec_set_names' =
1432 if length descr'' = 1 then [big_rec_name] else
1433 map ((curry (op ^) (big_rec_name ^ "_")) o string_of_int)
1434 (1 upto (length descr''));
1435 val rec_set_names = map (Sign.full_bname thy10) rec_set_names';
1437 val rec_fns = map (uncurry (mk_Free "f"))
1438 (rec_fn_Ts ~~ (1 upto (length rec_fn_Ts)));
1439 val rec_sets' = map (fn c => list_comb (Free c, rec_fns))
1440 (rec_set_names' ~~ rec_set_Ts);
1441 val rec_sets = map (fn c => list_comb (Const c, rec_fns))
1442 (rec_set_names ~~ rec_set_Ts);
1444 (* introduction rules for graph of recursion function *)
1446 val rec_preds = map (fn (a, T) =>
1447 Free (a, T --> HOLogic.boolT)) (pnames ~~ rec_result_Ts);
1449 fun mk_fresh3 rs [] = []
1450 | mk_fresh3 rs ((p as (ys, z)) :: yss) = maps (fn y as (_, T) =>
1451 map_filter (fn ((_, (_, x)), r as (_, U)) => if z = x then NONE
1452 else SOME (HOLogic.mk_Trueprop
1453 (fresh_const T U $ Free y $ Free r))) rs) ys @
1456 (* FIXME: avoid collisions with other variable names? *)
1457 val rec_ctxt = Free ("z", fsT');
1459 fun make_rec_intr T p rec_set ((cname, cargs), idxs)
1460 (rec_intr_ts, rec_prems, rec_prems', rec_eq_prems, l) =
1462 val Ts = map (typ_of_dtyp descr'' sorts) cargs;
1463 val frees = map (fn i => "x" ^ string_of_int i) (1 upto length Ts) ~~ Ts;
1464 val frees' = partition_cargs idxs frees;
1465 val binders = maps fst frees';
1466 val atomTs = distinct op = (maps (map snd o fst) frees');
1467 val recs = map_filter
1468 (fn ((_, DtRec i), p) => SOME (i, p) | _ => NONE)
1469 (partition_cargs idxs cargs ~~ frees');
1470 val frees'' = map (fn i => "y" ^ string_of_int i) (1 upto length recs) ~~
1471 map (fn (i, _) => nth rec_result_Ts i) recs;
1472 val prems1 = map (fn ((i, (_, x)), y) => HOLogic.mk_Trueprop
1473 (nth rec_sets' i $ Free x $ Free y)) (recs ~~ frees'');
1475 map (fn f => map (fn p as (_, T) => HOLogic.mk_Trueprop
1476 (fresh_const T (fastype_of f) $ Free p $ f)) binders) rec_fns;
1477 val prems3 = mk_fresh1 [] binders @ mk_fresh2 [] frees';
1478 val prems4 = map (fn ((i, _), y) =>
1479 HOLogic.mk_Trueprop (nth rec_preds i $ Free y)) (recs ~~ frees'');
1480 val prems5 = mk_fresh3 (recs ~~ frees'') frees';
1481 val prems6 = maps (fn aT => map (fn y as (_, T) => HOLogic.mk_Trueprop
1482 (Const ("Finite_Set.finite", HOLogic.mk_setT aT --> HOLogic.boolT) $
1483 (Const ("Nominal.supp", T --> HOLogic.mk_setT aT) $ Free y)))
1485 val prems7 = map (fn x as (_, T) => HOLogic.mk_Trueprop
1486 (fresh_const T fsT' $ Free x $ rec_ctxt)) binders;
1487 val result = list_comb (nth rec_fns l, map Free (frees @ frees''));
1488 val result_freshs = map (fn p as (_, T) =>
1489 fresh_const T (fastype_of result) $ Free p $ result) binders;
1490 val P = HOLogic.mk_Trueprop (p $ result)
1492 (rec_intr_ts @ [Logic.list_implies (flat prems2 @ prems3 @ prems1,
1493 HOLogic.mk_Trueprop (rec_set $
1494 list_comb (Const (cname, Ts ---> T), map Free frees) $ result))],
1495 rec_prems @ [list_all_free (frees @ frees'', Logic.list_implies (prems4, P))],
1496 rec_prems' @ map (fn fr => list_all_free (frees @ frees'',
1497 Logic.list_implies (nth prems2 l @ prems3 @ prems5 @ prems7 @ prems6 @ [P],
1498 HOLogic.mk_Trueprop fr))) result_freshs,
1499 rec_eq_prems @ [flat prems2 @ prems3],
1503 val (rec_intr_ts, rec_prems, rec_prems', rec_eq_prems, _) =
1504 fold (fn ((((d, d'), T), p), rec_set) =>
1505 fold (make_rec_intr T p rec_set) (#3 (snd d) ~~ snd d'))
1506 (descr'' ~~ ndescr ~~ recTs ~~ rec_preds ~~ rec_sets')
1507 ([], [], [], [], 0);
1509 val ({intrs = rec_intrs, elims = rec_elims, raw_induct = rec_induct, ...}, thy11) =
1511 |> Sign.map_naming Name_Space.conceal
1512 |> Inductive.add_inductive_global
1513 {quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name,
1514 coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false}
1515 (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
1516 (map dest_Free rec_fns)
1517 (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) []
1518 ||> Global_Theory.hide_fact true (Long_Name.append (Sign.full_bname thy10 big_rec_name) "induct")
1519 ||> Sign.restore_naming thy10;
1521 (** equivariance **)
1523 val fresh_bij = Global_Theory.get_thms thy11 "fresh_bij";
1524 val perm_bij = Global_Theory.get_thms thy11 "perm_bij";
1526 val (rec_equiv_thms, rec_equiv_thms') = ListPair.unzip (map (fn aT =>
1528 val permT = mk_permT aT;
1529 val pi = Free ("pi", permT);
1530 val rec_fns_pi = map (mk_perm [] pi o uncurry (mk_Free "f"))
1531 (rec_fn_Ts ~~ (1 upto (length rec_fn_Ts)));
1532 val rec_sets_pi = map (fn c => list_comb (Const c, rec_fns_pi))
1533 (rec_set_names ~~ rec_set_Ts);
1534 val ps = map (fn ((((T, U), R), R'), i) =>
1536 val x = Free ("x" ^ string_of_int i, T);
1537 val y = Free ("y" ^ string_of_int i, U)
1539 (R $ x $ y, R' $ mk_perm [] pi x $ mk_perm [] pi y)
1540 end) (recTs ~~ rec_result_Ts ~~ rec_sets ~~ rec_sets_pi ~~ (1 upto length recTs));
1541 val ths = map (fn th => Drule.export_without_context (th RS mp)) (split_conj_thm
1542 (Goal.prove_global thy11 [] []
1543 (augment_sort thy1 pt_cp_sort
1544 (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map HOLogic.mk_imp ps))))
1545 (fn _ => rtac rec_induct 1 THEN REPEAT
1546 (simp_tac (Simplifier.global_context thy11 HOL_basic_ss
1547 addsimps flat perm_simps'
1548 addsimprocs [NominalPermeq.perm_simproc_app]) 1 THEN
1549 (resolve_tac rec_intrs THEN_ALL_NEW
1550 asm_simp_tac (HOL_ss addsimps (fresh_bij @ perm_bij))) 1))))
1551 val ths' = map (fn ((P, Q), th) =>
1552 Goal.prove_global thy11 [] []
1553 (augment_sort thy1 pt_cp_sort
1554 (Logic.mk_implies (HOLogic.mk_Trueprop Q, HOLogic.mk_Trueprop P)))
1555 (fn _ => dtac (Thm.instantiate ([],
1556 [(cterm_of thy11 (Var (("pi", 0), permT)),
1557 cterm_of thy11 (Const ("List.rev", permT --> permT) $ pi))]) th) 1 THEN
1558 NominalPermeq.perm_simp_tac HOL_ss 1)) (ps ~~ ths)
1559 in (ths, ths') end) dt_atomTs);
1561 (** finite support **)
1563 val rec_fin_supp_thms = map (fn aT =>
1565 val name = Long_Name.base_name (fst (dest_Type aT));
1566 val fs_name = Global_Theory.get_thm thy11 ("fs_" ^ name ^ "1");
1567 val aset = HOLogic.mk_setT aT;
1568 val finite = Const ("Finite_Set.finite", aset --> HOLogic.boolT);
1569 val fins = map (fn (f, T) => HOLogic.mk_Trueprop
1570 (finite $ (Const ("Nominal.supp", T --> aset) $ f)))
1571 (rec_fns ~~ rec_fn_Ts)
1573 map (fn th => Drule.export_without_context (th RS mp)) (split_conj_thm
1574 (Goal.prove_global thy11 []
1575 (map (augment_sort thy11 fs_cp_sort) fins)
1576 (augment_sort thy11 fs_cp_sort
1577 (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
1578 (map (fn (((T, U), R), i) =>
1580 val x = Free ("x" ^ string_of_int i, T);
1581 val y = Free ("y" ^ string_of_int i, U)
1583 HOLogic.mk_imp (R $ x $ y,
1584 finite $ (Const ("Nominal.supp", U --> aset) $ y))
1585 end) (recTs ~~ rec_result_Ts ~~ rec_sets ~~
1586 (1 upto length recTs))))))
1587 (fn {prems = fins, ...} =>
1588 (rtac rec_induct THEN_ALL_NEW cut_facts_tac fins) 1 THEN REPEAT
1589 (NominalPermeq.finite_guess_tac (HOL_ss addsimps [fs_name]) 1))))
1594 val finite_premss = map (fn aT =>
1595 map (fn (f, T) => HOLogic.mk_Trueprop
1596 (Const ("Finite_Set.finite", HOLogic.mk_setT aT --> HOLogic.boolT) $
1597 (Const ("Nominal.supp", T --> HOLogic.mk_setT aT) $ f)))
1598 (rec_fns ~~ rec_fn_Ts)) dt_atomTs;
1600 val rec_fns' = map (augment_sort thy11 fs_cp_sort) rec_fns;
1602 val rec_fresh_thms = map (fn ((aT, eqvt_ths), finite_prems) =>
1604 val name = Long_Name.base_name (fst (dest_Type aT));
1605 val fs_name = Global_Theory.get_thm thy11 ("fs_" ^ name ^ "1");
1606 val a = Free ("a", aT);
1607 val freshs = map (fn (f, fT) => HOLogic.mk_Trueprop
1608 (fresh_const aT fT $ a $ f)) (rec_fns ~~ rec_fn_Ts)
1610 map (fn (((T, U), R), eqvt_th) =>
1612 val x = Free ("x", augment_sort_typ thy11 fs_cp_sort T);
1613 val y = Free ("y", U);
1614 val y' = Free ("y'", U)
1616 Drule.export_without_context (Goal.prove (Proof_Context.init_global thy11) []
1617 (map (augment_sort thy11 fs_cp_sort)
1619 [HOLogic.mk_Trueprop (R $ x $ y),
1620 HOLogic.mk_Trueprop (HOLogic.mk_all ("y'", U,
1621 HOLogic.mk_imp (R $ x $ y', HOLogic.mk_eq (y', y)))),
1622 HOLogic.mk_Trueprop (fresh_const aT T $ a $ x)] @
1624 (HOLogic.mk_Trueprop (fresh_const aT U $ a $ y))
1625 (fn {prems, context} =>
1627 val (finite_prems, rec_prem :: unique_prem ::
1628 fresh_prems) = chop (length finite_prems) prems;
1629 val unique_prem' = unique_prem RS spec RS mp;
1630 val unique = [unique_prem', unique_prem' RS sym] MRS trans;
1631 val _ $ (_ $ (_ $ S $ _)) $ _ = prop_of supports_fresh;
1632 val tuple = foldr1 HOLogic.mk_prod (x :: rec_fns')
1634 [rtac (Drule.cterm_instantiate
1636 cterm_of thy11 (Const ("Nominal.supp",
1637 fastype_of tuple --> HOLogic.mk_setT aT) $ tuple))]
1639 simp_tac (HOL_basic_ss addsimps
1640 [supports_def, Thm.symmetric fresh_def, fresh_prod]) 1,
1641 REPEAT_DETERM (resolve_tac [allI, impI] 1),
1642 REPEAT_DETERM (etac conjE 1),
1644 SUBPROOF (fn {prems = prems', params = [(_, a), (_, b)], ...} => EVERY
1645 [cut_facts_tac [rec_prem] 1,
1646 rtac (Thm.instantiate ([],
1647 [(cterm_of thy11 (Var (("pi", 0), mk_permT aT)),
1648 cterm_of thy11 (perm_of_pair (term_of a, term_of b)))]) eqvt_th) 1,
1649 asm_simp_tac (HOL_ss addsimps
1650 (prems' @ perm_swap @ perm_fresh_fresh)) 1]) context 1,
1652 simp_tac (HOL_ss addsimps (fs_name ::
1653 supp_prod :: finite_Un :: finite_prems)) 1,
1654 simp_tac (HOL_ss addsimps (Thm.symmetric fresh_def ::
1655 fresh_prod :: fresh_prems)) 1]
1657 end) (recTs ~~ rec_result_Ts ~~ rec_sets ~~ eqvt_ths)
1658 end) (dt_atomTs ~~ rec_equiv_thms' ~~ finite_premss);
1662 val fun_tuple = foldr1 HOLogic.mk_prod (rec_ctxt :: rec_fns);
1663 val fun_tupleT = fastype_of fun_tuple;
1664 val rec_unique_frees =
1665 Datatype_Prop.indexify_names (replicate (length recTs) "x") ~~ recTs;
1666 val rec_unique_frees'' = map (fn (s, T) => (s ^ "'", T)) rec_unique_frees;
1667 val rec_unique_frees' =
1668 Datatype_Prop.indexify_names (replicate (length recTs) "y") ~~ rec_result_Ts;
1669 val rec_unique_concls = map (fn ((x, U), R) =>
1670 Const (@{const_name Ex1}, (U --> HOLogic.boolT) --> HOLogic.boolT) $
1671 Abs ("y", U, R $ Free x $ Bound 0))
1672 (rec_unique_frees ~~ rec_result_Ts ~~ rec_sets);
1674 val induct_aux_rec = Drule.cterm_instantiate
1675 (map (pairself (cterm_of thy11) o apsnd (augment_sort thy11 fs_cp_sort))
1676 (map (fn (aT, f) => (Logic.varify_global f, Abs ("z", HOLogic.unitT,
1677 Const ("Nominal.supp", fun_tupleT --> HOLogic.mk_setT aT) $ fun_tuple)))
1679 map (fn (((P, T), (x, U)), Q) =>
1680 (Var ((P, 0), Logic.varifyT_global (fsT' --> T --> HOLogic.boolT)),
1681 Abs ("z", HOLogic.unitT, absfree (x, U, Q))))
1682 (pnames ~~ recTs ~~ rec_unique_frees ~~ rec_unique_concls) @
1683 map (fn (s, T) => (Var ((s, 0), Logic.varifyT_global T), Free (s, T)))
1684 rec_unique_frees)) induct_aux;
1686 fun obtain_fresh_name vs ths rec_fin_supp T (freshs1, freshs2, ctxt) =
1688 val p = foldr1 HOLogic.mk_prod (vs @ freshs1);
1689 val ex = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop
1690 (HOLogic.exists_const T $ Abs ("x", T,
1691 fresh_const T (fastype_of p) $ Bound 0 $ p)))
1693 [cut_facts_tac ths 1,
1694 REPEAT_DETERM (dresolve_tac (the (AList.lookup op = rec_fin_supp T)) 1),
1695 resolve_tac exists_fresh' 1,
1696 asm_simp_tac (HOL_ss addsimps (supp_prod :: finite_Un :: fs_atoms)) 1]);
1697 val (([(_, cx)], ths), ctxt') = Obtain.result
1700 full_simp_tac (HOL_ss addsimps (fresh_prod :: fresh_atm)) 1,
1701 REPEAT (etac conjE 1)])
1703 in (freshs1 @ [term_of cx], freshs2 @ ths, ctxt') end;
1705 val finite_ctxt_prems = map (fn aT =>
1707 (Const ("Finite_Set.finite", HOLogic.mk_setT aT --> HOLogic.boolT) $
1708 (Const ("Nominal.supp", fsT' --> HOLogic.mk_setT aT) $ rec_ctxt))) dt_atomTs;
1710 val rec_unique_thms = split_conj_thm (Goal.prove
1711 (Proof_Context.init_global thy11) (map fst rec_unique_frees)
1712 (map (augment_sort thy11 fs_cp_sort)
1713 (flat finite_premss @ finite_ctxt_prems @ rec_prems @ rec_prems'))
1714 (augment_sort thy11 fs_cp_sort
1715 (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj rec_unique_concls)))
1716 (fn {prems, context} =>
1718 val k = length rec_fns;
1719 val (finite_thss, ths1) = fold_map (fn T => fn xs =>
1720 apfst (pair T) (chop k xs)) dt_atomTs prems;
1721 val (finite_ctxt_ths, ths2) = chop (length dt_atomTs) ths1;
1722 val (P_ind_ths, fcbs) = chop k ths2;
1723 val P_ths = map (fn th => th RS mp) (split_conj_thm
1725 (map fst (rec_unique_frees'' @ rec_unique_frees')) []
1726 (augment_sort thy11 fs_cp_sort
1727 (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
1728 (map (fn (((x, y), S), P) => HOLogic.mk_imp
1729 (S $ Free x $ Free y, P $ (Free y)))
1730 (rec_unique_frees'' ~~ rec_unique_frees' ~~
1731 rec_sets ~~ rec_preds)))))
1733 rtac rec_induct 1 THEN
1734 REPEAT ((resolve_tac P_ind_ths THEN_ALL_NEW assume_tac) 1))));
1735 val rec_fin_supp_thms' = map
1736 (fn (ths, (T, fin_ths)) => (T, map (curry op MRS fin_ths) ths))
1737 (rec_fin_supp_thms ~~ finite_thss);
1739 ([rtac induct_aux_rec 1] @
1740 maps (fn ((_, finite_ths), finite_th) =>
1741 [cut_facts_tac (finite_th :: finite_ths) 1,
1742 asm_simp_tac (HOL_ss addsimps [supp_prod, finite_Un]) 1])
1743 (finite_thss ~~ finite_ctxt_ths) @
1744 maps (fn ((_, idxss), elim) => maps (fn idxs =>
1745 [full_simp_tac (HOL_ss addsimps [Thm.symmetric fresh_def, supp_prod, Un_iff]) 1,
1746 REPEAT_DETERM (eresolve_tac [conjE, ex1E] 1),
1748 (resolve_tac rec_intrs THEN_ALL_NEW atac) 1,
1750 ((DETERM o etac elim) THEN_ALL_NEW full_simp_tac
1751 (HOL_ss addsimps flat distinct_thms)) 1] @
1752 (if null idxs then [] else [hyp_subst_tac 1,
1753 SUBPROOF (fn {asms, concl, prems = prems', params, context = context', ...} =>
1755 val SOME prem = find_first (can (HOLogic.dest_eq o
1756 HOLogic.dest_Trueprop o prop_of)) prems';
1757 val _ $ (_ $ lhs $ rhs) = prop_of prem;
1758 val _ $ (_ $ lhs' $ rhs') = term_of concl;
1759 val rT = fastype_of lhs';
1760 val (c, cargsl) = strip_comb lhs;
1761 val cargsl' = partition_cargs idxs cargsl;
1762 val boundsl = maps fst cargsl';
1763 val (_, cargsr) = strip_comb rhs;
1764 val cargsr' = partition_cargs idxs cargsr;
1765 val boundsr = maps fst cargsr';
1766 val (params1, _ :: params2) =
1767 chop (length params div 2) (map (term_of o #2) params);
1768 val params' = params1 @ params2;
1769 val rec_prems = filter (fn th => case prop_of th of
1770 _ $ p => (case head_of p of
1771 Const (s, _) => member (op =) rec_set_names s
1773 | _ => false) prems';
1774 val fresh_prems = filter (fn th => case prop_of th of
1775 _ $ (Const ("Nominal.fresh", _) $ _ $ _) => true
1776 | _ $ (Const (@{const_name Not}, _) $ _) => true
1777 | _ => false) prems';
1778 val Ts = map fastype_of boundsl;
1780 val _ = warning "step 1: obtaining fresh names";
1781 val (freshs1, freshs2, context'') = fold
1782 (obtain_fresh_name (rec_ctxt :: rec_fns' @ params')
1783 (maps snd finite_thss @ finite_ctxt_ths @ rec_prems)
1785 Ts ([], [], context');
1786 val pi1 = map perm_of_pair (boundsl ~~ freshs1);
1788 val pi2 = map perm_of_pair (boundsr ~~ freshs1);
1791 val fresh_prems' = mk_not_sym fresh_prems;
1792 val freshs2' = mk_not_sym freshs2;
1794 (** as, bs, cs # K as ts, K bs us **)
1795 val _ = warning "step 2: as, bs, cs # K as ts, K bs us";
1796 val prove_fresh_ss = HOL_ss addsimps
1797 (finite_Diff :: flat fresh_thms @
1798 fs_atoms @ abs_fresh @ abs_supp @ fresh_atm);
1799 (* FIXME: avoid asm_full_simp_tac ? *)
1800 fun prove_fresh ths y x = Goal.prove context'' [] []
1801 (HOLogic.mk_Trueprop (fresh_const
1802 (fastype_of x) (fastype_of y) $ x $ y))
1803 (fn _ => cut_facts_tac ths 1 THEN asm_full_simp_tac prove_fresh_ss 1);
1804 val constr_fresh_thms =
1805 map (prove_fresh fresh_prems lhs) boundsl @
1806 map (prove_fresh fresh_prems rhs) boundsr @
1807 map (prove_fresh freshs2 lhs) freshs1 @
1808 map (prove_fresh freshs2 rhs) freshs1;
1810 (** pi1 o (K as ts) = pi2 o (K bs us) **)
1811 val _ = warning "step 3: pi1 o (K as ts) = pi2 o (K bs us)";
1812 val pi1_pi2_eq = Goal.prove context'' [] []
1813 (HOLogic.mk_Trueprop (HOLogic.mk_eq
1814 (fold_rev (mk_perm []) pi1 lhs, fold_rev (mk_perm []) pi2 rhs)))
1816 [cut_facts_tac constr_fresh_thms 1,
1817 asm_simp_tac (HOL_basic_ss addsimps perm_fresh_fresh) 1,
1820 (** pi1 o ts = pi2 o us **)
1821 val _ = warning "step 4: pi1 o ts = pi2 o us";
1822 val pi1_pi2_eqs = map (fn (t, u) =>
1823 Goal.prove context'' [] []
1824 (HOLogic.mk_Trueprop (HOLogic.mk_eq
1825 (fold_rev (mk_perm []) pi1 t, fold_rev (mk_perm []) pi2 u)))
1827 [cut_facts_tac [pi1_pi2_eq] 1,
1828 asm_full_simp_tac (HOL_ss addsimps
1829 (calc_atm @ flat perm_simps' @
1830 fresh_prems' @ freshs2' @ abs_perm @
1831 alpha @ flat inject_thms)) 1]))
1832 (map snd cargsl' ~~ map snd cargsr');
1834 (** pi1^-1 o pi2 o us = ts **)
1835 val _ = warning "step 5: pi1^-1 o pi2 o us = ts";
1836 val rpi1_pi2_eqs = map (fn ((t, u), eq) =>
1837 Goal.prove context'' [] []
1838 (HOLogic.mk_Trueprop (HOLogic.mk_eq
1839 (fold_rev (mk_perm []) (rpi1 @ pi2) u, t)))
1840 (fn _ => simp_tac (HOL_ss addsimps
1841 ((eq RS sym) :: perm_swap)) 1))
1842 (map snd cargsl' ~~ map snd cargsr' ~~ pi1_pi2_eqs);
1844 val (rec_prems1, rec_prems2) =
1845 chop (length rec_prems div 2) rec_prems;
1847 (** (ts, pi1^-1 o pi2 o vs) in rec_set **)
1848 val _ = warning "step 6: (ts, pi1^-1 o pi2 o vs) in rec_set";
1849 val rec_prems' = map (fn th =>
1851 val _ $ (S $ x $ y) = prop_of th;
1852 val Const (s, _) = head_of S;
1853 val k = find_index (equal s) rec_set_names;
1854 val pi = rpi1 @ pi2;
1855 fun mk_pi z = fold_rev (mk_perm []) pi z;
1858 val U as Type (_, [Type (_, [T, _])]) = fastype_of p;
1859 val l = find_index (equal T) dt_atomTs;
1860 val th = nth (nth rec_equiv_thms' l) k;
1861 val th' = Thm.instantiate ([],
1862 [(cterm_of thy11 (Var (("pi", 0), U)),
1863 cterm_of thy11 p)]) th;
1865 val th' = Goal.prove context'' [] []
1866 (HOLogic.mk_Trueprop (S $ mk_pi x $ mk_pi y))
1869 [simp_tac (HOL_ss addsimps (fresh_prems' @ freshs2' @
1870 perm_swap @ perm_fresh_fresh)) 1,
1874 (HOL_basic_ss addsimps rpi1_pi2_eqs) th'
1877 val ihs = filter (fn th => case prop_of th of
1878 _ $ (Const (@{const_name All}, _) $ _) => true | _ => false) prems';
1880 (** pi1 o rs = pi2 o vs , rs = pi1^-1 o pi2 o vs **)
1881 val _ = warning "step 7: pi1 o rs = pi2 o vs , rs = pi1^-1 o pi2 o vs";
1882 val rec_eqns = map (fn (th, ih) =>
1884 val th' = th RS (ih RS spec RS mp) RS sym;
1885 val _ $ (_ $ lhs $ rhs) = prop_of th';
1886 fun strip_perm (_ $ _ $ t) = strip_perm t
1889 Goal.prove context'' [] []
1890 (HOLogic.mk_Trueprop (HOLogic.mk_eq
1891 (fold_rev (mk_perm []) pi1 lhs,
1892 fold_rev (mk_perm []) pi2 (strip_perm rhs))))
1893 (fn _ => simp_tac (HOL_basic_ss addsimps
1894 (th' :: perm_swap)) 1)
1895 end) (rec_prems' ~~ ihs);
1898 val _ = warning "step 8: as # rs";
1900 maps (fn (rec_prem, ih) =>
1902 val _ $ (S $ x $ (y as Free (_, T))) =
1904 val k = find_index (equal S) rec_sets;
1905 val atoms = flat (map_filter (fn (bs, z) =>
1906 if z = x then NONE else SOME bs) cargsl')
1908 map (fn a as Free (_, aT) =>
1909 let val l = find_index (equal aT) dt_atomTs;
1911 Goal.prove context'' [] []
1912 (HOLogic.mk_Trueprop (fresh_const aT T $ a $ y))
1914 (rtac (nth (nth rec_fresh_thms l) k) 1 ::
1915 map (fn th => rtac th 1)
1916 (snd (nth finite_thss l)) @
1917 [rtac rec_prem 1, rtac ih 1,
1918 REPEAT_DETERM (resolve_tac fresh_prems 1)]))
1920 end) (rec_prems1 ~~ ihs);
1922 (** as # fK as ts rs , bs # fK bs us vs **)
1923 val _ = warning "step 9: as # fK as ts rs , bs # fK bs us vs";
1924 fun prove_fresh_result (a as Free (_, aT)) =
1925 Goal.prove context'' [] []
1926 (HOLogic.mk_Trueprop (fresh_const aT rT $ a $ rhs'))
1928 [resolve_tac fcbs 1,
1929 REPEAT_DETERM (resolve_tac
1930 (fresh_prems @ rec_freshs) 1),
1931 REPEAT_DETERM (resolve_tac (maps snd rec_fin_supp_thms') 1
1932 THEN resolve_tac rec_prems 1),
1933 resolve_tac P_ind_ths 1,
1934 REPEAT_DETERM (resolve_tac (P_ths @ rec_prems) 1)]);
1936 val fresh_results'' = map prove_fresh_result boundsl;
1938 fun prove_fresh_result'' ((a as Free (_, aT), b), th) =
1939 let val th' = Goal.prove context'' [] []
1940 (HOLogic.mk_Trueprop (fresh_const aT rT $
1941 fold_rev (mk_perm []) (rpi2 @ pi1) a $
1942 fold_rev (mk_perm []) (rpi2 @ pi1) rhs'))
1943 (fn _ => simp_tac (HOL_ss addsimps fresh_bij) 1 THEN
1946 Goal.prove context'' [] []
1947 (HOLogic.mk_Trueprop (fresh_const aT rT $ b $ lhs'))
1949 [cut_facts_tac [th'] 1,
1950 full_simp_tac (Simplifier.global_context thy11 HOL_ss
1951 addsimps rec_eqns @ pi1_pi2_eqs @ perm_swap
1952 addsimprocs [NominalPermeq.perm_simproc_app]) 1,
1953 full_simp_tac (HOL_ss addsimps (calc_atm @
1954 fresh_prems' @ freshs2' @ perm_fresh_fresh)) 1])
1957 val fresh_results = fresh_results'' @ map prove_fresh_result''
1958 (boundsl ~~ boundsr ~~ fresh_results'');
1960 (** cs # fK as ts rs , cs # fK bs us vs **)
1961 val _ = warning "step 10: cs # fK as ts rs , cs # fK bs us vs";
1962 fun prove_fresh_result' recs t (a as Free (_, aT)) =
1963 Goal.prove context'' [] []
1964 (HOLogic.mk_Trueprop (fresh_const aT rT $ a $ t))
1966 [cut_facts_tac recs 1,
1967 REPEAT_DETERM (dresolve_tac
1968 (the (AList.lookup op = rec_fin_supp_thms' aT)) 1),
1969 NominalPermeq.fresh_guess_tac
1970 (HOL_ss addsimps (freshs2 @
1971 fs_atoms @ fresh_atm @
1972 maps snd finite_thss)) 1]);
1974 val fresh_results' =
1975 map (prove_fresh_result' rec_prems1 rhs') freshs1 @
1976 map (prove_fresh_result' rec_prems2 lhs') freshs1;
1978 (** pi1 o (fK as ts rs) = pi2 o (fK bs us vs) **)
1979 val _ = warning "step 11: pi1 o (fK as ts rs) = pi2 o (fK bs us vs)";
1980 val pi1_pi2_result = Goal.prove context'' [] []
1981 (HOLogic.mk_Trueprop (HOLogic.mk_eq
1982 (fold_rev (mk_perm []) pi1 rhs', fold_rev (mk_perm []) pi2 lhs')))
1983 (fn _ => simp_tac (Simplifier.context context'' HOL_ss
1984 addsimps pi1_pi2_eqs @ rec_eqns
1985 addsimprocs [NominalPermeq.perm_simproc_app]) 1 THEN
1986 TRY (simp_tac (HOL_ss addsimps
1987 (fresh_prems' @ freshs2' @ calc_atm @ perm_fresh_fresh)) 1));
1989 val _ = warning "final result";
1990 val final = Goal.prove context'' [] [] (term_of concl)
1991 (fn _ => cut_facts_tac [pi1_pi2_result RS sym] 1 THEN
1992 full_simp_tac (HOL_basic_ss addsimps perm_fresh_fresh @
1993 fresh_results @ fresh_results') 1);
1994 val final' = Proof_Context.export context'' context' [final];
1995 val _ = warning "finished!"
1997 resolve_tac final' 1
1998 end) context 1])) idxss) (ndescr ~~ rec_elims))
2001 val rec_total_thms = map (fn r => r RS theI') rec_unique_thms;
2003 (* define primrec combinators *)
2005 val big_reccomb_name = (space_implode "_" new_type_names) ^ "_rec";
2006 val reccomb_names = map (Sign.full_bname thy11)
2007 (if length descr'' = 1 then [big_reccomb_name] else
2008 (map ((curry (op ^) (big_reccomb_name ^ "_")) o string_of_int)
2009 (1 upto (length descr''))));
2010 val reccombs = map (fn ((name, T), T') => list_comb
2011 (Const (name, rec_fn_Ts @ [T] ---> T'), rec_fns))
2012 (reccomb_names ~~ recTs ~~ rec_result_Ts);
2014 val (reccomb_defs, thy12) =
2016 |> Sign.add_consts_i (map (fn ((name, T), T') =>
2017 (Binding.name (Long_Name.base_name name), rec_fn_Ts @ [T] ---> T', NoSyn))
2018 (reccomb_names ~~ recTs ~~ rec_result_Ts))
2019 |> (Global_Theory.add_defs false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') =>
2020 (Binding.name (Long_Name.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T,
2021 Const (@{const_name The}, (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
2022 set $ Free ("x", T) $ Free ("y", T'))))))
2023 (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts));
2025 (* prove characteristic equations for primrec combinators *)
2027 val rec_thms = map (fn (prems, concl) =>
2029 val _ $ (_ $ (_ $ x) $ _) = concl;
2030 val (_, cargs) = strip_comb x;
2031 val ps = map (fn (x as Free (_, T), i) =>
2032 (Free ("x" ^ string_of_int i, T), x)) (cargs ~~ (1 upto length cargs));
2033 val concl' = subst_atomic_types (rec_result_Ts' ~~ rec_result_Ts) concl;
2034 val prems' = flat finite_premss @ finite_ctxt_prems @
2035 rec_prems @ rec_prems' @ map (subst_atomic ps) prems;
2036 fun solve rules prems = resolve_tac rules THEN_ALL_NEW
2037 (resolve_tac prems THEN_ALL_NEW atac)
2039 Goal.prove_global thy12 []
2040 (map (augment_sort thy12 fs_cp_sort) prems')
2041 (augment_sort thy12 fs_cp_sort concl')
2042 (fn {prems, ...} => EVERY
2043 [rewrite_goals_tac reccomb_defs,
2044 rtac the1_equality 1,
2045 solve rec_unique_thms prems 1,
2046 resolve_tac rec_intrs 1,
2047 REPEAT (solve (prems @ rec_total_thms) prems 1)])
2048 end) (rec_eq_prems ~~
2049 Datatype_Prop.make_primrecs new_type_names descr' sorts thy12);
2051 val dt_infos = map_index (make_dt_info pdescr sorts induct reccomb_names rec_thms)
2052 (descr1 ~~ distinct_thms ~~ inject_thms);
2054 (* FIXME: theorems are stored in database for testing only *)
2055 val (_, thy13) = thy12 |>
2056 Global_Theory.add_thmss
2057 [((Binding.name "rec_equiv", flat rec_equiv_thms), []),
2058 ((Binding.name "rec_equiv'", flat rec_equiv_thms'), []),
2059 ((Binding.name "rec_fin_supp", flat rec_fin_supp_thms), []),
2060 ((Binding.name "rec_fresh", flat rec_fresh_thms), []),
2061 ((Binding.name "rec_unique", map Drule.export_without_context rec_unique_thms), []),
2062 ((Binding.name "recs", rec_thms), [])] ||>
2063 Sign.parent_path ||>
2064 map_nominal_datatypes (fold Symtab.update dt_infos);
2070 val add_nominal_datatype = gen_add_nominal_datatype Datatype.read_typ;
2073 (* FIXME: The following stuff should be exported by Datatype *)
2076 Scan.option (Parse.$$$ "(" |-- Parse.name --| Parse.$$$ ")") --
2077 Parse.type_args -- Parse.name -- Parse.opt_mixfix --
2078 (Parse.$$$ "=" |-- Parse.enum1 "|" (Parse.name -- Scan.repeat Parse.typ -- Parse.opt_mixfix));
2080 fun mk_datatype args =
2082 val names = map (fn ((((NONE, _), t), _), _) => t | ((((SOME t, _), _), _), _) => t) args;
2083 val specs = map (fn ((((_, vs), t), mx), cons) =>
2084 (vs, t, mx, map (fn ((x, y), z) => (x, y, z)) cons)) args;
2085 in add_nominal_datatype Datatype.default_config names specs end;
2088 Outer_Syntax.command "nominal_datatype" "define inductive datatypes" Keyword.thy_decl
2089 (Parse.and_list1 datatype_decl >> (Toplevel.theory o mk_datatype));