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