# Theory Listn

Up to index of Isabelle/HOL/MicroJava

theory Listn
imports Err
begin

    (*  Title:      HOL/MicroJava/BV/Listn.thy
        ID:         $Id: Listn.thy,v 1.11 2005/06/17 14:13:08 haftmann Exp $
        Author:     Tobias Nipkow
        Copyright   2000 TUM

    Lists of a fixed length
    *)

    header {* \isaheader{Fixed Length Lists} *}

    theory Listn imports Err begin

    constdefs

     list :: "nat => 'a set => 'a list set"
    "list n A == {xs. length xs = n & set xs <= A}"

     le :: "'a ord => ('a list)ord"
    "le r == list_all2 (%x y. x <=_r y)"

    syntax "@lesublist" :: "'a list => 'a ord => 'a list => bool"
           ("(_ /<=[_] _)" [50, 0, 51] 50)
    syntax "@lesssublist" :: "'a list => 'a ord => 'a list => bool"
           ("(_ /<[_] _)" [50, 0, 51] 50)
    translations
     "x <=[r] y" == "x <=_(Listn.le r) y"
     "x <[r] y"  == "x <_(Listn.le r) y"

    constdefs
     map2 :: "('a => 'b => 'c) => 'a list => 'b list => 'c list"
    "map2 f == (%xs ys. map (split f) (zip xs ys))"

    syntax "@plussublist" :: "'a list => ('a => 'b => 'c) => 'b list => 'c list"
           ("(_ /+[_] _)" [65, 0, 66] 65)
    translations  "x +[f] y" == "x +_(map2 f) y"

    consts coalesce :: "'a err list => 'a list err"
    primrec
    "coalesce [] = OK[]"
    "coalesce (ex#exs) = Err.sup (op #) ex (coalesce exs)"

    constdefs
     sl :: "nat => 'a sl => 'a list sl"
    "sl n == %(A,r,f). (list n A, le r, map2 f)"

     sup :: "('a => 'b => 'c err) => 'a list => 'b list => 'c list err"
    "sup f == %xs ys. if size xs = size ys then coalesce(xs +[f] ys) else Err"

     upto_esl :: "nat => 'a esl => 'a list esl"
    "upto_esl m == %(A,r,f). (Union{list n A |n. n <= m}, le r, sup f)"

    lemmas [simp] = set_update_subsetI

    lemma unfold_lesub_list:
      "xs <=[r] ys == Listn.le r xs ys"
      by (simp add: lesub_def)

    lemma Nil_le_conv [iff]:
      "([] <=[r] ys) = (ys = [])"
    apply (unfold lesub_def Listn.le_def)
    apply simp
    done

    lemma Cons_notle_Nil [iff]:
      "~ x#xs <=[r] []"
    apply (unfold lesub_def Listn.le_def)
    apply simp
    done

    lemma Cons_le_Cons [iff]:
      "x#xs <=[r] y#ys = (x <=_r y & xs <=[r] ys)"
    apply (unfold lesub_def Listn.le_def)
    apply simp
    done

    lemma Cons_less_Conss [simp]:
      "order r ==>
      x#xs <_(Listn.le r) y#ys =
      (x <_r y & xs <=[r] ys  |  x = y & xs <_(Listn.le r) ys)"
    apply (unfold lesssub_def)
    apply blast
    done

    lemma list_update_le_cong:
      "[| i<size xs; xs <=[r] ys; x <=_r y |] ==> xs[i:=x] <=[r] ys[i:=y]";
    apply (unfold unfold_lesub_list)
    apply (unfold Listn.le_def)
    apply (simp add: list_all2_conv_all_nth nth_list_update)
    done

    lemma le_listD:
      "[| xs <=[r] ys; p < size xs |] ==> xs!p <=_r ys!p"
    apply (unfold Listn.le_def lesub_def)
    apply (simp add: list_all2_conv_all_nth)
    done

    lemma le_list_refl:
      "!x. x <=_r x ==> xs <=[r] xs"
    apply (unfold unfold_lesub_list)
    apply (simp add: Listn.le_def list_all2_conv_all_nth)
    done

    lemma le_list_trans:
      "[| order r; xs <=[r] ys; ys <=[r] zs |] ==> xs <=[r] zs"
    apply (unfold unfold_lesub_list)
    apply (simp add: Listn.le_def list_all2_conv_all_nth)
    apply clarify
    apply simp
    apply (blast intro: order_trans)
    done

    lemma le_list_antisym:
      "[| order r; xs <=[r] ys; ys <=[r] xs |] ==> xs = ys"
    apply (unfold unfold_lesub_list)
    apply (simp add: Listn.le_def list_all2_conv_all_nth)
    apply (rule nth_equalityI)
     apply blast
    apply clarify
    apply simp
    apply (blast intro: order_antisym)
    done

    lemma order_listI [simp, intro!]:
      "order r ==> order(Listn.le r)"
    apply (subst order_def)
    apply (blast intro: le_list_refl le_list_trans le_list_antisym
                 dest: order_refl)
    done

    lemma lesub_list_impl_same_size [simp]:
      "xs <=[r] ys ==> size ys = size xs"
    apply (unfold Listn.le_def lesub_def)
    apply (simp add: list_all2_conv_all_nth)
    done

    lemma lesssub_list_impl_same_size:
      "xs <_(Listn.le r) ys ==> size ys = size xs"
    apply (unfold lesssub_def)
    apply auto
    done

    lemma le_list_appendI:
      "!!b c d. a <=[r] b ==> c <=[r] d ==> a@c <=[r] b@d"
    apply (induct a)
     apply simp
    apply (case_tac b)
    apply auto
    done

    lemma le_listI:
      "length a = length b ==> (!!n. n < length a ==> a!n <=_r b!n) ==> a <=[r] b"
      apply (unfold lesub_def Listn.le_def)
      apply (simp add: list_all2_conv_all_nth)
      done

    lemma listI:
      "[| length xs = n; set xs <= A |] ==> xs : list n A"
    apply (unfold list_def)
    apply blast
    done

    lemma listE_length [simp]:
       "xs : list n A ==> length xs = n"
    apply (unfold list_def)
    apply blast
    done

    lemma less_lengthI:
      "[| xs : list n A; p < n |] ==> p < length xs"
      by simp

    lemma listE_set [simp]:
      "xs : list n A ==> set xs <= A"
    apply (unfold list_def)
    apply blast
    done

    lemma list_0 [simp]:
      "list 0 A = {[]}"
    apply (unfold list_def)
    apply auto
    done

    lemma in_list_Suc_iff:
      "(xs : list (Suc n) A) = (∃y∈ A. ∃ys∈ list n A. xs = y#ys)"
    apply (unfold list_def)
    apply (case_tac "xs")
    apply auto
    done

    lemma Cons_in_list_Suc [iff]:
      "(x#xs : list (Suc n) A) = (x∈ A & xs : list n A)";
    apply (simp add: in_list_Suc_iff)
    done

    lemma list_not_empty:
      "∃a. a∈ A ==> ∃xs. xs : list n A";
    apply (induct "n")
     apply simp
    apply (simp add: in_list_Suc_iff)
    apply blast
    done

    lemma nth_in [rule_format, simp]:
      "!i n. length xs = n --> set xs <= A --> i < n --> (xs!i) : A"
    apply (induct "xs")
     apply simp
    apply (simp add: nth_Cons split: nat.split)
    done

    lemma listE_nth_in:
      "[| xs : list n A; i < n |] ==> (xs!i) : A"
      by auto

    lemma listn_Cons_Suc [elim!]:
      "l#xs ∈ list n A ==> (!!n'. n = Suc n' ==> l ∈ A ==> xs ∈ list n' A ==> P) ==> P"
      by (cases n) auto

    lemma listn_appendE [elim!]:
      "a@b ∈ list n A ==> (!!n1 n2. n=n1+n2 ==> a ∈ list n1 A ==> b ∈ list n2 A ==> P) ==> P"
    proof -
      have "!!n. a@b ∈ list n A ==> ∃n1 n2. n=n1+n2 ∧ a ∈ list n1 A ∧ b ∈ list n2 A"
        (is "!!n. ?list a n ==> ∃n1 n2. ?P a n n1 n2")
      proof (induct a)
        fix n assume "?list [] n"
        hence "?P [] n 0 n" by simp
        thus "∃n1 n2. ?P [] n n1 n2" by fast
      next
        fix n l ls
        assume "?list (l#ls) n"
        then obtain n' where n: "n = Suc n'" "l ∈ A" and "ls@b ∈ list n' A" by fastsimp
        assume "!!n. ls @ b ∈ list n A ==> ∃n1 n2. n = n1 + n2 ∧ ls ∈ list n1 A ∧ b ∈ list n2 A"
        hence "∃n1 n2. n' = n1 + n2 ∧ ls ∈ list n1 A ∧ b ∈ list n2 A" .
        then obtain n1 n2 where "n' = n1 + n2" "ls ∈ list n1 A" "b ∈ list n2 A" by fast
        with n have "?P (l#ls) n (n1+1) n2" by simp
        thus "∃n1 n2. ?P (l#ls) n n1 n2" by fastsimp
      qed
      moreover
      assume "a@b ∈ list n A" "!!n1 n2. n=n1+n2 ==> a ∈ list n1 A ==> b ∈ list n2 A ==> P"
      ultimately
      show ?thesis by blast
    qed

    lemma listt_update_in_list [simp, intro!]:
      "[| xs : list n A; x∈ A |] ==> xs[i := x] : list n A"
    apply (unfold list_def)
    apply simp
    done

    lemma plus_list_Nil [simp]:
      "[] +[f] xs = []"
    apply (unfold plussub_def map2_def)
    apply simp
    done

    lemma plus_list_Cons [simp]:
      "(x#xs) +[f] ys = (case ys of [] => [] | y#ys => (x +_f y)#(xs +[f] ys))"
      by (simp add: plussub_def map2_def split: list.split)

    lemma length_plus_list [rule_format, simp]:
      "!ys. length(xs +[f] ys) = min(length xs) (length ys)"
    apply (induct xs)
     apply simp
    apply clarify
    apply (simp (no_asm_simp) split: list.split)
    done

    lemma nth_plus_list [rule_format, simp]:
      "!xs ys i. length xs = n --> length ys = n --> i<n -->
      (xs +[f] ys)!i = (xs!i) +_f (ys!i)"
    apply (induct n)
     apply simp
    apply clarify
    apply (case_tac xs)
     apply simp
    apply (force simp add: nth_Cons split: list.split nat.split)
    done

    lemma (in semilat) plus_list_ub1 [rule_format]:
     "[| set xs <= A; set ys <= A; size xs = size ys |]
      ==> xs <=[r] xs +[f] ys"
    apply (unfold unfold_lesub_list)
    apply (simp add: Listn.le_def list_all2_conv_all_nth)
    done

    lemma (in semilat) plus_list_ub2:
     "[|set xs <= A; set ys <= A; size xs = size ys |]
      ==> ys <=[r] xs +[f] ys"
    apply (unfold unfold_lesub_list)
    apply (simp add: Listn.le_def list_all2_conv_all_nth)
    done

    lemma (in semilat) plus_list_lub [rule_format]:
    shows "!xs ys zs. set xs <= A --> set ys <= A --> set zs <= A
      --> size xs = n & size ys = n -->
      xs <=[r] zs & ys <=[r] zs --> xs +[f] ys <=[r] zs"
    apply (unfold unfold_lesub_list)
    apply (simp add: Listn.le_def list_all2_conv_all_nth)
    done

    lemma (in semilat) list_update_incr [rule_format]:
     "x∈ A ==> set xs <= A -->
      (!i. i<size xs --> xs <=[r] xs[i := x +_f xs!i])"
    apply (unfold unfold_lesub_list)
    apply (simp add: Listn.le_def list_all2_conv_all_nth)
    apply (induct xs)
     apply simp
    apply (simp add: in_list_Suc_iff)
    apply clarify
    apply (simp add: nth_Cons split: nat.split)
    done

    lemma acc_le_listI [intro!]:
      "[| order r; acc r |] ==> acc(Listn.le r)"
    apply (unfold acc_def)
    apply (subgoal_tac
     "wf(UN n. {(ys,xs). size xs = n & size ys = n & xs <_(Listn.le r) ys})")
     apply (erule wf_subset)
     apply (blast intro: lesssub_list_impl_same_size)
    apply (rule wf_UN)
     prefer 2
     apply clarify
     apply (rename_tac m n)
     apply (case_tac "m=n")
      apply simp
     apply (fast intro!: equals0I dest: not_sym)
    apply clarify
    apply (rename_tac n)
    apply (induct_tac n)
     apply (simp add: lesssub_def cong: conj_cong)
    apply (rename_tac k)
    apply (simp add: wf_eq_minimal)
    apply (simp (no_asm) add: length_Suc_conv cong: conj_cong)
    apply clarify
    apply (rename_tac M m)
    apply (case_tac "∃x xs. size xs = k & x#xs : M")
     prefer 2
     apply (erule thin_rl)
     apply (erule thin_rl)
     apply blast
    apply (erule_tac x = "{a. ∃xs. size xs = k & a#xs:M}" in allE)
    apply (erule impE)
     apply blast
    apply (thin_tac "∃x xs. ?P x xs")
    apply clarify
    apply (rename_tac maxA xs)
    apply (erule_tac x = "{ys. size ys = size xs & maxA#ys : M}" in allE)
    apply (erule impE)
     apply blast
    apply clarify
    apply (thin_tac "m : M")
    apply (thin_tac "maxA#xs : M")
    apply (rule bexI)
     prefer 2
     apply assumption
    apply clarify
    apply simp
    apply blast
    done

    lemma closed_listI:
      "closed S f ==> closed (list n S) (map2 f)"
    apply (unfold closed_def)
    apply (induct n)
     apply simp
    apply clarify
    apply (simp add: in_list_Suc_iff)
    apply clarify
    apply simp
    done

    lemma Listn_sl_aux:
    includes semilat shows "semilat (Listn.sl n (A,r,f))"
    apply (unfold Listn.sl_def)
    apply (simp (no_asm) only: semilat_Def split_conv)
    apply (rule conjI)
     apply simp
    apply (rule conjI)
     apply (simp only: closedI closed_listI)
    apply (simp (no_asm) only: list_def)
    apply (simp (no_asm_simp) add: plus_list_ub1 plus_list_ub2 plus_list_lub)
    done

    lemma Listn_sl: "!!L. semilat L ==> semilat (Listn.sl n L)"
     by(simp add: Listn_sl_aux split_tupled_all)

    lemma coalesce_in_err_list [rule_format]:
      "!xes. xes : list n (err A) --> coalesce xes : err(list n A)"
    apply (induct n)
     apply simp
    apply clarify
    apply (simp add: in_list_Suc_iff)
    apply clarify
    apply (simp (no_asm) add: plussub_def Err.sup_def lift2_def split: err.split)
    apply force
    done

    lemma lem: "!!x xs. x +_(op #) xs = x#xs"
      by (simp add: plussub_def)

    lemma coalesce_eq_OK1_D [rule_format]:
      "semilat(err A, Err.le r, lift2 f) ==>
      !xs. xs : list n A --> (!ys. ys : list n A -->
      (!zs. coalesce (xs +[f] ys) = OK zs --> xs <=[r] zs))"
    apply (induct n)
      apply simp
    apply clarify
    apply (simp add: in_list_Suc_iff)
    apply clarify
    apply (simp split: err.split_asm add: lem Err.sup_def lift2_def)
    apply (force simp add: semilat_le_err_OK1)
    done

    lemma coalesce_eq_OK2_D [rule_format]:
      "semilat(err A, Err.le r, lift2 f) ==>
      !xs. xs : list n A --> (!ys. ys : list n A -->
      (!zs. coalesce (xs +[f] ys) = OK zs --> ys <=[r] zs))"
    apply (induct n)
     apply simp
    apply clarify
    apply (simp add: in_list_Suc_iff)
    apply clarify
    apply (simp split: err.split_asm add: lem Err.sup_def lift2_def)
    apply (force simp add: semilat_le_err_OK2)
    done

    lemma lift2_le_ub:
      "[| semilat(err A, Err.le r, lift2 f); x∈ A; y∈ A; x +_f y = OK z;
          u∈ A; x <=_r u; y <=_r u |] ==> z <=_r u"
    apply (unfold semilat_Def plussub_def err_def)
    apply (simp add: lift2_def)
    apply clarify
    apply (rotate_tac -3)
    apply (erule thin_rl)
    apply (erule thin_rl)
    apply force
    done

    lemma coalesce_eq_OK_ub_D [rule_format]:
      "semilat(err A, Err.le r, lift2 f) ==>
      !xs. xs : list n A --> (!ys. ys : list n A -->
      (!zs us. coalesce (xs +[f] ys) = OK zs & xs <=[r] us & ys <=[r] us
               & us : list n A --> zs <=[r] us))"
    apply (induct n)
     apply simp
    apply clarify
    apply (simp add: in_list_Suc_iff)
    apply clarify
    apply (simp (no_asm_use) split: err.split_asm add: lem Err.sup_def lift2_def)
    apply clarify
    apply (rule conjI)
     apply (blast intro: lift2_le_ub)
    apply blast
    done

    lemma lift2_eq_ErrD:
      "[| x +_f y = Err; semilat(err A, Err.le r, lift2 f); x∈ A; y∈ A |]
      ==> ~(∃u∈ A. x <=_r u & y <=_r u)"
      by (simp add: OK_plus_OK_eq_Err_conv [THEN iffD1])

    lemma coalesce_eq_Err_D [rule_format]:
      "[| semilat(err A, Err.le r, lift2 f) |]
      ==> !xs. xs∈ list n A --> (!ys. ys∈ list n A -->
          coalesce (xs +[f] ys) = Err -->
          ~(∃zs∈ list n A. xs <=[r] zs & ys <=[r] zs))"
    apply (induct n)
     apply simp
    apply clarify
    apply (simp add: in_list_Suc_iff)
    apply clarify
    apply (simp split: err.split_asm add: lem Err.sup_def lift2_def)
     apply (blast dest: lift2_eq_ErrD)
    done

    lemma closed_err_lift2_conv:
      "closed (err A) (lift2 f) = (∀x∈ A. ∀y∈ A. x +_f y : err A)"
    apply (unfold closed_def)
    apply (simp add: err_def)
    done

    lemma closed_map2_list [rule_format]:
      "closed (err A) (lift2 f) ==>
      ∀xs. xs : list n A --> (∀ys. ys : list n A -->
      map2 f xs ys : list n (err A))"
    apply (unfold map2_def)
    apply (induct n)
     apply simp
    apply clarify
    apply (simp add: in_list_Suc_iff)
    apply clarify
    apply (simp add: plussub_def closed_err_lift2_conv)
    done

    lemma closed_lift2_sup:
      "closed (err A) (lift2 f) ==>
      closed (err (list n A)) (lift2 (sup f))"
      by (fastsimp  simp add: closed_def plussub_def sup_def lift2_def
                              coalesce_in_err_list closed_map2_list
                    split: err.split)

    lemma err_semilat_sup:
      "err_semilat (A,r,f) ==>
      err_semilat (list n A, Listn.le r, sup f)"
    apply (unfold Err.sl_def)
    apply (simp only: split_conv)
    apply (simp (no_asm) only: semilat_Def plussub_def)
    apply (simp (no_asm_simp) only: semilat.closedI closed_lift2_sup)
    apply (rule conjI)
     apply (drule semilat.orderI)
     apply simp
    apply (simp (no_asm) only: unfold_lesub_err Err.le_def err_def sup_def lift2_def)
    apply (simp (no_asm_simp) add: coalesce_eq_OK1_D coalesce_eq_OK2_D split: err.split)
    apply (blast intro: coalesce_eq_OK_ub_D dest: coalesce_eq_Err_D)
    done

    lemma err_semilat_upto_esl:
      "!!L. err_semilat L ==> err_semilat(upto_esl m L)"
    apply (unfold Listn.upto_esl_def)
    apply (simp (no_asm_simp) only: split_tupled_all)
    apply simp
    apply (fastsimp intro!: err_semilat_UnionI err_semilat_sup
                    dest: lesub_list_impl_same_size
                    simp add: plussub_def Listn.sup_def)
    done

    end

lemmas

      [| set xs ⊆ A; x ∈ A |] ==> set (xs[i := x]) ⊆ A

lemmas

      [| set xs ⊆ A; x ∈ A |] ==> set (xs[i := x]) ⊆ A

lemma unfold_lesub_list:

      xs <=[r] ys == Listn.le r xs ys

lemma Nil_le_conv:

      ([] <=[r] ys) = (ys = [])

lemma Cons_notle_Nil:

      ¬ x # xs <=[r] []

lemma Cons_le_Cons:

      (x # xs <=[r] y # ys) = (x <=_r y ∧ xs <=[r] ys)

lemma Cons_less_Conss:

      order r ==> (x # xs <[r] y # ys) = (x <_r y ∧ xs <=[r] ys ∨ x = y ∧ xs <[r] ys)

lemma list_update_le_cong:

      [| i < length xs; xs <=[r] ys; x <=_r y |] ==> xs[i := x] <=[r] ys[i := y]

lemma le_listD:

      [| xs <=[r] ys; p < length xs |] ==> xs ! p <=_r ys ! p

lemma le_list_refl:

      ∀x. x <=_r x ==> xs <=[r] xs

lemma le_list_trans:

      [| order r; xs <=[r] ys; ys <=[r] zs |] ==> xs <=[r] zs

lemma le_list_antisym:

      [| order r; xs <=[r] ys; ys <=[r] xs |] ==> xs = ys

lemma order_listI:

      order r ==> order (Listn.le r)

lemma lesub_list_impl_same_size:

      xs <=[r] ys ==> length ys = length xs

lemma lesssub_list_impl_same_size:

      xs <[r] ys ==> length ys = length xs

lemma le_list_appendI:

      [| a <=[r] b; c <=[r] d |] ==> a @ c <=[r] b @ d

lemma le_listI:

      [| length a = length b; !!n. n < length a ==> a ! n <=_r b ! n |] ==> a <=[r] b

lemma listI:

      [| length xs = n; set xs ⊆ A |] ==> xs ∈ list n A

lemma listE_length:

      xs ∈ list n A ==> length xs = n

lemma less_lengthI:

      [| xs ∈ list n A; p < n |] ==> p < length xs

lemma listE_set:

      xs ∈ list n A ==> set xs ⊆ A

lemma list_0:

      list 0 A = {[]}

lemma in_list_Suc_iff:

      (xs ∈ list (Suc n) A) = (∃y∈A. ∃ys∈list n A. xs = y # ys)

lemma Cons_in_list_Suc:

      (x # xs ∈ list (Suc n) A) = (x ∈ A ∧ xs ∈ list n A)

lemma list_not_empty:

      ∃a. a ∈ A ==> ∃xs. xs ∈ list n A

lemma nth_in:

      [| length xs = n; set xs ⊆ A; i < n |] ==> xs ! i ∈ A

lemma listE_nth_in:

      [| xs ∈ list n A; i < n |] ==> xs ! i ∈ A

lemma listn_Cons_Suc:

      [| l # xs ∈ list n A; !!n'. [| n = Suc n'; l ∈ A; xs ∈ list n' A |] ==> P |]
      ==> P

lemma listn_appendE:

      [| a @ b ∈ list n A;
         !!n1 n2. [| n = n1 + n2; a ∈ list n1 A; b ∈ list n2 A |] ==> P |]
      ==> P

lemma listt_update_in_list:

      [| xs ∈ list n A; x ∈ A |] ==> xs[i := x] ∈ list n A

lemma plus_list_Nil:

      [] +[f] xs = []

lemma plus_list_Cons:

      x # xs +[f] ys = (case ys of [] => [] | y # ys => (x +_f y) # xs +[f] ys)

lemma length_plus_list:

      length (xs +[f] ys) = min (length xs) (length ys)

lemma nth_plus_list:

      [| length xs = n; length ys = n; i < n |]
      ==> (xs +[f] ys) ! i = xs ! i +_f ys ! i

lemma plus_list_ub1:

      [| semilat (A, r, f); set xs ⊆ A; set ys ⊆ A; length xs = length ys |]
      ==> xs <=[r] xs +[f] ys

lemma plus_list_ub2:

      [| semilat (A, r, f); set xs ⊆ A; set ys ⊆ A; length xs = length ys |]
      ==> ys <=[r] xs +[f] ys

lemma plus_list_lub:

      semilat (A, r, f)
      ==> ∀xs ys zs.
             set xs ⊆ A -->
             set ys ⊆ A -->
             set zs ⊆ A -->
             length xs = n ∧ length ys = n -->
             xs <=[r] zs ∧ ys <=[r] zs --> xs +[f] ys <=[r] zs

lemma list_update_incr:

      [| semilat (A, r, f); x ∈ A |]
      ==> set xs ⊆ A --> (∀i<length xs. xs <=[r] xs[i := x +_f xs ! i])

lemma acc_le_listI:

      [| order r; acc r |] ==> acc (Listn.le r)

lemma closed_listI:

      closed S f ==> closed (list n S) (map2 f)

lemma Listn_sl_aux:

      semilat (A, r, f) ==> semilat (Listn.sl n (A, r, f))

lemma Listn_sl:

      semilat L ==> semilat (Listn.sl n L)

lemma coalesce_in_err_list:

      xes ∈ list n (err A) ==> coalesce xes ∈ err (list n A)

lemma lem:

      x +_op # xs = x # xs

lemma coalesce_eq_OK1_D:

      [| semilat (err A, Err.le r, lift2 f); xs ∈ list n A; ys ∈ list n A;
         coalesce (xs +[f] ys) = OK zs |]
      ==> xs <=[r] zs

lemma coalesce_eq_OK2_D:

      [| semilat (err A, Err.le r, lift2 f); xs ∈ list n A; ys ∈ list n A;
         coalesce (xs +[f] ys) = OK zs |]
      ==> ys <=[r] zs

lemma lift2_le_ub:

      [| semilat (err A, Err.le r, lift2 f); x ∈ A; y ∈ A; x +_f y = OK z; u ∈ A;
         x <=_r u; y <=_r u |]
      ==> z <=_r u

lemma coalesce_eq_OK_ub_D:

      [| semilat (err A, Err.le r, lift2 f); xs ∈ list n A; ys ∈ list n A;
         coalesce (xs +[f] ys) = OK zs ∧ xs <=[r] us ∧ ys <=[r] us ∧ us ∈ list n A |]
      ==> zs <=[r] us

lemma lift2_eq_ErrD:

      [| x +_f y = Err; semilat (err A, Err.le r, lift2 f); x ∈ A; y ∈ A |]
      ==> ¬ (∃u∈A. x <=_r u ∧ y <=_r u)

lemma coalesce_eq_Err_D:

      [| semilat (err A, Err.le r, lift2 f); xs ∈ list n A; ys ∈ list n A;
         coalesce (xs +[f] ys) = Err |]
      ==> ¬ (∃zs∈list n A. xs <=[r] zs ∧ ys <=[r] zs)

lemma closed_err_lift2_conv:

      closed (err A) (lift2 f) = (∀x∈A. ∀y∈A. x +_f y ∈ err A)

lemma closed_map2_list:

      [| closed (err A) (lift2 f); xs ∈ list n A; ys ∈ list n A |]
      ==> map2 f xs ys ∈ list n (err A)

lemma closed_lift2_sup:

      closed (err A) (lift2 f) ==> closed (err (list n A)) (lift2 (Listn.sup f))

lemma err_semilat_sup:

      err_semilat (A, r, f) ==> err_semilat (list n A, Listn.le r, Listn.sup f)

lemma err_semilat_upto_esl:

      err_semilat L ==> err_semilat (upto_esl m L)