Theory Listn

(*  Title:      HOL/MicroJava/BV/Listn.thy
    ID:         $Id: Listn.html 1910 2004-05-19 04:46:04Z kleing $
    Author:     Tobias Nipkow
    Copyright   2000 TUM

Lists of a fixed length
*)

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

theory Listn = Err:

constdefs
  list :: "nat => 'a set => 'a list set"
  "list n A ≡ {xs. size xs = n ∧ set xs ⊆ A}"

  le :: "'a ord => ('a list)ord"
  "le r ≡ list_all2 (λx y. x \<sqsubseteq>r y)"

(*<*)
syntax 
  "lesublist" :: "'a list => 'a ord => 'a list => bool"  ("(_ /[<=_] _)" [50, 0, 51] 50)
  "lesssublist" :: "'a list => 'a ord => 'a list => bool"  ("(_ /[<_] _)" [50, 0, 51] 50)
(*>*)

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

(*<*)
syntax (xsymbols)
  "@lesublist" :: "'a list => 'a ord => 'a list => bool"  ("(_ /[\<sqsubseteq>_] _)" [50, 0, 51] 50)
  "@lesssublist" :: "'a list => 'a ord => 'a list => bool"  ("(_ /[\<sqsubset>_] _)" [50, 0, 51] 50)

translations
 "x [\<sqsubseteq>r] y" => "x [\<sqsubseteq>r] y"
 "x [\<sqsubset>r] y" => "x [\<sqsubset>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)
(*>*)

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

(*<*)
syntax
  "@plussublist" :: "'a list => ('a => 'b => 'c) => 'b list => 'c list" ("(_ /[\<squnion>_] _)" [65, 0, 66] 65)
translations  
  "x [\<squnion>f] y" == "x [\<squnion>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 [\<squnion>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 [\<sqsubseteq>r] ys ≡ Listn.le r xs ys"
(*<*) by (simp add: lesub_def) (*>*)

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

lemma Cons_notle_Nil [iff]: "¬ x#xs [\<sqsubseteq>r] []"
(*<*)
apply (unfold lesub_def Listn.le_def)
apply simp
done
(*>*)

lemma Cons_le_Cons [iff]: "x#xs [\<sqsubseteq>r] y#ys = (x \<sqsubseteq>r y ∧ xs [\<sqsubseteq>r] ys)"
(*<*)
apply (unfold lesub_def Listn.le_def)
apply simp
done
(*>*)

lemma Cons_less_Conss [simp]:
  "order r ==>  x#xs [\<sqsubset>r] y#ys = (x \<sqsubset>r y ∧ xs [\<sqsubseteq>r] ys ∨ x = y ∧ xs [\<sqsubset>r] ys)"
(*<*)
apply (unfold lesssub_def)
apply blast
done  
(*>*)

lemma list_update_le_cong:
  "[| i<size xs; xs [\<sqsubseteq>r] ys; x \<sqsubseteq>r y |] ==> xs[i:=x] [\<sqsubseteq>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 [\<sqsubseteq>r] ys; p < size xs |] ==> xs!p \<sqsubseteq>r ys!p"
(*<*)
apply (unfold Listn.le_def lesub_def)
apply (simp add: list_all2_nthD)
done
(*>*)

lemma le_list_refl: "∀x. x \<sqsubseteq>r x ==> xs [\<sqsubseteq>r] xs"
(*<*)
apply (unfold unfold_lesub_list lesub_def Listn.le_def)
apply (simp add: list_all2_refl)
done
(*>*)

lemma le_list_trans: "[| order r; xs [\<sqsubseteq>r] ys; ys [\<sqsubseteq>r] zs |] ==> xs [\<sqsubseteq>r] zs"
(*<*)
apply (unfold unfold_lesub_list)
apply (unfold Listn.le_def)
apply (rule list_all2_trans)
apply (erule order_trans)
apply assumption+
done
(*>*)

lemma le_list_antisym: "[| order r; xs [\<sqsubseteq>r] ys; ys [\<sqsubseteq>r] xs |] ==> xs = ys"
(*<*)
apply (unfold unfold_lesub_list)
apply (unfold Listn.le_def)
apply (rule list_all2_antisym)
apply (rule order_antisym)
apply assumption+
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 [\<sqsubseteq>r] ys ==> size ys = size xs"  
(*<*)
apply (unfold Listn.le_def lesub_def) 
apply (simp add: list_all2_lengthD)
done 
(*>*)

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

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

lemma le_listI: "size a = size b ==> (!!n. n < size a ==> a!n \<sqsubseteq>r b!n) ==> a [\<sqsubseteq>r] b"
(*<*)
  apply (unfold lesub_def Listn.le_def)
  apply (simp add: list_all2_all_nthI)
  done
(*>*)

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

(* FIXME: remove simp *)
lemma listE_length [simp]: "xs ∈ list n A ==> size xs = n"
(*<*)
apply (unfold list_def)
apply blast
done 
(*>*)

lemma less_lengthI: "[| xs ∈ list n A; p < n |] ==> p < size 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. 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 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 list_appendI [intro?]:
  "[| a ∈ list n A; b ∈ list m A |] ==> a @ b ∈ list (n+m) A"
(*<*) by (unfold list_def) auto (*>*)

lemma list_map [simp]: "(map f xs ∈ list (size xs) A) = (f ` set xs ⊆ A)"
(*<*) by (unfold list_def) simp (*>*)

lemma list_replicateI [intro]: "x ∈ A ==> replicate n x ∈ list n A"
(*<*) by (induct n) auto (*>*)

lemma plus_list_Nil [simp]: "[] [\<squnion>f] xs = []"
(*<*)
apply (unfold plussub_def map2_def)
apply simp
done 
(*>*)

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

lemma length_plus_list [rule_format, simp]:
  "∀ys. size(xs [\<squnion>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 [\<squnion>f] ys)!i = (xs!i) \<squnion>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 [\<sqsubseteq>r] xs [\<squnion>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 [\<sqsubseteq>r] xs [\<squnion>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 [\<sqsubseteq>r] zs ∧ ys [\<sqsubseteq>r] zs --> xs [\<squnion>f] ys [\<sqsubseteq>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 [\<sqsubseteq>r] xs[i := x \<squnion>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_lengthD)
apply (rule wf_UN)
 prefer 2
 apply clarify
 apply (rename_tac m n)
 apply (case_tac "m=n")
  apply simp
 apply (rule conjI)
  apply (fast intro!: equals0I dest: not_sym)
 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 \<squnion>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 [\<squnion>f] ys) = OK zs --> xs [\<sqsubseteq>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 [\<squnion>f] ys) = OK zs --> ys [\<sqsubseteq>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 \<squnion>f y = OK z; 
      u∈A; x \<sqsubseteq>r u; y \<sqsubseteq>r u |] ==> z \<sqsubseteq>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 [\<squnion>f] ys) = OK zs ∧ xs [\<sqsubseteq>r] us ∧ ys [\<sqsubseteq>r] us 
           ∧ us ∈ list n A --> zs [\<sqsubseteq>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 \<squnion>f y = Err; semilat(err A, Err.le r, lift2 f); x∈A; y∈A |] 
  ==> ¬(∃u∈A. x \<sqsubseteq>r u ∧ y \<sqsubseteq>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 [\<squnion>f] ys) = Err --> 
      ¬(∃zs ∈ list n A. xs [\<sqsubseteq>r] zs ∧ ys [\<sqsubseteq>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 \<squnion>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