1 (* Title: nominal_atoms/ML |
|
2 Authors: Brian Huffman, Christian Urban |
|
3 |
|
4 Command for defining concrete atom types. |
|
5 |
|
6 At the moment, only single-sorted atom types |
|
7 are supported. |
|
8 *) |
|
9 |
|
10 signature ATOM_DECL = |
|
11 sig |
|
12 val add_atom_decl: (binding * (binding option)) -> theory -> theory |
|
13 end; |
|
14 |
|
15 structure Atom_Decl :> ATOM_DECL = |
|
16 struct |
|
17 |
|
18 fun atom_decl_set (str : string) : term = |
|
19 let |
|
20 val a = Free ("a", @{typ atom}); |
|
21 val s = Const (@{const_name "Sort"}, @{typ "string => atom_sort list => atom_sort"}) |
|
22 $ HOLogic.mk_string str $ HOLogic.nil_const @{typ "atom_sort"}; |
|
23 in |
|
24 HOLogic.mk_Collect ("a", @{typ atom}, HOLogic.mk_eq (mk_sort_of a, s)) |
|
25 end |
|
26 |
|
27 fun add_atom_decl (name : binding, arg : binding option) (thy : theory) = |
|
28 let |
|
29 val _ = Theory.requires thy "Nominal2_Base" "nominal logic"; |
|
30 val str = Sign.full_name thy name; |
|
31 |
|
32 (* typedef *) |
|
33 val set = atom_decl_set str; |
|
34 val tac = rtac @{thm exists_eq_simple_sort} 1; |
|
35 val ((full_tname, info as ({Rep_name, Abs_name, ...}, {type_definition, ...})), thy) = |
|
36 Typedef.add_typedef_global false NONE (name, [], NoSyn) set NONE tac thy; |
|
37 |
|
38 (* definition of atom and permute *) |
|
39 val newT = #abs_type (fst info); |
|
40 val RepC = Const (Rep_name, newT --> @{typ atom}); |
|
41 val AbsC = Const (Abs_name, @{typ atom} --> newT); |
|
42 val a = Free ("a", newT); |
|
43 val p = Free ("p", @{typ perm}); |
|
44 val atom_eqn = |
|
45 HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_atom a, RepC $ a)); |
|
46 val permute_eqn = |
|
47 HOLogic.mk_Trueprop (HOLogic.mk_eq |
|
48 (mk_perm p a, AbsC $ (mk_perm p (RepC $ a)))); |
|
49 val atom_def_name = |
|
50 Binding.prefix_name "atom_" (Binding.suffix_name "_def" name); |
|
51 val permute_def_name = |
|
52 Binding.prefix_name "permute_" (Binding.suffix_name "_def" name); |
|
53 |
|
54 (* at class instance *) |
|
55 val lthy = |
|
56 Class.instantiation ([full_tname], [], @{sort at}) thy; |
|
57 val ((_, (_, permute_ldef)), lthy) = |
|
58 Specification.definition (NONE, ((permute_def_name, []), permute_eqn)) lthy; |
|
59 val ((_, (_, atom_ldef)), lthy) = |
|
60 Specification.definition (NONE, ((atom_def_name, []), atom_eqn)) lthy; |
|
61 val ctxt_thy = ProofContext.init_global (ProofContext.theory_of lthy); |
|
62 val permute_def = singleton (ProofContext.export lthy ctxt_thy) permute_ldef; |
|
63 val atom_def = singleton (ProofContext.export lthy ctxt_thy) atom_ldef; |
|
64 val class_thm = @{thm at_class} OF [type_definition, atom_def, permute_def]; |
|
65 val thy = lthy |
|
66 |> Class.prove_instantiation_instance (K (Tactic.rtac class_thm 1)) |
|
67 |> Local_Theory.exit_global; |
|
68 in |
|
69 thy |
|
70 end; |
|
71 |
|
72 (** outer syntax **) |
|
73 |
|
74 local structure P = Parse and K = Keyword in |
|
75 |
|
76 val _ = |
|
77 Outer_Syntax.command "atom_decl" "declaration of a concrete atom type" K.thy_decl |
|
78 ((P.binding -- Scan.option (Args.parens (P.binding))) >> |
|
79 (Toplevel.print oo (Toplevel.theory o add_atom_decl))); |
|
80 |
|
81 end; |
|
82 |
|
83 end; |
|