158 fix x assume "\<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>" |
158 fix x assume "\<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>" |
159 hence "a \<sim> x" .. thus "x \<sim> a" .. |
159 hence "a \<sim> x" .. thus "x \<sim> a" .. |
160 qed |
160 qed |
161 qed |
161 qed |
162 |
162 |
163 theorem pick_inverse: "\<lfloor>pick A\<rfloor> = A" |
163 theorem pick_inverse [intro]: "\<lfloor>pick A\<rfloor> = A" |
164 proof (cases A) |
164 proof (cases A) |
165 fix a assume a: "A = \<lfloor>a\<rfloor>" |
165 fix a assume a: "A = \<lfloor>a\<rfloor>" |
166 hence "pick A \<sim> a" by (simp only: pick_equiv) |
166 hence "pick A \<sim> a" by (simp only: pick_equiv) |
167 hence "\<lfloor>pick A\<rfloor> = \<lfloor>a\<rfloor>" .. |
167 hence "\<lfloor>pick A\<rfloor> = \<lfloor>a\<rfloor>" .. |
168 with a show ?thesis by simp |
168 with a show ?thesis by simp |
169 qed |
169 qed |
170 |
170 |
171 text {* |
171 text {* |
172 \medskip The following rules support canonical function definitions |
172 \medskip The following rules support canonical function definitions |
173 on quotient types. |
173 on quotient types (with up to two arguments). Note that the |
174 *} |
174 stripped-down version without additional conditions is sufficient |
175 |
175 most of the time. |
176 theorem quot_cond_function1: |
176 *} |
177 "(!!X. f X == g (pick X)) ==> |
177 |
178 (!!x x'. x \<sim> x' ==> P x ==> P x' ==> g x = g x') ==> |
178 theorem quot_cond_function: |
179 (!!x x'. x \<sim> x' ==> P x = P x') ==> |
|
180 P a ==> f \<lfloor>a\<rfloor> = g a" |
|
181 proof - |
|
182 assume cong_g: "!!x x'. x \<sim> x' ==> P x ==> P x' ==> g x = g x'" |
|
183 assume cong_P: "!!x x'. x \<sim> x' ==> P x = P x'" |
|
184 assume P: "P a" |
|
185 assume "!!X. f X == g (pick X)" |
|
186 hence "f \<lfloor>a\<rfloor> = g (pick \<lfloor>a\<rfloor>)" by (simp only:) |
|
187 also have "\<dots> = g a" |
|
188 proof (rule cong_g) |
|
189 show "pick \<lfloor>a\<rfloor> \<sim> a" .. |
|
190 hence "P (pick \<lfloor>a\<rfloor>) = P a" by (rule cong_P) |
|
191 also note P |
|
192 finally show "P (pick \<lfloor>a\<rfloor>)" . |
|
193 qed |
|
194 finally show ?thesis . |
|
195 qed |
|
196 |
|
197 theorem quot_function1: |
|
198 "(!!X. f X == g (pick X)) ==> |
|
199 (!!x x'. x \<sim> x' ==> g x = g x') ==> |
|
200 f \<lfloor>a\<rfloor> = g a" |
|
201 proof - |
|
202 case antecedent from this refl TrueI |
|
203 show ?thesis by (rule quot_cond_function1) |
|
204 qed |
|
205 |
|
206 theorem quot_cond_operation1: |
|
207 "(!!X. f X == \<lfloor>g (pick X)\<rfloor>) ==> |
|
208 (!!x x'. x \<sim> x' ==> P x ==> P x' ==> g x \<sim> g x') ==> |
|
209 (!!x x'. x \<sim> x' ==> P x = P x') ==> |
|
210 P a ==> f \<lfloor>a\<rfloor> = \<lfloor>g a\<rfloor>" |
|
211 proof - |
|
212 assume defn: "!!X. f X == \<lfloor>g (pick X)\<rfloor>" |
|
213 assume "!!x x'. x \<sim> x' ==> P x ==> P x' ==> g x \<sim> g x'" |
|
214 hence cong_g: "!!x x'. x \<sim> x' ==> P x ==> P x' ==> \<lfloor>g x\<rfloor> = \<lfloor>g x'\<rfloor>" .. |
|
215 assume "!!x x'. x \<sim> x' ==> P x = P x'" and "P a" |
|
216 with defn cong_g show ?thesis by (rule quot_cond_function1) |
|
217 qed |
|
218 |
|
219 theorem quot_operation1: |
|
220 "(!!X. f X == \<lfloor>g (pick X)\<rfloor>) ==> |
|
221 (!!x x'. x \<sim> x' ==> g x \<sim> g x') ==> |
|
222 f \<lfloor>a\<rfloor> = \<lfloor>g a\<rfloor>" |
|
223 proof - |
|
224 case antecedent from this refl TrueI |
|
225 show ?thesis by (rule quot_cond_operation1) |
|
226 qed |
|
227 |
|
228 theorem quot_cond_function2: |
|
229 "(!!X Y. f X Y == g (pick X) (pick Y)) ==> |
179 "(!!X Y. f X Y == g (pick X) (pick Y)) ==> |
230 (!!x x' y y'. x \<sim> x' ==> y \<sim> y' ==> P x y ==> P x' y' |
180 (!!x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> ==> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor> ==> P x y ==> P x' y' |
231 ==> g x y = g x' y') ==> |
181 ==> g x y = g x' y') ==> |
232 (!!x x' y y'. x \<sim> x' ==> y \<sim> y' ==> P x y = P x' y') ==> |
182 (!!x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> ==> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor> ==> P x y = P x' y') ==> |
233 P a b ==> f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b" |
183 P a b ==> f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b" |
234 proof - |
184 (is "PROP ?eq ==> PROP ?cong_g ==> PROP ?cong_P ==> _ ==> _") |
235 assume cong_g: "!!x x' y y'. x \<sim> x' ==> y \<sim> y' ==> P x y ==> P x' y' |
185 proof - |
236 ==> g x y = g x' y'" |
186 assume cong_g: "PROP ?cong_g" |
237 assume cong_P: "!!x x' y y'. x \<sim> x' ==> y \<sim> y' ==> P x y = P x' y'" |
187 and cong_P: "PROP ?cong_P" and P: "P a b" |
238 assume P: "P a b" |
188 assume "PROP ?eq" |
239 assume "!!X Y. f X Y == g (pick X) (pick Y)" |
189 hence "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g (pick \<lfloor>a\<rfloor>) (pick \<lfloor>b\<rfloor>)" |
240 hence "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g (pick \<lfloor>a\<rfloor>) (pick \<lfloor>b\<rfloor>)" by (simp only:) |
190 by (simp only:) |
241 also have "\<dots> = g a b" |
191 also have "\<dots> = g a b" |
242 proof (rule cong_g) |
192 proof (rule cong_g) |
243 show "pick \<lfloor>a\<rfloor> \<sim> a" .. |
193 show "\<lfloor>pick \<lfloor>a\<rfloor>\<rfloor> = \<lfloor>a\<rfloor>" .. |
244 moreover show "pick \<lfloor>b\<rfloor> \<sim> b" .. |
194 moreover |
245 ultimately have "P (pick \<lfloor>a\<rfloor>) (pick \<lfloor>b\<rfloor>) = P a b" by (rule cong_P) |
195 show "\<lfloor>pick \<lfloor>b\<rfloor>\<rfloor> = \<lfloor>b\<rfloor>" .. |
246 also show "P a b" . |
196 ultimately |
|
197 have "P (pick \<lfloor>a\<rfloor>) (pick \<lfloor>b\<rfloor>) = P a b" |
|
198 by (rule cong_P) |
|
199 also show \<dots> . |
247 finally show "P (pick \<lfloor>a\<rfloor>) (pick \<lfloor>b\<rfloor>)" . |
200 finally show "P (pick \<lfloor>a\<rfloor>) (pick \<lfloor>b\<rfloor>)" . |
248 qed |
201 qed |
249 finally show ?thesis . |
202 finally show ?thesis . |
250 qed |
203 qed |
251 |
204 |
252 theorem quot_function2: |
205 theorem quot_function: |
253 "(!!X Y. f X Y == g (pick X) (pick Y)) ==> |
206 "(!!X Y. f X Y == g (pick X) (pick Y)) ==> |
254 (!!x x' y y'. x \<sim> x' ==> y \<sim> y' ==> g x y = g x' y') ==> |
207 (!!x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> ==> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor> ==> g x y = g x' y') ==> |
255 f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b" |
208 f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b" |
256 proof - |
209 proof - |
257 case antecedent from this refl TrueI |
210 case antecedent from this refl TrueI |
258 show ?thesis by (rule quot_cond_function2) |
211 show ?thesis by (rule quot_cond_function) |
259 qed |
212 qed |
260 |
|
261 theorem quot_cond_operation2: |
|
262 "(!!X Y. f X Y == \<lfloor>g (pick X) (pick Y)\<rfloor>) ==> |
|
263 (!!x x' y y'. x \<sim> x' ==> y \<sim> y' ==> P x y ==> P x' y' |
|
264 ==> g x y \<sim> g x' y') ==> |
|
265 (!!x x' y y'. x \<sim> x' ==> y \<sim> y' ==> P x y = P x' y') ==> |
|
266 P a b ==> f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = \<lfloor>g a b\<rfloor>" |
|
267 proof - |
|
268 assume defn: "!!X Y. f X Y == \<lfloor>g (pick X) (pick Y)\<rfloor>" |
|
269 assume "!!x x' y y'. x \<sim> x' ==> y \<sim> y' ==> P x y ==> P x' y' |
|
270 ==> g x y \<sim> g x' y'" |
|
271 hence cong_g: "!!x x' y y'. x \<sim> x' ==> y \<sim> y' ==> P x y ==> P x' y' |
|
272 ==> \<lfloor>g x y\<rfloor> = \<lfloor>g x' y'\<rfloor>" .. |
|
273 assume "!!x x' y y'. x \<sim> x' ==> y \<sim> y' ==> P x y = P x' y'" and "P a b" |
|
274 with defn cong_g show ?thesis by (rule quot_cond_function2) |
|
275 qed |
|
276 |
|
277 theorem quot_operation2: |
|
278 "(!!X Y. f X Y == \<lfloor>g (pick X) (pick Y)\<rfloor>) ==> |
|
279 (!!x x' y y'. x \<sim> x' ==> y \<sim> y' ==> g x y \<sim> g x' y') ==> |
|
280 f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = \<lfloor>g a b\<rfloor>" |
|
281 proof - |
|
282 case antecedent from this refl TrueI |
|
283 show ?thesis by (rule quot_cond_operation2) |
|
284 qed |
|
285 |
|
286 text {* |
|
287 \medskip HOL's collection of overloaded standard operations is lifted |
|
288 to quotient types in the canonical manner. |
|
289 *} |
|
290 |
|
291 instance quot :: (zero) zero .. |
|
292 instance quot :: (plus) plus .. |
|
293 instance quot :: (minus) minus .. |
|
294 instance quot :: (times) times .. |
|
295 instance quot :: (inverse) inverse .. |
|
296 instance quot :: (power) power .. |
|
297 instance quot :: (number) number .. |
|
298 instance quot :: (ord) ord .. |
|
299 |
|
300 defs (overloaded) |
|
301 zero_quot_def: "0 == \<lfloor>0\<rfloor>" |
|
302 add_quot_def: "X + Y == \<lfloor>pick X + pick Y\<rfloor>" |
|
303 diff_quot_def: "X - Y == \<lfloor>pick X - pick Y\<rfloor>" |
|
304 minus_quot_def: "- X == \<lfloor>- pick X\<rfloor>" |
|
305 abs_quot_def: "abs X == \<lfloor>abs (pick X)\<rfloor>" |
|
306 mult_quot_def: "X * Y == \<lfloor>pick X * pick Y\<rfloor>" |
|
307 inverse_quot_def: "inverse X == \<lfloor>inverse (pick X)\<rfloor>" |
|
308 divide_quot_def: "X / Y == \<lfloor>pick X / pick Y\<rfloor>" |
|
309 power_quot_def: "X^n == \<lfloor>(pick X)^n\<rfloor>" |
|
310 number_of_quot_def: "number_of b == \<lfloor>number_of b\<rfloor>" |
|
311 le_quot_def: "X \<le> Y == pick X \<le> pick Y" |
|
312 less_quot_def: "X < Y == pick X < pick Y" |
|
313 |
213 |
314 end |
214 end |