72 by (force intro: Least_equality X z simp add: Sup_real_def) |
72 by (force intro: Least_equality X z simp add: Sup_real_def) |
73 |
73 |
74 lemma Sup_upper2: (*REAL_IMP_LE_SUP in HOL4*) |
74 lemma Sup_upper2: (*REAL_IMP_LE_SUP in HOL4*) |
75 fixes x :: real |
75 fixes x :: real |
76 shows "x \<in> X \<Longrightarrow> y \<le> x \<Longrightarrow> (!!x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> y \<le> Sup X" |
76 shows "x \<in> X \<Longrightarrow> y \<le> x \<Longrightarrow> (!!x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> y \<le> Sup X" |
77 by (metis Sup_upper real_le_trans) |
77 by (metis Sup_upper order_trans) |
78 |
78 |
79 lemma Sup_real_iff : (*REAL_SUP_LE in HOL4*) |
79 lemma Sup_real_iff : (*REAL_SUP_LE in HOL4*) |
80 fixes z :: real |
80 fixes z :: real |
81 shows "X ~= {} ==> (!!x. x \<in> X ==> x \<le> z) ==> (\<exists>x\<in>X. y<x) <-> y < Sup X" |
81 shows "X ~= {} ==> (!!x. x \<in> X ==> x \<le> z) ==> (\<exists>x\<in>X. y<x) <-> y < Sup X" |
82 by (metis Sup_least Sup_upper linorder_not_le le_less_trans) |
82 by (metis Sup_least Sup_upper linorder_not_le le_less_trans) |
84 lemma Sup_eq: |
84 lemma Sup_eq: |
85 fixes a :: real |
85 fixes a :: real |
86 shows "(!!x. x \<in> X \<Longrightarrow> x \<le> a) |
86 shows "(!!x. x \<in> X \<Longrightarrow> x \<le> a) |
87 \<Longrightarrow> (!!y. (!!x. x \<in> X \<Longrightarrow> x \<le> y) \<Longrightarrow> a \<le> y) \<Longrightarrow> Sup X = a" |
87 \<Longrightarrow> (!!y. (!!x. x \<in> X \<Longrightarrow> x \<le> y) \<Longrightarrow> a \<le> y) \<Longrightarrow> Sup X = a" |
88 by (metis Sup_least Sup_upper add_le_cancel_left diff_add_cancel insert_absorb |
88 by (metis Sup_least Sup_upper add_le_cancel_left diff_add_cancel insert_absorb |
89 insert_not_empty real_le_antisym) |
89 insert_not_empty order_antisym) |
90 |
90 |
91 lemma Sup_le: |
91 lemma Sup_le: |
92 fixes S :: "real set" |
92 fixes S :: "real set" |
93 shows "S \<noteq> {} \<Longrightarrow> S *<= b \<Longrightarrow> Sup S \<le> b" |
93 shows "S \<noteq> {} \<Longrightarrow> S *<= b \<Longrightarrow> Sup S \<le> b" |
94 by (metis SupInf.Sup_least setle_def) |
94 by (metis SupInf.Sup_least setle_def) |
107 case True |
107 case True |
108 thus ?thesis |
108 thus ?thesis |
109 apply (simp add: max_def) |
109 apply (simp add: max_def) |
110 apply (rule Sup_eq_maximum) |
110 apply (rule Sup_eq_maximum) |
111 apply (rule insertI1) |
111 apply (rule insertI1) |
112 apply (metis Sup_upper [OF _ z] insertE real_le_linear real_le_trans) |
112 apply (metis Sup_upper [OF _ z] insertE linear order_trans) |
113 done |
113 done |
114 next |
114 next |
115 case False |
115 case False |
116 hence 1:"a < Sup X" by simp |
116 hence 1:"a < Sup X" by simp |
117 have "Sup X \<le> Sup (insert a X)" |
117 have "Sup X \<le> Sup (insert a X)" |
118 apply (rule Sup_least) |
118 apply (rule Sup_least) |
119 apply (metis empty_psubset_nonempty psubset_eq x) |
119 apply (metis ex_in_conv x) |
120 apply (rule Sup_upper_EX) |
120 apply (rule Sup_upper_EX) |
121 apply blast |
121 apply blast |
122 apply (metis insert_iff real_le_linear real_le_refl real_le_trans z) |
122 apply (metis insert_iff linear order_refl order_trans z) |
123 done |
123 done |
124 moreover |
124 moreover |
125 have "Sup (insert a X) \<le> Sup X" |
125 have "Sup (insert a X) \<le> Sup X" |
126 apply (rule Sup_least) |
126 apply (rule Sup_least) |
127 apply blast |
127 apply blast |
128 apply (metis False Sup_upper insertE real_le_linear z) |
128 apply (metis False Sup_upper insertE linear z) |
129 done |
129 done |
130 ultimately have "Sup (insert a X) = Sup X" |
130 ultimately have "Sup (insert a X) = Sup X" |
131 by (blast intro: antisym ) |
131 by (blast intro: antisym ) |
132 thus ?thesis |
132 thus ?thesis |
133 by (metis 1 min_max.le_iff_sup real_less_def) |
133 by (metis 1 min_max.le_iff_sup less_le) |
134 qed |
134 qed |
135 |
135 |
136 lemma Sup_insert_if: |
136 lemma Sup_insert_if: |
137 fixes X :: "real set" |
137 fixes X :: "real set" |
138 assumes z: "!!x. x \<in> X \<Longrightarrow> x \<le> z" |
138 assumes z: "!!x. x \<in> X \<Longrightarrow> x \<le> z" |
175 |
175 |
176 lemma Sup_finite_le_iff: |
176 lemma Sup_finite_le_iff: |
177 fixes S :: "real set" |
177 fixes S :: "real set" |
178 assumes fS: "finite S" and Se: "S \<noteq> {}" |
178 assumes fS: "finite S" and Se: "S \<noteq> {}" |
179 shows "a \<ge> Sup S \<longleftrightarrow> (\<forall> x \<in> S. a \<ge> x)" |
179 shows "a \<ge> Sup S \<longleftrightarrow> (\<forall> x \<in> S. a \<ge> x)" |
180 by (metis Max_ge Se Sup_finite_Max Sup_finite_in fS real_le_trans) |
180 by (metis Max_ge Se Sup_finite_Max Sup_finite_in fS order_trans) |
181 |
181 |
182 lemma Sup_finite_gt_iff: |
182 lemma Sup_finite_gt_iff: |
183 fixes S :: "real set" |
183 fixes S :: "real set" |
184 assumes fS: "finite S" and Se: "S \<noteq> {}" |
184 assumes fS: "finite S" and Se: "S \<noteq> {}" |
185 shows "a < Sup S \<longleftrightarrow> (\<exists> x \<in> S. a < x)" |
185 shows "a < Sup S \<longleftrightarrow> (\<exists> x \<in> S. a < x)" |
289 qed |
289 qed |
290 |
290 |
291 lemma Inf_lower2: |
291 lemma Inf_lower2: |
292 fixes x :: real |
292 fixes x :: real |
293 shows "x \<in> X \<Longrightarrow> x \<le> y \<Longrightarrow> (!!x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> Inf X \<le> y" |
293 shows "x \<in> X \<Longrightarrow> x \<le> y \<Longrightarrow> (!!x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> Inf X \<le> y" |
294 by (metis Inf_lower real_le_trans) |
294 by (metis Inf_lower order_trans) |
295 |
295 |
296 lemma Inf_real_iff: |
296 lemma Inf_real_iff: |
297 fixes z :: real |
297 fixes z :: real |
298 shows "X \<noteq> {} \<Longrightarrow> (!!x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> (\<exists>x\<in>X. x<y) \<longleftrightarrow> Inf X < y" |
298 shows "X \<noteq> {} \<Longrightarrow> (!!x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> (\<exists>x\<in>X. x<y) \<longleftrightarrow> Inf X < y" |
299 by (metis Inf_greatest Inf_lower less_le_not_le real_le_linear |
299 by (metis Inf_greatest Inf_lower less_le_not_le linear |
300 order_less_le_trans) |
300 order_less_le_trans) |
301 |
301 |
302 lemma Inf_eq: |
302 lemma Inf_eq: |
303 fixes a :: real |
303 fixes a :: real |
304 shows "(!!x. x \<in> X \<Longrightarrow> a \<le> x) \<Longrightarrow> (!!y. (!!x. x \<in> X \<Longrightarrow> y \<le> x) \<Longrightarrow> y \<le> a) \<Longrightarrow> Inf X = a" |
304 shows "(!!x. x \<in> X \<Longrightarrow> a \<le> x) \<Longrightarrow> (!!y. (!!x. x \<in> X \<Longrightarrow> y \<le> x) \<Longrightarrow> y \<le> a) \<Longrightarrow> Inf X = a" |
305 by (metis Inf_greatest Inf_lower add_le_cancel_left diff_add_cancel |
305 by (metis Inf_greatest Inf_lower add_le_cancel_left diff_add_cancel |
306 insert_absorb insert_not_empty real_le_antisym) |
306 insert_absorb insert_not_empty order_antisym) |
307 |
307 |
308 lemma Inf_ge: |
308 lemma Inf_ge: |
309 fixes S :: "real set" |
309 fixes S :: "real set" |
310 shows "S \<noteq> {} \<Longrightarrow> b <=* S \<Longrightarrow> Inf S \<ge> b" |
310 shows "S \<noteq> {} \<Longrightarrow> b <=* S \<Longrightarrow> Inf S \<ge> b" |
311 by (metis SupInf.Inf_greatest setge_def) |
311 by (metis SupInf.Inf_greatest setge_def) |
322 shows "Inf (insert a X) = min a (Inf X)" |
322 shows "Inf (insert a X) = min a (Inf X)" |
323 proof (cases "a \<le> Inf X") |
323 proof (cases "a \<le> Inf X") |
324 case True |
324 case True |
325 thus ?thesis |
325 thus ?thesis |
326 by (simp add: min_def) |
326 by (simp add: min_def) |
327 (blast intro: Inf_eq_minimum real_le_refl real_le_trans z) |
327 (blast intro: Inf_eq_minimum order_trans z) |
328 next |
328 next |
329 case False |
329 case False |
330 hence 1:"Inf X < a" by simp |
330 hence 1:"Inf X < a" by simp |
331 have "Inf (insert a X) \<le> Inf X" |
331 have "Inf (insert a X) \<le> Inf X" |
332 apply (rule Inf_greatest) |
332 apply (rule Inf_greatest) |
333 apply (metis empty_psubset_nonempty psubset_eq x) |
333 apply (metis ex_in_conv x) |
334 apply (rule Inf_lower_EX) |
334 apply (rule Inf_lower_EX) |
335 apply (erule insertI2) |
335 apply (erule insertI2) |
336 apply (metis insert_iff real_le_linear real_le_refl real_le_trans z) |
336 apply (metis insert_iff linear order_refl order_trans z) |
337 done |
337 done |
338 moreover |
338 moreover |
339 have "Inf X \<le> Inf (insert a X)" |
339 have "Inf X \<le> Inf (insert a X)" |
340 apply (rule Inf_greatest) |
340 apply (rule Inf_greatest) |
341 apply blast |
341 apply blast |
342 apply (metis False Inf_lower insertE real_le_linear z) |
342 apply (metis False Inf_lower insertE linear z) |
343 done |
343 done |
344 ultimately have "Inf (insert a X) = Inf X" |
344 ultimately have "Inf (insert a X) = Inf X" |
345 by (blast intro: antisym ) |
345 by (blast intro: antisym ) |
346 thus ?thesis |
346 thus ?thesis |
347 by (metis False min_max.inf_absorb2 real_le_linear) |
347 by (metis False min_max.inf_absorb2 linear) |
348 qed |
348 qed |
349 |
349 |
350 lemma Inf_insert_if: |
350 lemma Inf_insert_if: |
351 fixes X :: "real set" |
351 fixes X :: "real set" |
352 assumes z: "!!x. x \<in> X \<Longrightarrow> z \<le> x" |
352 assumes z: "!!x. x \<in> X \<Longrightarrow> z \<le> x" |
375 using Inf_finite_Min[OF fS Se] Min_in[OF fS Se] by metis |
375 using Inf_finite_Min[OF fS Se] Min_in[OF fS Se] by metis |
376 |
376 |
377 lemma Inf_finite_ge_iff: |
377 lemma Inf_finite_ge_iff: |
378 fixes S :: "real set" |
378 fixes S :: "real set" |
379 shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<le> Inf S \<longleftrightarrow> (\<forall> x \<in> S. a \<le> x)" |
379 shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<le> Inf S \<longleftrightarrow> (\<forall> x \<in> S. a \<le> x)" |
380 by (metis Inf_finite_Min Inf_finite_in Min_le real_le_trans) |
380 by (metis Inf_finite_Min Inf_finite_in Min_le order_trans) |
381 |
381 |
382 lemma Inf_finite_le_iff: |
382 lemma Inf_finite_le_iff: |
383 fixes S :: "real set" |
383 fixes S :: "real set" |
384 shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<ge> Inf S \<longleftrightarrow> (\<exists> x \<in> S. a \<ge> x)" |
384 shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<ge> Inf S \<longleftrightarrow> (\<exists> x \<in> S. a \<ge> x)" |
385 by (metis Inf_finite_Min Inf_finite_ge_iff Inf_finite_in Min_le |
385 by (metis Inf_finite_Min Inf_finite_ge_iff Inf_finite_in Min_le |
386 real_le_antisym real_le_linear) |
386 order_antisym linear) |
387 |
387 |
388 lemma Inf_finite_gt_iff: |
388 lemma Inf_finite_gt_iff: |
389 fixes S :: "real set" |
389 fixes S :: "real set" |
390 shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a < Inf S \<longleftrightarrow> (\<forall> x \<in> S. a < x)" |
390 shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a < Inf S \<longleftrightarrow> (\<forall> x \<in> S. a < x)" |
391 by (metis Inf_finite_le_iff linorder_not_less) |
391 by (metis Inf_finite_le_iff linorder_not_less) |
415 have "\<bar>- Sup (uminus ` S) - l\<bar> = \<bar>Sup (uminus ` S) - (-l)\<bar>" |
415 have "\<bar>- Sup (uminus ` S) - l\<bar> = \<bar>Sup (uminus ` S) - (-l)\<bar>" |
416 by auto |
416 by auto |
417 also have "... \<le> e" |
417 also have "... \<le> e" |
418 apply (rule Sup_asclose) |
418 apply (rule Sup_asclose) |
419 apply (auto simp add: S) |
419 apply (auto simp add: S) |
420 apply (metis abs_minus_add_cancel b add_commute real_diff_def) |
420 apply (metis abs_minus_add_cancel b add_commute diff_def) |
421 done |
421 done |
422 finally have "\<bar>- Sup (uminus ` S) - l\<bar> \<le> e" . |
422 finally have "\<bar>- Sup (uminus ` S) - l\<bar> \<le> e" . |
423 thus ?thesis |
423 thus ?thesis |
424 by (simp add: Inf_real_def) |
424 by (simp add: Inf_real_def) |
425 qed |
425 qed |
472 shows "\<exists>c. a \<le> c & c \<le> b & (\<forall>x. a \<le> x & x < c --> P x) & |
472 shows "\<exists>c. a \<le> c & c \<le> b & (\<forall>x. a \<le> x & x < c --> P x) & |
473 (\<forall>d. (\<forall>x. a \<le> x & x < d --> P x) --> d \<le> c)" |
473 (\<forall>d. (\<forall>x. a \<le> x & x < d --> P x) --> d \<le> c)" |
474 proof (rule exI [where x = "Sup {d. \<forall>x. a \<le> x & x < d --> P x}"], auto) |
474 proof (rule exI [where x = "Sup {d. \<forall>x. a \<le> x & x < d --> P x}"], auto) |
475 show "a \<le> Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}" |
475 show "a \<le> Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}" |
476 by (rule SupInf.Sup_upper [where z=b], auto) |
476 by (rule SupInf.Sup_upper [where z=b], auto) |
477 (metis `a < b` `\<not> P b` real_le_linear real_less_def) |
477 (metis `a < b` `\<not> P b` linear less_le) |
478 next |
478 next |
479 show "Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c} \<le> b" |
479 show "Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c} \<le> b" |
480 apply (rule SupInf.Sup_least) |
480 apply (rule SupInf.Sup_least) |
481 apply (auto simp add: ) |
481 apply (auto simp add: ) |
482 apply (metis less_le_not_le) |
482 apply (metis less_le_not_le) |
483 apply (metis `a<b` `~ P b` real_le_linear real_less_def) |
483 apply (metis `a<b` `~ P b` linear less_le) |
484 done |
484 done |
485 next |
485 next |
486 fix x |
486 fix x |
487 assume x: "a \<le> x" and lt: "x < Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}" |
487 assume x: "a \<le> x" and lt: "x < Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}" |
488 show "P x" |
488 show "P x" |
493 next |
493 next |
494 fix d |
494 fix d |
495 assume 0: "\<forall>x. a \<le> x \<and> x < d \<longrightarrow> P x" |
495 assume 0: "\<forall>x. a \<le> x \<and> x < d \<longrightarrow> P x" |
496 thus "d \<le> Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}" |
496 thus "d \<le> Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}" |
497 by (rule_tac z="b" in SupInf.Sup_upper, auto) |
497 by (rule_tac z="b" in SupInf.Sup_upper, auto) |
498 (metis `a<b` `~ P b` real_le_linear real_less_def) |
498 (metis `a<b` `~ P b` linear less_le) |
499 qed |
499 qed |
500 |
500 |
501 end |
501 end |