337 val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distincts) alpha_cases_loc lthy4 |
337 val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distincts) alpha_cases_loc lthy4 |
338 val alpha_inj = ProofContext.export lthy4 lthy3 alpha_inj_loc |
338 val alpha_inj = ProofContext.export lthy4 lthy3 alpha_inj_loc |
339 fun alpha_eqvt_tac' _ = |
339 fun alpha_eqvt_tac' _ = |
340 if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy |
340 if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy |
341 else alpha_eqvt_tac alpha_induct_loc (raw_perm_def @ alpha_inj_loc) lthy4 1 |
341 else alpha_eqvt_tac alpha_induct_loc (raw_perm_def @ alpha_inj_loc) lthy4 1 |
342 val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc_nobn perms alpha_eqvt_tac' lthy4; |
342 val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc alpha_eqvt_tac' lthy4; |
343 val alpha_eqvt = ProofContext.export lthy4 lthy2 alpha_eqvt_loc; |
343 val alpha_eqvt = ProofContext.export lthy4 lthy2 alpha_eqvt_loc; |
|
344 val _ = map tracing (map PolyML.makestring alpha_eqvt) |
344 val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4; |
345 val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4; |
345 val fv_eqvt_tac = |
346 val fv_eqvt_tac = |
346 if !cheat_fv_eqvt then (fn _ => fn _ => Skip_Proof.cheat_tac thy) |
347 if !cheat_fv_eqvt then (fn _ => fn _ => Skip_Proof.cheat_tac thy) |
347 else build_eqvts_tac induct ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) lthy5 |
348 else build_eqvts_tac induct ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) lthy5 |
348 val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc fv_eqvt_tac lthy5; |
349 val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc fv_eqvt_tac lthy5; |