# Theory SupInf

Up to index of Isabelle/HOL

theory SupInf
imports RComplete
`(*  Author: Amine Chaieb and L C Paulson, University of Cambridge *)header {*Sup and Inf Operators on Sets of Reals.*}theory SupInfimports RCompletebegininstantiation real :: Sup begindefinition  Sup_real_def: "Sup X == (LEAST z::real. ∀x∈X. x≤z)"instance ..endinstantiation real :: Inf begindefinition  Inf_real_def: "Inf (X::real set) == - (Sup (uminus ` X))"instance ..endsubsection{*Supremum of a set of reals*}lemma Sup_upper [intro]: (*REAL_SUP_UBOUND in HOL4*)  fixes x :: real  assumes x: "x ∈ X"      and z: "!!x. x ∈ X ==> x ≤ z"  shows "x ≤ Sup X"proof (auto simp add: Sup_real_def)   from complete_real  obtain s where s: "(∀y∈X. y ≤ s) & (∀z. ((∀y∈X. y ≤ z) --> s ≤ z))"    by (blast intro: x z)  hence "x ≤ s"    by (blast intro: x z)  also with s have "... = (LEAST z. ∀x∈X. x ≤ z)"    by (fast intro: Least_equality [symmetric])    finally show "x ≤ (LEAST z. ∀x∈X. x ≤ z)" .qedlemma Sup_least [intro]: (*REAL_IMP_SUP_LE in HOL4*)  fixes z :: real  assumes x: "X ≠ {}"      and z: "!!x. x ∈ X ==> x ≤ z"  shows "Sup X ≤ z"proof (auto simp add: Sup_real_def)   from complete_real x  obtain s where s: "(∀y∈X. y ≤ s) & (∀z. ((∀y∈X. y ≤ z) --> s ≤ z))"    by (blast intro: z)  hence "(LEAST z. ∀x∈X. x ≤ z) = s"    by (best intro: Least_equality)    also with s z have "... ≤ z"    by blast  finally show "(LEAST z. ∀x∈X. x ≤ z) ≤ z" .qedlemma less_SupE:  fixes y :: real  assumes "y < Sup X" "X ≠ {}"  obtains x where "x∈X" "y < x"by (metis SupInf.Sup_least assms linorder_not_less that)lemma Sup_singleton [simp]: "Sup {x::real} = x"  by (force intro: Least_equality simp add: Sup_real_def) lemma Sup_eq_maximum: (*REAL_SUP_MAX in HOL4*)  fixes z :: real  assumes X: "z ∈ X" and z: "!!x. x ∈ X ==> x ≤ z"  shows  "Sup X = z"  by (force intro: Least_equality X z simp add: Sup_real_def) lemma Sup_upper2: (*REAL_IMP_LE_SUP in HOL4*)  fixes x :: real  shows "x ∈ X ==> y ≤ x ==> (!!x. x ∈ X ==> x ≤ z) ==> y ≤ Sup X"  by (metis Sup_upper order_trans)lemma Sup_real_iff : (*REAL_SUP_LE in HOL4*)  fixes z :: real  shows "X ~= {} ==> (!!x. x ∈ X ==> x ≤ z) ==> (∃x∈X. y<x) <-> y < Sup X"  by (rule iffI, metis less_le_trans Sup_upper, metis Sup_least not_less)lemma Sup_eq:  fixes a :: real  shows "(!!x. x ∈ X ==> x ≤ a)         ==> (!!y. (!!x. x ∈ X ==> x ≤ y) ==> a ≤ y) ==> Sup X = a"  by (metis Sup_least Sup_upper add_le_cancel_left diff_add_cancel insert_absorb        insert_not_empty order_antisym)lemma Sup_le:  fixes S :: "real set"  shows "S ≠ {} ==> S *<= b ==> Sup S ≤ b"by (metis SupInf.Sup_least setle_def)lemma Sup_upper_EX:   fixes x :: real  shows "x ∈ X ==> ∃z. ∀x. x ∈ X --> x ≤ z ==>  x ≤ Sup X"  by blastlemma Sup_insert_nonempty:   fixes x :: real  assumes x: "x ∈ X"      and z: "!!x. x ∈ X ==> x ≤ z"  shows "Sup (insert a X) = max a (Sup X)"proof (cases "Sup X ≤ a")  case True  thus ?thesis    apply (simp add: max_def)    apply (rule Sup_eq_maximum)    apply (rule insertI1)    apply (metis Sup_upper [OF _ z] insertE linear order_trans)    donenext  case False  hence 1:"a < Sup X" by simp  have "Sup X ≤ Sup (insert a X)"    apply (rule Sup_least)    apply (metis ex_in_conv x)    apply (rule Sup_upper_EX)     apply blast    apply (metis insert_iff linear order_trans z)    done  moreover   have "Sup (insert a X) ≤ Sup X"    apply (rule Sup_least)    apply blast    apply (metis False Sup_upper insertE linear z)    done  ultimately have "Sup (insert a X) = Sup X"    by (blast intro:  antisym )  thus ?thesis    by (metis 1 min_max.le_iff_sup less_le)qedlemma Sup_insert_if:   fixes X :: "real set"  assumes z: "!!x. x ∈ X ==> x ≤ z"  shows "Sup (insert a X) = (if X={} then a else max a (Sup X))"by auto (metis Sup_insert_nonempty z) lemma Sup:   fixes S :: "real set"  shows "S ≠ {} ==> (∃b. S *<= b) ==> isLub UNIV S (Sup S)"by  (auto simp add: isLub_def setle_def leastP_def isUb_def intro!: setgeI) lemma Sup_finite_Max:   fixes S :: "real set"  assumes fS: "finite S" and Se: "S ≠ {}"  shows "Sup S = Max S"using fS Seproof-  let ?m = "Max S"  from Max_ge[OF fS] have Sm: "∀ x∈ S. x ≤ ?m" by metis  with Sup[OF Se] have lub: "isLub UNIV S (Sup S)" by (metis setle_def)  from Max_in[OF fS Se] lub have mrS: "?m ≤ Sup S"    by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def)  moreover  have "Sup S ≤ ?m" using Sm lub    by (auto simp add: isLub_def leastP_def isUb_def setle_def setge_def)  ultimately  show ?thesis by arithqedlemma Sup_finite_in:  fixes S :: "real set"  assumes fS: "finite S" and Se: "S ≠ {}"  shows "Sup S ∈ S"  using Sup_finite_Max[OF fS Se] Max_in[OF fS Se] by metislemma Sup_finite_ge_iff:   fixes S :: "real set"  assumes fS: "finite S" and Se: "S ≠ {}"  shows "a ≤ Sup S <-> (∃ x ∈ S. a ≤ x)"by (metis Max_ge Se Sup_finite_Max Sup_finite_in fS linorder_not_le less_le_trans)lemma Sup_finite_le_iff:   fixes S :: "real set"  assumes fS: "finite S" and Se: "S ≠ {}"  shows "a ≥ Sup S <-> (∀ x ∈ S. a ≥ x)"by (metis Max_ge Se Sup_finite_Max Sup_finite_in fS order_trans)lemma Sup_finite_gt_iff:   fixes S :: "real set"  assumes fS: "finite S" and Se: "S ≠ {}"  shows "a < Sup S <-> (∃ x ∈ S. a < x)"by (metis Se Sup_finite_le_iff fS linorder_not_less)lemma Sup_finite_lt_iff:   fixes S :: "real set"  assumes fS: "finite S" and Se: "S ≠ {}"  shows "a > Sup S <-> (∀ x ∈ S. a > x)"by (metis Se Sup_finite_ge_iff fS linorder_not_less)lemma Sup_unique:  fixes S :: "real set"  shows "S *<= b ==> (∀b' < b. ∃x ∈ S. b' < x) ==> Sup S = b"unfolding setle_defapply (rule Sup_eq, auto) apply (metis linorder_not_less) donelemma Sup_abs_le:  fixes S :: "real set"  shows "S ≠ {} ==> (∀x∈S. ¦x¦ ≤ a) ==> ¦Sup S¦ ≤ a"by (auto simp add: abs_le_interval_iff) (metis Sup_upper2) lemma Sup_bounds:  fixes S :: "real set"  assumes Se: "S ≠ {}" and l: "a <=* S" and u: "S *<= b"  shows "a ≤ Sup S ∧ Sup S ≤ b"proof-  from Sup[OF Se] u have lub: "isLub UNIV S (Sup S)" by blast  hence b: "Sup S ≤ b" using u     by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def)   from Se obtain y where y: "y ∈ S" by blast  from lub l have "a ≤ Sup S"    by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def)       (metis le_iff_sup le_sup_iff y)  with b show ?thesis by blastqedlemma Sup_asclose:   fixes S :: "real set"  assumes S:"S ≠ {}" and b: "∀x∈S. ¦x - l¦ ≤ e" shows "¦Sup S - l¦ ≤ e"proof-  have th: "!!(x::real) l e. ¦x - l¦ ≤ e <-> l - e ≤ x ∧ x ≤ l + e" by arith  thus ?thesis using S b Sup_bounds[of S "l - e" "l+e"] unfolding th    by  (auto simp add: setge_def setle_def)qedlemma Sup_lessThan[simp]: "Sup {..<x} = (x::real)"  by (auto intro!: Sup_eq intro: dense_le)lemma Sup_greaterThanLessThan[simp]: "y < x ==> Sup {y<..<x} = (x::real)"  by (auto intro!: Sup_eq intro: dense_le_bounded)lemma Sup_atLeastLessThan[simp]: "y < x ==> Sup {y..<x} = (x::real)"  by (auto intro!: Sup_eq intro: dense_le_bounded)lemma Sup_atMost[simp]: "Sup {..x} = (x::real)"  by (auto intro!: Sup_eq_maximum)lemma Sup_greaterThanAtMost[simp]: "y < x ==> Sup {y<..x} = (x::real)"  by (auto intro!: Sup_eq_maximum)lemma Sup_atLeastAtMost[simp]: "y ≤ x ==> Sup {y..x} = (x::real)"  by (auto intro!: Sup_eq_maximum)subsection{*Infimum of a set of reals*}lemma Inf_lower [intro]:   fixes z :: real  assumes x: "x ∈ X"      and z: "!!x. x ∈ X ==> z ≤ x"  shows "Inf X ≤ x"proof -  have "-x ≤ Sup (uminus ` X)"    by (rule Sup_upper [where z = "-z"]) (auto simp add: image_iff x z)  thus ?thesis     by (auto simp add: Inf_real_def)qedlemma Inf_greatest [intro]:   fixes z :: real  assumes x: "X ≠ {}"      and z: "!!x. x ∈ X ==> z ≤ x"  shows "z ≤ Inf X"proof -  have "Sup (uminus ` X) ≤ -z" using x z by force  hence "z ≤ - Sup (uminus ` X)"    by simp  thus ?thesis     by (auto simp add: Inf_real_def)qedlemma Inf_singleton [simp]: "Inf {x::real} = x"  by (simp add: Inf_real_def)  lemma Inf_eq_minimum: (*REAL_INF_MIN in HOL4*)  fixes z :: real  assumes x: "z ∈ X" and z: "!!x. x ∈ X ==> z ≤ x"  shows  "Inf X = z"proof -  have "Sup (uminus ` X) = -z" using x z    by (force intro: Sup_eq_maximum x z)  thus ?thesis    by (simp add: Inf_real_def) qed lemma Inf_lower2:  fixes x :: real  shows "x ∈ X ==> x ≤ y ==> (!!x. x ∈ X ==> z ≤ x) ==> Inf X ≤ y"  by (metis Inf_lower order_trans)lemma Inf_real_iff:  fixes z :: real  shows "X ≠ {} ==> (!!x. x ∈ X ==> z ≤ x) ==> (∃x∈X. x<y) <-> Inf X < y"  by (metis Inf_greatest Inf_lower less_le_not_le linear            order_less_le_trans)lemma Inf_eq:  fixes a :: real  shows "(!!x. x ∈ X ==> a ≤ x) ==> (!!y. (!!x. x ∈ X ==> y ≤ x) ==> y ≤ a) ==> Inf X = a"  by (metis Inf_greatest Inf_lower add_le_cancel_left diff_add_cancel        insert_absorb insert_not_empty order_antisym)lemma Inf_ge:   fixes S :: "real set"  shows "S ≠ {} ==> b <=* S ==> Inf S ≥ b"by (metis SupInf.Inf_greatest setge_def)lemma Inf_lower_EX:   fixes x :: real  shows "x ∈ X ==> ∃z. ∀x. x ∈ X --> z ≤ x ==> Inf X ≤ x"  by blastlemma Inf_insert_nonempty:   fixes x :: real  assumes x: "x ∈ X"      and z: "!!x. x ∈ X ==> z ≤ x"  shows "Inf (insert a X) = min a (Inf X)"proof (cases "a ≤ Inf X")  case True  thus ?thesis    by (simp add: min_def)       (blast intro: Inf_eq_minimum order_trans z)next  case False  hence 1:"Inf X < a" by simp  have "Inf (insert a X) ≤ Inf X"    apply (rule Inf_greatest)    apply (metis ex_in_conv x)    apply (rule Inf_lower_EX)    apply (erule insertI2)    apply (metis insert_iff linear order_trans z)    done  moreover   have "Inf X ≤ Inf (insert a X)"    apply (rule Inf_greatest)    apply blast    apply (metis False Inf_lower insertE linear z)     done  ultimately have "Inf (insert a X) = Inf X"    by (blast intro:  antisym )  thus ?thesis    by (metis False min_max.inf_absorb2 linear)qedlemma Inf_insert_if:   fixes X :: "real set"  assumes z:  "!!x. x ∈ X ==> z ≤ x"  shows "Inf (insert a X) = (if X={} then a else min a (Inf X))"by auto (metis Inf_insert_nonempty z) lemma Inf_greater:  fixes z :: real  shows "X ≠ {} ==> Inf X < z ==> ∃x ∈ X. x < z"  by (metis Inf_real_iff not_leE)lemma Inf_close:  fixes e :: real  shows "X ≠ {} ==> 0 < e ==> ∃x ∈ X. x < Inf X + e"  by (metis add_strict_increasing add_commute Inf_greater linorder_not_le pos_add_strict)lemma Inf_finite_Min:  fixes S :: "real set"  shows "finite S ==> S ≠ {} ==> Inf S = Min S"by (simp add: Inf_real_def Sup_finite_Max image_image) lemma Inf_finite_in:   fixes S :: "real set"  assumes fS: "finite S" and Se: "S ≠ {}"  shows "Inf S ∈ S"  using Inf_finite_Min[OF fS Se] Min_in[OF fS Se] by metislemma Inf_finite_ge_iff:   fixes S :: "real set"  shows "finite S ==> S ≠ {} ==> a ≤ Inf S <-> (∀ x ∈ S. a ≤ x)"by (metis Inf_finite_Min Inf_finite_in Min_le order_trans)lemma Inf_finite_le_iff:  fixes S :: "real set"  shows "finite S ==> S ≠ {} ==> a ≥ Inf S <-> (∃ x ∈ S. a ≥ x)"by (metis Inf_finite_Min Inf_finite_ge_iff Inf_finite_in Min_le          order_antisym linear)lemma Inf_finite_gt_iff:   fixes S :: "real set"  shows "finite S ==> S ≠ {} ==> a < Inf S <-> (∀ x ∈ S. a < x)"by (metis Inf_finite_le_iff linorder_not_less)lemma Inf_finite_lt_iff:   fixes S :: "real set"  shows "finite S ==> S ≠ {} ==> a > Inf S <-> (∃ x ∈ S. a > x)"by (metis Inf_finite_ge_iff linorder_not_less)lemma Inf_unique:  fixes S :: "real set"  shows "b <=* S ==> (∀b' > b. ∃x ∈ S. b' > x) ==> Inf S = b"unfolding setge_defapply (rule Inf_eq, auto) apply (metis less_le_not_le linorder_not_less) donelemma Inf_abs_ge:  fixes S :: "real set"  shows "S ≠ {} ==> (∀x∈S. ¦x¦ ≤ a) ==> ¦Inf S¦ ≤ a"by (simp add: Inf_real_def) (rule Sup_abs_le, auto) lemma Inf_asclose:  fixes S :: "real set"  assumes S:"S ≠ {}" and b: "∀x∈S. ¦x - l¦ ≤ e" shows "¦Inf S - l¦ ≤ e"proof -  have "¦- Sup (uminus ` S) - l¦ =  ¦Sup (uminus ` S) - (-l)¦"    by auto  also have "... ≤ e"     apply (rule Sup_asclose)     apply (auto simp add: S)    apply (metis abs_minus_add_cancel b add_commute diff_minus)    done  finally have "¦- Sup (uminus ` S) - l¦ ≤ e" .  thus ?thesis    by (simp add: Inf_real_def)qedlemma Inf_greaterThanLessThan[simp]: "y < x ==> Inf {y<..<x} = (y::real)"  by (simp add: Inf_real_def)lemma Inf_atLeastLessThan[simp]: "y < x ==> Inf {y..<x} = (y::real)"  by (simp add: Inf_real_def)lemma Inf_atLeast[simp]: "Inf {x..} = (x::real)"  by (simp add: Inf_real_def)lemma Inf_greaterThanAtMost[simp]: "y < x ==> Inf {y<..x} = (y::real)"  by (simp add: Inf_real_def)lemma Inf_atLeastAtMost[simp]: "y ≤ x ==> Inf {y..x} = (y::real)"  by (simp add: Inf_real_def)subsection{*Relate max and min to Sup and Inf.*}lemma real_max_Sup:  fixes x :: real  shows "max x y = Sup {x,y}"proof-  have "Sup {x,y} ≤ max x y" by (simp add: Sup_finite_le_iff)  moreover  have "max x y ≤ Sup {x,y}" by (simp add: linorder_linear Sup_finite_ge_iff)  ultimately show ?thesis by arithqedlemma real_min_Inf:   fixes x :: real  shows "min x y = Inf {x,y}"proof-  have "Inf {x,y} ≤ min x y" by (simp add: linorder_linear Inf_finite_le_iff)  moreover  have "min x y ≤ Inf {x,y}" by (simp add:  Inf_finite_ge_iff)  ultimately show ?thesis by arithqedlemma reals_complete_interval:  fixes a::real and b::real  assumes "a < b" and "P a" and "~P b"  shows "∃c. a ≤ c & c ≤ b & (∀x. a ≤ x & x < c --> P x) &             (∀d. (∀x. a ≤ x & x < d --> P x) --> d ≤ c)"proof (rule exI [where x = "Sup {d. ∀x. a ≤ x & x < d --> P x}"], auto)  show "a ≤ Sup {d. ∀c. a ≤ c ∧ c < d --> P c}"    by (rule SupInf.Sup_upper [where z=b], auto)       (metis `a < b` `¬ P b` linear less_le)next  show "Sup {d. ∀c. a ≤ c ∧ c < d --> P c} ≤ b"    apply (rule SupInf.Sup_least)     apply (auto simp add: )    apply (metis less_le_not_le)    apply (metis `a<b` `~ P b` linear less_le)    donenext  fix x  assume x: "a ≤ x" and lt: "x < Sup {d. ∀c. a ≤ c ∧ c < d --> P c}"  show "P x"    apply (rule less_SupE [OF lt], auto)    apply (metis less_le_not_le)    apply (metis x)     donenext  fix d    assume 0: "∀x. a ≤ x ∧ x < d --> P x"    thus "d ≤ Sup {d. ∀c. a ≤ c ∧ c < d --> P c}"      by (rule_tac z="b" in SupInf.Sup_upper, auto)          (metis `a<b` `~ P b` linear less_le)qedend`