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 = |
212 val alpha_bn_type = |
213 if is_rec then @{typ perm} --> nth_dtyp ith_dtyp --> nth_dtyp ith_dtyp --> @{typ bool} |
213 (*if is_rec then @{typ perm} --> nth_dtyp ith_dtyp --> nth_dtyp ith_dtyp --> @{typ bool} else*) |
214 else nth_dtyp ith_dtyp --> nth_dtyp ith_dtyp --> @{typ bool}; |
214 nth_dtyp ith_dtyp --> nth_dtyp ith_dtyp --> @{typ bool}; |
215 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}) |
216 val pi = Free("pi", @{typ perm}) |
217 val alpha_bn_pi = if is_rec then alpha_bn_free $ pi else alpha_bn_free; |
|
218 fun alpha_bn_constr (cname, dts) args_in_bn = |
217 fun alpha_bn_constr (cname, dts) args_in_bn = |
219 let |
218 let |
220 val Ts = map (typ_of_dtyp descr sorts) dts; |
219 val Ts = map (typ_of_dtyp descr sorts) dts; |
221 val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts); |
220 val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts); |
222 val names2 = Name.variant_list ("pi" :: names) (Datatype_Prop.make_tnames Ts); |
221 val names2 = Name.variant_list ("pi" :: names) (Datatype_Prop.make_tnames Ts); |
223 val args = map Free (names ~~ Ts); |
222 val args = map Free (names ~~ Ts); |
224 val args2 = map Free (names2 ~~ Ts); |
223 val args2 = map Free (names2 ~~ Ts); |
225 val c = Const (cname, Ts ---> (nth_dtyp ith_dtyp)); |
224 val c = Const (cname, Ts ---> (nth_dtyp ith_dtyp)); |
226 val rhs = HOLogic.mk_Trueprop |
225 val rhs = HOLogic.mk_Trueprop |
227 (alpha_bn_pi $ (list_comb (c, args)) $ (list_comb (c, args2))); |
226 (alpha_bn_free $ (list_comb (c, args)) $ (list_comb (c, args2))); |
228 fun lhs_arg ((dt, arg_no), (arg, arg2)) = |
227 fun lhs_arg ((dt, arg_no), (arg, arg2)) = |
229 let |
228 let |
230 val argty = fastype_of arg; |
229 val argty = fastype_of arg; |
231 val permute = Const (@{const_name permute}, @{typ perm} --> argty --> argty); |
230 val permute = Const (@{const_name permute}, @{typ perm} --> argty --> argty); |
232 val permarg = if is_rec then permute $ pi $ arg else arg |
|
233 in |
231 in |
234 if is_rec_type dt then |
232 if is_rec_type dt then |
235 if arg_no mem args_in_bn then alpha_bn_pi $ arg $ arg2 |
233 if arg_no mem args_in_bn then alpha_bn_free $ arg $ arg2 |
236 else (nth alpha_frees (body_index dt)) $ permarg $ arg2 |
234 else (nth alpha_frees (body_index dt)) $ arg $ arg2 |
237 else |
235 else |
238 if arg_no mem args_in_bn then @{term True} |
236 if arg_no mem args_in_bn then @{term True} |
239 else HOLogic.mk_eq (permarg, arg2) |
237 else HOLogic.mk_eq (arg, arg2) |
240 end |
238 end |
241 val arg_nos = 0 upto (length dts - 1) |
239 val arg_nos = 0 upto (length dts - 1) |
242 val lhss = mk_conjl (map lhs_arg (dts ~~ arg_nos ~~ (args ~~ args2))) |
240 val lhss = mk_conjl (map lhs_arg (dts ~~ arg_nos ~~ (args ~~ args2))) |
243 val eq = Logic.mk_implies (HOLogic.mk_Trueprop lhss, rhs) |
241 val eq = Logic.mk_implies (HOLogic.mk_Trueprop lhss, rhs) |
244 in |
242 in |
353 ([], [], []) => |
351 ([], [], []) => |
354 if is_rec_type dt then (nth alpha_frees (body_index dt) $ arg $ arg2) |
352 if is_rec_type dt then (nth alpha_frees (body_index dt) $ arg $ arg2) |
355 else (HOLogic.mk_eq (arg, arg2)) |
353 else (HOLogic.mk_eq (arg, arg2)) |
356 | (_, [], []) => @{term True} |
354 | (_, [], []) => @{term True} |
357 | ([], ((((SOME (bn, is_rec)), _, _), pi) :: _), []) => |
355 | ([], ((((SOME (bn, is_rec)), _, _), pi) :: _), []) => |
358 let |
356 if not (bns_same rel_in_comp_binds) then error "incompatible bindings for an argument" else |
359 val alpha_bn_const = |
357 if is_rec then |
360 nth alpha_bn_frees (find_index (fn (b, _, _) => b = bn) bns) |
358 let |
361 val alpha_bn = |
359 val (rbinds, rpis) = split_list rel_in_comp_binds |
362 if is_rec then alpha_bn_const $ pi $ arg $ arg2 else alpha_bn_const $ arg $ arg2 |
360 val lhs_binds = fv_binds args rbinds |
363 val ty = fastype_of (bn $ arg) |
361 val lhs = mk_pair (lhs_binds, arg); |
364 val permute = Const(@{const_name permute}, @{typ perm} --> ty --> ty) |
362 val rhs_binds = fv_binds args2 rbinds; |
365 in |
363 val rhs = mk_pair (rhs_binds, arg2); |
366 if bns_same rel_in_comp_binds then |
364 val alpha = nth alpha_frees (body_index dt); |
367 alpha_bn |
365 val fv = nth fv_frees (body_index dt); |
368 (* HOLogic.mk_conj (alpha_bn, HOLogic.mk_eq (permute $ pi $ (bn $ arg), (bn $ arg2)))*) |
366 val pi = foldr1 add_perm (distinct (op =) rpis); |
369 else error "incompatible bindings for one argument" |
367 val alpha_gen_pre = Const (@{const_name alpha_gen}, dummyT) $ lhs $ alpha $ fv $ pi $ rhs; |
370 end |
368 val alpha_gen = Syntax.check_term lthy alpha_gen_pre |
|
369 in |
|
370 alpha_gen |
|
371 end |
|
372 else |
|
373 let |
|
374 val alpha_bn_const = |
|
375 nth alpha_bn_frees (find_index (fn (b, _, _) => b = bn) bns) |
|
376 val ty = fastype_of (bn $ arg) |
|
377 val permute = Const(@{const_name permute}, @{typ perm} --> ty --> ty) |
|
378 in |
|
379 alpha_bn_const $ arg $ arg2 |
|
380 end |
371 | ([], [], relevant) => |
381 | ([], [], relevant) => |
372 let |
382 let |
373 val (rbinds, rpis) = split_list relevant |
383 val (rbinds, rpis) = split_list relevant |
374 val lhs_binds = fv_binds args rbinds |
384 val lhs_binds = fv_binds args rbinds |
375 val lhs = mk_pair (lhs_binds, arg); |
385 val lhs = mk_pair (lhs_binds, arg); |
378 val alpha = nth alpha_frees (body_index dt); |
388 val alpha = nth alpha_frees (body_index dt); |
379 val fv = nth fv_frees (body_index dt); |
389 val fv = nth fv_frees (body_index dt); |
380 val pi = foldr1 add_perm (distinct (op =) rpis); |
390 val pi = foldr1 add_perm (distinct (op =) rpis); |
381 val alpha_gen_pre = Const (@{const_name alpha_gen}, dummyT) $ lhs $ alpha $ fv $ pi $ rhs; |
391 val alpha_gen_pre = Const (@{const_name alpha_gen}, dummyT) $ lhs $ alpha $ fv $ pi $ rhs; |
382 val alpha_gen = Syntax.check_term lthy alpha_gen_pre |
392 val alpha_gen = Syntax.check_term lthy alpha_gen_pre |
383 (* val pi_supps = map ((curry op $) @{term "supp :: perm \<Rightarrow> atom set"}) rpis; |
|
384 val pi_supps_eq = HOLogic.mk_eq (mk_inter pi_supps, @{term "{} :: atom set"}) *) |
|
385 in |
393 in |
386 (* if length pi_supps > 1 then HOLogic.mk_conj (alpha_gen, pi_supps_eq) else*) |
|
387 alpha_gen |
394 alpha_gen |
388 end |
395 end |
389 | _ => error "Fv.alpha: not supported binding structure" |
396 | _ => error "Fv.alpha: not supported binding structure" |
390 end |
397 end |
391 val alphas = map alpha_arg (dts ~~ arg_nos ~~ (args ~~ args2)) |
398 val alphas = map alpha_arg (dts ~~ arg_nos ~~ (args ~~ args2)) |