author | huffman |
Sat, 27 Nov 2010 16:08:10 -0800 | |
changeset 40774 | 0437dbc127b3 |
parent 40771 | src/HOLCF/Porder.thy@1c6f7d4b110e |
child 41182 | 717404c7d59a |
permissions | -rw-r--r-- |
15600 | 1 |
(* Title: HOLCF/Porder.thy |
25773 | 2 |
Author: Franz Regensburger and Brian Huffman |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
3 |
*) |
c22b85994e17
Franz Regensburger's Higher-Order 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 new-style 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 new-style 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 new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
16 |
|
23284
07ae93e58fea
use new-style 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 new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
19 |
|
23284
07ae93e58fea
use new-style 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 new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
22 |
|
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
|
23 |
lemma below_eq_trans: "\<lbrakk>a \<sqsubseteq> b; b = c\<rbrakk> \<Longrightarrow> a \<sqsubseteq> c" |
31071 | 24 |
by (rule subst) |
25 |
||
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
|
26 |
lemma eq_below_trans: "\<lbrakk>a = b; b \<sqsubseteq> c\<rbrakk> \<Longrightarrow> a \<sqsubseteq> c" |
31071 | 27 |
by (rule ssubst) |
28 |
||
29 |
end |
|
30 |
||
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
|
31 |
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
|
32 |
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
|
33 |
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
|
34 |
assumes below_antisym: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> x \<Longrightarrow> x = y" |
31071 | 35 |
begin |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
36 |
|
40432 | 37 |
lemma eq_imp_below: "x = y \<Longrightarrow> x \<sqsubseteq> y" |
38 |
by simp |
|
39 |
||
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
|
40 |
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
|
41 |
by (rule below_trans [OF below_trans]) |
17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
42 |
|
31071 | 43 |
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
|
44 |
by (fast intro!: below_antisym) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
45 |
|
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
|
46 |
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
|
47 |
by (rule below_trans) |
18647 | 48 |
|
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
|
49 |
lemma not_below2not_eq: "\<not> x \<sqsubseteq> y \<Longrightarrow> x \<noteq> y" |
31071 | 50 |
by auto |
51 |
||
52 |
end |
|
18647 | 53 |
|
54 |
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
|
55 |
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
|
56 |
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
|
57 |
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
|
58 |
eq_below_trans |
18647 | 59 |
|
31071 | 60 |
context po |
61 |
begin |
|
62 |
||
25777 | 63 |
subsection {* Upper bounds *} |
18071
940c2c0ff33a
cleaned up; chain_const and thelub_const are simp rules
huffman
parents:
17810
diff
changeset
|
64 |
|
40436 | 65 |
definition is_ub :: "'a set \<Rightarrow> 'a \<Rightarrow> bool" (infix "<|" 55) where |
39968 | 66 |
"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
|
67 |
|
25777 | 68 |
lemma is_ubI: "(\<And>x. x \<in> S \<Longrightarrow> x \<sqsubseteq> u) \<Longrightarrow> S <| u" |
31071 | 69 |
by (simp add: is_ub_def) |
25777 | 70 |
|
71 |
lemma is_ubD: "\<lbrakk>S <| u; x \<in> S\<rbrakk> \<Longrightarrow> x \<sqsubseteq> u" |
|
31071 | 72 |
by (simp add: is_ub_def) |
25777 | 73 |
|
74 |
lemma ub_imageI: "(\<And>x. x \<in> S \<Longrightarrow> f x \<sqsubseteq> u) \<Longrightarrow> (\<lambda>x. f x) ` S <| u" |
|
31071 | 75 |
unfolding is_ub_def by fast |
25777 | 76 |
|
77 |
lemma ub_imageD: "\<lbrakk>f ` S <| u; x \<in> S\<rbrakk> \<Longrightarrow> f x \<sqsubseteq> u" |
|
31071 | 78 |
unfolding is_ub_def by fast |
25777 | 79 |
|
80 |
lemma ub_rangeI: "(\<And>i. S i \<sqsubseteq> x) \<Longrightarrow> range S <| x" |
|
31071 | 81 |
unfolding is_ub_def by fast |
25777 | 82 |
|
83 |
lemma ub_rangeD: "range S <| x \<Longrightarrow> S i \<sqsubseteq> x" |
|
31071 | 84 |
unfolding is_ub_def by fast |
25777 | 85 |
|
25828
228c53fdb3b4
add new is_ub lemmas; clean up directed_finite proofs
huffman
parents:
25813
diff
changeset
|
86 |
lemma is_ub_empty [simp]: "{} <| u" |
31071 | 87 |
unfolding is_ub_def by fast |
25828
228c53fdb3b4
add new is_ub lemmas; clean up directed_finite proofs
huffman
parents:
25813
diff
changeset
|
88 |
|
228c53fdb3b4
add new is_ub lemmas; clean up directed_finite proofs
huffman
parents:
25813
diff
changeset
|
89 |
lemma is_ub_insert [simp]: "(insert x A) <| y = (x \<sqsubseteq> y \<and> A <| y)" |
31071 | 90 |
unfolding is_ub_def by fast |
25828
228c53fdb3b4
add new is_ub lemmas; clean up directed_finite proofs
huffman
parents:
25813
diff
changeset
|
91 |
|
228c53fdb3b4
add new is_ub lemmas; clean up directed_finite proofs
huffman
parents:
25813
diff
changeset
|
92 |
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
|
93 |
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
|
94 |
|
25777 | 95 |
subsection {* Least upper bounds *} |
96 |
||
40436 | 97 |
definition is_lub :: "'a set \<Rightarrow> 'a \<Rightarrow> bool" (infix "<<|" 55) where |
31071 | 98 |
"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
|
99 |
|
31071 | 100 |
definition lub :: "'a set \<Rightarrow> 'a" where |
25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
24728
diff
changeset
|
101 |
"lub S = (THE x. S <<| x)" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
102 |
|
31071 | 103 |
end |
104 |
||
25777 | 105 |
syntax |
106 |
"_BLub" :: "[pttrn, 'a set, 'b] \<Rightarrow> 'b" ("(3LUB _:_./ _)" [0,0, 10] 10) |
|
107 |
||
108 |
syntax (xsymbols) |
|
109 |
"_BLub" :: "[pttrn, 'a set, 'b] \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0,0, 10] 10) |
|
110 |
||
111 |
translations |
|
112 |
"LUB x:A. t" == "CONST lub ((%x. t) ` A)" |
|
113 |
||
31071 | 114 |
context po |
115 |
begin |
|
116 |
||
21524 | 117 |
abbreviation |
118 |
Lub (binder "LUB " 10) where |
|
119 |
"LUB n. t n == lub (range t)" |
|
2394 | 120 |
|
21524 | 121 |
notation (xsymbols) |
122 |
Lub (binder "\<Squnion> " 10) |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
123 |
|
25813 | 124 |
text {* access to some definition as inference rule *} |
125 |
||
126 |
lemma is_lubD1: "S <<| x \<Longrightarrow> S <| x" |
|
31071 | 127 |
unfolding is_lub_def by fast |
25813 | 128 |
|
40771 | 129 |
lemma is_lubD2: "\<lbrakk>S <<| x; S <| u\<rbrakk> \<Longrightarrow> x \<sqsubseteq> u" |
31071 | 130 |
unfolding is_lub_def by fast |
25813 | 131 |
|
132 |
lemma is_lubI: "\<lbrakk>S <| x; \<And>u. S <| u \<Longrightarrow> x \<sqsubseteq> u\<rbrakk> \<Longrightarrow> S <<| x" |
|
31071 | 133 |
unfolding is_lub_def by fast |
25813 | 134 |
|
39969 | 135 |
lemma is_lub_below_iff: "S <<| x \<Longrightarrow> x \<sqsubseteq> u \<longleftrightarrow> S <| u" |
136 |
unfolding is_lub_def is_ub_def by (metis below_trans) |
|
137 |
||
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
138 |
text {* lubs are unique *} |
15562 | 139 |
|
40771 | 140 |
lemma is_lub_unique: "\<lbrakk>S <<| x; S <<| y\<rbrakk> \<Longrightarrow> x = y" |
141 |
unfolding is_lub_def is_ub_def by (blast intro: below_antisym) |
|
15562 | 142 |
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
143 |
text {* technical lemmas about @{term lub} and @{term is_lub} *} |
15562 | 144 |
|
40771 | 145 |
lemma is_lub_lub: "M <<| x \<Longrightarrow> M <<| lub M" |
146 |
unfolding lub_def by (rule theI [OF _ is_lub_unique]) |
|
15562 | 147 |
|
40771 | 148 |
lemma lub_eqI: "M <<| l \<Longrightarrow> lub M = l" |
149 |
by (rule is_lub_unique [OF is_lub_lub]) |
|
15562 | 150 |
|
25780 | 151 |
lemma is_lub_singleton: "{x} <<| x" |
31071 | 152 |
by (simp add: is_lub_def) |
25780 | 153 |
|
17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
154 |
lemma lub_singleton [simp]: "lub {x} = x" |
40771 | 155 |
by (rule is_lub_singleton [THEN lub_eqI]) |
25780 | 156 |
|
157 |
lemma is_lub_bin: "x \<sqsubseteq> y \<Longrightarrow> {x, y} <<| y" |
|
31071 | 158 |
by (simp add: is_lub_def) |
25780 | 159 |
|
160 |
lemma lub_bin: "x \<sqsubseteq> y \<Longrightarrow> lub {x, y} = y" |
|
40771 | 161 |
by (rule is_lub_bin [THEN lub_eqI]) |
15562 | 162 |
|
25813 | 163 |
lemma is_lub_maximal: "\<lbrakk>S <| x; x \<in> S\<rbrakk> \<Longrightarrow> S <<| x" |
31071 | 164 |
by (erule is_lubI, erule (1) is_ubD) |
15562 | 165 |
|
25813 | 166 |
lemma lub_maximal: "\<lbrakk>S <| x; x \<in> S\<rbrakk> \<Longrightarrow> lub S = x" |
40771 | 167 |
by (rule is_lub_maximal [THEN lub_eqI]) |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
168 |
|
25695 | 169 |
subsection {* Countable chains *} |
170 |
||
31071 | 171 |
definition chain :: "(nat \<Rightarrow> 'a) \<Rightarrow> bool" where |
25695 | 172 |
-- {* 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
|
173 |
"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
|
174 |
|
cb04d05e95fb
rename lemma chain_mono3 -> chain_mono, chain_mono -> chain_mono_less
huffman
parents:
25897
diff
changeset
|
175 |
lemma chainI: "(\<And>i. Y i \<sqsubseteq> Y (Suc i)) \<Longrightarrow> chain Y" |
31071 | 176 |
unfolding chain_def by fast |
25922
cb04d05e95fb
rename lemma chain_mono3 -> chain_mono, chain_mono -> chain_mono_less
huffman
parents:
25897
diff
changeset
|
177 |
|
cb04d05e95fb
rename lemma chain_mono3 -> chain_mono, chain_mono -> chain_mono_less
huffman
parents:
25897
diff
changeset
|
178 |
lemma chainE: "chain Y \<Longrightarrow> Y i \<sqsubseteq> Y (Suc i)" |
31071 | 179 |
unfolding chain_def by fast |
25695 | 180 |
|
181 |
text {* chains are monotone functions *} |
|
182 |
||
27317 | 183 |
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
|
184 |
by (erule less_Suc_induct, erule chainE, erule below_trans) |
25695 | 185 |
|
27317 | 186 |
lemma chain_mono: "\<lbrakk>chain Y; i \<le> j\<rbrakk> \<Longrightarrow> Y i \<sqsubseteq> Y j" |
31071 | 187 |
by (cases "i = j", simp, simp add: chain_mono_less) |
15562 | 188 |
|
17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
189 |
lemma chain_shift: "chain Y \<Longrightarrow> chain (\<lambda>i. Y (i + j))" |
31071 | 190 |
by (rule chainI, simp, erule chainE) |
15562 | 191 |
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
192 |
text {* technical lemmas about (least) upper bounds of chains *} |
15562 | 193 |
|
40771 | 194 |
lemma is_lub_rangeD1: "range S <<| x \<Longrightarrow> S i \<sqsubseteq> x" |
31071 | 195 |
by (rule is_lubD1 [THEN ub_rangeD]) |
15562 | 196 |
|
16318
45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset
|
197 |
lemma is_ub_range_shift: |
45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset
|
198 |
"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
|
199 |
apply (rule iffI) |
45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset
|
200 |
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
|
201 |
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
|
202 |
apply (erule chain_mono) |
16318
45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset
|
203 |
apply (rule le_add1) |
45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset
|
204 |
apply (erule ub_rangeD) |
45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset
|
205 |
apply (rule ub_rangeI) |
45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset
|
206 |
apply (erule ub_rangeD) |
45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset
|
207 |
done |
45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset
|
208 |
|
45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset
|
209 |
lemma is_lub_range_shift: |
45b12a01382f
added theorems is_ub_range_shift and is_lub_range_shift
huffman
parents:
16092
diff
changeset
|
210 |
"chain S \<Longrightarrow> range (\<lambda>i. S (i + j)) <<| x = range S <<| x" |
31071 | 211 |
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
|
212 |
|
25695 | 213 |
text {* the lub of a constant chain is the constant *} |
214 |
||
215 |
lemma chain_const [simp]: "chain (\<lambda>i. c)" |
|
31071 | 216 |
by (simp add: chainI) |
25695 | 217 |
|
40771 | 218 |
lemma is_lub_const: "range (\<lambda>x. c) <<| c" |
25695 | 219 |
by (blast dest: ub_rangeD intro: is_lubI ub_rangeI) |
220 |
||
40771 | 221 |
lemma lub_const [simp]: "(\<Squnion>i. c) = c" |
222 |
by (rule is_lub_const [THEN lub_eqI]) |
|
25695 | 223 |
|
224 |
subsection {* Finite chains *} |
|
225 |
||
31071 | 226 |
definition max_in_chain :: "nat \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> bool" where |
25695 | 227 |
-- {* finite chains, needed for monotony of continuous functions *} |
31071 | 228 |
"max_in_chain i C \<longleftrightarrow> (\<forall>j. i \<le> j \<longrightarrow> C i = C j)" |
25695 | 229 |
|
31071 | 230 |
definition finite_chain :: "(nat \<Rightarrow> 'a) \<Rightarrow> bool" where |
25695 | 231 |
"finite_chain C = (chain C \<and> (\<exists>i. max_in_chain i C))" |
232 |
||
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
233 |
text {* results about finite chains *} |
15562 | 234 |
|
25878 | 235 |
lemma max_in_chainI: "(\<And>j. i \<le> j \<Longrightarrow> Y i = Y j) \<Longrightarrow> max_in_chain i Y" |
31071 | 236 |
unfolding max_in_chain_def by fast |
25878 | 237 |
|
238 |
lemma max_in_chainD: "\<lbrakk>max_in_chain i Y; i \<le> j\<rbrakk> \<Longrightarrow> Y i = Y j" |
|
31071 | 239 |
unfolding max_in_chain_def by fast |
25878 | 240 |
|
27317 | 241 |
lemma finite_chainI: |
242 |
"\<lbrakk>chain C; max_in_chain i C\<rbrakk> \<Longrightarrow> finite_chain C" |
|
31071 | 243 |
unfolding finite_chain_def by fast |
27317 | 244 |
|
245 |
lemma finite_chainE: |
|
246 |
"\<lbrakk>finite_chain C; \<And>i. \<lbrakk>chain C; max_in_chain i C\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R" |
|
31071 | 247 |
unfolding finite_chain_def by fast |
27317 | 248 |
|
17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
249 |
lemma lub_finch1: "\<lbrakk>chain C; max_in_chain i C\<rbrakk> \<Longrightarrow> range C <<| C i" |
15562 | 250 |
apply (rule is_lubI) |
17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
251 |
apply (rule ub_rangeI, rename_tac j) |
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
252 |
apply (rule_tac x=i and y=j in linorder_le_cases) |
25878 | 253 |
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
|
254 |
apply (erule (1) chain_mono) |
15562 | 255 |
apply (erule ub_rangeD) |
256 |
done |
|
257 |
||
25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
24728
diff
changeset
|
258 |
lemma lub_finch2: |
27317 | 259 |
"finite_chain C \<Longrightarrow> range C <<| C (LEAST i. max_in_chain i C)" |
260 |
apply (erule finite_chainE) |
|
261 |
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
|
262 |
apply (erule (1) lub_finch1) |
15562 | 263 |
done |
264 |
||
19621 | 265 |
lemma finch_imp_finite_range: "finite_chain Y \<Longrightarrow> finite (range Y)" |
27317 | 266 |
apply (erule finite_chainE) |
267 |
apply (rule_tac B="Y ` {..i}" in finite_subset) |
|
19621 | 268 |
apply (rule subsetI) |
269 |
apply (erule rangeE, rename_tac j) |
|
270 |
apply (rule_tac x=i and y=j in linorder_le_cases) |
|
271 |
apply (subgoal_tac "Y j = Y i", simp) |
|
272 |
apply (simp add: max_in_chain_def) |
|
273 |
apply simp |
|
27317 | 274 |
apply simp |
19621 | 275 |
done |
276 |
||
27317 | 277 |
lemma finite_range_has_max: |
278 |
fixes f :: "nat \<Rightarrow> 'a" and r :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
|
279 |
assumes mono: "\<And>i j. i \<le> j \<Longrightarrow> r (f i) (f j)" |
|
280 |
assumes finite_range: "finite (range f)" |
|
281 |
shows "\<exists>k. \<forall>i. r (f i) (f k)" |
|
282 |
proof (intro exI allI) |
|
283 |
fix i :: nat |
|
284 |
let ?j = "LEAST k. f k = f i" |
|
285 |
let ?k = "Max ((\<lambda>x. LEAST k. f k = x) ` range f)" |
|
286 |
have "?j \<le> ?k" |
|
287 |
proof (rule Max_ge) |
|
288 |
show "finite ((\<lambda>x. LEAST k. f k = x) ` range f)" |
|
289 |
using finite_range by (rule finite_imageI) |
|
290 |
show "?j \<in> (\<lambda>x. LEAST k. f k = x) ` range f" |
|
291 |
by (intro imageI rangeI) |
|
292 |
qed |
|
293 |
hence "r (f ?j) (f ?k)" |
|
294 |
by (rule mono) |
|
295 |
also have "f ?j = f i" |
|
296 |
by (rule LeastI, rule refl) |
|
297 |
finally show "r (f i) (f ?k)" . |
|
298 |
qed |
|
299 |
||
19621 | 300 |
lemma finite_range_imp_finch: |
301 |
"\<lbrakk>chain Y; finite (range Y)\<rbrakk> \<Longrightarrow> finite_chain Y" |
|
27317 | 302 |
apply (subgoal_tac "\<exists>k. \<forall>i. Y i \<sqsubseteq> Y k") |
303 |
apply (erule exE) |
|
304 |
apply (rule finite_chainI, assumption) |
|
305 |
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
|
306 |
apply (rule below_antisym) |
27317 | 307 |
apply (erule (1) chain_mono) |
308 |
apply (erule spec) |
|
309 |
apply (rule finite_range_has_max) |
|
310 |
apply (erule (1) chain_mono) |
|
311 |
apply assumption |
|
19621 | 312 |
done |
313 |
||
17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
314 |
lemma bin_chain: "x \<sqsubseteq> y \<Longrightarrow> chain (\<lambda>i. if i=0 then x else y)" |
31071 | 315 |
by (rule chainI, simp) |
17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
316 |
|
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
317 |
lemma bin_chainmax: |
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
318 |
"x \<sqsubseteq> y \<Longrightarrow> max_in_chain (Suc 0) (\<lambda>i. if i=0 then x else y)" |
31071 | 319 |
unfolding max_in_chain_def by simp |
15562 | 320 |
|
40771 | 321 |
lemma is_lub_bin_chain: |
17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
322 |
"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
|
323 |
apply (frule bin_chain) |
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
324 |
apply (drule bin_chainmax) |
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
325 |
apply (drule (1) lub_finch1) |
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
326 |
apply simp |
15562 | 327 |
done |
328 |
||
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
15562
diff
changeset
|
329 |
text {* the maximal element in a chain is its lub *} |
15562 | 330 |
|
17810
3bdf516d93d8
cleaned up; renamed "Porder.op <<" to "Porder.<<"
huffman
parents:
17372
diff
changeset
|
331 |
lemma lub_chain_maxelem: "\<lbrakk>Y i = c; \<forall>i. Y i \<sqsubseteq> c\<rbrakk> \<Longrightarrow> lub (range Y) = c" |
40771 | 332 |
by (blast dest: ub_rangeD intro: lub_eqI is_lubI ub_rangeI) |
15562 | 333 |
|
18071
940c2c0ff33a
cleaned up; chain_const and thelub_const are simp rules
huffman
parents:
17810
diff
changeset
|
334 |
end |
31071 | 335 |
|
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
|
336 |
end |