35 val Un_assoc = @{thm Un_assoc}; |
35 val Un_assoc = @{thm Un_assoc}; |
36 val Collect_disj_eq = @{thm Collect_disj_eq}; |
36 val Collect_disj_eq = @{thm Collect_disj_eq}; |
37 val Collect_False_empty = @{thm empty_def [THEN sym, THEN eq_reflection]}; |
37 val Collect_False_empty = @{thm empty_def [THEN sym, THEN eq_reflection]}; |
38 val empty_iff = @{thm empty_iff}; |
38 val empty_iff = @{thm empty_iff}; |
39 |
39 |
40 open Datatype_Aux; |
|
41 open NominalAtoms; |
40 open NominalAtoms; |
42 |
41 |
43 (** FIXME: Datatype should export this function **) |
42 (** FIXME: Datatype should export this function **) |
44 |
43 |
45 local |
44 local |
46 |
45 |
47 fun dt_recs (DtTFree _) = [] |
46 fun dt_recs (Datatype_Aux.DtTFree _) = [] |
48 | dt_recs (DtType (_, dts)) = maps dt_recs dts |
47 | dt_recs (Datatype_Aux.DtType (_, dts)) = maps dt_recs dts |
49 | dt_recs (DtRec i) = [i]; |
48 | dt_recs (Datatype_Aux.DtRec i) = [i]; |
50 |
49 |
51 fun dt_cases (descr: descr) (_, args, constrs) = |
50 fun dt_cases (descr: Datatype_Aux.descr) (_, args, constrs) = |
52 let |
51 let |
53 fun the_bname i = Long_Name.base_name (#1 (the (AList.lookup (op =) descr i))); |
52 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)); |
53 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; |
54 in map (fn (c, _) => space_implode "_" (Long_Name.base_name c :: bnames)) constrs end; |
56 |
55 |
254 val pi = Free ("pi", permT); |
255 val pi = Free ("pi", permT); |
255 val perm_types = map (fn (i, _) => |
256 val perm_types = map (fn (i, _) => |
256 let val T = nth_dtyp i |
257 let val T = nth_dtyp i |
257 in permT --> T --> T end) descr; |
258 in permT --> T --> T end) descr; |
258 val perm_names' = Datatype_Prop.indexify_names (map (fn (i, _) => |
259 val perm_names' = Datatype_Prop.indexify_names (map (fn (i, _) => |
259 "perm_" ^ name_of_typ (nth_dtyp i)) descr); |
260 "perm_" ^ Datatype_Aux.name_of_typ (nth_dtyp i)) descr); |
260 val perm_names = replicate (length new_type_names) "Nominal.perm" @ |
261 val perm_names = replicate (length new_type_names) "Nominal.perm" @ |
261 map (Sign.full_bname thy1) (List.drop (perm_names', length new_type_names)); |
262 map (Sign.full_bname thy1) (List.drop (perm_names', length new_type_names)); |
262 val perm_names_types = perm_names ~~ perm_types; |
263 val perm_names_types = perm_names ~~ perm_types; |
263 val perm_names_types' = perm_names' ~~ perm_types; |
264 val perm_names_types' = perm_names' ~~ perm_types; |
264 |
265 |
265 val perm_eqs = maps (fn (i, (_, _, constrs)) => |
266 val perm_eqs = maps (fn (i, (_, _, constrs)) => |
266 let val T = nth_dtyp i |
267 let val T = nth_dtyp i |
267 in map (fn (cname, dts) => |
268 in map (fn (cname, dts) => |
268 let |
269 let |
269 val Ts = map (typ_of_dtyp descr) dts; |
270 val Ts = map (Datatype_Aux.typ_of_dtyp descr) dts; |
270 val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts); |
271 val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts); |
271 val args = map Free (names ~~ Ts); |
272 val args = map Free (names ~~ Ts); |
272 val c = Const (cname, Ts ---> T); |
273 val c = Const (cname, Ts ---> T); |
273 fun perm_arg (dt, x) = |
274 fun perm_arg (dt, x) = |
274 let val T = type_of x |
275 let val T = type_of x |
275 in if is_rec_type dt then |
276 in if Datatype_Aux.is_rec_type dt then |
276 let val Us = binder_types T |
277 let val Us = binder_types T |
277 in list_abs (map (pair "x") Us, |
278 in list_abs (map (pair "x") Us, |
278 Free (nth perm_names_types' (body_index dt)) $ pi $ |
279 Free (nth perm_names_types' (Datatype_Aux.body_index dt)) $ pi $ |
279 list_comb (x, map (fn (i, U) => |
280 list_comb (x, map (fn (i, U) => |
280 Const ("Nominal.perm", permT --> U --> U) $ |
281 Const ("Nominal.perm", permT --> U --> U) $ |
281 (Const ("List.rev", permT --> permT) $ pi) $ |
282 (Const ("List.rev", permT --> permT) $ pi) $ |
282 Bound i) ((length Us - 1 downto 0) ~~ Us))) |
283 Bound i) ((length Us - 1 downto 0) ~~ Us))) |
283 end |
284 end |
307 val perm_indnames = Datatype_Prop.make_tnames (map body_type perm_types); |
308 val perm_indnames = Datatype_Prop.make_tnames (map body_type perm_types); |
308 val perm_fun_def = Simpdata.mk_eq @{thm perm_fun_def}; |
309 val perm_fun_def = Simpdata.mk_eq @{thm perm_fun_def}; |
309 |
310 |
310 val unfolded_perm_eq_thms = |
311 val unfolded_perm_eq_thms = |
311 if length descr = length new_type_names then [] |
312 if length descr = length new_type_names then [] |
312 else map Drule.export_without_context (List.drop (split_conj_thm |
313 else map Drule.export_without_context (List.drop (Datatype_Aux.split_conj_thm |
313 (Goal.prove_global thy2 [] [] |
314 (Goal.prove_global thy2 [] [] |
314 (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
315 (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
315 (map (fn (c as (s, T), x) => |
316 (map (fn (c as (s, T), x) => |
316 let val [T1, T2] = binder_types T |
317 let val [T1, T2] = binder_types T |
317 in HOLogic.mk_eq (Const c $ pi $ Free (x, T2), |
318 in HOLogic.mk_eq (Const c $ pi $ Free (x, T2), |
327 |
328 |
328 val _ = warning "perm_empty_thms"; |
329 val _ = warning "perm_empty_thms"; |
329 |
330 |
330 val perm_empty_thms = maps (fn a => |
331 val perm_empty_thms = maps (fn a => |
331 let val permT = mk_permT (Type (a, [])) |
332 let val permT = mk_permT (Type (a, [])) |
332 in map Drule.export_without_context (List.take (split_conj_thm |
333 in map Drule.export_without_context (List.take (Datatype_Aux.split_conj_thm |
333 (Goal.prove_global thy2 [] [] |
334 (Goal.prove_global thy2 [] [] |
334 (augment_sort thy2 [pt_class_of thy2 a] |
335 (augment_sort thy2 [pt_class_of thy2 a] |
335 (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
336 (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
336 (map (fn ((s, T), x) => HOLogic.mk_eq |
337 (map (fn ((s, T), x) => HOLogic.mk_eq |
337 (Const (s, permT --> T --> T) $ |
338 (Const (s, permT --> T --> T) $ |
359 val pi1 = Free ("pi1", permT); |
360 val pi1 = Free ("pi1", permT); |
360 val pi2 = Free ("pi2", permT); |
361 val pi2 = Free ("pi2", permT); |
361 val pt_inst = pt_inst_of thy2 a; |
362 val pt_inst = pt_inst_of thy2 a; |
362 val pt2' = pt_inst RS pt2; |
363 val pt2' = pt_inst RS pt2; |
363 val pt2_ax = Global_Theory.get_thm thy2 (Long_Name.map_base_name (fn s => "pt_" ^ s ^ "2") a); |
364 val pt2_ax = Global_Theory.get_thm thy2 (Long_Name.map_base_name (fn s => "pt_" ^ s ^ "2") a); |
364 in List.take (map Drule.export_without_context (split_conj_thm |
365 in List.take (map Drule.export_without_context (Datatype_Aux.split_conj_thm |
365 (Goal.prove_global thy2 [] [] |
366 (Goal.prove_global thy2 [] [] |
366 (augment_sort thy2 [pt_class_of thy2 a] |
367 (augment_sort thy2 [pt_class_of thy2 a] |
367 (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
368 (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
368 (map (fn ((s, T), x) => |
369 (map (fn ((s, T), x) => |
369 let val perm = Const (s, permT --> T --> T) |
370 let val perm = Const (s, permT --> T --> T) |
394 val at_inst = at_inst_of thy2 a; |
395 val at_inst = at_inst_of thy2 a; |
395 val pt_inst = pt_inst_of thy2 a; |
396 val pt_inst = pt_inst_of thy2 a; |
396 val pt3' = pt_inst RS pt3; |
397 val pt3' = pt_inst RS pt3; |
397 val pt3_rev' = at_inst RS (pt_inst RS pt3_rev); |
398 val pt3_rev' = at_inst RS (pt_inst RS pt3_rev); |
398 val pt3_ax = Global_Theory.get_thm thy2 (Long_Name.map_base_name (fn s => "pt_" ^ s ^ "3") a); |
399 val pt3_ax = Global_Theory.get_thm thy2 (Long_Name.map_base_name (fn s => "pt_" ^ s ^ "3") a); |
399 in List.take (map Drule.export_without_context (split_conj_thm |
400 in List.take (map Drule.export_without_context (Datatype_Aux.split_conj_thm |
400 (Goal.prove_global thy2 [] [] |
401 (Goal.prove_global thy2 [] [] |
401 (augment_sort thy2 [pt_class_of thy2 a] (Logic.mk_implies |
402 (augment_sort thy2 [pt_class_of thy2 a] (Logic.mk_implies |
402 (HOLogic.mk_Trueprop (Const ("Nominal.prm_eq", |
403 (HOLogic.mk_Trueprop (Const ("Nominal.prm_eq", |
403 permT --> permT --> HOLogic.boolT) $ pi1 $ pi2), |
404 permT --> permT --> HOLogic.boolT) $ pi1 $ pi2), |
404 HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
405 HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
445 [cp_inst RS cp1 RS sym, |
446 [cp_inst RS cp1 RS sym, |
446 at_inst RS (pt_inst RS pt_perm_compose) RS sym, |
447 at_inst RS (pt_inst RS pt_perm_compose) RS sym, |
447 at_inst RS (pt_inst RS pt_perm_compose_rev) RS sym] |
448 at_inst RS (pt_inst RS pt_perm_compose_rev) RS sym] |
448 end)) |
449 end)) |
449 val sort = Sign.minimize_sort thy (Sign.certify_sort thy (cp_class :: pt_class)); |
450 val sort = Sign.minimize_sort thy (Sign.certify_sort thy (cp_class :: pt_class)); |
450 val thms = split_conj_thm (Goal.prove_global thy [] [] |
451 val thms = Datatype_Aux.split_conj_thm (Goal.prove_global thy [] [] |
451 (augment_sort thy sort |
452 (augment_sort thy sort |
452 (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
453 (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
453 (map (fn ((s, T), x) => |
454 (map (fn ((s, T), x) => |
454 let |
455 let |
455 val pi1 = Free ("pi1", permT1); |
456 val pi1 = Free ("pi1", permT1); |
497 |
498 |
498 (**** Define representing sets ****) |
499 (**** Define representing sets ****) |
499 |
500 |
500 val _ = warning "representing sets"; |
501 val _ = warning "representing sets"; |
501 |
502 |
502 val rep_set_names = Datatype_Prop.indexify_names |
503 val rep_set_names = |
503 (map (fn (i, _) => name_of_typ (nth_dtyp i) ^ "_set") descr); |
504 Datatype_Prop.indexify_names |
|
505 (map (fn (i, _) => Datatype_Aux.name_of_typ (nth_dtyp i) ^ "_set") descr); |
504 val big_rep_name = |
506 val big_rep_name = |
505 space_implode "_" (Datatype_Prop.indexify_names (map_filter |
507 space_implode "_" (Datatype_Prop.indexify_names (map_filter |
506 (fn (i, ("Nominal.noption", _, _)) => NONE |
508 (fn (i, ("Nominal.noption", _, _)) => NONE |
507 | (i, _) => SOME (name_of_typ (nth_dtyp i))) descr)) ^ "_set"; |
509 | (i, _) => SOME (Datatype_Aux.name_of_typ (nth_dtyp i))) descr)) ^ "_set"; |
508 val _ = warning ("big_rep_name: " ^ big_rep_name); |
510 val _ = warning ("big_rep_name: " ^ big_rep_name); |
509 |
511 |
510 fun strip_option (dtf as DtType ("fun", [dt, DtRec i])) = |
512 fun strip_option (dtf as Datatype_Aux.DtType ("fun", [dt, Datatype_Aux.DtRec i])) = |
511 (case AList.lookup op = descr i of |
513 (case AList.lookup op = descr i of |
512 SOME ("Nominal.noption", _, [(_, [dt']), _]) => |
514 SOME ("Nominal.noption", _, [(_, [dt']), _]) => |
513 apfst (cons dt) (strip_option dt') |
515 apfst (cons dt) (strip_option dt') |
514 | _ => ([], dtf)) |
516 | _ => ([], dtf)) |
515 | strip_option (DtType ("fun", [dt, DtType ("Nominal.noption", [dt'])])) = |
517 | strip_option (Datatype_Aux.DtType ("fun", |
|
518 [dt, Datatype_Aux.DtType ("Nominal.noption", [dt'])])) = |
516 apfst (cons dt) (strip_option dt') |
519 apfst (cons dt) (strip_option dt') |
517 | strip_option dt = ([], dt); |
520 | strip_option dt = ([], dt); |
518 |
521 |
519 val dt_atomTs = distinct op = (map (typ_of_dtyp descr) |
522 val dt_atomTs = distinct op = (map (Datatype_Aux.typ_of_dtyp descr) |
520 (maps (fn (_, (_, _, cs)) => maps (maps (fst o strip_option) o snd) cs) descr)); |
523 (maps (fn (_, (_, _, cs)) => maps (maps (fst o strip_option) o snd) cs) descr)); |
521 val dt_atoms = map (fst o dest_Type) dt_atomTs; |
524 val dt_atoms = map (fst o dest_Type) dt_atomTs; |
522 |
525 |
523 fun make_intr s T (cname, cargs) = |
526 fun make_intr s T (cname, cargs) = |
524 let |
527 let |
525 fun mk_prem dt (j, j', prems, ts) = |
528 fun mk_prem dt (j, j', prems, ts) = |
526 let |
529 let |
527 val (dts, dt') = strip_option dt; |
530 val (dts, dt') = strip_option dt; |
528 val (dts', dt'') = strip_dtyp dt'; |
531 val (dts', dt'') = Datatype_Aux.strip_dtyp dt'; |
529 val Ts = map (typ_of_dtyp descr) dts; |
532 val Ts = map (Datatype_Aux.typ_of_dtyp descr) dts; |
530 val Us = map (typ_of_dtyp descr) dts'; |
533 val Us = map (Datatype_Aux.typ_of_dtyp descr) dts'; |
531 val T = typ_of_dtyp descr dt''; |
534 val T = Datatype_Aux.typ_of_dtyp descr dt''; |
532 val free = mk_Free "x" (Us ---> T) j; |
535 val free = Datatype_Aux.mk_Free "x" (Us ---> T) j; |
533 val free' = app_bnds free (length Us); |
536 val free' = Datatype_Aux.app_bnds free (length Us); |
534 fun mk_abs_fun T (i, t) = |
537 fun mk_abs_fun T (i, t) = |
535 let val U = fastype_of t |
538 let val U = fastype_of t |
536 in (i + 1, Const ("Nominal.abs_fun", [T, U, T] ---> |
539 in (i + 1, Const ("Nominal.abs_fun", [T, U, T] ---> |
537 Type ("Nominal.noption", [U])) $ mk_Free "y" T i $ t) |
540 Type ("Nominal.noption", [U])) $ Datatype_Aux.mk_Free "y" T i $ t) |
538 end |
541 end |
539 in (j + 1, j' + length Ts, |
542 in (j + 1, j' + length Ts, |
540 case dt'' of |
543 case dt'' of |
541 DtRec k => list_all (map (pair "x") Us, |
544 Datatype_Aux.DtRec k => list_all (map (pair "x") Us, |
542 HOLogic.mk_Trueprop (Free (nth rep_set_names k, |
545 HOLogic.mk_Trueprop (Free (nth rep_set_names k, |
543 T --> HOLogic.boolT) $ free')) :: prems |
546 T --> HOLogic.boolT) $ free')) :: prems |
544 | _ => prems, |
547 | _ => prems, |
545 snd (fold_rev mk_abs_fun Ts (j', free)) :: ts) |
548 snd (fold_rev mk_abs_fun Ts (j', free)) :: ts) |
546 end; |
549 end; |
715 |
718 |
716 val (ty_idxs, _) = List.foldl |
719 val (ty_idxs, _) = List.foldl |
717 (fn ((i, ("Nominal.noption", _, _)), p) => p |
720 (fn ((i, ("Nominal.noption", _, _)), p) => p |
718 | ((i, _), (ty_idxs, j)) => (ty_idxs @ [(i, j)], j + 1)) ([], 0) descr; |
721 | ((i, _), (ty_idxs, j)) => (ty_idxs @ [(i, j)], j + 1)) ([], 0) descr; |
719 |
722 |
720 fun reindex (DtType (s, dts)) = DtType (s, map reindex dts) |
723 fun reindex (Datatype_Aux.DtType (s, dts)) = Datatype_Aux.DtType (s, map reindex dts) |
721 | reindex (DtRec i) = DtRec (the (AList.lookup op = ty_idxs i)) |
724 | reindex (Datatype_Aux.DtRec i) = Datatype_Aux.DtRec (the (AList.lookup op = ty_idxs i)) |
722 | reindex dt = dt; |
725 | reindex dt = dt; |
723 |
726 |
724 fun strip_suffix i s = implode (List.take (raw_explode s, size s - i)); (* FIXME Symbol.explode (?) *) |
727 fun strip_suffix i s = implode (List.take (raw_explode s, size s - i)); (* FIXME Symbol.explode (?) *) |
725 |
728 |
726 (** strips the "_Rep" in type names *) |
729 (** strips the "_Rep" in type names *) |
752 |
755 |
753 val pdescr = map (fn ((i, (s, dts, constrs)), (_, idxss)) => (i, (s, dts, |
756 val pdescr = map (fn ((i, (s, dts, constrs)), (_, idxss)) => (i, (s, dts, |
754 map (fn ((cname, cargs), idxs) => (cname, partition_cargs idxs cargs)) |
757 map (fn ((cname, cargs), idxs) => (cname, partition_cargs idxs cargs)) |
755 (constrs ~~ idxss)))) (descr'' ~~ ndescr); |
758 (constrs ~~ idxss)))) (descr'' ~~ ndescr); |
756 |
759 |
757 fun nth_dtyp' i = typ_of_dtyp descr'' (DtRec i); |
760 fun nth_dtyp' i = Datatype_Aux.typ_of_dtyp descr'' (Datatype_Aux.DtRec i); |
758 |
761 |
759 val rep_names = map (fn s => |
762 val rep_names = map (fn s => |
760 Sign.intern_const thy7 ("Rep_" ^ s)) new_type_names; |
763 Sign.intern_const thy7 ("Rep_" ^ s)) new_type_names; |
761 val abs_names = map (fn s => |
764 val abs_names = map (fn s => |
762 Sign.intern_const thy7 ("Abs_" ^ s)) new_type_names; |
765 Sign.intern_const thy7 ("Abs_" ^ s)) new_type_names; |
763 |
766 |
764 val recTs = get_rec_types descr''; |
767 val recTs = Datatype_Aux.get_rec_types descr''; |
765 val newTs' = take (length new_type_names) recTs'; |
768 val newTs' = take (length new_type_names) recTs'; |
766 val newTs = take (length new_type_names) recTs; |
769 val newTs = take (length new_type_names) recTs; |
767 |
770 |
768 val full_new_type_names = map (Sign.full_bname thy) new_type_names; |
771 val full_new_type_names = map (Sign.full_bname thy) new_type_names; |
769 |
772 |
770 fun make_constr_def tname T T' (((cname_rep, _), (cname, cargs)), (cname', mx)) |
773 fun make_constr_def tname T T' (((cname_rep, _), (cname, cargs)), (cname', mx)) |
771 (thy, defs, eqns) = |
774 (thy, defs, eqns) = |
772 let |
775 let |
773 fun constr_arg (dts, dt) (j, l_args, r_args) = |
776 fun constr_arg (dts, dt) (j, l_args, r_args) = |
774 let |
777 let |
775 val xs = map (fn (dt, i) => mk_Free "x" (typ_of_dtyp descr'' dt) i) |
778 val xs = |
776 (dts ~~ (j upto j + length dts - 1)) |
779 map (fn (dt, i) => Datatype_Aux.mk_Free "x" (Datatype_Aux.typ_of_dtyp descr'' dt) i) |
777 val x = mk_Free "x" (typ_of_dtyp descr'' dt) (j + length dts) |
780 (dts ~~ (j upto j + length dts - 1)) |
|
781 val x = Datatype_Aux.mk_Free "x" (Datatype_Aux.typ_of_dtyp descr'' dt) (j + length dts) |
778 in |
782 in |
779 (j + length dts + 1, |
783 (j + length dts + 1, |
780 xs @ x :: l_args, |
784 xs @ x :: l_args, |
781 fold_rev mk_abs_fun xs |
785 fold_rev mk_abs_fun xs |
782 (case dt of |
786 (case dt of |
783 DtRec k => if k < length new_type_names then |
787 Datatype_Aux.DtRec k => if k < length new_type_names then |
784 Const (nth rep_names k, typ_of_dtyp descr'' dt --> |
788 Const (nth rep_names k, Datatype_Aux.typ_of_dtyp descr'' dt --> |
785 typ_of_dtyp descr dt) $ x |
789 Datatype_Aux.typ_of_dtyp descr dt) $ x |
786 else error "nested recursion not (yet) supported" |
790 else error "nested recursion not (yet) supported" |
787 | _ => x) :: r_args) |
791 | _ => x) :: r_args) |
788 end |
792 end |
789 |
793 |
790 val (_, l_args, r_args) = fold_rev constr_arg cargs (1, [], []); |
794 val (_, l_args, r_args) = fold_rev constr_arg cargs (1, [], []); |
948 val cname = Sign.intern_const thy8 |
954 val cname = Sign.intern_const thy8 |
949 (Long_Name.append tname (Long_Name.base_name cname)); |
955 (Long_Name.append tname (Long_Name.base_name cname)); |
950 |
956 |
951 fun make_inj (dts, dt) (j, args1, args2, eqs) = |
957 fun make_inj (dts, dt) (j, args1, args2, eqs) = |
952 let |
958 let |
953 val Ts_idx = map (typ_of_dtyp descr'') dts ~~ (j upto j + length dts - 1); |
959 val Ts_idx = |
954 val xs = map (fn (T, i) => mk_Free "x" T i) Ts_idx; |
960 map (Datatype_Aux.typ_of_dtyp descr'') dts ~~ (j upto j + length dts - 1); |
955 val ys = map (fn (T, i) => mk_Free "y" T i) Ts_idx; |
961 val xs = map (fn (T, i) => Datatype_Aux.mk_Free "x" T i) Ts_idx; |
956 val x = mk_Free "x" (typ_of_dtyp descr'' dt) (j + length dts); |
962 val ys = map (fn (T, i) => Datatype_Aux.mk_Free "y" T i) Ts_idx; |
957 val y = mk_Free "y" (typ_of_dtyp descr'' dt) (j + length dts); |
963 val x = |
|
964 Datatype_Aux.mk_Free "x" (Datatype_Aux.typ_of_dtyp descr'' dt) (j + length dts); |
|
965 val y = |
|
966 Datatype_Aux.mk_Free "y" (Datatype_Aux.typ_of_dtyp descr'' dt) (j + length dts); |
958 in |
967 in |
959 (j + length dts + 1, |
968 (j + length dts + 1, |
960 xs @ (x :: args1), ys @ (y :: args2), |
969 xs @ (x :: args1), ys @ (y :: args2), |
961 HOLogic.mk_eq |
970 HOLogic.mk_eq |
962 (fold_rev mk_abs_fun xs x, fold_rev mk_abs_fun ys y) :: eqs) |
971 (fold_rev mk_abs_fun xs x, fold_rev mk_abs_fun ys y) :: eqs) |
991 (Long_Name.append tname (Long_Name.base_name cname)); |
1000 (Long_Name.append tname (Long_Name.base_name cname)); |
992 val atomT = Type (atom, []); |
1001 val atomT = Type (atom, []); |
993 |
1002 |
994 fun process_constr (dts, dt) (j, args1, args2) = |
1003 fun process_constr (dts, dt) (j, args1, args2) = |
995 let |
1004 let |
996 val Ts_idx = map (typ_of_dtyp descr'') dts ~~ (j upto j + length dts - 1); |
1005 val Ts_idx = |
997 val xs = map (fn (T, i) => mk_Free "x" T i) Ts_idx; |
1006 map (Datatype_Aux.typ_of_dtyp descr'') dts ~~ (j upto j + length dts - 1); |
998 val x = mk_Free "x" (typ_of_dtyp descr'' dt) (j + length dts); |
1007 val xs = map (fn (T, i) => Datatype_Aux.mk_Free "x" T i) Ts_idx; |
|
1008 val x = |
|
1009 Datatype_Aux.mk_Free "x" (Datatype_Aux.typ_of_dtyp descr'' dt) (j + length dts); |
999 in |
1010 in |
1000 (j + length dts + 1, |
1011 (j + length dts + 1, |
1001 xs @ (x :: args1), fold_rev mk_abs_fun xs x :: args2) |
1012 xs @ (x :: args1), fold_rev mk_abs_fun xs x :: args2) |
1002 end; |
1013 end; |
1003 |
1014 |
1032 |
1043 |
1033 (**** weak induction theorem ****) |
1044 (**** weak induction theorem ****) |
1034 |
1045 |
1035 fun mk_indrule_lemma (((i, _), T), U) (prems, concls) = |
1046 fun mk_indrule_lemma (((i, _), T), U) (prems, concls) = |
1036 let |
1047 let |
1037 val Rep_t = Const (nth rep_names i, T --> U) $ mk_Free "x" T i; |
1048 val Rep_t = Const (nth rep_names i, T --> U) $ Datatype_Aux.mk_Free "x" T i; |
1038 |
1049 |
1039 val Abs_t = Const (nth abs_names i, U --> T); |
1050 val Abs_t = Const (nth abs_names i, U --> T); |
1040 |
1051 |
1041 in (prems @ [HOLogic.imp $ |
1052 in |
|
1053 (prems @ [HOLogic.imp $ |
1042 (Const (nth rep_set_names'' i, U --> HOLogic.boolT) $ Rep_t) $ |
1054 (Const (nth rep_set_names'' i, U --> HOLogic.boolT) $ Rep_t) $ |
1043 (mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ (Abs_t $ Rep_t))], |
1055 (Datatype_Aux.mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ (Abs_t $ Rep_t))], |
1044 concls @ [mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ mk_Free "x" T i]) |
1056 concls @ |
|
1057 [Datatype_Aux.mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ Datatype_Aux.mk_Free "x" T i]) |
1045 end; |
1058 end; |
1046 |
1059 |
1047 val (indrule_lemma_prems, indrule_lemma_concls) = |
1060 val (indrule_lemma_prems, indrule_lemma_concls) = |
1048 fold mk_indrule_lemma (descr'' ~~ recTs ~~ recTs') ([], []); |
1061 fold mk_indrule_lemma (descr'' ~~ recTs ~~ recTs') ([], []); |
1049 |
1062 |
1050 val indrule_lemma = Goal.prove_global thy8 [] [] |
1063 val indrule_lemma = Goal.prove_global thy8 [] [] |
1051 (Logic.mk_implies |
1064 (Logic.mk_implies |
1052 (HOLogic.mk_Trueprop (mk_conj indrule_lemma_prems), |
1065 (HOLogic.mk_Trueprop (Datatype_Aux.mk_conj indrule_lemma_prems), |
1053 HOLogic.mk_Trueprop (mk_conj indrule_lemma_concls))) (fn _ => EVERY |
1066 HOLogic.mk_Trueprop (Datatype_Aux.mk_conj indrule_lemma_concls))) (fn _ => EVERY |
1054 [REPEAT (etac conjE 1), |
1067 [REPEAT (etac conjE 1), |
1055 REPEAT (EVERY |
1068 REPEAT (EVERY |
1056 [TRY (rtac conjI 1), full_simp_tac (HOL_basic_ss addsimps Rep_inverse_thms) 1, |
1069 [TRY (rtac conjI 1), full_simp_tac (HOL_basic_ss addsimps Rep_inverse_thms) 1, |
1057 etac mp 1, resolve_tac Rep_thms 1])]); |
1070 etac mp 1, resolve_tac Rep_thms 1])]); |
1058 |
1071 |
1088 val supp_atm = Global_Theory.get_thms thy8 "supp_atm"; |
1101 val supp_atm = Global_Theory.get_thms thy8 "supp_atm"; |
1089 |
1102 |
1090 val finite_supp_thms = map (fn atom => |
1103 val finite_supp_thms = map (fn atom => |
1091 let val atomT = Type (atom, []) |
1104 let val atomT = Type (atom, []) |
1092 in map Drule.export_without_context (List.take |
1105 in map Drule.export_without_context (List.take |
1093 (split_conj_thm (Goal.prove_global thy8 [] [] |
1106 (Datatype_Aux.split_conj_thm (Goal.prove_global thy8 [] [] |
1094 (augment_sort thy8 (fs_class_of thy8 atom :: pt_cp_sort) |
1107 (augment_sort thy8 (fs_class_of thy8 atom :: pt_cp_sort) |
1095 (HOLogic.mk_Trueprop |
1108 (HOLogic.mk_Trueprop |
1096 (foldr1 HOLogic.mk_conj (map (fn (s, T) => |
1109 (foldr1 HOLogic.mk_conj (map (fn (s, T) => |
1097 Const ("Finite_Set.finite", HOLogic.mk_setT atomT --> HOLogic.boolT) $ |
1110 Const ("Finite_Set.finite", HOLogic.mk_setT atomT --> HOLogic.boolT) $ |
1098 (Const ("Nominal.supp", T --> HOLogic.mk_setT atomT) $ Free (s, T))) |
1111 (Const ("Nominal.supp", T --> HOLogic.mk_setT atomT) $ Free (s, T))) |
1158 (fresh_const T U $ Free y $ Free x)) (rev xss @ yss)) ys @ |
1171 (fresh_const T U $ Free y $ Free x)) (rev xss @ yss)) ys @ |
1159 mk_fresh2 (p :: xss) yss; |
1172 mk_fresh2 (p :: xss) yss; |
1160 |
1173 |
1161 fun make_ind_prem fsT f k T ((cname, cargs), idxs) = |
1174 fun make_ind_prem fsT f k T ((cname, cargs), idxs) = |
1162 let |
1175 let |
1163 val recs = filter is_rec_type cargs; |
1176 val recs = filter Datatype_Aux.is_rec_type cargs; |
1164 val Ts = map (typ_of_dtyp descr'') cargs; |
1177 val Ts = map (Datatype_Aux.typ_of_dtyp descr'') cargs; |
1165 val recTs' = map (typ_of_dtyp descr'') recs; |
1178 val recTs' = map (Datatype_Aux.typ_of_dtyp descr'') recs; |
1166 val tnames = Name.variant_list pnames (Datatype_Prop.make_tnames Ts); |
1179 val tnames = Name.variant_list pnames (Datatype_Prop.make_tnames Ts); |
1167 val rec_tnames = map fst (filter (is_rec_type o snd) (tnames ~~ cargs)); |
1180 val rec_tnames = map fst (filter (Datatype_Aux.is_rec_type o snd) (tnames ~~ cargs)); |
1168 val frees = tnames ~~ Ts; |
1181 val frees = tnames ~~ Ts; |
1169 val frees' = partition_cargs idxs frees; |
1182 val frees' = partition_cargs idxs frees; |
1170 val z = (singleton (Name.variant_list tnames) "z", fsT); |
1183 val z = (singleton (Name.variant_list tnames) "z", fsT); |
1171 |
1184 |
1172 fun mk_prem ((dt, s), T) = |
1185 fun mk_prem ((dt, s), T) = |
1173 let |
1186 let |
1174 val (Us, U) = strip_type T; |
1187 val (Us, U) = strip_type T; |
1175 val l = length Us |
1188 val l = length Us; |
1176 in list_all (z :: map (pair "x") Us, HOLogic.mk_Trueprop |
1189 in |
1177 (make_pred fsT (body_index dt) U $ Bound l $ app_bnds (Free (s, T)) l)) |
1190 list_all (z :: map (pair "x") Us, |
|
1191 HOLogic.mk_Trueprop |
|
1192 (make_pred fsT (Datatype_Aux.body_index dt) U $ Bound l $ |
|
1193 Datatype_Aux.app_bnds (Free (s, T)) l)) |
1178 end; |
1194 end; |
1179 |
1195 |
1180 val prems = map mk_prem (recs ~~ rec_tnames ~~ recTs'); |
1196 val prems = map mk_prem (recs ~~ rec_tnames ~~ recTs'); |
1181 val prems' = map (fn p as (_, T) => HOLogic.mk_Trueprop |
1197 val prems' = map (fn p as (_, T) => HOLogic.mk_Trueprop |
1182 (f T (Free p) (Free z))) (maps fst frees') @ |
1198 (f T (Free p) (Free z))) (maps fst frees') @ |
1430 if length descr'' = 1 then [big_rec_name] else |
1446 if length descr'' = 1 then [big_rec_name] else |
1431 map ((curry (op ^) (big_rec_name ^ "_")) o string_of_int) |
1447 map ((curry (op ^) (big_rec_name ^ "_")) o string_of_int) |
1432 (1 upto (length descr'')); |
1448 (1 upto (length descr'')); |
1433 val rec_set_names = map (Sign.full_bname thy10) rec_set_names'; |
1449 val rec_set_names = map (Sign.full_bname thy10) rec_set_names'; |
1434 |
1450 |
1435 val rec_fns = map (uncurry (mk_Free "f")) |
1451 val rec_fns = map (uncurry (Datatype_Aux.mk_Free "f")) |
1436 (rec_fn_Ts ~~ (1 upto (length rec_fn_Ts))); |
1452 (rec_fn_Ts ~~ (1 upto (length rec_fn_Ts))); |
1437 val rec_sets' = map (fn c => list_comb (Free c, rec_fns)) |
1453 val rec_sets' = map (fn c => list_comb (Free c, rec_fns)) |
1438 (rec_set_names' ~~ rec_set_Ts); |
1454 (rec_set_names' ~~ rec_set_Ts); |
1439 val rec_sets = map (fn c => list_comb (Const c, rec_fns)) |
1455 val rec_sets = map (fn c => list_comb (Const c, rec_fns)) |
1440 (rec_set_names ~~ rec_set_Ts); |
1456 (rec_set_names ~~ rec_set_Ts); |
1455 val rec_ctxt = Free ("z", fsT'); |
1471 val rec_ctxt = Free ("z", fsT'); |
1456 |
1472 |
1457 fun make_rec_intr T p rec_set ((cname, cargs), idxs) |
1473 fun make_rec_intr T p rec_set ((cname, cargs), idxs) |
1458 (rec_intr_ts, rec_prems, rec_prems', rec_eq_prems, l) = |
1474 (rec_intr_ts, rec_prems, rec_prems', rec_eq_prems, l) = |
1459 let |
1475 let |
1460 val Ts = map (typ_of_dtyp descr'') cargs; |
1476 val Ts = map (Datatype_Aux.typ_of_dtyp descr'') cargs; |
1461 val frees = map (fn i => "x" ^ string_of_int i) (1 upto length Ts) ~~ Ts; |
1477 val frees = map (fn i => "x" ^ string_of_int i) (1 upto length Ts) ~~ Ts; |
1462 val frees' = partition_cargs idxs frees; |
1478 val frees' = partition_cargs idxs frees; |
1463 val binders = maps fst frees'; |
1479 val binders = maps fst frees'; |
1464 val atomTs = distinct op = (maps (map snd o fst) frees'); |
1480 val atomTs = distinct op = (maps (map snd o fst) frees'); |
1465 val recs = map_filter |
1481 val recs = map_filter |
1466 (fn ((_, DtRec i), p) => SOME (i, p) | _ => NONE) |
1482 (fn ((_, Datatype_Aux.DtRec i), p) => SOME (i, p) | _ => NONE) |
1467 (partition_cargs idxs cargs ~~ frees'); |
1483 (partition_cargs idxs cargs ~~ frees'); |
1468 val frees'' = map (fn i => "y" ^ string_of_int i) (1 upto length recs) ~~ |
1484 val frees'' = map (fn i => "y" ^ string_of_int i) (1 upto length recs) ~~ |
1469 map (fn (i, _) => nth rec_result_Ts i) recs; |
1485 map (fn (i, _) => nth rec_result_Ts i) recs; |
1470 val prems1 = map (fn ((i, (_, x)), y) => HOLogic.mk_Trueprop |
1486 val prems1 = map (fn ((i, (_, x)), y) => HOLogic.mk_Trueprop |
1471 (nth rec_sets' i $ Free x $ Free y)) (recs ~~ frees''); |
1487 (nth rec_sets' i $ Free x $ Free y)) (recs ~~ frees''); |
1523 |
1539 |
1524 val (rec_equiv_thms, rec_equiv_thms') = ListPair.unzip (map (fn aT => |
1540 val (rec_equiv_thms, rec_equiv_thms') = ListPair.unzip (map (fn aT => |
1525 let |
1541 let |
1526 val permT = mk_permT aT; |
1542 val permT = mk_permT aT; |
1527 val pi = Free ("pi", permT); |
1543 val pi = Free ("pi", permT); |
1528 val rec_fns_pi = map (mk_perm [] pi o uncurry (mk_Free "f")) |
1544 val rec_fns_pi = map (mk_perm [] pi o uncurry (Datatype_Aux.mk_Free "f")) |
1529 (rec_fn_Ts ~~ (1 upto (length rec_fn_Ts))); |
1545 (rec_fn_Ts ~~ (1 upto (length rec_fn_Ts))); |
1530 val rec_sets_pi = map (fn c => list_comb (Const c, rec_fns_pi)) |
1546 val rec_sets_pi = map (fn c => list_comb (Const c, rec_fns_pi)) |
1531 (rec_set_names ~~ rec_set_Ts); |
1547 (rec_set_names ~~ rec_set_Ts); |
1532 val ps = map (fn ((((T, U), R), R'), i) => |
1548 val ps = map (fn ((((T, U), R), R'), i) => |
1533 let |
1549 let |
1534 val x = Free ("x" ^ string_of_int i, T); |
1550 val x = Free ("x" ^ string_of_int i, T); |
1535 val y = Free ("y" ^ string_of_int i, U) |
1551 val y = Free ("y" ^ string_of_int i, U) |
1536 in |
1552 in |
1537 (R $ x $ y, R' $ mk_perm [] pi x $ mk_perm [] pi y) |
1553 (R $ x $ y, R' $ mk_perm [] pi x $ mk_perm [] pi y) |
1538 end) (recTs ~~ rec_result_Ts ~~ rec_sets ~~ rec_sets_pi ~~ (1 upto length recTs)); |
1554 end) (recTs ~~ rec_result_Ts ~~ rec_sets ~~ rec_sets_pi ~~ (1 upto length recTs)); |
1539 val ths = map (fn th => Drule.export_without_context (th RS mp)) (split_conj_thm |
1555 val ths = map (fn th => Drule.export_without_context (th RS mp)) (Datatype_Aux.split_conj_thm |
1540 (Goal.prove_global thy11 [] [] |
1556 (Goal.prove_global thy11 [] [] |
1541 (augment_sort thy1 pt_cp_sort |
1557 (augment_sort thy1 pt_cp_sort |
1542 (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map HOLogic.mk_imp ps)))) |
1558 (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map HOLogic.mk_imp ps)))) |
1543 (fn _ => rtac rec_induct 1 THEN REPEAT |
1559 (fn _ => rtac rec_induct 1 THEN REPEAT |
1544 (simp_tac (Simplifier.global_context thy11 HOL_basic_ss |
1560 (simp_tac (Simplifier.global_context thy11 HOL_basic_ss |
1566 val finite = Const ("Finite_Set.finite", aset --> HOLogic.boolT); |
1582 val finite = Const ("Finite_Set.finite", aset --> HOLogic.boolT); |
1567 val fins = map (fn (f, T) => HOLogic.mk_Trueprop |
1583 val fins = map (fn (f, T) => HOLogic.mk_Trueprop |
1568 (finite $ (Const ("Nominal.supp", T --> aset) $ f))) |
1584 (finite $ (Const ("Nominal.supp", T --> aset) $ f))) |
1569 (rec_fns ~~ rec_fn_Ts) |
1585 (rec_fns ~~ rec_fn_Ts) |
1570 in |
1586 in |
1571 map (fn th => Drule.export_without_context (th RS mp)) (split_conj_thm |
1587 map (fn th => Drule.export_without_context (th RS mp)) (Datatype_Aux.split_conj_thm |
1572 (Goal.prove_global thy11 [] |
1588 (Goal.prove_global thy11 [] |
1573 (map (augment_sort thy11 fs_cp_sort) fins) |
1589 (map (augment_sort thy11 fs_cp_sort) fins) |
1574 (augment_sort thy11 fs_cp_sort |
1590 (augment_sort thy11 fs_cp_sort |
1575 (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
1591 (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
1576 (map (fn (((T, U), R), i) => |
1592 (map (fn (((T, U), R), i) => |
1703 val finite_ctxt_prems = map (fn aT => |
1719 val finite_ctxt_prems = map (fn aT => |
1704 HOLogic.mk_Trueprop |
1720 HOLogic.mk_Trueprop |
1705 (Const ("Finite_Set.finite", HOLogic.mk_setT aT --> HOLogic.boolT) $ |
1721 (Const ("Finite_Set.finite", HOLogic.mk_setT aT --> HOLogic.boolT) $ |
1706 (Const ("Nominal.supp", fsT' --> HOLogic.mk_setT aT) $ rec_ctxt))) dt_atomTs; |
1722 (Const ("Nominal.supp", fsT' --> HOLogic.mk_setT aT) $ rec_ctxt))) dt_atomTs; |
1707 |
1723 |
1708 val rec_unique_thms = split_conj_thm (Goal.prove |
1724 val rec_unique_thms = Datatype_Aux.split_conj_thm (Goal.prove |
1709 (Proof_Context.init_global thy11) (map fst rec_unique_frees) |
1725 (Proof_Context.init_global thy11) (map fst rec_unique_frees) |
1710 (map (augment_sort thy11 fs_cp_sort) |
1726 (map (augment_sort thy11 fs_cp_sort) |
1711 (flat finite_premss @ finite_ctxt_prems @ rec_prems @ rec_prems')) |
1727 (flat finite_premss @ finite_ctxt_prems @ rec_prems @ rec_prems')) |
1712 (augment_sort thy11 fs_cp_sort |
1728 (augment_sort thy11 fs_cp_sort |
1713 (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj rec_unique_concls))) |
1729 (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj rec_unique_concls))) |
1716 val k = length rec_fns; |
1732 val k = length rec_fns; |
1717 val (finite_thss, ths1) = fold_map (fn T => fn xs => |
1733 val (finite_thss, ths1) = fold_map (fn T => fn xs => |
1718 apfst (pair T) (chop k xs)) dt_atomTs prems; |
1734 apfst (pair T) (chop k xs)) dt_atomTs prems; |
1719 val (finite_ctxt_ths, ths2) = chop (length dt_atomTs) ths1; |
1735 val (finite_ctxt_ths, ths2) = chop (length dt_atomTs) ths1; |
1720 val (P_ind_ths, fcbs) = chop k ths2; |
1736 val (P_ind_ths, fcbs) = chop k ths2; |
1721 val P_ths = map (fn th => th RS mp) (split_conj_thm |
1737 val P_ths = map (fn th => th RS mp) (Datatype_Aux.split_conj_thm |
1722 (Goal.prove context |
1738 (Goal.prove context |
1723 (map fst (rec_unique_frees'' @ rec_unique_frees')) [] |
1739 (map fst (rec_unique_frees'' @ rec_unique_frees')) [] |
1724 (augment_sort thy11 fs_cp_sort |
1740 (augment_sort thy11 fs_cp_sort |
1725 (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
1741 (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
1726 (map (fn (((x, y), S), P) => HOLogic.mk_imp |
1742 (map (fn (((x, y), S), P) => HOLogic.mk_imp |