author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 42151  4da4fc77664b 
child 58880  0baae4311a9f 
permissions  rwrr 
42151  1 
(* Title: HOL/HOLCF/Porder.thy 
25773  2 
Author: Franz Regensburger and Brian Huffman 
243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

3 
*) 
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

4 

15587
f363e6e080e7
added subsections and text for document generation
huffman
parents:
15577
diff
changeset

5 
header {* Partial orders *} 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
15562
diff
changeset

6 

15577  7 
theory Porder 
27317  8 
imports Main 
15577  9 
begin 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
15562
diff
changeset

10 

15587
f363e6e080e7
added subsections and text for document generation
huffman
parents:
15577
diff
changeset

11 
subsection {* Type class for partial orders *} 
f363e6e080e7
added subsections and text for document generation
huffman
parents:
15577
diff
changeset

12 

31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
31071
diff
changeset

13 
class below = 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
31071
diff
changeset

14 
fixes below :: "'a \<Rightarrow> 'a \<Rightarrow> bool" 
31071  15 
begin 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
15562
diff
changeset

16 

23284
07ae93e58fea
use newstyle class for sq_ord; rename op << to sq_le
huffman
parents:
21524
diff
changeset

17 
notation 
40436  18 
below (infix "<<" 50) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
15562
diff
changeset

19 

23284
07ae93e58fea
use newstyle class for sq_ord; rename op << to sq_le
huffman
parents:
21524
diff
changeset

20 
notation (xsymbols) 
40436  21 
below (infix "\<sqsubseteq>" 50) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
15562
diff
changeset

22 

41182  23 
abbreviation 
24 
not_below :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "~<<" 50) 

25 
where "not_below x y \<equiv> \<not> below x y" 

26 

27 
notation (xsymbols) 

28 
not_below (infix "\<notsqsubseteq>" 50) 

29 

31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
31071
diff
changeset

30 
lemma below_eq_trans: "\<lbrakk>a \<sqsubseteq> b; b = c\<rbrakk> \<Longrightarrow> a \<sqsubseteq> c" 
31071  31 
by (rule subst) 
32 

31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
31071
diff
changeset

33 
lemma eq_below_trans: "\<lbrakk>a = b; b \<sqsubseteq> c\<rbrakk> \<Longrightarrow> a \<sqsubseteq> c" 
31071  34 
by (rule ssubst) 
35 

36 
end 

37 

31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
31071
diff
changeset

38 
class po = below + 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
31071
diff
changeset

39 
assumes below_refl [iff]: "x \<sqsubseteq> x" 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
31071
diff
changeset

40 
assumes below_trans: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> z" 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
31071
diff
changeset

41 
assumes below_antisym: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> x \<Longrightarrow> x = y" 
31071  42 
begin 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
15562
diff
changeset

43 

40432  44 
lemma eq_imp_below: "x = y \<Longrightarrow> x \<sqsubseteq> y" 
45 
by simp 

46 

31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
31071
diff
changeset

47 
lemma box_below: "a \<sqsubseteq> b \<Longrightarrow> c \<sqsubseteq> a \<Longrightarrow> b \<sqsubseteq> d \<Longrightarrow> c \<sqsubseteq> d" 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
31071
diff
changeset

48 
by (rule below_trans [OF below_trans]) 
17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

49 

31071  50 
lemma po_eq_conv: "x = y \<longleftrightarrow> x \<sqsubseteq> y \<and> y \<sqsubseteq> x" 
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
31071
diff
changeset

51 
by (fast intro!: below_antisym) 
15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
15562
diff
changeset

52 

31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
31071
diff
changeset

53 
lemma rev_below_trans: "y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z" 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
31071
diff
changeset

54 
by (rule below_trans) 
18647  55 

41182  56 
lemma not_below2not_eq: "x \<notsqsubseteq> y \<Longrightarrow> x \<noteq> y" 
31071  57 
by auto 
58 

59 
end 

18647  60 

61 
lemmas HOLCF_trans_rules [trans] = 

31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
31071
diff
changeset

62 
below_trans 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
31071
diff
changeset

63 
below_antisym 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
31071
diff
changeset

64 
below_eq_trans 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
31071
diff
changeset

65 
eq_below_trans 
18647  66 

31071  67 
context po 
68 
begin 

69 

25777  70 
subsection {* Upper bounds *} 
18071
940c2c0ff33a
cleaned up; chain_const and thelub_const are simp rules
huffman
parents:
17810
diff
changeset

71 

40436  72 
definition is_ub :: "'a set \<Rightarrow> 'a \<Rightarrow> bool" (infix "<" 55) where 
39968  73 
"S < x \<longleftrightarrow> (\<forall>y\<in>S. y \<sqsubseteq> x)" 
18071
940c2c0ff33a
cleaned up; chain_const and thelub_const are simp rules
huffman
parents:
17810
diff
changeset

74 

25777  75 
lemma is_ubI: "(\<And>x. x \<in> S \<Longrightarrow> x \<sqsubseteq> u) \<Longrightarrow> S < u" 
31071  76 
by (simp add: is_ub_def) 
25777  77 

78 
lemma is_ubD: "\<lbrakk>S < u; x \<in> S\<rbrakk> \<Longrightarrow> x \<sqsubseteq> u" 

31071  79 
by (simp add: is_ub_def) 
25777  80 

81 
lemma ub_imageI: "(\<And>x. x \<in> S \<Longrightarrow> f x \<sqsubseteq> u) \<Longrightarrow> (\<lambda>x. f x) ` S < u" 

31071  82 
unfolding is_ub_def by fast 
25777  83 

84 
lemma ub_imageD: "\<lbrakk>f ` S < u; x \<in> S\<rbrakk> \<Longrightarrow> f x \<sqsubseteq> u" 

31071  85 
unfolding is_ub_def by fast 
25777  86 

87 
lemma ub_rangeI: "(\<And>i. S i \<sqsubseteq> x) \<Longrightarrow> range S < x" 

31071  88 
unfolding is_ub_def by fast 
25777  89 

90 
lemma ub_rangeD: "range S < x \<Longrightarrow> S i \<sqsubseteq> x" 

31071  91 
unfolding is_ub_def by fast 
25777  92 

25828
228c53fdb3b4
add new is_ub lemmas; clean up directed_finite proofs
huffman
parents:
25813
diff
changeset

93 
lemma is_ub_empty [simp]: "{} < u" 
31071  94 
unfolding is_ub_def by fast 
25828
228c53fdb3b4
add new is_ub lemmas; clean up directed_finite proofs
huffman
parents:
25813
diff
changeset

95 

228c53fdb3b4
add new is_ub lemmas; clean up directed_finite proofs
huffman
parents:
25813
diff
changeset

96 
lemma is_ub_insert [simp]: "(insert x A) < y = (x \<sqsubseteq> y \<and> A < y)" 
31071  97 
unfolding is_ub_def by fast 
25828
228c53fdb3b4
add new is_ub lemmas; clean up directed_finite proofs
huffman
parents:
25813
diff
changeset

98 

228c53fdb3b4
add new is_ub lemmas; clean up directed_finite proofs
huffman
parents:
25813
diff
changeset

99 
lemma is_ub_upward: "\<lbrakk>S < x; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> S < y" 
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
31071
diff
changeset

100 
unfolding is_ub_def by (fast intro: below_trans) 
25828
228c53fdb3b4
add new is_ub lemmas; clean up directed_finite proofs
huffman
parents:
25813
diff
changeset

101 

25777  102 
subsection {* Least upper bounds *} 
103 

40436  104 
definition is_lub :: "'a set \<Rightarrow> 'a \<Rightarrow> bool" (infix "<<" 55) where 
31071  105 
"S << x \<longleftrightarrow> S < x \<and> (\<forall>u. S < u \<longrightarrow> x \<sqsubseteq> u)" 
18071
940c2c0ff33a
cleaned up; chain_const and thelub_const are simp rules
huffman
parents:
17810
diff
changeset

106 

31071  107 
definition lub :: "'a set \<Rightarrow> 'a" where 
25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
24728
diff
changeset

108 
"lub S = (THE x. S << x)" 
243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

109 

31071  110 
end 
111 

25777  112 
syntax 
113 
"_BLub" :: "[pttrn, 'a set, 'b] \<Rightarrow> 'b" ("(3LUB _:_./ _)" [0,0, 10] 10) 

114 

115 
syntax (xsymbols) 

116 
"_BLub" :: "[pttrn, 'a set, 'b] \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0,0, 10] 10) 

117 

118 
translations 

119 
"LUB x:A. t" == "CONST lub ((%x. t) ` A)" 

120 

31071  121 
context po 
122 
begin 

123 

21524  124 
abbreviation 
125 
Lub (binder "LUB " 10) where 

126 
"LUB n. t n == lub (range t)" 

2394  127 

21524  128 
notation (xsymbols) 
129 
Lub (binder "\<Squnion> " 10) 

243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

130 

25813  131 
text {* access to some definition as inference rule *} 
132 

133 
lemma is_lubD1: "S << x \<Longrightarrow> S < x" 

31071  134 
unfolding is_lub_def by fast 
25813  135 

40771  136 
lemma is_lubD2: "\<lbrakk>S << x; S < u\<rbrakk> \<Longrightarrow> x \<sqsubseteq> u" 
31071  137 
unfolding is_lub_def by fast 
25813  138 

139 
lemma is_lubI: "\<lbrakk>S < x; \<And>u. S < u \<Longrightarrow> x \<sqsubseteq> u\<rbrakk> \<Longrightarrow> S << x" 

31071  140 
unfolding is_lub_def by fast 
25813  141 

39969  142 
lemma is_lub_below_iff: "S << x \<Longrightarrow> x \<sqsubseteq> u \<longleftrightarrow> S < u" 
143 
unfolding is_lub_def is_ub_def by (metis below_trans) 

144 

15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
15562
diff
changeset

145 
text {* lubs are unique *} 
15562  146 

40771  147 
lemma is_lub_unique: "\<lbrakk>S << x; S << y\<rbrakk> \<Longrightarrow> x = y" 
148 
unfolding is_lub_def is_ub_def by (blast intro: below_antisym) 

15562  149 

15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
15562
diff
changeset

150 
text {* technical lemmas about @{term lub} and @{term is_lub} *} 
15562  151 

40771  152 
lemma is_lub_lub: "M << x \<Longrightarrow> M << lub M" 
153 
unfolding lub_def by (rule theI [OF _ is_lub_unique]) 

15562  154 

40771  155 
lemma lub_eqI: "M << l \<Longrightarrow> lub M = l" 
156 
by (rule is_lub_unique [OF is_lub_lub]) 

15562  157 

25780  158 
lemma is_lub_singleton: "{x} << x" 
31071  159 
by (simp add: is_lub_def) 
25780  160 

17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

161 
lemma lub_singleton [simp]: "lub {x} = x" 
40771  162 
by (rule is_lub_singleton [THEN lub_eqI]) 
25780  163 

164 
lemma is_lub_bin: "x \<sqsubseteq> y \<Longrightarrow> {x, y} << y" 

31071  165 
by (simp add: is_lub_def) 
25780  166 

167 
lemma lub_bin: "x \<sqsubseteq> y \<Longrightarrow> lub {x, y} = y" 

40771  168 
by (rule is_lub_bin [THEN lub_eqI]) 
15562  169 

25813  170 
lemma is_lub_maximal: "\<lbrakk>S < x; x \<in> S\<rbrakk> \<Longrightarrow> S << x" 
31071  171 
by (erule is_lubI, erule (1) is_ubD) 
15562  172 

25813  173 
lemma lub_maximal: "\<lbrakk>S < x; x \<in> S\<rbrakk> \<Longrightarrow> lub S = x" 
40771  174 
by (rule is_lub_maximal [THEN lub_eqI]) 
243
c22b85994e17
Franz Regensburger's HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

175 

25695  176 
subsection {* Countable chains *} 
177 

31071  178 
definition chain :: "(nat \<Rightarrow> 'a) \<Rightarrow> bool" where 
25695  179 
 {* Here we use countable chains and I prefer to code them as functions! *} 
25922
cb04d05e95fb
rename lemma chain_mono3 > chain_mono, chain_mono > chain_mono_less
huffman
parents:
25897
diff
changeset

180 
"chain Y = (\<forall>i. Y i \<sqsubseteq> Y (Suc i))" 
cb04d05e95fb
rename lemma chain_mono3 > chain_mono, chain_mono > chain_mono_less
huffman
parents:
25897
diff
changeset

181 

cb04d05e95fb
rename lemma chain_mono3 > chain_mono, chain_mono > chain_mono_less
huffman
parents:
25897
diff
changeset

182 
lemma chainI: "(\<And>i. Y i \<sqsubseteq> Y (Suc i)) \<Longrightarrow> chain Y" 
31071  183 
unfolding chain_def by fast 
25922
cb04d05e95fb
rename lemma chain_mono3 > chain_mono, chain_mono > chain_mono_less
huffman
parents:
25897
diff
changeset

184 

cb04d05e95fb
rename lemma chain_mono3 > chain_mono, chain_mono > chain_mono_less
huffman
parents:
25897
diff
changeset

185 
lemma chainE: "chain Y \<Longrightarrow> Y i \<sqsubseteq> Y (Suc i)" 
31071  186 
unfolding chain_def by fast 
25695  187 

188 
text {* chains are monotone functions *} 

189 

27317  190 
lemma chain_mono_less: "\<lbrakk>chain Y; i < j\<rbrakk> \<Longrightarrow> Y i \<sqsubseteq> Y j" 
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
31071
diff
changeset

191 
by (erule less_Suc_induct, erule chainE, erule below_trans) 
25695  192 

27317  193 
lemma chain_mono: "\<lbrakk>chain Y; i \<le> j\<rbrakk> \<Longrightarrow> Y i \<sqsubseteq> Y j" 
31071  194 
by (cases "i = j", simp, simp add: chain_mono_less) 
15562  195 

17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

196 
lemma chain_shift: "chain Y \<Longrightarrow> chain (\<lambda>i. Y (i + j))" 
31071  197 
by (rule chainI, simp, erule chainE) 
15562  198 

15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
15562
diff
changeset

199 
text {* technical lemmas about (least) upper bounds of chains *} 
15562  200 

40771  201 
lemma is_lub_rangeD1: "range S << x \<Longrightarrow> S i \<sqsubseteq> x" 
31071  202 
by (rule is_lubD1 [THEN ub_rangeD]) 
15562  203 

16318
45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset

204 
lemma is_ub_range_shift: 
45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset

205 
"chain S \<Longrightarrow> range (\<lambda>i. S (i + j)) < x = range S < x" 
45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset

206 
apply (rule iffI) 
45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset

207 
apply (rule ub_rangeI) 
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
31071
diff
changeset

208 
apply (rule_tac y="S (i + j)" in below_trans) 
25922
cb04d05e95fb
rename lemma chain_mono3 > chain_mono, chain_mono > chain_mono_less
huffman
parents:
25897
diff
changeset

209 
apply (erule chain_mono) 
16318
45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset

210 
apply (rule le_add1) 
45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset

211 
apply (erule ub_rangeD) 
45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset

212 
apply (rule ub_rangeI) 
45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset

213 
apply (erule ub_rangeD) 
45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset

214 
done 
45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset

215 

45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset

216 
lemma is_lub_range_shift: 
45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset

217 
"chain S \<Longrightarrow> range (\<lambda>i. S (i + j)) << x = range S << x" 
31071  218 
by (simp add: is_lub_def is_ub_range_shift) 
16318
45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset

219 

25695  220 
text {* the lub of a constant chain is the constant *} 
221 

222 
lemma chain_const [simp]: "chain (\<lambda>i. c)" 

31071  223 
by (simp add: chainI) 
25695  224 

40771  225 
lemma is_lub_const: "range (\<lambda>x. c) << c" 
25695  226 
by (blast dest: ub_rangeD intro: is_lubI ub_rangeI) 
227 

40771  228 
lemma lub_const [simp]: "(\<Squnion>i. c) = c" 
229 
by (rule is_lub_const [THEN lub_eqI]) 

25695  230 

231 
subsection {* Finite chains *} 

232 

31071  233 
definition max_in_chain :: "nat \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> bool" where 
25695  234 
 {* finite chains, needed for monotony of continuous functions *} 
31071  235 
"max_in_chain i C \<longleftrightarrow> (\<forall>j. i \<le> j \<longrightarrow> C i = C j)" 
25695  236 

31071  237 
definition finite_chain :: "(nat \<Rightarrow> 'a) \<Rightarrow> bool" where 
25695  238 
"finite_chain C = (chain C \<and> (\<exists>i. max_in_chain i C))" 
239 

15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
15562
diff
changeset

240 
text {* results about finite chains *} 
15562  241 

25878  242 
lemma max_in_chainI: "(\<And>j. i \<le> j \<Longrightarrow> Y i = Y j) \<Longrightarrow> max_in_chain i Y" 
31071  243 
unfolding max_in_chain_def by fast 
25878  244 

245 
lemma max_in_chainD: "\<lbrakk>max_in_chain i Y; i \<le> j\<rbrakk> \<Longrightarrow> Y i = Y j" 

31071  246 
unfolding max_in_chain_def by fast 
25878  247 

27317  248 
lemma finite_chainI: 
249 
"\<lbrakk>chain C; max_in_chain i C\<rbrakk> \<Longrightarrow> finite_chain C" 

31071  250 
unfolding finite_chain_def by fast 
27317  251 

252 
lemma finite_chainE: 

253 
"\<lbrakk>finite_chain C; \<And>i. \<lbrakk>chain C; max_in_chain i C\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R" 

31071  254 
unfolding finite_chain_def by fast 
27317  255 

17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

256 
lemma lub_finch1: "\<lbrakk>chain C; max_in_chain i C\<rbrakk> \<Longrightarrow> range C << C i" 
15562  257 
apply (rule is_lubI) 
17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

258 
apply (rule ub_rangeI, rename_tac j) 
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

259 
apply (rule_tac x=i and y=j in linorder_le_cases) 
25878  260 
apply (drule (1) max_in_chainD, simp) 
25922
cb04d05e95fb
rename lemma chain_mono3 > chain_mono, chain_mono > chain_mono_less
huffman
parents:
25897
diff
changeset

261 
apply (erule (1) chain_mono) 
15562  262 
apply (erule ub_rangeD) 
263 
done 

264 

25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
24728
diff
changeset

265 
lemma lub_finch2: 
27317  266 
"finite_chain C \<Longrightarrow> range C << C (LEAST i. max_in_chain i C)" 
267 
apply (erule finite_chainE) 

268 
apply (erule LeastI2 [where Q="\<lambda>i. range C << C i"]) 

17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

269 
apply (erule (1) lub_finch1) 
15562  270 
done 
271 

19621  272 
lemma finch_imp_finite_range: "finite_chain Y \<Longrightarrow> finite (range Y)" 
27317  273 
apply (erule finite_chainE) 
274 
apply (rule_tac B="Y ` {..i}" in finite_subset) 

19621  275 
apply (rule subsetI) 
276 
apply (erule rangeE, rename_tac j) 

277 
apply (rule_tac x=i and y=j in linorder_le_cases) 

278 
apply (subgoal_tac "Y j = Y i", simp) 

279 
apply (simp add: max_in_chain_def) 

280 
apply simp 

27317  281 
apply simp 
19621  282 
done 
283 

27317  284 
lemma finite_range_has_max: 
285 
fixes f :: "nat \<Rightarrow> 'a" and r :: "'a \<Rightarrow> 'a \<Rightarrow> bool" 

286 
assumes mono: "\<And>i j. i \<le> j \<Longrightarrow> r (f i) (f j)" 

287 
assumes finite_range: "finite (range f)" 

288 
shows "\<exists>k. \<forall>i. r (f i) (f k)" 

289 
proof (intro exI allI) 

290 
fix i :: nat 

291 
let ?j = "LEAST k. f k = f i" 

292 
let ?k = "Max ((\<lambda>x. LEAST k. f k = x) ` range f)" 

293 
have "?j \<le> ?k" 

294 
proof (rule Max_ge) 

295 
show "finite ((\<lambda>x. LEAST k. f k = x) ` range f)" 

296 
using finite_range by (rule finite_imageI) 

297 
show "?j \<in> (\<lambda>x. LEAST k. f k = x) ` range f" 

298 
by (intro imageI rangeI) 

299 
qed 

300 
hence "r (f ?j) (f ?k)" 

301 
by (rule mono) 

302 
also have "f ?j = f i" 

303 
by (rule LeastI, rule refl) 

304 
finally show "r (f i) (f ?k)" . 

305 
qed 

306 

19621  307 
lemma finite_range_imp_finch: 
308 
"\<lbrakk>chain Y; finite (range Y)\<rbrakk> \<Longrightarrow> finite_chain Y" 

27317  309 
apply (subgoal_tac "\<exists>k. \<forall>i. Y i \<sqsubseteq> Y k") 
310 
apply (erule exE) 

311 
apply (rule finite_chainI, assumption) 

312 
apply (rule max_in_chainI) 

31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
31071
diff
changeset

313 
apply (rule below_antisym) 
27317  314 
apply (erule (1) chain_mono) 
315 
apply (erule spec) 

316 
apply (rule finite_range_has_max) 

317 
apply (erule (1) chain_mono) 

318 
apply assumption 

19621  319 
done 
320 

17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

321 
lemma bin_chain: "x \<sqsubseteq> y \<Longrightarrow> chain (\<lambda>i. if i=0 then x else y)" 
31071  322 
by (rule chainI, simp) 
17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

323 

3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

324 
lemma bin_chainmax: 
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

325 
"x \<sqsubseteq> y \<Longrightarrow> max_in_chain (Suc 0) (\<lambda>i. if i=0 then x else y)" 
31071  326 
unfolding max_in_chain_def by simp 
15562  327 

40771  328 
lemma is_lub_bin_chain: 
17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

329 
"x \<sqsubseteq> y \<Longrightarrow> range (\<lambda>i::nat. if i=0 then x else y) << y" 
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

330 
apply (frule bin_chain) 
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

331 
apply (drule bin_chainmax) 
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

332 
apply (drule (1) lub_finch1) 
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

333 
apply simp 
15562  334 
done 
335 

15576
efb95d0d01f7
converted to newstyle theories, and combined numbered files
huffman
parents:
15562
diff
changeset

336 
text {* the maximal element in a chain is its lub *} 
15562  337 

17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset

338 
lemma lub_chain_maxelem: "\<lbrakk>Y i = c; \<forall>i. Y i \<sqsubseteq> c\<rbrakk> \<Longrightarrow> lub (range Y) = c" 
40771  339 
by (blast dest: ub_rangeD intro: lub_eqI is_lubI ub_rangeI) 
15562  340 

18071
940c2c0ff33a
cleaned up; chain_const and thelub_const are simp rules
huffman
parents:
17810
diff
changeset

341 
end 
31071  342 

31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
31071
diff
changeset

343 
end 