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