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