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 


286 
lemma plus_list_ub1 [rule_format]:

13006

287 
"\<lbrakk> semilat(A,r,f); set xs <= A; set ys <= A; size xs = size ys \<rbrakk>


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 


293 
lemma plus_list_ub2:

13006

294 
"\<lbrakk> semilat(A,r,f); set xs <= A; set ys <= A; size xs = size ys \<rbrakk>


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)


298 
done


299 


300 
lemma plus_list_lub [rule_format]:

13006

301 
"semilat(A,r,f) \<Longrightarrow> !xs ys zs. set xs <= A \<longrightarrow> set ys <= A \<longrightarrow> set zs <= A


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)


306 
done


307 


308 
lemma list_update_incr [rule_format]:

13006

309 
"\<lbrakk> semilat(A,r,f); x:A \<rbrakk> \<Longrightarrow> set xs <= A \<longrightarrow>


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)


318 
done


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


379 
done


380 


381 


382 
lemma semilat_Listn_sl:

13006

383 
"\<And>L. semilat L \<Longrightarrow> semilat (Listn.sl n L)"

10496

384 
apply (unfold Listn.sl_def)


385 
apply (simp (no_asm_simp) only: split_tupled_all)

10918

386 
apply (simp (no_asm) only: semilat_Def split_conv)

10496

387 
apply (rule conjI)


388 
apply simp


389 
apply (rule conjI)


390 
apply (simp only: semilatDclosedI closed_listI)


391 
apply (simp (no_asm) only: list_def)


392 
apply (simp (no_asm_simp) add: plus_list_ub1 plus_list_ub2 plus_list_lub)


393 
done


394 


395 


396 
lemma coalesce_in_err_list [rule_format]:

13006

397 
"!xes. xes : list n (err A) \<longrightarrow> coalesce xes : err(list n A)"

10496

398 
apply (induct n)


399 
apply simp


400 
apply clarify


401 
apply (simp add: in_list_Suc_iff)


402 
apply clarify


403 
apply (simp (no_asm) add: plussub_def Err.sup_def lift2_def split: err.split)


404 
apply force


405 
done


406 

13006

407 
lemma lem: "\<And>x xs. x +_(op #) xs = x#xs"

10496

408 
by (simp add: plussub_def)


409 


410 
lemma coalesce_eq_OK1_D [rule_format]:

13006

411 
"semilat(err A, Err.le r, lift2 f) \<Longrightarrow>


412 
!xs. xs : list n A \<longrightarrow> (!ys. ys : list n A \<longrightarrow>


413 
(!zs. coalesce (xs +[f] ys) = OK zs \<longrightarrow> xs <=[r] zs))"

10496

414 
apply (induct n)


415 
apply simp


416 
apply clarify


417 
apply (simp add: in_list_Suc_iff)


418 
apply clarify


419 
apply (simp split: err.split_asm add: lem Err.sup_def lift2_def)


420 
apply (force simp add: semilat_le_err_OK1)


421 
done


422 


423 
lemma coalesce_eq_OK2_D [rule_format]:

13006

424 
"semilat(err A, Err.le r, lift2 f) \<Longrightarrow>


425 
!xs. xs : list n A \<longrightarrow> (!ys. ys : list n A \<longrightarrow>


426 
(!zs. coalesce (xs +[f] ys) = OK zs \<longrightarrow> ys <=[r] zs))"

10496

427 
apply (induct n)


428 
apply simp


429 
apply clarify


430 
apply (simp add: in_list_Suc_iff)


431 
apply clarify


432 
apply (simp split: err.split_asm add: lem Err.sup_def lift2_def)


433 
apply (force simp add: semilat_le_err_OK2)


434 
done


435 


436 
lemma lift2_le_ub:

13006

437 
"\<lbrakk> semilat(err A, Err.le r, lift2 f); x:A; y:A; x +_f y = OK z;


438 
u:A; x <=_r u; y <=_r u \<rbrakk> \<Longrightarrow> z <=_r u"

10496

439 
apply (unfold semilat_Def plussub_def err_def)


440 
apply (simp add: lift2_def)


441 
apply clarify


442 
apply (rotate_tac 3)


443 
apply (erule thin_rl)


444 
apply (erule thin_rl)


445 
apply force


446 
done


447 


448 
lemma coalesce_eq_OK_ub_D [rule_format]:

13006

449 
"semilat(err A, Err.le r, lift2 f) \<Longrightarrow>


450 
!xs. xs : list n A \<longrightarrow> (!ys. ys : list n A \<longrightarrow>

10496

451 
(!zs us. coalesce (xs +[f] ys) = OK zs & xs <=[r] us & ys <=[r] us

13006

452 
& us : list n A \<longrightarrow> zs <=[r] us))"

10496

453 
apply (induct n)


454 
apply simp


455 
apply clarify


456 
apply (simp add: in_list_Suc_iff)


457 
apply clarify


458 
apply (simp (no_asm_use) split: err.split_asm add: lem Err.sup_def lift2_def)


459 
apply clarify


460 
apply (rule conjI)


461 
apply (blast intro: lift2_le_ub)


462 
apply blast


463 
done


464 


465 
lemma lift2_eq_ErrD:

13006

466 
"\<lbrakk> x +_f y = Err; semilat(err A, Err.le r, lift2 f); x:A; y:A \<rbrakk>


467 
\<Longrightarrow> ~(? u:A. x <=_r u & y <=_r u)"

10496

468 
by (simp add: OK_plus_OK_eq_Err_conv [THEN iffD1])


469 


470 


471 
lemma coalesce_eq_Err_D [rule_format]:

13006

472 
"\<lbrakk> semilat(err A, Err.le r, lift2 f) \<rbrakk>


473 
\<Longrightarrow> !xs. xs:list n A \<longrightarrow> (!ys. ys:list n A \<longrightarrow>


474 
coalesce (xs +[f] ys) = Err \<longrightarrow>

10496

475 
~(? zs:list n A. xs <=[r] zs & ys <=[r] zs))"


476 
apply (induct n)


477 
apply simp


478 
apply clarify


479 
apply (simp add: in_list_Suc_iff)


480 
apply clarify


481 
apply (simp split: err.split_asm add: lem Err.sup_def lift2_def)


482 
apply (blast dest: lift2_eq_ErrD)


483 
apply blast


484 
done


485 


486 
lemma closed_err_lift2_conv:


487 
"closed (err A) (lift2 f) = (!x:A. !y:A. x +_f y : err A)"


488 
apply (unfold closed_def)


489 
apply (simp add: err_def)


490 
done


491 


492 
lemma closed_map2_list [rule_format]:

13006

493 
"closed (err A) (lift2 f) \<Longrightarrow>


494 
!xs. xs : list n A \<longrightarrow> (!ys. ys : list n A \<longrightarrow>

10496

495 
map2 f xs ys : list n (err A))"


496 
apply (unfold map2_def)


497 
apply (induct n)


498 
apply simp


499 
apply clarify


500 
apply (simp add: in_list_Suc_iff)


501 
apply clarify


502 
apply (simp add: plussub_def closed_err_lift2_conv)


503 
done


504 


505 
lemma closed_lift2_sup:

13006

506 
"closed (err A) (lift2 f) \<Longrightarrow>

10496

507 
closed (err (list n A)) (lift2 (sup f))"


508 
by (fastsimp simp add: closed_def plussub_def sup_def lift2_def


509 
coalesce_in_err_list closed_map2_list


510 
split: err.split)


511 


512 
lemma err_semilat_sup:

13006

513 
"err_semilat (A,r,f) \<Longrightarrow>

10496

514 
err_semilat (list n A, Listn.le r, sup f)"


515 
apply (unfold Err.sl_def)

10918

516 
apply (simp only: split_conv)

10496

517 
apply (simp (no_asm) only: semilat_Def plussub_def)


518 
apply (simp (no_asm_simp) only: semilatDclosedI closed_lift2_sup)


519 
apply (rule conjI)


520 
apply (drule semilatDorderI)


521 
apply simp


522 
apply (simp (no_asm) only: unfold_lesub_err Err.le_def err_def sup_def lift2_def)


523 
apply (simp (no_asm_simp) add: coalesce_eq_OK1_D coalesce_eq_OK2_D split: err.split)


524 
apply (blast intro: coalesce_eq_OK_ub_D dest: coalesce_eq_Err_D)


525 
done


526 


527 
lemma err_semilat_upto_esl:

13006

528 
"\<And>L. err_semilat L \<Longrightarrow> err_semilat(upto_esl m L)"

10496

529 
apply (unfold Listn.upto_esl_def)


530 
apply (simp (no_asm_simp) only: split_tupled_all)


531 
apply simp


532 
apply (fastsimp intro!: err_semilat_UnionI err_semilat_sup


533 
dest: lesub_list_impl_same_size


534 
simp add: plussub_def Listn.sup_def)


535 
done


536 


537 
end
