author | huffman |
Sat, 27 Nov 2010 16:08:10 -0800 | |
changeset 40774 | 0437dbc127b3 |
parent 40771 | src/HOLCF/Up.thy@1c6f7d4b110e |
child 41182 | 717404c7d59a |
permissions | -rw-r--r-- |
15599
10cedbd5289e
instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents:
15593
diff
changeset
|
1 |
(* Title: HOLCF/Up.thy |
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
40327
diff
changeset
|
2 |
Author: Franz Regensburger |
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
40327
diff
changeset
|
3 |
Author: Brian Huffman |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
4 |
*) |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
5 |
|
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
6 |
header {* The type of lifted values *} |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
7 |
|
15577 | 8 |
theory Up |
40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
40327
diff
changeset
|
9 |
imports Cfun |
15577 | 10 |
begin |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
11 |
|
36452 | 12 |
default_sort cpo |
15599
10cedbd5289e
instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents:
15593
diff
changeset
|
13 |
|
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
14 |
subsection {* Definition of new type for lifting *} |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
15 |
|
16753 | 16 |
datatype 'a u = Ibottom | Iup 'a |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
17 |
|
35427 | 18 |
type_notation (xsymbols) |
19 |
u ("(_\<^sub>\<bottom>)" [1000] 999) |
|
18290 | 20 |
|
34941 | 21 |
primrec Ifup :: "('a \<rightarrow> 'b::pcpo) \<Rightarrow> 'a u \<Rightarrow> 'b" where |
22 |
"Ifup f Ibottom = \<bottom>" |
|
23 |
| "Ifup f (Iup x) = f\<cdot>x" |
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
24 |
|
18290 | 25 |
subsection {* Ordering on lifted cpo *} |
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
26 |
|
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents:
29530
diff
changeset
|
27 |
instantiation u :: (cpo) below |
25787 | 28 |
begin |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
29 |
|
25787 | 30 |
definition |
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents:
29530
diff
changeset
|
31 |
below_up_def: |
16753 | 32 |
"(op \<sqsubseteq>) \<equiv> (\<lambda>x y. case x of Ibottom \<Rightarrow> True | Iup a \<Rightarrow> |
33 |
(case y of Ibottom \<Rightarrow> False | Iup b \<Rightarrow> a \<sqsubseteq> b))" |
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
34 |
|
25787 | 35 |
instance .. |
36 |
end |
|
37 |
||
16753 | 38 |
lemma minimal_up [iff]: "Ibottom \<sqsubseteq> z" |
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents:
29530
diff
changeset
|
39 |
by (simp add: below_up_def) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
40 |
|
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents:
29530
diff
changeset
|
41 |
lemma not_Iup_below [iff]: "\<not> Iup x \<sqsubseteq> Ibottom" |
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents:
29530
diff
changeset
|
42 |
by (simp add: below_up_def) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
43 |
|
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents:
29530
diff
changeset
|
44 |
lemma Iup_below [iff]: "(Iup x \<sqsubseteq> Iup y) = (x \<sqsubseteq> y)" |
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents:
29530
diff
changeset
|
45 |
by (simp add: below_up_def) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
46 |
|
18290 | 47 |
subsection {* Lifted cpo is a partial order *} |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
48 |
|
15599
10cedbd5289e
instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents:
15593
diff
changeset
|
49 |
instance u :: (cpo) po |
25787 | 50 |
proof |
51 |
fix x :: "'a u" |
|
52 |
show "x \<sqsubseteq> x" |
|
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents:
29530
diff
changeset
|
53 |
unfolding below_up_def by (simp split: u.split) |
25787 | 54 |
next |
55 |
fix x y :: "'a u" |
|
56 |
assume "x \<sqsubseteq> y" "y \<sqsubseteq> x" thus "x = y" |
|
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents:
29530
diff
changeset
|
57 |
unfolding below_up_def |
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents:
29530
diff
changeset
|
58 |
by (auto split: u.split_asm intro: below_antisym) |
25787 | 59 |
next |
60 |
fix x y z :: "'a u" |
|
61 |
assume "x \<sqsubseteq> y" "y \<sqsubseteq> z" thus "x \<sqsubseteq> z" |
|
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents:
29530
diff
changeset
|
62 |
unfolding below_up_def |
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents:
29530
diff
changeset
|
63 |
by (auto split: u.split_asm intro: below_trans) |
25787 | 64 |
qed |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
65 |
|
18290 | 66 |
subsection {* Lifted cpo is a cpo *} |
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
67 |
|
16319
1ff2965cc2e7
major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents:
16215
diff
changeset
|
68 |
lemma is_lub_Iup: |
1ff2965cc2e7
major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents:
16215
diff
changeset
|
69 |
"range S <<| x \<Longrightarrow> range (\<lambda>i. Iup (S i)) <<| Iup x" |
40084 | 70 |
unfolding is_lub_def is_ub_def ball_simps |
71 |
by (auto simp add: below_up_def split: u.split) |
|
15599
10cedbd5289e
instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents:
15593
diff
changeset
|
72 |
|
17838 | 73 |
lemma up_chain_lemma: |
40084 | 74 |
assumes Y: "chain Y" obtains "\<forall>i. Y i = Ibottom" |
75 |
| A k where "\<forall>i. Iup (A i) = Y (i + k)" and "chain A" and "range Y <<| Iup (\<Squnion>i. A i)" |
|
76 |
proof (cases "\<exists>k. Y k \<noteq> Ibottom") |
|
77 |
case True |
|
78 |
then obtain k where k: "Y k \<noteq> Ibottom" .. |
|
79 |
def A \<equiv> "\<lambda>i. THE a. Iup a = Y (i + k)" |
|
80 |
have Iup_A: "\<forall>i. Iup (A i) = Y (i + k)" |
|
81 |
proof |
|
82 |
fix i :: nat |
|
83 |
from Y le_add2 have "Y k \<sqsubseteq> Y (i + k)" by (rule chain_mono) |
|
84 |
with k have "Y (i + k) \<noteq> Ibottom" by (cases "Y k", auto) |
|
85 |
thus "Iup (A i) = Y (i + k)" |
|
86 |
by (cases "Y (i + k)", simp_all add: A_def) |
|
87 |
qed |
|
88 |
from Y have chain_A: "chain A" |
|
89 |
unfolding chain_def Iup_below [symmetric] |
|
90 |
by (simp add: Iup_A) |
|
91 |
hence "range A <<| (\<Squnion>i. A i)" |
|
92 |
by (rule cpo_lubI) |
|
93 |
hence "range (\<lambda>i. Iup (A i)) <<| Iup (\<Squnion>i. A i)" |
|
94 |
by (rule is_lub_Iup) |
|
95 |
hence "range (\<lambda>i. Y (i + k)) <<| Iup (\<Squnion>i. A i)" |
|
96 |
by (simp only: Iup_A) |
|
97 |
hence "range (\<lambda>i. Y i) <<| Iup (\<Squnion>i. A i)" |
|
98 |
by (simp only: is_lub_range_shift [OF Y]) |
|
99 |
with Iup_A chain_A show ?thesis .. |
|
100 |
next |
|
101 |
case False |
|
102 |
then have "\<forall>i. Y i = Ibottom" by simp |
|
103 |
then show ?thesis .. |
|
104 |
qed |
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
105 |
|
15599
10cedbd5289e
instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents:
15593
diff
changeset
|
106 |
instance u :: (cpo) cpo |
40084 | 107 |
proof |
108 |
fix S :: "nat \<Rightarrow> 'a u" |
|
109 |
assume S: "chain S" |
|
110 |
thus "\<exists>x. range (\<lambda>i. S i) <<| x" |
|
111 |
proof (rule up_chain_lemma) |
|
112 |
assume "\<forall>i. S i = Ibottom" |
|
113 |
hence "range (\<lambda>i. S i) <<| Ibottom" |
|
40771 | 114 |
by (simp add: is_lub_const) |
40084 | 115 |
thus ?thesis .. |
116 |
next |
|
40085 | 117 |
fix A :: "nat \<Rightarrow> 'a" |
118 |
assume "range S <<| Iup (\<Squnion>i. A i)" |
|
40084 | 119 |
thus ?thesis .. |
120 |
qed |
|
121 |
qed |
|
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
122 |
|
18290 | 123 |
subsection {* Lifted cpo is pointed *} |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
124 |
|
15599
10cedbd5289e
instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents:
15593
diff
changeset
|
125 |
instance u :: (cpo) pcpo |
40084 | 126 |
by intro_classes fast |
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
127 |
|
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
128 |
text {* for compatibility with old HOLCF-Version *} |
16753 | 129 |
lemma inst_up_pcpo: "\<bottom> = Ibottom" |
16319
1ff2965cc2e7
major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents:
16215
diff
changeset
|
130 |
by (rule minimal_up [THEN UU_I, symmetric]) |
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
131 |
|
35900
aa5dfb03eb1e
remove LaTeX hyperref warnings by avoiding antiquotations within section headings
huffman
parents:
35783
diff
changeset
|
132 |
subsection {* Continuity of \emph{Iup} and \emph{Ifup} *} |
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
133 |
|
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
134 |
text {* continuity for @{term Iup} *} |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
135 |
|
16319
1ff2965cc2e7
major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents:
16215
diff
changeset
|
136 |
lemma cont_Iup: "cont Iup" |
16215 | 137 |
apply (rule contI) |
15599
10cedbd5289e
instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
huffman
parents:
15593
diff
changeset
|
138 |
apply (rule is_lub_Iup) |
26027 | 139 |
apply (erule cpo_lubI) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
140 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
141 |
|
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
142 |
text {* continuity for @{term Ifup} *} |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
143 |
|
16319
1ff2965cc2e7
major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents:
16215
diff
changeset
|
144 |
lemma cont_Ifup1: "cont (\<lambda>f. Ifup f x)" |
16753 | 145 |
by (induct x, simp_all) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
146 |
|
16319
1ff2965cc2e7
major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents:
16215
diff
changeset
|
147 |
lemma monofun_Ifup2: "monofun (\<lambda>x. Ifup f x)" |
1ff2965cc2e7
major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents:
16215
diff
changeset
|
148 |
apply (rule monofunI) |
16753 | 149 |
apply (case_tac x, simp) |
150 |
apply (case_tac y, simp) |
|
16319
1ff2965cc2e7
major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents:
16215
diff
changeset
|
151 |
apply (simp add: monofun_cfun_arg) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
152 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
153 |
|
16319
1ff2965cc2e7
major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents:
16215
diff
changeset
|
154 |
lemma cont_Ifup2: "cont (\<lambda>x. Ifup f x)" |
40084 | 155 |
proof (rule contI2) |
156 |
fix Y assume Y: "chain Y" and Y': "chain (\<lambda>i. Ifup f (Y i))" |
|
157 |
from Y show "Ifup f (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. Ifup f (Y i))" |
|
158 |
proof (rule up_chain_lemma) |
|
159 |
fix A and k |
|
160 |
assume A: "\<forall>i. Iup (A i) = Y (i + k)" |
|
161 |
assume "chain A" and "range Y <<| Iup (\<Squnion>i. A i)" |
|
162 |
hence "Ifup f (\<Squnion>i. Y i) = (\<Squnion>i. Ifup f (Iup (A i)))" |
|
40771 | 163 |
by (simp add: lub_eqI contlub_cfun_arg) |
40084 | 164 |
also have "\<dots> = (\<Squnion>i. Ifup f (Y (i + k)))" |
165 |
by (simp add: A) |
|
166 |
also have "\<dots> = (\<Squnion>i. Ifup f (Y i))" |
|
167 |
using Y' by (rule lub_range_shift) |
|
168 |
finally show ?thesis by simp |
|
169 |
qed simp |
|
170 |
qed (rule monofun_Ifup2) |
|
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
171 |
|
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
172 |
subsection {* Continuous versions of constants *} |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
173 |
|
25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19105
diff
changeset
|
174 |
definition |
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19105
diff
changeset
|
175 |
up :: "'a \<rightarrow> 'a u" where |
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19105
diff
changeset
|
176 |
"up = (\<Lambda> x. Iup x)" |
16319
1ff2965cc2e7
major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents:
16215
diff
changeset
|
177 |
|
25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19105
diff
changeset
|
178 |
definition |
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19105
diff
changeset
|
179 |
fup :: "('a \<rightarrow> 'b::pcpo) \<rightarrow> 'a u \<rightarrow> 'b" where |
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19105
diff
changeset
|
180 |
"fup = (\<Lambda> f p. Ifup f p)" |
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
181 |
|
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
182 |
translations |
26046 | 183 |
"case l of XCONST up\<cdot>x \<Rightarrow> t" == "CONST fup\<cdot>(\<Lambda> x. t)\<cdot>l" |
184 |
"\<Lambda>(XCONST up\<cdot>x). t" == "CONST fup\<cdot>(\<Lambda> x. t)" |
|
15593
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
185 |
|
24d770bbc44a
reordered and arranged for document generation, cleaned up some proofs
huffman
parents:
15577
diff
changeset
|
186 |
text {* continuous versions of lemmas for @{typ "('a)u"} *} |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
187 |
|
16753 | 188 |
lemma Exh_Up: "z = \<bottom> \<or> (\<exists>x. z = up\<cdot>x)" |
189 |
apply (induct z) |
|
16319
1ff2965cc2e7
major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents:
16215
diff
changeset
|
190 |
apply (simp add: inst_up_pcpo) |
1ff2965cc2e7
major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents:
16215
diff
changeset
|
191 |
apply (simp add: up_def cont_Iup) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
192 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
193 |
|
16753 | 194 |
lemma up_eq [simp]: "(up\<cdot>x = up\<cdot>y) = (x = y)" |
16319
1ff2965cc2e7
major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents:
16215
diff
changeset
|
195 |
by (simp add: up_def cont_Iup) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
196 |
|
16753 | 197 |
lemma up_inject: "up\<cdot>x = up\<cdot>y \<Longrightarrow> x = y" |
198 |
by simp |
|
16319
1ff2965cc2e7
major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents:
16215
diff
changeset
|
199 |
|
17838 | 200 |
lemma up_defined [simp]: "up\<cdot>x \<noteq> \<bottom>" |
16319
1ff2965cc2e7
major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents:
16215
diff
changeset
|
201 |
by (simp add: up_def cont_Iup inst_up_pcpo) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
202 |
|
25785 | 203 |
lemma not_up_less_UU: "\<not> up\<cdot>x \<sqsubseteq> \<bottom>" |
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents:
29530
diff
changeset
|
204 |
by simp (* FIXME: remove? *) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
205 |
|
31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
huffman
parents:
29530
diff
changeset
|
206 |
lemma up_below [simp]: "up\<cdot>x \<sqsubseteq> up\<cdot>y \<longleftrightarrow> x \<sqsubseteq> y" |
16319
1ff2965cc2e7
major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents:
16215
diff
changeset
|
207 |
by (simp add: up_def cont_Iup) |
1ff2965cc2e7
major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents:
16215
diff
changeset
|
208 |
|
35783 | 209 |
lemma upE [case_names bottom up, cases type: u]: |
210 |
"\<lbrakk>p = \<bottom> \<Longrightarrow> Q; \<And>x. p = up\<cdot>x \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q" |
|
25788
30cbe0764599
declare upE as cases rule; add new rule up_induct
huffman
parents:
25787
diff
changeset
|
211 |
apply (cases p) |
16319
1ff2965cc2e7
major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents:
16215
diff
changeset
|
212 |
apply (simp add: inst_up_pcpo) |
1ff2965cc2e7
major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents:
16215
diff
changeset
|
213 |
apply (simp add: up_def cont_Iup) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
214 |
done |
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
215 |
|
35783 | 216 |
lemma up_induct [case_names bottom up, induct type: u]: |
217 |
"\<lbrakk>P \<bottom>; \<And>x. P (up\<cdot>x)\<rbrakk> \<Longrightarrow> P x" |
|
25788
30cbe0764599
declare upE as cases rule; add new rule up_induct
huffman
parents:
25787
diff
changeset
|
218 |
by (cases x, simp_all) |
30cbe0764599
declare upE as cases rule; add new rule up_induct
huffman
parents:
25787
diff
changeset
|
219 |
|
25827
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25789
diff
changeset
|
220 |
text {* lifting preserves chain-finiteness *} |
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25789
diff
changeset
|
221 |
|
17838 | 222 |
lemma up_chain_cases: |
40084 | 223 |
assumes Y: "chain Y" obtains "\<forall>i. Y i = \<bottom>" |
224 |
| A k where "\<forall>i. up\<cdot>(A i) = Y (i + k)" and "chain A" and "(\<Squnion>i. Y i) = up\<cdot>(\<Squnion>i. A i)" |
|
225 |
apply (rule up_chain_lemma [OF Y]) |
|
40771 | 226 |
apply (simp_all add: inst_up_pcpo up_def cont_Iup lub_eqI) |
40084 | 227 |
done |
17838 | 228 |
|
25879 | 229 |
lemma compact_up: "compact x \<Longrightarrow> compact (up\<cdot>x)" |
230 |
apply (rule compactI2) |
|
40084 | 231 |
apply (erule up_chain_cases) |
232 |
apply simp |
|
25879 | 233 |
apply (drule (1) compactD2, simp) |
40084 | 234 |
apply (erule exE) |
235 |
apply (drule_tac f="up" and x="x" in monofun_cfun_arg) |
|
236 |
apply (simp, erule exI) |
|
25879 | 237 |
done |
238 |
||
239 |
lemma compact_upD: "compact (up\<cdot>x) \<Longrightarrow> compact x" |
|
240 |
unfolding compact_def |
|
40327 | 241 |
by (drule adm_subst [OF cont_Rep_cfun2 [where f=up]], simp) |
25879 | 242 |
|
243 |
lemma compact_up_iff [simp]: "compact (up\<cdot>x) = compact x" |
|
244 |
by (safe elim!: compact_up compact_upD) |
|
245 |
||
25827
c2adeb1bae5c
new instance proofs for classes finite_po, chfin, flat
huffman
parents:
25789
diff
changeset
|
246 |
instance u :: (chfin) chfin |
25921 | 247 |
apply intro_classes |
25879 | 248 |
apply (erule compact_imp_max_in_chain) |
25898 | 249 |
apply (rule_tac p="\<Squnion>i. Y i" in upE, simp_all) |
17838 | 250 |
done |
251 |
||
252 |
text {* properties of fup *} |
|
253 |
||
16319
1ff2965cc2e7
major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents:
16215
diff
changeset
|
254 |
lemma fup1 [simp]: "fup\<cdot>f\<cdot>\<bottom> = \<bottom>" |
29530
9905b660612b
change to simpler, more extensible continuity simproc
huffman
parents:
29138
diff
changeset
|
255 |
by (simp add: fup_def cont_Ifup1 cont_Ifup2 inst_up_pcpo cont2cont_LAM) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
256 |
|
16319
1ff2965cc2e7
major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
huffman
parents:
16215
diff
changeset
|
257 |
lemma fup2 [simp]: "fup\<cdot>f\<cdot>(up\<cdot>x) = f\<cdot>x" |
29530
9905b660612b
change to simpler, more extensible continuity simproc
huffman
parents:
29138
diff
changeset
|
258 |
by (simp add: up_def fup_def cont_Iup cont_Ifup1 cont_Ifup2 cont2cont_LAM) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
259 |
|
16553 | 260 |
lemma fup3 [simp]: "fup\<cdot>up\<cdot>x = x" |
25788
30cbe0764599
declare upE as cases rule; add new rule up_induct
huffman
parents:
25787
diff
changeset
|
261 |
by (cases x, simp_all) |
15576
efb95d0d01f7
converted to new-style theories, and combined numbered files
huffman
parents:
diff
changeset
|
262 |
|
26962
c8b20f615d6c
use new class package for classes profinite, bifinite; remove approx class
huffman
parents:
26407
diff
changeset
|
263 |
end |