src/HOL/Real/RComplete.thy
changeset 14387 e96d5c42c4b0
parent 14365 3d4df8c166ae
child 14476 758e7acdea2f
equal deleted inserted replaced
14386:ad1ffcc90162 14387:e96d5c42c4b0
     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)