1079
|
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 |
|
2891
304dfe6cc83a
the simplifier can simplify "sort (atom a)" if a is a concrete atom type declared with atom_decl
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
18 |
val simp_attr = Attrib.internal (K Simplifier.simp_add)
|
304dfe6cc83a
the simplifier can simplify "sort (atom a)" if a is a concrete atom type declared with atom_decl
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
19 |
|
1079
|
20 |
fun atom_decl_set (str : string) : term =
|
|
21 |
let
|
1962
84a13d1e2511
moved mk_atom into the library; that meant that concrete atom classes need to be in Nominal2_Base
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
22 |
val a = Free ("a", @{typ atom});
|
1079
|
23 |
val s = Const (@{const_name "Sort"}, @{typ "string => atom_sort list => atom_sort"})
|
|
24 |
$ HOLogic.mk_string str $ HOLogic.nil_const @{typ "atom_sort"};
|
|
25 |
in
|
1962
84a13d1e2511
moved mk_atom into the library; that meant that concrete atom classes need to be in Nominal2_Base
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
26 |
HOLogic.mk_Collect ("a", @{typ atom}, HOLogic.mk_eq (mk_sort_of a, s))
|
1079
|
27 |
end
|
|
28 |
|
|
29 |
fun add_atom_decl (name : binding, arg : binding option) (thy : theory) =
|
|
30 |
let
|
2467
|
31 |
val _ = Theory.requires thy "Nominal2_Base" "nominal logic";
|
1079
|
32 |
val str = Sign.full_name thy name;
|
|
33 |
|
|
34 |
(* typedef *)
|
|
35 |
val set = atom_decl_set str;
|
|
36 |
val tac = rtac @{thm exists_eq_simple_sort} 1;
|
1689
8c0eef2b84e7
fixed a problem due to a change in type-def (needs new Isabelle)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
37 |
val ((full_tname, info as ({Rep_name, Abs_name, ...}, {type_definition, ...})), thy) =
|
3202
|
38 |
Typedef.add_typedef_global (name, [], NoSyn) set NONE tac thy;
|
1079
|
39 |
|
|
40 |
(* definition of atom and permute *)
|
1689
8c0eef2b84e7
fixed a problem due to a change in type-def (needs new Isabelle)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
41 |
val newT = #abs_type (fst info);
|
1962
84a13d1e2511
moved mk_atom into the library; that meant that concrete atom classes need to be in Nominal2_Base
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
42 |
val RepC = Const (Rep_name, newT --> @{typ atom});
|
84a13d1e2511
moved mk_atom into the library; that meant that concrete atom classes need to be in Nominal2_Base
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
43 |
val AbsC = Const (Abs_name, @{typ atom} --> newT);
|
1079
|
44 |
val a = Free ("a", newT);
|
1962
84a13d1e2511
moved mk_atom into the library; that meant that concrete atom classes need to be in Nominal2_Base
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
45 |
val p = Free ("p", @{typ perm});
|
1079
|
46 |
val atom_eqn =
|
|
47 |
HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_atom a, RepC $ a));
|
|
48 |
val permute_eqn =
|
|
49 |
HOLogic.mk_Trueprop (HOLogic.mk_eq
|
1962
84a13d1e2511
moved mk_atom into the library; that meant that concrete atom classes need to be in Nominal2_Base
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
50 |
(mk_perm p a, AbsC $ (mk_perm p (RepC $ a))));
|
1079
|
51 |
val atom_def_name =
|
|
52 |
Binding.prefix_name "atom_" (Binding.suffix_name "_def" name);
|
2891
304dfe6cc83a
the simplifier can simplify "sort (atom a)" if a is a concrete atom type declared with atom_decl
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
53 |
val sort_thm_name =
|
304dfe6cc83a
the simplifier can simplify "sort (atom a)" if a is a concrete atom type declared with atom_decl
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
54 |
Binding.prefix_name "atom_" (Binding.suffix_name "_sort" name);
|
1079
|
55 |
val permute_def_name =
|
|
56 |
Binding.prefix_name "permute_" (Binding.suffix_name "_def" name);
|
|
57 |
|
|
58 |
(* at class instance *)
|
|
59 |
val lthy =
|
2396
|
60 |
Class.instantiation ([full_tname], [], @{sort at}) thy;
|
1079
|
61 |
val ((_, (_, permute_ldef)), lthy) =
|
|
62 |
Specification.definition (NONE, ((permute_def_name, []), permute_eqn)) lthy;
|
|
63 |
val ((_, (_, atom_ldef)), lthy) =
|
|
64 |
Specification.definition (NONE, ((atom_def_name, []), atom_eqn)) lthy;
|
3045
d0ad264f8c4f
updated to Isabelle 3 Nov; it includes a hack to work around a bug in the localised version of the quotient package
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
65 |
val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy);
|
d0ad264f8c4f
updated to Isabelle 3 Nov; it includes a hack to work around a bug in the localised version of the quotient package
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
66 |
val permute_def = singleton (Proof_Context.export lthy ctxt_thy) permute_ldef;
|
d0ad264f8c4f
updated to Isabelle 3 Nov; it includes a hack to work around a bug in the localised version of the quotient package
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
67 |
val atom_def = singleton (Proof_Context.export lthy ctxt_thy) atom_ldef;
|
1079
|
68 |
val class_thm = @{thm at_class} OF [type_definition, atom_def, permute_def];
|
2891
304dfe6cc83a
the simplifier can simplify "sort (atom a)" if a is a concrete atom type declared with atom_decl
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
69 |
val sort_thm = @{thm at_class_sort} OF [type_definition, atom_def]
|
1079
|
70 |
val thy = lthy
|
2891
304dfe6cc83a
the simplifier can simplify "sort (atom a)" if a is a concrete atom type declared with atom_decl
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
71 |
|> snd o (Local_Theory.note ((sort_thm_name, [simp_attr]), [sort_thm]))
|
304dfe6cc83a
the simplifier can simplify "sort (atom a)" if a is a concrete atom type declared with atom_decl
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
72 |
|> Class.prove_instantiation_instance (K (rtac class_thm 1))
|
1079
|
73 |
|> Local_Theory.exit_global;
|
|
74 |
in
|
|
75 |
thy
|
|
76 |
end;
|
|
77 |
|
|
78 |
(** outer syntax **)
|
|
79 |
val _ =
|
3193
|
80 |
Outer_Syntax.command @{command_spec "atom_decl"}
|
3135
|
81 |
"declaration of a concrete atom type"
|
|
82 |
((Parse.binding -- Scan.option (Args.parens (Parse.binding))) >>
|
|
83 |
(Toplevel.print oo (Toplevel.theory o add_atom_decl)))
|
1079
|
84 |
|
|
85 |
end;
|