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 .