324 val (_, lthy15) = Local_Theory.note ((Binding.name (q_name ^ "_perm"), []), q_perm) lthy14; |
324 val (_, lthy15) = Local_Theory.note ((Binding.name (q_name ^ "_perm"), []), q_perm) lthy14; |
325 val q_fv = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy15, th))) fv_def; |
325 val q_fv = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy15, th))) fv_def; |
326 val (_, lthy16) = Local_Theory.note ((Binding.name (q_name ^ "_fv"), []), q_fv) lthy15; |
326 val (_, lthy16) = Local_Theory.note ((Binding.name (q_name ^ "_fv"), []), q_fv) lthy15; |
327 val q_bn = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy16, th))) raw_bn_eqs; |
327 val q_bn = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy16, th))) raw_bn_eqs; |
328 val (_, lthy17) = Local_Theory.note ((Binding.name (q_name ^ "_bn"), []), q_bn) lthy16; |
328 val (_, lthy17) = Local_Theory.note ((Binding.name (q_name ^ "_bn"), []), q_bn) lthy16; |
329 val inj_unfolded = map (LocalDefs.unfold lthy17 @{thms alpha_gen}) alpha_inj |
329 val inj_unfolded = map (Local_Defs.unfold lthy17 @{thms alpha_gen}) alpha_inj |
330 val q_inj_pre = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy17, th))) inj_unfolded; |
330 val q_inj_pre = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy17, th))) inj_unfolded; |
331 val q_inj = map (LocalDefs.fold lthy17 @{thms alpha_gen}) q_inj_pre |
331 val q_inj = map (Local_Defs.fold lthy17 @{thms alpha_gen}) q_inj_pre |
332 val (_, lthy18) = Local_Theory.note ((Binding.name (q_name ^ "_inject"), []), q_inj) lthy17; |
332 val (_, lthy18) = Local_Theory.note ((Binding.name (q_name ^ "_inject"), []), q_inj) lthy17; |
333 val rel_dists = flat (map (distinct_rel lthy18 alpha_cases) |
333 val rel_dists = flat (map (distinct_rel lthy18 alpha_cases) |
334 (rel_distinct ~~ (List.take (alpha_ts, (length dts))))) |
334 (rel_distinct ~~ (List.take (alpha_ts, (length dts))))) |
335 val q_dis = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy18, th))) rel_dists; |
335 val q_dis = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy18, th))) rel_dists; |
336 val (_, lthy19) = Local_Theory.note ((Binding.name (q_name ^ "_distinct"), []), q_dis) lthy18; |
336 val (_, lthy19) = Local_Theory.note ((Binding.name (q_name ^ "_distinct"), []), q_dis) lthy18; |