equal
deleted
inserted
replaced
8 *) |
8 *) |
9 |
9 |
10 header {* Development of the Reals using Cauchy Sequences *} |
10 header {* Development of the Reals using Cauchy Sequences *} |
11 |
11 |
12 theory Real |
12 theory Real |
13 imports Rat Conditional_Complete_Lattices |
13 imports Rat Conditionally_Complete_Lattices |
14 begin |
14 begin |
15 |
15 |
16 text {* |
16 text {* |
17 This theory contains a formalization of the real numbers as |
17 This theory contains a formalization of the real numbers as |
18 equivalence classes of Cauchy sequences of rationals. See |
18 equivalence classes of Cauchy sequences of rationals. See |
923 show "\<exists>y. (\<forall>x\<in>S. x \<le> y) \<and> (\<forall>z. (\<forall>x\<in>S. x \<le> z) \<longrightarrow> y \<le> z)" |
923 show "\<exists>y. (\<forall>x\<in>S. x \<le> y) \<and> (\<forall>z. (\<forall>x\<in>S. x \<le> z) \<longrightarrow> y \<le> z)" |
924 using 1 2 3 by (rule_tac x="Real B" in exI, simp) |
924 using 1 2 3 by (rule_tac x="Real B" in exI, simp) |
925 qed |
925 qed |
926 |
926 |
927 |
927 |
928 instantiation real :: conditional_complete_linorder |
928 instantiation real :: conditionally_complete_linorder |
929 begin |
929 begin |
930 |
930 |
931 subsection{*Supremum of a set of reals*} |
931 subsection{*Supremum of a set of reals*} |
932 |
932 |
933 definition |
933 definition |