Theory Gram_Schmidt_Int
subsection ‹Gram-Schmidt Implementation for Integer Vectors›
text ‹This theory implements the Gram-Schmidt algorithm on integer vectors
using purely integer arithmetic. The formalization is based on \<^cite>‹"GS_EKM"›.›
theory Gram_Schmidt_Int
imports
Gram_Schmidt_2
More_IArray
begin
context fixes
fs :: "int vec iarray" and m :: nat
begin
fun sigma_array where
"sigma_array dmus dmusi dmusj dll l = (if l = 0 then dmusi !! l * dmusj !! l
else let l1 = l - 1; dll1 = dmus !! l1 !! l1 in
(dll * sigma_array dmus dmusi dmusj dll1 l1 + dmusi !! l * dmusj !! l) div
dll1)"
declare sigma_array.simps[simp del]
partial_function(tailrec) dmu_array_row_main where
[code]: "dmu_array_row_main fi i dmus j = (if j = i then dmus
else let sj = Suc j;
dmus_i = dmus !! i;
djj = dmus !! j !! j;
dmu_ij = djj * (fi ∙ fs !! sj) - sigma_array dmus dmus_i (dmus !! sj) djj j;
dmus' = iarray_update dmus i (iarray_append dmus_i dmu_ij)
in dmu_array_row_main fi i dmus' sj)"
definition dmu_array_row where
"dmu_array_row dmus i = (let fi = fs !! i in
dmu_array_row_main fi i (iarray_append dmus (IArray [fi ∙ fs !! 0])) 0)"
partial_function (tailrec) dmu_array where
[code]: "dmu_array dmus i = (if i = m then dmus else
let dmus' = dmu_array_row dmus i
in dmu_array dmus' (Suc i))"
end
definition dμ_impl :: "int vec list ⇒ int iarray iarray" where
"dμ_impl fs = dmu_array (IArray fs) (length fs) (IArray []) 0"
definition (in gram_schmidt) β where "β fs l = Gramian_determinant fs (Suc l) / Gramian_determinant fs l"
context gram_schmidt_fs_lin_indpt
begin
lemma Gramian_beta:
assumes "i < m"
shows "β fs i = ∥fs ! i∥⇧2 - (∑j = 0..<i. (μ i j)⇧2 * β fs j)"
proof -
let ?S = "M.sumlist (map (λj. - μ i j ⋅⇩v gso j) [0..<i])"
have S: "?S ∈ carrier_vec n"
using assms by (auto intro!: M.sumlist_carrier gso_carrier)
have fi: "fs ! i ∈ carrier_vec n" using assms by auto
have "β fs i = gso i ∙ gso i"
unfolding β_def
using assms dist by (auto simp add: Gramian_determinant_div sq_norm_vec_as_cscalar_prod)
also have "… = (fs ! i + ?S) ∙ (fs ! i + ?S)"
by (subst gso.simps, subst (2) gso.simps) auto
also have "… = fs ! i ∙ fs ! i + ?S ∙ fs ! i + fs ! i ∙ ?S + ?S ∙ ?S"
using assms S by (auto simp add: add_scalar_prod_distrib[of _ n] scalar_prod_add_distrib[of _ n])
also have "fs ! i ∙ ?S = ?S ∙ fs ! i"
by (rule comm_scalar_prod[OF fi S])
also have "?S ∙ fs ! i = ?S ∙ gso i - ?S ∙ ?S"
proof -
have "fs ! i = gso i - M.sumlist (map (λj. - μ i j ⋅⇩v gso j) [0..<i])"
using assms S by (subst gso.simps) auto
then show ?thesis
using assms S by (auto simp add: minus_scalar_prod_distrib[of _ n] scalar_prod_minus_distrib[of _ n])
qed
also have "?S ∙ gso i = 0"
using assms orthogonal
by(subst scalar_prod_left_sum_distrib)
(auto intro!: sum_list_neutral M.sumlist_carrier gso_carrier)
also have "?S ∙ ?S = (∑j = 0..<i. (μ i j)⇧2 * (gso j ∙ gso j))"
using assms dist by (subst scalar_prod_lincomb_gso)
(auto simp add: power2_eq_square interv_sum_list_conv_sum_set_nat)
also have "… = (∑j = 0..<i. (μ i j)⇧2 * β fs j)"
using assms dist
by (auto simp add: β_def Gramian_determinant_div sq_norm_vec_as_cscalar_prod
intro!: sum.cong)
finally show ?thesis
by (auto simp add: sq_norm_vec_as_cscalar_prod)
qed
lemma gso_norm_beta:
assumes "j < m"
shows "β fs j = sq_norm (gso j)"
unfolding β_def
using assms dist by (auto simp add: Gramian_determinant_div sq_norm_vec_as_cscalar_prod)
lemma mu_Gramian_beta_def:
assumes "j < i" "i < m"
shows "μ i j = (fs ! i ∙ fs ! j - (∑k = 0..<j. μ j k * μ i k * β fs k)) / β fs j"
proof -
let ?list = "map (λja. μ i ja ⋅⇩v gso ja) [0..<i]"
let ?neg_sum = "M.sumlist (map (λja. - μ j ja ⋅⇩v gso ja) [0..<j])"
have list: "set ?list ⊆ carrier_vec n" using gso_carrier assms by auto
define fi where "fi = fs ! i"
have list_id: "[0..<i] = [0..<j] @ [j..<i]"
using assms by (metis append.simps(1) neq0_conv upt.simps(1) upt_append)
have "μ i j = (fs ! i) ∙ (gso j) / sq_norm (gso j) "
unfolding μ.simps using assms by auto
also have " ... = fs ! i ∙ (fs ! j + ?neg_sum) / sq_norm (gso j)"
by (subst gso.simps, simp)
also have " ... = (fi ∙ fs ! j + fs ! i ∙ ?neg_sum) / sq_norm (gso j)"
using assms unfolding fi_def
by (subst scalar_prod_add_distrib [of _ n]) (auto intro!: M.sumlist_carrier gso_carrier)
also have "fs ! i = gso i + M.sumlist ?list "
by (rule fs_by_gso_def[OF assms(2)])
also have "... ∙ ?neg_sum = gso i ∙ ?neg_sum + M.sumlist ?list ∙ ?neg_sum"
using assms by (subst add_scalar_prod_distrib [of _ n]) (auto intro!: M.sumlist_carrier gso_carrier)
also have " M.sumlist ?list = M.sumlist (map (λja. μ i ja ⋅⇩v gso ja) [0..<j])
+ M.sumlist (map (λja. μ i ja ⋅⇩v gso ja) [j..<i]) " (is "_ = ?sumj + ?sumi")
unfolding list_id
by (subst M.sumlist_append[symmetric], insert gso_carrier assms, auto)
also have "gso i ∙ ?neg_sum = 0"
by (rule orthogonal_sumlist, insert gso_carrier dist assms orthogonal, auto)
also have " (?sumj + ?sumi) ∙ ?neg_sum = ?sumj ∙ ?neg_sum + ?sumi ∙ ?neg_sum"
using assms
by (subst add_scalar_prod_distrib [of _ n], auto intro!: M.sumlist_carrier gso_carrier)
also have " ?sumj ∙ ?neg_sum = (∑l = 0..<j. (μ i l) * (-μ j l) * (gso l ∙ gso l)) "
using assms
by (subst scalar_prod_lincomb_gso) (auto simp add: interv_sum_list_conv_sum_set_nat)
also have "… = - (∑l = 0..<j. (μ i l) * (μ j l) * (gso l ∙ gso l)) " (is "_ = - ?sum")
by (auto simp add: sum_negf)
also have "?sum = (∑l = 0..<j. (μ j l) * (μ i l) * β fs l)"
using assms
by (intro sum.cong, auto simp: gso_norm_beta sq_norm_vec_as_cscalar_prod)
also have "?sumi ∙ ?neg_sum = 0"
apply (rule orthogonal_sumlist, insert gso_carrier assms orthogonal, auto intro!: M.sumlist_carrier gso_carrier)
apply (subst comm_scalar_prod[of _ n], auto intro!: M.sumlist_carrier)
by (rule orthogonal_sumlist, use dist in auto)
also have "sq_norm (gso j) = β fs j"
using assms
by (subst gso_norm_beta, auto)
finally show ?thesis unfolding fi_def by simp
qed
end
lemma (in gram_schmidt) Gramian_matrix_alt_alt_alt_def:
assumes "k ≤ length fs" "set fs ⊆ carrier_vec n"
shows "Gramian_matrix fs k = mat k k (λ(i,j). fs ! i ∙ fs ! j)"
proof -
have *: "vec n (($) (fs ! i)) = fs ! i" if "i < length fs" for i
using that assms
by (metis carrier_vecD dim_vec eq_vecI index_vec nth_mem subsetCE)
then show ?thesis
unfolding Gramian_matrix_def using assms
by (intro eq_matI) (auto simp add: Let_def)
qed
lemma (in gram_schmidt_fs_Rn) Gramian_determinant_1 [simp]:
assumes "0 < length fs"
shows "Gramian_determinant fs (Suc 0) = ∥fs ! 0∥⇧2"
proof -
have "Gramian_determinant fs (Suc 0) = fs ! 0 ∙ fs ! 0"
using assms unfolding Gramian_determinant_def
by (subst det_def') (auto simp add: Gramian_matrix_def Let_def scalar_prod_def)
then show ?thesis
by (subst sq_norm_vec_as_cscalar_prod) simp
qed
context gram_schmidt_fs_lin_indpt
begin
definition μ' where "μ' i j ≡ d (Suc j) * μ i j"
fun σ where
"σ 0 i j = 0"
| "σ (Suc l) i j = (d (Suc l) * σ l i j + μ' i l * μ' j l) / d l"
lemma d_Suc: "d (Suc i) = μ' i i" unfolding μ'_def by (simp add: μ.simps)
lemma d_0: "d 0 = 1" by (rule Gramian_determinant_0)
lemma σ: assumes lj: "l ≤ m"
shows "σ l i j = d l * (∑k < l. μ i k * μ j k * β fs k)"
using lj
proof (induct l)
case (Suc l)
from Suc(2-) have lj: "l ≤ m" by auto
note IH = Suc(1)[OF lj]
let ?f = "λ k. μ i k * μ j k * β fs k"
have dl0: "d l > 0" using lj Gramian_determinant dist unfolding lin_indpt_list_def by auto
have "σ (Suc l) i j = (d (Suc l) * σ l i j + μ' i l * μ' j l) / d l" by simp
also have "… = (d (Suc l) * σ l i j) / d l + (μ' i l * μ' j l) / d l" using dl0
by (simp add: field_simps)
also have "(μ' i l * μ' j l) / d l = d (Suc l) * ?f l" (is "_ = ?one")
unfolding β_def μ'_def by auto
also have "(d (Suc l) * σ l i j) / d l = d (Suc l) * (∑k < l. ?f k)" (is "_ = ?sum")
using dl0 unfolding IH by simp
also have "?sum + ?one = d (Suc l) * (?f l + (∑k < l. ?f k))" by (simp add: field_simps)
also have "?f l + (∑k < l. ?f k) = (∑k < Suc l. ?f k)" by simp
finally show ?case .
qed auto
lemma μ': assumes j: "j ≤ i" and i: "i < m"
shows "μ' i j = d j * (fs ! i ∙ fs ! j) - σ j i j"
proof (cases "j < i")
case j: True
have dsj: "d (Suc j) > 0"
using j i Gramian_determinant dist unfolding lin_indpt_list_def
by (meson less_trans_Suc nat_less_le)
let ?sum = " (∑k = 0..<j. μ j k * μ i k * β fs k)"
have "μ' i j = (fs ! i ∙ fs ! j - ?sum) * (d (Suc j) / β fs j)"
unfolding mu_Gramian_beta_def[OF j i] μ'_def by simp
also have "d (Suc j) / β fs j = d j" unfolding β_def using dsj by auto
also have "(fs ! i ∙ fs ! j - ?sum) * d j = (fs ! i ∙ fs ! j) * d j - d j * ?sum"
by (simp add: ring_distribs)
also have "d j * ?sum = σ j i j"
by (subst σ, (insert j i, force), intro arg_cong[of _ _ "λ x. _ * x"] sum.cong, auto)
finally show ?thesis by simp
next
case False
with j have j: "j = i" by auto
have dsi: "d (Suc i) > 0" "d i > 0"
using i Suc_leI dist unfolding lin_indpt_list_def
by (simp_all add: Suc_leI Gramian_determinant(2))
let ?sum = " (∑k = 0..<i. μ i k * μ i k * β fs k)"
have bzero: "β fs i ≠ 0" unfolding β_def using dsi by auto
have "μ' i i = d (Suc i)" by (simp add: μ.simps μ'_def)
also have "… = β fs i * (d (Suc i) / β fs i)" using bzero by simp
also have "d (Suc i) / β fs i = d i" unfolding β_def using dsi by auto
also have "β fs i = (fs ! i ∙ fs ! i - ?sum)"
unfolding Gramian_beta[OF i]
by (rule arg_cong2[of _ _ _ _ "(-)", OF _ sum.cong],
auto simp: power2_eq_square sq_norm_vec_as_cscalar_prod)
also have "(fs ! i ∙ fs ! i - ?sum) * d i = (fs ! i ∙ fs ! i) * d i - d i * ?sum"
by (simp add: ring_distribs)
also have "d i * ?sum = σ i i i"
by (subst σ, (insert i i, force), intro arg_cong[of _ _ "λ x. _ * x"] sum.cong, auto)
finally show ?thesis using j by simp
qed
lemma σ_via_μ': "σ (Suc l) i j =
(if l = 0 then μ' i 0 * μ' j 0 else (μ' l l * σ l i j + μ' i l * μ' j l) / μ' (l - 1) (l - 1))"
by (cases l, auto simp: d_Suc)
lemma μ'_via_σ: assumes j: "j ≤ i" and i: "i < m"
shows "μ' i j =
(if j = 0 then fs ! i ∙ fs ! j else μ' (j - 1) (j - 1) * (fs ! i ∙ fs ! j) - σ j i j)"
unfolding μ'[OF assms] by (cases j, auto simp: d_Suc)
lemma fs_i_sumlist_κ:
assumes "i < m" "l ≤ i" "j < l"
shows "(fs ! i + sumlist (map (λj. κ i l j ⋅⇩v fs ! j) [0..<l])) ∙ fs ! j = 0"
proof -
have "fs ! i + sumlist (map (λj. κ i l j ⋅⇩v fs ! j) [0..<l])
= fs ! i - M.sumlist (map (λj. μ i j ⋅⇩v gso j) [0..<l])"
using assms gso_carrier assms
by (subst κ_def[symmetric]) (auto simp add: dim_sumlist sumlist_nth sum_negf)
also have "… = M.sumlist (map (λj. μ i j ⋅⇩v gso j) [l..<Suc i])"
proof -
have "fs ! i = M.sumlist (map (λj. μ i j ⋅⇩v gso j) [0..<Suc i])"
using assms by (intro fi_is_sum_of_mu_gso) auto
also have "… = M.sumlist (map (λj. μ i j ⋅⇩v gso j) [0..<l]) +
M.sumlist (map (λj. μ i j ⋅⇩v gso j) [l..<Suc i])"
proof -
have *: "[0..<Suc i] = [0..<l] @ [l..<Suc i]"
using assms by (metis diff_zero le_imp_less_Suc length_upt list_trisect upt_conv_Cons)
show ?thesis
by (subst *, subst map_append, subst sumlist_append) (use gso_carrier assms in auto)
qed
finally show ?thesis
using assms gso_carrier assms by (auto simp add: algebra_simps dim_sumlist)
qed
finally have "fs ! i + M.sumlist (map (λj. κ i l j ⋅⇩v fs ! j) [0..<l]) =
M.sumlist (map (λj. μ i j ⋅⇩v gso j) [l..<Suc i])"
by simp
moreover have "… ∙ (fs ! j) = 0"
using assms gso_carrier assms unfolding lin_indpt_list_def
by (subst scalar_prod_left_sum_distrib)
(auto simp add: algebra_simps dim_sumlist gso_scalar_zero intro!: sum_list_zero)
ultimately show ?thesis using assms by auto
qed
end
context gram_schmidt_fs_int
begin
lemma β_pos : "i < m ⟹ β fs i > 0"
using Gramian_determinant(2) unfolding lin_indpt_list_def β_def by auto
lemma β_zero : "i < m ⟹ β fs i ≠ 0"
using β_pos[of i] by simp
lemma σ_integer:
assumes l: "l ≤ j" and j: "j ≤ i" and i: "i < m"
shows "σ l i j ∈ ℤ"
proof -
from assms have ll: "l ≤ m" by auto
have fs_carr: "j < m ⟹ fs ! j ∈ carrier_vec n" for j using assms fs_carrier unfolding set_conv_nth by force
with assms have fs_carr_j: "fs ! j ∈ carrier_vec n" by auto
have dim_gso: "i < m ⟹ dim_vec (gso i) = n" for i using gso_carrier by auto
have dim_fs: "k < m ⟹ dim_vec (fs ! k) = n" for k using smult_carrier_vec fs_carr by auto
have i_l_m: "i < l ⟹ i < m" for i using assms by auto
have smult: "⋀ i j . j < n ⟹ i < l ⟹ (c ⋅⇩v fs ! i) $ j = c * (fs ! i $ j)" for c
using i_l_m dim_fs by auto
have "σ l i j = d l * (∑k < l. μ i k * μ j k * β fs k)"
unfolding σ[OF ll] by simp
also have " ... = d l * (∑k < l. μ i k * ((fs ! j) ∙ (gso k) / sq_norm (gso k)) * β fs k)" (is "_ = _ * ?sum")
unfolding μ.simps using assms by auto
also have "?sum = (∑k < l. μ i k * ((fs ! j) ∙ (gso k) / β fs k) * β fs k)"
using assms by (auto simp add: gso_norm_beta[symmetric] intro!: sum.cong)
also have "... = (∑k < l. μ i k * ((fs ! j) ∙ (gso k) ))"
using β_zero assms by (auto intro!: sum.cong)
also have " ... = (fs ! j) ∙ M.sumlist (map (λk. (μ i k) ⋅⇩v (gso k)) [0..<l] )"
using assms fs_carr[of j] gso_carrier
by (subst scalar_prod_right_sum_distrib) (auto intro!: gso_carrier fs_carr sum.cong simp: sum_list_sum_nth)
also have "d l * … = (fs ! j) ∙ (d l ⋅⇩v M.sumlist (map (λk. (μ i k) ⋅⇩v (gso k)) [0..<l]))" (is "_ = _ ∙ (_ ⋅⇩v ?sum2)")
apply (rule scalar_prod_smult_distrib[symmetric])
apply (rule fs_carr)
using assms gso_carrier
by (auto intro!: sumlist_carrier)
also have "?sum2 = - sumlist (map (λk. (- μ i k) ⋅⇩v (gso k)) [0..<l])"
apply(rule eq_vecI)
using fs_carr gso_carrier assms i_l_m
by(auto simp: sum_negf[symmetric] dim_sumlist sumlist_nth dim_gso intro!: sum.cong)
also have "… = - sumlist (map (λk. κ i l k ⋅⇩v fs ! k) [0..<l])"
using assms gso_carrier assms
apply (subst κ_def)
by (auto)
also have "(d l ⋅⇩v - sumlist (map (λk. κ i l k ⋅⇩v fs ! k) [0..<l])) =
(- sumlist (map (λk. (d l * κ i l k) ⋅⇩v fs ! k) [0..<l]))"
apply(rule eq_vecI)
using fs_carr smult_carrier_vec dim_fs
using dim_fs i_l_m
by (auto simp: smult dim_sumlist sumlist_nth sum_distrib_left intro!: sum.cong)
finally have id: " σ l i j = fs ! j ∙ - M.sumlist (map (λk. d l * κ i l k ⋅⇩v fs ! k) [0..<l]) " .
show "σ l i j ∈ ℤ" unfolding id
using i_l_m fs_carr assms fs_int d_κ_Ints
by (auto simp: dim_sumlist sumlist_nth smult
intro!: sumlist_carrier Ints_minus Ints_sum Ints_mult[of _ "fs ! _ $ _"] Ints_scalar_prod[OF fs_carr])
qed
end
context fs_int_indpt
begin
fun σs and μ' where
"σs 0 i j = μ' i 0 * μ' j 0"
| "σs (Suc l) i j = (μ' (Suc l) (Suc l) * σs l i j + μ' i (Suc l) * μ' j (Suc l)) div μ' l l"
| "μ' i j = (if j = 0 then fs ! i ∙ fs ! j else μ' (j - 1) (j - 1) * (fs ! i ∙ fs ! j) - σs (j - 1) i j)"
declare μ'.simps[simp del]
lemma σs_μ': "l < j ⟹ j ≤ i ⟹ i < m ⟹ of_int (σs l i j) = gs.σ (Suc l) i j"
"i < m ⟹ j ≤ i ⟹ of_int (μ' i j) = gs.μ' i j"
proof (induct l i j and i j rule: σs_μ'.induct)
case (1 i j)
thus ?case by (simp add: gs.σ.simps)
next
case (2 l i j)
have "gs.σ(Suc (Suc l)) i j ∈ ℤ"
by (rule gs.σ_integer, insert 2 gs.fs_carrier, auto)
then have "rat_of_int (μ' (Suc l) (Suc l) * σs l i j + μ' i (Suc l) * μ' j (Suc l)) / rat_of_int (μ' l l) ∈ ℤ"
using 2 gs.d_Suc by (auto)
then have "rat_of_int (σs (Suc l) i j) =
of_int (μ' (Suc l) (Suc l) * σs l i j + μ' i (Suc l) * μ' j (Suc l)) / of_int (μ' l l)"
by (subst σs.simps, subst exact_division) auto
also have "… = gs.σ (Suc (Suc l)) i j"
using 2 gs.d_Suc by (auto)
finally show ?case
by simp
next
case (3 i j)
have "dim_vec (fs ! j) = dim_vec (fs ! i)"
using 3 f_carrier[of i] f_carrier[of j] carrier_vec_def by auto
then have "of_int_hom.vec_hom (fs ! i) $ k = rat_of_int (fs ! i $ k)" if "k < dim_vec (fs ! j)" for k
using that by simp
then have *: "of_int_hom.vec_hom (fs ! i) ∙ of_int_hom.vec_hom (fs ! j) = rat_of_int (fs ! i ∙ fs ! j)"
using 3 by (auto simp add: scalar_prod_def)
show ?case
proof (cases "j = 0")
case True
have "dim_vec (fs ! 0) = dim_vec (fs ! i)"
using 3 f_carrier[of i] f_carrier[of 0] carrier_vec_def by fastforce
then have 1: "of_int_hom.vec_hom (fs ! i) $ k = rat_of_int (fs ! i $ k)" if "k < dim_vec (fs ! 0)" for k
using that by simp
have "(μ' i j) = fs ! i ∙ fs ! j"
using True by (simp add: μ'.simps)
also note *[symmetric]
also have "of_int_hom.vec_hom (fs ! j) = map of_int_hom.vec_hom fs ! j"
using 3 by auto
finally show ?thesis
using 3 True by (subst gs.μ'_via_σ) (auto)
next
case False
then have "gs.μ' i j = gs.μ' (j - Suc 0) (j - Suc 0) * (rat_of_int (fs ! i ∙ fs ! j)) - gs.σ j i j"
using * False 3 by (subst gs.μ'_via_σ) (auto)
then show ?thesis
using False 3 by (subst μ'.simps) (auto)
qed
qed
lemma μ': assumes "i < m" "j ≤ i"
shows "μ' i j = dμ i j"
"j = i ⟹ μ' i j = d fs (Suc i)"
proof -
let ?r = rat_of_int
from assms have "j < m" by auto
note dμ = dμ[OF this assms(1)]
have "?r (μ' i j) = gs.μ' i j"
using σs_μ' assms by auto
also have "… = ?r (dμ i j)"
unfolding gs.μ'_def dμ
by (subst of_int_Gramian_determinant, insert assms fs_carrier, auto simp: d_def subset_eq)
finally show 1: "μ' i j = dμ i j"
by simp
assume j: "j = i"
have "?r (μ' i j) = ?r (dμ i j)"
unfolding 1 ..
also have "… = ?r (d fs (Suc i))"
unfolding dμ unfolding j by (simp add: gs.μ.simps)
finally show "μ' i j = d fs (Suc i)"
by simp
qed
lemma sigma_array: assumes mm: "mm ≤ m" and j: "j < mm"
shows "l ≤ j ⟹ sigma_array (IArray.of_fun (λi. IArray.of_fun (μ' i) (if i = mm then Suc j else Suc i)) (Suc mm))
(IArray.of_fun (μ' mm) (Suc j)) (IArray.of_fun (μ' (Suc j)) (if Suc j = mm then Suc j else Suc (Suc j))) (μ' l l) l =
σs l mm (Suc j)"
proof (induct l)
case 0
show ?case unfolding σs.simps sigma_array.simps[of _ _ _ _ 0]
using mm j by (auto simp: nth_append)
next
case (Suc l)
hence l: "l < j" "l ≤ j" by auto
have id: "(Suc l = 0) = False" "Suc l - 1 = l" by auto
have ineq: "Suc l < Suc mm" "l < Suc mm"
"Suc l < (if Suc l = mm then Suc j else Suc (Suc l))"
"Suc l < (if Suc j = mm then Suc j else Suc (Suc j))"
"l < (if l = mm then Suc j else Suc l)"
"Suc l < Suc j"
using mm l j by auto
note IH = Suc(1)[OF l(2)]
show ?case unfolding sigma_array.simps[of _ _ _ _ "Suc l"] id if_False Let_def IH
of_fun_nth[OF ineq(1)] of_fun_nth[OF ineq(2)] of_fun_nth[OF ineq(3)]
of_fun_nth[OF ineq(4)] of_fun_nth[OF ineq(5)] of_fun_nth[OF ineq(6)]
unfolding σs.simps by simp
qed
lemma dmu_array_row_main: assumes mm: "mm ≤ m" shows
"j ≤ mm ⟹ dmu_array_row_main (IArray fs) (IArray fs !! mm) mm
(IArray.of_fun (λi. IArray.of_fun (μ' i) (if i = mm then Suc j else Suc i)) (Suc mm))
j = IArray.of_fun (λi. IArray.of_fun (μ' i) (Suc i)) (Suc mm)"
proof (induct "mm - j" arbitrary: j)
case 0
thus ?case unfolding dmu_array_row_main.simps[of _ _ _ _ j] by simp
next
case (Suc x j)
hence prems: "x = mm - Suc j" "Suc j ≤ mm" and j: "j < mm" by auto
note IH = Suc(1)[OF prems]
have id: "(j = mm) = False" "(mm = mm) = True" using Suc(2-) by auto
have id2: "IArray.of_fun (μ' mm) (Suc j) = IArray (map (μ' mm) [0..<Suc j])"
by simp
have id3: "IArray fs !! mm = fs ! mm" "IArray fs !! Suc j = fs ! Suc j" by auto
have le: "j < Suc j" "Suc j < Suc mm" "mm < Suc mm" "j < Suc mm"
"j < (if j = mm then Suc j else Suc j)" using j by auto
show ?case unfolding dmu_array_row_main.simps[of _ _ _ _ j]
IH[symmetric] Let_def id if_True if_False id3
of_fun_nth[OF le(1)] of_fun_nth[OF le(2)]
of_fun_nth[OF le(3)] of_fun_nth[OF le(4)]
of_fun_nth[OF le(5)]
sigma_array[OF mm j le_refl, folded id2]
iarray_length_of_fun iarray_update_of_fun iarray_append_of_fun
proof (rule arg_cong[of _ _ "λ x. dmu_array_row_main _ _ _ x _"], rule iarray_cong', goal_cases)
case (1 i)
show ?case unfolding of_fun_nth[OF 1] using j 1
by (cases "i = mm", auto simp: μ'.simps[of _ "Suc j"])
qed
qed
lemma dmu_array_row: assumes mm: "mm ≤ m" shows
"dmu_array_row (IArray fs) (IArray.of_fun (λi. IArray.of_fun (μ' i) (Suc i)) mm) mm =
IArray.of_fun (λi. IArray.of_fun (μ' i) (Suc i)) (Suc mm)"
proof -
have 0: "0 ≤ mm" by auto
show ?thesis unfolding dmu_array_row_def Let_def dmu_array_row_main[OF assms 0, symmetric]
unfolding iarray_append.simps IArray.of_fun_def id map_append list.simps
by (rule arg_cong[of _ _ "λ x. dmu_array_row_main _ _ _ (IArray x) _"], rule nth_equalityI,
auto simp: nth_append μ'.simps[of _ 0])
qed
lemma dmu_array: assumes "mm ≤ m"
shows "dmu_array (IArray fs) m (IArray.of_fun (λ i. IArray.of_fun (λ j. μ' i j) (Suc i)) mm) mm
= IArray.of_fun (λ i. IArray.of_fun (λ j. μ' i j) (Suc i)) m"
using assms
proof (induct mm rule: wf_induct[OF wf_measure[of "λ mm. m - mm"]])
case (1 mm)
show ?case
proof (cases "mm = m")
case True
thus ?thesis unfolding dmu_array.simps[of _ _ _ mm] by simp
next
case False
with 1(2-)
have mm: "mm ≤ m" and id: "(Suc mm = 0) = False" "Suc mm - 1 = mm" "(mm = m) = False"
and prems: "(Suc mm, mm) ∈ measure ((-) m)" "Suc mm ≤ m" by auto
have list: "[0..<Suc mm] = [0..< mm] @ [mm]" by auto
note IH = 1(1)[rule_format, OF prems]
show ?thesis unfolding dmu_array.simps[of _ _ _ mm] id if_False Let_def
unfolding dmu_array_row[OF mm] IH[symmetric]
by (rule arg_cong[of _ _ "λ x. dmu_array _ _ x _"], rule iarray_cong, auto)
qed
qed
lemma dμ_impl: "dμ_impl fs = IArray.of_fun (λ i. IArray.of_fun (λ j. dμ i j) (Suc i)) m"
unfolding dμ_impl_def using dmu_array[of 0] by (auto simp: μ')
end
context gram_schmidt_fs_int
begin
lemma N_μ':
assumes "i < m" "j ≤ i"
shows "(μ' i j)⇧2 ≤ N ^ (3 * Suc j)"
proof -
have 1: "1 ≤ N * N ^ j"
using assms N_1 one_le_power[of _ "Suc j"] by fastforce
have "0 < d (Suc j)"
using assms by (intro Gramian_determinant) auto
then have [simp]: "0 ≤ d (Suc j)"
by arith
have N_d: "d (Suc j) ≤ N ^ (Suc j)"
using assms by (intro N_d) auto
have "(μ' i j)⇧2 = (d (Suc j)) * (d (Suc j)) * (μ i j)⇧2"
unfolding μ'_def by (auto simp add: power2_eq_square)
also have "… ≤ (d (Suc j)) * (d (Suc j)) * N ^ (Suc j)"
proof -
have "(μ i j)⇧2 ≤ N ^ (Suc j)" if "i = j"
using that 1 by (auto simp add: μ.simps)
moreover have "(μ i j)⇧2 ≤ N ^ (Suc j)" if "i ≠ j"
using N_mu assms that by (auto)
ultimately have "(μ i j)⇧2 ≤ N ^ (Suc j)"
by fastforce
then show ?thesis
by (intro mult_mono[of _ _ "(μ i j)⇧2"]) (auto)
qed
also have "… ≤ N ^ (Suc j) * N ^ (Suc j) * N ^ (Suc j)"
using assms 1 N_d by (auto intro!: mult_mono)
also have "N ^ (Suc j) * N ^ (Suc j) * N ^ (Suc j) = N ^ (3 * (Suc j))"
using nat_pow_distrib nat_pow_pow power3_eq_cube by metis
finally show ?thesis
by simp
qed
lemma N_σ:
assumes "i < m" "j ≤ i" "l ≤ j"
shows "¦σ l i j¦ ≤ of_nat l * N ^ (2 * l + 2)"
proof -
have 1: "¦d l¦ = d l"
using Gramian_determinant(2) assms by (intro abs_of_pos) auto
then have "¦σ l i j¦ = d l * ¦∑k<l. μ i k * μ j k * β fs k¦"
using assms by (subst σ, fastforce, subst abs_mult) auto
also have "… ≤ N ^ l * (of_nat l * N ^ (l + 2))"
proof -
have "¦∑k<l. μ i k * μ j k * β fs k¦ ≤ of_nat l * N ^ (l + 2)"
proof -
have [simp]: "0 ≤ β fs k" "∥gso k∥⇧2 ≤ N" if "k < l" for k
using that assms N_gso β_pos[of k] by auto
have [simp]: "0 ≤ N * N ^ k" for k
using N_ge_0 assms by fastforce
have "¦(∑k < l. μ i k * μ j k * β fs k)¦ ≤ (∑k < l. ¦μ i k * μ j k * β fs k¦)"
using sum_abs by blast
also have "… = (∑k < l. ¦μ i k * μ j k¦ * β fs k)"
using assms by (auto intro!: sum.cong simp add: gso_norm_beta abs_mult_pos sq_norm_vec_ge_0)
also have "… = (∑k < l. ¦μ i k¦ * ¦μ j k¦ * β fs k)"
using abs_mult by (fastforce intro!: sum.cong)
also have "… ≤ (∑k < l. (max ¦μ i k¦ ¦μ j k¦) * (max ¦μ i k¦ ¦μ j k¦) * β fs k)"
by (auto intro!: sum_mono mult_mono)
also have "… = (∑k < l. (max ¦μ i k¦ ¦μ j k¦)⇧2 * β fs k)"
by (auto simp add: power2_eq_square)
also have "… ≤ (∑k < l. N ^ (Suc k) * β fs k)"
using assms N_mu[of i] N_mu[of j] assms
by (auto intro!: sum_mono mult_right_mono simp add: max_def)
also have "… ≤ (∑k < l. N ^ (Suc k) * N)"
using assms by (auto simp add: gso_norm_beta intro!: sum_mono mult_left_mono)
also have "… ≤ (∑k < l. N ^ (Suc l) * N)"
using assms N_1 N_ge_0 assms by (fastforce intro!: sum_mono mult_right_mono power_increasing)
also have "… = of_nat l * N ^ (l + 2)"
by auto
finally show ?thesis
by auto
qed
then show ?thesis
using assms N_d N_ge_0 by (fastforce intro!: mult_mono zero_le_power)
qed
also have "… = of_nat l * N ^ (2 * l + 2)"
by (auto simp add: field_simps mult_2_right simp flip: power_add)
finally show ?thesis
by simp
qed
lemma leq_squared: "(z::int) ≤ z⇧2"
proof (cases "0 < z")
case True
then show ?thesis
by (auto intro!: self_le_power)
next
case False
then have "z ≤ 0"
by (simp)
also have "0 ≤ z⇧2"
by (auto)
finally show ?thesis
by simp
qed
lemma abs_leq_squared: "¦z::int¦ ≤ z⇧2"
using leq_squared[of "¦z¦"] by auto
end
context gram_schmidt_fs_int
begin
definition gso' where "gso' i = d i ⋅⇩v (gso i)"
fun a where
"a i 0 = fs ! i" |
"a i (Suc l) = (1 / d l) ⋅⇩v ((d (Suc l) ⋅⇩v (a i l)) - ( μ' i l) ⋅⇩v gso' l)"
lemma gso'_carrier_vec:
assumes "i < m"
shows "gso' i ∈ carrier_vec n"
using assms by (auto simp add: gso'_def)
lemma a_carrier_vec:
assumes "l ≤ i" "i < m"
shows "a i l ∈ carrier_vec n"
using assms by (induction l arbitrary: i) (auto simp add: gso'_def)
lemma a_l:
assumes "l ≤ i" "i < m"
shows "a i l = d l ⋅⇩v (fs ! i + M.sumlist (map (λj. - μ i j ⋅⇩v gso j) [0..<l]))"
using assms proof (induction l)
case 0
then show ?case by auto
next
case (Suc l)
have fsi: "fs ! i ∈ carrier_vec n" using f_carrier[of i] assms by auto
have l_i_m: "l ≤ i ⟹ l < m" using assms by auto
let ?a = "fs ! i"
let ?sum = "M.sumlist (map (λj. - μ i j ⋅⇩v gso j) [0..<l])"
let ?term = "(- μ i l ⋅⇩v gso l)"
have carr: "{?a,?sum,?term} ⊆ carrier_vec n"
using gso_dim l_i_m Suc(2) sumlist_dim assms
by (auto intro!: sumlist_carrier)
have "a i (Suc l) =
(1 / d l) ⋅⇩v ((d (Suc l) ⋅⇩v (d l ⋅⇩v (fs ! i + M.sumlist (map (λj. - μ i j ⋅⇩v gso j) [0..<l]))))
- ( μ' i l) ⋅⇩v gso' l)" using a.simps Suc by auto
also have "… = (1 / d l) ⋅⇩v ((d (Suc l) ⋅⇩v (d l ⋅⇩v (fs ! i + M.sumlist (map (λj. - μ i j ⋅⇩v gso j) [0..<l]))))
+ -d (Suc l) * μ i l * d l ⋅⇩v gso l )" (is "_ = _ ⋅⇩v (?t1 + ?t2)")
unfolding μ'_def gso'_def by auto
also have "?t2 = d l ⋅⇩v (-d (Suc l) * μ i l ⋅⇩v gso l )" (is "_ = d l ⋅⇩v ?tt2")
using smult_smult_assoc by (auto)
also have "?t1 = d l ⋅⇩v ((d (Suc l) ⋅⇩v (fs ! i + M.sumlist (map (λj. - μ i j ⋅⇩v gso j) [0..<l]))))" (is "_ = d l ⋅⇩v ?tt1")
using smult_smult_assoc smult_smult_assoc[symmetric] by (auto)
also have "d l ⋅⇩v ?tt1 + d l ⋅⇩v ?tt2 = d l ⋅⇩v (?tt1 + ?tt2)"
using gso_carrier l_i_m Suc fsi
by (auto intro!: smult_add_distrib_vec[symmetric, of _ n] add_carrier_vec sumlist_carrier)
also have "(1 / d l) ⋅⇩v … = (d l / d l) ⋅⇩v (?tt1 + ?tt2)"
by (intro eq_vecI, auto)
also have "d l / d l = 1"
using Gramian_determinant(2)[of l] l_i_m Suc by(auto simp: field_simps)
also have "1 ⋅⇩v (?tt1 + ?tt2) = ?tt1 + ?tt2" by simp
also have "?tt2 = d (Suc l) ⋅⇩v (- μ i l ⋅⇩v gso l)" by auto
also have "d (Suc l) ⋅⇩v (fs ! i + ?sum) + … =
d (Suc l) ⋅⇩v (fs ! i + ?sum + ?term)"
using carr by (subst smult_add_distrib_vec) (auto)
also have "(?a + ?sum) + ?term = ?a + (?sum + ?term)"
using carr by auto
also have "?term = M.sumlist (map (λj. - μ i j ⋅⇩v gso j) [l..<Suc l])"
using gso_carrier Suc l_i_m by auto
also have "?sum + ... = M.sumlist (map (λj. - μ i j ⋅⇩v gso j) [0..<Suc l])"
apply(subst sumlist_append[symmetric])
using fsi l_i_m Suc sumlist_carrier gso_carrier by (auto intro!: sumlist_carrier)
finally show ?case by auto
qed
lemma a_l':
assumes "i < m"
shows "a i i = gso' i"
proof -
have "a i i = d i ⋅⇩v (fs ! i + M.sumlist (map (λj. - μ i j ⋅⇩v gso j) [0..<i]))"
using a_l assms by auto
also have "… = d i ⋅⇩v gso i"
by (subst gso.simps, auto)
finally have "a i i = gso' i" using gso'_def by auto
from this show ?thesis by auto
qed
lemma
assumes "i < m" "l' ≤ i"
shows "a i l' = (case l' of
0 ⇒ fs ! i |
Suc l ⇒ (1 / d l) ⋅⇩v (d (Suc l) ⋅⇩v (a i l) - (μ' i l) ⋅⇩v a l l))"
proof (cases l')
case (Suc l)
have "a i (Suc l) = (1 / d l) ⋅⇩v ((d (Suc l) ⋅⇩v (a i l)) - ( μ' i l) ⋅⇩v a l l)"
using assms a_l Suc by(subst a_l', auto)
from this Suc show ?thesis by auto
qed auto
lemma a_Ints:
assumes "i < m" "l ≤ i" "k < n"
shows "a i l $ k ∈ ℤ"
proof -
have fsi: "fs ! i ∈ carrier_vec n" using f_carrier[of i] assms by auto
have "a i l = d l ⋅⇩v (fs ! i + M.sumlist (map (λj. - μ i j ⋅⇩v gso j) [0..<l]))"
(is "_ = _ ⋅⇩v (_ + ?sum)")
using assms by (subst a_l, auto)
also have "?sum = sumlist (map (λk. κ i l k ⋅⇩v fs ! k) [0..<l])"
using assms gso_carrier
by (subst κ_def, auto)
also have "d l ⋅⇩v (fs ! i + sumlist (map (λk. κ i l k ⋅⇩v fs ! k) [0..<l]))
= d l ⋅⇩v fs ! i + d l ⋅⇩v sumlist (map (λk. κ i l k ⋅⇩v fs ! k) [0..<l])"
(is "_ = _ + ?sum")
using sumlist_carrier fsi apply
(subst smult_add_distrib_vec[symmetric])
apply force
using assms fsi by (subst sumlist_carrier, auto)
also have "?sum = sumlist (map (λk. (d l * κ i l k) ⋅⇩v fs ! k) [0..<l])"
apply(subst eq_vecI sumlist_nth)
using fsi assms
by (auto simp: dim_sumlist sum_distrib_left sumlist_nth smult_smult_assoc algebra_simps)
finally have "a i l = d l ⋅⇩v fs ! i + sumlist (map (λk. (d l * κ i l k) ⋅⇩v fs ! k) [0..<l])"
by auto
hence "a i l $ k = (d l ⋅⇩v fs ! i + sumlist (map (λk. (d l * κ i l k) ⋅⇩v fs ! k) [0..<l])) $ k" by simp
also have "… = (d l ⋅⇩v fs ! i) $ k + (sumlist (map (λk. (d l * κ i l k) ⋅⇩v fs ! k) [0..<l])) $ k"
apply (subst index_add_vec)
using assms fsi by (subst sumlist_dim, auto)
finally have id: "a i l $ k = (d l ⋅⇩v fs ! i) $ k + (sumlist (map (λk. (d l * κ i l k) ⋅⇩v fs ! k) [0..<l])) $ k".
show ?thesis unfolding id
using fsi assms d_κ_Ints fs_int
by (auto simp: dim_sumlist sumlist_nth
intro!: Gramian_determinant_Ints sumlist_carrier Ints_minus Ints_add Ints_sum Ints_mult[of _ "fs ! _ $ _"] Ints_scalar_prod[OF fsi])
qed
lemma a_alt_def:
assumes "l < length fs"
shows "a i (Suc l) = (let v = μ' l l ⋅⇩v (a i l) - ( μ' i l) ⋅⇩v a l l in
(if l = 0 then v else (1 / μ' (l - 1) (l - 1)) ⋅⇩v v))"
proof -
have [simp]: "μ' (l - Suc 0) (l - Suc 0) = d l" if "0 < l"
using that unfolding μ'_def by (auto simp add: μ.simps)
have [simp]: "μ' l l = d (Suc l)"
unfolding μ'_def by (auto simp add: μ.simps)
show ?thesis
using assms by (auto simp add: Let_def a_l')
qed
end
context fs_int_indpt
begin
fun gso_int :: "nat ⇒ nat ⇒ int vec" where
"gso_int i 0 = fs ! i" |
"gso_int i (Suc l) = (let v = μ' l l ⋅⇩v (gso_int i l) - μ' i l ⋅⇩v gso_int l l in
(if l = 0 then v else map_vec (λk. k div μ' (l - 1) (l - 1)) v))"
lemma gso_int_carrier_vec:
assumes "i < length fs" "l ≤ i"
shows "gso_int i l ∈ carrier_vec n"
using assms by (induction l arbitrary: i) (fastforce simp add: Let_def)+
lemma gso_int:
assumes "i < length fs" "l ≤ i"
shows "of_int_hom.vec_hom (gso_int i l) = gs.a i l"
proof -
have "dim_vec (gso_int i l) = n" "dim_vec (gs.a i l) = n"
using gs.a_carrier_vec assms gso_int_carrier_vec carrier_dim_vec by auto
moreover have "of_int_hom.vec_hom (gso_int i l) $ k = gs.a i l $ k" if k: "k < n" for k
using assms proof (induction l arbitrary: i)
case (Suc l)
note IH = Suc(1)
have [simp]: "dim_vec (gso_int i l) = n" "dim_vec (gs.a i l) = n" "dim_vec (gso_int l l) = n"
"dim_vec (gs.a l l) = n"
using Suc gs.a_carrier_vec gso_int_carrier_vec carrier_dim_vec gs.gso'_carrier_vec by auto
have "rat_of_int (gso_int i l $ k) = gs.a i l $ k" "rat_of_int (gso_int l l $ k) = gs.a l l $ k"
using that Suc(1)[of l] Suc(1)[of i] Suc by auto
then have ?case if "l = 0"
proof -
have [simp]: "fs ≠ []"
using Suc by auto
have [simp]: "dim_vec (gso_int i 0) = n" "dim_vec (gso_int 0 0) = n" "dim_vec (gs.a i 0) = n"
"dim_vec (gs.a 0 0) = n"
using Suc fs_carrier carrier_dim_vec gs.a_carrier_vec f_carrier by auto
have [simp]: "rat_of_int (μ' i 0) = gs.μ' i 0" "rat_of_int (μ' 0 0) = gs.μ' 0 0"
using Suc σs_μ' by (auto intro!: σs_μ')
then show ?thesis
using that k Suc IH[of i ] Suc(1)[of 0]
by (subst gso_int.simps, subst gs.a_alt_def) (auto simp del: gso_int.simps gs.a.simps)
qed
moreover have ?case if "0 < l"
proof -
have *: "rat_of_int (μ' l l * gso_int i l $ k - μ' i l * gso_int l l $ k) / rat_of_int (μ' (l - Suc 0) (l - Suc 0))
= gs.a i (Suc l) $ k"
using Suc IH[of l] IH[of i] σs_μ' k that by (subst gs.a_alt_def) (auto simp add: Let_def )
have "of_int_hom.vec_hom (gso_int i (Suc l)) $ k =
rat_of_int ((μ' l l * gso_int i l $ k - μ' i l * gso_int l l $ k)
div μ' (l - Suc 0) (l - Suc 0))"
using that gso_int_carrier_vec k by (auto)
also have "… = rat_of_int (μ' l l * gso_int i l $ k - μ' i l * gso_int l l $ k) / rat_of_int (μ' (l - Suc 0) (l - Suc 0))"
using gs.a_Ints k Suc by (intro exact_division, subst *, force)
also note *
finally show ?thesis
by (auto)
qed
ultimately show ?case
by blast
qed (auto)
ultimately show ?thesis
by auto
qed
function gso_int_tail' :: "nat ⇒ nat ⇒ int vec ⇒ int vec" where
"gso_int_tail' i l acc = (if l ≥ i then acc
else (let v = μ' l l ⋅⇩v acc - μ' i l ⋅⇩v gso_int l l;
acc' = (map_vec (λk. k div μ' (l - 1) (l - 1)) v)
in gso_int_tail' i (l + 1) acc'))"
by pat_completeness auto
termination
by (relation "(λ(i,l,acc). i - l) <*mlex*> {}", goal_cases) (auto intro!: mlex_less wf_mlex)
fun gso_int_tail :: "nat ⇒ int vec" where
"gso_int_tail i = (if i = 0 then fs ! 0 else
let acc = μ' 0 0 ⋅⇩v fs ! i - μ' i 0 ⋅⇩v fs ! 0 in
gso_int_tail' i 1 acc)"
lemma gso_int_tail':
assumes "acc = gso_int i l" "0 < i" "0 < l" "l ≤ i"
shows "gso_int_tail' i l acc = gso_int i i"
using assms proof (induction i l acc rule: gso_int_tail'.induct)
case (1 i l acc)
{ assume li: "l < i"
then have "gso_int_tail' i l acc =
gso_int_tail' i (l + 1) (map_vec (λk. k div μ' (l - 1) (l - 1)) (μ' l l ⋅⇩v acc - μ' i l ⋅⇩v gso_int l l))"
using 1 by (auto simp add: Let_def)
also have "… = gso_int i i"
using 1 li by (intro 1) (auto)
}
then show ?case
using 1 by fastforce
qed
lemma gso_int_tail: "gso_int_tail i = gso_int i i"
proof (cases "0 < i")
assume i: "0 < i"
then have "gso_int_tail i = gso_int_tail' i (Suc 0) (gso_int i 1)"
by (subst gso_int_tail.simps) (auto)
also have "… = gso_int i i"
using i by (intro gso_int_tail') (auto intro!: gso_int_tail')
finally show "gso_int_tail i = gso_int i i"
by simp
qed (auto)
end
locale gso_array
begin
function while :: "nat ⇒ nat ⇒ int vec iarray ⇒ int iarray iarray ⇒ int vec ⇒ int vec" where
"while i l gsa dmusa acc = (if l ≥ i then acc
else (let v = dmusa !! l !! l ⋅⇩v acc - dmusa !! i !! l ⋅⇩v gsa !! l;
acc' = (map_vec (λk. k div dmusa !! (l - 1) !! (l - 1)) v)
in while i (l + 1) gsa dmusa acc'))"
by pat_completeness auto
termination
by (relation "(λ(i,l,acc). i - l) <*mlex*> {}", goal_cases) (auto intro!: mlex_less wf_mlex)
declare while.simps[simp del]
definition gso' where
"gso' i fsa gsa dmusa = (if i = 0 then fsa !! 0 else
let acc = dmusa !! 0 !! 0 ⋅⇩v fsa !! i - dmusa !! i !! 0 ⋅⇩v fsa !! 0 in
while i 1 gsa dmusa acc)"
function gsos' where
"gsos' i n dmusa fsa gsa = (if i ≥ n then gsa else
gsos' (i + 1) n dmusa fsa (iarray_append gsa (gso' i fsa gsa dmusa)))"
by pat_completeness auto
termination
by (relation "(λ(i,n,dmusa,fsa,gsa). n - i) <*mlex*> {}", goal_cases) (auto intro!: mlex_less wf_mlex)
declare gsos'.simps[simp del]
definition gso'_array where
"gso'_array dmusa fs = gsos' 0 (length fs) dmusa (IArray fs) (IArray [])"
definition gso_array where
"gso_array fs = (let dmusa = dμ_impl fs; gsa = gso'_array dmusa fs
in IArray.of_fun (λi. (if i = 0 then 1 else inverse (rat_of_int (dmusa !! (i - 1) !! (i - 1))))
⋅⇩v of_int_hom.vec_hom (gsa !! i)) (length fs))"
end
declare gso_array.gso_array_def[code]
declare gso_array.gso'_array_def[code]
declare gso_array.gsos'.simps[code]
declare gso_array.gso'_def[code]
declare gso_array.while.simps[code]
lemma map_vec_id[simp]: "map_vec id = id"
by (auto intro!: eq_vecI)
context fs_int_indpt
begin
lemma "gso_array.gso'_array (dμ_impl fs) fs = IArray (map (λk. gso_int k k) [0..<length fs])"
proof -
have a[simp]: "IArray (IArray.list_of a) = a" for a:: "'a iarray"
by (metis iarray.exhaust list_of.simps)
have [simp]: "length (IArray.list_of (iarray_append xs x)) = Suc (IArray.length xs)" for x xs
unfolding iarray_append_code by (simp)
have [simp]: "map_iarray f as = IArray (map f (IArray.list_of as))" for f as
by (metis a iarray.simps(4))
have d[simp]: "IArray.list_of (IArray.list_of (dμ_impl fs) ! i) ! j = μ' i j"
if "i < length fs" "j ≤ i" for j i
using that by (auto simp add: μ' dμ_impl nth_append)
let ?rat_vec = "of_int_hom.vec_hom"
have *: "gso_array.while i j gsa (dμ_impl fs) acc = gso_int_tail' i j acc'"
if "i < length fs" "j ≤ i" "acc = acc'"
"⋀k. k < i ⟹ gsa !! k = gso_int k k" for i j gsa acc acc'
using that apply (induction i j acc arbitrary: acc' rule: gso_int_tail'.induct)
by (subst gso_array.while.simps, subst gso_int_tail'.simps, auto)
then have *: "gso_array.gso' i (IArray fs) gsa (dμ_impl fs) = gso_int i i"
if assms: "i < length fs" "⋀k. k < i ⟹ gsa !! k = gso_int k k" for i gsa
proof -
have "IArray.list_of (IArray.list_of (dμ_impl fs) ! 0) ! 0 = μ' 0 0"
using that by (subst d) (auto)
then have "gso_array.gso' i (IArray fs) gsa (dμ_impl fs) = gso_int_tail i"
unfolding gso_array.gso'_def gso_int_tail.simps Let_def
using that * by (auto simp del: gso_int_tail'.simps)
then show ?thesis
using gso_int_tail by simp
qed
then have *: "gso_array.gsos' i n (dμ_impl fs) (IArray fs) gsa =
IArray (IArray.list_of gsa @ (map (λk. gso_int k k) [i..<n]))"
if "n ≤ length fs"
"gsa = IArray.of_fun (λk. gso_int k k) i" for i n gsa
using that proof (induction i n "(dμ_impl fs)" "(IArray fs)" gsa rule: gso_array.gsos'.induct)
case (1 i n gsa)
{ assume i_n: "i < n"
have [simp]: "gso_array.gso' i (IArray fs) gsa (dμ_impl fs) = gso_int i i"
using 1 i_n by (intro *) auto
have "gso_array.gsos' i n (dμ_impl fs) (IArray fs) gsa = gso_array.gsos' (i + 1) n (dμ_impl fs) (IArray fs) (iarray_append gsa (gso_array.gso' i (IArray fs) gsa (dμ_impl fs)))"
using i_n by (simp add: gso_array.gsos'.simps)
also have "… = IArray (IArray.list_of gsa @ gso_int i i # map (λk. gso_int k k) [Suc i..<n])"
using 1 i_n by (subst 1) (auto simp add: iarray_append_code)
also have "… = IArray (IArray.list_of gsa @ map (λk. gso_int k k) [i..<n])"
using i_n by (auto simp add: upt_conv_Cons)
finally have ?case
by simp }
then show ?case
by (auto simp add: gso_array.gsos'.simps)
qed
then show ?thesis
unfolding gso_array.gso'_array_def by (subst *) auto
qed
end
subsection ‹Lemmas Summarizing All Bounds During GSO Computation›
context gram_schmidt_fs_int
begin
lemma combined_size_bound_integer:
assumes x: "x ∈ {fs ! i $ j | i j. i < m ∧ j < n}
∪ {μ' i j | i j. j ≤ i ∧ i < m}
∪ {σ l i j | i j l. i < m ∧ j ≤ i ∧ l ≤ j}"
(is "x ∈ ?fs ∪ ?μ' ∪ ?σ")
and m: "m ≠ 0"
shows "¦x¦ ≤ of_nat m * N ^ (3 * Suc m)"
proof -
let ?m = "(of_nat m)::'a::trivial_conjugatable_linordered_field"
have [simp]: "1 ≤ ?m"
using m by (metis Num.of_nat_simps One_nat_def Suc_leI neq0_conv of_nat_mono)
have [simp]: "¦(of_int z)::'a::trivial_conjugatable_linordered_field¦ ≤ (of_int z)⇧2" for z
using abs_leq_squared by (metis of_int_abs of_int_le_iff of_int_power)
have "¦fs ! i $ j¦ ≤ of_nat m * N ^ (3 * Suc m)" if "i < m" "j < n" for i j
proof -
have "¦fs ! i $ j¦ ≤ ¦fs ! i $ j¦⇧2"
by (rule Ints_cases[of "fs ! i $ j"]) (use fs_int that in auto)
also have "¦fs ! i $ j¦⇧2 ≤ ∥fs ! i∥⇧2"
using that by (intro vec_le_sq_norm) (auto)
also have "... ≤ 1 * N"
using N_fs that by auto
also have "… ≤ of_nat m * N ^ (3 * Suc m)"
using m N_1 by (intro mult_mono) (auto intro!: mult_mono self_le_power)
finally show ?thesis
by (auto)
qed
then have "¦x¦ ≤ of_nat m * N ^ (3 * Suc m)" if "x ∈ ?fs"
using that by auto
moreover have "¦x¦ ≤ of_nat m * N ^ (3 * Suc m)" if "x ∈ ?μ'"
proof -
have "¦μ' i j¦ ≤ of_nat m * N ^ (3 + 3 * m)" if "j ≤ i" "i < m" for i j
proof -
have "μ' i j ∈ ℤ"
unfolding μ'_def using that d_mu_Ints by auto
then have "¦μ' i j¦ ≤ (μ' i j)⇧2"
by (rule Ints_cases[of "μ' i j"]) auto
also have "… ≤ N ^ (3 * Suc j)"
using that N_μ' by auto
also have "… ≤ 1 * N ^ (3 * Suc m)"
using that assms N_1 by (auto intro!: power_increasing)
also have "… ≤ of_nat m * N ^ (3 * Suc m)"
using N_ge_0 assms zero_le_power by (intro mult_mono) auto
finally show ?thesis
by auto
qed
then show ?thesis
using that by auto
qed
moreover have "¦x¦ ≤ of_nat m * N ^ (3 * Suc m)" if "x ∈ ?σ"
proof -
have "¦σ l i j¦ ≤ of_nat m * N ^ (3 + 3 * m)" if "i < m" "j ≤ i" "l ≤ j" for i j l
proof -
have "¦σ l i j¦ ≤ of_nat l * N ^ (2 * l + 2)"
using that N_σ by auto
also have "… ≤ of_nat m * N ^ (2 * l + 2)"
using that N_ge_0 assms zero_le_power by (intro mult_mono) auto
also have "… ≤ of_nat m * N ^ (3 * Suc m)"
proof -
have "N ^ (2 * l + 2) ≤ N ^ (3 * Suc m)"
using that assms N_1 by (intro power_increasing) (auto intro!: power_increasing)
then show ?thesis
using that assms N_1 by (intro mult_mono) (auto)
qed
finally show ?thesis
by simp
qed
then show ?thesis
using that by (auto)
qed
ultimately show ?thesis
using assms by auto
qed
end
context fs_int_indpt
begin
lemma combined_size_bound_rat_log:
assumes x: "x ∈ {gs.μ' i j | i j. j ≤ i ∧ i < m}
∪ {gs.σ l i j | i j l. i < m ∧ j ≤ i ∧ l ≤ j}"
(is "x ∈ ?μ' ∪ ?σ")
and m: "m ≠ 0" "x ≠ 0"
shows "log 2 ¦real_of_rat x¦ ≤ log 2 m + (3 + 3 * m) * log 2 (real_of_rat gs.N)"
proof -
let ?r_fs = "map of_int_hom.vec_hom fs::rat vec list"
have 1: "map of_int_hom.vec_hom fs ! i $ j = of_int (fs ! i $ j)" if "i < m" "j < n" for i j
using that by auto
then have "{?r_fs ! i $ j |i j. i < length ?r_fs ∧ j < n} =
{rat_of_int (fs ! i $ j) |i j. i < length fs ∧ j < n}"
by (metis (mono_tags, opaque_lifting) length_map)
then have "x ∈ {?r_fs ! i $ j |i j. i < length (map of_int_hom.vec_hom fs) ∧ j < n}
∪ {gs.μ' i j |i j. j ≤ i ∧ i < length ?r_fs}
∪ {gs.σ l i j |i j l. i < length ?r_fs ∧ j ≤ i ∧ l ≤ j}"
using assms by auto
then have 1: "¦x¦ ≤ rat_of_nat (length ?r_fs) * gs.N ^ (3 * Suc (length ?r_fs))" (is "?ax ≤ ?t")
using assms by (intro gs.combined_size_bound_integer) auto
then have 1: "real_of_rat ?ax ≤ real_of_rat ?t"
using of_rat_less_eq 1 by auto
have 2: "¦real_of_rat x¦ = real_of_rat ¦x¦"
by auto
have "log 2 ¦real_of_rat x¦ ≤ log 2 (real_of_rat ?t)"
proof -
have "0 < rat_of_nat (length fs) * gs.N ^ (3 + 3 * length fs)"
using assms gs.N_1 by (auto)
then show ?thesis
using 1 assms by (subst log_le_cancel_iff) (auto)
qed
also have "real_of_rat ?t = real m * real_of_rat gs.N ^ (3 + 3 * m)"
by (auto simp add: of_rat_mult of_rat_power)
also have "log 2 (m * real_of_rat gs.N ^ (3 + 3 * m)) = log 2 m + log 2 (real_of_rat gs.N ^ (3 + 3 * m))"
using gs.N_1 assms by (subst log_mult) auto
also have "log 2 (real_of_rat gs.N ^ (3 + 3 * m)) = real (3 + 3 * length fs) * log 2 (real_of_rat gs.N)"
using gs.N_1 assms by (subst log_nat_power) auto
finally show ?thesis
by (auto)
qed
lemma combined_size_bound_integer_log:
assumes x: "x ∈ {μ' i j | i j. j ≤ i ∧ i < m}
∪ {σs l i j | i j l. i < m ∧ j ≤ i ∧ l < j}"
(is "x ∈ ?μ' ∪ ?σ")
and m: "m ≠ 0" "x ≠ 0"
shows "log 2 ¦real_of_int x¦ ≤ log 2 m + (3 + 3 * m) * log 2 (real_of_rat gs.N)"
proof -
let ?x = "rat_of_int x"
from m have m: "m ≠ 0" "?x ≠ 0" by auto
show ?thesis
proof (rule order_trans[OF _ combined_size_bound_rat_log[OF _ m]], force)
from x consider (1) i j where "x = μ' i j" "j ≤ i" "i < m"
| (2) l i j where "x = σs l i j" "i < m" "j ≤ i" "l < j" by blast
thus "?x ∈ {gs.μ' i j |i j. j ≤ i ∧ i < m} ∪ {gs.σ l i j |i j l. i < m ∧ j ≤ i ∧ l ≤ j}"
proof (cases)
case (1 i j)
with σs_μ'(2) show ?thesis by blast
next
case (2 l i j)
hence "Suc l ≤ j" by auto
from σs_μ'(1) 2 this show ?thesis by blast
qed
qed
qed
end
end