equal
deleted
inserted
replaced
385 "nat z == contents (\<Union>(x,y) \<in> Rep_Integ z. { x-y })" |
385 "nat z == contents (\<Union>(x,y) \<in> Rep_Integ z. { x-y })" |
386 |
386 |
387 lemma nat: "nat (Abs_Integ (intrel``{(x,y)})) = x-y" |
387 lemma nat: "nat (Abs_Integ (intrel``{(x,y)})) = x-y" |
388 proof - |
388 proof - |
389 have "(\<lambda>(x,y). {x-y}) respects intrel" |
389 have "(\<lambda>(x,y). {x-y}) respects intrel" |
390 by (simp add: congruent_def, arith) |
390 by (simp add: congruent_def, arith) |
391 thus ?thesis |
391 thus ?thesis |
392 by (simp add: nat_def UN_equiv_class [OF equiv_intrel]) |
392 by (simp add: nat_def UN_equiv_class [OF equiv_intrel]) |
393 qed |
393 qed |
394 |
394 |
395 lemma nat_int [simp]: "nat(int n) = n" |
395 lemma nat_int [simp]: "nat(int n) = n" |