2 imports "../Nominal-General/Nominal2_Atoms" |
2 imports "../Nominal-General/Nominal2_Atoms" |
3 begin |
3 begin |
4 |
4 |
5 ML {* |
5 ML {* |
6 open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *) |
6 open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *) |
7 fun permute ty = Const (@{const_name permute}, @{typ perm} --> ty --> ty); |
7 open Nominal_Library; |
8 val minus_perm = Const (@{const_name minus}, @{typ perm} --> @{typ perm}); |
|
9 *} |
8 *} |
10 |
9 |
11 ML {* |
10 ML {* |
12 fun quotient_lift_consts_export qtys spec ctxt = |
11 fun quotient_lift_consts_export qtys spec ctxt = |
13 let |
12 let |
92 if is_rec_type dt then |
91 if is_rec_type dt then |
93 let val (Us, _) = strip_type T |
92 let val (Us, _) = strip_type T |
94 in list_abs (map (pair "x") Us, |
93 in list_abs (map (pair "x") Us, |
95 Free (nth perm_names_types' (body_index dt)) $ pi $ |
94 Free (nth perm_names_types' (body_index dt)) $ pi $ |
96 list_comb (x, map (fn (i, U) => |
95 list_comb (x, map (fn (i, U) => |
97 (permute U) $ (minus_perm $ pi) $ Bound i) |
96 (mk_perm_ty U (mk_minus pi) (Bound i))) |
98 ((length Us - 1 downto 0) ~~ Us))) |
97 ((length Us - 1 downto 0) ~~ Us))) |
99 end |
98 end |
100 else (permute T) $ pi $ x |
99 else (mk_perm_ty T pi x) |
101 end; |
100 end; |
102 in |
101 in |
103 (Attrib.empty_binding, HOLogic.mk_Trueprop (HOLogic.mk_eq |
102 (Attrib.empty_binding, HOLogic.mk_Trueprop (HOLogic.mk_eq |
104 (Free (nth perm_names_types' i) $ |
103 (Free (nth perm_names_types' i) $ |
105 Free ("pi", @{typ perm}) $ list_comb (c, args), |
104 Free ("pi", @{typ perm}) $ list_comb (c, args), |
123 (map (Morphism.thm phi) dfs, map (Morphism.thm phi) simps, map (Morphism.term phi) fvs); |
122 (map (Morphism.thm phi) dfs, map (Morphism.thm phi) simps, map (Morphism.term phi) fvs); |
124 in |
123 in |
125 lthy' |
124 lthy' |
126 |> snd o (Local_Theory.note ((perms_zero_bind, []), perm_empty_thms)) |
125 |> snd o (Local_Theory.note ((perms_zero_bind, []), perm_empty_thms)) |
127 |> snd o (Local_Theory.note ((perms_append_bind, []), perm_append_thms)) |
126 |> snd o (Local_Theory.note ((perms_append_bind, []), perm_append_thms)) |
128 |> Class_Target.prove_instantiation_exit_result morphism tac (perm_ldef, (perm_empty_thms @ perm_append_thms), perm_frees) |
127 |> Class_Target.prove_instantiation_exit_result morphism tac |
|
128 (perm_ldef, (perm_empty_thms @ perm_append_thms), perm_frees) |
129 end |
129 end |
130 |
130 |
131 *} |
131 *} |
132 |
132 |
133 ML {* |
133 ML {* |