33 val mk_id: term -> term |
33 val mk_id: term -> term |
34 val mk_all: (string * typ) -> term -> term |
34 val mk_all: (string * typ) -> term -> term |
35 val mk_All: (string * typ) -> term -> term |
35 val mk_All: (string * typ) -> term -> term |
36 val mk_exists: (string * typ) -> term -> term |
36 val mk_exists: (string * typ) -> term -> term |
37 |
37 |
38 val sum_case_const: typ -> typ -> typ -> term |
38 val case_sum_const: typ -> typ -> typ -> term |
39 val mk_sum_case: term -> term -> term |
39 val mk_case_sum: term -> term -> term |
40 |
40 |
41 val mk_equiv: thm -> thm |
41 val mk_equiv: thm -> thm |
42 val safe_mk_equiv: thm -> thm |
42 val safe_mk_equiv: thm -> thm |
43 |
43 |
44 val mk_minus: term -> term |
44 val mk_minus: term -> term |
146 |
146 |
147 fun mk_All (a, T) t = HOLogic.all_const T $ Abs (a, T, t) |
147 fun mk_All (a, T) t = HOLogic.all_const T $ Abs (a, T, t) |
148 |
148 |
149 fun mk_exists (a, T) t = HOLogic.exists_const T $ Abs (a, T, t) |
149 fun mk_exists (a, T) t = HOLogic.exists_const T $ Abs (a, T, t) |
150 |
150 |
151 fun sum_case_const ty1 ty2 ty3 = |
151 fun case_sum_const ty1 ty2 ty3 = |
152 Const (@{const_name sum_case}, [ty1 --> ty3, ty2 --> ty3, Type (@{type_name sum}, [ty1, ty2])] ---> ty3) |
152 Const (@{const_name case_sum}, [ty1 --> ty3, ty2 --> ty3, Type (@{type_name sum}, [ty1, ty2])] ---> ty3) |
153 |
153 |
154 fun mk_sum_case trm1 trm2 = |
154 fun mk_case_sum trm1 trm2 = |
155 let |
155 let |
156 val ([ty1], ty3) = strip_type (fastype_of trm1) |
156 val ([ty1], ty3) = strip_type (fastype_of trm1) |
157 val ty2 = domain_type (fastype_of trm2) |
157 val ty2 = domain_type (fastype_of trm2) |
158 in |
158 in |
159 sum_case_const ty1 ty2 ty3 $ trm1 $ trm2 |
159 case_sum_const ty1 ty2 ty3 $ trm1 $ trm2 |
160 end |
160 end |
161 |
161 |
162 fun mk_equiv r = r RS @{thm eq_reflection} |
162 fun mk_equiv r = r RS @{thm eq_reflection} |
163 fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r |
163 fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r |
164 |
164 |