author | wenzelm |
Wed, 12 Mar 2025 11:39:00 +0100 | |
changeset 82265 | 4b875a4c83b0 |
parent 81980 | 13b5aa1b3fb4 |
permissions | -rw-r--r-- |
47108 | 1 |
(* Title: HOL/Num.thy |
2 |
Author: Florian Haftmann |
|
3 |
Author: Brian Huffman |
|
4 |
*) |
|
5 |
||
60758 | 6 |
section \<open>Binary Numerals\<close> |
47108 | 7 |
|
8 |
theory Num |
|
64178 | 9 |
imports BNF_Least_Fixpoint Transfer |
47108 | 10 |
begin |
11 |
||
61799 | 12 |
subsection \<open>The \<open>num\<close> type\<close> |
47108 | 13 |
|
58310 | 14 |
datatype num = One | Bit0 num | Bit1 num |
47108 | 15 |
|
69593 | 16 |
text \<open>Increment function for type \<^typ>\<open>num\<close>\<close> |
47108 | 17 |
|
81980 | 18 |
primrec inc :: \<open>num \<Rightarrow> num\<close> |
63654 | 19 |
where |
81980 | 20 |
\<open>inc One = Bit0 One\<close> |
21 |
| \<open>inc (Bit0 x) = Bit1 x\<close> |
|
22 |
| \<open>inc (Bit1 x) = Bit0 (inc x)\<close> |
|
47108 | 23 |
|
69593 | 24 |
text \<open>Converting between type \<^typ>\<open>num\<close> and type \<^typ>\<open>nat\<close>\<close> |
47108 | 25 |
|
81980 | 26 |
primrec nat_of_num :: \<open>num \<Rightarrow> nat\<close> |
63654 | 27 |
where |
81980 | 28 |
\<open>nat_of_num One = Suc 0\<close> |
29 |
| \<open>nat_of_num (Bit0 x) = nat_of_num x + nat_of_num x\<close> |
|
30 |
| \<open>nat_of_num (Bit1 x) = Suc (nat_of_num x + nat_of_num x)\<close> |
|
47108 | 31 |
|
81980 | 32 |
primrec num_of_nat :: \<open>nat \<Rightarrow> num\<close> |
63654 | 33 |
where |
81980 | 34 |
\<open>num_of_nat 0 = One\<close> |
35 |
| \<open>num_of_nat (Suc n) = (if 0 < n then inc (num_of_nat n) else One)\<close> |
|
47108 | 36 |
|
81980 | 37 |
lemma nat_of_num_pos: \<open>0 < nat_of_num x\<close> |
47108 | 38 |
by (induct x) simp_all |
39 |
||
81980 | 40 |
lemma nat_of_num_neq_0: \<open> nat_of_num x \<noteq> 0\<close> |
47108 | 41 |
by (induct x) simp_all |
42 |
||
81980 | 43 |
lemma nat_of_num_inc: \<open>nat_of_num (inc x) = Suc (nat_of_num x)\<close> |
47108 | 44 |
by (induct x) simp_all |
45 |
||
81980 | 46 |
lemma num_of_nat_double: \<open>0 < n \<Longrightarrow> num_of_nat (n + n) = Bit0 (num_of_nat n)\<close> |
47108 | 47 |
by (induct n) simp_all |
48 |
||
69593 | 49 |
text \<open>Type \<^typ>\<open>num\<close> is isomorphic to the strictly positive natural numbers.\<close> |
47108 | 50 |
|
81980 | 51 |
lemma nat_of_num_inverse: \<open>num_of_nat (nat_of_num x) = x\<close> |
47108 | 52 |
by (induct x) (simp_all add: num_of_nat_double nat_of_num_pos) |
53 |
||
81980 | 54 |
lemma num_of_nat_inverse: \<open>0 < n \<Longrightarrow> nat_of_num (num_of_nat n) = n\<close> |
47108 | 55 |
by (induct n) (simp_all add: nat_of_num_inc) |
56 |
||
81980 | 57 |
lemma num_eq_iff: \<open>x = y \<longleftrightarrow> nat_of_num x = nat_of_num y\<close> |
47108 | 58 |
apply safe |
59 |
apply (drule arg_cong [where f=num_of_nat]) |
|
60 |
apply (simp add: nat_of_num_inverse) |
|
61 |
done |
|
62 |
||
63 |
lemma num_induct [case_names One inc]: |
|
81980 | 64 |
fixes P :: \<open>num \<Rightarrow> bool\<close> |
65 |
assumes One: \<open>P One\<close> |
|
66 |
and inc: \<open>\<And>x. P x \<Longrightarrow> P (inc x)\<close> |
|
67 |
shows \<open>P x\<close> |
|
47108 | 68 |
proof - |
81980 | 69 |
obtain n where n: \<open>Suc n = nat_of_num x\<close> |
70 |
by (cases \<open>nat_of_num x\<close>) (simp_all add: nat_of_num_neq_0) |
|
71 |
have \<open>P (num_of_nat (Suc n))\<close> |
|
47108 | 72 |
proof (induct n) |
63654 | 73 |
case 0 |
74 |
from One show ?case by simp |
|
47108 | 75 |
next |
76 |
case (Suc n) |
|
81980 | 77 |
then have \<open>P (inc (num_of_nat (Suc n)))\<close> by (rule inc) |
78 |
then show \<open>P (num_of_nat (Suc (Suc n)))\<close> by simp |
|
47108 | 79 |
qed |
81980 | 80 |
with n show \<open>P x\<close> |
47108 | 81 |
by (simp add: nat_of_num_inverse) |
82 |
qed |
|
83 |
||
60758 | 84 |
text \<open> |
69593 | 85 |
From now on, there are two possible models for \<^typ>\<open>num\<close>: as positive |
63654 | 86 |
naturals (rule \<open>num_induct\<close>) and as digit representation (rules |
87 |
\<open>num.induct\<close>, \<open>num.cases\<close>). |
|
60758 | 88 |
\<close> |
47108 | 89 |
|
90 |
||
60758 | 91 |
subsection \<open>Numeral operations\<close> |
47108 | 92 |
|
81980 | 93 |
instantiation num :: \<open>{plus,times,linorder}\<close> |
47108 | 94 |
begin |
95 |
||
81980 | 96 |
definition [code del]: \<open>m + n = num_of_nat (nat_of_num m + nat_of_num n)\<close> |
47108 | 97 |
|
81980 | 98 |
definition [code del]: \<open>m * n = num_of_nat (nat_of_num m * nat_of_num n)\<close> |
47108 | 99 |
|
81980 | 100 |
definition [code del]: \<open>m \<le> n \<longleftrightarrow> nat_of_num m \<le> nat_of_num n\<close> |
47108 | 101 |
|
81980 | 102 |
definition [code del]: \<open>m < n \<longleftrightarrow> nat_of_num m < nat_of_num n\<close> |
47108 | 103 |
|
104 |
instance |
|
61169 | 105 |
by standard (auto simp add: less_num_def less_eq_num_def num_eq_iff) |
47108 | 106 |
|
107 |
end |
|
108 |
||
81980 | 109 |
lemma nat_of_num_add: \<open>nat_of_num (x + y) = nat_of_num x + nat_of_num y\<close> |
47108 | 110 |
unfolding plus_num_def |
111 |
by (intro num_of_nat_inverse add_pos_pos nat_of_num_pos) |
|
112 |
||
81980 | 113 |
lemma nat_of_num_mult: \<open>nat_of_num (x * y) = nat_of_num x * nat_of_num y\<close> |
47108 | 114 |
unfolding times_num_def |
115 |
by (intro num_of_nat_inverse mult_pos_pos nat_of_num_pos) |
|
116 |
||
117 |
lemma add_num_simps [simp, code]: |
|
81980 | 118 |
\<open>One + One = Bit0 One\<close> |
119 |
\<open>One + Bit0 n = Bit1 n\<close> |
|
120 |
\<open>One + Bit1 n = Bit0 (n + One)\<close> |
|
121 |
\<open>Bit0 m + One = Bit1 m\<close> |
|
122 |
\<open>Bit0 m + Bit0 n = Bit0 (m + n)\<close> |
|
123 |
\<open>Bit0 m + Bit1 n = Bit1 (m + n)\<close> |
|
124 |
\<open>Bit1 m + One = Bit0 (m + One)\<close> |
|
125 |
\<open>Bit1 m + Bit0 n = Bit1 (m + n)\<close> |
|
126 |
\<open>Bit1 m + Bit1 n = Bit0 (m + n + One)\<close> |
|
47108 | 127 |
by (simp_all add: num_eq_iff nat_of_num_add) |
128 |
||
129 |
lemma mult_num_simps [simp, code]: |
|
81980 | 130 |
\<open>m * One = m\<close> |
131 |
\<open>One * n = n\<close> |
|
132 |
\<open>Bit0 m * Bit0 n = Bit0 (Bit0 (m * n))\<close> |
|
133 |
\<open>Bit0 m * Bit1 n = Bit0 (m * Bit1 n)\<close> |
|
134 |
\<open>Bit1 m * Bit0 n = Bit0 (Bit1 m * n)\<close> |
|
135 |
\<open>Bit1 m * Bit1 n = Bit1 (m + n + Bit0 (m * n))\<close> |
|
63654 | 136 |
by (simp_all add: num_eq_iff nat_of_num_add nat_of_num_mult distrib_right distrib_left) |
47108 | 137 |
|
138 |
lemma eq_num_simps: |
|
81980 | 139 |
\<open>One = One \<longleftrightarrow> True\<close> |
140 |
\<open>One = Bit0 n \<longleftrightarrow> False\<close> |
|
141 |
\<open>One = Bit1 n \<longleftrightarrow> False\<close> |
|
142 |
\<open>Bit0 m = One \<longleftrightarrow> False\<close> |
|
143 |
\<open>Bit1 m = One \<longleftrightarrow> False\<close> |
|
144 |
\<open>Bit0 m = Bit0 n \<longleftrightarrow> m = n\<close> |
|
145 |
\<open>Bit0 m = Bit1 n \<longleftrightarrow> False\<close> |
|
146 |
\<open>Bit1 m = Bit0 n \<longleftrightarrow> False\<close> |
|
147 |
\<open>Bit1 m = Bit1 n \<longleftrightarrow> m = n\<close> |
|
47108 | 148 |
by simp_all |
149 |
||
150 |
lemma le_num_simps [simp, code]: |
|
81980 | 151 |
\<open>One \<le> n \<longleftrightarrow> True\<close> |
152 |
\<open>Bit0 m \<le> One \<longleftrightarrow> False\<close> |
|
153 |
\<open>Bit1 m \<le> One \<longleftrightarrow> False\<close> |
|
154 |
\<open>Bit0 m \<le> Bit0 n \<longleftrightarrow> m \<le> n\<close> |
|
155 |
\<open>Bit0 m \<le> Bit1 n \<longleftrightarrow> m \<le> n\<close> |
|
156 |
\<open>Bit1 m \<le> Bit1 n \<longleftrightarrow> m \<le> n\<close> |
|
157 |
\<open>Bit1 m \<le> Bit0 n \<longleftrightarrow> m < n\<close> |
|
47108 | 158 |
using nat_of_num_pos [of n] nat_of_num_pos [of m] |
159 |
by (auto simp add: less_eq_num_def less_num_def) |
|
160 |
||
161 |
lemma less_num_simps [simp, code]: |
|
81980 | 162 |
\<open>m < One \<longleftrightarrow> False\<close> |
163 |
\<open>One < Bit0 n \<longleftrightarrow> True\<close> |
|
164 |
\<open>One < Bit1 n \<longleftrightarrow> True\<close> |
|
165 |
\<open>Bit0 m < Bit0 n \<longleftrightarrow> m < n\<close> |
|
166 |
\<open>Bit0 m < Bit1 n \<longleftrightarrow> m \<le> n\<close> |
|
167 |
\<open>Bit1 m < Bit1 n \<longleftrightarrow> m < n\<close> |
|
168 |
\<open>Bit1 m < Bit0 n \<longleftrightarrow> m < n\<close> |
|
47108 | 169 |
using nat_of_num_pos [of n] nat_of_num_pos [of m] |
170 |
by (auto simp add: less_eq_num_def less_num_def) |
|
171 |
||
81980 | 172 |
lemma le_num_One_iff: \<open>x \<le> One \<longleftrightarrow> x = One\<close> |
63654 | 173 |
by (simp add: antisym_conv) |
61630 | 174 |
|
63654 | 175 |
text \<open>Rules using \<open>One\<close> and \<open>inc\<close> as constructors.\<close> |
47108 | 176 |
|
81980 | 177 |
lemma add_One: \<open>x + One = inc x\<close> |
47108 | 178 |
by (simp add: num_eq_iff nat_of_num_add nat_of_num_inc) |
179 |
||
81980 | 180 |
lemma add_One_commute: \<open>One + n = n + One\<close> |
47108 | 181 |
by (induct n) simp_all |
182 |
||
81980 | 183 |
lemma add_inc: \<open>x + inc y = inc (x + y)\<close> |
47108 | 184 |
by (simp add: num_eq_iff nat_of_num_add nat_of_num_inc) |
185 |
||
81980 | 186 |
lemma mult_inc: \<open>x * inc y = x * y + x\<close> |
47108 | 187 |
by (simp add: num_eq_iff nat_of_num_mult nat_of_num_add nat_of_num_inc) |
188 |
||
69593 | 189 |
text \<open>The \<^const>\<open>num_of_nat\<close> conversion.\<close> |
47108 | 190 |
|
81980 | 191 |
lemma num_of_nat_One: \<open>n \<le> 1 \<Longrightarrow> num_of_nat n = One\<close> |
47108 | 192 |
by (cases n) simp_all |
193 |
||
194 |
lemma num_of_nat_plus_distrib: |
|
81980 | 195 |
\<open>0 < m \<Longrightarrow> 0 < n \<Longrightarrow> num_of_nat (m + n) = num_of_nat m + num_of_nat n\<close> |
47108 | 196 |
by (induct n) (auto simp add: add_One add_One_commute add_inc) |
197 |
||
63654 | 198 |
text \<open>A double-and-decrement function.\<close> |
47108 | 199 |
|
81980 | 200 |
primrec BitM :: \<open>num \<Rightarrow> num\<close> |
63654 | 201 |
where |
81980 | 202 |
\<open>BitM One = One\<close> |
203 |
| \<open>BitM (Bit0 n) = Bit1 (BitM n)\<close> |
|
204 |
| \<open>BitM (Bit1 n) = Bit1 (Bit0 n)\<close> |
|
47108 | 205 |
|
81980 | 206 |
lemma BitM_plus_one: \<open>BitM n + One = Bit0 n\<close> |
47108 | 207 |
by (induct n) simp_all |
208 |
||
81980 | 209 |
lemma one_plus_BitM: \<open>One + BitM n = Bit0 n\<close> |
47108 | 210 |
unfolding add_One_commute BitM_plus_one .. |
211 |
||
71991 | 212 |
lemma BitM_inc_eq: |
81980 | 213 |
\<open>BitM (inc n) = Bit1 n\<close> |
71991 | 214 |
by (induction n) simp_all |
215 |
||
216 |
lemma inc_BitM_eq: |
|
81980 | 217 |
\<open>inc (BitM n) = Bit0 n\<close> |
71991 | 218 |
by (simp add: BitM_plus_one[symmetric] add_One) |
219 |
||
63654 | 220 |
text \<open>Squaring and exponentiation.\<close> |
47108 | 221 |
|
81980 | 222 |
primrec sqr :: \<open>num \<Rightarrow> num\<close> |
63654 | 223 |
where |
81980 | 224 |
\<open>sqr One = One\<close> |
225 |
| \<open>sqr (Bit0 n) = Bit0 (Bit0 (sqr n))\<close> |
|
226 |
| \<open>sqr (Bit1 n) = Bit1 (Bit0 (sqr n + n))\<close> |
|
47108 | 227 |
|
81980 | 228 |
primrec pow :: \<open>num \<Rightarrow> num \<Rightarrow> num\<close> |
63654 | 229 |
where |
81980 | 230 |
\<open>pow x One = x\<close> |
231 |
| \<open>pow x (Bit0 y) = sqr (pow x y)\<close> |
|
232 |
| \<open>pow x (Bit1 y) = sqr (pow x y) * x\<close> |
|
47108 | 233 |
|
81980 | 234 |
lemma nat_of_num_sqr: \<open>nat_of_num (sqr x) = nat_of_num x * nat_of_num x\<close> |
63654 | 235 |
by (induct x) (simp_all add: algebra_simps nat_of_num_add) |
47108 | 236 |
|
81980 | 237 |
lemma sqr_conv_mult: \<open>sqr x = x * x\<close> |
47108 | 238 |
by (simp add: num_eq_iff nat_of_num_sqr nat_of_num_mult) |
239 |
||
70226 | 240 |
lemma num_double [simp]: |
81980 | 241 |
\<open>Bit0 num.One * n = Bit0 n\<close> |
70226 | 242 |
by (simp add: num_eq_iff nat_of_num_mult) |
243 |
||
47108 | 244 |
|
60758 | 245 |
subsection \<open>Binary numerals\<close> |
47108 | 246 |
|
60758 | 247 |
text \<open> |
47211 | 248 |
We embed binary representations into a generic algebraic |
61799 | 249 |
structure using \<open>numeral\<close>. |
60758 | 250 |
\<close> |
47108 | 251 |
|
252 |
class numeral = one + semigroup_add |
|
253 |
begin |
|
254 |
||
81980 | 255 |
primrec numeral :: \<open>num \<Rightarrow> 'a\<close> |
63654 | 256 |
where |
81980 | 257 |
numeral_One: \<open>numeral One = 1\<close> |
258 |
| numeral_Bit0: \<open>numeral (Bit0 n) = numeral n + numeral n\<close> |
|
259 |
| numeral_Bit1: \<open>numeral (Bit1 n) = numeral n + numeral n + 1\<close> |
|
47108 | 260 |
|
50817 | 261 |
lemma numeral_code [code]: |
81980 | 262 |
\<open>numeral One = 1\<close> |
263 |
\<open>numeral (Bit0 n) = (let m = numeral n in m + m)\<close> |
|
264 |
\<open>numeral (Bit1 n) = (let m = numeral n in m + m + 1)\<close> |
|
50817 | 265 |
by (simp_all add: Let_def) |
63654 | 266 |
|
81980 | 267 |
lemma one_plus_numeral_commute: \<open>1 + numeral x = numeral x + 1\<close> |
63654 | 268 |
proof (induct x) |
269 |
case One |
|
270 |
then show ?case by simp |
|
271 |
next |
|
272 |
case Bit0 |
|
273 |
then show ?case by (simp add: add.assoc [symmetric]) (simp add: add.assoc) |
|
274 |
next |
|
275 |
case Bit1 |
|
276 |
then show ?case by (simp add: add.assoc [symmetric]) (simp add: add.assoc) |
|
277 |
qed |
|
47108 | 278 |
|
81980 | 279 |
lemma numeral_inc: \<open>numeral (inc x) = numeral x + 1\<close> |
47108 | 280 |
proof (induct x) |
63654 | 281 |
case One |
282 |
then show ?case by simp |
|
283 |
next |
|
284 |
case Bit0 |
|
285 |
then show ?case by simp |
|
286 |
next |
|
47108 | 287 |
case (Bit1 x) |
81980 | 288 |
have \<open>numeral x + (1 + numeral x) + 1 = numeral x + (numeral x + 1) + 1\<close> |
47108 | 289 |
by (simp only: one_plus_numeral_commute) |
290 |
with Bit1 show ?case |
|
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
55974
diff
changeset
|
291 |
by (simp add: add.assoc) |
63654 | 292 |
qed |
47108 | 293 |
|
294 |
declare numeral.simps [simp del] |
|
295 |
||
81980 | 296 |
abbreviation \<open>Numeral1 \<equiv> numeral One\<close> |
47108 | 297 |
|
298 |
declare numeral_One [code_post] |
|
299 |
||
300 |
end |
|
301 |
||
60758 | 302 |
text \<open>Numeral syntax.\<close> |
47108 | 303 |
|
304 |
syntax |
|
81980 | 305 |
"_Numeral" :: \<open>num_const \<Rightarrow> 'a\<close> (\<open>(\<open>open_block notation=\<open>literal number\<close>\<close>_)\<close>) |
47108 | 306 |
|
69605 | 307 |
ML_file \<open>Tools/numeral.ML\<close> |
58410
6d46ad54a2ab
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents:
58310
diff
changeset
|
308 |
|
60758 | 309 |
parse_translation \<open> |
52143 | 310 |
let |
69593 | 311 |
fun numeral_tr [(c as Const (\<^syntax_const>\<open>_constrain\<close>, _)) $ t $ u] = |
52143 | 312 |
c $ numeral_tr [t] $ u |
313 |
| numeral_tr [Const (num, _)] = |
|
58421 | 314 |
(Numeral.mk_number_syntax o #value o Lexicon.read_num) num |
52143 | 315 |
| numeral_tr ts = raise TERM ("numeral_tr", ts); |
69593 | 316 |
in [(\<^syntax_const>\<open>_Numeral\<close>, K numeral_tr)] end |
60758 | 317 |
\<close> |
47108 | 318 |
|
60758 | 319 |
typed_print_translation \<open> |
52143 | 320 |
let |
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
321 |
fun num_tr' ctxt T [n] = |
52143 | 322 |
let |
62597 | 323 |
val k = Numeral.dest_num_syntax n; |
52187 | 324 |
val t' = |
69593 | 325 |
Syntax.const \<^syntax_const>\<open>_Numeral\<close> $ |
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
326 |
Syntax.free (string_of_int k); |
52143 | 327 |
in |
328 |
(case T of |
|
69593 | 329 |
Type (\<^type_name>\<open>fun\<close>, [_, T']) => |
52210
0226035df99d
more explicit Printer.type_emphasis, depending on show_type_emphasis;
wenzelm
parents:
52187
diff
changeset
|
330 |
if Printer.type_emphasis ctxt T' then |
69593 | 331 |
Syntax.const \<^syntax_const>\<open>_constrain\<close> $ t' $ |
52210
0226035df99d
more explicit Printer.type_emphasis, depending on show_type_emphasis;
wenzelm
parents:
52187
diff
changeset
|
332 |
Syntax_Phases.term_of_typ ctxt T' |
0226035df99d
more explicit Printer.type_emphasis, depending on show_type_emphasis;
wenzelm
parents:
52187
diff
changeset
|
333 |
else t' |
52187 | 334 |
| _ => if T = dummyT then t' else raise Match) |
52143 | 335 |
end; |
336 |
in |
|
69593 | 337 |
[(\<^const_syntax>\<open>numeral\<close>, num_tr')] |
52143 | 338 |
end |
60758 | 339 |
\<close> |
47108 | 340 |
|
47228 | 341 |
|
60758 | 342 |
subsection \<open>Class-specific numeral rules\<close> |
47108 | 343 |
|
69593 | 344 |
text \<open>\<^const>\<open>numeral\<close> is a morphism.\<close> |
63654 | 345 |
|
47108 | 346 |
|
61799 | 347 |
subsubsection \<open>Structures with addition: class \<open>numeral\<close>\<close> |
47108 | 348 |
|
349 |
context numeral |
|
350 |
begin |
|
351 |
||
81980 | 352 |
lemma numeral_add: \<open>numeral (m + n) = numeral m + numeral n\<close> |
47108 | 353 |
by (induct n rule: num_induct) |
63654 | 354 |
(simp_all only: numeral_One add_One add_inc numeral_inc add.assoc) |
47108 | 355 |
|
81980 | 356 |
lemma numeral_plus_numeral: \<open>numeral m + numeral n = numeral (m + n)\<close> |
47108 | 357 |
by (rule numeral_add [symmetric]) |
358 |
||
81980 | 359 |
lemma numeral_plus_one: \<open>numeral n + 1 = numeral (n + One)\<close> |
47108 | 360 |
using numeral_add [of n One] by (simp add: numeral_One) |
361 |
||
81980 | 362 |
lemma one_plus_numeral: \<open>1 + numeral n = numeral (One + n)\<close> |
47108 | 363 |
using numeral_add [of One n] by (simp add: numeral_One) |
364 |
||
81980 | 365 |
lemma one_add_one: \<open>1 + 1 = 2\<close> |
47108 | 366 |
using numeral_add [of One One] by (simp add: numeral_One) |
367 |
||
368 |
lemmas add_numeral_special = |
|
369 |
numeral_plus_one one_plus_numeral one_add_one |
|
370 |
||
371 |
end |
|
372 |
||
63654 | 373 |
|
374 |
subsubsection \<open>Structures with negation: class \<open>neg_numeral\<close>\<close> |
|
47108 | 375 |
|
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
376 |
class neg_numeral = numeral + group_add |
47108 | 377 |
begin |
378 |
||
81980 | 379 |
lemma uminus_numeral_One: \<open>- Numeral1 = - 1\<close> |
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
380 |
by (simp add: numeral_One) |
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
381 |
|
60758 | 382 |
text \<open>Numerals form an abelian subgroup.\<close> |
47108 | 383 |
|
81980 | 384 |
inductive is_num :: \<open>'a \<Rightarrow> bool\<close> |
63654 | 385 |
where |
81980 | 386 |
\<open>is_num 1\<close> |
387 |
| \<open>is_num x \<Longrightarrow> is_num (- x)\<close> |
|
388 |
| \<open>is_num x \<Longrightarrow> is_num y \<Longrightarrow> is_num (x + y)\<close> |
|
47108 | 389 |
|
81980 | 390 |
lemma is_num_numeral: \<open>is_num (numeral k)\<close> |
63654 | 391 |
by (induct k) (simp_all add: numeral.simps is_num.intros) |
47108 | 392 |
|
81980 | 393 |
lemma is_num_add_commute: \<open>is_num x \<Longrightarrow> is_num y \<Longrightarrow> x + y = y + x\<close> |
75669
43f5dfb7fa35
tuned (some HOL lints, by Yecine Megdiche);
Fabian Huch <huch@in.tum.de>
parents:
74592
diff
changeset
|
394 |
proof(induction x rule: is_num.induct) |
43f5dfb7fa35
tuned (some HOL lints, by Yecine Megdiche);
Fabian Huch <huch@in.tum.de>
parents:
74592
diff
changeset
|
395 |
case 1 |
43f5dfb7fa35
tuned (some HOL lints, by Yecine Megdiche);
Fabian Huch <huch@in.tum.de>
parents:
74592
diff
changeset
|
396 |
then show ?case |
43f5dfb7fa35
tuned (some HOL lints, by Yecine Megdiche);
Fabian Huch <huch@in.tum.de>
parents:
74592
diff
changeset
|
397 |
proof (induction y rule: is_num.induct) |
43f5dfb7fa35
tuned (some HOL lints, by Yecine Megdiche);
Fabian Huch <huch@in.tum.de>
parents:
74592
diff
changeset
|
398 |
case 1 |
43f5dfb7fa35
tuned (some HOL lints, by Yecine Megdiche);
Fabian Huch <huch@in.tum.de>
parents:
74592
diff
changeset
|
399 |
then show ?case by simp |
43f5dfb7fa35
tuned (some HOL lints, by Yecine Megdiche);
Fabian Huch <huch@in.tum.de>
parents:
74592
diff
changeset
|
400 |
next |
43f5dfb7fa35
tuned (some HOL lints, by Yecine Megdiche);
Fabian Huch <huch@in.tum.de>
parents:
74592
diff
changeset
|
401 |
case (2 y) |
81980 | 402 |
then have \<open>y + (1 + - y) + y = y + (- y + 1) + y\<close> |
75669
43f5dfb7fa35
tuned (some HOL lints, by Yecine Megdiche);
Fabian Huch <huch@in.tum.de>
parents:
74592
diff
changeset
|
403 |
by (simp add: add.assoc) |
81980 | 404 |
then have \<open>y + (1 + - y) = y + (- y + 1)\<close> |
75669
43f5dfb7fa35
tuned (some HOL lints, by Yecine Megdiche);
Fabian Huch <huch@in.tum.de>
parents:
74592
diff
changeset
|
405 |
by simp |
43f5dfb7fa35
tuned (some HOL lints, by Yecine Megdiche);
Fabian Huch <huch@in.tum.de>
parents:
74592
diff
changeset
|
406 |
then show ?case |
43f5dfb7fa35
tuned (some HOL lints, by Yecine Megdiche);
Fabian Huch <huch@in.tum.de>
parents:
74592
diff
changeset
|
407 |
by (rule add_left_imp_eq[of y]) |
43f5dfb7fa35
tuned (some HOL lints, by Yecine Megdiche);
Fabian Huch <huch@in.tum.de>
parents:
74592
diff
changeset
|
408 |
next |
43f5dfb7fa35
tuned (some HOL lints, by Yecine Megdiche);
Fabian Huch <huch@in.tum.de>
parents:
74592
diff
changeset
|
409 |
case (3 x y) |
81980 | 410 |
then have \<open>1 + (x + y) = x + 1 + y\<close> |
75669
43f5dfb7fa35
tuned (some HOL lints, by Yecine Megdiche);
Fabian Huch <huch@in.tum.de>
parents:
74592
diff
changeset
|
411 |
by (simp add: add.assoc [symmetric]) |
43f5dfb7fa35
tuned (some HOL lints, by Yecine Megdiche);
Fabian Huch <huch@in.tum.de>
parents:
74592
diff
changeset
|
412 |
then show ?case using 3 |
43f5dfb7fa35
tuned (some HOL lints, by Yecine Megdiche);
Fabian Huch <huch@in.tum.de>
parents:
74592
diff
changeset
|
413 |
by (simp add: add.assoc) |
43f5dfb7fa35
tuned (some HOL lints, by Yecine Megdiche);
Fabian Huch <huch@in.tum.de>
parents:
74592
diff
changeset
|
414 |
qed |
43f5dfb7fa35
tuned (some HOL lints, by Yecine Megdiche);
Fabian Huch <huch@in.tum.de>
parents:
74592
diff
changeset
|
415 |
next |
43f5dfb7fa35
tuned (some HOL lints, by Yecine Megdiche);
Fabian Huch <huch@in.tum.de>
parents:
74592
diff
changeset
|
416 |
case (2 x) |
81980 | 417 |
then have \<open>x + (- x + y) + x = x + (y + - x) + x\<close> |
75669
43f5dfb7fa35
tuned (some HOL lints, by Yecine Megdiche);
Fabian Huch <huch@in.tum.de>
parents:
74592
diff
changeset
|
418 |
by (simp add: add.assoc) |
81980 | 419 |
then have \<open>x + (- x + y) = x + (y + - x)\<close> |
75669
43f5dfb7fa35
tuned (some HOL lints, by Yecine Megdiche);
Fabian Huch <huch@in.tum.de>
parents:
74592
diff
changeset
|
420 |
by simp |
43f5dfb7fa35
tuned (some HOL lints, by Yecine Megdiche);
Fabian Huch <huch@in.tum.de>
parents:
74592
diff
changeset
|
421 |
then show ?case |
43f5dfb7fa35
tuned (some HOL lints, by Yecine Megdiche);
Fabian Huch <huch@in.tum.de>
parents:
74592
diff
changeset
|
422 |
by (rule add_left_imp_eq[of x]) |
43f5dfb7fa35
tuned (some HOL lints, by Yecine Megdiche);
Fabian Huch <huch@in.tum.de>
parents:
74592
diff
changeset
|
423 |
next |
43f5dfb7fa35
tuned (some HOL lints, by Yecine Megdiche);
Fabian Huch <huch@in.tum.de>
parents:
74592
diff
changeset
|
424 |
case (3 x z) |
81980 | 425 |
moreover have \<open>x + (y + z) = (x + y) + z\<close> |
75669
43f5dfb7fa35
tuned (some HOL lints, by Yecine Megdiche);
Fabian Huch <huch@in.tum.de>
parents:
74592
diff
changeset
|
426 |
by (simp add: add.assoc[symmetric]) |
43f5dfb7fa35
tuned (some HOL lints, by Yecine Megdiche);
Fabian Huch <huch@in.tum.de>
parents:
74592
diff
changeset
|
427 |
ultimately show ?case |
43f5dfb7fa35
tuned (some HOL lints, by Yecine Megdiche);
Fabian Huch <huch@in.tum.de>
parents:
74592
diff
changeset
|
428 |
by (simp add: add.assoc) |
43f5dfb7fa35
tuned (some HOL lints, by Yecine Megdiche);
Fabian Huch <huch@in.tum.de>
parents:
74592
diff
changeset
|
429 |
qed |
47108 | 430 |
|
81980 | 431 |
lemma is_num_add_left_commute: \<open>is_num x \<Longrightarrow> is_num y \<Longrightarrow> x + (y + z) = y + (x + z)\<close> |
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
55974
diff
changeset
|
432 |
by (simp only: add.assoc [symmetric] is_num_add_commute) |
47108 | 433 |
|
434 |
lemmas is_num_normalize = |
|
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
55974
diff
changeset
|
435 |
add.assoc is_num_add_commute is_num_add_left_commute |
47108 | 436 |
is_num.intros is_num_numeral |
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
53064
diff
changeset
|
437 |
minus_add |
47108 | 438 |
|
81980 | 439 |
definition dbl :: \<open>'a \<Rightarrow> 'a\<close> |
440 |
where \<open>dbl x = x + x\<close> |
|
63654 | 441 |
|
81980 | 442 |
definition dbl_inc :: \<open>'a \<Rightarrow> 'a\<close> |
443 |
where \<open>dbl_inc x = x + x + 1\<close> |
|
47108 | 444 |
|
81980 | 445 |
definition dbl_dec :: \<open>'a \<Rightarrow> 'a\<close> |
446 |
where \<open>dbl_dec x = x + x - 1\<close> |
|
63654 | 447 |
|
81980 | 448 |
definition sub :: \<open>num \<Rightarrow> num \<Rightarrow> 'a\<close> |
449 |
where \<open>sub k l = numeral k - numeral l\<close> |
|
47108 | 450 |
|
81980 | 451 |
lemma numeral_BitM: \<open>numeral (BitM n) = numeral (Bit0 n) - 1\<close> |
47108 | 452 |
by (simp only: BitM_plus_one [symmetric] numeral_add numeral_One eq_diff_eq) |
453 |
||
71991 | 454 |
lemma sub_inc_One_eq: |
81980 | 455 |
\<open>sub (inc n) num.One = numeral n\<close> |
71991 | 456 |
by (simp_all add: sub_def diff_eq_eq numeral_inc numeral.numeral_One) |
457 |
||
47108 | 458 |
lemma dbl_simps [simp]: |
81980 | 459 |
\<open>dbl (- numeral k) = - dbl (numeral k)\<close> |
460 |
\<open>dbl 0 = 0\<close> |
|
461 |
\<open>dbl 1 = 2\<close> |
|
462 |
\<open>dbl (- 1) = - 2\<close> |
|
463 |
\<open>dbl (numeral k) = numeral (Bit0 k)\<close> |
|
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
464 |
by (simp_all add: dbl_def numeral.simps minus_add) |
47108 | 465 |
|
466 |
lemma dbl_inc_simps [simp]: |
|
81980 | 467 |
\<open>dbl_inc (- numeral k) = - dbl_dec (numeral k)\<close> |
468 |
\<open>dbl_inc 0 = 1\<close> |
|
469 |
\<open>dbl_inc 1 = 3\<close> |
|
470 |
\<open>dbl_inc (- 1) = - 1\<close> |
|
471 |
\<open>dbl_inc (numeral k) = numeral (Bit1 k)\<close> |
|
63654 | 472 |
by (simp_all add: dbl_inc_def dbl_dec_def numeral.simps numeral_BitM is_num_normalize algebra_simps |
473 |
del: add_uminus_conv_diff) |
|
47108 | 474 |
|
475 |
lemma dbl_dec_simps [simp]: |
|
81980 | 476 |
\<open>dbl_dec (- numeral k) = - dbl_inc (numeral k)\<close> |
477 |
\<open>dbl_dec 0 = - 1\<close> |
|
478 |
\<open>dbl_dec 1 = 1\<close> |
|
479 |
\<open>dbl_dec (- 1) = - 3\<close> |
|
480 |
\<open>dbl_dec (numeral k) = numeral (BitM k)\<close> |
|
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
481 |
by (simp_all add: dbl_dec_def dbl_inc_def numeral.simps numeral_BitM is_num_normalize) |
47108 | 482 |
|
483 |
lemma sub_num_simps [simp]: |
|
81980 | 484 |
\<open>sub One One = 0\<close> |
485 |
\<open>sub One (Bit0 l) = - numeral (BitM l)\<close> |
|
486 |
\<open>sub One (Bit1 l) = - numeral (Bit0 l)\<close> |
|
487 |
\<open>sub (Bit0 k) One = numeral (BitM k)\<close> |
|
488 |
\<open>sub (Bit1 k) One = numeral (Bit0 k)\<close> |
|
489 |
\<open>sub (Bit0 k) (Bit0 l) = dbl (sub k l)\<close> |
|
490 |
\<open>sub (Bit0 k) (Bit1 l) = dbl_dec (sub k l)\<close> |
|
491 |
\<open>sub (Bit1 k) (Bit0 l) = dbl_inc (sub k l)\<close> |
|
492 |
\<open>sub (Bit1 k) (Bit1 l) = dbl (sub k l)\<close> |
|
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
493 |
by (simp_all add: dbl_def dbl_dec_def dbl_inc_def sub_def numeral.simps |
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
53064
diff
changeset
|
494 |
numeral_BitM is_num_normalize del: add_uminus_conv_diff add: diff_conv_add_uminus) |
47108 | 495 |
|
496 |
lemma add_neg_numeral_simps: |
|
81980 | 497 |
\<open>numeral m + - numeral n = sub m n\<close> |
498 |
\<open>- numeral m + numeral n = sub n m\<close> |
|
499 |
\<open>- numeral m + - numeral n = - (numeral m + numeral n)\<close> |
|
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
500 |
by (simp_all add: sub_def numeral_add numeral.simps is_num_normalize |
63654 | 501 |
del: add_uminus_conv_diff add: diff_conv_add_uminus) |
47108 | 502 |
|
503 |
lemma add_neg_numeral_special: |
|
81980 | 504 |
\<open>1 + - numeral m = sub One m\<close> |
505 |
\<open>- numeral m + 1 = sub One m\<close> |
|
506 |
\<open>numeral m + - 1 = sub m One\<close> |
|
507 |
\<open>- 1 + numeral n = sub n One\<close> |
|
508 |
\<open>- 1 + - numeral n = - numeral (inc n)\<close> |
|
509 |
\<open>- numeral m + - 1 = - numeral (inc m)\<close> |
|
510 |
\<open>1 + - 1 = 0\<close> |
|
511 |
\<open>- 1 + 1 = 0\<close> |
|
512 |
\<open>- 1 + - 1 = - 2\<close> |
|
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
513 |
by (simp_all add: sub_def numeral_add numeral.simps is_num_normalize right_minus numeral_inc |
63654 | 514 |
del: add_uminus_conv_diff add: diff_conv_add_uminus) |
47108 | 515 |
|
516 |
lemma diff_numeral_simps: |
|
81980 | 517 |
\<open>numeral m - numeral n = sub m n\<close> |
518 |
\<open>numeral m - - numeral n = numeral (m + n)\<close> |
|
519 |
\<open>- numeral m - numeral n = - numeral (m + n)\<close> |
|
520 |
\<open>- numeral m - - numeral n = sub n m\<close> |
|
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
521 |
by (simp_all add: sub_def numeral_add numeral.simps is_num_normalize |
63654 | 522 |
del: add_uminus_conv_diff add: diff_conv_add_uminus) |
47108 | 523 |
|
524 |
lemma diff_numeral_special: |
|
81980 | 525 |
\<open>1 - numeral n = sub One n\<close> |
526 |
\<open>numeral m - 1 = sub m One\<close> |
|
527 |
\<open>1 - - numeral n = numeral (One + n)\<close> |
|
528 |
\<open>- numeral m - 1 = - numeral (m + One)\<close> |
|
529 |
\<open>- 1 - numeral n = - numeral (inc n)\<close> |
|
530 |
\<open>numeral m - - 1 = numeral (inc m)\<close> |
|
531 |
\<open>- 1 - - numeral n = sub n One\<close> |
|
532 |
\<open>- numeral m - - 1 = sub One m\<close> |
|
533 |
\<open>1 - 1 = 0\<close> |
|
534 |
\<open>- 1 - 1 = - 2\<close> |
|
535 |
\<open>1 - - 1 = 2\<close> |
|
536 |
\<open>- 1 - - 1 = 0\<close> |
|
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
537 |
by (simp_all add: sub_def numeral_add numeral.simps is_num_normalize numeral_inc |
63654 | 538 |
del: add_uminus_conv_diff add: diff_conv_add_uminus) |
47108 | 539 |
|
540 |
end |
|
541 |
||
63654 | 542 |
|
543 |
subsubsection \<open>Structures with multiplication: class \<open>semiring_numeral\<close>\<close> |
|
47108 | 544 |
|
545 |
class semiring_numeral = semiring + monoid_mult |
|
546 |
begin |
|
547 |
||
548 |
subclass numeral .. |
|
549 |
||
81980 | 550 |
lemma numeral_mult: \<open>numeral (m * n) = numeral m * numeral n\<close> |
63654 | 551 |
by (induct n rule: num_induct) |
552 |
(simp_all add: numeral_One mult_inc numeral_inc numeral_add distrib_left) |
|
47108 | 553 |
|
81980 | 554 |
lemma numeral_times_numeral: \<open>numeral m * numeral n = numeral (m * n)\<close> |
47108 | 555 |
by (rule numeral_mult [symmetric]) |
556 |
||
81980 | 557 |
lemma mult_2: \<open>2 * z = z + z\<close> |
63654 | 558 |
by (simp add: one_add_one [symmetric] distrib_right) |
53064 | 559 |
|
81980 | 560 |
lemma mult_2_right: \<open>z * 2 = z + z\<close> |
63654 | 561 |
by (simp add: one_add_one [symmetric] distrib_left) |
53064 | 562 |
|
66936 | 563 |
lemma left_add_twice: |
81980 | 564 |
\<open>a + (a + b) = 2 * a + b\<close> |
66936 | 565 |
by (simp add: mult_2 ac_simps) |
566 |
||
79590 | 567 |
lemma numeral_Bit0_eq_double: |
81980 | 568 |
\<open>numeral (Bit0 n) = 2 * numeral n\<close> |
79590 | 569 |
by (simp add: mult_2) (simp add: numeral_Bit0) |
570 |
||
571 |
lemma numeral_Bit1_eq_inc_double: |
|
81980 | 572 |
\<open>numeral (Bit1 n) = 2 * numeral n + 1\<close> |
79590 | 573 |
by (simp add: mult_2) (simp add: numeral_Bit1) |
574 |
||
47108 | 575 |
end |
576 |
||
63654 | 577 |
|
578 |
subsubsection \<open>Structures with a zero: class \<open>semiring_1\<close>\<close> |
|
47108 | 579 |
|
580 |
context semiring_1 |
|
581 |
begin |
|
582 |
||
583 |
subclass semiring_numeral .. |
|
584 |
||
81980 | 585 |
lemma of_nat_numeral [simp]: \<open>of_nat (numeral n) = numeral n\<close> |
63654 | 586 |
by (induct n) (simp_all only: numeral.simps numeral_class.numeral.simps of_nat_add of_nat_1) |
47108 | 587 |
|
70927 | 588 |
end |
64178 | 589 |
|
81980 | 590 |
lemma nat_of_num_numeral [code_abbrev]: \<open>nat_of_num = numeral\<close> |
47108 | 591 |
proof |
592 |
fix n |
|
81980 | 593 |
have \<open>numeral n = nat_of_num n\<close> |
47108 | 594 |
by (induct n) (simp_all add: numeral.simps) |
81980 | 595 |
then show \<open>nat_of_num n = numeral n\<close> |
63654 | 596 |
by simp |
47108 | 597 |
qed |
598 |
||
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
50817
diff
changeset
|
599 |
lemma nat_of_num_code [code]: |
81980 | 600 |
\<open>nat_of_num One = 1\<close> |
601 |
\<open>nat_of_num (Bit0 n) = (let m = nat_of_num n in m + m)\<close> |
|
602 |
\<open>nat_of_num (Bit1 n) = (let m = nat_of_num n in Suc (m + m))\<close> |
|
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
50817
diff
changeset
|
603 |
by (simp_all add: Let_def) |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
50817
diff
changeset
|
604 |
|
63654 | 605 |
|
606 |
subsubsection \<open>Equality: class \<open>semiring_char_0\<close>\<close> |
|
47108 | 607 |
|
608 |
context semiring_char_0 |
|
609 |
begin |
|
610 |
||
81980 | 611 |
lemma numeral_eq_iff: \<open>numeral m = numeral n \<longleftrightarrow> m = n\<close> |
63654 | 612 |
by (simp only: of_nat_numeral [symmetric] nat_of_num_numeral [symmetric] |
613 |
of_nat_eq_iff num_eq_iff) |
|
47108 | 614 |
|
81980 | 615 |
lemma numeral_eq_one_iff: \<open>numeral n = 1 \<longleftrightarrow> n = One\<close> |
47108 | 616 |
by (rule numeral_eq_iff [of n One, unfolded numeral_One]) |
617 |
||
81980 | 618 |
lemma one_eq_numeral_iff: \<open>1 = numeral n \<longleftrightarrow> One = n\<close> |
47108 | 619 |
by (rule numeral_eq_iff [of One n, unfolded numeral_One]) |
620 |
||
81980 | 621 |
lemma numeral_neq_zero: \<open>numeral n \<noteq> 0\<close> |
63654 | 622 |
by (simp add: of_nat_numeral [symmetric] nat_of_num_numeral [symmetric] nat_of_num_pos) |
47108 | 623 |
|
81980 | 624 |
lemma zero_neq_numeral: \<open>0 \<noteq> numeral n\<close> |
47108 | 625 |
unfolding eq_commute [of 0] by (rule numeral_neq_zero) |
626 |
||
627 |
lemmas eq_numeral_simps [simp] = |
|
628 |
numeral_eq_iff |
|
629 |
numeral_eq_one_iff |
|
630 |
one_eq_numeral_iff |
|
631 |
numeral_neq_zero |
|
632 |
zero_neq_numeral |
|
633 |
||
634 |
end |
|
635 |
||
63654 | 636 |
|
70270
4065e3b0e5bf
Generalisations involving numerals; comparisons should now work for ennreal
paulson <lp15@cam.ac.uk>
parents:
70226
diff
changeset
|
637 |
subsubsection \<open>Comparisons: class \<open>linordered_nonzero_semiring\<close>\<close> |
47108 | 638 |
|
70270
4065e3b0e5bf
Generalisations involving numerals; comparisons should now work for ennreal
paulson <lp15@cam.ac.uk>
parents:
70226
diff
changeset
|
639 |
context linordered_nonzero_semiring |
47108 | 640 |
begin |
641 |
||
81980 | 642 |
lemma numeral_le_iff: \<open>numeral m \<le> numeral n \<longleftrightarrow> m \<le> n\<close> |
47108 | 643 |
proof - |
81980 | 644 |
have \<open>of_nat (numeral m) \<le> of_nat (numeral n) \<longleftrightarrow> m \<le> n\<close> |
63654 | 645 |
by (simp only: less_eq_num_def nat_of_num_numeral of_nat_le_iff) |
47108 | 646 |
then show ?thesis by simp |
647 |
qed |
|
648 |
||
81980 | 649 |
lemma one_le_numeral: \<open>1 \<le> numeral n\<close> |
650 |
using numeral_le_iff [of One n] by (simp add: numeral_One) |
|
47108 | 651 |
|
81980 | 652 |
lemma numeral_le_one_iff: \<open>numeral n \<le> 1 \<longleftrightarrow> n \<le> One\<close> |
653 |
using numeral_le_iff [of n One] by (simp add: numeral_One) |
|
47108 | 654 |
|
81980 | 655 |
lemma numeral_less_iff: \<open>numeral m < numeral n \<longleftrightarrow> m < n\<close> |
47108 | 656 |
proof - |
81980 | 657 |
have \<open>of_nat (numeral m) < of_nat (numeral n) \<longleftrightarrow> m < n\<close> |
47108 | 658 |
unfolding less_num_def nat_of_num_numeral of_nat_less_iff .. |
659 |
then show ?thesis by simp |
|
660 |
qed |
|
661 |
||
81980 | 662 |
lemma not_numeral_less_one: \<open>\<not> numeral n < 1\<close> |
663 |
using numeral_less_iff [of n One] by (simp add: numeral_One) |
|
47108 | 664 |
|
81980 | 665 |
lemma one_less_numeral_iff: \<open>1 < numeral n \<longleftrightarrow> One < n\<close> |
666 |
using numeral_less_iff [of One n] by (simp add: numeral_One) |
|
47108 | 667 |
|
81980 | 668 |
lemma zero_le_numeral: \<open>0 \<le> numeral n\<close> |
70270
4065e3b0e5bf
Generalisations involving numerals; comparisons should now work for ennreal
paulson <lp15@cam.ac.uk>
parents:
70226
diff
changeset
|
669 |
using dual_order.trans one_le_numeral zero_le_one by blast |
47108 | 670 |
|
81980 | 671 |
lemma zero_less_numeral: \<open>0 < numeral n\<close> |
70270
4065e3b0e5bf
Generalisations involving numerals; comparisons should now work for ennreal
paulson <lp15@cam.ac.uk>
parents:
70226
diff
changeset
|
672 |
using less_linear not_numeral_less_one order.strict_trans zero_less_one by blast |
47108 | 673 |
|
81980 | 674 |
lemma not_numeral_le_zero: \<open>\<not> numeral n \<le> 0\<close> |
47108 | 675 |
by (simp add: not_le zero_less_numeral) |
676 |
||
81980 | 677 |
lemma not_numeral_less_zero: \<open>\<not> numeral n < 0\<close> |
47108 | 678 |
by (simp add: not_less zero_le_numeral) |
679 |
||
81980 | 680 |
lemma one_of_nat_le_iff [simp]: \<open>1 \<le> of_nat k \<longleftrightarrow> 1 \<le> k\<close> |
80612
e65eed943bee
A lot of new material from the Ramsey development, including a couple of new simprules.
paulson <lp15@cam.ac.uk>
parents:
79590
diff
changeset
|
681 |
using of_nat_le_iff [of 1] by simp |
e65eed943bee
A lot of new material from the Ramsey development, including a couple of new simprules.
paulson <lp15@cam.ac.uk>
parents:
79590
diff
changeset
|
682 |
|
81980 | 683 |
lemma numeral_nat_le_iff [simp]: \<open>numeral n \<le> of_nat k \<longleftrightarrow> numeral n \<le> k\<close> |
684 |
using of_nat_le_iff [of \<open>numeral n\<close>] by simp |
|
80612
e65eed943bee
A lot of new material from the Ramsey development, including a couple of new simprules.
paulson <lp15@cam.ac.uk>
parents:
79590
diff
changeset
|
685 |
|
81980 | 686 |
lemma of_nat_le_1_iff [simp]: \<open>of_nat k \<le> 1 \<longleftrightarrow> k \<le> 1\<close> |
80612
e65eed943bee
A lot of new material from the Ramsey development, including a couple of new simprules.
paulson <lp15@cam.ac.uk>
parents:
79590
diff
changeset
|
687 |
using of_nat_le_iff [of _ 1] by simp |
e65eed943bee
A lot of new material from the Ramsey development, including a couple of new simprules.
paulson <lp15@cam.ac.uk>
parents:
79590
diff
changeset
|
688 |
|
81980 | 689 |
lemma of_nat_le_numeral_iff [simp]: \<open>of_nat k \<le> numeral n \<longleftrightarrow> k \<le> numeral n\<close> |
690 |
using of_nat_le_iff [of _ \<open>numeral n\<close>] by simp |
|
80612
e65eed943bee
A lot of new material from the Ramsey development, including a couple of new simprules.
paulson <lp15@cam.ac.uk>
parents:
79590
diff
changeset
|
691 |
|
81980 | 692 |
lemma one_of_nat_less_iff [simp]: \<open>1 < of_nat k \<longleftrightarrow> 1 < k\<close> |
80612
e65eed943bee
A lot of new material from the Ramsey development, including a couple of new simprules.
paulson <lp15@cam.ac.uk>
parents:
79590
diff
changeset
|
693 |
using of_nat_less_iff [of 1] by simp |
e65eed943bee
A lot of new material from the Ramsey development, including a couple of new simprules.
paulson <lp15@cam.ac.uk>
parents:
79590
diff
changeset
|
694 |
|
81980 | 695 |
lemma numeral_nat_less_iff [simp]: \<open>numeral n < of_nat k \<longleftrightarrow> numeral n < k\<close> |
696 |
using of_nat_less_iff [of \<open>numeral n\<close>] by simp |
|
80612
e65eed943bee
A lot of new material from the Ramsey development, including a couple of new simprules.
paulson <lp15@cam.ac.uk>
parents:
79590
diff
changeset
|
697 |
|
81980 | 698 |
lemma of_nat_less_1_iff [simp]: \<open>of_nat k < 1 \<longleftrightarrow> k < 1\<close> |
80612
e65eed943bee
A lot of new material from the Ramsey development, including a couple of new simprules.
paulson <lp15@cam.ac.uk>
parents:
79590
diff
changeset
|
699 |
using of_nat_less_iff [of _ 1] by simp |
e65eed943bee
A lot of new material from the Ramsey development, including a couple of new simprules.
paulson <lp15@cam.ac.uk>
parents:
79590
diff
changeset
|
700 |
|
81980 | 701 |
lemma of_nat_less_numeral_iff [simp]: \<open>of_nat k < numeral n \<longleftrightarrow> k < numeral n\<close> |
702 |
using of_nat_less_iff [of _ \<open>numeral n\<close>] by simp |
|
80612
e65eed943bee
A lot of new material from the Ramsey development, including a couple of new simprules.
paulson <lp15@cam.ac.uk>
parents:
79590
diff
changeset
|
703 |
|
81980 | 704 |
lemma of_nat_eq_numeral_iff [simp]: \<open>of_nat k = numeral n \<longleftrightarrow> k = numeral n\<close> |
705 |
using of_nat_eq_iff [of _ \<open>numeral n\<close>] by simp |
|
80612
e65eed943bee
A lot of new material from the Ramsey development, including a couple of new simprules.
paulson <lp15@cam.ac.uk>
parents:
79590
diff
changeset
|
706 |
|
47108 | 707 |
lemmas le_numeral_extra = |
708 |
zero_le_one not_one_le_zero |
|
709 |
order_refl [of 0] order_refl [of 1] |
|
710 |
||
711 |
lemmas less_numeral_extra = |
|
712 |
zero_less_one not_one_less_zero |
|
713 |
less_irrefl [of 0] less_irrefl [of 1] |
|
714 |
||
715 |
lemmas le_numeral_simps [simp] = |
|
716 |
numeral_le_iff |
|
717 |
one_le_numeral |
|
718 |
numeral_le_one_iff |
|
719 |
zero_le_numeral |
|
720 |
not_numeral_le_zero |
|
721 |
||
722 |
lemmas less_numeral_simps [simp] = |
|
723 |
numeral_less_iff |
|
724 |
one_less_numeral_iff |
|
725 |
not_numeral_less_one |
|
726 |
zero_less_numeral |
|
727 |
not_numeral_less_zero |
|
728 |
||
61630 | 729 |
lemma min_0_1 [simp]: |
81980 | 730 |
fixes min' :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close> |
731 |
defines \<open>min' \<equiv> min\<close> |
|
63654 | 732 |
shows |
81980 | 733 |
\<open>min' 0 1 = 0\<close> |
734 |
\<open>min' 1 0 = 0\<close> |
|
735 |
\<open>min' 0 (numeral x) = 0\<close> |
|
736 |
\<open>min' (numeral x) 0 = 0\<close> |
|
737 |
\<open>min' 1 (numeral x) = 1\<close> |
|
738 |
\<open>min' (numeral x) 1 = 1\<close> |
|
63654 | 739 |
by (simp_all add: min'_def min_def le_num_One_iff) |
61630 | 740 |
|
63654 | 741 |
lemma max_0_1 [simp]: |
81980 | 742 |
fixes max' :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close> |
743 |
defines \<open>max' \<equiv> max\<close> |
|
63654 | 744 |
shows |
81980 | 745 |
\<open>max' 0 1 = 1\<close> |
746 |
\<open>max' 1 0 = 1\<close> |
|
747 |
\<open>max' 0 (numeral x) = numeral x\<close> |
|
748 |
\<open>max' (numeral x) 0 = numeral x\<close> |
|
749 |
\<open>max' 1 (numeral x) = numeral x\<close> |
|
750 |
\<open>max' (numeral x) 1 = numeral x\<close> |
|
63654 | 751 |
by (simp_all add: max'_def max_def le_num_One_iff) |
61630 | 752 |
|
47108 | 753 |
end |
754 |
||
67116 | 755 |
text \<open>Unfold \<open>min\<close> and \<open>max\<close> on numerals.\<close> |
756 |
||
757 |
lemmas max_number_of [simp] = |
|
81980 | 758 |
max_def [of \<open>numeral u\<close> \<open>numeral v\<close>] |
759 |
max_def [of \<open>numeral u\<close> \<open>- numeral v\<close>] |
|
760 |
max_def [of \<open>- numeral u\<close> \<open>numeral v\<close>] |
|
761 |
max_def [of \<open>- numeral u\<close> \<open>- numeral v\<close>] for u v |
|
67116 | 762 |
|
763 |
lemmas min_number_of [simp] = |
|
81980 | 764 |
min_def [of \<open>numeral u\<close> \<open>numeral v\<close>] |
765 |
min_def [of \<open>numeral u\<close> \<open>- numeral v\<close>] |
|
766 |
min_def [of \<open>- numeral u\<close> \<open>numeral v\<close>] |
|
767 |
min_def [of \<open>- numeral u\<close> \<open>- numeral v\<close>] for u v |
|
67116 | 768 |
|
63654 | 769 |
|
770 |
subsubsection \<open>Multiplication and negation: class \<open>ring_1\<close>\<close> |
|
47108 | 771 |
|
772 |
context ring_1 |
|
773 |
begin |
|
774 |
||
775 |
subclass neg_numeral .. |
|
776 |
||
777 |
lemma mult_neg_numeral_simps: |
|
81980 | 778 |
\<open>- numeral m * - numeral n = numeral (m * n)\<close> |
779 |
\<open>- numeral m * numeral n = - numeral (m * n)\<close> |
|
780 |
\<open>numeral m * - numeral n = - numeral (m * n)\<close> |
|
63654 | 781 |
by (simp_all only: mult_minus_left mult_minus_right minus_minus numeral_mult) |
47108 | 782 |
|
81980 | 783 |
lemma mult_minus1 [simp]: \<open>- 1 * z = - z\<close> |
63654 | 784 |
by (simp add: numeral.simps) |
47108 | 785 |
|
81980 | 786 |
lemma mult_minus1_right [simp]: \<open>z * - 1 = - z\<close> |
63654 | 787 |
by (simp add: numeral.simps) |
47108 | 788 |
|
71758 | 789 |
lemma minus_sub_one_diff_one [simp]: |
790 |
\<open>- sub m One - 1 = - numeral m\<close> |
|
791 |
proof - |
|
792 |
have \<open>sub m One + 1 = numeral m\<close> |
|
793 |
by (simp flip: eq_diff_eq add: diff_numeral_special) |
|
794 |
then have \<open>- (sub m One + 1) = - numeral m\<close> |
|
795 |
by simp |
|
796 |
then show ?thesis |
|
797 |
by simp |
|
798 |
qed |
|
799 |
||
47108 | 800 |
end |
801 |
||
63654 | 802 |
|
803 |
subsubsection \<open>Equality using \<open>iszero\<close> for rings with non-zero characteristic\<close> |
|
47108 | 804 |
|
805 |
context ring_1 |
|
806 |
begin |
|
807 |
||
81980 | 808 |
definition iszero :: \<open>'a \<Rightarrow> bool\<close> |
809 |
where \<open>iszero z \<longleftrightarrow> z = 0\<close> |
|
47108 | 810 |
|
81980 | 811 |
lemma iszero_0 [simp]: \<open>iszero 0\<close> |
47108 | 812 |
by (simp add: iszero_def) |
813 |
||
81980 | 814 |
lemma not_iszero_1 [simp]: \<open>\<not> iszero 1\<close> |
47108 | 815 |
by (simp add: iszero_def) |
816 |
||
81980 | 817 |
lemma not_iszero_Numeral1: \<open>\<not> iszero Numeral1\<close> |
47108 | 818 |
by (simp add: numeral_One) |
819 |
||
81980 | 820 |
lemma not_iszero_neg_1 [simp]: \<open>\<not> iszero (- 1)\<close> |
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
821 |
by (simp add: iszero_def) |
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
822 |
|
81980 | 823 |
lemma not_iszero_neg_Numeral1: \<open>\<not> iszero (- Numeral1)\<close> |
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
824 |
by (simp add: numeral_One) |
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
825 |
|
81980 | 826 |
lemma iszero_neg_numeral [simp]: \<open>iszero (- numeral w) \<longleftrightarrow> iszero (numeral w)\<close> |
63654 | 827 |
unfolding iszero_def by (rule neg_equal_0_iff_equal) |
47108 | 828 |
|
81980 | 829 |
lemma eq_iff_iszero_diff: \<open>x = y \<longleftrightarrow> iszero (x - y)\<close> |
47108 | 830 |
unfolding iszero_def by (rule eq_iff_diff_eq_0) |
831 |
||
63654 | 832 |
text \<open> |
833 |
The \<open>eq_numeral_iff_iszero\<close> lemmas are not declared \<open>[simp]\<close> by default, |
|
834 |
because for rings of characteristic zero, better simp rules are possible. |
|
835 |
For a type like integers mod \<open>n\<close>, type-instantiated versions of these rules |
|
836 |
should be added to the simplifier, along with a type-specific rule for |
|
837 |
deciding propositions of the form \<open>iszero (numeral w)\<close>. |
|
47108 | 838 |
|
63654 | 839 |
bh: Maybe it would not be so bad to just declare these as simp rules anyway? |
840 |
I should test whether these rules take precedence over the \<open>ring_char_0\<close> |
|
841 |
rules in the simplifier. |
|
60758 | 842 |
\<close> |
47108 | 843 |
|
844 |
lemma eq_numeral_iff_iszero: |
|
81980 | 845 |
\<open>numeral x = numeral y \<longleftrightarrow> iszero (sub x y)\<close> |
846 |
\<open>numeral x = - numeral y \<longleftrightarrow> iszero (numeral (x + y))\<close> |
|
847 |
\<open>- numeral x = numeral y \<longleftrightarrow> iszero (numeral (x + y))\<close> |
|
848 |
\<open>- numeral x = - numeral y \<longleftrightarrow> iszero (sub y x)\<close> |
|
849 |
\<open>numeral x = 1 \<longleftrightarrow> iszero (sub x One)\<close> |
|
850 |
\<open>1 = numeral y \<longleftrightarrow> iszero (sub One y)\<close> |
|
851 |
\<open>- numeral x = 1 \<longleftrightarrow> iszero (numeral (x + One))\<close> |
|
852 |
\<open>1 = - numeral y \<longleftrightarrow> iszero (numeral (One + y))\<close> |
|
853 |
\<open>numeral x = 0 \<longleftrightarrow> iszero (numeral x)\<close> |
|
854 |
\<open>0 = numeral y \<longleftrightarrow> iszero (numeral y)\<close> |
|
855 |
\<open>- numeral x = 0 \<longleftrightarrow> iszero (numeral x)\<close> |
|
856 |
\<open>0 = - numeral y \<longleftrightarrow> iszero (numeral y)\<close> |
|
47108 | 857 |
unfolding eq_iff_iszero_diff diff_numeral_simps diff_numeral_special |
858 |
by simp_all |
|
859 |
||
860 |
end |
|
861 |
||
63654 | 862 |
|
863 |
subsubsection \<open>Equality and negation: class \<open>ring_char_0\<close>\<close> |
|
47108 | 864 |
|
62481
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62348
diff
changeset
|
865 |
context ring_char_0 |
47108 | 866 |
begin |
867 |
||
81980 | 868 |
lemma not_iszero_numeral [simp]: \<open>\<not> iszero (numeral w)\<close> |
47108 | 869 |
by (simp add: iszero_def) |
870 |
||
81980 | 871 |
lemma neg_numeral_eq_iff: \<open>- numeral m = - numeral n \<longleftrightarrow> m = n\<close> |
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
872 |
by simp |
47108 | 873 |
|
81980 | 874 |
lemma numeral_neq_neg_numeral: \<open>numeral m \<noteq> - numeral n\<close> |
63654 | 875 |
by (simp add: eq_neg_iff_add_eq_0 numeral_plus_numeral) |
47108 | 876 |
|
81980 | 877 |
lemma neg_numeral_neq_numeral: \<open>- numeral m \<noteq> numeral n\<close> |
47108 | 878 |
by (rule numeral_neq_neg_numeral [symmetric]) |
879 |
||
81980 | 880 |
lemma zero_neq_neg_numeral: \<open>0 \<noteq> - numeral n\<close> |
63654 | 881 |
by simp |
47108 | 882 |
|
81980 | 883 |
lemma neg_numeral_neq_zero: \<open>- numeral n \<noteq> 0\<close> |
63654 | 884 |
by simp |
47108 | 885 |
|
81980 | 886 |
lemma one_neq_neg_numeral: \<open>1 \<noteq> - numeral n\<close> |
47108 | 887 |
using numeral_neq_neg_numeral [of One n] by (simp add: numeral_One) |
888 |
||
81980 | 889 |
lemma neg_numeral_neq_one: \<open>- numeral n \<noteq> 1\<close> |
47108 | 890 |
using neg_numeral_neq_numeral [of n One] by (simp add: numeral_One) |
891 |
||
81980 | 892 |
lemma neg_one_neq_numeral: \<open>- 1 \<noteq> numeral n\<close> |
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
893 |
using neg_numeral_neq_numeral [of One n] by (simp add: numeral_One) |
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
894 |
|
81980 | 895 |
lemma numeral_neq_neg_one: \<open>numeral n \<noteq> - 1\<close> |
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
896 |
using numeral_neq_neg_numeral [of n One] by (simp add: numeral_One) |
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
897 |
|
81980 | 898 |
lemma neg_one_eq_numeral_iff: \<open>- 1 = - numeral n \<longleftrightarrow> n = One\<close> |
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
899 |
using neg_numeral_eq_iff [of One n] by (auto simp add: numeral_One) |
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
900 |
|
81980 | 901 |
lemma numeral_eq_neg_one_iff: \<open>- numeral n = - 1 \<longleftrightarrow> n = One\<close> |
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
902 |
using neg_numeral_eq_iff [of n One] by (auto simp add: numeral_One) |
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
903 |
|
81980 | 904 |
lemma neg_one_neq_zero: \<open>- 1 \<noteq> 0\<close> |
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
905 |
by simp |
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
906 |
|
81980 | 907 |
lemma zero_neq_neg_one: \<open>0 \<noteq> - 1\<close> |
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
908 |
by simp |
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
909 |
|
81980 | 910 |
lemma neg_one_neq_one: \<open>- 1 \<noteq> 1\<close> |
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
911 |
using neg_numeral_neq_numeral [of One One] by (simp only: numeral_One not_False_eq_True) |
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
912 |
|
81980 | 913 |
lemma one_neq_neg_one: \<open>1 \<noteq> - 1\<close> |
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
914 |
using numeral_neq_neg_numeral [of One One] by (simp only: numeral_One not_False_eq_True) |
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
915 |
|
47108 | 916 |
lemmas eq_neg_numeral_simps [simp] = |
917 |
neg_numeral_eq_iff |
|
918 |
numeral_neq_neg_numeral neg_numeral_neq_numeral |
|
919 |
one_neq_neg_numeral neg_numeral_neq_one |
|
920 |
zero_neq_neg_numeral neg_numeral_neq_zero |
|
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
921 |
neg_one_neq_numeral numeral_neq_neg_one |
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
922 |
neg_one_eq_numeral_iff numeral_eq_neg_one_iff |
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
923 |
neg_one_neq_zero zero_neq_neg_one |
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
924 |
neg_one_neq_one one_neq_neg_one |
47108 | 925 |
|
926 |
end |
|
927 |
||
62348 | 928 |
|
63654 | 929 |
subsubsection \<open>Structures with negation and order: class \<open>linordered_idom\<close>\<close> |
47108 | 930 |
|
931 |
context linordered_idom |
|
932 |
begin |
|
933 |
||
934 |
subclass ring_char_0 .. |
|
935 |
||
81980 | 936 |
lemma neg_numeral_le_iff: \<open>- numeral m \<le> - numeral n \<longleftrightarrow> n \<le> m\<close> |
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
937 |
by (simp only: neg_le_iff_le numeral_le_iff) |
47108 | 938 |
|
81980 | 939 |
lemma neg_numeral_less_iff: \<open>- numeral m < - numeral n \<longleftrightarrow> n < m\<close> |
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
940 |
by (simp only: neg_less_iff_less numeral_less_iff) |
47108 | 941 |
|
81980 | 942 |
lemma neg_numeral_less_zero: \<open>- numeral n < 0\<close> |
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
943 |
by (simp only: neg_less_0_iff_less zero_less_numeral) |
47108 | 944 |
|
81980 | 945 |
lemma neg_numeral_le_zero: \<open>- numeral n \<le> 0\<close> |
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
946 |
by (simp only: neg_le_0_iff_le zero_le_numeral) |
47108 | 947 |
|
81980 | 948 |
lemma not_zero_less_neg_numeral: \<open>\<not> 0 < - numeral n\<close> |
47108 | 949 |
by (simp only: not_less neg_numeral_le_zero) |
950 |
||
81980 | 951 |
lemma not_zero_le_neg_numeral: \<open>\<not> 0 \<le> - numeral n\<close> |
47108 | 952 |
by (simp only: not_le neg_numeral_less_zero) |
953 |
||
81980 | 954 |
lemma neg_numeral_less_numeral: \<open>- numeral m < numeral n\<close> |
47108 | 955 |
using neg_numeral_less_zero zero_less_numeral by (rule less_trans) |
956 |
||
81980 | 957 |
lemma neg_numeral_le_numeral: \<open>- numeral m \<le> numeral n\<close> |
47108 | 958 |
by (simp only: less_imp_le neg_numeral_less_numeral) |
959 |
||
81980 | 960 |
lemma not_numeral_less_neg_numeral: \<open>\<not> numeral m < - numeral n\<close> |
47108 | 961 |
by (simp only: not_less neg_numeral_le_numeral) |
962 |
||
81980 | 963 |
lemma not_numeral_le_neg_numeral: \<open>\<not> numeral m \<le> - numeral n\<close> |
47108 | 964 |
by (simp only: not_le neg_numeral_less_numeral) |
63654 | 965 |
|
81980 | 966 |
lemma neg_numeral_less_one: \<open>- numeral m < 1\<close> |
47108 | 967 |
by (rule neg_numeral_less_numeral [of m One, unfolded numeral_One]) |
968 |
||
81980 | 969 |
lemma neg_numeral_le_one: \<open>- numeral m \<le> 1\<close> |
47108 | 970 |
by (rule neg_numeral_le_numeral [of m One, unfolded numeral_One]) |
971 |
||
81980 | 972 |
lemma not_one_less_neg_numeral: \<open>\<not> 1 < - numeral m\<close> |
47108 | 973 |
by (simp only: not_less neg_numeral_le_one) |
974 |
||
81980 | 975 |
lemma not_one_le_neg_numeral: \<open>\<not> 1 \<le> - numeral m\<close> |
47108 | 976 |
by (simp only: not_le neg_numeral_less_one) |
977 |
||
81980 | 978 |
lemma not_numeral_less_neg_one: \<open>\<not> numeral m < - 1\<close> |
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
979 |
using not_numeral_less_neg_numeral [of m One] by (simp add: numeral_One) |
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
980 |
|
81980 | 981 |
lemma not_numeral_le_neg_one: \<open>\<not> numeral m \<le> - 1\<close> |
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
982 |
using not_numeral_le_neg_numeral [of m One] by (simp add: numeral_One) |
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
983 |
|
81980 | 984 |
lemma neg_one_less_numeral: \<open>- 1 < numeral m\<close> |
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
985 |
using neg_numeral_less_numeral [of One m] by (simp add: numeral_One) |
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
986 |
|
81980 | 987 |
lemma neg_one_le_numeral: \<open>- 1 \<le> numeral m\<close> |
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
988 |
using neg_numeral_le_numeral [of One m] by (simp add: numeral_One) |
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
989 |
|
81980 | 990 |
lemma neg_numeral_less_neg_one_iff: \<open>- numeral m < - 1 \<longleftrightarrow> m \<noteq> One\<close> |
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
991 |
by (cases m) simp_all |
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
992 |
|
81980 | 993 |
lemma neg_numeral_le_neg_one: \<open>- numeral m \<le> - 1\<close> |
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
994 |
by simp |
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
995 |
|
81980 | 996 |
lemma not_neg_one_less_neg_numeral: \<open>\<not> - 1 < - numeral m\<close> |
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
997 |
by simp |
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
998 |
|
81980 | 999 |
lemma not_neg_one_le_neg_numeral_iff: \<open>\<not> - 1 \<le> - numeral m \<longleftrightarrow> m \<noteq> One\<close> |
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
1000 |
by (cases m) simp_all |
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
1001 |
|
81980 | 1002 |
lemma sub_non_negative: \<open>sub n m \<ge> 0 \<longleftrightarrow> n \<ge> m\<close> |
47108 | 1003 |
by (simp only: sub_def le_diff_eq) simp |
1004 |
||
81980 | 1005 |
lemma sub_positive: \<open>sub n m > 0 \<longleftrightarrow> n > m\<close> |
47108 | 1006 |
by (simp only: sub_def less_diff_eq) simp |
1007 |
||
81980 | 1008 |
lemma sub_non_positive: \<open>sub n m \<le> 0 \<longleftrightarrow> n \<le> m\<close> |
47108 | 1009 |
by (simp only: sub_def diff_le_eq) simp |
1010 |
||
81980 | 1011 |
lemma sub_negative: \<open>sub n m < 0 \<longleftrightarrow> n < m\<close> |
47108 | 1012 |
by (simp only: sub_def diff_less_eq) simp |
1013 |
||
1014 |
lemmas le_neg_numeral_simps [simp] = |
|
1015 |
neg_numeral_le_iff |
|
1016 |
neg_numeral_le_numeral not_numeral_le_neg_numeral |
|
1017 |
neg_numeral_le_zero not_zero_le_neg_numeral |
|
1018 |
neg_numeral_le_one not_one_le_neg_numeral |
|
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
1019 |
neg_one_le_numeral not_numeral_le_neg_one |
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
1020 |
neg_numeral_le_neg_one not_neg_one_le_neg_numeral_iff |
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
1021 |
|
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
1022 |
lemma le_minus_one_simps [simp]: |
81980 | 1023 |
\<open>- 1 \<le> 0\<close> |
1024 |
\<open>- 1 \<le> 1\<close> |
|
1025 |
\<open>\<not> 0 \<le> - 1\<close> |
|
1026 |
\<open>\<not> 1 \<le> - 1\<close> |
|
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
1027 |
by simp_all |
47108 | 1028 |
|
1029 |
lemmas less_neg_numeral_simps [simp] = |
|
1030 |
neg_numeral_less_iff |
|
1031 |
neg_numeral_less_numeral not_numeral_less_neg_numeral |
|
1032 |
neg_numeral_less_zero not_zero_less_neg_numeral |
|
1033 |
neg_numeral_less_one not_one_less_neg_numeral |
|
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
1034 |
neg_one_less_numeral not_numeral_less_neg_one |
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
1035 |
neg_numeral_less_neg_one_iff not_neg_one_less_neg_numeral |
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
1036 |
|
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
1037 |
lemma less_minus_one_simps [simp]: |
81980 | 1038 |
\<open>- 1 < 0\<close> |
1039 |
\<open>- 1 < 1\<close> |
|
1040 |
\<open>\<not> 0 < - 1\<close> |
|
1041 |
\<open>\<not> 1 < - 1\<close> |
|
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
1042 |
by (simp_all add: less_le) |
47108 | 1043 |
|
81980 | 1044 |
lemma abs_numeral [simp]: \<open>\<bar>numeral n\<bar> = numeral n\<close> |
47108 | 1045 |
by simp |
1046 |
||
81980 | 1047 |
lemma abs_neg_numeral [simp]: \<open>\<bar>- numeral n\<bar> = numeral n\<close> |
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
1048 |
by (simp only: abs_minus_cancel abs_numeral) |
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
1049 |
|
81980 | 1050 |
lemma abs_neg_one [simp]: \<open>\<bar>- 1\<bar> = 1\<close> |
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
1051 |
by simp |
47108 | 1052 |
|
1053 |
end |
|
1054 |
||
63654 | 1055 |
|
1056 |
subsubsection \<open>Natural numbers\<close> |
|
47108 | 1057 |
|
67959 | 1058 |
lemma numeral_num_of_nat: |
81980 | 1059 |
\<open>numeral (num_of_nat n) = n\<close> if \<open>n > 0\<close> |
67959 | 1060 |
using that nat_of_num_numeral num_of_nat_inverse by simp |
1061 |
||
81980 | 1062 |
lemma Suc_1 [simp]: \<open>Suc 1 = 2\<close> |
47299 | 1063 |
unfolding Suc_eq_plus1 by (rule one_add_one) |
1064 |
||
81980 | 1065 |
lemma Suc_numeral [simp]: \<open>Suc (numeral n) = numeral (n + One)\<close> |
47299 | 1066 |
unfolding Suc_eq_plus1 by (rule numeral_plus_one) |
47108 | 1067 |
|
81980 | 1068 |
definition pred_numeral :: \<open>num \<Rightarrow> nat\<close> |
1069 |
where \<open>pred_numeral k = numeral k - 1\<close> |
|
67959 | 1070 |
|
1071 |
declare [[code drop: pred_numeral]] |
|
47209
4893907fe872
add constant pred_numeral k = numeral k - (1::nat);
huffman
parents:
47207
diff
changeset
|
1072 |
|
81980 | 1073 |
lemma numeral_eq_Suc: \<open>numeral k = Suc (pred_numeral k)\<close> |
63654 | 1074 |
by (simp add: pred_numeral_def) |
47209
4893907fe872
add constant pred_numeral k = numeral k - (1::nat);
huffman
parents:
47207
diff
changeset
|
1075 |
|
47220
52426c62b5d0
replace lemmas eval_nat_numeral with a simpler reformulation
huffman
parents:
47218
diff
changeset
|
1076 |
lemma eval_nat_numeral: |
81980 | 1077 |
\<open>numeral One = Suc 0\<close> |
1078 |
\<open>numeral (Bit0 n) = Suc (numeral (BitM n))\<close> |
|
1079 |
\<open>numeral (Bit1 n) = Suc (numeral (Bit0 n))\<close> |
|
47108 | 1080 |
by (simp_all add: numeral.simps BitM_plus_one) |
1081 |
||
47209
4893907fe872
add constant pred_numeral k = numeral k - (1::nat);
huffman
parents:
47207
diff
changeset
|
1082 |
lemma pred_numeral_simps [simp]: |
81980 | 1083 |
\<open>pred_numeral One = 0\<close> |
1084 |
\<open>pred_numeral (Bit0 k) = numeral (BitM k)\<close> |
|
1085 |
\<open>pred_numeral (Bit1 k) = numeral (Bit0 k)\<close> |
|
63654 | 1086 |
by (simp_all only: pred_numeral_def eval_nat_numeral diff_Suc_Suc diff_0) |
47209
4893907fe872
add constant pred_numeral k = numeral k - (1::nat);
huffman
parents:
47207
diff
changeset
|
1087 |
|
67959 | 1088 |
lemma pred_numeral_inc [simp]: |
81980 | 1089 |
\<open>pred_numeral (inc k) = numeral k\<close> |
67959 | 1090 |
by (simp only: pred_numeral_def numeral_inc diff_add_inverse2) |
1091 |
||
81980 | 1092 |
lemma numeral_2_eq_2: \<open>2 = Suc (Suc 0)\<close> |
47220
52426c62b5d0
replace lemmas eval_nat_numeral with a simpler reformulation
huffman
parents:
47218
diff
changeset
|
1093 |
by (simp add: eval_nat_numeral) |
47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
1094 |
|
81980 | 1095 |
lemma numeral_3_eq_3: \<open>3 = Suc (Suc (Suc 0))\<close> |
47220
52426c62b5d0
replace lemmas eval_nat_numeral with a simpler reformulation
huffman
parents:
47218
diff
changeset
|
1096 |
by (simp add: eval_nat_numeral) |
47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
1097 |
|
81980 | 1098 |
lemma numeral_1_eq_Suc_0: \<open>Numeral1 = Suc 0\<close> |
47207
9368aa814518
move lemmas from Nat_Numeral to Int.thy and Num.thy
huffman
parents:
47192
diff
changeset
|
1099 |
by (simp only: numeral_One One_nat_def) |
9368aa814518
move lemmas from Nat_Numeral to Int.thy and Num.thy
huffman
parents:
47192
diff
changeset
|
1100 |
|
81980 | 1101 |
lemma Suc_nat_number_of_add: \<open>Suc (numeral v + n) = numeral (v + One) + n\<close> |
47207
9368aa814518
move lemmas from Nat_Numeral to Int.thy and Num.thy
huffman
parents:
47192
diff
changeset
|
1102 |
by simp |
9368aa814518
move lemmas from Nat_Numeral to Int.thy and Num.thy
huffman
parents:
47192
diff
changeset
|
1103 |
|
81980 | 1104 |
lemma numerals: \<open>Numeral1 = (1::nat)\<close> \<open>2 = Suc (Suc 0)\<close> |
63654 | 1105 |
by (rule numeral_One) (rule numeral_2_eq_2) |
47207
9368aa814518
move lemmas from Nat_Numeral to Int.thy and Num.thy
huffman
parents:
47192
diff
changeset
|
1106 |
|
63913 | 1107 |
lemmas numeral_nat = eval_nat_numeral BitM.simps One_nat_def |
1108 |
||
69593 | 1109 |
text \<open>Comparisons involving \<^term>\<open>Suc\<close>.\<close> |
47209
4893907fe872
add constant pred_numeral k = numeral k - (1::nat);
huffman
parents:
47207
diff
changeset
|
1110 |
|
81980 | 1111 |
lemma eq_numeral_Suc [simp]: \<open>numeral k = Suc n \<longleftrightarrow> pred_numeral k = n\<close> |
47209
4893907fe872
add constant pred_numeral k = numeral k - (1::nat);
huffman
parents:
47207
diff
changeset
|
1112 |
by (simp add: numeral_eq_Suc) |
4893907fe872
add constant pred_numeral k = numeral k - (1::nat);
huffman
parents:
47207
diff
changeset
|
1113 |
|
81980 | 1114 |
lemma Suc_eq_numeral [simp]: \<open>Suc n = numeral k \<longleftrightarrow> n = pred_numeral k\<close> |
47209
4893907fe872
add constant pred_numeral k = numeral k - (1::nat);
huffman
parents:
47207
diff
changeset
|
1115 |
by (simp add: numeral_eq_Suc) |
4893907fe872
add constant pred_numeral k = numeral k - (1::nat);
huffman
parents:
47207
diff
changeset
|
1116 |
|
81980 | 1117 |
lemma less_numeral_Suc [simp]: \<open>numeral k < Suc n \<longleftrightarrow> pred_numeral k < n\<close> |
47209
4893907fe872
add constant pred_numeral k = numeral k - (1::nat);
huffman
parents:
47207
diff
changeset
|
1118 |
by (simp add: numeral_eq_Suc) |
4893907fe872
add constant pred_numeral k = numeral k - (1::nat);
huffman
parents:
47207
diff
changeset
|
1119 |
|
81980 | 1120 |
lemma less_Suc_numeral [simp]: \<open>Suc n < numeral k \<longleftrightarrow> n < pred_numeral k\<close> |
47209
4893907fe872
add constant pred_numeral k = numeral k - (1::nat);
huffman
parents:
47207
diff
changeset
|
1121 |
by (simp add: numeral_eq_Suc) |
4893907fe872
add constant pred_numeral k = numeral k - (1::nat);
huffman
parents:
47207
diff
changeset
|
1122 |
|
81980 | 1123 |
lemma le_numeral_Suc [simp]: \<open>numeral k \<le> Suc n \<longleftrightarrow> pred_numeral k \<le> n\<close> |
47209
4893907fe872
add constant pred_numeral k = numeral k - (1::nat);
huffman
parents:
47207
diff
changeset
|
1124 |
by (simp add: numeral_eq_Suc) |
4893907fe872
add constant pred_numeral k = numeral k - (1::nat);
huffman
parents:
47207
diff
changeset
|
1125 |
|
81980 | 1126 |
lemma le_Suc_numeral [simp]: \<open>Suc n \<le> numeral k \<longleftrightarrow> n \<le> pred_numeral k\<close> |
47209
4893907fe872
add constant pred_numeral k = numeral k - (1::nat);
huffman
parents:
47207
diff
changeset
|
1127 |
by (simp add: numeral_eq_Suc) |
4893907fe872
add constant pred_numeral k = numeral k - (1::nat);
huffman
parents:
47207
diff
changeset
|
1128 |
|
81980 | 1129 |
lemma diff_Suc_numeral [simp]: \<open>Suc n - numeral k = n - pred_numeral k\<close> |
47218
2b652cbadde1
new lemmas for simplifying subtraction on nat numerals
huffman
parents:
47216
diff
changeset
|
1130 |
by (simp add: numeral_eq_Suc) |
2b652cbadde1
new lemmas for simplifying subtraction on nat numerals
huffman
parents:
47216
diff
changeset
|
1131 |
|
81980 | 1132 |
lemma diff_numeral_Suc [simp]: \<open>numeral k - Suc n = pred_numeral k - n\<close> |
47218
2b652cbadde1
new lemmas for simplifying subtraction on nat numerals
huffman
parents:
47216
diff
changeset
|
1133 |
by (simp add: numeral_eq_Suc) |
2b652cbadde1
new lemmas for simplifying subtraction on nat numerals
huffman
parents:
47216
diff
changeset
|
1134 |
|
81980 | 1135 |
lemma max_Suc_numeral [simp]: \<open>max (Suc n) (numeral k) = Suc (max n (pred_numeral k))\<close> |
47209
4893907fe872
add constant pred_numeral k = numeral k - (1::nat);
huffman
parents:
47207
diff
changeset
|
1136 |
by (simp add: numeral_eq_Suc) |
4893907fe872
add constant pred_numeral k = numeral k - (1::nat);
huffman
parents:
47207
diff
changeset
|
1137 |
|
81980 | 1138 |
lemma max_numeral_Suc [simp]: \<open>max (numeral k) (Suc n) = Suc (max (pred_numeral k) n)\<close> |
47209
4893907fe872
add constant pred_numeral k = numeral k - (1::nat);
huffman
parents:
47207
diff
changeset
|
1139 |
by (simp add: numeral_eq_Suc) |
4893907fe872
add constant pred_numeral k = numeral k - (1::nat);
huffman
parents:
47207
diff
changeset
|
1140 |
|
81980 | 1141 |
lemma min_Suc_numeral [simp]: \<open>min (Suc n) (numeral k) = Suc (min n (pred_numeral k))\<close> |
47209
4893907fe872
add constant pred_numeral k = numeral k - (1::nat);
huffman
parents:
47207
diff
changeset
|
1142 |
by (simp add: numeral_eq_Suc) |
4893907fe872
add constant pred_numeral k = numeral k - (1::nat);
huffman
parents:
47207
diff
changeset
|
1143 |
|
81980 | 1144 |
lemma min_numeral_Suc [simp]: \<open>min (numeral k) (Suc n) = Suc (min (pred_numeral k) n)\<close> |
47209
4893907fe872
add constant pred_numeral k = numeral k - (1::nat);
huffman
parents:
47207
diff
changeset
|
1145 |
by (simp add: numeral_eq_Suc) |
4893907fe872
add constant pred_numeral k = numeral k - (1::nat);
huffman
parents:
47207
diff
changeset
|
1146 |
|
69593 | 1147 |
text \<open>For \<^term>\<open>case_nat\<close> and \<^term>\<open>rec_nat\<close>.\<close> |
47216
4d0878d54ca5
move more theorems from Nat_Numeral.thy to Num.thy
huffman
parents:
47211
diff
changeset
|
1148 |
|
81980 | 1149 |
lemma case_nat_numeral [simp]: \<open>case_nat a f (numeral v) = (let pv = pred_numeral v in f pv)\<close> |
47216
4d0878d54ca5
move more theorems from Nat_Numeral.thy to Num.thy
huffman
parents:
47211
diff
changeset
|
1150 |
by (simp add: numeral_eq_Suc) |
4d0878d54ca5
move more theorems from Nat_Numeral.thy to Num.thy
huffman
parents:
47211
diff
changeset
|
1151 |
|
55415 | 1152 |
lemma case_nat_add_eq_if [simp]: |
81980 | 1153 |
\<open>case_nat a f ((numeral v) + n) = (let pv = pred_numeral v in f (pv + n))\<close> |
47216
4d0878d54ca5
move more theorems from Nat_Numeral.thy to Num.thy
huffman
parents:
47211
diff
changeset
|
1154 |
by (simp add: numeral_eq_Suc) |
4d0878d54ca5
move more theorems from Nat_Numeral.thy to Num.thy
huffman
parents:
47211
diff
changeset
|
1155 |
|
55415 | 1156 |
lemma rec_nat_numeral [simp]: |
81980 | 1157 |
\<open>rec_nat a f (numeral v) = (let pv = pred_numeral v in f pv (rec_nat a f pv))\<close> |
47216
4d0878d54ca5
move more theorems from Nat_Numeral.thy to Num.thy
huffman
parents:
47211
diff
changeset
|
1158 |
by (simp add: numeral_eq_Suc Let_def) |
4d0878d54ca5
move more theorems from Nat_Numeral.thy to Num.thy
huffman
parents:
47211
diff
changeset
|
1159 |
|
55415 | 1160 |
lemma rec_nat_add_eq_if [simp]: |
81980 | 1161 |
\<open>rec_nat a f (numeral v + n) = (let pv = pred_numeral v in f (pv + n) (rec_nat a f (pv + n)))\<close> |
47216
4d0878d54ca5
move more theorems from Nat_Numeral.thy to Num.thy
huffman
parents:
47211
diff
changeset
|
1162 |
by (simp add: numeral_eq_Suc Let_def) |
4d0878d54ca5
move more theorems from Nat_Numeral.thy to Num.thy
huffman
parents:
47211
diff
changeset
|
1163 |
|
69593 | 1164 |
text \<open>Case analysis on \<^term>\<open>n < 2\<close>.\<close> |
81980 | 1165 |
lemma less_2_cases: \<open>n < 2 \<Longrightarrow> n = 0 \<or> n = Suc 0\<close> |
47255
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47228
diff
changeset
|
1166 |
by (auto simp add: numeral_2_eq_2) |
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47228
diff
changeset
|
1167 |
|
81980 | 1168 |
lemma less_2_cases_iff: \<open>n < 2 \<longleftrightarrow> n = 0 \<or> n = Suc 0\<close> |
71452 | 1169 |
by (auto simp add: numeral_2_eq_2) |
1170 |
||
63654 | 1171 |
text \<open>Removal of Small Numerals: 0, 1 and (in additive positions) 2.\<close> |
71452 | 1172 |
text \<open>bh: Are these rules really a good idea? LCP: well, it already happens for 0 and 1!\<close> |
47255
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47228
diff
changeset
|
1173 |
|
81980 | 1174 |
lemma add_2_eq_Suc [simp]: \<open>2 + n = Suc (Suc n)\<close> |
47255
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47228
diff
changeset
|
1175 |
by simp |
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47228
diff
changeset
|
1176 |
|
81980 | 1177 |
lemma add_2_eq_Suc' [simp]: \<open>n + 2 = Suc (Suc n)\<close> |
47255
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47228
diff
changeset
|
1178 |
by simp |
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47228
diff
changeset
|
1179 |
|
60758 | 1180 |
text \<open>Can be used to eliminate long strings of Sucs, but not by default.\<close> |
81980 | 1181 |
lemma Suc3_eq_add_3: \<open>Suc (Suc (Suc n)) = 3 + n\<close> |
47255
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47228
diff
changeset
|
1182 |
by simp |
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47228
diff
changeset
|
1183 |
|
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47228
diff
changeset
|
1184 |
lemmas nat_1_add_1 = one_add_one [where 'a=nat] (* legacy *) |
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47228
diff
changeset
|
1185 |
|
71760 | 1186 |
context semiring_numeral |
1187 |
begin |
|
1188 |
||
1189 |
lemma numeral_add_unfold_funpow: |
|
1190 |
\<open>numeral k + a = ((+) 1 ^^ numeral k) a\<close> |
|
1191 |
proof (rule sym, induction k arbitrary: a) |
|
1192 |
case One |
|
1193 |
then show ?case |
|
81980 | 1194 |
by (simp add: Num.numeral_One numeral_One) |
71760 | 1195 |
next |
1196 |
case (Bit0 k) |
|
1197 |
then show ?case |
|
81980 | 1198 |
by (simp add: Num.numeral_Bit0 numeral_Bit0 ac_simps funpow_add) |
71760 | 1199 |
next |
1200 |
case (Bit1 k) |
|
1201 |
then show ?case |
|
81980 | 1202 |
by (simp add: Num.numeral_Bit1 numeral_Bit1 ac_simps funpow_add) |
71760 | 1203 |
qed |
1204 |
||
1205 |
end |
|
1206 |
||
1207 |
context semiring_1 |
|
1208 |
begin |
|
1209 |
||
1210 |
lemma numeral_unfold_funpow: |
|
1211 |
\<open>numeral k = ((+) 1 ^^ numeral k) 0\<close> |
|
1212 |
using numeral_add_unfold_funpow [of k 0] by simp |
|
1213 |
||
1214 |
end |
|
1215 |
||
1216 |
context |
|
1217 |
includes lifting_syntax |
|
1218 |
begin |
|
1219 |
||
1220 |
lemma transfer_rule_numeral: |
|
1221 |
\<open>((=) ===> R) numeral numeral\<close> |
|
1222 |
if [transfer_rule]: \<open>R 0 0\<close> \<open>R 1 1\<close> |
|
1223 |
\<open>(R ===> R ===> R) (+) (+)\<close> |
|
1224 |
for R :: \<open>'a::{semiring_numeral,monoid_add} \<Rightarrow> 'b::{semiring_numeral,monoid_add} \<Rightarrow> bool\<close> |
|
1225 |
proof - |
|
81980 | 1226 |
have \<open>((=) ===> R) (\<lambda>k. ((+) 1 ^^ numeral k) 0) (\<lambda>k. ((+) 1 ^^ numeral k) 0)\<close> |
71760 | 1227 |
by transfer_prover |
1228 |
moreover have \<open>numeral = (\<lambda>k. ((+) (1::'a) ^^ numeral k) 0)\<close> |
|
1229 |
using numeral_add_unfold_funpow [where ?'a = 'a, of _ 0] |
|
1230 |
by (simp add: fun_eq_iff) |
|
1231 |
moreover have \<open>numeral = (\<lambda>k. ((+) (1::'b) ^^ numeral k) 0)\<close> |
|
1232 |
using numeral_add_unfold_funpow [where ?'a = 'b, of _ 0] |
|
1233 |
by (simp add: fun_eq_iff) |
|
1234 |
ultimately show ?thesis |
|
1235 |
by simp |
|
1236 |
qed |
|
1237 |
||
1238 |
end |
|
1239 |
||
47108 | 1240 |
|
69593 | 1241 |
subsection \<open>Particular lemmas concerning \<^term>\<open>2\<close>\<close> |
58512
dc4d76dfa8f0
moved lemmas out of Int.thy which have nothing to do with int
haftmann
parents:
58421
diff
changeset
|
1242 |
|
59867
58043346ca64
given up separate type classes demanding `inverse 0 = 0`
haftmann
parents:
59621
diff
changeset
|
1243 |
context linordered_field |
58512
dc4d76dfa8f0
moved lemmas out of Int.thy which have nothing to do with int
haftmann
parents:
58421
diff
changeset
|
1244 |
begin |
dc4d76dfa8f0
moved lemmas out of Int.thy which have nothing to do with int
haftmann
parents:
58421
diff
changeset
|
1245 |
|
62348 | 1246 |
subclass field_char_0 .. |
1247 |
||
81980 | 1248 |
lemma half_gt_zero_iff: \<open>0 < a / 2 \<longleftrightarrow> 0 < a\<close> |
58512
dc4d76dfa8f0
moved lemmas out of Int.thy which have nothing to do with int
haftmann
parents:
58421
diff
changeset
|
1249 |
by (auto simp add: field_simps) |
dc4d76dfa8f0
moved lemmas out of Int.thy which have nothing to do with int
haftmann
parents:
58421
diff
changeset
|
1250 |
|
81980 | 1251 |
lemma half_gt_zero [simp]: \<open>0 < a \<Longrightarrow> 0 < a / 2\<close> |
58512
dc4d76dfa8f0
moved lemmas out of Int.thy which have nothing to do with int
haftmann
parents:
58421
diff
changeset
|
1252 |
by (simp add: half_gt_zero_iff) |
dc4d76dfa8f0
moved lemmas out of Int.thy which have nothing to do with int
haftmann
parents:
58421
diff
changeset
|
1253 |
|
dc4d76dfa8f0
moved lemmas out of Int.thy which have nothing to do with int
haftmann
parents:
58421
diff
changeset
|
1254 |
end |
dc4d76dfa8f0
moved lemmas out of Int.thy which have nothing to do with int
haftmann
parents:
58421
diff
changeset
|
1255 |
|
dc4d76dfa8f0
moved lemmas out of Int.thy which have nothing to do with int
haftmann
parents:
58421
diff
changeset
|
1256 |
|
60758 | 1257 |
subsection \<open>Numeral equations as default simplification rules\<close> |
47108 | 1258 |
|
1259 |
declare (in numeral) numeral_One [simp] |
|
1260 |
declare (in numeral) numeral_plus_numeral [simp] |
|
1261 |
declare (in numeral) add_numeral_special [simp] |
|
1262 |
declare (in neg_numeral) add_neg_numeral_simps [simp] |
|
1263 |
declare (in neg_numeral) add_neg_numeral_special [simp] |
|
1264 |
declare (in neg_numeral) diff_numeral_simps [simp] |
|
1265 |
declare (in neg_numeral) diff_numeral_special [simp] |
|
1266 |
declare (in semiring_numeral) numeral_times_numeral [simp] |
|
1267 |
declare (in ring_1) mult_neg_numeral_simps [simp] |
|
1268 |
||
67116 | 1269 |
|
1270 |
subsubsection \<open>Special Simplification for Constants\<close> |
|
1271 |
||
1272 |
text \<open>These distributive laws move literals inside sums and differences.\<close> |
|
1273 |
||
81980 | 1274 |
lemmas distrib_right_numeral [simp] = distrib_right [of _ _ \<open>numeral v\<close>] for v |
1275 |
lemmas distrib_left_numeral [simp] = distrib_left [of \<open>numeral v\<close>] for v |
|
1276 |
lemmas left_diff_distrib_numeral [simp] = left_diff_distrib [of _ _ \<open>numeral v\<close>] for v |
|
1277 |
lemmas right_diff_distrib_numeral [simp] = right_diff_distrib [of \<open>numeral v\<close>] for v |
|
67116 | 1278 |
|
1279 |
text \<open>These are actually for fields, like real\<close> |
|
1280 |
||
81980 | 1281 |
lemmas zero_less_divide_iff_numeral [simp, no_atp] = zero_less_divide_iff [of \<open>numeral w\<close>] for w |
1282 |
lemmas divide_less_0_iff_numeral [simp, no_atp] = divide_less_0_iff [of \<open>numeral w\<close>] for w |
|
1283 |
lemmas zero_le_divide_iff_numeral [simp, no_atp] = zero_le_divide_iff [of \<open>numeral w\<close>] for w |
|
1284 |
lemmas divide_le_0_iff_numeral [simp, no_atp] = divide_le_0_iff [of \<open>numeral w\<close>] for w |
|
67116 | 1285 |
|
1286 |
text \<open>Replaces \<open>inverse #nn\<close> by \<open>1/#nn\<close>. It looks |
|
1287 |
strange, but then other simprocs simplify the quotient.\<close> |
|
1288 |
||
1289 |
lemmas inverse_eq_divide_numeral [simp] = |
|
81980 | 1290 |
inverse_eq_divide [of \<open>numeral w\<close>] for w |
67116 | 1291 |
|
1292 |
lemmas inverse_eq_divide_neg_numeral [simp] = |
|
81980 | 1293 |
inverse_eq_divide [of \<open>- numeral w\<close>] for w |
67116 | 1294 |
|
1295 |
text \<open>These laws simplify inequalities, moving unary minus from a term |
|
1296 |
into the literal.\<close> |
|
1297 |
||
1298 |
lemmas equation_minus_iff_numeral [no_atp] = |
|
81980 | 1299 |
equation_minus_iff [of \<open>numeral v\<close>] for v |
67116 | 1300 |
|
1301 |
lemmas minus_equation_iff_numeral [no_atp] = |
|
81980 | 1302 |
minus_equation_iff [of _ \<open>numeral v\<close>] for v |
67116 | 1303 |
|
1304 |
lemmas le_minus_iff_numeral [no_atp] = |
|
81980 | 1305 |
le_minus_iff [of \<open>numeral v\<close>] for v |
67116 | 1306 |
|
1307 |
lemmas minus_le_iff_numeral [no_atp] = |
|
81980 | 1308 |
minus_le_iff [of _ \<open>numeral v\<close>] for v |
67116 | 1309 |
|
1310 |
lemmas less_minus_iff_numeral [no_atp] = |
|
81980 | 1311 |
less_minus_iff [of \<open>numeral v\<close>] for v |
67116 | 1312 |
|
1313 |
lemmas minus_less_iff_numeral [no_atp] = |
|
81980 | 1314 |
minus_less_iff [of _ \<open>numeral v\<close>] for v |
67116 | 1315 |
|
1316 |
(* FIXME maybe simproc *) |
|
1317 |
||
1318 |
text \<open>Cancellation of constant factors in comparisons (\<open><\<close> and \<open>\<le>\<close>)\<close> |
|
1319 |
||
81980 | 1320 |
lemmas mult_less_cancel_left_numeral [simp, no_atp] = mult_less_cancel_left [of \<open>numeral v\<close>] for v |
1321 |
lemmas mult_less_cancel_right_numeral [simp, no_atp] = mult_less_cancel_right [of _ \<open>numeral v\<close>] for v |
|
1322 |
lemmas mult_le_cancel_left_numeral [simp, no_atp] = mult_le_cancel_left [of \<open>numeral v\<close>] for v |
|
1323 |
lemmas mult_le_cancel_right_numeral [simp, no_atp] = mult_le_cancel_right [of _ \<open>numeral v\<close>] for v |
|
67116 | 1324 |
|
1325 |
text \<open>Multiplying out constant divisors in comparisons (\<open><\<close>, \<open>\<le>\<close> and \<open>=\<close>)\<close> |
|
1326 |
||
81980 | 1327 |
named_theorems divide_const_simps \<open>simplification rules to simplify comparisons involving constant divisors\<close> |
67116 | 1328 |
|
1329 |
lemmas le_divide_eq_numeral1 [simp,divide_const_simps] = |
|
81980 | 1330 |
pos_le_divide_eq [of \<open>numeral w\<close>, OF zero_less_numeral] |
1331 |
neg_le_divide_eq [of \<open>- numeral w\<close>, OF neg_numeral_less_zero] for w |
|
67116 | 1332 |
|
1333 |
lemmas divide_le_eq_numeral1 [simp,divide_const_simps] = |
|
81980 | 1334 |
pos_divide_le_eq [of \<open>numeral w\<close>, OF zero_less_numeral] |
1335 |
neg_divide_le_eq [of \<open>- numeral w\<close>, OF neg_numeral_less_zero] for w |
|
67116 | 1336 |
|
1337 |
lemmas less_divide_eq_numeral1 [simp,divide_const_simps] = |
|
81980 | 1338 |
pos_less_divide_eq [of \<open>numeral w\<close>, OF zero_less_numeral] |
1339 |
neg_less_divide_eq [of \<open>- numeral w\<close>, OF neg_numeral_less_zero] for w |
|
67116 | 1340 |
|
1341 |
lemmas divide_less_eq_numeral1 [simp,divide_const_simps] = |
|
81980 | 1342 |
pos_divide_less_eq [of \<open>numeral w\<close>, OF zero_less_numeral] |
1343 |
neg_divide_less_eq [of \<open>- numeral w\<close>, OF neg_numeral_less_zero] for w |
|
67116 | 1344 |
|
1345 |
lemmas eq_divide_eq_numeral1 [simp,divide_const_simps] = |
|
81980 | 1346 |
eq_divide_eq [of _ _ \<open>numeral w\<close>] |
1347 |
eq_divide_eq [of _ _ \<open>- numeral w\<close>] for w |
|
67116 | 1348 |
|
1349 |
lemmas divide_eq_eq_numeral1 [simp,divide_const_simps] = |
|
81980 | 1350 |
divide_eq_eq [of _ \<open>numeral w\<close>] |
1351 |
divide_eq_eq [of _ \<open>- numeral w\<close>] for w |
|
67116 | 1352 |
|
1353 |
||
1354 |
subsubsection \<open>Optional Simplification Rules Involving Constants\<close> |
|
1355 |
||
1356 |
text \<open>Simplify quotients that are compared with a literal constant.\<close> |
|
1357 |
||
1358 |
lemmas le_divide_eq_numeral [divide_const_simps] = |
|
81980 | 1359 |
le_divide_eq [of \<open>numeral w\<close>] |
1360 |
le_divide_eq [of \<open>- numeral w\<close>] for w |
|
67116 | 1361 |
|
1362 |
lemmas divide_le_eq_numeral [divide_const_simps] = |
|
81980 | 1363 |
divide_le_eq [of _ _ \<open>numeral w\<close>] |
1364 |
divide_le_eq [of _ _ \<open>- numeral w\<close>] for w |
|
67116 | 1365 |
|
1366 |
lemmas less_divide_eq_numeral [divide_const_simps] = |
|
81980 | 1367 |
less_divide_eq [of \<open>numeral w\<close>] |
1368 |
less_divide_eq [of \<open>- numeral w\<close>] for w |
|
67116 | 1369 |
|
1370 |
lemmas divide_less_eq_numeral [divide_const_simps] = |
|
81980 | 1371 |
divide_less_eq [of _ _ \<open>numeral w\<close>] |
1372 |
divide_less_eq [of _ _ \<open>- numeral w\<close>] for w |
|
67116 | 1373 |
|
1374 |
lemmas eq_divide_eq_numeral [divide_const_simps] = |
|
81980 | 1375 |
eq_divide_eq [of \<open>numeral w\<close>] |
1376 |
eq_divide_eq [of \<open>- numeral w\<close>] for w |
|
67116 | 1377 |
|
1378 |
lemmas divide_eq_eq_numeral [divide_const_simps] = |
|
81980 | 1379 |
divide_eq_eq [of _ _ \<open>numeral w\<close>] |
1380 |
divide_eq_eq [of _ _ \<open>- numeral w\<close>] for w |
|
67116 | 1381 |
|
1382 |
text \<open>Not good as automatic simprules because they cause case splits.\<close> |
|
1383 |
||
1384 |
lemmas [divide_const_simps] = |
|
1385 |
le_divide_eq_1 divide_le_eq_1 less_divide_eq_1 divide_less_eq_1 |
|
1386 |
||
1387 |
||
60758 | 1388 |
subsection \<open>Setting up simprocs\<close> |
47108 | 1389 |
|
81980 | 1390 |
lemma mult_numeral_1: \<open>Numeral1 * a = a\<close> |
1391 |
for a :: \<open>'a::semiring_numeral\<close> |
|
47108 | 1392 |
by simp |
1393 |
||
81980 | 1394 |
lemma mult_numeral_1_right: \<open>a * Numeral1 = a\<close> |
1395 |
for a :: \<open>'a::semiring_numeral\<close> |
|
47108 | 1396 |
by simp |
1397 |
||
81980 | 1398 |
lemma divide_numeral_1: \<open>a / Numeral1 = a\<close> |
1399 |
for a :: \<open>'a::field\<close> |
|
47108 | 1400 |
by simp |
1401 |
||
81980 | 1402 |
lemma inverse_numeral_1: \<open>inverse Numeral1 = (Numeral1::'a::division_ring)\<close> |
47108 | 1403 |
by simp |
1404 |
||
63654 | 1405 |
text \<open> |
1406 |
Theorem lists for the cancellation simprocs. The use of a binary |
|
1407 |
numeral for 1 reduces the number of special cases. |
|
1408 |
\<close> |
|
47108 | 1409 |
|
68536 | 1410 |
lemma mult_1s_semiring_numeral: |
81980 | 1411 |
\<open>Numeral1 * a = a\<close> |
1412 |
\<open>a * Numeral1 = a\<close> |
|
1413 |
for a :: \<open>'a::semiring_numeral\<close> |
|
68536 | 1414 |
by simp_all |
1415 |
||
1416 |
lemma mult_1s_ring_1: |
|
81980 | 1417 |
\<open>- Numeral1 * b = - b\<close> |
1418 |
\<open>b * - Numeral1 = - b\<close> |
|
1419 |
for b :: \<open>'a::ring_1\<close> |
|
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
1420 |
by simp_all |
47108 | 1421 |
|
68536 | 1422 |
lemmas mult_1s = mult_1s_semiring_numeral mult_1s_ring_1 |
1423 |
||
60758 | 1424 |
setup \<open> |
47226 | 1425 |
Reorient_Proc.add |
69593 | 1426 |
(fn Const (\<^const_name>\<open>numeral\<close>, _) $ _ => true |
1427 |
| Const (\<^const_name>\<open>uminus\<close>, _) $ (Const (\<^const_name>\<open>numeral\<close>, _) $ _) => true |
|
63654 | 1428 |
| _ => false) |
60758 | 1429 |
\<close> |
47226 | 1430 |
|
81980 | 1431 |
simproc_setup reorient_numeral (\<open>numeral w = x\<close> | \<open>- numeral w = y\<close>) = |
78099
4d9349989d94
more uniform simproc_setup: avoid vacuous abstraction over morphism, which sometimes captures context values in its functional closure;
wenzelm
parents:
75669
diff
changeset
|
1432 |
\<open>K Reorient_Proc.proc\<close> |
47226 | 1433 |
|
47108 | 1434 |
|
63654 | 1435 |
subsubsection \<open>Simplification of arithmetic operations on integer constants\<close> |
47108 | 1436 |
|
1437 |
lemmas arith_special = (* already declared simp above *) |
|
1438 |
add_numeral_special add_neg_numeral_special |
|
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
1439 |
diff_numeral_special |
47108 | 1440 |
|
63654 | 1441 |
lemmas arith_extra_simps = (* rules already in simpset *) |
47108 | 1442 |
numeral_plus_numeral add_neg_numeral_simps add_0_left add_0_right |
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
1443 |
minus_zero |
47108 | 1444 |
diff_numeral_simps diff_0 diff_0_right |
1445 |
numeral_times_numeral mult_neg_numeral_simps |
|
1446 |
mult_zero_left mult_zero_right |
|
1447 |
abs_numeral abs_neg_numeral |
|
1448 |
||
60758 | 1449 |
text \<open> |
47108 | 1450 |
For making a minimal simpset, one must include these default simprules. |
61799 | 1451 |
Also include \<open>simp_thms\<close>. |
60758 | 1452 |
\<close> |
47108 | 1453 |
|
1454 |
lemmas arith_simps = |
|
1455 |
add_num_simps mult_num_simps sub_num_simps |
|
1456 |
BitM.simps dbl_simps dbl_inc_simps dbl_dec_simps |
|
1457 |
abs_zero abs_one arith_extra_simps |
|
1458 |
||
54249 | 1459 |
lemmas more_arith_simps = |
1460 |
neg_le_iff_le |
|
1461 |
minus_zero left_minus right_minus |
|
1462 |
mult_1_left mult_1_right |
|
1463 |
mult_minus_left mult_minus_right |
|
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
55974
diff
changeset
|
1464 |
minus_add_distrib minus_minus mult.assoc |
54249 | 1465 |
|
1466 |
lemmas of_nat_simps = |
|
1467 |
of_nat_0 of_nat_1 of_nat_Suc of_nat_add of_nat_mult |
|
1468 |
||
63654 | 1469 |
text \<open>Simplification of relational operations.\<close> |
47108 | 1470 |
|
1471 |
lemmas eq_numeral_extra = |
|
1472 |
zero_neq_one one_neq_zero |
|
1473 |
||
1474 |
lemmas rel_simps = |
|
1475 |
le_num_simps less_num_simps eq_num_simps |
|
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
1476 |
le_numeral_simps le_neg_numeral_simps le_minus_one_simps le_numeral_extra |
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54249
diff
changeset
|
1477 |
less_numeral_simps less_neg_numeral_simps less_minus_one_simps less_numeral_extra |
47108 | 1478 |
eq_numeral_simps eq_neg_numeral_simps eq_numeral_extra |
1479 |
||
81980 | 1480 |
lemma Let_numeral [simp]: \<open>Let (numeral v) f = f (numeral v)\<close> |
61799 | 1481 |
\<comment> \<open>Unfold all \<open>let\<close>s involving constants\<close> |
54249 | 1482 |
unfolding Let_def .. |
1483 |
||
81980 | 1484 |
lemma Let_neg_numeral [simp]: \<open>Let (- numeral v) f = f (- numeral v)\<close> |
61799 | 1485 |
\<comment> \<open>Unfold all \<open>let\<close>s involving constants\<close> |
54249 | 1486 |
unfolding Let_def .. |
1487 |
||
60758 | 1488 |
declaration \<open> |
63654 | 1489 |
let |
59996 | 1490 |
fun number_of ctxt T n = |
69593 | 1491 |
if not (Sign.of_sort (Proof_Context.theory_of ctxt) (T, \<^sort>\<open>numeral\<close>)) |
54249 | 1492 |
then raise CTERM ("number_of", []) |
59996 | 1493 |
else Numeral.mk_cnumber (Thm.ctyp_of ctxt T) n; |
54249 | 1494 |
in |
1495 |
K ( |
|
70356
4a327c061870
streamlined setup for linear algebra, particularly removed redundant rule declarations
haftmann
parents:
70270
diff
changeset
|
1496 |
Lin_Arith.set_number_of number_of |
63654 | 1497 |
#> Lin_Arith.add_simps |
70356
4a327c061870
streamlined setup for linear algebra, particularly removed redundant rule declarations
haftmann
parents:
70270
diff
changeset
|
1498 |
@{thms arith_simps more_arith_simps rel_simps pred_numeral_simps |
4a327c061870
streamlined setup for linear algebra, particularly removed redundant rule declarations
haftmann
parents:
70270
diff
changeset
|
1499 |
arith_special numeral_One of_nat_simps uminus_numeral_One |
4a327c061870
streamlined setup for linear algebra, particularly removed redundant rule declarations
haftmann
parents:
70270
diff
changeset
|
1500 |
Suc_numeral Let_numeral Let_neg_numeral Let_0 Let_1 |
63654 | 1501 |
le_Suc_numeral le_numeral_Suc less_Suc_numeral less_numeral_Suc |
70356
4a327c061870
streamlined setup for linear algebra, particularly removed redundant rule declarations
haftmann
parents:
70270
diff
changeset
|
1502 |
Suc_eq_numeral eq_numeral_Suc mult_Suc mult_Suc_right of_nat_numeral}) |
54249 | 1503 |
end |
60758 | 1504 |
\<close> |
54249 | 1505 |
|
47108 | 1506 |
|
63654 | 1507 |
subsubsection \<open>Simplification of arithmetic when nested to the right\<close> |
47108 | 1508 |
|
81980 | 1509 |
lemma add_numeral_left [simp]: \<open>numeral v + (numeral w + z) = (numeral(v + w) + z)\<close> |
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
55974
diff
changeset
|
1510 |
by (simp_all add: add.assoc [symmetric]) |
47108 | 1511 |
|
1512 |
lemma add_neg_numeral_left [simp]: |
|
81980 | 1513 |
\<open>numeral v + (- numeral w + y) = (sub v w + y)\<close> |
1514 |
\<open>- numeral v + (numeral w + y) = (sub w v + y)\<close> |
|
1515 |
\<open>- numeral v + (- numeral w + y) = (- numeral(v + w) + y)\<close> |
|
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
55974
diff
changeset
|
1516 |
by (simp_all add: add.assoc [symmetric]) |
47108 | 1517 |
|
68536 | 1518 |
lemma mult_numeral_left_semiring_numeral: |
81980 | 1519 |
\<open>numeral v * (numeral w * z) = (numeral(v * w) * z :: 'a::semiring_numeral)\<close> |
68536 | 1520 |
by (simp add: mult.assoc [symmetric]) |
1521 |
||
1522 |
lemma mult_numeral_left_ring_1: |
|
81980 | 1523 |
\<open>- numeral v * (numeral w * y) = (- numeral(v * w) * y :: 'a::ring_1)\<close> |
1524 |
\<open>numeral v * (- numeral w * y) = (- numeral(v * w) * y :: 'a::ring_1)\<close> |
|
1525 |
\<open>- numeral v * (- numeral w * y) = (numeral(v * w) * y :: 'a::ring_1)\<close> |
|
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
55974
diff
changeset
|
1526 |
by (simp_all add: mult.assoc [symmetric]) |
47108 | 1527 |
|
68536 | 1528 |
lemmas mult_numeral_left [simp] = |
1529 |
mult_numeral_left_semiring_numeral |
|
1530 |
mult_numeral_left_ring_1 |
|
1531 |
||
47108 | 1532 |
|
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
50817
diff
changeset
|
1533 |
|
63654 | 1534 |
subsection \<open>Code module namespace\<close> |
47108 | 1535 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52210
diff
changeset
|
1536 |
code_identifier |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52210
diff
changeset
|
1537 |
code_module Num \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith |
47108 | 1538 |
|
66283
adf3155c57e2
Printing natural numbers as numerals in evaluation
eberlm <eberlm@in.tum.de>
parents:
64238
diff
changeset
|
1539 |
subsection \<open>Printing of evaluated natural numbers as numerals\<close> |
adf3155c57e2
Printing natural numbers as numerals in evaluation
eberlm <eberlm@in.tum.de>
parents:
64238
diff
changeset
|
1540 |
|
adf3155c57e2
Printing natural numbers as numerals in evaluation
eberlm <eberlm@in.tum.de>
parents:
64238
diff
changeset
|
1541 |
lemma [code_post]: |
81980 | 1542 |
\<open>Suc 0 = 1\<close> |
1543 |
\<open>Suc 1 = 2\<close> |
|
1544 |
\<open>Suc (numeral n) = numeral (inc n)\<close> |
|
66283
adf3155c57e2
Printing natural numbers as numerals in evaluation
eberlm <eberlm@in.tum.de>
parents:
64238
diff
changeset
|
1545 |
by (simp_all add: numeral_inc) |
adf3155c57e2
Printing natural numbers as numerals in evaluation
eberlm <eberlm@in.tum.de>
parents:
64238
diff
changeset
|
1546 |
|
81980 | 1547 |
lemmas [code_post] = inc.simps |
66283
adf3155c57e2
Printing natural numbers as numerals in evaluation
eberlm <eberlm@in.tum.de>
parents:
64238
diff
changeset
|
1548 |
|
74592 | 1549 |
|
1550 |
subsection \<open>More on auxiliary conversion\<close> |
|
1551 |
||
1552 |
context semiring_1 |
|
1553 |
begin |
|
1554 |
||
1555 |
lemma num_of_nat_numeral_eq [simp]: |
|
1556 |
\<open>num_of_nat (numeral q) = q\<close> |
|
81980 | 1557 |
by (simp flip: nat_of_num_numeral add: nat_of_num_inverse) |
1558 |
||
1559 |
lemma numeral_num_of_nat_unfold: |
|
1560 |
\<open>numeral (num_of_nat n) = (if n = 0 then 1 else of_nat n)\<close> |
|
1561 |
apply (simp only: of_nat_numeral [symmetric, of \<open>num_of_nat n\<close>] flip: nat_of_num_numeral) |
|
1562 |
apply (auto simp add: num_of_nat_inverse) |
|
1563 |
done |
|
74592 | 1564 |
|
47108 | 1565 |
end |
74592 | 1566 |
|
81980 | 1567 |
|
1568 |
hide_const (open) One Bit0 Bit1 BitM inc pow sqr sub dbl dbl_inc dbl_dec |
|
1569 |
||
74592 | 1570 |
end |