author  webertj 
Fri, 19 Oct 2012 15:12:52 +0200  
changeset 49962  a8cc904a6820 
parent 46509  c4b2ec379fdd 
child 51520  e9b361845809 
permissions  rwrr 
46509  1 
(* Title: HOL/Lubs.thy 
2 
Author: Jacques D. Fleuriot, University of Cambridge 

14368
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset

3 
*) 
5078  4 

46509  5 
header {* Definitions of Upper Bounds and Least Upper Bounds *} 
5078  6 

15131  7 
theory Lubs 
30738  8 
imports Main 
15131  9 
begin 
5078  10 

46509  11 
text {* Thanks to suggestions by James Margetson *} 
5078  12 

46509  13 
definition setle :: "'a set \<Rightarrow> 'a::ord \<Rightarrow> bool" (infixl "*<=" 70) 
14 
where "S *<= x = (ALL y: S. y \<le> x)" 

14368
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset

15 

46509  16 
definition setge :: "'a::ord \<Rightarrow> 'a set \<Rightarrow> bool" (infixl "<=*" 70) 
17 
where "x <=* S = (ALL y: S. x \<le> y)" 

14368
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset

18 

46509  19 
definition leastP :: "('a \<Rightarrow> bool) \<Rightarrow> 'a::ord \<Rightarrow> bool" 
20 
where "leastP P x = (P x \<and> x <=* Collect P)" 

5078  21 

46509  22 
definition isUb :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool" 
23 
where "isUb R S x = (S *<= x \<and> x: R)" 

14653  24 

46509  25 
definition isLub :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool" 
26 
where "isLub R S x = leastP (isUb R S) x" 

5078  27 

46509  28 
definition ubs :: "'a set \<Rightarrow> 'a::ord set \<Rightarrow> 'a set" 
29 
where "ubs R S = Collect (isUb R S)" 

5078  30 

14368
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset

31 

46509  32 
subsection {* Rules for the Relations @{text "*<="} and @{text "<=*"} *} 
14368
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset

33 

46509  34 
lemma setleI: "ALL y: S. y \<le> x \<Longrightarrow> S *<= x" 
35 
by (simp add: setle_def) 

14368
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset

36 

46509  37 
lemma setleD: "S *<= x \<Longrightarrow> y: S \<Longrightarrow> y \<le> x" 
38 
by (simp add: setle_def) 

14368
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset

39 

46509  40 
lemma setgeI: "ALL y: S. x \<le> y \<Longrightarrow> x <=* S" 
41 
by (simp add: setge_def) 

14368
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset

42 

46509  43 
lemma setgeD: "x <=* S \<Longrightarrow> y: S \<Longrightarrow> x \<le> y" 
44 
by (simp add: setge_def) 

14368
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset

45 

2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset

46 

46509  47 
subsection {* Rules about the Operators @{term leastP}, @{term ub} and @{term lub} *} 
14368
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset

48 

46509  49 
lemma leastPD1: "leastP P x \<Longrightarrow> P x" 
50 
by (simp add: leastP_def) 

14368
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset

51 

46509  52 
lemma leastPD2: "leastP P x \<Longrightarrow> x <=* Collect P" 
53 
by (simp add: leastP_def) 

14368
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset

54 

46509  55 
lemma leastPD3: "leastP P x \<Longrightarrow> y: Collect P \<Longrightarrow> x \<le> y" 
56 
by (blast dest!: leastPD2 setgeD) 

14368
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset

57 

46509  58 
lemma isLubD1: "isLub R S x \<Longrightarrow> S *<= x" 
59 
by (simp add: isLub_def isUb_def leastP_def) 

14368
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset

60 

46509  61 
lemma isLubD1a: "isLub R S x \<Longrightarrow> x: R" 
62 
by (simp add: isLub_def isUb_def leastP_def) 

14368
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset

63 

46509  64 
lemma isLub_isUb: "isLub R S x \<Longrightarrow> isUb R S x" 
65 
unfolding isUb_def by (blast dest: isLubD1 isLubD1a) 

14368
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset

66 

46509  67 
lemma isLubD2: "isLub R S x \<Longrightarrow> y : S \<Longrightarrow> y \<le> x" 
68 
by (blast dest!: isLubD1 setleD) 

14368
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset

69 

46509  70 
lemma isLubD3: "isLub R S x \<Longrightarrow> leastP (isUb R S) x" 
71 
by (simp add: isLub_def) 

14368
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset

72 

46509  73 
lemma isLubI1: "leastP(isUb R S) x \<Longrightarrow> isLub R S x" 
74 
by (simp add: isLub_def) 

14368
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset

75 

46509  76 
lemma isLubI2: "isUb R S x \<Longrightarrow> x <=* Collect (isUb R S) \<Longrightarrow> isLub R S x" 
77 
by (simp add: isLub_def leastP_def) 

5078  78 

46509  79 
lemma isUbD: "isUb R S x \<Longrightarrow> y : S \<Longrightarrow> y \<le> x" 
80 
by (simp add: isUb_def setle_def) 

14368
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset

81 

46509  82 
lemma isUbD2: "isUb R S x \<Longrightarrow> S *<= x" 
83 
by (simp add: isUb_def) 

14368
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset

84 

46509  85 
lemma isUbD2a: "isUb R S x \<Longrightarrow> x: R" 
86 
by (simp add: isUb_def) 

14368
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset

87 

46509  88 
lemma isUbI: "S *<= x \<Longrightarrow> x: R \<Longrightarrow> isUb R S x" 
89 
by (simp add: isUb_def) 

14368
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset

90 

46509  91 
lemma isLub_le_isUb: "isLub R S x \<Longrightarrow> isUb R S y \<Longrightarrow> x \<le> y" 
92 
unfolding isLub_def by (blast intro!: leastPD3) 

93 

94 
lemma isLub_ubs: "isLub R S x \<Longrightarrow> x <=* ubs R S" 

95 
unfolding ubs_def isLub_def by (rule leastPD2) 

5078  96 

14368
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
9279
diff
changeset

97 
end 