# HG changeset patch
# User haftmann
# Date 1427133914 -3600
# Node ID 2d9cf954a8297624216df97a4d382201d3860cd6
# Parent  6320064f22bba3026c4198a72730b7b1914f540f
modernized

diff -r 6320064f22bb -r 2d9cf954a829 src/HOL/ex/Dedekind_Real.thy
--- a/src/HOL/ex/Dedekind_Real.thy	Wed Mar 25 17:51:34 2015 +0100
+++ b/src/HOL/ex/Dedekind_Real.thy	Mon Mar 23 19:05:14 2015 +0100
@@ -44,10 +44,16 @@
 qed
 
 
-definition "preal = {A. cut A}"
+typedef preal = "Collect cut"
+  by (blast intro: cut_of_rat [OF zero_less_one])
 
-typedef preal = preal
-  unfolding preal_def by (blast intro: cut_of_rat [OF zero_less_one])
+lemma Abs_preal_induct [induct type: preal]:
+  "(\<And>x. cut x \<Longrightarrow> P (Abs_preal x)) \<Longrightarrow> P x"
+  using Abs_preal_induct [of P x] by simp
+
+lemma Rep_preal:
+  "cut (Rep_preal x)"
+  using Rep_preal [of x] by simp
 
 definition
   psup :: "preal set => preal" where
@@ -111,34 +117,34 @@
 declare Abs_preal_inject [simp]
 declare Abs_preal_inverse [simp]
 
-lemma rat_mem_preal: "0 < q ==> {r::rat. 0 < r & r < q} \<in> preal"
-by (simp add: preal_def cut_of_rat)
+lemma rat_mem_preal: "0 < q ==> cut {r::rat. 0 < r & r < q}"
+by (simp add: cut_of_rat)
 
-lemma preal_nonempty: "A \<in> preal ==> \<exists>x\<in>A. 0 < x"
-  unfolding preal_def cut_def [abs_def] by blast
+lemma preal_nonempty: "cut A ==> \<exists>x\<in>A. 0 < x"
+  unfolding cut_def [abs_def] by blast
 
-lemma preal_Ex_mem: "A \<in> preal \<Longrightarrow> \<exists>x. x \<in> A"
+lemma preal_Ex_mem: "cut A \<Longrightarrow> \<exists>x. x \<in> A"
   apply (drule preal_nonempty)
   apply fast
   done
 
-lemma preal_imp_psubset_positives: "A \<in> preal ==> A < {r. 0 < r}"
-  by (force simp add: preal_def cut_def)
+lemma preal_imp_psubset_positives: "cut A ==> A < {r. 0 < r}"
+  by (force simp add: cut_def)
 
-lemma preal_exists_bound: "A \<in> preal ==> \<exists>x. 0 < x & x \<notin> A"
+lemma preal_exists_bound: "cut A ==> \<exists>x. 0 < x & x \<notin> A"
   apply (drule preal_imp_psubset_positives)
   apply auto
   done
 
-lemma preal_exists_greater: "[| A \<in> preal; y \<in> A |] ==> \<exists>u \<in> A. y < u"
-  unfolding preal_def cut_def [abs_def] by blast
+lemma preal_exists_greater: "[| cut A; y \<in> A |] ==> \<exists>u \<in> A. y < u"
+  unfolding cut_def [abs_def] by blast
 
-lemma preal_downwards_closed: "[| A \<in> preal; y \<in> A; 0 < z; z < y |] ==> z \<in> A"
-  unfolding preal_def cut_def [abs_def] by blast
+lemma preal_downwards_closed: "[| cut A; y \<in> A; 0 < z; z < y |] ==> z \<in> A"
+  unfolding cut_def [abs_def] by blast
 
 text{*Relaxing the final premise*}
 lemma preal_downwards_closed':
-     "[| A \<in> preal; y \<in> A; 0 < z; z \<le> y |] ==> z \<in> A"
+     "[| cut A; y \<in> A; 0 < z; z \<le> y |] ==> z \<in> A"
 apply (simp add: order_le_less)
 apply (blast intro: preal_downwards_closed)
 done
@@ -147,7 +153,7 @@
  Gleason p. 122 - Remark (1)*}
 
 lemma not_in_preal_ub:
-  assumes A: "A \<in> preal"
+  assumes A: "cut A"
     and notx: "x \<notin> A"
     and y: "y \<in> A"
     and pos: "0 < x"
@@ -167,6 +173,7 @@
 text {* preal lemmas instantiated to @{term "Rep_preal X"} *}
 
 lemma mem_Rep_preal_Ex: "\<exists>x. x \<in> Rep_preal X"
+thm preal_Ex_mem
 by (rule preal_Ex_mem [OF Rep_preal])
 
 lemma Rep_preal_exists_bound: "\<exists>x>0. x \<notin> Rep_preal X"
@@ -195,7 +202,7 @@
   by (auto simp add: preal_le_def preal_less_def Rep_preal_inject)
 qed  
 
-lemma preal_imp_pos: "[|A \<in> preal; r \<in> A|] ==> 0 < r"
+lemma preal_imp_pos: "[|cut A; r \<in> A|] ==> 0 < r"
 by (insert preal_imp_psubset_positives, blast)
 
 instance preal :: linorder
@@ -237,7 +244,7 @@
 
 text{*Part 1 of Dedekind sections definition*}
 lemma add_set_not_empty:
-     "[|A \<in> preal; B \<in> preal|] ==> {} \<subset> add_set A B"
+     "[|cut A; cut B|] ==> {} \<subset> add_set A B"
 apply (drule preal_nonempty)+
 apply (auto simp add: add_set_def)
 done
@@ -245,7 +252,7 @@
 text{*Part 2 of Dedekind sections definition.  A structured version of
 this proof is @{text preal_not_mem_mult_set_Ex} below.*}
 lemma preal_not_mem_add_set_Ex:
-     "[|A \<in> preal; B \<in> preal|] ==> \<exists>q>0. q \<notin> add_set A B"
+     "[|cut A; cut B|] ==> \<exists>q>0. q \<notin> add_set A B"
 apply (insert preal_exists_bound [of A] preal_exists_bound [of B], auto) 
 apply (rule_tac x = "x+xa" in exI)
 apply (simp add: add_set_def, clarify)
@@ -254,8 +261,8 @@
 done
 
 lemma add_set_not_rat_set:
-   assumes A: "A \<in> preal" 
-       and B: "B \<in> preal"
+   assumes A: "cut A" 
+       and B: "cut B"
      shows "add_set A B < {r. 0 < r}"
 proof
   from preal_imp_pos [OF A] preal_imp_pos [OF B]
@@ -267,12 +274,12 @@
 
 text{*Part 3 of Dedekind sections definition*}
 lemma add_set_lemma3:
-     "[|A \<in> preal; B \<in> preal; u \<in> add_set A B; 0 < z; z < u|] 
+     "[|cut A; cut B; u \<in> add_set A B; 0 < z; z < u|] 
       ==> z \<in> add_set A B"
 proof (unfold add_set_def, clarify)
   fix x::rat and y::rat
-  assume A: "A \<in> preal" 
-    and B: "B \<in> preal"
+  assume A: "cut A" 
+    and B: "cut B"
     and [simp]: "0 < z"
     and zless: "z < x + y"
     and x:  "x \<in> A"
@@ -310,7 +317,7 @@
 
 text{*Part 4 of Dedekind sections definition*}
 lemma add_set_lemma4:
-     "[|A \<in> preal; B \<in> preal; y \<in> add_set A B|] ==> \<exists>u \<in> add_set A B. y < u"
+     "[|cut A; cut B; y \<in> add_set A B|] ==> \<exists>u \<in> add_set A B. y < u"
 apply (auto simp add: add_set_def)
 apply (frule preal_exists_greater [of A], auto) 
 apply (rule_tac x="u + ya" in exI)
@@ -318,8 +325,8 @@
 done
 
 lemma mem_add_set:
-     "[|A \<in> preal; B \<in> preal|] ==> add_set A B \<in> preal"
-apply (simp (no_asm_simp) add: preal_def cut_def)
+     "[|cut A; cut B|] ==> cut (add_set A B)"
+apply (simp (no_asm_simp) add: cut_def)
 apply (blast intro!: add_set_not_empty add_set_not_rat_set
                      add_set_lemma3 add_set_lemma4)
 done
@@ -353,15 +360,15 @@
 
 text{*Part 1 of Dedekind sections definition*}
 lemma mult_set_not_empty:
-     "[|A \<in> preal; B \<in> preal|] ==> {} \<subset> mult_set A B"
+     "[|cut A; cut B|] ==> {} \<subset> mult_set A B"
 apply (insert preal_nonempty [of A] preal_nonempty [of B]) 
 apply (auto simp add: mult_set_def)
 done
 
 text{*Part 2 of Dedekind sections definition*}
 lemma preal_not_mem_mult_set_Ex:
-  assumes A: "A \<in> preal" 
-    and B: "B \<in> preal"
+  assumes A: "cut A" 
+    and B: "cut B"
   shows "\<exists>q. 0 < q & q \<notin> mult_set A B"
 proof -
   from preal_exists_bound [OF A] obtain x where 1 [simp]: "0 < x" "x \<notin> A" by blast
@@ -389,8 +396,8 @@
 qed
 
 lemma mult_set_not_rat_set:
-  assumes A: "A \<in> preal" 
-    and B: "B \<in> preal"
+  assumes A: "cut A" 
+    and B: "cut B"
   shows "mult_set A B < {r. 0 < r}"
 proof
   show "mult_set A B \<subseteq> {r. 0 < r}"
@@ -404,12 +411,12 @@
 
 text{*Part 3 of Dedekind sections definition*}
 lemma mult_set_lemma3:
-     "[|A \<in> preal; B \<in> preal; u \<in> mult_set A B; 0 < z; z < u|] 
+     "[|cut A; cut B; u \<in> mult_set A B; 0 < z; z < u|] 
       ==> z \<in> mult_set A B"
 proof (unfold mult_set_def, clarify)
   fix x::rat and y::rat
-  assume A: "A \<in> preal" 
-    and B: "B \<in> preal"
+  assume A: "cut A" 
+    and B: "cut B"
     and [simp]: "0 < z"
     and zless: "z < x * y"
     and x:  "x \<in> A"
@@ -436,7 +443,7 @@
 
 text{*Part 4 of Dedekind sections definition*}
 lemma mult_set_lemma4:
-     "[|A \<in> preal; B \<in> preal; y \<in> mult_set A B|] ==> \<exists>u \<in> mult_set A B. y < u"
+     "[|cut A; cut B; y \<in> mult_set A B|] ==> \<exists>u \<in> mult_set A B. y < u"
 apply (auto simp add: mult_set_def)
 apply (frule preal_exists_greater [of A], auto) 
 apply (rule_tac x="u * ya" in exI)
@@ -446,8 +453,8 @@
 
 
 lemma mem_mult_set:
-     "[|A \<in> preal; B \<in> preal|] ==> mult_set A B \<in> preal"
-apply (simp (no_asm_simp) add: preal_def cut_def)
+     "[|cut A; cut B|] ==> cut (mult_set A B)"
+apply (simp (no_asm_simp) add: cut_def)
 apply (blast intro!: mult_set_not_empty mult_set_not_rat_set
                      mult_set_lemma3 mult_set_lemma4)
 done
@@ -470,7 +477,7 @@
 lemma preal_mult_1: "(1::preal) * z = z"
 proof (induct z)
   fix A :: "rat set"
-  assume A: "A \<in> preal"
+  assume A: "cut A"
   have "{w. \<exists>u. 0 < u \<and> u < 1 & (\<exists>v \<in> A. w = u * v)} = A" (is "?lhs = A")
   proof
     show "?lhs \<subseteq> A"
@@ -588,7 +595,7 @@
 subsection{*Existence of Inverse, a Positive Real*}
 
 lemma mem_inv_set_ex:
-  assumes A: "A \<in> preal" shows "\<exists>x y. 0 < x & x < y & inverse y \<notin> A"
+  assumes A: "cut A" shows "\<exists>x y. 0 < x & x < y & inverse y \<notin> A"
 proof -
   from preal_exists_bound [OF A]
   obtain x where [simp]: "0<x" "x \<notin> A" by blast
@@ -605,7 +612,7 @@
 
 text{*Part 1 of Dedekind sections definition*}
 lemma inverse_set_not_empty:
-     "A \<in> preal ==> {} \<subset> inverse_set A"
+     "cut A ==> {} \<subset> inverse_set A"
 apply (insert mem_inv_set_ex [of A])
 apply (auto simp add: inverse_set_def)
 done
@@ -613,7 +620,7 @@
 text{*Part 2 of Dedekind sections definition*}
 
 lemma preal_not_mem_inverse_set_Ex:
-   assumes A: "A \<in> preal"  shows "\<exists>q. 0 < q & q \<notin> inverse_set A"
+   assumes A: "cut A"  shows "\<exists>q. 0 < q & q \<notin> inverse_set A"
 proof -
   from preal_nonempty [OF A]
   obtain x where x: "x \<in> A" and  xpos [simp]: "0<x" ..
@@ -635,7 +642,7 @@
 qed
 
 lemma inverse_set_not_rat_set:
-   assumes A: "A \<in> preal"  shows "inverse_set A < {r. 0 < r}"
+   assumes A: "cut A"  shows "inverse_set A < {r. 0 < r}"
 proof
   show "inverse_set A \<subseteq> {r. 0 < r}"  by (force simp add: inverse_set_def)
 next
@@ -645,7 +652,7 @@
 
 text{*Part 3 of Dedekind sections definition*}
 lemma inverse_set_lemma3:
-     "[|A \<in> preal; u \<in> inverse_set A; 0 < z; z < u|] 
+     "[|cut A; u \<in> inverse_set A; 0 < z; z < u|] 
       ==> z \<in> inverse_set A"
 apply (auto simp add: inverse_set_def)
 apply (auto intro: order_less_trans)
@@ -653,7 +660,7 @@
 
 text{*Part 4 of Dedekind sections definition*}
 lemma inverse_set_lemma4:
-     "[|A \<in> preal; y \<in> inverse_set A|] ==> \<exists>u \<in> inverse_set A. y < u"
+     "[|cut A; y \<in> inverse_set A|] ==> \<exists>u \<in> inverse_set A. y < u"
 apply (auto simp add: inverse_set_def)
 apply (drule dense [of y]) 
 apply (blast intro: order_less_trans)
@@ -661,8 +668,8 @@
 
 
 lemma mem_inverse_set:
-     "A \<in> preal ==> inverse_set A \<in> preal"
-apply (simp (no_asm_simp) add: preal_def cut_def)
+     "cut A ==> cut (inverse_set A)"
+apply (simp (no_asm_simp) add: cut_def)
 apply (blast intro!: inverse_set_not_empty inverse_set_not_rat_set
                      inverse_set_lemma3 inverse_set_lemma4)
 done
@@ -671,7 +678,7 @@
 subsection{*Gleason's Lemma 9-3.4, page 122*}
 
 lemma Gleason9_34_exists:
-  assumes A: "A \<in> preal"
+  assumes A: "cut A"
     and "\<forall>x\<in>A. x + u \<in> A"
     and "0 \<le> z"
   shows "\<exists>b\<in>A. b + (of_int z) * u \<in> A"
@@ -694,7 +701,7 @@
 qed
 
 lemma Gleason9_34_contra:
-  assumes A: "A \<in> preal"
+  assumes A: "cut A"
     shows "[|\<forall>x\<in>A. x + u \<in> A; 0 < u; 0 < y; y \<notin> A|] ==> False"
 proof (induct u, induct y)
   fix a::int and b::int
@@ -734,7 +741,7 @@
 
 
 lemma Gleason9_34:
-  assumes A: "A \<in> preal"
+  assumes A: "cut A"
     and upos: "0 < u"
   shows "\<exists>r \<in> A. r + u \<notin> A"
 proof (rule ccontr, simp)
@@ -750,7 +757,7 @@
 subsection{*Gleason's Lemma 9-3.6*}
 
 lemma lemma_gleason9_36:
-  assumes A: "A \<in> preal"
+  assumes A: "cut A"
     and x: "1 < x"
   shows "\<exists>r \<in> A. r*x \<notin> A"
 proof -
@@ -965,8 +972,8 @@
 done
 
 lemma mem_diff_set:
-     "R < S ==> diff_set (Rep_preal S) (Rep_preal R) \<in> preal"
-apply (unfold preal_def cut_def [abs_def])
+     "R < S ==> cut (diff_set (Rep_preal S) (Rep_preal R))"
+apply (unfold cut_def)
 apply (blast intro!: diff_set_not_empty diff_set_not_rat_set
                      diff_set_lemma3 diff_set_lemma4)
 done
@@ -1134,8 +1141,8 @@
 by (blast dest: Rep_preal [THEN preal_exists_greater])
 
 lemma preal_sup:
-     "[|P \<noteq> {}; \<forall>X \<in> P. X \<le> Y|] ==> (\<Union>X \<in> P. Rep_preal(X)) \<in> preal"
-apply (unfold preal_def cut_def [abs_def])
+     "[|P \<noteq> {}; \<forall>X \<in> P. X \<le> Y|] ==> cut (\<Union>X \<in> P. Rep_preal(X))"
+apply (unfold cut_def)
 apply (blast intro!: preal_sup_set_not_empty preal_sup_set_not_rat_set
                      preal_sup_set_lemma3 preal_sup_set_lemma4)
 done