207 fun alpha_bn thy (dt_info : Datatype_Aux.info) alpha_frees ((bn, ith_dtyp, args_in_bns), is_rec) = |
207 fun alpha_bn thy (dt_info : Datatype_Aux.info) alpha_frees ((bn, ith_dtyp, args_in_bns), is_rec) = |
208 let |
208 let |
209 val {descr, sorts, ...} = dt_info; |
209 val {descr, sorts, ...} = dt_info; |
210 fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); |
210 fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); |
211 val alpha_bn_name = "alpha_" ^ (Long_Name.base_name (fst (dest_Const bn))); |
211 val alpha_bn_name = "alpha_" ^ (Long_Name.base_name (fst (dest_Const bn))); |
212 val alpha_bn_type = @{typ perm} --> nth_dtyp ith_dtyp --> nth_dtyp ith_dtyp --> @{typ bool} |
212 val alpha_bn_type = |
|
213 if is_rec then @{typ perm} --> nth_dtyp ith_dtyp --> nth_dtyp ith_dtyp --> @{typ bool} |
|
214 else nth_dtyp ith_dtyp --> nth_dtyp ith_dtyp --> @{typ bool}; |
213 val alpha_bn_free = Free(alpha_bn_name, alpha_bn_type); |
215 val alpha_bn_free = Free(alpha_bn_name, alpha_bn_type); |
|
216 val pi = Free("pi", @{typ perm}) |
|
217 val alpha_bn_pi = if is_rec then alpha_bn_free $ pi else alpha_bn_free; |
214 fun alpha_bn_constr (cname, dts) args_in_bn = |
218 fun alpha_bn_constr (cname, dts) args_in_bn = |
215 let |
219 let |
216 val Ts = map (typ_of_dtyp descr sorts) dts; |
220 val Ts = map (typ_of_dtyp descr sorts) dts; |
217 val pi = Free("pi", @{typ perm}) |
|
218 val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts); |
221 val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts); |
219 val names2 = Name.variant_list ("pi" :: names) (Datatype_Prop.make_tnames Ts); |
222 val names2 = Name.variant_list ("pi" :: names) (Datatype_Prop.make_tnames Ts); |
220 val args = map Free (names ~~ Ts); |
223 val args = map Free (names ~~ Ts); |
221 val args2 = map Free (names2 ~~ Ts); |
224 val args2 = map Free (names2 ~~ Ts); |
222 val c = Const (cname, Ts ---> (nth_dtyp ith_dtyp)); |
225 val c = Const (cname, Ts ---> (nth_dtyp ith_dtyp)); |
223 val rhs = HOLogic.mk_Trueprop |
226 val rhs = HOLogic.mk_Trueprop |
224 (alpha_bn_free $ pi $ (list_comb (c, args)) $ (list_comb (c, args2))); |
227 (alpha_bn_pi $ (list_comb (c, args)) $ (list_comb (c, args2))); |
225 fun lhs_arg ((dt, arg_no), (arg, arg2)) = |
228 fun lhs_arg ((dt, arg_no), (arg, arg2)) = |
226 let |
229 let |
227 val argty = fastype_of arg; |
230 val argty = fastype_of arg; |
228 val permute = Const (@{const_name permute}, @{typ perm} --> argty --> argty); |
231 val permute = Const (@{const_name permute}, @{typ perm} --> argty --> argty); |
229 val permarg = if is_rec then permute $ pi $ arg else arg |
232 val permarg = if is_rec then permute $ pi $ arg else arg |
230 in |
233 in |
231 if is_rec_type dt then |
234 if is_rec_type dt then |
232 if arg_no mem args_in_bn then alpha_bn_free $ pi $ arg $ arg2 |
235 if arg_no mem args_in_bn then alpha_bn_pi $ arg $ arg2 |
233 else (nth alpha_frees (body_index dt)) $ permarg $ arg2 |
236 else (nth alpha_frees (body_index dt)) $ permarg $ arg2 |
234 else |
237 else |
235 if arg_no mem args_in_bn then @{term True} |
238 if arg_no mem args_in_bn then @{term True} |
236 else HOLogic.mk_eq (permarg, arg2) |
239 else HOLogic.mk_eq (permarg, arg2) |
237 end |
240 end |
349 case (rel_in_simp_binds, rel_in_comp_binds, rel_has_binds) of |
352 case (rel_in_simp_binds, rel_in_comp_binds, rel_has_binds) of |
350 ([], [], []) => |
353 ([], [], []) => |
351 if is_rec_type dt then (nth alpha_frees (body_index dt) $ arg $ arg2) |
354 if is_rec_type dt then (nth alpha_frees (body_index dt) $ arg $ arg2) |
352 else (HOLogic.mk_eq (arg, arg2)) |
355 else (HOLogic.mk_eq (arg, arg2)) |
353 | (_, [], []) => @{term True} |
356 | (_, [], []) => @{term True} |
354 | ([], ((((SOME (bn, _)), _, _), pi) :: _), []) => |
357 | ([], ((((SOME (bn, is_rec)), _, _), pi) :: _), []) => |
355 let |
358 let |
356 val alpha_bn = nth alpha_bn_frees (find_index (fn (b, _, _) => b = bn) bns) $ pi $ arg $ arg2 |
359 val alpha_bn_const = |
|
360 nth alpha_bn_frees (find_index (fn (b, _, _) => b = bn) bns) |
|
361 val alpha_bn = |
|
362 if is_rec then alpha_bn_const $ pi $ arg $ arg2 else alpha_bn_const $ arg $ arg2 |
357 val ty = fastype_of (bn $ arg) |
363 val ty = fastype_of (bn $ arg) |
358 val permute = Const(@{const_name permute}, @{typ perm} --> ty --> ty) |
364 val permute = Const(@{const_name permute}, @{typ perm} --> ty --> ty) |
359 in |
365 in |
360 if bns_same rel_in_comp_binds then |
366 if bns_same rel_in_comp_binds then |
361 alpha_bn |
367 alpha_bn |