# HG changeset patch
# User wenzelm
# Date 974483330 3600
# Node ID eb93ace45a6e6e5e3aaeaa644965fbb3063c94f4
# Parent 41de88cb2108ca72bba38c93dac57936f00de4c2
removed quot_cond_function1, quot_function1;
removed overloaded standard operations;
diff r 41de88cb2108 r eb93ace45a6e src/HOL/Library/Quotient.thy
 a/src/HOL/Library/Quotient.thy Fri Nov 17 18:48:00 2000 +0100
+++ b/src/HOL/Library/Quotient.thy Fri Nov 17 18:48:50 2000 +0100
@@ 1,11 +1,11 @@
(* Title: HOL/Library/Quotient.thy
ID: $Id$
 Author: Gertrud Bauer and Markus Wenzel, TU Muenchen
+ Author: Markus Wenzel, TU Muenchen
*)
header {*
\title{Quotient types}
 \author{Gertrud Bauer and Markus Wenzel}
+ \author{Markus Wenzel}
*}
theory Quotient = Main:
@@ 160,7 +160,7 @@
qed
qed
theorem pick_inverse: "\pick A\ = A"
+theorem pick_inverse [intro]: "\pick A\ = A"
proof (cases A)
fix a assume a: "A = \a\"
hence "pick A \ a" by (simp only: pick_equiv)
@@ 170,145 +170,45 @@
text {*
\medskip The following rules support canonical function definitions
 on quotient types.
+ on quotient types (with up to two arguments). Note that the
+ strippeddown version without additional conditions is sufficient
+ most of the time.
*}
theorem quot_cond_function1:
 "(!!X. f X == g (pick X)) ==>
 (!!x x'. x \ x' ==> P x ==> P x' ==> g x = g x') ==>
 (!!x x'. x \ x' ==> P x = P x') ==>
 P a ==> f \a\ = g a"
proof 
 assume cong_g: "!!x x'. x \ x' ==> P x ==> P x' ==> g x = g x'"
 assume cong_P: "!!x x'. x \ x' ==> P x = P x'"
 assume P: "P a"
 assume "!!X. f X == g (pick X)"
 hence "f \a\ = g (pick \a\)" by (simp only:)
 also have "\ = g a"
 proof (rule cong_g)
 show "pick \a\ \ a" ..
 hence "P (pick \a\) = P a" by (rule cong_P)
 also note P
 finally show "P (pick \a\)" .
 qed
 finally show ?thesis .
qed

theorem quot_function1:
 "(!!X. f X == g (pick X)) ==>
 (!!x x'. x \ x' ==> g x = g x') ==>
 f \a\ = g a"
+theorem quot_cond_function:
+ "(!!X Y. f X Y == g (pick X) (pick Y)) ==>
+ (!!x x' y y'. \x\ = \x'\ ==> \y\ = \y'\ ==> P x y ==> P x' y'
+ ==> g x y = g x' y') ==>
+ (!!x x' y y'. \x\ = \x'\ ==> \y\ = \y'\ ==> P x y = P x' y') ==>
+ P a b ==> f \a\ \b\ = g a b"
+ (is "PROP ?eq ==> PROP ?cong_g ==> PROP ?cong_P ==> _ ==> _")
proof 
 case antecedent from this refl TrueI
 show ?thesis by (rule quot_cond_function1)
qed

theorem quot_cond_operation1:
 "(!!X. f X == \g (pick X)\) ==>
 (!!x x'. x \ x' ==> P x ==> P x' ==> g x \ g x') ==>
 (!!x x'. x \ x' ==> P x = P x') ==>
 P a ==> f \a\ = \g a\"
proof 
 assume defn: "!!X. f X == \g (pick X)\"
 assume "!!x x'. x \ x' ==> P x ==> P x' ==> g x \ g x'"
 hence cong_g: "!!x x'. x \ x' ==> P x ==> P x' ==> \g x\ = \g x'\" ..
 assume "!!x x'. x \ x' ==> P x = P x'" and "P a"
 with defn cong_g show ?thesis by (rule quot_cond_function1)
qed

theorem quot_operation1:
 "(!!X. f X == \g (pick X)\) ==>
 (!!x x'. x \ x' ==> g x \ g x') ==>
 f \a\ = \g a\"
proof 
 case antecedent from this refl TrueI
 show ?thesis by (rule quot_cond_operation1)
qed

theorem quot_cond_function2:
 "(!!X Y. f X Y == g (pick X) (pick Y)) ==>
 (!!x x' y y'. x \ x' ==> y \ y' ==> P x y ==> P x' y'
 ==> g x y = g x' y') ==>
 (!!x x' y y'. x \ x' ==> y \ y' ==> P x y = P x' y') ==>
 P a b ==> f \a\ \b\ = g a b"
proof 
 assume cong_g: "!!x x' y y'. x \ x' ==> y \ y' ==> P x y ==> P x' y'
 ==> g x y = g x' y'"
 assume cong_P: "!!x x' y y'. x \ x' ==> y \ y' ==> P x y = P x' y'"
 assume P: "P a b"
 assume "!!X Y. f X Y == g (pick X) (pick Y)"
 hence "f \a\ \b\ = g (pick \a\) (pick \b\)" by (simp only:)
+ assume cong_g: "PROP ?cong_g"
+ and cong_P: "PROP ?cong_P" and P: "P a b"
+ assume "PROP ?eq"
+ hence "f \a\ \b\ = g (pick \a\) (pick \b\)"
+ by (simp only:)
also have "\ = g a b"
proof (rule cong_g)
 show "pick \a\ \ a" ..
 moreover show "pick \b\ \ b" ..
 ultimately have "P (pick \a\) (pick \b\) = P a b" by (rule cong_P)
 also show "P a b" .
+ show "\pick \a\\ = \a\" ..
+ moreover
+ show "\pick \b\\ = \b\" ..
+ ultimately
+ have "P (pick \a\) (pick \b\) = P a b"
+ by (rule cong_P)
+ also show \ .
finally show "P (pick \a\) (pick \b\)" .
qed
finally show ?thesis .
qed
theorem quot_function2:
+theorem quot_function:
"(!!X Y. f X Y == g (pick X) (pick Y)) ==>
 (!!x x' y y'. x \ x' ==> y \ y' ==> g x y = g x' y') ==>
+ (!!x x' y y'. \x\ = \x'\ ==> \y\ = \y'\ ==> g x y = g x' y') ==>
f \a\ \b\ = g a b"
proof 
case antecedent from this refl TrueI
 show ?thesis by (rule quot_cond_function2)
qed

theorem quot_cond_operation2:
 "(!!X Y. f X Y == \g (pick X) (pick Y)\) ==>
 (!!x x' y y'. x \ x' ==> y \ y' ==> P x y ==> P x' y'
 ==> g x y \ g x' y') ==>
 (!!x x' y y'. x \ x' ==> y \ y' ==> P x y = P x' y') ==>
 P a b ==> f \a\ \b\ = \g a b\"
proof 
 assume defn: "!!X Y. f X Y == \g (pick X) (pick Y)\"
 assume "!!x x' y y'. x \ x' ==> y \ y' ==> P x y ==> P x' y'
 ==> g x y \ g x' y'"
 hence cong_g: "!!x x' y y'. x \ x' ==> y \ y' ==> P x y ==> P x' y'
 ==> \g x y\ = \g x' y'\" ..
 assume "!!x x' y y'. x \ x' ==> y \ y' ==> P x y = P x' y'" and "P a b"
 with defn cong_g show ?thesis by (rule quot_cond_function2)
qed

theorem quot_operation2:
 "(!!X Y. f X Y == \g (pick X) (pick Y)\) ==>
 (!!x x' y y'. x \ x' ==> y \ y' ==> g x y \ g x' y') ==>
 f \a\ \b\ = \g a b\"
proof 
 case antecedent from this refl TrueI
 show ?thesis by (rule quot_cond_operation2)
+ show ?thesis by (rule quot_cond_function)
qed
text {*
 \medskip HOL's collection of overloaded standard operations is lifted
 to quotient types in the canonical manner.
*}

instance quot :: (zero) zero ..
instance quot :: (plus) plus ..
instance quot :: (minus) minus ..
instance quot :: (times) times ..
instance quot :: (inverse) inverse ..
instance quot :: (power) power ..
instance quot :: (number) number ..
instance quot :: (ord) ord ..

defs (overloaded)
 zero_quot_def: "0 == \0\"
 add_quot_def: "X + Y == \pick X + pick Y\"
 diff_quot_def: "X  Y == \pick X  pick Y\"
 minus_quot_def: " X == \ pick X\"
 abs_quot_def: "abs X == \abs (pick X)\"
 mult_quot_def: "X * Y == \pick X * pick Y\"
 inverse_quot_def: "inverse X == \inverse (pick X)\"
 divide_quot_def: "X / Y == \pick X / pick Y\"
 power_quot_def: "X^n == \(pick X)^n\"
 number_of_quot_def: "number_of b == \number_of b\"
 le_quot_def: "X \ Y == pick X \ pick Y"
 less_quot_def: "X < Y == pick X < pick Y"

end