src/HOL/Isar_Examples/Group.thy
 author haftmann Tue Feb 23 10:11:15 2010 +0100 (2010-02-23) changeset 35317 d57da4abb47d parent 33026 8f35633c4922 child 37671 fa53d267dab3 permissions -rw-r--r--
dropped axclass; dropped Id
 wenzelm@33026  1 (* Title: HOL/Isar_Examples/Group.thy  wenzelm@6763  2  Author: Markus Wenzel, TU Muenchen  wenzelm@6763  3 *)  wenzelm@6763  4 wenzelm@10007  5 header {* Basic group theory *}  wenzelm@7748  6 wenzelm@31758  7 theory Group  wenzelm@31758  8 imports Main  wenzelm@31758  9 begin  wenzelm@6763  10 wenzelm@10007  11 subsection {* Groups and calculational reasoning *}  wenzelm@6784  12 wenzelm@6784  13 text {*  wenzelm@7968  14  Groups over signature $({\times} :: \alpha \To \alpha \To \alpha,  wenzelm@10141  15  \idt{one} :: \alpha, \idt{inverse} :: \alpha \To \alpha)$ are defined  wenzelm@10141  16  as an axiomatic type class as follows. Note that the parent class  wenzelm@7968  17  $\idt{times}$ is provided by the basic HOL theory.  wenzelm@10007  18 *}  wenzelm@6763  19 haftmann@35317  20 notation Groups.one ("one")  wenzelm@6763  21 haftmann@35317  22 class group = times + one + inverse +  haftmann@35317  23  assumes group_assoc: "(x * y) * z = x * (y * z)"  haftmann@35317  24  assumes group_left_one: "one * x = x"  haftmann@35317  25  assumes group_left_inverse: "inverse x * x = one"  wenzelm@6763  26 wenzelm@6784  27 text {*  wenzelm@10141  28  The group axioms only state the properties of left one and inverse,  wenzelm@7874  29  the right versions may be derived as follows.  wenzelm@10007  30 *}  wenzelm@6763  31 wenzelm@10141  32 theorem group_right_inverse: "x * inverse x = (one::'a::group)"  wenzelm@10007  33 proof -  wenzelm@10141  34  have "x * inverse x = one * (x * inverse x)"  wenzelm@10141  35  by (simp only: group_left_one)  wenzelm@10141  36  also have "... = one * x * inverse x"  wenzelm@10007  37  by (simp only: group_assoc)  wenzelm@10141  38  also have "... = inverse (inverse x) * inverse x * x * inverse x"  wenzelm@10007  39  by (simp only: group_left_inverse)  wenzelm@10141  40  also have "... = inverse (inverse x) * (inverse x * x) * inverse x"  wenzelm@10007  41  by (simp only: group_assoc)  wenzelm@10141  42  also have "... = inverse (inverse x) * one * inverse x"  wenzelm@10007  43  by (simp only: group_left_inverse)  wenzelm@10141  44  also have "... = inverse (inverse x) * (one * inverse x)"  wenzelm@10007  45  by (simp only: group_assoc)  wenzelm@10141  46  also have "... = inverse (inverse x) * inverse x"  wenzelm@10141  47  by (simp only: group_left_one)  wenzelm@10007  48  also have "... = one"  wenzelm@10007  49  by (simp only: group_left_inverse)  wenzelm@10007  50  finally show ?thesis .  wenzelm@10007  51 qed  wenzelm@6763  52 wenzelm@6784  53 text {*  wenzelm@7982  54  With \name{group-right-inverse} already available,  wenzelm@10141  55  \name{group-right-one}\label{thm:group-right-one} is now established  wenzelm@10141  56  much easier.  wenzelm@10007  57 *}  wenzelm@6763  58 wenzelm@10141  59 theorem group_right_one: "x * one = (x::'a::group)"  wenzelm@10007  60 proof -  wenzelm@10141  61  have "x * one = x * (inverse x * x)"  wenzelm@10007  62  by (simp only: group_left_inverse)  wenzelm@10141  63  also have "... = x * inverse x * x"  wenzelm@10007  64  by (simp only: group_assoc)  wenzelm@10007  65  also have "... = one * x"  wenzelm@10007  66  by (simp only: group_right_inverse)  wenzelm@10007  67  also have "... = x"  wenzelm@10141  68  by (simp only: group_left_one)  wenzelm@10007  69  finally show ?thesis .  wenzelm@10007  70 qed  wenzelm@6763  71 wenzelm@6784  72 text {*  wenzelm@7874  73  \medskip The calculational proof style above follows typical  wenzelm@7874  74  presentations given in any introductory course on algebra. The basic  wenzelm@7874  75  technique is to form a transitive chain of equations, which in turn  wenzelm@7874  76  are established by simplifying with appropriate rules. The low-level  wenzelm@7982  77  logical details of equational reasoning are left implicit.  wenzelm@6784  78 wenzelm@7982  79  Note that $\dots$'' is just a special term variable that is bound  wenzelm@7982  80  automatically to the argument\footnote{The argument of a curried  wenzelm@7982  81  infix expression happens to be its right-hand side.} of the last fact  wenzelm@7982  82  achieved by any local assumption or proven statement. In contrast to  wenzelm@7982  83  $\var{thesis}$, the $\dots$'' variable is bound \emph{after} the  wenzelm@7982  84  proof is finished, though.  wenzelm@7874  85 wenzelm@7874  86  There are only two separate Isar language elements for calculational  wenzelm@7874  87  proofs: \isakeyword{also}'' for initial or intermediate  wenzelm@7874  88  calculational steps, and \isakeyword{finally}'' for exhibiting the  wenzelm@7874  89  result of a calculation. These constructs are not hardwired into  wenzelm@7874  90  Isabelle/Isar, but defined on top of the basic Isar/VM interpreter.  wenzelm@7874  91  Expanding the \isakeyword{also} and \isakeyword{finally} derived  wenzelm@7982  92  language elements, calculations may be simulated by hand as  wenzelm@7982  93  demonstrated below.  wenzelm@10007  94 *}  wenzelm@6784  95 wenzelm@10007  96 theorem "x * one = (x::'a::group)"  wenzelm@10007  97 proof -  wenzelm@10141  98  have "x * one = x * (inverse x * x)"  wenzelm@10007  99  by (simp only: group_left_inverse)  wenzelm@6763  100 wenzelm@7433  101  note calculation = this  wenzelm@10007  102  -- {* first calculational step: init calculation register *}  wenzelm@6763  103 wenzelm@10141  104  have "... = x * inverse x * x"  wenzelm@10007  105  by (simp only: group_assoc)  wenzelm@6763  106 wenzelm@7433  107  note calculation = trans [OF calculation this]  wenzelm@10007  108  -- {* general calculational step: compose with transitivity rule *}  wenzelm@6763  109 wenzelm@10007  110  have "... = one * x"  wenzelm@10007  111  by (simp only: group_right_inverse)  wenzelm@6763  112 wenzelm@7433  113  note calculation = trans [OF calculation this]  wenzelm@10007  114  -- {* general calculational step: compose with transitivity rule *}  wenzelm@6763  115 wenzelm@10007  116  have "... = x"  wenzelm@10141  117  by (simp only: group_left_one)  wenzelm@6763  118 wenzelm@7433  119  note calculation = trans [OF calculation this]  wenzelm@10007  120  -- {* final calculational step: compose with transitivity rule ... *}  wenzelm@6784  121  from calculation  wenzelm@10007  122  -- {* ... and pick up the final result *}  wenzelm@6763  123 wenzelm@10007  124  show ?thesis .  wenzelm@10007  125 qed  wenzelm@6763  126 wenzelm@7874  127 text {*  wenzelm@7874  128  Note that this scheme of calculations is not restricted to plain  wenzelm@7874  129  transitivity. Rules like anti-symmetry, or even forward and backward  wenzelm@7982  130  substitution work as well. For the actual implementation of  wenzelm@7982  131  \isacommand{also} and \isacommand{finally}, Isabelle/Isar maintains  wenzelm@7982  132  separate context information of transitivity'' rules. Rule  wenzelm@7982  133  selection takes place automatically by higher-order unification.  wenzelm@10007  134 *}  wenzelm@7874  135 wenzelm@6763  136 wenzelm@10007  137 subsection {* Groups as monoids *}  wenzelm@6793  138 wenzelm@6793  139 text {*  wenzelm@7874  140  Monoids over signature $({\times} :: \alpha \To \alpha \To \alpha,  wenzelm@7874  141  \idt{one} :: \alpha)$ are defined like this.  wenzelm@10007  142 *}  wenzelm@6793  143 haftmann@35317  144 class monoid = times + one +  haftmann@35317  145  assumes monoid_assoc: "(x * y) * z = x * (y * z)"  haftmann@35317  146  assumes monoid_left_one: "one * x = x"  haftmann@35317  147  assumes monoid_right_one: "x * one = x"  wenzelm@6793  148 wenzelm@6793  149 text {*  wenzelm@7748  150  Groups are \emph{not} yet monoids directly from the definition. For  wenzelm@10141  151  monoids, \name{right-one} had to be included as an axiom, but for  wenzelm@10141  152  groups both \name{right-one} and \name{right-inverse} are derivable  wenzelm@10141  153  from the other axioms. With \name{group-right-one} derived as a  wenzelm@10141  154  theorem of group theory (see page~\pageref{thm:group-right-one}), we  wenzelm@10141  155  may still instantiate $\idt{group} \subseteq \idt{monoid}$ properly  wenzelm@10141  156  as follows.  wenzelm@10007  157 *}  wenzelm@6793  158 wenzelm@10007  159 instance group < monoid  wenzelm@7356  160  by (intro_classes,  wenzelm@6793  161  rule group_assoc,  wenzelm@10141  162  rule group_left_one,  wenzelm@10141  163  rule group_right_one)  wenzelm@6793  164 wenzelm@7874  165 text {*  wenzelm@7874  166  The \isacommand{instance} command actually is a version of  wenzelm@7874  167  \isacommand{theorem}, setting up a goal that reflects the intended  wenzelm@7874  168  class relation (or type constructor arity). Thus any Isar proof  wenzelm@7874  169  language element may be involved to establish this statement. When  wenzelm@7982  170  concluding the proof, the result is transformed into the intended  wenzelm@7874  171  type signature extension behind the scenes.  wenzelm@10007  172 *}  wenzelm@7874  173 wenzelm@10141  174 subsection {* More theorems of group theory *}  wenzelm@10141  175 wenzelm@10141  176 text {*  wenzelm@10141  177  The one element is already uniquely determined by preserving an  wenzelm@10141  178  \emph{arbitrary} group element.  wenzelm@10141  179 *}  wenzelm@10141  180 wenzelm@10141  181 theorem group_one_equality: "e * x = x ==> one = (e::'a::group)"  wenzelm@10141  182 proof -  wenzelm@10141  183  assume eq: "e * x = x"  wenzelm@10141  184  have "one = x * inverse x"  wenzelm@10141  185  by (simp only: group_right_inverse)  wenzelm@10141  186  also have "... = (e * x) * inverse x"  wenzelm@10141  187  by (simp only: eq)  wenzelm@10141  188  also have "... = e * (x * inverse x)"  wenzelm@10141  189  by (simp only: group_assoc)  wenzelm@10141  190  also have "... = e * one"  wenzelm@10141  191  by (simp only: group_right_inverse)  wenzelm@10141  192  also have "... = e"  wenzelm@10141  193  by (simp only: group_right_one)  wenzelm@10141  194  finally show ?thesis .  wenzelm@10141  195 qed  wenzelm@10141  196 wenzelm@10141  197 text {*  wenzelm@10141  198  Likewise, the inverse is already determined by the cancel property.  wenzelm@10141  199 *}  wenzelm@10141  200 wenzelm@10141  201 theorem group_inverse_equality:  wenzelm@10141  202  "x' * x = one ==> inverse x = (x'::'a::group)"  wenzelm@10141  203 proof -  wenzelm@10141  204  assume eq: "x' * x = one"  wenzelm@10141  205  have "inverse x = one * inverse x"  wenzelm@10141  206  by (simp only: group_left_one)  wenzelm@10141  207  also have "... = (x' * x) * inverse x"  wenzelm@10141  208  by (simp only: eq)  wenzelm@10141  209  also have "... = x' * (x * inverse x)"  wenzelm@10141  210  by (simp only: group_assoc)  wenzelm@10141  211  also have "... = x' * one"  wenzelm@10141  212  by (simp only: group_right_inverse)  wenzelm@10141  213  also have "... = x'"  wenzelm@10141  214  by (simp only: group_right_one)  wenzelm@10141  215  finally show ?thesis .  wenzelm@10141  216 qed  wenzelm@10141  217 wenzelm@10141  218 text {*  wenzelm@10141  219  The inverse operation has some further characteristic properties.  wenzelm@10141  220 *}  wenzelm@10141  221 wenzelm@10141  222 theorem group_inverse_times:  wenzelm@10141  223  "inverse (x * y) = inverse y * inverse (x::'a::group)"  wenzelm@10141  224 proof (rule group_inverse_equality)  wenzelm@10141  225  show "(inverse y * inverse x) * (x * y) = one"  wenzelm@10141  226  proof -  wenzelm@10141  227  have "(inverse y * inverse x) * (x * y) =  wenzelm@10141  228  (inverse y * (inverse x * x)) * y"  wenzelm@10141  229  by (simp only: group_assoc)  wenzelm@10141  230  also have "... = (inverse y * one) * y"  wenzelm@10141  231  by (simp only: group_left_inverse)  wenzelm@10141  232  also have "... = inverse y * y"  wenzelm@10141  233  by (simp only: group_right_one)  wenzelm@10141  234  also have "... = one"  wenzelm@10141  235  by (simp only: group_left_inverse)  wenzelm@10141  236  finally show ?thesis .  wenzelm@10141  237  qed  wenzelm@10141  238 qed  wenzelm@10141  239 wenzelm@10141  240 theorem inverse_inverse: "inverse (inverse x) = (x::'a::group)"  wenzelm@10141  241 proof (rule group_inverse_equality)  wenzelm@10141  242  show "x * inverse x = one"  wenzelm@10141  243  by (simp only: group_right_inverse)  wenzelm@10141  244 qed  wenzelm@10141  245 wenzelm@10141  246 theorem inverse_inject: "inverse x = inverse y ==> x = (y::'a::group)"  wenzelm@10141  247 proof -  wenzelm@10141  248  assume eq: "inverse x = inverse y"  wenzelm@10141  249  have "x = x * one"  wenzelm@10141  250  by (simp only: group_right_one)  wenzelm@10141  251  also have "... = x * (inverse y * y)"  wenzelm@10141  252  by (simp only: group_left_inverse)  wenzelm@10141  253  also have "... = x * (inverse x * y)"  wenzelm@10141  254  by (simp only: eq)  wenzelm@10141  255  also have "... = (x * inverse x) * y"  wenzelm@10141  256  by (simp only: group_assoc)  wenzelm@10141  257  also have "... = one * y"  wenzelm@10141  258  by (simp only: group_right_inverse)  wenzelm@10141  259  also have "... = y"  wenzelm@10141  260  by (simp only: group_left_one)  wenzelm@10141  261  finally show ?thesis .  wenzelm@10141  262 qed  wenzelm@10141  263 wenzelm@10141  264 end