equal
deleted
inserted
replaced
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 |
10 val mk_plus: term -> term -> term |
11 |
11 |
|
12 val perm_ty: typ -> typ |
12 val mk_perm_ty: typ -> term -> term -> term |
13 val mk_perm_ty: typ -> term -> term -> term |
13 val mk_perm: term -> term -> term |
14 val mk_perm: term -> term -> term |
14 val dest_perm: term -> term * term |
15 val dest_perm: term -> term * term |
15 |
16 |
16 val mk_equiv: thm -> thm |
17 val mk_equiv: thm -> thm |
25 @{term "uminus::perm => perm"} $ p |
26 @{term "uminus::perm => perm"} $ p |
26 |
27 |
27 fun mk_plus p q = |
28 fun mk_plus p q = |
28 @{term "plus::perm => perm => perm"} $ p $ q |
29 @{term "plus::perm => perm => perm"} $ p $ q |
29 |
30 |
|
31 fun perm_ty ty = @{typ perm} --> ty --> ty |
|
32 |
30 fun mk_perm_ty ty p trm = |
33 fun mk_perm_ty ty p trm = |
31 Const (@{const_name "permute"}, @{typ "perm"} --> ty --> ty) $ p $ trm |
34 Const (@{const_name "permute"}, perm_ty ty) $ p $ trm |
32 |
35 |
33 fun mk_perm p trm = mk_perm_ty (fastype_of trm) p trm |
36 fun mk_perm p trm = mk_perm_ty (fastype_of trm) p trm |
34 |
37 |
35 fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t) |
38 fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t) |
36 | dest_perm t = raise TERM ("dest_perm", [t]) |
39 | dest_perm t = raise TERM ("dest_perm", [t]) |