267 val alpha_cases_loc = #elims alpha |
267 val alpha_cases_loc = #elims alpha |
268 val alpha_cases = ProofContext.export lthy4 lthy3 alpha_cases_loc |
268 val alpha_cases = ProofContext.export lthy4 lthy3 alpha_cases_loc |
269 val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distinct) alpha_cases_loc lthy4 |
269 val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distinct) alpha_cases_loc lthy4 |
270 val alpha_inj = ProofContext.export lthy4 lthy3 alpha_inj_loc |
270 val alpha_inj = ProofContext.export lthy4 lthy3 alpha_inj_loc |
271 in |
271 in |
272 if !restricted_nominal then |
272 if !restricted_nominal = 0 then |
273 ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy4) |
273 ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy4) |
274 else |
274 else |
275 let |
275 let |
276 val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt perms (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4; |
276 val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt perms (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4; |
277 val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc perms |
277 val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc perms |
297 map (fn (cname, dts) => |
297 map (fn (cname, dts) => |
298 Const (cname, map (typ_of_dtyp descr sorts) dts ---> |
298 Const (cname, map (typ_of_dtyp descr sorts) dts ---> |
299 typ_of_dtyp descr sorts (DtRec i))) l) descr); |
299 typ_of_dtyp descr sorts (DtRec i))) l) descr); |
300 val (consts_defs, lthy8) = fold_map Quotient_Def.quotient_lift_const (const_names ~~ raw_consts) lthy7; |
300 val (consts_defs, lthy8) = fold_map Quotient_Def.quotient_lift_const (const_names ~~ raw_consts) lthy7; |
301 val (consts, const_defs) = split_list consts_defs; |
301 val (consts, const_defs) = split_list consts_defs; |
|
302 in |
|
303 if !restricted_nominal = 1 then |
|
304 ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy8) |
|
305 else |
|
306 let |
302 val (bns_rsp_pre, lthy9) = fold_map ( |
307 val (bns_rsp_pre, lthy9) = fold_map ( |
303 fn (bn_t, i) => prove_const_rsp Binding.empty [bn_t] |
308 fn (bn_t, i) => prove_const_rsp Binding.empty [bn_t] |
304 (fn _ => fvbv_rsp_tac (nth alpha_inducts i) raw_bn_eqs 1)) bns lthy8; |
309 (fn _ => fvbv_rsp_tac (nth alpha_inducts i) raw_bn_eqs 1)) bns lthy8; |
305 val bns_rsp = flat (map snd bns_rsp_pre); |
310 val bns_rsp = flat (map snd bns_rsp_pre); |
306 val ((_, fv_rsp), lthy10) = prove_const_rsp Binding.empty fv_ts |
311 val ((_, fv_rsp), lthy10) = prove_const_rsp Binding.empty fv_ts |
339 [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19; |
344 [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19; |
340 in |
345 in |
341 ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy20) |
346 ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy20) |
342 end |
347 end |
343 end |
348 end |
|
349 end |
344 *} |
350 *} |
345 |
351 |
346 ML {* |
352 ML {* |
347 (* parsing the datatypes and declaring *) |
353 (* parsing the datatypes and declaring *) |
348 (* constructors in the local theory *) |
354 (* constructors in the local theory *) |