258 fun build_alpha alpha = |
258 fun build_alpha alpha = |
259 let |
259 let |
260 val ty = domain_type (fastype_of alpha); |
260 val ty = domain_type (fastype_of alpha); |
261 val var = Free("x", ty); |
261 val var = Free("x", ty); |
262 val var2 = Free("y", ty); |
262 val var2 = Free("y", ty); |
|
263 val var3 = Free("z", ty); |
|
264 val symp = HOLogic.mk_imp (alpha $ var $ var2, alpha $ var2 $ var); |
|
265 val transp = HOLogic.mk_imp (alpha $ var $ var2, |
|
266 HOLogic.mk_all ("z", ty, |
|
267 HOLogic.mk_imp (alpha $ var2 $ var3, alpha $ var $ var3))) |
263 in |
268 in |
264 ((alpha $ var $ var), (HOLogic.mk_imp (alpha $ var $ var2, alpha $ var2 $ var))) |
269 ((alpha $ var $ var), (symp, transp)) |
265 end; |
270 end; |
266 val (refl_eqs, sym_eqs) = split_list (map build_alpha alphas) |
271 val (refl_eqs, eqs) = split_list (map build_alpha alphas) |
|
272 val (sym_eqs, trans_eqs) = split_list eqs |
|
273 fun conj l = @{term Trueprop} $ foldr1 HOLogic.mk_conj l |
267 in |
274 in |
268 Logic.mk_conjunction |
275 (conj refl_eqs, (conj sym_eqs, conj trans_eqs)) |
269 (@{term Trueprop} $ foldr1 HOLogic.mk_conj refl_eqs, |
276 end |
270 @{term Trueprop} $ foldr1 HOLogic.mk_conj sym_eqs) |
277 *} |
271 end |
278 |
272 *} |
279 |
273 |
280 end |
274 |
|
275 end |
|