src/HOL/Library/Quotient.thy
 changeset 23373 ead82c82da9e parent 22473 753123c89d72 child 23394 474ff28210c0
```     1.1 --- a/src/HOL/Library/Quotient.thy	Wed Jun 13 16:43:02 2007 +0200
1.2 +++ b/src/HOL/Library/Quotient.thy	Wed Jun 13 18:30:11 2007 +0200
1.3 @@ -31,27 +31,27 @@
1.4
1.5  lemma equiv_not_sym [sym]: "\<not> (x \<sim> y) ==> \<not> (y \<sim> (x::'a::equiv))"
1.6  proof -
1.7 -  assume "\<not> (x \<sim> y)" thus "\<not> (y \<sim> x)"
1.8 +  assume "\<not> (x \<sim> y)" then show "\<not> (y \<sim> x)"
1.9      by (rule contrapos_nn) (rule equiv_sym)
1.10  qed
1.11
1.12  lemma not_equiv_trans1 [trans]: "\<not> (x \<sim> y) ==> y \<sim> z ==> \<not> (x \<sim> (z::'a::equiv))"
1.13  proof -
1.14 -  assume "\<not> (x \<sim> y)" and yz: "y \<sim> z"
1.15 +  assume "\<not> (x \<sim> y)" and "y \<sim> z"
1.16    show "\<not> (x \<sim> z)"
1.17    proof
1.18      assume "x \<sim> z"
1.19 -    also from yz have "z \<sim> y" ..
1.20 +    also from `y \<sim> z` have "z \<sim> y" ..
1.21      finally have "x \<sim> y" .
1.22 -    thus False by contradiction
1.23 +    with `\<not> (x \<sim> y)` show False by contradiction
1.24    qed
1.25  qed
1.26
1.27  lemma not_equiv_trans2 [trans]: "x \<sim> y ==> \<not> (y \<sim> z) ==> \<not> (x \<sim> (z::'a::equiv))"
1.28  proof -
1.29 -  assume "\<not> (y \<sim> z)" hence "\<not> (z \<sim> y)" ..
1.30 -  also assume "x \<sim> y" hence "y \<sim> x" ..
1.31 -  finally have "\<not> (z \<sim> x)" . thus "(\<not> x \<sim> z)" ..
1.32 +  assume "\<not> (y \<sim> z)" then have "\<not> (z \<sim> y)" ..
1.33 +  also assume "x \<sim> y" then have "y \<sim> x" ..
1.34 +  finally have "\<not> (z \<sim> x)" . then show "(\<not> x \<sim> z)" ..
1.35  qed
1.36
1.37  text {*
1.38 @@ -80,9 +80,9 @@
1.39  theorem quot_exhaust: "\<exists>a. A = \<lfloor>a\<rfloor>"
1.40  proof (cases A)
1.41    fix R assume R: "A = Abs_quot R"
1.42 -  assume "R \<in> quot" hence "\<exists>a. R = {x. a \<sim> x}" by blast
1.43 +  assume "R \<in> quot" then have "\<exists>a. R = {x. a \<sim> x}" by blast
1.44    with R have "\<exists>a. A = Abs_quot {x. a \<sim> x}" by blast
1.45 -  thus ?thesis unfolding class_def .
1.46 +  then show ?thesis unfolding class_def .
1.47  qed
1.48
1.49  lemma quot_cases [cases type: quot]: "(!!a. A = \<lfloor>a\<rfloor> ==> C) ==> C"
1.50 @@ -105,8 +105,8 @@
1.51        by (simp only: class_def Abs_quot_inject quotI)
1.52      moreover have "a \<sim> a" ..
1.53      ultimately have "a \<in> {x. b \<sim> x}" by blast
1.54 -    hence "b \<sim> a" by blast
1.55 -    thus ?thesis ..
1.56 +    then have "b \<sim> a" by blast
1.57 +    then show ?thesis ..
1.58    qed
1.59  next
1.60    assume ab: "a \<sim> b"
1.61 @@ -125,7 +125,7 @@
1.62          finally show "a \<sim> x" .
1.63        qed
1.64      qed
1.65 -    thus ?thesis by (simp only: class_def)
1.66 +    then show ?thesis by (simp only: class_def)
1.67    qed
1.68  qed
1.69
1.70 @@ -142,15 +142,15 @@
1.71    proof (rule someI2)
1.72      show "\<lfloor>a\<rfloor> = \<lfloor>a\<rfloor>" ..
1.73      fix x assume "\<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>"
1.74 -    hence "a \<sim> x" .. thus "x \<sim> a" ..
1.75 +    then have "a \<sim> x" .. then show "x \<sim> a" ..
1.76    qed
1.77  qed
1.78
1.79  theorem pick_inverse [intro]: "\<lfloor>pick A\<rfloor> = A"
1.80  proof (cases A)
1.81    fix a assume a: "A = \<lfloor>a\<rfloor>"
1.82 -  hence "pick A \<sim> a" by (simp only: pick_equiv)
1.83 -  hence "\<lfloor>pick A\<rfloor> = \<lfloor>a\<rfloor>" ..
1.84 +  then have "pick A \<sim> a" by (simp only: pick_equiv)
1.85 +  then have "\<lfloor>pick A\<rfloor> = \<lfloor>a\<rfloor>" ..
1.86    with a show ?thesis by simp
1.87  qed
1.88
1.89 @@ -175,7 +175,7 @@
1.90      moreover
1.91      show "\<lfloor>pick \<lfloor>b\<rfloor>\<rfloor> = \<lfloor>b\<rfloor>" ..
1.92      moreover
1.93 -    show "P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor>" .
1.94 +    show "P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor>" by (rule P)
1.95      ultimately show "P \<lfloor>pick \<lfloor>a\<rfloor>\<rfloor> \<lfloor>pick \<lfloor>b\<rfloor>\<rfloor>" by (simp only:)
1.96    qed
1.97    finally show ?thesis .
```