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.63 -by (simp add: setle_def)
    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.68 -by (simp add: setle_def)
    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.73 -by (simp add: setge_def)
    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.78 -by (simp add: setge_def)
    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.88 -by (simp add: leastP_def)
    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.93 -by (simp add: leastP_def)
    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.113 -apply (simp add: isUb_def)
   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.125 -by (simp add: isLub_def)
   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.130 -by (simp add: isLub_def)
   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.143 -by (simp add: isUb_def)
   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.148 -by (simp add: isUb_def)
   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.153 -by (simp add: isUb_def)
   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.158 -apply (simp add: isLub_def)
   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