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

src/HOL/Isar_Examples/Group.thy

changeset 58614 | 7338eb25226c |

parent 55656 | eb07b0acbebc |

child 58882 | 6e2010ab8bd9 |

1.1 --- a/src/HOL/Isar_Examples/Group.thy Tue Oct 07 20:43:18 2014 +0200 1.2 +++ b/src/HOL/Isar_Examples/Group.thy Tue Oct 07 20:59:46 2014 +0200 1.3 @@ -2,26 +2,26 @@ 1.4 Author: Markus Wenzel, TU Muenchen 1.5 *) 1.6 1.7 -header {* Basic group theory *} 1.8 +header \<open>Basic group theory\<close> 1.9 1.10 theory Group 1.11 imports Main 1.12 begin 1.13 1.14 -subsection {* Groups and calculational reasoning *} 1.15 +subsection \<open>Groups and calculational reasoning\<close> 1.16 1.17 -text {* Groups over signature $({\times} :: \alpha \To \alpha \To 1.18 +text \<open>Groups over signature $({\times} :: \alpha \To \alpha \To 1.19 \alpha, \idt{one} :: \alpha, \idt{inverse} :: \alpha \To \alpha)$ 1.20 are defined as an axiomatic type class as follows. Note that the 1.21 - parent class $\idt{times}$ is provided by the basic HOL theory. *} 1.22 + parent class $\idt{times}$ is provided by the basic HOL theory.\<close> 1.23 1.24 class group = times + one + inverse + 1.25 assumes group_assoc: "(x * y) * z = x * (y * z)" 1.26 and group_left_one: "1 * x = x" 1.27 and group_left_inverse: "inverse x * x = 1" 1.28 1.29 -text {* The group axioms only state the properties of left one and 1.30 - inverse, the right versions may be derived as follows. *} 1.31 +text \<open>The group axioms only state the properties of left one and 1.32 + inverse, the right versions may be derived as follows.\<close> 1.33 1.34 theorem (in group) group_right_inverse: "x * inverse x = 1" 1.35 proof - 1.36 @@ -44,9 +44,9 @@ 1.37 finally show ?thesis . 1.38 qed 1.39 1.40 -text {* With \name{group-right-inverse} already available, 1.41 +text \<open>With \name{group-right-inverse} already available, 1.42 \name{group-right-one}\label{thm:group-right-one} is now established 1.43 - much easier. *} 1.44 + much easier.\<close> 1.45 1.46 theorem (in group) group_right_one: "x * 1 = x" 1.47 proof - 1.48 @@ -61,7 +61,7 @@ 1.49 finally show ?thesis . 1.50 qed 1.51 1.52 -text {* \medskip The calculational proof style above follows typical 1.53 +text \<open>\medskip The calculational proof style above follows typical 1.54 presentations given in any introductory course on algebra. The 1.55 basic technique is to form a transitive chain of equations, which in 1.56 turn are established by simplifying with appropriate rules. The 1.57 @@ -81,8 +81,7 @@ 1.58 Isabelle/Isar, but defined on top of the basic Isar/VM interpreter. 1.59 Expanding the \isakeyword{also} and \isakeyword{finally} derived 1.60 language elements, calculations may be simulated by hand as 1.61 - demonstrated below. 1.62 -*} 1.63 + demonstrated below.\<close> 1.64 1.65 theorem (in group) "x * 1 = x" 1.66 proof - 1.67 @@ -90,58 +89,57 @@ 1.68 by (simp only: group_left_inverse) 1.69 1.70 note calculation = this 1.71 - -- {* first calculational step: init calculation register *} 1.72 + -- \<open>first calculational step: init calculation register\<close> 1.73 1.74 have "\<dots> = x * inverse x * x" 1.75 by (simp only: group_assoc) 1.76 1.77 note calculation = trans [OF calculation this] 1.78 - -- {* general calculational step: compose with transitivity rule *} 1.79 + -- \<open>general calculational step: compose with transitivity rule\<close> 1.80 1.81 have "\<dots> = 1 * x" 1.82 by (simp only: group_right_inverse) 1.83 1.84 note calculation = trans [OF calculation this] 1.85 - -- {* general calculational step: compose with transitivity rule *} 1.86 + -- \<open>general calculational step: compose with transitivity rule\<close> 1.87 1.88 have "\<dots> = x" 1.89 by (simp only: group_left_one) 1.90 1.91 note calculation = trans [OF calculation this] 1.92 - -- {* final calculational step: compose with transitivity rule \dots *} 1.93 + -- \<open>final calculational step: compose with transitivity rule \dots\<close> 1.94 from calculation 1.95 - -- {* \dots\ and pick up the final result *} 1.96 + -- \<open>\dots\ and pick up the final result\<close> 1.97 1.98 show ?thesis . 1.99 qed 1.100 1.101 -text {* Note that this scheme of calculations is not restricted to 1.102 +text \<open>Note that this scheme of calculations is not restricted to 1.103 plain transitivity. Rules like anti-symmetry, or even forward and 1.104 backward substitution work as well. For the actual implementation 1.105 of \isacommand{also} and \isacommand{finally}, Isabelle/Isar 1.106 maintains separate context information of ``transitivity'' rules. 1.107 Rule selection takes place automatically by higher-order 1.108 - unification. *} 1.109 + unification.\<close> 1.110 1.111 1.112 -subsection {* Groups as monoids *} 1.113 +subsection \<open>Groups as monoids\<close> 1.114 1.115 -text {* Monoids over signature $({\times} :: \alpha \To \alpha \To 1.116 - \alpha, \idt{one} :: \alpha)$ are defined like this. 1.117 -*} 1.118 +text \<open>Monoids over signature $({\times} :: \alpha \To \alpha \To 1.119 + \alpha, \idt{one} :: \alpha)$ are defined like this.\<close> 1.120 1.121 class monoid = times + one + 1.122 assumes monoid_assoc: "(x * y) * z = x * (y * z)" 1.123 and monoid_left_one: "1 * x = x" 1.124 and monoid_right_one: "x * 1 = x" 1.125 1.126 -text {* Groups are \emph{not} yet monoids directly from the 1.127 +text \<open>Groups are \emph{not} yet monoids directly from the 1.128 definition. For monoids, \name{right-one} had to be included as an 1.129 axiom, but for groups both \name{right-one} and \name{right-inverse} 1.130 are derivable from the other axioms. With \name{group-right-one} 1.131 derived as a theorem of group theory (see 1.132 page~\pageref{thm:group-right-one}), we may still instantiate 1.133 - $\idt{group} \subseteq \idt{monoid}$ properly as follows. *} 1.134 + $\idt{group} \subseteq \idt{monoid}$ properly as follows.\<close> 1.135 1.136 instance group < monoid 1.137 by intro_classes 1.138 @@ -149,18 +147,18 @@ 1.139 rule group_left_one, 1.140 rule group_right_one) 1.141 1.142 -text {* The \isacommand{instance} command actually is a version of 1.143 +text \<open>The \isacommand{instance} command actually is a version of 1.144 \isacommand{theorem}, setting up a goal that reflects the intended 1.145 class relation (or type constructor arity). Thus any Isar proof 1.146 language element may be involved to establish this statement. When 1.147 concluding the proof, the result is transformed into the intended 1.148 - type signature extension behind the scenes. *} 1.149 + type signature extension behind the scenes.\<close> 1.150 1.151 1.152 -subsection {* More theorems of group theory *} 1.153 +subsection \<open>More theorems of group theory\<close> 1.154 1.155 -text {* The one element is already uniquely determined by preserving 1.156 - an \emph{arbitrary} group element. *} 1.157 +text \<open>The one element is already uniquely determined by preserving 1.158 + an \emph{arbitrary} group element.\<close> 1.159 1.160 theorem (in group) group_one_equality: 1.161 assumes eq: "e * x = x" 1.162 @@ -179,7 +177,7 @@ 1.163 finally show ?thesis . 1.164 qed 1.165 1.166 -text {* Likewise, the inverse is already determined by the cancel property. *} 1.167 +text \<open>Likewise, the inverse is already determined by the cancel property.\<close> 1.168 1.169 theorem (in group) group_inverse_equality: 1.170 assumes eq: "x' * x = 1" 1.171 @@ -198,7 +196,7 @@ 1.172 finally show ?thesis . 1.173 qed 1.174 1.175 -text {* The inverse operation has some further characteristic properties. *} 1.176 +text \<open>The inverse operation has some further characteristic properties.\<close> 1.177 1.178 theorem (in group) group_inverse_times: "inverse (x * y) = inverse y * inverse x" 1.179 proof (rule group_inverse_equality)