equal
deleted
inserted
replaced
4 Basic function for nominal. |
4 Basic function for nominal. |
5 *) |
5 *) |
6 |
6 |
7 signature NOMINAL_LIBRARY = |
7 signature NOMINAL_LIBRARY = |
8 sig |
8 sig |
|
9 |
|
10 |
9 val mk_minus: term -> term |
11 val mk_minus: term -> term |
10 val mk_plus: term -> term -> term |
12 val mk_plus: term -> term -> term |
11 |
13 |
12 val perm_ty: typ -> typ |
14 val perm_ty: typ -> typ |
13 val mk_perm_ty: typ -> term -> term -> term |
15 val mk_perm_ty: typ -> term -> term -> term |
14 val mk_perm: term -> term -> term |
16 val mk_perm: term -> term -> term |
15 val dest_perm: term -> term * term |
17 val dest_perm: term -> term * term |
|
18 |
|
19 val mk_sort_of: term -> term |
|
20 val mk_atom_ty: typ -> term -> term |
|
21 val mk_atom: term -> term |
16 |
22 |
17 val mk_equiv: thm -> thm |
23 val mk_equiv: thm -> thm |
18 val safe_mk_equiv: thm -> thm |
24 val safe_mk_equiv: thm -> thm |
19 end |
25 end |
20 |
26 |
36 fun mk_perm p trm = mk_perm_ty (fastype_of trm) p trm |
42 fun mk_perm p trm = mk_perm_ty (fastype_of trm) p trm |
37 |
43 |
38 fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t) |
44 fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t) |
39 | dest_perm t = raise TERM ("dest_perm", [t]) |
45 | dest_perm t = raise TERM ("dest_perm", [t]) |
40 |
46 |
|
47 |
|
48 fun mk_sort_of t = @{term "sort_of"} $ t; |
|
49 |
|
50 fun mk_atom_ty T t = Const (@{const_name atom}, T --> @{typ atom}) $ t; |
|
51 fun mk_atom t = mk_atom_ty (fastype_of t) t; |
|
52 |
41 fun mk_equiv r = r RS @{thm eq_reflection}; |
53 fun mk_equiv r = r RS @{thm eq_reflection}; |
42 fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r; |
54 fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r; |
|
55 |
43 |
56 |
44 end (* structure *) |
57 end (* structure *) |
45 |
58 |
46 open Nominal_Library; |
59 open Nominal_Library; |