Theory Listn
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 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 [⊔⇘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 "∀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 [⊑⇘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 "∀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"
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 r⇙ xs"
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 ⊑⇘?r⇙ x" using ord le_list_refl' by auto
moreover have "∀x∈?A. ∀y∈?A. x ⊑⇘?r⇙ y ∧ y ⊑⇘?r⇙ x ⟶ x=y" using ord le_list_antisym by auto
moreover have "∀x∈?A. ∀y∈?A. ∀z∈?A. x ⊑⇘?r⇙y ∧ y ⊑⇘?r⇙ z ⟶ x ⊑⇘?r⇙ z" 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 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 [⊑⇘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 "∀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 [⊑⇘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:"∀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
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 ⊑⇘?r⇙y ∧ 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 [⊑⇘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]:
"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_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); 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 ∈ 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); 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 [⊔⇘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) = (∀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 ∈ 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