src/HOL/Library/Quotient.thy
 changeset 10437 7528f9e30ca4 parent 10392 f27afee8475d child 10459 df3cd3e76046
```     1.1 --- a/src/HOL/Library/Quotient.thy	Fri Nov 10 19:05:28 2000 +0100
1.2 +++ b/src/HOL/Library/Quotient.thy	Fri Nov 10 19:06:30 2000 +0100
1.3 @@ -136,35 +136,67 @@
1.4   on quotient types.
1.5  *}
1.6
1.7 -theorem cong_definition1:
1.8 -  "(!!X. f X == g (pick X)) ==>
1.9 -    (!!x x'. x \<sim> x' ==> g x = g x') ==>
1.10 -    f \<lfloor>a\<rfloor> = g a"
1.11 +theorem quot_definition1:
1.12 +  "(!!X. f X == \<lfloor>g (pick X)\<rfloor>) ==>
1.13 +    (!!x x'. x \<sim> x' ==> g x \<sim> g x') ==>
1.14 +    f \<lfloor>a\<rfloor> = \<lfloor>g a\<rfloor>"
1.15  proof -
1.16 -  assume cong: "!!x x'. x \<sim> x' ==> g x = g x'"
1.17 -  assume "!!X. f X == g (pick X)"
1.18 -  hence "f \<lfloor>a\<rfloor> = g (pick \<lfloor>a\<rfloor>)" by (simp only:)
1.19 -  also have "\<dots> = g a"
1.20 -  proof (rule cong)
1.21 -    show "pick \<lfloor>a\<rfloor> \<sim> a" ..
1.22 +  assume cong: "!!x x'. x \<sim> x' ==> g x \<sim> g x'"
1.23 +  assume "!!X. f X == \<lfloor>g (pick X)\<rfloor>"
1.24 +  hence "f \<lfloor>a\<rfloor> = \<lfloor>g (pick \<lfloor>a\<rfloor>)\<rfloor>" by (simp only:)
1.25 +  also have "\<dots> = \<lfloor>g a\<rfloor>"
1.26 +  proof
1.27 +    show "g (pick \<lfloor>a\<rfloor>) \<sim> g a"
1.28 +    proof (rule cong)
1.29 +      show "pick \<lfloor>a\<rfloor> \<sim> a" ..
1.30 +    qed
1.31    qed
1.32    finally show ?thesis .
1.33  qed
1.34
1.35 -theorem cong_definition2:
1.36 -  "(!!X Y. f X Y == g (pick X) (pick Y)) ==>
1.37 -    (!!x x' y y'. x \<sim> x' ==> y \<sim> y' ==> g x y = g x' y') ==>
1.38 -    f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
1.39 +theorem quot_definition2:
1.40 +  "(!!X Y. f X Y == \<lfloor>g (pick X) (pick Y)\<rfloor>) ==>
1.41 +    (!!x x' y y'. x \<sim> x' ==> y \<sim> y' ==> g x y \<sim> g x' y') ==>
1.42 +    f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = \<lfloor>g a b\<rfloor>"
1.43  proof -
1.44 -  assume cong: "!!x x' y y'. x \<sim> x' ==> y \<sim> y' ==> g x y = g x' y'"
1.45 -  assume "!!X Y. f X Y == g (pick X) (pick Y)"
1.46 -  hence "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g (pick \<lfloor>a\<rfloor>) (pick \<lfloor>b\<rfloor>)" by (simp only:)
1.47 -  also have "\<dots> = g a b"
1.48 -  proof (rule cong)
1.49 -    show "pick \<lfloor>a\<rfloor> \<sim> a" ..
1.50 -    show "pick \<lfloor>b\<rfloor> \<sim> b" ..
1.51 +  assume cong: "!!x x' y y'. x \<sim> x' ==> y \<sim> y' ==> g x y \<sim> g x' y'"
1.52 +  assume "!!X Y. f X Y == \<lfloor>g (pick X) (pick Y)\<rfloor>"
1.53 +  hence "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = \<lfloor>g (pick \<lfloor>a\<rfloor>) (pick \<lfloor>b\<rfloor>)\<rfloor>" by (simp only:)
1.54 +  also have "\<dots> = \<lfloor>g a b\<rfloor>"
1.55 +  proof
1.56 +    show "g (pick \<lfloor>a\<rfloor>) (pick \<lfloor>b\<rfloor>) \<sim> g a b"
1.57 +    proof (rule cong)
1.58 +      show "pick \<lfloor>a\<rfloor> \<sim> a" ..
1.59 +      show "pick \<lfloor>b\<rfloor> \<sim> b" ..
1.60 +    qed
1.61    qed
1.62    finally show ?thesis .
1.63  qed
1.64
1.65 +
1.66 +text {*
1.67 + \medskip HOL's collection of overloaded standard operations is lifted
1.68 + to quotient types in the canonical manner.
1.69 +*}
1.70 +
1.71 +instance quot :: (zero) zero ..
1.72 +instance quot :: (plus) plus ..
1.73 +instance quot :: (minus) minus ..
1.74 +instance quot :: (times) times ..
1.75 +instance quot :: (inverse) inverse ..
1.76 +instance quot :: (power) power ..
1.77 +instance quot :: (number) number ..
1.78 +