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 +
    1.79 +defs (overloaded)
    1.80 +  zero_quot_def: "0 == \<lfloor>0\<rfloor>"
    1.81 +  add_quot_def: "X + Y == \<lfloor>pick X + pick Y\<rfloor>"
    1.82 +  diff_quot_def: "X - Y == \<lfloor>pick X - pick Y\<rfloor>"
    1.83 +  minus_quot_def: "- X == \<lfloor>- pick X\<rfloor>"
    1.84 +  abs_quot_def: "abs X == \<lfloor>abs (pick X)\<rfloor>"
    1.85 +  mult_quot_def: "X * Y == \<lfloor>pick X * pick Y\<rfloor>"
    1.86 +  inverse_quot_def: "inverse X == \<lfloor>inverse (pick X)\<rfloor>"
    1.87 +  divide_quot_def: "X / Y == \<lfloor>pick X / pick Y\<rfloor>"
    1.88 +  power_quot_def: "X^n == \<lfloor>(pick X)^n\<rfloor>"
    1.89 +  number_of_quot_def: "number_of b == \<lfloor>number_of b\<rfloor>"
    1.90 +
    1.91  end