# Theory Listn

```(*  Title:      HOL/MicroJava/BV/Listn.thy
Author:     Tobias Nipkow

Lists of a fixed length.
*)

section ‹Fixed Length Lists›

theory Listn
imports Err
begin

definition list :: "nat ⇒ 'a set ⇒ 'a list set"
where
"list n A = {xs. size xs = n ∧ set xs ⊆ A}"

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 f⇙ y"

(*<*)
notation
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). (list 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{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)"
(*<*)
(*>*)

lemma Cons_less_Conss [simp]:
"order r ⟹  x#xs [⊏⇩r] y#ys = (x ⊏⇩r y ∧ xs [⊑⇘r⇙] ys ∨ x = y ∧ xs [⊏⇩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)
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: "⟦ order r; xs [⊑⇘r⇙] ys; ys [⊑⇘r⇙] zs ⟧ ⟹ xs [⊑⇘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 [⊑⇘r⇙] ys; ys [⊑⇘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 [⊑⇘r⇙] ys ⟹ size ys = size xs"
(*<*)
apply (unfold Listn.le_def lesub_def)
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"
then show ?thesis by (simp add: Listn.le_def lesub_def)
qed
(*>*)

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

lemma list_not_empty:
"∃a. a∈A ⟹ ∃xs. xs ∈ list n A"
(*<*)
apply (induct "n")
apply simp
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 n': "ls@b ∈ list n' A" by fastforce
assume "⋀n. ls @ b ∈ list n A ⟹ ∃n1 n2. n = n1 + n2 ∧ ls ∈ list n1 A ∧ b ∈ list n2 A"
from this and n' have "∃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 fastforce
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]: "[] [⊔⇘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)
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)
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)
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 (induct xs)
apply simp
apply clarify
apply (simp add: nth_Cons split: nat.split)
done
(*>*)

lemma acc_le_listI' [intro!]:
"⟦ order r; acc A r ⟧ ⟹ acc (⋃n. list n A) (Listn.le r)"
(*<*)
apply (unfold acc_def)
apply (subgoal_tac
"wf(UN n. {(ys,xs). xs ∈ list n A ∧ ys ∈ list n A ∧ xs <_(Listn.le r) ys})")
apply (erule wf_subset)
apply clarify
apply(rule UN_I)
prefer 2
apply clarify
apply(frule lesssub_lengthD)
apply fastforce
apply simp
apply (rule wf_UN)
prefer 2
apply (rename_tac m n)
apply (case_tac "m=n")
apply simp
apply (clarsimp intro!: equals0I)
apply (drule lesssub_lengthD)+
apply simp
apply (induct_tac n)
apply (simp add: lesssub_def cong: conj_cong)
apply (rename_tac k)
apply (simp (no_asm) add: in_list_Suc_iff cong: conj_cong)
apply clarify
apply (rename_tac M m)
apply (case_tac "∃x∈A. ∃xs∈list k A. x#xs ∈ M")
prefer 2
apply (erule thin_rl)
apply (erule thin_rl)
apply blast
apply (erule_tac x = "{a. a ∈ A ∧ (∃xs∈list k A. a#xs∈M)}" in allE)
apply (erule impE)
apply blast
apply (thin_tac "∃x∈A. ∃xs∈list k A. P x xs" for P)
apply clarify
apply (rename_tac maxA xs)
apply (erule_tac x = "{ys. ys ∈ list k A ∧ 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 (erule disjE)
prefer 2
apply blast
by fastforce

lemma acc_le_listI [intro!]:
"⟦ order r; acc A r ⟧ ⟹ acc (list n A) (Listn.le r)"
apply(drule (1) acc_le_listI')
apply(erule thin_rl)
apply(unfold acc_def)
apply(erule wf_subset)
apply blast
done

lemma acc_le_list_uptoI [intro!]:
"⟦ order r; acc A r ⟧ ⟹ acc (⋃{list n A|n. n ≤ mxs}) (Listn.le r)"
apply(drule (1) acc_le_listI')
apply(erule thin_rl)
apply(unfold acc_def)
apply(erule wf_subset)
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 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_listI)
apply (simp (no_asm) only: list_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 ∈ list n (err A) ⟶ coalesce xes ∈ err(list n A)"
(*<*)
apply (induct n)
apply simp
apply clarify
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 ∈ 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 clarify
apply (simp split: err.split_asm add: lem Err.sup_def lift2_def)
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 clarify
apply (simp split: err.split_asm add: lem Err.sup_def lift2_def)
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 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 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 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)
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 (induct n)
apply simp
apply clarify
apply clarify
done
(*>*)

lemma closed_lift2_sup:
"closed (err A) (lift2 f) ⟹
closed (err (list 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 (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 [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
done
(*>*)

end
```