author  huffman 
Thu, 22 Dec 2011 12:14:26 +0100  
changeset 45952  ed9cc0634aaf 
parent 45856  caa99836aed8 
child 45953  1d6fcb19aa50 
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 

45848  46 
lemma BIT_eq_iff [iff]: "u BIT b = v BIT c \<longleftrightarrow> u = v \<and> b = c" 
45843
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 

45849  49 
lemma BIT_bin_simps [simp]: 
50 
"number_of w BIT 0 = number_of (Int.Bit0 w)" 

51 
"number_of w BIT 1 = number_of (Int.Bit1 w)" 

52 
unfolding Bit_def number_of_is_id numeral_simps by simp_all 

53 

54 
lemma BIT_special_simps [simp]: 

55 
shows "0 BIT 0 = 0" and "0 BIT 1 = 1" and "1 BIT 0 = 2" and "1 BIT 1 = 3" 

56 
unfolding Bit_def by simp_all 

57 

45851
19f7ac6cf3cc
add simp rules for bin_rest and bin_last applied to numerals
huffman
parents:
45850
diff
changeset

58 
lemma bin_last_numeral_simps [simp]: 
19f7ac6cf3cc
add simp rules for bin_rest and bin_last applied to numerals
huffman
parents:
45850
diff
changeset

59 
"bin_last 0 = 0" 
19f7ac6cf3cc
add simp rules for bin_rest and bin_last applied to numerals
huffman
parents:
45850
diff
changeset

60 
"bin_last 1 = 1" 
19f7ac6cf3cc
add simp rules for bin_rest and bin_last applied to numerals
huffman
parents:
45850
diff
changeset

61 
"bin_last 1 = 1" 
19f7ac6cf3cc
add simp rules for bin_rest and bin_last applied to numerals
huffman
parents:
45850
diff
changeset

62 
"bin_last (number_of (Int.Bit0 w)) = 0" 
19f7ac6cf3cc
add simp rules for bin_rest and bin_last applied to numerals
huffman
parents:
45850
diff
changeset

63 
"bin_last (number_of (Int.Bit1 w)) = 1" 
19f7ac6cf3cc
add simp rules for bin_rest and bin_last applied to numerals
huffman
parents:
45850
diff
changeset

64 
unfolding bin_last_def by simp_all 
19f7ac6cf3cc
add simp rules for bin_rest and bin_last applied to numerals
huffman
parents:
45850
diff
changeset

65 

19f7ac6cf3cc
add simp rules for bin_rest and bin_last applied to numerals
huffman
parents:
45850
diff
changeset

66 
lemma bin_rest_numeral_simps [simp]: 
19f7ac6cf3cc
add simp rules for bin_rest and bin_last applied to numerals
huffman
parents:
45850
diff
changeset

67 
"bin_rest 0 = 0" 
19f7ac6cf3cc
add simp rules for bin_rest and bin_last applied to numerals
huffman
parents:
45850
diff
changeset

68 
"bin_rest 1 = 0" 
19f7ac6cf3cc
add simp rules for bin_rest and bin_last applied to numerals
huffman
parents:
45850
diff
changeset

69 
"bin_rest 1 = 1" 
19f7ac6cf3cc
add simp rules for bin_rest and bin_last applied to numerals
huffman
parents:
45850
diff
changeset

70 
"bin_rest (number_of (Int.Bit0 w)) = number_of w" 
19f7ac6cf3cc
add simp rules for bin_rest and bin_last applied to numerals
huffman
parents:
45850
diff
changeset

71 
"bin_rest (number_of (Int.Bit1 w)) = number_of w" 
19f7ac6cf3cc
add simp rules for bin_rest and bin_last applied to numerals
huffman
parents:
45850
diff
changeset

72 
unfolding bin_rest_def by simp_all 
19f7ac6cf3cc
add simp rules for bin_rest and bin_last applied to numerals
huffman
parents:
45850
diff
changeset

73 

45847  74 
lemma BIT_B0_eq_Bit0: "w BIT 0 = Int.Bit0 w" 
26557  75 
unfolding Bit_def Bit0_def by simp 
76 

45847  77 
lemma BIT_B1_eq_Bit1: "w BIT 1 = Int.Bit1 w" 
26557  78 
unfolding Bit_def Bit1_def by simp 
79 

80 
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

81 

26557  82 
lemma number_of_False_cong: 
83 
"False \<Longrightarrow> number_of x = number_of y" 

84 
by (rule FalseE) 

85 

86 
lemma less_Bits: 

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

26557  90 
lemma le_Bits: 
37654  91 
"(v BIT b <= w BIT c) = (v < w  v <= w & (b ~= (1::bit)  c ~= (0::bit)))" 
37667  92 
unfolding Bit_def by (auto simp add: bitval_def split: bit.split) 
26557  93 

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

95 
unfolding number_of_eq by simp 

96 

97 
lemma Bit_B0: 

37654  98 
"k BIT (0::bit) = k + k" 
26557  99 
by (unfold Bit_def) simp 
100 

101 
lemma Bit_B1: 

37654  102 
"k BIT (1::bit) = k + k + 1" 
26557  103 
by (unfold Bit_def) simp 
104 

37654  105 
lemma Bit_B0_2t: "k BIT (0::bit) = 2 * k" 
26557  106 
by (rule trans, rule Bit_B0) simp 
107 

37654  108 
lemma Bit_B1_2t: "k BIT (1::bit) = 2 * k + 1" 
26557  109 
by (rule trans, rule Bit_B1) simp 
110 

111 
lemma B_mod_2': 

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

24465  115 
done 
24333  116 

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

24333  119 

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

122 

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

26557  126 
shows "P" 
127 
apply (rule y) 

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

129 
apply (simp add: ne) 

130 
done 

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

131 

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

134 
apply (cases "even bin") 

135 
apply (clarsimp simp: even_equiv_def) 

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

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

138 

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

141 
shows "Q" 

142 
apply (insert bin_ex_rl [of bin]) 

143 
apply (erule exE)+ 

144 
apply (rule Q) 

145 
apply force 

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

146 
done 
24333  147 

148 

24465  149 
subsection {* Destructors for binary integers *} 
24364  150 

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

153 

154 
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

155 
unfolding bin_rl_def by (auto simp: bin_rest_BIT bin_last_BIT) 
26557  156 

26514  157 
primrec bin_nth where 
37654  158 
Z: "bin_nth w 0 = (bin_last w = (1::bit))" 
26557  159 
 Suc: "bin_nth w (Suc n) = bin_nth (bin_rest w) n" 
24364  160 

26557  161 
lemma bin_rl_simps [simp]: 
37654  162 
"bin_rl Int.Pls = (Int.Pls, (0::bit))" 
163 
"bin_rl Int.Min = (Int.Min, (1::bit))" 

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

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

26557  166 
"bin_rl (r BIT b) = (r, b)" 
45847  167 
unfolding bin_rl_char by (simp_all add: BIT_simps) 
26557  168 

169 
lemma bin_abs_lem: 

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

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

172 
apply (clarsimp simp add: bin_rl_char) 

173 
apply (unfold Pls_def Min_def Bit_def) 

174 
apply (cases b) 

175 
apply (clarsimp, arith) 

176 
apply (clarsimp, arith) 

177 
done 

178 

179 
lemma bin_induct: 

180 
assumes PPls: "P Int.Pls" 

181 
and PMin: "P Int.Min" 

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

183 
shows "P bin" 

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

185 
in wf_measure [THEN wf_induct]) 

186 
apply (simp add: measure_def inv_image_def) 

187 
apply (case_tac x rule: bin_exhaust) 

188 
apply (frule bin_abs_lem) 

189 
apply (auto simp add : PPls PMin PBit) 

190 
done 

191 

192 
lemma numeral_induct: 

193 
assumes Pls: "P Int.Pls" 

194 
assumes Min: "P Int.Min" 

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

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

197 
shows "P x" 

198 
apply (induct x rule: bin_induct) 

199 
apply (rule Pls) 

200 
apply (rule Min) 

201 
apply (case_tac bit) 

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

45847  203 
apply (simp add: BIT_simps) 
204 
apply (simp add: Bit0 BIT_simps) 

26557  205 
apply (case_tac "bin = Int.Min") 
45847  206 
apply (simp add: BIT_simps) 
207 
apply (simp add: Bit1 BIT_simps) 

26557  208 
done 
209 

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

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

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

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

214 
"bin_rest (Int.Bit1 w) = w" 
26514  215 
"bin_rest (w BIT b) = w" 
37546  216 
using bin_rl_simps bin_rl_def by auto 
24465  217 

218 
lemma bin_last_simps [simp]: 

37654  219 
"bin_last Int.Pls = (0::bit)" 
220 
"bin_last Int.Min = (1::bit)" 

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

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

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

225 

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

227 
unfolding bin_rest_def [symmetric] by auto 
24333  228 

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

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

231 

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

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

234 

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

237 
apply (induct x rule: bin_induct) 

238 
apply safe 

239 
apply (erule rev_mp) 

240 
apply (induct_tac y rule: bin_induct) 

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

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

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

45847  245 
apply (drule_tac x=0 in fun_cong, force simp: BIT_simps) 
24333  246 
apply (erule rev_mp) 
247 
apply (induct_tac y rule: bin_induct) 

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

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

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

45847  252 
apply (drule_tac x=0 in fun_cong, force simp: BIT_simps) 
24333  253 
apply (case_tac y rule: bin_exhaust) 
254 
apply clarify 

255 
apply (erule allE) 

256 
apply (erule impE) 

257 
prefer 2 

45848  258 
apply (erule conjI) 
24333  259 
apply (drule_tac x=0 in fun_cong, force) 
260 
apply (rule ext) 

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

262 
done 

263 

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

265 
by (auto elim: bin_nth_lem) 

266 

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

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

269 
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

270 
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

271 

45853  272 
lemma bin_nth_zero [simp]: "\<not> bin_nth 0 n" 
273 
by (induct n) auto 

274 

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

275 
lemma bin_nth_Pls [simp]: "~ bin_nth Int.Pls n" 
24333  276 
by (induct n) auto 
277 

45952  278 
lemma bin_nth_minus1 [simp]: "bin_nth 1 n" 
279 
by (induct n) auto 

280 

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

281 
lemma bin_nth_Min [simp]: "bin_nth Int.Min n" 
24333  282 
by (induct n) auto 
283 

37654  284 
lemma bin_nth_0_BIT: "bin_nth (w BIT b) 0 = (b = (1::bit))" 
24333  285 
by auto 
286 

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

288 
by auto 

289 

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

291 
by (cases n) auto 

292 

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

293 
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

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

296 

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

297 
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

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

300 

24333  301 
lemmas bin_nth_0 = bin_nth.simps(1) 
302 
lemmas bin_nth_Suc = bin_nth.simps(2) 

303 

304 
lemmas bin_nth_simps = 

305 
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

306 
bin_nth_minus_Bit0 bin_nth_minus_Bit1 
24333  307 

26557  308 

309 
subsection {* Truncating binary integers *} 

310 

45846  311 
definition bin_sign :: "int \<Rightarrow> int" where 
37667  312 
bin_sign_def: "bin_sign k = (if k \<ge> 0 then 0 else  1)" 
26557  313 

314 
lemma bin_sign_simps [simp]: 

45850  315 
"bin_sign 0 = 0" 
316 
"bin_sign 1 = 1" 

317 
"bin_sign (number_of (Int.Bit0 w)) = bin_sign (number_of w)" 

318 
"bin_sign (number_of (Int.Bit1 w)) = bin_sign (number_of w)" 

26557  319 
"bin_sign Int.Pls = Int.Pls" 
320 
"bin_sign Int.Min = Int.Min" 

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

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

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

45850  324 
unfolding bin_sign_def numeral_simps Bit_def bitval_def number_of_is_id 
325 
by (simp_all split: bit.split) 

26557  326 

24364  327 
lemma bin_sign_rest [simp]: 
37667  328 
"bin_sign (bin_rest w) = bin_sign w" 
26557  329 
by (cases w rule: bin_exhaust) auto 
24364  330 

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

332 
Z : "bintrunc 0 bin = Int.Pls" 
37667  333 
 Suc : "bintrunc (Suc n) bin = bintrunc n (bin_rest bin) BIT (bin_last bin)" 
24364  334 

37667  335 
primrec sbintrunc :: "nat => int => int" where 
24364  336 
Z : "sbintrunc 0 bin = 
37654  337 
(case bin_last bin of (1::bit) => Int.Min  (0::bit) => Int.Pls)" 
37667  338 
 Suc : "sbintrunc (Suc n) bin = sbintrunc n (bin_rest bin) BIT (bin_last bin)" 
339 

340 
lemma [code]: 

341 
"sbintrunc 0 bin = 

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

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

45845
4158f35a5c6f
remove some unwanted numeralrepresentationspecific simp rules
huffman
parents:
45844
diff
changeset

344 
apply simp_all 
4158f35a5c6f
remove some unwanted numeralrepresentationspecific simp rules
huffman
parents:
45844
diff
changeset

345 
apply (simp only: Pls_def Min_def) 
4158f35a5c6f
remove some unwanted numeralrepresentationspecific simp rules
huffman
parents:
45844
diff
changeset

346 
done 
24364  347 

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

349 
"!!w. bin_sign (bintrunc n w) = Int.Pls" 
24333  350 
by (induct n) auto 
351 

352 
lemma bintrunc_mod2p: 

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

45845
4158f35a5c6f
remove some unwanted numeralrepresentationspecific simp rules
huffman
parents:
45844
diff
changeset

354 
apply (induct n) 
4158f35a5c6f
remove some unwanted numeralrepresentationspecific simp rules
huffman
parents:
45844
diff
changeset

355 
apply (simp add: Pls_def) 
45529
0e1037d4e049
remove redundant lemmas bin_last_mod and bin_rest_div, use bin_last_def and bin_rest_def instead
huffman
parents:
44939
diff
changeset

356 
apply (simp add: bin_last_def bin_rest_def Bit_def zmod_zmult2_eq 
24333  357 
cong: number_of_False_cong) 
358 
done 

359 

360 
lemma sbintrunc_mod2p: 

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

362 
apply (induct n) 

363 
apply clarsimp 

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

365 
apply (simp add: bin_last_def) 
24333  366 
apply (simp add: number_of_eq) 
45845
4158f35a5c6f
remove some unwanted numeralrepresentationspecific simp rules
huffman
parents:
45844
diff
changeset

367 
apply (simp add: Pls_def) 
45529
0e1037d4e049
remove redundant lemmas bin_last_mod and bin_rest_div, use bin_last_def and bin_rest_def instead
huffman
parents:
44939
diff
changeset

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

370 
apply (clarsimp simp: mod_mult_mult1 [symmetric] 
24333  371 
zmod_zdiv_equality [THEN diff_eq_eq [THEN iffD2 [THEN sym]]]) 
372 
apply (rule trans [symmetric, OF _ emep1]) 

373 
apply auto 

374 
apply (auto simp: even_def) 

375 
done 

376 

24465  377 
subsection "Simplifications for (s)bintrunc" 
378 

45852  379 
lemma bintrunc_n_0 [simp]: "bintrunc n 0 = 0" 
380 
by (induct n) (auto simp add: Int.Pls_def) 

381 

45855  382 
lemma sbintrunc_n_0 [simp]: "sbintrunc n 0 = 0" 
383 
by (induct n) (auto simp add: Int.Pls_def) 

384 

45856  385 
lemma sbintrunc_n_minus1 [simp]: "sbintrunc n 1 = 1" 
386 
by (induct n) (auto, simp add: number_of_is_id) 

387 

45852  388 
lemma bintrunc_Suc_numeral: 
389 
"bintrunc (Suc n) 1 = 1" 

390 
"bintrunc (Suc n) 1 = bintrunc n 1 BIT 1" 

391 
"bintrunc (Suc n) (number_of (Int.Bit0 w)) = bintrunc n (number_of w) BIT 0" 

392 
"bintrunc (Suc n) (number_of (Int.Bit1 w)) = bintrunc n (number_of w) BIT 1" 

393 
by simp_all 

394 

45856  395 
lemma sbintrunc_0_numeral [simp]: 
396 
"sbintrunc 0 1 = 1" 

397 
"sbintrunc 0 (number_of (Int.Bit0 w)) = 0" 

398 
"sbintrunc 0 (number_of (Int.Bit1 w)) = 1" 

399 
by (simp_all, unfold Pls_def number_of_is_id, simp_all) 

400 

45855  401 
lemma sbintrunc_Suc_numeral: 
402 
"sbintrunc (Suc n) 1 = 1" 

403 
"sbintrunc (Suc n) (number_of (Int.Bit0 w)) = sbintrunc n (number_of w) BIT 0" 

404 
"sbintrunc (Suc n) (number_of (Int.Bit1 w)) = sbintrunc n (number_of w) BIT 1" 

405 
by simp_all 

406 

24465  407 
lemma bit_bool: 
37654  408 
"(b = (b' = (1::bit))) = (b' = (if b then (1::bit) else (0::bit)))" 
24465  409 
by (cases b') auto 
410 

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

24333  412 

413 
lemma bin_sign_lem: 

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

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

417 
done 

418 

419 
lemma nth_bintr: 

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

421 
apply (induct n) 

422 
apply (case_tac m, auto)[1] 

423 
apply (case_tac m, auto)[1] 

424 
done 

425 

426 
lemma nth_sbintr: 

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

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

429 
apply (induct n) 

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

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

432 
done 

433 

434 
lemma bin_nth_Bit: 

37654  435 
"bin_nth (w BIT b) n = (n = 0 & b = (1::bit)  (EX m. n = Suc m & bin_nth w m))" 
24333  436 
by (cases n) auto 
437 

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

438 
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

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

441 

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

442 
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

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

445 

24333  446 
lemma bintrunc_bintrunc_l: 
447 
"n <= m ==> (bintrunc m (bintrunc n w) = bintrunc n w)" 

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

449 

450 
lemma sbintrunc_sbintrunc_l: 

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

32439  452 
by (rule bin_eqI) (auto simp: nth_sbintr) 
24333  453 

454 
lemma bintrunc_bintrunc_ge: 

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

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

457 

458 
lemma bintrunc_bintrunc_min [simp]: 

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

460 
apply (rule bin_eqI) 

461 
apply (auto simp: nth_bintr) 

462 
done 

463 

464 
lemma sbintrunc_sbintrunc_min [simp]: 

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

466 
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

467 
apply (auto simp: nth_sbintr min_max.inf_absorb1 min_max.inf_absorb2) 
24333  468 
done 
469 

470 
lemmas bintrunc_Pls = 

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

473 
lemmas bintrunc_Min [simp] = 

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

476 
lemmas bintrunc_BIT [simp] = 

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

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

479 
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

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

482 

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

483 
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

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

486 

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

488 
bintrunc_Bit0 bintrunc_Bit1 
45852  489 
bintrunc_Suc_numeral 
24333  490 

491 
lemmas sbintrunc_Suc_Pls = 

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

494 
lemmas sbintrunc_Suc_Min = 

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

497 
lemmas sbintrunc_Suc_BIT [simp] = 

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

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

500 
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

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

503 

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

504 
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

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

507 

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

509 
sbintrunc_Suc_Bit0 sbintrunc_Suc_Bit1 
45855  510 
sbintrunc_Suc_numeral 
24333  511 

512 
lemmas sbintrunc_Pls = 

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

513 
sbintrunc.Z [where bin="Int.Pls", 
45604  514 
simplified bin_last_simps bin_rest_simps bit.simps] 
24333  515 

516 
lemmas sbintrunc_Min = 

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

517 
sbintrunc.Z [where bin="Int.Min", 
45604  518 
simplified bin_last_simps bin_rest_simps bit.simps] 
24333  519 

520 
lemmas sbintrunc_0_BIT_B0 [simp] = 

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

524 
lemmas sbintrunc_0_BIT_B1 [simp] = 

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

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

528 
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

529 
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

530 

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

531 
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

532 
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

533 

24333  534 
lemmas sbintrunc_0_simps = 
535 
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

536 
sbintrunc_0_Bit0 sbintrunc_0_Bit1 
24333  537 

538 
lemmas bintrunc_simps = bintrunc.Z bintrunc_Sucs 

539 
lemmas sbintrunc_simps = sbintrunc_0_simps sbintrunc_Sucs 

540 

541 
lemma bintrunc_minus: 

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

543 
by auto 

544 

545 
lemma sbintrunc_minus: 

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

547 
by auto 

548 

549 
lemmas bintrunc_minus_simps = 

45604  550 
bintrunc_Sucs [THEN [2] bintrunc_minus [symmetric, THEN trans]] 
24333  551 
lemmas sbintrunc_minus_simps = 
45604  552 
sbintrunc_Sucs [THEN [2] sbintrunc_minus [symmetric, THEN trans]] 
24333  553 

554 
lemma bintrunc_n_Pls [simp]: 

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

555 
"bintrunc n Int.Pls = Int.Pls" 
45847  556 
by (induct n) (auto simp: BIT_simps) 
24333  557 

558 
lemma sbintrunc_n_PM [simp]: 

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

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

560 
"sbintrunc n Int.Min = Int.Min" 
45847  561 
by (induct n) (auto simp: BIT_simps) 
24333  562 

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

565 
lemmas bintrunc_BIT_I = trans [OF bintrunc_BIT thobini1] 

566 
lemmas bintrunc_Min_I = trans [OF bintrunc_Min thobini1] 

567 

45604  568 
lemmas bmsts = bintrunc_minus_simps(13) [THEN thobini1 [THEN [2] trans]] 
24333  569 
lemmas bintrunc_Pls_minus_I = bmsts(1) 
570 
lemmas bintrunc_Min_minus_I = bmsts(2) 

571 
lemmas bintrunc_BIT_minus_I = bmsts(3) 

572 

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

573 
lemma bintrunc_0_Min: "bintrunc 0 Int.Min = Int.Pls" 
45852  574 
by (fact bintrunc.Z) (* FIXME: delete *) 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25349
diff
changeset

575 
lemma bintrunc_0_BIT: "bintrunc 0 (w BIT b) = Int.Pls" 
45852  576 
by (fact bintrunc.Z) (* FIXME: delete *) 
24333  577 

578 
lemma bintrunc_Suc_lem: 

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

580 
by auto 

581 

582 
lemmas bintrunc_Suc_Ialts = 

45604  583 
bintrunc_Min_I [THEN bintrunc_Suc_lem] 
584 
bintrunc_BIT_I [THEN bintrunc_Suc_lem] 

24333  585 

586 
lemmas sbintrunc_BIT_I = trans [OF sbintrunc_Suc_BIT thobini1] 

587 

588 
lemmas sbintrunc_Suc_Is = 

45604  589 
sbintrunc_Sucs(13) [THEN thobini1 [THEN [2] trans]] 
24333  590 

591 
lemmas sbintrunc_Suc_minus_Is = 

45604  592 
sbintrunc_minus_simps(13) [THEN thobini1 [THEN [2] trans]] 
24333  593 

594 
lemma sbintrunc_Suc_lem: 

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

596 
by auto 

597 

598 
lemmas sbintrunc_Suc_Ialts = 

45604  599 
sbintrunc_Suc_Is [THEN sbintrunc_Suc_lem] 
24333  600 

601 
lemma sbintrunc_bintrunc_lt: 

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

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

604 

605 
lemma bintrunc_sbintrunc_le: 

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

607 
apply (rule bin_eqI) 

608 
apply (auto simp: nth_sbintr nth_bintr) 

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

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

611 
done 

612 

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

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

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

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

617 

618 
lemma bintrunc_sbintrunc' [simp]: 

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

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

621 

622 
lemma sbintrunc_bintrunc' [simp]: 

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

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

625 

626 
lemma bin_sbin_eq_iff: 

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

628 
sbintrunc n x = sbintrunc n y" 

629 
apply (rule iffI) 

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

631 
apply simp 

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

633 
apply simp 

634 
done 

635 

636 
lemma bin_sbin_eq_iff': 

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

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

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

640 

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

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

643 

644 
lemmas bintrunc_bintrunc_l' = le_add1 [THEN bintrunc_bintrunc_l] 

645 
lemmas sbintrunc_sbintrunc_l' = le_add1 [THEN sbintrunc_sbintrunc_l] 

646 

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

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

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

650 

651 
lemmas nat_non0_gr = 

45604  652 
trans [OF iszero_def [THEN Not_eq_iff [THEN iffD2]] refl] 
24333  653 

654 
lemmas bintrunc_pred_simps [simp] = 

45604  655 
bintrunc_minus_simps [of "number_of bin", simplified nobm1] for bin 
24333  656 

657 
lemmas sbintrunc_pred_simps [simp] = 

45604  658 
sbintrunc_minus_simps [of "number_of bin", simplified nobm1] for bin 
24333  659 

660 
lemma no_bintr_alt: 

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

662 
by (simp add: number_of_eq bintrunc_mod2p) 

663 

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

665 
by (rule ext) (rule bintrunc_mod2p) 

666 

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

668 
apply (unfold no_bintr_alt1) 

669 
apply (auto simp add: image_iff) 

670 
apply (rule exI) 

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

672 
done 

673 

674 
lemma no_bintr: 

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

676 
by (simp add : bintrunc_mod2p number_of_eq) 

677 

678 
lemma no_sbintr_alt2: 

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

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

681 

682 
lemma no_sbintr: 

683 
"number_of (sbintrunc n w) = 

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

685 
by (simp add : no_sbintr_alt2 number_of_eq) 

686 

687 
lemma range_sbintrunc: 

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

689 
apply (unfold no_sbintr_alt2) 

690 
apply (auto simp add: image_iff eq_diff_eq) 

691 
apply (rule exI) 

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

693 
done 

694 

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

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

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

697 
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

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

699 
done 
24333  700 

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

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

702 
"(a::int) <  (2^k) \<Longrightarrow> a + 2^k + 2^(Suc k) <= (a + 2^k) mod 2^(Suc k)" 
35048  703 
by (rule sb_inc_lem) simp 
24333  704 

705 
lemma sbintrunc_inc: 

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

706 
"x <  (2^n) ==> x + 2^(Suc n) <= sbintrunc n x" 
24333  707 
unfolding no_sbintr_alt2 by (drule sb_inc_lem') simp 
708 

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

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

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

711 
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

712 
simplified zless2p, OF _ TrueI, simplified]) 
24333  713 

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

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

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

716 
by (rule iffD1 [OF diff_le_eq', THEN sb_dec_lem, simplified]) 
24333  717 

718 
lemma sbintrunc_dec: 

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

720 
unfolding no_sbintr_alt2 by (drule sb_dec_lem') simp 

721 

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

24333  724 

725 
lemmas brdmod1s' [symmetric] = 

30034  726 
mod_add_left_eq mod_add_right_eq 
24333  727 
zmod_zsub_left_eq zmod_zsub_right_eq 
728 
zmod_zmult1_eq zmod_zmult1_eq_rev 

729 

730 
lemmas brdmods' [symmetric] = 

731 
zpower_zmod' [symmetric] 

30034  732 
trans [OF mod_add_left_eq mod_add_right_eq] 
24333  733 
trans [OF zmod_zsub_left_eq zmod_zsub_right_eq] 
734 
trans [OF zmod_zmult1_eq zmod_zmult1_eq_rev] 

735 
zmod_uminus' [symmetric] 

30034  736 
mod_add_left_eq [where b = "1::int"] 
24333  737 
zmod_zsub_left_eq [where b = "1"] 
738 

739 
lemmas bintr_arith1s = 

45604  740 
brdmod1s' [where c="2^n::int", folded pred_def succ_def bintrunc_mod2p] for n 
24333  741 
lemmas bintr_ariths = 
45604  742 
brdmods' [where c="2^n::int", folded pred_def succ_def bintrunc_mod2p] for n 
24333  743 

45604  744 
lemmas m2pths = pos_mod_sign pos_mod_bound [OF zless2p] 
24364  745 

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

748 

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

750 
by (simp add : no_bintr m2pths) 

751 

752 
lemma bintr_Min: 

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

753 
"number_of (bintrunc n Int.Min) = (2 ^ n :: int)  1" 
24333  754 
by (simp add : no_bintr m1mod2k) 
755 

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

757 
by (simp add : no_sbintr m2pths) 

758 

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

760 
by (simp add : no_sbintr m2pths) 

761 

762 
lemma bintrunc_Suc: 

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

764 
by (case_tac bin rule: bin_exhaust) auto 

765 

766 
lemma sign_Pls_ge_0: 

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

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

768 
by (induct bin rule: numeral_induct) auto 
24333  769 

770 
lemma sign_Min_lt_0: 

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

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

772 
by (induct bin rule: numeral_induct) auto 
24333  773 

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

775 

776 
lemma bin_rest_trunc: 

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

778 
by (induct n) auto 

779 

780 
lemma bin_rest_power_trunc [rule_format] : 

30971  781 
"(bin_rest ^^ k) (bintrunc n bin) = 
782 
bintrunc (n  k) ((bin_rest ^^ k) bin)" 

24333  783 
by (induct k) (auto simp: bin_rest_trunc) 
784 

785 
lemma bin_rest_trunc_i: 

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

787 
by auto 

788 

789 
lemma bin_rest_strunc: 

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

791 
by (induct n) auto 

792 

793 
lemma bintrunc_rest [simp]: 

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

795 
apply (induct n, simp) 

796 
apply (case_tac bin rule: bin_exhaust) 

797 
apply (auto simp: bintrunc_bintrunc_l) 

798 
done 

799 

800 
lemma sbintrunc_rest [simp]: 

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

802 
apply (induct n, simp) 

803 
apply (case_tac bin rule: bin_exhaust) 

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

805 
done 

806 

807 
lemma bintrunc_rest': 

808 
"bintrunc n o bin_rest o bintrunc n = bin_rest o bintrunc n" 

809 
by (rule ext) auto 

810 

811 
lemma sbintrunc_rest' : 

812 
"sbintrunc n o bin_rest o sbintrunc n = bin_rest o sbintrunc n" 

813 
by (rule ext) auto 

814 

815 
lemma rco_lem: 

30971  816 
"f o g o f = g o f ==> f o (g o f) ^^ n = g ^^ n o f" 
24333  817 
apply (rule ext) 
818 
apply (induct_tac n) 

819 
apply (simp_all (no_asm)) 

820 
apply (drule fun_cong) 

821 
apply (unfold o_def) 

822 
apply (erule trans) 

823 
apply simp 

824 
done 

825 

30971  826 
lemma rco_alt: "(f o g) ^^ n o f = f o (g o f) ^^ n" 
24333  827 
apply (rule ext) 
828 
apply (induct n) 

829 
apply (simp_all add: o_def) 

830 
done 

831 

832 
lemmas rco_bintr = bintrunc_rest' 

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

834 
lemmas rco_sbintr = sbintrunc_rest' 

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

836 

24364  837 
subsection {* Splitting and concatenation *} 
838 

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

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

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

24364  843 

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

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

847 
by (simp_all add: Pls_def) 

848 

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

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

24364  852 

853 
subsection {* Miscellaneous lemmas *} 

854 

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

855 
lemma funpow_minus_simp: 
30971  856 
"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

857 
by (cases n) simp_all 
24364  858 

859 
lemmas funpow_pred_simp [simp] = 

45604  860 
funpow_minus_simp [of "number_of bin", simplified nobm1] for bin 
24364  861 

862 
lemmas replicate_minus_simp = 

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

865 
lemmas replicate_pred_simp [simp] = 

45604  866 
replicate_minus_simp [of "number_of bin", simplified nobm1] for bin 
24364  867 

45604  868 
lemmas power_Suc_no [simp] = power_Suc [of "number_of a"] for a 
24364  869 

870 
lemmas power_minus_simp = 

45604  871 
trans [OF gen_minus [where f = "power f"] power_Suc] for f 
24364  872 

873 
lemmas power_pred_simp = 

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

24364  876 

877 
lemma list_exhaust_size_gt0: 

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

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

880 
apply (cases y, simp) 

881 
apply (rule y) 

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

882 
apply fastforce 
24364  883 
done 
884 

885 
lemma list_exhaust_size_eq0: 

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

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

888 
apply (cases y) 

889 
apply (rule y, simp) 

890 
apply simp 

891 
done 

892 

893 
lemma size_Cons_lem_eq: 

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

895 
by auto 

896 

897 
lemma size_Cons_lem_eq_bin: 

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

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

901 

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

902 
lemmas ls_splits = prod.split prod.split_asm split_if_asm 
24333  903 

37654  904 
lemma not_B1_is_B0: "y \<noteq> (1::bit) \<Longrightarrow> y = (0::bit)" 
24333  905 
by (cases y) auto 
906 

907 
lemma B1_ass_B0: 

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

24333  910 
apply (rule classical) 
911 
apply (drule not_B1_is_B0) 

912 
apply (erule y) 

913 
done 

914 

915 
 "simplifications for specific word lengths" 

916 
lemmas n2s_ths [THEN eq_reflection] = add_2_eq_Suc add_2_eq_Suc' 

917 

918 
lemmas s2n_ths = n2s_ths [symmetric] 

919 

920 
end 