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 type-definitions.\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