7 signature NOMINAL_LIBRARY = |
7 signature NOMINAL_LIBRARY = |
8 sig |
8 sig |
9 val last2: 'a list -> 'a * 'a |
9 val last2: 'a list -> 'a * 'a |
10 |
10 |
11 val dest_listT: typ -> typ |
11 val dest_listT: typ -> typ |
|
12 |
|
13 val size_const: typ -> term |
12 |
14 |
13 val mk_minus: term -> term |
15 val mk_minus: term -> term |
14 val mk_plus: term -> term -> term |
16 val mk_plus: term -> term -> term |
15 |
17 |
16 val perm_ty: typ -> typ |
18 val perm_ty: typ -> typ |
71 | last2 (_ :: xs) = last2 xs |
73 | last2 (_ :: xs) = last2 xs |
72 |
74 |
73 fun dest_listT (Type (@{type_name list}, [T])) = T |
75 fun dest_listT (Type (@{type_name list}, [T])) = T |
74 | dest_listT T = raise TYPE ("dest_listT: list type expected", [T], []) |
76 | dest_listT T = raise TYPE ("dest_listT: list type expected", [T], []) |
75 |
77 |
76 fun mk_minus p = @{term "uminus::perm => perm"} $ p; |
78 fun size_const ty = Const (@{const_name size}, ty --> @{typ nat}) |
77 |
79 |
78 fun mk_plus p q = @{term "plus::perm => perm => perm"} $ p $ q; |
80 fun mk_minus p = @{term "uminus::perm => perm"} $ p |
79 |
81 |
80 fun perm_ty ty = @{typ "perm"} --> ty --> ty; |
82 fun mk_plus p q = @{term "plus::perm => perm => perm"} $ p $ q |
81 fun mk_perm_ty ty p trm = Const (@{const_name "permute"}, perm_ty ty) $ p $ trm; |
83 |
82 fun mk_perm p trm = mk_perm_ty (fastype_of trm) p trm; |
84 fun perm_ty ty = @{typ "perm"} --> ty --> ty |
|
85 fun mk_perm_ty ty p trm = Const (@{const_name "permute"}, perm_ty ty) $ p $ trm |
|
86 fun mk_perm p trm = mk_perm_ty (fastype_of trm) p trm |
83 |
87 |
84 fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t) |
88 fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t) |
85 | dest_perm t = raise TERM ("dest_perm", [t]); |
89 | dest_perm t = raise TERM ("dest_perm", [t]); |
86 |
90 |
87 fun mk_sort_of t = @{term "sort_of"} $ t; |
91 fun mk_sort_of t = @{term "sort_of"} $ t; |