517 val lthy16 = note_simp_suffix "fv" q_fv lthy15; |
517 val lthy16 = note_simp_suffix "fv" q_fv lthy15; |
518 val q_bn = map (lift_thm qtys lthy16) raw_bn_eqs; |
518 val q_bn = map (lift_thm qtys lthy16) raw_bn_eqs; |
519 val lthy17 = note_simp_suffix "bn" q_bn lthy16; |
519 val lthy17 = note_simp_suffix "bn" q_bn lthy16; |
520 val _ = warning "Lifting eq-iff"; |
520 val _ = warning "Lifting eq-iff"; |
521 (*val _ = map tracing (map PolyML.makestring alpha_eq_iff);*) |
521 (*val _ = map tracing (map PolyML.makestring alpha_eq_iff);*) |
522 val eq_iff_unfolded0 = map (Local_Defs.unfold lthy17 @{thms alphas3}) alpha_eq_iff_simp |
522 val eq_iff_unfolded0 = map (Local_Defs.unfold lthy17 @{thms alphas}) alpha_eq_iff_simp |
523 val eq_iff_unfolded1 = map (Local_Defs.unfold lthy17 @{thms alphas2}) eq_iff_unfolded0 |
523 val eq_iff_unfolded1 = map (Local_Defs.unfold lthy17 @{thms Pair_eqvt}) eq_iff_unfolded0 |
524 val eq_iff_unfolded2 = map (Local_Defs.unfold lthy17 @{thms alphas} ) eq_iff_unfolded1 |
524 val q_eq_iff_pre0 = map (lift_thm qtys lthy17) eq_iff_unfolded1; |
525 val q_eq_iff_pre0 = map (lift_thm qtys lthy17) eq_iff_unfolded2; |
525 val q_eq_iff_pre1 = map (Local_Defs.fold lthy17 @{thms Pair_eqvt}) q_eq_iff_pre0 |
526 val q_eq_iff_pre1 = map (Local_Defs.fold lthy17 @{thms alphas3}) q_eq_iff_pre0 |
526 val q_eq_iff_pre2 = map (Local_Defs.fold lthy17 @{thms alphas}) q_eq_iff_pre1 |
527 val q_eq_iff_pre2 = map (Local_Defs.fold lthy17 @{thms alphas2}) q_eq_iff_pre1 |
527 val q_eq_iff = map (Local_Defs.unfold lthy17 (Quotient_Info.id_simps_get lthy17)) q_eq_iff_pre2 |
528 val q_eq_iff = map (Local_Defs.fold lthy17 @{thms alphas}) q_eq_iff_pre2 |
|
529 val (_, lthy18) = Local_Theory.note ((suffix_bind "eq_iff", []), q_eq_iff) lthy17; |
528 val (_, lthy18) = Local_Theory.note ((suffix_bind "eq_iff", []), q_eq_iff) lthy17; |
530 val q_dis = map (lift_thm qtys lthy18) rel_dists; |
529 val q_dis = map (lift_thm qtys lthy18) rel_dists; |
531 val lthy19 = note_simp_suffix "distinct" q_dis lthy18; |
530 val lthy19 = note_simp_suffix "distinct" q_dis lthy18; |
532 val q_eqvt = map (lift_thm qtys lthy19) (bv_eqvt @ fv_eqvt); |
531 val q_eqvt = map (lift_thm qtys lthy19) (bv_eqvt @ fv_eqvt); |
533 val (_, lthy20) = Local_Theory.note ((Binding.empty, |
532 val (_, lthy20) = Local_Theory.note ((Binding.empty, |