# HG changeset patch
# User wenzelm
# Date 1329429280 -3600
# Node ID c4b2ec379fdd448b5f91eb7ff156075094b6b5fd
# Parent  ec9630fe9ca77a30aa069fe939d9029a4245107f
more symbols;
misc tuning;

diff -r ec9630fe9ca7 -r c4b2ec379fdd src/HOL/Library/Glbs.thy
--- a/src/HOL/Library/Glbs.thy	Thu Feb 16 22:53:56 2012 +0100
+++ b/src/HOL/Library/Glbs.thy	Thu Feb 16 22:54:40 2012 +0100
@@ -6,77 +6,68 @@
 imports Lubs
 begin
 
-definition
-  greatestP      :: "['a =>bool,'a::ord] => bool" where
-  "greatestP P x = (P x & Collect P *<=  x)"
+definition greatestP :: "('a \<Rightarrow> bool) \<Rightarrow> 'a::ord \<Rightarrow> bool"
+  where "greatestP P x = (P x \<and> Collect P *<=  x)"
 
-definition
-  isLb        :: "['a set, 'a set, 'a::ord] => bool" where
-  "isLb R S x = (x <=* S & x: R)"
+definition isLb :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool"
+  where "isLb R S x = (x <=* S \<and> x: R)"
 
-definition
-  isGlb       :: "['a set, 'a set, 'a::ord] => bool" where
-  "isGlb R S x = greatestP (isLb R S) x"
+definition isGlb :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> 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)"
+definition lbs :: "'a set \<Rightarrow> 'a::ord set \<Rightarrow> 'a set"
+  where "lbs R S = Collect (isLb R S)"
+
 
-subsection{*Rules about the Operators @{term greatestP}, @{term isLb}
-    and @{term isGlb}*}
+subsection {* Rules about the Operators @{term greatestP}, @{term isLb}
+  and @{term isGlb} *}
 
-lemma leastPD1: "greatestP P x ==> P x"
-by (simp add: greatestP_def)
+lemma leastPD1: "greatestP P x \<Longrightarrow> P x"
+  by (simp add: greatestP_def)
 
-lemma greatestPD2: "greatestP P x ==> Collect P *<= x"
-by (simp add: greatestP_def)
+lemma greatestPD2: "greatestP P x \<Longrightarrow> Collect P *<= x"
+  by (simp add: greatestP_def)
 
-lemma greatestPD3: "[| greatestP P x; y: Collect P |] ==> x >= y"
-by (blast dest!: greatestPD2 setleD)
+lemma greatestPD3: "greatestP P x \<Longrightarrow> y: Collect P \<Longrightarrow> x \<ge> y"
+  by (blast dest!: greatestPD2 setleD)
 
-lemma isGlbD1: "isGlb R S x ==> x <=* S"
-by (simp add: isGlb_def isLb_def greatestP_def)
+lemma isGlbD1: "isGlb R S x \<Longrightarrow> 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 isGlbD1a: "isGlb R S x \<Longrightarrow> x: R"
+  by (simp add: isGlb_def isLb_def greatestP_def)
 
-lemma isGlb_isLb: "isGlb R S x ==> isLb R S x"
-apply (simp add: isLb_def)
-apply (blast dest: isGlbD1 isGlbD1a)
-done
+lemma isGlb_isLb: "isGlb R S x \<Longrightarrow> 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 isGlbD2: "isGlb R S x \<Longrightarrow> y : S \<Longrightarrow> y \<ge> x"
+  by (blast dest!: isGlbD1 setgeD)
 
-lemma isGlbD3: "isGlb R S x ==> greatestP(isLb R S) x"
-by (simp add: isGlb_def)
+lemma isGlbD3: "isGlb R S x \<Longrightarrow> 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 isGlbI1: "greatestP (isLb R S) x \<Longrightarrow> 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 isGlbI2: "isLb R S x \<Longrightarrow> Collect (isLb R S) *<= x \<Longrightarrow> 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 isLbD: "isLb R S x \<Longrightarrow> y : S \<Longrightarrow> y \<ge> x"
+  by (simp add: isLb_def setge_def)
 
-lemma isLbD2: "isLb R S x ==> x <=* S "
-by (simp add: isLb_def)
+lemma isLbD2: "isLb R S x \<Longrightarrow> x <=* S "
+  by (simp add: isLb_def)
 
-lemma isLbD2a: "isLb R S x ==> x: R"
-by (simp add: isLb_def)
+lemma isLbD2a: "isLb R S x \<Longrightarrow> x: R"
+  by (simp add: isLb_def)
 
-lemma isLbI: "[| x <=* S ; x: R |] ==> isLb R S x"
-by (simp add: isLb_def)
+lemma isLbI: "x <=* S \<Longrightarrow> x: R \<Longrightarrow> isLb R S x"
+  by (simp add: isLb_def)
 
-lemma isGlb_le_isLb: "[| isGlb R S x; isLb R S y |] ==> x >= y"
-apply (simp add: isGlb_def)
-apply (blast intro!: greatestPD3)
-done
+lemma isGlb_le_isLb: "isGlb R S x \<Longrightarrow> isLb R S y \<Longrightarrow> x \<ge> y"
+  unfolding isGlb_def by (blast intro!: greatestPD3)
 
-lemma isGlb_ubs: "isGlb R S x ==> lbs R S *<= x"
-apply (simp add: lbs_def isGlb_def)
-apply (erule greatestPD2)
-done
+lemma isGlb_ubs: "isGlb R S x \<Longrightarrow> lbs R S *<= x"
+  unfolding lbs_def isGlb_def by (rule greatestPD2)
 
 end
diff -r ec9630fe9ca7 -r c4b2ec379fdd src/HOL/Lubs.thy
--- a/src/HOL/Lubs.thy	Thu Feb 16 22:53:56 2012 +0100
+++ b/src/HOL/Lubs.thy	Thu Feb 16 22:54:40 2012 +0100
@@ -1,112 +1,97 @@
-(*  Title       : Lubs.thy
-    Author      : Jacques D. Fleuriot
-    Copyright   : 1998  University of Cambridge
+(*  Title:      HOL/Lubs.thy
+    Author:     Jacques D. Fleuriot, University of Cambridge
 *)
 
-header{*Definitions of Upper Bounds and Least Upper Bounds*}
+header {* Definitions of Upper Bounds and Least Upper Bounds *}
 
 theory Lubs
 imports Main
 begin
 
-text{*Thanks to suggestions by James Margetson*}
+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 setle :: "'a set \<Rightarrow> 'a::ord \<Rightarrow> bool"  (infixl "*<=" 70)
+  where "S *<= x = (ALL y: S. y \<le> x)"
 
-definition
-  setge :: "['a::ord, 'a set] => bool"  (infixl "<=*" 70) where
-  "x <=* S = (ALL y: S. x <= y)"
+definition setge :: "'a::ord \<Rightarrow> 'a set \<Rightarrow> bool"  (infixl "<=*" 70)
+  where "x <=* S = (ALL y: S. x \<le> y)"
 
-definition
-  leastP      :: "['a =>bool,'a::ord] => bool" where
-  "leastP P x = (P x & x <=* Collect P)"
+definition leastP :: "('a \<Rightarrow> bool) \<Rightarrow> 'a::ord \<Rightarrow> bool"
+  where "leastP P x = (P x \<and> x <=* Collect P)"
 
-definition
-  isUb        :: "['a set, 'a set, 'a::ord] => bool" where
-  "isUb R S x = (S *<= x & x: R)"
+definition isUb :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool"
+  where "isUb R S x = (S *<= x \<and> x: R)"
 
-definition
-  isLub       :: "['a set, 'a set, 'a::ord] => bool" where
-  "isLub R S x = leastP (isUb R S) x"
+definition isLub :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> 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)"
+definition ubs :: "'a set \<Rightarrow> 'a::ord set \<Rightarrow> 'a set"
+  where "ubs R S = Collect (isUb R S)"
 
 
-
-subsection{*Rules for the Relations @{text "*<="} and @{text "<=*"}*}
+subsection {* Rules for the Relations @{text "*<="} and @{text "<=*"} *}
 
-lemma setleI: "ALL y: S. y <= x ==> S *<= x"
-by (simp add: setle_def)
+lemma setleI: "ALL y: S. y \<le> x \<Longrightarrow> S *<= x"
+  by (simp add: setle_def)
 
-lemma setleD: "[| S *<= x; y: S |] ==> y <= x"
-by (simp add: setle_def)
+lemma setleD: "S *<= x \<Longrightarrow> y: S \<Longrightarrow> y \<le> x"
+  by (simp add: setle_def)
 
-lemma setgeI: "ALL y: S. x<= y ==> x <=* S"
-by (simp add: setge_def)
+lemma setgeI: "ALL y: S. x \<le> y \<Longrightarrow> x <=* S"
+  by (simp add: setge_def)
 
-lemma setgeD: "[| x <=* S; y: S |] ==> x <= y"
-by (simp add: setge_def)
+lemma setgeD: "x <=* S \<Longrightarrow> y: S \<Longrightarrow> x \<le> y"
+  by (simp add: setge_def)
 
 
-subsection{*Rules about the Operators @{term leastP}, @{term ub}
-    and @{term lub}*}
+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 leastPD1: "leastP P x \<Longrightarrow> P x"
+  by (simp add: leastP_def)
 
-lemma leastPD2: "leastP P x ==> x <=* Collect P"
-by (simp add: leastP_def)
+lemma leastPD2: "leastP P x \<Longrightarrow> x <=* Collect P"
+  by (simp add: leastP_def)
 
-lemma leastPD3: "[| leastP P x; y: Collect P |] ==> x <= y"
-by (blast dest!: leastPD2 setgeD)
+lemma leastPD3: "leastP P x \<Longrightarrow> y: Collect P \<Longrightarrow> x \<le> y"
+  by (blast dest!: leastPD2 setgeD)
 
-lemma isLubD1: "isLub R S x ==> S *<= x"
-by (simp add: isLub_def isUb_def leastP_def)
+lemma isLubD1: "isLub R S x \<Longrightarrow> 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 isLubD1a: "isLub R S x \<Longrightarrow> x: R"
+  by (simp add: isLub_def isUb_def leastP_def)
 
-lemma isLub_isUb: "isLub R S x ==> isUb R S x"
-apply (simp add: isUb_def)
-apply (blast dest: isLubD1 isLubD1a)
-done
+lemma isLub_isUb: "isLub R S x \<Longrightarrow> 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 isLubD2: "isLub R S x \<Longrightarrow> y : S \<Longrightarrow> y \<le> x"
+  by (blast dest!: isLubD1 setleD)
 
-lemma isLubD3: "isLub R S x ==> leastP(isUb R S) x"
-by (simp add: isLub_def)
+lemma isLubD3: "isLub R S x \<Longrightarrow> 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 isLubI1: "leastP(isUb R S) x \<Longrightarrow> 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 isLubI2: "isUb R S x \<Longrightarrow> x <=* Collect (isUb R S) \<Longrightarrow> 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 isUbD: "isUb R S x \<Longrightarrow> y : S \<Longrightarrow> y \<le> x"
+  by (simp add: isUb_def setle_def)
 
-lemma isUbD2a: "isUb R S x ==> x: R"
-by (simp add: isUb_def)
+lemma isUbD2: "isUb R S x \<Longrightarrow> S *<= x"
+  by (simp add: isUb_def)
 
-lemma isUbI: "[| S *<= x; x: R |] ==> isUb R S x"
-by (simp add: isUb_def)
+lemma isUbD2a: "isUb R S x \<Longrightarrow> x: R"
+  by (simp add: isUb_def)
 
-lemma isLub_le_isUb: "[| isLub R S x; isUb R S y |] ==> x <= y"
-apply (simp add: isLub_def)
-apply (blast intro!: leastPD3)
-done
+lemma isUbI: "S *<= x \<Longrightarrow> x: R \<Longrightarrow> isUb R S x"
+  by (simp add: isUb_def)
 
-lemma isLub_ubs: "isLub R S x ==> x <=* ubs R S"
-apply (simp add: ubs_def isLub_def)
-apply (erule leastPD2)
-done
+lemma isLub_le_isUb: "isLub R S x \<Longrightarrow> isUb R S y \<Longrightarrow> x \<le> y"
+  unfolding isLub_def by (blast intro!: leastPD3)
+
+lemma isLub_ubs: "isLub R S x \<Longrightarrow> x <=* ubs R S"
+  unfolding ubs_def isLub_def by (rule leastPD2)
 
 end