src/HOL/ex/Dedekind_Real.thy
changeset 45694 4a8743618257
parent 41541 1fa4725c4656
child 46905 6b1c0a80a57a
     1.1 --- a/src/HOL/ex/Dedekind_Real.thy	Wed Nov 30 16:05:15 2011 +0100
     1.2 +++ b/src/HOL/ex/Dedekind_Real.thy	Wed Nov 30 16:27:10 2011 +0100
     1.3 @@ -44,8 +44,10 @@
     1.4  qed
     1.5  
     1.6  
     1.7 -typedef preal = "{A. cut A}"
     1.8 -  by (blast intro: cut_of_rat [OF zero_less_one])
     1.9 +definition "preal = {A. cut A}"
    1.10 +
    1.11 +typedef (open) preal = preal
    1.12 +  unfolding preal_def by (blast intro: cut_of_rat [OF zero_less_one])
    1.13  
    1.14  definition
    1.15    psup :: "preal set => preal" where
    1.16 @@ -113,22 +115,26 @@
    1.17  by (simp add: preal_def cut_of_rat)
    1.18  
    1.19  lemma preal_nonempty: "A \<in> preal ==> \<exists>x\<in>A. 0 < x"
    1.20 -by (unfold preal_def cut_def, blast)
    1.21 +  unfolding preal_def cut_def_raw by blast
    1.22  
    1.23  lemma preal_Ex_mem: "A \<in> preal \<Longrightarrow> \<exists>x. x \<in> A"
    1.24 -by (drule preal_nonempty, fast)
    1.25 +  apply (drule preal_nonempty)
    1.26 +  apply fast
    1.27 +  done
    1.28  
    1.29  lemma preal_imp_psubset_positives: "A \<in> preal ==> A < {r. 0 < r}"
    1.30 -by (force simp add: preal_def cut_def)
    1.31 +  by (force simp add: preal_def cut_def)
    1.32  
    1.33  lemma preal_exists_bound: "A \<in> preal ==> \<exists>x. 0 < x & x \<notin> A"
    1.34 -by (drule preal_imp_psubset_positives, auto)
    1.35 +  apply (drule preal_imp_psubset_positives)
    1.36 +  apply auto
    1.37 +  done
    1.38  
    1.39  lemma preal_exists_greater: "[| A \<in> preal; y \<in> A |] ==> \<exists>u \<in> A. y < u"
    1.40 -by (unfold preal_def cut_def, blast)
    1.41 +  unfolding preal_def cut_def_raw by blast
    1.42  
    1.43  lemma preal_downwards_closed: "[| A \<in> preal; y \<in> A; 0 < z; z < y |] ==> z \<in> A"
    1.44 -by (unfold preal_def cut_def, blast)
    1.45 +  unfolding preal_def cut_def_raw by blast
    1.46  
    1.47  text{*Relaxing the final premise*}
    1.48  lemma preal_downwards_closed':
    1.49 @@ -960,7 +966,7 @@
    1.50  
    1.51  lemma mem_diff_set:
    1.52       "R < S ==> diff_set (Rep_preal S) (Rep_preal R) \<in> preal"
    1.53 -apply (unfold preal_def cut_def)
    1.54 +apply (unfold preal_def cut_def_raw)
    1.55  apply (blast intro!: diff_set_not_empty diff_set_not_rat_set
    1.56                       diff_set_lemma3 diff_set_lemma4)
    1.57  done
    1.58 @@ -1129,7 +1135,7 @@
    1.59  
    1.60  lemma preal_sup:
    1.61       "[|P \<noteq> {}; \<forall>X \<in> P. X \<le> Y|] ==> (\<Union>X \<in> P. Rep_preal(X)) \<in> preal"
    1.62 -apply (unfold preal_def cut_def)
    1.63 +apply (unfold preal_def cut_def_raw)
    1.64  apply (blast intro!: preal_sup_set_not_empty preal_sup_set_not_rat_set
    1.65                       preal_sup_set_lemma3 preal_sup_set_lemma4)
    1.66  done
    1.67 @@ -1163,8 +1169,11 @@
    1.68    realrel   ::  "((preal * preal) * (preal * preal)) set" where
    1.69    "realrel = {p. \<exists>x1 y1 x2 y2. p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1}"
    1.70  
    1.71 -typedef (Real)  real = "UNIV//realrel"
    1.72 -  by (auto simp add: quotient_def)
    1.73 +definition "Real = UNIV//realrel"
    1.74 +
    1.75 +typedef (open) real = Real
    1.76 +  morphisms Rep_Real Abs_Real
    1.77 +  unfolding Real_def by (auto simp add: quotient_def)
    1.78  
    1.79  definition
    1.80    (** these don't use the overloaded "real" function: users don't see them **)