1 (* Title: HOLCF/Up.thy |
|
2 Author: Franz Regensburger |
|
3 Author: Brian Huffman |
|
4 *) |
|
5 |
|
6 header {* The type of lifted values *} |
|
7 |
|
8 theory Up |
|
9 imports Cfun |
|
10 begin |
|
11 |
|
12 default_sort cpo |
|
13 |
|
14 subsection {* Definition of new type for lifting *} |
|
15 |
|
16 datatype 'a u = Ibottom | Iup 'a |
|
17 |
|
18 type_notation (xsymbols) |
|
19 u ("(_\<^sub>\<bottom>)" [1000] 999) |
|
20 |
|
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" |
|
24 |
|
25 subsection {* Ordering on lifted cpo *} |
|
26 |
|
27 instantiation u :: (cpo) below |
|
28 begin |
|
29 |
|
30 definition |
|
31 below_up_def: |
|
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))" |
|
34 |
|
35 instance .. |
|
36 end |
|
37 |
|
38 lemma minimal_up [iff]: "Ibottom \<sqsubseteq> z" |
|
39 by (simp add: below_up_def) |
|
40 |
|
41 lemma not_Iup_below [iff]: "\<not> Iup x \<sqsubseteq> Ibottom" |
|
42 by (simp add: below_up_def) |
|
43 |
|
44 lemma Iup_below [iff]: "(Iup x \<sqsubseteq> Iup y) = (x \<sqsubseteq> y)" |
|
45 by (simp add: below_up_def) |
|
46 |
|
47 subsection {* Lifted cpo is a partial order *} |
|
48 |
|
49 instance u :: (cpo) po |
|
50 proof |
|
51 fix x :: "'a u" |
|
52 show "x \<sqsubseteq> x" |
|
53 unfolding below_up_def by (simp split: u.split) |
|
54 next |
|
55 fix x y :: "'a u" |
|
56 assume "x \<sqsubseteq> y" "y \<sqsubseteq> x" thus "x = y" |
|
57 unfolding below_up_def |
|
58 by (auto split: u.split_asm intro: below_antisym) |
|
59 next |
|
60 fix x y z :: "'a u" |
|
61 assume "x \<sqsubseteq> y" "y \<sqsubseteq> z" thus "x \<sqsubseteq> z" |
|
62 unfolding below_up_def |
|
63 by (auto split: u.split_asm intro: below_trans) |
|
64 qed |
|
65 |
|
66 subsection {* Lifted cpo is a cpo *} |
|
67 |
|
68 lemma is_lub_Iup: |
|
69 "range S <<| x \<Longrightarrow> range (\<lambda>i. Iup (S i)) <<| Iup x" |
|
70 unfolding is_lub_def is_ub_def ball_simps |
|
71 by (auto simp add: below_up_def split: u.split) |
|
72 |
|
73 lemma up_chain_lemma: |
|
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 |
|
105 |
|
106 instance u :: (cpo) cpo |
|
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" |
|
114 by (simp add: is_lub_const) |
|
115 thus ?thesis .. |
|
116 next |
|
117 fix A :: "nat \<Rightarrow> 'a" |
|
118 assume "range S <<| Iup (\<Squnion>i. A i)" |
|
119 thus ?thesis .. |
|
120 qed |
|
121 qed |
|
122 |
|
123 subsection {* Lifted cpo is pointed *} |
|
124 |
|
125 instance u :: (cpo) pcpo |
|
126 by intro_classes fast |
|
127 |
|
128 text {* for compatibility with old HOLCF-Version *} |
|
129 lemma inst_up_pcpo: "\<bottom> = Ibottom" |
|
130 by (rule minimal_up [THEN UU_I, symmetric]) |
|
131 |
|
132 subsection {* Continuity of \emph{Iup} and \emph{Ifup} *} |
|
133 |
|
134 text {* continuity for @{term Iup} *} |
|
135 |
|
136 lemma cont_Iup: "cont Iup" |
|
137 apply (rule contI) |
|
138 apply (rule is_lub_Iup) |
|
139 apply (erule cpo_lubI) |
|
140 done |
|
141 |
|
142 text {* continuity for @{term Ifup} *} |
|
143 |
|
144 lemma cont_Ifup1: "cont (\<lambda>f. Ifup f x)" |
|
145 by (induct x, simp_all) |
|
146 |
|
147 lemma monofun_Ifup2: "monofun (\<lambda>x. Ifup f x)" |
|
148 apply (rule monofunI) |
|
149 apply (case_tac x, simp) |
|
150 apply (case_tac y, simp) |
|
151 apply (simp add: monofun_cfun_arg) |
|
152 done |
|
153 |
|
154 lemma cont_Ifup2: "cont (\<lambda>x. Ifup f x)" |
|
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)))" |
|
163 by (simp add: lub_eqI contlub_cfun_arg) |
|
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) |
|
171 |
|
172 subsection {* Continuous versions of constants *} |
|
173 |
|
174 definition |
|
175 up :: "'a \<rightarrow> 'a u" where |
|
176 "up = (\<Lambda> x. Iup x)" |
|
177 |
|
178 definition |
|
179 fup :: "('a \<rightarrow> 'b::pcpo) \<rightarrow> 'a u \<rightarrow> 'b" where |
|
180 "fup = (\<Lambda> f p. Ifup f p)" |
|
181 |
|
182 translations |
|
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)" |
|
185 |
|
186 text {* continuous versions of lemmas for @{typ "('a)u"} *} |
|
187 |
|
188 lemma Exh_Up: "z = \<bottom> \<or> (\<exists>x. z = up\<cdot>x)" |
|
189 apply (induct z) |
|
190 apply (simp add: inst_up_pcpo) |
|
191 apply (simp add: up_def cont_Iup) |
|
192 done |
|
193 |
|
194 lemma up_eq [simp]: "(up\<cdot>x = up\<cdot>y) = (x = y)" |
|
195 by (simp add: up_def cont_Iup) |
|
196 |
|
197 lemma up_inject: "up\<cdot>x = up\<cdot>y \<Longrightarrow> x = y" |
|
198 by simp |
|
199 |
|
200 lemma up_defined [simp]: "up\<cdot>x \<noteq> \<bottom>" |
|
201 by (simp add: up_def cont_Iup inst_up_pcpo) |
|
202 |
|
203 lemma not_up_less_UU: "\<not> up\<cdot>x \<sqsubseteq> \<bottom>" |
|
204 by simp (* FIXME: remove? *) |
|
205 |
|
206 lemma up_below [simp]: "up\<cdot>x \<sqsubseteq> up\<cdot>y \<longleftrightarrow> x \<sqsubseteq> y" |
|
207 by (simp add: up_def cont_Iup) |
|
208 |
|
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" |
|
211 apply (cases p) |
|
212 apply (simp add: inst_up_pcpo) |
|
213 apply (simp add: up_def cont_Iup) |
|
214 done |
|
215 |
|
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" |
|
218 by (cases x, simp_all) |
|
219 |
|
220 text {* lifting preserves chain-finiteness *} |
|
221 |
|
222 lemma up_chain_cases: |
|
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]) |
|
226 apply (simp_all add: inst_up_pcpo up_def cont_Iup lub_eqI) |
|
227 done |
|
228 |
|
229 lemma compact_up: "compact x \<Longrightarrow> compact (up\<cdot>x)" |
|
230 apply (rule compactI2) |
|
231 apply (erule up_chain_cases) |
|
232 apply simp |
|
233 apply (drule (1) compactD2, simp) |
|
234 apply (erule exE) |
|
235 apply (drule_tac f="up" and x="x" in monofun_cfun_arg) |
|
236 apply (simp, erule exI) |
|
237 done |
|
238 |
|
239 lemma compact_upD: "compact (up\<cdot>x) \<Longrightarrow> compact x" |
|
240 unfolding compact_def |
|
241 by (drule adm_subst [OF cont_Rep_cfun2 [where f=up]], simp) |
|
242 |
|
243 lemma compact_up_iff [simp]: "compact (up\<cdot>x) = compact x" |
|
244 by (safe elim!: compact_up compact_upD) |
|
245 |
|
246 instance u :: (chfin) chfin |
|
247 apply intro_classes |
|
248 apply (erule compact_imp_max_in_chain) |
|
249 apply (rule_tac p="\<Squnion>i. Y i" in upE, simp_all) |
|
250 done |
|
251 |
|
252 text {* properties of fup *} |
|
253 |
|
254 lemma fup1 [simp]: "fup\<cdot>f\<cdot>\<bottom> = \<bottom>" |
|
255 by (simp add: fup_def cont_Ifup1 cont_Ifup2 inst_up_pcpo cont2cont_LAM) |
|
256 |
|
257 lemma fup2 [simp]: "fup\<cdot>f\<cdot>(up\<cdot>x) = f\<cdot>x" |
|
258 by (simp add: up_def fup_def cont_Iup cont_Ifup1 cont_Ifup2 cont2cont_LAM) |
|
259 |
|
260 lemma fup3 [simp]: "fup\<cdot>up\<cdot>x = x" |
|
261 by (cases x, simp_all) |
|
262 |
|
263 end |
|