# HG changeset patch # User wenzelm # Date 1414575300 -3600 # Node ID 922a233805d26f97c2b38518601e24c714ea2ef0 # Parent 3c34490ccd4c5f4912be17a6f9a280496d926cf6 more standard theory name; diff -r 3c34490ccd4c -r 922a233805d2 src/HOL/Library/Library.thy --- a/src/HOL/Library/Library.thy Wed Oct 29 09:42:46 2014 +0100 +++ b/src/HOL/Library/Library.thy Wed Oct 29 10:35:00 2014 +0100 @@ -38,7 +38,7 @@ Lattice_Constructions Linear_Temporal_Logic_on_Streams ListVector - Lubs_Glbs + Lub_Glb Mapping Monad_Syntax More_List diff -r 3c34490ccd4c -r 922a233805d2 src/HOL/Library/Lub_Glb.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Lub_Glb.thy Wed Oct 29 10:35:00 2014 +0100 @@ -0,0 +1,245 @@ +(* Title: HOL/Library/Lub_Glb.thy + Author: Jacques D. Fleuriot, University of Cambridge + Author: Amine Chaieb, University of Cambridge *) + +header {* Definitions of Least Upper Bounds and Greatest Lower Bounds *} + +theory Lub_Glb +imports Complex_Main +begin + +text {* Thanks to suggestions by James Margetson *} + +definition setle :: "'a set \ 'a::ord \ bool" (infixl "*<=" 70) + where "S *<= x = (ALL y: S. y \ x)" + +definition setge :: "'a::ord \ 'a set \ bool" (infixl "<=*" 70) + where "x <=* S = (ALL y: S. x \ y)" + + +subsection {* Rules for the Relations @{text "*<="} and @{text "<=*"} *} + +lemma setleI: "ALL y: S. y \ x \ S *<= x" + by (simp add: setle_def) + +lemma setleD: "S *<= x \ y: S \ y \ x" + by (simp add: setle_def) + +lemma setgeI: "ALL y: S. x \ y \ x <=* S" + by (simp add: setge_def) + +lemma setgeD: "x <=* S \ y: S \ x \ y" + by (simp add: setge_def) + + +definition leastP :: "('a \ bool) \ 'a::ord \ bool" + where "leastP P x = (P x \ x <=* Collect P)" + +definition isUb :: "'a set \ 'a set \ 'a::ord \ bool" + where "isUb R S x = (S *<= x \ x: R)" + +definition isLub :: "'a set \ 'a set \ 'a::ord \ bool" + where "isLub R S x = leastP (isUb R S) x" + +definition ubs :: "'a set \ 'a::ord set \ 'a set" + where "ubs R S = Collect (isUb R S)" + + +subsection {* Rules about the Operators @{term leastP}, @{term ub} and @{term lub} *} + +lemma leastPD1: "leastP P x \ P x" + by (simp add: leastP_def) + +lemma leastPD2: "leastP P x \ x <=* Collect P" + by (simp add: leastP_def) + +lemma leastPD3: "leastP P x \ y: Collect P \ x \ y" + by (blast dest!: leastPD2 setgeD) + +lemma isLubD1: "isLub R S x \ S *<= x" + by (simp add: isLub_def isUb_def leastP_def) + +lemma isLubD1a: "isLub R S x \ x: R" + by (simp add: isLub_def isUb_def leastP_def) + +lemma isLub_isUb: "isLub R S x \ isUb R S x" + unfolding isUb_def by (blast dest: isLubD1 isLubD1a) + +lemma isLubD2: "isLub R S x \ y : S \ y \ x" + by (blast dest!: isLubD1 setleD) + +lemma isLubD3: "isLub R S x \ leastP (isUb R S) x" + by (simp add: isLub_def) + +lemma isLubI1: "leastP(isUb R S) x \ isLub R S x" + by (simp add: isLub_def) + +lemma isLubI2: "isUb R S x \ x <=* Collect (isUb R S) \ isLub R S x" + by (simp add: isLub_def leastP_def) + +lemma isUbD: "isUb R S x \ y : S \ y \ x" + by (simp add: isUb_def setle_def) + +lemma isUbD2: "isUb R S x \ S *<= x" + by (simp add: isUb_def) + +lemma isUbD2a: "isUb R S x \ x: R" + by (simp add: isUb_def) + +lemma isUbI: "S *<= x \ x: R \ isUb R S x" + by (simp add: isUb_def) + +lemma isLub_le_isUb: "isLub R S x \ isUb R S y \ x \ y" + unfolding isLub_def by (blast intro!: leastPD3) + +lemma isLub_ubs: "isLub R S x \ x <=* ubs R S" + unfolding ubs_def isLub_def by (rule leastPD2) + +lemma isLub_unique: "[| isLub R S x; isLub R S y |] ==> x = (y::'a::linorder)" + apply (frule isLub_isUb) + apply (frule_tac x = y in isLub_isUb) + apply (blast intro!: order_antisym dest!: isLub_le_isUb) + done + +lemma isUb_UNIV_I: "(\y. y \ S \ y \ u) \ isUb UNIV S u" + by (simp add: isUbI setleI) + + +definition greatestP :: "('a \ bool) \ 'a::ord \ bool" + where "greatestP P x = (P x \ Collect P *<= x)" + +definition isLb :: "'a set \ 'a set \ 'a::ord \ bool" + where "isLb R S x = (x <=* S \ x: R)" + +definition isGlb :: "'a set \ 'a set \ 'a::ord \ bool" + where "isGlb R S x = greatestP (isLb R S) x" + +definition lbs :: "'a set \ 'a::ord set \ 'a set" + where "lbs R S = Collect (isLb R S)" + + +subsection {* Rules about the Operators @{term greatestP}, @{term isLb} and @{term isGlb} *} + +lemma greatestPD1: "greatestP P x \ P x" + by (simp add: greatestP_def) + +lemma greatestPD2: "greatestP P x \ Collect P *<= x" + by (simp add: greatestP_def) + +lemma greatestPD3: "greatestP P x \ y: Collect P \ x \ y" + by (blast dest!: greatestPD2 setleD) + +lemma isGlbD1: "isGlb R S x \ x <=* S" + by (simp add: isGlb_def isLb_def greatestP_def) + +lemma isGlbD1a: "isGlb R S x \ x: R" + by (simp add: isGlb_def isLb_def greatestP_def) + +lemma isGlb_isLb: "isGlb R S x \ isLb R S x" + unfolding isLb_def by (blast dest: isGlbD1 isGlbD1a) + +lemma isGlbD2: "isGlb R S x \ y : S \ y \ x" + by (blast dest!: isGlbD1 setgeD) + +lemma isGlbD3: "isGlb R S x \ greatestP (isLb R S) x" + by (simp add: isGlb_def) + +lemma isGlbI1: "greatestP (isLb R S) x \ isGlb R S x" + by (simp add: isGlb_def) + +lemma isGlbI2: "isLb R S x \ Collect (isLb R S) *<= x \ isGlb R S x" + by (simp add: isGlb_def greatestP_def) + +lemma isLbD: "isLb R S x \ y : S \ y \ x" + by (simp add: isLb_def setge_def) + +lemma isLbD2: "isLb R S x \ x <=* S " + by (simp add: isLb_def) + +lemma isLbD2a: "isLb R S x \ x: R" + by (simp add: isLb_def) + +lemma isLbI: "x <=* S \ x: R \ isLb R S x" + by (simp add: isLb_def) + +lemma isGlb_le_isLb: "isGlb R S x \ isLb R S y \ x \ y" + unfolding isGlb_def by (blast intro!: greatestPD3) + +lemma isGlb_ubs: "isGlb R S x \ lbs R S *<= x" + unfolding lbs_def isGlb_def by (rule greatestPD2) + +lemma isGlb_unique: "[| isGlb R S x; isGlb R S y |] ==> x = (y::'a::linorder)" + apply (frule isGlb_isLb) + apply (frule_tac x = y in isGlb_isLb) + apply (blast intro!: order_antisym dest!: isGlb_le_isLb) + done + +lemma bdd_above_setle: "bdd_above A \ (\a. A *<= a)" + by (auto simp: bdd_above_def setle_def) + +lemma bdd_below_setge: "bdd_below A \ (\a. a <=* A)" + by (auto simp: bdd_below_def setge_def) + +lemma isLub_cSup: + "(S::'a :: conditionally_complete_lattice set) \ {} \ (\b. S *<= b) \ isLub UNIV S (Sup S)" + by (auto simp add: isLub_def setle_def leastP_def isUb_def + intro!: setgeI cSup_upper cSup_least) + +lemma isGlb_cInf: + "(S::'a :: conditionally_complete_lattice set) \ {} \ (\b. b <=* S) \ isGlb UNIV S (Inf S)" + by (auto simp add: isGlb_def setge_def greatestP_def isLb_def + intro!: setleI cInf_lower cInf_greatest) + +lemma cSup_le: "(S::'a::conditionally_complete_lattice set) \ {} \ S *<= b \ Sup S \ b" + by (metis cSup_least setle_def) + +lemma cInf_ge: "(S::'a :: conditionally_complete_lattice set) \ {} \ b <=* S \ Inf S \ b" + by (metis cInf_greatest setge_def) + +lemma cSup_bounds: + fixes S :: "'a :: conditionally_complete_lattice set" + shows "S \ {} \ a <=* S \ S *<= b \ a \ Sup S \ Sup S \ b" + using cSup_least[of S b] cSup_upper2[of _ S a] + by (auto simp: bdd_above_setle setge_def setle_def) + +lemma cSup_unique: "(S::'a :: {conditionally_complete_linorder, no_bot} set) *<= b \ (\b'x\S. b' < x) \ Sup S = b" + by (rule cSup_eq) (auto simp: not_le[symmetric] setle_def) + +lemma cInf_unique: "b <=* (S::'a :: {conditionally_complete_linorder, no_top} set) \ (\b'>b. \x\S. b' > x) \ Inf S = b" + by (rule cInf_eq) (auto simp: not_le[symmetric] setge_def) + +text{* Use completeness of reals (supremum property) to show that any bounded sequence has a least upper bound*} + +lemma reals_complete: "\X. X \ S \ \Y. isUb (UNIV::real set) S Y \ \t. isLub (UNIV :: real set) S t" + by (intro exI[of _ "Sup S"] isLub_cSup) (auto simp: setle_def isUb_def intro!: cSup_upper) + +lemma Bseq_isUb: "\X :: nat \ real. Bseq X \ \U. isUb (UNIV::real set) {x. \n. X n = x} U" + by (auto intro: isUbI setleI simp add: Bseq_def abs_le_iff) + +lemma Bseq_isLub: "\X :: nat \ real. Bseq X \ \U. isLub (UNIV::real set) {x. \n. X n = x} U" + by (blast intro: reals_complete Bseq_isUb) + +lemma isLub_mono_imp_LIMSEQ: + fixes X :: "nat \ real" + assumes u: "isLub UNIV {x. \n. X n = x} u" (* FIXME: use 'range X' *) + assumes X: "\m n. m \ n \ X m \ X n" + shows "X ----> u" +proof - + have "X ----> (SUP i. X i)" + using u[THEN isLubD1] X + by (intro LIMSEQ_incseq_SUP) (auto simp: incseq_def image_def eq_commute bdd_above_setle) + also have "(SUP i. X i) = u" + using isLub_cSup[of "range X"] u[THEN isLubD1] + by (intro isLub_unique[OF _ u]) (auto simp add: SUP_def image_def eq_commute) + finally show ?thesis . +qed + +lemmas real_isGlb_unique = isGlb_unique[where 'a=real] + +lemma real_le_inf_subset: "t \ {} \ t \ s \ \b. b <=* s \ Inf s \ Inf (t::real set)" + by (rule cInf_superset_mono) (auto simp: bdd_below_setge) + +lemma real_ge_sup_subset: "t \ {} \ t \ s \ \b. s *<= b \ Sup s \ Sup (t::real set)" + by (rule cSup_subset_mono) (auto simp: bdd_above_setle) + +end diff -r 3c34490ccd4c -r 922a233805d2 src/HOL/Library/Lubs_Glbs.thy --- a/src/HOL/Library/Lubs_Glbs.thy Wed Oct 29 09:42:46 2014 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,245 +0,0 @@ -(* Title: HOL/Library/Lubs_Glbs.thy - Author: Jacques D. Fleuriot, University of Cambridge - Author: Amine Chaieb, University of Cambridge *) - -header {* Definitions of Least Upper Bounds and Greatest Lower Bounds *} - -theory Lubs_Glbs -imports Complex_Main -begin - -text {* Thanks to suggestions by James Margetson *} - -definition setle :: "'a set \ 'a::ord \ bool" (infixl "*<=" 70) - where "S *<= x = (ALL y: S. y \ x)" - -definition setge :: "'a::ord \ 'a set \ bool" (infixl "<=*" 70) - where "x <=* S = (ALL y: S. x \ y)" - - -subsection {* Rules for the Relations @{text "*<="} and @{text "<=*"} *} - -lemma setleI: "ALL y: S. y \ x \ S *<= x" - by (simp add: setle_def) - -lemma setleD: "S *<= x \ y: S \ y \ x" - by (simp add: setle_def) - -lemma setgeI: "ALL y: S. x \ y \ x <=* S" - by (simp add: setge_def) - -lemma setgeD: "x <=* S \ y: S \ x \ y" - by (simp add: setge_def) - - -definition leastP :: "('a \ bool) \ 'a::ord \ bool" - where "leastP P x = (P x \ x <=* Collect P)" - -definition isUb :: "'a set \ 'a set \ 'a::ord \ bool" - where "isUb R S x = (S *<= x \ x: R)" - -definition isLub :: "'a set \ 'a set \ 'a::ord \ bool" - where "isLub R S x = leastP (isUb R S) x" - -definition ubs :: "'a set \ 'a::ord set \ 'a set" - where "ubs R S = Collect (isUb R S)" - - -subsection {* Rules about the Operators @{term leastP}, @{term ub} and @{term lub} *} - -lemma leastPD1: "leastP P x \ P x" - by (simp add: leastP_def) - -lemma leastPD2: "leastP P x \ x <=* Collect P" - by (simp add: leastP_def) - -lemma leastPD3: "leastP P x \ y: Collect P \ x \ y" - by (blast dest!: leastPD2 setgeD) - -lemma isLubD1: "isLub R S x \ S *<= x" - by (simp add: isLub_def isUb_def leastP_def) - -lemma isLubD1a: "isLub R S x \ x: R" - by (simp add: isLub_def isUb_def leastP_def) - -lemma isLub_isUb: "isLub R S x \ isUb R S x" - unfolding isUb_def by (blast dest: isLubD1 isLubD1a) - -lemma isLubD2: "isLub R S x \ y : S \ y \ x" - by (blast dest!: isLubD1 setleD) - -lemma isLubD3: "isLub R S x \ leastP (isUb R S) x" - by (simp add: isLub_def) - -lemma isLubI1: "leastP(isUb R S) x \ isLub R S x" - by (simp add: isLub_def) - -lemma isLubI2: "isUb R S x \ x <=* Collect (isUb R S) \ isLub R S x" - by (simp add: isLub_def leastP_def) - -lemma isUbD: "isUb R S x \ y : S \ y \ x" - by (simp add: isUb_def setle_def) - -lemma isUbD2: "isUb R S x \ S *<= x" - by (simp add: isUb_def) - -lemma isUbD2a: "isUb R S x \ x: R" - by (simp add: isUb_def) - -lemma isUbI: "S *<= x \ x: R \ isUb R S x" - by (simp add: isUb_def) - -lemma isLub_le_isUb: "isLub R S x \ isUb R S y \ x \ y" - unfolding isLub_def by (blast intro!: leastPD3) - -lemma isLub_ubs: "isLub R S x \ x <=* ubs R S" - unfolding ubs_def isLub_def by (rule leastPD2) - -lemma isLub_unique: "[| isLub R S x; isLub R S y |] ==> x = (y::'a::linorder)" - apply (frule isLub_isUb) - apply (frule_tac x = y in isLub_isUb) - apply (blast intro!: order_antisym dest!: isLub_le_isUb) - done - -lemma isUb_UNIV_I: "(\y. y \ S \ y \ u) \ isUb UNIV S u" - by (simp add: isUbI setleI) - - -definition greatestP :: "('a \ bool) \ 'a::ord \ bool" - where "greatestP P x = (P x \ Collect P *<= x)" - -definition isLb :: "'a set \ 'a set \ 'a::ord \ bool" - where "isLb R S x = (x <=* S \ x: R)" - -definition isGlb :: "'a set \ 'a set \ 'a::ord \ bool" - where "isGlb R S x = greatestP (isLb R S) x" - -definition lbs :: "'a set \ 'a::ord set \ 'a set" - where "lbs R S = Collect (isLb R S)" - - -subsection {* Rules about the Operators @{term greatestP}, @{term isLb} and @{term isGlb} *} - -lemma greatestPD1: "greatestP P x \ P x" - by (simp add: greatestP_def) - -lemma greatestPD2: "greatestP P x \ Collect P *<= x" - by (simp add: greatestP_def) - -lemma greatestPD3: "greatestP P x \ y: Collect P \ x \ y" - by (blast dest!: greatestPD2 setleD) - -lemma isGlbD1: "isGlb R S x \ x <=* S" - by (simp add: isGlb_def isLb_def greatestP_def) - -lemma isGlbD1a: "isGlb R S x \ x: R" - by (simp add: isGlb_def isLb_def greatestP_def) - -lemma isGlb_isLb: "isGlb R S x \ isLb R S x" - unfolding isLb_def by (blast dest: isGlbD1 isGlbD1a) - -lemma isGlbD2: "isGlb R S x \ y : S \ y \ x" - by (blast dest!: isGlbD1 setgeD) - -lemma isGlbD3: "isGlb R S x \ greatestP (isLb R S) x" - by (simp add: isGlb_def) - -lemma isGlbI1: "greatestP (isLb R S) x \ isGlb R S x" - by (simp add: isGlb_def) - -lemma isGlbI2: "isLb R S x \ Collect (isLb R S) *<= x \ isGlb R S x" - by (simp add: isGlb_def greatestP_def) - -lemma isLbD: "isLb R S x \ y : S \ y \ x" - by (simp add: isLb_def setge_def) - -lemma isLbD2: "isLb R S x \ x <=* S " - by (simp add: isLb_def) - -lemma isLbD2a: "isLb R S x \ x: R" - by (simp add: isLb_def) - -lemma isLbI: "x <=* S \ x: R \ isLb R S x" - by (simp add: isLb_def) - -lemma isGlb_le_isLb: "isGlb R S x \ isLb R S y \ x \ y" - unfolding isGlb_def by (blast intro!: greatestPD3) - -lemma isGlb_ubs: "isGlb R S x \ lbs R S *<= x" - unfolding lbs_def isGlb_def by (rule greatestPD2) - -lemma isGlb_unique: "[| isGlb R S x; isGlb R S y |] ==> x = (y::'a::linorder)" - apply (frule isGlb_isLb) - apply (frule_tac x = y in isGlb_isLb) - apply (blast intro!: order_antisym dest!: isGlb_le_isLb) - done - -lemma bdd_above_setle: "bdd_above A \ (\a. A *<= a)" - by (auto simp: bdd_above_def setle_def) - -lemma bdd_below_setge: "bdd_below A \ (\a. a <=* A)" - by (auto simp: bdd_below_def setge_def) - -lemma isLub_cSup: - "(S::'a :: conditionally_complete_lattice set) \ {} \ (\b. S *<= b) \ isLub UNIV S (Sup S)" - by (auto simp add: isLub_def setle_def leastP_def isUb_def - intro!: setgeI cSup_upper cSup_least) - -lemma isGlb_cInf: - "(S::'a :: conditionally_complete_lattice set) \ {} \ (\b. b <=* S) \ isGlb UNIV S (Inf S)" - by (auto simp add: isGlb_def setge_def greatestP_def isLb_def - intro!: setleI cInf_lower cInf_greatest) - -lemma cSup_le: "(S::'a::conditionally_complete_lattice set) \ {} \ S *<= b \ Sup S \ b" - by (metis cSup_least setle_def) - -lemma cInf_ge: "(S::'a :: conditionally_complete_lattice set) \ {} \ b <=* S \ Inf S \ b" - by (metis cInf_greatest setge_def) - -lemma cSup_bounds: - fixes S :: "'a :: conditionally_complete_lattice set" - shows "S \ {} \ a <=* S \ S *<= b \ a \ Sup S \ Sup S \ b" - using cSup_least[of S b] cSup_upper2[of _ S a] - by (auto simp: bdd_above_setle setge_def setle_def) - -lemma cSup_unique: "(S::'a :: {conditionally_complete_linorder, no_bot} set) *<= b \ (\b'x\S. b' < x) \ Sup S = b" - by (rule cSup_eq) (auto simp: not_le[symmetric] setle_def) - -lemma cInf_unique: "b <=* (S::'a :: {conditionally_complete_linorder, no_top} set) \ (\b'>b. \x\S. b' > x) \ Inf S = b" - by (rule cInf_eq) (auto simp: not_le[symmetric] setge_def) - -text{* Use completeness of reals (supremum property) to show that any bounded sequence has a least upper bound*} - -lemma reals_complete: "\X. X \ S \ \Y. isUb (UNIV::real set) S Y \ \t. isLub (UNIV :: real set) S t" - by (intro exI[of _ "Sup S"] isLub_cSup) (auto simp: setle_def isUb_def intro!: cSup_upper) - -lemma Bseq_isUb: "\X :: nat \ real. Bseq X \ \U. isUb (UNIV::real set) {x. \n. X n = x} U" - by (auto intro: isUbI setleI simp add: Bseq_def abs_le_iff) - -lemma Bseq_isLub: "\X :: nat \ real. Bseq X \ \U. isLub (UNIV::real set) {x. \n. X n = x} U" - by (blast intro: reals_complete Bseq_isUb) - -lemma isLub_mono_imp_LIMSEQ: - fixes X :: "nat \ real" - assumes u: "isLub UNIV {x. \n. X n = x} u" (* FIXME: use 'range X' *) - assumes X: "\m n. m \ n \ X m \ X n" - shows "X ----> u" -proof - - have "X ----> (SUP i. X i)" - using u[THEN isLubD1] X - by (intro LIMSEQ_incseq_SUP) (auto simp: incseq_def image_def eq_commute bdd_above_setle) - also have "(SUP i. X i) = u" - using isLub_cSup[of "range X"] u[THEN isLubD1] - by (intro isLub_unique[OF _ u]) (auto simp add: SUP_def image_def eq_commute) - finally show ?thesis . -qed - -lemmas real_isGlb_unique = isGlb_unique[where 'a=real] - -lemma real_le_inf_subset: "t \ {} \ t \ s \ \b. b <=* s \ Inf s \ Inf (t::real set)" - by (rule cInf_superset_mono) (auto simp: bdd_below_setge) - -lemma real_ge_sup_subset: "t \ {} \ t \ s \ \b. s *<= b \ Sup s \ Sup (t::real set)" - by (rule cSup_subset_mono) (auto simp: bdd_above_setle) - -end diff -r 3c34490ccd4c -r 922a233805d2 src/HOL/NSA/NSA.thy --- a/src/HOL/NSA/NSA.thy Wed Oct 29 09:42:46 2014 +0100 +++ b/src/HOL/NSA/NSA.thy Wed Oct 29 10:35:00 2014 +0100 @@ -6,7 +6,7 @@ header{*Infinite Numbers, Infinitesimals, Infinitely Close Relation*} theory NSA -imports HyperDef "~~/src/HOL/Library/Lubs_Glbs" +imports HyperDef "~~/src/HOL/Library/Lub_Glb" begin definition