335 else alpha_eqvt_tac alpha_induct (raw_perm_def @ alpha_eq_iff @ raw_fv_bv_eqvt) lthy6a 1 |
335 else alpha_eqvt_tac alpha_induct (raw_perm_def @ alpha_eq_iff @ raw_fv_bv_eqvt) lthy6a 1 |
336 val alpha_eqvt = build_alpha_eqvts alpha_ts alpha_eqvt_tac' lthy6a; |
336 val alpha_eqvt = build_alpha_eqvts alpha_ts alpha_eqvt_tac' lthy6a; |
337 val _ = tracing "Proving equivalence"; |
337 val _ = tracing "Proving equivalence"; |
338 val (rfv_ts_nobn, rfv_ts_bn) = chop (length perms) ordered_fv_ts; |
338 val (rfv_ts_nobn, rfv_ts_bn) = chop (length perms) ordered_fv_ts; |
339 val fv_alpha_all = combine_fv_alpha_bns (rfv_ts_nobn, rfv_ts_bn) (alpha_ts_nobn, alpha_ts_bn) bn_nos; |
339 val fv_alpha_all = combine_fv_alpha_bns (rfv_ts_nobn, rfv_ts_bn) (alpha_ts_nobn, alpha_ts_bn) bn_nos; |
340 val reflps = build_alpha_refl fv_alpha_all induct alpha_eq_iff lthy6a; |
340 val reflps = build_alpha_refl fv_alpha_all alpha_ts induct alpha_eq_iff lthy6a; |
341 val alpha_equivp = |
341 val alpha_equivp = |
342 if !cheat_equivp then map (equivp_hack lthy6a) alpha_ts_nobn |
342 if !cheat_equivp then map (equivp_hack lthy6a) alpha_ts_nobn |
343 else build_equivps alpha_ts reflps alpha_induct |
343 else build_equivps alpha_ts reflps alpha_induct |
344 inject alpha_eq_iff distincts alpha_cases alpha_eqvt lthy6a; |
344 inject alpha_eq_iff distincts alpha_cases alpha_eqvt lthy6a; |
345 val qty_binds = map (fn (_, b, _, _) => b) dts; |
345 val qty_binds = map (fn (_, b, _, _) => b) dts; |