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