equal
deleted
inserted
replaced
5 *) |
5 *) |
6 |
6 |
7 signature NOMINAL_LIBRARY = |
7 signature NOMINAL_LIBRARY = |
8 sig |
8 sig |
9 val mk_minus: term -> term |
9 val mk_minus: term -> term |
|
10 val mk_plus: term -> term -> term |
|
11 |
10 val mk_perm_ty: typ -> term -> term -> term |
12 val mk_perm_ty: typ -> term -> term -> term |
11 val mk_perm: term -> term -> term |
13 val mk_perm: term -> term -> term |
12 val dest_perm: term -> term * term |
14 val dest_perm: term -> term * term |
13 |
15 |
14 val mk_equiv: thm -> thm |
16 val mk_equiv: thm -> thm |
18 |
20 |
19 structure Nominal_Library: NOMINAL_LIBRARY = |
21 structure Nominal_Library: NOMINAL_LIBRARY = |
20 struct |
22 struct |
21 |
23 |
22 fun mk_minus p = |
24 fun mk_minus p = |
23 Const (@{const_name "uminus"}, @{typ "perm => perm"}) $ p |
25 @{term "uminus::perm => perm"} $ p |
|
26 |
|
27 fun mk_plus p q = |
|
28 @{term "plus::perm => perm => perm"} $ p $ q |
24 |
29 |
25 fun mk_perm_ty ty p trm = |
30 fun mk_perm_ty ty p trm = |
26 Const (@{const_name "permute"}, @{typ "perm"} --> ty --> ty) $ p $ trm |
31 Const (@{const_name "permute"}, @{typ "perm"} --> ty --> ty) $ p $ trm |
27 |
32 |
28 fun mk_perm p trm = mk_perm_ty (fastype_of trm) p trm |
33 fun mk_perm p trm = mk_perm_ty (fastype_of trm) p trm |