329 apply simp |
326 apply simp |
330 apply(fastsimp simp add:inj_on_def) |
327 apply(fastsimp simp add:inj_on_def) |
331 apply simp |
328 apply simp |
332 done |
329 done |
333 |
330 |
|
331 |
|
332 subsection {* Equivalence relations -- predicate version *} |
|
333 |
|
334 text {* Partial equivalences *} |
|
335 |
|
336 definition part_equivp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where |
|
337 "part_equivp R \<longleftrightarrow> (\<exists>x. R x x) \<and> (\<forall>x y. R x y \<longleftrightarrow> R x x \<and> R y y \<and> R x = R y)" |
|
338 -- {* John-Harrison-style characterization *} |
|
339 |
|
340 lemma part_equivpI: |
|
341 "(\<exists>x. R x x) \<Longrightarrow> symp R \<Longrightarrow> transp R \<Longrightarrow> part_equivp R" |
|
342 by (auto simp add: part_equivp_def mem_def) (auto elim: sympE transpE) |
|
343 |
|
344 lemma part_equivpE: |
|
345 assumes "part_equivp R" |
|
346 obtains x where "R x x" and "symp R" and "transp R" |
|
347 proof - |
|
348 from assms have 1: "\<exists>x. R x x" |
|
349 and 2: "\<And>x y. R x y \<longleftrightarrow> R x x \<and> R y y \<and> R x = R y" |
|
350 by (unfold part_equivp_def) blast+ |
|
351 from 1 obtain x where "R x x" .. |
|
352 moreover have "symp R" |
|
353 proof (rule sympI) |
|
354 fix x y |
|
355 assume "R x y" |
|
356 with 2 [of x y] show "R y x" by auto |
|
357 qed |
|
358 moreover have "transp R" |
|
359 proof (rule transpI) |
|
360 fix x y z |
|
361 assume "R x y" and "R y z" |
|
362 with 2 [of x y] 2 [of y z] show "R x z" by auto |
|
363 qed |
|
364 ultimately show thesis by (rule that) |
|
365 qed |
|
366 |
|
367 lemma part_equivp_refl_symp_transp: |
|
368 "part_equivp R \<longleftrightarrow> (\<exists>x. R x x) \<and> symp R \<and> transp R" |
|
369 by (auto intro: part_equivpI elim: part_equivpE) |
|
370 |
|
371 lemma part_equivp_symp: |
|
372 "part_equivp R \<Longrightarrow> R x y \<Longrightarrow> R y x" |
|
373 by (erule part_equivpE, erule sympE) |
|
374 |
|
375 lemma part_equivp_transp: |
|
376 "part_equivp R \<Longrightarrow> R x y \<Longrightarrow> R y z \<Longrightarrow> R x z" |
|
377 by (erule part_equivpE, erule transpE) |
|
378 |
|
379 lemma part_equivp_typedef: |
|
380 "part_equivp R \<Longrightarrow> \<exists>d. d \<in> (\<lambda>c. \<exists>x. R x x \<and> c = R x)" |
|
381 by (auto elim: part_equivpE simp add: mem_def) |
|
382 |
|
383 |
|
384 text {* Total equivalences *} |
|
385 |
|
386 definition equivp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where |
|
387 "equivp R \<longleftrightarrow> (\<forall>x y. R x y = (R x = R y))" -- {* John-Harrison-style characterization *} |
|
388 |
|
389 lemma equivpI: |
|
390 "reflp R \<Longrightarrow> symp R \<Longrightarrow> transp R \<Longrightarrow> equivp R" |
|
391 by (auto elim: reflpE sympE transpE simp add: equivp_def mem_def) |
|
392 |
|
393 lemma equivpE: |
|
394 assumes "equivp R" |
|
395 obtains "reflp R" and "symp R" and "transp R" |
|
396 using assms by (auto intro!: that reflpI sympI transpI simp add: equivp_def) |
|
397 |
|
398 lemma equivp_implies_part_equivp: |
|
399 "equivp R \<Longrightarrow> part_equivp R" |
|
400 by (auto intro: part_equivpI elim: equivpE reflpE) |
|
401 |
|
402 lemma equivp_equiv: |
|
403 "equiv UNIV A \<longleftrightarrow> equivp (\<lambda>x y. (x, y) \<in> A)" |
|
404 by (auto intro: equivpI elim: equivpE simp add: equiv_def reflp_def symp_def transp_def) |
|
405 |
|
406 lemma equivp_reflp_symp_transp: |
|
407 shows "equivp R \<longleftrightarrow> reflp R \<and> symp R \<and> transp R" |
|
408 by (auto intro: equivpI elim: equivpE) |
|
409 |
|
410 lemma identity_equivp: |
|
411 "equivp (op =)" |
|
412 by (auto intro: equivpI reflpI sympI transpI) |
|
413 |
|
414 lemma equivp_reflp: |
|
415 "equivp R \<Longrightarrow> R x x" |
|
416 by (erule equivpE, erule reflpE) |
|
417 |
|
418 lemma equivp_symp: |
|
419 "equivp R \<Longrightarrow> R x y \<Longrightarrow> R y x" |
|
420 by (erule equivpE, erule sympE) |
|
421 |
|
422 lemma equivp_transp: |
|
423 "equivp R \<Longrightarrow> R x y \<Longrightarrow> R y z \<Longrightarrow> R x z" |
|
424 by (erule equivpE, erule transpE) |
|
425 |
334 end |
426 end |