# HG changeset patch # User huffman # Date 1308845060 25200 # Node ID cc46a678faafe9e7dff404f850651b3d4ce96b79 # Parent f05a707fdf9147f3eeb7041c7f8fe84076c86d00 added number_semiring class, plus a few new lemmas; no changes to the simpset yet diff -r f05a707fdf91 -r cc46a678faaf src/HOL/Int.thy --- a/src/HOL/Int.thy Thu Jun 23 16:31:20 2011 +0200 +++ b/src/HOL/Int.thy Thu Jun 23 09:04:20 2011 -0700 @@ -941,6 +941,15 @@ class number_ring = number + comm_ring_1 + assumes number_of_eq: "number_of k = of_int k" +class number_semiring = number + comm_semiring_1 + + assumes number_of_int: "number_of (of_nat n) = of_nat n" + +instance number_ring \ number_semiring +proof + fix n show "number_of (of_nat n) = (of_nat n :: 'a)" + unfolding number_of_eq by (rule of_int_of_nat_eq) +qed + text {* self-embedding of the integers *} instantiation int :: number_ring @@ -995,13 +1004,23 @@ Converting numerals 0 and 1 to their abstract versions. *} +lemma semiring_numeral_0_eq_0: + "Numeral0 = (0::'a::number_semiring)" + using number_of_int [where 'a='a and n=0] + unfolding numeral_simps by simp + +lemma semiring_numeral_1_eq_1: + "Numeral1 = (1::'a::number_semiring)" + using number_of_int [where 'a='a and n=1] + unfolding numeral_simps by simp + lemma numeral_0_eq_0 [simp, code_post]: "Numeral0 = (0::'a::number_ring)" - unfolding number_of_eq numeral_simps by simp + by (rule semiring_numeral_0_eq_0) lemma numeral_1_eq_1 [simp, code_post]: "Numeral1 = (1::'a::number_ring)" - unfolding number_of_eq numeral_simps by simp + by (rule semiring_numeral_1_eq_1) text {* Special-case simplification for small constants. @@ -1467,8 +1486,12 @@ lemmas add_number_of_eq = number_of_add [symmetric] text{*Allow 1 on either or both sides*} +lemma semiring_one_add_one_is_two: "1 + 1 = (2::'a::number_semiring)" + using number_of_int [where 'a='a and n="Suc (Suc 0)"] + by (simp add: numeral_simps) + lemma one_add_one_is_two: "1 + 1 = (2::'a::number_ring)" -by (simp del: numeral_1_eq_1 add: numeral_1_eq_1 [symmetric]) +by (rule semiring_one_add_one_is_two) lemmas add_special = one_add_one_is_two @@ -1555,11 +1578,18 @@ by (simp add: number_of_eq) text{*Lemmas for specialist use, NOT as default simprules*} +(* TODO: see if semiring duplication can be removed without breaking proofs *) +lemma semiring_mult_2: "2 * z = (z+z::'a::number_semiring)" +unfolding semiring_one_add_one_is_two [symmetric] left_distrib by simp + +lemma semiring_mult_2_right: "z * 2 = (z+z::'a::number_semiring)" +by (subst mult_commute, rule semiring_mult_2) + lemma mult_2: "2 * z = (z+z::'a::number_ring)" -unfolding one_add_one_is_two [symmetric] left_distrib by simp +by (rule semiring_mult_2) lemma mult_2_right: "z * 2 = (z+z::'a::number_ring)" -by (subst mult_commute, rule mult_2) +by (rule semiring_mult_2_right) subsection{*More Inequality Reasoning*} diff -r f05a707fdf91 -r cc46a678faaf src/HOL/Nat_Numeral.thy --- a/src/HOL/Nat_Numeral.thy Thu Jun 23 16:31:20 2011 +0200 +++ b/src/HOL/Nat_Numeral.thy Thu Jun 23 09:04:20 2011 -0700 @@ -15,14 +15,17 @@ Arithmetic for naturals is reduced to that for the non-negative integers. *} -instantiation nat :: number +instantiation nat :: number_semiring begin definition nat_number_of_def [code_unfold, code del]: "number_of v = nat (number_of v)" -instance .. - +instance proof + fix n show "number_of (int n) = (of_nat n :: nat)" + unfolding nat_number_of_def number_of_eq by simp +qed + end lemma [code_post]: @@ -250,9 +253,9 @@ end lemma power2_sum: - fixes x y :: "'a::number_ring" + fixes x y :: "'a::number_semiring" shows "(x + y)\ = x\ + y\ + 2 * x * y" - by (simp add: ring_distribs power2_eq_square mult_2) (rule mult_commute) + by (simp add: algebra_simps power2_eq_square semiring_mult_2_right) lemma power2_diff: fixes x y :: "'a::number_ring" @@ -345,6 +348,9 @@ unfolding nat_number_of_def number_of_is_id neg_def by simp +lemma nonneg_int_cases: + fixes k :: int assumes "0 \ k" obtains n where "k = of_nat n" + using assms by (cases k, simp, simp) subsubsection{*Successor *} @@ -390,7 +396,30 @@ by (simp add: nat_add_distrib) lemma nat_1_add_1 [simp]: "1 + 1 = (2::nat)" - by (rule int_int_eq [THEN iffD1]) simp + by (rule semiring_one_add_one_is_two) + +text {* TODO: replace simp rules above with these generic ones: *} + +lemma semiring_add_number_of: + "\Int.Pls \ v; Int.Pls \ v'\ \ + (number_of v :: 'a::number_semiring) + number_of v' = number_of (v + v')" + unfolding Int.Pls_def + by (elim nonneg_int_cases, + simp only: number_of_int of_nat_add [symmetric]) + +lemma semiring_number_of_add_1: + "Int.Pls \ v \ + number_of v + (1::'a::number_semiring) = number_of (Int.succ v)" + unfolding Int.Pls_def Int.succ_def + by (elim nonneg_int_cases, + simp only: number_of_int add_commute [where b=1] of_nat_Suc [symmetric]) + +lemma semiring_1_add_number_of: + "Int.Pls \ v \ + (1::'a::number_semiring) + number_of v = number_of (Int.succ v)" + unfolding Int.Pls_def Int.succ_def + by (elim nonneg_int_cases, + simp only: number_of_int add_commute [where b=1] of_nat_Suc [symmetric]) subsubsection{*Subtraction *} @@ -426,6 +455,14 @@ unfolding nat_number_of_def number_of_is_id numeral_simps by (simp add: nat_mult_distrib) +(* TODO: replace mult_nat_number_of with this next rule *) +lemma semiring_mult_number_of: + "\Int.Pls \ v; Int.Pls \ v'\ \ + (number_of v :: 'a::number_semiring) * number_of v' = number_of (v * v')" + unfolding Int.Pls_def + by (elim nonneg_int_cases, + simp only: number_of_int of_nat_mult [symmetric]) + subsection{*Comparisons*} @@ -842,10 +879,10 @@ text{*Lemmas for specialist use, NOT as default simprules*} lemma nat_mult_2: "2 * z = (z+z::nat)" -unfolding nat_1_add_1 [symmetric] left_distrib by simp +by (rule semiring_mult_2) lemma nat_mult_2_right: "z * 2 = (z+z::nat)" -by (subst mult_commute, rule nat_mult_2) +by (rule semiring_mult_2_right) text{*Case analysis on @{term "n<2"}*} lemma less_2_cases: "(n::nat) < 2 ==> n = 0 | n = Suc 0"