equal
deleted
inserted
replaced
30 |
30 |
31 val supp_ty: typ -> typ |
31 val supp_ty: typ -> typ |
32 val supp_const: typ -> term |
32 val supp_const: typ -> term |
33 val mk_supp_ty: typ -> term -> term |
33 val mk_supp_ty: typ -> term -> term |
34 val mk_supp: term -> term |
34 val mk_supp: term -> term |
|
35 |
|
36 val supp_rel_ty: typ -> typ |
|
37 val supp_rel_const: typ -> term |
|
38 val mk_supp_rel_ty: typ -> term -> term -> term |
|
39 val mk_supp_rel: term -> term -> term |
35 |
40 |
36 val supports_const: typ -> term |
41 val supports_const: typ -> term |
37 val mk_supports_ty: typ -> term -> term -> term |
42 val mk_supports_ty: typ -> term -> term -> term |
38 val mk_supports: term -> term -> term |
43 val mk_supports: term -> term -> term |
39 |
44 |
122 fun mk_atom t = mk_atom_ty (fastype_of t) t; |
127 fun mk_atom t = mk_atom_ty (fastype_of t) t; |
123 |
128 |
124 |
129 |
125 fun supp_ty ty = ty --> @{typ "atom set"}; |
130 fun supp_ty ty = ty --> @{typ "atom set"}; |
126 fun supp_const ty = Const (@{const_name supp}, supp_ty ty) |
131 fun supp_const ty = Const (@{const_name supp}, supp_ty ty) |
127 fun mk_supp_ty ty t = supp_const ty $ t; |
132 fun mk_supp_ty ty t = supp_const ty $ t |
128 fun mk_supp t = mk_supp_ty (fastype_of t) t; |
133 fun mk_supp t = mk_supp_ty (fastype_of t) t |
|
134 |
|
135 fun supp_rel_ty ty = ([ty, ty] ---> @{typ bool}) --> ty --> @{typ "atom set"}; |
|
136 fun supp_rel_const ty = Const (@{const_name supp_rel}, supp_rel_ty ty) |
|
137 fun mk_supp_rel_ty ty r t = supp_rel_const ty $ r $ t |
|
138 fun mk_supp_rel r t = mk_supp_rel_ty (fastype_of t) r t |
129 |
139 |
130 fun supports_const ty = Const (@{const_name supports}, [@{typ "atom set"}, ty] ---> @{typ bool}); |
140 fun supports_const ty = Const (@{const_name supports}, [@{typ "atom set"}, ty] ---> @{typ bool}); |
131 fun mk_supports_ty ty t1 t2 = supports_const ty $ t1 $ t2; |
141 fun mk_supports_ty ty t1 t2 = supports_const ty $ t1 $ t2; |
132 fun mk_supports t1 t2 = mk_supports_ty (fastype_of t2) t1 t2; |
142 fun mk_supports t1 t2 = mk_supports_ty (fastype_of t2) t1 t2; |
133 |
143 |