379 val thy' = define_lifted_perms qty_full_names (perm_names ~~ perms) raw_perm_simps thy; |
379 val thy' = define_lifted_perms qty_full_names (perm_names ~~ perms) raw_perm_simps thy; |
380 val lthy13 = Theory_Target.init NONE thy'; |
380 val lthy13 = Theory_Target.init NONE thy'; |
381 val q_name = space_implode "_" qty_names; |
381 val q_name = space_implode "_" qty_names; |
382 val _ = tracing "Lifting induction"; |
382 val _ = tracing "Lifting induction"; |
383 val q_induct = lift_thm lthy13 induct; |
383 val q_induct = lift_thm lthy13 induct; |
|
384 fun note_simp_suffix s th ctxt = |
|
385 snd (Local_Theory.note ((Binding.name (q_name ^ "_" ^ s), |
|
386 [Attrib.internal (K Simplifier.simp_add)]), th) ctxt); |
384 val (_, lthy14) = Local_Theory.note ((Binding.name (q_name ^ "_induct"), []), [q_induct]) lthy13; |
387 val (_, lthy14) = Local_Theory.note ((Binding.name (q_name ^ "_induct"), []), [q_induct]) lthy13; |
385 val q_inducts = Project_Rule.projects lthy13 (1 upto (length alpha_inducts)) q_induct |
388 val q_inducts = Project_Rule.projects lthy13 (1 upto (length alpha_inducts)) q_induct |
386 val (_, lthy14a) = Local_Theory.note ((Binding.name (q_name ^ "_inducts"), []), q_inducts) lthy14; |
389 val (_, lthy14a) = Local_Theory.note ((Binding.name (q_name ^ "_inducts"), []), q_inducts) lthy14; |
387 val q_perm = map (lift_thm lthy14) raw_perm_def; |
390 val q_perm = map (lift_thm lthy14) raw_perm_def; |
388 val (_, lthy15) = Local_Theory.note ((Binding.name (q_name ^ "_perm"), []), q_perm) lthy14a; |
391 val lthy15 = note_simp_suffix "perm" q_perm lthy14a; |
389 val q_fv = map (lift_thm lthy15) fv_def; |
392 val q_fv = map (lift_thm lthy15) fv_def; |
390 val (_, lthy16) = Local_Theory.note ((Binding.name (q_name ^ "_fv"), []), q_fv) lthy15; |
393 val lthy16 = note_simp_suffix "fv" q_fv lthy15; |
391 val q_bn = map (lift_thm lthy16) raw_bn_eqs; |
394 val q_bn = map (lift_thm lthy16) raw_bn_eqs; |
392 val (_, lthy17) = Local_Theory.note ((Binding.name (q_name ^ "_bn"), []), q_bn) lthy16; |
395 val lthy17 = note_simp_suffix "bn" q_bn lthy16; |
393 val _ = tracing "Lifting eq-iff"; |
396 val _ = tracing "Lifting eq-iff"; |
394 val eq_iff_unfolded1 = map (Local_Defs.unfold lthy17 @{thms alpha_gen2}) alpha_eq_iff |
397 val eq_iff_unfolded1 = map (Local_Defs.unfold lthy17 @{thms alpha_gen2}) alpha_eq_iff |
395 val eq_iff_unfolded2 = map (Local_Defs.unfold lthy17 @{thms alpha_gen}) eq_iff_unfolded1 |
398 val eq_iff_unfolded2 = map (Local_Defs.unfold lthy17 @{thms alpha_gen}) eq_iff_unfolded1 |
396 val q_eq_iff_pre1 = map (lift_thm lthy17) eq_iff_unfolded2; |
399 val q_eq_iff_pre1 = map (lift_thm lthy17) eq_iff_unfolded2; |
397 val q_eq_iff_pre2 = map (Local_Defs.fold lthy17 @{thms alpha_gen2}) q_eq_iff_pre1 |
400 val q_eq_iff_pre2 = map (Local_Defs.fold lthy17 @{thms alpha_gen2}) q_eq_iff_pre1 |
398 val q_eq_iff = map (Local_Defs.fold lthy17 @{thms alpha_gen}) q_eq_iff_pre2 |
401 val q_eq_iff = map (Local_Defs.fold lthy17 @{thms alpha_gen}) q_eq_iff_pre2 |
399 val (_, lthy18) = Local_Theory.note ((Binding.name (q_name ^ "_eq_iff"), []), q_eq_iff) lthy17; |
402 val (_, lthy18) = Local_Theory.note ((Binding.name (q_name ^ "_eq_iff"), []), q_eq_iff) lthy17; |
400 val rel_dists = flat (map (distinct_rel lthy18 alpha_cases) |
403 val rel_dists = flat (map (distinct_rel lthy18 alpha_cases) |
401 (rel_distinct ~~ (List.take (alpha_ts, (length dts))))) |
404 (rel_distinct ~~ (List.take (alpha_ts, (length dts))))) |
402 val q_dis = map (lift_thm lthy18) rel_dists; |
405 val q_dis = map (lift_thm lthy18) rel_dists; |
403 val (_, lthy19) = Local_Theory.note ((Binding.name (q_name ^ "_distinct"), []), q_dis) lthy18; |
406 val lthy19 = note_simp_suffix "distinct" q_dis lthy18; |
404 val q_eqvt = map (lift_thm lthy19) raw_fv_bv_eqvt; |
407 val q_eqvt = map (lift_thm lthy19) raw_fv_bv_eqvt; |
405 val (_, lthy20) = Local_Theory.note ((Binding.empty, |
408 val (_, lthy20) = Local_Theory.note ((Binding.empty, |
406 [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19; |
409 [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19; |
407 val _ = tracing "Finite Support"; |
410 val _ = tracing "Finite Support"; |
408 val supports = map (prove_supports lthy20 q_perm) consts |
411 val supports = map (prove_supports lthy20 q_perm) consts |