author | huffman |
Mon, 04 Oct 2010 06:45:57 -0700 | |
changeset 39968 | d841744718fe |
parent 39966 | 20c74cf9c112 |
child 40771 | 1c6f7d4b110e |
permissions | -rw-r--r-- |
39143 | 1 |
(* Title: HOLCF/Library/List_Cpo.thy |
2 |
Author: Brian Huffman |
|
3 |
*) |
|
4 |
||
5 |
header {* Lists as a complete partial order *} |
|
6 |
||
7 |
theory List_Cpo |
|
8 |
imports HOLCF |
|
9 |
begin |
|
10 |
||
11 |
subsection {* Lists are a partial order *} |
|
12 |
||
13 |
instantiation list :: (po) po |
|
14 |
begin |
|
15 |
||
16 |
definition |
|
17 |
"xs \<sqsubseteq> ys \<longleftrightarrow> list_all2 (op \<sqsubseteq>) xs ys" |
|
18 |
||
19 |
instance proof |
|
20 |
fix xs :: "'a list" |
|
21 |
from below_refl show "xs \<sqsubseteq> xs" |
|
22 |
unfolding below_list_def |
|
23 |
by (rule list_all2_refl) |
|
24 |
next |
|
25 |
fix xs ys zs :: "'a list" |
|
26 |
assume "xs \<sqsubseteq> ys" and "ys \<sqsubseteq> zs" |
|
27 |
with below_trans show "xs \<sqsubseteq> zs" |
|
28 |
unfolding below_list_def |
|
29 |
by (rule list_all2_trans) |
|
30 |
next |
|
31 |
fix xs ys zs :: "'a list" |
|
32 |
assume "xs \<sqsubseteq> ys" and "ys \<sqsubseteq> xs" |
|
33 |
with below_antisym show "xs = ys" |
|
34 |
unfolding below_list_def |
|
35 |
by (rule list_all2_antisym) |
|
36 |
qed |
|
37 |
||
38 |
end |
|
39 |
||
40 |
lemma below_list_simps [simp]: |
|
41 |
"[] \<sqsubseteq> []" |
|
42 |
"x # xs \<sqsubseteq> y # ys \<longleftrightarrow> x \<sqsubseteq> y \<and> xs \<sqsubseteq> ys" |
|
43 |
"\<not> [] \<sqsubseteq> y # ys" |
|
44 |
"\<not> x # xs \<sqsubseteq> []" |
|
45 |
by (simp_all add: below_list_def) |
|
46 |
||
47 |
lemma Nil_below_iff [simp]: "[] \<sqsubseteq> xs \<longleftrightarrow> xs = []" |
|
48 |
by (cases xs, simp_all) |
|
49 |
||
50 |
lemma below_Nil_iff [simp]: "xs \<sqsubseteq> [] \<longleftrightarrow> xs = []" |
|
51 |
by (cases xs, simp_all) |
|
52 |
||
39966 | 53 |
lemma list_below_induct [consumes 1, case_names Nil Cons]: |
54 |
assumes "xs \<sqsubseteq> ys" |
|
55 |
assumes 1: "P [] []" |
|
56 |
assumes 2: "\<And>x y xs ys. \<lbrakk>x \<sqsubseteq> y; xs \<sqsubseteq> ys; P xs ys\<rbrakk> \<Longrightarrow> P (x # xs) (y # ys)" |
|
57 |
shows "P xs ys" |
|
58 |
using `xs \<sqsubseteq> ys` |
|
59 |
proof (induct xs arbitrary: ys) |
|
60 |
case Nil thus ?case by (simp add: 1) |
|
61 |
next |
|
62 |
case (Cons x xs) thus ?case by (cases ys, simp_all add: 2) |
|
63 |
qed |
|
64 |
||
65 |
lemma list_below_cases: |
|
66 |
assumes "xs \<sqsubseteq> ys" |
|
67 |
obtains "xs = []" and "ys = []" | |
|
68 |
x y xs' ys' where "xs = x # xs'" and "ys = y # ys'" |
|
69 |
using assms by (cases xs, simp, cases ys, auto) |
|
70 |
||
39143 | 71 |
text "Thanks to Joachim Breitner" |
72 |
||
73 |
lemma list_Cons_below: |
|
74 |
assumes "a # as \<sqsubseteq> xs" |
|
75 |
obtains b and bs where "a \<sqsubseteq> b" and "as \<sqsubseteq> bs" and "xs = b # bs" |
|
76 |
using assms by (cases xs, auto) |
|
77 |
||
78 |
lemma list_below_Cons: |
|
79 |
assumes "xs \<sqsubseteq> b # bs" |
|
80 |
obtains a and as where "a \<sqsubseteq> b" and "as \<sqsubseteq> bs" and "xs = a # as" |
|
81 |
using assms by (cases xs, auto) |
|
82 |
||
83 |
lemma hd_mono: "xs \<sqsubseteq> ys \<Longrightarrow> hd xs \<sqsubseteq> hd ys" |
|
84 |
by (cases xs, simp, cases ys, simp, simp) |
|
85 |
||
86 |
lemma tl_mono: "xs \<sqsubseteq> ys \<Longrightarrow> tl xs \<sqsubseteq> tl ys" |
|
87 |
by (cases xs, simp, cases ys, simp, simp) |
|
88 |
||
89 |
lemma ch2ch_hd [simp]: "chain (\<lambda>i. S i) \<Longrightarrow> chain (\<lambda>i. hd (S i))" |
|
90 |
by (rule chainI, rule hd_mono, erule chainE) |
|
91 |
||
92 |
lemma ch2ch_tl [simp]: "chain (\<lambda>i. S i) \<Longrightarrow> chain (\<lambda>i. tl (S i))" |
|
93 |
by (rule chainI, rule tl_mono, erule chainE) |
|
94 |
||
95 |
lemma below_same_length: "xs \<sqsubseteq> ys \<Longrightarrow> length xs = length ys" |
|
96 |
unfolding below_list_def by (rule list_all2_lengthD) |
|
97 |
||
39966 | 98 |
lemma list_chain_induct [consumes 1, case_names Nil Cons]: |
99 |
assumes "chain S" |
|
100 |
assumes 1: "P (\<lambda>i. [])" |
|
101 |
assumes 2: "\<And>A B. chain A \<Longrightarrow> chain B \<Longrightarrow> P B \<Longrightarrow> P (\<lambda>i. A i # B i)" |
|
102 |
shows "P S" |
|
103 |
using `chain S` |
|
104 |
proof (induct "S 0" arbitrary: S) |
|
105 |
case Nil |
|
106 |
have "\<forall>i. S 0 \<sqsubseteq> S i" by (simp add: chain_mono [OF `chain S`]) |
|
107 |
with Nil have "\<forall>i. S i = []" by simp |
|
108 |
thus ?case by (simp add: 1) |
|
109 |
next |
|
110 |
case (Cons x xs) |
|
111 |
have "\<forall>i. S 0 \<sqsubseteq> S i" by (simp add: chain_mono [OF `chain S`]) |
|
112 |
hence *: "\<forall>i. S i \<noteq> []" by (rule all_forward, insert Cons) auto |
|
113 |
have "chain (\<lambda>i. hd (S i))" and "chain (\<lambda>i. tl (S i))" |
|
114 |
using `chain S` by simp_all |
|
115 |
moreover have "P (\<lambda>i. tl (S i))" |
|
116 |
using `chain S` and `x # xs = S 0` [symmetric] |
|
117 |
by (simp add: Cons(1)) |
|
118 |
ultimately have "P (\<lambda>i. hd (S i) # tl (S i))" |
|
119 |
by (rule 2) |
|
120 |
thus "P S" by (simp add: *) |
|
121 |
qed |
|
122 |
||
39143 | 123 |
lemma list_chain_cases: |
124 |
assumes S: "chain S" |
|
39966 | 125 |
obtains "S = (\<lambda>i. [])" | |
126 |
A B where "chain A" and "chain B" and "S = (\<lambda>i. A i # B i)" |
|
127 |
using S by (induct rule: list_chain_induct) simp_all |
|
39143 | 128 |
|
129 |
subsection {* Lists are a complete partial order *} |
|
130 |
||
131 |
lemma is_lub_Cons: |
|
132 |
assumes A: "range A <<| x" |
|
133 |
assumes B: "range B <<| xs" |
|
134 |
shows "range (\<lambda>i. A i # B i) <<| x # xs" |
|
135 |
using assms |
|
39968 | 136 |
unfolding is_lub_def is_ub_def |
39143 | 137 |
by (clarsimp, case_tac u, simp_all) |
138 |
||
139 |
instance list :: (cpo) cpo |
|
140 |
proof |
|
141 |
fix S :: "nat \<Rightarrow> 'a list" |
|
39966 | 142 |
assume "chain S" thus "\<exists>x. range S <<| x" |
143 |
proof (induct rule: list_chain_induct) |
|
144 |
case Nil thus ?case by (auto intro: lub_const) |
|
145 |
next |
|
146 |
case (Cons A B) thus ?case by (auto intro: is_lub_Cons cpo_lubI) |
|
147 |
qed |
|
39143 | 148 |
qed |
149 |
||
150 |
subsection {* Continuity of list operations *} |
|
151 |
||
152 |
lemma cont2cont_Cons [simp, cont2cont]: |
|
153 |
assumes f: "cont (\<lambda>x. f x)" |
|
154 |
assumes g: "cont (\<lambda>x. g x)" |
|
155 |
shows "cont (\<lambda>x. f x # g x)" |
|
156 |
apply (rule contI) |
|
157 |
apply (rule is_lub_Cons) |
|
158 |
apply (erule contE [OF f]) |
|
159 |
apply (erule contE [OF g]) |
|
160 |
done |
|
161 |
||
162 |
lemma lub_Cons: |
|
163 |
fixes A :: "nat \<Rightarrow> 'a::cpo" |
|
164 |
assumes A: "chain A" and B: "chain B" |
|
165 |
shows "(\<Squnion>i. A i # B i) = (\<Squnion>i. A i) # (\<Squnion>i. B i)" |
|
166 |
by (intro thelubI is_lub_Cons cpo_lubI A B) |
|
167 |
||
168 |
lemma cont2cont_list_case: |
|
169 |
assumes f: "cont (\<lambda>x. f x)" |
|
170 |
assumes g: "cont (\<lambda>x. g x)" |
|
171 |
assumes h1: "\<And>y ys. cont (\<lambda>x. h x y ys)" |
|
172 |
assumes h2: "\<And>x ys. cont (\<lambda>y. h x y ys)" |
|
173 |
assumes h3: "\<And>x y. cont (\<lambda>ys. h x y ys)" |
|
174 |
shows "cont (\<lambda>x. case f x of [] \<Rightarrow> g x | y # ys \<Rightarrow> h x y ys)" |
|
175 |
apply (rule cont_apply [OF f]) |
|
176 |
apply (rule contI) |
|
177 |
apply (erule list_chain_cases) |
|
178 |
apply (simp add: lub_const) |
|
179 |
apply (simp add: lub_Cons) |
|
180 |
apply (simp add: cont2contlubE [OF h2]) |
|
181 |
apply (simp add: cont2contlubE [OF h3]) |
|
182 |
apply (simp add: diag_lub ch2ch_cont [OF h2] ch2ch_cont [OF h3]) |
|
183 |
apply (rule cpo_lubI, rule chainI, rule below_trans) |
|
184 |
apply (erule cont2monofunE [OF h2 chainE]) |
|
185 |
apply (erule cont2monofunE [OF h3 chainE]) |
|
186 |
apply (case_tac y, simp_all add: g h1) |
|
187 |
done |
|
188 |
||
189 |
lemma cont2cont_list_case' [simp, cont2cont]: |
|
190 |
assumes f: "cont (\<lambda>x. f x)" |
|
191 |
assumes g: "cont (\<lambda>x. g x)" |
|
192 |
assumes h: "cont (\<lambda>p. h (fst p) (fst (snd p)) (snd (snd p)))" |
|
193 |
shows "cont (\<lambda>x. case f x of [] \<Rightarrow> g x | y # ys \<Rightarrow> h x y ys)" |
|
39808
1410c84013b9
rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs
huffman
parents:
39302
diff
changeset
|
194 |
using assms by (simp add: cont2cont_list_case prod_cont_iff) |
39143 | 195 |
|
196 |
text {* The simple version (due to Joachim Breitner) is needed if the |
|
197 |
element type of the list is not a cpo. *} |
|
198 |
||
199 |
lemma cont2cont_list_case_simple [simp, cont2cont]: |
|
200 |
assumes "cont (\<lambda>x. f1 x)" |
|
201 |
assumes "\<And>y ys. cont (\<lambda>x. f2 x y ys)" |
|
202 |
shows "cont (\<lambda>x. case l of [] \<Rightarrow> f1 x | y # ys \<Rightarrow> f2 x y ys)" |
|
203 |
using assms by (cases l) auto |
|
204 |
||
39966 | 205 |
text {* Lemma for proving continuity of recursive list functions: *} |
206 |
||
207 |
lemma list_contI: |
|
208 |
fixes f :: "'a::cpo list \<Rightarrow> 'b::cpo" |
|
209 |
assumes f: "\<And>x xs. f (x # xs) = g x xs (f xs)" |
|
210 |
assumes g1: "\<And>xs y. cont (\<lambda>x. g x xs y)" |
|
211 |
assumes g2: "\<And>x y. cont (\<lambda>xs. g x xs y)" |
|
212 |
assumes g3: "\<And>x xs. cont (\<lambda>y. g x xs y)" |
|
213 |
shows "cont f" |
|
214 |
proof (rule contI2) |
|
215 |
obtain h where h: "\<And>x xs y. g x xs y = h\<cdot>x\<cdot>xs\<cdot>y" |
|
216 |
proof |
|
217 |
fix x xs y show "g x xs y = (\<Lambda> x xs y. g x xs y)\<cdot>x\<cdot>xs\<cdot>y" |
|
218 |
by (simp add: cont2cont_LAM g1 g2 g3) |
|
219 |
qed |
|
220 |
show mono: "monofun f" |
|
221 |
apply (rule monofunI) |
|
222 |
apply (erule list_below_induct) |
|
223 |
apply simp |
|
224 |
apply (simp add: f h monofun_cfun) |
|
225 |
done |
|
226 |
fix Y :: "nat \<Rightarrow> 'a list" |
|
227 |
assume "chain Y" thus "f (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. f (Y i))" |
|
228 |
apply (induct rule: list_chain_induct) |
|
229 |
apply simp |
|
230 |
apply (simp add: lub_Cons f h) |
|
231 |
apply (simp add: contlub_cfun [symmetric] ch2ch_monofun [OF mono]) |
|
232 |
apply (simp add: monofun_cfun) |
|
233 |
done |
|
234 |
qed |
|
235 |
||
39143 | 236 |
text {* There are probably lots of other list operations that also |
237 |
deserve to have continuity lemmas. I'll add more as they are |
|
238 |
needed. *} |
|
239 |
||
39212 | 240 |
subsection {* Using lists with fixrec *} |
241 |
||
242 |
definition |
|
243 |
match_Nil :: "'a::cpo list \<rightarrow> 'b match \<rightarrow> 'b match" |
|
244 |
where |
|
245 |
"match_Nil = (\<Lambda> xs k. case xs of [] \<Rightarrow> k | y # ys \<Rightarrow> Fixrec.fail)" |
|
246 |
||
247 |
definition |
|
248 |
match_Cons :: "'a::cpo list \<rightarrow> ('a \<rightarrow> 'a list \<rightarrow> 'b match) \<rightarrow> 'b match" |
|
249 |
where |
|
250 |
"match_Cons = (\<Lambda> xs k. case xs of [] \<Rightarrow> Fixrec.fail | y # ys \<Rightarrow> k\<cdot>y\<cdot>ys)" |
|
251 |
||
252 |
lemma match_Nil_simps [simp]: |
|
253 |
"match_Nil\<cdot>[]\<cdot>k = k" |
|
254 |
"match_Nil\<cdot>(x # xs)\<cdot>k = Fixrec.fail" |
|
255 |
unfolding match_Nil_def by simp_all |
|
256 |
||
257 |
lemma match_Cons_simps [simp]: |
|
258 |
"match_Cons\<cdot>[]\<cdot>k = Fixrec.fail" |
|
259 |
"match_Cons\<cdot>(x # xs)\<cdot>k = k\<cdot>x\<cdot>xs" |
|
260 |
unfolding match_Cons_def by simp_all |
|
261 |
||
262 |
setup {* |
|
263 |
Fixrec.add_matchers |
|
264 |
[ (@{const_name Nil}, @{const_name match_Nil}), |
|
265 |
(@{const_name Cons}, @{const_name match_Cons}) ] |
|
266 |
*} |
|
267 |
||
39143 | 268 |
end |