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