1 (* Title: nominal_library.ML |
1 (* Title: nominal_library.ML |
2 Author: Christian Urban |
2 Author: Christian Urban |
3 |
3 |
4 Basic function for nominal. |
4 Basic functions for nominal. |
5 *) |
5 *) |
6 |
6 |
7 signature NOMINAL_LIBRARY = |
7 signature NOMINAL_LIBRARY = |
8 sig |
8 sig |
9 |
|
10 |
|
11 val mk_minus: term -> term |
9 val mk_minus: term -> term |
12 val mk_plus: term -> term -> term |
10 val mk_plus: term -> term -> term |
13 |
11 |
14 val perm_ty: typ -> typ |
12 val perm_ty: typ -> typ |
15 val mk_perm_ty: typ -> term -> term -> term |
13 val mk_perm_ty: typ -> term -> term -> term |
16 val mk_perm: term -> term -> term |
14 val mk_perm: term -> term -> term |
17 val dest_perm: term -> term * term |
15 val dest_perm: term -> term * term |
18 |
16 |
19 val mk_sort_of: term -> term |
17 val mk_sort_of: term -> term |
|
18 val atom_ty: typ -> typ |
20 val mk_atom_ty: typ -> term -> term |
19 val mk_atom_ty: typ -> term -> term |
21 val mk_atom: term -> term |
20 val mk_atom: term -> term |
|
21 |
|
22 val supp_ty: typ -> typ |
|
23 val mk_supp_ty: typ -> term -> term |
|
24 val mk_supp: term -> term |
22 |
25 |
23 val mk_equiv: thm -> thm |
26 val mk_equiv: thm -> thm |
24 val safe_mk_equiv: thm -> thm |
27 val safe_mk_equiv: thm -> thm |
25 end |
28 end |
26 |
29 |
27 |
30 |
28 structure Nominal_Library: NOMINAL_LIBRARY = |
31 structure Nominal_Library: NOMINAL_LIBRARY = |
29 struct |
32 struct |
30 |
33 |
31 fun mk_minus p = |
34 fun mk_minus p = @{term "uminus::perm => perm"} $ p; |
32 @{term "uminus::perm => perm"} $ p |
|
33 |
35 |
34 fun mk_plus p q = |
36 fun mk_plus p q = @{term "plus::perm => perm => perm"} $ p $ q; |
35 @{term "plus::perm => perm => perm"} $ p $ q |
|
36 |
37 |
37 fun perm_ty ty = @{typ "perm"} --> ty --> ty |
38 fun perm_ty ty = @{typ "perm"} --> ty --> ty; |
38 fun mk_perm_ty ty p trm = |
39 fun mk_perm_ty ty p trm = Const (@{const_name "permute"}, perm_ty ty) $ p $ trm; |
39 Const (@{const_name "permute"}, perm_ty ty) $ p $ trm |
40 fun mk_perm p trm = mk_perm_ty (fastype_of trm) p trm; |
40 fun mk_perm p trm = mk_perm_ty (fastype_of trm) p trm |
|
41 |
41 |
42 fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t) |
42 fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t) |
43 | dest_perm t = raise TERM ("dest_perm", [t]) |
43 | dest_perm t = raise TERM ("dest_perm", [t]); |
44 |
44 |
45 |
45 |
46 fun mk_sort_of t = @{term "sort_of"} $ t; |
46 fun mk_sort_of t = @{term "sort_of"} $ t; |
47 |
47 |
48 fun atom_ty ty = ty --> @{typ "atom"} |
48 fun atom_ty ty = ty --> @{typ "atom"}; |
49 fun mk_atom_ty ty t = Const (@{const_name "atom"}, atom_ty ty) $ t; |
49 fun mk_atom_ty ty t = Const (@{const_name "atom"}, atom_ty ty) $ t; |
50 fun mk_atom t = mk_atom_ty (fastype_of t) t; |
50 fun mk_atom t = mk_atom_ty (fastype_of t) t; |
|
51 |
|
52 |
|
53 fun supp_ty ty = ty --> @{typ "atom set"}; |
|
54 fun mk_supp_ty ty t = Const (@{const_name "supp"}, supp_ty ty) $ t; |
|
55 fun mk_supp t = mk_supp_ty (fastype_of t) t; |
|
56 |
51 |
57 |
52 fun mk_equiv r = r RS @{thm eq_reflection}; |
58 fun mk_equiv r = r RS @{thm eq_reflection}; |
53 fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r; |
59 fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r; |
54 |
60 |
55 |
61 |