src/HOL/Isar_Examples/Group.thy
 author haftmann Wed Jun 30 16:46:44 2010 +0200 (2010-06-30) changeset 37659 14cabf5fa710 parent 35317 d57da4abb47d child 37671 fa53d267dab3 permissions -rw-r--r--
more speaking names
     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 {*

    14  Groups over signature $({\times} :: \alpha \To \alpha \To \alpha,   15 \idt{one} :: \alpha, \idt{inverse} :: \alpha \To \alpha)$ are defined

    16  as an axiomatic type class as follows.  Note that the parent class

    17  $\idt{times}$ is provided by the basic HOL theory.

    18 *}

    19

    20 notation Groups.one ("one")

    21

    22 class group = times + one + inverse +

    23   assumes group_assoc:         "(x * y) * z = x * (y * z)"

    24   assumes group_left_one:      "one * x = x"

    25   assumes group_left_inverse:  "inverse x * x = one"

    26

    27 text {*

    28  The group axioms only state the properties of left one and inverse,

    29  the right versions may be derived as follows.

    30 *}

    31

    32 theorem group_right_inverse: "x * inverse x = (one::'a::group)"

    33 proof -

    34   have "x * inverse x = one * (x * inverse x)"

    35     by (simp only: group_left_one)

    36   also have "... = one * x * inverse x"

    37     by (simp only: group_assoc)

    38   also have "... = inverse (inverse x) * inverse x * x * inverse x"

    39     by (simp only: group_left_inverse)

    40   also have "... = inverse (inverse x) * (inverse x * x) * inverse x"

    41     by (simp only: group_assoc)

    42   also have "... = inverse (inverse x) * one * inverse x"

    43     by (simp only: group_left_inverse)

    44   also have "... = inverse (inverse x) * (one * inverse x)"

    45     by (simp only: group_assoc)

    46   also have "... = inverse (inverse x) * inverse x"

    47     by (simp only: group_left_one)

    48   also have "... = one"

    49     by (simp only: group_left_inverse)

    50   finally show ?thesis .

    51 qed

    52

    53 text {*

    54  With \name{group-right-inverse} already available,

    55  \name{group-right-one}\label{thm:group-right-one} is now established

    56  much easier.

    57 *}

    58

    59 theorem group_right_one: "x * one = (x::'a::group)"

    60 proof -

    61   have "x * one = x * (inverse x * x)"

    62     by (simp only: group_left_inverse)

    63   also have "... = x * inverse x * x"

    64     by (simp only: group_assoc)

    65   also have "... = one * x"

    66     by (simp only: group_right_inverse)

    67   also have "... = x"

    68     by (simp only: group_left_one)

    69   finally show ?thesis .

    70 qed

    71

    72 text {*

    73  \medskip The calculational proof style above follows typical

    74  presentations given in any introductory course on algebra.  The basic

    75  technique is to form a transitive chain of equations, which in turn

    76  are established by simplifying with appropriate rules.  The low-level

    77  logical details of equational reasoning are left implicit.

    78

    79  Note that $\dots$'' is just a special term variable that is bound

    80  automatically to the argument\footnote{The argument of a curried

    81  infix expression happens to be its right-hand side.} of the last fact

    82  achieved by any local assumption or proven statement.  In contrast to

    83  $\var{thesis}$, the $\dots$'' variable is bound \emph{after} the

    84  proof is finished, though.

    85

    86  There are only two separate Isar language elements for calculational

    87  proofs: \isakeyword{also}'' for initial or intermediate

    88  calculational steps, and \isakeyword{finally}'' for exhibiting the

    89  result of a calculation.  These constructs are not hardwired into

    90  Isabelle/Isar, but defined on top of the basic Isar/VM interpreter.

    91  Expanding the \isakeyword{also} and \isakeyword{finally} derived

    92  language elements, calculations may be simulated by hand as

    93  demonstrated below.

    94 *}

    95

    96 theorem "x * one = (x::'a::group)"

    97 proof -

    98   have "x * one = x * (inverse x * x)"

    99     by (simp only: group_left_inverse)

   100

   101   note calculation = this

   102     -- {* first calculational step: init calculation register *}

   103

   104   have "... = x * inverse x * x"

   105     by (simp only: group_assoc)

   106

   107   note calculation = trans [OF calculation this]

   108     -- {* general calculational step: compose with transitivity rule *}

   109

   110   have "... = one * x"

   111     by (simp only: group_right_inverse)

   112

   113   note calculation = trans [OF calculation this]

   114     -- {* general calculational step: compose with transitivity rule *}

   115

   116   have "... = x"

   117     by (simp only: group_left_one)

   118

   119   note calculation = trans [OF calculation this]

   120     -- {* final calculational step: compose with transitivity rule ... *}

   121   from calculation

   122     -- {* ... and pick up the final result *}

   123

   124   show ?thesis .

   125 qed

   126

   127 text {*

   128  Note that this scheme of calculations is not restricted to plain

   129  transitivity.  Rules like anti-symmetry, or even forward and backward

   130  substitution work as well.  For the actual implementation of

   131  \isacommand{also} and \isacommand{finally}, Isabelle/Isar maintains

   132  separate context information of transitivity'' rules.  Rule

   133  selection takes place automatically by higher-order unification.

   134 *}

   135

   136

   137 subsection {* Groups as monoids *}

   138

   139 text {*

   140  Monoids over signature $({\times} :: \alpha \To \alpha \To \alpha,   141 \idt{one} :: \alpha)$ are defined like this.

   142 *}

   143

   144 class monoid = times + one +

   145   assumes monoid_assoc:       "(x * y) * z = x * (y * z)"

   146   assumes monoid_left_one:   "one * x = x"

   147   assumes monoid_right_one:  "x * one = x"

   148

   149 text {*

   150  Groups are \emph{not} yet monoids directly from the definition.  For

   151  monoids, \name{right-one} had to be included as an axiom, but for

   152  groups both \name{right-one} and \name{right-inverse} are derivable

   153  from the other axioms.  With \name{group-right-one} derived as a

   154  theorem of group theory (see page~\pageref{thm:group-right-one}), we

   155  may still instantiate $\idt{group} \subseteq \idt{monoid}$ properly

   156  as follows.

   157 *}

   158

   159 instance group < monoid

   160   by (intro_classes,

   161        rule group_assoc,

   162        rule group_left_one,

   163        rule group_right_one)

   164

   165 text {*

   166  The \isacommand{instance} command actually is a version of

   167  \isacommand{theorem}, setting up a goal that reflects the intended

   168  class relation (or type constructor arity).  Thus any Isar proof

   169  language element may be involved to establish this statement.  When

   170  concluding the proof, the result is transformed into the intended

   171  type signature extension behind the scenes.

   172 *}

   173

   174 subsection {* More theorems of group theory *}

   175

   176 text {*

   177  The one element is already uniquely determined by preserving an

   178  \emph{arbitrary} group element.

   179 *}

   180

   181 theorem group_one_equality: "e * x = x ==> one = (e::'a::group)"

   182 proof -

   183   assume eq: "e * x = x"

   184   have "one = x * inverse x"

   185     by (simp only: group_right_inverse)

   186   also have "... = (e * x) * inverse x"

   187     by (simp only: eq)

   188   also have "... = e * (x * inverse x)"

   189     by (simp only: group_assoc)

   190   also have "... = e * one"

   191     by (simp only: group_right_inverse)

   192   also have "... = e"

   193     by (simp only: group_right_one)

   194   finally show ?thesis .

   195 qed

   196

   197 text {*

   198  Likewise, the inverse is already determined by the cancel property.

   199 *}

   200

   201 theorem group_inverse_equality:

   202   "x' * x = one ==> inverse x = (x'::'a::group)"

   203 proof -

   204   assume eq: "x' * x = one"

   205   have "inverse x = one * inverse x"

   206     by (simp only: group_left_one)

   207   also have "... = (x' * x) * inverse x"

   208     by (simp only: eq)

   209   also have "... = x' * (x * inverse x)"

   210     by (simp only: group_assoc)

   211   also have "... = x' * one"

   212     by (simp only: group_right_inverse)

   213   also have "... = x'"

   214     by (simp only: group_right_one)

   215   finally show ?thesis .

   216 qed

   217

   218 text {*

   219  The inverse operation has some further characteristic properties.

   220 *}

   221

   222 theorem group_inverse_times:

   223   "inverse (x * y) = inverse y * inverse (x::'a::group)"

   224 proof (rule group_inverse_equality)

   225   show "(inverse y * inverse x) * (x * y) = one"

   226   proof -

   227     have "(inverse y * inverse x) * (x * y) =

   228         (inverse y * (inverse x * x)) * y"

   229       by (simp only: group_assoc)

   230     also have "... = (inverse y * one) * y"

   231       by (simp only: group_left_inverse)

   232     also have "... = inverse y * y"

   233       by (simp only: group_right_one)

   234     also have "... = one"

   235       by (simp only: group_left_inverse)

   236     finally show ?thesis .

   237   qed

   238 qed

   239

   240 theorem inverse_inverse: "inverse (inverse x) = (x::'a::group)"

   241 proof (rule group_inverse_equality)

   242   show "x * inverse x = one"

   243     by (simp only: group_right_inverse)

   244 qed

   245

   246 theorem inverse_inject: "inverse x = inverse y ==> x = (y::'a::group)"

   247 proof -

   248   assume eq: "inverse x = inverse y"

   249   have "x = x * one"

   250     by (simp only: group_right_one)

   251   also have "... = x * (inverse y * y)"

   252     by (simp only: group_left_inverse)

   253   also have "... = x * (inverse x * y)"

   254     by (simp only: eq)

   255   also have "... = (x * inverse x) * y"

   256     by (simp only: group_assoc)

   257   also have "... = one * y"

   258     by (simp only: group_right_inverse)

   259   also have "... = y"

   260     by (simp only: group_left_one)

   261   finally show ?thesis .

   262 qed

   263

   264 end