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_perm_ty: typ -> term -> term -> term |
10 val mk_perm: term -> term -> term |
11 val mk_perm: term -> term -> term |
11 val dest_perm: term -> term * term |
12 val dest_perm: term -> term * term |
12 |
13 |
13 val mk_equiv: thm -> thm |
14 val mk_equiv: thm -> thm |
14 val safe_mk_equiv: thm -> thm |
15 val safe_mk_equiv: thm -> thm |
19 struct |
20 struct |
20 |
21 |
21 fun mk_minus p = |
22 fun mk_minus p = |
22 Const (@{const_name "uminus"}, @{typ "perm => perm"}) $ p |
23 Const (@{const_name "uminus"}, @{typ "perm => perm"}) $ p |
23 |
24 |
24 fun mk_perm p trm = |
25 fun mk_perm_ty ty p trm = |
25 let |
|
26 val ty = fastype_of trm |
|
27 in |
|
28 Const (@{const_name "permute"}, @{typ "perm"} --> ty --> ty) $ p $ trm |
26 Const (@{const_name "permute"}, @{typ "perm"} --> ty --> ty) $ p $ trm |
29 end |
27 |
|
28 fun mk_perm p trm = mk_perm_ty (fastype_of trm) p trm |
30 |
29 |
31 fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t) |
30 fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t) |
32 | dest_perm t = raise TERM ("dest_perm", [t]) |
31 | dest_perm t = raise TERM ("dest_perm", [t]) |
33 |
32 |
34 fun mk_equiv r = r RS @{thm eq_reflection}; |
33 fun mk_equiv r = r RS @{thm eq_reflection}; |