diff -r 0035be079bee -r ead82c82da9e src/HOL/Library/Quotient.thy --- a/src/HOL/Library/Quotient.thy Wed Jun 13 16:43:02 2007 +0200 +++ b/src/HOL/Library/Quotient.thy Wed Jun 13 18:30:11 2007 +0200 @@ -31,27 +31,27 @@ lemma equiv_not_sym [sym]: "\ (x \ y) ==> \ (y \ (x::'a::equiv))" proof - - assume "\ (x \ y)" thus "\ (y \ x)" + assume "\ (x \ y)" then show "\ (y \ x)" by (rule contrapos_nn) (rule equiv_sym) qed lemma not_equiv_trans1 [trans]: "\ (x \ y) ==> y \ z ==> \ (x \ (z::'a::equiv))" proof - - assume "\ (x \ y)" and yz: "y \ z" + assume "\ (x \ y)" and "y \ z" show "\ (x \ z)" proof assume "x \ z" - also from yz have "z \ y" .. + also from `y \ z` have "z \ y" .. finally have "x \ y" . - thus False by contradiction + with `\ (x \ y)` show False by contradiction qed qed lemma not_equiv_trans2 [trans]: "x \ y ==> \ (y \ z) ==> \ (x \ (z::'a::equiv))" proof - - assume "\ (y \ z)" hence "\ (z \ y)" .. - also assume "x \ y" hence "y \ x" .. - finally have "\ (z \ x)" . thus "(\ x \ z)" .. + assume "\ (y \ z)" then have "\ (z \ y)" .. + also assume "x \ y" then have "y \ x" .. + finally have "\ (z \ x)" . then show "(\ x \ z)" .. qed text {* @@ -80,9 +80,9 @@ theorem quot_exhaust: "\a. A = \a\" proof (cases A) fix R assume R: "A = Abs_quot R" - assume "R \ quot" hence "\a. R = {x. a \ x}" by blast + assume "R \ quot" then have "\a. R = {x. a \ x}" by blast with R have "\a. A = Abs_quot {x. a \ x}" by blast - thus ?thesis unfolding class_def . + then show ?thesis unfolding class_def . qed lemma quot_cases [cases type: quot]: "(!!a. A = \a\ ==> C) ==> C" @@ -105,8 +105,8 @@ by (simp only: class_def Abs_quot_inject quotI) moreover have "a \ a" .. ultimately have "a \ {x. b \ x}" by blast - hence "b \ a" by blast - thus ?thesis .. + then have "b \ a" by blast + then show ?thesis .. qed next assume ab: "a \ b" @@ -125,7 +125,7 @@ finally show "a \ x" . qed qed - thus ?thesis by (simp only: class_def) + then show ?thesis by (simp only: class_def) qed qed @@ -142,15 +142,15 @@ proof (rule someI2) show "\a\ = \a\" .. fix x assume "\a\ = \x\" - hence "a \ x" .. thus "x \ a" .. + then have "a \ x" .. then show "x \ a" .. qed qed 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) - hence "\pick A\ = \a\" .. + then have "pick A \ a" by (simp only: pick_equiv) + then have "\pick A\ = \a\" .. with a show ?thesis by simp qed @@ -175,7 +175,7 @@ moreover show "\pick \b\\ = \b\" .. moreover - show "P \a\ \b\" . + show "P \a\ \b\" by (rule P) ultimately show "P \pick \a\\ \pick \b\\" by (simp only:) qed finally show ?thesis .