src/HOL/Isar_Examples/Group.thy
 author blanchet Thu Sep 11 18:54:36 2014 +0200 (2014-09-11) changeset 58306 117ba6cbe414 parent 55656 eb07b0acbebc child 58614 7338eb25226c permissions -rw-r--r--
renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
     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