1.1 --- a/src/HOL/ex/Numeral.thy Sun Feb 15 19:53:20 2009 -0800
1.2 +++ b/src/HOL/ex/Numeral.thy Mon Feb 16 12:53:59 2009 -0800
1.3 @@ -50,6 +50,16 @@
1.4 "num_of_nat m = num_of_nat n \<longleftrightarrow> m = n \<or> (m = 0 \<or> m = 1) \<and> (n = 0 \<or> n = 1)"
1.5 by (auto simp add: num_of_nat_def num_of_nat_abs_inject [unfolded mem_def])
1.6
1.7 +lemma nat_of_num_gt_0: "0 < nat_of_num x"
1.8 + using nat_of_num [of x, unfolded mem_def] .
1.9 +
1.10 +lemma num_eq_iff: "x = y \<longleftrightarrow> nat_of_num x = nat_of_num y"
1.11 + apply safe
1.12 + apply (drule arg_cong [where f=num_of_nat_abs])
1.13 + apply (simp add: nat_of_num_inverse)
1.14 + done
1.15 +
1.16 +
1.17 lemma split_num_all:
1.18 "(\<And>m. PROP P m) \<equiv> (\<And>n. PROP P (num_of_nat n))"
1.19 proof
1.20 @@ -70,11 +80,11 @@
1.21
1.22 subsection {* Digit representation for @{typ num} *}
1.23
1.24 -instantiation num :: "{semiring, monoid_mult}"
1.25 +instantiation num :: "semiring"
1.26 begin
1.27
1.28 -definition one_num :: num where
1.29 - [code del]: "1 = num_of_nat 1"
1.30 +definition One :: num where
1.31 + one_num_def [code del]: "One = num_of_nat 1"
1.32
1.33 definition plus_num :: "num \<Rightarrow> num \<Rightarrow> num" where
1.34 [code del]: "m + n = num_of_nat (nat_of_num m + nat_of_num n)"
1.35 @@ -86,7 +96,7 @@
1.36 [code del]: "Dig0 n = n + n"
1.37
1.38 definition Dig1 :: "num \<Rightarrow> num" where
1.39 - [code del]: "Dig1 n = n + n + 1"
1.40 + [code del]: "Dig1 n = n + n + One"
1.41
1.42 instance proof
1.43 qed (simp_all add: one_num_def plus_num_def times_num_def
1.44 @@ -164,22 +174,22 @@
1.45 qed
1.46 qed
1.47
1.48 -lemma num_of_nat_Suc: "num_of_nat (Suc n) = (if n = 0 then 1 else num_of_nat n + 1)"
1.49 +lemma num_of_nat_Suc: "num_of_nat (Suc n) = (if n = 0 then One else num_of_nat n + One)"
1.50 by (cases n) (auto simp add: one_num_def plus_num_def num_of_nat_inverse)
1.51
1.52 lemma num_induct [case_names 1 Suc, induct type: num]:
1.53 fixes P :: "num \<Rightarrow> bool"
1.54 - assumes 1: "P 1"
1.55 - and Suc: "\<And>n. P n \<Longrightarrow> P (n + 1)"
1.56 + assumes 1: "P One"
1.57 + and Suc: "\<And>n. P n \<Longrightarrow> P (n + One)"
1.58 shows "P n"
1.59 proof (cases n)
1.60 case (nat m) then show ?thesis by (induct m arbitrary: n)
1.61 (auto simp: num_of_nat_Suc intro: 1 Suc split: split_if_asm)
1.62 qed
1.63
1.64 -rep_datatype "1::num" Dig0 Dig1 proof -
1.65 +rep_datatype One Dig0 Dig1 proof -
1.66 fix P m
1.67 - assume 1: "P 1"
1.68 + assume 1: "P One"
1.69 and Dig0: "\<And>m. P m \<Longrightarrow> P (Dig0 m)"
1.70 and Dig1: "\<And>m. P m \<Longrightarrow> P (Dig1 m)"
1.71 obtain n where "0 < n" and m: "m = num_of_nat n"
1.72 @@ -210,12 +220,12 @@
1.73 by (auto simp add: Dig1_def plus_num_def num_of_nat_inverse num_of_nat_inject)
1.74 next
1.75 fix n
1.76 - show "1 \<noteq> Dig0 n"
1.77 + show "One \<noteq> Dig0 n"
1.78 apply (cases n)
1.79 by (auto simp add: Dig0_def one_num_def plus_num_def num_of_nat_inverse num_of_nat_inject)
1.80 next
1.81 fix n
1.82 - show "1 \<noteq> Dig1 n"
1.83 + show "One \<noteq> Dig1 n"
1.84 apply (cases n)
1.85 by (auto simp add: Dig1_def one_num_def plus_num_def num_of_nat_inverse num_of_nat_inject)
1.86 next
1.87 @@ -263,7 +273,7 @@
1.88 begin
1.89
1.90 primrec of_num :: "num \<Rightarrow> 'a" where
1.91 - of_num_one [numeral]: "of_num 1 = 1"
1.92 + of_num_one [numeral]: "of_num One = 1"
1.93 | "of_num (Dig0 n) = of_num n + of_num n"
1.94 | "of_num (Dig1 n) = of_num n + of_num n + 1"
1.95
1.96 @@ -276,14 +286,14 @@
1.97 *}
1.98
1.99 ML {*
1.100 -fun mk_num 1 = @{term "1::num"}
1.101 +fun mk_num 1 = @{term One}
1.102 | mk_num k =
1.103 let
1.104 val (l, b) = Integer.div_mod k 2;
1.105 val bit = (if b = 0 then @{term Dig0} else @{term Dig1});
1.106 in bit $ (mk_num l) end;
1.107
1.108 -fun dest_num @{term "1::num"} = 1
1.109 +fun dest_num @{term One} = 1
1.110 | dest_num (@{term Dig0} $ n) = 2 * dest_num n
1.111 | dest_num (@{term Dig1} $ n) = 2 * dest_num n + 1;
1.112
1.113 @@ -302,7 +312,7 @@
1.114 parse_translation {*
1.115 let
1.116 fun num_of_int n = if n > 0 then case IntInf.quotRem (n, 2)
1.117 - of (0, 1) => Const (@{const_name HOL.one}, dummyT)
1.118 + of (0, 1) => Const (@{const_name One}, dummyT)
1.119 | (n, 0) => Const (@{const_name Dig0}, dummyT) $ num_of_int n
1.120 | (n, 1) => Const (@{const_name Dig1}, dummyT) $ num_of_int n
1.121 else raise Match;
1.122 @@ -323,7 +333,7 @@
1.123 dig 0 (int_of_num' n)
1.124 | int_of_num' (Const (@{const_syntax Dig1}, _) $ n) =
1.125 dig 1 (int_of_num' n)
1.126 - | int_of_num' (Const (@{const_syntax HOL.one}, _)) = 1;
1.127 + | int_of_num' (Const (@{const_syntax One}, _)) = 1;
1.128 fun num_tr' show_sorts T [n] =
1.129 let
1.130 val k = int_of_num' n;
1.131 @@ -344,29 +354,48 @@
1.132 First, addition and multiplication on digits.
1.133 *}
1.134
1.135 +lemma nat_of_num_add: "nat_of_num (x + y) = nat_of_num x + nat_of_num y"
1.136 + unfolding plus_num_def by (simp add: num_of_nat_inverse nat_of_num_gt_0)
1.137 +
1.138 +lemma nat_of_num_mult: "nat_of_num (x * y) = nat_of_num x * nat_of_num y"
1.139 + unfolding times_num_def by (simp add: num_of_nat_inverse nat_of_num_gt_0)
1.140 +
1.141 +lemma nat_of_num_One: "nat_of_num One = 1"
1.142 + unfolding one_num_def by (simp add: num_of_nat_inverse)
1.143 +
1.144 +lemma nat_of_num_Dig0: "nat_of_num (Dig0 x) = nat_of_num x + nat_of_num x"
1.145 + unfolding Dig0_def by (simp add: nat_of_num_add)
1.146 +
1.147 +lemma nat_of_num_Dig1: "nat_of_num (Dig1 x) = nat_of_num x + nat_of_num x + 1"
1.148 + unfolding Dig1_def by (simp add: nat_of_num_add nat_of_num_One)
1.149 +
1.150 +lemmas nat_of_num_simps =
1.151 + nat_of_num_One nat_of_num_Dig0 nat_of_num_Dig1
1.152 + nat_of_num_add nat_of_num_mult
1.153 +
1.154 lemma Dig_plus [numeral, simp, code]:
1.155 - "1 + 1 = Dig0 1"
1.156 - "1 + Dig0 m = Dig1 m"
1.157 - "1 + Dig1 m = Dig0 (m + 1)"
1.158 - "Dig0 n + 1 = Dig1 n"
1.159 + "One + One = Dig0 One"
1.160 + "One + Dig0 m = Dig1 m"
1.161 + "One + Dig1 m = Dig0 (m + One)"
1.162 + "Dig0 n + One = Dig1 n"
1.163 "Dig0 n + Dig0 m = Dig0 (n + m)"
1.164 "Dig0 n + Dig1 m = Dig1 (n + m)"
1.165 - "Dig1 n + 1 = Dig0 (n + 1)"
1.166 + "Dig1 n + One = Dig0 (n + One)"
1.167 "Dig1 n + Dig0 m = Dig1 (n + m)"
1.168 - "Dig1 n + Dig1 m = Dig0 (n + m + 1)"
1.169 - by (simp_all add: add_ac Dig0_def Dig1_def)
1.170 + "Dig1 n + Dig1 m = Dig0 (n + m + One)"
1.171 + by (simp_all add: num_eq_iff nat_of_num_simps)
1.172
1.173 lemma Dig_times [numeral, simp, code]:
1.174 - "1 * 1 = (1::num)"
1.175 - "1 * Dig0 n = Dig0 n"
1.176 - "1 * Dig1 n = Dig1 n"
1.177 - "Dig0 n * 1 = Dig0 n"
1.178 + "One * One = One"
1.179 + "One * Dig0 n = Dig0 n"
1.180 + "One * Dig1 n = Dig1 n"
1.181 + "Dig0 n * One = Dig0 n"
1.182 "Dig0 n * Dig0 m = Dig0 (n * Dig0 m)"
1.183 "Dig0 n * Dig1 m = Dig0 (n * Dig1 m)"
1.184 - "Dig1 n * 1 = Dig1 n"
1.185 + "Dig1 n * One = Dig1 n"
1.186 "Dig1 n * Dig0 m = Dig0 (n * Dig0 m + m)"
1.187 "Dig1 n * Dig1 m = Dig1 (n * Dig1 m + m)"
1.188 - by (simp_all add: left_distrib right_distrib add_ac Dig0_def Dig1_def)
1.189 + by (simp_all add: num_eq_iff nat_of_num_simps left_distrib right_distrib)
1.190
1.191 text {*
1.192 @{const of_num} is a morphism.
1.193 @@ -387,11 +416,11 @@
1.194 *}
1.195
1.196 lemma of_num_plus_one [numeral]:
1.197 - "of_num n + 1 = of_num (n + 1)"
1.198 + "of_num n + 1 = of_num (n + One)"
1.199 by (rule sym, induct n) (simp_all add: Dig_plus of_num.simps add_ac)
1.200
1.201 lemma of_num_one_plus [numeral]:
1.202 - "1 + of_num n = of_num (n + 1)"
1.203 + "1 + of_num n = of_num (n + One)"
1.204 unfolding of_num_plus_one [symmetric] add_commute ..
1.205
1.206 lemma of_num_plus [numeral]:
1.207 @@ -408,6 +437,9 @@
1.208 "1 * of_num n = of_num n"
1.209 by simp
1.210
1.211 +lemma times_One [simp]: "m * One = m"
1.212 + by (simp add: num_eq_iff nat_of_num_simps)
1.213 +
1.214 lemma of_num_times [numeral]:
1.215 "of_num m * of_num n = of_num (m * n)"
1.216 by (induct n rule: num_induct)
1.217 @@ -471,14 +503,14 @@
1.218 of_nat_eq_iff nat_of_num_inject ..
1.219
1.220 lemma of_num_eq_one_iff [numeral]:
1.221 - "of_num n = 1 \<longleftrightarrow> n = 1"
1.222 + "of_num n = 1 \<longleftrightarrow> n = One"
1.223 proof -
1.224 - have "of_num n = of_num 1 \<longleftrightarrow> n = 1" unfolding of_num_eq_iff ..
1.225 + have "of_num n = of_num One \<longleftrightarrow> n = One" unfolding of_num_eq_iff ..
1.226 then show ?thesis by (simp add: of_num_one)
1.227 qed
1.228
1.229 lemma one_eq_of_num_iff [numeral]:
1.230 - "1 = of_num n \<longleftrightarrow> n = 1"
1.231 + "1 = of_num n \<longleftrightarrow> n = One"
1.232 unfolding of_num_eq_one_iff [symmetric] by auto
1.233
1.234 end
1.235 @@ -515,9 +547,9 @@
1.236 end
1.237
1.238 lemma less_eq_num_code [numeral, simp, code]:
1.239 - "(1::num) \<le> n \<longleftrightarrow> True"
1.240 - "Dig0 m \<le> 1 \<longleftrightarrow> False"
1.241 - "Dig1 m \<le> 1 \<longleftrightarrow> False"
1.242 + "One \<le> n \<longleftrightarrow> True"
1.243 + "Dig0 m \<le> One \<longleftrightarrow> False"
1.244 + "Dig1 m \<le> One \<longleftrightarrow> False"
1.245 "Dig0 m \<le> Dig0 n \<longleftrightarrow> m \<le> n"
1.246 "Dig0 m \<le> Dig1 n \<longleftrightarrow> m \<le> n"
1.247 "Dig1 m \<le> Dig1 n \<longleftrightarrow> m \<le> n"
1.248 @@ -526,10 +558,10 @@
1.249 by (auto simp add: less_eq_num_def less_num_def nat_of_num_of_num of_num.simps)
1.250
1.251 lemma less_num_code [numeral, simp, code]:
1.252 - "m < (1::num) \<longleftrightarrow> False"
1.253 - "(1::num) < 1 \<longleftrightarrow> False"
1.254 - "1 < Dig0 n \<longleftrightarrow> True"
1.255 - "1 < Dig1 n \<longleftrightarrow> True"
1.256 + "m < One \<longleftrightarrow> False"
1.257 + "One < One \<longleftrightarrow> False"
1.258 + "One < Dig0 n \<longleftrightarrow> True"
1.259 + "One < Dig1 n \<longleftrightarrow> True"
1.260 "Dig0 m < Dig0 n \<longleftrightarrow> m < n"
1.261 "Dig0 m < Dig1 n \<longleftrightarrow> m \<le> n"
1.262 "Dig1 m < Dig1 n \<longleftrightarrow> m < n"
1.263 @@ -547,16 +579,16 @@
1.264 then show ?thesis by (simp add: of_nat_of_num)
1.265 qed
1.266
1.267 -lemma of_num_less_eq_one_iff [numeral]: "of_num n \<le> 1 \<longleftrightarrow> n = 1"
1.268 +lemma of_num_less_eq_one_iff [numeral]: "of_num n \<le> 1 \<longleftrightarrow> n = One"
1.269 proof -
1.270 - have "of_num n \<le> of_num 1 \<longleftrightarrow> n = 1"
1.271 + have "of_num n \<le> of_num One \<longleftrightarrow> n = One"
1.272 by (cases n) (simp_all add: of_num_less_eq_iff)
1.273 then show ?thesis by (simp add: of_num_one)
1.274 qed
1.275
1.276 lemma one_less_eq_of_num_iff [numeral]: "1 \<le> of_num n"
1.277 proof -
1.278 - have "of_num 1 \<le> of_num n"
1.279 + have "of_num One \<le> of_num n"
1.280 by (cases n) (simp_all add: of_num_less_eq_iff)
1.281 then show ?thesis by (simp add: of_num_one)
1.282 qed
1.283 @@ -570,14 +602,14 @@
1.284
1.285 lemma of_num_less_one_iff [numeral]: "\<not> of_num n < 1"
1.286 proof -
1.287 - have "\<not> of_num n < of_num 1"
1.288 + have "\<not> of_num n < of_num One"
1.289 by (cases n) (simp_all add: of_num_less_iff)
1.290 then show ?thesis by (simp add: of_num_one)
1.291 qed
1.292
1.293 -lemma one_less_of_num_iff [numeral]: "1 < of_num n \<longleftrightarrow> n \<noteq> 1"
1.294 +lemma one_less_of_num_iff [numeral]: "1 < of_num n \<longleftrightarrow> n \<noteq> One"
1.295 proof -
1.296 - have "of_num 1 < of_num n \<longleftrightarrow> n \<noteq> 1"
1.297 + have "of_num One < of_num n \<longleftrightarrow> n \<noteq> One"
1.298 by (cases n) (simp_all add: of_num_less_iff)
1.299 then show ?thesis by (simp add: of_num_one)
1.300 qed
1.301 @@ -591,15 +623,15 @@
1.302 text {* A double-and-decrement function *}
1.303
1.304 primrec DigM :: "num \<Rightarrow> num" where
1.305 - "DigM 1 = 1"
1.306 + "DigM One = One"
1.307 | "DigM (Dig0 n) = Dig1 (DigM n)"
1.308 | "DigM (Dig1 n) = Dig1 (Dig0 n)"
1.309
1.310 -lemma DigM_plus_one: "DigM n + 1 = Dig0 n"
1.311 +lemma DigM_plus_one: "DigM n + One = Dig0 n"
1.312 by (induct n) simp_all
1.313
1.314 -lemma one_plus_DigM: "1 + DigM n = Dig0 n"
1.315 - unfolding add_commute [of 1] DigM_plus_one ..
1.316 +lemma one_plus_DigM: "One + DigM n = Dig0 n"
1.317 + unfolding add_commute [of One] DigM_plus_one ..
1.318
1.319 class semiring_minus = semiring + minus + zero +
1.320 assumes minus_inverts_plus1: "a + b = c \<Longrightarrow> c - b = a"
1.321 @@ -632,7 +664,7 @@
1.322 by (rule minus_minus_zero_inverts_plus1) (simp add: of_num_plus assms)
1.323
1.324 lemmas Dig_plus_eval =
1.325 - of_num_plus of_num_eq_iff Dig_plus refl [of "1::num", THEN eqTrueI] num.inject
1.326 + of_num_plus of_num_eq_iff Dig_plus refl [of One, THEN eqTrueI] num.inject
1.327
1.328 simproc_setup numeral_minus ("of_num m - of_num n") = {*
1.329 let
1.330 @@ -728,12 +760,12 @@
1.331
1.332 instance nat :: semiring_1_minus proof qed simp_all
1.333
1.334 -lemma Suc_of_num [numeral]: "Suc (of_num n) = of_num (n + 1)"
1.335 +lemma Suc_of_num [numeral]: "Suc (of_num n) = of_num (n + One)"
1.336 unfolding of_num_plus_one [symmetric] by simp
1.337
1.338 lemma nat_number:
1.339 "1 = Suc 0"
1.340 - "of_num 1 = Suc 0"
1.341 + "of_num One = Suc 0"
1.342 "of_num (Dig0 n) = Suc (of_num (DigM n))"
1.343 "of_num (Dig1 n) = Suc (of_num (Dig0 n))"
1.344 by (simp_all add: of_num.simps DigM_plus_one Suc_of_num)
1.345 @@ -760,11 +792,11 @@
1.346 [code del]: "dup k = 2 * k"
1.347
1.348 lemma Dig_sub [code]:
1.349 - "sub 1 1 = 0"
1.350 - "sub (Dig0 m) 1 = of_num (DigM m)"
1.351 - "sub (Dig1 m) 1 = of_num (Dig0 m)"
1.352 - "sub 1 (Dig0 n) = - of_num (DigM n)"
1.353 - "sub 1 (Dig1 n) = - of_num (Dig0 n)"
1.354 + "sub One One = 0"
1.355 + "sub (Dig0 m) One = of_num (DigM m)"
1.356 + "sub (Dig1 m) One = of_num (Dig0 m)"
1.357 + "sub One (Dig0 n) = - of_num (DigM n)"
1.358 + "sub One (Dig1 n) = - of_num (Dig0 n)"
1.359 "sub (Dig0 m) (Dig0 n) = dup (sub m n)"
1.360 "sub (Dig1 m) (Dig1 n) = dup (sub m n)"
1.361 "sub (Dig1 m) (Dig0 n) = dup (sub m n) + 1"
1.362 @@ -792,7 +824,7 @@
1.363 by rule+
1.364
1.365 lemma one_int_code [code]:
1.366 - "1 = Pls 1"
1.367 + "1 = Pls One"
1.368 by (simp add: of_num_one)
1.369
1.370 lemma plus_int_code [code]: