author  huffman 
Fri, 24 Feb 2012 16:59:20 +0100  
changeset 46655  be76913ec1a4 
parent 46653  a557db8f2fbf 
child 47108  2a1953f0d20d 
permissions  rwrr 
24333  1 
(* 
2 
Author: Jeremy Dawson, NICTA 

3 

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

4 
Theorems to do with integers, expressed using Pls, Min, BIT, 
24333  5 
theorems linking them to lists of booleans, and repeated splitting 
6 
and concatenation. 

7 
*) 

8 

9 
header "Bool lists and integers" 

10 

37658  11 
theory Bool_List_Representation 
12 
imports Bit_Int 

26557  13 
begin 
24333  14 

37657  15 
subsection {* Operations on lists of booleans *} 
16 

17 
primrec bl_to_bin_aux :: "bool list \<Rightarrow> int \<Rightarrow> int" where 

18 
Nil: "bl_to_bin_aux [] w = w" 

19 
 Cons: "bl_to_bin_aux (b # bs) w = 

20 
bl_to_bin_aux bs (w BIT (if b then 1 else 0))" 

21 

22 
definition bl_to_bin :: "bool list \<Rightarrow> int" where 

46001
0b562d564d5f
redefine some binary operations on integers work on abstract numerals instead of Int.Pls and Int.Min
huffman
parents:
45997
diff
changeset

23 
bl_to_bin_def: "bl_to_bin bs = bl_to_bin_aux bs 0" 
37667  24 

37657  25 
primrec bin_to_bl_aux :: "nat \<Rightarrow> int \<Rightarrow> bool list \<Rightarrow> bool list" where 
26 
Z: "bin_to_bl_aux 0 w bl = bl" 

27 
 Suc: "bin_to_bl_aux (Suc n) w bl = 

28 
bin_to_bl_aux n (bin_rest w) ((bin_last w = 1) # bl)" 

29 

30 
definition bin_to_bl :: "nat \<Rightarrow> int \<Rightarrow> bool list" where 

31 
bin_to_bl_def : "bin_to_bl n w = bin_to_bl_aux n w []" 

32 

33 
primrec bl_of_nth :: "nat \<Rightarrow> (nat \<Rightarrow> bool) \<Rightarrow> bool list" where 

34 
Suc: "bl_of_nth (Suc n) f = f n # bl_of_nth n f" 

35 
 Z: "bl_of_nth 0 f = []" 

36 

37 
primrec takefill :: "'a \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where 

38 
Z: "takefill fill 0 xs = []" 

39 
 Suc: "takefill fill (Suc n) xs = ( 

40 
case xs of [] => fill # takefill fill n xs 

41 
 y # ys => y # takefill fill n ys)" 

42 

43 
definition map2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list" where 

44 
"map2 f as bs = map (split f) (zip as bs)" 

45 

46 
lemma map2_Nil [simp]: "map2 f [] ys = []" 

47 
unfolding map2_def by auto 

48 

49 
lemma map2_Nil2 [simp]: "map2 f xs [] = []" 

50 
unfolding map2_def by auto 

51 

52 
lemma map2_Cons [simp]: 

53 
"map2 f (x # xs) (y # ys) = f x y # map2 f xs ys" 

54 
unfolding map2_def by auto 

55 

56 

24465  57 
subsection "Arithmetic in terms of bool lists" 
58 

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

59 
text {* 
5930d35c976d
removed unused legacy lemma names, some comment cleanup.
kleing
parents:
41842
diff
changeset

60 
Arithmetic operations in terms of the reversed bool list, 
5930d35c976d
removed unused legacy lemma names, some comment cleanup.
kleing
parents:
41842
diff
changeset

61 
assuming input list(s) the same length, and don't extend them. 
5930d35c976d
removed unused legacy lemma names, some comment cleanup.
kleing
parents:
41842
diff
changeset

62 
*} 
24465  63 

26557  64 
primrec rbl_succ :: "bool list => bool list" where 
24465  65 
Nil: "rbl_succ Nil = Nil" 
26557  66 
 Cons: "rbl_succ (x # xs) = (if x then False # rbl_succ xs else True # xs)" 
24465  67 

26557  68 
primrec rbl_pred :: "bool list => bool list" where 
69 
Nil: "rbl_pred Nil = Nil" 

70 
 Cons: "rbl_pred (x # xs) = (if x then False # xs else True # rbl_pred xs)" 

24465  71 

26557  72 
primrec rbl_add :: "bool list => bool list => bool list" where 
44939
5930d35c976d
removed unused legacy lemma names, some comment cleanup.
kleing
parents:
41842
diff
changeset

73 
 "result is length of first arg, second arg may be longer" 
26557  74 
Nil: "rbl_add Nil x = Nil" 
75 
 Cons: "rbl_add (y # ys) x = (let ws = rbl_add ys (tl x) in 

24465  76 
(y ~= hd x) # (if hd x & y then rbl_succ ws else ws))" 
77 

26557  78 
primrec rbl_mult :: "bool list => bool list => bool list" where 
44939
5930d35c976d
removed unused legacy lemma names, some comment cleanup.
kleing
parents:
41842
diff
changeset

79 
 "result is length of first arg, second arg may be longer" 
26557  80 
Nil: "rbl_mult Nil x = Nil" 
81 
 Cons: "rbl_mult (y # ys) x = (let ws = False # rbl_mult ys x in 

24465  82 
if y then rbl_add ws x else ws)" 
24333  83 

84 
lemma butlast_power: 

30971  85 
"(butlast ^^ n) bl = take (length bl  n) bl" 
24333  86 
by (induct n) (auto simp: butlast_take) 
87 

46001
0b562d564d5f
redefine some binary operations on integers work on abstract numerals instead of Int.Pls and Int.Min
huffman
parents:
45997
diff
changeset

88 
lemma bin_to_bl_aux_zero_minus_simp [simp]: 
0b562d564d5f
redefine some binary operations on integers work on abstract numerals instead of Int.Pls and Int.Min
huffman
parents:
45997
diff
changeset

89 
"0 < n \<Longrightarrow> bin_to_bl_aux n 0 bl = 
0b562d564d5f
redefine some binary operations on integers work on abstract numerals instead of Int.Pls and Int.Min
huffman
parents:
45997
diff
changeset

90 
bin_to_bl_aux (n  1) 0 (False # bl)" 
0b562d564d5f
redefine some binary operations on integers work on abstract numerals instead of Int.Pls and Int.Min
huffman
parents:
45997
diff
changeset

91 
by (cases n) auto 
0b562d564d5f
redefine some binary operations on integers work on abstract numerals instead of Int.Pls and Int.Min
huffman
parents:
45997
diff
changeset

92 

46617
8c5d10d41391
make bool list functions respect int/bin distinction
huffman
parents:
46240
diff
changeset

93 
lemma bin_to_bl_aux_minus1_minus_simp [simp]: 
8c5d10d41391
make bool list functions respect int/bin distinction
huffman
parents:
46240
diff
changeset

94 
"0 < n ==> bin_to_bl_aux n 1 bl = 
8c5d10d41391
make bool list functions respect int/bin distinction
huffman
parents:
46240
diff
changeset

95 
bin_to_bl_aux (n  1) 1 (True # bl)" 
24333  96 
by (cases n) auto 
97 

46617
8c5d10d41391
make bool list functions respect int/bin distinction
huffman
parents:
46240
diff
changeset

98 
lemma bin_to_bl_aux_one_minus_simp [simp]: 
8c5d10d41391
make bool list functions respect int/bin distinction
huffman
parents:
46240
diff
changeset

99 
"0 < n \<Longrightarrow> bin_to_bl_aux n 1 bl = 
8c5d10d41391
make bool list functions respect int/bin distinction
huffman
parents:
46240
diff
changeset

100 
bin_to_bl_aux (n  1) 0 (True # bl)" 
24333  101 
by (cases n) auto 
102 

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

103 
lemma bin_to_bl_aux_Bit_minus_simp [simp]: 
24333  104 
"0 < n ==> bin_to_bl_aux n (w BIT b) bl = 
37654  105 
bin_to_bl_aux (n  1) w ((b = 1) # bl)" 
24333  106 
by (cases n) auto 
107 

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

108 
lemma bin_to_bl_aux_Bit0_minus_simp [simp]: 
46617
8c5d10d41391
make bool list functions respect int/bin distinction
huffman
parents:
46240
diff
changeset

109 
"0 < n ==> bin_to_bl_aux n (number_of (Int.Bit0 w)) bl = 
8c5d10d41391
make bool list functions respect int/bin distinction
huffman
parents:
46240
diff
changeset

110 
bin_to_bl_aux (n  1) (number_of w) (False # bl)" 
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26008
diff
changeset

111 
by (cases n) auto 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26008
diff
changeset

112 

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

113 
lemma bin_to_bl_aux_Bit1_minus_simp [simp]: 
46617
8c5d10d41391
make bool list functions respect int/bin distinction
huffman
parents:
46240
diff
changeset

114 
"0 < n ==> bin_to_bl_aux n (number_of (Int.Bit1 w)) bl = 
8c5d10d41391
make bool list functions respect int/bin distinction
huffman
parents:
46240
diff
changeset

115 
bin_to_bl_aux (n  1) (number_of w) (True # bl)" 
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
26008
diff
changeset

116 
by (cases n) auto 
24333  117 

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

118 
text {* Link between bin and bool list. *} 
24465  119 

26557  120 
lemma bl_to_bin_aux_append: 
121 
"bl_to_bin_aux (bs @ cs) w = bl_to_bin_aux cs (bl_to_bin_aux bs w)" 

122 
by (induct bs arbitrary: w) auto 

24465  123 

26557  124 
lemma bin_to_bl_aux_append: 
125 
"bin_to_bl_aux n w bs @ cs = bin_to_bl_aux n w (bs @ cs)" 

126 
by (induct n arbitrary: w bs) auto 

24333  127 

24465  128 
lemma bl_to_bin_append: 
26557  129 
"bl_to_bin (bs @ cs) = bl_to_bin_aux cs (bl_to_bin bs)" 
24465  130 
unfolding bl_to_bin_def by (rule bl_to_bin_aux_append) 
131 

24333  132 
lemma bin_to_bl_aux_alt: 
133 
"bin_to_bl_aux n w bs = bin_to_bl n w @ bs" 

134 
unfolding bin_to_bl_def by (simp add : bin_to_bl_aux_append) 

135 

45996
e69d631fe9af
declare simp rules immediately, instead of using 'declare' commands
huffman
parents:
45854
diff
changeset

136 
lemma bin_to_bl_0 [simp]: "bin_to_bl 0 bs = []" 
24333  137 
unfolding bin_to_bl_def by auto 
138 

26557  139 
lemma size_bin_to_bl_aux: 
140 
"size (bin_to_bl_aux n w bs) = n + length bs" 

141 
by (induct n arbitrary: w bs) auto 

24333  142 

45996
e69d631fe9af
declare simp rules immediately, instead of using 'declare' commands
huffman
parents:
45854
diff
changeset

143 
lemma size_bin_to_bl [simp]: "size (bin_to_bl n w) = n" 
24333  144 
unfolding bin_to_bl_def by (simp add : size_bin_to_bl_aux) 
145 

26557  146 
lemma bin_bl_bin': 
147 
"bl_to_bin (bin_to_bl_aux n w bs) = 

148 
bl_to_bin_aux bs (bintrunc n w)" 

149 
by (induct n arbitrary: w bs) (auto simp add : bl_to_bin_def) 

24465  150 

45996
e69d631fe9af
declare simp rules immediately, instead of using 'declare' commands
huffman
parents:
45854
diff
changeset

151 
lemma bin_bl_bin [simp]: "bl_to_bin (bin_to_bl n w) = bintrunc n w" 
24465  152 
unfolding bin_to_bl_def bin_bl_bin' by auto 
153 

26557  154 
lemma bl_bin_bl': 
155 
"bin_to_bl (n + length bs) (bl_to_bin_aux bs w) = 

24465  156 
bin_to_bl_aux n w bs" 
26557  157 
apply (induct bs arbitrary: w n) 
24465  158 
apply auto 
159 
apply (simp_all only : add_Suc [symmetric]) 

160 
apply (auto simp add : bin_to_bl_def) 

161 
done 

162 

45996
e69d631fe9af
declare simp rules immediately, instead of using 'declare' commands
huffman
parents:
45854
diff
changeset

163 
lemma bl_bin_bl [simp]: "bin_to_bl (length bs) (bl_to_bin bs) = bs" 
24465  164 
unfolding bl_to_bin_def 
165 
apply (rule box_equals) 

166 
apply (rule bl_bin_bl') 

167 
prefer 2 

168 
apply (rule bin_to_bl_aux.Z) 

169 
apply simp 

170 
done 

171 

172 
lemma bl_to_bin_inj: 

173 
"bl_to_bin bs = bl_to_bin cs ==> length bs = length cs ==> bs = cs" 

174 
apply (rule_tac box_equals) 

175 
defer 

176 
apply (rule bl_bin_bl) 

177 
apply (rule bl_bin_bl) 

178 
apply simp 

179 
done 

180 

45996
e69d631fe9af
declare simp rules immediately, instead of using 'declare' commands
huffman
parents:
45854
diff
changeset

181 
lemma bl_to_bin_False [simp]: "bl_to_bin (False # bl) = bl_to_bin bl" 
46001
0b562d564d5f
redefine some binary operations on integers work on abstract numerals instead of Int.Pls and Int.Min
huffman
parents:
45997
diff
changeset

182 
unfolding bl_to_bin_def by auto 
45996
e69d631fe9af
declare simp rules immediately, instead of using 'declare' commands
huffman
parents:
45854
diff
changeset

183 

46001
0b562d564d5f
redefine some binary operations on integers work on abstract numerals instead of Int.Pls and Int.Min
huffman
parents:
45997
diff
changeset

184 
lemma bl_to_bin_Nil [simp]: "bl_to_bin [] = 0" 
24465  185 
unfolding bl_to_bin_def by auto 
186 

46001
0b562d564d5f
redefine some binary operations on integers work on abstract numerals instead of Int.Pls and Int.Min
huffman
parents:
45997
diff
changeset

187 
lemma bin_to_bl_zero_aux: 
0b562d564d5f
redefine some binary operations on integers work on abstract numerals instead of Int.Pls and Int.Min
huffman
parents:
45997
diff
changeset

188 
"bin_to_bl_aux n 0 bl = replicate n False @ bl" 
0b562d564d5f
redefine some binary operations on integers work on abstract numerals instead of Int.Pls and Int.Min
huffman
parents:
45997
diff
changeset

189 
by (induct n arbitrary: bl) (auto simp: replicate_app_Cons_same) 
0b562d564d5f
redefine some binary operations on integers work on abstract numerals instead of Int.Pls and Int.Min
huffman
parents:
45997
diff
changeset

190 

46617
8c5d10d41391
make bool list functions respect int/bin distinction
huffman
parents:
46240
diff
changeset

191 
lemma bin_to_bl_zero: "bin_to_bl n 0 = replicate n False" 
8c5d10d41391
make bool list functions respect int/bin distinction
huffman
parents:
46240
diff
changeset

192 
unfolding bin_to_bl_def by (simp add: bin_to_bl_zero_aux) 
8c5d10d41391
make bool list functions respect int/bin distinction
huffman
parents:
46240
diff
changeset

193 

8c5d10d41391
make bool list functions respect int/bin distinction
huffman
parents:
46240
diff
changeset

194 
lemma bin_to_bl_minus1_aux: 
8c5d10d41391
make bool list functions respect int/bin distinction
huffman
parents:
46240
diff
changeset

195 
"bin_to_bl_aux n 1 bl = replicate n True @ bl" 
26557  196 
by (induct n arbitrary: bl) (auto simp: replicate_app_Cons_same) 
24333  197 

46617
8c5d10d41391
make bool list functions respect int/bin distinction
huffman
parents:
46240
diff
changeset

198 
lemma bin_to_bl_minus1: "bin_to_bl n 1 = replicate n True" 
8c5d10d41391
make bool list functions respect int/bin distinction
huffman
parents:
46240
diff
changeset

199 
unfolding bin_to_bl_def by (simp add: bin_to_bl_minus1_aux) 
24333  200 

24465  201 
lemma bl_to_bin_rep_F: 
202 
"bl_to_bin (replicate n False @ bl) = bl_to_bin bl" 

46001
0b562d564d5f
redefine some binary operations on integers work on abstract numerals instead of Int.Pls and Int.Min
huffman
parents:
45997
diff
changeset

203 
apply (simp add: bin_to_bl_zero_aux [symmetric] bin_bl_bin') 
24465  204 
apply (simp add: bl_to_bin_def) 
205 
done 

206 

45996
e69d631fe9af
declare simp rules immediately, instead of using 'declare' commands
huffman
parents:
45854
diff
changeset

207 
lemma bin_to_bl_trunc [simp]: 
24465  208 
"n <= m ==> bin_to_bl n (bintrunc m w) = bin_to_bl n w" 
209 
by (auto intro: bl_to_bin_inj) 

210 

45997
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

211 
lemma bin_to_bl_aux_bintr: 
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

212 
"bin_to_bl_aux n (bintrunc m bin) bl = 
24333  213 
replicate (n  m) False @ bin_to_bl_aux (min n m) bin bl" 
45997
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

214 
apply (induct n arbitrary: m bin bl) 
24333  215 
apply clarsimp 
216 
apply clarsimp 

217 
apply (case_tac "m") 

46001
0b562d564d5f
redefine some binary operations on integers work on abstract numerals instead of Int.Pls and Int.Min
huffman
parents:
45997
diff
changeset

218 
apply (clarsimp simp: bin_to_bl_zero_aux) 
24333  219 
apply (erule thin_rl) 
220 
apply (induct_tac n) 

221 
apply auto 

222 
done 

223 

45854
40554613b4f0
replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents:
45847
diff
changeset

224 
lemma bin_to_bl_bintr: 
40554613b4f0
replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents:
45847
diff
changeset

225 
"bin_to_bl n (bintrunc m bin) = 
40554613b4f0
replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents:
45847
diff
changeset

226 
replicate (n  m) False @ bin_to_bl (min n m) bin" 
40554613b4f0
replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents:
45847
diff
changeset

227 
unfolding bin_to_bl_def by (rule bin_to_bl_aux_bintr) 
24333  228 

46001
0b562d564d5f
redefine some binary operations on integers work on abstract numerals instead of Int.Pls and Int.Min
huffman
parents:
45997
diff
changeset

229 
lemma bl_to_bin_rep_False: "bl_to_bin (replicate n False) = 0" 
24465  230 
by (induct n) auto 
231 

26557  232 
lemma len_bin_to_bl_aux: 
233 
"length (bin_to_bl_aux n w bs) = n + length bs" 

234 
by (induct n arbitrary: w bs) auto 

24333  235 

236 
lemma len_bin_to_bl [simp]: "length (bin_to_bl n w) = n" 

46617
8c5d10d41391
make bool list functions respect int/bin distinction
huffman
parents:
46240
diff
changeset

237 
by (fact size_bin_to_bl) (* FIXME: duplicate *) 
24333  238 

26557  239 
lemma sign_bl_bin': 
240 
"bin_sign (bl_to_bin_aux bs w) = bin_sign w" 

241 
by (induct bs arbitrary: w) auto 

24333  242 

46001
0b562d564d5f
redefine some binary operations on integers work on abstract numerals instead of Int.Pls and Int.Min
huffman
parents:
45997
diff
changeset

243 
lemma sign_bl_bin: "bin_sign (bl_to_bin bs) = 0" 
24333  244 
unfolding bl_to_bin_def by (simp add : sign_bl_bin') 
245 

26557  246 
lemma bl_sbin_sign_aux: 
247 
"hd (bin_to_bl_aux (Suc n) w bs) = 

46001
0b562d564d5f
redefine some binary operations on integers work on abstract numerals instead of Int.Pls and Int.Min
huffman
parents:
45997
diff
changeset

248 
(bin_sign (sbintrunc n w) = 1)" 
26557  249 
apply (induct n arbitrary: w bs) 
24333  250 
apply clarsimp 
26557  251 
apply (cases w rule: bin_exhaust) 
24333  252 
apply (simp split add : bit.split) 
253 
apply clarsimp 

254 
done 

255 

256 
lemma bl_sbin_sign: 

46001
0b562d564d5f
redefine some binary operations on integers work on abstract numerals instead of Int.Pls and Int.Min
huffman
parents:
45997
diff
changeset

257 
"hd (bin_to_bl (Suc n) w) = (bin_sign (sbintrunc n w) = 1)" 
24333  258 
unfolding bin_to_bl_def by (rule bl_sbin_sign_aux) 
259 

45997
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

260 
lemma bin_nth_of_bl_aux: 
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

261 
"bin_nth (bl_to_bin_aux bl w) n = 
24333  262 
(n < size bl & rev bl ! n  n >= length bl & bin_nth w (n  size bl))" 
45997
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

263 
apply (induct bl arbitrary: w) 
24333  264 
apply clarsimp 
265 
apply clarsimp 

45997
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

266 
apply (cut_tac x=n and y="size bl" in linorder_less_linear) 
24333  267 
apply (erule disjE, simp add: nth_append)+ 
26557  268 
apply auto 
24333  269 
done 
270 

45475  271 
lemma bin_nth_of_bl: "bin_nth (bl_to_bin bl) n = (n < length bl & rev bl ! n)" 
24333  272 
unfolding bl_to_bin_def by (simp add : bin_nth_of_bl_aux) 
273 

45997
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

274 
lemma bin_nth_bl: "n < m \<Longrightarrow> bin_nth w n = nth (rev (bin_to_bl m w)) n" 
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

275 
apply (induct n arbitrary: m w) 
24333  276 
apply clarsimp 
277 
apply (case_tac m, clarsimp) 

278 
apply (clarsimp simp: bin_to_bl_def) 

279 
apply (simp add: bin_to_bl_aux_alt) 

280 
apply clarsimp 

281 
apply (case_tac m, clarsimp) 

282 
apply (clarsimp simp: bin_to_bl_def) 

283 
apply (simp add: bin_to_bl_aux_alt) 

284 
done 

285 

45997
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

286 
lemma nth_rev: 
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

287 
"n < length xs \<Longrightarrow> rev xs ! n = xs ! (length xs  1  n)" 
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

288 
apply (induct xs) 
24465  289 
apply simp 
290 
apply (clarsimp simp add : nth_append nth.simps split add : nat.split) 

45997
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

291 
apply (rule_tac f = "\<lambda>n. xs ! n" in arg_cong) 
24465  292 
apply arith 
293 
done 

294 

45854
40554613b4f0
replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents:
45847
diff
changeset

295 
lemma nth_rev_alt: "n < length ys \<Longrightarrow> ys ! n = rev ys ! (length ys  Suc n)" 
40554613b4f0
replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents:
45847
diff
changeset

296 
by (simp add: nth_rev) 
24465  297 

45997
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

298 
lemma nth_bin_to_bl_aux: 
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

299 
"n < m + length bl \<Longrightarrow> (bin_to_bl_aux m w bl) ! n = 
24333  300 
(if n < m then bin_nth w (m  1  n) else bl ! (n  m))" 
45997
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

301 
apply (induct m arbitrary: w n bl) 
24333  302 
apply clarsimp 
303 
apply clarsimp 

304 
apply (case_tac w rule: bin_exhaust) 

305 
apply simp 

306 
done 

45997
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

307 

24333  308 
lemma nth_bin_to_bl: "n < m ==> (bin_to_bl m w) ! n = bin_nth w (m  Suc n)" 
309 
unfolding bin_to_bl_def by (simp add : nth_bin_to_bl_aux) 

310 

45997
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

311 
lemma bl_to_bin_lt2p_aux: 
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

312 
"bl_to_bin_aux bs w < (w + 1) * (2 ^ length bs)" 
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

313 
apply (induct bs arbitrary: w) 
24333  314 
apply clarsimp 
315 
apply clarsimp 

316 
apply safe 

46240
933f35c4e126
factorcancellation simprocs now call the full simplifier to prove that factors are nonzero
huffman
parents:
46001
diff
changeset

317 
apply (drule meta_spec, erule xtr8 [rotated], simp add: Bit_def)+ 
24333  318 
done 
319 

320 
lemma bl_to_bin_lt2p: "bl_to_bin bs < (2 ^ length bs)" 

321 
apply (unfold bl_to_bin_def) 

322 
apply (rule xtr1) 

323 
prefer 2 

324 
apply (rule bl_to_bin_lt2p_aux) 

325 
apply simp 

326 
done 

327 

45997
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

328 
lemma bl_to_bin_ge2p_aux: 
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

329 
"bl_to_bin_aux bs w >= w * (2 ^ length bs)" 
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

330 
apply (induct bs arbitrary: w) 
24333  331 
apply clarsimp 
332 
apply clarsimp 

333 
apply safe 

46652  334 
apply (drule meta_spec, erule order_trans [rotated], 
335 
simp add: Bit_B0_2t Bit_B1_2t algebra_simps)+ 

24333  336 
done 
337 

338 
lemma bl_to_bin_ge0: "bl_to_bin bs >= 0" 

339 
apply (unfold bl_to_bin_def) 

340 
apply (rule xtr4) 

341 
apply (rule bl_to_bin_ge2p_aux) 

46617
8c5d10d41391
make bool list functions respect int/bin distinction
huffman
parents:
46240
diff
changeset

342 
apply simp 
24333  343 
done 
344 

345 
lemma butlast_rest_bin: 

346 
"butlast (bin_to_bl n w) = bin_to_bl (n  1) (bin_rest w)" 

347 
apply (unfold bin_to_bl_def) 

348 
apply (cases w rule: bin_exhaust) 

349 
apply (cases n, clarsimp) 

350 
apply clarsimp 

351 
apply (auto simp add: bin_to_bl_aux_alt) 

352 
done 

353 

45854
40554613b4f0
replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents:
45847
diff
changeset

354 
lemma butlast_bin_rest: 
40554613b4f0
replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents:
45847
diff
changeset

355 
"butlast bl = bin_to_bl (length bl  Suc 0) (bin_rest (bl_to_bin bl))" 
40554613b4f0
replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents:
45847
diff
changeset

356 
using butlast_rest_bin [where w="bl_to_bin bl" and n="length bl"] by simp 
24333  357 

26557  358 
lemma butlast_rest_bl2bin_aux: 
359 
"bl ~= [] \<Longrightarrow> 

360 
bl_to_bin_aux (butlast bl) w = bin_rest (bl_to_bin_aux bl w)" 

361 
by (induct bl arbitrary: w) auto 

24333  362 

363 
lemma butlast_rest_bl2bin: 

364 
"bl_to_bin (butlast bl) = bin_rest (bl_to_bin bl)" 

365 
apply (unfold bl_to_bin_def) 

366 
apply (cases bl) 

367 
apply (auto simp add: butlast_rest_bl2bin_aux) 

368 
done 

369 

45997
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

370 
lemma trunc_bl2bin_aux: 
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

371 
"bintrunc m (bl_to_bin_aux bl w) = 
26557  372 
bl_to_bin_aux (drop (length bl  m) bl) (bintrunc (m  length bl) w)" 
45997
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

373 
apply (induct bl arbitrary: w) 
24333  374 
apply clarsimp 
375 
apply clarsimp 

376 
apply safe 

45997
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

377 
apply (case_tac "m  size bl") 
24333  378 
apply (simp add : diff_is_0_eq [THEN iffD1, THEN Suc_diff_le]) 
46652  379 
apply simp 
380 
apply (rule_tac f = "%nat. bl_to_bin_aux bl (bintrunc nat w BIT 1)" 

45997
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

381 
in arg_cong) 
24333  382 
apply simp 
45997
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

383 
apply (case_tac "m  size bl") 
24333  384 
apply (simp add: diff_is_0_eq [THEN iffD1, THEN Suc_diff_le]) 
46652  385 
apply simp 
386 
apply (rule_tac f = "%nat. bl_to_bin_aux bl (bintrunc nat w BIT 0)" 

45997
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

387 
in arg_cong) 
24333  388 
apply simp 
389 
done 

390 

391 
lemma trunc_bl2bin: 

392 
"bintrunc m (bl_to_bin bl) = bl_to_bin (drop (length bl  m) bl)" 

393 
unfolding bl_to_bin_def by (simp add : trunc_bl2bin_aux) 

394 

45854
40554613b4f0
replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents:
45847
diff
changeset

395 
lemma trunc_bl2bin_len [simp]: 
40554613b4f0
replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents:
45847
diff
changeset

396 
"bintrunc (length bl) (bl_to_bin bl) = bl_to_bin bl" 
40554613b4f0
replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents:
45847
diff
changeset

397 
by (simp add: trunc_bl2bin) 
24333  398 

399 
lemma bl2bin_drop: 

400 
"bl_to_bin (drop k bl) = bintrunc (length bl  k) (bl_to_bin bl)" 

401 
apply (rule trans) 

402 
prefer 2 

403 
apply (rule trunc_bl2bin [symmetric]) 

404 
apply (cases "k <= length bl") 

405 
apply auto 

406 
done 

407 

45997
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

408 
lemma nth_rest_power_bin: 
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

409 
"bin_nth ((bin_rest ^^ k) w) n = bin_nth w (n + k)" 
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

410 
apply (induct k arbitrary: n, clarsimp) 
24333  411 
apply clarsimp 
412 
apply (simp only: bin_nth.Suc [symmetric] add_Suc) 

413 
done 

414 

415 
lemma take_rest_power_bin: 

30971  416 
"m <= n ==> take m (bin_to_bl n w) = bin_to_bl m ((bin_rest ^^ (n  m)) w)" 
24333  417 
apply (rule nth_equalityI) 
418 
apply simp 

419 
apply (clarsimp simp add: nth_bin_to_bl nth_rest_power_bin) 

420 
done 

421 

24465  422 
lemma hd_butlast: "size xs > 1 ==> hd (butlast xs) = hd xs" 
423 
by (cases xs) auto 

24333  424 

26557  425 
lemma last_bin_last': 
37654  426 
"size xs > 0 \<Longrightarrow> last xs = (bin_last (bl_to_bin_aux xs w) = 1)" 
26557  427 
by (induct xs arbitrary: w) auto 
24333  428 

429 
lemma last_bin_last: 

37654  430 
"size xs > 0 ==> last xs = (bin_last (bl_to_bin xs) = 1)" 
24333  431 
unfolding bl_to_bin_def by (erule last_bin_last') 
432 

433 
lemma bin_last_last: 

37654  434 
"bin_last w = (if last (bin_to_bl (Suc n) w) then 1 else 0)" 
24333  435 
apply (unfold bin_to_bl_def) 
436 
apply simp 

437 
apply (auto simp add: bin_to_bl_aux_alt) 

438 
done 

439 

24465  440 
(** links between bitwise operations and operations on bool lists **) 
441 

45997
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

442 
lemma bl_xor_aux_bin: 
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

443 
"map2 (%x y. x ~= y) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) = 
26557  444 
bin_to_bl_aux n (v XOR w) (map2 (%x y. x ~= y) bs cs)" 
45997
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

445 
apply (induct n arbitrary: v w bs cs) 
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

446 
apply simp 
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

447 
apply (case_tac v rule: bin_exhaust) 
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

448 
apply (case_tac w rule: bin_exhaust) 
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

449 
apply clarsimp 
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

450 
apply (case_tac b) 
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

451 
apply (case_tac ba, safe, simp_all)+ 
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

452 
done 
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

453 

13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

454 
lemma bl_or_aux_bin: 
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

455 
"map2 (op  ) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) = 
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

456 
bin_to_bl_aux n (v OR w) (map2 (op  ) bs cs)" 
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

457 
apply (induct n arbitrary: v w bs cs) 
24333  458 
apply simp 
459 
apply (case_tac v rule: bin_exhaust) 

460 
apply (case_tac w rule: bin_exhaust) 

461 
apply clarsimp 

462 
apply (case_tac b) 

463 
apply (case_tac ba, safe, simp_all)+ 

464 
done 

465 

45997
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

466 
lemma bl_and_aux_bin: 
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

467 
"map2 (op & ) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) = 
26557  468 
bin_to_bl_aux n (v AND w) (map2 (op & ) bs cs)" 
45997
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

469 
apply (induct n arbitrary: v w bs cs) 
24333  470 
apply simp 
471 
apply (case_tac v rule: bin_exhaust) 

472 
apply (case_tac w rule: bin_exhaust) 

473 
apply clarsimp 

474 
done 

475 

45997
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

476 
lemma bl_not_aux_bin: 
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

477 
"map Not (bin_to_bl_aux n w cs) = 
24353  478 
bin_to_bl_aux n (NOT w) (map Not cs)" 
45997
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

479 
apply (induct n arbitrary: w cs) 
24333  480 
apply clarsimp 
481 
apply clarsimp 

482 
done 

483 

45854
40554613b4f0
replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents:
45847
diff
changeset

484 
lemma bl_not_bin: "map Not (bin_to_bl n w) = bin_to_bl n (NOT w)" 
40554613b4f0
replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents:
45847
diff
changeset

485 
unfolding bin_to_bl_def by (simp add: bl_not_aux_bin) 
24333  486 

45854
40554613b4f0
replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents:
45847
diff
changeset

487 
lemma bl_and_bin: 
40554613b4f0
replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents:
45847
diff
changeset

488 
"map2 (op \<and>) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v AND w)" 
40554613b4f0
replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents:
45847
diff
changeset

489 
unfolding bin_to_bl_def by (simp add: bl_and_aux_bin) 
24333  490 

45854
40554613b4f0
replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents:
45847
diff
changeset

491 
lemma bl_or_bin: 
40554613b4f0
replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents:
45847
diff
changeset

492 
"map2 (op \<or>) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v OR w)" 
40554613b4f0
replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents:
45847
diff
changeset

493 
unfolding bin_to_bl_def by (simp add: bl_or_aux_bin) 
24333  494 

45854
40554613b4f0
replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents:
45847
diff
changeset

495 
lemma bl_xor_bin: 
40554613b4f0
replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents:
45847
diff
changeset

496 
"map2 (\<lambda>x y. x \<noteq> y) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v XOR w)" 
40554613b4f0
replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents:
45847
diff
changeset

497 
unfolding bin_to_bl_def by (simp only: bl_xor_aux_bin map2_Nil) 
24333  498 

45997
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

499 
lemma drop_bin2bl_aux: 
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

500 
"drop m (bin_to_bl_aux n bin bs) = 
24333  501 
bin_to_bl_aux (n  m) bin (drop (m  n) bs)" 
45997
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

502 
apply (induct n arbitrary: m bin bs, clarsimp) 
24333  503 
apply clarsimp 
504 
apply (case_tac bin rule: bin_exhaust) 

505 
apply (case_tac "m <= n", simp) 

506 
apply (case_tac "m  n", simp) 

507 
apply simp 

508 
apply (rule_tac f = "%nat. drop nat bs" in arg_cong) 

509 
apply simp 

510 
done 

511 

512 
lemma drop_bin2bl: "drop m (bin_to_bl n bin) = bin_to_bl (n  m) bin" 

513 
unfolding bin_to_bl_def by (simp add : drop_bin2bl_aux) 

514 

45997
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

515 
lemma take_bin2bl_lem1: 
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

516 
"take m (bin_to_bl_aux m w bs) = bin_to_bl m w" 
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

517 
apply (induct m arbitrary: w bs, clarsimp) 
24333  518 
apply clarsimp 
519 
apply (simp add: bin_to_bl_aux_alt) 

520 
apply (simp add: bin_to_bl_def) 

521 
apply (simp add: bin_to_bl_aux_alt) 

522 
done 

523 

45997
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

524 
lemma take_bin2bl_lem: 
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

525 
"take m (bin_to_bl_aux (m + n) w bs) = 
24333  526 
take m (bin_to_bl (m + n) w)" 
45997
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

527 
apply (induct n arbitrary: w bs) 
24333  528 
apply (simp_all (no_asm) add: bin_to_bl_def take_bin2bl_lem1) 
529 
apply simp 

530 
done 

531 

45997
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

532 
lemma bin_split_take: 
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

533 
"bin_split n c = (a, b) \<Longrightarrow> 
24333  534 
bin_to_bl m a = take m (bin_to_bl (m + n) c)" 
45997
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

535 
apply (induct n arbitrary: b c) 
24333  536 
apply clarsimp 
537 
apply (clarsimp simp: Let_def split: ls_splits) 

538 
apply (simp add: bin_to_bl_def) 

539 
apply (simp add: take_bin2bl_lem) 

540 
done 

541 

542 
lemma bin_split_take1: 

543 
"k = m + n ==> bin_split n c = (a, b) ==> 

544 
bin_to_bl m a = take m (bin_to_bl k c)" 

545 
by (auto elim: bin_split_take) 

546 

45997
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

547 
lemma nth_takefill: "m < n \<Longrightarrow> 
24333  548 
takefill fill n l ! m = (if m < length l then l ! m else fill)" 
45997
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

549 
apply (induct n arbitrary: m l, clarsimp) 
24333  550 
apply clarsimp 
551 
apply (case_tac m) 

552 
apply (simp split: list.split) 

553 
apply (simp split: list.split) 

554 
done 

555 

45997
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

556 
lemma takefill_alt: 
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

557 
"takefill fill n l = take n l @ replicate (n  length l) fill" 
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

558 
by (induct n arbitrary: l) (auto split: list.split) 
24333  559 

560 
lemma takefill_replicate [simp]: 

561 
"takefill fill n (replicate m fill) = replicate n fill" 

562 
by (simp add : takefill_alt replicate_add [symmetric]) 

563 

45997
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

564 
lemma takefill_le': 
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

565 
"n = m + k \<Longrightarrow> takefill x m (takefill x n l) = takefill x m l" 
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

566 
by (induct m arbitrary: l n) (auto split: list.split) 
24333  567 

568 
lemma length_takefill [simp]: "length (takefill fill n l) = n" 

569 
by (simp add : takefill_alt) 

570 

571 
lemma take_takefill': 

572 
"!!w n. n = k + m ==> take k (takefill fill n w) = takefill fill k w" 

573 
by (induct k) (auto split add : list.split) 

574 

575 
lemma drop_takefill: 

576 
"!!w. drop k (takefill fill (m + k) w) = takefill fill m (drop k w)" 

577 
by (induct k) (auto split add : list.split) 

578 

579 
lemma takefill_le [simp]: 

580 
"m \<le> n \<Longrightarrow> takefill x m (takefill x n l) = takefill x m l" 

581 
by (auto simp: le_iff_add takefill_le') 

582 

583 
lemma take_takefill [simp]: 

584 
"m \<le> n \<Longrightarrow> take m (takefill fill n w) = takefill fill m w" 

585 
by (auto simp: le_iff_add take_takefill') 

586 

587 
lemma takefill_append: 

588 
"takefill fill (m + length xs) (xs @ w) = xs @ (takefill fill m w)" 

589 
by (induct xs) auto 

590 

591 
lemma takefill_same': 

592 
"l = length xs ==> takefill fill l xs = xs" 

593 
by clarify (induct xs, auto) 

594 

595 
lemmas takefill_same [simp] = takefill_same' [OF refl] 

596 

597 
lemma takefill_bintrunc: 

598 
"takefill False n bl = rev (bin_to_bl n (bl_to_bin (rev bl)))" 

599 
apply (rule nth_equalityI) 

600 
apply simp 

601 
apply (clarsimp simp: nth_takefill nth_rev nth_bin_to_bl bin_nth_of_bl) 

602 
done 

603 

604 
lemma bl_bin_bl_rtf: 

605 
"bin_to_bl n (bl_to_bin bl) = rev (takefill False n (rev bl))" 

606 
by (simp add : takefill_bintrunc) 

45854
40554613b4f0
replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents:
45847
diff
changeset

607 

40554613b4f0
replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents:
45847
diff
changeset

608 
lemma bl_bin_bl_rep_drop: 
40554613b4f0
replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents:
45847
diff
changeset

609 
"bin_to_bl n (bl_to_bin bl) = 
40554613b4f0
replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents:
45847
diff
changeset

610 
replicate (n  length bl) False @ drop (length bl  n) bl" 
40554613b4f0
replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents:
45847
diff
changeset

611 
by (simp add: bl_bin_bl_rtf takefill_alt rev_take) 
24333  612 

613 
lemma tf_rev: 

614 
"n + k = m + length bl ==> takefill x m (rev (takefill y n bl)) = 

615 
rev (takefill y m (rev (takefill x k (rev bl))))" 

616 
apply (rule nth_equalityI) 

617 
apply (auto simp add: nth_takefill nth_rev) 

618 
apply (rule_tac f = "%n. bl ! n" in arg_cong) 

619 
apply arith 

620 
done 

621 

622 
lemma takefill_minus: 

623 
"0 < n ==> takefill fill (Suc (n  1)) w = takefill fill n w" 

624 
by auto 

625 

626 
lemmas takefill_Suc_cases = 

45604  627 
list.cases [THEN takefill.Suc [THEN trans]] 
24333  628 

629 
lemmas takefill_Suc_Nil = takefill_Suc_cases (1) 

630 
lemmas takefill_Suc_Cons = takefill_Suc_cases (2) 

631 

632 
lemmas takefill_minus_simps = takefill_Suc_cases [THEN [2] 

45604  633 
takefill_minus [symmetric, THEN trans]] 
24333  634 

635 
lemmas takefill_pred_simps [simp] = 

45604  636 
takefill_minus_simps [where n="number_of bin", simplified nobm1] for bin 
24333  637 

638 
(* links with function bl_to_bin *) 

639 

640 
lemma bl_to_bin_aux_cat: 

26557  641 
"!!nv v. bl_to_bin_aux bs (bin_cat w nv v) = 
642 
bin_cat w (nv + length bs) (bl_to_bin_aux bs v)" 

24333  643 
apply (induct bs) 
644 
apply simp 

645 
apply (simp add: bin_cat_Suc_Bit [symmetric] del: bin_cat.simps) 

646 
done 

647 

648 
lemma bin_to_bl_aux_cat: 

649 
"!!w bs. bin_to_bl_aux (nv + nw) (bin_cat v nw w) bs = 

650 
bin_to_bl_aux nv v (bin_to_bl_aux nw w bs)" 

651 
by (induct nw) auto 

652 

45854
40554613b4f0
replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents:
45847
diff
changeset

653 
lemma bl_to_bin_aux_alt: 
40554613b4f0
replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents:
45847
diff
changeset

654 
"bl_to_bin_aux bs w = bin_cat w (length bs) (bl_to_bin bs)" 
46001
0b562d564d5f
redefine some binary operations on integers work on abstract numerals instead of Int.Pls and Int.Min
huffman
parents:
45997
diff
changeset

655 
using bl_to_bin_aux_cat [where nv = "0" and v = "0"] 
45854
40554613b4f0
replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents:
45847
diff
changeset

656 
unfolding bl_to_bin_def [symmetric] by simp 
24333  657 

45854
40554613b4f0
replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents:
45847
diff
changeset

658 
lemma bin_to_bl_cat: 
40554613b4f0
replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents:
45847
diff
changeset

659 
"bin_to_bl (nv + nw) (bin_cat v nw w) = 
40554613b4f0
replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents:
45847
diff
changeset

660 
bin_to_bl_aux nv v (bin_to_bl nw w)" 
40554613b4f0
replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents:
45847
diff
changeset

661 
unfolding bin_to_bl_def by (simp add: bin_to_bl_aux_cat) 
24333  662 

663 
lemmas bl_to_bin_aux_app_cat = 

664 
trans [OF bl_to_bin_aux_append bl_to_bin_aux_alt] 

665 

666 
lemmas bin_to_bl_aux_cat_app = 

667 
trans [OF bin_to_bl_aux_cat bin_to_bl_aux_alt] 

668 

45854
40554613b4f0
replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents:
45847
diff
changeset

669 
lemma bl_to_bin_app_cat: 
40554613b4f0
replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents:
45847
diff
changeset

670 
"bl_to_bin (bsa @ bs) = bin_cat (bl_to_bin bsa) (length bs) (bl_to_bin bs)" 
40554613b4f0
replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents:
45847
diff
changeset

671 
by (simp only: bl_to_bin_aux_app_cat bl_to_bin_def) 
24333  672 

45854
40554613b4f0
replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents:
45847
diff
changeset

673 
lemma bin_to_bl_cat_app: 
40554613b4f0
replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents:
45847
diff
changeset

674 
"bin_to_bl (n + nw) (bin_cat w nw wa) = bin_to_bl n w @ bin_to_bl nw wa" 
40554613b4f0
replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents:
45847
diff
changeset

675 
by (simp only: bin_to_bl_def bin_to_bl_aux_cat_app) 
24333  676 

677 
(* bl_to_bin_app_cat_alt and bl_to_bin_app_cat are easily interderivable *) 

678 
lemma bl_to_bin_app_cat_alt: 

679 
"bin_cat (bl_to_bin cs) n w = bl_to_bin (cs @ bin_to_bl n w)" 

680 
by (simp add : bl_to_bin_app_cat) 

681 

682 
lemma mask_lem: "(bl_to_bin (True # replicate n False)) = 

46645
573aff6b9b0a
adapt lemma mask_lem to respect int/bin distinction
huffman
parents:
46617
diff
changeset

683 
(bl_to_bin (replicate n True)) + 1" 
24333  684 
apply (unfold bl_to_bin_def) 
685 
apply (induct n) 

46645
573aff6b9b0a
adapt lemma mask_lem to respect int/bin distinction
huffman
parents:
46617
diff
changeset

686 
apply simp 
31790  687 
apply (simp only: Suc_eq_plus1 replicate_add 
24333  688 
append_Cons [symmetric] bl_to_bin_aux_append) 
46645
573aff6b9b0a
adapt lemma mask_lem to respect int/bin distinction
huffman
parents:
46617
diff
changeset

689 
apply (simp add: Bit_B0_2t Bit_B1_2t) 
24333  690 
done 
691 

24465  692 
(* function bl_of_nth *) 
24333  693 
lemma length_bl_of_nth [simp]: "length (bl_of_nth n f) = n" 
694 
by (induct n) auto 

695 

696 
lemma nth_bl_of_nth [simp]: 

697 
"m < n \<Longrightarrow> rev (bl_of_nth n f) ! m = f m" 

698 
apply (induct n) 

699 
apply simp 

700 
apply (clarsimp simp add : nth_append) 

701 
apply (rule_tac f = "f" in arg_cong) 

702 
apply simp 

703 
done 

704 

705 
lemma bl_of_nth_inj: 

706 
"(!!k. k < n ==> f k = g k) ==> bl_of_nth n f = bl_of_nth n g" 

707 
by (induct n) auto 

708 

45997
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

709 
lemma bl_of_nth_nth_le: 
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

710 
"n \<le> length xs \<Longrightarrow> bl_of_nth n (nth (rev xs)) = drop (length xs  n) xs" 
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

711 
apply (induct n arbitrary: xs, clarsimp) 
24333  712 
apply clarsimp 
713 
apply (rule trans [OF _ hd_Cons_tl]) 

714 
apply (frule Suc_le_lessD) 

715 
apply (simp add: nth_rev trans [OF drop_Suc drop_tl, symmetric]) 

716 
apply (subst hd_drop_conv_nth) 

717 
apply force 

718 
apply simp_all 

719 
apply (rule_tac f = "%n. drop n xs" in arg_cong) 

720 
apply simp 

721 
done 

722 

45854
40554613b4f0
replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents:
45847
diff
changeset

723 
lemma bl_of_nth_nth [simp]: "bl_of_nth (length xs) (op ! (rev xs)) = xs" 
40554613b4f0
replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents:
45847
diff
changeset

724 
by (simp add: bl_of_nth_nth_le) 
24333  725 

726 
lemma size_rbl_pred: "length (rbl_pred bl) = length bl" 

727 
by (induct bl) auto 

728 

729 
lemma size_rbl_succ: "length (rbl_succ bl) = length bl" 

730 
by (induct bl) auto 

731 

732 
lemma size_rbl_add: 

733 
"!!cl. length (rbl_add bl cl) = length bl" 

734 
by (induct bl) (auto simp: Let_def size_rbl_succ) 

735 

736 
lemma size_rbl_mult: 

737 
"!!cl. length (rbl_mult bl cl) = length bl" 

738 
by (induct bl) (auto simp add : Let_def size_rbl_add) 

739 

740 
lemmas rbl_sizes [simp] = 

741 
size_rbl_pred size_rbl_succ size_rbl_add size_rbl_mult 

742 

743 
lemmas rbl_Nils = 

744 
rbl_pred.Nil rbl_succ.Nil rbl_add.Nil rbl_mult.Nil 

745 

46653  746 
lemma pred_BIT_simps [simp]: 
747 
"x BIT 0  1 = (x  1) BIT 1" 

748 
"x BIT 1  1 = x BIT 0" 

749 
by (simp_all add: Bit_B0_2t Bit_B1_2t) 

750 

751 
lemma rbl_pred: 

752 
"rbl_pred (rev (bin_to_bl n bin)) = rev (bin_to_bl n (bin  1))" 

753 
apply (induct n arbitrary: bin, simp) 

24333  754 
apply (unfold bin_to_bl_def) 
755 
apply clarsimp 

756 
apply (case_tac bin rule: bin_exhaust) 

757 
apply (case_tac b) 

46653  758 
apply (clarsimp simp: bin_to_bl_aux_alt)+ 
24333  759 
done 
760 

46653  761 
lemma succ_BIT_simps [simp]: 
762 
"x BIT 0 + 1 = x BIT 1" 

763 
"x BIT 1 + 1 = (x + 1) BIT 0" 

764 
by (simp_all add: Bit_B0_2t Bit_B1_2t) 

765 

24333  766 
lemma rbl_succ: 
46653  767 
"rbl_succ (rev (bin_to_bl n bin)) = rev (bin_to_bl n (bin + 1))" 
768 
apply (induct n arbitrary: bin, simp) 

24333  769 
apply (unfold bin_to_bl_def) 
770 
apply clarsimp 

771 
apply (case_tac bin rule: bin_exhaust) 

772 
apply (case_tac b) 

46653  773 
apply (clarsimp simp: bin_to_bl_aux_alt)+ 
24333  774 
done 
775 

46653  776 
lemma add_BIT_simps [simp]: (* FIXME: move *) 
777 
"x BIT 0 + y BIT 0 = (x + y) BIT 0" 

778 
"x BIT 0 + y BIT 1 = (x + y) BIT 1" 

779 
"x BIT 1 + y BIT 0 = (x + y) BIT 1" 

780 
"x BIT 1 + y BIT 1 = (x + y + 1) BIT 0" 

781 
by (simp_all add: Bit_B0_2t Bit_B1_2t) 

782 

24333  783 
lemma rbl_add: 
784 
"!!bina binb. rbl_add (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb)) = 

785 
rev (bin_to_bl n (bina + binb))" 

786 
apply (induct n, simp) 

787 
apply (unfold bin_to_bl_def) 

788 
apply clarsimp 

789 
apply (case_tac bina rule: bin_exhaust) 

790 
apply (case_tac binb rule: bin_exhaust) 

791 
apply (case_tac b) 

792 
apply (case_tac [!] "ba") 

46655  793 
apply (auto simp: rbl_succ bin_to_bl_aux_alt Let_def add_ac) 
24333  794 
done 
795 

796 
lemma rbl_add_app2: 

797 
"!!blb. length blb >= length bla ==> 

798 
rbl_add bla (blb @ blc) = rbl_add bla blb" 

799 
apply (induct bla, simp) 

800 
apply clarsimp 

801 
apply (case_tac blb, clarsimp) 

802 
apply (clarsimp simp: Let_def) 

803 
done 

804 

805 
lemma rbl_add_take2: 

806 
"!!blb. length blb >= length bla ==> 

807 
rbl_add bla (take (length bla) blb) = rbl_add bla blb" 

808 
apply (induct bla, simp) 

809 
apply clarsimp 

810 
apply (case_tac blb, clarsimp) 

811 
apply (clarsimp simp: Let_def) 

812 
done 

813 

814 
lemma rbl_add_long: 

815 
"m >= n ==> rbl_add (rev (bin_to_bl n bina)) (rev (bin_to_bl m binb)) = 

816 
rev (bin_to_bl n (bina + binb))" 

817 
apply (rule box_equals [OF _ rbl_add_take2 rbl_add]) 

818 
apply (rule_tac f = "rbl_add (rev (bin_to_bl n bina))" in arg_cong) 

819 
apply (rule rev_swap [THEN iffD1]) 

820 
apply (simp add: rev_take drop_bin2bl) 

821 
apply simp 

822 
done 

823 

824 
lemma rbl_mult_app2: 

825 
"!!blb. length blb >= length bla ==> 

826 
rbl_mult bla (blb @ blc) = rbl_mult bla blb" 

827 
apply (induct bla, simp) 

828 
apply clarsimp 

829 
apply (case_tac blb, clarsimp) 

830 
apply (clarsimp simp: Let_def rbl_add_app2) 

831 
done 

832 

833 
lemma rbl_mult_take2: 

834 
"length blb >= length bla ==> 

835 
rbl_mult bla (take (length bla) blb) = rbl_mult bla blb" 

836 
apply (rule trans) 

837 
apply (rule rbl_mult_app2 [symmetric]) 

838 
apply simp 

839 
apply (rule_tac f = "rbl_mult bla" in arg_cong) 

840 
apply (rule append_take_drop_id) 

841 
done 

842 

843 
lemma rbl_mult_gt1: 

844 
"m >= length bl ==> rbl_mult bl (rev (bin_to_bl m binb)) = 

845 
rbl_mult bl (rev (bin_to_bl (length bl) binb))" 

846 
apply (rule trans) 

847 
apply (rule rbl_mult_take2 [symmetric]) 

848 
apply simp_all 

849 
apply (rule_tac f = "rbl_mult bl" in arg_cong) 

850 
apply (rule rev_swap [THEN iffD1]) 

851 
apply (simp add: rev_take drop_bin2bl) 

852 
done 

853 

854 
lemma rbl_mult_gt: 

855 
"m > n ==> rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl m binb)) = 

856 
rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb))" 

857 
by (auto intro: trans [OF rbl_mult_gt1]) 

858 

859 
lemmas rbl_mult_Suc = lessI [THEN rbl_mult_gt] 

860 

861 
lemma rbbl_Cons: 

37654  862 
"b # rev (bin_to_bl n x) = rev (bin_to_bl (Suc n) (x BIT If b 1 0))" 
24333  863 
apply (unfold bin_to_bl_def) 
864 
apply simp 

865 
apply (simp add: bin_to_bl_aux_alt) 

866 
done 

46653  867 

868 
lemma mult_BIT_simps [simp]: 

869 
"x BIT 0 * y = (x * y) BIT 0" 

870 
"x * y BIT 0 = (x * y) BIT 0" 

871 
"x BIT 1 * y = (x * y) BIT 0 + y" 

872 
by (simp_all add: Bit_B0_2t Bit_B1_2t algebra_simps) 

873 

24333  874 
lemma rbl_mult: "!!bina binb. 
875 
rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb)) = 

876 
rev (bin_to_bl n (bina * binb))" 

877 
apply (induct n) 

878 
apply simp 

879 
apply (unfold bin_to_bl_def) 

880 
apply clarsimp 

881 
apply (case_tac bina rule: bin_exhaust) 

882 
apply (case_tac binb rule: bin_exhaust) 

883 
apply (case_tac b) 

884 
apply (case_tac [!] "ba") 

46653  885 
apply (auto simp: bin_to_bl_aux_alt Let_def) 
886 
apply (auto simp: rbbl_Cons rbl_mult_Suc rbl_add) 

24333  887 
done 
888 

889 
lemma rbl_add_split: 

890 
"P (rbl_add (y # ys) (x # xs)) = 

891 
(ALL ws. length ws = length ys > ws = rbl_add ys xs > 

26008  892 
(y > ((x > P (False # rbl_succ ws)) & (~ x > P (True # ws)))) & 
24333  893 
(~ y > P (x # ws)))" 
894 
apply (auto simp add: Let_def) 

895 
apply (case_tac [!] "y") 

896 
apply auto 

897 
done 

898 

899 
lemma rbl_mult_split: 

900 
"P (rbl_mult (y # ys) xs) = 

901 
(ALL ws. length ws = Suc (length ys) > ws = False # rbl_mult ys xs > 

902 
(y > P (rbl_add ws xs)) & (~ y > P ws))" 

903 
by (clarsimp simp add : Let_def) 

904 

905 
lemma and_len: "xs = ys ==> xs = ys & length xs = length ys" 

906 
by auto 

907 

908 
lemma size_if: "size (if p then xs else ys) = (if p then size xs else size ys)" 

909 
by auto 

910 

911 
lemma tl_if: "tl (if p then xs else ys) = (if p then tl xs else tl ys)" 

912 
by auto 

913 

914 
lemma hd_if: "hd (if p then xs else ys) = (if p then hd xs else hd ys)" 

915 
by auto 

916 

24465  917 
lemma if_Not_x: "(if p then ~ x else x) = (p = (~ x))" 
918 
by auto 

919 

920 
lemma if_x_Not: "(if p then x else ~ x) = (p = x)" 

921 
by auto 

922 

24333  923 
lemma if_same_and: "(If p x y & If p u v) = (if p then x & u else y & v)" 
924 
by auto 

925 

926 
lemma if_same_eq: "(If p x y = (If p u v)) = (if p then x = (u) else y = (v))" 

927 
by auto 

928 

929 
lemma if_same_eq_not: 

930 
"(If p x y = (~ If p u v)) = (if p then x = (~u) else y = (~v))" 

931 
by auto 

932 

933 
(* note  if_Cons can cause blowup in the size, if p is complex, 

934 
so make a simproc *) 

935 
lemma if_Cons: "(if p then x # xs else y # ys) = If p x y # If p xs ys" 

936 
by auto 

937 

938 
lemma if_single: 

939 
"(if xc then [xab] else [an]) = [if xc then xab else an]" 

940 
by auto 

941 

24465  942 
lemma if_bool_simps: 
943 
"If p True y = (p  y) & If p False y = (~p & y) & 

944 
If p y True = (p > y) & If p y False = (p & y)" 

945 
by auto 

946 

947 
lemmas if_simps = if_x_Not if_Not_x if_cancel if_True if_False if_bool_simps 

948 

45854
40554613b4f0
replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents:
45847
diff
changeset

949 
lemmas seqr = eq_reflection [where x = "size w"] for w (* FIXME: delete *) 
24333  950 

45854
40554613b4f0
replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents:
45847
diff
changeset

951 
(* TODO: move name bindings to List.thy *) 
24333  952 
lemmas tl_Nil = tl.simps (1) 
953 
lemmas tl_Cons = tl.simps (2) 

954 

955 

24350  956 
subsection "Repeated splitting or concatenation" 
24333  957 

958 
lemma sclem: 

959 
"size (concat (map (bin_to_bl n) xs)) = length xs * n" 

960 
by (induct xs) auto 

961 

45997
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

962 
lemma bin_cat_foldl_lem: 
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

963 
"foldl (%u. bin_cat u n) x xs = 
24333  964 
bin_cat x (size xs * n) (foldl (%u. bin_cat u n) y xs)" 
45997
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

965 
apply (induct xs arbitrary: x) 
24333  966 
apply simp 
967 
apply (simp (no_asm)) 

968 
apply (frule asm_rl) 

45997
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

969 
apply (drule meta_spec) 
24333  970 
apply (erule trans) 
45997
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

971 
apply (drule_tac x = "bin_cat y n a" in meta_spec) 
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

972 
apply (simp add : bin_cat_assoc_sym min_max.inf_absorb2) 
24333  973 
done 
974 

975 
lemma bin_rcat_bl: 

976 
"(bin_rcat n wl) = bl_to_bin (concat (map (bin_to_bl n) wl))" 

977 
apply (unfold bin_rcat_def) 

978 
apply (rule sym) 

979 
apply (induct wl) 

980 
apply (auto simp add : bl_to_bin_append) 

981 
apply (simp add : bl_to_bin_aux_alt sclem) 

982 
apply (simp add : bin_cat_foldl_lem [symmetric]) 

983 
done 

984 

985 
lemmas bin_rsplit_aux_simps = bin_rsplit_aux.simps bin_rsplitl_aux.simps 

986 
lemmas rsplit_aux_simps = bin_rsplit_aux_simps 

987 

45604  988 
lemmas th_if_simp1 = split_if [where P = "op = l", THEN iffD1, THEN conjunct1, THEN mp] for l 
989 
lemmas th_if_simp2 = split_if [where P = "op = l", THEN iffD1, THEN conjunct2, THEN mp] for l 

24333  990 

991 
lemmas rsplit_aux_simp1s = rsplit_aux_simps [THEN th_if_simp1] 

992 

993 
lemmas rsplit_aux_simp2ls = rsplit_aux_simps [THEN th_if_simp2] 

994 
(* these safe to [simp add] as require calculating m  n *) 

995 
lemmas bin_rsplit_aux_simp2s [simp] = rsplit_aux_simp2ls [unfolded Let_def] 

996 
lemmas rbscl = bin_rsplit_aux_simp2s (2) 

997 

998 
lemmas rsplit_aux_0_simps [simp] = 

999 
rsplit_aux_simp1s [OF disjI1] rsplit_aux_simp1s [OF disjI2] 

1000 

1001 
lemma bin_rsplit_aux_append: 

26557  1002 
"bin_rsplit_aux n m c (bs @ cs) = bin_rsplit_aux n m c bs @ cs" 
1003 
apply (induct n m c bs rule: bin_rsplit_aux.induct) 

24333  1004 
apply (subst bin_rsplit_aux.simps) 
1005 
apply (subst bin_rsplit_aux.simps) 

1006 
apply (clarsimp split: ls_splits) 

26557  1007 
apply auto 
24333  1008 
done 
1009 

1010 
lemma bin_rsplitl_aux_append: 

26557  1011 
"bin_rsplitl_aux n m c (bs @ cs) = bin_rsplitl_aux n m c bs @ cs" 
1012 
apply (induct n m c bs rule: bin_rsplitl_aux.induct) 

24333  1013 
apply (subst bin_rsplitl_aux.simps) 
1014 
apply (subst bin_rsplitl_aux.simps) 

1015 
apply (clarsimp split: ls_splits) 

26557  1016 
apply auto 
24333  1017 
done 
1018 

1019 
lemmas rsplit_aux_apps [where bs = "[]"] = 

1020 
bin_rsplit_aux_append bin_rsplitl_aux_append 

1021 

1022 
lemmas rsplit_def_auxs = bin_rsplit_def bin_rsplitl_def 

1023 

1024 
lemmas rsplit_aux_alts = rsplit_aux_apps 

1025 
[unfolded append_Nil rsplit_def_auxs [symmetric]] 

1026 

1027 
lemma bin_split_minus: "0 < n ==> bin_split (Suc (n  1)) w = bin_split n w" 

1028 
by auto 

1029 

1030 
lemmas bin_split_minus_simp = 

45604  1031 
bin_split.Suc [THEN [2] bin_split_minus [symmetric, THEN trans]] 
24333  1032 

1033 
lemma bin_split_pred_simp [simp]: 

1034 
"(0::nat) < number_of bin \<Longrightarrow> 

1035 
bin_split (number_of bin) w = 

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

1036 
(let (w1, w2) = bin_split (number_of (Int.pred bin)) (bin_rest w) 
24333  1037 
in (w1, w2 BIT bin_last w))" 
1038 
by (simp only: nobm1 bin_split_minus_simp) 

1039 

1040 
lemma bin_rsplit_aux_simp_alt: 

26557  1041 
"bin_rsplit_aux n m c bs = 
24333  1042 
(if m = 0 \<or> n = 0 
1043 
then bs 

1044 
else let (a, b) = bin_split n c in bin_rsplit n (m  n, a) @ b # bs)" 

26557  1045 
unfolding bin_rsplit_aux.simps [of n m c bs] 
1046 
apply simp 

1047 
apply (subst rsplit_aux_alts) 

1048 
apply (simp add: bin_rsplit_def) 

24333  1049 
done 
1050 

1051 
lemmas bin_rsplit_simp_alt = 

45604  1052 
trans [OF bin_rsplit_def bin_rsplit_aux_simp_alt] 
24333  1053 

1054 
lemmas bthrs = bin_rsplit_simp_alt [THEN [2] trans] 

1055 

1056 
lemma bin_rsplit_size_sign' [rule_format] : 

45997
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

1057 
"\<lbrakk>n > 0; rev sw = bin_rsplit n (nw, w)\<rbrakk> \<Longrightarrow> 
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

1058 
(ALL v: set sw. bintrunc n v = v)" 
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

1059 
apply (induct sw arbitrary: nw w v) 
24333  1060 
apply clarsimp 
1061 
apply clarsimp 

1062 
apply (drule bthrs) 

1063 
apply (simp (no_asm_use) add: Let_def split: ls_splits) 

1064 
apply clarify 

1065 
apply (drule split_bintrunc) 

1066 
apply simp 

1067 
done 

1068 

1069 
lemmas bin_rsplit_size_sign = bin_rsplit_size_sign' [OF asm_rl 

45604  1070 
rev_rev_ident [THEN trans] set_rev [THEN equalityD2 [THEN subsetD]]] 
24333  1071 

1072 
lemma bin_nth_rsplit [rule_format] : 

1073 
"n > 0 ==> m < n ==> (ALL w k nw. rev sw = bin_rsplit n (nw, w) > 

1074 
k < size sw > bin_nth (sw ! k) m = bin_nth w (k * n + m))" 

1075 
apply (induct sw) 

1076 
apply clarsimp 

1077 
apply clarsimp 

1078 
apply (drule bthrs) 

1079 
apply (simp (no_asm_use) add: Let_def split: ls_splits) 

1080 
apply clarify 

1081 
apply (erule allE, erule impE, erule exI) 

1082 
apply (case_tac k) 

1083 
apply clarsimp 

1084 
prefer 2 

1085 
apply clarsimp 

1086 
apply (erule allE) 

1087 
apply (erule (1) impE) 

1088 
apply (drule bin_nth_split, erule conjE, erule allE, 

1089 
erule trans, simp add : add_ac)+ 

1090 
done 

1091 

1092 
lemma bin_rsplit_all: 

1093 
"0 < nw ==> nw <= n ==> bin_rsplit n (nw, w) = [bintrunc n w]" 

1094 
unfolding bin_rsplit_def 

1095 
by (clarsimp dest!: split_bintrunc simp: rsplit_aux_simp2ls split: ls_splits) 

1096 

1097 
lemma bin_rsplit_l [rule_format] : 

1098 
"ALL bin. bin_rsplitl n (m, bin) = bin_rsplit n (m, bintrunc m bin)" 

1099 
apply (rule_tac a = "m" in wf_less_than [THEN wf_induct]) 

1100 
apply (simp (no_asm) add : bin_rsplitl_def bin_rsplit_def) 

1101 
apply (rule allI) 

1102 
apply (subst bin_rsplitl_aux.simps) 

1103 
apply (subst bin_rsplit_aux.simps) 

26557  1104 
apply (clarsimp simp: Let_def split: ls_splits) 
24333  1105 
apply (drule bin_split_trunc) 
1106 
apply (drule sym [THEN trans], assumption) 

26557  1107 
apply (subst rsplit_aux_alts(1)) 
1108 
apply (subst rsplit_aux_alts(2)) 

1109 
apply clarsimp 

1110 
unfolding bin_rsplit_def bin_rsplitl_def 

1111 
apply simp 

24333  1112 
done 
26557  1113 

24333  1114 
lemma bin_rsplit_rcat [rule_format] : 
1115 
"n > 0 > bin_rsplit n (n * size ws, bin_rcat n ws) = map (bintrunc n) ws" 

1116 
apply (unfold bin_rsplit_def bin_rcat_def) 

1117 
apply (rule_tac xs = "ws" in rev_induct) 

1118 
apply clarsimp 

1119 
apply clarsimp 

26557  1120 
apply (subst rsplit_aux_alts) 
1121 
unfolding bin_split_cat 

1122 
apply simp 

24333  1123 
done 
1124 

1125 
lemma bin_rsplit_aux_len_le [rule_format] : 

26557  1126 
"\<forall>ws m. n \<noteq> 0 \<longrightarrow> ws = bin_rsplit_aux n nw w bs \<longrightarrow> 
1127 
length ws \<le> m \<longleftrightarrow> nw + length bs * n \<le> m * n" 

1128 
apply (induct n nw w bs rule: bin_rsplit_aux.induct) 

24333  1129 
apply (subst bin_rsplit_aux.simps) 
26557  1130 
apply (simp add: lrlem Let_def split: ls_splits) 
24333  1131 
done 
1132 

1133 
lemma bin_rsplit_len_le: 

25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

1134 
"n \<noteq> 0 > ws = bin_rsplit n (nw, w) > (length ws <= m) = (nw <= m * n)" 
24333  1135 
unfolding bin_rsplit_def by (clarsimp simp add : bin_rsplit_aux_len_le) 
1136 

45997
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

1137 
lemma bin_rsplit_aux_len: 
13392893ea12
use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents:
45996
diff
changeset

1138 
"n \<noteq> 0 \<Longrightarrow> length (bin_rsplit_aux n nw w cs) = 
24333  1139 
(nw + n  1) div n + length cs" 
26557  1140 
apply (induct n nw w cs rule: bin_rsplit_aux.induct) 
24333  1141 
apply (subst bin_rsplit_aux.simps) 
1142 
apply (clarsimp simp: Let_def split: ls_splits) 

1143 
apply (erule thin_rl) 

27651
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27105
diff
changeset

1144 
apply (case_tac m) 
16a26996c30e
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents:
27105
diff
changeset

1145 
apply simp 
24333  1146 
apply (case_tac "m <= n") 
27677  1147 
apply auto 
24333  1148 
done 
1149 

1150 
lemma bin_rsplit_len: 

25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

1151 
"n\<noteq>0 ==> length (bin_rsplit n (nw, w)) = (nw + n  1) div n" 
24333  1152 
unfolding bin_rsplit_def by (clarsimp simp add : bin_rsplit_aux_len) 
1153 

26557  1154 
lemma bin_rsplit_aux_len_indep: 
1155 
"n \<noteq> 0 \<Longrightarrow> length bs = length cs \<Longrightarrow> 

1156 
length (bin_rsplit_aux n nw v bs) = 

1157 
length (bin_rsplit_aux n nw w cs)" 

1158 
proof (induct n nw w cs arbitrary: v bs rule: bin_rsplit_aux.induct) 

1159 
case (1 n m w cs v bs) show ?case 

1160 
proof (cases "m = 0") 

28298  1161 
case True then show ?thesis using `length bs = length cs` by simp 
26557  1162 
next 
1163 
case False 

1164 
from "1.hyps" `m \<noteq> 0` `n \<noteq> 0` have hyp: "\<And>v bs. length bs = Suc (length cs) \<Longrightarrow> 

1165 
length (bin_rsplit_aux n (m  n) v bs) = 

1166 
length (bin_rsplit_aux n (m  n) (fst (bin_split n w)) (snd (bin_split n w) # cs))" 

1167 
by auto 

1168 
show ?thesis using `length bs = length cs` `n \<noteq> 0` 

1169 
by (auto simp add: bin_rsplit_aux_simp_alt Let_def bin_rsplit_len 

1170 
split: ls_splits) 

1171 
qed 

1172 
qed 

24333  1173 

1174 
lemma bin_rsplit_len_indep: 

25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

1175 
"n\<noteq>0 ==> length (bin_rsplit n (nw, v)) = length (bin_rsplit n (nw, w))" 
24333  1176 
apply (unfold bin_rsplit_def) 
26557  1177 
apply (simp (no_asm)) 
24333  1178 
apply (erule bin_rsplit_aux_len_indep) 
1179 
apply (rule refl) 

1180 
done 

1181 

1182 
end 