src/HOL/MicroJava/BV/Listn.thy
author haftmann
Fri Jun 17 16:12:49 2005 +0200 (2005-06-17)
changeset 16417 9bc16273c2d4
parent 15341 254f6f00b60e
child 22068 00bed5ac9884
permissions -rw-r--r--
migrated theory headers to new format
     1 (*  Title:      HOL/MicroJava/BV/Listn.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   2000 TUM
     5 
     6 Lists of a fixed length
     7 *)
     8 
     9 header {* \isaheader{Fixed Length Lists} *}
    10 
    11 theory Listn imports Err begin
    12 
    13 constdefs
    14 
    15  list :: "nat \<Rightarrow> 'a set \<Rightarrow> 'a list set"
    16 "list n A == {xs. length xs = n & set xs <= A}"
    17 
    18  le :: "'a ord \<Rightarrow> ('a list)ord"
    19 "le r == list_all2 (%x y. x <=_r y)"
    20 
    21 syntax "@lesublist" :: "'a list \<Rightarrow> 'a ord \<Rightarrow> 'a list \<Rightarrow> bool"
    22        ("(_ /<=[_] _)" [50, 0, 51] 50)
    23 syntax "@lesssublist" :: "'a list \<Rightarrow> 'a ord \<Rightarrow> 'a list \<Rightarrow> bool"
    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
    30  map2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list"
    31 "map2 f == (%xs ys. map (split f) (zip xs ys))"
    32 
    33 syntax "@plussublist" :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b list \<Rightarrow> 'c list"
    34        ("(_ /+[_] _)" [65, 0, 66] 65)
    35 translations  "x +[f] y" == "x +_(map2 f) y"
    36 
    37 consts coalesce :: "'a err list \<Rightarrow> 'a list err"
    38 primrec
    39 "coalesce [] = OK[]"
    40 "coalesce (ex#exs) = Err.sup (op #) ex (coalesce exs)"
    41 
    42 constdefs
    43  sl :: "nat \<Rightarrow> 'a sl \<Rightarrow> 'a list sl"
    44 "sl n == %(A,r,f). (list n A, le r, map2 f)"
    45 
    46  sup :: "('a \<Rightarrow> 'b \<Rightarrow> 'c err) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list err"
    47 "sup f == %xs ys. if size xs = size ys then coalesce(xs +[f] ys) else Err"
    48 
    49  upto_esl :: "nat \<Rightarrow> 'a esl \<Rightarrow> 'a list esl"
    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]:
    78   "order r \<Longrightarrow> 
    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:
    86   "\<lbrakk> i<size xs; xs <=[r] ys; x <=_r y \<rbrakk> \<Longrightarrow> xs[i:=x] <=[r] ys[i:=y]";
    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:
    94   "\<lbrakk> xs <=[r] ys; p < size xs \<rbrakk> \<Longrightarrow> xs!p <=_r ys!p"
    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:
   100   "!x. x <=_r x \<Longrightarrow> xs <=[r] xs"
   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:
   106   "\<lbrakk> order r; xs <=[r] ys; ys <=[r] zs \<rbrakk> \<Longrightarrow> xs <=[r] zs"
   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:
   115   "\<lbrakk> order r; xs <=[r] ys; ys <=[r] xs \<rbrakk> \<Longrightarrow> xs = ys"
   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!]:
   126   "order r \<Longrightarrow> order(Listn.le r)"
   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]:
   134   "xs <=[r] ys \<Longrightarrow> size ys = size xs"  
   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:
   140   "xs <_(Listn.le r) ys \<Longrightarrow> size ys = size xs"
   141 apply (unfold lesssub_def)
   142 apply auto
   143 done  
   144 
   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 
   159 lemma listI:
   160   "\<lbrakk> length xs = n; set xs <= A \<rbrakk> \<Longrightarrow> xs : list n A"
   161 apply (unfold list_def)
   162 apply blast
   163 done
   164 
   165 lemma listE_length [simp]:
   166    "xs : list n A \<Longrightarrow> length xs = n"
   167 apply (unfold list_def)
   168 apply blast
   169 done 
   170 
   171 lemma less_lengthI:
   172   "\<lbrakk> xs : list n A; p < n \<rbrakk> \<Longrightarrow> p < length xs"
   173   by simp
   174 
   175 lemma listE_set [simp]:
   176   "xs : list n A \<Longrightarrow> set xs <= A"
   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) = (\<exists>y\<in> A. \<exists>ys\<in> 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\<in> A & xs : list n A)";
   196 apply (simp add: in_list_Suc_iff)
   197 done 
   198 
   199 lemma list_not_empty:
   200   "\<exists>a. a\<in> A \<Longrightarrow> \<exists>xs. xs : list n A";
   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]:
   209   "!i n. length xs = n \<longrightarrow> set xs <= A \<longrightarrow> i < n \<longrightarrow> (xs!i) : A"
   210 apply (induct "xs")
   211  apply simp
   212 apply (simp add: nth_Cons split: nat.split)
   213 done
   214 
   215 lemma listE_nth_in:
   216   "\<lbrakk> xs : list n A; i < n \<rbrakk> \<Longrightarrow> (xs!i) : A"
   217   by auto
   218 
   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 
   250 lemma listt_update_in_list [simp, intro!]:
   251   "\<lbrakk> xs : list n A; x\<in> A \<rbrakk> \<Longrightarrow> xs[i := x] : list n A"
   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]:
   263   "(x#xs) +[f] ys = (case ys of [] \<Rightarrow> [] | y#ys \<Rightarrow> (x +_f y)#(xs +[f] ys))"
   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]:
   275   "!xs ys i. length xs = n \<longrightarrow> length ys = n \<longrightarrow> i<n \<longrightarrow> 
   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 (in semilat) plus_list_ub1 [rule_format]:
   287  "\<lbrakk> set xs <= A; set ys <= A; size xs = size ys \<rbrakk> 
   288   \<Longrightarrow> xs <=[r] xs +[f] ys"
   289 apply (unfold unfold_lesub_list)
   290 apply (simp add: Listn.le_def list_all2_conv_all_nth)
   291 done
   292 
   293 lemma (in semilat) plus_list_ub2:
   294  "\<lbrakk>set xs <= A; set ys <= A; size xs = size ys \<rbrakk>
   295   \<Longrightarrow> ys <=[r] xs +[f] ys"
   296 apply (unfold unfold_lesub_list)
   297 apply (simp add: Listn.le_def list_all2_conv_all_nth)
   298 done
   299 
   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 
   302   \<longrightarrow> size xs = n & size ys = n \<longrightarrow> 
   303   xs <=[r] zs & ys <=[r] zs \<longrightarrow> xs +[f] ys <=[r] zs"
   304 apply (unfold unfold_lesub_list)
   305 apply (simp add: Listn.le_def list_all2_conv_all_nth)
   306 done
   307 
   308 lemma (in semilat) list_update_incr [rule_format]:
   309  "x\<in> A \<Longrightarrow> set xs <= A \<longrightarrow> 
   310   (!i. i<size xs \<longrightarrow> xs <=[r] xs[i := x +_f xs!i])"
   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!]:
   321   "\<lbrakk> order r; acc r \<rbrakk> \<Longrightarrow> acc(Listn.le r)"
   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 (fast intro!: equals0I dest: not_sym)
   334 apply clarify
   335 apply (rename_tac n)
   336 apply (induct_tac n)
   337  apply (simp add: lesssub_def cong: conj_cong)
   338 apply (rename_tac k)
   339 apply (simp add: wf_eq_minimal)
   340 apply (simp (no_asm) add: length_Suc_conv cong: conj_cong)
   341 apply clarify
   342 apply (rename_tac M m)
   343 apply (case_tac "\<exists>x xs. size xs = k & x#xs : M")
   344  prefer 2
   345  apply (erule thin_rl)
   346  apply (erule thin_rl)
   347  apply blast
   348 apply (erule_tac x = "{a. \<exists>xs. size xs = k & a#xs:M}" in allE)
   349 apply (erule impE)
   350  apply blast
   351 apply (thin_tac "\<exists>x xs. ?P x xs")
   352 apply clarify
   353 apply (rename_tac maxA xs)
   354 apply (erule_tac x = "{ys. size ys = size xs & maxA#ys : M}" in allE)
   355 apply (erule impE)
   356  apply blast
   357 apply clarify
   358 apply (thin_tac "m : M")
   359 apply (thin_tac "maxA#xs : M")
   360 apply (rule bexI)
   361  prefer 2
   362  apply assumption
   363 apply clarify
   364 apply simp
   365 apply blast
   366 done 
   367 
   368 lemma closed_listI:
   369   "closed S f \<Longrightarrow> closed (list n S) (map2 f)"
   370 apply (unfold closed_def)
   371 apply (induct n)
   372  apply simp
   373 apply clarify
   374 apply (simp add: in_list_Suc_iff)
   375 apply clarify
   376 apply simp
   377 done
   378 
   379 
   380 lemma Listn_sl_aux:
   381 includes semilat shows "semilat (Listn.sl n (A,r,f))"
   382 apply (unfold Listn.sl_def)
   383 apply (simp (no_asm) only: semilat_Def split_conv)
   384 apply (rule conjI)
   385  apply simp
   386 apply (rule conjI)
   387  apply (simp only: closedI closed_listI)
   388 apply (simp (no_asm) only: list_def)
   389 apply (simp (no_asm_simp) add: plus_list_ub1 plus_list_ub2 plus_list_lub)
   390 done
   391 
   392 lemma Listn_sl: "\<And>L. semilat L \<Longrightarrow> semilat (Listn.sl n L)"
   393  by(simp add: Listn_sl_aux split_tupled_all)
   394 
   395 lemma coalesce_in_err_list [rule_format]:
   396   "!xes. xes : list n (err A) \<longrightarrow> coalesce xes : err(list n A)"
   397 apply (induct n)
   398  apply simp
   399 apply clarify
   400 apply (simp add: in_list_Suc_iff)
   401 apply clarify
   402 apply (simp (no_asm) add: plussub_def Err.sup_def lift2_def split: err.split)
   403 apply force
   404 done 
   405 
   406 lemma lem: "\<And>x xs. x +_(op #) xs = x#xs"
   407   by (simp add: plussub_def)
   408 
   409 lemma coalesce_eq_OK1_D [rule_format]:
   410   "semilat(err A, Err.le r, lift2 f) \<Longrightarrow> 
   411   !xs. xs : list n A \<longrightarrow> (!ys. ys : list n A \<longrightarrow> 
   412   (!zs. coalesce (xs +[f] ys) = OK zs \<longrightarrow> xs <=[r] zs))"
   413 apply (induct n)
   414   apply simp
   415 apply clarify
   416 apply (simp add: in_list_Suc_iff)
   417 apply clarify
   418 apply (simp split: err.split_asm add: lem Err.sup_def lift2_def)
   419 apply (force simp add: semilat_le_err_OK1)
   420 done
   421 
   422 lemma coalesce_eq_OK2_D [rule_format]:
   423   "semilat(err A, Err.le r, lift2 f) \<Longrightarrow> 
   424   !xs. xs : list n A \<longrightarrow> (!ys. ys : list n A \<longrightarrow> 
   425   (!zs. coalesce (xs +[f] ys) = OK zs \<longrightarrow> ys <=[r] zs))"
   426 apply (induct n)
   427  apply simp
   428 apply clarify
   429 apply (simp add: in_list_Suc_iff)
   430 apply clarify
   431 apply (simp split: err.split_asm add: lem Err.sup_def lift2_def)
   432 apply (force simp add: semilat_le_err_OK2)
   433 done 
   434 
   435 lemma lift2_le_ub:
   436   "\<lbrakk> semilat(err A, Err.le r, lift2 f); x\<in> A; y\<in> A; x +_f y = OK z; 
   437       u\<in> A; x <=_r u; y <=_r u \<rbrakk> \<Longrightarrow> z <=_r u"
   438 apply (unfold semilat_Def plussub_def err_def)
   439 apply (simp add: lift2_def)
   440 apply clarify
   441 apply (rotate_tac -3)
   442 apply (erule thin_rl)
   443 apply (erule thin_rl)
   444 apply force
   445 done
   446 
   447 lemma coalesce_eq_OK_ub_D [rule_format]:
   448   "semilat(err A, Err.le r, lift2 f) \<Longrightarrow> 
   449   !xs. xs : list n A \<longrightarrow> (!ys. ys : list n A \<longrightarrow> 
   450   (!zs us. coalesce (xs +[f] ys) = OK zs & xs <=[r] us & ys <=[r] us 
   451            & us : list n A \<longrightarrow> zs <=[r] us))"
   452 apply (induct n)
   453  apply simp
   454 apply clarify
   455 apply (simp add: in_list_Suc_iff)
   456 apply clarify
   457 apply (simp (no_asm_use) split: err.split_asm add: lem Err.sup_def lift2_def)
   458 apply clarify
   459 apply (rule conjI)
   460  apply (blast intro: lift2_le_ub)
   461 apply blast
   462 done 
   463 
   464 lemma lift2_eq_ErrD:
   465   "\<lbrakk> x +_f y = Err; semilat(err A, Err.le r, lift2 f); x\<in> A; y\<in> A \<rbrakk> 
   466   \<Longrightarrow> ~(\<exists>u\<in> A. x <=_r u & y <=_r u)"
   467   by (simp add: OK_plus_OK_eq_Err_conv [THEN iffD1])
   468 
   469 
   470 lemma coalesce_eq_Err_D [rule_format]:
   471   "\<lbrakk> semilat(err A, Err.le r, lift2 f) \<rbrakk> 
   472   \<Longrightarrow> !xs. xs\<in> list n A \<longrightarrow> (!ys. ys\<in> list n A \<longrightarrow> 
   473       coalesce (xs +[f] ys) = Err \<longrightarrow> 
   474       ~(\<exists>zs\<in> list n A. xs <=[r] zs & ys <=[r] zs))"
   475 apply (induct n)
   476  apply simp
   477 apply clarify
   478 apply (simp add: in_list_Suc_iff)
   479 apply clarify
   480 apply (simp split: err.split_asm add: lem Err.sup_def lift2_def)
   481  apply (blast dest: lift2_eq_ErrD)
   482 done 
   483 
   484 lemma closed_err_lift2_conv:
   485   "closed (err A) (lift2 f) = (\<forall>x\<in> A. \<forall>y\<in> A. x +_f y : err A)"
   486 apply (unfold closed_def)
   487 apply (simp add: err_def)
   488 done 
   489 
   490 lemma closed_map2_list [rule_format]:
   491   "closed (err A) (lift2 f) \<Longrightarrow> 
   492   \<forall>xs. xs : list n A \<longrightarrow> (\<forall>ys. ys : list n A \<longrightarrow> 
   493   map2 f xs ys : list n (err A))"
   494 apply (unfold map2_def)
   495 apply (induct n)
   496  apply simp
   497 apply clarify
   498 apply (simp add: in_list_Suc_iff)
   499 apply clarify
   500 apply (simp add: plussub_def closed_err_lift2_conv)
   501 done
   502 
   503 lemma closed_lift2_sup:
   504   "closed (err A) (lift2 f) \<Longrightarrow> 
   505   closed (err (list n A)) (lift2 (sup f))"
   506   by (fastsimp  simp add: closed_def plussub_def sup_def lift2_def
   507                           coalesce_in_err_list closed_map2_list
   508                 split: err.split)
   509 
   510 lemma err_semilat_sup:
   511   "err_semilat (A,r,f) \<Longrightarrow> 
   512   err_semilat (list n A, Listn.le r, sup f)"
   513 apply (unfold Err.sl_def)
   514 apply (simp only: split_conv)
   515 apply (simp (no_asm) only: semilat_Def plussub_def)
   516 apply (simp (no_asm_simp) only: semilat.closedI closed_lift2_sup)
   517 apply (rule conjI)
   518  apply (drule semilat.orderI)
   519  apply simp
   520 apply (simp (no_asm) only: unfold_lesub_err Err.le_def err_def sup_def lift2_def)
   521 apply (simp (no_asm_simp) add: coalesce_eq_OK1_D coalesce_eq_OK2_D split: err.split)
   522 apply (blast intro: coalesce_eq_OK_ub_D dest: coalesce_eq_Err_D)
   523 done 
   524 
   525 lemma err_semilat_upto_esl:
   526   "\<And>L. err_semilat L \<Longrightarrow> err_semilat(upto_esl m L)"
   527 apply (unfold Listn.upto_esl_def)
   528 apply (simp (no_asm_simp) only: split_tupled_all)
   529 apply simp
   530 apply (fastsimp intro!: err_semilat_UnionI err_semilat_sup
   531                 dest: lesub_list_impl_same_size 
   532                 simp add: plussub_def Listn.sup_def)
   533 done
   534 
   535 end