298 val inducts = #inducts dtinfo; |
298 val inducts = #inducts dtinfo; |
299 val ((raw_perm_def, raw_perm_simps, perms), lthy3) = |
299 val ((raw_perm_def, raw_perm_simps, perms), lthy3) = |
300 Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy2; |
300 Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy2; |
301 val raw_binds_flat = map (map flat) raw_binds; |
301 val raw_binds_flat = map (map flat) raw_binds; |
302 val (((fv_ts_loc, fv_def_loc), alpha), lthy4) = define_fv_alpha dtinfo raw_binds_flat bn_funs_decls lthy3; |
302 val (((fv_ts_loc, fv_def_loc), alpha), lthy4) = define_fv_alpha dtinfo raw_binds_flat bn_funs_decls lthy3; |
303 in |
|
304 if !restricted_nominal = 0 then |
|
305 ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy4) |
|
306 else |
|
307 let |
|
308 val alpha_ts_loc = #preds alpha |
303 val alpha_ts_loc = #preds alpha |
309 val morphism_4_3 = ProofContext.export_morphism lthy4 lthy3; |
304 val morphism_4_3 = ProofContext.export_morphism lthy4 lthy3; |
310 val fv_ts = map (Morphism.term morphism_4_3) fv_ts_loc; |
305 val fv_ts = map (Morphism.term morphism_4_3) fv_ts_loc; |
311 val alpha_ts = map (Morphism.term morphism_4_3) alpha_ts_loc; |
306 val alpha_ts = map (Morphism.term morphism_4_3) alpha_ts_loc; |
312 val alpha_induct_loc = #induct alpha |
307 val alpha_induct_loc = #induct alpha |
328 val raw_fv_bv_eqvt_loc = flat (map snd bv_eqvts) @ (snd fv_eqvts) |
323 val raw_fv_bv_eqvt_loc = flat (map snd bv_eqvts) @ (snd fv_eqvts) |
329 val raw_fv_bv_eqvt = ProofContext.export lthy6 lthy3 raw_fv_bv_eqvt_loc; |
324 val raw_fv_bv_eqvt = ProofContext.export lthy6 lthy3 raw_fv_bv_eqvt_loc; |
330 val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc perms |
325 val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc perms |
331 (raw_perm_def @ alpha_inj_loc) alpha_induct_loc lthy6; |
326 (raw_perm_def @ alpha_inj_loc) alpha_induct_loc lthy6; |
332 val alpha_eqvt = ProofContext.export lthy6 lthy2 alpha_eqvt_loc; |
327 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; |