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