src/HOL/Real/RComplete.thy
 changeset 14387 e96d5c42c4b0 parent 14365 3d4df8c166ae child 14476 758e7acdea2f
equal inserted replaced
`     6                   reals and reals `
`     6                   reals and reals `
`     7 *) `
`     7 *) `
`     8 `
`     8 `
`     9 header{*Completeness Theorems for Positive Reals and Reals.*}`
`     9 header{*Completeness Theorems for Positive Reals and Reals.*}`
`    10 `
`    10 `
`    11 theory RComplete = Lubs + RealArith:`
`    11 theory RComplete = Lubs + RealDef:`
`    12 `
`    12 `
`    13 lemma real_sum_of_halves: "x/2 + x/2 = (x::real)"`
`    13 lemma real_sum_of_halves: "x/2 + x/2 = (x::real)"`
`    14 apply (simp)`
`    14 by simp`
`    15 done`
`       `
`    16 `
`    15 `
`    17 `
`    16 `
`    18 subsection{*Completeness of Reals by Supremum Property of type @{typ preal}*} `
`    17 subsection{*Completeness of Reals by Supremum Property of type @{typ preal}*} `
`    19 `
`    18 `
`    20  (*a few lemmas*)`
`    19  (*a few lemmas*)`
`    30 apply (rule conjI)`
`    29 apply (rule conjI)`
`    31 apply (blast dest: bspec real_gt_zero_preal_Ex [THEN iffD1], auto)`
`    30 apply (blast dest: bspec real_gt_zero_preal_Ex [THEN iffD1], auto)`
`    32 apply (drule bspec, assumption)`
`    31 apply (drule bspec, assumption)`
`    33 apply (frule bspec, assumption)`
`    32 apply (frule bspec, assumption)`
`    34 apply (drule order_less_trans, assumption)`
`    33 apply (drule order_less_trans, assumption)`
`    35 apply (drule real_gt_zero_preal_Ex [THEN iffD1])`
`    34 apply (drule real_gt_zero_preal_Ex [THEN iffD1], force) `
`    36 apply (force) `
`       `
`    37 done`
`    35 done`
`    38 `
`    36 `
`    39 (*-------------------------------------------------------------`
`    37 (*-------------------------------------------------------------`
`    40             Completeness of Positive Reals`
`    38             Completeness of Positive Reals`
`    41  -------------------------------------------------------------*)`
`    39  -------------------------------------------------------------*)`
`    53 apply (rule_tac x = "real_of_preal (psup ({w. real_of_preal w \<in> P}))" in exI)`
`    51 apply (rule_tac x = "real_of_preal (psup ({w. real_of_preal w \<in> P}))" in exI)`
`    54 apply clarify`
`    52 apply clarify`
`    55 apply (case_tac "0 < ya", auto)`
`    53 apply (case_tac "0 < ya", auto)`
`    56 apply (frule real_sup_lemma2, assumption+)`
`    54 apply (frule real_sup_lemma2, assumption+)`
`    57 apply (drule real_gt_zero_preal_Ex [THEN iffD1])`
`    55 apply (drule real_gt_zero_preal_Ex [THEN iffD1])`
`    58 apply (drule_tac [3] real_less_all_real2)`
`    56 apply (drule_tac [3] real_less_all_real2, auto)`
`    59 apply (auto)`
`       `
`    60 apply (rule preal_complete [THEN iffD1])`
`    57 apply (rule preal_complete [THEN iffD1])`
`    61 apply (auto intro: order_less_imp_le)`
`    58 apply (auto intro: order_less_imp_le)`
`    62 apply (frule real_gt_preal_preal_Ex)`
`    59 apply (frule real_gt_preal_preal_Ex, force)`
`    63 apply (force)`
`       `
`    64 (* second part *)`
`    60 (* second part *)`
`    65 apply (rule real_sup_lemma1 [THEN iffD2], assumption)`
`    61 apply (rule real_sup_lemma1 [THEN iffD2], assumption)`
`    66 apply (auto dest!: real_less_all_real2 real_gt_zero_preal_Ex [THEN iffD1])`
`    62 apply (auto dest!: real_less_all_real2 real_gt_zero_preal_Ex [THEN iffD1])`
`    67 apply (frule_tac [2] real_sup_lemma2)`
`    63 apply (frule_tac [2] real_sup_lemma2)`
`    68 apply (frule real_sup_lemma2, assumption+, clarify) `
`    64 apply (frule real_sup_lemma2, assumption+, clarify) `
`   129       ==> \<exists>t. isLub (UNIV :: real set) S t"`
`   125       ==> \<exists>t. isLub (UNIV :: real set) S t"`
`   130 apply safe`
`   126 apply safe`
`   131 apply (subgoal_tac "\<exists>u. u\<in> {z. \<exists>x \<in>S. z = x + (-X) + 1} Int {x. 0 < x}")`
`   127 apply (subgoal_tac "\<exists>u. u\<in> {z. \<exists>x \<in>S. z = x + (-X) + 1} Int {x. 0 < x}")`
`   132 apply (subgoal_tac "isUb (UNIV::real set) ({z. \<exists>x \<in>S. z = x + (-X) + 1} Int {x. 0 < x}) (Y + (-X) + 1) ")`
`   128 apply (subgoal_tac "isUb (UNIV::real set) ({z. \<exists>x \<in>S. z = x + (-X) + 1} Int {x. 0 < x}) (Y + (-X) + 1) ")`
`   133 apply (cut_tac P = S and xa = X in real_sup_lemma3)`
`   129 apply (cut_tac P = S and xa = X in real_sup_lemma3)`
`   134 apply (frule posreals_complete [OF _ _ exI], blast, blast) `
`   130 apply (frule posreals_complete [OF _ _ exI], blast, blast, safe)`
`   135 apply safe`
`       `
`   136 apply (rule_tac x = "t + X + (- 1) " in exI)`
`   131 apply (rule_tac x = "t + X + (- 1) " in exI)`
`   137 apply (rule isLubI2)`
`   132 apply (rule isLubI2)`
`   138 apply (rule_tac [2] setgeI, safe)`
`   133 apply (rule_tac [2] setgeI, safe)`
`   139 apply (subgoal_tac [2] "isUb (UNIV:: real set) ({z. \<exists>x \<in>S. z = x + (-X) + 1} Int {x. 0 < x}) (y + (-X) + 1) ")`
`   134 apply (subgoal_tac [2] "isUb (UNIV:: real set) ({z. \<exists>x \<in>S. z = x + (-X) + 1} Int {x. 0 < x}) (y + (-X) + 1) ")`
`   140 apply (drule_tac [2] y = " (y + (- X) + 1) " in isLub_le_isUb)`
`   135 apply (drule_tac [2] y = " (y + (- X) + 1) " in isLub_le_isUb)`