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