469 val qconstrs = map #qconst qconstrs_info |
469 val qconstrs = map #qconst qconstrs_info |
470 val qbns = map #qconst qbns_info |
470 val qbns = map #qconst qbns_info |
471 val qfvs = map #qconst qfvs_info |
471 val qfvs = map #qconst qfvs_info |
472 val qfv_bns = map #qconst qfv_bns_info |
472 val qfv_bns = map #qconst qfv_bns_info |
473 val qalpha_bns = map #qconst qalpha_bns_info |
473 val qalpha_bns = map #qconst qalpha_bns_info |
|
474 |
|
475 (* lifting of the theorems *) |
|
476 val _ = warning "Lifting of Theorems" |
|
477 |
|
478 val eq_iff_simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel.simps |
|
479 prod.cases} |
|
480 |
|
481 val ((((((qdistincts, qeq_iffs), qfv_defs), qbn_defs), qperm_simps), qfv_qbn_eqvts), lthyA) = |
|
482 if get_STEPS lthy > 20 |
|
483 then |
|
484 lthy9a |
|
485 |> lift_thms qtys [] alpha_distincts |
|
486 ||>> lift_thms qtys eq_iff_simps alpha_eq_iff |
|
487 ||>> lift_thms qtys [] raw_fv_defs |
|
488 ||>> lift_thms qtys [] raw_bn_defs |
|
489 ||>> lift_thms qtys [] raw_perm_simps |
|
490 ||>> lift_thms qtys [] (raw_fv_eqvt @ raw_bn_eqvt) |
|
491 else raise TEST lthy9a |
|
492 |
|
493 val (((qsize_eqvt, [qinduct]), qexhausts), lthyB) = |
|
494 if get_STEPS lthy > 20 |
|
495 then |
|
496 lthyA |
|
497 |> lift_thms qtys [] raw_size_eqvt |
|
498 ||>> lift_thms qtys [] [raw_induct_thm] |
|
499 ||>> lift_thms qtys [] raw_exhaust_thms |
|
500 else raise TEST lthyA |
|
501 |
474 |
502 |
475 (* temporary theorem bindings *) |
503 (* temporary theorem bindings *) |
476 val (_, lthy9') = lthy9a |
504 val (_, lthy9') = lthyB |
477 |> Local_Theory.note ((@{binding "distinct"}, []), alpha_distincts) |
505 |> Local_Theory.note ((@{binding "distinct"}, []), qdistincts) |
478 ||>> Local_Theory.note ((@{binding "eq_iff"}, []), alpha_eq_iff) |
506 ||>> Local_Theory.note ((@{binding "eq_iff"}, []), qeq_iffs) |
479 ||>> Local_Theory.note ((@{binding "eq_iff_simps"}, []), alpha_eq_iff_simps) |
507 ||>> Local_Theory.note ((@{binding "fv_defs"}, []), qfv_defs) |
480 ||>> Local_Theory.note ((@{binding "fv_defs"}, []), raw_fv_defs) |
508 ||>> Local_Theory.note ((@{binding "bn_defs"}, []), qbn_defs) |
481 ||>> Local_Theory.note ((@{binding "bn_defs"}, []), raw_bn_defs) |
509 ||>> Local_Theory.note ((@{binding "perm_simps"}, []), qperm_simps) |
482 ||>> Local_Theory.note ((@{binding "perm_simps"}, []), raw_perm_simps) |
510 ||>> Local_Theory.note ((@{binding "fv_bn_eqvt"}, []), qfv_qbn_eqvts) |
483 ||>> Local_Theory.note ((@{binding "perm_laws"}, []), raw_perm_laws) |
511 ||>> Local_Theory.note ((@{binding "size_eqvt"}, []), qsize_eqvt) |
484 ||>> Local_Theory.note ((@{binding "alpha_bn_imps"}, []), alpha_bn_imp_thms) |
512 ||>> Local_Theory.note ((@{binding "induct"}, []), [qinduct]) |
485 ||>> Local_Theory.note ((@{binding "alpha_equivp"}, []), alpha_equivp_thms) |
513 ||>> Local_Theory.note ((@{binding "exhaust"}, []), qexhausts) |
486 ||>> Local_Theory.note ((@{binding "fv_eqvt"}, []), raw_fv_eqvt) |
514 |
487 ||>> Local_Theory.note ((@{binding "bn_eqvt"}, []), raw_bn_eqvt) |
|
488 ||>> Local_Theory.note ((@{binding "size_eqvt"}, []), raw_size_eqvt) |
|
489 |
515 |
490 val _ = |
516 val _ = |
491 if get_STEPS lthy > 20 |
517 if get_STEPS lthy > 21 |
492 then true else raise TEST lthy9' |
518 then true else raise TEST lthy9' |
493 |
519 |
494 (* old stuff *) |
520 (* old stuff *) |
495 |
521 |
496 val thy = ProofContext.theory_of lthy9' |
522 val thy = ProofContext.theory_of lthy9' |
551 |
577 |
552 val q_name = space_implode "_" qty_names; |
578 val q_name = space_implode "_" qty_names; |
553 fun suffix_bind s = Binding.qualify true q_name (Binding.name s); |
579 fun suffix_bind s = Binding.qualify true q_name (Binding.name s); |
554 val _ = warning "Lifting induction"; |
580 val _ = warning "Lifting induction"; |
555 val constr_names = map (Long_Name.base_name o fst o dest_Const) []; |
581 val constr_names = map (Long_Name.base_name o fst o dest_Const) []; |
556 val q_induct = Rule_Cases.name constr_names (lift_thm lthy13 qtys [] raw_induct_thm); |
582 val q_induct = Rule_Cases.name constr_names (the_single (fst (lift_thms qtys [] [raw_induct_thm] lthy13))); |
557 fun note_suffix s th ctxt = |
583 fun note_suffix s th ctxt = |
558 snd (Local_Theory.note ((suffix_bind s, []), th) ctxt); |
584 snd (Local_Theory.note ((suffix_bind s, []), th) ctxt); |
559 fun note_simp_suffix s th ctxt = |
585 fun note_simp_suffix s th ctxt = |
560 snd (Local_Theory.note ((suffix_bind s, [Attrib.internal (K Simplifier.simp_add)]), th) ctxt); |
586 snd (Local_Theory.note ((suffix_bind s, [Attrib.internal (K Simplifier.simp_add)]), th) ctxt); |
561 val (_, lthy14) = Local_Theory.note ((suffix_bind "induct", |
587 val (_, lthy14) = Local_Theory.note ((suffix_bind "induct", |
562 [Attrib.internal (K (Rule_Cases.case_names constr_names))]), |
588 [Attrib.internal (K (Rule_Cases.case_names constr_names))]), |
563 [Rule_Cases.name constr_names q_induct]) lthy13; |
589 [Rule_Cases.name constr_names q_induct]) lthy13; |
564 val q_inducts = Project_Rule.projects lthy13 (1 upto (length raw_fvs)) q_induct |
590 val q_inducts = Project_Rule.projects lthy13 (1 upto (length raw_fvs)) q_induct |
565 val (_, lthy14a) = Local_Theory.note ((suffix_bind "inducts", []), q_inducts) lthy14; |
591 val (_, lthy14a) = Local_Theory.note ((suffix_bind "inducts", []), q_inducts) lthy14; |
566 val q_perm = map (lift_thm lthy14 qtys []) raw_perm_simps; |
592 val q_perm = fst (lift_thms qtys [] raw_perm_simps lthy14); |
567 val lthy15 = note_simp_suffix "perm" q_perm lthy14a; |
593 val lthy15 = note_simp_suffix "perm" q_perm lthy14a; |
568 val q_fv = map (lift_thm lthy15 qtys []) raw_fv_defs; |
594 val q_fv = fst (lift_thms qtys [] raw_fv_defs lthy15); |
569 val lthy16 = note_simp_suffix "fv" q_fv lthy15; |
595 val lthy16 = note_simp_suffix "fv" q_fv lthy15; |
570 val q_bn = map (lift_thm lthy16 qtys []) raw_bn_defs; |
596 val q_bn = fst (lift_thms qtys [] raw_bn_defs lthy16); |
571 val lthy17 = note_simp_suffix "bn" q_bn lthy16; |
597 val lthy17 = note_simp_suffix "bn" q_bn lthy16; |
572 val _ = warning "Lifting eq-iff"; |
598 val _ = warning "Lifting eq-iff"; |
573 (*val _ = map tracing (map PolyML.makestring alpha_eq_iff);*) |
599 (*val _ = map tracing (map PolyML.makestring alpha_eq_iff);*) |
574 val eq_iff_unfolded0 = map (Local_Defs.unfold lthy17 @{thms alphas}) alpha_eq_iff |
600 val eq_iff_unfolded0 = map (Local_Defs.unfold lthy17 @{thms alphas}) alpha_eq_iff |
575 val eq_iff_unfolded1 = map (Local_Defs.unfold lthy17 @{thms Pair_eqvt}) eq_iff_unfolded0 |
601 val eq_iff_unfolded1 = map (Local_Defs.unfold lthy17 @{thms Pair_eqvt}) eq_iff_unfolded0 |
576 val q_eq_iff_pre0 = map (lift_thm lthy17 qtys []) eq_iff_unfolded1; |
602 val q_eq_iff_pre0 = fst (lift_thms qtys [] eq_iff_unfolded1 lthy17); |
577 val q_eq_iff_pre1 = map (Local_Defs.fold lthy17 @{thms Pair_eqvt}) q_eq_iff_pre0 |
603 val q_eq_iff_pre1 = map (Local_Defs.fold lthy17 @{thms Pair_eqvt}) q_eq_iff_pre0 |
578 val q_eq_iff_pre2 = map (Local_Defs.fold lthy17 @{thms alphas}) q_eq_iff_pre1 |
604 val q_eq_iff_pre2 = map (Local_Defs.fold lthy17 @{thms alphas}) q_eq_iff_pre1 |
579 val q_eq_iff = map (Local_Defs.unfold lthy17 (Quotient_Info.id_simps_get lthy17)) q_eq_iff_pre2 |
605 val q_eq_iff = map (Local_Defs.unfold lthy17 (Quotient_Info.id_simps_get lthy17)) q_eq_iff_pre2 |
580 val (_, lthy18) = Local_Theory.note ((suffix_bind "eq_iff", []), q_eq_iff) lthy17; |
606 val (_, lthy18) = Local_Theory.note ((suffix_bind "eq_iff", []), q_eq_iff) lthy17; |
581 val q_dis = map (lift_thm lthy18 qtys []) alpha_distincts; |
607 val q_dis = fst (lift_thms qtys [] alpha_distincts lthy18); |
582 val lthy19 = note_simp_suffix "distinct" q_dis lthy18; |
608 val lthy19 = note_simp_suffix "distinct" q_dis lthy18; |
583 val q_eqvt = map (lift_thm lthy19 qtys []) (raw_bn_eqvt @ raw_fv_eqvt); |
609 val q_eqvt = fst (lift_thms qtys [] (raw_bn_eqvt @ raw_fv_eqvt) lthy19); |
584 val (_, lthy20) = Local_Theory.note ((Binding.empty, |
610 val (_, lthy20) = Local_Theory.note ((Binding.empty, |
585 [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19; |
611 [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19; |
586 val _ = warning "Supports"; |
612 val _ = warning "Supports"; |
587 val supports = map (prove_supports lthy20 q_perm) []; |
613 val supports = map (prove_supports lthy20 q_perm) []; |
588 val fin_supp = HOLogic.conj_elims (prove_fs lthy20 q_induct supports qtys); |
614 val fin_supp = HOLogic.conj_elims (prove_fs lthy20 q_induct supports qtys); |