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 |
|
|
53 |
text "Thanks to Joachim Breitner"
|
|
54 |
|
|
55 |
lemma list_Cons_below:
|
|
56 |
assumes "a # as \<sqsubseteq> xs"
|
|
57 |
obtains b and bs where "a \<sqsubseteq> b" and "as \<sqsubseteq> bs" and "xs = b # bs"
|
|
58 |
using assms by (cases xs, auto)
|
|
59 |
|
|
60 |
lemma list_below_Cons:
|
|
61 |
assumes "xs \<sqsubseteq> b # bs"
|
|
62 |
obtains a and as where "a \<sqsubseteq> b" and "as \<sqsubseteq> bs" and "xs = a # as"
|
|
63 |
using assms by (cases xs, auto)
|
|
64 |
|
|
65 |
lemma hd_mono: "xs \<sqsubseteq> ys \<Longrightarrow> hd xs \<sqsubseteq> hd ys"
|
|
66 |
by (cases xs, simp, cases ys, simp, simp)
|
|
67 |
|
|
68 |
lemma tl_mono: "xs \<sqsubseteq> ys \<Longrightarrow> tl xs \<sqsubseteq> tl ys"
|
|
69 |
by (cases xs, simp, cases ys, simp, simp)
|
|
70 |
|
|
71 |
lemma ch2ch_hd [simp]: "chain (\<lambda>i. S i) \<Longrightarrow> chain (\<lambda>i. hd (S i))"
|
|
72 |
by (rule chainI, rule hd_mono, erule chainE)
|
|
73 |
|
|
74 |
lemma ch2ch_tl [simp]: "chain (\<lambda>i. S i) \<Longrightarrow> chain (\<lambda>i. tl (S i))"
|
|
75 |
by (rule chainI, rule tl_mono, erule chainE)
|
|
76 |
|
|
77 |
lemma below_same_length: "xs \<sqsubseteq> ys \<Longrightarrow> length xs = length ys"
|
|
78 |
unfolding below_list_def by (rule list_all2_lengthD)
|
|
79 |
|
|
80 |
lemma list_chain_cases:
|
|
81 |
assumes S: "chain S"
|
|
82 |
obtains "\<forall>i. S i = []" |
|
|
83 |
A B where "chain A" and "chain B" and "\<forall>i. S i = A i # B i"
|
|
84 |
proof (cases "S 0")
|
|
85 |
case Nil
|
|
86 |
have "\<forall>i. S 0 \<sqsubseteq> S i" by (simp add: chain_mono [OF S])
|
|
87 |
with Nil have "\<forall>i. S i = []" by simp
|
|
88 |
thus ?thesis ..
|
|
89 |
next
|
|
90 |
case (Cons x xs)
|
|
91 |
have "\<forall>i. S 0 \<sqsubseteq> S i" by (simp add: chain_mono [OF S])
|
|
92 |
hence *: "\<forall>i. S i \<noteq> []" by (rule all_forward) (auto simp add: Cons)
|
|
93 |
let ?A = "\<lambda>i. hd (S i)"
|
|
94 |
let ?B = "\<lambda>i. tl (S i)"
|
|
95 |
from S have "chain ?A" and "chain ?B" by simp_all
|
|
96 |
moreover have "\<forall>i. S i = ?A i # ?B i" by (simp add: *)
|
|
97 |
ultimately show ?thesis ..
|
|
98 |
qed
|
|
99 |
|
|
100 |
subsection {* Lists are a complete partial order *}
|
|
101 |
|
|
102 |
lemma is_lub_Cons:
|
|
103 |
assumes A: "range A <<| x"
|
|
104 |
assumes B: "range B <<| xs"
|
|
105 |
shows "range (\<lambda>i. A i # B i) <<| x # xs"
|
|
106 |
using assms
|
|
107 |
unfolding is_lub_def is_ub_def Ball_def [symmetric]
|
|
108 |
by (clarsimp, case_tac u, simp_all)
|
|
109 |
|
|
110 |
lemma list_cpo_lemma:
|
|
111 |
fixes S :: "nat \<Rightarrow> 'a::cpo list"
|
|
112 |
assumes "chain S" and "\<forall>i. length (S i) = n"
|
|
113 |
shows "\<exists>x. range S <<| x"
|
|
114 |
using assms
|
|
115 |
apply (induct n arbitrary: S)
|
|
116 |
apply (subgoal_tac "S = (\<lambda>i. [])")
|
|
117 |
apply (fast intro: lub_const)
|
39199
|
118 |
apply (simp add: ext_iff)
|
39143
|
119 |
apply (drule_tac x="\<lambda>i. tl (S i)" in meta_spec, clarsimp)
|
|
120 |
apply (rule_tac x="(\<Squnion>i. hd (S i)) # x" in exI)
|
|
121 |
apply (subgoal_tac "range (\<lambda>i. hd (S i) # tl (S i)) = range S")
|
|
122 |
apply (erule subst)
|
|
123 |
apply (rule is_lub_Cons)
|
|
124 |
apply (rule thelubE [OF _ refl])
|
|
125 |
apply (erule ch2ch_hd)
|
|
126 |
apply assumption
|
|
127 |
apply (rule_tac f="\<lambda>S. range S" in arg_cong)
|
|
128 |
apply (rule ext)
|
|
129 |
apply (rule hd_Cons_tl)
|
|
130 |
apply (drule_tac x=i in spec, auto)
|
|
131 |
done
|
|
132 |
|
|
133 |
instance list :: (cpo) cpo
|
|
134 |
proof
|
|
135 |
fix S :: "nat \<Rightarrow> 'a list"
|
|
136 |
assume "chain S"
|
|
137 |
hence "\<forall>i. S 0 \<sqsubseteq> S i" by (simp add: chain_mono)
|
|
138 |
hence "\<forall>i. length (S i) = length (S 0)"
|
|
139 |
by (fast intro: below_same_length [symmetric])
|
|
140 |
with `chain S` show "\<exists>x. range S <<| x"
|
|
141 |
by (rule list_cpo_lemma)
|
|
142 |
qed
|
|
143 |
|
|
144 |
subsection {* Continuity of list operations *}
|
|
145 |
|
|
146 |
lemma cont2cont_Cons [simp, cont2cont]:
|
|
147 |
assumes f: "cont (\<lambda>x. f x)"
|
|
148 |
assumes g: "cont (\<lambda>x. g x)"
|
|
149 |
shows "cont (\<lambda>x. f x # g x)"
|
|
150 |
apply (rule contI)
|
|
151 |
apply (rule is_lub_Cons)
|
|
152 |
apply (erule contE [OF f])
|
|
153 |
apply (erule contE [OF g])
|
|
154 |
done
|
|
155 |
|
|
156 |
lemma lub_Cons:
|
|
157 |
fixes A :: "nat \<Rightarrow> 'a::cpo"
|
|
158 |
assumes A: "chain A" and B: "chain B"
|
|
159 |
shows "(\<Squnion>i. A i # B i) = (\<Squnion>i. A i) # (\<Squnion>i. B i)"
|
|
160 |
by (intro thelubI is_lub_Cons cpo_lubI A B)
|
|
161 |
|
|
162 |
lemma cont2cont_list_case:
|
|
163 |
assumes f: "cont (\<lambda>x. f x)"
|
|
164 |
assumes g: "cont (\<lambda>x. g x)"
|
|
165 |
assumes h1: "\<And>y ys. cont (\<lambda>x. h x y ys)"
|
|
166 |
assumes h2: "\<And>x ys. cont (\<lambda>y. h x y ys)"
|
|
167 |
assumes h3: "\<And>x y. cont (\<lambda>ys. h x y ys)"
|
|
168 |
shows "cont (\<lambda>x. case f x of [] \<Rightarrow> g x | y # ys \<Rightarrow> h x y ys)"
|
|
169 |
apply (rule cont_apply [OF f])
|
|
170 |
apply (rule contI)
|
|
171 |
apply (erule list_chain_cases)
|
|
172 |
apply (simp add: lub_const)
|
|
173 |
apply (simp add: lub_Cons)
|
|
174 |
apply (simp add: cont2contlubE [OF h2])
|
|
175 |
apply (simp add: cont2contlubE [OF h3])
|
|
176 |
apply (simp add: diag_lub ch2ch_cont [OF h2] ch2ch_cont [OF h3])
|
|
177 |
apply (rule cpo_lubI, rule chainI, rule below_trans)
|
|
178 |
apply (erule cont2monofunE [OF h2 chainE])
|
|
179 |
apply (erule cont2monofunE [OF h3 chainE])
|
|
180 |
apply (case_tac y, simp_all add: g h1)
|
|
181 |
done
|
|
182 |
|
|
183 |
lemma cont2cont_list_case' [simp, cont2cont]:
|
|
184 |
assumes f: "cont (\<lambda>x. f x)"
|
|
185 |
assumes g: "cont (\<lambda>x. g x)"
|
|
186 |
assumes h: "cont (\<lambda>p. h (fst p) (fst (snd p)) (snd (snd p)))"
|
|
187 |
shows "cont (\<lambda>x. case f x of [] \<Rightarrow> g x | y # ys \<Rightarrow> h x y ys)"
|
|
188 |
proof -
|
|
189 |
have "\<And>y ys. cont (\<lambda>x. h x (fst (y, ys)) (snd (y, ys)))"
|
|
190 |
by (rule h [THEN cont_fst_snd_D1])
|
|
191 |
hence h1: "\<And>y ys. cont (\<lambda>x. h x y ys)" by simp
|
|
192 |
note h2 = h [THEN cont_fst_snd_D2, THEN cont_fst_snd_D1]
|
|
193 |
note h3 = h [THEN cont_fst_snd_D2, THEN cont_fst_snd_D2]
|
|
194 |
from f g h1 h2 h3 show ?thesis by (rule cont2cont_list_case)
|
|
195 |
qed
|
|
196 |
|
|
197 |
text {* The simple version (due to Joachim Breitner) is needed if the
|
|
198 |
element type of the list is not a cpo. *}
|
|
199 |
|
|
200 |
lemma cont2cont_list_case_simple [simp, cont2cont]:
|
|
201 |
assumes "cont (\<lambda>x. f1 x)"
|
|
202 |
assumes "\<And>y ys. cont (\<lambda>x. f2 x y ys)"
|
|
203 |
shows "cont (\<lambda>x. case l of [] \<Rightarrow> f1 x | y # ys \<Rightarrow> f2 x y ys)"
|
|
204 |
using assms by (cases l) auto
|
|
205 |
|
|
206 |
text {* There are probably lots of other list operations that also
|
|
207 |
deserve to have continuity lemmas. I'll add more as they are
|
|
208 |
needed. *}
|
|
209 |
|
39212
|
210 |
subsection {* Using lists with fixrec *}
|
|
211 |
|
|
212 |
definition
|
|
213 |
match_Nil :: "'a::cpo list \<rightarrow> 'b match \<rightarrow> 'b match"
|
|
214 |
where
|
|
215 |
"match_Nil = (\<Lambda> xs k. case xs of [] \<Rightarrow> k | y # ys \<Rightarrow> Fixrec.fail)"
|
|
216 |
|
|
217 |
definition
|
|
218 |
match_Cons :: "'a::cpo list \<rightarrow> ('a \<rightarrow> 'a list \<rightarrow> 'b match) \<rightarrow> 'b match"
|
|
219 |
where
|
|
220 |
"match_Cons = (\<Lambda> xs k. case xs of [] \<Rightarrow> Fixrec.fail | y # ys \<Rightarrow> k\<cdot>y\<cdot>ys)"
|
|
221 |
|
|
222 |
lemma match_Nil_simps [simp]:
|
|
223 |
"match_Nil\<cdot>[]\<cdot>k = k"
|
|
224 |
"match_Nil\<cdot>(x # xs)\<cdot>k = Fixrec.fail"
|
|
225 |
unfolding match_Nil_def by simp_all
|
|
226 |
|
|
227 |
lemma match_Cons_simps [simp]:
|
|
228 |
"match_Cons\<cdot>[]\<cdot>k = Fixrec.fail"
|
|
229 |
"match_Cons\<cdot>(x # xs)\<cdot>k = k\<cdot>x\<cdot>xs"
|
|
230 |
unfolding match_Cons_def by simp_all
|
|
231 |
|
|
232 |
setup {*
|
|
233 |
Fixrec.add_matchers
|
|
234 |
[ (@{const_name Nil}, @{const_name match_Nil}),
|
|
235 |
(@{const_name Cons}, @{const_name match_Cons}) ]
|
|
236 |
*}
|
|
237 |
|
39143
|
238 |
end
|