414 val (_, lthy15) = Local_Theory.note ((Binding.name (q_name ^ "_perm"), []), q_perm) lthy14a; |
414 val (_, lthy15) = Local_Theory.note ((Binding.name (q_name ^ "_perm"), []), q_perm) lthy14a; |
415 val q_fv = map (lift_thm lthy15) fv_def; |
415 val q_fv = map (lift_thm lthy15) fv_def; |
416 val (_, lthy16) = Local_Theory.note ((Binding.name (q_name ^ "_fv"), []), q_fv) lthy15; |
416 val (_, lthy16) = Local_Theory.note ((Binding.name (q_name ^ "_fv"), []), q_fv) lthy15; |
417 val q_bn = map (lift_thm lthy16) raw_bn_eqs; |
417 val q_bn = map (lift_thm lthy16) raw_bn_eqs; |
418 val (_, lthy17) = Local_Theory.note ((Binding.name (q_name ^ "_bn"), []), q_bn) lthy16; |
418 val (_, lthy17) = Local_Theory.note ((Binding.name (q_name ^ "_bn"), []), q_bn) lthy16; |
419 val inj_unfolded = map (Local_Defs.unfold lthy17 @{thms alpha_gen}) alpha_inj |
419 val inj_unfolded1 = map (Local_Defs.unfold lthy17 @{thms alpha_gen2}) alpha_inj |
420 val q_inj_pre = map (lift_thm lthy17) inj_unfolded; |
420 val inj_unfolded2 = map (Local_Defs.unfold lthy17 @{thms alpha_gen}) inj_unfolded1 |
421 val q_inj = map (Local_Defs.fold lthy17 @{thms alpha_gen}) q_inj_pre |
421 val q_inj_pre1 = map (lift_thm lthy17) inj_unfolded2; |
|
422 val q_inj_pre2 = map (Local_Defs.fold lthy17 @{thms alpha_gen2}) q_inj_pre1 |
|
423 val q_inj = map (Local_Defs.fold lthy17 @{thms alpha_gen}) q_inj_pre2 |
422 val (_, lthy18) = Local_Theory.note ((Binding.name (q_name ^ "_inject"), []), q_inj) lthy17; |
424 val (_, lthy18) = Local_Theory.note ((Binding.name (q_name ^ "_inject"), []), q_inj) lthy17; |
423 val rel_dists = flat (map (distinct_rel lthy18 alpha_cases) |
425 val rel_dists = flat (map (distinct_rel lthy18 alpha_cases) |
424 (rel_distinct ~~ (List.take (alpha_ts, (length dts))))) |
426 (rel_distinct ~~ (List.take (alpha_ts, (length dts))))) |
425 val q_dis = map (lift_thm lthy18) rel_dists; |
427 val q_dis = map (lift_thm lthy18) rel_dists; |
426 val (_, lthy19) = Local_Theory.note ((Binding.name (q_name ^ "_distinct"), []), q_dis) lthy18; |
428 val (_, lthy19) = Local_Theory.note ((Binding.name (q_name ^ "_distinct"), []), q_dis) lthy18; |