1 (* |
1 (* Title: HOL/Word/Bool_List_Representation.thy |
2 Author: Jeremy Dawson, NICTA |
2 Author: Jeremy Dawson, NICTA |
3 |
3 |
4 Theorems to do with integers, expressed using Pls, Min, BIT, |
4 Theorems to do with integers, expressed using Pls, Min, BIT, |
5 theorems linking them to lists of booleans, and repeated splitting |
5 theorems linking them to lists of booleans, and repeated splitting |
6 and concatenation. |
6 and concatenation. |
7 *) |
7 *) |
8 |
8 |
9 section "Bool lists and integers" |
9 section "Bool lists and integers" |
10 |
10 |
11 theory Bool_List_Representation |
11 theory Bool_List_Representation |
12 imports Main Bits_Int |
12 imports Bits_Int |
13 begin |
13 begin |
14 |
14 |
15 definition map2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list" |
15 definition map2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list" |
16 where |
16 where "map2 f as bs = map (case_prod f) (zip as bs)" |
17 "map2 f as bs = map (case_prod f) (zip as bs)" |
17 |
18 |
18 lemma map2_Nil [simp, code]: "map2 f [] ys = []" |
19 lemma map2_Nil [simp, code]: |
19 by (auto simp: map2_def) |
20 "map2 f [] ys = []" |
20 |
21 unfolding map2_def by auto |
21 lemma map2_Nil2 [simp, code]: "map2 f xs [] = []" |
22 |
22 by (auto simp: map2_def) |
23 lemma map2_Nil2 [simp, code]: |
23 |
24 "map2 f xs [] = []" |
24 lemma map2_Cons [simp, code]: "map2 f (x # xs) (y # ys) = f x y # map2 f xs ys" |
25 unfolding map2_def by auto |
25 by (auto simp: map2_def) |
26 |
|
27 lemma map2_Cons [simp, code]: |
|
28 "map2 f (x # xs) (y # ys) = f x y # map2 f xs ys" |
|
29 unfolding map2_def by auto |
|
30 |
26 |
31 |
27 |
32 subsection \<open>Operations on lists of booleans\<close> |
28 subsection \<open>Operations on lists of booleans\<close> |
33 |
29 |
34 primrec bl_to_bin_aux :: "bool list \<Rightarrow> int \<Rightarrow> int" |
30 primrec bl_to_bin_aux :: "bool list \<Rightarrow> int \<Rightarrow> int" |
35 where |
31 where |
36 Nil: "bl_to_bin_aux [] w = w" |
32 Nil: "bl_to_bin_aux [] w = w" |
37 | Cons: "bl_to_bin_aux (b # bs) w = |
33 | Cons: "bl_to_bin_aux (b # bs) w = bl_to_bin_aux bs (w BIT b)" |
38 bl_to_bin_aux bs (w BIT b)" |
|
39 |
34 |
40 definition bl_to_bin :: "bool list \<Rightarrow> int" |
35 definition bl_to_bin :: "bool list \<Rightarrow> int" |
41 where |
36 where "bl_to_bin bs = bl_to_bin_aux bs 0" |
42 bl_to_bin_def: "bl_to_bin bs = bl_to_bin_aux bs 0" |
|
43 |
37 |
44 primrec bin_to_bl_aux :: "nat \<Rightarrow> int \<Rightarrow> bool list \<Rightarrow> bool list" |
38 primrec bin_to_bl_aux :: "nat \<Rightarrow> int \<Rightarrow> bool list \<Rightarrow> bool list" |
45 where |
39 where |
46 Z: "bin_to_bl_aux 0 w bl = bl" |
40 Z: "bin_to_bl_aux 0 w bl = bl" |
47 | Suc: "bin_to_bl_aux (Suc n) w bl = |
41 | Suc: "bin_to_bl_aux (Suc n) w bl = bin_to_bl_aux n (bin_rest w) ((bin_last w) # bl)" |
48 bin_to_bl_aux n (bin_rest w) ((bin_last w) # bl)" |
|
49 |
42 |
50 definition bin_to_bl :: "nat \<Rightarrow> int \<Rightarrow> bool list" |
43 definition bin_to_bl :: "nat \<Rightarrow> int \<Rightarrow> bool list" |
51 where |
44 where "bin_to_bl n w = bin_to_bl_aux n w []" |
52 bin_to_bl_def : "bin_to_bl n w = bin_to_bl_aux n w []" |
|
53 |
45 |
54 primrec bl_of_nth :: "nat \<Rightarrow> (nat \<Rightarrow> bool) \<Rightarrow> bool list" |
46 primrec bl_of_nth :: "nat \<Rightarrow> (nat \<Rightarrow> bool) \<Rightarrow> bool list" |
55 where |
47 where |
56 Suc: "bl_of_nth (Suc n) f = f n # bl_of_nth n f" |
48 Suc: "bl_of_nth (Suc n) f = f n # bl_of_nth n f" |
57 | Z: "bl_of_nth 0 f = []" |
49 | Z: "bl_of_nth 0 f = []" |
58 |
50 |
59 primrec takefill :: "'a \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list" |
51 primrec takefill :: "'a \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list" |
60 where |
52 where |
61 Z: "takefill fill 0 xs = []" |
53 Z: "takefill fill 0 xs = []" |
62 | Suc: "takefill fill (Suc n) xs = ( |
54 | Suc: "takefill fill (Suc n) xs = |
63 case xs of [] => fill # takefill fill n xs |
55 (case xs of |
64 | y # ys => y # takefill fill n ys)" |
56 [] \<Rightarrow> fill # takefill fill n xs |
|
57 | y # ys \<Rightarrow> y # takefill fill n ys)" |
65 |
58 |
66 |
59 |
67 subsection "Arithmetic in terms of bool lists" |
60 subsection "Arithmetic in terms of bool lists" |
68 |
61 |
69 text \<open> |
62 text \<open> |
70 Arithmetic operations in terms of the reversed bool list, |
63 Arithmetic operations in terms of the reversed bool list, |
71 assuming input list(s) the same length, and don't extend them. |
64 assuming input list(s) the same length, and don't extend them. |
72 \<close> |
65 \<close> |
73 |
66 |
74 primrec rbl_succ :: "bool list => bool list" |
67 primrec rbl_succ :: "bool list \<Rightarrow> bool list" |
75 where |
68 where |
76 Nil: "rbl_succ Nil = Nil" |
69 Nil: "rbl_succ Nil = Nil" |
77 | Cons: "rbl_succ (x # xs) = (if x then False # rbl_succ xs else True # xs)" |
70 | Cons: "rbl_succ (x # xs) = (if x then False # rbl_succ xs else True # xs)" |
78 |
71 |
79 primrec rbl_pred :: "bool list => bool list" |
72 primrec rbl_pred :: "bool list \<Rightarrow> bool list" |
80 where |
73 where |
81 Nil: "rbl_pred Nil = Nil" |
74 Nil: "rbl_pred Nil = Nil" |
82 | Cons: "rbl_pred (x # xs) = (if x then False # xs else True # rbl_pred xs)" |
75 | Cons: "rbl_pred (x # xs) = (if x then False # xs else True # rbl_pred xs)" |
83 |
76 |
84 primrec rbl_add :: "bool list => bool list => bool list" |
77 primrec rbl_add :: "bool list \<Rightarrow> bool list \<Rightarrow> bool list" |
85 where |
78 where \<comment> "result is length of first arg, second arg may be longer" |
86 \<comment> "result is length of first arg, second arg may be longer" |
79 Nil: "rbl_add Nil x = Nil" |
87 Nil: "rbl_add Nil x = Nil" |
80 | Cons: "rbl_add (y # ys) x = |
88 | Cons: "rbl_add (y # ys) x = (let ws = rbl_add ys (tl x) in |
81 (let ws = rbl_add ys (tl x) |
89 (y ~= hd x) # (if hd x & y then rbl_succ ws else ws))" |
82 in (y \<noteq> hd x) # (if hd x \<and> y then rbl_succ ws else ws))" |
90 |
83 |
91 primrec rbl_mult :: "bool list => bool list => bool list" |
84 primrec rbl_mult :: "bool list \<Rightarrow> bool list \<Rightarrow> bool list" |
92 where |
85 where \<comment> "result is length of first arg, second arg may be longer" |
93 \<comment> "result is length of first arg, second arg may be longer" |
86 Nil: "rbl_mult Nil x = Nil" |
94 Nil: "rbl_mult Nil x = Nil" |
87 | Cons: "rbl_mult (y # ys) x = |
95 | Cons: "rbl_mult (y # ys) x = (let ws = False # rbl_mult ys x in |
88 (let ws = False # rbl_mult ys x |
96 if y then rbl_add ws x else ws)" |
89 in if y then rbl_add ws x else ws)" |
97 |
90 |
98 lemma butlast_power: |
91 lemma butlast_power: "(butlast ^^ n) bl = take (length bl - n) bl" |
99 "(butlast ^^ n) bl = take (length bl - n) bl" |
|
100 by (induct n) (auto simp: butlast_take) |
92 by (induct n) (auto simp: butlast_take) |
101 |
93 |
102 lemma bin_to_bl_aux_zero_minus_simp [simp]: |
94 lemma bin_to_bl_aux_zero_minus_simp [simp]: |
103 "0 < n \<Longrightarrow> bin_to_bl_aux n 0 bl = |
95 "0 < n \<Longrightarrow> bin_to_bl_aux n 0 bl = bin_to_bl_aux (n - 1) 0 (False # bl)" |
104 bin_to_bl_aux (n - 1) 0 (False # bl)" |
|
105 by (cases n) auto |
96 by (cases n) auto |
106 |
97 |
107 lemma bin_to_bl_aux_minus1_minus_simp [simp]: |
98 lemma bin_to_bl_aux_minus1_minus_simp [simp]: |
108 "0 < n ==> bin_to_bl_aux n (- 1) bl = |
99 "0 < n \<Longrightarrow> bin_to_bl_aux n (- 1) bl = bin_to_bl_aux (n - 1) (- 1) (True # bl)" |
109 bin_to_bl_aux (n - 1) (- 1) (True # bl)" |
|
110 by (cases n) auto |
100 by (cases n) auto |
111 |
101 |
112 lemma bin_to_bl_aux_one_minus_simp [simp]: |
102 lemma bin_to_bl_aux_one_minus_simp [simp]: |
113 "0 < n \<Longrightarrow> bin_to_bl_aux n 1 bl = |
103 "0 < n \<Longrightarrow> bin_to_bl_aux n 1 bl = bin_to_bl_aux (n - 1) 0 (True # bl)" |
114 bin_to_bl_aux (n - 1) 0 (True # bl)" |
|
115 by (cases n) auto |
104 by (cases n) auto |
116 |
105 |
117 lemma bin_to_bl_aux_Bit_minus_simp [simp]: |
106 lemma bin_to_bl_aux_Bit_minus_simp [simp]: |
118 "0 < n ==> bin_to_bl_aux n (w BIT b) bl = |
107 "0 < n \<Longrightarrow> bin_to_bl_aux n (w BIT b) bl = bin_to_bl_aux (n - 1) w (b # bl)" |
119 bin_to_bl_aux (n - 1) w (b # bl)" |
|
120 by (cases n) auto |
108 by (cases n) auto |
121 |
109 |
122 lemma bin_to_bl_aux_Bit0_minus_simp [simp]: |
110 lemma bin_to_bl_aux_Bit0_minus_simp [simp]: |
123 "0 < n ==> bin_to_bl_aux n (numeral (Num.Bit0 w)) bl = |
111 "0 < n \<Longrightarrow> |
124 bin_to_bl_aux (n - 1) (numeral w) (False # bl)" |
112 bin_to_bl_aux n (numeral (Num.Bit0 w)) bl = bin_to_bl_aux (n - 1) (numeral w) (False # bl)" |
125 by (cases n) auto |
113 by (cases n) auto |
126 |
114 |
127 lemma bin_to_bl_aux_Bit1_minus_simp [simp]: |
115 lemma bin_to_bl_aux_Bit1_minus_simp [simp]: |
128 "0 < n ==> bin_to_bl_aux n (numeral (Num.Bit1 w)) bl = |
116 "0 < n \<Longrightarrow> |
129 bin_to_bl_aux (n - 1) (numeral w) (True # bl)" |
117 bin_to_bl_aux n (numeral (Num.Bit1 w)) bl = bin_to_bl_aux (n - 1) (numeral w) (True # bl)" |
130 by (cases n) auto |
118 by (cases n) auto |
131 |
119 |
132 text \<open>Link between bin and bool list.\<close> |
120 text \<open>Link between bin and bool list.\<close> |
133 |
121 |
134 lemma bl_to_bin_aux_append: |
122 lemma bl_to_bin_aux_append: "bl_to_bin_aux (bs @ cs) w = bl_to_bin_aux cs (bl_to_bin_aux bs w)" |
135 "bl_to_bin_aux (bs @ cs) w = bl_to_bin_aux cs (bl_to_bin_aux bs w)" |
|
136 by (induct bs arbitrary: w) auto |
123 by (induct bs arbitrary: w) auto |
137 |
124 |
138 lemma bin_to_bl_aux_append: |
125 lemma bin_to_bl_aux_append: "bin_to_bl_aux n w bs @ cs = bin_to_bl_aux n w (bs @ cs)" |
139 "bin_to_bl_aux n w bs @ cs = bin_to_bl_aux n w (bs @ cs)" |
|
140 by (induct n arbitrary: w bs) auto |
126 by (induct n arbitrary: w bs) auto |
141 |
127 |
142 lemma bl_to_bin_append: |
128 lemma bl_to_bin_append: "bl_to_bin (bs @ cs) = bl_to_bin_aux cs (bl_to_bin bs)" |
143 "bl_to_bin (bs @ cs) = bl_to_bin_aux cs (bl_to_bin bs)" |
|
144 unfolding bl_to_bin_def by (rule bl_to_bin_aux_append) |
129 unfolding bl_to_bin_def by (rule bl_to_bin_aux_append) |
145 |
130 |
146 lemma bin_to_bl_aux_alt: |
131 lemma bin_to_bl_aux_alt: "bin_to_bl_aux n w bs = bin_to_bl n w @ bs" |
147 "bin_to_bl_aux n w bs = bin_to_bl n w @ bs" |
132 by (simp add: bin_to_bl_def bin_to_bl_aux_append) |
148 unfolding bin_to_bl_def by (simp add : bin_to_bl_aux_append) |
|
149 |
133 |
150 lemma bin_to_bl_0 [simp]: "bin_to_bl 0 bs = []" |
134 lemma bin_to_bl_0 [simp]: "bin_to_bl 0 bs = []" |
151 unfolding bin_to_bl_def by auto |
135 by (auto simp: bin_to_bl_def) |
152 |
136 |
153 lemma size_bin_to_bl_aux: |
137 lemma size_bin_to_bl_aux: "size (bin_to_bl_aux n w bs) = n + length bs" |
154 "size (bin_to_bl_aux n w bs) = n + length bs" |
|
155 by (induct n arbitrary: w bs) auto |
138 by (induct n arbitrary: w bs) auto |
156 |
139 |
157 lemma size_bin_to_bl [simp]: "size (bin_to_bl n w) = n" |
140 lemma size_bin_to_bl [simp]: "size (bin_to_bl n w) = n" |
158 unfolding bin_to_bl_def by (simp add : size_bin_to_bl_aux) |
141 by (simp add: bin_to_bl_def size_bin_to_bl_aux) |
159 |
142 |
160 lemma bin_bl_bin': |
143 lemma bin_bl_bin': "bl_to_bin (bin_to_bl_aux n w bs) = bl_to_bin_aux bs (bintrunc n w)" |
161 "bl_to_bin (bin_to_bl_aux n w bs) = |
144 by (induct n arbitrary: w bs) (auto simp: bl_to_bin_def) |
162 bl_to_bin_aux bs (bintrunc n w)" |
|
163 by (induct n arbitrary: w bs) (auto simp add : bl_to_bin_def) |
|
164 |
145 |
165 lemma bin_bl_bin [simp]: "bl_to_bin (bin_to_bl n w) = bintrunc n w" |
146 lemma bin_bl_bin [simp]: "bl_to_bin (bin_to_bl n w) = bintrunc n w" |
166 unfolding bin_to_bl_def bin_bl_bin' by auto |
147 by (auto simp: bin_to_bl_def bin_bl_bin') |
167 |
148 |
168 lemma bl_bin_bl': |
149 lemma bl_bin_bl': "bin_to_bl (n + length bs) (bl_to_bin_aux bs w) = bin_to_bl_aux n w bs" |
169 "bin_to_bl (n + length bs) (bl_to_bin_aux bs w) = |
|
170 bin_to_bl_aux n w bs" |
|
171 apply (induct bs arbitrary: w n) |
150 apply (induct bs arbitrary: w n) |
172 apply auto |
151 apply auto |
173 apply (simp_all only : add_Suc [symmetric]) |
152 apply (simp_all only: add_Suc [symmetric]) |
174 apply (auto simp add : bin_to_bl_def) |
153 apply (auto simp add: bin_to_bl_def) |
175 done |
154 done |
176 |
155 |
177 lemma bl_bin_bl [simp]: "bin_to_bl (length bs) (bl_to_bin bs) = bs" |
156 lemma bl_bin_bl [simp]: "bin_to_bl (length bs) (bl_to_bin bs) = bs" |
178 unfolding bl_to_bin_def |
157 unfolding bl_to_bin_def |
179 apply (rule box_equals) |
158 apply (rule box_equals) |
180 apply (rule bl_bin_bl') |
159 apply (rule bl_bin_bl') |
181 prefer 2 |
160 prefer 2 |
182 apply (rule bin_to_bl_aux.Z) |
161 apply (rule bin_to_bl_aux.Z) |
183 apply simp |
162 apply simp |
184 done |
163 done |
185 |
164 |
186 lemma bl_to_bin_inj: |
165 lemma bl_to_bin_inj: "bl_to_bin bs = bl_to_bin cs \<Longrightarrow> length bs = length cs \<Longrightarrow> bs = cs" |
187 "bl_to_bin bs = bl_to_bin cs ==> length bs = length cs ==> bs = cs" |
|
188 apply (rule_tac box_equals) |
166 apply (rule_tac box_equals) |
189 defer |
167 defer |
190 apply (rule bl_bin_bl) |
168 apply (rule bl_bin_bl) |
191 apply (rule bl_bin_bl) |
169 apply (rule bl_bin_bl) |
192 apply simp |
170 apply simp |
193 done |
171 done |
194 |
172 |
195 lemma bl_to_bin_False [simp]: "bl_to_bin (False # bl) = bl_to_bin bl" |
173 lemma bl_to_bin_False [simp]: "bl_to_bin (False # bl) = bl_to_bin bl" |
196 unfolding bl_to_bin_def by auto |
174 by (auto simp: bl_to_bin_def) |
197 |
175 |
198 lemma bl_to_bin_Nil [simp]: "bl_to_bin [] = 0" |
176 lemma bl_to_bin_Nil [simp]: "bl_to_bin [] = 0" |
199 unfolding bl_to_bin_def by auto |
177 by (auto simp: bl_to_bin_def) |
200 |
178 |
201 lemma bin_to_bl_zero_aux: |
179 lemma bin_to_bl_zero_aux: "bin_to_bl_aux n 0 bl = replicate n False @ bl" |
202 "bin_to_bl_aux n 0 bl = replicate n False @ bl" |
|
203 by (induct n arbitrary: bl) (auto simp: replicate_app_Cons_same) |
180 by (induct n arbitrary: bl) (auto simp: replicate_app_Cons_same) |
204 |
181 |
205 lemma bin_to_bl_zero: "bin_to_bl n 0 = replicate n False" |
182 lemma bin_to_bl_zero: "bin_to_bl n 0 = replicate n False" |
206 unfolding bin_to_bl_def by (simp add: bin_to_bl_zero_aux) |
183 by (simp add: bin_to_bl_def bin_to_bl_zero_aux) |
207 |
184 |
208 lemma bin_to_bl_minus1_aux: |
185 lemma bin_to_bl_minus1_aux: "bin_to_bl_aux n (- 1) bl = replicate n True @ bl" |
209 "bin_to_bl_aux n (- 1) bl = replicate n True @ bl" |
|
210 by (induct n arbitrary: bl) (auto simp: replicate_app_Cons_same) |
186 by (induct n arbitrary: bl) (auto simp: replicate_app_Cons_same) |
211 |
187 |
212 lemma bin_to_bl_minus1: "bin_to_bl n (- 1) = replicate n True" |
188 lemma bin_to_bl_minus1: "bin_to_bl n (- 1) = replicate n True" |
213 unfolding bin_to_bl_def by (simp add: bin_to_bl_minus1_aux) |
189 by (simp add: bin_to_bl_def bin_to_bl_minus1_aux) |
214 |
190 |
215 lemma bl_to_bin_rep_F: |
191 lemma bl_to_bin_rep_F: "bl_to_bin (replicate n False @ bl) = bl_to_bin bl" |
216 "bl_to_bin (replicate n False @ bl) = bl_to_bin bl" |
192 by (simp add: bin_to_bl_zero_aux [symmetric] bin_bl_bin') (simp add: bl_to_bin_def) |
217 apply (simp add: bin_to_bl_zero_aux [symmetric] bin_bl_bin') |
193 |
218 apply (simp add: bl_to_bin_def) |
194 lemma bin_to_bl_trunc [simp]: "n \<le> m \<Longrightarrow> bin_to_bl n (bintrunc m w) = bin_to_bl n w" |
219 done |
|
220 |
|
221 lemma bin_to_bl_trunc [simp]: |
|
222 "n <= m ==> bin_to_bl n (bintrunc m w) = bin_to_bl n w" |
|
223 by (auto intro: bl_to_bin_inj) |
195 by (auto intro: bl_to_bin_inj) |
224 |
196 |
225 lemma bin_to_bl_aux_bintr: |
197 lemma bin_to_bl_aux_bintr: |
226 "bin_to_bl_aux n (bintrunc m bin) bl = |
198 "bin_to_bl_aux n (bintrunc m bin) bl = |
227 replicate (n - m) False @ bin_to_bl_aux (min n m) bin bl" |
199 replicate (n - m) False @ bin_to_bl_aux (min n m) bin bl" |
228 apply (induct n arbitrary: m bin bl) |
200 apply (induct n arbitrary: m bin bl) |
229 apply clarsimp |
201 apply clarsimp |
230 apply clarsimp |
202 apply clarsimp |
231 apply (case_tac "m") |
203 apply (case_tac "m") |
232 apply (clarsimp simp: bin_to_bl_zero_aux) |
204 apply (clarsimp simp: bin_to_bl_zero_aux) |
233 apply (erule thin_rl) |
205 apply (erule thin_rl) |
234 apply (induct_tac n) |
206 apply (induct_tac n) |
235 apply auto |
207 apply auto |
236 done |
208 done |
237 |
209 |
238 lemma bin_to_bl_bintr: |
210 lemma bin_to_bl_bintr: |
239 "bin_to_bl n (bintrunc m bin) = |
211 "bin_to_bl n (bintrunc m bin) = replicate (n - m) False @ bin_to_bl (min n m) bin" |
240 replicate (n - m) False @ bin_to_bl (min n m) bin" |
|
241 unfolding bin_to_bl_def by (rule bin_to_bl_aux_bintr) |
212 unfolding bin_to_bl_def by (rule bin_to_bl_aux_bintr) |
242 |
213 |
243 lemma bl_to_bin_rep_False: "bl_to_bin (replicate n False) = 0" |
214 lemma bl_to_bin_rep_False: "bl_to_bin (replicate n False) = 0" |
244 by (induct n) auto |
215 by (induct n) auto |
245 |
216 |
246 lemma len_bin_to_bl_aux: |
217 lemma len_bin_to_bl_aux: "length (bin_to_bl_aux n w bs) = n + length bs" |
247 "length (bin_to_bl_aux n w bs) = n + length bs" |
|
248 by (fact size_bin_to_bl_aux) |
218 by (fact size_bin_to_bl_aux) |
249 |
219 |
250 lemma len_bin_to_bl [simp]: "length (bin_to_bl n w) = n" |
220 lemma len_bin_to_bl: "length (bin_to_bl n w) = n" |
251 by (fact size_bin_to_bl) (* FIXME: duplicate *) |
221 by (fact size_bin_to_bl) (* FIXME: duplicate *) |
252 |
222 |
253 lemma sign_bl_bin': |
223 lemma sign_bl_bin': "bin_sign (bl_to_bin_aux bs w) = bin_sign w" |
254 "bin_sign (bl_to_bin_aux bs w) = bin_sign w" |
|
255 by (induct bs arbitrary: w) auto |
224 by (induct bs arbitrary: w) auto |
256 |
225 |
257 lemma sign_bl_bin: "bin_sign (bl_to_bin bs) = 0" |
226 lemma sign_bl_bin: "bin_sign (bl_to_bin bs) = 0" |
258 unfolding bl_to_bin_def by (simp add : sign_bl_bin') |
227 by (simp add: bl_to_bin_def sign_bl_bin') |
259 |
228 |
260 lemma bl_sbin_sign_aux: |
229 lemma bl_sbin_sign_aux: "hd (bin_to_bl_aux (Suc n) w bs) = (bin_sign (sbintrunc n w) = -1)" |
261 "hd (bin_to_bl_aux (Suc n) w bs) = |
|
262 (bin_sign (sbintrunc n w) = -1)" |
|
263 apply (induct n arbitrary: w bs) |
230 apply (induct n arbitrary: w bs) |
264 apply clarsimp |
231 apply clarsimp |
265 apply (cases w rule: bin_exhaust) |
232 apply (cases w rule: bin_exhaust) |
266 apply simp |
233 apply simp |
267 done |
234 done |
268 |
235 |
269 lemma bl_sbin_sign: |
236 lemma bl_sbin_sign: "hd (bin_to_bl (Suc n) w) = (bin_sign (sbintrunc n w) = -1)" |
270 "hd (bin_to_bl (Suc n) w) = (bin_sign (sbintrunc n w) = -1)" |
|
271 unfolding bin_to_bl_def by (rule bl_sbin_sign_aux) |
237 unfolding bin_to_bl_def by (rule bl_sbin_sign_aux) |
272 |
238 |
273 lemma bin_nth_of_bl_aux: |
239 lemma bin_nth_of_bl_aux: |
274 "bin_nth (bl_to_bin_aux bl w) n = |
240 "bin_nth (bl_to_bin_aux bl w) n = |
275 (n < size bl & rev bl ! n | n >= length bl & bin_nth w (n - size bl))" |
241 (n < size bl \<and> rev bl ! n | n \<ge> length bl \<and> bin_nth w (n - size bl))" |
276 apply (induct bl arbitrary: w) |
242 apply (induct bl arbitrary: w) |
277 apply clarsimp |
243 apply clarsimp |
278 apply clarsimp |
244 apply clarsimp |
279 apply (cut_tac x=n and y="size bl" in linorder_less_linear) |
245 apply (cut_tac x=n and y="size bl" in linorder_less_linear) |
280 apply (erule disjE, simp add: nth_append)+ |
246 apply (erule disjE, simp add: nth_append)+ |
281 apply auto |
247 apply auto |
282 done |
248 done |
283 |
249 |
284 lemma bin_nth_of_bl: "bin_nth (bl_to_bin bl) n = (n < length bl & rev bl ! n)" |
250 lemma bin_nth_of_bl: "bin_nth (bl_to_bin bl) n = (n < length bl \<and> rev bl ! n)" |
285 unfolding bl_to_bin_def by (simp add : bin_nth_of_bl_aux) |
251 by (simp add: bl_to_bin_def bin_nth_of_bl_aux) |
286 |
252 |
287 lemma bin_nth_bl: "n < m \<Longrightarrow> bin_nth w n = nth (rev (bin_to_bl m w)) n" |
253 lemma bin_nth_bl: "n < m \<Longrightarrow> bin_nth w n = nth (rev (bin_to_bl m w)) n" |
288 apply (induct n arbitrary: m w) |
254 apply (induct n arbitrary: m w) |
289 apply clarsimp |
255 apply clarsimp |
290 apply (case_tac m, clarsimp) |
256 apply (case_tac m, clarsimp) |
294 apply (case_tac m, clarsimp) |
260 apply (case_tac m, clarsimp) |
295 apply (clarsimp simp: bin_to_bl_def) |
261 apply (clarsimp simp: bin_to_bl_def) |
296 apply (simp add: bin_to_bl_aux_alt) |
262 apply (simp add: bin_to_bl_aux_alt) |
297 done |
263 done |
298 |
264 |
299 lemma nth_rev: |
265 lemma nth_rev: "n < length xs \<Longrightarrow> rev xs ! n = xs ! (length xs - 1 - n)" |
300 "n < length xs \<Longrightarrow> rev xs ! n = xs ! (length xs - 1 - n)" |
|
301 apply (induct xs) |
266 apply (induct xs) |
302 apply simp |
267 apply simp |
303 apply (clarsimp simp add : nth_append nth.simps split: nat.split) |
268 apply (clarsimp simp add: nth_append nth.simps split: nat.split) |
304 apply (rule_tac f = "\<lambda>n. xs ! n" in arg_cong) |
269 apply (rule_tac f = "\<lambda>n. xs ! n" in arg_cong) |
305 apply arith |
270 apply arith |
306 done |
271 done |
307 |
272 |
308 lemma nth_rev_alt: "n < length ys \<Longrightarrow> ys ! n = rev ys ! (length ys - Suc n)" |
273 lemma nth_rev_alt: "n < length ys \<Longrightarrow> ys ! n = rev ys ! (length ys - Suc n)" |
309 by (simp add: nth_rev) |
274 by (simp add: nth_rev) |
310 |
275 |
311 lemma nth_bin_to_bl_aux: |
276 lemma nth_bin_to_bl_aux: |
312 "n < m + length bl \<Longrightarrow> (bin_to_bl_aux m w bl) ! n = |
277 "n < m + length bl \<Longrightarrow> (bin_to_bl_aux m w bl) ! n = |
313 (if n < m then bin_nth w (m - 1 - n) else bl ! (n - m))" |
278 (if n < m then bin_nth w (m - 1 - n) else bl ! (n - m))" |
314 apply (induct m arbitrary: w n bl) |
279 apply (induct m arbitrary: w n bl) |
315 apply clarsimp |
280 apply clarsimp |
316 apply clarsimp |
281 apply clarsimp |
317 apply (case_tac w rule: bin_exhaust) |
282 apply (case_tac w rule: bin_exhaust) |
318 apply simp |
283 apply simp |
319 done |
284 done |
320 |
285 |
321 lemma nth_bin_to_bl: "n < m ==> (bin_to_bl m w) ! n = bin_nth w (m - Suc n)" |
286 lemma nth_bin_to_bl: "n < m \<Longrightarrow> (bin_to_bl m w) ! n = bin_nth w (m - Suc n)" |
322 unfolding bin_to_bl_def by (simp add : nth_bin_to_bl_aux) |
287 by (simp add: bin_to_bl_def nth_bin_to_bl_aux) |
323 |
288 |
324 lemma bl_to_bin_lt2p_aux: |
289 lemma bl_to_bin_lt2p_aux: "bl_to_bin_aux bs w < (w + 1) * (2 ^ length bs)" |
325 "bl_to_bin_aux bs w < (w + 1) * (2 ^ length bs)" |
|
326 apply (induct bs arbitrary: w) |
290 apply (induct bs arbitrary: w) |
327 apply clarsimp |
291 apply clarsimp |
328 apply clarsimp |
292 apply clarsimp |
329 apply (drule meta_spec, erule xtrans(8) [rotated], simp add: Bit_def)+ |
293 apply (drule meta_spec, erule xtrans(8) [rotated], simp add: Bit_def)+ |
330 done |
294 done |
331 |
295 |
332 lemma bl_to_bin_lt2p_drop: |
296 lemma bl_to_bin_lt2p_drop: "bl_to_bin bs < 2 ^ length (dropWhile Not bs)" |
333 "bl_to_bin bs < 2 ^ length (dropWhile Not bs)" |
|
334 proof (induct bs) |
297 proof (induct bs) |
|
298 case Nil |
|
299 then show ?case by simp |
|
300 next |
335 case (Cons b bs) with bl_to_bin_lt2p_aux[where w=1] |
301 case (Cons b bs) with bl_to_bin_lt2p_aux[where w=1] |
336 show ?case unfolding bl_to_bin_def by simp |
302 show ?case unfolding bl_to_bin_def by simp |
337 qed simp |
303 qed |
338 |
304 |
339 lemma bl_to_bin_lt2p: "bl_to_bin bs < 2 ^ length bs" |
305 lemma bl_to_bin_lt2p: "bl_to_bin bs < 2 ^ length bs" |
340 by (metis bin_bl_bin bintr_lt2p bl_bin_bl) |
306 by (metis bin_bl_bin bintr_lt2p bl_bin_bl) |
341 |
307 |
342 lemma bl_to_bin_ge2p_aux: |
308 lemma bl_to_bin_ge2p_aux: "bl_to_bin_aux bs w \<ge> w * (2 ^ length bs)" |
343 "bl_to_bin_aux bs w >= w * (2 ^ length bs)" |
|
344 apply (induct bs arbitrary: w) |
309 apply (induct bs arbitrary: w) |
345 apply clarsimp |
310 apply clarsimp |
346 apply clarsimp |
311 apply clarsimp |
347 apply (drule meta_spec, erule order_trans [rotated], |
312 apply (drule meta_spec, erule order_trans [rotated], |
348 simp add: Bit_B0_2t Bit_B1_2t algebra_simps)+ |
313 simp add: Bit_B0_2t Bit_B1_2t algebra_simps)+ |
349 apply (simp add: Bit_def) |
314 apply (simp add: Bit_def) |
350 done |
315 done |
351 |
316 |
352 lemma bl_to_bin_ge0: "bl_to_bin bs >= 0" |
317 lemma bl_to_bin_ge0: "bl_to_bin bs \<ge> 0" |
353 apply (unfold bl_to_bin_def) |
318 apply (unfold bl_to_bin_def) |
354 apply (rule xtrans(4)) |
319 apply (rule xtrans(4)) |
355 apply (rule bl_to_bin_ge2p_aux) |
320 apply (rule bl_to_bin_ge2p_aux) |
356 apply simp |
321 apply simp |
357 done |
322 done |
358 |
323 |
359 lemma butlast_rest_bin: |
324 lemma butlast_rest_bin: "butlast (bin_to_bl n w) = bin_to_bl (n - 1) (bin_rest w)" |
360 "butlast (bin_to_bl n w) = bin_to_bl (n - 1) (bin_rest w)" |
|
361 apply (unfold bin_to_bl_def) |
325 apply (unfold bin_to_bl_def) |
362 apply (cases w rule: bin_exhaust) |
326 apply (cases w rule: bin_exhaust) |
363 apply (cases n, clarsimp) |
327 apply (cases n, clarsimp) |
364 apply clarsimp |
328 apply clarsimp |
365 apply (auto simp add: bin_to_bl_aux_alt) |
329 apply (auto simp add: bin_to_bl_aux_alt) |
366 done |
330 done |
367 |
331 |
368 lemma butlast_bin_rest: |
332 lemma butlast_bin_rest: "butlast bl = bin_to_bl (length bl - Suc 0) (bin_rest (bl_to_bin bl))" |
369 "butlast bl = bin_to_bl (length bl - Suc 0) (bin_rest (bl_to_bin bl))" |
|
370 using butlast_rest_bin [where w="bl_to_bin bl" and n="length bl"] by simp |
333 using butlast_rest_bin [where w="bl_to_bin bl" and n="length bl"] by simp |
371 |
334 |
372 lemma butlast_rest_bl2bin_aux: |
335 lemma butlast_rest_bl2bin_aux: |
373 "bl ~= [] \<Longrightarrow> |
336 "bl \<noteq> [] \<Longrightarrow> bl_to_bin_aux (butlast bl) w = bin_rest (bl_to_bin_aux bl w)" |
374 bl_to_bin_aux (butlast bl) w = bin_rest (bl_to_bin_aux bl w)" |
|
375 by (induct bl arbitrary: w) auto |
337 by (induct bl arbitrary: w) auto |
376 |
338 |
377 lemma butlast_rest_bl2bin: |
339 lemma butlast_rest_bl2bin: "bl_to_bin (butlast bl) = bin_rest (bl_to_bin bl)" |
378 "bl_to_bin (butlast bl) = bin_rest (bl_to_bin bl)" |
340 by (cases bl) (auto simp: bl_to_bin_def butlast_rest_bl2bin_aux) |
379 apply (unfold bl_to_bin_def) |
|
380 apply (cases bl) |
|
381 apply (auto simp add: butlast_rest_bl2bin_aux) |
|
382 done |
|
383 |
341 |
384 lemma trunc_bl2bin_aux: |
342 lemma trunc_bl2bin_aux: |
385 "bintrunc m (bl_to_bin_aux bl w) = |
343 "bintrunc m (bl_to_bin_aux bl w) = |
386 bl_to_bin_aux (drop (length bl - m) bl) (bintrunc (m - length bl) w)" |
344 bl_to_bin_aux (drop (length bl - m) bl) (bintrunc (m - length bl) w)" |
387 proof (induct bl arbitrary: w) |
345 proof (induct bl arbitrary: w) |
388 case Nil show ?case by simp |
346 case Nil |
|
347 show ?case by simp |
389 next |
348 next |
390 case (Cons b bl) show ?case |
349 case (Cons b bl) |
|
350 show ?case |
391 proof (cases "m - length bl") |
351 proof (cases "m - length bl") |
392 case 0 then have "Suc (length bl) - m = Suc (length bl - m)" by simp |
352 case 0 |
|
353 then have "Suc (length bl) - m = Suc (length bl - m)" by simp |
393 with Cons show ?thesis by simp |
354 with Cons show ?thesis by simp |
394 next |
355 next |
395 case (Suc n) then have *: "m - Suc (length bl) = n" by simp |
356 case (Suc n) |
396 with Suc Cons show ?thesis by simp |
357 then have "m - Suc (length bl) = n" by simp |
|
358 with Cons Suc show ?thesis by simp |
397 qed |
359 qed |
398 qed |
360 qed |
399 |
361 |
400 lemma trunc_bl2bin: |
362 lemma trunc_bl2bin: "bintrunc m (bl_to_bin bl) = bl_to_bin (drop (length bl - m) bl)" |
401 "bintrunc m (bl_to_bin bl) = bl_to_bin (drop (length bl - m) bl)" |
363 by (simp add: bl_to_bin_def trunc_bl2bin_aux) |
402 unfolding bl_to_bin_def by (simp add : trunc_bl2bin_aux) |
364 |
403 |
365 lemma trunc_bl2bin_len [simp]: "bintrunc (length bl) (bl_to_bin bl) = bl_to_bin bl" |
404 lemma trunc_bl2bin_len [simp]: |
|
405 "bintrunc (length bl) (bl_to_bin bl) = bl_to_bin bl" |
|
406 by (simp add: trunc_bl2bin) |
366 by (simp add: trunc_bl2bin) |
407 |
367 |
408 lemma bl2bin_drop: |
368 lemma bl2bin_drop: "bl_to_bin (drop k bl) = bintrunc (length bl - k) (bl_to_bin bl)" |
409 "bl_to_bin (drop k bl) = bintrunc (length bl - k) (bl_to_bin bl)" |
|
410 apply (rule trans) |
369 apply (rule trans) |
411 prefer 2 |
370 prefer 2 |
412 apply (rule trunc_bl2bin [symmetric]) |
371 apply (rule trunc_bl2bin [symmetric]) |
413 apply (cases "k <= length bl") |
372 apply (cases "k \<le> length bl") |
414 apply auto |
373 apply auto |
415 done |
374 done |
416 |
375 |
417 lemma nth_rest_power_bin: |
376 lemma nth_rest_power_bin: "bin_nth ((bin_rest ^^ k) w) n = bin_nth w (n + k)" |
418 "bin_nth ((bin_rest ^^ k) w) n = bin_nth w (n + k)" |
377 apply (induct k arbitrary: n) |
419 apply (induct k arbitrary: n, clarsimp) |
378 apply clarsimp |
420 apply clarsimp |
379 apply clarsimp |
421 apply (simp only: bin_nth.Suc [symmetric] add_Suc) |
380 apply (simp only: bin_nth.Suc [symmetric] add_Suc) |
422 done |
381 done |
423 |
382 |
424 lemma take_rest_power_bin: |
383 lemma take_rest_power_bin: "m \<le> n \<Longrightarrow> take m (bin_to_bl n w) = bin_to_bl m ((bin_rest ^^ (n - m)) w)" |
425 "m <= n ==> take m (bin_to_bl n w) = bin_to_bl m ((bin_rest ^^ (n - m)) w)" |
|
426 apply (rule nth_equalityI) |
384 apply (rule nth_equalityI) |
427 apply simp |
385 apply simp |
428 apply (clarsimp simp add: nth_bin_to_bl nth_rest_power_bin) |
386 apply (clarsimp simp add: nth_bin_to_bl nth_rest_power_bin) |
429 done |
387 done |
430 |
388 |
431 lemma hd_butlast: "size xs > 1 ==> hd (butlast xs) = hd xs" |
389 lemma hd_butlast: "size xs > 1 \<Longrightarrow> hd (butlast xs) = hd xs" |
432 by (cases xs) auto |
390 by (cases xs) auto |
433 |
391 |
434 lemma last_bin_last': |
392 lemma last_bin_last': "size xs > 0 \<Longrightarrow> last xs \<longleftrightarrow> bin_last (bl_to_bin_aux xs w)" |
435 "size xs > 0 \<Longrightarrow> last xs \<longleftrightarrow> bin_last (bl_to_bin_aux xs w)" |
|
436 by (induct xs arbitrary: w) auto |
393 by (induct xs arbitrary: w) auto |
437 |
394 |
438 lemma last_bin_last: |
395 lemma last_bin_last: "size xs > 0 \<Longrightarrow> last xs \<longleftrightarrow> bin_last (bl_to_bin xs)" |
439 "size xs > 0 ==> last xs \<longleftrightarrow> bin_last (bl_to_bin xs)" |
|
440 unfolding bl_to_bin_def by (erule last_bin_last') |
396 unfolding bl_to_bin_def by (erule last_bin_last') |
441 |
397 |
442 lemma bin_last_last: |
398 lemma bin_last_last: "bin_last w \<longleftrightarrow> last (bin_to_bl (Suc n) w)" |
443 "bin_last w \<longleftrightarrow> last (bin_to_bl (Suc n) w)" |
399 by (simp add: bin_to_bl_def) (auto simp: bin_to_bl_aux_alt) |
444 apply (unfold bin_to_bl_def) |
400 |
445 apply simp |
401 |
446 apply (auto simp add: bin_to_bl_aux_alt) |
402 subsection \<open>Links between bit-wise operations and operations on bool lists\<close> |
447 done |
403 |
448 |
|
449 (** links between bit-wise operations and operations on bool lists **) |
|
450 |
|
451 lemma bl_xor_aux_bin: |
404 lemma bl_xor_aux_bin: |
452 "map2 (%x y. x ~= y) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) = |
405 "map2 (\<lambda>x y. x \<noteq> y) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) = |
453 bin_to_bl_aux n (v XOR w) (map2 (%x y. x ~= y) bs cs)" |
406 bin_to_bl_aux n (v XOR w) (map2 (\<lambda>x y. x \<noteq> y) bs cs)" |
454 apply (induct n arbitrary: v w bs cs) |
407 apply (induct n arbitrary: v w bs cs) |
455 apply simp |
408 apply simp |
456 apply (case_tac v rule: bin_exhaust) |
409 apply (case_tac v rule: bin_exhaust) |
457 apply (case_tac w rule: bin_exhaust) |
410 apply (case_tac w rule: bin_exhaust) |
458 apply clarsimp |
411 apply clarsimp |
459 apply (case_tac b) |
412 apply (case_tac b) |
460 apply auto |
413 apply auto |
461 done |
414 done |
462 |
415 |
463 lemma bl_or_aux_bin: |
416 lemma bl_or_aux_bin: |
464 "map2 (op | ) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) = |
417 "map2 (op \<or>) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) = |
465 bin_to_bl_aux n (v OR w) (map2 (op | ) bs cs)" |
418 bin_to_bl_aux n (v OR w) (map2 (op \<or>) bs cs)" |
466 apply (induct n arbitrary: v w bs cs) |
419 apply (induct n arbitrary: v w bs cs) |
467 apply simp |
420 apply simp |
468 apply (case_tac v rule: bin_exhaust) |
421 apply (case_tac v rule: bin_exhaust) |
469 apply (case_tac w rule: bin_exhaust) |
422 apply (case_tac w rule: bin_exhaust) |
470 apply clarsimp |
423 apply clarsimp |
471 done |
424 done |
472 |
425 |
473 lemma bl_and_aux_bin: |
426 lemma bl_and_aux_bin: |
474 "map2 (op & ) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) = |
427 "map2 (op \<and>) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) = |
475 bin_to_bl_aux n (v AND w) (map2 (op & ) bs cs)" |
428 bin_to_bl_aux n (v AND w) (map2 (op \<and>) bs cs)" |
476 apply (induct n arbitrary: v w bs cs) |
429 apply (induct n arbitrary: v w bs cs) |
477 apply simp |
430 apply simp |
478 apply (case_tac v rule: bin_exhaust) |
431 apply (case_tac v rule: bin_exhaust) |
479 apply (case_tac w rule: bin_exhaust) |
432 apply (case_tac w rule: bin_exhaust) |
480 apply clarsimp |
433 apply clarsimp |
481 done |
434 done |
482 |
435 |
483 lemma bl_not_aux_bin: |
436 lemma bl_not_aux_bin: "map Not (bin_to_bl_aux n w cs) = bin_to_bl_aux n (NOT w) (map Not cs)" |
484 "map Not (bin_to_bl_aux n w cs) = |
437 by (induct n arbitrary: w cs) auto |
485 bin_to_bl_aux n (NOT w) (map Not cs)" |
|
486 apply (induct n arbitrary: w cs) |
|
487 apply clarsimp |
|
488 apply clarsimp |
|
489 done |
|
490 |
438 |
491 lemma bl_not_bin: "map Not (bin_to_bl n w) = bin_to_bl n (NOT w)" |
439 lemma bl_not_bin: "map Not (bin_to_bl n w) = bin_to_bl n (NOT w)" |
492 unfolding bin_to_bl_def by (simp add: bl_not_aux_bin) |
440 by (simp add: bin_to_bl_def bl_not_aux_bin) |
493 |
441 |
494 lemma bl_and_bin: |
442 lemma bl_and_bin: "map2 (op \<and>) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v AND w)" |
495 "map2 (op \<and>) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v AND w)" |
443 by (simp add: bin_to_bl_def bl_and_aux_bin) |
496 unfolding bin_to_bl_def by (simp add: bl_and_aux_bin) |
444 |
497 |
445 lemma bl_or_bin: "map2 (op \<or>) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v OR w)" |
498 lemma bl_or_bin: |
446 by (simp add: bin_to_bl_def bl_or_aux_bin) |
499 "map2 (op \<or>) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v OR w)" |
447 |
500 unfolding bin_to_bl_def by (simp add: bl_or_aux_bin) |
448 lemma bl_xor_bin: "map2 (\<lambda>x y. x \<noteq> y) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v XOR w)" |
501 |
449 by (simp only: bin_to_bl_def bl_xor_aux_bin map2_Nil) |
502 lemma bl_xor_bin: |
|
503 "map2 (\<lambda>x y. x \<noteq> y) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v XOR w)" |
|
504 unfolding bin_to_bl_def by (simp only: bl_xor_aux_bin map2_Nil) |
|
505 |
450 |
506 lemma drop_bin2bl_aux: |
451 lemma drop_bin2bl_aux: |
507 "drop m (bin_to_bl_aux n bin bs) = |
452 "drop m (bin_to_bl_aux n bin bs) = |
508 bin_to_bl_aux (n - m) bin (drop (m - n) bs)" |
453 bin_to_bl_aux (n - m) bin (drop (m - n) bs)" |
509 apply (induct n arbitrary: m bin bs, clarsimp) |
454 apply (induct n arbitrary: m bin bs, clarsimp) |
510 apply clarsimp |
455 apply clarsimp |
511 apply (case_tac bin rule: bin_exhaust) |
456 apply (case_tac bin rule: bin_exhaust) |
512 apply (case_tac "m <= n", simp) |
457 apply (case_tac "m \<le> n", simp) |
513 apply (case_tac "m - n", simp) |
458 apply (case_tac "m - n", simp) |
514 apply simp |
459 apply simp |
515 apply (rule_tac f = "%nat. drop nat bs" in arg_cong) |
460 apply (rule_tac f = "\<lambda>nat. drop nat bs" in arg_cong) |
516 apply simp |
461 apply simp |
517 done |
462 done |
518 |
463 |
519 lemma drop_bin2bl: "drop m (bin_to_bl n bin) = bin_to_bl (n - m) bin" |
464 lemma drop_bin2bl: "drop m (bin_to_bl n bin) = bin_to_bl (n - m) bin" |
520 unfolding bin_to_bl_def by (simp add : drop_bin2bl_aux) |
465 by (simp add: bin_to_bl_def drop_bin2bl_aux) |
521 |
466 |
522 lemma take_bin2bl_lem1: |
467 lemma take_bin2bl_lem1: "take m (bin_to_bl_aux m w bs) = bin_to_bl m w" |
523 "take m (bin_to_bl_aux m w bs) = bin_to_bl m w" |
468 apply (induct m arbitrary: w bs) |
524 apply (induct m arbitrary: w bs, clarsimp) |
469 apply clarsimp |
525 apply clarsimp |
470 apply clarsimp |
526 apply (simp add: bin_to_bl_aux_alt) |
471 apply (simp add: bin_to_bl_aux_alt) |
527 apply (simp add: bin_to_bl_def) |
472 apply (simp add: bin_to_bl_def) |
528 apply (simp add: bin_to_bl_aux_alt) |
473 apply (simp add: bin_to_bl_aux_alt) |
529 done |
474 done |
530 |
475 |
531 lemma take_bin2bl_lem: |
476 lemma take_bin2bl_lem: "take m (bin_to_bl_aux (m + n) w bs) = take m (bin_to_bl (m + n) w)" |
532 "take m (bin_to_bl_aux (m + n) w bs) = |
477 by (induct n arbitrary: w bs) (simp_all (no_asm) add: bin_to_bl_def take_bin2bl_lem1, simp) |
533 take m (bin_to_bl (m + n) w)" |
478 |
534 apply (induct n arbitrary: w bs) |
479 lemma bin_split_take: "bin_split n c = (a, b) \<Longrightarrow> bin_to_bl m a = take m (bin_to_bl (m + n) c)" |
535 apply (simp_all (no_asm) add: bin_to_bl_def take_bin2bl_lem1) |
|
536 apply simp |
|
537 done |
|
538 |
|
539 lemma bin_split_take: |
|
540 "bin_split n c = (a, b) \<Longrightarrow> |
|
541 bin_to_bl m a = take m (bin_to_bl (m + n) c)" |
|
542 apply (induct n arbitrary: b c) |
480 apply (induct n arbitrary: b c) |
543 apply clarsimp |
481 apply clarsimp |
544 apply (clarsimp simp: Let_def split: prod.split_asm) |
482 apply (clarsimp simp: Let_def split: prod.split_asm) |
545 apply (simp add: bin_to_bl_def) |
483 apply (simp add: bin_to_bl_def) |
546 apply (simp add: take_bin2bl_lem) |
484 apply (simp add: take_bin2bl_lem) |
547 done |
485 done |
548 |
486 |
549 lemma bin_split_take1: |
487 lemma bin_split_take1: |
550 "k = m + n ==> bin_split n c = (a, b) ==> |
488 "k = m + n \<Longrightarrow> bin_split n c = (a, b) \<Longrightarrow> bin_to_bl m a = take m (bin_to_bl k c)" |
551 bin_to_bl m a = take m (bin_to_bl k c)" |
|
552 by (auto elim: bin_split_take) |
489 by (auto elim: bin_split_take) |
553 |
490 |
554 lemma nth_takefill: "m < n \<Longrightarrow> |
491 lemma nth_takefill: "m < n \<Longrightarrow> takefill fill n l ! m = (if m < length l then l ! m else fill)" |
555 takefill fill n l ! m = (if m < length l then l ! m else fill)" |
492 apply (induct n arbitrary: m l) |
556 apply (induct n arbitrary: m l, clarsimp) |
493 apply clarsimp |
557 apply clarsimp |
494 apply clarsimp |
558 apply (case_tac m) |
495 apply (case_tac m) |
559 apply (simp split: list.split) |
496 apply (simp split: list.split) |
560 apply (simp split: list.split) |
497 apply (simp split: list.split) |
561 done |
498 done |
562 |
499 |
563 lemma takefill_alt: |
500 lemma takefill_alt: "takefill fill n l = take n l @ replicate (n - length l) fill" |
564 "takefill fill n l = take n l @ replicate (n - length l) fill" |
|
565 by (induct n arbitrary: l) (auto split: list.split) |
501 by (induct n arbitrary: l) (auto split: list.split) |
566 |
502 |
567 lemma takefill_replicate [simp]: |
503 lemma takefill_replicate [simp]: "takefill fill n (replicate m fill) = replicate n fill" |
568 "takefill fill n (replicate m fill) = replicate n fill" |
504 by (simp add: takefill_alt replicate_add [symmetric]) |
569 by (simp add : takefill_alt replicate_add [symmetric]) |
505 |
570 |
506 lemma takefill_le': "n = m + k \<Longrightarrow> takefill x m (takefill x n l) = takefill x m l" |
571 lemma takefill_le': |
|
572 "n = m + k \<Longrightarrow> takefill x m (takefill x n l) = takefill x m l" |
|
573 by (induct m arbitrary: l n) (auto split: list.split) |
507 by (induct m arbitrary: l n) (auto split: list.split) |
574 |
508 |
575 lemma length_takefill [simp]: "length (takefill fill n l) = n" |
509 lemma length_takefill [simp]: "length (takefill fill n l) = n" |
576 by (simp add : takefill_alt) |
510 by (simp add: takefill_alt) |
577 |
511 |
578 lemma take_takefill': |
512 lemma take_takefill': "\<And>w n. n = k + m \<Longrightarrow> take k (takefill fill n w) = takefill fill k w" |
579 "!!w n. n = k + m ==> take k (takefill fill n w) = takefill fill k w" |
513 by (induct k) (auto split: list.split) |
580 by (induct k) (auto split: list.split) |
514 |
581 |
515 lemma drop_takefill: "\<And>w. drop k (takefill fill (m + k) w) = takefill fill m (drop k w)" |
582 lemma drop_takefill: |
516 by (induct k) (auto split: list.split) |
583 "!!w. drop k (takefill fill (m + k) w) = takefill fill m (drop k w)" |
517 |
584 by (induct k) (auto split: list.split) |
518 lemma takefill_le [simp]: "m \<le> n \<Longrightarrow> takefill x m (takefill x n l) = takefill x m l" |
585 |
|
586 lemma takefill_le [simp]: |
|
587 "m \<le> n \<Longrightarrow> takefill x m (takefill x n l) = takefill x m l" |
|
588 by (auto simp: le_iff_add takefill_le') |
519 by (auto simp: le_iff_add takefill_le') |
589 |
520 |
590 lemma take_takefill [simp]: |
521 lemma take_takefill [simp]: "m \<le> n \<Longrightarrow> take m (takefill fill n w) = takefill fill m w" |
591 "m \<le> n \<Longrightarrow> take m (takefill fill n w) = takefill fill m w" |
|
592 by (auto simp: le_iff_add take_takefill') |
522 by (auto simp: le_iff_add take_takefill') |
593 |
523 |
594 lemma takefill_append: |
524 lemma takefill_append: "takefill fill (m + length xs) (xs @ w) = xs @ (takefill fill m w)" |
595 "takefill fill (m + length xs) (xs @ w) = xs @ (takefill fill m w)" |
|
596 by (induct xs) auto |
525 by (induct xs) auto |
597 |
526 |
598 lemma takefill_same': |
527 lemma takefill_same': "l = length xs \<Longrightarrow> takefill fill l xs = xs" |
599 "l = length xs ==> takefill fill l xs = xs" |
528 by (induct xs arbitrary: l) auto |
600 by (induct xs arbitrary: l, auto) |
529 |
601 |
|
602 lemmas takefill_same [simp] = takefill_same' [OF refl] |
530 lemmas takefill_same [simp] = takefill_same' [OF refl] |
603 |
531 |
604 lemma takefill_bintrunc: |
532 lemma takefill_bintrunc: "takefill False n bl = rev (bin_to_bl n (bl_to_bin (rev bl)))" |
605 "takefill False n bl = rev (bin_to_bl n (bl_to_bin (rev bl)))" |
|
606 apply (rule nth_equalityI) |
533 apply (rule nth_equalityI) |
607 apply simp |
534 apply simp |
608 apply (clarsimp simp: nth_takefill nth_rev nth_bin_to_bl bin_nth_of_bl) |
535 apply (clarsimp simp: nth_takefill nth_rev nth_bin_to_bl bin_nth_of_bl) |
609 done |
536 done |
610 |
537 |
611 lemma bl_bin_bl_rtf: |
538 lemma bl_bin_bl_rtf: "bin_to_bl n (bl_to_bin bl) = rev (takefill False n (rev bl))" |
612 "bin_to_bl n (bl_to_bin bl) = rev (takefill False n (rev bl))" |
539 by (simp add: takefill_bintrunc) |
613 by (simp add : takefill_bintrunc) |
|
614 |
540 |
615 lemma bl_bin_bl_rep_drop: |
541 lemma bl_bin_bl_rep_drop: |
616 "bin_to_bl n (bl_to_bin bl) = |
542 "bin_to_bl n (bl_to_bin bl) = |
617 replicate (n - length bl) False @ drop (length bl - n) bl" |
543 replicate (n - length bl) False @ drop (length bl - n) bl" |
618 by (simp add: bl_bin_bl_rtf takefill_alt rev_take) |
544 by (simp add: bl_bin_bl_rtf takefill_alt rev_take) |
619 |
545 |
620 lemma tf_rev: |
546 lemma tf_rev: |
621 "n + k = m + length bl ==> takefill x m (rev (takefill y n bl)) = |
547 "n + k = m + length bl \<Longrightarrow> takefill x m (rev (takefill y n bl)) = |
622 rev (takefill y m (rev (takefill x k (rev bl))))" |
548 rev (takefill y m (rev (takefill x k (rev bl))))" |
623 apply (rule nth_equalityI) |
549 apply (rule nth_equalityI) |
624 apply (auto simp add: nth_takefill nth_rev) |
550 apply (auto simp add: nth_takefill nth_rev) |
625 apply (rule_tac f = "%n. bl ! n" in arg_cong) |
551 apply (rule_tac f = "\<lambda>n. bl ! n" in arg_cong) |
626 apply arith |
552 apply arith |
627 done |
553 done |
628 |
554 |
629 lemma takefill_minus: |
555 lemma takefill_minus: "0 < n \<Longrightarrow> takefill fill (Suc (n - 1)) w = takefill fill n w" |
630 "0 < n ==> takefill fill (Suc (n - 1)) w = takefill fill n w" |
|
631 by auto |
556 by auto |
632 |
557 |
633 lemmas takefill_Suc_cases = |
558 lemmas takefill_Suc_cases = |
634 list.cases [THEN takefill.Suc [THEN trans]] |
559 list.cases [THEN takefill.Suc [THEN trans]] |
635 |
560 |
636 lemmas takefill_Suc_Nil = takefill_Suc_cases (1) |
561 lemmas takefill_Suc_Nil = takefill_Suc_cases (1) |
637 lemmas takefill_Suc_Cons = takefill_Suc_cases (2) |
562 lemmas takefill_Suc_Cons = takefill_Suc_cases (2) |
638 |
563 |
639 lemmas takefill_minus_simps = takefill_Suc_cases [THEN [2] |
564 lemmas takefill_minus_simps = takefill_Suc_cases [THEN [2] |
640 takefill_minus [symmetric, THEN trans]] |
565 takefill_minus [symmetric, THEN trans]] |
641 |
566 |
642 lemma takefill_numeral_Nil [simp]: |
567 lemma takefill_numeral_Nil [simp]: |
643 "takefill fill (numeral k) [] = fill # takefill fill (pred_numeral k) []" |
568 "takefill fill (numeral k) [] = fill # takefill fill (pred_numeral k) []" |
644 by (simp add: numeral_eq_Suc) |
569 by (simp add: numeral_eq_Suc) |
645 |
570 |
646 lemma takefill_numeral_Cons [simp]: |
571 lemma takefill_numeral_Cons [simp]: |
647 "takefill fill (numeral k) (x # xs) = x # takefill fill (pred_numeral k) xs" |
572 "takefill fill (numeral k) (x # xs) = x # takefill fill (pred_numeral k) xs" |
648 by (simp add: numeral_eq_Suc) |
573 by (simp add: numeral_eq_Suc) |
649 |
574 |
650 (* links with function bl_to_bin *) |
575 |
651 |
576 subsection \<open>Links with function \<open>bl_to_bin\<close>\<close> |
652 lemma bl_to_bin_aux_cat: |
577 |
653 "!!nv v. bl_to_bin_aux bs (bin_cat w nv v) = |
578 lemma bl_to_bin_aux_cat: |
|
579 "\<And>nv v. bl_to_bin_aux bs (bin_cat w nv v) = |
654 bin_cat w (nv + length bs) (bl_to_bin_aux bs v)" |
580 bin_cat w (nv + length bs) (bl_to_bin_aux bs v)" |
655 apply (induct bs) |
581 by (induct bs) (simp, simp add: bin_cat_Suc_Bit [symmetric] del: bin_cat.simps) |
656 apply simp |
582 |
657 apply (simp add: bin_cat_Suc_Bit [symmetric] del: bin_cat.simps) |
583 lemma bin_to_bl_aux_cat: |
658 done |
584 "\<And>w bs. bin_to_bl_aux (nv + nw) (bin_cat v nw w) bs = |
659 |
|
660 lemma bin_to_bl_aux_cat: |
|
661 "!!w bs. bin_to_bl_aux (nv + nw) (bin_cat v nw w) bs = |
|
662 bin_to_bl_aux nv v (bin_to_bl_aux nw w bs)" |
585 bin_to_bl_aux nv v (bin_to_bl_aux nw w bs)" |
663 by (induct nw) auto |
586 by (induct nw) auto |
664 |
587 |
665 lemma bl_to_bin_aux_alt: |
588 lemma bl_to_bin_aux_alt: "bl_to_bin_aux bs w = bin_cat w (length bs) (bl_to_bin bs)" |
666 "bl_to_bin_aux bs w = bin_cat w (length bs) (bl_to_bin bs)" |
|
667 using bl_to_bin_aux_cat [where nv = "0" and v = "0"] |
589 using bl_to_bin_aux_cat [where nv = "0" and v = "0"] |
668 unfolding bl_to_bin_def [symmetric] by simp |
590 by (simp add: bl_to_bin_def [symmetric]) |
669 |
591 |
670 lemma bin_to_bl_cat: |
592 lemma bin_to_bl_cat: |
671 "bin_to_bl (nv + nw) (bin_cat v nw w) = |
593 "bin_to_bl (nv + nw) (bin_cat v nw w) = |
672 bin_to_bl_aux nv v (bin_to_bl nw w)" |
594 bin_to_bl_aux nv v (bin_to_bl nw w)" |
673 unfolding bin_to_bl_def by (simp add: bin_to_bl_aux_cat) |
595 by (simp add: bin_to_bl_def bin_to_bl_aux_cat) |
674 |
596 |
675 lemmas bl_to_bin_aux_app_cat = |
597 lemmas bl_to_bin_aux_app_cat = |
676 trans [OF bl_to_bin_aux_append bl_to_bin_aux_alt] |
598 trans [OF bl_to_bin_aux_append bl_to_bin_aux_alt] |
677 |
599 |
678 lemmas bin_to_bl_aux_cat_app = |
600 lemmas bin_to_bl_aux_cat_app = |
679 trans [OF bin_to_bl_aux_cat bin_to_bl_aux_alt] |
601 trans [OF bin_to_bl_aux_cat bin_to_bl_aux_alt] |
680 |
602 |
739 by (induct bl) auto |
658 by (induct bl) auto |
740 |
659 |
741 lemma size_rbl_succ: "length (rbl_succ bl) = length bl" |
660 lemma size_rbl_succ: "length (rbl_succ bl) = length bl" |
742 by (induct bl) auto |
661 by (induct bl) auto |
743 |
662 |
744 lemma size_rbl_add: |
663 lemma size_rbl_add: "length (rbl_add bl cl) = length bl" |
745 "!!cl. length (rbl_add bl cl) = length bl" |
664 by (induct bl arbitrary: cl) (auto simp: Let_def size_rbl_succ) |
746 by (induct bl) (auto simp: Let_def size_rbl_succ) |
665 |
747 |
666 lemma size_rbl_mult: "length (rbl_mult bl cl) = length bl" |
748 lemma size_rbl_mult: |
667 by (induct bl arbitrary: cl) (auto simp add: Let_def size_rbl_add) |
749 "!!cl. length (rbl_mult bl cl) = length bl" |
668 |
750 by (induct bl) (auto simp add : Let_def size_rbl_add) |
669 lemmas rbl_sizes [simp] = |
751 |
|
752 lemmas rbl_sizes [simp] = |
|
753 size_rbl_pred size_rbl_succ size_rbl_add size_rbl_mult |
670 size_rbl_pred size_rbl_succ size_rbl_add size_rbl_mult |
754 |
671 |
755 lemmas rbl_Nils = |
672 lemmas rbl_Nils = |
756 rbl_pred.Nil rbl_succ.Nil rbl_add.Nil rbl_mult.Nil |
673 rbl_pred.Nil rbl_succ.Nil rbl_add.Nil rbl_mult.Nil |
757 |
674 |
758 lemma rbl_pred: |
675 lemma rbl_pred: "rbl_pred (rev (bin_to_bl n bin)) = rev (bin_to_bl n (bin - 1))" |
759 "rbl_pred (rev (bin_to_bl n bin)) = rev (bin_to_bl n (bin - 1))" |
|
760 apply (induct n arbitrary: bin, simp) |
|
761 apply (unfold bin_to_bl_def) |
676 apply (unfold bin_to_bl_def) |
|
677 apply (induct n arbitrary: bin) |
|
678 apply simp |
762 apply clarsimp |
679 apply clarsimp |
763 apply (case_tac bin rule: bin_exhaust) |
680 apply (case_tac bin rule: bin_exhaust) |
764 apply (case_tac b) |
681 apply (case_tac b) |
765 apply (clarsimp simp: bin_to_bl_aux_alt)+ |
682 apply (clarsimp simp: bin_to_bl_aux_alt)+ |
766 done |
683 done |
767 |
684 |
768 lemma rbl_succ: |
685 lemma rbl_succ: "rbl_succ (rev (bin_to_bl n bin)) = rev (bin_to_bl n (bin + 1))" |
769 "rbl_succ (rev (bin_to_bl n bin)) = rev (bin_to_bl n (bin + 1))" |
|
770 apply (induct n arbitrary: bin, simp) |
|
771 apply (unfold bin_to_bl_def) |
686 apply (unfold bin_to_bl_def) |
|
687 apply (induct n arbitrary: bin) |
|
688 apply simp |
772 apply clarsimp |
689 apply clarsimp |
773 apply (case_tac bin rule: bin_exhaust) |
690 apply (case_tac bin rule: bin_exhaust) |
774 apply (case_tac b) |
691 apply (case_tac b) |
775 apply (clarsimp simp: bin_to_bl_aux_alt)+ |
692 apply (clarsimp simp: bin_to_bl_aux_alt)+ |
776 done |
693 done |
777 |
694 |
778 lemma rbl_add: |
695 lemma rbl_add: |
779 "!!bina binb. rbl_add (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb)) = |
696 "\<And>bina binb. rbl_add (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb)) = |
780 rev (bin_to_bl n (bina + binb))" |
697 rev (bin_to_bl n (bina + binb))" |
781 apply (induct n, simp) |
|
782 apply (unfold bin_to_bl_def) |
698 apply (unfold bin_to_bl_def) |
|
699 apply (induct n) |
|
700 apply simp |
783 apply clarsimp |
701 apply clarsimp |
784 apply (case_tac bina rule: bin_exhaust) |
702 apply (case_tac bina rule: bin_exhaust) |
785 apply (case_tac binb rule: bin_exhaust) |
703 apply (case_tac binb rule: bin_exhaust) |
786 apply (case_tac b) |
704 apply (case_tac b) |
787 apply (case_tac [!] "ba") |
705 apply (case_tac [!] "ba") |
788 apply (auto simp: rbl_succ bin_to_bl_aux_alt Let_def ac_simps) |
706 apply (auto simp: rbl_succ bin_to_bl_aux_alt Let_def ac_simps) |
789 done |
707 done |
790 |
708 |
791 lemma rbl_add_app2: |
709 lemma rbl_add_app2: "length blb \<ge> length bla \<Longrightarrow> rbl_add bla (blb @ blc) = rbl_add bla blb" |
792 "!!blb. length blb >= length bla ==> |
710 apply (induct bla arbitrary: blb) |
793 rbl_add bla (blb @ blc) = rbl_add bla blb" |
711 apply simp |
794 apply (induct bla, simp) |
|
795 apply clarsimp |
712 apply clarsimp |
796 apply (case_tac blb, clarsimp) |
713 apply (case_tac blb, clarsimp) |
797 apply (clarsimp simp: Let_def) |
714 apply (clarsimp simp: Let_def) |
798 done |
715 done |
799 |
716 |
800 lemma rbl_add_take2: |
717 lemma rbl_add_take2: |
801 "!!blb. length blb >= length bla ==> |
718 "length blb >= length bla ==> rbl_add bla (take (length bla) blb) = rbl_add bla blb" |
802 rbl_add bla (take (length bla) blb) = rbl_add bla blb" |
719 apply (induct bla arbitrary: blb) |
803 apply (induct bla, simp) |
720 apply simp |
804 apply clarsimp |
721 apply clarsimp |
805 apply (case_tac blb, clarsimp) |
722 apply (case_tac blb, clarsimp) |
806 apply (clarsimp simp: Let_def) |
723 apply (clarsimp simp: Let_def) |
807 done |
724 done |
808 |
725 |
809 lemma rbl_add_long: |
726 lemma rbl_add_long: |
810 "m >= n ==> rbl_add (rev (bin_to_bl n bina)) (rev (bin_to_bl m binb)) = |
727 "m \<ge> n \<Longrightarrow> rbl_add (rev (bin_to_bl n bina)) (rev (bin_to_bl m binb)) = |
811 rev (bin_to_bl n (bina + binb))" |
728 rev (bin_to_bl n (bina + binb))" |
812 apply (rule box_equals [OF _ rbl_add_take2 rbl_add]) |
729 apply (rule box_equals [OF _ rbl_add_take2 rbl_add]) |
813 apply (rule_tac f = "rbl_add (rev (bin_to_bl n bina))" in arg_cong) |
730 apply (rule_tac f = "rbl_add (rev (bin_to_bl n bina))" in arg_cong) |
814 apply (rule rev_swap [THEN iffD1]) |
731 apply (rule rev_swap [THEN iffD1]) |
815 apply (simp add: rev_take drop_bin2bl) |
732 apply (simp add: rev_take drop_bin2bl) |
816 apply simp |
733 apply simp |
817 done |
734 done |
818 |
735 |
819 lemma rbl_mult_app2: |
736 lemma rbl_mult_app2: "length blb \<ge> length bla \<Longrightarrow> rbl_mult bla (blb @ blc) = rbl_mult bla blb" |
820 "!!blb. length blb >= length bla ==> |
737 apply (induct bla arbitrary: blb) |
821 rbl_mult bla (blb @ blc) = rbl_mult bla blb" |
738 apply simp |
822 apply (induct bla, simp) |
|
823 apply clarsimp |
739 apply clarsimp |
824 apply (case_tac blb, clarsimp) |
740 apply (case_tac blb, clarsimp) |
825 apply (clarsimp simp: Let_def rbl_add_app2) |
741 apply (clarsimp simp: Let_def rbl_add_app2) |
826 done |
742 done |
827 |
743 |
828 lemma rbl_mult_take2: |
744 lemma rbl_mult_take2: |
829 "length blb >= length bla ==> |
745 "length blb \<ge> length bla \<Longrightarrow> rbl_mult bla (take (length bla) blb) = rbl_mult bla blb" |
830 rbl_mult bla (take (length bla) blb) = rbl_mult bla blb" |
|
831 apply (rule trans) |
746 apply (rule trans) |
832 apply (rule rbl_mult_app2 [symmetric]) |
747 apply (rule rbl_mult_app2 [symmetric]) |
833 apply simp |
748 apply simp |
834 apply (rule_tac f = "rbl_mult bla" in arg_cong) |
749 apply (rule_tac f = "rbl_mult bla" in arg_cong) |
835 apply (rule append_take_drop_id) |
750 apply (rule append_take_drop_id) |
836 done |
751 done |
837 |
752 |
838 lemma rbl_mult_gt1: |
753 lemma rbl_mult_gt1: |
839 "m >= length bl ==> rbl_mult bl (rev (bin_to_bl m binb)) = |
754 "m \<ge> length bl \<Longrightarrow> |
|
755 rbl_mult bl (rev (bin_to_bl m binb)) = |
840 rbl_mult bl (rev (bin_to_bl (length bl) binb))" |
756 rbl_mult bl (rev (bin_to_bl (length bl) binb))" |
841 apply (rule trans) |
757 apply (rule trans) |
842 apply (rule rbl_mult_take2 [symmetric]) |
758 apply (rule rbl_mult_take2 [symmetric]) |
843 apply simp_all |
759 apply simp_all |
844 apply (rule_tac f = "rbl_mult bl" in arg_cong) |
760 apply (rule_tac f = "rbl_mult bl" in arg_cong) |
845 apply (rule rev_swap [THEN iffD1]) |
761 apply (rule rev_swap [THEN iffD1]) |
846 apply (simp add: rev_take drop_bin2bl) |
762 apply (simp add: rev_take drop_bin2bl) |
847 done |
763 done |
848 |
764 |
849 lemma rbl_mult_gt: |
765 lemma rbl_mult_gt: |
850 "m > n ==> rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl m binb)) = |
766 "m > n \<Longrightarrow> |
|
767 rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl m binb)) = |
851 rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb))" |
768 rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb))" |
852 by (auto intro: trans [OF rbl_mult_gt1]) |
769 by (auto intro: trans [OF rbl_mult_gt1]) |
853 |
770 |
854 lemmas rbl_mult_Suc = lessI [THEN rbl_mult_gt] |
771 lemmas rbl_mult_Suc = lessI [THEN rbl_mult_gt] |
855 |
772 |
856 lemma rbbl_Cons: |
773 lemma rbbl_Cons: "b # rev (bin_to_bl n x) = rev (bin_to_bl (Suc n) (x BIT b))" |
857 "b # rev (bin_to_bl n x) = rev (bin_to_bl (Suc n) (x BIT b))" |
774 by (simp add: bin_to_bl_def) (simp add: bin_to_bl_aux_alt) |
858 apply (unfold bin_to_bl_def) |
775 |
859 apply simp |
776 lemma rbl_mult: |
860 apply (simp add: bin_to_bl_aux_alt) |
777 "rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb)) = |
861 done |
|
862 |
|
863 lemma rbl_mult: "!!bina binb. |
|
864 rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb)) = |
|
865 rev (bin_to_bl n (bina * binb))" |
778 rev (bin_to_bl n (bina * binb))" |
866 apply (induct n) |
779 apply (induct n arbitrary: bina binb) |
867 apply simp |
780 apply simp |
868 apply (unfold bin_to_bl_def) |
781 apply (unfold bin_to_bl_def) |
869 apply clarsimp |
782 apply clarsimp |
870 apply (case_tac bina rule: bin_exhaust) |
783 apply (case_tac bina rule: bin_exhaust) |
871 apply (case_tac binb rule: bin_exhaust) |
784 apply (case_tac binb rule: bin_exhaust) |
956 lemmas rsplit_aux_apps [where bs = "[]"] = |
862 lemmas rsplit_aux_apps [where bs = "[]"] = |
957 bin_rsplit_aux_append bin_rsplitl_aux_append |
863 bin_rsplit_aux_append bin_rsplitl_aux_append |
958 |
864 |
959 lemmas rsplit_def_auxs = bin_rsplit_def bin_rsplitl_def |
865 lemmas rsplit_def_auxs = bin_rsplit_def bin_rsplitl_def |
960 |
866 |
961 lemmas rsplit_aux_alts = rsplit_aux_apps |
867 lemmas rsplit_aux_alts = rsplit_aux_apps |
962 [unfolded append_Nil rsplit_def_auxs [symmetric]] |
868 [unfolded append_Nil rsplit_def_auxs [symmetric]] |
963 |
869 |
964 lemma bin_split_minus: "0 < n ==> bin_split (Suc (n - 1)) w = bin_split n w" |
870 lemma bin_split_minus: "0 < n \<Longrightarrow> bin_split (Suc (n - 1)) w = bin_split n w" |
965 by auto |
871 by auto |
966 |
872 |
967 lemmas bin_split_minus_simp = |
873 lemmas bin_split_minus_simp = |
968 bin_split.Suc [THEN [2] bin_split_minus [symmetric, THEN trans]] |
874 bin_split.Suc [THEN [2] bin_split_minus [symmetric, THEN trans]] |
969 |
875 |
970 lemma bin_split_pred_simp [simp]: |
876 lemma bin_split_pred_simp [simp]: |
971 "(0::nat) < numeral bin \<Longrightarrow> |
877 "(0::nat) < numeral bin \<Longrightarrow> |
972 bin_split (numeral bin) w = |
878 bin_split (numeral bin) w = |
973 (let (w1, w2) = bin_split (numeral bin - 1) (bin_rest w) |
879 (let (w1, w2) = bin_split (numeral bin - 1) (bin_rest w) |
974 in (w1, w2 BIT bin_last w))" |
880 in (w1, w2 BIT bin_last w))" |
975 by (simp only: bin_split_minus_simp) |
881 by (simp only: bin_split_minus_simp) |
976 |
882 |
977 lemma bin_rsplit_aux_simp_alt: |
883 lemma bin_rsplit_aux_simp_alt: |
978 "bin_rsplit_aux n m c bs = |
884 "bin_rsplit_aux n m c bs = |
979 (if m = 0 \<or> n = 0 |
885 (if m = 0 \<or> n = 0 then bs |
980 then bs |
886 else let (a, b) = bin_split n c in bin_rsplit n (m - n, a) @ b # bs)" |
981 else let (a, b) = bin_split n c in bin_rsplit n (m - n, a) @ b # bs)" |
887 apply (simp add: bin_rsplit_aux.simps [of n m c bs]) |
982 unfolding bin_rsplit_aux.simps [of n m c bs] |
|
983 apply simp |
|
984 apply (subst rsplit_aux_alts) |
888 apply (subst rsplit_aux_alts) |
985 apply (simp add: bin_rsplit_def) |
889 apply (simp add: bin_rsplit_def) |
986 done |
890 done |
987 |
891 |
988 lemmas bin_rsplit_simp_alt = |
892 lemmas bin_rsplit_simp_alt = |
989 trans [OF bin_rsplit_def bin_rsplit_aux_simp_alt] |
893 trans [OF bin_rsplit_def bin_rsplit_aux_simp_alt] |
990 |
894 |
991 lemmas bthrs = bin_rsplit_simp_alt [THEN [2] trans] |
895 lemmas bthrs = bin_rsplit_simp_alt [THEN [2] trans] |
992 |
896 |
993 lemma bin_rsplit_size_sign' [rule_format] : |
897 lemma bin_rsplit_size_sign' [rule_format]: |
994 "\<lbrakk>n > 0; rev sw = bin_rsplit n (nw, w)\<rbrakk> \<Longrightarrow> |
898 "n > 0 \<Longrightarrow> rev sw = bin_rsplit n (nw, w) \<Longrightarrow> \<forall>v\<in>set sw. bintrunc n v = v" |
995 (ALL v: set sw. bintrunc n v = v)" |
|
996 apply (induct sw arbitrary: nw w) |
899 apply (induct sw arbitrary: nw w) |
997 apply clarsimp |
900 apply clarsimp |
998 apply clarsimp |
901 apply clarsimp |
999 apply (drule bthrs) |
902 apply (drule bthrs) |
1000 apply (simp (no_asm_use) add: Let_def split: prod.split_asm if_split_asm) |
903 apply (simp (no_asm_use) add: Let_def split: prod.split_asm if_split_asm) |
1001 apply clarify |
904 apply clarify |
1002 apply (drule split_bintrunc) |
905 apply (drule split_bintrunc) |
1003 apply simp |
906 apply simp |
1004 done |
907 done |
1005 |
908 |
1006 lemmas bin_rsplit_size_sign = bin_rsplit_size_sign' [OF asm_rl |
909 lemmas bin_rsplit_size_sign = bin_rsplit_size_sign' [OF asm_rl |
1007 rev_rev_ident [THEN trans] set_rev [THEN equalityD2 [THEN subsetD]]] |
910 rev_rev_ident [THEN trans] set_rev [THEN equalityD2 [THEN subsetD]]] |
1008 |
911 |
1009 lemma bin_nth_rsplit [rule_format] : |
912 lemma bin_nth_rsplit [rule_format] : |
1010 "n > 0 ==> m < n ==> (ALL w k nw. rev sw = bin_rsplit n (nw, w) --> |
913 "n > 0 \<Longrightarrow> m < n \<Longrightarrow> |
1011 k < size sw --> bin_nth (sw ! k) m = bin_nth w (k * n + m))" |
914 \<forall>w k nw. |
|
915 rev sw = bin_rsplit n (nw, w) \<longrightarrow> |
|
916 k < size sw \<longrightarrow> bin_nth (sw ! k) m = bin_nth w (k * n + m)" |
1012 apply (induct sw) |
917 apply (induct sw) |
1013 apply clarsimp |
918 apply clarsimp |
1014 apply clarsimp |
919 apply clarsimp |
1015 apply (drule bthrs) |
920 apply (drule bthrs) |
1016 apply (simp (no_asm_use) add: Let_def split: prod.split_asm if_split_asm) |
921 apply (simp (no_asm_use) add: Let_def split: prod.split_asm if_split_asm) |
1017 apply clarify |
922 apply clarify |
1018 apply (erule allE, erule impE, erule exI) |
923 apply (erule allE, erule impE, erule exI) |
1019 apply (case_tac k) |
924 apply (case_tac k) |
1020 apply clarsimp |
925 apply clarsimp |
1021 prefer 2 |
926 prefer 2 |
1022 apply clarsimp |
927 apply clarsimp |
1023 apply (erule allE) |
928 apply (erule allE) |
1024 apply (erule (1) impE) |
929 apply (erule (1) impE) |
1025 apply (drule bin_nth_split, erule conjE, erule allE, |
930 apply (drule bin_nth_split, erule conjE, erule allE, erule trans, simp add: ac_simps)+ |
1026 erule trans, simp add : ac_simps)+ |
931 done |
1027 done |
932 |
1028 |
933 lemma bin_rsplit_all: "0 < nw \<Longrightarrow> nw \<le> n \<Longrightarrow> bin_rsplit n (nw, w) = [bintrunc n w]" |
1029 lemma bin_rsplit_all: |
934 by (auto simp: bin_rsplit_def rsplit_aux_simp2ls split: prod.split dest!: split_bintrunc) |
1030 "0 < nw ==> nw <= n ==> bin_rsplit n (nw, w) = [bintrunc n w]" |
935 |
1031 unfolding bin_rsplit_def |
936 lemma bin_rsplit_l [rule_format]: |
1032 by (clarsimp dest!: split_bintrunc simp: rsplit_aux_simp2ls split: prod.split) |
937 "\<forall>bin. bin_rsplitl n (m, bin) = bin_rsplit n (m, bintrunc m bin)" |
1033 |
|
1034 lemma bin_rsplit_l [rule_format] : |
|
1035 "ALL bin. bin_rsplitl n (m, bin) = bin_rsplit n (m, bintrunc m bin)" |
|
1036 apply (rule_tac a = "m" in wf_less_than [THEN wf_induct]) |
938 apply (rule_tac a = "m" in wf_less_than [THEN wf_induct]) |
1037 apply (simp (no_asm) add : bin_rsplitl_def bin_rsplit_def) |
939 apply (simp (no_asm) add: bin_rsplitl_def bin_rsplit_def) |
1038 apply (rule allI) |
940 apply (rule allI) |
1039 apply (subst bin_rsplitl_aux.simps) |
941 apply (subst bin_rsplitl_aux.simps) |
1040 apply (subst bin_rsplit_aux.simps) |
942 apply (subst bin_rsplit_aux.simps) |
1041 apply (clarsimp simp: Let_def split: prod.split) |
943 apply (clarsimp simp: Let_def split: prod.split) |
1042 apply (drule bin_split_trunc) |
944 apply (drule bin_split_trunc) |
1061 |
963 |
1062 lemma bin_rsplit_aux_len_le [rule_format] : |
964 lemma bin_rsplit_aux_len_le [rule_format] : |
1063 "\<forall>ws m. n \<noteq> 0 \<longrightarrow> ws = bin_rsplit_aux n nw w bs \<longrightarrow> |
965 "\<forall>ws m. n \<noteq> 0 \<longrightarrow> ws = bin_rsplit_aux n nw w bs \<longrightarrow> |
1064 length ws \<le> m \<longleftrightarrow> nw + length bs * n \<le> m * n" |
966 length ws \<le> m \<longleftrightarrow> nw + length bs * n \<le> m * n" |
1065 proof - |
967 proof - |
1066 { fix i j j' k k' m :: nat and R |
968 have *: R |
1067 assume d: "(i::nat) \<le> j \<or> m < j'" |
969 if d: "i \<le> j \<or> m < j'" |
1068 assume R1: "i * k \<le> j * k \<Longrightarrow> R" |
970 and R1: "i * k \<le> j * k \<Longrightarrow> R" |
1069 assume R2: "Suc m * k' \<le> j' * k' \<Longrightarrow> R" |
971 and R2: "Suc m * k' \<le> j' * k' \<Longrightarrow> R" |
1070 have "R" using d |
972 for i j j' k k' m :: nat and R |
1071 apply safe |
973 using d |
1072 apply (rule R1, erule mult_le_mono1) |
974 apply safe |
1073 apply (rule R2, erule Suc_le_eq [THEN iffD2 [THEN mult_le_mono1]]) |
975 apply (rule R1, erule mult_le_mono1) |
1074 done |
976 apply (rule R2, erule Suc_le_eq [THEN iffD2 [THEN mult_le_mono1]]) |
1075 } note A = this |
977 done |
1076 { fix sc m n lb :: nat |
978 have **: "0 < sc \<Longrightarrow> sc - n + (n + lb * n) \<le> m * n \<longleftrightarrow> sc + lb * n \<le> m * n" |
1077 have "(0::nat) < sc \<Longrightarrow> sc - n + (n + lb * n) \<le> m * n \<longleftrightarrow> sc + lb * n \<le> m * n" |
979 for sc m n lb :: nat |
1078 apply safe |
980 apply safe |
1079 apply arith |
981 apply arith |
1080 apply (case_tac "sc >= n") |
982 apply (case_tac "sc \<ge> n") |
1081 apply arith |
983 apply arith |
1082 apply (insert linorder_le_less_linear [of m lb]) |
984 apply (insert linorder_le_less_linear [of m lb]) |
1083 apply (erule_tac k2=n and k'2=n in A) |
985 apply (erule_tac k=n and k'=n in *) |
1084 apply arith |
986 apply arith |
1085 apply simp |
987 apply simp |
1086 done |
988 done |
1087 } note B = this |
|
1088 show ?thesis |
989 show ?thesis |
1089 apply (induct n nw w bs rule: bin_rsplit_aux.induct) |
990 apply (induct n nw w bs rule: bin_rsplit_aux.induct) |
1090 apply (subst bin_rsplit_aux.simps) |
991 apply (subst bin_rsplit_aux.simps) |
1091 apply (simp add: B Let_def split: prod.split) |
992 apply (simp add: ** Let_def split: prod.split) |
1092 done |
993 done |
1093 qed |
994 qed |
1094 |
995 |
1095 lemma bin_rsplit_len_le: |
996 lemma bin_rsplit_len_le: "n \<noteq> 0 \<longrightarrow> ws = bin_rsplit n (nw, w) \<longrightarrow> length ws \<le> m \<longleftrightarrow> nw \<le> m * n" |
1096 "n \<noteq> 0 --> ws = bin_rsplit n (nw, w) --> (length ws <= m) = (nw <= m * n)" |
997 by (auto simp: bin_rsplit_def bin_rsplit_aux_len_le) |
1097 unfolding bin_rsplit_def by (clarsimp simp add : bin_rsplit_aux_len_le) |
998 |
1098 |
|
1099 lemma bin_rsplit_aux_len: |
999 lemma bin_rsplit_aux_len: |
1100 "n \<noteq> 0 \<Longrightarrow> length (bin_rsplit_aux n nw w cs) = |
1000 "n \<noteq> 0 \<Longrightarrow> length (bin_rsplit_aux n nw w cs) = (nw + n - 1) div n + length cs" |
1101 (nw + n - 1) div n + length cs" |
|
1102 apply (induct n nw w cs rule: bin_rsplit_aux.induct) |
1001 apply (induct n nw w cs rule: bin_rsplit_aux.induct) |
1103 apply (subst bin_rsplit_aux.simps) |
1002 apply (subst bin_rsplit_aux.simps) |
1104 apply (clarsimp simp: Let_def split: prod.split) |
1003 apply (clarsimp simp: Let_def split: prod.split) |
1105 apply (erule thin_rl) |
1004 apply (erule thin_rl) |
1106 apply (case_tac m) |
1005 apply (case_tac m) |
1107 apply simp |
1006 apply simp |
1108 apply (case_tac "m <= n") |
1007 apply (case_tac "m \<le> n") |
1109 apply (auto simp add: div_add_self2) |
1008 apply (auto simp add: div_add_self2) |
1110 done |
1009 done |
1111 |
1010 |
1112 lemma bin_rsplit_len: |
1011 lemma bin_rsplit_len: "n \<noteq> 0 \<Longrightarrow> length (bin_rsplit n (nw, w)) = (nw + n - 1) div n" |
1113 "n\<noteq>0 ==> length (bin_rsplit n (nw, w)) = (nw + n - 1) div n" |
1012 by (auto simp: bin_rsplit_def bin_rsplit_aux_len) |
1114 unfolding bin_rsplit_def by (clarsimp simp add : bin_rsplit_aux_len) |
|
1115 |
1013 |
1116 lemma bin_rsplit_aux_len_indep: |
1014 lemma bin_rsplit_aux_len_indep: |
1117 "n \<noteq> 0 \<Longrightarrow> length bs = length cs \<Longrightarrow> |
1015 "n \<noteq> 0 \<Longrightarrow> length bs = length cs \<Longrightarrow> |
1118 length (bin_rsplit_aux n nw v bs) = |
1016 length (bin_rsplit_aux n nw v bs) = |
1119 length (bin_rsplit_aux n nw w cs)" |
1017 length (bin_rsplit_aux n nw w cs)" |
1120 proof (induct n nw w cs arbitrary: v bs rule: bin_rsplit_aux.induct) |
1018 proof (induct n nw w cs arbitrary: v bs rule: bin_rsplit_aux.induct) |
1121 case (1 n m w cs v bs) show ?case |
1019 case (1 n m w cs v bs) |
|
1020 show ?case |
1122 proof (cases "m = 0") |
1021 proof (cases "m = 0") |
1123 case True then show ?thesis using \<open>length bs = length cs\<close> by simp |
1022 case True |
|
1023 with \<open>length bs = length cs\<close> show ?thesis by simp |
1124 next |
1024 next |
1125 case False |
1025 case False |
1126 from "1.hyps" \<open>m \<noteq> 0\<close> \<open>n \<noteq> 0\<close> have hyp: "\<And>v bs. length bs = Suc (length cs) \<Longrightarrow> |
1026 from "1.hyps" \<open>m \<noteq> 0\<close> \<open>n \<noteq> 0\<close> have hyp: "\<And>v bs. length bs = Suc (length cs) \<Longrightarrow> |
1127 length (bin_rsplit_aux n (m - n) v bs) = |
1027 length (bin_rsplit_aux n (m - n) v bs) = |
1128 length (bin_rsplit_aux n (m - n) (fst (bin_split n w)) (snd (bin_split n w) # cs))" |
1028 length (bin_rsplit_aux n (m - n) (fst (bin_split n w)) (snd (bin_split n w) # cs))" |
1129 by auto |
1029 by auto |
1130 show ?thesis using \<open>length bs = length cs\<close> \<open>n \<noteq> 0\<close> |
1030 from \<open>length bs = length cs\<close> \<open>n \<noteq> 0\<close> show ?thesis |
1131 by (auto simp add: bin_rsplit_aux_simp_alt Let_def bin_rsplit_len |
1031 by (auto simp add: bin_rsplit_aux_simp_alt Let_def bin_rsplit_len split: prod.split) |
1132 split: prod.split) |
|
1133 qed |
1032 qed |
1134 qed |
1033 qed |
1135 |
1034 |
1136 lemma bin_rsplit_len_indep: |
1035 lemma bin_rsplit_len_indep: |
1137 "n\<noteq>0 ==> length (bin_rsplit n (nw, v)) = length (bin_rsplit n (nw, w))" |
1036 "n \<noteq> 0 \<Longrightarrow> length (bin_rsplit n (nw, v)) = length (bin_rsplit n (nw, w))" |
1138 apply (unfold bin_rsplit_def) |
1037 apply (unfold bin_rsplit_def) |
1139 apply (simp (no_asm)) |
1038 apply (simp (no_asm)) |
1140 apply (erule bin_rsplit_aux_len_indep) |
1039 apply (erule bin_rsplit_aux_len_indep) |
1141 apply (rule refl) |
1040 apply (rule refl) |
1142 done |
1041 done |