src/HOL/Library/Glbs.thy
changeset 46509 c4b2ec379fdd
parent 30661 54858c8ad226
child 51342 763c6872bd10
     1.1 --- a/src/HOL/Library/Glbs.thy	Thu Feb 16 22:53:56 2012 +0100
     1.2 +++ b/src/HOL/Library/Glbs.thy	Thu Feb 16 22:54:40 2012 +0100
     1.3 @@ -6,77 +6,68 @@
     1.4  imports Lubs
     1.5  begin
     1.6  
     1.7 -definition
     1.8 -  greatestP      :: "['a =>bool,'a::ord] => bool" where
     1.9 -  "greatestP P x = (P x & Collect P *<=  x)"
    1.10 +definition greatestP :: "('a \<Rightarrow> bool) \<Rightarrow> 'a::ord \<Rightarrow> bool"
    1.11 +  where "greatestP P x = (P x \<and> Collect P *<=  x)"
    1.12  
    1.13 -definition
    1.14 -  isLb        :: "['a set, 'a set, 'a::ord] => bool" where
    1.15 -  "isLb R S x = (x <=* S & x: R)"
    1.16 +definition isLb :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool"
    1.17 +  where "isLb R S x = (x <=* S \<and> x: R)"
    1.18  
    1.19 -definition
    1.20 -  isGlb       :: "['a set, 'a set, 'a::ord] => bool" where
    1.21 -  "isGlb R S x = greatestP (isLb R S) x"
    1.22 +definition isGlb :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool"
    1.23 +  where "isGlb R S x = greatestP (isLb R S) x"
    1.24  
    1.25 -definition
    1.26 -  lbs         :: "['a set, 'a::ord set] => 'a set" where
    1.27 -  "lbs R S = Collect (isLb R S)"
    1.28 +definition lbs :: "'a set \<Rightarrow> 'a::ord set \<Rightarrow> 'a set"
    1.29 +  where "lbs R S = Collect (isLb R S)"
    1.30 +
    1.31  
    1.32 -subsection{*Rules about the Operators @{term greatestP}, @{term isLb}
    1.33 -    and @{term isGlb}*}
    1.34 +subsection {* Rules about the Operators @{term greatestP}, @{term isLb}
    1.35 +  and @{term isGlb} *}
    1.36  
    1.37 -lemma leastPD1: "greatestP P x ==> P x"
    1.38 -by (simp add: greatestP_def)
    1.39 +lemma leastPD1: "greatestP P x \<Longrightarrow> P x"
    1.40 +  by (simp add: greatestP_def)
    1.41  
    1.42 -lemma greatestPD2: "greatestP P x ==> Collect P *<= x"
    1.43 -by (simp add: greatestP_def)
    1.44 +lemma greatestPD2: "greatestP P x \<Longrightarrow> Collect P *<= x"
    1.45 +  by (simp add: greatestP_def)
    1.46  
    1.47 -lemma greatestPD3: "[| greatestP P x; y: Collect P |] ==> x >= y"
    1.48 -by (blast dest!: greatestPD2 setleD)
    1.49 +lemma greatestPD3: "greatestP P x \<Longrightarrow> y: Collect P \<Longrightarrow> x \<ge> y"
    1.50 +  by (blast dest!: greatestPD2 setleD)
    1.51  
    1.52 -lemma isGlbD1: "isGlb R S x ==> x <=* S"
    1.53 -by (simp add: isGlb_def isLb_def greatestP_def)
    1.54 +lemma isGlbD1: "isGlb R S x \<Longrightarrow> x <=* S"
    1.55 +  by (simp add: isGlb_def isLb_def greatestP_def)
    1.56  
    1.57 -lemma isGlbD1a: "isGlb R S x ==> x: R"
    1.58 -by (simp add: isGlb_def isLb_def greatestP_def)
    1.59 +lemma isGlbD1a: "isGlb R S x \<Longrightarrow> x: R"
    1.60 +  by (simp add: isGlb_def isLb_def greatestP_def)
    1.61  
    1.62 -lemma isGlb_isLb: "isGlb R S x ==> isLb R S x"
    1.63 -apply (simp add: isLb_def)
    1.64 -apply (blast dest: isGlbD1 isGlbD1a)
    1.65 -done
    1.66 +lemma isGlb_isLb: "isGlb R S x \<Longrightarrow> isLb R S x"
    1.67 +  unfolding isLb_def by (blast dest: isGlbD1 isGlbD1a)
    1.68  
    1.69 -lemma isGlbD2: "[| isGlb R S x; y : S |] ==> y >= x"
    1.70 -by (blast dest!: isGlbD1 setgeD)
    1.71 +lemma isGlbD2: "isGlb R S x \<Longrightarrow> y : S \<Longrightarrow> y \<ge> x"
    1.72 +  by (blast dest!: isGlbD1 setgeD)
    1.73  
    1.74 -lemma isGlbD3: "isGlb R S x ==> greatestP(isLb R S) x"
    1.75 -by (simp add: isGlb_def)
    1.76 +lemma isGlbD3: "isGlb R S x \<Longrightarrow> greatestP (isLb R S) x"
    1.77 +  by (simp add: isGlb_def)
    1.78  
    1.79 -lemma isGlbI1: "greatestP(isLb R S) x ==> isGlb R S x"
    1.80 -by (simp add: isGlb_def)
    1.81 +lemma isGlbI1: "greatestP (isLb R S) x \<Longrightarrow> isGlb R S x"
    1.82 +  by (simp add: isGlb_def)
    1.83  
    1.84 -lemma isGlbI2: "[| isLb R S x; Collect (isLb R S) *<= x |] ==> isGlb R S x"
    1.85 -by (simp add: isGlb_def greatestP_def)
    1.86 +lemma isGlbI2: "isLb R S x \<Longrightarrow> Collect (isLb R S) *<= x \<Longrightarrow> isGlb R S x"
    1.87 +  by (simp add: isGlb_def greatestP_def)
    1.88  
    1.89 -lemma isLbD: "[| isLb R S x; y : S |] ==> y >= x"
    1.90 -by (simp add: isLb_def setge_def)
    1.91 +lemma isLbD: "isLb R S x \<Longrightarrow> y : S \<Longrightarrow> y \<ge> x"
    1.92 +  by (simp add: isLb_def setge_def)
    1.93  
    1.94 -lemma isLbD2: "isLb R S x ==> x <=* S "
    1.95 -by (simp add: isLb_def)
    1.96 +lemma isLbD2: "isLb R S x \<Longrightarrow> x <=* S "
    1.97 +  by (simp add: isLb_def)
    1.98  
    1.99 -lemma isLbD2a: "isLb R S x ==> x: R"
   1.100 -by (simp add: isLb_def)
   1.101 +lemma isLbD2a: "isLb R S x \<Longrightarrow> x: R"
   1.102 +  by (simp add: isLb_def)
   1.103  
   1.104 -lemma isLbI: "[| x <=* S ; x: R |] ==> isLb R S x"
   1.105 -by (simp add: isLb_def)
   1.106 +lemma isLbI: "x <=* S \<Longrightarrow> x: R \<Longrightarrow> isLb R S x"
   1.107 +  by (simp add: isLb_def)
   1.108  
   1.109 -lemma isGlb_le_isLb: "[| isGlb R S x; isLb R S y |] ==> x >= y"
   1.110 -apply (simp add: isGlb_def)
   1.111 -apply (blast intro!: greatestPD3)
   1.112 -done
   1.113 +lemma isGlb_le_isLb: "isGlb R S x \<Longrightarrow> isLb R S y \<Longrightarrow> x \<ge> y"
   1.114 +  unfolding isGlb_def by (blast intro!: greatestPD3)
   1.115  
   1.116 -lemma isGlb_ubs: "isGlb R S x ==> lbs R S *<= x"
   1.117 -apply (simp add: lbs_def isGlb_def)
   1.118 -apply (erule greatestPD2)
   1.119 -done
   1.120 +lemma isGlb_ubs: "isGlb R S x \<Longrightarrow> lbs R S *<= x"
   1.121 +  unfolding lbs_def isGlb_def by (rule greatestPD2)
   1.122  
   1.123  end