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

src/HOL/Isar_examples/Group.thy

author | wenzelm |

Sat Sep 04 21:13:01 1999 +0200 (1999-09-04) | |

changeset 7480 | 0a0e0dbe1269 |

parent 7433 | 27887c52b9c8 |

child 7740 | 2fbe5ce9845f |

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

replaced ?? by ?;

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

2 ID: $Id$

3 Author: Markus Wenzel, TU Muenchen

4 *)

6 theory Group = Main:;

8 title {* Basic group theory *};

10 section {* Groups *};

12 text {*

13 We define an axiomatic type class of general groups over signature

14 (op *, one, inv).

15 *};

17 consts

18 one :: "'a"

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

21 axclass

22 group < times

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

24 group_left_unit: "one * x = x"

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

27 text {*

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

29 the right versions are derivable as follows. The calculational proof

30 style below closely follows typical presentations given in any basic

31 course on algebra.

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 group_right_inverse already at our disposal, group_right_unit is

57 now obtained much easier as follows.

58 *};

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

61 proof -;

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

63 by (simp only: group_left_inverse);

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

65 by (simp only: group_assoc);

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

67 by (simp only: group_right_inverse);

68 also; have "... = x";

69 by (simp only: group_left_unit);

70 finally; show ?thesis; .;

71 qed;

73 text {*

74 There are only two Isar language elements for calculational proofs:

75 'also' for initial or intermediate calculational steps, and 'finally'

76 for building the result of a calculation. These constructs are not

77 hardwired into Isabelle/Isar, but defined on top of the basic Isar/VM

78 interpreter. Expanding the 'also' or 'finally' derived language

79 elements, calculations may be simulated as demonstrated below.

81 Note that "..." is just a special term binding that happens to be

82 bound automatically to the argument of the last fact established by

83 assume or any local goal. In contrast to ?thesis, "..." is bound

84 after the proof is finished.

85 *};

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

88 proof -;

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

90 by (simp only: group_left_inverse);

92 note calculation = this

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

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

96 by (simp only: group_assoc);

98 note calculation = trans [OF calculation this]

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

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

102 by (simp only: group_right_inverse);

104 note calculation = trans [OF calculation this]

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

107 have "... = x";

108 by (simp only: group_left_unit);

110 note calculation = trans [OF calculation this]

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

112 from calculation

113 -- {* ... and pick up final result *};

115 show ?thesis; .;

116 qed;

119 section {* Groups and monoids *};

121 text {*

122 Monoids are usually defined like this.

123 *};

125 axclass monoid < times

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

127 monoid_left_unit: "one * x = x"

128 monoid_right_unit: "x * one = x";

130 text {*

131 Groups are *not* yet monoids directly from the definition. For

132 monoids, right_unit had to be included as an axiom, but for groups

133 both right_unit and right_inverse are derivable from the other

134 axioms. With group_right_unit derived as a theorem of group theory

135 (see above), we may still instantiate group < monoid properly as

136 follows.

137 *};

139 instance group < monoid;

140 by (intro_classes,

141 rule group_assoc,

142 rule group_left_unit,

143 rule group_right_unit);

146 end;