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 .