1 theory Perm |
1 theory Perm |
2 imports |
2 imports |
3 "../Nominal-General/Nominal2_Base" |
3 "../Nominal-General/Nominal2_Base" |
4 "../Nominal-General/Nominal2_Atoms" |
4 "../Nominal-General/Nominal2_Atoms" |
5 "Nominal2_FSet" |
5 "Nominal2_FSet" "Abs" |
6 uses ("nominal_dt_rawperm.ML") |
6 uses ("nominal_dt_rawperm.ML") |
7 ("nominal_dt_rawfuns.ML") |
7 ("nominal_dt_rawfuns.ML") |
|
8 ("nominal_dt_alpha.ML") |
8 begin |
9 begin |
9 |
10 |
10 use "nominal_dt_rawperm.ML" |
11 use "nominal_dt_rawperm.ML" |
|
12 ML {* open Nominal_Dt_RawPerm *} |
|
13 |
11 use "nominal_dt_rawfuns.ML" |
14 use "nominal_dt_rawfuns.ML" |
|
15 ML {* open Nominal_Dt_RawFuns *} |
12 |
16 |
13 ML {* |
17 use "nominal_dt_alpha.ML" |
14 open Nominal_Dt_RawPerm |
18 ML {* open Nominal_Dt_Alpha *} |
15 open Nominal_Dt_RawFuns |
|
16 *} |
|
17 |
19 |
18 ML {* |
|
19 fun is_atom ctxt ty = |
|
20 Sign.of_sort (ProofContext.theory_of ctxt) (ty, @{sort at_base}) |
|
21 |
|
22 fun is_atom_set ctxt (Type ("fun", [t, @{typ bool}])) = is_atom ctxt t |
|
23 | is_atom_set _ _ = false; |
|
24 |
|
25 fun is_atom_fset ctxt (Type (@{type_name "fset"}, [t])) = is_atom ctxt t |
|
26 | is_atom_fset _ _ = false; |
|
27 |
|
28 fun is_atom_list ctxt (Type (@{type_name "list"}, [t])) = is_atom ctxt t |
|
29 | is_atom_list _ _ = false |
|
30 |
|
31 |
|
32 (* functions for producing sets, fsets and lists of general atom type |
|
33 out from concrete atom types *) |
|
34 fun mk_atom_set t = |
|
35 let |
|
36 val ty = fastype_of t; |
|
37 val atom_ty = HOLogic.dest_setT ty --> @{typ "atom"}; |
|
38 val img_ty = atom_ty --> ty --> @{typ "atom set"}; |
|
39 in |
|
40 Const (@{const_name image}, img_ty) $ mk_atom_ty atom_ty t |
|
41 end |
|
42 |
|
43 fun mk_atom_fset t = |
|
44 let |
|
45 val ty = fastype_of t; |
|
46 val atom_ty = dest_fsetT ty --> @{typ "atom"}; |
|
47 val fmap_ty = atom_ty --> ty --> @{typ "atom fset"}; |
|
48 val fset_to_set = @{term "fset_to_set :: atom fset => atom set"} |
|
49 in |
|
50 fset_to_set $ (Const (@{const_name fmap}, fmap_ty) $ Const (@{const_name atom}, atom_ty) $ t) |
|
51 end |
|
52 *} |
|
53 (* permutations for quotient types *) |
20 (* permutations for quotient types *) |
54 |
|
55 ML {* Class_Target.prove_instantiation_exit_result *} |
|
56 |
21 |
57 ML {* |
22 ML {* |
58 fun quotient_lift_consts_export qtys spec ctxt = |
23 fun quotient_lift_consts_export qtys spec ctxt = |
59 let |
24 let |
60 val (result, ctxt') = fold_map (Quotient_Def.quotient_lift_const qtys) spec ctxt; |
25 val (result, ctxt') = fold_map (Quotient_Def.quotient_lift_const qtys) spec ctxt; |