44 val pi = Free ("pi", @{typ perm}); |
44 val pi = Free ("pi", @{typ perm}); |
45 fun permute ty = Const (@{const_name permute}, @{typ perm} --> ty --> ty); |
45 fun permute ty = Const (@{const_name permute}, @{typ perm} --> ty --> ty); |
46 val minus_perm = Const (@{const_name minus}, @{typ perm} --> @{typ perm}); |
46 val minus_perm = Const (@{const_name minus}, @{typ perm} --> @{typ perm}); |
47 *} |
47 *} |
48 ML {* |
48 ML {* |
49 fun perm_eq (i, (_, _, constrs)) = |
49 fun perm_eq_constr i (cname, dts) = |
50 map (fn (cname, dts) => |
50 let |
51 let |
51 val Ts = map (typ_of_dtyp descr sorts) dts; |
52 val Ts = map (typ_of_dtyp descr sorts) dts; |
52 val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts); |
53 val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts); |
53 val args = map Free (names ~~ Ts); |
54 val args = map Free (names ~~ Ts); |
54 val c = Const (cname, Ts ---> (nth_dtyp i)); |
55 val c = Const (cname, Ts ---> (nth_dtyp i)); |
55 fun perm_arg (dt, x) = |
56 fun perm_arg (dt, x) = |
56 let val T = type_of x |
57 let val T = type_of x |
57 in |
58 in |
58 if is_rec_type dt then |
59 if is_rec_type dt then |
59 let val (Us, _) = strip_type T |
60 let val (Us, _) = strip_type T |
60 in list_abs (map (pair "x") Us, |
61 in list_abs (map (pair "x") Us, |
61 Free (nth perm_names_types' (body_index dt)) $ pi $ |
62 Free (nth perm_names_types' (body_index dt)) $ pi $ |
62 list_comb (x, map (fn (i, U) => |
63 list_comb (x, map (fn (i, U) => |
63 (permute U) $ (minus_perm $ pi) $ Bound i) |
64 (permute U) $ (minus_perm $ pi) $ Bound i) |
64 ((length Us - 1 downto 0) ~~ Us))) |
65 ((length Us - 1 downto 0) ~~ Us))) |
65 end |
66 end |
66 else (permute T) $ pi $ x |
67 else (permute T) $ pi $ x |
67 end; |
68 end; |
68 in |
69 in |
69 (Attrib.empty_binding, HOLogic.mk_Trueprop (HOLogic.mk_eq |
70 (Attrib.empty_binding, HOLogic.mk_Trueprop (HOLogic.mk_eq |
70 (Free (nth perm_names_types' i) $ |
71 (Free (nth perm_names_types' i) $ |
71 Free ("pi", @{typ perm}) $ list_comb (c, args), |
72 Free ("pi", @{typ perm}) $ list_comb (c, args), |
72 list_comb (c, map perm_arg (dts ~~ args))))) |
73 list_comb (c, map perm_arg (dts ~~ args))))) |
73 end; |
74 end) constrs; |
74 fun perm_eq (i, (_, _, constrs)) = map (perm_eq_constr i) constrs; |
75 val perm_eqs = maps perm_eq descr; |
75 val perm_eqs = maps perm_eq descr; |
76 *} |
76 *} |
77 |
77 |
78 local_setup {* |
78 local_setup {* |
79 snd o (Primrec.add_primrec |
79 snd o (Primrec.add_primrec |