1.1 --- a/src/HOL/Lubs.thy	Thu Dec 05 17:52:12 2013 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,103 +0,0 @@
     1.4 -(*  Title:      HOL/Lubs.thy
     1.5 -    Author:     Jacques D. Fleuriot, University of Cambridge
     1.6 -*)
     1.7 -
     1.8 -header {* Definitions of Upper Bounds and Least Upper Bounds *}
     1.9 -
    1.10 -theory Lubs
    1.11 -imports Main
    1.12 -begin
    1.13 -
    1.14 -text {* Thanks to suggestions by James Margetson *}
    1.15 -
    1.16 -definition setle :: "'a set \<Rightarrow> 'a::ord \<Rightarrow> bool"  (infixl "*<=" 70)
    1.17 -  where "S *<= x = (ALL y: S. y \<le> x)"
    1.18 -
    1.19 -definition setge :: "'a::ord \<Rightarrow> 'a set \<Rightarrow> bool"  (infixl "<=*" 70)
    1.20 -  where "x <=* S = (ALL y: S. x \<le> y)"
    1.21 -
    1.22 -definition leastP :: "('a \<Rightarrow> bool) \<Rightarrow> 'a::ord \<Rightarrow> bool"
    1.23 -  where "leastP P x = (P x \<and> x <=* Collect P)"
    1.24 -
    1.25 -definition isUb :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool"
    1.26 -  where "isUb R S x = (S *<= x \<and> x: R)"
    1.27 -
    1.28 -definition isLub :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool"
    1.29 -  where "isLub R S x = leastP (isUb R S) x"
    1.30 -
    1.31 -definition ubs :: "'a set \<Rightarrow> 'a::ord set \<Rightarrow> 'a set"
    1.32 -  where "ubs R S = Collect (isUb R S)"
    1.33 -
    1.34 -
    1.35 -subsection {* Rules for the Relations @{text "*<="} and @{text "<=*"} *}
    1.36 -
    1.37 -lemma setleI: "ALL y: S. y \<le> x \<Longrightarrow> S *<= x"
    1.38 -  by (simp add: setle_def)
    1.39 -
    1.40 -lemma setleD: "S *<= x \<Longrightarrow> y: S \<Longrightarrow> y \<le> x"
    1.41 -  by (simp add: setle_def)
    1.42 -
    1.43 -lemma setgeI: "ALL y: S. x \<le> y \<Longrightarrow> x <=* S"
    1.44 -  by (simp add: setge_def)
    1.45 -
    1.46 -lemma setgeD: "x <=* S \<Longrightarrow> y: S \<Longrightarrow> x \<le> y"
    1.47 -  by (simp add: setge_def)
    1.48 -
    1.49 -
    1.50 -subsection {* Rules about the Operators @{term leastP}, @{term ub} and @{term lub} *}
    1.51 -
    1.52 -lemma leastPD1: "leastP P x \<Longrightarrow> P x"
    1.53 -  by (simp add: leastP_def)
    1.54 -
    1.55 -lemma leastPD2: "leastP P x \<Longrightarrow> x <=* Collect P"
    1.56 -  by (simp add: leastP_def)
    1.57 -
    1.58 -lemma leastPD3: "leastP P x \<Longrightarrow> y: Collect P \<Longrightarrow> x \<le> y"
    1.59 -  by (blast dest!: leastPD2 setgeD)
    1.60 -
    1.61 -lemma isLubD1: "isLub R S x \<Longrightarrow> S *<= x"
    1.62 -  by (simp add: isLub_def isUb_def leastP_def)
    1.63 -
    1.64 -lemma isLubD1a: "isLub R S x \<Longrightarrow> x: R"
    1.65 -  by (simp add: isLub_def isUb_def leastP_def)
    1.66 -
    1.67 -lemma isLub_isUb: "isLub R S x \<Longrightarrow> isUb R S x"
    1.68 -  unfolding isUb_def by (blast dest: isLubD1 isLubD1a)
    1.69 -
    1.70 -lemma isLubD2: "isLub R S x \<Longrightarrow> y : S \<Longrightarrow> y \<le> x"
    1.71 -  by (blast dest!: isLubD1 setleD)
    1.72 -
    1.73 -lemma isLubD3: "isLub R S x \<Longrightarrow> leastP (isUb R S) x"
    1.74 -  by (simp add: isLub_def)
    1.75 -
    1.76 -lemma isLubI1: "leastP(isUb R S) x \<Longrightarrow> isLub R S x"
    1.77 -  by (simp add: isLub_def)
    1.78 -
    1.79 -lemma isLubI2: "isUb R S x \<Longrightarrow> x <=* Collect (isUb R S) \<Longrightarrow> isLub R S x"
    1.80 -  by (simp add: isLub_def leastP_def)
    1.81 -
    1.82 -lemma isUbD: "isUb R S x \<Longrightarrow> y : S \<Longrightarrow> y \<le> x"
    1.83 -  by (simp add: isUb_def setle_def)
    1.84 -
    1.85 -lemma isUbD2: "isUb R S x \<Longrightarrow> S *<= x"
    1.86 -  by (simp add: isUb_def)
    1.87 -
    1.88 -lemma isUbD2a: "isUb R S x \<Longrightarrow> x: R"
    1.89 -  by (simp add: isUb_def)
    1.90 -
    1.91 -lemma isUbI: "S *<= x \<Longrightarrow> x: R \<Longrightarrow> isUb R S x"
    1.92 -  by (simp add: isUb_def)
    1.93 -
    1.94 -lemma isLub_le_isUb: "isLub R S x \<Longrightarrow> isUb R S y \<Longrightarrow> x \<le> y"
    1.95 -  unfolding isLub_def by (blast intro!: leastPD3)
    1.96 -
    1.97 -lemma isLub_ubs: "isLub R S x \<Longrightarrow> x <=* ubs R S"
    1.98 -  unfolding ubs_def isLub_def by (rule leastPD2)
    1.99 -
   1.100 -lemma isLub_unique: "[| isLub R S x; isLub R S y |] ==> x = (y::'a::linorder)"
   1.101 -  apply (frule isLub_isUb)
   1.102 -  apply (frule_tac x = y in isLub_isUb)
   1.103 -  apply (blast intro!: order_antisym dest!: isLub_le_isUb)
   1.104 -  done
   1.105 -
   1.106 -end