Theory List_Vector
section ‹Vectors as Lists of Naturals›
theory List_Vector
imports Main
begin
lemma lex_lengthD: "(x, y) ∈ lex P ⟹ length x = length y"
by (auto simp: lexord_lex)
lemma lex_take_index:
assumes "(xs, ys) ∈ lex r"
obtains i where "length ys = length xs"
and "i < length xs" and "take i xs = take i ys"
and "(xs ! i, ys ! i) ∈ r"
proof -
obtain n us x xs' y ys' where "(xs, ys) ∈ lexn r n" and "length xs = n" and "length ys = n"
and "xs = us @ x # xs'" and "ys = us @ y # ys'" and "(x, y) ∈ r"
using assms by (fastforce simp: lex_def lexn_conv)
then show ?thesis by (intro that [of "length us"]) auto
qed
lemma mods_with_nats:
assumes "(v::nat) > w"
and "(v * b) mod a = (w * b) mod a"
shows "((v - w) * b) mod a = 0"
using assms by (simp add: mod_eq_dvd_iff_nat algebra_simps)
abbreviation zeroes :: "nat ⇒ nat list"
where
"zeroes n ≡ replicate n 0"
lemma rep_upd_unit:
assumes "x = (zeroes n)[i := a]"
shows "∀j < length x. (j ≠ i ⟶ x ! j = 0) ∧ (j = i ⟶ x ! j = a)"
using assms by simp
definition nonzero_iff: "nonzero xs ⟷ (∃x∈set xs. x ≠ 0)"
lemma nonzero_append [simp]:
"nonzero (xs @ ys) ⟷ nonzero xs ∨ nonzero ys" by (auto simp: nonzero_iff)
subsection ‹The Inner Product›
definition dotprod :: "nat list ⇒ nat list ⇒ nat" (infixl ‹∙› 70)
where
"xs ∙ ys = (∑i<min (length xs) (length ys). xs ! i * ys ! i)"
lemma dotprod_code [code]:
"xs ∙ ys = sum_list (map (λ(x, y). x * y) (zip xs ys))"
by (auto simp: dotprod_def sum_list_sum_nth lessThan_atLeast0)
lemma dotprod_commute:
assumes "length xs = length ys"
shows "xs ∙ ys = ys ∙ xs"
using assms by (auto simp: dotprod_def mult.commute)
lemma dotprod_Nil [simp]: "[] ∙ [] = 0"
by (simp add: dotprod_def)
lemma dotprod_Cons [simp]:
"(x # xs) ∙ (y # ys) = x * y + xs ∙ ys"
unfolding dotprod_def and length_Cons and min_Suc_Suc and sum.lessThan_Suc_shift by auto
lemma dotprod_1_right [simp]:
"xs ∙ replicate (length xs) 1 = sum_list xs"
by (induct xs) (simp_all)
lemma dotprod_0_right [simp]:
"xs ∙ zeroes (length xs) = 0"
by (induct xs) (simp_all)
lemma dotprod_unit [simp]:
assumes "length a = n"
and "k < n"
shows "a ∙ (zeroes n)[k := zk] = a ! k * zk"
using assms by (induct a arbitrary: k n) (auto split: nat.splits)
lemma dotprod_gt0:
assumes "length x = length y" and "∃i<length y. x ! i > 0 ∧ y ! i > 0"
shows "x ∙ y > 0"
using assms by (induct x y rule: list_induct2) (fastforce simp: nth_Cons split: nat.splits)+
lemma dotprod_gt0D:
assumes "length x = length y"
and "x ∙ y > 0"
shows "∃i<length y. x ! i > 0 ∧ y ! i > 0"
using assms by (induct x y rule: list_induct2) (auto simp: Ex_less_Suc2)
lemma dotprod_gt0_iff [iff]:
assumes "length x = length y"
shows "x ∙ y > 0 ⟷ (∃i<length y. x ! i > 0 ∧ y ! i > 0)"
using assms and dotprod_gt0D and dotprod_gt0 by blast
lemma dotprod_append:
assumes "length a = length b"
shows"(a @ x) ∙ (b @ y) = a ∙ b + x ∙ y"
using assms by (induct a b rule: list_induct2) auto
lemma dotprod_le_take:
assumes "length a = length b"
and "k ≤ length a"
shows"take k a ∙ take k b ≤ a ∙ b"
using assms and append_take_drop_id [of k a] and append_take_drop_id [of k b]
by (metis add_right_cancel leI length_append length_drop not_add_less1 dotprod_append)
lemma dotprod_le_drop:
assumes "length a = length b"
and "k ≤ length a"
shows "drop k a ∙ drop k b ≤ a ∙ b"
using assms and append_take_drop_id [of k a] and append_take_drop_id [of k b]
by (metis dotprod_append length_take order_refl trans_le_add2)
lemma dotprod_is_0 [simp]:
assumes "length x = length y"
shows "x ∙ y = 0 ⟷ (∀i<length y. x ! i = 0 ∨ y ! i = 0)"
using assms by (metis dotprod_gt0_iff neq0_conv)
lemma dotprod_eq_0_iff:
assumes "length x = length a"
and "0 ∉ set a"
shows "x ∙ a = 0 ⟷ (∀e ∈ set x. e = 0)"
using assms by (fastforce simp: in_set_conv_nth)
lemma dotprod_eq_nonzero_iff:
assumes "a ∙ x = b ∙ y" and "length x = length a" and "length y = length b"
and "0 ∉ set a" and "0 ∉ set b"
shows "nonzero x ⟷ nonzero y"
using assms by (auto simp: nonzero_iff) (metis dotprod_commute dotprod_eq_0_iff neq0_conv)+
lemma eq_0_iff:
"xs = zeroes n ⟷ length xs = n ∧ (∀x∈set xs. x = 0)"
using in_set_replicate [of _ n 0] and replicate_eqI [of xs n 0] by auto
lemma not_nonzero_iff: "¬ nonzero x ⟷ x = zeroes (length x)"
by (auto simp: nonzero_iff replicate_length_same eq_0_iff)
lemma neq_0_iff':
"xs ≠ zeroes n ⟷ length xs ≠ n ∨ (∃x∈set xs. x > 0)"
by (auto simp: eq_0_iff)
lemma dotprod_pointwise_le:
assumes "length as = length xs"
and "i < length as"
shows "as ! i * xs ! i ≤ as ∙ xs"
proof -
have "as ∙ xs = (∑i<min (length as) (length xs). as ! i * xs ! i)"
by (simp add: dotprod_def)
then show ?thesis
using assms by (auto intro: member_le_sum)
qed
lemma replicate_dotprod:
assumes "length y = n"
shows "replicate n x ∙ y = x * sum_list y"
proof -
have "x * (∑i<length y. y ! i) = (∑i<length y. x * y ! i)"
using sum_distrib_left by blast
then show ?thesis
using assms by (auto simp: dotprod_def sum_list_sum_nth atLeast0LessThan)
qed
subsection ‹The Pointwise Order on Vectors›
definition less_eq :: "nat list ⇒ nat list ⇒ bool" (‹_/ ≤⇩v _› [51, 51] 50)
where
"xs ≤⇩v ys ⟷ length xs = length ys ∧ (∀i<length xs. xs ! i ≤ ys ! i)"
definition less :: "nat list ⇒ nat list ⇒ bool" (‹_/ <⇩v _› [51, 51] 50)
where
"xs <⇩v ys ⟷ xs ≤⇩v ys ∧ ¬ ys ≤⇩v xs"