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