summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/Library/Quotient.thy

changeset 23373 | ead82c82da9e |

parent 22473 | 753123c89d72 |

child 23394 | 474ff28210c0 |

--- 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]: "\<not> (x \<sim> y) ==> \<not> (y \<sim> (x::'a::equiv))" proof - - assume "\<not> (x \<sim> y)" thus "\<not> (y \<sim> x)" + assume "\<not> (x \<sim> y)" then show "\<not> (y \<sim> x)" by (rule contrapos_nn) (rule equiv_sym) qed lemma not_equiv_trans1 [trans]: "\<not> (x \<sim> y) ==> y \<sim> z ==> \<not> (x \<sim> (z::'a::equiv))" proof - - assume "\<not> (x \<sim> y)" and yz: "y \<sim> z" + assume "\<not> (x \<sim> y)" and "y \<sim> z" show "\<not> (x \<sim> z)" proof assume "x \<sim> z" - also from yz have "z \<sim> y" .. + also from `y \<sim> z` have "z \<sim> y" .. finally have "x \<sim> y" . - thus False by contradiction + with `\<not> (x \<sim> y)` show False by contradiction qed qed lemma not_equiv_trans2 [trans]: "x \<sim> y ==> \<not> (y \<sim> z) ==> \<not> (x \<sim> (z::'a::equiv))" proof - - assume "\<not> (y \<sim> z)" hence "\<not> (z \<sim> y)" .. - also assume "x \<sim> y" hence "y \<sim> x" .. - finally have "\<not> (z \<sim> x)" . thus "(\<not> x \<sim> z)" .. + assume "\<not> (y \<sim> z)" then have "\<not> (z \<sim> y)" .. + also assume "x \<sim> y" then have "y \<sim> x" .. + finally have "\<not> (z \<sim> x)" . then show "(\<not> x \<sim> z)" .. qed text {* @@ -80,9 +80,9 @@ theorem quot_exhaust: "\<exists>a. A = \<lfloor>a\<rfloor>" proof (cases A) fix R assume R: "A = Abs_quot R" - assume "R \<in> quot" hence "\<exists>a. R = {x. a \<sim> x}" by blast + assume "R \<in> quot" then have "\<exists>a. R = {x. a \<sim> x}" by blast with R have "\<exists>a. A = Abs_quot {x. a \<sim> x}" by blast - thus ?thesis unfolding class_def . + then show ?thesis unfolding class_def . qed lemma quot_cases [cases type: quot]: "(!!a. A = \<lfloor>a\<rfloor> ==> C) ==> C" @@ -105,8 +105,8 @@ by (simp only: class_def Abs_quot_inject quotI) moreover have "a \<sim> a" .. ultimately have "a \<in> {x. b \<sim> x}" by blast - hence "b \<sim> a" by blast - thus ?thesis .. + then have "b \<sim> a" by blast + then show ?thesis .. qed next assume ab: "a \<sim> b" @@ -125,7 +125,7 @@ finally show "a \<sim> 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 "\<lfloor>a\<rfloor> = \<lfloor>a\<rfloor>" .. fix x assume "\<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>" - hence "a \<sim> x" .. thus "x \<sim> a" .. + then have "a \<sim> x" .. then show "x \<sim> a" .. qed qed theorem pick_inverse [intro]: "\<lfloor>pick A\<rfloor> = A" proof (cases A) fix a assume a: "A = \<lfloor>a\<rfloor>" - hence "pick A \<sim> a" by (simp only: pick_equiv) - hence "\<lfloor>pick A\<rfloor> = \<lfloor>a\<rfloor>" .. + then have "pick A \<sim> a" by (simp only: pick_equiv) + then have "\<lfloor>pick A\<rfloor> = \<lfloor>a\<rfloor>" .. with a show ?thesis by simp qed @@ -175,7 +175,7 @@ moreover show "\<lfloor>pick \<lfloor>b\<rfloor>\<rfloor> = \<lfloor>b\<rfloor>" .. moreover - show "P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor>" . + show "P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor>" by (rule P) ultimately show "P \<lfloor>pick \<lfloor>a\<rfloor>\<rfloor> \<lfloor>pick \<lfloor>b\<rfloor>\<rfloor>" by (simp only:) qed finally show ?thesis .