434 |
434 |
435 (* proving equivariance lemmas *) |
435 (* proving equivariance lemmas *) |
436 val _ = warning "Proving equivariance"; |
436 val _ = warning "Proving equivariance"; |
437 val (bv_eqvt, lthy5) = prove_eqvt raw_tys induct_thm (raw_bn_eqs @ raw_perm_def) (map fst bns) lthy4 |
437 val (bv_eqvt, lthy5) = prove_eqvt raw_tys induct_thm (raw_bn_eqs @ raw_perm_def) (map fst bns) lthy4 |
438 val (fv_eqvt, lthy6) = prove_eqvt raw_tys induct_thm (fv_def @ raw_perm_def) (fv @ fvbn) lthy5 |
438 val (fv_eqvt, lthy6) = prove_eqvt raw_tys induct_thm (fv_def @ raw_perm_def) (fv @ fvbn) lthy5 |
439 fun alpha_eqvt_tac' _ = |
439 val (alpha_eqvt, lthy6a) = Nominal_Eqvt.equivariance alpha_ts alpha_induct alpha_intros lthy6; |
440 if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy |
|
441 else alpha_eqvt_tac alpha_induct (raw_perm_def @ alpha_eq_iff_simp) lthy6 1 |
|
442 val alpha_eqvt = build_alpha_eqvts alpha_ts alpha_eqvt_tac' lthy6; |
|
443 |
440 |
444 (* proving alpha equivalence *) |
441 (* proving alpha equivalence *) |
445 val _ = warning "Proving equivalence"; |
442 val _ = warning "Proving equivalence"; |
446 val fv_alpha_all = combine_fv_alpha_bns (fv, fvbn) (alpha_ts_nobn, alpha_ts_bn) bn_nos; |
443 val fv_alpha_all = combine_fv_alpha_bns (fv, fvbn) (alpha_ts_nobn, alpha_ts_bn) bn_nos; |
447 val reflps = build_alpha_refl fv_alpha_all alpha_ts induct_thm alpha_eq_iff_simp lthy6; |
444 val reflps = build_alpha_refl fv_alpha_all alpha_ts induct_thm alpha_eq_iff_simp lthy6a; |
448 val alpha_equivp = |
445 val alpha_equivp = |
449 if !cheat_equivp then map (equivp_hack lthy6) alpha_ts |
446 if !cheat_equivp then map (equivp_hack lthy6a) alpha_ts |
450 else build_equivps alpha_ts reflps alpha_induct |
447 else build_equivps alpha_ts reflps alpha_induct |
451 inject_thms alpha_eq_iff_simp distinct_thms alpha_cases alpha_eqvt lthy6; |
448 inject_thms alpha_eq_iff_simp distinct_thms alpha_cases alpha_eqvt lthy6a; |
452 val qty_binds = map (fn (_, b, _, _) => b) dts; |
449 val qty_binds = map (fn (_, b, _, _) => b) dts; |
453 val qty_names = map Name.of_binding qty_binds; |
450 val qty_names = map Name.of_binding qty_binds; |
454 val qty_full_names = map (Long_Name.qualify thy_name) qty_names |
451 val qty_full_names = map (Long_Name.qualify thy_name) qty_names |
455 val (qtys, lthy7) = define_quotient_types qty_binds all_typs alpha_ts_nobn alpha_equivp lthy6; |
452 val (qtys, lthy7) = define_quotient_types qty_binds all_typs alpha_ts_nobn alpha_equivp lthy6a; |
456 val const_names = map Name.of_binding (flat (map (fn (_, _, _, t) => map (fn (b, _, _) => b) t) dts)); |
453 val const_names = map Name.of_binding (flat (map (fn (_, _, _, t) => map (fn (b, _, _) => b) t) dts)); |
457 val raw_consts = |
454 val raw_consts = |
458 flat (map (fn (i, (_, _, l)) => |
455 flat (map (fn (i, (_, _, l)) => |
459 map (fn (cname, dts) => |
456 map (fn (cname, dts) => |
460 Const (cname, map (Datatype_Aux.typ_of_dtyp descr sorts) dts ---> |
457 Const (cname, map (Datatype_Aux.typ_of_dtyp descr sorts) dts ---> |