Quelle  Listn.thy

(*  Title:      HOL/MicroJava/BV/Listn.thy
    Author:     Tobias Nipkow
    Copyright   2000 TUM

Lists of a fixed length.
*)

section ‹Fixed Length Lists›

theory Listn
imports Err "HOL-Library.NList"
begin

definition le :: "'a ord ==> ('a list)ord"
where
  "le r = list_all2 (λx y. x ⊑_r y)"

abbreviation
  lesublist :: "'a list ==> 'a ord ==> 'a list ==> bool"  (‹(_ /[⊑] _)› [50, 0, 51] 50) where
  "x [⊑] y == x <=_(Listn.le r) y"

abbreviation
  lesssublist :: "'a list ==> 'a ord ==> 'a list ==> bool"  (‹(_ /[⊏] _)› [50, 0, 51] 50) where
  "x [⊏] y == x <_(Listn.le r) y"

(*<*)
notation (ASCII)
  lesublist  (‹(_ /[<=_] _)› [50, 0, 51] 50) and
  lesssublist  (‹(_ /[<_] _)› [50, 0, 51] 50)

abbreviation (input)
  lesublist2 :: "'a list ==> 'a ord ==> 'a list ==> bool"  (‹(_ /[⊑_{_}] _)› [50, 0, 51] 50) where
  "x [⊑_r] y == x [⊑] y"

abbreviation (input)
  lesssublist2 :: "'a list ==> 'a ord ==> 'a list ==> bool"  (‹(_ /[⊏_{_}] _)› [50, 0, 51] 50) where
  "x [⊏_r] y == x [⊏] y"
(*>*)

abbreviation
  plussublist :: "'a list ==> ('a ==> 'b ==> 'c) ==> 'b list ==> 'c list"
    (‹(_ /[⊔] _)› [65, 0, 66] 65) where
  "x [⊔] y == x ⊔ _f y"

(*<*)
notation (ASCII)
  plussublist  (‹(_ /[+_] _)› [65, 0, 66] 65)

abbreviation (input)
  plussublist2 :: "'a list ==> ('a ==> 'b ==> 'c) ==> 'b list ==> 'c list"
    (‹(_ /[⊔_{_}] _)› [65, 0, 66] 65) where
  "x [⊔_f] y == x [⊔] y"
(*>*)


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

definition sl :: "nat ==> 'a sl ==> 'a list sl"
where
  "sl n = (λ(A,r,f). (nlists n A, le r, map2 f))"

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

definition upto_esl :: "nat ==> 'a esl ==> 'a list esl"
where
  "upto_esl m = (λ(A,r,f). (Union{nlists n A |n. n ≤ m}, le r, sup f))"


lemmas [simp] = set_update_subsetI

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

lemma Nil_le_conv [iff]: "([] [⊑] ys) = (ys = [])"
(*<*)
  by (simp add: Listn.le_def lesub_def)
(*>*)

lemma Cons_notle_Nil [iff]: "¬ x#xs [⊑] []"
(*<*)
  by (simp add: Listn.le_def lesub_def)
(*>*)

lemma Cons_le_Cons [iff]: "x#xs [⊑] y#ys = (x ⊑_r y ∧ xs [⊑] ys)"
(*<*)
by (simp add: lesub_def Listn.le_def)
(*>*)

lemma list_update_le_cong:
  "[ i<size xs; xs [⊑] ys; x ⊑_r y ] ==> xs[i:=x] [⊑] ys[i:=y]"
(*<*)
  by (metis Listn.le_def list_all2_update_cong unfold_lesub_list)
(*>*)


lemma le_listD: "[ xs [⊑] ys; p < size xs ] ==> xs!p ⊑_r ys!p"
(*<*)
  by (simp add: Listn.le_def lesub_def list_all2_nthD)
(*>*)

lemma le_list_refl: "∀x. x ⊑_r x ==> xs [⊑] xs"
(*<*)
  by (simp add: unfold_lesub_list lesub_def Listn.le_def list_all2_refl)
(*>*)


lemma le_list_trans: 
  assumes ord: "order r A"
      and xs:  "xs ∈ nlists n A" and ys: "ys ∈ nlists n A" and zs: "zs ∈ nlists n A"
      and      "xs [⊑] ys" and "ys [⊑] zs"
    shows      "xs [⊑] zs"
(*<*)
  using assms
proof (unfold le_def lesssub_def lesub_def)
  assume "list_all2 r xs ys" and "list_all2 r ys zs"
  hence xs_ys_zs:  "∀i < length xs. r (xs!i) (ys!i) ∧ r (ys!i) (zs!i)" 
        and len_xs_zs: "length xs = length zs" by (auto simp add: list_all2_conv_all_nth)
  from xs ys zs have inA: "∀i<length xs. xs!i ∈ A ∧ ys!i ∈ A ∧ zs!i ∈ A" by (unfold nlists_def) auto
  
  from ord have "∀x∈A. ∀y∈A. ∀z∈A. x ⊑_r y ∧ y ⊑_r z ⟶ x ⊑_r z" by (unfold order_def) blast
  hence "∀x∈A. ∀y∈A. ∀z∈A. r x y ∧ r y z ⟶ r x z" by (unfold lesssub_def lesub_def)
  with xs_ys_zs inA have "∀i<length xs. r (xs!i) (zs!i)" by blast
  with len_xs_zs show "list_all2 r xs zs" by (simp add:list_all2_conv_all_nth)
qed

lemma le_list_antisym: 
  assumes ord: "order r A"
      and xs:  "xs ∈ nlists n A" and ys: "ys ∈ nlists n A"
      and      "xs [⊑] ys" and "ys [⊑] xs"
    shows      "xs = ys"
(*<*)
  using assms
proof (simp add: le_def lesssub_def lesub_def)
  assume "list_all2 r xs ys" and "list_all2 r ys xs"
  hence xs_ys:  "∀i < length xs. r (xs!i) (ys!i) ∧ r (ys!i) (xs!i)" 
        and len_xs_ys: "length xs = length ys" by (auto simp add: list_all2_conv_all_nth)
  from xs ys have inA: "∀i<length xs. xs!i ∈ A ∧ ys!i ∈ A" by (unfold nlists_def) auto
  
  from ord have "∀x∈A. ∀y∈A. x ⊑_r y ∧ y ⊑_r x ⟶ x = y" by (unfold order_def) blast
  hence "∀x∈A. ∀y∈A. r x y ∧ r y x ⟶ x = y" by (unfold lesssub_def lesub_def)
  with xs_ys inA have "∀i<length xs. xs!i = ys!i" by blast
  with len_xs_ys show "xs = ys" by (simp add:list_eq_iff_nth_eq)
qed
(*>*)

lemma nth_in [rule_format, simp]:
  "∀i n. size xs = n ⟶ set xs ⊆ A ⟶ i < n ⟶ (xs!i) ∈ A"
(*<*)
  by auto
(*>*)

lemma le_list_refl': "order r A ==> xs ∈ nlists n A ==> xs ⊑_{.le r} xs"
  by (metis Listn.le_def Semilat.order_refl list_all2_conv_all_nth nlistsE_length
      nlistsE_nth_in unfold_lesub_list)  

lemma order_listI [simp, intro!]: "order r A ==> order(Listn.le r) (nlists n A)"
(*<*)
  by (smt (verit) le_list_antisym le_list_refl' le_list_trans order_def)  
(*>*)

lemma le_list_refl2': "order r A ==> xs ∈ (∪{nlists n A |n. n ≤ mxs})==> xs ⊑_{.le r} xs"  
  by (auto simp add:le_list_refl')
lemma le_list_trans2: 
  assumes "order r A"
      and "xs ∈ (∪{nlists n A |n. n ≤ mxs})" and "ys ∈(∪{nlists n A |n. n ≤ mxs})" and "zs ∈(∪{nlists n A |n. n ≤ mxs})"
      and "xs [⊑] ys" and "ys [⊑] zs"
    shows "xs [⊑] zs"
(*<*)using assms
proof(auto simp only:nlists_def le_def lesssub_def lesub_def)
  assume xA: "set xs ⊆ A" and "length xs ≤ mxs " and " length ys ≤ mxs "
     and yA: "set ys ⊆ A" and len_zs: "length zs ≤ mxs" 
     and zA: "set zs ⊆ A" and xy: "list_all2 r xs ys" and yz: "list_all2 r ys zs"
     and ord: "order r A" 
  from xy yz have xs_ys: "length xs = length ys" and ys_zs: "length ys = length zs" by (auto simp add:list_all2_conv_all_nth)
  from ord have "∀x∈A. ∀y∈A. ∀z∈A. x ⊑_r y ∧ y ⊑_r z ⟶ x ⊑_r z" by (unfold order_def) blast
  hence trans: "∀x∈A. ∀y∈A. ∀z∈A. r x y ∧ r y z ⟶ r x z" by (simp only:lesssub_def lesub_def)

  from xA yA zA have x_inA: "∀i<length xs. xs!i ∈ A"
                 and y_inA: "∀i<length xs. ys!i ∈ A" 
                 and z_inA: "∀i<length xs. zs!i ∈ A"  using xs_ys ys_zs  by auto
  
  from xy yz have "∀i < length xs. r (xs!i) (ys!i)" 
              and "∀i < length ys. r (ys!i) (zs!i)" by (auto simp add:list_all2_conv_all_nth)
  hence "∀i < length xs. r (xs!i) (ys!i) ∧ r (ys!i) (zs!i)" using xs_ys ys_zs by auto

  with x_inA y_inA z_inA
  have "∀i<length xs. r (xs!i) (zs!i)" using trans  xs_ys ys_zs by blast
  thus "list_all2 r xs zs" using xs_ys ys_zs by (simp add:list_all2_conv_all_nth)
qed


lemma le_list_antisym2: 
  assumes "order r A"
      and "xs ∈(∪{nlists n A |n. n ≤ mxs})" and "ys ∈(∪{nlists n A |n. n ≤ mxs})" 
      and "xs [⊑] ys" and "ys [⊑] xs"
    shows " xs = ys"
(*<*)
  using assms
proof(auto simp only:nlists_def le_def lesssub_def lesub_def)
  assume xA: "set xs ⊆ A" and len_ys: "length ys ≤ mxs" and len_xs: "length xs ≤ mxs" 
     and yA: "set ys ⊆ A" and xy: "list_all2 r xs ys" and yx: "list_all2 r ys xs" 
     and ord: "order r A"
  from xy have len_eq_xs_ys: "length xs = length ys" by (simp add:list_all2_conv_all_nth)
  
  from ord have antisymm:"∀x∈A. ∀y∈A. r x y ∧ r y x⟶ x=y " by (auto simp only:lesssub_def lesub_def order_def)
  from xA yA have x_inA: "∀i<length xs. xs!i ∈ A" and y_inA: "∀i<length ys. ys!i ∈ A" by auto
  from xy yx have "∀i < length xs. r (xs!i) (ys!i)" and "∀i < length ys. r (ys!i) (xs!i)" by (auto simp add:list_all2_conv_all_nth)
  with x_inA y_inA
  have "∀i<length xs. xs!i = ys!i" using antisymm len_eq_xs_ys by auto
  then show "xs = ys" using len_eq_xs_ys by (simp add:list_eq_iff_nth_eq)
qed
(*<*)


lemma order_listI2[intro!] : "order r A ==> order(Listn.le r) (∪{nlists n A |n. n ≤ mxs})"
(*<*)
proof-
  assume ord: "order r A"  
  let ?r = "Listn.le r"
  let ?A = "(∪{nlists n A |n. n ≤ mxs})" 
  have "∀x∈?A. x ⊑_r x" using ord le_list_refl2' by auto  ―‹ use order_listI ›
  moreover have "∀x∈?A. ∀y∈?A. x ⊑_r y ∧ y ⊑_r x ⟶ x=y" using ord le_list_antisym2 by blast
  moreover have "∀x∈?A. ∀y∈?A. ∀z∈?A. x ⊑_ry ∧ y ⊑_r z ⟶ x ⊑_r z" using ord le_list_trans2 by blast
  ultimately show ?thesis by (auto simp only: order_def)
qed


lemma lesub_list_impl_same_size [simp]: "xs [⊑] ys ==> size ys = size xs"
(*<*)
  by (simp add: Listn.le_def lesub_def list_all2_conv_all_nth)
(*>*)

lemma lesssub_lengthD: "xs [⊏_r] ys ==> size ys = size xs"
(*<*)
  by (metis lesssub_def lesub_list_impl_same_size)
(*>*)


lemma le_list_appendI: "a [⊑] b ==> c [⊑] d ==> a@c [⊑] b@d"
(*<*)
  by (metis Listn.le_def list_all2_appendI unfold_lesub_list)
(*>*)

lemma le_listI:
  assumes "length a = length b"
  assumes "∧n. n < length a ==> a!n ⊑_r b!n"
  shows "a [⊑] b"
(*<*)
  by (metis Listn.le_def assms lesub_def list_all2_conv_all_nth)
(*>*)

lemma plus_list_Nil [simp]: "[] [⊔] xs = []"
(*<*)
  by (simp add: plussub_def)
(*>*)

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

lemma length_plus_list [simp]: "size(xs [⊔] ys) = min(size xs) (size ys)"
(*<*)
  by (metis length_map length_zip plussub_def)
(*>*)

lemma nth_plus_list [simp]:
  "size xs = n ==> size ys = n ==> i<n ==> (xs [⊔] ys)!i = (xs!i) ⊔_f (ys!i)"
(*<*)
  by (induct n) (auto simp add: plussub_def)
(*>*)


lemma (in Semilat) plus_list_ub1 [rule_format]:
 "[ set xs ⊆ A; set ys ⊆ A; size xs = size ys ]
  ==> xs [⊑] xs [⊔] ys"
(*<*)
  unfolding unfold_lesub_list
  by (simp add: Listn.le_def list_all2_conv_all_nth)
(*>*)

lemma (in Semilat) plus_list_ub2:
 "[set xs ⊆ A; set ys ⊆ A; size xs = size ys ] ==> ys [⊑] xs [⊔] ys"
(*<*)
  unfolding unfold_lesub_list
  by (simp add: Listn.le_def list_all2_conv_all_nth)
(*>*)

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 [⊑] zs ∧ ys [⊑] zs ⟶ xs [⊔] ys [⊑] zs"
(*<*)
  unfolding unfold_lesub_list
  by (simp add: Listn.le_def list_all2_conv_all_nth)
(*>*)

lemma (in Semilat) list_update_incr [rule_format]:
  "x∈A ==> set xs ⊆ A ==> i<size xs ==> xs [⊑] xs[i := x ⊔_f xs!i]"
(*<*)
  by (metis le_list_refl' list_update_id list_update_le_cong nlistsI nth_in orderI
      ub2)
(*>*)


lemma closed_nlistsI:
  "closed S f ==> closed (nlists n S) (map2 f)"
(*<*)
  unfolding closed_def
  by (induct n) (auto simp add: in_nlists_Suc_iff)
(*>*)


lemma Listn_sl_aux:
assumes "Semilat A r f" shows "semilat (Listn.sl n (A,r,f))"
(*<*)
proof -
  interpret Semilat A r f by fact
  show ?thesis
    unfolding Listn.sl_def semilat_Def split_conv
    by (simp add: closed_nlistsI plus_list_lub plus_list_ub1 plus_list_ub2)
qed
(*>*)

lemma Listn_sl: "semilat L ==> semilat (Listn.sl n L)"
(*<*) 
  by (metis Listn_sl_aux Semilat_def surj_pair)
(*>*)

lemma coalesce_in_err_list [rule_format]:
  "∀xes. xes ∈ nlists n (err A) ⟶ coalesce xes ∈ err(nlists n A)"
(*<*)
apply (induct n)
 apply simp
  by (force simp add: in_nlists_Suc_iff plussub_def Err.sup_def lift2_def split: err.split)
(*>*)

lemma lem: "∧x xs. x ⊔_#) 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 ∈ nlists n A ⟶ (∀ys. ys ∈ nlists n A ⟶
  (∀zs. coalesce (xs [⊔] ys) = OK zs ⟶ xs [⊑] zs))"
(*<*)
apply (induct n)
  apply simp
apply clarify
apply (simp add: in_nlists_Suc_iff)
apply (force simp add: semilat_le_err_OK1 split: err.split_asm)
done
(*>*)

lemma coalesce_eq_OK2_D [rule_format]:
  "semilat(err A, Err.le r, lift2 f) ==>
  ∀xs. xs ∈ nlists n A ⟶ (∀ys. ys ∈ nlists n A ⟶
  (∀zs. coalesce (xs [⊔] ys) = OK zs ⟶ ys [⊑] zs))"
(*<*)
apply (induct n)
 apply simp
apply clarify
apply (simp add: in_nlists_Suc_iff)
apply (force simp add: semilat_le_err_OK2 split: err.split_asm)
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 (clarsimp simp: semilat_Def plussub_def err_def' lift2_def)
  by (metis (no_types, lifting) err.inject)
(*>*)

lemma coalesce_eq_OK_ub_D [rule_format]:
  "semilat(err A, Err.le r, lift2 f) ==>
  ∀xs. xs ∈ nlists n A ⟶ (∀ys. ys ∈ nlists n A ⟶
  (∀zs us. coalesce (xs [⊔] ys) = OK zs ∧ xs [⊑] us ∧ ys [⊑] us
           ∧ us ∈ nlists n A ⟶ zs [⊑] us))"
(*<*)
  apply (induct n)
   apply simp
  apply clarify
  apply (simp add: in_nlists_Suc_iff)
  apply clarify
  apply (simp (no_asm_use) split: err.split_asm add: lem Err.sup_def lift2_def)
  by (metis Cons_le_Cons lift2_le_ub)
(*>*)

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 ∈ nlists n A ⟶ (∀ys. ys ∈ nlists n A ⟶
      coalesce (xs [⊔] ys) = Err ⟶
      ¬(∃zs ∈ nlists n A. xs [⊑] zs ∧ ys [⊑] zs))"
(*<*)
apply (induct n)
 apply simp
apply clarify
apply (simp add: in_nlists_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)"
(*<*)
  by (simp add: closed_def err_def')
(*>*)

lemma closed_map2_list [rule_format]:
  "closed (err A) (lift2 f) ==>
  ∀xs. xs ∈ nlists n A ⟶ (∀ys. ys ∈ nlists n A ⟶
  map2 f xs ys ∈ nlists n (err A))"
(*<*)
  by (induct n) (auto simp add: in_nlists_Suc_iff plussub_def closed_err_lift2_conv)
(*>*)

lemma closed_lift2_sup:
  "closed (err A) (lift2 f) ==> closed (err (nlists n A)) (lift2 (sup f))"
(*<*) by (simp add: Listn.sup_def closed_err_lift2_conv closed_map2_list
      coalesce_in_err_list plussub_def) 
(*>*)

lemma err_semilat_sup:
  "err_semilat (A,r,f) ==> err_semilat (nlists n A, Listn.le r, sup f)"
  (*<*)
  unfolding Err.sl_def split_conv
  apply (simp (no_asm) only: semilat_Def plussub_def)
  apply (simp (no_asm_simp) only: Semilat.closedI [OF Semilat.intro] closed_lift2_sup)
  apply (rule conjI)
   apply (simp add: semilat_Def)
  apply (simp (no_asm) add: unfold_lesub_err Err.le_def err_def' sup_def lift2_def split: err.split)
  by (smt (verit, del_insts) coalesce_eq_Err_D coalesce_eq_OK1_D coalesce_eq_OK2_D
      coalesce_eq_OK_ub_D plussub_def)
    (*>*)

lemma err_semilat_upto_esl:
  "∧L. err_semilat L ==> err_semilat(upto_esl m L)"
(*<*)
  unfolding Listn.upto_esl_def
apply (simp add: split_tupled_all)
apply (fastforce intro!: err_semilat_UnionI err_semilat_sup
                dest: lesub_list_impl_same_size
                simp add: plussub_def Listn.sup_def)
done
(*>*)

end