src/HOL/Lubs.thy
 changeset 46509 c4b2ec379fdd parent 30738 0842e906300c child 51520 e9b361845809
```     1.1 --- a/src/HOL/Lubs.thy	Thu Feb 16 22:53:56 2012 +0100
1.2 +++ b/src/HOL/Lubs.thy	Thu Feb 16 22:54:40 2012 +0100
1.3 @@ -1,112 +1,97 @@
1.4 -(*  Title       : Lubs.thy
1.5 -    Author      : Jacques D. Fleuriot
1.6 -    Copyright   : 1998  University of Cambridge
1.7 +(*  Title:      HOL/Lubs.thy
1.8 +    Author:     Jacques D. Fleuriot, University of Cambridge
1.9  *)
1.10
1.11 -header{*Definitions of Upper Bounds and Least Upper Bounds*}
1.12 +header {* Definitions of Upper Bounds and Least Upper Bounds *}
1.13
1.14  theory Lubs
1.15  imports Main
1.16  begin
1.17
1.18 -text{*Thanks to suggestions by James Margetson*}
1.19 +text {* Thanks to suggestions by James Margetson *}
1.20
1.21 -definition
1.22 -  setle :: "['a set, 'a::ord] => bool"  (infixl "*<=" 70) where
1.23 -  "S *<= x = (ALL y: S. y <= x)"
1.24 +definition setle :: "'a set \<Rightarrow> 'a::ord \<Rightarrow> bool"  (infixl "*<=" 70)
1.25 +  where "S *<= x = (ALL y: S. y \<le> x)"
1.26
1.27 -definition
1.28 -  setge :: "['a::ord, 'a set] => bool"  (infixl "<=*" 70) where
1.29 -  "x <=* S = (ALL y: S. x <= y)"
1.30 +definition setge :: "'a::ord \<Rightarrow> 'a set \<Rightarrow> bool"  (infixl "<=*" 70)
1.31 +  where "x <=* S = (ALL y: S. x \<le> y)"
1.32
1.33 -definition
1.34 -  leastP      :: "['a =>bool,'a::ord] => bool" where
1.35 -  "leastP P x = (P x & x <=* Collect P)"
1.36 +definition leastP :: "('a \<Rightarrow> bool) \<Rightarrow> 'a::ord \<Rightarrow> bool"
1.37 +  where "leastP P x = (P x \<and> x <=* Collect P)"
1.38
1.39 -definition
1.40 -  isUb        :: "['a set, 'a set, 'a::ord] => bool" where
1.41 -  "isUb R S x = (S *<= x & x: R)"
1.42 +definition isUb :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool"
1.43 +  where "isUb R S x = (S *<= x \<and> x: R)"
1.44
1.45 -definition
1.46 -  isLub       :: "['a set, 'a set, 'a::ord] => bool" where
1.47 -  "isLub R S x = leastP (isUb R S) x"
1.48 +definition isLub :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool"
1.49 +  where "isLub R S x = leastP (isUb R S) x"
1.50
1.51 -definition
1.52 -  ubs         :: "['a set, 'a::ord set] => 'a set" where
1.53 -  "ubs R S = Collect (isUb R S)"
1.54 +definition ubs :: "'a set \<Rightarrow> 'a::ord set \<Rightarrow> 'a set"
1.55 +  where "ubs R S = Collect (isUb R S)"
1.56
1.57
1.58 -
1.59 -subsection{*Rules for the Relations @{text "*<="} and @{text "<=*"}*}
1.60 +subsection {* Rules for the Relations @{text "*<="} and @{text "<=*"} *}
1.61
1.62 -lemma setleI: "ALL y: S. y <= x ==> S *<= x"
1.64 +lemma setleI: "ALL y: S. y \<le> x \<Longrightarrow> S *<= x"
1.65 +  by (simp add: setle_def)
1.66
1.67 -lemma setleD: "[| S *<= x; y: S |] ==> y <= x"
1.69 +lemma setleD: "S *<= x \<Longrightarrow> y: S \<Longrightarrow> y \<le> x"
1.70 +  by (simp add: setle_def)
1.71
1.72 -lemma setgeI: "ALL y: S. x<= y ==> x <=* S"
1.74 +lemma setgeI: "ALL y: S. x \<le> y \<Longrightarrow> x <=* S"
1.75 +  by (simp add: setge_def)
1.76
1.77 -lemma setgeD: "[| x <=* S; y: S |] ==> x <= y"
1.79 +lemma setgeD: "x <=* S \<Longrightarrow> y: S \<Longrightarrow> x \<le> y"
1.80 +  by (simp add: setge_def)
1.81
1.82
1.83 -subsection{*Rules about the Operators @{term leastP}, @{term ub}
1.84 -    and @{term lub}*}
1.85 +subsection {* Rules about the Operators @{term leastP}, @{term ub} and @{term lub} *}
1.86
1.87 -lemma leastPD1: "leastP P x ==> P x"
1.89 +lemma leastPD1: "leastP P x \<Longrightarrow> P x"
1.90 +  by (simp add: leastP_def)
1.91
1.92 -lemma leastPD2: "leastP P x ==> x <=* Collect P"
1.94 +lemma leastPD2: "leastP P x \<Longrightarrow> x <=* Collect P"
1.95 +  by (simp add: leastP_def)
1.96
1.97 -lemma leastPD3: "[| leastP P x; y: Collect P |] ==> x <= y"
1.98 -by (blast dest!: leastPD2 setgeD)
1.99 +lemma leastPD3: "leastP P x \<Longrightarrow> y: Collect P \<Longrightarrow> x \<le> y"
1.100 +  by (blast dest!: leastPD2 setgeD)
1.101
1.102 -lemma isLubD1: "isLub R S x ==> S *<= x"
1.103 -by (simp add: isLub_def isUb_def leastP_def)
1.104 +lemma isLubD1: "isLub R S x \<Longrightarrow> S *<= x"
1.105 +  by (simp add: isLub_def isUb_def leastP_def)
1.106
1.107 -lemma isLubD1a: "isLub R S x ==> x: R"
1.108 -by (simp add: isLub_def isUb_def leastP_def)
1.109 +lemma isLubD1a: "isLub R S x \<Longrightarrow> x: R"
1.110 +  by (simp add: isLub_def isUb_def leastP_def)
1.111
1.112 -lemma isLub_isUb: "isLub R S x ==> isUb R S x"
1.114 -apply (blast dest: isLubD1 isLubD1a)
1.115 -done
1.116 +lemma isLub_isUb: "isLub R S x \<Longrightarrow> isUb R S x"
1.117 +  unfolding isUb_def by (blast dest: isLubD1 isLubD1a)
1.118
1.119 -lemma isLubD2: "[| isLub R S x; y : S |] ==> y <= x"
1.120 -by (blast dest!: isLubD1 setleD)
1.121 +lemma isLubD2: "isLub R S x \<Longrightarrow> y : S \<Longrightarrow> y \<le> x"
1.122 +  by (blast dest!: isLubD1 setleD)
1.123
1.124 -lemma isLubD3: "isLub R S x ==> leastP(isUb R S) x"
1.126 +lemma isLubD3: "isLub R S x \<Longrightarrow> leastP (isUb R S) x"
1.127 +  by (simp add: isLub_def)
1.128
1.129 -lemma isLubI1: "leastP(isUb R S) x ==> isLub R S x"
1.131 +lemma isLubI1: "leastP(isUb R S) x \<Longrightarrow> isLub R S x"
1.132 +  by (simp add: isLub_def)
1.133
1.134 -lemma isLubI2: "[| isUb R S x; x <=* Collect (isUb R S) |] ==> isLub R S x"
1.135 -by (simp add: isLub_def leastP_def)
1.136 +lemma isLubI2: "isUb R S x \<Longrightarrow> x <=* Collect (isUb R S) \<Longrightarrow> isLub R S x"
1.137 +  by (simp add: isLub_def leastP_def)
1.138
1.139 -lemma isUbD: "[| isUb R S x; y : S |] ==> y <= x"
1.140 -by (simp add: isUb_def setle_def)
1.141 -
1.142 -lemma isUbD2: "isUb R S x ==> S *<= x"
1.144 +lemma isUbD: "isUb R S x \<Longrightarrow> y : S \<Longrightarrow> y \<le> x"
1.145 +  by (simp add: isUb_def setle_def)
1.146
1.147 -lemma isUbD2a: "isUb R S x ==> x: R"
1.149 +lemma isUbD2: "isUb R S x \<Longrightarrow> S *<= x"
1.150 +  by (simp add: isUb_def)
1.151
1.152 -lemma isUbI: "[| S *<= x; x: R |] ==> isUb R S x"
1.154 +lemma isUbD2a: "isUb R S x \<Longrightarrow> x: R"
1.155 +  by (simp add: isUb_def)
1.156
1.157 -lemma isLub_le_isUb: "[| isLub R S x; isUb R S y |] ==> x <= y"
1.159 -apply (blast intro!: leastPD3)
1.160 -done
1.161 +lemma isUbI: "S *<= x \<Longrightarrow> x: R \<Longrightarrow> isUb R S x"
1.162 +  by (simp add: isUb_def)
1.163
1.164 -lemma isLub_ubs: "isLub R S x ==> x <=* ubs R S"
1.165 -apply (simp add: ubs_def isLub_def)
1.166 -apply (erule leastPD2)
1.167 -done
1.168 +lemma isLub_le_isUb: "isLub R S x \<Longrightarrow> isUb R S y \<Longrightarrow> x \<le> y"
1.169 +  unfolding isLub_def by (blast intro!: leastPD3)
1.170 +
1.171 +lemma isLub_ubs: "isLub R S x \<Longrightarrow> x <=* ubs R S"
1.172 +  unfolding ubs_def isLub_def by (rule leastPD2)
1.173
1.174  end
```