660 qed "eq_Abs_pnat"; |
660 qed "eq_Abs_pnat"; |
661 |
661 |
662 (** embedding of naturals in positive naturals **) |
662 (** embedding of naturals in positive naturals **) |
663 |
663 |
664 (* pnat_one_eq! *) |
664 (* pnat_one_eq! *) |
665 Goalw [pnat_nat_def,pnat_one_def]"1p = *#0"; |
665 Goalw [pnat_of_nat_def,pnat_one_def]"1p = pnat_of_nat 0"; |
666 by (Full_simp_tac 1); |
666 by (Full_simp_tac 1); |
667 qed "pnat_one_iff"; |
667 qed "pnat_one_iff"; |
668 |
668 |
669 Goalw [pnat_nat_def,pnat_one_def,pnat_add_def] "1p + 1p = *#1"; |
669 Goalw [pnat_of_nat_def,pnat_one_def, |
|
670 pnat_add_def] "1p + 1p = pnat_of_nat 1"; |
670 by (res_inst_tac [("f","Abs_pnat")] arg_cong 1); |
671 by (res_inst_tac [("f","Abs_pnat")] arg_cong 1); |
671 by (auto_tac (claset() addIs [(gt_0_mem_pnat RS Abs_pnat_inverse RS ssubst)], |
672 by (auto_tac (claset() addIs [(gt_0_mem_pnat RS Abs_pnat_inverse RS ssubst)], |
672 simpset())); |
673 simpset())); |
673 qed "pnat_two_eq"; |
674 qed "pnat_two_eq"; |
674 |
675 |
675 Goal "inj(pnat_nat)"; |
676 Goal "inj(pnat_of_nat)"; |
676 by (rtac injI 1); |
677 by (rtac injI 1); |
677 by (rewtac pnat_nat_def); |
678 by (rewtac pnat_of_nat_def); |
678 by (dtac (inj_on_Abs_pnat RS inj_onD) 1); |
679 by (dtac (inj_on_Abs_pnat RS inj_onD) 1); |
679 by (auto_tac (claset() addSIs [gt_0_mem_pnat],simpset())); |
680 by (auto_tac (claset() addSIs [gt_0_mem_pnat],simpset())); |
680 qed "inj_pnat_nat"; |
681 qed "inj_pnat_of_nat"; |
681 |
682 |
682 Goal "0 < n + 1"; |
683 Goal "0 < n + 1"; |
683 by Auto_tac; |
684 by Auto_tac; |
684 qed "nat_add_one_less"; |
685 qed "nat_add_one_less"; |
685 |
686 |
686 Goal "0 < n1 + n2 + 1"; |
687 Goal "0 < n1 + n2 + 1"; |
687 by Auto_tac; |
688 by Auto_tac; |
688 qed "nat_add_one_less1"; |
689 qed "nat_add_one_less1"; |
689 |
690 |
690 (* this worked with one call to auto_tac before! *) |
691 (* this worked with one call to auto_tac before! *) |
691 Goalw [pnat_add_def,pnat_nat_def,pnat_one_def] |
692 Goalw [pnat_add_def,pnat_of_nat_def,pnat_one_def] |
692 "*#n1 + *#n2 = *#(n1 + n2) + 1p"; |
693 "pnat_of_nat n1 + pnat_of_nat n2 = \ |
|
694 \ pnat_of_nat (n1 + n2) + 1p"; |
693 by (res_inst_tac [("f","Abs_pnat")] arg_cong 1); |
695 by (res_inst_tac [("f","Abs_pnat")] arg_cong 1); |
694 by (rtac (gt_0_mem_pnat RS Abs_pnat_inverse RS ssubst) 1); |
696 by (rtac (gt_0_mem_pnat RS Abs_pnat_inverse RS ssubst) 1); |
695 by (rtac (gt_0_mem_pnat RS Abs_pnat_inverse RS ssubst) 2); |
697 by (rtac (gt_0_mem_pnat RS Abs_pnat_inverse RS ssubst) 2); |
696 by (rtac (gt_0_mem_pnat RS Abs_pnat_inverse RS ssubst) 3); |
698 by (rtac (gt_0_mem_pnat RS Abs_pnat_inverse RS ssubst) 3); |
697 by (rtac (gt_0_mem_pnat RS Abs_pnat_inverse RS ssubst) 4); |
699 by (rtac (gt_0_mem_pnat RS Abs_pnat_inverse RS ssubst) 4); |
698 by (auto_tac (claset(), |
700 by (auto_tac (claset(), |
699 simpset() addsimps [sum_Rep_pnat_sum, |
701 simpset() addsimps [sum_Rep_pnat_sum, |
700 nat_add_one_less,nat_add_one_less1])); |
702 nat_add_one_less,nat_add_one_less1])); |
701 qed "pnat_nat_add"; |
703 qed "pnat_of_nat_add"; |
702 |
704 |
703 Goalw [pnat_nat_def,pnat_less_def] "(n < m) = (*#n < *#m)"; |
705 Goalw [pnat_of_nat_def,pnat_less_def] |
|
706 "(n < m) = (pnat_of_nat n < pnat_of_nat m)"; |
704 by (auto_tac (claset(),simpset() |
707 by (auto_tac (claset(),simpset() |
705 addsimps [Abs_pnat_inverse,Collect_pnat_gt_0])); |
708 addsimps [Abs_pnat_inverse,Collect_pnat_gt_0])); |
706 qed "pnat_nat_less_iff"; |
709 qed "pnat_of_nat_less_iff"; |
707 |
710 Addsimps [pnat_of_nat_less_iff RS sym]; |
708 Addsimps [pnat_nat_less_iff RS sym]; |
711 |
709 |
|