# HG changeset patch
# User hoelzl
# Date 1466149456 -7200
# Node ID 247eac9758dd655a0d0652234d0fabc089443ff4
# Parent  8d591640c3bd029467a64b1bf311668165e80264
move Conditional_Complete_Lattices to Main

diff -r 8d591640c3bd -r 247eac9758dd src/HOL/Archimedean_Field.thy
--- a/src/HOL/Archimedean_Field.thy	Wed Jun 15 15:55:02 2016 +0200
+++ b/src/HOL/Archimedean_Field.thy	Fri Jun 17 09:44:16 2016 +0200
@@ -8,6 +8,63 @@
 imports Main
 begin
 
+lemma cInf_abs_ge:
+  fixes S :: "('a::{linordered_idom,conditionally_complete_linorder}) set"
+  assumes "S \<noteq> {}" and bdd: "\<And>x. x\<in>S \<Longrightarrow> \<bar>x\<bar> \<le> a"
+  shows "\<bar>Inf S\<bar> \<le> a"
+proof -
+  have "Sup (uminus ` S) = - (Inf S)"
+  proof (rule antisym)
+    show "- (Inf S) \<le> Sup(uminus ` S)"
+      apply (subst minus_le_iff)
+      apply (rule cInf_greatest [OF \<open>S \<noteq> {}\<close>])
+      apply (subst minus_le_iff)
+      apply (rule cSup_upper, force)
+      using bdd apply (force simp add: abs_le_iff bdd_above_def)
+      done
+  next
+    show "Sup (uminus ` S) \<le> - Inf S"
+      apply (rule cSup_least)
+       using \<open>S \<noteq> {}\<close> apply (force simp add: )
+      apply clarsimp
+      apply (rule cInf_lower)
+      apply assumption
+      using bdd apply (simp add: bdd_below_def)
+      apply (rule_tac x="-a" in exI)
+      apply force
+      done
+  qed
+  with cSup_abs_le [of "uminus ` S"] assms show ?thesis by fastforce
+qed
+
+lemma cSup_asclose:
+  fixes S :: "('a::{linordered_idom,conditionally_complete_linorder}) set"
+  assumes S: "S \<noteq> {}"
+    and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e"
+  shows "\<bar>Sup S - l\<bar> \<le> e"
+proof -
+  have th: "\<And>(x::'a) l e. \<bar>x - l\<bar> \<le> e \<longleftrightarrow> l - e \<le> x \<and> x \<le> l + e"
+    by arith
+  have "bdd_above S"
+    using b by (auto intro!: bdd_aboveI[of _ "l + e"])
+  with S b show ?thesis
+    unfolding th by (auto intro!: cSup_upper2 cSup_least)
+qed
+
+lemma cInf_asclose:
+  fixes S :: "('a::{linordered_idom,conditionally_complete_linorder}) set"
+  assumes S: "S \<noteq> {}"
+    and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e"
+  shows "\<bar>Inf S - l\<bar> \<le> e"
+proof -
+  have th: "\<And>(x::'a) l e. \<bar>x - l\<bar> \<le> e \<longleftrightarrow> l - e \<le> x \<and> x \<le> l + e"
+    by arith
+  have "bdd_below S"
+    using b by (auto intro!: bdd_belowI[of _ "l - e"])
+  with S b show ?thesis
+    unfolding th by (auto intro!: cInf_lower2 cInf_greatest)
+qed
+
 subsection \<open>Class of Archimedean fields\<close>
 
 text \<open>Archimedean fields have no infinite elements.\<close>
@@ -329,10 +386,10 @@
   also have "\<dots> = (of_int (k div l) + of_int (k mod l) / of_int l) * of_int l"
     using False by (simp only: of_int_add) (simp add: field_simps)
   finally have "(of_int k / of_int l :: 'a) = \<dots> / of_int l"
-    by simp 
+    by simp
   then have "(of_int k / of_int l :: 'a) = of_int (k div l) + of_int (k mod l) / of_int l"
     using False by (simp only:) (simp add: field_simps)
-  then have "\<lfloor>of_int k / of_int l :: 'a\<rfloor> = \<lfloor>of_int (k div l) + of_int (k mod l) / of_int l :: 'a\<rfloor>" 
+  then have "\<lfloor>of_int k / of_int l :: 'a\<rfloor> = \<lfloor>of_int (k div l) + of_int (k mod l) / of_int l :: 'a\<rfloor>"
     by simp
   then have "\<lfloor>of_int k / of_int l :: 'a\<rfloor> = \<lfloor>of_int (k mod l) / of_int l + of_int (k div l) :: 'a\<rfloor>"
     by (simp add: ac_simps)
@@ -355,10 +412,10 @@
   also have "\<dots> = (of_nat (m div n) + of_nat (m mod n) / of_nat n) * of_nat n"
     using False by (simp only: of_nat_add) (simp add: field_simps of_nat_mult)
   finally have "(of_nat m / of_nat n :: 'a) = \<dots> / of_nat n"
-    by simp 
+    by simp
   then have "(of_nat m / of_nat n :: 'a) = of_nat (m div n) + of_nat (m mod n) / of_nat n"
     using False by (simp only:) simp
-  then have "\<lfloor>of_nat m / of_nat n :: 'a\<rfloor> = \<lfloor>of_nat (m div n) + of_nat (m mod n) / of_nat n :: 'a\<rfloor>" 
+  then have "\<lfloor>of_nat m / of_nat n :: 'a\<rfloor> = \<lfloor>of_nat (m div n) + of_nat (m mod n) / of_nat n :: 'a\<rfloor>"
     by simp
   then have "\<lfloor>of_nat m / of_nat n :: 'a\<rfloor> = \<lfloor>of_nat (m mod n) / of_nat n + of_nat (m div n) :: 'a\<rfloor>"
     by (simp add: ac_simps)
@@ -376,7 +433,7 @@
   where "\<lceil>x\<rceil> = - \<lfloor>- x\<rfloor>"
 
 lemma ceiling_correct: "of_int \<lceil>x\<rceil> - 1 < x \<and> x \<le> of_int \<lceil>x\<rceil>"
-  unfolding ceiling_def using floor_correct [of "- x"] by (simp add: le_minus_iff) 
+  unfolding ceiling_def using floor_correct [of "- x"] by (simp add: le_minus_iff)
 
 lemma ceiling_unique: "\<lbrakk>of_int z - 1 < x; x \<le> of_int z\<rbrakk> \<Longrightarrow> \<lceil>x\<rceil> = z"
   unfolding ceiling_def using floor_unique [of "- z" "- x"] by simp
@@ -512,7 +569,7 @@
 
 lemma ceiling_diff_floor_le_1: "\<lceil>x\<rceil> - \<lfloor>x\<rfloor> \<le> 1"
 proof -
-  have "of_int \<lceil>x\<rceil> - 1 < x" 
+  have "of_int \<lceil>x\<rceil> - 1 < x"
     using ceiling_correct[of x] by simp
   also have "x < of_int \<lfloor>x\<rfloor> + 1"
     using floor_correct[of x] by simp_all
@@ -552,7 +609,7 @@
 lemma frac_of_int [simp]: "frac (of_int z) = 0"
   by (simp add: frac_def)
 
-lemma floor_add: "\<lfloor>x + y\<rfloor> = (if frac x + frac y < 1 then \<lfloor>x\<rfloor> + \<lfloor>y\<rfloor> else (\<lfloor>x\<rfloor> + \<lfloor>y\<rfloor>) + 1)"  
+lemma floor_add: "\<lfloor>x + y\<rfloor> = (if frac x + frac y < 1 then \<lfloor>x\<rfloor> + \<lfloor>y\<rfloor> else (\<lfloor>x\<rfloor> + \<lfloor>y\<rfloor>) + 1)"
 proof -
   {assume "x + y < 1 + (of_int \<lfloor>x\<rfloor> + of_int \<lfloor>y\<rfloor>)"
    then have "\<lfloor>x + y\<rfloor> = \<lfloor>x\<rfloor> + \<lfloor>y\<rfloor>"
@@ -563,14 +620,14 @@
     then have "\<lfloor>x + y\<rfloor> = 1 + (\<lfloor>x\<rfloor> + \<lfloor>y\<rfloor>)"
       apply (simp add: floor_unique_iff)
       apply (auto simp add: algebra_simps)
-      by linarith    
+      by linarith
   }
   ultimately show ?thesis
     by (auto simp add: frac_def algebra_simps)
 qed
 
 lemma frac_add: "frac (x + y) = (if frac x + frac y < 1 then frac x + frac y
-                                 else (frac x + frac y) - 1)"  
+                                 else (frac x + frac y) - 1)"
   by (simp add: frac_def floor_add)
 
 lemma frac_unique_iff:
@@ -582,7 +639,7 @@
 
 lemma frac_eq: "(frac x) = x \<longleftrightarrow> 0 \<le> x \<and> x < 1"
   by (simp add: frac_unique_iff)
-  
+
 lemma frac_neg:
   fixes x :: "'a::floor_ceiling"
   shows  "frac (-x) = (if x \<in> \<int> then 0 else 1 - frac x)"
@@ -643,8 +700,8 @@
   unfolding round_def by (intro floor_mono) simp
 
 lemma ceiling_ge_round: "\<lceil>x\<rceil> \<ge> round x" unfolding round_altdef by simp
-     
-lemma round_diff_minimal: 
+
+lemma round_diff_minimal:
   fixes z :: "'a :: floor_ceiling"
   shows "\<bar>z - of_int (round z)\<bar> \<le> \<bar>z - of_int m\<bar>"
 proof (cases "of_int m \<ge> z")
diff -r 8d591640c3bd -r 247eac9758dd src/HOL/Conditionally_Complete_Lattices.thy
--- a/src/HOL/Conditionally_Complete_Lattices.thy	Wed Jun 15 15:55:02 2016 +0200
+++ b/src/HOL/Conditionally_Complete_Lattices.thy	Fri Jun 17 09:44:16 2016 +0200
@@ -7,7 +7,7 @@
 section \<open>Conditionally-complete Lattices\<close>
 
 theory Conditionally_Complete_Lattices
-imports Main
+imports Finite_Set Lattices_Big Set_Interval
 begin
 
 lemma (in linorder) Sup_fin_eq_Max: "finite X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Sup_fin X = Max X"
@@ -107,7 +107,7 @@
 
 lemma bdd_below_image_mono: "mono f \<Longrightarrow> bdd_below A \<Longrightarrow> bdd_below (f`A)"
   by (auto simp: bdd_below_def mono_def)
-  
+
 lemma bdd_above_image_antimono: "antimono f \<Longrightarrow> bdd_below A \<Longrightarrow> bdd_above (f`A)"
   by (auto simp: bdd_above_def bdd_below_def antimono_def)
 
@@ -394,7 +394,7 @@
 class conditionally_complete_linorder = conditionally_complete_lattice + linorder
 begin
 
-lemma less_cSup_iff : (*REAL_SUP_LE in HOL4*)
+lemma less_cSup_iff:
   "X \<noteq> {} \<Longrightarrow> bdd_above X \<Longrightarrow> y < Sup X \<longleftrightarrow> (\<exists>x\<in>X. y < x)"
   by (rule iffI) (metis cSup_least not_less, metis cSup_upper less_le_trans)
 
@@ -429,7 +429,7 @@
        (metis \<open>a < b\<close> \<open>\<not> P b\<close> linear less_le)
 next
   show "Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c} \<le> b"
-    apply (rule cSup_least) 
+    apply (rule cSup_least)
     apply auto
     apply (metis less_le_not_le)
     apply (metis \<open>a<b\<close> \<open>~ P b\<close> linear less_le)
@@ -440,7 +440,7 @@
   show "P x"
     apply (rule less_cSupE [OF lt], auto)
     apply (metis less_le_not_le)
-    apply (metis x) 
+    apply (metis x)
     done
 next
   fix d
@@ -512,7 +512,7 @@
       unfolding Inf_nat_def ex_in_conv[symmetric] by (rule LeastI2_ex) }
   { assume "x \<in> X" "bdd_above X" then show "x \<le> Sup X"
       by (simp add: Sup_nat_def bdd_above_nat) }
-  { assume "X \<noteq> {}" "\<And>y. y \<in> X \<Longrightarrow> y \<le> x" 
+  { assume "X \<noteq> {}" "\<And>y. y \<in> X \<Longrightarrow> y \<le> x"
     moreover then have "bdd_above X"
       by (auto simp: bdd_above_def)
     ultimately show "Sup X \<le> x"
@@ -593,7 +593,7 @@
   define lower upper where "lower = {x. \<exists>s\<in>S. s \<le> x}" and "upper = {x. \<exists>s\<in>S. x \<le> s}"
   with ivl have "S = lower \<inter> upper"
     by auto
-  moreover 
+  moreover
   have "\<exists>a. upper = UNIV \<or> upper = {} \<or> upper = {.. a} \<or> upper = {..< a}"
   proof cases
     assume *: "bdd_above S \<and> S \<noteq> {}"
@@ -644,7 +644,7 @@
 using a bdd
 apply (auto simp: cINF_lower)
 apply (metis eq cSUP_upper)
-done 
+done
 
 lemma cSUP_UNION:
   fixes f :: "_ \<Rightarrow> 'b::conditionally_complete_lattice"
@@ -686,67 +686,10 @@
     by (rule order_antisym)
 qed
 
-lemma cSup_abs_le: 
+lemma cSup_abs_le:
   fixes S :: "('a::{linordered_idom,conditionally_complete_linorder}) set"
   shows "S \<noteq> {} \<Longrightarrow> (\<And>x. x\<in>S \<Longrightarrow> \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>Sup S\<bar> \<le> a"
   apply (auto simp add: abs_le_iff intro: cSup_least)
   by (metis bdd_aboveI cSup_upper neg_le_iff_le order_trans)
 
-lemma cInf_abs_ge:
-  fixes S :: "('a::{linordered_idom,conditionally_complete_linorder}) set"
-  assumes "S \<noteq> {}" and bdd: "\<And>x. x\<in>S \<Longrightarrow> \<bar>x\<bar> \<le> a"
-  shows "\<bar>Inf S\<bar> \<le> a"
-proof -
-  have "Sup (uminus ` S) = - (Inf S)"
-  proof (rule antisym)
-    show "- (Inf S) \<le> Sup(uminus ` S)"
-      apply (subst minus_le_iff)
-      apply (rule cInf_greatest [OF \<open>S \<noteq> {}\<close>])
-      apply (subst minus_le_iff)
-      apply (rule cSup_upper, force)
-      using bdd apply (force simp add: abs_le_iff bdd_above_def)
-      done
-  next
-    show "Sup (uminus ` S) \<le> - Inf S"
-      apply (rule cSup_least)
-       using \<open>S \<noteq> {}\<close> apply (force simp add: )
-      apply clarsimp  
-      apply (rule cInf_lower)
-      apply assumption
-      using bdd apply (simp add: bdd_below_def)
-      apply (rule_tac x="-a" in exI)
-      apply force
-      done
-  qed
-  with cSup_abs_le [of "uminus ` S"] assms show ?thesis by fastforce
-qed
-
-lemma cSup_asclose:
-  fixes S :: "('a::{linordered_idom,conditionally_complete_linorder}) set"
-  assumes S: "S \<noteq> {}"
-    and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e"
-  shows "\<bar>Sup S - l\<bar> \<le> e"
-proof -
-  have th: "\<And>(x::'a) l e. \<bar>x - l\<bar> \<le> e \<longleftrightarrow> l - e \<le> x \<and> x \<le> l + e"
-    by arith
-  have "bdd_above S"
-    using b by (auto intro!: bdd_aboveI[of _ "l + e"])
-  with S b show ?thesis
-    unfolding th by (auto intro!: cSup_upper2 cSup_least)
-qed
-
-lemma cInf_asclose:
-  fixes S :: "('a::{linordered_idom,conditionally_complete_linorder}) set"
-  assumes S: "S \<noteq> {}"
-    and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e"
-  shows "\<bar>Inf S - l\<bar> \<le> e"
-proof -
-  have th: "\<And>(x::'a) l e. \<bar>x - l\<bar> \<le> e \<longleftrightarrow> l - e \<le> x \<and> x \<le> l + e"
-    by arith
-  have "bdd_below S"
-    using b by (auto intro!: bdd_belowI[of _ "l - e"])
-  with S b show ?thesis
-    unfolding th by (auto intro!: cInf_lower2 cInf_greatest)
-qed
-
 end
diff -r 8d591640c3bd -r 247eac9758dd src/HOL/Library/FSet.thy
--- a/src/HOL/Library/FSet.thy	Wed Jun 15 15:55:02 2016 +0200
+++ b/src/HOL/Library/FSet.thy	Fri Jun 17 09:44:16 2016 +0200
@@ -7,7 +7,7 @@
 section \<open>Type of finite sets defined as a subtype of sets\<close>
 
 theory FSet
-imports Conditionally_Complete_Lattices
+imports Main
 begin
 
 subsection \<open>Definition of the type\<close>
@@ -31,18 +31,18 @@
 
 interpretation lifting_syntax .
 
-lift_definition bot_fset :: "'a fset" is "{}" parametric empty_transfer by simp 
+lift_definition bot_fset :: "'a fset" is "{}" parametric empty_transfer by simp
 
-lift_definition less_eq_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" is subset_eq parametric subset_transfer 
+lift_definition less_eq_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" is subset_eq parametric subset_transfer
   .
 
 definition less_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" where "xs < ys \<equiv> xs \<le> ys \<and> xs \<noteq> (ys::'a fset)"
 
 lemma less_fset_transfer[transfer_rule]:
-  assumes [transfer_rule]: "bi_unique A" 
+  assumes [transfer_rule]: "bi_unique A"
   shows "((pcr_fset A) ===> (pcr_fset A) ===> op =) op \<subset> op <"
   unfolding less_fset_def[abs_def] psubset_eq[abs_def] by transfer_prover
-  
+
 
 lift_definition sup_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" is union parametric union_transfer
   by simp
@@ -69,7 +69,7 @@
 begin
 definition "HOL.equal A B \<longleftrightarrow> A |\<subseteq>| B \<and> B |\<subseteq>| A"
 instance by intro_classes (auto simp add: equal_fset_def)
-end 
+end
 
 instantiation fset :: (type) conditionally_complete_lattice
 begin
@@ -78,18 +78,18 @@
 
 lemma right_total_Inf_fset_transfer:
   assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "right_total A"
-  shows "(rel_set (rel_set A) ===> rel_set A) 
-    (\<lambda>S. if finite (\<Inter>S \<inter> Collect (Domainp A)) then \<Inter>S \<inter> Collect (Domainp A) else {}) 
+  shows "(rel_set (rel_set A) ===> rel_set A)
+    (\<lambda>S. if finite (\<Inter>S \<inter> Collect (Domainp A)) then \<Inter>S \<inter> Collect (Domainp A) else {})
       (\<lambda>S. if finite (Inf S) then Inf S else {})"
     by transfer_prover
 
 lemma Inf_fset_transfer:
   assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "bi_total A"
-  shows "(rel_set (rel_set A) ===> rel_set A) (\<lambda>A. if finite (Inf A) then Inf A else {}) 
+  shows "(rel_set (rel_set A) ===> rel_set A) (\<lambda>A. if finite (Inf A) then Inf A else {})
     (\<lambda>A. if finite (Inf A) then Inf A else {})"
   by transfer_prover
 
-lift_definition Inf_fset :: "'a fset set \<Rightarrow> 'a fset" is "\<lambda>A. if finite (Inf A) then Inf A else {}" 
+lift_definition Inf_fset :: "'a fset set \<Rightarrow> 'a fset" is "\<lambda>A. if finite (Inf A) then Inf A else {}"
 parametric right_total_Inf_fset_transfer Inf_fset_transfer by simp
 
 lemma Sup_fset_transfer:
@@ -107,11 +107,11 @@
   by auto
 
 instance
-proof 
+proof
   fix x z :: "'a fset"
   fix X :: "'a fset set"
   {
-    assume "x \<in> X" "bdd_below X" 
+    assume "x \<in> X" "bdd_below X"
     then show "Inf X |\<subseteq>| x" by transfer auto
   next
     assume "X \<noteq> {}" "(\<And>x. x \<in> X \<Longrightarrow> z |\<subseteq>| x)"
@@ -129,7 +129,7 @@
 qed
 end
 
-instantiation fset :: (finite) complete_lattice 
+instantiation fset :: (finite) complete_lattice
 begin
 
 lift_definition top_fset :: "'a fset" is UNIV parametric right_total_UNIV_transfer UNIV_transfer
@@ -143,7 +143,7 @@
 instantiation fset :: (finite) complete_boolean_algebra
 begin
 
-lift_definition uminus_fset :: "'a fset \<Rightarrow> 'a fset" is uminus 
+lift_definition uminus_fset :: "'a fset \<Rightarrow> 'a fset" is uminus
   parametric right_total_Compl_transfer Compl_transfer by simp
 
 instance
@@ -169,7 +169,7 @@
   "{|x, xs|}" == "CONST finsert x {|xs|}"
   "{|x|}"     == "CONST finsert x {||}"
 
-lift_definition fmember :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<in>|" 50) is Set.member 
+lift_definition fmember :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<in>|" 50) is Set.member
   parametric member_transfer .
 
 abbreviation notin_fset :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<notin>|" 50) where "x |\<notin>| S \<equiv> \<not> (x |\<in>| S)"
@@ -179,20 +179,20 @@
 
 interpretation lifting_syntax .
 
-lift_definition ffilter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset" is Set.filter 
+lift_definition ffilter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset" is Set.filter
   parametric Lifting_Set.filter_transfer unfolding Set.filter_def by simp
 
-lift_definition fPow :: "'a fset \<Rightarrow> 'a fset fset" is Pow parametric Pow_transfer 
+lift_definition fPow :: "'a fset \<Rightarrow> 'a fset fset" is Pow parametric Pow_transfer
 by (simp add: finite_subset)
 
 lift_definition fcard :: "'a fset \<Rightarrow> nat" is card parametric card_transfer .
 
-lift_definition fimage :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" (infixr "|`|" 90) is image 
+lift_definition fimage :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" (infixr "|`|" 90) is image
   parametric image_transfer by simp
 
 lift_definition fthe_elem :: "'a fset \<Rightarrow> 'a" is the_elem .
 
-lift_definition fbind :: "'a fset \<Rightarrow> ('a \<Rightarrow> 'b fset) \<Rightarrow> 'b fset" is Set.bind parametric bind_transfer 
+lift_definition fbind :: "'a fset \<Rightarrow> ('a \<Rightarrow> 'b fset) \<Rightarrow> 'b fset" is Set.bind parametric bind_transfer
 by (simp add: Set.bind_def)
 
 lift_definition ffUnion :: "'a fset fset \<Rightarrow> 'a fset" is Union parametric Union_transfer by simp
@@ -464,7 +464,7 @@
 
 lemmas fset_simps[simp] = bot_fset.rep_eq finsert.rep_eq
 
-lemma finite_fset [simp]: 
+lemma finite_fset [simp]:
   shows "finite (fset S)"
   by transfer simp
 
@@ -485,16 +485,16 @@
 
 subsubsection \<open>\<open>filter_fset\<close>\<close>
 
-lemma subset_ffilter: 
+lemma subset_ffilter:
   "ffilter P A |\<subseteq>| ffilter Q A = (\<forall> x. x |\<in>| A \<longrightarrow> P x \<longrightarrow> Q x)"
   by transfer auto
 
-lemma eq_ffilter: 
+lemma eq_ffilter:
   "(ffilter P A = ffilter Q A) = (\<forall>x. x |\<in>| A \<longrightarrow> P x = Q x)"
   by transfer auto
 
 lemma pfsubset_ffilter:
-  "(\<And>x. x |\<in>| A \<Longrightarrow> P x \<Longrightarrow> Q x) \<Longrightarrow> (x |\<in>| A & \<not> P x & Q x) \<Longrightarrow> 
+  "(\<And>x. x |\<in>| A \<Longrightarrow> P x \<Longrightarrow> Q x) \<Longrightarrow> (x |\<in>| A & \<not> P x & Q x) \<Longrightarrow>
     ffilter P A |\<subset>| ffilter Q A"
   unfolding less_fset_def by (auto simp add: subset_ffilter eq_ffilter)
 
@@ -520,9 +520,9 @@
 subsubsection \<open>bounded quantification\<close>
 
 lemma bex_simps [simp, no_atp]:
-  "\<And>A P Q. fBex A (\<lambda>x. P x \<and> Q) = (fBex A P \<and> Q)" 
+  "\<And>A P Q. fBex A (\<lambda>x. P x \<and> Q) = (fBex A P \<and> Q)"
   "\<And>A P Q. fBex A (\<lambda>x. P \<and> Q x) = (P \<and> fBex A Q)"
-  "\<And>P. fBex {||} P = False" 
+  "\<And>P. fBex {||} P = False"
   "\<And>a B P. fBex (finsert a B) P = (P a \<or> fBex B P)"
   "\<And>A P f. fBex (f |`| A) P = fBex A (\<lambda>x. P (f x))"
   "\<And>A P. (\<not> fBex A P) = fBall A (\<lambda>x. \<not> P x)"
@@ -601,7 +601,7 @@
 lemma pfsubset_fcard_mono: "A |\<subset>| B \<Longrightarrow> fcard A < fcard B"
 by transfer (rule psubset_card_mono)
 
-lemma fcard_funion_finter: 
+lemma fcard_funion_finter:
   "fcard A + fcard B = fcard (A |\<union>| B) + fcard (A |\<inter>| B)"
 by transfer (rule card_Un_Int)
 
@@ -656,7 +656,7 @@
     assumes "x |\<in>| A"
     shows "ffold f z A = f x (ffold f z (A |-| {|x|}))"
     using assms by (transfer fixing: f) (rule fold_rec)
-  
+
   lemma ffold_finsert_fremove:
     "ffold f z (finsert x A) = f x (ffold f z (A |-| {|x|}))"
      by (transfer fixing: f) (rule fold_insert_remove)
@@ -680,9 +680,9 @@
   lemma ffold_finsert_idem:
     "ffold f z (finsert x A) = f x (ffold f z A)"
     by (transfer fixing: f) (rule fold_insert_idem)
-  
+
   declare ffold_finsert [simp del] ffold_finsert_idem [simp]
-  
+
   lemma ffold_finsert_idem2:
     "ffold f z (finsert x A) = ffold f (f x z) A"
     by (transfer fixing: f) (rule fold_insert_idem2)
@@ -692,7 +692,7 @@
 
 subsection \<open>Choice in fsets\<close>
 
-lemma fset_choice: 
+lemma fset_choice:
   assumes "\<forall>x. x |\<in>| A \<longrightarrow> (\<exists>y. P x y)"
   shows "\<exists>f. \<forall>x. x |\<in>| A \<longrightarrow> P x (f x)"
   using assms by transfer metis
@@ -701,7 +701,7 @@
 subsection \<open>Induction and Cases rules for fsets\<close>
 
 lemma fset_exhaust [case_names empty insert, cases type: fset]:
-  assumes fempty_case: "S = {||} \<Longrightarrow> P" 
+  assumes fempty_case: "S = {||} \<Longrightarrow> P"
   and     finsert_case: "\<And>x S'. S = finsert x S' \<Longrightarrow> P"
   shows "P"
   using assms by transfer blast
@@ -739,9 +739,9 @@
   case (insert x S)
   have h: "P S" by fact
   have "x |\<notin>| S" by fact
-  then have "Suc (fcard S) = fcard (finsert x S)" 
+  then have "Suc (fcard S) = fcard (finsert x S)"
     by transfer auto
-  then show "P (finsert x S)" 
+  then show "P (finsert x S)"
     using h card_fset_Suc_case by simp
 qed
 
@@ -771,11 +771,11 @@
 lift_definition rel_fset :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'b fset \<Rightarrow> bool" is rel_set
 parametric rel_set_transfer .
 
-lemma rel_fset_alt_def: "rel_fset R = (\<lambda>A B. (\<forall>x.\<exists>y. x|\<in>|A \<longrightarrow> y|\<in>|B \<and> R x y) 
+lemma rel_fset_alt_def: "rel_fset R = (\<lambda>A B. (\<forall>x.\<exists>y. x|\<in>|A \<longrightarrow> y|\<in>|B \<and> R x y)
   \<and> (\<forall>y. \<exists>x. y|\<in>|B \<longrightarrow> x|\<in>|A \<and> R x y))"
 apply (rule ext)+
 apply transfer'
-apply (subst rel_set_def[unfolded fun_eq_iff]) 
+apply (subst rel_set_def[unfolded fun_eq_iff])
 by blast
 
 lemma finite_rel_set:
@@ -787,12 +787,12 @@
   apply atomize_elim
   apply (subst bchoice_iff[symmetric])
   using R_S[unfolded rel_set_def OO_def] by blast
-  
+
   obtain g where g: "\<forall>z\<in>Z. S (g z) z \<and> (\<exists>x\<in>X. R x (g z))"
   apply atomize_elim
   apply (subst bchoice_iff[symmetric])
   using R_S[unfolded rel_set_def OO_def] by blast
-  
+
   let ?Y = "f ` X \<union> g ` Z"
   have "finite ?Y" by (simp add: fin)
   moreover have "rel_set R X ?Y"
@@ -960,7 +960,7 @@
 
 bnf "'a fset"
   map: fimage
-  sets: fset 
+  sets: fset
   bd: natLeq
   wits: "{||}"
   rel: rel_fset
@@ -974,7 +974,7 @@
     apply transfer apply (metis ordLess_imp_ordLeq finite_iff_ordLess_natLeq)
    apply (fastforce simp: rel_fset_alt)
  apply (simp add: Grp_def relcompp.simps conversep.simps fun_eq_iff rel_fset_alt
-   rel_fset_aux[unfolded OO_Grp_alt]) 
+   rel_fset_aux[unfolded OO_Grp_alt])
 apply transfer apply simp
 done
 
@@ -1009,7 +1009,7 @@
 lemma fset_size_o_map: "inj f \<Longrightarrow> size_fset g \<circ> fimage f = size_fset (g \<circ> f)"
   apply (subst fun_eq_iff)
   including fset.lifting by transfer (auto intro: setsum.reindex_cong subset_inj_on)
-  
+
 setup \<open>
 BNF_LFP_Size.register_size_global @{type_name fset} @{const_name size_fset}
   @{thm size_fset_overloaded_def} @{thms size_fset_simps size_fset_overloaded_simps}
@@ -1023,8 +1023,8 @@
 
 (* Set vs. sum relators: *)
 
-lemma rel_set_rel_sum[simp]: 
-"rel_set (rel_sum \<chi> \<phi>) A1 A2 \<longleftrightarrow> 
+lemma rel_set_rel_sum[simp]:
+"rel_set (rel_sum \<chi> \<phi>) A1 A2 \<longleftrightarrow>
  rel_set \<chi> (Inl -` A1) (Inl -` A2) \<and> rel_set \<phi> (Inr -` A1) (Inr -` A2)"
 (is "?L \<longleftrightarrow> ?Rl \<and> ?Rr")
 proof safe
diff -r 8d591640c3bd -r 247eac9758dd src/HOL/Main.thy
--- a/src/HOL/Main.thy	Wed Jun 15 15:55:02 2016 +0200
+++ b/src/HOL/Main.thy	Fri Jun 17 09:44:16 2016 +0200
@@ -1,7 +1,7 @@
 section \<open>Main HOL\<close>
 
 theory Main
-imports Predicate_Compile Quickcheck_Narrowing Extraction Coinduction Nitpick BNF_Greatest_Fixpoint Filter
+imports Predicate_Compile Quickcheck_Narrowing Extraction Coinduction Nitpick BNF_Greatest_Fixpoint Filter Conditionally_Complete_Lattices
 begin
 
 text \<open>
diff -r 8d591640c3bd -r 247eac9758dd src/HOL/Real.thy
--- a/src/HOL/Real.thy	Wed Jun 15 15:55:02 2016 +0200
+++ b/src/HOL/Real.thy	Fri Jun 17 09:44:16 2016 +0200
@@ -10,7 +10,7 @@
 section \<open>Development of the Reals using Cauchy Sequences\<close>
 
 theory Real
-imports Rat Conditionally_Complete_Lattices
+imports Rat
 begin
 
 text \<open>
@@ -961,7 +961,6 @@
 qed
 end
 
-
 subsection \<open>Hiding implementation details\<close>
 
 hide_const (open) vanishes cauchy positive Real