34 val mk_supp: term -> term |
34 val mk_supp: term -> term |
35 |
35 |
36 val supports_const: typ -> term |
36 val supports_const: typ -> term |
37 val mk_supports_ty: typ -> term -> term -> term |
37 val mk_supports_ty: typ -> term -> term -> term |
38 val mk_supports: term -> term -> term |
38 val mk_supports: term -> term -> term |
|
39 |
|
40 val finite_const: typ -> term |
|
41 val mk_finite_ty: typ -> term -> term |
|
42 val mk_finite: term -> term |
|
43 |
39 |
44 |
40 val mk_equiv: thm -> thm |
45 val mk_equiv: thm -> thm |
41 val safe_mk_equiv: thm -> thm |
46 val safe_mk_equiv: thm -> thm |
42 |
47 |
43 val mk_diff: term * term -> term |
48 val mk_diff: term * term -> term |
115 fun mk_atom_ty ty t = Const (@{const_name "atom"}, atom_ty ty) $ t; |
120 fun mk_atom_ty ty t = Const (@{const_name "atom"}, atom_ty ty) $ t; |
116 fun mk_atom t = mk_atom_ty (fastype_of t) t; |
121 fun mk_atom t = mk_atom_ty (fastype_of t) t; |
117 |
122 |
118 |
123 |
119 fun supp_ty ty = ty --> @{typ "atom set"}; |
124 fun supp_ty ty = ty --> @{typ "atom set"}; |
120 fun supp_const ty = Const (@{const_name "supp"}, supp_ty ty) |
125 fun supp_const ty = Const (@{const_name supp}, supp_ty ty) |
121 fun mk_supp_ty ty t = supp_const ty $ t; |
126 fun mk_supp_ty ty t = supp_const ty $ t; |
122 fun mk_supp t = mk_supp_ty (fastype_of t) t; |
127 fun mk_supp t = mk_supp_ty (fastype_of t) t; |
123 |
128 |
124 fun supports_const ty = Const (@{const_name "supports"}, [@{typ "atom set"}, ty] ---> @{typ bool}); |
129 fun supports_const ty = Const (@{const_name supports}, [@{typ "atom set"}, ty] ---> @{typ bool}); |
125 fun mk_supports_ty ty t1 t2 = supports_const ty $ t1 $ t2; |
130 fun mk_supports_ty ty t1 t2 = supports_const ty $ t1 $ t2; |
126 fun mk_supports t1 t2 = mk_supports_ty (fastype_of t2) t1 t2; |
131 fun mk_supports t1 t2 = mk_supports_ty (fastype_of t2) t1 t2; |
|
132 |
|
133 fun finite_const ty = Const (@{const_name finite}, ty --> @{typ bool}) |
|
134 fun mk_finite_ty ty t = finite_const ty $ t |
|
135 fun mk_finite t = mk_finite_ty (fastype_of t) t |
|
136 |
127 |
137 |
128 fun mk_equiv r = r RS @{thm eq_reflection}; |
138 fun mk_equiv r = r RS @{thm eq_reflection}; |
129 fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r; |
139 fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r; |
130 |
140 |
131 |
141 |