author | huffman |
Tue, 13 Dec 2011 12:36:41 +0100 | |
changeset 45847 | b4254b2e2b4a |
parent 45846 | 518a245a1ab6 |
child 45848 | ec252975e82c |
permissions | -rw-r--r-- |
24333 | 1 |
(* |
2 |
Author: Jeremy Dawson, NICTA |
|
3 |
||
44939
5930d35c976d
removed unused legacy lemma names, some comment cleanup.
kleing
parents:
44890
diff
changeset
|
4 |
Basic definitions to do with integers, expressed using Pls, Min, BIT. |
24333 | 5 |
*) |
6 |
||
24350 | 7 |
header {* Basic Definitions for Binary Integers *} |
8 |
||
37658 | 9 |
theory Bit_Representation |
41413
64cd30d6b0b8
explicit file specifications -- avoid secondary load path;
wenzelm
parents:
37667
diff
changeset
|
10 |
imports Misc_Numeric "~~/src/HOL/Library/Bit" |
24333 | 11 |
begin |
12 |
||
26557 | 13 |
subsection {* Further properties of numerals *} |
14 |
||
37667 | 15 |
definition bitval :: "bit \<Rightarrow> 'a\<Colon>zero_neq_one" where |
16 |
"bitval = bit_case 0 1" |
|
17 |
||
18 |
lemma bitval_simps [simp]: |
|
19 |
"bitval 0 = 0" |
|
20 |
"bitval 1 = 1" |
|
21 |
by (simp_all add: bitval_def) |
|
22 |
||
37654 | 23 |
definition Bit :: "int \<Rightarrow> bit \<Rightarrow> int" (infixl "BIT" 90) where |
37667 | 24 |
"k BIT b = bitval b + k + k" |
26557 | 25 |
|
45843
c58ce659ce2a
reorder some definitions and proofs, in preparation for new numeral representation
huffman
parents:
45604
diff
changeset
|
26 |
definition bin_last :: "int \<Rightarrow> bit" where |
c58ce659ce2a
reorder some definitions and proofs, in preparation for new numeral representation
huffman
parents:
45604
diff
changeset
|
27 |
"bin_last w = (if w mod 2 = 0 then (0::bit) else (1::bit))" |
c58ce659ce2a
reorder some definitions and proofs, in preparation for new numeral representation
huffman
parents:
45604
diff
changeset
|
28 |
|
c58ce659ce2a
reorder some definitions and proofs, in preparation for new numeral representation
huffman
parents:
45604
diff
changeset
|
29 |
definition bin_rest :: "int \<Rightarrow> int" where |
c58ce659ce2a
reorder some definitions and proofs, in preparation for new numeral representation
huffman
parents:
45604
diff
changeset
|
30 |
"bin_rest w = w div 2" |
c58ce659ce2a
reorder some definitions and proofs, in preparation for new numeral representation
huffman
parents:
45604
diff
changeset
|
31 |
|
c58ce659ce2a
reorder some definitions and proofs, in preparation for new numeral representation
huffman
parents:
45604
diff
changeset
|
32 |
lemma bin_rl_simp [simp]: |
c58ce659ce2a
reorder some definitions and proofs, in preparation for new numeral representation
huffman
parents:
45604
diff
changeset
|
33 |
"bin_rest w BIT bin_last w = w" |
c58ce659ce2a
reorder some definitions and proofs, in preparation for new numeral representation
huffman
parents:
45604
diff
changeset
|
34 |
unfolding bin_rest_def bin_last_def Bit_def |
c58ce659ce2a
reorder some definitions and proofs, in preparation for new numeral representation
huffman
parents:
45604
diff
changeset
|
35 |
using mod_div_equality [of w 2] |
c58ce659ce2a
reorder some definitions and proofs, in preparation for new numeral representation
huffman
parents:
45604
diff
changeset
|
36 |
by (cases "w mod 2 = 0", simp_all) |
c58ce659ce2a
reorder some definitions and proofs, in preparation for new numeral representation
huffman
parents:
45604
diff
changeset
|
37 |
|
c58ce659ce2a
reorder some definitions and proofs, in preparation for new numeral representation
huffman
parents:
45604
diff
changeset
|
38 |
lemma bin_rest_BIT: "bin_rest (x BIT b) = x" |
c58ce659ce2a
reorder some definitions and proofs, in preparation for new numeral representation
huffman
parents:
45604
diff
changeset
|
39 |
unfolding bin_rest_def Bit_def |
c58ce659ce2a
reorder some definitions and proofs, in preparation for new numeral representation
huffman
parents:
45604
diff
changeset
|
40 |
by (cases b, simp_all) |
c58ce659ce2a
reorder some definitions and proofs, in preparation for new numeral representation
huffman
parents:
45604
diff
changeset
|
41 |
|
c58ce659ce2a
reorder some definitions and proofs, in preparation for new numeral representation
huffman
parents:
45604
diff
changeset
|
42 |
lemma bin_last_BIT: "bin_last (x BIT b) = b" |
c58ce659ce2a
reorder some definitions and proofs, in preparation for new numeral representation
huffman
parents:
45604
diff
changeset
|
43 |
unfolding bin_last_def Bit_def |
c58ce659ce2a
reorder some definitions and proofs, in preparation for new numeral representation
huffman
parents:
45604
diff
changeset
|
44 |
by (cases b, simp_all add: z1pmod2) |
c58ce659ce2a
reorder some definitions and proofs, in preparation for new numeral representation
huffman
parents:
45604
diff
changeset
|
45 |
|
c58ce659ce2a
reorder some definitions and proofs, in preparation for new numeral representation
huffman
parents:
45604
diff
changeset
|
46 |
lemma BIT_eq: "u BIT b = v BIT c ==> u = v & b = c" |
c58ce659ce2a
reorder some definitions and proofs, in preparation for new numeral representation
huffman
parents:
45604
diff
changeset
|
47 |
by (metis bin_rest_BIT bin_last_BIT) |
c58ce659ce2a
reorder some definitions and proofs, in preparation for new numeral representation
huffman
parents:
45604
diff
changeset
|
48 |
|
45847 | 49 |
lemma BIT_B0_eq_Bit0: "w BIT 0 = Int.Bit0 w" |
26557 | 50 |
unfolding Bit_def Bit0_def by simp |
51 |
||
45847 | 52 |
lemma BIT_B1_eq_Bit1: "w BIT 1 = Int.Bit1 w" |
26557 | 53 |
unfolding Bit_def Bit1_def by simp |
54 |
||
55 |
lemmas BIT_simps = BIT_B0_eq_Bit0 BIT_B1_eq_Bit1 |
|
24384
0002537695df
move BIT datatype stuff from Num_Lemmas to BinGeneral
huffman
parents:
24383
diff
changeset
|
56 |
|
26557 | 57 |
lemma number_of_False_cong: |
58 |
"False \<Longrightarrow> number_of x = number_of y" |
|
59 |
by (rule FalseE) |
|
60 |
||
45604 | 61 |
lemmas BIT_eqE [elim!] = BIT_eq [THEN conjE] |
26557 | 62 |
|
63 |
lemma BIT_eq_iff [simp]: |
|
64 |
"(u BIT b = v BIT c) = (u = v \<and> b = c)" |
|
65 |
by (rule iffI) auto |
|
66 |
||
67 |
lemmas BIT_eqI [intro!] = conjI [THEN BIT_eq_iff [THEN iffD2]] |
|
68 |
||
69 |
lemma less_Bits: |
|
37654 | 70 |
"(v BIT b < w BIT c) = (v < w | v <= w & b = (0::bit) & c = (1::bit))" |
37667 | 71 |
unfolding Bit_def by (auto simp add: bitval_def split: bit.split) |
24333 | 72 |
|
26557 | 73 |
lemma le_Bits: |
37654 | 74 |
"(v BIT b <= w BIT c) = (v < w | v <= w & (b ~= (1::bit) | c ~= (0::bit)))" |
37667 | 75 |
unfolding Bit_def by (auto simp add: bitval_def split: bit.split) |
26557 | 76 |
|
77 |
lemma no_no [simp]: "number_of (number_of i) = i" |
|
78 |
unfolding number_of_eq by simp |
|
79 |
||
80 |
lemma Bit_B0: |
|
37654 | 81 |
"k BIT (0::bit) = k + k" |
26557 | 82 |
by (unfold Bit_def) simp |
83 |
||
84 |
lemma Bit_B1: |
|
37654 | 85 |
"k BIT (1::bit) = k + k + 1" |
26557 | 86 |
by (unfold Bit_def) simp |
87 |
||
37654 | 88 |
lemma Bit_B0_2t: "k BIT (0::bit) = 2 * k" |
26557 | 89 |
by (rule trans, rule Bit_B0) simp |
90 |
||
37654 | 91 |
lemma Bit_B1_2t: "k BIT (1::bit) = 2 * k + 1" |
26557 | 92 |
by (rule trans, rule Bit_B1) simp |
93 |
||
94 |
lemma B_mod_2': |
|
37654 | 95 |
"X = 2 ==> (w BIT (1::bit)) mod X = 1 & (w BIT (0::bit)) mod X = 0" |
26557 | 96 |
apply (simp (no_asm) only: Bit_B0 Bit_B1) |
97 |
apply (simp add: z1pmod2) |
|
24465 | 98 |
done |
24333 | 99 |
|
26557 | 100 |
lemma B1_mod_2 [simp]: "(Int.Bit1 w) mod 2 = 1" |
101 |
unfolding numeral_simps number_of_is_id by (simp add: z1pmod2) |
|
24333 | 102 |
|
26557 | 103 |
lemma B0_mod_2 [simp]: "(Int.Bit0 w) mod 2 = 0" |
104 |
unfolding numeral_simps number_of_is_id by simp |
|
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset
|
105 |
|
26557 | 106 |
lemma neB1E [elim!]: |
37654 | 107 |
assumes ne: "y \<noteq> (1::bit)" |
108 |
assumes y: "y = (0::bit) \<Longrightarrow> P" |
|
26557 | 109 |
shows "P" |
110 |
apply (rule y) |
|
111 |
apply (cases y rule: bit.exhaust, simp) |
|
112 |
apply (simp add: ne) |
|
113 |
done |
|
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset
|
114 |
|
26557 | 115 |
lemma bin_ex_rl: "EX w b. w BIT b = bin" |
116 |
apply (unfold Bit_def) |
|
117 |
apply (cases "even bin") |
|
118 |
apply (clarsimp simp: even_equiv_def) |
|
37667 | 119 |
apply (auto simp: odd_equiv_def bitval_def split: bit.split) |
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset
|
120 |
done |
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset
|
121 |
|
26557 | 122 |
lemma bin_exhaust: |
123 |
assumes Q: "\<And>x b. bin = x BIT b \<Longrightarrow> Q" |
|
124 |
shows "Q" |
|
125 |
apply (insert bin_ex_rl [of bin]) |
|
126 |
apply (erule exE)+ |
|
127 |
apply (rule Q) |
|
128 |
apply force |
|
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset
|
129 |
done |
24333 | 130 |
|
131 |
||
24465 | 132 |
subsection {* Destructors for binary integers *} |
24364 | 133 |
|
37546 | 134 |
definition bin_rl :: "int \<Rightarrow> int \<times> bit" where |
135 |
"bin_rl w = (bin_rest w, bin_last w)" |
|
136 |
||
137 |
lemma bin_rl_char: "bin_rl w = (r, l) \<longleftrightarrow> r BIT l = w" |
|
45843
c58ce659ce2a
reorder some definitions and proofs, in preparation for new numeral representation
huffman
parents:
45604
diff
changeset
|
138 |
unfolding bin_rl_def by (auto simp: bin_rest_BIT bin_last_BIT) |
26557 | 139 |
|
26514 | 140 |
primrec bin_nth where |
37654 | 141 |
Z: "bin_nth w 0 = (bin_last w = (1::bit))" |
26557 | 142 |
| Suc: "bin_nth w (Suc n) = bin_nth (bin_rest w) n" |
24364 | 143 |
|
26557 | 144 |
lemma bin_rl_simps [simp]: |
37654 | 145 |
"bin_rl Int.Pls = (Int.Pls, (0::bit))" |
146 |
"bin_rl Int.Min = (Int.Min, (1::bit))" |
|
147 |
"bin_rl (Int.Bit0 r) = (r, (0::bit))" |
|
148 |
"bin_rl (Int.Bit1 r) = (r, (1::bit))" |
|
26557 | 149 |
"bin_rl (r BIT b) = (r, b)" |
45847 | 150 |
unfolding bin_rl_char by (simp_all add: BIT_simps) |
26557 | 151 |
|
152 |
lemma bin_abs_lem: |
|
153 |
"bin = (w BIT b) ==> ~ bin = Int.Min --> ~ bin = Int.Pls --> |
|
154 |
nat (abs w) < nat (abs bin)" |
|
155 |
apply (clarsimp simp add: bin_rl_char) |
|
156 |
apply (unfold Pls_def Min_def Bit_def) |
|
157 |
apply (cases b) |
|
158 |
apply (clarsimp, arith) |
|
159 |
apply (clarsimp, arith) |
|
160 |
done |
|
161 |
||
162 |
lemma bin_induct: |
|
163 |
assumes PPls: "P Int.Pls" |
|
164 |
and PMin: "P Int.Min" |
|
165 |
and PBit: "!!bin bit. P bin ==> P (bin BIT bit)" |
|
166 |
shows "P bin" |
|
167 |
apply (rule_tac P=P and a=bin and f1="nat o abs" |
|
168 |
in wf_measure [THEN wf_induct]) |
|
169 |
apply (simp add: measure_def inv_image_def) |
|
170 |
apply (case_tac x rule: bin_exhaust) |
|
171 |
apply (frule bin_abs_lem) |
|
172 |
apply (auto simp add : PPls PMin PBit) |
|
173 |
done |
|
174 |
||
175 |
lemma numeral_induct: |
|
176 |
assumes Pls: "P Int.Pls" |
|
177 |
assumes Min: "P Int.Min" |
|
178 |
assumes Bit0: "\<And>w. \<lbrakk>P w; w \<noteq> Int.Pls\<rbrakk> \<Longrightarrow> P (Int.Bit0 w)" |
|
179 |
assumes Bit1: "\<And>w. \<lbrakk>P w; w \<noteq> Int.Min\<rbrakk> \<Longrightarrow> P (Int.Bit1 w)" |
|
180 |
shows "P x" |
|
181 |
apply (induct x rule: bin_induct) |
|
182 |
apply (rule Pls) |
|
183 |
apply (rule Min) |
|
184 |
apply (case_tac bit) |
|
185 |
apply (case_tac "bin = Int.Pls") |
|
45847 | 186 |
apply (simp add: BIT_simps) |
187 |
apply (simp add: Bit0 BIT_simps) |
|
26557 | 188 |
apply (case_tac "bin = Int.Min") |
45847 | 189 |
apply (simp add: BIT_simps) |
190 |
apply (simp add: Bit1 BIT_simps) |
|
26557 | 191 |
done |
192 |
||
24465 | 193 |
lemma bin_rest_simps [simp]: |
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25349
diff
changeset
|
194 |
"bin_rest Int.Pls = Int.Pls" |
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25349
diff
changeset
|
195 |
"bin_rest Int.Min = Int.Min" |
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset
|
196 |
"bin_rest (Int.Bit0 w) = w" |
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset
|
197 |
"bin_rest (Int.Bit1 w) = w" |
26514 | 198 |
"bin_rest (w BIT b) = w" |
37546 | 199 |
using bin_rl_simps bin_rl_def by auto |
24465 | 200 |
|
201 |
lemma bin_last_simps [simp]: |
|
37654 | 202 |
"bin_last Int.Pls = (0::bit)" |
203 |
"bin_last Int.Min = (1::bit)" |
|
204 |
"bin_last (Int.Bit0 w) = (0::bit)" |
|
205 |
"bin_last (Int.Bit1 w) = (1::bit)" |
|
26514 | 206 |
"bin_last (w BIT b) = b" |
37546 | 207 |
using bin_rl_simps bin_rl_def by auto |
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset
|
208 |
|
24333 | 209 |
lemma bin_r_l_extras [simp]: |
37654 | 210 |
"bin_last 0 = (0::bit)" |
211 |
"bin_last (- 1) = (1::bit)" |
|
212 |
"bin_last -1 = (1::bit)" |
|
213 |
"bin_last 1 = (1::bit)" |
|
24333 | 214 |
"bin_rest 1 = 0" |
215 |
"bin_rest 0 = 0" |
|
216 |
"bin_rest (- 1) = - 1" |
|
217 |
"bin_rest -1 = -1" |
|
37654 | 218 |
by (simp_all add: bin_last_def bin_rest_def) |
24333 | 219 |
|
220 |
lemma Bit_div2 [simp]: "(w BIT b) div 2 = w" |
|
45529
0e1037d4e049
remove redundant lemmas bin_last_mod and bin_rest_div, use bin_last_def and bin_rest_def instead
huffman
parents:
44939
diff
changeset
|
221 |
unfolding bin_rest_def [symmetric] by auto |
24333 | 222 |
|
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset
|
223 |
lemma Bit0_div2 [simp]: "(Int.Bit0 w) div 2 = w" |
45847 | 224 |
using Bit_div2 [where b="(0::bit)"] by (simp add: BIT_simps) |
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset
|
225 |
|
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset
|
226 |
lemma Bit1_div2 [simp]: "(Int.Bit1 w) div 2 = w" |
45847 | 227 |
using Bit_div2 [where b="(1::bit)"] by (simp add: BIT_simps) |
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset
|
228 |
|
24333 | 229 |
lemma bin_nth_lem [rule_format]: |
230 |
"ALL y. bin_nth x = bin_nth y --> x = y" |
|
231 |
apply (induct x rule: bin_induct) |
|
232 |
apply safe |
|
233 |
apply (erule rev_mp) |
|
234 |
apply (induct_tac y rule: bin_induct) |
|
26827
a62f8db42f4a
Deleted subset_antisym in a few proofs, because it is
berghofe
parents:
26557
diff
changeset
|
235 |
apply (safe del: subset_antisym) |
24333 | 236 |
apply (drule_tac x=0 in fun_cong, force) |
237 |
apply (erule notE, rule ext, |
|
238 |
drule_tac x="Suc x" in fun_cong, force) |
|
45847 | 239 |
apply (drule_tac x=0 in fun_cong, force simp: BIT_simps) |
24333 | 240 |
apply (erule rev_mp) |
241 |
apply (induct_tac y rule: bin_induct) |
|
26827
a62f8db42f4a
Deleted subset_antisym in a few proofs, because it is
berghofe
parents:
26557
diff
changeset
|
242 |
apply (safe del: subset_antisym) |
24333 | 243 |
apply (drule_tac x=0 in fun_cong, force) |
244 |
apply (erule notE, rule ext, |
|
245 |
drule_tac x="Suc x" in fun_cong, force) |
|
45847 | 246 |
apply (drule_tac x=0 in fun_cong, force simp: BIT_simps) |
24333 | 247 |
apply (case_tac y rule: bin_exhaust) |
248 |
apply clarify |
|
249 |
apply (erule allE) |
|
250 |
apply (erule impE) |
|
251 |
prefer 2 |
|
252 |
apply (erule BIT_eqI) |
|
253 |
apply (drule_tac x=0 in fun_cong, force) |
|
254 |
apply (rule ext) |
|
255 |
apply (drule_tac x="Suc ?x" in fun_cong, force) |
|
256 |
done |
|
257 |
||
258 |
lemma bin_nth_eq_iff: "(bin_nth x = bin_nth y) = (x = y)" |
|
259 |
by (auto elim: bin_nth_lem) |
|
260 |
||
45604 | 261 |
lemmas bin_eqI = ext [THEN bin_nth_eq_iff [THEN iffD1]] |
24333 | 262 |
|
45543
827bf668c822
HOL-Word: add simp rules for bin_rest, bin_last; shorten several proofs
huffman
parents:
45529
diff
changeset
|
263 |
lemma bin_eq_iff: "x = y \<longleftrightarrow> (\<forall>n. bin_nth x n = bin_nth y n)" |
827bf668c822
HOL-Word: add simp rules for bin_rest, bin_last; shorten several proofs
huffman
parents:
45529
diff
changeset
|
264 |
by (auto intro!: bin_nth_lem del: equalityI) |
827bf668c822
HOL-Word: add simp rules for bin_rest, bin_last; shorten several proofs
huffman
parents:
45529
diff
changeset
|
265 |
|
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25349
diff
changeset
|
266 |
lemma bin_nth_Pls [simp]: "~ bin_nth Int.Pls n" |
24333 | 267 |
by (induct n) auto |
268 |
||
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25349
diff
changeset
|
269 |
lemma bin_nth_Min [simp]: "bin_nth Int.Min n" |
24333 | 270 |
by (induct n) auto |
271 |
||
37654 | 272 |
lemma bin_nth_0_BIT: "bin_nth (w BIT b) 0 = (b = (1::bit))" |
24333 | 273 |
by auto |
274 |
||
275 |
lemma bin_nth_Suc_BIT: "bin_nth (w BIT b) (Suc n) = bin_nth w n" |
|
276 |
by auto |
|
277 |
||
278 |
lemma bin_nth_minus [simp]: "0 < n ==> bin_nth (w BIT b) n = bin_nth w (n - 1)" |
|
279 |
by (cases n) auto |
|
280 |
||
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset
|
281 |
lemma bin_nth_minus_Bit0 [simp]: |
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset
|
282 |
"0 < n ==> bin_nth (Int.Bit0 w) n = bin_nth w (n - 1)" |
45847 | 283 |
using bin_nth_minus [where b="(0::bit)"] by (simp add: BIT_simps) |
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset
|
284 |
|
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset
|
285 |
lemma bin_nth_minus_Bit1 [simp]: |
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset
|
286 |
"0 < n ==> bin_nth (Int.Bit1 w) n = bin_nth w (n - 1)" |
45847 | 287 |
using bin_nth_minus [where b="(1::bit)"] by (simp add: BIT_simps) |
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset
|
288 |
|
24333 | 289 |
lemmas bin_nth_0 = bin_nth.simps(1) |
290 |
lemmas bin_nth_Suc = bin_nth.simps(2) |
|
291 |
||
292 |
lemmas bin_nth_simps = |
|
293 |
bin_nth_0 bin_nth_Suc bin_nth_Pls bin_nth_Min bin_nth_minus |
|
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset
|
294 |
bin_nth_minus_Bit0 bin_nth_minus_Bit1 |
24333 | 295 |
|
26557 | 296 |
|
297 |
subsection {* Truncating binary integers *} |
|
298 |
||
45846 | 299 |
definition bin_sign :: "int \<Rightarrow> int" where |
37667 | 300 |
bin_sign_def: "bin_sign k = (if k \<ge> 0 then 0 else - 1)" |
26557 | 301 |
|
302 |
lemma bin_sign_simps [simp]: |
|
303 |
"bin_sign Int.Pls = Int.Pls" |
|
304 |
"bin_sign Int.Min = Int.Min" |
|
305 |
"bin_sign (Int.Bit0 w) = bin_sign w" |
|
306 |
"bin_sign (Int.Bit1 w) = bin_sign w" |
|
307 |
"bin_sign (w BIT b) = bin_sign w" |
|
37667 | 308 |
by (unfold bin_sign_def numeral_simps Bit_def bitval_def) (simp_all split: bit.split) |
26557 | 309 |
|
24364 | 310 |
lemma bin_sign_rest [simp]: |
37667 | 311 |
"bin_sign (bin_rest w) = bin_sign w" |
26557 | 312 |
by (cases w rule: bin_exhaust) auto |
24364 | 313 |
|
37667 | 314 |
primrec bintrunc :: "nat \<Rightarrow> int \<Rightarrow> int" where |
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25349
diff
changeset
|
315 |
Z : "bintrunc 0 bin = Int.Pls" |
37667 | 316 |
| Suc : "bintrunc (Suc n) bin = bintrunc n (bin_rest bin) BIT (bin_last bin)" |
24364 | 317 |
|
37667 | 318 |
primrec sbintrunc :: "nat => int => int" where |
24364 | 319 |
Z : "sbintrunc 0 bin = |
37654 | 320 |
(case bin_last bin of (1::bit) => Int.Min | (0::bit) => Int.Pls)" |
37667 | 321 |
| Suc : "sbintrunc (Suc n) bin = sbintrunc n (bin_rest bin) BIT (bin_last bin)" |
322 |
||
323 |
lemma [code]: |
|
324 |
"sbintrunc 0 bin = |
|
325 |
(case bin_last bin of (1::bit) => - 1 | (0::bit) => 0)" |
|
326 |
"sbintrunc (Suc n) bin = sbintrunc n (bin_rest bin) BIT (bin_last bin)" |
|
45845
4158f35a5c6f
remove some unwanted numeral-representation-specific simp rules
huffman
parents:
45844
diff
changeset
|
327 |
apply simp_all |
4158f35a5c6f
remove some unwanted numeral-representation-specific simp rules
huffman
parents:
45844
diff
changeset
|
328 |
apply (simp only: Pls_def Min_def) |
4158f35a5c6f
remove some unwanted numeral-representation-specific simp rules
huffman
parents:
45844
diff
changeset
|
329 |
done |
24364 | 330 |
|
24333 | 331 |
lemma sign_bintr: |
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25349
diff
changeset
|
332 |
"!!w. bin_sign (bintrunc n w) = Int.Pls" |
24333 | 333 |
by (induct n) auto |
334 |
||
335 |
lemma bintrunc_mod2p: |
|
336 |
"!!w. bintrunc n w = (w mod 2 ^ n :: int)" |
|
45845
4158f35a5c6f
remove some unwanted numeral-representation-specific simp rules
huffman
parents:
45844
diff
changeset
|
337 |
apply (induct n) |
4158f35a5c6f
remove some unwanted numeral-representation-specific simp rules
huffman
parents:
45844
diff
changeset
|
338 |
apply (simp add: Pls_def) |
45529
0e1037d4e049
remove redundant lemmas bin_last_mod and bin_rest_div, use bin_last_def and bin_rest_def instead
huffman
parents:
44939
diff
changeset
|
339 |
apply (simp add: bin_last_def bin_rest_def Bit_def zmod_zmult2_eq |
24333 | 340 |
cong: number_of_False_cong) |
341 |
done |
|
342 |
||
343 |
lemma sbintrunc_mod2p: |
|
344 |
"!!w. sbintrunc n w = ((w + 2 ^ n) mod 2 ^ (Suc n) - 2 ^ n :: int)" |
|
345 |
apply (induct n) |
|
346 |
apply clarsimp |
|
30034 | 347 |
apply (subst mod_add_left_eq) |
45529
0e1037d4e049
remove redundant lemmas bin_last_mod and bin_rest_div, use bin_last_def and bin_rest_def instead
huffman
parents:
44939
diff
changeset
|
348 |
apply (simp add: bin_last_def) |
24333 | 349 |
apply (simp add: number_of_eq) |
45845
4158f35a5c6f
remove some unwanted numeral-representation-specific simp rules
huffman
parents:
45844
diff
changeset
|
350 |
apply (simp add: Pls_def) |
45529
0e1037d4e049
remove redundant lemmas bin_last_mod and bin_rest_div, use bin_last_def and bin_rest_def instead
huffman
parents:
44939
diff
changeset
|
351 |
apply (simp add: bin_last_def bin_rest_def Bit_def |
24333 | 352 |
cong: number_of_False_cong) |
30940
663af91c0720
zmod_zmult_zmult1 now subsumed by mod_mult_mult1
haftmann
parents:
30034
diff
changeset
|
353 |
apply (clarsimp simp: mod_mult_mult1 [symmetric] |
24333 | 354 |
zmod_zdiv_equality [THEN diff_eq_eq [THEN iffD2 [THEN sym]]]) |
355 |
apply (rule trans [symmetric, OF _ emep1]) |
|
356 |
apply auto |
|
357 |
apply (auto simp: even_def) |
|
358 |
done |
|
359 |
||
24465 | 360 |
subsection "Simplifications for (s)bintrunc" |
361 |
||
362 |
lemma bit_bool: |
|
37654 | 363 |
"(b = (b' = (1::bit))) = (b' = (if b then (1::bit) else (0::bit)))" |
24465 | 364 |
by (cases b') auto |
365 |
||
366 |
lemmas bit_bool1 [simp] = refl [THEN bit_bool [THEN iffD1], symmetric] |
|
24333 | 367 |
|
368 |
lemma bin_sign_lem: |
|
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25349
diff
changeset
|
369 |
"!!bin. (bin_sign (sbintrunc n bin) = Int.Min) = bin_nth bin n" |
24333 | 370 |
apply (induct n) |
371 |
apply (case_tac bin rule: bin_exhaust, case_tac b, auto)+ |
|
372 |
done |
|
373 |
||
374 |
lemma nth_bintr: |
|
375 |
"!!w m. bin_nth (bintrunc m w) n = (n < m & bin_nth w n)" |
|
376 |
apply (induct n) |
|
377 |
apply (case_tac m, auto)[1] |
|
378 |
apply (case_tac m, auto)[1] |
|
379 |
done |
|
380 |
||
381 |
lemma nth_sbintr: |
|
382 |
"!!w m. bin_nth (sbintrunc m w) n = |
|
383 |
(if n < m then bin_nth w n else bin_nth w m)" |
|
384 |
apply (induct n) |
|
385 |
apply (case_tac m, simp_all split: bit.splits)[1] |
|
386 |
apply (case_tac m, simp_all split: bit.splits)[1] |
|
387 |
done |
|
388 |
||
389 |
lemma bin_nth_Bit: |
|
37654 | 390 |
"bin_nth (w BIT b) n = (n = 0 & b = (1::bit) | (EX m. n = Suc m & bin_nth w m))" |
24333 | 391 |
by (cases n) auto |
392 |
||
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset
|
393 |
lemma bin_nth_Bit0: |
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset
|
394 |
"bin_nth (Int.Bit0 w) n = (EX m. n = Suc m & bin_nth w m)" |
45847 | 395 |
using bin_nth_Bit [where b="(0::bit)"] by (simp add: BIT_simps) |
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset
|
396 |
|
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset
|
397 |
lemma bin_nth_Bit1: |
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset
|
398 |
"bin_nth (Int.Bit1 w) n = (n = 0 | (EX m. n = Suc m & bin_nth w m))" |
45847 | 399 |
using bin_nth_Bit [where b="(1::bit)"] by (simp add: BIT_simps) |
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset
|
400 |
|
24333 | 401 |
lemma bintrunc_bintrunc_l: |
402 |
"n <= m ==> (bintrunc m (bintrunc n w) = bintrunc n w)" |
|
403 |
by (rule bin_eqI) (auto simp add : nth_bintr) |
|
404 |
||
405 |
lemma sbintrunc_sbintrunc_l: |
|
406 |
"n <= m ==> (sbintrunc m (sbintrunc n w) = sbintrunc n w)" |
|
32439 | 407 |
by (rule bin_eqI) (auto simp: nth_sbintr) |
24333 | 408 |
|
409 |
lemma bintrunc_bintrunc_ge: |
|
410 |
"n <= m ==> (bintrunc n (bintrunc m w) = bintrunc n w)" |
|
411 |
by (rule bin_eqI) (auto simp: nth_bintr) |
|
412 |
||
413 |
lemma bintrunc_bintrunc_min [simp]: |
|
414 |
"bintrunc m (bintrunc n w) = bintrunc (min m n) w" |
|
415 |
apply (rule bin_eqI) |
|
416 |
apply (auto simp: nth_bintr) |
|
417 |
done |
|
418 |
||
419 |
lemma sbintrunc_sbintrunc_min [simp]: |
|
420 |
"sbintrunc m (sbintrunc n w) = sbintrunc (min m n) w" |
|
421 |
apply (rule bin_eqI) |
|
32642
026e7c6a6d08
be more cautious wrt. simp rules: inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no simp rules by default any longer
haftmann
parents:
32439
diff
changeset
|
422 |
apply (auto simp: nth_sbintr min_max.inf_absorb1 min_max.inf_absorb2) |
24333 | 423 |
done |
424 |
||
425 |
lemmas bintrunc_Pls = |
|
45604 | 426 |
bintrunc.Suc [where bin="Int.Pls", simplified bin_last_simps bin_rest_simps] |
24333 | 427 |
|
428 |
lemmas bintrunc_Min [simp] = |
|
45604 | 429 |
bintrunc.Suc [where bin="Int.Min", simplified bin_last_simps bin_rest_simps] |
24333 | 430 |
|
431 |
lemmas bintrunc_BIT [simp] = |
|
45604 | 432 |
bintrunc.Suc [where bin="w BIT b", simplified bin_last_simps bin_rest_simps] for w b |
24333 | 433 |
|
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset
|
434 |
lemma bintrunc_Bit0 [simp]: |
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset
|
435 |
"bintrunc (Suc n) (Int.Bit0 w) = Int.Bit0 (bintrunc n w)" |
45847 | 436 |
using bintrunc_BIT [where b="(0::bit)"] by (simp add: BIT_simps) |
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset
|
437 |
|
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset
|
438 |
lemma bintrunc_Bit1 [simp]: |
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset
|
439 |
"bintrunc (Suc n) (Int.Bit1 w) = Int.Bit1 (bintrunc n w)" |
45847 | 440 |
using bintrunc_BIT [where b="(1::bit)"] by (simp add: BIT_simps) |
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset
|
441 |
|
24333 | 442 |
lemmas bintrunc_Sucs = bintrunc_Pls bintrunc_Min bintrunc_BIT |
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset
|
443 |
bintrunc_Bit0 bintrunc_Bit1 |
24333 | 444 |
|
445 |
lemmas sbintrunc_Suc_Pls = |
|
45604 | 446 |
sbintrunc.Suc [where bin="Int.Pls", simplified bin_last_simps bin_rest_simps] |
24333 | 447 |
|
448 |
lemmas sbintrunc_Suc_Min = |
|
45604 | 449 |
sbintrunc.Suc [where bin="Int.Min", simplified bin_last_simps bin_rest_simps] |
24333 | 450 |
|
451 |
lemmas sbintrunc_Suc_BIT [simp] = |
|
45604 | 452 |
sbintrunc.Suc [where bin="w BIT b", simplified bin_last_simps bin_rest_simps] for w b |
24333 | 453 |
|
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset
|
454 |
lemma sbintrunc_Suc_Bit0 [simp]: |
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset
|
455 |
"sbintrunc (Suc n) (Int.Bit0 w) = Int.Bit0 (sbintrunc n w)" |
45847 | 456 |
using sbintrunc_Suc_BIT [where b="(0::bit)"] by (simp add: BIT_simps) |
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset
|
457 |
|
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset
|
458 |
lemma sbintrunc_Suc_Bit1 [simp]: |
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset
|
459 |
"sbintrunc (Suc n) (Int.Bit1 w) = Int.Bit1 (sbintrunc n w)" |
45847 | 460 |
using sbintrunc_Suc_BIT [where b="(1::bit)"] by (simp add: BIT_simps) |
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset
|
461 |
|
24333 | 462 |
lemmas sbintrunc_Sucs = sbintrunc_Suc_Pls sbintrunc_Suc_Min sbintrunc_Suc_BIT |
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset
|
463 |
sbintrunc_Suc_Bit0 sbintrunc_Suc_Bit1 |
24333 | 464 |
|
465 |
lemmas sbintrunc_Pls = |
|
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25349
diff
changeset
|
466 |
sbintrunc.Z [where bin="Int.Pls", |
45604 | 467 |
simplified bin_last_simps bin_rest_simps bit.simps] |
24333 | 468 |
|
469 |
lemmas sbintrunc_Min = |
|
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25349
diff
changeset
|
470 |
sbintrunc.Z [where bin="Int.Min", |
45604 | 471 |
simplified bin_last_simps bin_rest_simps bit.simps] |
24333 | 472 |
|
473 |
lemmas sbintrunc_0_BIT_B0 [simp] = |
|
37654 | 474 |
sbintrunc.Z [where bin="w BIT (0::bit)", |
45604 | 475 |
simplified bin_last_simps bin_rest_simps bit.simps] for w |
24333 | 476 |
|
477 |
lemmas sbintrunc_0_BIT_B1 [simp] = |
|
37654 | 478 |
sbintrunc.Z [where bin="w BIT (1::bit)", |
45604 | 479 |
simplified bin_last_simps bin_rest_simps bit.simps] for w |
24333 | 480 |
|
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset
|
481 |
lemma sbintrunc_0_Bit0 [simp]: "sbintrunc 0 (Int.Bit0 w) = Int.Pls" |
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset
|
482 |
using sbintrunc_0_BIT_B0 by simp |
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset
|
483 |
|
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset
|
484 |
lemma sbintrunc_0_Bit1 [simp]: "sbintrunc 0 (Int.Bit1 w) = Int.Min" |
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset
|
485 |
using sbintrunc_0_BIT_B1 by simp |
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset
|
486 |
|
24333 | 487 |
lemmas sbintrunc_0_simps = |
488 |
sbintrunc_Pls sbintrunc_Min sbintrunc_0_BIT_B0 sbintrunc_0_BIT_B1 |
|
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset
|
489 |
sbintrunc_0_Bit0 sbintrunc_0_Bit1 |
24333 | 490 |
|
491 |
lemmas bintrunc_simps = bintrunc.Z bintrunc_Sucs |
|
492 |
lemmas sbintrunc_simps = sbintrunc_0_simps sbintrunc_Sucs |
|
493 |
||
494 |
lemma bintrunc_minus: |
|
495 |
"0 < n ==> bintrunc (Suc (n - 1)) w = bintrunc n w" |
|
496 |
by auto |
|
497 |
||
498 |
lemma sbintrunc_minus: |
|
499 |
"0 < n ==> sbintrunc (Suc (n - 1)) w = sbintrunc n w" |
|
500 |
by auto |
|
501 |
||
502 |
lemmas bintrunc_minus_simps = |
|
45604 | 503 |
bintrunc_Sucs [THEN [2] bintrunc_minus [symmetric, THEN trans]] |
24333 | 504 |
lemmas sbintrunc_minus_simps = |
45604 | 505 |
sbintrunc_Sucs [THEN [2] sbintrunc_minus [symmetric, THEN trans]] |
24333 | 506 |
|
507 |
lemma bintrunc_n_Pls [simp]: |
|
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25349
diff
changeset
|
508 |
"bintrunc n Int.Pls = Int.Pls" |
45847 | 509 |
by (induct n) (auto simp: BIT_simps) |
24333 | 510 |
|
511 |
lemma sbintrunc_n_PM [simp]: |
|
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25349
diff
changeset
|
512 |
"sbintrunc n Int.Pls = Int.Pls" |
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25349
diff
changeset
|
513 |
"sbintrunc n Int.Min = Int.Min" |
45847 | 514 |
by (induct n) (auto simp: BIT_simps) |
24333 | 515 |
|
45604 | 516 |
lemmas thobini1 = arg_cong [where f = "%w. w BIT b"] for b |
24333 | 517 |
|
518 |
lemmas bintrunc_BIT_I = trans [OF bintrunc_BIT thobini1] |
|
519 |
lemmas bintrunc_Min_I = trans [OF bintrunc_Min thobini1] |
|
520 |
||
45604 | 521 |
lemmas bmsts = bintrunc_minus_simps(1-3) [THEN thobini1 [THEN [2] trans]] |
24333 | 522 |
lemmas bintrunc_Pls_minus_I = bmsts(1) |
523 |
lemmas bintrunc_Min_minus_I = bmsts(2) |
|
524 |
lemmas bintrunc_BIT_minus_I = bmsts(3) |
|
525 |
||
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25349
diff
changeset
|
526 |
lemma bintrunc_0_Min: "bintrunc 0 Int.Min = Int.Pls" |
24333 | 527 |
by auto |
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25349
diff
changeset
|
528 |
lemma bintrunc_0_BIT: "bintrunc 0 (w BIT b) = Int.Pls" |
24333 | 529 |
by auto |
530 |
||
531 |
lemma bintrunc_Suc_lem: |
|
532 |
"bintrunc (Suc n) x = y ==> m = Suc n ==> bintrunc m x = y" |
|
533 |
by auto |
|
534 |
||
535 |
lemmas bintrunc_Suc_Ialts = |
|
45604 | 536 |
bintrunc_Min_I [THEN bintrunc_Suc_lem] |
537 |
bintrunc_BIT_I [THEN bintrunc_Suc_lem] |
|
24333 | 538 |
|
539 |
lemmas sbintrunc_BIT_I = trans [OF sbintrunc_Suc_BIT thobini1] |
|
540 |
||
541 |
lemmas sbintrunc_Suc_Is = |
|
45604 | 542 |
sbintrunc_Sucs(1-3) [THEN thobini1 [THEN [2] trans]] |
24333 | 543 |
|
544 |
lemmas sbintrunc_Suc_minus_Is = |
|
45604 | 545 |
sbintrunc_minus_simps(1-3) [THEN thobini1 [THEN [2] trans]] |
24333 | 546 |
|
547 |
lemma sbintrunc_Suc_lem: |
|
548 |
"sbintrunc (Suc n) x = y ==> m = Suc n ==> sbintrunc m x = y" |
|
549 |
by auto |
|
550 |
||
551 |
lemmas sbintrunc_Suc_Ialts = |
|
45604 | 552 |
sbintrunc_Suc_Is [THEN sbintrunc_Suc_lem] |
24333 | 553 |
|
554 |
lemma sbintrunc_bintrunc_lt: |
|
555 |
"m > n ==> sbintrunc n (bintrunc m w) = sbintrunc n w" |
|
556 |
by (rule bin_eqI) (auto simp: nth_sbintr nth_bintr) |
|
557 |
||
558 |
lemma bintrunc_sbintrunc_le: |
|
559 |
"m <= Suc n ==> bintrunc m (sbintrunc n w) = bintrunc m w" |
|
560 |
apply (rule bin_eqI) |
|
561 |
apply (auto simp: nth_sbintr nth_bintr) |
|
562 |
apply (subgoal_tac "x=n", safe, arith+)[1] |
|
563 |
apply (subgoal_tac "x=n", safe, arith+)[1] |
|
564 |
done |
|
565 |
||
566 |
lemmas bintrunc_sbintrunc [simp] = order_refl [THEN bintrunc_sbintrunc_le] |
|
567 |
lemmas sbintrunc_bintrunc [simp] = lessI [THEN sbintrunc_bintrunc_lt] |
|
568 |
lemmas bintrunc_bintrunc [simp] = order_refl [THEN bintrunc_bintrunc_l] |
|
569 |
lemmas sbintrunc_sbintrunc [simp] = order_refl [THEN sbintrunc_sbintrunc_l] |
|
570 |
||
571 |
lemma bintrunc_sbintrunc' [simp]: |
|
572 |
"0 < n \<Longrightarrow> bintrunc n (sbintrunc (n - 1) w) = bintrunc n w" |
|
573 |
by (cases n) (auto simp del: bintrunc.Suc) |
|
574 |
||
575 |
lemma sbintrunc_bintrunc' [simp]: |
|
576 |
"0 < n \<Longrightarrow> sbintrunc (n - 1) (bintrunc n w) = sbintrunc (n - 1) w" |
|
577 |
by (cases n) (auto simp del: bintrunc.Suc) |
|
578 |
||
579 |
lemma bin_sbin_eq_iff: |
|
580 |
"bintrunc (Suc n) x = bintrunc (Suc n) y <-> |
|
581 |
sbintrunc n x = sbintrunc n y" |
|
582 |
apply (rule iffI) |
|
583 |
apply (rule box_equals [OF _ sbintrunc_bintrunc sbintrunc_bintrunc]) |
|
584 |
apply simp |
|
585 |
apply (rule box_equals [OF _ bintrunc_sbintrunc bintrunc_sbintrunc]) |
|
586 |
apply simp |
|
587 |
done |
|
588 |
||
589 |
lemma bin_sbin_eq_iff': |
|
590 |
"0 < n \<Longrightarrow> bintrunc n x = bintrunc n y <-> |
|
591 |
sbintrunc (n - 1) x = sbintrunc (n - 1) y" |
|
592 |
by (cases n) (simp_all add: bin_sbin_eq_iff del: bintrunc.Suc) |
|
593 |
||
594 |
lemmas bintrunc_sbintruncS0 [simp] = bintrunc_sbintrunc' [unfolded One_nat_def] |
|
595 |
lemmas sbintrunc_bintruncS0 [simp] = sbintrunc_bintrunc' [unfolded One_nat_def] |
|
596 |
||
597 |
lemmas bintrunc_bintrunc_l' = le_add1 [THEN bintrunc_bintrunc_l] |
|
598 |
lemmas sbintrunc_sbintrunc_l' = le_add1 [THEN sbintrunc_sbintrunc_l] |
|
599 |
||
600 |
(* although bintrunc_minus_simps, if added to default simpset, |
|
601 |
tends to get applied where it's not wanted in developing the theories, |
|
602 |
we get a version for when the word length is given literally *) |
|
603 |
||
604 |
lemmas nat_non0_gr = |
|
45604 | 605 |
trans [OF iszero_def [THEN Not_eq_iff [THEN iffD2]] refl] |
24333 | 606 |
|
607 |
lemmas bintrunc_pred_simps [simp] = |
|
45604 | 608 |
bintrunc_minus_simps [of "number_of bin", simplified nobm1] for bin |
24333 | 609 |
|
610 |
lemmas sbintrunc_pred_simps [simp] = |
|
45604 | 611 |
sbintrunc_minus_simps [of "number_of bin", simplified nobm1] for bin |
24333 | 612 |
|
613 |
lemma no_bintr_alt: |
|
614 |
"number_of (bintrunc n w) = w mod 2 ^ n" |
|
615 |
by (simp add: number_of_eq bintrunc_mod2p) |
|
616 |
||
617 |
lemma no_bintr_alt1: "bintrunc n = (%w. w mod 2 ^ n :: int)" |
|
618 |
by (rule ext) (rule bintrunc_mod2p) |
|
619 |
||
620 |
lemma range_bintrunc: "range (bintrunc n) = {i. 0 <= i & i < 2 ^ n}" |
|
621 |
apply (unfold no_bintr_alt1) |
|
622 |
apply (auto simp add: image_iff) |
|
623 |
apply (rule exI) |
|
624 |
apply (auto intro: int_mod_lem [THEN iffD1, symmetric]) |
|
625 |
done |
|
626 |
||
627 |
lemma no_bintr: |
|
628 |
"number_of (bintrunc n w) = (number_of w mod 2 ^ n :: int)" |
|
629 |
by (simp add : bintrunc_mod2p number_of_eq) |
|
630 |
||
631 |
lemma no_sbintr_alt2: |
|
632 |
"sbintrunc n = (%w. (w + 2 ^ n) mod 2 ^ Suc n - 2 ^ n :: int)" |
|
633 |
by (rule ext) (simp add : sbintrunc_mod2p) |
|
634 |
||
635 |
lemma no_sbintr: |
|
636 |
"number_of (sbintrunc n w) = |
|
637 |
((number_of w + 2 ^ n) mod 2 ^ Suc n - 2 ^ n :: int)" |
|
638 |
by (simp add : no_sbintr_alt2 number_of_eq) |
|
639 |
||
640 |
lemma range_sbintrunc: |
|
641 |
"range (sbintrunc n) = {i. - (2 ^ n) <= i & i < 2 ^ n}" |
|
642 |
apply (unfold no_sbintr_alt2) |
|
643 |
apply (auto simp add: image_iff eq_diff_eq) |
|
644 |
apply (rule exI) |
|
645 |
apply (auto intro: int_mod_lem [THEN iffD1, symmetric]) |
|
646 |
done |
|
647 |
||
25349
0d46bea01741
eliminated illegal schematic variables in where/of;
wenzelm
parents:
25134
diff
changeset
|
648 |
lemma sb_inc_lem: |
0d46bea01741
eliminated illegal schematic variables in where/of;
wenzelm
parents:
25134
diff
changeset
|
649 |
"(a::int) + 2^k < 0 \<Longrightarrow> a + 2^k + 2^(Suc k) <= (a + 2^k) mod 2^(Suc k)" |
0d46bea01741
eliminated illegal schematic variables in where/of;
wenzelm
parents:
25134
diff
changeset
|
650 |
apply (erule int_mod_ge' [where n = "2 ^ (Suc k)" and b = "a + 2 ^ k", simplified zless2p]) |
0d46bea01741
eliminated illegal schematic variables in where/of;
wenzelm
parents:
25134
diff
changeset
|
651 |
apply (rule TrueI) |
0d46bea01741
eliminated illegal schematic variables in where/of;
wenzelm
parents:
25134
diff
changeset
|
652 |
done |
24333 | 653 |
|
25349
0d46bea01741
eliminated illegal schematic variables in where/of;
wenzelm
parents:
25134
diff
changeset
|
654 |
lemma sb_inc_lem': |
0d46bea01741
eliminated illegal schematic variables in where/of;
wenzelm
parents:
25134
diff
changeset
|
655 |
"(a::int) < - (2^k) \<Longrightarrow> a + 2^k + 2^(Suc k) <= (a + 2^k) mod 2^(Suc k)" |
35048 | 656 |
by (rule sb_inc_lem) simp |
24333 | 657 |
|
658 |
lemma sbintrunc_inc: |
|
25349
0d46bea01741
eliminated illegal schematic variables in where/of;
wenzelm
parents:
25134
diff
changeset
|
659 |
"x < - (2^n) ==> x + 2^(Suc n) <= sbintrunc n x" |
24333 | 660 |
unfolding no_sbintr_alt2 by (drule sb_inc_lem') simp |
661 |
||
25349
0d46bea01741
eliminated illegal schematic variables in where/of;
wenzelm
parents:
25134
diff
changeset
|
662 |
lemma sb_dec_lem: |
0d46bea01741
eliminated illegal schematic variables in where/of;
wenzelm
parents:
25134
diff
changeset
|
663 |
"(0::int) <= - (2^k) + a ==> (a + 2^k) mod (2 * 2 ^ k) <= - (2 ^ k) + a" |
0d46bea01741
eliminated illegal schematic variables in where/of;
wenzelm
parents:
25134
diff
changeset
|
664 |
by (rule int_mod_le' [where n = "2 ^ (Suc k)" and b = "a + 2 ^ k", |
0d46bea01741
eliminated illegal schematic variables in where/of;
wenzelm
parents:
25134
diff
changeset
|
665 |
simplified zless2p, OF _ TrueI, simplified]) |
24333 | 666 |
|
25349
0d46bea01741
eliminated illegal schematic variables in where/of;
wenzelm
parents:
25134
diff
changeset
|
667 |
lemma sb_dec_lem': |
0d46bea01741
eliminated illegal schematic variables in where/of;
wenzelm
parents:
25134
diff
changeset
|
668 |
"(2::int) ^ k <= a ==> (a + 2 ^ k) mod (2 * 2 ^ k) <= - (2 ^ k) + a" |
0d46bea01741
eliminated illegal schematic variables in where/of;
wenzelm
parents:
25134
diff
changeset
|
669 |
by (rule iffD1 [OF diff_le_eq', THEN sb_dec_lem, simplified]) |
24333 | 670 |
|
671 |
lemma sbintrunc_dec: |
|
672 |
"x >= (2 ^ n) ==> x - 2 ^ (Suc n) >= sbintrunc n x" |
|
673 |
unfolding no_sbintr_alt2 by (drule sb_dec_lem') simp |
|
674 |
||
45604 | 675 |
lemmas zmod_uminus' = zmod_uminus [where b=c] for c |
676 |
lemmas zpower_zmod' = zpower_zmod [where m=c and y=k] for c k |
|
24333 | 677 |
|
678 |
lemmas brdmod1s' [symmetric] = |
|
30034 | 679 |
mod_add_left_eq mod_add_right_eq |
24333 | 680 |
zmod_zsub_left_eq zmod_zsub_right_eq |
681 |
zmod_zmult1_eq zmod_zmult1_eq_rev |
|
682 |
||
683 |
lemmas brdmods' [symmetric] = |
|
684 |
zpower_zmod' [symmetric] |
|
30034 | 685 |
trans [OF mod_add_left_eq mod_add_right_eq] |
24333 | 686 |
trans [OF zmod_zsub_left_eq zmod_zsub_right_eq] |
687 |
trans [OF zmod_zmult1_eq zmod_zmult1_eq_rev] |
|
688 |
zmod_uminus' [symmetric] |
|
30034 | 689 |
mod_add_left_eq [where b = "1::int"] |
24333 | 690 |
zmod_zsub_left_eq [where b = "1"] |
691 |
||
692 |
lemmas bintr_arith1s = |
|
45604 | 693 |
brdmod1s' [where c="2^n::int", folded pred_def succ_def bintrunc_mod2p] for n |
24333 | 694 |
lemmas bintr_ariths = |
45604 | 695 |
brdmods' [where c="2^n::int", folded pred_def succ_def bintrunc_mod2p] for n |
24333 | 696 |
|
45604 | 697 |
lemmas m2pths = pos_mod_sign pos_mod_bound [OF zless2p] |
24364 | 698 |
|
24333 | 699 |
lemma bintr_ge0: "(0 :: int) <= number_of (bintrunc n w)" |
700 |
by (simp add : no_bintr m2pths) |
|
701 |
||
702 |
lemma bintr_lt2p: "number_of (bintrunc n w) < (2 ^ n :: int)" |
|
703 |
by (simp add : no_bintr m2pths) |
|
704 |
||
705 |
lemma bintr_Min: |
|
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25349
diff
changeset
|
706 |
"number_of (bintrunc n Int.Min) = (2 ^ n :: int) - 1" |
24333 | 707 |
by (simp add : no_bintr m1mod2k) |
708 |
||
709 |
lemma sbintr_ge: "(- (2 ^ n) :: int) <= number_of (sbintrunc n w)" |
|
710 |
by (simp add : no_sbintr m2pths) |
|
711 |
||
712 |
lemma sbintr_lt: "number_of (sbintrunc n w) < (2 ^ n :: int)" |
|
713 |
by (simp add : no_sbintr m2pths) |
|
714 |
||
715 |
lemma bintrunc_Suc: |
|
716 |
"bintrunc (Suc n) bin = bintrunc n (bin_rest bin) BIT bin_last bin" |
|
717 |
by (case_tac bin rule: bin_exhaust) auto |
|
718 |
||
719 |
lemma sign_Pls_ge_0: |
|
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25349
diff
changeset
|
720 |
"(bin_sign bin = Int.Pls) = (number_of bin >= (0 :: int))" |
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset
|
721 |
by (induct bin rule: numeral_induct) auto |
24333 | 722 |
|
723 |
lemma sign_Min_lt_0: |
|
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25349
diff
changeset
|
724 |
"(bin_sign bin = Int.Min) = (number_of bin < (0 :: int))" |
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset
|
725 |
by (induct bin rule: numeral_induct) auto |
24333 | 726 |
|
727 |
lemmas sign_Min_neg = trans [OF sign_Min_lt_0 neg_def [symmetric]] |
|
728 |
||
729 |
lemma bin_rest_trunc: |
|
730 |
"!!bin. (bin_rest (bintrunc n bin)) = bintrunc (n - 1) (bin_rest bin)" |
|
731 |
by (induct n) auto |
|
732 |
||
733 |
lemma bin_rest_power_trunc [rule_format] : |
|
30971 | 734 |
"(bin_rest ^^ k) (bintrunc n bin) = |
735 |
bintrunc (n - k) ((bin_rest ^^ k) bin)" |
|
24333 | 736 |
by (induct k) (auto simp: bin_rest_trunc) |
737 |
||
738 |
lemma bin_rest_trunc_i: |
|
739 |
"bintrunc n (bin_rest bin) = bin_rest (bintrunc (Suc n) bin)" |
|
740 |
by auto |
|
741 |
||
742 |
lemma bin_rest_strunc: |
|
743 |
"!!bin. bin_rest (sbintrunc (Suc n) bin) = sbintrunc n (bin_rest bin)" |
|
744 |
by (induct n) auto |
|
745 |
||
746 |
lemma bintrunc_rest [simp]: |
|
747 |
"!!bin. bintrunc n (bin_rest (bintrunc n bin)) = bin_rest (bintrunc n bin)" |
|
748 |
apply (induct n, simp) |
|
749 |
apply (case_tac bin rule: bin_exhaust) |
|
750 |
apply (auto simp: bintrunc_bintrunc_l) |
|
751 |
done |
|
752 |
||
753 |
lemma sbintrunc_rest [simp]: |
|
754 |
"!!bin. sbintrunc n (bin_rest (sbintrunc n bin)) = bin_rest (sbintrunc n bin)" |
|
755 |
apply (induct n, simp) |
|
756 |
apply (case_tac bin rule: bin_exhaust) |
|
757 |
apply (auto simp: bintrunc_bintrunc_l split: bit.splits) |
|
758 |
done |
|
759 |
||
760 |
lemma bintrunc_rest': |
|
761 |
"bintrunc n o bin_rest o bintrunc n = bin_rest o bintrunc n" |
|
762 |
by (rule ext) auto |
|
763 |
||
764 |
lemma sbintrunc_rest' : |
|
765 |
"sbintrunc n o bin_rest o sbintrunc n = bin_rest o sbintrunc n" |
|
766 |
by (rule ext) auto |
|
767 |
||
768 |
lemma rco_lem: |
|
30971 | 769 |
"f o g o f = g o f ==> f o (g o f) ^^ n = g ^^ n o f" |
24333 | 770 |
apply (rule ext) |
771 |
apply (induct_tac n) |
|
772 |
apply (simp_all (no_asm)) |
|
773 |
apply (drule fun_cong) |
|
774 |
apply (unfold o_def) |
|
775 |
apply (erule trans) |
|
776 |
apply simp |
|
777 |
done |
|
778 |
||
30971 | 779 |
lemma rco_alt: "(f o g) ^^ n o f = f o (g o f) ^^ n" |
24333 | 780 |
apply (rule ext) |
781 |
apply (induct n) |
|
782 |
apply (simp_all add: o_def) |
|
783 |
done |
|
784 |
||
785 |
lemmas rco_bintr = bintrunc_rest' |
|
786 |
[THEN rco_lem [THEN fun_cong], unfolded o_def] |
|
787 |
lemmas rco_sbintr = sbintrunc_rest' |
|
788 |
[THEN rco_lem [THEN fun_cong], unfolded o_def] |
|
789 |
||
24364 | 790 |
subsection {* Splitting and concatenation *} |
791 |
||
26557 | 792 |
primrec bin_split :: "nat \<Rightarrow> int \<Rightarrow> int \<times> int" where |
793 |
Z: "bin_split 0 w = (w, Int.Pls)" |
|
794 |
| Suc: "bin_split (Suc n) w = (let (w1, w2) = bin_split n (bin_rest w) |
|
795 |
in (w1, w2 BIT bin_last w))" |
|
24364 | 796 |
|
37667 | 797 |
lemma [code]: |
798 |
"bin_split (Suc n) w = (let (w1, w2) = bin_split n (bin_rest w) in (w1, w2 BIT bin_last w))" |
|
799 |
"bin_split 0 w = (w, 0)" |
|
800 |
by (simp_all add: Pls_def) |
|
801 |
||
26557 | 802 |
primrec bin_cat :: "int \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int" where |
803 |
Z: "bin_cat w 0 v = w" |
|
804 |
| Suc: "bin_cat w (Suc n) v = bin_cat w n (bin_rest v) BIT bin_last v" |
|
24364 | 805 |
|
806 |
subsection {* Miscellaneous lemmas *} |
|
807 |
||
30952
7ab2716dd93b
power operation on functions with syntax o^; power operation on relations with syntax ^^
haftmann
parents:
30940
diff
changeset
|
808 |
lemma funpow_minus_simp: |
30971 | 809 |
"0 < n \<Longrightarrow> f ^^ n = f \<circ> f ^^ (n - 1)" |
30952
7ab2716dd93b
power operation on functions with syntax o^; power operation on relations with syntax ^^
haftmann
parents:
30940
diff
changeset
|
810 |
by (cases n) simp_all |
24364 | 811 |
|
812 |
lemmas funpow_pred_simp [simp] = |
|
45604 | 813 |
funpow_minus_simp [of "number_of bin", simplified nobm1] for bin |
24364 | 814 |
|
815 |
lemmas replicate_minus_simp = |
|
45604 | 816 |
trans [OF gen_minus [where f = "%n. replicate n x"] replicate.replicate_Suc] for x |
24364 | 817 |
|
818 |
lemmas replicate_pred_simp [simp] = |
|
45604 | 819 |
replicate_minus_simp [of "number_of bin", simplified nobm1] for bin |
24364 | 820 |
|
45604 | 821 |
lemmas power_Suc_no [simp] = power_Suc [of "number_of a"] for a |
24364 | 822 |
|
823 |
lemmas power_minus_simp = |
|
45604 | 824 |
trans [OF gen_minus [where f = "power f"] power_Suc] for f |
24364 | 825 |
|
826 |
lemmas power_pred_simp = |
|
45604 | 827 |
power_minus_simp [of "number_of bin", simplified nobm1] for bin |
828 |
lemmas power_pred_simp_no [simp] = power_pred_simp [where f= "number_of f"] for f |
|
24364 | 829 |
|
830 |
lemma list_exhaust_size_gt0: |
|
831 |
assumes y: "\<And>a list. y = a # list \<Longrightarrow> P" |
|
832 |
shows "0 < length y \<Longrightarrow> P" |
|
833 |
apply (cases y, simp) |
|
834 |
apply (rule y) |
|
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
41413
diff
changeset
|
835 |
apply fastforce |
24364 | 836 |
done |
837 |
||
838 |
lemma list_exhaust_size_eq0: |
|
839 |
assumes y: "y = [] \<Longrightarrow> P" |
|
840 |
shows "length y = 0 \<Longrightarrow> P" |
|
841 |
apply (cases y) |
|
842 |
apply (rule y, simp) |
|
843 |
apply simp |
|
844 |
done |
|
845 |
||
846 |
lemma size_Cons_lem_eq: |
|
847 |
"y = xa # list ==> size y = Suc k ==> size list = k" |
|
848 |
by auto |
|
849 |
||
850 |
lemma size_Cons_lem_eq_bin: |
|
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25349
diff
changeset
|
851 |
"y = xa # list ==> size y = number_of (Int.succ k) ==> |
24364 | 852 |
size list = number_of k" |
853 |
by (auto simp: pred_def succ_def split add : split_if_asm) |
|
854 |
||
44939
5930d35c976d
removed unused legacy lemma names, some comment cleanup.
kleing
parents:
44890
diff
changeset
|
855 |
lemmas ls_splits = prod.split prod.split_asm split_if_asm |
24333 | 856 |
|
37654 | 857 |
lemma not_B1_is_B0: "y \<noteq> (1::bit) \<Longrightarrow> y = (0::bit)" |
24333 | 858 |
by (cases y) auto |
859 |
||
860 |
lemma B1_ass_B0: |
|
37654 | 861 |
assumes y: "y = (0::bit) \<Longrightarrow> y = (1::bit)" |
862 |
shows "y = (1::bit)" |
|
24333 | 863 |
apply (rule classical) |
864 |
apply (drule not_B1_is_B0) |
|
865 |
apply (erule y) |
|
866 |
done |
|
867 |
||
868 |
-- "simplifications for specific word lengths" |
|
869 |
lemmas n2s_ths [THEN eq_reflection] = add_2_eq_Suc add_2_eq_Suc' |
|
870 |
||
871 |
lemmas s2n_ths = n2s_ths [symmetric] |
|
872 |
||
873 |
end |