author  huffman 
Fri, 23 Dec 2011 11:50:12 +0100  
changeset 45953  1d6fcb19aa50 
parent 45952  ed9cc0634aaf 
child 45954  f67d3bb5f09c 
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 Bit_B0: 

37654  95 
"k BIT (0::bit) = k + k" 
26557  96 
by (unfold Bit_def) simp 
97 

98 
lemma Bit_B1: 

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

37654  102 
lemma Bit_B0_2t: "k BIT (0::bit) = 2 * k" 
26557  103 
by (rule trans, rule Bit_B0) simp 
104 

37654  105 
lemma Bit_B1_2t: "k BIT (1::bit) = 2 * k + 1" 
26557  106 
by (rule trans, rule Bit_B1) simp 
107 

108 
lemma B_mod_2': 

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

24465  112 
done 
24333  113 

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

24333  116 

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

119 

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

26557  123 
shows "P" 
124 
apply (rule y) 

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

126 
apply (simp add: ne) 

127 
done 

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

128 

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

131 
apply (cases "even bin") 

132 
apply (clarsimp simp: even_equiv_def) 

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

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

135 

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

138 
shows "Q" 

139 
apply (insert bin_ex_rl [of bin]) 

140 
apply (erule exE)+ 

141 
apply (rule Q) 

142 
apply force 

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

143 
done 
24333  144 

145 

24465  146 
subsection {* Destructors for binary integers *} 
24364  147 

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

150 

151 
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

152 
unfolding bin_rl_def by (auto simp: bin_rest_BIT bin_last_BIT) 
26557  153 

26514  154 
primrec bin_nth where 
37654  155 
Z: "bin_nth w 0 = (bin_last w = (1::bit))" 
26557  156 
 Suc: "bin_nth w (Suc n) = bin_nth (bin_rest w) n" 
24364  157 

26557  158 
lemma bin_rl_simps [simp]: 
37654  159 
"bin_rl Int.Pls = (Int.Pls, (0::bit))" 
160 
"bin_rl Int.Min = (Int.Min, (1::bit))" 

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

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

26557  163 
"bin_rl (r BIT b) = (r, b)" 
45847  164 
unfolding bin_rl_char by (simp_all add: BIT_simps) 
26557  165 

166 
lemma bin_abs_lem: 

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

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

169 
apply (clarsimp simp add: bin_rl_char) 

170 
apply (unfold Pls_def Min_def Bit_def) 

171 
apply (cases b) 

172 
apply (clarsimp, arith) 

173 
apply (clarsimp, arith) 

174 
done 

175 

176 
lemma bin_induct: 

177 
assumes PPls: "P Int.Pls" 

178 
and PMin: "P Int.Min" 

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

180 
shows "P bin" 

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

182 
in wf_measure [THEN wf_induct]) 

183 
apply (simp add: measure_def inv_image_def) 

184 
apply (case_tac x rule: bin_exhaust) 

185 
apply (frule bin_abs_lem) 

186 
apply (auto simp add : PPls PMin PBit) 

187 
done 

188 

189 
lemma numeral_induct: 

190 
assumes Pls: "P Int.Pls" 

191 
assumes Min: "P Int.Min" 

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

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

194 
shows "P x" 

195 
apply (induct x rule: bin_induct) 

196 
apply (rule Pls) 

197 
apply (rule Min) 

198 
apply (case_tac bit) 

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

45847  200 
apply (simp add: BIT_simps) 
201 
apply (simp add: Bit0 BIT_simps) 

26557  202 
apply (case_tac "bin = Int.Min") 
45847  203 
apply (simp add: BIT_simps) 
204 
apply (simp add: Bit1 BIT_simps) 

26557  205 
done 
206 

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

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

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

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

211 
"bin_rest (Int.Bit1 w) = w" 
26514  212 
"bin_rest (w BIT b) = w" 
37546  213 
using bin_rl_simps bin_rl_def by auto 
24465  214 

215 
lemma bin_last_simps [simp]: 

37654  216 
"bin_last Int.Pls = (0::bit)" 
217 
"bin_last Int.Min = (1::bit)" 

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

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

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

222 

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

224 
unfolding bin_rest_def [symmetric] by auto 
24333  225 

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

226 
lemma Bit0_div2 [simp]: "(Int.Bit0 w) div 2 = w" 
45847  227 
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

228 

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

229 
lemma Bit1_div2 [simp]: "(Int.Bit1 w) div 2 = w" 
45847  230 
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

231 

24333  232 
lemma bin_nth_lem [rule_format]: 
233 
"ALL y. bin_nth x = bin_nth y > x = y" 

234 
apply (induct x rule: bin_induct) 

235 
apply safe 

236 
apply (erule rev_mp) 

237 
apply (induct_tac y rule: bin_induct) 

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

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

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

45847  242 
apply (drule_tac x=0 in fun_cong, force simp: BIT_simps) 
24333  243 
apply (erule rev_mp) 
244 
apply (induct_tac y rule: bin_induct) 

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

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

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

45847  249 
apply (drule_tac x=0 in fun_cong, force simp: BIT_simps) 
24333  250 
apply (case_tac y rule: bin_exhaust) 
251 
apply clarify 

252 
apply (erule allE) 

253 
apply (erule impE) 

254 
prefer 2 

45848  255 
apply (erule conjI) 
24333  256 
apply (drule_tac x=0 in fun_cong, force) 
257 
apply (rule ext) 

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

259 
done 

260 

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

262 
by (auto elim: bin_nth_lem) 

263 

45604  264 
lemmas bin_eqI = ext [THEN bin_nth_eq_iff [THEN iffD1]] 
24333  265 

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

266 
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

267 
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

268 

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

271 

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

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

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

277 

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

278 
lemma bin_nth_Min [simp]: "bin_nth Int.Min n" 
24333  279 
by (induct n) auto 
280 

37654  281 
lemma bin_nth_0_BIT: "bin_nth (w BIT b) 0 = (b = (1::bit))" 
24333  282 
by auto 
283 

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

285 
by auto 

286 

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

288 
by (cases n) auto 

289 

26086
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_Bit0 [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.Bit0 w) n = bin_nth w (n  1)" 
45847  292 
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

293 

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

294 
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

295 
"0 < n ==> bin_nth (Int.Bit1 w) n = bin_nth w (n  1)" 
45847  296 
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

297 

24333  298 
lemmas bin_nth_0 = bin_nth.simps(1) 
299 
lemmas bin_nth_Suc = bin_nth.simps(2) 

300 

301 
lemmas bin_nth_simps = 

302 
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

303 
bin_nth_minus_Bit0 bin_nth_minus_Bit1 
24333  304 

26557  305 

306 
subsection {* Truncating binary integers *} 

307 

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

311 
lemma bin_sign_simps [simp]: 

45850  312 
"bin_sign 0 = 0" 
313 
"bin_sign 1 = 1" 

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

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

26557  316 
"bin_sign Int.Pls = Int.Pls" 
317 
"bin_sign Int.Min = Int.Min" 

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

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

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

45850  321 
unfolding bin_sign_def numeral_simps Bit_def bitval_def number_of_is_id 
322 
by (simp_all split: bit.split) 

26557  323 

24364  324 
lemma bin_sign_rest [simp]: 
37667  325 
"bin_sign (bin_rest w) = bin_sign w" 
26557  326 
by (cases w rule: bin_exhaust) auto 
24364  327 

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

329 
Z : "bintrunc 0 bin = Int.Pls" 
37667  330 
 Suc : "bintrunc (Suc n) bin = bintrunc n (bin_rest bin) BIT (bin_last bin)" 
24364  331 

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

337 
lemma [code]: 

338 
"sbintrunc 0 bin = 

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

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

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

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

343 
done 
24364  344 

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

346 
"!!w. bin_sign (bintrunc n w) = Int.Pls" 
24333  347 
by (induct n) auto 
348 

349 
lemma bintrunc_mod2p: 

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

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

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

352 
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

353 
apply (simp add: bin_last_def bin_rest_def Bit_def zmod_zmult2_eq 
24333  354 
cong: number_of_False_cong) 
355 
done 

356 

357 
lemma sbintrunc_mod2p: 

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

359 
apply (induct n) 

360 
apply clarsimp 

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

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

364 
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

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

367 
apply (clarsimp simp: mod_mult_mult1 [symmetric] 
24333  368 
zmod_zdiv_equality [THEN diff_eq_eq [THEN iffD2 [THEN sym]]]) 
369 
apply (rule trans [symmetric, OF _ emep1]) 

370 
apply auto 

371 
apply (auto simp: even_def) 

372 
done 

373 

24465  374 
subsection "Simplifications for (s)bintrunc" 
375 

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

378 

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

381 

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

384 

45852  385 
lemma bintrunc_Suc_numeral: 
386 
"bintrunc (Suc n) 1 = 1" 

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

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

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

390 
by simp_all 

391 

45856  392 
lemma sbintrunc_0_numeral [simp]: 
393 
"sbintrunc 0 1 = 1" 

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

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

396 
by (simp_all, unfold Pls_def number_of_is_id, simp_all) 

397 

45855  398 
lemma sbintrunc_Suc_numeral: 
399 
"sbintrunc (Suc n) 1 = 1" 

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

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

402 
by simp_all 

403 

24465  404 
lemma bit_bool: 
37654  405 
"(b = (b' = (1::bit))) = (b' = (if b then (1::bit) else (0::bit)))" 
24465  406 
by (cases b') auto 
407 

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

24333  409 

410 
lemma bin_sign_lem: 

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

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

414 
done 

415 

416 
lemma nth_bintr: 

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

418 
apply (induct n) 

419 
apply (case_tac m, auto)[1] 

420 
apply (case_tac m, auto)[1] 

421 
done 

422 

423 
lemma nth_sbintr: 

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

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

426 
apply (induct n) 

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

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

429 
done 

430 

431 
lemma bin_nth_Bit: 

37654  432 
"bin_nth (w BIT b) n = (n = 0 & b = (1::bit)  (EX m. n = Suc m & bin_nth w m))" 
24333  433 
by (cases n) auto 
434 

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

435 
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

436 
"bin_nth (Int.Bit0 w) n = (EX m. n = Suc m & bin_nth w m)" 
45847  437 
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

438 

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

439 
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

440 
"bin_nth (Int.Bit1 w) n = (n = 0  (EX m. n = Suc m & bin_nth w m))" 
45847  441 
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

442 

24333  443 
lemma bintrunc_bintrunc_l: 
444 
"n <= m ==> (bintrunc m (bintrunc n w) = bintrunc n w)" 

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

446 

447 
lemma sbintrunc_sbintrunc_l: 

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

32439  449 
by (rule bin_eqI) (auto simp: nth_sbintr) 
24333  450 

451 
lemma bintrunc_bintrunc_ge: 

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

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

454 

455 
lemma bintrunc_bintrunc_min [simp]: 

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

457 
apply (rule bin_eqI) 

458 
apply (auto simp: nth_bintr) 

459 
done 

460 

461 
lemma sbintrunc_sbintrunc_min [simp]: 

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

463 
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

464 
apply (auto simp: nth_sbintr min_max.inf_absorb1 min_max.inf_absorb2) 
24333  465 
done 
466 

467 
lemmas bintrunc_Pls = 

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

470 
lemmas bintrunc_Min [simp] = 

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

473 
lemmas bintrunc_BIT [simp] = 

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

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

476 
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

477 
"bintrunc (Suc n) (Int.Bit0 w) = Int.Bit0 (bintrunc n w)" 
45847  478 
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

479 

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

480 
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

481 
"bintrunc (Suc n) (Int.Bit1 w) = Int.Bit1 (bintrunc n w)" 
45847  482 
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

483 

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

485 
bintrunc_Bit0 bintrunc_Bit1 
45852  486 
bintrunc_Suc_numeral 
24333  487 

488 
lemmas sbintrunc_Suc_Pls = 

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

491 
lemmas sbintrunc_Suc_Min = 

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

494 
lemmas sbintrunc_Suc_BIT [simp] = 

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

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

497 
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

498 
"sbintrunc (Suc n) (Int.Bit0 w) = Int.Bit0 (sbintrunc n w)" 
45847  499 
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

500 

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

501 
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

502 
"sbintrunc (Suc n) (Int.Bit1 w) = Int.Bit1 (sbintrunc n w)" 
45847  503 
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

504 

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

506 
sbintrunc_Suc_Bit0 sbintrunc_Suc_Bit1 
45855  507 
sbintrunc_Suc_numeral 
24333  508 

509 
lemmas sbintrunc_Pls = 

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

510 
sbintrunc.Z [where bin="Int.Pls", 
45604  511 
simplified bin_last_simps bin_rest_simps bit.simps] 
24333  512 

513 
lemmas sbintrunc_Min = 

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

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

517 
lemmas sbintrunc_0_BIT_B0 [simp] = 

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

521 
lemmas sbintrunc_0_BIT_B1 [simp] = 

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

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

525 
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

526 
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

527 

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_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

529 
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

530 

24333  531 
lemmas sbintrunc_0_simps = 
532 
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

533 
sbintrunc_0_Bit0 sbintrunc_0_Bit1 
24333  534 

535 
lemmas bintrunc_simps = bintrunc.Z bintrunc_Sucs 

536 
lemmas sbintrunc_simps = sbintrunc_0_simps sbintrunc_Sucs 

537 

538 
lemma bintrunc_minus: 

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

540 
by auto 

541 

542 
lemma sbintrunc_minus: 

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

544 
by auto 

545 

546 
lemmas bintrunc_minus_simps = 

45604  547 
bintrunc_Sucs [THEN [2] bintrunc_minus [symmetric, THEN trans]] 
24333  548 
lemmas sbintrunc_minus_simps = 
45604  549 
sbintrunc_Sucs [THEN [2] sbintrunc_minus [symmetric, THEN trans]] 
24333  550 

551 
lemma bintrunc_n_Pls [simp]: 

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

552 
"bintrunc n Int.Pls = Int.Pls" 
45847  553 
by (induct n) (auto simp: BIT_simps) 
24333  554 

555 
lemma sbintrunc_n_PM [simp]: 

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

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

557 
"sbintrunc n Int.Min = Int.Min" 
45847  558 
by (induct n) (auto simp: BIT_simps) 
24333  559 

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

562 
lemmas bintrunc_BIT_I = trans [OF bintrunc_BIT thobini1] 

563 
lemmas bintrunc_Min_I = trans [OF bintrunc_Min thobini1] 

564 

45604  565 
lemmas bmsts = bintrunc_minus_simps(13) [THEN thobini1 [THEN [2] trans]] 
24333  566 
lemmas bintrunc_Pls_minus_I = bmsts(1) 
567 
lemmas bintrunc_Min_minus_I = bmsts(2) 

568 
lemmas bintrunc_BIT_minus_I = bmsts(3) 

569 

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

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

572 
lemma bintrunc_0_BIT: "bintrunc 0 (w BIT b) = Int.Pls" 
45852  573 
by (fact bintrunc.Z) (* FIXME: delete *) 
24333  574 

575 
lemma bintrunc_Suc_lem: 

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

577 
by auto 

578 

579 
lemmas bintrunc_Suc_Ialts = 

45604  580 
bintrunc_Min_I [THEN bintrunc_Suc_lem] 
581 
bintrunc_BIT_I [THEN bintrunc_Suc_lem] 

24333  582 

583 
lemmas sbintrunc_BIT_I = trans [OF sbintrunc_Suc_BIT thobini1] 

584 

585 
lemmas sbintrunc_Suc_Is = 

45604  586 
sbintrunc_Sucs(13) [THEN thobini1 [THEN [2] trans]] 
24333  587 

588 
lemmas sbintrunc_Suc_minus_Is = 

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

591 
lemma sbintrunc_Suc_lem: 

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

593 
by auto 

594 

595 
lemmas sbintrunc_Suc_Ialts = 

45604  596 
sbintrunc_Suc_Is [THEN sbintrunc_Suc_lem] 
24333  597 

598 
lemma sbintrunc_bintrunc_lt: 

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

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

601 

602 
lemma bintrunc_sbintrunc_le: 

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

604 
apply (rule bin_eqI) 

605 
apply (auto simp: nth_sbintr nth_bintr) 

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

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

608 
done 

609 

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

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

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

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

614 

615 
lemma bintrunc_sbintrunc' [simp]: 

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

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

618 

619 
lemma sbintrunc_bintrunc' [simp]: 

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

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

622 

623 
lemma bin_sbin_eq_iff: 

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

625 
sbintrunc n x = sbintrunc n y" 

626 
apply (rule iffI) 

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

628 
apply simp 

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

630 
apply simp 

631 
done 

632 

633 
lemma bin_sbin_eq_iff': 

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

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

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

637 

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

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

640 

641 
lemmas bintrunc_bintrunc_l' = le_add1 [THEN bintrunc_bintrunc_l] 

642 
lemmas sbintrunc_sbintrunc_l' = le_add1 [THEN sbintrunc_sbintrunc_l] 

643 

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

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

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

647 

648 
lemmas nat_non0_gr = 

45604  649 
trans [OF iszero_def [THEN Not_eq_iff [THEN iffD2]] refl] 
24333  650 

651 
lemmas bintrunc_pred_simps [simp] = 

45604  652 
bintrunc_minus_simps [of "number_of bin", simplified nobm1] for bin 
24333  653 

654 
lemmas sbintrunc_pred_simps [simp] = 

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

657 
lemma no_bintr_alt: 

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

659 
by (simp add: number_of_eq bintrunc_mod2p) 

660 

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

662 
by (rule ext) (rule bintrunc_mod2p) 

663 

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

665 
apply (unfold no_bintr_alt1) 

666 
apply (auto simp add: image_iff) 

667 
apply (rule exI) 

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

669 
done 

670 

671 
lemma no_bintr: 

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

673 
by (simp add : bintrunc_mod2p number_of_eq) 

674 

675 
lemma no_sbintr_alt2: 

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

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

678 

679 
lemma no_sbintr: 

680 
"number_of (sbintrunc n w) = 

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

682 
by (simp add : no_sbintr_alt2 number_of_eq) 

683 

684 
lemma range_sbintrunc: 

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

686 
apply (unfold no_sbintr_alt2) 

687 
apply (auto simp add: image_iff eq_diff_eq) 

688 
apply (rule exI) 

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

690 
done 

691 

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

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

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

694 
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

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

696 
done 
24333  697 

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

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

699 
"(a::int) <  (2^k) \<Longrightarrow> a + 2^k + 2^(Suc k) <= (a + 2^k) mod 2^(Suc k)" 
35048  700 
by (rule sb_inc_lem) simp 
24333  701 

702 
lemma sbintrunc_inc: 

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

703 
"x <  (2^n) ==> x + 2^(Suc n) <= sbintrunc n x" 
24333  704 
unfolding no_sbintr_alt2 by (drule sb_inc_lem') simp 
705 

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

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

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

708 
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

709 
simplified zless2p, OF _ TrueI, simplified]) 
24333  710 

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

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

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

713 
by (rule iffD1 [OF diff_le_eq', THEN sb_dec_lem, simplified]) 
24333  714 

715 
lemma sbintrunc_dec: 

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

717 
unfolding no_sbintr_alt2 by (drule sb_dec_lem') simp 

718 

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

24333  721 

722 
lemmas brdmod1s' [symmetric] = 

30034  723 
mod_add_left_eq mod_add_right_eq 
24333  724 
zmod_zsub_left_eq zmod_zsub_right_eq 
725 
zmod_zmult1_eq zmod_zmult1_eq_rev 

726 

727 
lemmas brdmods' [symmetric] = 

728 
zpower_zmod' [symmetric] 

30034  729 
trans [OF mod_add_left_eq mod_add_right_eq] 
24333  730 
trans [OF zmod_zsub_left_eq zmod_zsub_right_eq] 
731 
trans [OF zmod_zmult1_eq zmod_zmult1_eq_rev] 

732 
zmod_uminus' [symmetric] 

30034  733 
mod_add_left_eq [where b = "1::int"] 
24333  734 
zmod_zsub_left_eq [where b = "1"] 
735 

736 
lemmas bintr_arith1s = 

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

45604  741 
lemmas m2pths = pos_mod_sign pos_mod_bound [OF zless2p] 
24364  742 

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

745 

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

747 
by (simp add : no_bintr m2pths) 

748 

749 
lemma bintr_Min: 

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

750 
"number_of (bintrunc n Int.Min) = (2 ^ n :: int)  1" 
24333  751 
by (simp add : no_bintr m1mod2k) 
752 

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

754 
by (simp add : no_sbintr m2pths) 

755 

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

757 
by (simp add : no_sbintr m2pths) 

758 

759 
lemma bintrunc_Suc: 

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

761 
by (case_tac bin rule: bin_exhaust) auto 

762 

763 
lemma sign_Pls_ge_0: 

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

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

765 
by (induct bin rule: numeral_induct) auto 
24333  766 

767 
lemma sign_Min_lt_0: 

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

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

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

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

772 

773 
lemma bin_rest_trunc: 

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

775 
by (induct n) auto 

776 

777 
lemma bin_rest_power_trunc [rule_format] : 

30971  778 
"(bin_rest ^^ k) (bintrunc n bin) = 
779 
bintrunc (n  k) ((bin_rest ^^ k) bin)" 

24333  780 
by (induct k) (auto simp: bin_rest_trunc) 
781 

782 
lemma bin_rest_trunc_i: 

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

784 
by auto 

785 

786 
lemma bin_rest_strunc: 

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

788 
by (induct n) auto 

789 

790 
lemma bintrunc_rest [simp]: 

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

792 
apply (induct n, simp) 

793 
apply (case_tac bin rule: bin_exhaust) 

794 
apply (auto simp: bintrunc_bintrunc_l) 

795 
done 

796 

797 
lemma sbintrunc_rest [simp]: 

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

799 
apply (induct n, simp) 

800 
apply (case_tac bin rule: bin_exhaust) 

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

802 
done 

803 

804 
lemma bintrunc_rest': 

805 
"bintrunc n o bin_rest o bintrunc n = bin_rest o bintrunc n" 

806 
by (rule ext) auto 

807 

808 
lemma sbintrunc_rest' : 

809 
"sbintrunc n o bin_rest o sbintrunc n = bin_rest o sbintrunc n" 

810 
by (rule ext) auto 

811 

812 
lemma rco_lem: 

30971  813 
"f o g o f = g o f ==> f o (g o f) ^^ n = g ^^ n o f" 
24333  814 
apply (rule ext) 
815 
apply (induct_tac n) 

816 
apply (simp_all (no_asm)) 

817 
apply (drule fun_cong) 

818 
apply (unfold o_def) 

819 
apply (erule trans) 

820 
apply simp 

821 
done 

822 

30971  823 
lemma rco_alt: "(f o g) ^^ n o f = f o (g o f) ^^ n" 
24333  824 
apply (rule ext) 
825 
apply (induct n) 

826 
apply (simp_all add: o_def) 

827 
done 

828 

829 
lemmas rco_bintr = bintrunc_rest' 

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

831 
lemmas rco_sbintr = sbintrunc_rest' 

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

833 

24364  834 
subsection {* Splitting and concatenation *} 
835 

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

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

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

24364  840 

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

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

844 
by (simp_all add: Pls_def) 

845 

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

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

24364  849 

850 
subsection {* Miscellaneous lemmas *} 

851 

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

852 
lemma funpow_minus_simp: 
30971  853 
"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

854 
by (cases n) simp_all 
24364  855 

856 
lemmas funpow_pred_simp [simp] = 

45604  857 
funpow_minus_simp [of "number_of bin", simplified nobm1] for bin 
24364  858 

859 
lemmas replicate_minus_simp = 

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

862 
lemmas replicate_pred_simp [simp] = 

45604  863 
replicate_minus_simp [of "number_of bin", simplified nobm1] for bin 
24364  864 

45604  865 
lemmas power_Suc_no [simp] = power_Suc [of "number_of a"] for a 
24364  866 

867 
lemmas power_minus_simp = 

45604  868 
trans [OF gen_minus [where f = "power f"] power_Suc] for f 
24364  869 

870 
lemmas power_pred_simp = 

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

24364  873 

874 
lemma list_exhaust_size_gt0: 

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

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

877 
apply (cases y, simp) 

878 
apply (rule y) 

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

879 
apply fastforce 
24364  880 
done 
881 

882 
lemma list_exhaust_size_eq0: 

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

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

885 
apply (cases y) 

886 
apply (rule y, simp) 

887 
apply simp 

888 
done 

889 

890 
lemma size_Cons_lem_eq: 

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

892 
by auto 

893 

894 
lemma size_Cons_lem_eq_bin: 

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

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

898 

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

899 
lemmas ls_splits = prod.split prod.split_asm split_if_asm 
24333  900 

37654  901 
lemma not_B1_is_B0: "y \<noteq> (1::bit) \<Longrightarrow> y = (0::bit)" 
24333  902 
by (cases y) auto 
903 

904 
lemma B1_ass_B0: 

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

24333  907 
apply (rule classical) 
908 
apply (drule not_B1_is_B0) 

909 
apply (erule y) 

910 
done 

911 

912 
 "simplifications for specific word lengths" 

913 
lemmas n2s_ths [THEN eq_reflection] = add_2_eq_Suc add_2_eq_Suc' 

914 

915 
lemmas s2n_ths = n2s_ths [symmetric] 

916 

917 
end 