13 end; |
13 end; |
14 |
14 |
15 structure Atom_Decl :> ATOM_DECL = |
15 structure Atom_Decl :> ATOM_DECL = |
16 struct |
16 struct |
17 |
17 |
18 val atomT = @{typ atom}; |
|
19 val permT = @{typ perm}; |
|
20 |
|
21 val sort_of_const = @{term sort_of}; |
|
22 fun atom_const T = Const (@{const_name atom}, T --> atomT); |
|
23 fun permute_const T = Const (@{const_name permute}, permT --> T --> T); |
|
24 |
|
25 fun mk_sort_of t = sort_of_const $ t; |
|
26 fun mk_atom t = atom_const (fastype_of t) $ t; |
|
27 fun mk_permute (p, t) = permute_const (fastype_of t) $ p $ t; |
|
28 |
|
29 fun atom_decl_set (str : string) : term = |
18 fun atom_decl_set (str : string) : term = |
30 let |
19 let |
31 val a = Free ("a", atomT); |
20 val a = Free ("a", @{typ atom}); |
32 val s = Const (@{const_name "Sort"}, @{typ "string => atom_sort list => atom_sort"}) |
21 val s = Const (@{const_name "Sort"}, @{typ "string => atom_sort list => atom_sort"}) |
33 $ HOLogic.mk_string str $ HOLogic.nil_const @{typ "atom_sort"}; |
22 $ HOLogic.mk_string str $ HOLogic.nil_const @{typ "atom_sort"}; |
34 in |
23 in |
35 HOLogic.mk_Collect ("a", atomT, HOLogic.mk_eq (mk_sort_of a, s)) |
24 HOLogic.mk_Collect ("a", @{typ atom}, HOLogic.mk_eq (mk_sort_of a, s)) |
36 end |
25 end |
37 |
26 |
38 fun add_atom_decl (name : binding, arg : binding option) (thy : theory) = |
27 fun add_atom_decl (name : binding, arg : binding option) (thy : theory) = |
39 let |
28 let |
40 val _ = Theory.requires thy "Nominal2_Atoms" "nominal logic"; |
29 val _ = Theory.requires thy "Nominal2_Atoms" "nominal logic"; |
46 val ((full_tname, info as ({Rep_name, Abs_name, ...}, {type_definition, ...})), thy) = |
35 val ((full_tname, info as ({Rep_name, Abs_name, ...}, {type_definition, ...})), thy) = |
47 Typedef.add_typedef_global false NONE (name, [], NoSyn) set NONE tac thy; |
36 Typedef.add_typedef_global false NONE (name, [], NoSyn) set NONE tac thy; |
48 |
37 |
49 (* definition of atom and permute *) |
38 (* definition of atom and permute *) |
50 val newT = #abs_type (fst info); |
39 val newT = #abs_type (fst info); |
51 val RepC = Const (Rep_name, newT --> atomT); |
40 val RepC = Const (Rep_name, newT --> @{typ atom}); |
52 val AbsC = Const (Abs_name, atomT --> newT); |
41 val AbsC = Const (Abs_name, @{typ atom} --> newT); |
53 val a = Free ("a", newT); |
42 val a = Free ("a", newT); |
54 val p = Free ("p", permT); |
43 val p = Free ("p", @{typ perm}); |
55 val atom_eqn = |
44 val atom_eqn = |
56 HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_atom a, RepC $ a)); |
45 HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_atom a, RepC $ a)); |
57 val permute_eqn = |
46 val permute_eqn = |
58 HOLogic.mk_Trueprop (HOLogic.mk_eq |
47 HOLogic.mk_Trueprop (HOLogic.mk_eq |
59 (mk_permute (p, a), AbsC $ (mk_permute (p, RepC $ a)))); |
48 (mk_perm p a, AbsC $ (mk_perm p (RepC $ a)))); |
60 val atom_def_name = |
49 val atom_def_name = |
61 Binding.prefix_name "atom_" (Binding.suffix_name "_def" name); |
50 Binding.prefix_name "atom_" (Binding.suffix_name "_def" name); |
62 val permute_def_name = |
51 val permute_def_name = |
63 Binding.prefix_name "permute_" (Binding.suffix_name "_def" name); |
52 Binding.prefix_name "permute_" (Binding.suffix_name "_def" name); |
64 |
53 |