12516
|
1 |
(* Title: HOL/MicroJava/BV/Listn.thy
|
10496
|
2 |
ID: $Id$
|
|
3 |
Author: Tobias Nipkow
|
|
4 |
Copyright 2000 TUM
|
|
5 |
|
|
6 |
Lists of a fixed length
|
|
7 |
*)
|
|
8 |
|
12911
|
9 |
header {* \isaheader{Fixed Length Lists} *}
|
10496
|
10 |
|
|
11 |
theory Listn = Err:
|
|
12 |
|
|
13 |
constdefs
|
|
14 |
|
13006
|
15 |
list :: "nat \<Rightarrow> 'a set \<Rightarrow> 'a list set"
|
10496
|
16 |
"list n A == {xs. length xs = n & set xs <= A}"
|
|
17 |
|
13006
|
18 |
le :: "'a ord \<Rightarrow> ('a list)ord"
|
10496
|
19 |
"le r == list_all2 (%x y. x <=_r y)"
|
|
20 |
|
13006
|
21 |
syntax "@lesublist" :: "'a list \<Rightarrow> 'a ord \<Rightarrow> 'a list \<Rightarrow> bool"
|
10496
|
22 |
("(_ /<=[_] _)" [50, 0, 51] 50)
|
13006
|
23 |
syntax "@lesssublist" :: "'a list \<Rightarrow> 'a ord \<Rightarrow> 'a list \<Rightarrow> bool"
|
10496
|
24 |
("(_ /<[_] _)" [50, 0, 51] 50)
|
|
25 |
translations
|
|
26 |
"x <=[r] y" == "x <=_(Listn.le r) y"
|
|
27 |
"x <[r] y" == "x <_(Listn.le r) y"
|
|
28 |
|
|
29 |
constdefs
|
13006
|
30 |
map2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list"
|
10496
|
31 |
"map2 f == (%xs ys. map (split f) (zip xs ys))"
|
|
32 |
|
13006
|
33 |
syntax "@plussublist" :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b list \<Rightarrow> 'c list"
|
10496
|
34 |
("(_ /+[_] _)" [65, 0, 66] 65)
|
|
35 |
translations "x +[f] y" == "x +_(map2 f) y"
|
|
36 |
|
13006
|
37 |
consts coalesce :: "'a err list \<Rightarrow> 'a list err"
|
10496
|
38 |
primrec
|
|
39 |
"coalesce [] = OK[]"
|
|
40 |
"coalesce (ex#exs) = Err.sup (op #) ex (coalesce exs)"
|
|
41 |
|
|
42 |
constdefs
|
13006
|
43 |
sl :: "nat \<Rightarrow> 'a sl \<Rightarrow> 'a list sl"
|
10496
|
44 |
"sl n == %(A,r,f). (list n A, le r, map2 f)"
|
|
45 |
|
13006
|
46 |
sup :: "('a \<Rightarrow> 'b \<Rightarrow> 'c err) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list err"
|
10496
|
47 |
"sup f == %xs ys. if size xs = size ys then coalesce(xs +[f] ys) else Err"
|
|
48 |
|
13006
|
49 |
upto_esl :: "nat \<Rightarrow> 'a esl \<Rightarrow> 'a list esl"
|
10496
|
50 |
"upto_esl m == %(A,r,f). (Union{list n A |n. n <= m}, le r, sup f)"
|
|
51 |
|
|
52 |
lemmas [simp] = set_update_subsetI
|
|
53 |
|
|
54 |
lemma unfold_lesub_list:
|
|
55 |
"xs <=[r] ys == Listn.le r xs ys"
|
|
56 |
by (simp add: lesub_def)
|
|
57 |
|
|
58 |
lemma Nil_le_conv [iff]:
|
|
59 |
"([] <=[r] ys) = (ys = [])"
|
|
60 |
apply (unfold lesub_def Listn.le_def)
|
|
61 |
apply simp
|
|
62 |
done
|
|
63 |
|
|
64 |
lemma Cons_notle_Nil [iff]:
|
|
65 |
"~ x#xs <=[r] []"
|
|
66 |
apply (unfold lesub_def Listn.le_def)
|
|
67 |
apply simp
|
|
68 |
done
|
|
69 |
|
|
70 |
|
|
71 |
lemma Cons_le_Cons [iff]:
|
|
72 |
"x#xs <=[r] y#ys = (x <=_r y & xs <=[r] ys)"
|
|
73 |
apply (unfold lesub_def Listn.le_def)
|
|
74 |
apply simp
|
|
75 |
done
|
|
76 |
|
|
77 |
lemma Cons_less_Conss [simp]:
|
13006
|
78 |
"order r \<Longrightarrow>
|
10496
|
79 |
x#xs <_(Listn.le r) y#ys =
|
|
80 |
(x <_r y & xs <=[r] ys | x = y & xs <_(Listn.le r) ys)"
|
|
81 |
apply (unfold lesssub_def)
|
|
82 |
apply blast
|
|
83 |
done
|
|
84 |
|
|
85 |
lemma list_update_le_cong:
|
13006
|
86 |
"\<lbrakk> i<size xs; xs <=[r] ys; x <=_r y \<rbrakk> \<Longrightarrow> xs[i:=x] <=[r] ys[i:=y]";
|
10496
|
87 |
apply (unfold unfold_lesub_list)
|
|
88 |
apply (unfold Listn.le_def)
|
|
89 |
apply (simp add: list_all2_conv_all_nth nth_list_update)
|
|
90 |
done
|
|
91 |
|
|
92 |
|
|
93 |
lemma le_listD:
|
13006
|
94 |
"\<lbrakk> xs <=[r] ys; p < size xs \<rbrakk> \<Longrightarrow> xs!p <=_r ys!p"
|
10496
|
95 |
apply (unfold Listn.le_def lesub_def)
|
|
96 |
apply (simp add: list_all2_conv_all_nth)
|
|
97 |
done
|
|
98 |
|
|
99 |
lemma le_list_refl:
|
13006
|
100 |
"!x. x <=_r x \<Longrightarrow> xs <=[r] xs"
|
10496
|
101 |
apply (unfold unfold_lesub_list)
|
|
102 |
apply (simp add: Listn.le_def list_all2_conv_all_nth)
|
|
103 |
done
|
|
104 |
|
|
105 |
lemma le_list_trans:
|
13006
|
106 |
"\<lbrakk> order r; xs <=[r] ys; ys <=[r] zs \<rbrakk> \<Longrightarrow> xs <=[r] zs"
|
10496
|
107 |
apply (unfold unfold_lesub_list)
|
|
108 |
apply (simp add: Listn.le_def list_all2_conv_all_nth)
|
|
109 |
apply clarify
|
|
110 |
apply simp
|
|
111 |
apply (blast intro: order_trans)
|
|
112 |
done
|
|
113 |
|
|
114 |
lemma le_list_antisym:
|
13006
|
115 |
"\<lbrakk> order r; xs <=[r] ys; ys <=[r] xs \<rbrakk> \<Longrightarrow> xs = ys"
|
10496
|
116 |
apply (unfold unfold_lesub_list)
|
|
117 |
apply (simp add: Listn.le_def list_all2_conv_all_nth)
|
|
118 |
apply (rule nth_equalityI)
|
|
119 |
apply blast
|
|
120 |
apply clarify
|
|
121 |
apply simp
|
|
122 |
apply (blast intro: order_antisym)
|
|
123 |
done
|
|
124 |
|
|
125 |
lemma order_listI [simp, intro!]:
|
13006
|
126 |
"order r \<Longrightarrow> order(Listn.le r)"
|
10496
|
127 |
apply (subst order_def)
|
|
128 |
apply (blast intro: le_list_refl le_list_trans le_list_antisym
|
|
129 |
dest: order_refl)
|
|
130 |
done
|
|
131 |
|
|
132 |
|
|
133 |
lemma lesub_list_impl_same_size [simp]:
|
13006
|
134 |
"xs <=[r] ys \<Longrightarrow> size ys = size xs"
|
10496
|
135 |
apply (unfold Listn.le_def lesub_def)
|
|
136 |
apply (simp add: list_all2_conv_all_nth)
|
|
137 |
done
|
|
138 |
|
|
139 |
lemma lesssub_list_impl_same_size:
|
13006
|
140 |
"xs <_(Listn.le r) ys \<Longrightarrow> size ys = size xs"
|
10496
|
141 |
apply (unfold lesssub_def)
|
|
142 |
apply auto
|
|
143 |
done
|
|
144 |
|
13066
|
145 |
lemma le_list_appendI:
|
|
146 |
"\<And>b c d. a <=[r] b \<Longrightarrow> c <=[r] d \<Longrightarrow> a@c <=[r] b@d"
|
|
147 |
apply (induct a)
|
|
148 |
apply simp
|
|
149 |
apply (case_tac b)
|
|
150 |
apply auto
|
|
151 |
done
|
|
152 |
|
|
153 |
lemma le_listI:
|
|
154 |
"length a = length b \<Longrightarrow> (\<And>n. n < length a \<Longrightarrow> a!n <=_r b!n) \<Longrightarrow> a <=[r] b"
|
|
155 |
apply (unfold lesub_def Listn.le_def)
|
|
156 |
apply (simp add: list_all2_conv_all_nth)
|
|
157 |
done
|
|
158 |
|
10496
|
159 |
lemma listI:
|
13006
|
160 |
"\<lbrakk> length xs = n; set xs <= A \<rbrakk> \<Longrightarrow> xs : list n A"
|
10496
|
161 |
apply (unfold list_def)
|
|
162 |
apply blast
|
|
163 |
done
|
|
164 |
|
|
165 |
lemma listE_length [simp]:
|
13006
|
166 |
"xs : list n A \<Longrightarrow> length xs = n"
|
10496
|
167 |
apply (unfold list_def)
|
|
168 |
apply blast
|
|
169 |
done
|
|
170 |
|
|
171 |
lemma less_lengthI:
|
13006
|
172 |
"\<lbrakk> xs : list n A; p < n \<rbrakk> \<Longrightarrow> p < length xs"
|
10496
|
173 |
by simp
|
|
174 |
|
|
175 |
lemma listE_set [simp]:
|
13006
|
176 |
"xs : list n A \<Longrightarrow> set xs <= A"
|
10496
|
177 |
apply (unfold list_def)
|
|
178 |
apply blast
|
|
179 |
done
|
|
180 |
|
|
181 |
lemma list_0 [simp]:
|
|
182 |
"list 0 A = {[]}"
|
|
183 |
apply (unfold list_def)
|
|
184 |
apply auto
|
|
185 |
done
|
|
186 |
|
|
187 |
lemma in_list_Suc_iff:
|
|
188 |
"(xs : list (Suc n) A) = (? y:A. ? ys:list n A. xs = y#ys)"
|
|
189 |
apply (unfold list_def)
|
|
190 |
apply (case_tac "xs")
|
|
191 |
apply auto
|
|
192 |
done
|
|
193 |
|
|
194 |
lemma Cons_in_list_Suc [iff]:
|
|
195 |
"(x#xs : list (Suc n) A) = (x:A & xs : list n A)";
|
|
196 |
apply (simp add: in_list_Suc_iff)
|
|
197 |
done
|
|
198 |
|
|
199 |
lemma list_not_empty:
|
13006
|
200 |
"? a. a:A \<Longrightarrow> ? xs. xs : list n A";
|
10496
|
201 |
apply (induct "n")
|
|
202 |
apply simp
|
|
203 |
apply (simp add: in_list_Suc_iff)
|
|
204 |
apply blast
|
|
205 |
done
|
|
206 |
|
|
207 |
|
|
208 |
lemma nth_in [rule_format, simp]:
|
13006
|
209 |
"!i n. length xs = n \<longrightarrow> set xs <= A \<longrightarrow> i < n \<longrightarrow> (xs!i) : A"
|
10496
|
210 |
apply (induct "xs")
|
|
211 |
apply simp
|
|
212 |
apply (simp add: nth_Cons split: nat.split)
|
|
213 |
done
|
|
214 |
|
|
215 |
lemma listE_nth_in:
|
13006
|
216 |
"\<lbrakk> xs : list n A; i < n \<rbrakk> \<Longrightarrow> (xs!i) : A"
|
10496
|
217 |
by auto
|
|
218 |
|
13066
|
219 |
|
|
220 |
lemma listn_Cons_Suc [elim!]:
|
|
221 |
"l#xs \<in> list n A \<Longrightarrow> (\<And>n'. n = Suc n' \<Longrightarrow> l \<in> A \<Longrightarrow> xs \<in> list n' A \<Longrightarrow> P) \<Longrightarrow> P"
|
|
222 |
by (cases n) auto
|
|
223 |
|
|
224 |
lemma listn_appendE [elim!]:
|
|
225 |
"a@b \<in> list n A \<Longrightarrow> (\<And>n1 n2. n=n1+n2 \<Longrightarrow> a \<in> list n1 A \<Longrightarrow> b \<in> list n2 A \<Longrightarrow> P) \<Longrightarrow> P"
|
|
226 |
proof -
|
|
227 |
have "\<And>n. a@b \<in> list n A \<Longrightarrow> \<exists>n1 n2. n=n1+n2 \<and> a \<in> list n1 A \<and> b \<in> list n2 A"
|
|
228 |
(is "\<And>n. ?list a n \<Longrightarrow> \<exists>n1 n2. ?P a n n1 n2")
|
|
229 |
proof (induct a)
|
|
230 |
fix n assume "?list [] n"
|
|
231 |
hence "?P [] n 0 n" by simp
|
|
232 |
thus "\<exists>n1 n2. ?P [] n n1 n2" by fast
|
|
233 |
next
|
|
234 |
fix n l ls
|
|
235 |
assume "?list (l#ls) n"
|
|
236 |
then obtain n' where n: "n = Suc n'" "l \<in> A" and "ls@b \<in> list n' A" by fastsimp
|
|
237 |
assume "\<And>n. ls @ b \<in> list n A \<Longrightarrow> \<exists>n1 n2. n = n1 + n2 \<and> ls \<in> list n1 A \<and> b \<in> list n2 A"
|
|
238 |
hence "\<exists>n1 n2. n' = n1 + n2 \<and> ls \<in> list n1 A \<and> b \<in> list n2 A" .
|
|
239 |
then obtain n1 n2 where "n' = n1 + n2" "ls \<in> list n1 A" "b \<in> list n2 A" by fast
|
|
240 |
with n have "?P (l#ls) n (n1+1) n2" by simp
|
|
241 |
thus "\<exists>n1 n2. ?P (l#ls) n n1 n2" by fastsimp
|
|
242 |
qed
|
|
243 |
moreover
|
|
244 |
assume "a@b \<in> list n A" "\<And>n1 n2. n=n1+n2 \<Longrightarrow> a \<in> list n1 A \<Longrightarrow> b \<in> list n2 A \<Longrightarrow> P"
|
|
245 |
ultimately
|
|
246 |
show ?thesis by blast
|
|
247 |
qed
|
|
248 |
|
|
249 |
|
10496
|
250 |
lemma listt_update_in_list [simp, intro!]:
|
13006
|
251 |
"\<lbrakk> xs : list n A; x:A \<rbrakk> \<Longrightarrow> xs[i := x] : list n A"
|
10496
|
252 |
apply (unfold list_def)
|
|
253 |
apply simp
|
|
254 |
done
|
|
255 |
|
|
256 |
lemma plus_list_Nil [simp]:
|
|
257 |
"[] +[f] xs = []"
|
|
258 |
apply (unfold plussub_def map2_def)
|
|
259 |
apply simp
|
|
260 |
done
|
|
261 |
|
|
262 |
lemma plus_list_Cons [simp]:
|
13006
|
263 |
"(x#xs) +[f] ys = (case ys of [] \<Rightarrow> [] | y#ys \<Rightarrow> (x +_f y)#(xs +[f] ys))"
|
10496
|
264 |
by (simp add: plussub_def map2_def split: list.split)
|
|
265 |
|
|
266 |
lemma length_plus_list [rule_format, simp]:
|
|
267 |
"!ys. length(xs +[f] ys) = min(length xs) (length ys)"
|
|
268 |
apply (induct xs)
|
|
269 |
apply simp
|
|
270 |
apply clarify
|
|
271 |
apply (simp (no_asm_simp) split: list.split)
|
|
272 |
done
|
|
273 |
|
|
274 |
lemma nth_plus_list [rule_format, simp]:
|
13006
|
275 |
"!xs ys i. length xs = n \<longrightarrow> length ys = n \<longrightarrow> i<n \<longrightarrow>
|
10496
|
276 |
(xs +[f] ys)!i = (xs!i) +_f (ys!i)"
|
|
277 |
apply (induct n)
|
|
278 |
apply simp
|
|
279 |
apply clarify
|
|
280 |
apply (case_tac xs)
|
|
281 |
apply simp
|
|
282 |
apply (force simp add: nth_Cons split: list.split nat.split)
|
|
283 |
done
|
|
284 |
|
|
285 |
|
13074
|
286 |
lemma (in semilat) plus_list_ub1 [rule_format]:
|
|
287 |
"\<lbrakk> set xs <= A; set ys <= A; size xs = size ys \<rbrakk>
|
13006
|
288 |
\<Longrightarrow> xs <=[r] xs +[f] ys"
|
10496
|
289 |
apply (unfold unfold_lesub_list)
|
|
290 |
apply (simp add: Listn.le_def list_all2_conv_all_nth)
|
|
291 |
done
|
|
292 |
|
13074
|
293 |
lemma (in semilat) plus_list_ub2:
|
|
294 |
"\<lbrakk>set xs <= A; set ys <= A; size xs = size ys \<rbrakk>
|
13006
|
295 |
\<Longrightarrow> ys <=[r] xs +[f] ys"
|
10496
|
296 |
apply (unfold unfold_lesub_list)
|
|
297 |
apply (simp add: Listn.le_def list_all2_conv_all_nth)
|
13074
|
298 |
done
|
10496
|
299 |
|
13074
|
300 |
lemma (in semilat) plus_list_lub [rule_format]:
|
|
301 |
shows "!xs ys zs. set xs <= A \<longrightarrow> set ys <= A \<longrightarrow> set zs <= A
|
13006
|
302 |
\<longrightarrow> size xs = n & size ys = n \<longrightarrow>
|
|
303 |
xs <=[r] zs & ys <=[r] zs \<longrightarrow> xs +[f] ys <=[r] zs"
|
10496
|
304 |
apply (unfold unfold_lesub_list)
|
|
305 |
apply (simp add: Listn.le_def list_all2_conv_all_nth)
|
13074
|
306 |
done
|
10496
|
307 |
|
13074
|
308 |
lemma (in semilat) list_update_incr [rule_format]:
|
|
309 |
"x:A \<Longrightarrow> set xs <= A \<longrightarrow>
|
13006
|
310 |
(!i. i<size xs \<longrightarrow> xs <=[r] xs[i := x +_f xs!i])"
|
10496
|
311 |
apply (unfold unfold_lesub_list)
|
|
312 |
apply (simp add: Listn.le_def list_all2_conv_all_nth)
|
|
313 |
apply (induct xs)
|
|
314 |
apply simp
|
|
315 |
apply (simp add: in_list_Suc_iff)
|
|
316 |
apply clarify
|
|
317 |
apply (simp add: nth_Cons split: nat.split)
|
13074
|
318 |
done
|
10496
|
319 |
|
|
320 |
lemma acc_le_listI [intro!]:
|
13006
|
321 |
"\<lbrakk> order r; acc r \<rbrakk> \<Longrightarrow> acc(Listn.le r)"
|
10496
|
322 |
apply (unfold acc_def)
|
|
323 |
apply (subgoal_tac
|
|
324 |
"wf(UN n. {(ys,xs). size xs = n & size ys = n & xs <_(Listn.le r) ys})")
|
|
325 |
apply (erule wf_subset)
|
|
326 |
apply (blast intro: lesssub_list_impl_same_size)
|
|
327 |
apply (rule wf_UN)
|
|
328 |
prefer 2
|
|
329 |
apply clarify
|
|
330 |
apply (rename_tac m n)
|
|
331 |
apply (case_tac "m=n")
|
|
332 |
apply simp
|
|
333 |
apply (rule conjI)
|
|
334 |
apply (fast intro!: equals0I dest: not_sym)
|
|
335 |
apply (fast intro!: equals0I dest: not_sym)
|
|
336 |
apply clarify
|
|
337 |
apply (rename_tac n)
|
|
338 |
apply (induct_tac n)
|
|
339 |
apply (simp add: lesssub_def cong: conj_cong)
|
|
340 |
apply (rename_tac k)
|
|
341 |
apply (simp add: wf_eq_minimal)
|
|
342 |
apply (simp (no_asm) add: length_Suc_conv cong: conj_cong)
|
|
343 |
apply clarify
|
|
344 |
apply (rename_tac M m)
|
|
345 |
apply (case_tac "? x xs. size xs = k & x#xs : M")
|
|
346 |
prefer 2
|
|
347 |
apply (erule thin_rl)
|
|
348 |
apply (erule thin_rl)
|
|
349 |
apply blast
|
|
350 |
apply (erule_tac x = "{a. ? xs. size xs = k & a#xs:M}" in allE)
|
|
351 |
apply (erule impE)
|
|
352 |
apply blast
|
|
353 |
apply (thin_tac "? x xs. ?P x xs")
|
|
354 |
apply clarify
|
|
355 |
apply (rename_tac maxA xs)
|
|
356 |
apply (erule_tac x = "{ys. size ys = size xs & maxA#ys : M}" in allE)
|
|
357 |
apply (erule impE)
|
|
358 |
apply blast
|
|
359 |
apply clarify
|
|
360 |
apply (thin_tac "m : M")
|
|
361 |
apply (thin_tac "maxA#xs : M")
|
|
362 |
apply (rule bexI)
|
|
363 |
prefer 2
|
|
364 |
apply assumption
|
|
365 |
apply clarify
|
|
366 |
apply simp
|
|
367 |
apply blast
|
|
368 |
done
|
|
369 |
|
|
370 |
lemma closed_listI:
|
13006
|
371 |
"closed S f \<Longrightarrow> closed (list n S) (map2 f)"
|
10496
|
372 |
apply (unfold closed_def)
|
|
373 |
apply (induct n)
|
|
374 |
apply simp
|
|
375 |
apply clarify
|
|
376 |
apply (simp add: in_list_Suc_iff)
|
|
377 |
apply clarify
|
|
378 |
apply simp
|
13074
|
379 |
done
|
10496
|
380 |
|
|
381 |
|
13074
|
382 |
lemma Listn_sl_aux:
|
|
383 |
includes semilat shows "semilat (Listn.sl n (A,r,f))"
|
10496
|
384 |
apply (unfold Listn.sl_def)
|
10918
|
385 |
apply (simp (no_asm) only: semilat_Def split_conv)
|
10496
|
386 |
apply (rule conjI)
|
|
387 |
apply simp
|
|
388 |
apply (rule conjI)
|
13074
|
389 |
apply (simp only: closedI closed_listI)
|
10496
|
390 |
apply (simp (no_asm) only: list_def)
|
|
391 |
apply (simp (no_asm_simp) add: plus_list_ub1 plus_list_ub2 plus_list_lub)
|
13074
|
392 |
done
|
10496
|
393 |
|
13074
|
394 |
lemma Listn_sl: "\<And>L. semilat L \<Longrightarrow> semilat (Listn.sl n L)"
|
|
395 |
by(simp add: Listn_sl_aux split_tupled_all)
|
10496
|
396 |
|
|
397 |
lemma coalesce_in_err_list [rule_format]:
|
13006
|
398 |
"!xes. xes : list n (err A) \<longrightarrow> coalesce xes : err(list n A)"
|
10496
|
399 |
apply (induct n)
|
|
400 |
apply simp
|
|
401 |
apply clarify
|
|
402 |
apply (simp add: in_list_Suc_iff)
|
|
403 |
apply clarify
|
|
404 |
apply (simp (no_asm) add: plussub_def Err.sup_def lift2_def split: err.split)
|
|
405 |
apply force
|
|
406 |
done
|
|
407 |
|
13006
|
408 |
lemma lem: "\<And>x xs. x +_(op #) xs = x#xs"
|
10496
|
409 |
by (simp add: plussub_def)
|
|
410 |
|
|
411 |
lemma coalesce_eq_OK1_D [rule_format]:
|
13006
|
412 |
"semilat(err A, Err.le r, lift2 f) \<Longrightarrow>
|
|
413 |
!xs. xs : list n A \<longrightarrow> (!ys. ys : list n A \<longrightarrow>
|
|
414 |
(!zs. coalesce (xs +[f] ys) = OK zs \<longrightarrow> xs <=[r] zs))"
|
10496
|
415 |
apply (induct n)
|
|
416 |
apply simp
|
|
417 |
apply clarify
|
|
418 |
apply (simp add: in_list_Suc_iff)
|
|
419 |
apply clarify
|
|
420 |
apply (simp split: err.split_asm add: lem Err.sup_def lift2_def)
|
|
421 |
apply (force simp add: semilat_le_err_OK1)
|
|
422 |
done
|
|
423 |
|
|
424 |
lemma coalesce_eq_OK2_D [rule_format]:
|
13006
|
425 |
"semilat(err A, Err.le r, lift2 f) \<Longrightarrow>
|
|
426 |
!xs. xs : list n A \<longrightarrow> (!ys. ys : list n A \<longrightarrow>
|
|
427 |
(!zs. coalesce (xs +[f] ys) = OK zs \<longrightarrow> ys <=[r] zs))"
|
10496
|
428 |
apply (induct n)
|
|
429 |
apply simp
|
|
430 |
apply clarify
|
|
431 |
apply (simp add: in_list_Suc_iff)
|
|
432 |
apply clarify
|
|
433 |
apply (simp split: err.split_asm add: lem Err.sup_def lift2_def)
|
|
434 |
apply (force simp add: semilat_le_err_OK2)
|
|
435 |
done
|
|
436 |
|
|
437 |
lemma lift2_le_ub:
|
13006
|
438 |
"\<lbrakk> semilat(err A, Err.le r, lift2 f); x:A; y:A; x +_f y = OK z;
|
|
439 |
u:A; x <=_r u; y <=_r u \<rbrakk> \<Longrightarrow> z <=_r u"
|
10496
|
440 |
apply (unfold semilat_Def plussub_def err_def)
|
|
441 |
apply (simp add: lift2_def)
|
|
442 |
apply clarify
|
|
443 |
apply (rotate_tac -3)
|
|
444 |
apply (erule thin_rl)
|
|
445 |
apply (erule thin_rl)
|
|
446 |
apply force
|
13074
|
447 |
done
|
10496
|
448 |
|
|
449 |
lemma coalesce_eq_OK_ub_D [rule_format]:
|
13006
|
450 |
"semilat(err A, Err.le r, lift2 f) \<Longrightarrow>
|
|
451 |
!xs. xs : list n A \<longrightarrow> (!ys. ys : list n A \<longrightarrow>
|
10496
|
452 |
(!zs us. coalesce (xs +[f] ys) = OK zs & xs <=[r] us & ys <=[r] us
|
13006
|
453 |
& us : list n A \<longrightarrow> zs <=[r] us))"
|
10496
|
454 |
apply (induct n)
|
|
455 |
apply simp
|
|
456 |
apply clarify
|
|
457 |
apply (simp add: in_list_Suc_iff)
|
|
458 |
apply clarify
|
|
459 |
apply (simp (no_asm_use) split: err.split_asm add: lem Err.sup_def lift2_def)
|
|
460 |
apply clarify
|
|
461 |
apply (rule conjI)
|
|
462 |
apply (blast intro: lift2_le_ub)
|
|
463 |
apply blast
|
|
464 |
done
|
|
465 |
|
|
466 |
lemma lift2_eq_ErrD:
|
13006
|
467 |
"\<lbrakk> x +_f y = Err; semilat(err A, Err.le r, lift2 f); x:A; y:A \<rbrakk>
|
|
468 |
\<Longrightarrow> ~(? u:A. x <=_r u & y <=_r u)"
|
10496
|
469 |
by (simp add: OK_plus_OK_eq_Err_conv [THEN iffD1])
|
|
470 |
|
|
471 |
|
|
472 |
lemma coalesce_eq_Err_D [rule_format]:
|
13006
|
473 |
"\<lbrakk> semilat(err A, Err.le r, lift2 f) \<rbrakk>
|
|
474 |
\<Longrightarrow> !xs. xs:list n A \<longrightarrow> (!ys. ys:list n A \<longrightarrow>
|
|
475 |
coalesce (xs +[f] ys) = Err \<longrightarrow>
|
10496
|
476 |
~(? zs:list n A. xs <=[r] zs & ys <=[r] zs))"
|
|
477 |
apply (induct n)
|
|
478 |
apply simp
|
|
479 |
apply clarify
|
|
480 |
apply (simp add: in_list_Suc_iff)
|
|
481 |
apply clarify
|
|
482 |
apply (simp split: err.split_asm add: lem Err.sup_def lift2_def)
|
|
483 |
apply (blast dest: lift2_eq_ErrD)
|
|
484 |
apply blast
|
|
485 |
done
|
|
486 |
|
|
487 |
lemma closed_err_lift2_conv:
|
|
488 |
"closed (err A) (lift2 f) = (!x:A. !y:A. x +_f y : err A)"
|
|
489 |
apply (unfold closed_def)
|
|
490 |
apply (simp add: err_def)
|
|
491 |
done
|
|
492 |
|
|
493 |
lemma closed_map2_list [rule_format]:
|
13006
|
494 |
"closed (err A) (lift2 f) \<Longrightarrow>
|
|
495 |
!xs. xs : list n A \<longrightarrow> (!ys. ys : list n A \<longrightarrow>
|
10496
|
496 |
map2 f xs ys : list n (err A))"
|
|
497 |
apply (unfold map2_def)
|
|
498 |
apply (induct n)
|
|
499 |
apply simp
|
|
500 |
apply clarify
|
|
501 |
apply (simp add: in_list_Suc_iff)
|
|
502 |
apply clarify
|
|
503 |
apply (simp add: plussub_def closed_err_lift2_conv)
|
13074
|
504 |
done
|
10496
|
505 |
|
|
506 |
lemma closed_lift2_sup:
|
13006
|
507 |
"closed (err A) (lift2 f) \<Longrightarrow>
|
10496
|
508 |
closed (err (list n A)) (lift2 (sup f))"
|
|
509 |
by (fastsimp simp add: closed_def plussub_def sup_def lift2_def
|
|
510 |
coalesce_in_err_list closed_map2_list
|
|
511 |
split: err.split)
|
|
512 |
|
|
513 |
lemma err_semilat_sup:
|
13006
|
514 |
"err_semilat (A,r,f) \<Longrightarrow>
|
10496
|
515 |
err_semilat (list n A, Listn.le r, sup f)"
|
|
516 |
apply (unfold Err.sl_def)
|
10918
|
517 |
apply (simp only: split_conv)
|
10496
|
518 |
apply (simp (no_asm) only: semilat_Def plussub_def)
|
13074
|
519 |
apply (simp (no_asm_simp) only: semilat.closedI closed_lift2_sup)
|
10496
|
520 |
apply (rule conjI)
|
13074
|
521 |
apply (drule semilat.orderI)
|
10496
|
522 |
apply simp
|
|
523 |
apply (simp (no_asm) only: unfold_lesub_err Err.le_def err_def sup_def lift2_def)
|
|
524 |
apply (simp (no_asm_simp) add: coalesce_eq_OK1_D coalesce_eq_OK2_D split: err.split)
|
|
525 |
apply (blast intro: coalesce_eq_OK_ub_D dest: coalesce_eq_Err_D)
|
|
526 |
done
|
|
527 |
|
|
528 |
lemma err_semilat_upto_esl:
|
13006
|
529 |
"\<And>L. err_semilat L \<Longrightarrow> err_semilat(upto_esl m L)"
|
10496
|
530 |
apply (unfold Listn.upto_esl_def)
|
|
531 |
apply (simp (no_asm_simp) only: split_tupled_all)
|
|
532 |
apply simp
|
|
533 |
apply (fastsimp intro!: err_semilat_UnionI err_semilat_sup
|
|
534 |
dest: lesub_list_impl_same_size
|
|
535 |
simp add: plussub_def Listn.sup_def)
|
|
536 |
done
|
|
537 |
|
|
538 |
end
|