src/HOL/Isar_Examples/Group.thy
changeset 33026 8f35633c4922
parent 31758 3edd5f813f01
child 35317 d57da4abb47d
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Isar_Examples/Group.thy	Tue Oct 20 19:37:09 2009 +0200
     1.3 @@ -0,0 +1,267 @@
     1.4 +(*  Title:      HOL/Isar_Examples/Group.thy
     1.5 +    Author:     Markus Wenzel, TU Muenchen
     1.6 +*)
     1.7 +
     1.8 +header {* Basic group theory *}
     1.9 +
    1.10 +theory Group
    1.11 +imports Main
    1.12 +begin
    1.13 +
    1.14 +subsection {* Groups and calculational reasoning *} 
    1.15 +
    1.16 +text {*
    1.17 + Groups over signature $({\times} :: \alpha \To \alpha \To \alpha,
    1.18 + \idt{one} :: \alpha, \idt{inverse} :: \alpha \To \alpha)$ are defined
    1.19 + as an axiomatic type class as follows.  Note that the parent class
    1.20 + $\idt{times}$ is provided by the basic HOL theory.
    1.21 +*}
    1.22 +
    1.23 +consts
    1.24 +  one :: "'a"
    1.25 +  inverse :: "'a => 'a"
    1.26 +
    1.27 +axclass
    1.28 +  group < times
    1.29 +  group_assoc:         "(x * y) * z = x * (y * z)"
    1.30 +  group_left_one:      "one * x = x"
    1.31 +  group_left_inverse:  "inverse x * x = one"
    1.32 +
    1.33 +text {*
    1.34 + The group axioms only state the properties of left one and inverse,
    1.35 + the right versions may be derived as follows.
    1.36 +*}
    1.37 +
    1.38 +theorem group_right_inverse: "x * inverse x = (one::'a::group)"
    1.39 +proof -
    1.40 +  have "x * inverse x = one * (x * inverse x)"
    1.41 +    by (simp only: group_left_one)
    1.42 +  also have "... = one * x * inverse x"
    1.43 +    by (simp only: group_assoc)
    1.44 +  also have "... = inverse (inverse x) * inverse x * x * inverse x"
    1.45 +    by (simp only: group_left_inverse)
    1.46 +  also have "... = inverse (inverse x) * (inverse x * x) * inverse x"
    1.47 +    by (simp only: group_assoc)
    1.48 +  also have "... = inverse (inverse x) * one * inverse x"
    1.49 +    by (simp only: group_left_inverse)
    1.50 +  also have "... = inverse (inverse x) * (one * inverse x)"
    1.51 +    by (simp only: group_assoc)
    1.52 +  also have "... = inverse (inverse x) * inverse x"
    1.53 +    by (simp only: group_left_one)
    1.54 +  also have "... = one"
    1.55 +    by (simp only: group_left_inverse)
    1.56 +  finally show ?thesis .
    1.57 +qed
    1.58 +
    1.59 +text {*
    1.60 + With \name{group-right-inverse} already available,
    1.61 + \name{group-right-one}\label{thm:group-right-one} is now established
    1.62 + much easier.
    1.63 +*}
    1.64 +
    1.65 +theorem group_right_one: "x * one = (x::'a::group)"
    1.66 +proof -
    1.67 +  have "x * one = x * (inverse x * x)"
    1.68 +    by (simp only: group_left_inverse)
    1.69 +  also have "... = x * inverse x * x"
    1.70 +    by (simp only: group_assoc)
    1.71 +  also have "... = one * x"
    1.72 +    by (simp only: group_right_inverse)
    1.73 +  also have "... = x"
    1.74 +    by (simp only: group_left_one)
    1.75 +  finally show ?thesis .
    1.76 +qed
    1.77 +
    1.78 +text {*
    1.79 + \medskip The calculational proof style above follows typical
    1.80 + presentations given in any introductory course on algebra.  The basic
    1.81 + technique is to form a transitive chain of equations, which in turn
    1.82 + are established by simplifying with appropriate rules.  The low-level
    1.83 + logical details of equational reasoning are left implicit.
    1.84 +
    1.85 + Note that ``$\dots$'' is just a special term variable that is bound
    1.86 + automatically to the argument\footnote{The argument of a curried
    1.87 + infix expression happens to be its right-hand side.} of the last fact
    1.88 + achieved by any local assumption or proven statement.  In contrast to
    1.89 + $\var{thesis}$, the ``$\dots$'' variable is bound \emph{after} the
    1.90 + proof is finished, though.
    1.91 +
    1.92 + There are only two separate Isar language elements for calculational
    1.93 + proofs: ``\isakeyword{also}'' for initial or intermediate
    1.94 + calculational steps, and ``\isakeyword{finally}'' for exhibiting the
    1.95 + result of a calculation.  These constructs are not hardwired into
    1.96 + Isabelle/Isar, but defined on top of the basic Isar/VM interpreter.
    1.97 + Expanding the \isakeyword{also} and \isakeyword{finally} derived
    1.98 + language elements, calculations may be simulated by hand as
    1.99 + demonstrated below.
   1.100 +*}
   1.101 +
   1.102 +theorem "x * one = (x::'a::group)"
   1.103 +proof -
   1.104 +  have "x * one = x * (inverse x * x)"
   1.105 +    by (simp only: group_left_inverse)
   1.106 +
   1.107 +  note calculation = this
   1.108 +    -- {* first calculational step: init calculation register *}
   1.109 +
   1.110 +  have "... = x * inverse x * x"
   1.111 +    by (simp only: group_assoc)
   1.112 +
   1.113 +  note calculation = trans [OF calculation this]
   1.114 +    -- {* general calculational step: compose with transitivity rule *}
   1.115 +
   1.116 +  have "... = one * x"
   1.117 +    by (simp only: group_right_inverse)
   1.118 +
   1.119 +  note calculation = trans [OF calculation this]
   1.120 +    -- {* general calculational step: compose with transitivity rule *}
   1.121 +
   1.122 +  have "... = x"
   1.123 +    by (simp only: group_left_one)
   1.124 +
   1.125 +  note calculation = trans [OF calculation this]
   1.126 +    -- {* final calculational step: compose with transitivity rule ... *}
   1.127 +  from calculation
   1.128 +    -- {* ... and pick up the final result *}
   1.129 +
   1.130 +  show ?thesis .
   1.131 +qed
   1.132 +
   1.133 +text {*
   1.134 + Note that this scheme of calculations is not restricted to plain
   1.135 + transitivity.  Rules like anti-symmetry, or even forward and backward
   1.136 + substitution work as well.  For the actual implementation of
   1.137 + \isacommand{also} and \isacommand{finally}, Isabelle/Isar maintains
   1.138 + separate context information of ``transitivity'' rules.  Rule
   1.139 + selection takes place automatically by higher-order unification.
   1.140 +*}
   1.141 +
   1.142 +
   1.143 +subsection {* Groups as monoids *}
   1.144 +
   1.145 +text {*
   1.146 + Monoids over signature $({\times} :: \alpha \To \alpha \To \alpha,
   1.147 + \idt{one} :: \alpha)$ are defined like this.
   1.148 +*}
   1.149 +
   1.150 +axclass monoid < times
   1.151 +  monoid_assoc:       "(x * y) * z = x * (y * z)"
   1.152 +  monoid_left_one:   "one * x = x"
   1.153 +  monoid_right_one:  "x * one = x"
   1.154 +
   1.155 +text {*
   1.156 + Groups are \emph{not} yet monoids directly from the definition.  For
   1.157 + monoids, \name{right-one} had to be included as an axiom, but for
   1.158 + groups both \name{right-one} and \name{right-inverse} are derivable
   1.159 + from the other axioms.  With \name{group-right-one} derived as a
   1.160 + theorem of group theory (see page~\pageref{thm:group-right-one}), we
   1.161 + may still instantiate $\idt{group} \subseteq \idt{monoid}$ properly
   1.162 + as follows.
   1.163 +*}
   1.164 +
   1.165 +instance group < monoid
   1.166 +  by (intro_classes,
   1.167 +       rule group_assoc,
   1.168 +       rule group_left_one,
   1.169 +       rule group_right_one)
   1.170 +
   1.171 +text {*
   1.172 + The \isacommand{instance} command actually is a version of
   1.173 + \isacommand{theorem}, setting up a goal that reflects the intended
   1.174 + class relation (or type constructor arity).  Thus any Isar proof
   1.175 + language element may be involved to establish this statement.  When
   1.176 + concluding the proof, the result is transformed into the intended
   1.177 + type signature extension behind the scenes.
   1.178 +*}
   1.179 +
   1.180 +subsection {* More theorems of group theory *}
   1.181 +
   1.182 +text {*
   1.183 + The one element is already uniquely determined by preserving an
   1.184 + \emph{arbitrary} group element.
   1.185 +*}
   1.186 +
   1.187 +theorem group_one_equality: "e * x = x ==> one = (e::'a::group)"
   1.188 +proof -
   1.189 +  assume eq: "e * x = x"
   1.190 +  have "one = x * inverse x"
   1.191 +    by (simp only: group_right_inverse)
   1.192 +  also have "... = (e * x) * inverse x"
   1.193 +    by (simp only: eq)
   1.194 +  also have "... = e * (x * inverse x)"
   1.195 +    by (simp only: group_assoc)
   1.196 +  also have "... = e * one"
   1.197 +    by (simp only: group_right_inverse)
   1.198 +  also have "... = e"
   1.199 +    by (simp only: group_right_one)
   1.200 +  finally show ?thesis .
   1.201 +qed
   1.202 +
   1.203 +text {*
   1.204 + Likewise, the inverse is already determined by the cancel property.
   1.205 +*}
   1.206 +
   1.207 +theorem group_inverse_equality:
   1.208 +  "x' * x = one ==> inverse x = (x'::'a::group)"
   1.209 +proof -
   1.210 +  assume eq: "x' * x = one"
   1.211 +  have "inverse x = one * inverse x"
   1.212 +    by (simp only: group_left_one)
   1.213 +  also have "... = (x' * x) * inverse x"
   1.214 +    by (simp only: eq)
   1.215 +  also have "... = x' * (x * inverse x)"
   1.216 +    by (simp only: group_assoc)
   1.217 +  also have "... = x' * one"
   1.218 +    by (simp only: group_right_inverse)
   1.219 +  also have "... = x'"
   1.220 +    by (simp only: group_right_one)
   1.221 +  finally show ?thesis .
   1.222 +qed
   1.223 +
   1.224 +text {*
   1.225 + The inverse operation has some further characteristic properties.
   1.226 +*}
   1.227 +
   1.228 +theorem group_inverse_times:
   1.229 +  "inverse (x * y) = inverse y * inverse (x::'a::group)"
   1.230 +proof (rule group_inverse_equality)
   1.231 +  show "(inverse y * inverse x) * (x * y) = one"
   1.232 +  proof -
   1.233 +    have "(inverse y * inverse x) * (x * y) =
   1.234 +        (inverse y * (inverse x * x)) * y"
   1.235 +      by (simp only: group_assoc)
   1.236 +    also have "... = (inverse y * one) * y"
   1.237 +      by (simp only: group_left_inverse)
   1.238 +    also have "... = inverse y * y"
   1.239 +      by (simp only: group_right_one)
   1.240 +    also have "... = one"
   1.241 +      by (simp only: group_left_inverse)
   1.242 +    finally show ?thesis .
   1.243 +  qed
   1.244 +qed
   1.245 +
   1.246 +theorem inverse_inverse: "inverse (inverse x) = (x::'a::group)"
   1.247 +proof (rule group_inverse_equality)
   1.248 +  show "x * inverse x = one"
   1.249 +    by (simp only: group_right_inverse)
   1.250 +qed
   1.251 +
   1.252 +theorem inverse_inject: "inverse x = inverse y ==> x = (y::'a::group)"
   1.253 +proof -
   1.254 +  assume eq: "inverse x = inverse y"
   1.255 +  have "x = x * one"
   1.256 +    by (simp only: group_right_one)
   1.257 +  also have "... = x * (inverse y * y)"
   1.258 +    by (simp only: group_left_inverse)
   1.259 +  also have "... = x * (inverse x * y)"
   1.260 +    by (simp only: eq)
   1.261 +  also have "... = (x * inverse x) * y"
   1.262 +    by (simp only: group_assoc)
   1.263 +  also have "... = one * y"
   1.264 +    by (simp only: group_right_inverse)
   1.265 +  also have "... = y"
   1.266 +    by (simp only: group_left_one)
   1.267 +  finally show ?thesis .
   1.268 +qed
   1.269 +
   1.270 +end
   1.271 \ No newline at end of file