18 case (3 bin bit) |
18 case (3 bin bit) |
19 show ?case |
19 show ?case |
20 proof (cases y rule: bin_exhaust) |
20 proof (cases y rule: bin_exhaust) |
21 case (1 bin' bit') |
21 case (1 bin' bit') |
22 from 3 have "0 \<le> bin" |
22 from 3 have "0 \<le> bin" |
23 by (simp add: Bit_def bitval_def split add: bit.split_asm) |
23 by (cases bit) (simp_all add: Bit_def) |
24 then have "0 \<le> bin AND bin'" by (rule 3) |
24 then have "0 \<le> bin AND bin'" by (rule 3) |
25 with 1 show ?thesis |
25 with 1 show ?thesis |
26 by simp (simp add: Bit_def bitval_def split add: bit.split) |
26 by simp (simp add: Bit_def) |
27 qed |
27 qed |
28 next |
28 next |
29 case 2 |
29 case 2 |
30 then show ?case by (simp only: Min_def) |
30 then show ?case by (simp only: Min_def) |
31 qed simp |
31 qed simp |
39 case (3 bin bit) |
39 case (3 bin bit) |
40 show ?case |
40 show ?case |
41 proof (cases y rule: bin_exhaust) |
41 proof (cases y rule: bin_exhaust) |
42 case (1 bin' bit') |
42 case (1 bin' bit') |
43 from 3 have "0 \<le> bin" |
43 from 3 have "0 \<le> bin" |
44 by (simp add: Bit_def bitval_def split add: bit.split_asm) |
44 by (cases bit) (simp_all add: Bit_def) |
45 moreover from 1 3 have "0 \<le> bin'" |
45 moreover from 1 3 have "0 \<le> bin'" |
46 by (simp add: Bit_def bitval_def split add: bit.split_asm) |
46 by (cases bit') (simp_all add: Bit_def) |
47 ultimately have "0 \<le> bin OR bin'" by (rule 3) |
47 ultimately have "0 \<le> bin OR bin'" by (rule 3) |
48 with 1 show ?thesis |
48 with 1 show ?thesis |
49 by simp (simp add: Bit_def bitval_def split add: bit.split) |
49 by simp (simp add: Bit_def) |
50 qed |
50 qed |
51 qed simp_all |
51 qed simp_all |
52 |
52 |
53 lemma XOR_lower [simp]: |
53 lemma XOR_lower [simp]: |
54 fixes x :: int and y :: int |
54 fixes x :: int and y :: int |
59 case (3 bin bit) |
59 case (3 bin bit) |
60 show ?case |
60 show ?case |
61 proof (cases y rule: bin_exhaust) |
61 proof (cases y rule: bin_exhaust) |
62 case (1 bin' bit') |
62 case (1 bin' bit') |
63 from 3 have "0 \<le> bin" |
63 from 3 have "0 \<le> bin" |
64 by (simp add: Bit_def bitval_def split add: bit.split_asm) |
64 by (cases bit) (simp_all add: Bit_def) |
65 moreover from 1 3 have "0 \<le> bin'" |
65 moreover from 1 3 have "0 \<le> bin'" |
66 by (simp add: Bit_def bitval_def split add: bit.split_asm) |
66 by (cases bit') (simp_all add: Bit_def) |
67 ultimately have "0 \<le> bin XOR bin'" by (rule 3) |
67 ultimately have "0 \<le> bin XOR bin'" by (rule 3) |
68 with 1 show ?thesis |
68 with 1 show ?thesis |
69 by simp (simp add: Bit_def bitval_def split add: bit.split) |
69 by simp (simp add: Bit_def) |
70 qed |
70 qed |
71 next |
71 next |
72 case 2 |
72 case 2 |
73 then show ?case by (simp only: Min_def) |
73 then show ?case by (simp only: Min_def) |
74 qed simp |
74 qed simp |
82 case (3 bin bit) |
82 case (3 bin bit) |
83 show ?case |
83 show ?case |
84 proof (cases y rule: bin_exhaust) |
84 proof (cases y rule: bin_exhaust) |
85 case (1 bin' bit') |
85 case (1 bin' bit') |
86 from 3 have "0 \<le> bin" |
86 from 3 have "0 \<le> bin" |
87 by (simp add: Bit_def bitval_def split add: bit.split_asm) |
87 by (cases bit) (simp_all add: Bit_def) |
88 then have "bin AND bin' \<le> bin" by (rule 3) |
88 then have "bin AND bin' \<le> bin" by (rule 3) |
89 with 1 show ?thesis |
89 with 1 show ?thesis |
90 by simp (simp add: Bit_def bitval_def split add: bit.split) |
90 by simp (simp add: Bit_def) |
91 qed |
91 qed |
92 next |
92 next |
93 case 2 |
93 case 2 |
94 then show ?case by (simp only: Min_def) |
94 then show ?case by (simp only: Min_def) |
95 qed simp |
95 qed simp |
106 case (3 bin bit) |
106 case (3 bin bit) |
107 show ?case |
107 show ?case |
108 proof (cases x rule: bin_exhaust) |
108 proof (cases x rule: bin_exhaust) |
109 case (1 bin' bit') |
109 case (1 bin' bit') |
110 from 3 have "0 \<le> bin" |
110 from 3 have "0 \<le> bin" |
111 by (simp add: Bit_def bitval_def split add: bit.split_asm) |
111 by (cases bit) (simp_all add: Bit_def) |
112 then have "bin' AND bin \<le> bin" by (rule 3) |
112 then have "bin' AND bin \<le> bin" by (rule 3) |
113 with 1 show ?thesis |
113 with 1 show ?thesis |
114 by simp (simp add: Bit_def bitval_def split add: bit.split) |
114 by simp (simp add: Bit_def) |
115 qed |
115 qed |
116 next |
116 next |
117 case 2 |
117 case 2 |
118 then show ?case by (simp only: Min_def) |
118 then show ?case by (simp only: Min_def) |
119 qed simp |
119 qed simp |
133 case (1 bin' bit') |
133 case (1 bin' bit') |
134 show ?thesis |
134 show ?thesis |
135 proof (cases n) |
135 proof (cases n) |
136 case 0 |
136 case 0 |
137 with 3 have "bin BIT bit = 0" by simp |
137 with 3 have "bin BIT bit = 0" by simp |
138 then have "bin = 0" "bit = 0" |
138 then have "bin = 0" and "\<not> bit" |
139 by (auto simp add: Bit_def bitval_def split add: bit.split_asm) arith |
139 by (auto simp add: Bit_def split: if_splits) arith |
140 then show ?thesis using 0 1 `y < 2 ^ n` |
140 then show ?thesis using 0 1 `y < 2 ^ n` |
141 by simp |
141 by simp |
142 next |
142 next |
143 case (Suc m) |
143 case (Suc m) |
144 from 3 have "0 \<le> bin" |
144 from 3 have "0 \<le> bin" |
145 by (simp add: Bit_def bitval_def split add: bit.split_asm) |
145 by (cases bit) (simp_all add: Bit_def) |
146 moreover from 3 Suc have "bin < 2 ^ m" |
146 moreover from 3 Suc have "bin < 2 ^ m" |
147 by (simp add: Bit_def bitval_def split add: bit.split_asm) |
147 by (cases bit) (simp_all add: Bit_def) |
148 moreover from 1 3 Suc have "bin' < 2 ^ m" |
148 moreover from 1 3 Suc have "bin' < 2 ^ m" |
149 by (simp add: Bit_def bitval_def split add: bit.split_asm) |
149 by (cases bit') (simp_all add: Bit_def) |
150 ultimately have "bin OR bin' < 2 ^ m" by (rule 3) |
150 ultimately have "bin OR bin' < 2 ^ m" by (rule 3) |
151 with 1 Suc show ?thesis |
151 with 1 Suc show ?thesis |
152 by simp (simp add: Bit_def bitval_def split add: bit.split) |
152 by simp (simp add: Bit_def) |
153 qed |
153 qed |
154 qed |
154 qed |
155 qed simp_all |
155 qed simp_all |
156 |
156 |
157 lemma XOR_upper: |
157 lemma XOR_upper: |
166 case (1 bin' bit') |
166 case (1 bin' bit') |
167 show ?thesis |
167 show ?thesis |
168 proof (cases n) |
168 proof (cases n) |
169 case 0 |
169 case 0 |
170 with 3 have "bin BIT bit = 0" by simp |
170 with 3 have "bin BIT bit = 0" by simp |
171 then have "bin = 0" "bit = 0" |
171 then have "bin = 0" and "\<not> bit" |
172 by (auto simp add: Bit_def bitval_def split add: bit.split_asm) arith |
172 by (auto simp add: Bit_def split: if_splits) arith |
173 then show ?thesis using 0 1 `y < 2 ^ n` |
173 then show ?thesis using 0 1 `y < 2 ^ n` |
174 by simp |
174 by simp |
175 next |
175 next |
176 case (Suc m) |
176 case (Suc m) |
177 from 3 have "0 \<le> bin" |
177 from 3 have "0 \<le> bin" |
178 by (simp add: Bit_def bitval_def split add: bit.split_asm) |
178 by (cases bit) (simp_all add: Bit_def) |
179 moreover from 3 Suc have "bin < 2 ^ m" |
179 moreover from 3 Suc have "bin < 2 ^ m" |
180 by (simp add: Bit_def bitval_def split add: bit.split_asm) |
180 by (cases bit) (simp_all add: Bit_def) |
181 moreover from 1 3 Suc have "bin' < 2 ^ m" |
181 moreover from 1 3 Suc have "bin' < 2 ^ m" |
182 by (simp add: Bit_def bitval_def split add: bit.split_asm) |
182 by (cases bit') (simp_all add: Bit_def) |
183 ultimately have "bin XOR bin' < 2 ^ m" by (rule 3) |
183 ultimately have "bin XOR bin' < 2 ^ m" by (rule 3) |
184 with 1 Suc show ?thesis |
184 with 1 Suc show ?thesis |
185 by simp (simp add: Bit_def bitval_def split add: bit.split) |
185 by simp (simp add: Bit_def) |
186 qed |
186 qed |
187 qed |
187 qed |
188 next |
188 next |
189 case 2 |
189 case 2 |
190 then show ?case by (simp only: Min_def) |
190 then show ?case by (simp only: Min_def) |