789 by (simp only: nat_number_of_def) |
789 by (simp only: nat_number_of_def) |
790 |
790 |
791 lemma of_nat_number_of_lemma: |
791 lemma of_nat_number_of_lemma: |
792 "of_nat (number_of v :: nat) = |
792 "of_nat (number_of v :: nat) = |
793 (if 0 \<le> (number_of v :: int) |
793 (if 0 \<le> (number_of v :: int) |
794 then (number_of v :: 'a :: number_ring) |
794 then (number_of v :: 'a :: number_semiring) |
795 else 0)" |
795 else 0)" |
796 by (simp add: int_number_of_def nat_number_of_def number_of_eq of_nat_nat) |
796 by (auto simp add: int_number_of_def nat_number_of_def number_of_int |
|
797 elim!: nonneg_int_cases) |
797 |
798 |
798 lemma of_nat_number_of_eq [simp]: |
799 lemma of_nat_number_of_eq [simp]: |
799 "of_nat (number_of v :: nat) = |
800 "of_nat (number_of v :: nat) = |
800 (if neg (number_of v :: int) then 0 |
801 (if neg (number_of v :: int) then 0 |
801 else (number_of v :: 'a :: number_ring))" |
802 else (number_of v :: 'a :: number_semiring))" |
802 by (simp only: of_nat_number_of_lemma neg_def, simp) |
803 by (simp only: of_nat_number_of_lemma neg_def, simp) |
803 |
804 |
804 |
805 |
805 subsubsection{*For simplifying @{term "Suc m - K"} and @{term "K - Suc m"}*} |
806 subsubsection{*For simplifying @{term "Suc m - K"} and @{term "K - Suc m"}*} |
806 |
807 |
807 text{*Where K above is a literal*} |
808 text{*Where K above is a literal*} |