equal
deleted
inserted
replaced
474 lemma inverse_Real: |
474 lemma inverse_Real: |
475 assumes X: "cauchy X" |
475 assumes X: "cauchy X" |
476 shows "inverse (Real X) = |
476 shows "inverse (Real X) = |
477 (if vanishes X then 0 else Real (\<lambda>n. inverse (X n)))" |
477 (if vanishes X then 0 else Real (\<lambda>n. inverse (X n)))" |
478 using assms inverse_real.transfer zero_real.transfer |
478 using assms inverse_real.transfer zero_real.transfer |
479 unfolding cr_real_eq rel_fun_def by (simp split: split_if_asm, metis) |
479 unfolding cr_real_eq rel_fun_def by (simp split: if_split_asm, metis) |
480 |
480 |
481 instance proof |
481 instance proof |
482 fix a b c :: real |
482 fix a b c :: real |
483 show "a + b = b + a" |
483 show "a + b = b + a" |
484 by transfer (simp add: ac_simps realrel_def) |
484 by transfer (simp add: ac_simps realrel_def) |