501 let |
501 let |
502 val qu_name = Sign.full_bname thy' ak_name'; |
502 val qu_name = Sign.full_bname thy' ak_name'; |
503 val cls_name = Sign.full_bname thy' ("pt_"^ak_name); |
503 val cls_name = Sign.full_bname thy' ("pt_"^ak_name); |
504 val at_inst = Global_Theory.get_thm thy' ("at_" ^ ak_name' ^ "_inst"); |
504 val at_inst = Global_Theory.get_thm thy' ("at_" ^ ak_name' ^ "_inst"); |
505 |
505 |
506 val proof1 = EVERY [Class.intro_classes_tac [], |
506 fun proof1 ctxt = EVERY [Class.intro_classes_tac ctxt [], |
507 rtac ((at_inst RS at_pt_inst) RS pt1) 1, |
507 rtac ((at_inst RS at_pt_inst) RS pt1) 1, |
508 rtac ((at_inst RS at_pt_inst) RS pt2) 1, |
508 rtac ((at_inst RS at_pt_inst) RS pt2) 1, |
509 rtac ((at_inst RS at_pt_inst) RS pt3) 1, |
509 rtac ((at_inst RS at_pt_inst) RS pt3) 1, |
510 atac 1]; |
510 atac 1]; |
511 fun proof2 ctxt = |
511 fun proof2 ctxt = |
512 Class.intro_classes_tac [] THEN |
512 Class.intro_classes_tac ctxt [] THEN |
513 REPEAT (asm_simp_tac |
513 REPEAT (asm_simp_tac |
514 (put_simpset HOL_basic_ss ctxt addsimps |
514 (put_simpset HOL_basic_ss ctxt addsimps |
515 maps (Global_Theory.get_thms thy') [ak_name ^ "_prm_" ^ ak_name' ^ "_def"]) 1); |
515 maps (Global_Theory.get_thms thy') [ak_name ^ "_prm_" ^ ak_name' ^ "_def"]) 1); |
516 in |
516 in |
517 thy' |
517 thy' |
518 |> Axclass.prove_arity (qu_name,[],[cls_name]) |
518 |> Axclass.prove_arity (qu_name,[],[cls_name]) |
519 (fn ctxt => if ak_name = ak_name' then proof1 else proof2 ctxt) |
519 (fn ctxt => if ak_name = ak_name' then proof1 ctxt else proof2 ctxt) |
520 end) ak_names thy) ak_names thy12d; |
520 end) ak_names thy) ak_names thy12d; |
521 |
521 |
522 (* show that *) |
522 (* show that *) |
523 (* fun(pt_<ak>,pt_<ak>) *) |
523 (* fun(pt_<ak>,pt_<ak>) *) |
524 (* noption(pt_<ak>) *) |
524 (* noption(pt_<ak>) *) |
534 val cls_name = Sign.full_bname thy ("pt_"^ak_name); |
534 val cls_name = Sign.full_bname thy ("pt_"^ak_name); |
535 val at_thm = Global_Theory.get_thm thy ("at_"^ak_name^"_inst"); |
535 val at_thm = Global_Theory.get_thm thy ("at_"^ak_name^"_inst"); |
536 val pt_inst = Global_Theory.get_thm thy ("pt_"^ak_name^"_inst"); |
536 val pt_inst = Global_Theory.get_thm thy ("pt_"^ak_name^"_inst"); |
537 |
537 |
538 fun pt_proof thm ctxt = |
538 fun pt_proof thm ctxt = |
539 EVERY [Class.intro_classes_tac [], |
539 EVERY [Class.intro_classes_tac ctxt [], |
540 rtac (thm RS pt1) 1, rtac (thm RS pt2) 1, rtac (thm RS pt3) 1, atac 1]; |
540 rtac (thm RS pt1) 1, rtac (thm RS pt2) 1, rtac (thm RS pt3) 1, atac 1]; |
541 |
541 |
542 val pt_thm_fun = at_thm RS (pt_inst RS (pt_inst RS pt_fun_inst)); |
542 val pt_thm_fun = at_thm RS (pt_inst RS (pt_inst RS pt_fun_inst)); |
543 val pt_thm_set = pt_inst RS pt_set_inst; |
543 val pt_thm_set = pt_inst RS pt_set_inst; |
544 val pt_thm_noptn = pt_inst RS pt_noptn_inst; |
544 val pt_thm_noptn = pt_inst RS pt_noptn_inst; |
580 val qu_class = Sign.full_bname thy' ("fs_"^ak_name); |
580 val qu_class = Sign.full_bname thy' ("fs_"^ak_name); |
581 fun proof ctxt = |
581 fun proof ctxt = |
582 (if ak_name = ak_name' |
582 (if ak_name = ak_name' |
583 then |
583 then |
584 let val at_thm = Global_Theory.get_thm thy' ("at_"^ak_name^"_inst"); |
584 let val at_thm = Global_Theory.get_thm thy' ("at_"^ak_name^"_inst"); |
585 in EVERY [Class.intro_classes_tac [], |
585 in EVERY [Class.intro_classes_tac ctxt [], |
586 rtac ((at_thm RS fs_at_inst) RS fs1) 1] end |
586 rtac ((at_thm RS fs_at_inst) RS fs1) 1] end |
587 else |
587 else |
588 let val dj_inst = Global_Theory.get_thm thy' ("dj_"^ak_name'^"_"^ak_name); |
588 let val dj_inst = Global_Theory.get_thm thy' ("dj_"^ak_name'^"_"^ak_name); |
589 val simp_s = |
589 val simp_s = |
590 put_simpset HOL_basic_ss ctxt addsimps [dj_inst RS dj_supp, finite_emptyI]; |
590 put_simpset HOL_basic_ss ctxt addsimps [dj_inst RS dj_supp, finite_emptyI]; |
591 in EVERY [Class.intro_classes_tac [], asm_simp_tac simp_s 1] end) |
591 in EVERY [Class.intro_classes_tac ctxt [], asm_simp_tac simp_s 1] end) |
592 in |
592 in |
593 Axclass.prove_arity (qu_name,[],[qu_class]) proof thy' |
593 Axclass.prove_arity (qu_name,[],[qu_class]) proof thy' |
594 end) ak_names thy) ak_names thy18; |
594 end) ak_names thy) ak_names thy18; |
595 |
595 |
596 (* shows that *) |
596 (* shows that *) |
603 |
603 |
604 val thy24 = fold (fn ak_name => fn thy => |
604 val thy24 = fold (fn ak_name => fn thy => |
605 let |
605 let |
606 val cls_name = Sign.full_bname thy ("fs_"^ak_name); |
606 val cls_name = Sign.full_bname thy ("fs_"^ak_name); |
607 val fs_inst = Global_Theory.get_thm thy ("fs_"^ak_name^"_inst"); |
607 val fs_inst = Global_Theory.get_thm thy ("fs_"^ak_name^"_inst"); |
608 fun fs_proof thm ctxt = EVERY [Class.intro_classes_tac [], rtac (thm RS fs1) 1]; |
608 fun fs_proof thm ctxt = EVERY [Class.intro_classes_tac ctxt [], rtac (thm RS fs1) 1]; |
609 |
609 |
610 val fs_thm_unit = fs_unit_inst; |
610 val fs_thm_unit = fs_unit_inst; |
611 val fs_thm_prod = fs_inst RS (fs_inst RS fs_prod_inst); |
611 val fs_thm_prod = fs_inst RS (fs_inst RS fs_prod_inst); |
612 val fs_thm_nprod = fs_inst RS (fs_inst RS fs_nprod_inst); |
612 val fs_thm_nprod = fs_inst RS (fs_inst RS fs_nprod_inst); |
613 val fs_thm_list = fs_inst RS fs_list_inst; |
613 val fs_thm_list = fs_inst RS fs_list_inst; |
649 (if (ak_name'=ak_name'') then |
649 (if (ak_name'=ak_name'') then |
650 (let |
650 (let |
651 val pt_inst = Global_Theory.get_thm thy'' ("pt_"^ak_name''^"_inst"); |
651 val pt_inst = Global_Theory.get_thm thy'' ("pt_"^ak_name''^"_inst"); |
652 val at_inst = Global_Theory.get_thm thy'' ("at_"^ak_name''^"_inst"); |
652 val at_inst = Global_Theory.get_thm thy'' ("at_"^ak_name''^"_inst"); |
653 in |
653 in |
654 EVERY [Class.intro_classes_tac [], |
654 EVERY [Class.intro_classes_tac ctxt [], |
655 rtac (at_inst RS (pt_inst RS pt_perm_compose)) 1] |
655 rtac (at_inst RS (pt_inst RS pt_perm_compose)) 1] |
656 end) |
656 end) |
657 else |
657 else |
658 (let |
658 (let |
659 val dj_inst = Global_Theory.get_thm thy'' ("dj_"^ak_name''^"_"^ak_name'); |
659 val dj_inst = Global_Theory.get_thm thy'' ("dj_"^ak_name''^"_"^ak_name'); |
661 ((dj_inst RS dj_pp_forget):: |
661 ((dj_inst RS dj_pp_forget):: |
662 (maps (Global_Theory.get_thms thy'') |
662 (maps (Global_Theory.get_thms thy'') |
663 [ak_name' ^"_prm_"^ak_name^"_def", |
663 [ak_name' ^"_prm_"^ak_name^"_def", |
664 ak_name''^"_prm_"^ak_name^"_def"])); |
664 ak_name''^"_prm_"^ak_name^"_def"])); |
665 in |
665 in |
666 EVERY [Class.intro_classes_tac [], simp_tac simp_s 1] |
666 EVERY [Class.intro_classes_tac ctxt [], simp_tac simp_s 1] |
667 end)) |
667 end)) |
668 in |
668 in |
669 Axclass.prove_arity (name,[],[cls_name]) proof thy'' |
669 Axclass.prove_arity (name,[],[cls_name]) proof thy'' |
670 end) ak_names thy') ak_names thy) ak_names thy24; |
670 end) ak_names thy') ak_names thy) ak_names thy24; |
671 |
671 |
684 val cls_name = Sign.full_bname thy' ("cp_"^ak_name^"_"^ak_name'); |
684 val cls_name = Sign.full_bname thy' ("cp_"^ak_name^"_"^ak_name'); |
685 val cp_inst = Global_Theory.get_thm thy' ("cp_"^ak_name^"_"^ak_name'^"_inst"); |
685 val cp_inst = Global_Theory.get_thm thy' ("cp_"^ak_name^"_"^ak_name'^"_inst"); |
686 val pt_inst = Global_Theory.get_thm thy' ("pt_"^ak_name^"_inst"); |
686 val pt_inst = Global_Theory.get_thm thy' ("pt_"^ak_name^"_inst"); |
687 val at_inst = Global_Theory.get_thm thy' ("at_"^ak_name^"_inst"); |
687 val at_inst = Global_Theory.get_thm thy' ("at_"^ak_name^"_inst"); |
688 |
688 |
689 fun cp_proof thm ctxt = EVERY [Class.intro_classes_tac [],rtac (thm RS cp1) 1]; |
689 fun cp_proof thm ctxt = EVERY [Class.intro_classes_tac ctxt [], rtac (thm RS cp1) 1]; |
690 |
690 |
691 val cp_thm_unit = cp_unit_inst; |
691 val cp_thm_unit = cp_unit_inst; |
692 val cp_thm_prod = cp_inst RS (cp_inst RS cp_prod_inst); |
692 val cp_thm_prod = cp_inst RS (cp_inst RS cp_prod_inst); |
693 val cp_thm_list = cp_inst RS cp_list_inst; |
693 val cp_thm_list = cp_inst RS cp_list_inst; |
694 val cp_thm_fun = at_inst RS (pt_inst RS (cp_inst RS (cp_inst RS cp_fun_inst))); |
694 val cp_thm_fun = at_inst RS (pt_inst RS (cp_inst RS (cp_inst RS cp_fun_inst))); |
715 fun discrete_pt_inst discrete_ty defn = |
715 fun discrete_pt_inst discrete_ty defn = |
716 fold (fn ak_name => fn thy => |
716 fold (fn ak_name => fn thy => |
717 let |
717 let |
718 val qu_class = Sign.full_bname thy ("pt_"^ak_name); |
718 val qu_class = Sign.full_bname thy ("pt_"^ak_name); |
719 fun proof ctxt = |
719 fun proof ctxt = |
720 Class.intro_classes_tac [] THEN |
720 Class.intro_classes_tac ctxt [] THEN |
721 REPEAT (asm_simp_tac (put_simpset HOL_basic_ss ctxt addsimps [Simpdata.mk_eq defn]) 1); |
721 REPEAT (asm_simp_tac (put_simpset HOL_basic_ss ctxt addsimps [Simpdata.mk_eq defn]) 1); |
722 in |
722 in |
723 Axclass.prove_arity (discrete_ty, [], [qu_class]) proof thy |
723 Axclass.prove_arity (discrete_ty, [], [qu_class]) proof thy |
724 end) ak_names; |
724 end) ak_names; |
725 |
725 |
727 fold (fn ak_name => fn thy => |
727 fold (fn ak_name => fn thy => |
728 let |
728 let |
729 val qu_class = Sign.full_bname thy ("fs_"^ak_name); |
729 val qu_class = Sign.full_bname thy ("fs_"^ak_name); |
730 val supp_def = Simpdata.mk_eq @{thm "Nominal.supp_def"}; |
730 val supp_def = Simpdata.mk_eq @{thm "Nominal.supp_def"}; |
731 fun proof ctxt = |
731 fun proof ctxt = |
732 Class.intro_classes_tac [] THEN |
732 Class.intro_classes_tac ctxt [] THEN |
733 asm_simp_tac (put_simpset HOL_ss ctxt |
733 asm_simp_tac (put_simpset HOL_ss ctxt |
734 addsimps [supp_def, Collect_const, finite_emptyI, Simpdata.mk_eq defn]) 1; |
734 addsimps [supp_def, Collect_const, finite_emptyI, Simpdata.mk_eq defn]) 1; |
735 in |
735 in |
736 Axclass.prove_arity (discrete_ty, [], [qu_class]) proof thy |
736 Axclass.prove_arity (discrete_ty, [], [qu_class]) proof thy |
737 end) ak_names; |
737 end) ak_names; |
740 fold (fn ak_name' => (fold (fn ak_name => fn thy => |
740 fold (fn ak_name' => (fold (fn ak_name => fn thy => |
741 let |
741 let |
742 val qu_class = Sign.full_bname thy ("cp_"^ak_name^"_"^ak_name'); |
742 val qu_class = Sign.full_bname thy ("cp_"^ak_name^"_"^ak_name'); |
743 val supp_def = Simpdata.mk_eq @{thm "Nominal.supp_def"}; |
743 val supp_def = Simpdata.mk_eq @{thm "Nominal.supp_def"}; |
744 fun proof ctxt = |
744 fun proof ctxt = |
745 Class.intro_classes_tac [] THEN |
745 Class.intro_classes_tac ctxt [] THEN |
746 asm_simp_tac (put_simpset HOL_ss ctxt addsimps [Simpdata.mk_eq defn]) 1; |
746 asm_simp_tac (put_simpset HOL_ss ctxt addsimps [Simpdata.mk_eq defn]) 1; |
747 in |
747 in |
748 Axclass.prove_arity (discrete_ty, [], [qu_class]) proof thy |
748 Axclass.prove_arity (discrete_ty, [], [qu_class]) proof thy |
749 end) ak_names)) ak_names; |
749 end) ak_names)) ak_names; |
750 |
750 |