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