335 val alpha_cases_loc = #elims alpha |
335 val alpha_cases_loc = #elims alpha |
336 val alpha_cases = ProofContext.export lthy4 lthy3 alpha_cases_loc |
336 val alpha_cases = ProofContext.export lthy4 lthy3 alpha_cases_loc |
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 val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4; |
339 val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4; |
|
340 val _ = tracing "3"; |
340 val fv_eqvt_tac = |
341 val fv_eqvt_tac = |
341 if !cheat_fv_eqvt then (fn _ => fn _ => Skip_Proof.cheat_tac thy) |
342 if !cheat_fv_eqvt then (fn _ => fn _ => Skip_Proof.cheat_tac thy) |
342 else build_eqvts_tac induct ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) lthy5 |
343 else build_eqvts_tac induct ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) lthy5 |
|
344 val _ = tracing "4"; |
343 val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc_nobn fv_eqvt_tac lthy5; |
345 val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc_nobn fv_eqvt_tac lthy5; |
344 val (fv_bn_eqvts, lthy6a) = fold_map (build_bv_eqvt ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) inducts) (fv_ts_loc_bn ~~ (map snd bns)) lthy6; |
346 val _ = tracing "4a"; |
|
347 val (fv_bn_eqvts, lthy6a) = |
|
348 if fv_ts_loc_bn = [] then ([], lthy6) else |
|
349 fold_map (build_bv_eqvt ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) inducts) |
|
350 (fv_ts_loc_bn ~~ (map snd bns)) lthy6; |
|
351 val _ = tracing "4b"; |
345 val lthy6 = lthy6a; |
352 val lthy6 = lthy6a; |
346 val raw_fv_bv_eqvt_loc = flat (map snd bv_eqvts) @ (snd fv_eqvts) |
353 val raw_fv_bv_eqvt_loc = flat (map snd bv_eqvts) @ (snd fv_eqvts) |
347 val raw_fv_bv_eqvt = ProofContext.export lthy6 lthy3 raw_fv_bv_eqvt_loc; |
354 val raw_fv_bv_eqvt = ProofContext.export lthy6 lthy3 raw_fv_bv_eqvt_loc; |
|
355 val _ = tracing "5"; |
348 fun alpha_eqvt_tac' _ = |
356 fun alpha_eqvt_tac' _ = |
349 if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy |
357 if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy |
350 else alpha_eqvt_tac alpha_induct_loc (raw_perm_def @ alpha_inj_loc @ raw_fv_bv_eqvt_loc) lthy6 1 |
358 else alpha_eqvt_tac alpha_induct_loc (raw_perm_def @ alpha_inj_loc @ raw_fv_bv_eqvt_loc) lthy6 1 |
351 val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc alpha_eqvt_tac' lthy6; |
359 val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc alpha_eqvt_tac' lthy6; |
352 val alpha_eqvt = ProofContext.export lthy6 lthy2 alpha_eqvt_loc; |
360 val alpha_eqvt = ProofContext.export lthy6 lthy2 alpha_eqvt_loc; |