author  huffman 
Tue, 13 Dec 2011 15:34:59 +0100  
changeset 45855  b49cffac6c97 
parent 45853  cbb6f2243b52 
child 45856  caa99836aed8 
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 

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 

45852  382 
lemma bintrunc_Suc_numeral: 
383 
"bintrunc (Suc n) 1 = 1" 

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

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

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

387 
by simp_all 

388 

45855  389 
lemma sbintrunc_Suc_numeral: 
390 
"sbintrunc (Suc n) 1 = 1" 

391 
"sbintrunc (Suc n) 1 = sbintrunc n 1 BIT 1" 

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

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

394 
by simp_all 

395 

24465  396 
lemma bit_bool: 
37654  397 
"(b = (b' = (1::bit))) = (b' = (if b then (1::bit) else (0::bit)))" 
24465  398 
by (cases b') auto 
399 

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

24333  401 

402 
lemma bin_sign_lem: 

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

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

406 
done 

407 

408 
lemma nth_bintr: 

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

410 
apply (induct n) 

411 
apply (case_tac m, auto)[1] 

412 
apply (case_tac m, auto)[1] 

413 
done 

414 

415 
lemma nth_sbintr: 

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

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

418 
apply (induct n) 

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

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

421 
done 

422 

423 
lemma bin_nth_Bit: 

37654  424 
"bin_nth (w BIT b) n = (n = 0 & b = (1::bit)  (EX m. n = Suc m & bin_nth w m))" 
24333  425 
by (cases n) auto 
426 

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

427 
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

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

430 

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

431 
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

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

434 

24333  435 
lemma bintrunc_bintrunc_l: 
436 
"n <= m ==> (bintrunc m (bintrunc n w) = bintrunc n w)" 

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

438 

439 
lemma sbintrunc_sbintrunc_l: 

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

32439  441 
by (rule bin_eqI) (auto simp: nth_sbintr) 
24333  442 

443 
lemma bintrunc_bintrunc_ge: 

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

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

446 

447 
lemma bintrunc_bintrunc_min [simp]: 

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

449 
apply (rule bin_eqI) 

450 
apply (auto simp: nth_bintr) 

451 
done 

452 

453 
lemma sbintrunc_sbintrunc_min [simp]: 

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

455 
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

456 
apply (auto simp: nth_sbintr min_max.inf_absorb1 min_max.inf_absorb2) 
24333  457 
done 
458 

459 
lemmas bintrunc_Pls = 

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

462 
lemmas bintrunc_Min [simp] = 

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

465 
lemmas bintrunc_BIT [simp] = 

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

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

468 
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

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

471 

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

472 
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

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

475 

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

477 
bintrunc_Bit0 bintrunc_Bit1 
45852  478 
bintrunc_Suc_numeral 
24333  479 

480 
lemmas sbintrunc_Suc_Pls = 

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

483 
lemmas sbintrunc_Suc_Min = 

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

486 
lemmas sbintrunc_Suc_BIT [simp] = 

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

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

489 
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

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

492 

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

493 
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

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

496 

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

498 
sbintrunc_Suc_Bit0 sbintrunc_Suc_Bit1 
45855  499 
sbintrunc_Suc_numeral 
24333  500 

501 
lemmas sbintrunc_Pls = 

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

502 
sbintrunc.Z [where bin="Int.Pls", 
45604  503 
simplified bin_last_simps bin_rest_simps bit.simps] 
24333  504 

505 
lemmas sbintrunc_Min = 

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

506 
sbintrunc.Z [where bin="Int.Min", 
45604  507 
simplified bin_last_simps bin_rest_simps bit.simps] 
24333  508 

509 
lemmas sbintrunc_0_BIT_B0 [simp] = 

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

513 
lemmas sbintrunc_0_BIT_B1 [simp] = 

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

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

517 
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

518 
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

519 

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

520 
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

521 
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

522 

24333  523 
lemmas sbintrunc_0_simps = 
524 
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

525 
sbintrunc_0_Bit0 sbintrunc_0_Bit1 
24333  526 

527 
lemmas bintrunc_simps = bintrunc.Z bintrunc_Sucs 

528 
lemmas sbintrunc_simps = sbintrunc_0_simps sbintrunc_Sucs 

529 

530 
lemma bintrunc_minus: 

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

532 
by auto 

533 

534 
lemma sbintrunc_minus: 

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

536 
by auto 

537 

538 
lemmas bintrunc_minus_simps = 

45604  539 
bintrunc_Sucs [THEN [2] bintrunc_minus [symmetric, THEN trans]] 
24333  540 
lemmas sbintrunc_minus_simps = 
45604  541 
sbintrunc_Sucs [THEN [2] sbintrunc_minus [symmetric, THEN trans]] 
24333  542 

543 
lemma bintrunc_n_Pls [simp]: 

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

544 
"bintrunc n Int.Pls = Int.Pls" 
45847  545 
by (induct n) (auto simp: BIT_simps) 
24333  546 

547 
lemma sbintrunc_n_PM [simp]: 

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

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

549 
"sbintrunc n Int.Min = Int.Min" 
45847  550 
by (induct n) (auto simp: BIT_simps) 
24333  551 

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

554 
lemmas bintrunc_BIT_I = trans [OF bintrunc_BIT thobini1] 

555 
lemmas bintrunc_Min_I = trans [OF bintrunc_Min thobini1] 

556 

45604  557 
lemmas bmsts = bintrunc_minus_simps(13) [THEN thobini1 [THEN [2] trans]] 
24333  558 
lemmas bintrunc_Pls_minus_I = bmsts(1) 
559 
lemmas bintrunc_Min_minus_I = bmsts(2) 

560 
lemmas bintrunc_BIT_minus_I = bmsts(3) 

561 

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

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

564 
lemma bintrunc_0_BIT: "bintrunc 0 (w BIT b) = Int.Pls" 
45852  565 
by (fact bintrunc.Z) (* FIXME: delete *) 
24333  566 

567 
lemma bintrunc_Suc_lem: 

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

569 
by auto 

570 

571 
lemmas bintrunc_Suc_Ialts = 

45604  572 
bintrunc_Min_I [THEN bintrunc_Suc_lem] 
573 
bintrunc_BIT_I [THEN bintrunc_Suc_lem] 

24333  574 

575 
lemmas sbintrunc_BIT_I = trans [OF sbintrunc_Suc_BIT thobini1] 

576 

577 
lemmas sbintrunc_Suc_Is = 

45604  578 
sbintrunc_Sucs(13) [THEN thobini1 [THEN [2] trans]] 
24333  579 

580 
lemmas sbintrunc_Suc_minus_Is = 

45604  581 
sbintrunc_minus_simps(13) [THEN thobini1 [THEN [2] trans]] 
24333  582 

583 
lemma sbintrunc_Suc_lem: 

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

585 
by auto 

586 

587 
lemmas sbintrunc_Suc_Ialts = 

45604  588 
sbintrunc_Suc_Is [THEN sbintrunc_Suc_lem] 
24333  589 

590 
lemma sbintrunc_bintrunc_lt: 

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

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

593 

594 
lemma bintrunc_sbintrunc_le: 

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

596 
apply (rule bin_eqI) 

597 
apply (auto simp: nth_sbintr nth_bintr) 

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

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

600 
done 

601 

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

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

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

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

606 

607 
lemma bintrunc_sbintrunc' [simp]: 

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

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

610 

611 
lemma sbintrunc_bintrunc' [simp]: 

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

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

614 

615 
lemma bin_sbin_eq_iff: 

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

617 
sbintrunc n x = sbintrunc n y" 

618 
apply (rule iffI) 

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

620 
apply simp 

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

622 
apply simp 

623 
done 

624 

625 
lemma bin_sbin_eq_iff': 

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

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

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

629 

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

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

632 

633 
lemmas bintrunc_bintrunc_l' = le_add1 [THEN bintrunc_bintrunc_l] 

634 
lemmas sbintrunc_sbintrunc_l' = le_add1 [THEN sbintrunc_sbintrunc_l] 

635 

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

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

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

639 

640 
lemmas nat_non0_gr = 

45604  641 
trans [OF iszero_def [THEN Not_eq_iff [THEN iffD2]] refl] 
24333  642 

643 
lemmas bintrunc_pred_simps [simp] = 

45604  644 
bintrunc_minus_simps [of "number_of bin", simplified nobm1] for bin 
24333  645 

646 
lemmas sbintrunc_pred_simps [simp] = 

45604  647 
sbintrunc_minus_simps [of "number_of bin", simplified nobm1] for bin 
24333  648 

649 
lemma no_bintr_alt: 

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

651 
by (simp add: number_of_eq bintrunc_mod2p) 

652 

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

654 
by (rule ext) (rule bintrunc_mod2p) 

655 

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

657 
apply (unfold no_bintr_alt1) 

658 
apply (auto simp add: image_iff) 

659 
apply (rule exI) 

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

661 
done 

662 

663 
lemma no_bintr: 

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

665 
by (simp add : bintrunc_mod2p number_of_eq) 

666 

667 
lemma no_sbintr_alt2: 

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

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

670 

671 
lemma no_sbintr: 

672 
"number_of (sbintrunc n w) = 

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

674 
by (simp add : no_sbintr_alt2 number_of_eq) 

675 

676 
lemma range_sbintrunc: 

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

678 
apply (unfold no_sbintr_alt2) 

679 
apply (auto simp add: image_iff eq_diff_eq) 

680 
apply (rule exI) 

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

682 
done 

683 

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

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

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

686 
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

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

688 
done 
24333  689 

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

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

691 
"(a::int) <  (2^k) \<Longrightarrow> a + 2^k + 2^(Suc k) <= (a + 2^k) mod 2^(Suc k)" 
35048  692 
by (rule sb_inc_lem) simp 
24333  693 

694 
lemma sbintrunc_inc: 

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

695 
"x <  (2^n) ==> x + 2^(Suc n) <= sbintrunc n x" 
24333  696 
unfolding no_sbintr_alt2 by (drule sb_inc_lem') simp 
697 

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

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

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

700 
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

701 
simplified zless2p, OF _ TrueI, simplified]) 
24333  702 

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

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

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

705 
by (rule iffD1 [OF diff_le_eq', THEN sb_dec_lem, simplified]) 
24333  706 

707 
lemma sbintrunc_dec: 

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

709 
unfolding no_sbintr_alt2 by (drule sb_dec_lem') simp 

710 

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

24333  713 

714 
lemmas brdmod1s' [symmetric] = 

30034  715 
mod_add_left_eq mod_add_right_eq 
24333  716 
zmod_zsub_left_eq zmod_zsub_right_eq 
717 
zmod_zmult1_eq zmod_zmult1_eq_rev 

718 

719 
lemmas brdmods' [symmetric] = 

720 
zpower_zmod' [symmetric] 

30034  721 
trans [OF mod_add_left_eq mod_add_right_eq] 
24333  722 
trans [OF zmod_zsub_left_eq zmod_zsub_right_eq] 
723 
trans [OF zmod_zmult1_eq zmod_zmult1_eq_rev] 

724 
zmod_uminus' [symmetric] 

30034  725 
mod_add_left_eq [where b = "1::int"] 
24333  726 
zmod_zsub_left_eq [where b = "1"] 
727 

728 
lemmas bintr_arith1s = 

45604  729 
brdmod1s' [where c="2^n::int", folded pred_def succ_def bintrunc_mod2p] for n 
24333  730 
lemmas bintr_ariths = 
45604  731 
brdmods' [where c="2^n::int", folded pred_def succ_def bintrunc_mod2p] for n 
24333  732 

45604  733 
lemmas m2pths = pos_mod_sign pos_mod_bound [OF zless2p] 
24364  734 

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

737 

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

739 
by (simp add : no_bintr m2pths) 

740 

741 
lemma bintr_Min: 

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

742 
"number_of (bintrunc n Int.Min) = (2 ^ n :: int)  1" 
24333  743 
by (simp add : no_bintr m1mod2k) 
744 

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

746 
by (simp add : no_sbintr m2pths) 

747 

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

749 
by (simp add : no_sbintr m2pths) 

750 

751 
lemma bintrunc_Suc: 

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

753 
by (case_tac bin rule: bin_exhaust) auto 

754 

755 
lemma sign_Pls_ge_0: 

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

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

757 
by (induct bin rule: numeral_induct) auto 
24333  758 

759 
lemma sign_Min_lt_0: 

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

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

761 
by (induct bin rule: numeral_induct) auto 
24333  762 

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

764 

765 
lemma bin_rest_trunc: 

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

767 
by (induct n) auto 

768 

769 
lemma bin_rest_power_trunc [rule_format] : 

30971  770 
"(bin_rest ^^ k) (bintrunc n bin) = 
771 
bintrunc (n  k) ((bin_rest ^^ k) bin)" 

24333  772 
by (induct k) (auto simp: bin_rest_trunc) 
773 

774 
lemma bin_rest_trunc_i: 

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

776 
by auto 

777 

778 
lemma bin_rest_strunc: 

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

780 
by (induct n) auto 

781 

782 
lemma bintrunc_rest [simp]: 

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

784 
apply (induct n, simp) 

785 
apply (case_tac bin rule: bin_exhaust) 

786 
apply (auto simp: bintrunc_bintrunc_l) 

787 
done 

788 

789 
lemma sbintrunc_rest [simp]: 

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

791 
apply (induct n, simp) 

792 
apply (case_tac bin rule: bin_exhaust) 

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

794 
done 

795 

796 
lemma bintrunc_rest': 

797 
"bintrunc n o bin_rest o bintrunc n = bin_rest o bintrunc n" 

798 
by (rule ext) auto 

799 

800 
lemma sbintrunc_rest' : 

801 
"sbintrunc n o bin_rest o sbintrunc n = bin_rest o sbintrunc n" 

802 
by (rule ext) auto 

803 

804 
lemma rco_lem: 

30971  805 
"f o g o f = g o f ==> f o (g o f) ^^ n = g ^^ n o f" 
24333  806 
apply (rule ext) 
807 
apply (induct_tac n) 

808 
apply (simp_all (no_asm)) 

809 
apply (drule fun_cong) 

810 
apply (unfold o_def) 

811 
apply (erule trans) 

812 
apply simp 

813 
done 

814 

30971  815 
lemma rco_alt: "(f o g) ^^ n o f = f o (g o f) ^^ n" 
24333  816 
apply (rule ext) 
817 
apply (induct n) 

818 
apply (simp_all add: o_def) 

819 
done 

820 

821 
lemmas rco_bintr = bintrunc_rest' 

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

823 
lemmas rco_sbintr = sbintrunc_rest' 

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

825 

24364  826 
subsection {* Splitting and concatenation *} 
827 

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

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

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

24364  832 

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

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

836 
by (simp_all add: Pls_def) 

837 

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

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

24364  841 

842 
subsection {* Miscellaneous lemmas *} 

843 

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

844 
lemma funpow_minus_simp: 
30971  845 
"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

846 
by (cases n) simp_all 
24364  847 

848 
lemmas funpow_pred_simp [simp] = 

45604  849 
funpow_minus_simp [of "number_of bin", simplified nobm1] for bin 
24364  850 

851 
lemmas replicate_minus_simp = 

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

854 
lemmas replicate_pred_simp [simp] = 

45604  855 
replicate_minus_simp [of "number_of bin", simplified nobm1] for bin 
24364  856 

45604  857 
lemmas power_Suc_no [simp] = power_Suc [of "number_of a"] for a 
24364  858 

859 
lemmas power_minus_simp = 

45604  860 
trans [OF gen_minus [where f = "power f"] power_Suc] for f 
24364  861 

862 
lemmas power_pred_simp = 

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

24364  865 

866 
lemma list_exhaust_size_gt0: 

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

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

869 
apply (cases y, simp) 

870 
apply (rule y) 

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

871 
apply fastforce 
24364  872 
done 
873 

874 
lemma list_exhaust_size_eq0: 

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

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

877 
apply (cases y) 

878 
apply (rule y, simp) 

879 
apply simp 

880 
done 

881 

882 
lemma size_Cons_lem_eq: 

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

884 
by auto 

885 

886 
lemma size_Cons_lem_eq_bin: 

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

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

890 

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

891 
lemmas ls_splits = prod.split prod.split_asm split_if_asm 
24333  892 

37654  893 
lemma not_B1_is_B0: "y \<noteq> (1::bit) \<Longrightarrow> y = (0::bit)" 
24333  894 
by (cases y) auto 
895 

896 
lemma B1_ass_B0: 

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

24333  899 
apply (rule classical) 
900 
apply (drule not_B1_is_B0) 

901 
apply (erule y) 

902 
done 

903 

904 
 "simplifications for specific word lengths" 

905 
lemmas n2s_ths [THEN eq_reflection] = add_2_eq_Suc add_2_eq_Suc' 

906 

907 
lemmas s2n_ths = n2s_ths [symmetric] 

908 

909 
end 