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