equal
deleted
inserted
replaced
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: term -> term -> term |
10 val mk_perm: term -> term -> term |
|
11 val dest_perm: term -> term * term |
|
12 |
|
13 val mk_equiv: thm -> thm |
|
14 val safe_mk_equiv: thm -> thm |
11 end |
15 end |
12 |
16 |
13 |
17 |
14 structure Nominal_Library: NOMINAL_LIBRARY = |
18 structure Nominal_Library: NOMINAL_LIBRARY = |
15 struct |
19 struct |
22 val ty = fastype_of trm |
26 val ty = fastype_of trm |
23 in |
27 in |
24 Const (@{const_name "permute"}, @{typ "perm"} --> ty --> ty) $ p $ trm |
28 Const (@{const_name "permute"}, @{typ "perm"} --> ty --> ty) $ p $ trm |
25 end |
29 end |
26 |
30 |
|
31 fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t) |
|
32 | dest_perm t = raise TERM ("dest_perm", [t]) |
27 |
33 |
|
34 fun mk_equiv r = r RS @{thm eq_reflection}; |
|
35 fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r; |
28 |
36 |
29 end (* structure *) |
37 end (* structure *) |
30 |
38 |
31 open Nominal_Library; |
39 open Nominal_Library; |