Theory Jinja.Listn

(*  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 [⊑⇘r⇙] y == x <=_(Listn.le r) y"

abbreviation
  lesssublist :: "'a list  'a ord  'a list  bool"  ("(_ /[⊏⇘_⇙] _)" [50, 0, 51] 50) where
  "x [⊏⇘r⇙] 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 [⊑⇘r⇙] y"

abbreviation (input)
  lesssublist2 :: "'a list  'a ord  'a list  bool"  ("(_ /[⊏⇩_] _)" [50, 0, 51] 50) where
  "x [⊏⇩r] y == x [⊏⇘r⇙] y"
(*>*)

abbreviation
  plussublist :: "'a list  ('a  'b  'c)  'b list  'c list"
    ("(_ /[⊔⇘_⇙] _)" [65, 0, 66] 65) where
  "x [⊔⇘f⇙] y == x ⊔⇘map2 fy"

(*<*)
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 [⊔⇘f⇙] 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 [⊔⇘f⇙] 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 [⊑⇘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)"
(*<*)
by (simp add: lesub_def Listn.le_def)
(*>*)

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_update_cong)
done
(*>*)


lemma le_listD: " xs [⊑⇘r⇙] 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 [⊑⇘r⇙] xs"
(*<*)
apply (simp add: unfold_lesub_list lesub_def Listn.le_def list_all2_refl)
done
(*>*)


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 [⊑⇘r⇙] ys" and "ys [⊑⇘r⇙] zs"
    shows      "xs [⊑⇘r⇙] 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 "xA. yA. zA. x ⊑⇩r y  y ⊑⇩r z  x ⊑⇩r z" by (unfold order_def) blast
  hence "xA. yA. zA. 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
(*
  apply (unfold lesssub_def lesub_def)
  apply (unfold Listn.le_def)  
  apply (frule list_all2_trans)
    apply simp
  apply blast
  apply (simp add:list_all2_conv_all_nth)
  apply (intro strip)
  apply (erule order_trans) 
  apply (unfold list_def)
  apply (auto)
*)

lemma le_list_antisym: 
  assumes ord: "order r A"
      and xs:  "xs  nlists n A" and ys: "ys  nlists n A"
      and      "xs [⊑⇘r⇙] ys" and "ys [⊑⇘r⇙] 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 "xA. yA. x ⊑⇩r y  y ⊑⇩r x  x = y" by (unfold order_def) blast
  hence "xA. yA. 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
(*
apply (unfold unfold_lesub_list)
  apply (unfold Listn.le_def)
  apply (auto simp add: list_eq_iff_nth_eq list_def list_all2_conv_all_nth)
  apply (rule order_antisym)     
 apply (auto simp add: list_def)
done
*)
(*>*)

lemma nth_in [rule_format, simp]:
  "i n. size 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 le_list_refl': "order r A  xs  nlists n A  xs ⊑⇘Listn.le rxs"  
  apply (unfold le_def lesssub_def lesub_def list_all2_conv_all_nth)
  apply auto  
  apply (subgoal_tac "xs ! i  A")  
   apply (subgoal_tac "(xs ! i) ⊑⇩r (xs ! i)")
    apply (simp only: lesssub_def lesub_def)
   apply (fastforce dest: nlistsE_nth_in)
   apply (fastforce dest: order_refl)
  done

lemma order_listI [simp, intro!]: "order r A  order(Listn.le r) (nlists n A)"  
(*<*)
proof-
  assume ord: "order r A"
  let ?r = "Listn.le r"
  let ?A = "nlists n A" 
  have "x?A. x ⊑⇘?rx" using ord le_list_refl' by auto
  moreover have "x?A. y?A. x ⊑⇘?ry  y ⊑⇘?rx  x=y" using ord le_list_antisym by auto
  moreover have "x?A. y?A. z?A. x ⊑⇘?ry  y ⊑⇘?rz  x ⊑⇘?rz" using ord le_list_trans by auto
  ultimately show ?thesis by (auto simp only: order_def)
qed
(*>*)

lemma le_list_refl2': "order r A  xs  ({nlists n A |n. n  mxs}) xs ⊑⇘Listn.le rxs"  
  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 [⊑⇘r⇙] ys" and "ys [⊑⇘r⇙] zs"
    shows "xs [⊑⇘r⇙] 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 "xA.  yA. zA. x ⊑⇩r y  y ⊑⇩r z  x ⊑⇩r z" by (unfold order_def) blast
  hence trans: "xA. yA. zA. 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 [⊑⇘r⇙] ys" and "ys [⊑⇘r⇙] 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:"xA. yA. 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 ⊑⇘?rx" using ord le_list_refl2' by auto  ―‹ use order_listI ›
  moreover have "x?A. y?A. x ⊑⇘?ry  y ⊑⇘?rx  x=y" using ord le_list_antisym2 by blast
  moreover have "x?A.  y?A. z?A. x ⊑⇘?ry  y ⊑⇘?rz  x ⊑⇘?rz" 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 [⊑⇘r⇙] ys  size ys = size xs"
(*<*)
apply (unfold Listn.le_def lesub_def)
apply (simp add: list_all2_lengthD)
done
(*>*)

lemma lesssub_lengthD: "xs [⊏⇩r] ys  size ys = size xs"
(*<*)
apply (unfold lesssub_def)
apply auto
done
(*>*)


lemma le_list_appendI: "a [⊑⇘r⇙] b  c [⊑⇘r⇙] d  a@c [⊑⇘r⇙] b@d"
(*<*)
apply (unfold Listn.le_def lesub_def)
apply (rule list_all2_appendI, assumption+)
done
(*>*)

lemma le_listI:
  assumes "length a = length b"
  assumes "n. n < length a  a!n ⊑⇩r b!n"
  shows "a [⊑⇘r⇙] b"
(*<*)
proof -
  from assms have "list_all2 r a b"
    by (simp add: list_all2_all_nthI lesub_def)
  then show ?thesis by (simp add: Listn.le_def lesub_def)
qed
(*>*)

lemma plus_list_Nil [simp]: "[] [⊔⇘f⇙] xs = []"
(*<*)
apply (unfold plussub_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 split: list.split) (*>*)

lemma length_plus_list [rule_format, simp]:
  "ys. size(xs [⊔⇘f⇙] ys) = min(size xs) (size 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. size xs = n  size 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]:
 "xA  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_nlists_Suc_iff)
apply clarify
apply (simp add: nth_Cons split: nat.split)
done
(*>*)


lemma closed_nlistsI:
  "closed S f  closed (nlists n S) (map2 f)"
(*<*)
apply (unfold closed_def)
apply (induct n)
 apply simp
apply clarify
apply (simp add: in_nlists_Suc_iff)
apply clarify
apply simp
done
(*>*)


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
  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_nlistsI)
  apply (simp (no_asm) only: nlists_def)
  apply (simp (no_asm_simp) add: plus_list_ub1 plus_list_ub2 plus_list_lub)
  done
qed
(*>*)

lemma Listn_sl: "semilat L  semilat (Listn.sl n L)"
(*<*) apply (cases L) apply simp
apply (drule Semilat.intro)
by (simp add: Listn_sl_aux split_tupled_all) (*>*)

lemma coalesce_in_err_list [rule_format]:
  "xes. xes  nlists n (err A)  coalesce xes  err(nlists n A)"
(*<*)
apply (induct n)
 apply simp
apply clarify
apply (simp add: in_nlists_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 ⊔⇘(#)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 [⊔⇘f⇙] ys) = OK zs  xs [⊑⇘r⇙] 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 (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  nlists n A  (ys. ys  nlists n A 
  (zs. coalesce (xs [⊔⇘f⇙] ys) = OK zs  ys [⊑⇘r⇙] 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 (force simp add: semilat_le_err_OK2)
done
(*>*)

lemma lift2_le_ub:
  " semilat(err A, Err.le r, lift2 f); xA; yA; x ⊔⇩f y = OK z;
      uA; 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  nlists n A  (ys. ys  nlists n A 
  (zs us. coalesce (xs [⊔⇘f⇙] ys) = OK zs  xs [⊑⇘r⇙] us  ys [⊑⇘r⇙] us
            us  nlists n A  zs [⊑⇘r⇙] 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)
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); xA; yA 
   ¬(uA. 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 [⊔⇘f⇙] ys) = Err 
      ¬(zs  nlists n A. xs [⊑⇘r⇙] zs  ys [⊑⇘r⇙] 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) = (xA. yA. 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  nlists n A  (ys. ys  nlists n A 
  map2 f xs ys  nlists n (err A))"
(*<*)
apply (induct n)
 apply simp
apply clarify
apply (simp add: in_nlists_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 (nlists n A)) (lift2 (sup f))"
(*<*) by (fastforce  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 (nlists 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 [OF Semilat.intro] closed_lift2_sup)
apply (rule conjI)
 apply (drule Semilat.orderI [OF Semilat.intro])
 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 (fastforce intro!: err_semilat_UnionI err_semilat_sup
                dest: lesub_list_impl_same_size
                simp add: plussub_def Listn.sup_def)
done
(*>*)

end