src/HOL/Isar_examples/Group.thy
 author obua Mon Apr 10 16:00:34 2006 +0200 (2006-04-10) changeset 19404 9bf2cdc9e8e8 parent 16417 9bc16273c2d4 child 31758 3edd5f813f01 permissions -rw-r--r--
Moved stuff from Ring_and_Field to Matrix
     1 (*  Title:      HOL/Isar_examples/Group.thy

     2     ID:         $Id$

     3     Author:     Markus Wenzel, TU Muenchen

     4 *)

     5

     6 header {* Basic group theory *}

     7

     8 theory Group imports Main begin

     9

    10 subsection {* Groups and calculational reasoning *}

    11

    12 text {*

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

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

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

    17 *}

    18

    19 consts

    20   one :: "'a"

    21   inverse :: "'a => 'a"

    22

    23 axclass

    24   group < times

    25   group_assoc:         "(x * y) * z = x * (y * z)"

    26   group_left_one:      "one * x = x"

    27   group_left_inverse:  "inverse x * x = one"

    28

    29 text {*

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

    31  the right versions may be derived as follows.

    32 *}

    33

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

    35 proof -

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

    37     by (simp only: group_left_one)

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

    39     by (simp only: group_assoc)

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

    41     by (simp only: group_left_inverse)

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

    43     by (simp only: group_assoc)

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

    45     by (simp only: group_left_inverse)

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

    47     by (simp only: group_assoc)

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

    49     by (simp only: group_left_one)

    50   also have "... = one"

    51     by (simp only: group_left_inverse)

    52   finally show ?thesis .

    53 qed

    54

    55 text {*

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

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

    58  much easier.

    59 *}

    60

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

    62 proof -

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

    64     by (simp only: group_left_inverse)

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

    66     by (simp only: group_assoc)

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

    68     by (simp only: group_right_inverse)

    69   also have "... = x"

    70     by (simp only: group_left_one)

    71   finally show ?thesis .

    72 qed

    73

    74 text {*

    75  \medskip The calculational proof style above follows typical

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

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

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

    79  logical details of equational reasoning are left implicit.

    80

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

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

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

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

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

    86  proof is finished, though.

    87

    88  There are only two separate Isar language elements for calculational

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

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

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

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

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

    94  language elements, calculations may be simulated by hand as

    95  demonstrated below.

    96 *}

    97

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

    99 proof -

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

   101     by (simp only: group_left_inverse)

   102

   103   note calculation = this

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

   105

   106   have "... = x * inverse x * x"

   107     by (simp only: group_assoc)

   108

   109   note calculation = trans [OF calculation this]

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

   111

   112   have "... = one * x"

   113     by (simp only: group_right_inverse)

   114

   115   note calculation = trans [OF calculation this]

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

   117

   118   have "... = x"

   119     by (simp only: group_left_one)

   120

   121   note calculation = trans [OF calculation this]

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

   123   from calculation

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

   125

   126   show ?thesis .

   127 qed

   128

   129 text {*

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

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

   132  substitution work as well.  For the actual implementation of

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

   134  separate context information of transitivity'' rules.  Rule

   135  selection takes place automatically by higher-order unification.

   136 *}

   137

   138

   139 subsection {* Groups as monoids *}

   140

   141 text {*

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

   144 *}

   145

   146 axclass monoid < times

   147   monoid_assoc:       "(x * y) * z = x * (y * z)"

   148   monoid_left_one:   "one * x = x"

   149   monoid_right_one:  "x * one = x"

   150

   151 text {*

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

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

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

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

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

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

   158  as follows.

   159 *}

   160

   161 instance group < monoid

   162   by (intro_classes,

   163        rule group_assoc,

   164        rule group_left_one,

   165        rule group_right_one)

   166

   167 text {*

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

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

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

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

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

   173  type signature extension behind the scenes.

   174 *}

   175

   176 subsection {* More theorems of group theory *}

   177

   178 text {*

   179  The one element is already uniquely determined by preserving an

   180  \emph{arbitrary} group element.

   181 *}

   182

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

   184 proof -

   185   assume eq: "e * x = x"

   186   have "one = x * inverse x"

   187     by (simp only: group_right_inverse)

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

   189     by (simp only: eq)

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

   191     by (simp only: group_assoc)

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

   193     by (simp only: group_right_inverse)

   194   also have "... = e"

   195     by (simp only: group_right_one)

   196   finally show ?thesis .

   197 qed

   198

   199 text {*

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

   201 *}

   202

   203 theorem group_inverse_equality:

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

   205 proof -

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

   207   have "inverse x = one * inverse x"

   208     by (simp only: group_left_one)

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

   210     by (simp only: eq)

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

   212     by (simp only: group_assoc)

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

   214     by (simp only: group_right_inverse)

   215   also have "... = x'"

   216     by (simp only: group_right_one)

   217   finally show ?thesis .

   218 qed

   219

   220 text {*

   221  The inverse operation has some further characteristic properties.

   222 *}

   223

   224 theorem group_inverse_times:

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

   226 proof (rule group_inverse_equality)

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

   228   proof -

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

   230         (inverse y * (inverse x * x)) * y"

   231       by (simp only: group_assoc)

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

   233       by (simp only: group_left_inverse)

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

   235       by (simp only: group_right_one)

   236     also have "... = one"

   237       by (simp only: group_left_inverse)

   238     finally show ?thesis .

   239   qed

   240 qed

   241

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

   243 proof (rule group_inverse_equality)

   244   show "x * inverse x = one"

   245     by (simp only: group_right_inverse)

   246 qed

   247

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

   249 proof -

   250   assume eq: "inverse x = inverse y"

   251   have "x = x * one"

   252     by (simp only: group_right_one)

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

   254     by (simp only: group_left_inverse)

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

   256     by (simp only: eq)

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

   258     by (simp only: group_assoc)

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

   260     by (simp only: group_right_inverse)

   261   also have "... = y"

   262     by (simp only: group_left_one)

   263   finally show ?thesis .

   264 qed

   265

   266 end