equal
deleted
inserted
replaced
33 |
33 |
34 lemma equivpI: |
34 lemma equivpI: |
35 assumes "reflp R" "symp R" "transp R" |
35 assumes "reflp R" "symp R" "transp R" |
36 shows "equivp R" |
36 shows "equivp R" |
37 using assms by (simp add: equivp_reflp_symp_transp) |
37 using assms by (simp add: equivp_reflp_symp_transp) |
|
38 |
|
39 lemma eq_imp_rel: |
|
40 shows "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b" |
|
41 by (simp add: equivp_reflp) |
38 |
42 |
39 definition |
43 definition |
40 "part_equivp E \<equiv> (\<exists>x. E x x) \<and> (\<forall>x y. E x y = (E x x \<and> E y y \<and> (E x = E y)))" |
44 "part_equivp E \<equiv> (\<exists>x. E x x) \<and> (\<forall>x y. E x y = (E x x \<and> E y y \<and> (E x = E y)))" |
41 |
45 |
42 lemma equivp_IMP_part_equivp: |
46 lemma equivp_IMP_part_equivp: |
378 apply metis |
382 apply metis |
379 apply metis |
383 apply metis |
380 apply rule+ |
384 apply rule+ |
381 apply (erule_tac x="xb" in ballE) |
385 apply (erule_tac x="xb" in ballE) |
382 prefer 2 |
386 prefer 2 |
383 apply (metis in_respects) |
387 apply (metis) |
384 apply (erule_tac x="ya" in ballE) |
388 apply (erule_tac x="ya" in ballE) |
385 prefer 2 |
389 prefer 2 |
386 apply (metis in_respects) |
390 apply (metis) |
387 apply (metis in_respects) |
391 apply (metis in_respects) |
388 apply (erule conjE)+ |
392 apply (erule conjE)+ |
389 apply (erule bexE) |
393 apply (erule bexE) |
390 apply rule |
394 apply rule |
391 apply (rule_tac x="xa" in bexI) |
395 apply (rule_tac x="xa" in bexI) |
392 apply metis |
396 apply metis |
393 apply metis |
397 apply metis |
394 apply rule+ |
398 apply rule+ |
395 apply (erule_tac x="xb" in ballE) |
399 apply (erule_tac x="xb" in ballE) |
396 prefer 2 |
400 prefer 2 |
397 apply (metis in_respects) |
401 apply (metis) |
398 apply (erule_tac x="ya" in ballE) |
402 apply (erule_tac x="ya" in ballE) |
399 prefer 2 |
403 prefer 2 |
400 apply (metis in_respects) |
404 apply (metis) |
401 apply (metis in_respects) |
405 apply (metis in_respects) |
402 done |
406 done |
403 |
407 |
404 lemma babs_rsp: |
408 lemma babs_rsp: |
405 assumes q: "Quotient R1 Abs1 Rep1" |
409 assumes q: "Quotient R1 Abs1 Rep1" |