# 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 \ {}" and bdd: "\x. x\S \ \x\ \ a" + shows "\Inf S\ \ a" +proof - + have "Sup (uminus ` S) = - (Inf S)" + proof (rule antisym) + show "- (Inf S) \ Sup(uminus ` S)" + apply (subst minus_le_iff) + apply (rule cInf_greatest [OF \S \ {}\]) + 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) \ - Inf S" + apply (rule cSup_least) + using \S \ {}\ 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 \ {}" + and b: "\x\S. \x - l\ \ e" + shows "\Sup S - l\ \ e" +proof - + have th: "\(x::'a) l e. \x - l\ \ e \ l - e \ x \ x \ 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 \ {}" + and b: "\x\S. \x - l\ \ e" + shows "\Inf S - l\ \ e" +proof - + have th: "\(x::'a) l e. \x - l\ \ e \ l - e \ x \ x \ 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 \Class of Archimedean fields\ text \Archimedean fields have no infinite elements.\ @@ -329,10 +386,10 @@ also have "\ = (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) = \ / 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 "\of_int k / of_int l :: 'a\ = \of_int (k div l) + of_int (k mod l) / of_int l :: 'a\" + then have "\of_int k / of_int l :: 'a\ = \of_int (k div l) + of_int (k mod l) / of_int l :: 'a\" by simp then have "\of_int k / of_int l :: 'a\ = \of_int (k mod l) / of_int l + of_int (k div l) :: 'a\" by (simp add: ac_simps) @@ -355,10 +412,10 @@ also have "\ = (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) = \ / 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 "\of_nat m / of_nat n :: 'a\ = \of_nat (m div n) + of_nat (m mod n) / of_nat n :: 'a\" + then have "\of_nat m / of_nat n :: 'a\ = \of_nat (m div n) + of_nat (m mod n) / of_nat n :: 'a\" by simp then have "\of_nat m / of_nat n :: 'a\ = \of_nat (m mod n) / of_nat n + of_nat (m div n) :: 'a\" by (simp add: ac_simps) @@ -376,7 +433,7 @@ where "\x\ = - \- x\" lemma ceiling_correct: "of_int \x\ - 1 < x \ x \ of_int \x\" - 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: "\of_int z - 1 < x; x \ of_int z\ \ \x\ = z" unfolding ceiling_def using floor_unique [of "- z" "- x"] by simp @@ -512,7 +569,7 @@ lemma ceiling_diff_floor_le_1: "\x\ - \x\ \ 1" proof - - have "of_int \x\ - 1 < x" + have "of_int \x\ - 1 < x" using ceiling_correct[of x] by simp also have "x < of_int \x\ + 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: "\x + y\ = (if frac x + frac y < 1 then \x\ + \y\ else (\x\ + \y\) + 1)" +lemma floor_add: "\x + y\ = (if frac x + frac y < 1 then \x\ + \y\ else (\x\ + \y\) + 1)" proof - {assume "x + y < 1 + (of_int \x\ + of_int \y\)" then have "\x + y\ = \x\ + \y\" @@ -563,14 +620,14 @@ then have "\x + y\ = 1 + (\x\ + \y\)" 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 \ 0 \ x \ x < 1" by (simp add: frac_unique_iff) - + lemma frac_neg: fixes x :: "'a::floor_ceiling" shows "frac (-x) = (if x \ \ then 0 else 1 - frac x)" @@ -643,8 +700,8 @@ unfolding round_def by (intro floor_mono) simp lemma ceiling_ge_round: "\x\ \ round x" unfolding round_altdef by simp - -lemma round_diff_minimal: + +lemma round_diff_minimal: fixes z :: "'a :: floor_ceiling" shows "\z - of_int (round z)\ \ \z - of_int m\" proof (cases "of_int m \ 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 \Conditionally-complete Lattices\ theory Conditionally_Complete_Lattices -imports Main +imports Finite_Set Lattices_Big Set_Interval begin lemma (in linorder) Sup_fin_eq_Max: "finite X \ X \ {} \ Sup_fin X = Max X" @@ -107,7 +107,7 @@ lemma bdd_below_image_mono: "mono f \ bdd_below A \ bdd_below (f`A)" by (auto simp: bdd_below_def mono_def) - + lemma bdd_above_image_antimono: "antimono f \ bdd_below A \ 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 \ {} \ bdd_above X \ y < Sup X \ (\x\X. y < x)" by (rule iffI) (metis cSup_least not_less, metis cSup_upper less_le_trans) @@ -429,7 +429,7 @@ (metis \a < b\ \\ P b\ linear less_le) next show "Sup {d. \c. a \ c \ c < d \ P c} \ b" - apply (rule cSup_least) + apply (rule cSup_least) apply auto apply (metis less_le_not_le) apply (metis \a \~ P b\ 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 \ X" "bdd_above X" then show "x \ Sup X" by (simp add: Sup_nat_def bdd_above_nat) } - { assume "X \ {}" "\y. y \ X \ y \ x" + { assume "X \ {}" "\y. y \ X \ y \ x" moreover then have "bdd_above X" by (auto simp: bdd_above_def) ultimately show "Sup X \ x" @@ -593,7 +593,7 @@ define lower upper where "lower = {x. \s\S. s \ x}" and "upper = {x. \s\S. x \ s}" with ivl have "S = lower \ upper" by auto - moreover + moreover have "\a. upper = UNIV \ upper = {} \ upper = {.. a} \ upper = {..< a}" proof cases assume *: "bdd_above S \ S \ {}" @@ -644,7 +644,7 @@ using a bdd apply (auto simp: cINF_lower) apply (metis eq cSUP_upper) -done +done lemma cSUP_UNION: fixes f :: "_ \ '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 \ {} \ (\x. x\S \ \x\ \ a) \ \Sup S\ \ 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 \ {}" and bdd: "\x. x\S \ \x\ \ a" - shows "\Inf S\ \ a" -proof - - have "Sup (uminus ` S) = - (Inf S)" - proof (rule antisym) - show "- (Inf S) \ Sup(uminus ` S)" - apply (subst minus_le_iff) - apply (rule cInf_greatest [OF \S \ {}\]) - 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) \ - Inf S" - apply (rule cSup_least) - using \S \ {}\ 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 \ {}" - and b: "\x\S. \x - l\ \ e" - shows "\Sup S - l\ \ e" -proof - - have th: "\(x::'a) l e. \x - l\ \ e \ l - e \ x \ x \ 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 \ {}" - and b: "\x\S. \x - l\ \ e" - shows "\Inf S - l\ \ e" -proof - - have th: "\(x::'a) l e. \x - l\ \ e \ l - e \ x \ x \ 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 \Type of finite sets defined as a subtype of sets\ theory FSet -imports Conditionally_Complete_Lattices +imports Main begin subsection \Definition of the type\ @@ -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 \ 'a fset \ bool" is subset_eq parametric subset_transfer +lift_definition less_eq_fset :: "'a fset \ 'a fset \ bool" is subset_eq parametric subset_transfer . definition less_fset :: "'a fset \ 'a fset \ bool" where "xs < ys \ xs \ ys \ xs \ (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 \ op <" unfolding less_fset_def[abs_def] psubset_eq[abs_def] by transfer_prover - + lift_definition sup_fset :: "'a fset \ 'a fset \ 'a fset" is union parametric union_transfer by simp @@ -69,7 +69,7 @@ begin definition "HOL.equal A B \ A |\| B \ B |\| 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) - (\S. if finite (\S \ Collect (Domainp A)) then \S \ Collect (Domainp A) else {}) + shows "(rel_set (rel_set A) ===> rel_set A) + (\S. if finite (\S \ Collect (Domainp A)) then \S \ Collect (Domainp A) else {}) (\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) (\A. if finite (Inf A) then Inf A else {}) + shows "(rel_set (rel_set A) ===> rel_set A) (\A. if finite (Inf A) then Inf A else {}) (\A. if finite (Inf A) then Inf A else {})" by transfer_prover -lift_definition Inf_fset :: "'a fset set \ 'a fset" is "\A. if finite (Inf A) then Inf A else {}" +lift_definition Inf_fset :: "'a fset set \ 'a fset" is "\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 \ X" "bdd_below X" + assume "x \ X" "bdd_below X" then show "Inf X |\| x" by transfer auto next assume "X \ {}" "(\x. x \ X \ z |\| 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 \ 'a fset" is uminus +lift_definition uminus_fset :: "'a fset \ '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 \ 'a fset \ bool" (infix "|\|" 50) is Set.member +lift_definition fmember :: "'a \ 'a fset \ bool" (infix "|\|" 50) is Set.member parametric member_transfer . abbreviation notin_fset :: "'a \ 'a fset \ bool" (infix "|\|" 50) where "x |\| S \ \ (x |\| S)" @@ -179,20 +179,20 @@ interpretation lifting_syntax . -lift_definition ffilter :: "('a \ bool) \ 'a fset \ 'a fset" is Set.filter +lift_definition ffilter :: "('a \ bool) \ 'a fset \ 'a fset" is Set.filter parametric Lifting_Set.filter_transfer unfolding Set.filter_def by simp -lift_definition fPow :: "'a fset \ 'a fset fset" is Pow parametric Pow_transfer +lift_definition fPow :: "'a fset \ 'a fset fset" is Pow parametric Pow_transfer by (simp add: finite_subset) lift_definition fcard :: "'a fset \ nat" is card parametric card_transfer . -lift_definition fimage :: "('a \ 'b) \ 'a fset \ 'b fset" (infixr "|`|" 90) is image +lift_definition fimage :: "('a \ 'b) \ 'a fset \ 'b fset" (infixr "|`|" 90) is image parametric image_transfer by simp lift_definition fthe_elem :: "'a fset \ 'a" is the_elem . -lift_definition fbind :: "'a fset \ ('a \ 'b fset) \ 'b fset" is Set.bind parametric bind_transfer +lift_definition fbind :: "'a fset \ ('a \ 'b fset) \ 'b fset" is Set.bind parametric bind_transfer by (simp add: Set.bind_def) lift_definition ffUnion :: "'a fset fset \ '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 \\filter_fset\\ -lemma subset_ffilter: +lemma subset_ffilter: "ffilter P A |\| ffilter Q A = (\ x. x |\| A \ P x \ Q x)" by transfer auto -lemma eq_ffilter: +lemma eq_ffilter: "(ffilter P A = ffilter Q A) = (\x. x |\| A \ P x = Q x)" by transfer auto lemma pfsubset_ffilter: - "(\x. x |\| A \ P x \ Q x) \ (x |\| A & \ P x & Q x) \ + "(\x. x |\| A \ P x \ Q x) \ (x |\| A & \ P x & Q x) \ ffilter P A |\| ffilter Q A" unfolding less_fset_def by (auto simp add: subset_ffilter eq_ffilter) @@ -520,9 +520,9 @@ subsubsection \bounded quantification\ lemma bex_simps [simp, no_atp]: - "\A P Q. fBex A (\x. P x \ Q) = (fBex A P \ Q)" + "\A P Q. fBex A (\x. P x \ Q) = (fBex A P \ Q)" "\A P Q. fBex A (\x. P \ Q x) = (P \ fBex A Q)" - "\P. fBex {||} P = False" + "\P. fBex {||} P = False" "\a B P. fBex (finsert a B) P = (P a \ fBex B P)" "\A P f. fBex (f |`| A) P = fBex A (\x. P (f x))" "\A P. (\ fBex A P) = fBall A (\x. \ P x)" @@ -601,7 +601,7 @@ lemma pfsubset_fcard_mono: "A |\| B \ fcard A < fcard B" by transfer (rule psubset_card_mono) -lemma fcard_funion_finter: +lemma fcard_funion_finter: "fcard A + fcard B = fcard (A |\| B) + fcard (A |\| B)" by transfer (rule card_Un_Int) @@ -656,7 +656,7 @@ assumes "x |\| 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 \Choice in fsets\ -lemma fset_choice: +lemma fset_choice: assumes "\x. x |\| A \ (\y. P x y)" shows "\f. \x. x |\| A \ P x (f x)" using assms by transfer metis @@ -701,7 +701,7 @@ subsection \Induction and Cases rules for fsets\ lemma fset_exhaust [case_names empty insert, cases type: fset]: - assumes fempty_case: "S = {||} \ P" + assumes fempty_case: "S = {||} \ P" and finsert_case: "\x S'. S = finsert x S' \ P" shows "P" using assms by transfer blast @@ -739,9 +739,9 @@ case (insert x S) have h: "P S" by fact have "x |\| 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 \ 'b \ bool) \ 'a fset \ 'b fset \ bool" is rel_set parametric rel_set_transfer . -lemma rel_fset_alt_def: "rel_fset R = (\A B. (\x.\y. x|\|A \ y|\|B \ R x y) +lemma rel_fset_alt_def: "rel_fset R = (\A B. (\x.\y. x|\|A \ y|\|B \ R x y) \ (\y. \x. y|\|B \ x|\|A \ 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: "\z\Z. S (g z) z \ (\x\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 \ 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 \ size_fset g \ fimage f = size_fset (g \ f)" apply (subst fun_eq_iff) including fset.lifting by transfer (auto intro: setsum.reindex_cong subset_inj_on) - + setup \ 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 \ \) A1 A2 \ +lemma rel_set_rel_sum[simp]: +"rel_set (rel_sum \ \) A1 A2 \ rel_set \ (Inl -` A1) (Inl -` A2) \ rel_set \ (Inr -` A1) (Inr -` A2)" (is "?L \ ?Rl \ ?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 \Main HOL\ 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 \ 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 \Development of the Reals using Cauchy Sequences\ theory Real -imports Rat Conditionally_Complete_Lattices +imports Rat begin text \ @@ -961,7 +961,6 @@ qed end - subsection \Hiding implementation details\ hide_const (open) vanishes cauchy positive Real