author  wenzelm 
Wed, 14 Jul 1999 13:07:09 +0200  
changeset 7005  cc778d613217 
parent 6908  1bf0590f4790 
child 7133  64c9f2364dae 
permissions  rwrr 
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset

1 
(* Title: HOL/Isar_examples/Group.thy 
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset

2 
ID: $Id$ 
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset

3 
Author: Markus Wenzel, TU Muenchen 
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset

4 
*) 
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset

5 

df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset

6 
theory Group = Main:; 
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset

7 

6793  8 
title {* Basic group theory *}; 
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset

9 

6784  10 
section {* Groups *}; 
11 

12 
text {* 

6793  13 
We define an axiomatic type class of general groups over signature 
6784  14 
(op *, one, inv). 
15 
*}; 

6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset

16 

df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset

17 
consts 
6784  18 
one :: "'a" 
19 
inv :: "'a => 'a"; 

6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset

20 

df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset

21 
axclass 
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset

22 
group < times 
6793  23 
group_assoc: "(x * y) * z = x * (y * z)" 
24 
group_left_unit: "one * x = x" 

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

6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset

26 

6784  27 
text {* 
6793  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. 

6784  32 
*}; 
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset

33 

6793  34 
theorem group_right_inverse: "x * inv x = (one::'a::group)"; 
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset

35 
proof same; 
6784  36 
have "x * inv x = one * (x * inv x)"; 
6908  37 
by (simp only: group_left_unit); 
6784  38 
also; have "... = (one * x) * inv x"; 
6908  39 
by (simp only: group_assoc); 
6784  40 
also; have "... = inv (inv x) * inv x * x * inv x"; 
6908  41 
by (simp only: group_left_inverse); 
6784  42 
also; have "... = inv (inv x) * (inv x * x) * inv x"; 
6908  43 
by (simp only: group_assoc); 
6784  44 
also; have "... = inv (inv x) * one * inv x"; 
6908  45 
by (simp only: group_left_inverse); 
6784  46 
also; have "... = inv (inv x) * (one * inv x)"; 
6908  47 
by (simp only: group_assoc); 
6784  48 
also; have "... = inv (inv x) * inv x"; 
6908  49 
by (simp only: group_left_unit); 
6784  50 
also; have "... = one"; 
6908  51 
by (simp only: group_left_inverse); 
6784  52 
finally; show ??thesis; .; 
53 
qed; 

6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset

54 

6784  55 
text {* 
6793  56 
With group_right_inverse already at our disposal, group_right_unit is 
57 
now obtained much easier as follows. 

6784  58 
*}; 
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset

59 

6793  60 
theorem group_right_unit: "x * one = (x::'a::group)"; 
6784  61 
proof same; 
62 
have "x * one = x * (inv x * x)"; 

6908  63 
by (simp only: group_left_inverse); 
6784  64 
also; have "... = x * inv x * x"; 
6908  65 
by (simp only: group_assoc); 
6784  66 
also; have "... = one * x"; 
6908  67 
by (simp only: group_right_inverse); 
6784  68 
also; have "... = x"; 
6908  69 
by (simp only: group_left_unit); 
6784  70 
finally; show ??thesis; .; 
71 
qed; 

6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset

72 

6784  73 
text {* 
6793  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. 

6784  80 

6793  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. 

6784  85 
*}; 
86 

6793  87 
theorem "x * one = (x::'a::group)"; 
6784  88 
proof same; 
89 
have "x * one = x * (inv x * x)"; 

6908  90 
by (simp only: group_left_inverse); 
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset

91 

6784  92 
note calculation = facts 
6793  93 
 {* first calculational step: init calculation register *}; 
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset

94 

6784  95 
have "... = x * inv x * x"; 
6908  96 
by (simp only: group_assoc); 
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset

97 

6892  98 
note calculation = trans [OF calculation facts] 
6784  99 
 {* general calculational step: compose with transitivity rule *}; 
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset

100 

df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset

101 
have "... = one * x"; 
6908  102 
by (simp only: group_right_inverse); 
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset

103 

6892  104 
note calculation = trans [OF calculation facts] 
6784  105 
 {* general calculational step: compose with transitivity rule *}; 
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset

106 

df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset

107 
have "... = x"; 
6908  108 
by (simp only: group_left_unit); 
6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset

109 

6892  110 
note calculation = trans [OF calculation facts] 
6784  111 
 {* final calculational step: compose with transitivity rule ... *}; 
112 
from calculation 

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

6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset

114 

df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset

115 
show ??thesis; .; 
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset

116 
qed; 
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset

117 

df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset

118 

6793  119 
section {* Groups and monoids *}; 
120 

121 
text {* 

122 
Monoids are usually defined like this. 

123 
*}; 

124 

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"; 

129 

130 
text {* 

7005  131 
Groups are *not* yet monoids directly from the definition. For 
6793  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 
*}; 

138 

139 
instance group < monoid; 

140 
by (expand_classes, 

141 
rule group_assoc, 

142 
rule group_left_unit, 

143 
rule group_right_unit); 

144 

145 

6763
df12aef00932
Some bits of group theory. Demonstrate calculational proofs.
wenzelm
parents:
diff
changeset

146 
end; 