462 val q_fv = map (lift_thm lthy15) fv_def; |
462 val q_fv = map (lift_thm lthy15) fv_def; |
463 val lthy16 = note_simp_suffix "fv" q_fv lthy15; |
463 val lthy16 = note_simp_suffix "fv" q_fv lthy15; |
464 val q_bn = map (lift_thm lthy16) raw_bn_eqs; |
464 val q_bn = map (lift_thm lthy16) raw_bn_eqs; |
465 val lthy17 = note_simp_suffix "bn" q_bn lthy16; |
465 val lthy17 = note_simp_suffix "bn" q_bn lthy16; |
466 val _ = tracing "Lifting eq-iff"; |
466 val _ = tracing "Lifting eq-iff"; |
467 val eq_iff_unfolded1 = map (Local_Defs.unfold lthy17 @{thms alpha_gen2}) alpha_eq_iff |
467 val eq_iff_unfolded1 = map (Local_Defs.unfold lthy17 @{thms alphas2}) alpha_eq_iff |
468 val eq_iff_unfolded2 = map (Local_Defs.unfold lthy17 @{thms alpha_gen}) eq_iff_unfolded1 |
468 val eq_iff_unfolded2 = map (Local_Defs.unfold lthy17 @{thms alphas}) eq_iff_unfolded1 |
469 val q_eq_iff_pre1 = map (lift_thm lthy17) eq_iff_unfolded2; |
469 val q_eq_iff_pre1 = map (lift_thm lthy17) eq_iff_unfolded2; |
470 val q_eq_iff_pre2 = map (Local_Defs.fold lthy17 @{thms alpha_gen2}) q_eq_iff_pre1 |
470 val q_eq_iff_pre2 = map (Local_Defs.fold lthy17 @{thms alphas2}) q_eq_iff_pre1 |
471 val q_eq_iff = map (Local_Defs.fold lthy17 @{thms alpha_gen}) q_eq_iff_pre2 |
471 val q_eq_iff = map (Local_Defs.fold lthy17 @{thms alphas}) q_eq_iff_pre2 |
472 val (_, lthy18) = Local_Theory.note ((suffix_bind "eq_iff", []), q_eq_iff) lthy17; |
472 val (_, lthy18) = Local_Theory.note ((suffix_bind "eq_iff", []), q_eq_iff) lthy17; |
473 val q_dis = map (lift_thm lthy18) rel_dists; |
473 val q_dis = map (lift_thm lthy18) rel_dists; |
474 val lthy19 = note_simp_suffix "distinct" q_dis lthy18; |
474 val lthy19 = note_simp_suffix "distinct" q_dis lthy18; |
475 val q_eqvt = map (lift_thm lthy19) (bv_eqvt @ fv_eqvt); |
475 val q_eqvt = map (lift_thm lthy19) (bv_eqvt @ fv_eqvt); |
476 val (_, lthy20) = Local_Theory.note ((Binding.empty, |
476 val (_, lthy20) = Local_Theory.note ((Binding.empty, |