summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Isar_examples/Group.thy

author | wenzelm |

Sat Oct 30 20:20:48 1999 +0200 (1999-10-30) | |

changeset 7982 | d534b897ce39 |

parent 7968 | 964b65b4e433 |

child 8910 | 981ac87f905c |

permissions | -rw-r--r-- |

improved presentation;

1 (* Title: HOL/Isar_examples/Group.thy

2 ID: $Id$

3 Author: Markus Wenzel, TU Muenchen

4 *)

6 header {* Basic group theory *};

8 theory Group = Main:;

10 subsection {* Groups and calculational reasoning *};

12 text {*

13 Groups over signature $({\times} :: \alpha \To \alpha \To \alpha,

14 \idt{one} :: \alpha, \idt{inv} :: \alpha \To \alpha)$ are defined as

15 an axiomatic type class as follows. Note that the parent class

16 $\idt{times}$ is provided by the basic HOL theory.

17 *};

19 consts

20 one :: "'a"

21 inv :: "'a => 'a";

23 axclass

24 group < times

25 group_assoc: "(x * y) * z = x * (y * z)"

26 group_left_unit: "one * x = x"

27 group_left_inverse: "inv x * x = one";

29 text {*

30 The group axioms only state the properties of left unit and inverse,

31 the right versions may be derived as follows.

32 *};

34 theorem group_right_inverse: "x * inv x = (one::'a::group)";

35 proof -;

36 have "x * inv x = one * (x * inv x)";

37 by (simp only: group_left_unit);

38 also; have "... = (one * x) * inv x";

39 by (simp only: group_assoc);

40 also; have "... = inv (inv x) * inv x * x * inv x";

41 by (simp only: group_left_inverse);

42 also; have "... = inv (inv x) * (inv x * x) * inv x";

43 by (simp only: group_assoc);

44 also; have "... = inv (inv x) * one * inv x";

45 by (simp only: group_left_inverse);

46 also; have "... = inv (inv x) * (one * inv x)";

47 by (simp only: group_assoc);

48 also; have "... = inv (inv x) * inv x";

49 by (simp only: group_left_unit);

50 also; have "... = one";

51 by (simp only: group_left_inverse);

52 finally; show ?thesis; .;

53 qed;

55 text {*

56 With \name{group-right-inverse} already available,

57 \name{group-right-unit}\label{thm:group-right-unit} is now

58 established much easier.

59 *};

61 theorem group_right_unit: "x * one = (x::'a::group)";

62 proof -;

63 have "x * one = x * (inv x * x)";

64 by (simp only: group_left_inverse);

65 also; have "... = x * inv x * x";

66 by (simp only: group_assoc);

67 also; have "... = one * x";

68 by (simp only: group_right_inverse);

69 also; have "... = x";

70 by (simp only: group_left_unit);

71 finally; show ?thesis; .;

72 qed;

74 text {*

75 \medskip The calculational proof style above follows typical

76 presentations given in any introductory course on algebra. The basic

77 technique is to form a transitive chain of equations, which in turn

78 are established by simplifying with appropriate rules. The low-level

79 logical details of equational reasoning are left implicit.

81 Note that ``$\dots$'' is just a special term variable that is bound

82 automatically to the argument\footnote{The argument of a curried

83 infix expression happens to be its right-hand side.} of the last fact

84 achieved by any local assumption or proven statement. In contrast to

85 $\var{thesis}$, the ``$\dots$'' variable is bound \emph{after} the

86 proof is finished, though.

88 There are only two separate Isar language elements for calculational

89 proofs: ``\isakeyword{also}'' for initial or intermediate

90 calculational steps, and ``\isakeyword{finally}'' for exhibiting the

91 result of a calculation. These constructs are not hardwired into

92 Isabelle/Isar, but defined on top of the basic Isar/VM interpreter.

93 Expanding the \isakeyword{also} and \isakeyword{finally} derived

94 language elements, calculations may be simulated by hand as

95 demonstrated below.

96 *};

98 theorem "x * one = (x::'a::group)";

99 proof -;

100 have "x * one = x * (inv x * x)";

101 by (simp only: group_left_inverse);

103 note calculation = this

104 -- {* first calculational step: init calculation register *};

106 have "... = x * inv x * x";

107 by (simp only: group_assoc);

109 note calculation = trans [OF calculation this]

110 -- {* general calculational step: compose with transitivity rule *};

112 have "... = one * x";

113 by (simp only: group_right_inverse);

115 note calculation = trans [OF calculation this]

116 -- {* general calculational step: compose with transitivity rule *};

118 have "... = x";

119 by (simp only: group_left_unit);

121 note calculation = trans [OF calculation this]

122 -- {* final calculational step: compose with transitivity rule ... *};

123 from calculation

124 -- {* ... and pick up the final result *};

126 show ?thesis; .;

127 qed;

129 text {*

130 Note that this scheme of calculations is not restricted to plain

131 transitivity. Rules like anti-symmetry, or even forward and backward

132 substitution work as well. For the actual implementation of

133 \isacommand{also} and \isacommand{finally}, Isabelle/Isar maintains

134 separate context information of ``transitivity'' rules. Rule

135 selection takes place automatically by higher-order unification.

136 *};

139 subsection {* Groups as monoids *};

141 text {*

142 Monoids over signature $({\times} :: \alpha \To \alpha \To \alpha,

143 \idt{one} :: \alpha)$ are defined like this.

144 *};

146 axclass monoid < times

147 monoid_assoc: "(x * y) * z = x * (y * z)"

148 monoid_left_unit: "one * x = x"

149 monoid_right_unit: "x * one = x";

151 text {*

152 Groups are \emph{not} yet monoids directly from the definition. For

153 monoids, \name{right-unit} had to be included as an axiom, but for

154 groups both \name{right-unit} and \name{right-inverse} are derivable

155 from the other axioms. With \name{group-right-unit} derived as a

156 theorem of group theory (see page~\pageref{thm:group-right-unit}), we

157 may still instantiate $\idt{group} \subset \idt{monoid}$ properly as

158 follows.

159 *};

161 instance group < monoid;

162 by (intro_classes,

163 rule group_assoc,

164 rule group_left_unit,

165 rule group_right_unit);

167 text {*

168 The \isacommand{instance} command actually is a version of

169 \isacommand{theorem}, setting up a goal that reflects the intended

170 class relation (or type constructor arity). Thus any Isar proof

171 language element may be involved to establish this statement. When

172 concluding the proof, the result is transformed into the intended

173 type signature extension behind the scenes.

174 *};

176 end;