202 val alpha_bn_type = @{typ perm} --> nth_dtyp ith_dtyp --> nth_dtyp ith_dtyp --> @{typ bool} |
202 val alpha_bn_type = @{typ perm} --> nth_dtyp ith_dtyp --> nth_dtyp ith_dtyp --> @{typ bool} |
203 val alpha_bn_free = Free(alpha_bn_name, alpha_bn_type); |
203 val alpha_bn_free = Free(alpha_bn_name, alpha_bn_type); |
204 fun alpha_bn_constr (cname, dts) args_in_bn = |
204 fun alpha_bn_constr (cname, dts) args_in_bn = |
205 let |
205 let |
206 val Ts = map (typ_of_dtyp descr sorts) dts; |
206 val Ts = map (typ_of_dtyp descr sorts) dts; |
|
207 val pi = Free("pi", @{typ perm}) |
207 val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts); |
208 val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts); |
208 val names2 = Name.variant_list ("pi" :: names) (Datatype_Prop.make_tnames Ts); |
209 val names2 = Name.variant_list ("pi" :: names) (Datatype_Prop.make_tnames Ts); |
209 val args = map Free (names ~~ Ts); |
210 val args = map Free (names ~~ Ts); |
210 val args2 = map Free (names2 ~~ Ts); |
211 val args2 = map Free (names2 ~~ Ts); |
211 val c = Const (cname, Ts ---> (nth_dtyp ith_dtyp)); |
212 val c = Const (cname, Ts ---> (nth_dtyp ith_dtyp)); |
212 (*...*) |
213 val rhs = HOLogic.mk_Trueprop |
|
214 (alpha_bn_free $ pi $ (list_comb (c, args)) $ (list_comb (c, args2))); |
|
215 fun lhs_arg ((dt, arg_no), (arg, arg2)) = |
|
216 (*...*) |
|
217 @{term True} |
|
218 val arg_nos = 0 upto (length dts - 1) |
|
219 val lhss = mk_conjl (map lhs_arg (dts ~~ arg_nos ~~ (args ~~ args2))) |
|
220 val eq = Logic.mk_implies (HOLogic.mk_Trueprop lhss, rhs) |
213 in |
221 in |
214 [] |
222 eq |
215 end |
223 end |
216 val (_, (_, _, constrs)) = nth descr ith_dtyp; |
224 val (_, (_, _, constrs)) = nth descr ith_dtyp; |
217 val eqs = map2i alpha_bn_constr constrs args_in_bns |
225 val eqs = map2i alpha_bn_constr constrs args_in_bns |
218 in |
226 in |
219 ((bn, alpha_bn_name), (alpha_bn_free, eqs)) |
227 ((bn, alpha_bn_name), (alpha_bn_free, eqs)) |