564 |
564 |
565 val q_name = space_implode "_" qty_names; |
565 val q_name = space_implode "_" qty_names; |
566 fun suffix_bind s = Binding.qualify true q_name (Binding.name s); |
566 fun suffix_bind s = Binding.qualify true q_name (Binding.name s); |
567 val _ = warning "Lifting induction"; |
567 val _ = warning "Lifting induction"; |
568 val constr_names = map (Long_Name.base_name o fst o dest_Const) qconstrs; |
568 val constr_names = map (Long_Name.base_name o fst o dest_Const) qconstrs; |
569 val q_induct = Rule_Cases.name constr_names (lift_thm qtys lthy13 raw_induct_thm); |
569 val q_induct = Rule_Cases.name constr_names (lift_thm lthy13 qtys raw_induct_thm); |
570 fun note_suffix s th ctxt = |
570 fun note_suffix s th ctxt = |
571 snd (Local_Theory.note ((suffix_bind s, []), th) ctxt); |
571 snd (Local_Theory.note ((suffix_bind s, []), th) ctxt); |
572 fun note_simp_suffix s th ctxt = |
572 fun note_simp_suffix s th ctxt = |
573 snd (Local_Theory.note ((suffix_bind s, [Attrib.internal (K Simplifier.simp_add)]), th) ctxt); |
573 snd (Local_Theory.note ((suffix_bind s, [Attrib.internal (K Simplifier.simp_add)]), th) ctxt); |
574 val (_, lthy14) = Local_Theory.note ((suffix_bind "induct", |
574 val (_, lthy14) = Local_Theory.note ((suffix_bind "induct", |
575 [Attrib.internal (K (Rule_Cases.case_names constr_names))]), |
575 [Attrib.internal (K (Rule_Cases.case_names constr_names))]), |
576 [Rule_Cases.name constr_names q_induct]) lthy13; |
576 [Rule_Cases.name constr_names q_induct]) lthy13; |
577 val q_inducts = Project_Rule.projects lthy13 (1 upto (length raw_fvs)) q_induct |
577 val q_inducts = Project_Rule.projects lthy13 (1 upto (length raw_fvs)) q_induct |
578 val (_, lthy14a) = Local_Theory.note ((suffix_bind "inducts", []), q_inducts) lthy14; |
578 val (_, lthy14a) = Local_Theory.note ((suffix_bind "inducts", []), q_inducts) lthy14; |
579 val q_perm = map (lift_thm qtys lthy14) raw_perm_simps; |
579 val q_perm = map (lift_thm lthy14 qtys) raw_perm_simps; |
580 val lthy15 = note_simp_suffix "perm" q_perm lthy14a; |
580 val lthy15 = note_simp_suffix "perm" q_perm lthy14a; |
581 val q_fv = map (lift_thm qtys lthy15) raw_fv_defs; |
581 val q_fv = map (lift_thm lthy15 qtys) raw_fv_defs; |
582 val lthy16 = note_simp_suffix "fv" q_fv lthy15; |
582 val lthy16 = note_simp_suffix "fv" q_fv lthy15; |
583 val q_bn = map (lift_thm qtys lthy16) raw_bn_defs; |
583 val q_bn = map (lift_thm lthy16 qtys) raw_bn_defs; |
584 val lthy17 = note_simp_suffix "bn" q_bn lthy16; |
584 val lthy17 = note_simp_suffix "bn" q_bn lthy16; |
585 val _ = warning "Lifting eq-iff"; |
585 val _ = warning "Lifting eq-iff"; |
586 (*val _ = map tracing (map PolyML.makestring alpha_eq_iff);*) |
586 (*val _ = map tracing (map PolyML.makestring alpha_eq_iff);*) |
587 val eq_iff_unfolded0 = map (Local_Defs.unfold lthy17 @{thms alphas}) alpha_eq_iff |
587 val eq_iff_unfolded0 = map (Local_Defs.unfold lthy17 @{thms alphas}) alpha_eq_iff |
588 val eq_iff_unfolded1 = map (Local_Defs.unfold lthy17 @{thms Pair_eqvt}) eq_iff_unfolded0 |
588 val eq_iff_unfolded1 = map (Local_Defs.unfold lthy17 @{thms Pair_eqvt}) eq_iff_unfolded0 |
589 val q_eq_iff_pre0 = map (lift_thm qtys lthy17) eq_iff_unfolded1; |
589 val q_eq_iff_pre0 = map (lift_thm lthy17 qtys) eq_iff_unfolded1; |
590 val q_eq_iff_pre1 = map (Local_Defs.fold lthy17 @{thms Pair_eqvt}) q_eq_iff_pre0 |
590 val q_eq_iff_pre1 = map (Local_Defs.fold lthy17 @{thms Pair_eqvt}) q_eq_iff_pre0 |
591 val q_eq_iff_pre2 = map (Local_Defs.fold lthy17 @{thms alphas}) q_eq_iff_pre1 |
591 val q_eq_iff_pre2 = map (Local_Defs.fold lthy17 @{thms alphas}) q_eq_iff_pre1 |
592 val q_eq_iff = map (Local_Defs.unfold lthy17 (Quotient_Info.id_simps_get lthy17)) q_eq_iff_pre2 |
592 val q_eq_iff = map (Local_Defs.unfold lthy17 (Quotient_Info.id_simps_get lthy17)) q_eq_iff_pre2 |
593 val (_, lthy18) = Local_Theory.note ((suffix_bind "eq_iff", []), q_eq_iff) lthy17; |
593 val (_, lthy18) = Local_Theory.note ((suffix_bind "eq_iff", []), q_eq_iff) lthy17; |
594 val q_dis = map (lift_thm qtys lthy18) alpha_distincts; |
594 val q_dis = map (lift_thm lthy18 qtys) alpha_distincts; |
595 val lthy19 = note_simp_suffix "distinct" q_dis lthy18; |
595 val lthy19 = note_simp_suffix "distinct" q_dis lthy18; |
596 val q_eqvt = map (lift_thm qtys lthy19) (raw_bn_eqvt @ raw_fv_eqvt); |
596 val q_eqvt = map (lift_thm lthy19 qtys) (raw_bn_eqvt @ raw_fv_eqvt); |
597 val (_, lthy20) = Local_Theory.note ((Binding.empty, |
597 val (_, lthy20) = Local_Theory.note ((Binding.empty, |
598 [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19; |
598 [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19; |
599 val _ = warning "Supports"; |
599 val _ = warning "Supports"; |
600 val supports = map (prove_supports lthy20 q_perm) qconstrs; |
600 val supports = map (prove_supports lthy20 q_perm) qconstrs; |
601 val fin_supp = HOLogic.conj_elims (prove_fs lthy20 q_induct supports qtys); |
601 val fin_supp = HOLogic.conj_elims (prove_fs lthy20 q_induct supports qtys); |