211 val args2 = map Free (names2 ~~ Ts); |
211 val args2 = map Free (names2 ~~ Ts); |
212 val c = Const (cname, Ts ---> (nth_dtyp ith_dtyp)); |
212 val c = Const (cname, Ts ---> (nth_dtyp ith_dtyp)); |
213 val rhs = HOLogic.mk_Trueprop |
213 val rhs = HOLogic.mk_Trueprop |
214 (alpha_bn_free $ pi $ (list_comb (c, args)) $ (list_comb (c, args2))); |
214 (alpha_bn_free $ pi $ (list_comb (c, args)) $ (list_comb (c, args2))); |
215 fun lhs_arg ((dt, arg_no), (arg, arg2)) = |
215 fun lhs_arg ((dt, arg_no), (arg, arg2)) = |
216 (*...*) |
216 let |
217 @{term True} |
217 val argty = fastype_of arg; |
|
218 val permute = Const (@{const_name permute}, @{typ perm} --> argty --> argty); |
|
219 val permarg = if is_rec then permute $ pi $ arg else arg |
|
220 in |
|
221 if is_rec_type dt then |
|
222 if arg_no mem args_in_bn then alpha_bn_free $ pi $ arg $ arg2 |
|
223 else (nth alpha_frees (body_index dt)) $ permarg $ arg2 |
|
224 else |
|
225 if arg_no mem args_in_bn then @{term True} |
|
226 else HOLogic.mk_eq (permarg, arg2) |
|
227 end |
218 val arg_nos = 0 upto (length dts - 1) |
228 val arg_nos = 0 upto (length dts - 1) |
219 val lhss = mk_conjl (map lhs_arg (dts ~~ arg_nos ~~ (args ~~ args2))) |
229 val lhss = mk_conjl (map lhs_arg (dts ~~ arg_nos ~~ (args ~~ args2))) |
220 val eq = Logic.mk_implies (HOLogic.mk_Trueprop lhss, rhs) |
230 val eq = Logic.mk_implies (HOLogic.mk_Trueprop lhss, rhs) |
221 in |
231 in |
222 eq |
232 eq |