diff r 081c8641aa11 r ea1bf4b6255c src/HOL/Library/Quotient.thy
 a/src/HOL/Library/Quotient.thy Thu Oct 19 21:22:44 2000 +0200
+++ b/src/HOL/Library/Quotient.thy Thu Oct 19 21:23:15 2000 +0200
@@ 162,51 +162,6 @@
lemma quotE [elim]: "R \ quot ==> (!!a. R = {x. a \ x} ==> C) ==> C"
by (unfold quot_def) blast

text {*
 \medskip Standard properties of typedefinitions.\footnote{(FIXME)
 Better incorporate these into the typedef package?}
*}

theorem Rep_quot_inject: "(Rep_quot x = Rep_quot y) = (x = y)"
proof
 assume "Rep_quot x = Rep_quot y"
 hence "Abs_quot (Rep_quot x) = Abs_quot (Rep_quot y)" by (simp only:)
 thus "x = y" by (simp only: Rep_quot_inverse)
next
 assume "x = y"
 thus "Rep_quot x = Rep_quot y" by simp
qed

theorem Abs_quot_inject:
 "x \ quot ==> y \ quot ==> (Abs_quot x = Abs_quot y) = (x = y)"
proof
 assume "Abs_quot x = Abs_quot y"
 hence "Rep_quot (Abs_quot x) = Rep_quot (Abs_quot y)" by simp
 also assume "x \ quot" hence "Rep_quot (Abs_quot x) = x" by (rule Abs_quot_inverse)
 also assume "y \ quot" hence "Rep_quot (Abs_quot y) = y" by (rule Abs_quot_inverse)
 finally show "x = y" .
next
 assume "x = y"
 thus "Abs_quot x = Abs_quot y" by simp
qed

theorem Rep_quot_induct: "y \ quot ==> (!!x. P (Rep_quot x)) ==> P y"
proof 
 assume "!!x. P (Rep_quot x)" hence "P (Rep_quot (Abs_quot y))" .
 also assume "y \ quot" hence "Rep_quot (Abs_quot y) = y" by (rule Abs_quot_inverse)
 finally show "P y" .
qed

theorem Abs_quot_induct: "(!!y. y \ quot ==> P (Abs_quot y)) ==> P x"
proof 
 assume r: "!!y. y \ quot ==> P (Abs_quot y)"
 have "Rep_quot x \ quot" by (rule Rep_quot)
 hence "P (Abs_quot (Rep_quot x))" by (rule r)
 also have "Abs_quot (Rep_quot x) = x" by (rule Rep_quot_inverse)
 finally show "P x" .
qed

text {*
\medskip Abstracted equivalence classes are the canonical
representation of elements of a quotient type.
@@ 217,13 +172,11 @@
"\a\ == Abs_quot {x. a \ x}"
theorem quot_rep: "\a. A = \a\"
proof (unfold eqv_class_def)
 show "\a. A = Abs_quot {x. a \ x}"
 proof (induct A rule: Abs_quot_induct)
 fix R assume "R \ quot"
 hence "\a. R = {x. a \ x}" by blast
 thus "\a. Abs_quot R = Abs_quot {x. a \ x}" by blast
 qed
+proof (cases A)
+ fix R assume R: "A = Abs_quot R"
+ assume "R \ quot" hence "\a. R = {x. a \ x}" by blast
+ with R have "\a. A = Abs_quot {x. a \ x}" by blast
+ thus ?thesis by (unfold eqv_class_def)
qed
lemma quot_cases [case_names rep, cases type: quot]:
@@ 302,10 +255,10 @@
show "a \ domain" ..
qed
theorem pick_inverse: "\pick A\ = (A::'a::equiv quot)" (* FIXME tune proof *)
+theorem pick_inverse: "\pick A\ = (A::'a::equiv quot)"
proof (cases A)
fix a assume a: "A = \a\"
 hence "pick A \ a" by (simp only: pick_eqv)
+ hence "pick A \ a" by simp
hence "\pick A\ = \a\" by simp
with a show ?thesis by simp
qed