154 end |
154 end |
155 *} |
155 *} |
156 |
156 |
157 (* We assume no bindings in the type on which bn is defined *) |
157 (* We assume no bindings in the type on which bn is defined *) |
158 ML {* |
158 ML {* |
159 fun fv_bn thy (dt_info : Datatype_Aux.info) fv_frees (bn, ith_dtyp, args_in_bn) = |
159 fun fv_bn thy (dt_info : Datatype_Aux.info) fv_frees (bn, ith_dtyp, args_in_bns) = |
160 let |
160 let |
161 val {descr, sorts, ...} = dt_info; |
161 val {descr, sorts, ...} = dt_info; |
162 fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); |
162 fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); |
163 val fvbn_name = "fv_" ^ (Long_Name.base_name (fst (dest_Const bn))); |
163 val fvbn_name = "fv_" ^ (Long_Name.base_name (fst (dest_Const bn))); |
164 val fvbn = Free (fvbn_name, fastype_of (nth fv_frees ith_dtyp)); |
164 val fvbn = Free (fvbn_name, fastype_of (nth fv_frees ith_dtyp)); |
165 fun fv_bn_constr (cname, dts) = |
165 fun fv_bn_constr (cname, dts) args_in_bn = |
166 let |
166 let |
167 val Ts = map (typ_of_dtyp descr sorts) dts; |
167 val Ts = map (typ_of_dtyp descr sorts) dts; |
168 val names = Datatype_Prop.make_tnames Ts; |
168 val names = Datatype_Prop.make_tnames Ts; |
169 val args = map Free (names ~~ Ts); |
169 val args = map Free (names ~~ Ts); |
170 val c = Const (cname, Ts ---> (nth_dtyp ith_dtyp)); |
170 val c = Const (cname, Ts ---> (nth_dtyp ith_dtyp)); |
185 in |
185 in |
186 HOLogic.mk_Trueprop (HOLogic.mk_eq |
186 HOLogic.mk_Trueprop (HOLogic.mk_eq |
187 (fvbn $ list_comb (c, args), mk_union (map fv_arg (dts ~~ args ~~ arg_nos)))) |
187 (fvbn $ list_comb (c, args), mk_union (map fv_arg (dts ~~ args ~~ arg_nos)))) |
188 end; |
188 end; |
189 val (_, (_, _, constrs)) = nth descr ith_dtyp; |
189 val (_, (_, _, constrs)) = nth descr ith_dtyp; |
190 val eqs = map fv_bn_constr constrs |
190 val eqs = map2i fv_bn_constr constrs args_in_bns |
191 in |
191 in |
192 ((bn, fvbn), (fvbn_name, eqs)) |
192 ((bn, fvbn), (fvbn_name, eqs)) |
193 end |
193 end |
194 *} |
194 *} |
195 |
195 |
350 setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Fv.lam") 2 *} |
350 setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Fv.lam") 2 *} |
351 |
351 |
352 |
352 |
353 local_setup {* |
353 local_setup {* |
354 snd o define_fv_alpha (Datatype.the_info @{theory} "Fv.lam") |
354 snd o define_fv_alpha (Datatype.the_info @{theory} "Fv.lam") |
355 [[[], [], [(SOME (@{term bi}, false), 0, 1)]], [[]]] [(@{term bi}, 1, [0])] *} |
355 [[[], [], [(SOME (@{term bi}, false), 0, 1)]], [[]]] [(@{term bi}, 1, [[0]])] *} |
356 print_theorems |
356 print_theorems |
357 *) |
357 *) |
358 |
358 |
359 (* |
359 (* |
360 datatype rtrm1 = |
360 datatype rtrm1 = |