author  nipkow 
Fri, 24 Nov 2000 16:49:27 +0100  
changeset 10519  ade64af4c57c 
parent 8936  a1c426541757 
child 11701  3d51fbf81c17 
permissions  rwrr 
5078  1 
(* Title: HOL/Integ/Group.ML 
2 
ID: $Id$ 

3 
Author: Tobias Nipkow 

4 
Copyright 1997 TU Muenchen 

5 
*) 

6 

7 
(*** Groups ***) 

8 

9 
(* Derives the wellknown convergent set of equations for groups 

8936
a1c426541757
Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents:
5078
diff
changeset

10 
based on the unary inverse 0x. 
5078  11 
*) 
12 

8936
a1c426541757
Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents:
5078
diff
changeset

13 
Goal "!!x::'a::add_group. (0x)+(x+y) = y"; 
5078  14 
by (rtac trans 1); 
15 
by (rtac (plus_assoc RS sym) 1); 

16 
by (stac left_inv 1); 

17 
by (rtac zeroL 1); 

18 
qed "left_inv2"; 

19 

8936
a1c426541757
Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents:
5078
diff
changeset

20 
Goal "!!x::'a::add_group. (0(0x)) = x"; 
5078  21 
by (rtac trans 1); 
8936
a1c426541757
Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents:
5078
diff
changeset

22 
by (res_inst_tac [("x","0x")] left_inv2 2); 
5078  23 
by (stac left_inv 1); 
24 
by (rtac (zeroR RS sym) 1); 

25 
qed "inv_inv"; 

26 

8936
a1c426541757
Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents:
5078
diff
changeset

27 
Goal "00 = (0::'a::add_group)"; 
5078  28 
by (rtac trans 1); 
29 
by (rtac (zeroR RS sym) 1); 

30 
by (rtac trans 1); 

8936
a1c426541757
Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents:
5078
diff
changeset

31 
by (res_inst_tac [("x","0")] left_inv2 2); 
5078  32 
by (simp_tac (simpset() addsimps [zeroR]) 1); 
33 
qed "inv_zero"; 

34 

8936
a1c426541757
Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents:
5078
diff
changeset

35 
Goal "!!x::'a::add_group. x+(0x) = 0"; 
5078  36 
by (rtac trans 1); 
8936
a1c426541757
Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents:
5078
diff
changeset

37 
by (res_inst_tac [("x","0x")] left_inv 2); 
5078  38 
by (stac inv_inv 1); 
39 
by (rtac refl 1); 

40 
qed "right_inv"; 

41 

8936
a1c426541757
Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents:
5078
diff
changeset

42 
Goal "!!x::'a::add_group. x+((0x)+y) = y"; 
5078  43 
by (rtac trans 1); 
8936
a1c426541757
Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents:
5078
diff
changeset

44 
by (res_inst_tac [("x","0x")] left_inv2 2); 
5078  45 
by (stac inv_inv 1); 
46 
by (rtac refl 1); 

47 
qed "right_inv2"; 

48 

49 
val plus_cong = read_instantiate [("f1","op +")] (arg_cong RS cong); 

50 

8936
a1c426541757
Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents:
5078
diff
changeset

51 
Goal "!!x::'a::add_group. 0(x+y) = (0y)+(0x)"; 
5078  52 
by (rtac trans 1); 
53 
by (rtac zeroR 2); 

54 
by (rtac trans 1); 

55 
by (rtac plus_cong 2); 

56 
by (rtac refl 2); 

57 
by (res_inst_tac [("x","x+y")] right_inv 2); 

58 
by (rtac trans 1); 

59 
by (rtac plus_assoc 2); 

60 
by (rtac trans 1); 

61 
by (rtac plus_cong 2); 

62 
by (simp_tac (simpset() addsimps 

63 
[plus_assoc,left_inv,left_inv2,right_inv,right_inv2]) 2); 

64 
by (rtac refl 2); 

65 
by (rtac (zeroL RS sym) 1); 

66 
qed "inv_plus"; 

67 

8936
a1c426541757
Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents:
5078
diff
changeset

68 
(*** convergent TRS for groups with unary inverse 0x ***) 
5078  69 
val group1_simps = 
70 
[zeroL,zeroR,plus_assoc,left_inv,left_inv2,right_inv,right_inv2,inv_inv, 

71 
inv_zero,inv_plus]; 

72 

73 
val group1_tac = 

74 
let val ss = HOL_basic_ss addsimps group1_simps 

75 
in simp_tac ss end; 

76 

77 
(* I believe there is no convergent TRS for groups with binary `', 

78 
unless you have an extra unary `' and simply define xy = x+(y). 

8936
a1c426541757
Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents:
5078
diff
changeset

79 
This does not work with only a binary `' because xy = x+(0y) does 
5078  80 
not terminate. Hence we have a special tactic for converting all 
8936
a1c426541757
Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents:
5078
diff
changeset

81 
occurrences of xy into x+(0y): 
5078  82 
*) 
83 

84 
local 

85 
fun find(Const("op ",Type("fun",[T,_]))$s$t) = [(T,s,t)] @ find s @ find t 

86 
 find(s$t) = find s @ find t 

87 
 find _ = []; 

88 

89 
fun subst_tac sg (tacf,(T,s,t)) = 

90 
let val typinst = [(("'a",0),ctyp_of sg T)]; 

91 
val terminst = [(cterm_of sg (Var(("x",0),T)),cterm_of sg s), 

92 
(cterm_of sg (Var(("y",0),T)),cterm_of sg t)]; 

93 
in tacf THEN' rtac ((instantiate(typinst,terminst) minus_inv) RS ssubst) end; 

94 

95 
in 

96 
val mk_group1_tac = SUBGOAL(fn (t,i) => fn st => 

97 
let val sg = #sign(rep_thm st) 

98 
in foldl (subst_tac sg) (K all_tac,find t) i st 

99 
end) 

100 
end; 

101 

102 
(* The following two equations are not used in any of the decision procedures, 

103 
but are still very useful. They also demonstrate mk_group1_tac. 

104 
*) 

8936
a1c426541757
Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents:
5078
diff
changeset

105 
Goal "xx = (0::'a::add_group)"; 
5078  106 
by (mk_group1_tac 1); 
107 
by (group1_tac 1); 

108 
qed "minus_self_zero"; 

109 

8936
a1c426541757
Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents:
5078
diff
changeset

110 
Goal "x0 = (x::'a::add_group)"; 
5078  111 
by (mk_group1_tac 1); 
112 
by (group1_tac 1); 

113 
qed "minus_zero"; 

114 

115 
(*** Abelian Groups ***) 

116 

117 
Goal "x+(y+z)=y+(x+z::'a::add_agroup)"; 

118 
by (rtac trans 1); 

119 
by (rtac plus_commute 1); 

120 
by (rtac trans 1); 

121 
by (rtac plus_assoc 1); 

122 
by (simp_tac (simpset() addsimps [plus_commute]) 1); 

123 
qed "plus_commuteL"; 

124 

8936
a1c426541757
Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents:
5078
diff
changeset

125 
(* Convergent TRS for Abelian groups with unary inverse 0x. 
5078  126 
Requires ordered rewriting 
127 
*) 

128 

129 
val agroup1_simps = plus_commute::plus_commuteL::group1_simps; 

130 

131 
val agroup1_tac = 

132 
let val ss = HOL_basic_ss addsimps agroup1_simps 

133 
in simp_tac ss end; 

134 

135 
(* Again, I do not believe there is a convergent TRS for Abelian Groups with 

136 
binary `'. However, we can still decide the word problem using additional 

137 
rules for 

138 
1. floating `' to the top: 

139 
"x + (y  z) = (x + y)  (z::'a::add_group)" 

140 
"(x  y) + z = (x + z)  (y::'a::add_agroup)" 

141 
"(x  y)  z = x  (y + (z::'a::add_agroup))" 

142 
"x  (y  z) = (x + z)  (y::'a::add_agroup)" 

143 
2. and for moving `' over to the other side: 

144 
(xy = z) = (x = z+y) and (x = yz) = (x+z = y) 

145 
*) 

146 
Goal "x + (y  z) = (x + y)  (z::'a::add_group)"; 

147 
by (mk_group1_tac 1); 

148 
by (group1_tac 1); 

149 
qed "plus_minusR"; 

150 

151 
Goal "(x  y) + z = (x + z)  (y::'a::add_agroup)"; 

152 
by (mk_group1_tac 1); 

153 
by (agroup1_tac 1); 

154 
qed "plus_minusL"; 

155 

156 
Goal "(x  y)  z = x  (y + (z::'a::add_agroup))"; 

157 
by (mk_group1_tac 1); 

158 
by (agroup1_tac 1); 

159 
qed "minus_minusL"; 

160 

161 
Goal "x  (y  z) = (x + z)  (y::'a::add_agroup)"; 

162 
by (mk_group1_tac 1); 

163 
by (agroup1_tac 1); 

164 
qed "minus_minusR"; 

165 

166 
Goal "!!x::'a::add_group. (xy = z) = (x = z+y)"; 

167 
by (stac minus_inv 1); 

168 
by (fast_tac (claset() addss (HOL_basic_ss addsimps group1_simps)) 1); 

169 
qed "minusL_iff"; 

170 

171 
Goal "!!x::'a::add_group. (x = yz) = (x+z = y)"; 

172 
by (stac minus_inv 1); 

173 
by (fast_tac (claset() addss (HOL_basic_ss addsimps group1_simps)) 1); 

174 
qed "minusR_iff"; 

175 

176 
val agroup2_simps = 

177 
[zeroL,zeroR,plus_assoc,plus_commute,plus_commuteL, 

178 
plus_minusR,plus_minusL,minus_minusL,minus_minusR,minusL_iff,minusR_iff]; 

179 

180 
(* This twophase ordered rewriting tactic works, but agroup_simps are 

181 
simpler. However, agroup_simps is not confluent for arbitrary terms, 

182 
it merely decides equality. 

183 
(* Phase 1 *) 

184 

8936
a1c426541757
Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents:
5078
diff
changeset

185 
Goal "!!x::'a::add_agroup. (x+(0y))+z = (x+z)+(0y)"; 
5078  186 
by (Simp_tac 1); 
187 
val lemma = result(); 

188 
bind_thm("plus_minusL",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma); 

189 

8936
a1c426541757
Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents:
5078
diff
changeset

190 
Goal "!!x::'a::add_agroup. x+(0(y+z)) = (x+(0y))+(0z)"; 
5078  191 
by (Simp_tac 1); 
192 
val lemma = result(); 

193 
bind_thm("minus_plusR",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma); 

194 

8936
a1c426541757
Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents:
5078
diff
changeset

195 
Goal "!!x::'a::add_agroup. x+(0(y+(0z))) = (x+z)+(0y)"; 
5078  196 
by (Simp_tac 1); 
197 
val lemma = result(); 

198 
bind_thm("minus_minusR",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma); 

199 

8936
a1c426541757
Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents:
5078
diff
changeset

200 
Goal "!!x::'a::add_agroup. x+(y+(0z)) = (x+y)+(0z)"; 
5078  201 
by (Simp_tac 1); 
202 
val lemma = result(); 

203 
bind_thm("plus_minusR",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma); 

204 

205 
(* Phase 2 *) 

206 

8936
a1c426541757
Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents:
5078
diff
changeset

207 
Goal "!!x::'a::add_agroup. (x+y)+(0z) = x+(y+(0z))"; 
5078  208 
by (Simp_tac 1); 
209 
val lemma = result(); 

210 
bind_thm("minus_plusL2",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma); 

211 

8936
a1c426541757
Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents:
5078
diff
changeset

212 
Goal "!!x::'a::add_agroup. (x+y)+(0x) = y"; 
5078  213 
by (rtac (plus_assoc RS trans) 1); 
214 
by (rtac trans 1); 

215 
by (rtac plus_cong 1); 

216 
by (rtac refl 1); 

217 
by (rtac right_inv2 2); 

218 
by (rtac plus_commute 1); 

219 
val lemma = result(); 

220 
bind_thm("minus_plusL3",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma); 

221 

222 
*) 