1.1 --- a/src/HOL/ex/Numeral.thy Thu Apr 30 07:33:40 2009 -0700
1.2 +++ b/src/HOL/ex/Numeral.thy Thu Apr 30 11:14:04 2009 -0700
1.3 @@ -33,7 +33,7 @@
1.4 lemma nat_of_num_pos: "0 < nat_of_num x"
1.5 by (induct x) simp_all
1.6
1.7 -lemma nat_of_num_neq_0: " nat_of_num x \<noteq> 0"
1.8 +lemma nat_of_num_neq_0: "nat_of_num x \<noteq> 0"
1.9 by (induct x) simp_all
1.10
1.11 lemma nat_of_num_inc: "nat_of_num (inc x) = Suc (nat_of_num x)"
1.12 @@ -241,13 +241,24 @@
1.13 begin
1.14
1.15 primrec of_num :: "num \<Rightarrow> 'a" where
1.16 - of_num_one [numeral]: "of_num One = 1"
1.17 + of_num_One [numeral]: "of_num One = 1"
1.18 | "of_num (Dig0 n) = of_num n + of_num n"
1.19 | "of_num (Dig1 n) = of_num n + of_num n + 1"
1.20
1.21 lemma of_num_inc: "of_num (inc x) = of_num x + 1"
1.22 by (induct x) (simp_all add: add_ac)
1.23
1.24 +lemma of_num_add: "of_num (m + n) = of_num m + of_num n"
1.25 + apply (induct n rule: num_induct)
1.26 + apply (simp_all add: add_One add_inc of_num_inc add_ac)
1.27 + done
1.28 +
1.29 +lemma of_num_mult: "of_num (m * n) = of_num m * of_num n"
1.30 + apply (induct n rule: num_induct)
1.31 + apply (simp add: mult_One)
1.32 + apply (simp add: mult_inc of_num_add of_num_inc right_distrib)
1.33 + done
1.34 +
1.35 declare of_num.simps [simp del]
1.36
1.37 end
1.38 @@ -345,16 +356,15 @@
1.39
1.40 lemma of_num_plus_one [numeral]:
1.41 "of_num n + 1 = of_num (n + One)"
1.42 - by (rule sym, induct n) (simp_all add: of_num.simps add_ac)
1.43 + by (simp only: of_num_add of_num_One)
1.44
1.45 lemma of_num_one_plus [numeral]:
1.46 - "1 + of_num n = of_num (n + One)"
1.47 - unfolding of_num_plus_one [symmetric] add_commute ..
1.48 + "1 + of_num n = of_num (One + n)"
1.49 + by (simp only: of_num_add of_num_One)
1.50
1.51 lemma of_num_plus [numeral]:
1.52 "of_num m + of_num n = of_num (m + n)"
1.53 - by (induct n rule: num_induct)
1.54 - (simp_all add: add_One add_inc of_num_one of_num_inc add_ac)
1.55 + unfolding of_num_add ..
1.56
1.57 lemma of_num_times_one [numeral]:
1.58 "of_num n * 1 = of_num n"
1.59 @@ -366,9 +376,7 @@
1.60
1.61 lemma of_num_times [numeral]:
1.62 "of_num m * of_num n = of_num (m * n)"
1.63 - by (induct n rule: num_induct)
1.64 - (simp_all add: of_num_plus [symmetric] mult_One mult_inc
1.65 - semiring_class.right_distrib right_distrib of_num_one of_num_inc)
1.66 + unfolding of_num_mult ..
1.67
1.68 end
1.69
1.70 @@ -418,21 +426,15 @@
1.71 context semiring_char_0
1.72 begin
1.73
1.74 -lemma of_num_eq_iff [numeral]:
1.75 - "of_num m = of_num n \<longleftrightarrow> m = n"
1.76 +lemma of_num_eq_iff [numeral]: "of_num m = of_num n \<longleftrightarrow> m = n"
1.77 unfolding of_nat_of_num [symmetric] nat_of_num_of_num [symmetric]
1.78 of_nat_eq_iff num_eq_iff ..
1.79
1.80 -lemma of_num_eq_one_iff [numeral]:
1.81 - "of_num n = 1 \<longleftrightarrow> n = One"
1.82 -proof -
1.83 - have "of_num n = of_num One \<longleftrightarrow> n = One" unfolding of_num_eq_iff ..
1.84 - then show ?thesis by (simp add: of_num_one)
1.85 -qed
1.86 +lemma of_num_eq_one_iff [numeral]: "of_num n = 1 \<longleftrightarrow> n = One"
1.87 + using of_num_eq_iff [of n One] by (simp add: of_num_One)
1.88
1.89 -lemma one_eq_of_num_iff [numeral]:
1.90 - "1 = of_num n \<longleftrightarrow> n = One"
1.91 - unfolding of_num_eq_one_iff [symmetric] by auto
1.92 +lemma one_eq_of_num_iff [numeral]: "1 = of_num n \<longleftrightarrow> One = n"
1.93 + using of_num_eq_iff [of One n] by (simp add: of_num_One)
1.94
1.95 end
1.96
1.97 @@ -455,19 +457,11 @@
1.98 then show ?thesis by (simp add: of_nat_of_num)
1.99 qed
1.100
1.101 -lemma of_num_less_eq_one_iff [numeral]: "of_num n \<le> 1 \<longleftrightarrow> n = One"
1.102 -proof -
1.103 - have "of_num n \<le> of_num One \<longleftrightarrow> n = One"
1.104 - by (cases n) (simp_all add: of_num_less_eq_iff)
1.105 - then show ?thesis by (simp add: of_num_one)
1.106 -qed
1.107 +lemma of_num_less_eq_one_iff [numeral]: "of_num n \<le> 1 \<longleftrightarrow> n \<le> One"
1.108 + using of_num_less_eq_iff [of n One] by (simp add: of_num_One)
1.109
1.110 lemma one_less_eq_of_num_iff [numeral]: "1 \<le> of_num n"
1.111 -proof -
1.112 - have "of_num One \<le> of_num n"
1.113 - by (cases n) (simp_all add: of_num_less_eq_iff)
1.114 - then show ?thesis by (simp add: of_num_one)
1.115 -qed
1.116 + using of_num_less_eq_iff [of One n] by (simp add: of_num_One)
1.117
1.118 lemma of_num_less_iff [numeral]: "of_num m < of_num n \<longleftrightarrow> m < n"
1.119 proof -
1.120 @@ -477,18 +471,10 @@
1.121 qed
1.122
1.123 lemma of_num_less_one_iff [numeral]: "\<not> of_num n < 1"
1.124 -proof -
1.125 - have "\<not> of_num n < of_num One"
1.126 - by (cases n) (simp_all add: of_num_less_iff)
1.127 - then show ?thesis by (simp add: of_num_one)
1.128 -qed
1.129 + using of_num_less_iff [of n One] by (simp add: of_num_One)
1.130
1.131 -lemma one_less_of_num_iff [numeral]: "1 < of_num n \<longleftrightarrow> n \<noteq> One"
1.132 -proof -
1.133 - have "of_num One < of_num n \<longleftrightarrow> n \<noteq> One"
1.134 - by (cases n) (simp_all add: of_num_less_iff)
1.135 - then show ?thesis by (simp add: of_num_one)
1.136 -qed
1.137 +lemma one_less_of_num_iff [numeral]: "1 < of_num n \<longleftrightarrow> One < n"
1.138 + using of_num_less_iff [of One n] by (simp add: of_num_One)
1.139
1.140 lemma of_num_nonneg [numeral]: "0 \<le> of_num n"
1.141 by (induct n) (simp_all add: of_num.simps add_nonneg_nonneg)
1.142 @@ -512,13 +498,13 @@
1.143 qed
1.144
1.145 lemma minus_of_num_less_one_iff: "- of_num n < 1"
1.146 -using minus_of_num_less_of_num_iff [of n One] by (simp add: of_num_one)
1.147 + using minus_of_num_less_of_num_iff [of n One] by (simp add: of_num_One)
1.148
1.149 lemma minus_one_less_of_num_iff: "- 1 < of_num n"
1.150 -using minus_of_num_less_of_num_iff [of One n] by (simp add: of_num_one)
1.151 + using minus_of_num_less_of_num_iff [of One n] by (simp add: of_num_One)
1.152
1.153 lemma minus_one_less_one_iff: "- 1 < 1"
1.154 -using minus_of_num_less_of_num_iff [of One One] by (simp add: of_num_one)
1.155 + using minus_of_num_less_of_num_iff [of One One] by (simp add: of_num_One)
1.156
1.157 lemma minus_of_num_le_of_num_iff: "- of_num m \<le> of_num n"
1.158 by (simp add: less_imp_le minus_of_num_less_of_num_iff)
1.159 @@ -697,7 +683,7 @@
1.160 "- of_num n * of_num m = - (of_num n * of_num m)"
1.161 "of_num n * - of_num m = - (of_num n * of_num m)"
1.162 "- of_num n * - of_num m = of_num n * of_num m"
1.163 - by (simp_all add: minus_mult_left [symmetric] minus_mult_right [symmetric])
1.164 + by simp_all
1.165
1.166 lemma of_int_of_num [numeral]: "of_int (of_num n) = of_num n"
1.167 by (induct n)
1.168 @@ -713,38 +699,29 @@
1.169
1.170 lemma of_num_square: "of_num (square x) = of_num x * of_num x"
1.171 by (induct x)
1.172 - (simp_all add: of_num.simps of_num_plus [symmetric] algebra_simps)
1.173 + (simp_all add: of_num.simps of_num_add algebra_simps)
1.174
1.175 -lemma of_num_pow:
1.176 - "(of_num (pow x y)::'a::{semiring_numeral}) = of_num x ^ of_num y"
1.177 +lemma of_num_pow: "of_num (pow x y) = of_num x ^ of_num y"
1.178 by (induct y)
1.179 - (simp_all add: of_num.simps of_num_square of_num_times [symmetric]
1.180 - power_Suc power_add)
1.181 + (simp_all add: of_num.simps of_num_square of_num_mult power_add)
1.182
1.183 -lemma power_of_num [numeral]:
1.184 - "of_num x ^ of_num y = (of_num (pow x y)::'a::{semiring_numeral})"
1.185 - by (rule of_num_pow [symmetric])
1.186 +lemma power_of_num [numeral]: "of_num x ^ of_num y = of_num (pow x y)"
1.187 + unfolding of_num_pow ..
1.188
1.189 lemma power_zero_of_num [numeral]:
1.190 "0 ^ of_num n = (0::'a::{semiring_0,power})"
1.191 using of_num_pos [where n=n and ?'a=nat]
1.192 by (simp add: power_0_left)
1.193
1.194 -lemma power_minus_one_double:
1.195 - "(- 1) ^ (n + n) = (1::'a::{ring_1})"
1.196 - by (induct n) (simp_all add: power_Suc)
1.197 -
1.198 lemma power_minus_Dig0 [numeral]:
1.199 fixes x :: "'a::{ring_1}"
1.200 shows "(- x) ^ of_num (Dig0 n) = x ^ of_num (Dig0 n)"
1.201 - by (subst power_minus)
1.202 - (simp add: of_num.simps power_minus_one_double)
1.203 + by (induct n rule: num_induct) (simp_all add: of_num.simps of_num_inc)
1.204
1.205 lemma power_minus_Dig1 [numeral]:
1.206 fixes x :: "'a::{ring_1}"
1.207 shows "(- x) ^ of_num (Dig1 n) = - (x ^ of_num (Dig1 n))"
1.208 - by (subst power_minus)
1.209 - (simp add: of_num.simps power_Suc power_minus_one_double)
1.210 + by (induct n rule: num_induct) (simp_all add: of_num.simps of_num_inc)
1.211
1.212 declare power_one [numeral]
1.213
1.214 @@ -820,7 +797,7 @@
1.215
1.216 lemma one_int_code [code]:
1.217 "1 = Pls One"
1.218 - by (simp add: of_num_one)
1.219 + by (simp add: of_num_One)
1.220
1.221 lemma plus_int_code [code]:
1.222 "k + 0 = (k::int)"
1.223 @@ -829,7 +806,7 @@
1.224 "Pls m - Pls n = sub m n"
1.225 "Mns m + Mns n = Mns (m + n)"
1.226 "Mns m - Mns n = sub n m"
1.227 - by (simp_all add: of_num_plus [symmetric])
1.228 + by (simp_all add: of_num_add)
1.229
1.230 lemma uminus_int_code [code]:
1.231 "uminus 0 = (0::int)"
1.232 @@ -844,7 +821,7 @@
1.233 "Pls m - Mns n = Pls (m + n)"
1.234 "Mns m - Pls n = Mns (m + n)"
1.235 "Mns m - Mns n = sub n m"
1.236 - by (simp_all add: of_num_plus [symmetric])
1.237 + by (simp_all add: of_num_add)
1.238
1.239 lemma times_int_code [code]:
1.240 "k * 0 = (0::int)"
1.241 @@ -853,7 +830,7 @@
1.242 "Pls m * Mns n = Mns (m * n)"
1.243 "Mns m * Pls n = Mns (m * n)"
1.244 "Mns m * Mns n = Pls (m * n)"
1.245 - by (simp_all add: of_num_times [symmetric])
1.246 + by (simp_all add: of_num_mult)
1.247
1.248 lemma eq_int_code [code]:
1.249 "eq_class.eq 0 (0::int) \<longleftrightarrow> True"