equal
deleted
inserted
replaced
31 val atomify: Proof.context -> term -> term |
31 val atomify: Proof.context -> term -> term |
32 val setify_ty: Proof.context -> typ -> term -> term |
32 val setify_ty: Proof.context -> typ -> term -> term |
33 val setify: Proof.context -> term -> term |
33 val setify: Proof.context -> term -> term |
34 val listify_ty: Proof.context -> typ -> term -> term |
34 val listify_ty: Proof.context -> typ -> term -> term |
35 val listify: Proof.context -> term -> term |
35 val listify: Proof.context -> term -> term |
|
36 |
|
37 val fresh_ty: typ -> typ |
|
38 val fresh_const: typ -> term |
|
39 val mk_fresh_ty: typ -> term -> term -> term |
|
40 val mk_fresh: term -> term -> term |
36 |
41 |
37 val fresh_star_ty: typ -> typ |
42 val fresh_star_ty: typ -> typ |
38 val fresh_star_const: typ -> term |
43 val fresh_star_const: typ -> term |
39 val mk_fresh_star_ty: typ -> term -> term -> term |
44 val mk_fresh_star_ty: typ -> term -> term -> term |
40 val mk_fresh_star: term -> term -> term |
45 val mk_fresh_star: term -> term -> term |
198 else raise TERM ("listify", [t]) |
203 else raise TERM ("listify", [t]) |
199 |
204 |
200 fun atomify ctxt t = atomify_ty ctxt (fastype_of t) t |
205 fun atomify ctxt t = atomify_ty ctxt (fastype_of t) t |
201 fun setify ctxt t = setify_ty ctxt (fastype_of t) t |
206 fun setify ctxt t = setify_ty ctxt (fastype_of t) t |
202 fun listify ctxt t = listify_ty ctxt (fastype_of t) t |
207 fun listify ctxt t = listify_ty ctxt (fastype_of t) t |
|
208 |
|
209 fun fresh_ty ty = [@{typ atom}, ty] ---> @{typ bool} |
|
210 fun fresh_const ty = Const (@{const_name fresh}, fresh_ty ty) |
|
211 fun mk_fresh_ty ty t1 t2 = fresh_const ty $ t1 $ t2 |
|
212 fun mk_fresh t1 t2 = mk_fresh_ty (fastype_of t2) t1 t2 |
203 |
213 |
204 fun fresh_star_ty ty = [@{typ "atom set"}, ty] ---> @{typ bool} |
214 fun fresh_star_ty ty = [@{typ "atom set"}, ty] ---> @{typ bool} |
205 fun fresh_star_const ty = Const (@{const_name fresh_star}, fresh_star_ty ty) |
215 fun fresh_star_const ty = Const (@{const_name fresh_star}, fresh_star_ty ty) |
206 fun mk_fresh_star_ty ty t1 t2 = fresh_star_const ty $ t1 $ t2 |
216 fun mk_fresh_star_ty ty t1 t2 = fresh_star_const ty $ t1 $ t2 |
207 fun mk_fresh_star t1 t2 = mk_fresh_star_ty (fastype_of t2) t1 t2 |
217 fun mk_fresh_star t1 t2 = mk_fresh_star_ty (fastype_of t2) t1 t2 |