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