equal
deleted
inserted
replaced
42 ultimately have "a * b'' = a'' * b" by simp |
42 ultimately have "a * b'' = a'' * b" by simp |
43 with A B show "((a, b), (a'', b'')) \<in> ratrel" by auto |
43 with A B show "((a, b), (a'', b'')) \<in> ratrel" by auto |
44 qed |
44 qed |
45 |
45 |
46 lemma equiv_ratrel: "equiv {x. snd x \<noteq> 0} ratrel" |
46 lemma equiv_ratrel: "equiv {x. snd x \<noteq> 0} ratrel" |
47 by (rule equiv.intro [OF refl_on_ratrel sym_ratrel trans_ratrel]) |
47 by (rule equivI [OF refl_on_ratrel sym_ratrel trans_ratrel]) |
48 |
48 |
49 lemmas UN_ratrel = UN_equiv_class [OF equiv_ratrel] |
49 lemmas UN_ratrel = UN_equiv_class [OF equiv_ratrel] |
50 lemmas UN_ratrel2 = UN_equiv_class2 [OF equiv_ratrel equiv_ratrel] |
50 lemmas UN_ratrel2 = UN_equiv_class2 [OF equiv_ratrel equiv_ratrel] |
51 |
51 |
52 lemma equiv_ratrel_iff [iff]: |
52 lemma equiv_ratrel_iff [iff]: |