equal
deleted
inserted
replaced
371 |
371 |
372 quotient_type real = "nat \<Rightarrow> rat" / partial: realrel |
372 quotient_type real = "nat \<Rightarrow> rat" / partial: realrel |
373 morphisms rep_real Real |
373 morphisms rep_real Real |
374 by (rule part_equivp_realrel) |
374 by (rule part_equivp_realrel) |
375 |
375 |
376 lemma cr_real_eq: "cr_real = (\<lambda>x y. cauchy x \<and> Real x = y)" |
376 lemma cr_real_eq: "pcr_real = (\<lambda>x y. cauchy x \<and> Real x = y)" |
377 unfolding cr_real_def realrel_def by simp |
377 unfolding real.pcr_cr_eq cr_real_def realrel_def by auto |
378 |
378 |
379 lemma Real_induct [induct type: real]: (* TODO: generate automatically *) |
379 lemma Real_induct [induct type: real]: (* TODO: generate automatically *) |
380 assumes "\<And>X. cauchy X \<Longrightarrow> P (Real X)" shows "P x" |
380 assumes "\<And>X. cauchy X \<Longrightarrow> P (Real X)" shows "P x" |
381 proof (induct x) |
381 proof (induct x) |
382 case (1 X) |
382 case (1 X) |
385 qed |
385 qed |
386 |
386 |
387 lemma eq_Real: |
387 lemma eq_Real: |
388 "cauchy X \<Longrightarrow> cauchy Y \<Longrightarrow> Real X = Real Y \<longleftrightarrow> vanishes (\<lambda>n. X n - Y n)" |
388 "cauchy X \<Longrightarrow> cauchy Y \<Longrightarrow> Real X = Real Y \<longleftrightarrow> vanishes (\<lambda>n. X n - Y n)" |
389 using real.rel_eq_transfer |
389 using real.rel_eq_transfer |
390 unfolding cr_real_def fun_rel_def realrel_def by simp |
390 unfolding real.pcr_cr_eq cr_real_def fun_rel_def realrel_def by simp |
391 |
391 |
392 declare real.forall_transfer [transfer_rule del] |
392 declare real.forall_transfer [transfer_rule del] |
393 |
393 |
394 lemma forall_real_transfer [transfer_rule]: (* TODO: generate automatically *) |
394 lemma forall_real_transfer [transfer_rule]: (* TODO: generate automatically *) |
395 "(fun_rel (fun_rel cr_real op =) op =) |
395 "(fun_rel (fun_rel pcr_real op =) op =) |
396 (transfer_bforall cauchy) transfer_forall" |
396 (transfer_bforall cauchy) transfer_forall" |
397 using Quotient_forall_transfer [OF Quotient_real] |
397 using real.forall_transfer |
398 by (simp add: realrel_def) |
398 by (simp add: realrel_def) |
399 |
399 |
400 instantiation real :: field_inverse_zero |
400 instantiation real :: field_inverse_zero |
401 begin |
401 begin |
402 |
402 |