summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Isar_Examples/Group.thy

changeset 55656 | eb07b0acbebc |

parent 37671 | fa53d267dab3 |

child 58614 | 7338eb25226c |

1.1 --- a/src/HOL/Isar_Examples/Group.thy Fri Feb 21 17:06:48 2014 +0100 1.2 +++ b/src/HOL/Isar_Examples/Group.thy Fri Feb 21 18:23:11 2014 +0100 1.3 @@ -27,19 +27,19 @@ 1.4 proof - 1.5 have "x * inverse x = 1 * (x * inverse x)" 1.6 by (simp only: group_left_one) 1.7 - also have "... = 1 * x * inverse x" 1.8 + also have "\<dots> = 1 * x * inverse x" 1.9 by (simp only: group_assoc) 1.10 - also have "... = inverse (inverse x) * inverse x * x * inverse x" 1.11 + also have "\<dots> = inverse (inverse x) * inverse x * x * inverse x" 1.12 by (simp only: group_left_inverse) 1.13 - also have "... = inverse (inverse x) * (inverse x * x) * inverse x" 1.14 + also have "\<dots> = inverse (inverse x) * (inverse x * x) * inverse x" 1.15 by (simp only: group_assoc) 1.16 - also have "... = inverse (inverse x) * 1 * inverse x" 1.17 + also have "\<dots> = inverse (inverse x) * 1 * inverse x" 1.18 by (simp only: group_left_inverse) 1.19 - also have "... = inverse (inverse x) * (1 * inverse x)" 1.20 + also have "\<dots> = inverse (inverse x) * (1 * inverse x)" 1.21 by (simp only: group_assoc) 1.22 - also have "... = inverse (inverse x) * inverse x" 1.23 + also have "\<dots> = inverse (inverse x) * inverse x" 1.24 by (simp only: group_left_one) 1.25 - also have "... = 1" 1.26 + also have "\<dots> = 1" 1.27 by (simp only: group_left_inverse) 1.28 finally show ?thesis . 1.29 qed 1.30 @@ -52,11 +52,11 @@ 1.31 proof - 1.32 have "x * 1 = x * (inverse x * x)" 1.33 by (simp only: group_left_inverse) 1.34 - also have "... = x * inverse x * x" 1.35 + also have "\<dots> = x * inverse x * x" 1.36 by (simp only: group_assoc) 1.37 - also have "... = 1 * x" 1.38 + also have "\<dots> = 1 * x" 1.39 by (simp only: group_right_inverse) 1.40 - also have "... = x" 1.41 + also have "\<dots> = x" 1.42 by (simp only: group_left_one) 1.43 finally show ?thesis . 1.44 qed 1.45 @@ -92,25 +92,25 @@ 1.46 note calculation = this 1.47 -- {* first calculational step: init calculation register *} 1.48 1.49 - have "... = x * inverse x * x" 1.50 + have "\<dots> = x * inverse x * x" 1.51 by (simp only: group_assoc) 1.52 1.53 note calculation = trans [OF calculation this] 1.54 -- {* general calculational step: compose with transitivity rule *} 1.55 1.56 - have "... = 1 * x" 1.57 + have "\<dots> = 1 * x" 1.58 by (simp only: group_right_inverse) 1.59 1.60 note calculation = trans [OF calculation this] 1.61 -- {* general calculational step: compose with transitivity rule *} 1.62 1.63 - have "... = x" 1.64 + have "\<dots> = x" 1.65 by (simp only: group_left_one) 1.66 1.67 note calculation = trans [OF calculation this] 1.68 - -- {* final calculational step: compose with transitivity rule ... *} 1.69 + -- {* final calculational step: compose with transitivity rule \dots *} 1.70 from calculation 1.71 - -- {* ... and pick up the final result *} 1.72 + -- {* \dots\ and pick up the final result *} 1.73 1.74 show ?thesis . 1.75 qed 1.76 @@ -168,13 +168,13 @@ 1.77 proof - 1.78 have "1 = x * inverse x" 1.79 by (simp only: group_right_inverse) 1.80 - also have "... = (e * x) * inverse x" 1.81 + also have "\<dots> = (e * x) * inverse x" 1.82 by (simp only: eq) 1.83 - also have "... = e * (x * inverse x)" 1.84 + also have "\<dots> = e * (x * inverse x)" 1.85 by (simp only: group_assoc) 1.86 - also have "... = e * 1" 1.87 + also have "\<dots> = e * 1" 1.88 by (simp only: group_right_inverse) 1.89 - also have "... = e" 1.90 + also have "\<dots> = e" 1.91 by (simp only: group_right_one) 1.92 finally show ?thesis . 1.93 qed 1.94 @@ -187,13 +187,13 @@ 1.95 proof - 1.96 have "inverse x = 1 * inverse x" 1.97 by (simp only: group_left_one) 1.98 - also have "... = (x' * x) * inverse x" 1.99 + also have "\<dots> = (x' * x) * inverse x" 1.100 by (simp only: eq) 1.101 - also have "... = x' * (x * inverse x)" 1.102 + also have "\<dots> = x' * (x * inverse x)" 1.103 by (simp only: group_assoc) 1.104 - also have "... = x' * 1" 1.105 + also have "\<dots> = x' * 1" 1.106 by (simp only: group_right_inverse) 1.107 - also have "... = x'" 1.108 + also have "\<dots> = x'" 1.109 by (simp only: group_right_one) 1.110 finally show ?thesis . 1.111 qed 1.112 @@ -207,11 +207,11 @@ 1.113 have "(inverse y * inverse x) * (x * y) = 1.114 (inverse y * (inverse x * x)) * y" 1.115 by (simp only: group_assoc) 1.116 - also have "... = (inverse y * 1) * y" 1.117 + also have "\<dots> = (inverse y * 1) * y" 1.118 by (simp only: group_left_inverse) 1.119 - also have "... = inverse y * y" 1.120 + also have "\<dots> = inverse y * y" 1.121 by (simp only: group_right_one) 1.122 - also have "... = 1" 1.123 + also have "\<dots> = 1" 1.124 by (simp only: group_left_inverse) 1.125 finally show ?thesis . 1.126 qed 1.127 @@ -229,15 +229,15 @@ 1.128 proof - 1.129 have "x = x * 1" 1.130 by (simp only: group_right_one) 1.131 - also have "... = x * (inverse y * y)" 1.132 + also have "\<dots> = x * (inverse y * y)" 1.133 by (simp only: group_left_inverse) 1.134 - also have "... = x * (inverse x * y)" 1.135 + also have "\<dots> = x * (inverse x * y)" 1.136 by (simp only: eq) 1.137 - also have "... = (x * inverse x) * y" 1.138 + also have "\<dots> = (x * inverse x) * y" 1.139 by (simp only: group_assoc) 1.140 - also have "... = 1 * y" 1.141 + also have "\<dots> = 1 * y" 1.142 by (simp only: group_right_inverse) 1.143 - also have "... = y" 1.144 + also have "\<dots> = y" 1.145 by (simp only: group_left_one) 1.146 finally show ?thesis . 1.147 qed