author  nipkow 
Fri, 13 Nov 2009 14:14:04 +0100  
changeset 33657  a4179bf442d1 
parent 29237  e90d9d51106b 
child 35355  613e133966ea 
permissions  rwrr 
27701  1 
(* 
2 
Title: Algebra/Congruence.thy 

3 
Author: Clemens Ballarin, started 3 January 2008 

4 
Copyright: Clemens Ballarin 

5 
*) 

6 

7 
theory Congruence imports Main begin 

8 

9 
section {* Objects *} 

10 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27701
diff
changeset

11 
subsection {* Structure with Carrier Set. *} 
27701  12 

13 
record 'a partial_object = 

14 
carrier :: "'a set" 

15 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27701
diff
changeset

16 

21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27701
diff
changeset

17 
subsection {* Structure with Carrier and Equivalence Relation @{text eq} *} 
27701  18 

19 
record 'a eq_object = "'a partial_object" + 

20 
eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl ".=\<index>" 50) 

21 

22 
constdefs (structure S) 

23 
elem :: "_ \<Rightarrow> 'a \<Rightarrow> 'a set \<Rightarrow> bool" (infixl ".\<in>\<index>" 50) 

24 
"x .\<in> A \<equiv> (\<exists>y \<in> A. x .= y)" 

25 

26 
set_eq :: "_ \<Rightarrow> 'a set \<Rightarrow> 'a set \<Rightarrow> bool" (infixl "{.=}\<index>" 50) 

27 
"A {.=} B == ((\<forall>x \<in> A. x .\<in> B) \<and> (\<forall>x \<in> B. x .\<in> A))" 

28 

29 
eq_class_of :: "_ \<Rightarrow> 'a \<Rightarrow> 'a set" ("class'_of\<index> _") 

30 
"class_of x == {y \<in> carrier S. x .= y}" 

31 

32 
eq_closure_of :: "_ \<Rightarrow> 'a set \<Rightarrow> 'a set" ("closure'_of\<index> _") 

33 
"closure_of A == {y \<in> carrier S. y .\<in> A}" 

34 

35 
eq_is_closed :: "_ \<Rightarrow> 'a set \<Rightarrow> bool" ("is'_closed\<index> _") 

36 
"is_closed A == (A \<subseteq> carrier S \<and> closure_of A = A)" 

37 

38 
syntax 

39 
not_eq :: "_ \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl ".\<noteq>\<index>" 50) 

40 
not_elem :: "_ \<Rightarrow> 'a \<Rightarrow> 'a set \<Rightarrow> bool" (infixl ".\<notin>\<index>" 50) 

41 
set_not_eq :: "_ \<Rightarrow> 'a set \<Rightarrow> 'a set \<Rightarrow> bool" (infixl "{.\<noteq>}\<index>" 50) 

42 

43 
translations 

44 
"x .\<noteq>\<index> y" == "~(x .=\<index> y)" 

45 
"x .\<notin>\<index> A" == "~(x .\<in>\<index> A)" 

46 
"A {.\<noteq>}\<index> B" == "~(A {.=}\<index> B)" 

47 

48 
locale equivalence = 

49 
fixes S (structure) 

50 
assumes refl [simp, intro]: "x \<in> carrier S \<Longrightarrow> x .= x" 

51 
and sym [sym]: "\<lbrakk> x .= y; x \<in> carrier S; y \<in> carrier S \<rbrakk> \<Longrightarrow> y .= x" 

52 
and trans [trans]: "\<lbrakk> x .= y; y .= z; x \<in> carrier S; y \<in> carrier S; z \<in> carrier S \<rbrakk> \<Longrightarrow> x .= z" 

53 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27701
diff
changeset

54 
(* Lemmas by Stephan Hohe *) 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27701
diff
changeset

55 

27701  56 
lemma elemI: 
57 
fixes R (structure) 

58 
assumes "a' \<in> A" and "a .= a'" 

59 
shows "a .\<in> A" 

60 
unfolding elem_def 

61 
using assms 

62 
by fast 

63 

64 
lemma (in equivalence) elem_exact: 

65 
assumes "a \<in> carrier S" and "a \<in> A" 

66 
shows "a .\<in> A" 

67 
using assms 

68 
by (fast intro: elemI) 

69 

70 
lemma elemE: 

71 
fixes S (structure) 

72 
assumes "a .\<in> A" 

73 
and "\<And>a'. \<lbrakk>a' \<in> A; a .= a'\<rbrakk> \<Longrightarrow> P" 

74 
shows "P" 

75 
using assms 

76 
unfolding elem_def 

77 
by fast 

78 

79 
lemma (in equivalence) elem_cong_l [trans]: 

80 
assumes cong: "a' .= a" 

81 
and a: "a .\<in> A" 

82 
and carr: "a \<in> carrier S" "a' \<in> carrier S" 

83 
and Acarr: "A \<subseteq> carrier S" 

84 
shows "a' .\<in> A" 

85 
using a 

86 
apply (elim elemE, intro elemI) 

87 
proof assumption 

88 
fix b 

89 
assume bA: "b \<in> A" 

90 
note [simp] = carr bA[THEN subsetD[OF Acarr]] 

91 
note cong 

92 
also assume "a .= b" 

93 
finally show "a' .= b" by simp 

94 
qed 

95 

96 
lemma (in equivalence) elem_subsetD: 

97 
assumes "A \<subseteq> B" 

98 
and aA: "a .\<in> A" 

99 
shows "a .\<in> B" 

100 
using assms 

101 
by (fast intro: elemI elim: elemE dest: subsetD) 

102 

103 
lemma (in equivalence) mem_imp_elem [simp, intro]: 

104 
"[ x \<in> A; x \<in> carrier S ] ==> x .\<in> A" 

105 
unfolding elem_def by blast 

106 

107 
lemma set_eqI: 

108 
fixes R (structure) 

109 
assumes ltr: "\<And>a. a \<in> A \<Longrightarrow> a .\<in> B" 

110 
and rtl: "\<And>b. b \<in> B \<Longrightarrow> b .\<in> A" 

111 
shows "A {.=} B" 

112 
unfolding set_eq_def 

113 
by (fast intro: ltr rtl) 

114 

115 
lemma set_eqI2: 

116 
fixes R (structure) 

117 
assumes ltr: "\<And>a b. a \<in> A \<Longrightarrow> \<exists>b\<in>B. a .= b" 

118 
and rtl: "\<And>b. b \<in> B \<Longrightarrow> \<exists>a\<in>A. b .= a" 

119 
shows "A {.=} B" 

120 
by (intro set_eqI, unfold elem_def) (fast intro: ltr rtl)+ 

121 

122 
lemma set_eqD1: 

123 
fixes R (structure) 

124 
assumes AA': "A {.=} A'" 

125 
and "a \<in> A" 

126 
shows "\<exists>a'\<in>A'. a .= a'" 

127 
using assms 

128 
unfolding set_eq_def elem_def 

129 
by fast 

130 

131 
lemma set_eqD2: 

132 
fixes R (structure) 

133 
assumes AA': "A {.=} A'" 

134 
and "a' \<in> A'" 

135 
shows "\<exists>a\<in>A. a' .= a" 

136 
using assms 

137 
unfolding set_eq_def elem_def 

138 
by fast 

139 

140 
lemma set_eqE: 

141 
fixes R (structure) 

142 
assumes AB: "A {.=} B" 

143 
and r: "\<lbrakk>\<forall>a\<in>A. a .\<in> B; \<forall>b\<in>B. b .\<in> A\<rbrakk> \<Longrightarrow> P" 

144 
shows "P" 

145 
using AB 

146 
unfolding set_eq_def 

147 
by (blast dest: r) 

148 

149 
lemma set_eqE2: 

150 
fixes R (structure) 

151 
assumes AB: "A {.=} B" 

152 
and r: "\<lbrakk>\<forall>a\<in>A. (\<exists>b\<in>B. a .= b); \<forall>b\<in>B. (\<exists>a\<in>A. b .= a)\<rbrakk> \<Longrightarrow> P" 

153 
shows "P" 

154 
using AB 

155 
unfolding set_eq_def elem_def 

156 
by (blast dest: r) 

157 

158 
lemma set_eqE': 

159 
fixes R (structure) 

160 
assumes AB: "A {.=} B" 

161 
and aA: "a \<in> A" and bB: "b \<in> B" 

162 
and r: "\<And>a' b'. \<lbrakk>a' \<in> A; b .= a'; b' \<in> B; a .= b'\<rbrakk> \<Longrightarrow> P" 

163 
shows "P" 

164 
proof  

165 
from AB aA 

166 
have "\<exists>b'\<in>B. a .= b'" by (rule set_eqD1) 

167 
from this obtain b' 

168 
where b': "b' \<in> B" "a .= b'" by auto 

169 

170 
from AB bB 

171 
have "\<exists>a'\<in>A. b .= a'" by (rule set_eqD2) 

172 
from this obtain a' 

173 
where a': "a' \<in> A" "b .= a'" by auto 

174 

175 
from a' b' 

176 
show "P" by (rule r) 

177 
qed 

178 

179 
lemma (in equivalence) eq_elem_cong_r [trans]: 

180 
assumes a: "a .\<in> A" 

181 
and cong: "A {.=} A'" 

182 
and carr: "a \<in> carrier S" 

183 
and Carr: "A \<subseteq> carrier S" "A' \<subseteq> carrier S" 

184 
shows "a .\<in> A'" 

185 
using a cong 

186 
proof (elim elemE set_eqE) 

187 
fix b 

188 
assume bA: "b \<in> A" 

189 
and inA': "\<forall>b\<in>A. b .\<in> A'" 

190 
note [simp] = carr Carr Carr[THEN subsetD] bA 

191 
assume "a .= b" 

192 
also from bA inA' 

193 
have "b .\<in> A'" by fast 

194 
finally 

195 
show "a .\<in> A'" by simp 

196 
qed 

197 

198 
lemma (in equivalence) set_eq_sym [sym]: 

199 
assumes "A {.=} B" 

200 
and "A \<subseteq> carrier S" "B \<subseteq> carrier S" 

201 
shows "B {.=} A" 

202 
using assms 

203 
unfolding set_eq_def elem_def 

204 
by fast 

205 

206 
(* FIXME: the following two required in Isabelle 2008, not Isabelle 2007 *) 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27701
diff
changeset

207 
(* alternatively, could declare lemmas [trans] = ssubst [where 'a = "'a set"] *) 
27701  208 

209 
lemma (in equivalence) equal_set_eq_trans [trans]: 

210 
assumes AB: "A = B" and BC: "B {.=} C" 

211 
shows "A {.=} C" 

212 
using AB BC by simp 

213 

214 
lemma (in equivalence) set_eq_equal_trans [trans]: 

215 
assumes AB: "A {.=} B" and BC: "B = C" 

216 
shows "A {.=} C" 

217 
using AB BC by simp 

218 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27701
diff
changeset

219 

27701  220 
lemma (in equivalence) set_eq_trans [trans]: 
221 
assumes AB: "A {.=} B" and BC: "B {.=} C" 

222 
and carr: "A \<subseteq> carrier S" "B \<subseteq> carrier S" "C \<subseteq> carrier S" 

223 
shows "A {.=} C" 

224 
proof (intro set_eqI) 

225 
fix a 

226 
assume aA: "a \<in> A" 

227 
with carr have "a \<in> carrier S" by fast 

228 
note [simp] = carr this 

229 

230 
from aA 

231 
have "a .\<in> A" by (simp add: elem_exact) 

232 
also note AB 

233 
also note BC 

234 
finally 

235 
show "a .\<in> C" by simp 

236 
next 

237 
fix c 

238 
assume cC: "c \<in> C" 

239 
with carr have "c \<in> carrier S" by fast 

240 
note [simp] = carr this 

241 

242 
from cC 

243 
have "c .\<in> C" by (simp add: elem_exact) 

244 
also note BC[symmetric] 

245 
also note AB[symmetric] 

246 
finally 

247 
show "c .\<in> A" by simp 

248 
qed 

249 

250 
(* FIXME: generalise for insert *) 

251 

252 
(* 

253 
lemma (in equivalence) set_eq_insert: 

254 
assumes x: "x .= x'" 

255 
and carr: "x \<in> carrier S" "x' \<in> carrier S" "A \<subseteq> carrier S" 

256 
shows "insert x A {.=} insert x' A" 

257 
unfolding set_eq_def elem_def 

258 
apply rule 

259 
apply rule 

260 
apply (case_tac "xa = x") 

261 
using x apply fast 

262 
apply (subgoal_tac "xa \<in> A") prefer 2 apply fast 

263 
apply (rule_tac x=xa in bexI) 

264 
using carr apply (rule_tac refl) apply auto [1] 

265 
apply safe 

266 
*) 

267 

268 
lemma (in equivalence) set_eq_pairI: 

269 
assumes xx': "x .= x'" 

270 
and carr: "x \<in> carrier S" "x' \<in> carrier S" "y \<in> carrier S" 

271 
shows "{x, y} {.=} {x', y}" 

272 
unfolding set_eq_def elem_def 

273 
proof safe 

274 
have "x' \<in> {x', y}" by fast 

275 
with xx' show "\<exists>b\<in>{x', y}. x .= b" by fast 

276 
next 

277 
have "y \<in> {x', y}" by fast 

278 
with carr show "\<exists>b\<in>{x', y}. y .= b" by fast 

279 
next 

280 
have "x \<in> {x, y}" by fast 

281 
with xx'[symmetric] carr 

282 
show "\<exists>a\<in>{x, y}. x' .= a" by fast 

283 
next 

284 
have "y \<in> {x, y}" by fast 

285 
with carr show "\<exists>a\<in>{x, y}. y .= a" by fast 

286 
qed 

287 

288 
lemma (in equivalence) is_closedI: 

289 
assumes closed: "!!x y. [ x .= y; x \<in> A; y \<in> carrier S ] ==> y \<in> A" 

290 
and S: "A \<subseteq> carrier S" 

291 
shows "is_closed A" 

292 
unfolding eq_is_closed_def eq_closure_of_def elem_def 

293 
using S 

294 
by (blast dest: closed sym) 

295 

296 
lemma (in equivalence) closure_of_eq: 

297 
"[ x .= x'; A \<subseteq> carrier S; x \<in> closure_of A; x \<in> carrier S; x' \<in> carrier S ] ==> x' \<in> closure_of A" 

298 
unfolding eq_closure_of_def elem_def 

299 
by (blast intro: trans sym) 

300 

301 
lemma (in equivalence) is_closed_eq [dest]: 

302 
"[ x .= x'; x \<in> A; is_closed A; x \<in> carrier S; x' \<in> carrier S ] ==> x' \<in> A" 

303 
unfolding eq_is_closed_def 

304 
using closure_of_eq [where A = A] 

305 
by simp 

306 

307 
lemma (in equivalence) is_closed_eq_rev [dest]: 

308 
"[ x .= x'; x' \<in> A; is_closed A; x \<in> carrier S; x' \<in> carrier S ] ==> x \<in> A" 

309 
by (drule sym) (simp_all add: is_closed_eq) 

310 

311 
lemma closure_of_closed [simp, intro]: 

312 
fixes S (structure) 

313 
shows "closure_of A \<subseteq> carrier S" 

314 
unfolding eq_closure_of_def 

315 
by fast 

316 

317 
lemma closure_of_memI: 

318 
fixes S (structure) 

319 
assumes "a .\<in> A" 

320 
and "a \<in> carrier S" 

321 
shows "a \<in> closure_of A" 

322 
unfolding eq_closure_of_def 

323 
using assms 

324 
by fast 

325 

326 
lemma closure_ofI2: 

327 
fixes S (structure) 

328 
assumes "a .= a'" 

329 
and "a' \<in> A" 

330 
and "a \<in> carrier S" 

331 
shows "a \<in> closure_of A" 

332 
unfolding eq_closure_of_def elem_def 

333 
using assms 

334 
by fast 

335 

336 
lemma closure_of_memE: 

337 
fixes S (structure) 

338 
assumes p: "a \<in> closure_of A" 

339 
and r: "\<lbrakk>a \<in> carrier S; a .\<in> A\<rbrakk> \<Longrightarrow> P" 

340 
shows "P" 

341 
proof  

342 
from p 

343 
have acarr: "a \<in> carrier S" 

344 
and "a .\<in> A" 

345 
by (simp add: eq_closure_of_def)+ 

346 
thus "P" by (rule r) 

347 
qed 

348 

349 
lemma closure_ofE2: 

350 
fixes S (structure) 

351 
assumes p: "a \<in> closure_of A" 

352 
and r: "\<And>a'. \<lbrakk>a \<in> carrier S; a' \<in> A; a .= a'\<rbrakk> \<Longrightarrow> P" 

353 
shows "P" 

354 
proof  

355 
from p have acarr: "a \<in> carrier S" by (simp add: eq_closure_of_def) 

356 

357 
from p have "\<exists>a'\<in>A. a .= a'" by (simp add: eq_closure_of_def elem_def) 

358 
from this obtain a' 

359 
where "a' \<in> A" and "a .= a'" by auto 

360 

361 
from acarr and this 

362 
show "P" by (rule r) 

363 
qed 

364 

365 
(* 

366 
lemma (in equivalence) classes_consistent: 

367 
assumes Acarr: "A \<subseteq> carrier S" 

368 
shows "is_closed (closure_of A)" 

369 
apply (blast intro: elemI elim elemE) 

370 
using assms 

371 
apply (intro is_closedI closure_of_memI, simp) 

372 
apply (elim elemE closure_of_memE) 

373 
proof  

374 
fix x a' a'' 

375 
assume carr: "x \<in> carrier S" "a' \<in> carrier S" 

376 
assume a''A: "a'' \<in> A" 

377 
with Acarr have "a'' \<in> carrier S" by fast 

378 
note [simp] = carr this Acarr 

379 

380 
assume "x .= a'" 

381 
also assume "a' .= a''" 

382 
also from a''A 

383 
have "a'' .\<in> A" by (simp add: elem_exact) 

384 
finally show "x .\<in> A" by simp 

385 
qed 

386 
*) 

387 
(* 

388 
lemma (in equivalence) classes_small: 

389 
assumes "is_closed B" 

390 
and "A \<subseteq> B" 

391 
shows "closure_of A \<subseteq> B" 

392 
using assms 

393 
by (blast dest: is_closedD2 elem_subsetD elim: closure_of_memE) 

394 

395 
lemma (in equivalence) classes_eq: 

396 
assumes "A \<subseteq> carrier S" 

397 
shows "A {.=} closure_of A" 

398 
using assms 

399 
by (blast intro: set_eqI elem_exact closure_of_memI elim: closure_of_memE) 

400 

401 
lemma (in equivalence) complete_classes: 

402 
assumes c: "is_closed A" 

403 
shows "A = closure_of A" 

404 
using assms 

405 
by (blast intro: closure_of_memI elem_exact dest: is_closedD1 is_closedD2 closure_of_memE) 

406 
*) 

407 

408 
end 