src/HOL/MicroJava/BV/Listn.thy
 author berghofe Wed Jul 11 11:32:02 2007 +0200 (2007-07-11) changeset 23757 087b0a241557 parent 23464 bc2563c37b1a child 26806 40b411ec05aa permissions -rw-r--r--
- Renamed inductive2 to inductive
- Renamed some theorems about transitive closure for predicates
```     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 Semilat.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 list_n': "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" by this (rule list_n')
```
```   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  "wfP (SUP n. (\<lambda>ys xs. size xs = n & size ys = n & xs <_(Listn.le r) ys))")
```
```   325  apply (erule wfP_subset)
```
```   326  apply (blast intro: lesssub_list_impl_same_size)
```
```   327 apply (rule wfP_SUP)
```
```   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 [to_pred bot_empty_eq] 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: wfP_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
```