author | Cezary Kaliszyk <kaliszyk@in.tum.de> |
Wed, 26 May 2010 16:09:09 +0200 | |
changeset 2187 | f9cc69b432ff |
parent 1979 | 760257a66604 |
child 2288 | 3b83960f9544 |
permissions | -rw-r--r-- |
1833
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1 |
(* Title: nominal_library.ML |
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
2 |
Author: Christian Urban |
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
3 |
|
1979
760257a66604
added basic functions for constructing supp-terms
Christian Urban <urbanc@in.tum.de>
parents:
1963
diff
changeset
|
4 |
Basic functions for nominal. |
1833
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
5 |
*) |
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
6 |
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
7 |
signature NOMINAL_LIBRARY = |
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
8 |
sig |
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
9 |
val mk_minus: term -> term |
1896
996d4411e95e
tuned; fleshed out some library functions about permutations; closed Datatype_Aux structure (increases readability)
Christian Urban <urbanc@in.tum.de>
parents:
1871
diff
changeset
|
10 |
val mk_plus: term -> term -> term |
996d4411e95e
tuned; fleshed out some library functions about permutations; closed Datatype_Aux structure (increases readability)
Christian Urban <urbanc@in.tum.de>
parents:
1871
diff
changeset
|
11 |
|
1899
8e0bfb14f6bf
optimised the code of define_raw_perm
Christian Urban <urbanc@in.tum.de>
parents:
1896
diff
changeset
|
12 |
val perm_ty: typ -> typ |
1871
c704d129862b
moved some general function into nominal_library.ML
Christian Urban <urbanc@in.tum.de>
parents:
1834
diff
changeset
|
13 |
val mk_perm_ty: typ -> term -> term -> term |
1833
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
14 |
val mk_perm: term -> term -> term |
1834
9909cc3566c5
moved a couple of more functions to the library
Christian Urban <urbanc@in.tum.de>
parents:
1833
diff
changeset
|
15 |
val dest_perm: term -> term * term |
9909cc3566c5
moved a couple of more functions to the library
Christian Urban <urbanc@in.tum.de>
parents:
1833
diff
changeset
|
16 |
|
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>
parents:
1899
diff
changeset
|
17 |
val mk_sort_of: term -> term |
1979
760257a66604
added basic functions for constructing supp-terms
Christian Urban <urbanc@in.tum.de>
parents:
1963
diff
changeset
|
18 |
val atom_ty: typ -> typ |
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>
parents:
1899
diff
changeset
|
19 |
val mk_atom_ty: typ -> term -> term |
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>
parents:
1899
diff
changeset
|
20 |
val mk_atom: term -> term |
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>
parents:
1899
diff
changeset
|
21 |
|
1979
760257a66604
added basic functions for constructing supp-terms
Christian Urban <urbanc@in.tum.de>
parents:
1963
diff
changeset
|
22 |
val supp_ty: typ -> typ |
760257a66604
added basic functions for constructing supp-terms
Christian Urban <urbanc@in.tum.de>
parents:
1963
diff
changeset
|
23 |
val mk_supp_ty: typ -> term -> term |
760257a66604
added basic functions for constructing supp-terms
Christian Urban <urbanc@in.tum.de>
parents:
1963
diff
changeset
|
24 |
val mk_supp: term -> term |
760257a66604
added basic functions for constructing supp-terms
Christian Urban <urbanc@in.tum.de>
parents:
1963
diff
changeset
|
25 |
|
1834
9909cc3566c5
moved a couple of more functions to the library
Christian Urban <urbanc@in.tum.de>
parents:
1833
diff
changeset
|
26 |
val mk_equiv: thm -> thm |
9909cc3566c5
moved a couple of more functions to the library
Christian Urban <urbanc@in.tum.de>
parents:
1833
diff
changeset
|
27 |
val safe_mk_equiv: thm -> thm |
1833
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
28 |
end |
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
29 |
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
30 |
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
31 |
structure Nominal_Library: NOMINAL_LIBRARY = |
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
32 |
struct |
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
33 |
|
1979
760257a66604
added basic functions for constructing supp-terms
Christian Urban <urbanc@in.tum.de>
parents:
1963
diff
changeset
|
34 |
fun mk_minus p = @{term "uminus::perm => perm"} $ p; |
760257a66604
added basic functions for constructing supp-terms
Christian Urban <urbanc@in.tum.de>
parents:
1963
diff
changeset
|
35 |
|
760257a66604
added basic functions for constructing supp-terms
Christian Urban <urbanc@in.tum.de>
parents:
1963
diff
changeset
|
36 |
fun mk_plus p q = @{term "plus::perm => perm => perm"} $ p $ q; |
1896
996d4411e95e
tuned; fleshed out some library functions about permutations; closed Datatype_Aux structure (increases readability)
Christian Urban <urbanc@in.tum.de>
parents:
1871
diff
changeset
|
37 |
|
1979
760257a66604
added basic functions for constructing supp-terms
Christian Urban <urbanc@in.tum.de>
parents:
1963
diff
changeset
|
38 |
fun perm_ty ty = @{typ "perm"} --> ty --> ty; |
760257a66604
added basic functions for constructing supp-terms
Christian Urban <urbanc@in.tum.de>
parents:
1963
diff
changeset
|
39 |
fun mk_perm_ty ty p trm = Const (@{const_name "permute"}, perm_ty ty) $ p $ trm; |
760257a66604
added basic functions for constructing supp-terms
Christian Urban <urbanc@in.tum.de>
parents:
1963
diff
changeset
|
40 |
fun mk_perm p trm = mk_perm_ty (fastype_of trm) p trm; |
1833
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
41 |
|
1834
9909cc3566c5
moved a couple of more functions to the library
Christian Urban <urbanc@in.tum.de>
parents:
1833
diff
changeset
|
42 |
fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t) |
1979
760257a66604
added basic functions for constructing supp-terms
Christian Urban <urbanc@in.tum.de>
parents:
1963
diff
changeset
|
43 |
| dest_perm t = raise TERM ("dest_perm", [t]); |
1833
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
44 |
|
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>
parents:
1899
diff
changeset
|
45 |
|
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>
parents:
1899
diff
changeset
|
46 |
fun mk_sort_of t = @{term "sort_of"} $ t; |
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>
parents:
1899
diff
changeset
|
47 |
|
1979
760257a66604
added basic functions for constructing supp-terms
Christian Urban <urbanc@in.tum.de>
parents:
1963
diff
changeset
|
48 |
fun atom_ty ty = ty --> @{typ "atom"}; |
1963 | 49 |
fun mk_atom_ty ty t = Const (@{const_name "atom"}, atom_ty ty) $ t; |
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>
parents:
1899
diff
changeset
|
50 |
fun mk_atom t = mk_atom_ty (fastype_of t) t; |
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>
parents:
1899
diff
changeset
|
51 |
|
1979
760257a66604
added basic functions for constructing supp-terms
Christian Urban <urbanc@in.tum.de>
parents:
1963
diff
changeset
|
52 |
|
760257a66604
added basic functions for constructing supp-terms
Christian Urban <urbanc@in.tum.de>
parents:
1963
diff
changeset
|
53 |
fun supp_ty ty = ty --> @{typ "atom set"}; |
760257a66604
added basic functions for constructing supp-terms
Christian Urban <urbanc@in.tum.de>
parents:
1963
diff
changeset
|
54 |
fun mk_supp_ty ty t = Const (@{const_name "supp"}, supp_ty ty) $ t; |
760257a66604
added basic functions for constructing supp-terms
Christian Urban <urbanc@in.tum.de>
parents:
1963
diff
changeset
|
55 |
fun mk_supp t = mk_supp_ty (fastype_of t) t; |
760257a66604
added basic functions for constructing supp-terms
Christian Urban <urbanc@in.tum.de>
parents:
1963
diff
changeset
|
56 |
|
760257a66604
added basic functions for constructing supp-terms
Christian Urban <urbanc@in.tum.de>
parents:
1963
diff
changeset
|
57 |
|
1834
9909cc3566c5
moved a couple of more functions to the library
Christian Urban <urbanc@in.tum.de>
parents:
1833
diff
changeset
|
58 |
fun mk_equiv r = r RS @{thm eq_reflection}; |
9909cc3566c5
moved a couple of more functions to the library
Christian Urban <urbanc@in.tum.de>
parents:
1833
diff
changeset
|
59 |
fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r; |
1833
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
60 |
|
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>
parents:
1899
diff
changeset
|
61 |
|
1833
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
62 |
end (* structure *) |
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
63 |
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
64 |
open Nominal_Library; |