315 val alpha_intros = #intrs alpha; |
315 val alpha_intros = #intrs alpha; |
316 val alpha_cases_loc = #elims alpha |
316 val alpha_cases_loc = #elims alpha |
317 val alpha_cases = ProofContext.export lthy4 lthy3 alpha_cases_loc |
317 val alpha_cases = ProofContext.export lthy4 lthy3 alpha_cases_loc |
318 val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distinct) alpha_cases_loc lthy4 |
318 val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distinct) alpha_cases_loc lthy4 |
319 val alpha_inj = ProofContext.export lthy4 lthy3 alpha_inj_loc |
319 val alpha_inj = ProofContext.export lthy4 lthy3 alpha_inj_loc |
|
320 in |
|
321 if !restricted_nominal = 0 then |
|
322 ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy5) |
|
323 else |
|
324 let |
320 val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt perms (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4; |
325 val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt perms (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4; |
321 val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc perms |
326 val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc perms |
322 ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) induct lthy5; |
327 ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) induct lthy5; |
323 val raw_fv_bv_eqvt_loc = flat (map snd bv_eqvts) @ (snd fv_eqvts) |
328 val raw_fv_bv_eqvt_loc = flat (map snd bv_eqvts) @ (snd fv_eqvts) |
324 val raw_fv_bv_eqvt = ProofContext.export lthy6 lthy3 raw_fv_bv_eqvt_loc; |
329 val raw_fv_bv_eqvt = ProofContext.export lthy6 lthy3 raw_fv_bv_eqvt_loc; |
325 val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc perms |
330 val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc perms |
326 (raw_perm_def @ alpha_inj_loc) alpha_induct_loc lthy6; |
331 (raw_perm_def @ alpha_inj_loc) alpha_induct_loc lthy6; |
327 val alpha_eqvt = ProofContext.export lthy6 lthy2 alpha_eqvt_loc; |
332 val alpha_eqvt = ProofContext.export lthy6 lthy2 alpha_eqvt_loc; |
328 in |
|
329 if !restricted_nominal = 0 then |
|
330 ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy5) |
|
331 else |
|
332 let |
|
333 val alpha_equivp_loc = map (equivp_hack lthy6) alpha_ts_loc |
333 val alpha_equivp_loc = map (equivp_hack lthy6) alpha_ts_loc |
334 val alpha_equivp_loc = build_equivps alpha_ts_loc induct alpha_induct_loc |
334 val alpha_equivp_loc = build_equivps alpha_ts_loc induct alpha_induct_loc |
335 inject alpha_inj_loc distinct alpha_cases_loc alpha_eqvt_loc lthy6; |
335 inject alpha_inj_loc distinct alpha_cases_loc alpha_eqvt_loc lthy6; |
336 val alpha_equivp = ProofContext.export lthy6 lthy2 alpha_equivp_loc; |
336 val alpha_equivp = ProofContext.export lthy6 lthy2 alpha_equivp_loc; |
337 val qty_binds = map (fn (_, b, _, _) => b) dts; |
337 val qty_binds = map (fn (_, b, _, _) => b) dts; |