330 fun alpha_eqvt_tac' _ = |
330 fun alpha_eqvt_tac' _ = |
331 if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy |
331 if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy |
332 else alpha_eqvt_tac alpha_induct (raw_perm_def @ alpha_eq_iff @ raw_fv_bv_eqvt) lthy6a 1 |
332 else alpha_eqvt_tac alpha_induct (raw_perm_def @ alpha_eq_iff @ raw_fv_bv_eqvt) lthy6a 1 |
333 val alpha_eqvt = build_alpha_eqvts alpha_ts alpha_eqvt_tac' lthy6a; |
333 val alpha_eqvt = build_alpha_eqvts alpha_ts alpha_eqvt_tac' lthy6a; |
334 val _ = tracing "Proving equivalence"; |
334 val _ = tracing "Proving equivalence"; |
|
335 val fv_alpha_all = combine_fv_alpha_bns (fv_ts_nobn, fv_ts_bn) (alpha_ts_nobn, alpha_ts_bn) bn_nos; |
|
336 val reflps = build_alpha_refl fv_alpha_all induct alpha_eq_iff lthy6a; |
335 val alpha_equivp = |
337 val alpha_equivp = |
336 if !cheat_equivp then map (equivp_hack lthy6a) alpha_ts_nobn |
338 if !cheat_equivp then map (equivp_hack lthy6a) alpha_ts_nobn |
337 else build_equivps alpha_ts induct alpha_induct |
339 else build_equivps alpha_ts reflps alpha_induct |
338 inject alpha_eq_iff distincts alpha_cases alpha_eqvt lthy6a; |
340 inject alpha_eq_iff distincts alpha_cases alpha_eqvt lthy6a; |
339 val qty_binds = map (fn (_, b, _, _) => b) dts; |
341 val qty_binds = map (fn (_, b, _, _) => b) dts; |
340 val qty_names = map Name.of_binding qty_binds; |
342 val qty_names = map Name.of_binding qty_binds; |
341 val qty_full_names = map (Long_Name.qualify thy_name) qty_names |
343 val qty_full_names = map (Long_Name.qualify thy_name) qty_names |
342 val lthy7 = define_quotient_type |
344 val lthy7 = define_quotient_type |