321 fun alpha_eqvt_tac' _ = |
321 fun alpha_eqvt_tac' _ = |
322 if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy |
322 if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy |
323 else alpha_eqvt_tac alpha_induct_loc (raw_perm_def @ alpha_inj_loc) lthy4 1 |
323 else alpha_eqvt_tac alpha_induct_loc (raw_perm_def @ alpha_inj_loc) lthy4 1 |
324 val alpha_eqvt_loc = build_alpha_eqvts (List.take (alpha_ts_loc, length perms)) perms alpha_eqvt_tac' lthy4; |
324 val alpha_eqvt_loc = build_alpha_eqvts (List.take (alpha_ts_loc, length perms)) perms alpha_eqvt_tac' lthy4; |
325 val alpha_eqvt = ProofContext.export lthy4 lthy2 alpha_eqvt_loc; |
325 val alpha_eqvt = ProofContext.export lthy4 lthy2 alpha_eqvt_loc; |
|
326 val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4; |
326 in |
327 in |
327 if !restricted_nominal = 0 then |
328 if !restricted_nominal = 0 then |
328 ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy4) |
329 ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy4) |
329 else |
330 else |
330 let |
331 let |
331 val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt perms (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4; |
332 val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc |
332 val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc perms |
|
333 ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) induct lthy5; |
333 ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) induct lthy5; |
334 val raw_fv_bv_eqvt_loc = flat (map snd bv_eqvts) @ (snd fv_eqvts) |
334 val raw_fv_bv_eqvt_loc = flat (map snd bv_eqvts) @ (snd fv_eqvts) |
335 val raw_fv_bv_eqvt = ProofContext.export lthy6 lthy3 raw_fv_bv_eqvt_loc; |
335 val raw_fv_bv_eqvt = ProofContext.export lthy6 lthy3 raw_fv_bv_eqvt_loc; |
336 val alpha_equivp_loc = map (equivp_hack lthy6) alpha_ts_loc |
336 val alpha_equivp_loc = map (equivp_hack lthy6) alpha_ts_loc |
337 val alpha_equivp_loc = build_equivps alpha_ts_loc induct alpha_induct_loc |
337 val alpha_equivp_loc = build_equivps alpha_ts_loc induct alpha_induct_loc |