396 val thy' = define_lifted_perms qty_full_names (perm_names ~~ perms) raw_perm_simps thy; |
396 val thy' = define_lifted_perms qty_full_names (perm_names ~~ perms) raw_perm_simps thy; |
397 val lthy13 = Theory_Target.init NONE thy'; |
397 val lthy13 = Theory_Target.init NONE thy'; |
398 val q_name = space_implode "_" qty_names; |
398 val q_name = space_implode "_" qty_names; |
399 val q_induct = lift_thm lthy13 induct; |
399 val q_induct = lift_thm lthy13 induct; |
400 val (_, lthy14) = Local_Theory.note ((Binding.name (q_name ^ "_induct"), []), [q_induct]) lthy13; |
400 val (_, lthy14) = Local_Theory.note ((Binding.name (q_name ^ "_induct"), []), [q_induct]) lthy13; |
|
401 val q_inducts = Project_Rule.projects lthy13 (1 upto (length alpha_inducts)) q_induct |
|
402 val (_, lthy14a) = Local_Theory.note ((Binding.name (q_name ^ "_inducts"), []), q_inducts) lthy14; |
401 val q_perm = map (lift_thm lthy14) raw_perm_def; |
403 val q_perm = map (lift_thm lthy14) raw_perm_def; |
402 val (_, lthy15) = Local_Theory.note ((Binding.name (q_name ^ "_perm"), []), q_perm) lthy14; |
404 val (_, lthy15) = Local_Theory.note ((Binding.name (q_name ^ "_perm"), []), q_perm) lthy14a; |
403 val q_fv = map (lift_thm lthy15) fv_def; |
405 val q_fv = map (lift_thm lthy15) fv_def; |
404 val (_, lthy16) = Local_Theory.note ((Binding.name (q_name ^ "_fv"), []), q_fv) lthy15; |
406 val (_, lthy16) = Local_Theory.note ((Binding.name (q_name ^ "_fv"), []), q_fv) lthy15; |
405 val q_bn = map (lift_thm lthy16) raw_bn_eqs; |
407 val q_bn = map (lift_thm lthy16) raw_bn_eqs; |
406 val (_, lthy17) = Local_Theory.note ((Binding.name (q_name ^ "_bn"), []), q_bn) lthy16; |
408 val (_, lthy17) = Local_Theory.note ((Binding.name (q_name ^ "_bn"), []), q_bn) lthy16; |
407 val inj_unfolded = map (Local_Defs.unfold lthy17 @{thms alpha_gen}) alpha_inj |
409 val inj_unfolded = map (Local_Defs.unfold lthy17 @{thms alpha_gen}) alpha_inj |