author  huffman 
Tue, 13 Dec 2011 11:48:59 +0100  
changeset 45844  6374cd925b18 
parent 45843  c58ce659ce2a 
child 45845  4158f35a5c6f 
permissions  rwrr 
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 

37654  49 
lemma BIT_B0_eq_Bit0 [simp]: "w BIT 0 = Int.Bit0 w" 
26557  50 
unfolding Bit_def Bit0_def by simp 
51 

37654  52 
lemma BIT_B1_eq_Bit1 [simp]: "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 
lemmas PlsMin_defs [intro!] = 
58 
Pls_def Min_def Pls_def [symmetric] Min_def [symmetric] 

59 

60 
lemmas PlsMin_simps [simp] = PlsMin_defs [THEN Eq_TrueI] 

61 

62 
lemma number_of_False_cong: 

63 
"False \<Longrightarrow> number_of x = number_of y" 

64 
by (rule FalseE) 

65 

45604  66 
lemmas BIT_eqE [elim!] = BIT_eq [THEN conjE] 
26557  67 

68 
lemma BIT_eq_iff [simp]: 

69 
"(u BIT b = v BIT c) = (u = v \<and> b = c)" 

70 
by (rule iffI) auto 

71 

72 
lemmas BIT_eqI [intro!] = conjI [THEN BIT_eq_iff [THEN iffD2]] 

73 

74 
lemma less_Bits: 

37654  75 
"(v BIT b < w BIT c) = (v < w  v <= w & b = (0::bit) & c = (1::bit))" 
37667  76 
unfolding Bit_def by (auto simp add: bitval_def split: bit.split) 
24333  77 

26557  78 
lemma le_Bits: 
37654  79 
"(v BIT b <= w BIT c) = (v < w  v <= w & (b ~= (1::bit)  c ~= (0::bit)))" 
37667  80 
unfolding Bit_def by (auto simp add: bitval_def split: bit.split) 
26557  81 

82 
lemma no_no [simp]: "number_of (number_of i) = i" 

83 
unfolding number_of_eq by simp 

84 

85 
lemma Bit_B0: 

37654  86 
"k BIT (0::bit) = k + k" 
26557  87 
by (unfold Bit_def) simp 
88 

89 
lemma Bit_B1: 

37654  90 
"k BIT (1::bit) = k + k + 1" 
26557  91 
by (unfold Bit_def) simp 
92 

37654  93 
lemma Bit_B0_2t: "k BIT (0::bit) = 2 * k" 
26557  94 
by (rule trans, rule Bit_B0) simp 
95 

37654  96 
lemma Bit_B1_2t: "k BIT (1::bit) = 2 * k + 1" 
26557  97 
by (rule trans, rule Bit_B1) simp 
98 

99 
lemma B_mod_2': 

37654  100 
"X = 2 ==> (w BIT (1::bit)) mod X = 1 & (w BIT (0::bit)) mod X = 0" 
26557  101 
apply (simp (no_asm) only: Bit_B0 Bit_B1) 
102 
apply (simp add: z1pmod2) 

24465  103 
done 
24333  104 

26557  105 
lemma B1_mod_2 [simp]: "(Int.Bit1 w) mod 2 = 1" 
106 
unfolding numeral_simps number_of_is_id by (simp add: z1pmod2) 

24333  107 

26557  108 
lemma B0_mod_2 [simp]: "(Int.Bit0 w) mod 2 = 0" 
109 
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

110 

26557  111 
lemma neB1E [elim!]: 
37654  112 
assumes ne: "y \<noteq> (1::bit)" 
113 
assumes y: "y = (0::bit) \<Longrightarrow> P" 

26557  114 
shows "P" 
115 
apply (rule y) 

116 
apply (cases y rule: bit.exhaust, simp) 

117 
apply (simp add: ne) 

118 
done 

26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset

119 

26557  120 
lemma bin_ex_rl: "EX w b. w BIT b = bin" 
121 
apply (unfold Bit_def) 

122 
apply (cases "even bin") 

123 
apply (clarsimp simp: even_equiv_def) 

37667  124 
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

125 
done 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset

126 

26557  127 
lemma bin_exhaust: 
128 
assumes Q: "\<And>x b. bin = x BIT b \<Longrightarrow> Q" 

129 
shows "Q" 

130 
apply (insert bin_ex_rl [of bin]) 

131 
apply (erule exE)+ 

132 
apply (rule Q) 

133 
apply force 

26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset

134 
done 
24333  135 

136 

24465  137 
subsection {* Destructors for binary integers *} 
24364  138 

37546  139 
definition bin_rl :: "int \<Rightarrow> int \<times> bit" where 
140 
"bin_rl w = (bin_rest w, bin_last w)" 

141 

142 
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

143 
unfolding bin_rl_def by (auto simp: bin_rest_BIT bin_last_BIT) 
26557  144 

26514  145 
primrec bin_nth where 
37654  146 
Z: "bin_nth w 0 = (bin_last w = (1::bit))" 
26557  147 
 Suc: "bin_nth w (Suc n) = bin_nth (bin_rest w) n" 
24364  148 

26557  149 
lemma bin_rl_simps [simp]: 
37654  150 
"bin_rl Int.Pls = (Int.Pls, (0::bit))" 
151 
"bin_rl Int.Min = (Int.Min, (1::bit))" 

152 
"bin_rl (Int.Bit0 r) = (r, (0::bit))" 

153 
"bin_rl (Int.Bit1 r) = (r, (1::bit))" 

26557  154 
"bin_rl (r BIT b) = (r, b)" 
155 
unfolding bin_rl_char by simp_all 

156 

157 
lemma bin_abs_lem: 

158 
"bin = (w BIT b) ==> ~ bin = Int.Min > ~ bin = Int.Pls > 

159 
nat (abs w) < nat (abs bin)" 

160 
apply (clarsimp simp add: bin_rl_char) 

161 
apply (unfold Pls_def Min_def Bit_def) 

162 
apply (cases b) 

163 
apply (clarsimp, arith) 

164 
apply (clarsimp, arith) 

165 
done 

166 

167 
lemma bin_induct: 

168 
assumes PPls: "P Int.Pls" 

169 
and PMin: "P Int.Min" 

170 
and PBit: "!!bin bit. P bin ==> P (bin BIT bit)" 

171 
shows "P bin" 

172 
apply (rule_tac P=P and a=bin and f1="nat o abs" 

173 
in wf_measure [THEN wf_induct]) 

174 
apply (simp add: measure_def inv_image_def) 

175 
apply (case_tac x rule: bin_exhaust) 

176 
apply (frule bin_abs_lem) 

177 
apply (auto simp add : PPls PMin PBit) 

178 
done 

179 

180 
lemma numeral_induct: 

181 
assumes Pls: "P Int.Pls" 

182 
assumes Min: "P Int.Min" 

183 
assumes Bit0: "\<And>w. \<lbrakk>P w; w \<noteq> Int.Pls\<rbrakk> \<Longrightarrow> P (Int.Bit0 w)" 

184 
assumes Bit1: "\<And>w. \<lbrakk>P w; w \<noteq> Int.Min\<rbrakk> \<Longrightarrow> P (Int.Bit1 w)" 

185 
shows "P x" 

186 
apply (induct x rule: bin_induct) 

187 
apply (rule Pls) 

188 
apply (rule Min) 

189 
apply (case_tac bit) 

190 
apply (case_tac "bin = Int.Pls") 

191 
apply simp 

192 
apply (simp add: Bit0) 

193 
apply (case_tac "bin = Int.Min") 

194 
apply simp 

195 
apply (simp add: Bit1) 

196 
done 

197 

24465  198 
lemma bin_rest_simps [simp]: 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25349
diff
changeset

199 
"bin_rest Int.Pls = Int.Pls" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25349
diff
changeset

200 
"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

201 
"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

202 
"bin_rest (Int.Bit1 w) = w" 
26514  203 
"bin_rest (w BIT b) = w" 
37546  204 
using bin_rl_simps bin_rl_def by auto 
24465  205 

206 
lemma bin_last_simps [simp]: 

37654  207 
"bin_last Int.Pls = (0::bit)" 
208 
"bin_last Int.Min = (1::bit)" 

209 
"bin_last (Int.Bit0 w) = (0::bit)" 

210 
"bin_last (Int.Bit1 w) = (1::bit)" 

26514  211 
"bin_last (w BIT b) = b" 
37546  212 
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

213 

24333  214 
lemma bin_r_l_extras [simp]: 
37654  215 
"bin_last 0 = (0::bit)" 
216 
"bin_last ( 1) = (1::bit)" 

217 
"bin_last 1 = (1::bit)" 

218 
"bin_last 1 = (1::bit)" 

24333  219 
"bin_rest 1 = 0" 
220 
"bin_rest 0 = 0" 

221 
"bin_rest ( 1) =  1" 

222 
"bin_rest 1 = 1" 

37654  223 
by (simp_all add: bin_last_def bin_rest_def) 
24333  224 

225 
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

226 
unfolding bin_rest_def [symmetric] by auto 
24333  227 

26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset

228 
lemma Bit0_div2 [simp]: "(Int.Bit0 w) div 2 = w" 
37654  229 
using Bit_div2 [where b="(0::bit)"] by simp 
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset

230 

3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset

231 
lemma Bit1_div2 [simp]: "(Int.Bit1 w) div 2 = w" 
37654  232 
using Bit_div2 [where b="(1::bit)"] by simp 
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset

233 

24333  234 
lemma bin_nth_lem [rule_format]: 
235 
"ALL y. bin_nth x = bin_nth y > x = y" 

236 
apply (induct x rule: bin_induct) 

237 
apply safe 

238 
apply (erule rev_mp) 

239 
apply (induct_tac y rule: bin_induct) 

26827
a62f8db42f4a
Deleted subset_antisym in a few proofs, because it is
berghofe
parents:
26557
diff
changeset

240 
apply (safe del: subset_antisym) 
24333  241 
apply (drule_tac x=0 in fun_cong, force) 
242 
apply (erule notE, rule ext, 

243 
drule_tac x="Suc x" in fun_cong, force) 

244 
apply (drule_tac x=0 in fun_cong, force) 

245 
apply (erule rev_mp) 

246 
apply (induct_tac y rule: bin_induct) 

26827
a62f8db42f4a
Deleted subset_antisym in a few proofs, because it is
berghofe
parents:
26557
diff
changeset

247 
apply (safe del: subset_antisym) 
24333  248 
apply (drule_tac x=0 in fun_cong, force) 
249 
apply (erule notE, rule ext, 

250 
drule_tac x="Suc x" in fun_cong, force) 

251 
apply (drule_tac x=0 in fun_cong, force) 

252 
apply (case_tac y rule: bin_exhaust) 

253 
apply clarify 

254 
apply (erule allE) 

255 
apply (erule impE) 

256 
prefer 2 

257 
apply (erule BIT_eqI) 

258 
apply (drule_tac x=0 in fun_cong, force) 

259 
apply (rule ext) 

260 
apply (drule_tac x="Suc ?x" in fun_cong, force) 

261 
done 

262 

263 
lemma bin_nth_eq_iff: "(bin_nth x = bin_nth y) = (x = y)" 

264 
by (auto elim: bin_nth_lem) 

265 

45604  266 
lemmas bin_eqI = ext [THEN bin_nth_eq_iff [THEN iffD1]] 
24333  267 

45543
827bf668c822
HOLWord: add simp rules for bin_rest, bin_last; shorten several proofs
huffman
parents:
45529
diff
changeset

268 
lemma bin_eq_iff: "x = y \<longleftrightarrow> (\<forall>n. bin_nth x n = bin_nth y n)" 
827bf668c822
HOLWord: add simp rules for bin_rest, bin_last; shorten several proofs
huffman
parents:
45529
diff
changeset

269 
by (auto intro!: bin_nth_lem del: equalityI) 
827bf668c822
HOLWord: add simp rules for bin_rest, bin_last; shorten several proofs
huffman
parents:
45529
diff
changeset

270 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25349
diff
changeset

271 
lemma bin_nth_Pls [simp]: "~ bin_nth Int.Pls n" 
24333  272 
by (induct n) auto 
273 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25349
diff
changeset

274 
lemma bin_nth_Min [simp]: "bin_nth Int.Min n" 
24333  275 
by (induct n) auto 
276 

37654  277 
lemma bin_nth_0_BIT: "bin_nth (w BIT b) 0 = (b = (1::bit))" 
24333  278 
by auto 
279 

280 
lemma bin_nth_Suc_BIT: "bin_nth (w BIT b) (Suc n) = bin_nth w n" 

281 
by auto 

282 

283 
lemma bin_nth_minus [simp]: "0 < n ==> bin_nth (w BIT b) n = bin_nth w (n  1)" 

284 
by (cases n) auto 

285 

26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset

286 
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

287 
"0 < n ==> bin_nth (Int.Bit0 w) n = bin_nth w (n  1)" 
37654  288 
using bin_nth_minus [where b="(0::bit)"] by simp 
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset

289 

3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset

290 
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

291 
"0 < n ==> bin_nth (Int.Bit1 w) n = bin_nth w (n  1)" 
37654  292 
using bin_nth_minus [where b="(1::bit)"] by simp 
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset

293 

24333  294 
lemmas bin_nth_0 = bin_nth.simps(1) 
295 
lemmas bin_nth_Suc = bin_nth.simps(2) 

296 

297 
lemmas bin_nth_simps = 

298 
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

299 
bin_nth_minus_Bit0 bin_nth_minus_Bit1 
24333  300 

26557  301 

302 
subsection {* Truncating binary integers *} 

303 

304 
definition 

37667  305 
bin_sign_def: "bin_sign k = (if k \<ge> 0 then 0 else  1)" 
26557  306 

307 
lemma bin_sign_simps [simp]: 

308 
"bin_sign Int.Pls = Int.Pls" 

309 
"bin_sign Int.Min = Int.Min" 

310 
"bin_sign (Int.Bit0 w) = bin_sign w" 

311 
"bin_sign (Int.Bit1 w) = bin_sign w" 

312 
"bin_sign (w BIT b) = bin_sign w" 

37667  313 
by (unfold bin_sign_def numeral_simps Bit_def bitval_def) (simp_all split: bit.split) 
26557  314 

24364  315 
lemma bin_sign_rest [simp]: 
37667  316 
"bin_sign (bin_rest w) = bin_sign w" 
26557  317 
by (cases w rule: bin_exhaust) auto 
24364  318 

37667  319 
primrec bintrunc :: "nat \<Rightarrow> int \<Rightarrow> int" where 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25349
diff
changeset

320 
Z : "bintrunc 0 bin = Int.Pls" 
37667  321 
 Suc : "bintrunc (Suc n) bin = bintrunc n (bin_rest bin) BIT (bin_last bin)" 
24364  322 

37667  323 
primrec sbintrunc :: "nat => int => int" where 
24364  324 
Z : "sbintrunc 0 bin = 
37654  325 
(case bin_last bin of (1::bit) => Int.Min  (0::bit) => Int.Pls)" 
37667  326 
 Suc : "sbintrunc (Suc n) bin = sbintrunc n (bin_rest bin) BIT (bin_last bin)" 
327 

328 
lemma [code]: 

329 
"sbintrunc 0 bin = 

330 
(case bin_last bin of (1::bit) =>  1  (0::bit) => 0)" 

331 
"sbintrunc (Suc n) bin = sbintrunc n (bin_rest bin) BIT (bin_last bin)" 

332 
apply simp_all apply (cases "bin_last bin") apply simp apply (unfold Min_def number_of_is_id) apply simp done 

24364  333 

24333  334 
lemma sign_bintr: 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25349
diff
changeset

335 
"!!w. bin_sign (bintrunc n w) = Int.Pls" 
24333  336 
by (induct n) auto 
337 

338 
lemma bintrunc_mod2p: 

339 
"!!w. bintrunc n w = (w mod 2 ^ n :: int)" 

340 
apply (induct n, clarsimp) 

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

341 
apply (simp add: bin_last_def bin_rest_def Bit_def zmod_zmult2_eq 
24333  342 
cong: number_of_False_cong) 
343 
done 

344 

345 
lemma sbintrunc_mod2p: 

346 
"!!w. sbintrunc n w = ((w + 2 ^ n) mod 2 ^ (Suc n)  2 ^ n :: int)" 

347 
apply (induct n) 

348 
apply clarsimp 

30034  349 
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

350 
apply (simp add: bin_last_def) 
24333  351 
apply (simp add: number_of_eq) 
352 
apply clarsimp 

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

353 
apply (simp add: bin_last_def bin_rest_def Bit_def 
24333  354 
cong: number_of_False_cong) 
30940
663af91c0720
zmod_zmult_zmult1 now subsumed by mod_mult_mult1
haftmann
parents:
30034
diff
changeset

355 
apply (clarsimp simp: mod_mult_mult1 [symmetric] 
24333  356 
zmod_zdiv_equality [THEN diff_eq_eq [THEN iffD2 [THEN sym]]]) 
357 
apply (rule trans [symmetric, OF _ emep1]) 

358 
apply auto 

359 
apply (auto simp: even_def) 

360 
done 

361 

24465  362 
subsection "Simplifications for (s)bintrunc" 
363 

364 
lemma bit_bool: 

37654  365 
"(b = (b' = (1::bit))) = (b' = (if b then (1::bit) else (0::bit)))" 
24465  366 
by (cases b') auto 
367 

368 
lemmas bit_bool1 [simp] = refl [THEN bit_bool [THEN iffD1], symmetric] 

24333  369 

370 
lemma bin_sign_lem: 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25349
diff
changeset

371 
"!!bin. (bin_sign (sbintrunc n bin) = Int.Min) = bin_nth bin n" 
24333  372 
apply (induct n) 
373 
apply (case_tac bin rule: bin_exhaust, case_tac b, auto)+ 

374 
done 

375 

376 
lemma nth_bintr: 

377 
"!!w m. bin_nth (bintrunc m w) n = (n < m & bin_nth w n)" 

378 
apply (induct n) 

379 
apply (case_tac m, auto)[1] 

380 
apply (case_tac m, auto)[1] 

381 
done 

382 

383 
lemma nth_sbintr: 

384 
"!!w m. bin_nth (sbintrunc m w) n = 

385 
(if n < m then bin_nth w n else bin_nth w m)" 

386 
apply (induct n) 

387 
apply (case_tac m, simp_all split: bit.splits)[1] 

388 
apply (case_tac m, simp_all split: bit.splits)[1] 

389 
done 

390 

391 
lemma bin_nth_Bit: 

37654  392 
"bin_nth (w BIT b) n = (n = 0 & b = (1::bit)  (EX m. n = Suc m & bin_nth w m))" 
24333  393 
by (cases n) auto 
394 

26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset

395 
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

396 
"bin_nth (Int.Bit0 w) n = (EX m. n = Suc m & bin_nth w m)" 
37654  397 
using bin_nth_Bit [where b="(0::bit)"] by simp 
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset

398 

3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset

399 
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

400 
"bin_nth (Int.Bit1 w) n = (n = 0  (EX m. n = Suc m & bin_nth w m))" 
37654  401 
using bin_nth_Bit [where b="(1::bit)"] by simp 
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset

402 

24333  403 
lemma bintrunc_bintrunc_l: 
404 
"n <= m ==> (bintrunc m (bintrunc n w) = bintrunc n w)" 

405 
by (rule bin_eqI) (auto simp add : nth_bintr) 

406 

407 
lemma sbintrunc_sbintrunc_l: 

408 
"n <= m ==> (sbintrunc m (sbintrunc n w) = sbintrunc n w)" 

32439  409 
by (rule bin_eqI) (auto simp: nth_sbintr) 
24333  410 

411 
lemma bintrunc_bintrunc_ge: 

412 
"n <= m ==> (bintrunc n (bintrunc m w) = bintrunc n w)" 

413 
by (rule bin_eqI) (auto simp: nth_bintr) 

414 

415 
lemma bintrunc_bintrunc_min [simp]: 

416 
"bintrunc m (bintrunc n w) = bintrunc (min m n) w" 

417 
apply (rule bin_eqI) 

418 
apply (auto simp: nth_bintr) 

419 
done 

420 

421 
lemma sbintrunc_sbintrunc_min [simp]: 

422 
"sbintrunc m (sbintrunc n w) = sbintrunc (min m n) w" 

423 
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

424 
apply (auto simp: nth_sbintr min_max.inf_absorb1 min_max.inf_absorb2) 
24333  425 
done 
426 

427 
lemmas bintrunc_Pls = 

45604  428 
bintrunc.Suc [where bin="Int.Pls", simplified bin_last_simps bin_rest_simps] 
24333  429 

430 
lemmas bintrunc_Min [simp] = 

45604  431 
bintrunc.Suc [where bin="Int.Min", simplified bin_last_simps bin_rest_simps] 
24333  432 

433 
lemmas bintrunc_BIT [simp] = 

45604  434 
bintrunc.Suc [where bin="w BIT b", simplified bin_last_simps bin_rest_simps] for w b 
24333  435 

26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset

436 
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

437 
"bintrunc (Suc n) (Int.Bit0 w) = Int.Bit0 (bintrunc n w)" 
37654  438 
using bintrunc_BIT [where b="(0::bit)"] by simp 
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset

439 

3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset

440 
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

441 
"bintrunc (Suc n) (Int.Bit1 w) = Int.Bit1 (bintrunc n w)" 
37654  442 
using bintrunc_BIT [where b="(1::bit)"] by simp 
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset

443 

24333  444 
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

445 
bintrunc_Bit0 bintrunc_Bit1 
24333  446 

447 
lemmas sbintrunc_Suc_Pls = 

45604  448 
sbintrunc.Suc [where bin="Int.Pls", simplified bin_last_simps bin_rest_simps] 
24333  449 

450 
lemmas sbintrunc_Suc_Min = 

45604  451 
sbintrunc.Suc [where bin="Int.Min", simplified bin_last_simps bin_rest_simps] 
24333  452 

453 
lemmas sbintrunc_Suc_BIT [simp] = 

45604  454 
sbintrunc.Suc [where bin="w BIT b", simplified bin_last_simps bin_rest_simps] for w b 
24333  455 

26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset

456 
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

457 
"sbintrunc (Suc n) (Int.Bit0 w) = Int.Bit0 (sbintrunc n w)" 
37654  458 
using sbintrunc_Suc_BIT [where b="(0::bit)"] by simp 
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset

459 

3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset

460 
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

461 
"sbintrunc (Suc n) (Int.Bit1 w) = Int.Bit1 (sbintrunc n w)" 
37654  462 
using sbintrunc_Suc_BIT [where b="(1::bit)"] by simp 
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset

463 

24333  464 
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

465 
sbintrunc_Suc_Bit0 sbintrunc_Suc_Bit1 
24333  466 

467 
lemmas sbintrunc_Pls = 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25349
diff
changeset

468 
sbintrunc.Z [where bin="Int.Pls", 
45604  469 
simplified bin_last_simps bin_rest_simps bit.simps] 
24333  470 

471 
lemmas sbintrunc_Min = 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25349
diff
changeset

472 
sbintrunc.Z [where bin="Int.Min", 
45604  473 
simplified bin_last_simps bin_rest_simps bit.simps] 
24333  474 

475 
lemmas sbintrunc_0_BIT_B0 [simp] = 

37654  476 
sbintrunc.Z [where bin="w BIT (0::bit)", 
45604  477 
simplified bin_last_simps bin_rest_simps bit.simps] for w 
24333  478 

479 
lemmas sbintrunc_0_BIT_B1 [simp] = 

37654  480 
sbintrunc.Z [where bin="w BIT (1::bit)", 
45604  481 
simplified bin_last_simps bin_rest_simps bit.simps] for w 
24333  482 

26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset

483 
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

484 
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

485 

3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset

486 
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

487 
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

488 

24333  489 
lemmas sbintrunc_0_simps = 
490 
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

491 
sbintrunc_0_Bit0 sbintrunc_0_Bit1 
24333  492 

493 
lemmas bintrunc_simps = bintrunc.Z bintrunc_Sucs 

494 
lemmas sbintrunc_simps = sbintrunc_0_simps sbintrunc_Sucs 

495 

496 
lemma bintrunc_minus: 

497 
"0 < n ==> bintrunc (Suc (n  1)) w = bintrunc n w" 

498 
by auto 

499 

500 
lemma sbintrunc_minus: 

501 
"0 < n ==> sbintrunc (Suc (n  1)) w = sbintrunc n w" 

502 
by auto 

503 

504 
lemmas bintrunc_minus_simps = 

45604  505 
bintrunc_Sucs [THEN [2] bintrunc_minus [symmetric, THEN trans]] 
24333  506 
lemmas sbintrunc_minus_simps = 
45604  507 
sbintrunc_Sucs [THEN [2] sbintrunc_minus [symmetric, THEN trans]] 
24333  508 

509 
lemma bintrunc_n_Pls [simp]: 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25349
diff
changeset

510 
"bintrunc n Int.Pls = Int.Pls" 
24333  511 
by (induct n) auto 
512 

513 
lemma sbintrunc_n_PM [simp]: 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25349
diff
changeset

514 
"sbintrunc n Int.Pls = Int.Pls" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25349
diff
changeset

515 
"sbintrunc n Int.Min = Int.Min" 
24333  516 
by (induct n) auto 
517 

45604  518 
lemmas thobini1 = arg_cong [where f = "%w. w BIT b"] for b 
24333  519 

520 
lemmas bintrunc_BIT_I = trans [OF bintrunc_BIT thobini1] 

521 
lemmas bintrunc_Min_I = trans [OF bintrunc_Min thobini1] 

522 

45604  523 
lemmas bmsts = bintrunc_minus_simps(13) [THEN thobini1 [THEN [2] trans]] 
24333  524 
lemmas bintrunc_Pls_minus_I = bmsts(1) 
525 
lemmas bintrunc_Min_minus_I = bmsts(2) 

526 
lemmas bintrunc_BIT_minus_I = bmsts(3) 

527 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25349
diff
changeset

528 
lemma bintrunc_0_Min: "bintrunc 0 Int.Min = Int.Pls" 
24333  529 
by auto 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25349
diff
changeset

530 
lemma bintrunc_0_BIT: "bintrunc 0 (w BIT b) = Int.Pls" 
24333  531 
by auto 
532 

533 
lemma bintrunc_Suc_lem: 

534 
"bintrunc (Suc n) x = y ==> m = Suc n ==> bintrunc m x = y" 

535 
by auto 

536 

537 
lemmas bintrunc_Suc_Ialts = 

45604  538 
bintrunc_Min_I [THEN bintrunc_Suc_lem] 
539 
bintrunc_BIT_I [THEN bintrunc_Suc_lem] 

24333  540 

541 
lemmas sbintrunc_BIT_I = trans [OF sbintrunc_Suc_BIT thobini1] 

542 

543 
lemmas sbintrunc_Suc_Is = 

45604  544 
sbintrunc_Sucs(13) [THEN thobini1 [THEN [2] trans]] 
24333  545 

546 
lemmas sbintrunc_Suc_minus_Is = 

45604  547 
sbintrunc_minus_simps(13) [THEN thobini1 [THEN [2] trans]] 
24333  548 

549 
lemma sbintrunc_Suc_lem: 

550 
"sbintrunc (Suc n) x = y ==> m = Suc n ==> sbintrunc m x = y" 

551 
by auto 

552 

553 
lemmas sbintrunc_Suc_Ialts = 

45604  554 
sbintrunc_Suc_Is [THEN sbintrunc_Suc_lem] 
24333  555 

556 
lemma sbintrunc_bintrunc_lt: 

557 
"m > n ==> sbintrunc n (bintrunc m w) = sbintrunc n w" 

558 
by (rule bin_eqI) (auto simp: nth_sbintr nth_bintr) 

559 

560 
lemma bintrunc_sbintrunc_le: 

561 
"m <= Suc n ==> bintrunc m (sbintrunc n w) = bintrunc m w" 

562 
apply (rule bin_eqI) 

563 
apply (auto simp: nth_sbintr nth_bintr) 

564 
apply (subgoal_tac "x=n", safe, arith+)[1] 

565 
apply (subgoal_tac "x=n", safe, arith+)[1] 

566 
done 

567 

568 
lemmas bintrunc_sbintrunc [simp] = order_refl [THEN bintrunc_sbintrunc_le] 

569 
lemmas sbintrunc_bintrunc [simp] = lessI [THEN sbintrunc_bintrunc_lt] 

570 
lemmas bintrunc_bintrunc [simp] = order_refl [THEN bintrunc_bintrunc_l] 

571 
lemmas sbintrunc_sbintrunc [simp] = order_refl [THEN sbintrunc_sbintrunc_l] 

572 

573 
lemma bintrunc_sbintrunc' [simp]: 

574 
"0 < n \<Longrightarrow> bintrunc n (sbintrunc (n  1) w) = bintrunc n w" 

575 
by (cases n) (auto simp del: bintrunc.Suc) 

576 

577 
lemma sbintrunc_bintrunc' [simp]: 

578 
"0 < n \<Longrightarrow> sbintrunc (n  1) (bintrunc n w) = sbintrunc (n  1) w" 

579 
by (cases n) (auto simp del: bintrunc.Suc) 

580 

581 
lemma bin_sbin_eq_iff: 

582 
"bintrunc (Suc n) x = bintrunc (Suc n) y <> 

583 
sbintrunc n x = sbintrunc n y" 

584 
apply (rule iffI) 

585 
apply (rule box_equals [OF _ sbintrunc_bintrunc sbintrunc_bintrunc]) 

586 
apply simp 

587 
apply (rule box_equals [OF _ bintrunc_sbintrunc bintrunc_sbintrunc]) 

588 
apply simp 

589 
done 

590 

591 
lemma bin_sbin_eq_iff': 

592 
"0 < n \<Longrightarrow> bintrunc n x = bintrunc n y <> 

593 
sbintrunc (n  1) x = sbintrunc (n  1) y" 

594 
by (cases n) (simp_all add: bin_sbin_eq_iff del: bintrunc.Suc) 

595 

596 
lemmas bintrunc_sbintruncS0 [simp] = bintrunc_sbintrunc' [unfolded One_nat_def] 

597 
lemmas sbintrunc_bintruncS0 [simp] = sbintrunc_bintrunc' [unfolded One_nat_def] 

598 

599 
lemmas bintrunc_bintrunc_l' = le_add1 [THEN bintrunc_bintrunc_l] 

600 
lemmas sbintrunc_sbintrunc_l' = le_add1 [THEN sbintrunc_sbintrunc_l] 

601 

602 
(* although bintrunc_minus_simps, if added to default simpset, 

603 
tends to get applied where it's not wanted in developing the theories, 

604 
we get a version for when the word length is given literally *) 

605 

606 
lemmas nat_non0_gr = 

45604  607 
trans [OF iszero_def [THEN Not_eq_iff [THEN iffD2]] refl] 
24333  608 

609 
lemmas bintrunc_pred_simps [simp] = 

45604  610 
bintrunc_minus_simps [of "number_of bin", simplified nobm1] for bin 
24333  611 

612 
lemmas sbintrunc_pred_simps [simp] = 

45604  613 
sbintrunc_minus_simps [of "number_of bin", simplified nobm1] for bin 
24333  614 

615 
lemma no_bintr_alt: 

616 
"number_of (bintrunc n w) = w mod 2 ^ n" 

617 
by (simp add: number_of_eq bintrunc_mod2p) 

618 

619 
lemma no_bintr_alt1: "bintrunc n = (%w. w mod 2 ^ n :: int)" 

620 
by (rule ext) (rule bintrunc_mod2p) 

621 

622 
lemma range_bintrunc: "range (bintrunc n) = {i. 0 <= i & i < 2 ^ n}" 

623 
apply (unfold no_bintr_alt1) 

624 
apply (auto simp add: image_iff) 

625 
apply (rule exI) 

626 
apply (auto intro: int_mod_lem [THEN iffD1, symmetric]) 

627 
done 

628 

629 
lemma no_bintr: 

630 
"number_of (bintrunc n w) = (number_of w mod 2 ^ n :: int)" 

631 
by (simp add : bintrunc_mod2p number_of_eq) 

632 

633 
lemma no_sbintr_alt2: 

634 
"sbintrunc n = (%w. (w + 2 ^ n) mod 2 ^ Suc n  2 ^ n :: int)" 

635 
by (rule ext) (simp add : sbintrunc_mod2p) 

636 

637 
lemma no_sbintr: 

638 
"number_of (sbintrunc n w) = 

639 
((number_of w + 2 ^ n) mod 2 ^ Suc n  2 ^ n :: int)" 

640 
by (simp add : no_sbintr_alt2 number_of_eq) 

641 

642 
lemma range_sbintrunc: 

643 
"range (sbintrunc n) = {i.  (2 ^ n) <= i & i < 2 ^ n}" 

644 
apply (unfold no_sbintr_alt2) 

645 
apply (auto simp add: image_iff eq_diff_eq) 

646 
apply (rule exI) 

647 
apply (auto intro: int_mod_lem [THEN iffD1, symmetric]) 

648 
done 

649 

25349
0d46bea01741
eliminated illegal schematic variables in where/of;
wenzelm
parents:
25134
diff
changeset

650 
lemma sb_inc_lem: 
0d46bea01741
eliminated illegal schematic variables in where/of;
wenzelm
parents:
25134
diff
changeset

651 
"(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

652 
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

653 
apply (rule TrueI) 
0d46bea01741
eliminated illegal schematic variables in where/of;
wenzelm
parents:
25134
diff
changeset

654 
done 
24333  655 

25349
0d46bea01741
eliminated illegal schematic variables in where/of;
wenzelm
parents:
25134
diff
changeset

656 
lemma sb_inc_lem': 
0d46bea01741
eliminated illegal schematic variables in where/of;
wenzelm
parents:
25134
diff
changeset

657 
"(a::int) <  (2^k) \<Longrightarrow> a + 2^k + 2^(Suc k) <= (a + 2^k) mod 2^(Suc k)" 
35048  658 
by (rule sb_inc_lem) simp 
24333  659 

660 
lemma sbintrunc_inc: 

25349
0d46bea01741
eliminated illegal schematic variables in where/of;
wenzelm
parents:
25134
diff
changeset

661 
"x <  (2^n) ==> x + 2^(Suc n) <= sbintrunc n x" 
24333  662 
unfolding no_sbintr_alt2 by (drule sb_inc_lem') simp 
663 

25349
0d46bea01741
eliminated illegal schematic variables in where/of;
wenzelm
parents:
25134
diff
changeset

664 
lemma sb_dec_lem: 
0d46bea01741
eliminated illegal schematic variables in where/of;
wenzelm
parents:
25134
diff
changeset

665 
"(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

666 
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

667 
simplified zless2p, OF _ TrueI, simplified]) 
24333  668 

25349
0d46bea01741
eliminated illegal schematic variables in where/of;
wenzelm
parents:
25134
diff
changeset

669 
lemma sb_dec_lem': 
0d46bea01741
eliminated illegal schematic variables in where/of;
wenzelm
parents:
25134
diff
changeset

670 
"(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

671 
by (rule iffD1 [OF diff_le_eq', THEN sb_dec_lem, simplified]) 
24333  672 

673 
lemma sbintrunc_dec: 

674 
"x >= (2 ^ n) ==> x  2 ^ (Suc n) >= sbintrunc n x" 

675 
unfolding no_sbintr_alt2 by (drule sb_dec_lem') simp 

676 

45604  677 
lemmas zmod_uminus' = zmod_uminus [where b=c] for c 
678 
lemmas zpower_zmod' = zpower_zmod [where m=c and y=k] for c k 

24333  679 

680 
lemmas brdmod1s' [symmetric] = 

30034  681 
mod_add_left_eq mod_add_right_eq 
24333  682 
zmod_zsub_left_eq zmod_zsub_right_eq 
683 
zmod_zmult1_eq zmod_zmult1_eq_rev 

684 

685 
lemmas brdmods' [symmetric] = 

686 
zpower_zmod' [symmetric] 

30034  687 
trans [OF mod_add_left_eq mod_add_right_eq] 
24333  688 
trans [OF zmod_zsub_left_eq zmod_zsub_right_eq] 
689 
trans [OF zmod_zmult1_eq zmod_zmult1_eq_rev] 

690 
zmod_uminus' [symmetric] 

30034  691 
mod_add_left_eq [where b = "1::int"] 
24333  692 
zmod_zsub_left_eq [where b = "1"] 
693 

694 
lemmas bintr_arith1s = 

45604  695 
brdmod1s' [where c="2^n::int", folded pred_def succ_def bintrunc_mod2p] for n 
24333  696 
lemmas bintr_ariths = 
45604  697 
brdmods' [where c="2^n::int", folded pred_def succ_def bintrunc_mod2p] for n 
24333  698 

45604  699 
lemmas m2pths = pos_mod_sign pos_mod_bound [OF zless2p] 
24364  700 

24333  701 
lemma bintr_ge0: "(0 :: int) <= number_of (bintrunc n w)" 
702 
by (simp add : no_bintr m2pths) 

703 

704 
lemma bintr_lt2p: "number_of (bintrunc n w) < (2 ^ n :: int)" 

705 
by (simp add : no_bintr m2pths) 

706 

707 
lemma bintr_Min: 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25349
diff
changeset

708 
"number_of (bintrunc n Int.Min) = (2 ^ n :: int)  1" 
24333  709 
by (simp add : no_bintr m1mod2k) 
710 

711 
lemma sbintr_ge: "( (2 ^ n) :: int) <= number_of (sbintrunc n w)" 

712 
by (simp add : no_sbintr m2pths) 

713 

714 
lemma sbintr_lt: "number_of (sbintrunc n w) < (2 ^ n :: int)" 

715 
by (simp add : no_sbintr m2pths) 

716 

717 
lemma bintrunc_Suc: 

718 
"bintrunc (Suc n) bin = bintrunc n (bin_rest bin) BIT bin_last bin" 

719 
by (case_tac bin rule: bin_exhaust) auto 

720 

721 
lemma sign_Pls_ge_0: 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25349
diff
changeset

722 
"(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

723 
by (induct bin rule: numeral_induct) auto 
24333  724 

725 
lemma sign_Min_lt_0: 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25349
diff
changeset

726 
"(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

727 
by (induct bin rule: numeral_induct) auto 
24333  728 

729 
lemmas sign_Min_neg = trans [OF sign_Min_lt_0 neg_def [symmetric]] 

730 

731 
lemma bin_rest_trunc: 

732 
"!!bin. (bin_rest (bintrunc n bin)) = bintrunc (n  1) (bin_rest bin)" 

733 
by (induct n) auto 

734 

735 
lemma bin_rest_power_trunc [rule_format] : 

30971  736 
"(bin_rest ^^ k) (bintrunc n bin) = 
737 
bintrunc (n  k) ((bin_rest ^^ k) bin)" 

24333  738 
by (induct k) (auto simp: bin_rest_trunc) 
739 

740 
lemma bin_rest_trunc_i: 

741 
"bintrunc n (bin_rest bin) = bin_rest (bintrunc (Suc n) bin)" 

742 
by auto 

743 

744 
lemma bin_rest_strunc: 

745 
"!!bin. bin_rest (sbintrunc (Suc n) bin) = sbintrunc n (bin_rest bin)" 

746 
by (induct n) auto 

747 

748 
lemma bintrunc_rest [simp]: 

749 
"!!bin. bintrunc n (bin_rest (bintrunc n bin)) = bin_rest (bintrunc n bin)" 

750 
apply (induct n, simp) 

751 
apply (case_tac bin rule: bin_exhaust) 

752 
apply (auto simp: bintrunc_bintrunc_l) 

753 
done 

754 

755 
lemma sbintrunc_rest [simp]: 

756 
"!!bin. sbintrunc n (bin_rest (sbintrunc n bin)) = bin_rest (sbintrunc n bin)" 

757 
apply (induct n, simp) 

758 
apply (case_tac bin rule: bin_exhaust) 

759 
apply (auto simp: bintrunc_bintrunc_l split: bit.splits) 

760 
done 

761 

762 
lemma bintrunc_rest': 

763 
"bintrunc n o bin_rest o bintrunc n = bin_rest o bintrunc n" 

764 
by (rule ext) auto 

765 

766 
lemma sbintrunc_rest' : 

767 
"sbintrunc n o bin_rest o sbintrunc n = bin_rest o sbintrunc n" 

768 
by (rule ext) auto 

769 

770 
lemma rco_lem: 

30971  771 
"f o g o f = g o f ==> f o (g o f) ^^ n = g ^^ n o f" 
24333  772 
apply (rule ext) 
773 
apply (induct_tac n) 

774 
apply (simp_all (no_asm)) 

775 
apply (drule fun_cong) 

776 
apply (unfold o_def) 

777 
apply (erule trans) 

778 
apply simp 

779 
done 

780 

30971  781 
lemma rco_alt: "(f o g) ^^ n o f = f o (g o f) ^^ n" 
24333  782 
apply (rule ext) 
783 
apply (induct n) 

784 
apply (simp_all add: o_def) 

785 
done 

786 

787 
lemmas rco_bintr = bintrunc_rest' 

788 
[THEN rco_lem [THEN fun_cong], unfolded o_def] 

789 
lemmas rco_sbintr = sbintrunc_rest' 

790 
[THEN rco_lem [THEN fun_cong], unfolded o_def] 

791 

24364  792 
subsection {* Splitting and concatenation *} 
793 

26557  794 
primrec bin_split :: "nat \<Rightarrow> int \<Rightarrow> int \<times> int" where 
795 
Z: "bin_split 0 w = (w, Int.Pls)" 

796 
 Suc: "bin_split (Suc n) w = (let (w1, w2) = bin_split n (bin_rest w) 

797 
in (w1, w2 BIT bin_last w))" 

24364  798 

37667  799 
lemma [code]: 
800 
"bin_split (Suc n) w = (let (w1, w2) = bin_split n (bin_rest w) in (w1, w2 BIT bin_last w))" 

801 
"bin_split 0 w = (w, 0)" 

802 
by (simp_all add: Pls_def) 

803 

26557  804 
primrec bin_cat :: "int \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int" where 
805 
Z: "bin_cat w 0 v = w" 

806 
 Suc: "bin_cat w (Suc n) v = bin_cat w n (bin_rest v) BIT bin_last v" 

24364  807 

808 
subsection {* Miscellaneous lemmas *} 

809 

30952
7ab2716dd93b
power operation on functions with syntax o^; power operation on relations with syntax ^^
haftmann
parents:
30940
diff
changeset

810 
lemma funpow_minus_simp: 
30971  811 
"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

812 
by (cases n) simp_all 
24364  813 

814 
lemmas funpow_pred_simp [simp] = 

45604  815 
funpow_minus_simp [of "number_of bin", simplified nobm1] for bin 
24364  816 

817 
lemmas replicate_minus_simp = 

45604  818 
trans [OF gen_minus [where f = "%n. replicate n x"] replicate.replicate_Suc] for x 
24364  819 

820 
lemmas replicate_pred_simp [simp] = 

45604  821 
replicate_minus_simp [of "number_of bin", simplified nobm1] for bin 
24364  822 

45604  823 
lemmas power_Suc_no [simp] = power_Suc [of "number_of a"] for a 
24364  824 

825 
lemmas power_minus_simp = 

45604  826 
trans [OF gen_minus [where f = "power f"] power_Suc] for f 
24364  827 

828 
lemmas power_pred_simp = 

45604  829 
power_minus_simp [of "number_of bin", simplified nobm1] for bin 
830 
lemmas power_pred_simp_no [simp] = power_pred_simp [where f= "number_of f"] for f 

24364  831 

832 
lemma list_exhaust_size_gt0: 

833 
assumes y: "\<And>a list. y = a # list \<Longrightarrow> P" 

834 
shows "0 < length y \<Longrightarrow> P" 

835 
apply (cases y, simp) 

836 
apply (rule y) 

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
41413
diff
changeset

837 
apply fastforce 
24364  838 
done 
839 

840 
lemma list_exhaust_size_eq0: 

841 
assumes y: "y = [] \<Longrightarrow> P" 

842 
shows "length y = 0 \<Longrightarrow> P" 

843 
apply (cases y) 

844 
apply (rule y, simp) 

845 
apply simp 

846 
done 

847 

848 
lemma size_Cons_lem_eq: 

849 
"y = xa # list ==> size y = Suc k ==> size list = k" 

850 
by auto 

851 

852 
lemma size_Cons_lem_eq_bin: 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25349
diff
changeset

853 
"y = xa # list ==> size y = number_of (Int.succ k) ==> 
24364  854 
size list = number_of k" 
855 
by (auto simp: pred_def succ_def split add : split_if_asm) 

856 

44939
5930d35c976d
removed unused legacy lemma names, some comment cleanup.
kleing
parents:
44890
diff
changeset

857 
lemmas ls_splits = prod.split prod.split_asm split_if_asm 
24333  858 

37654  859 
lemma not_B1_is_B0: "y \<noteq> (1::bit) \<Longrightarrow> y = (0::bit)" 
24333  860 
by (cases y) auto 
861 

862 
lemma B1_ass_B0: 

37654  863 
assumes y: "y = (0::bit) \<Longrightarrow> y = (1::bit)" 
864 
shows "y = (1::bit)" 

24333  865 
apply (rule classical) 
866 
apply (drule not_B1_is_B0) 

867 
apply (erule y) 

868 
done 

869 

870 
 "simplifications for specific word lengths" 

871 
lemmas n2s_ths [THEN eq_reflection] = add_2_eq_Suc add_2_eq_Suc' 

872 

873 
lemmas s2n_ths = n2s_ths [symmetric] 

874 

875 
end 