Theory Gram_Schmidt_2

(*
    Authors:    Ralph Bottesch
                Jose Divasón
                Maximilian Haslbeck
                Sebastiaan Joosten
                René Thiemann
                Akihisa Yamada
    License:    BSD
*)

section ‹Gram-Schmidt›

theory Gram_Schmidt_2
  imports 
    Jordan_Normal_Form.Gram_Schmidt
    Jordan_Normal_Form.Show_Matrix
    Jordan_Normal_Form.Matrix_Impl
    Norms
    Int_Rat_Operations
begin
(* TODO: Documentation and add references to computer algebra book *)

unbundle no m_inv_syntax


(* TODO: move *)

lemma rev_unsimp: "rev xs @ (r # rs) = rev (r#xs) @ rs" by simp


(* TODO: unify *)

lemma corthogonal_is_orthogonal[simp]: 
  "corthogonal (xs :: 'a :: trivial_conjugatable_ordered_field vec list) = orthogonal xs"
  unfolding corthogonal_def orthogonal_def by simp


context cof_vec_space
begin

definition lin_indpt_list :: "'a vec list  bool" where
  "lin_indpt_list fs = (set fs  carrier_vec n  distinct fs  lin_indpt (set fs))" 

definition basis_list :: "'a vec list  bool" where
  "basis_list fs = (set fs  carrier_vec n  length fs = n  carrier_vec n  span (set fs))"

lemma upper_triangular_imp_lin_indpt_list:
  assumes A: "A  carrier_mat n n"
    and tri: "upper_triangular A"
    and diag: "0  set (diag_mat A)"
  shows "lin_indpt_list (rows A)"
  using upper_triangular_imp_distinct[OF assms]
  using upper_triangular_imp_lin_indpt_rows[OF assms] A
  unfolding lin_indpt_list_def by (auto simp: rows_def)

lemma basis_list_basis: assumes "basis_list fs" 
  shows "distinct fs" "lin_indpt (set fs)" "basis (set fs)" 
proof -
  from assms[unfolded basis_list_def] 
  have len: "length fs = n" and C: "set fs  carrier_vec n" 
    and span: "carrier_vec n  span (set fs)" by auto
  show b: "basis (set fs)" 
  proof (rule dim_gen_is_basis[OF finite_set C])
    show "card (set fs)  dim" unfolding dim_is_n unfolding len[symmetric] by (rule card_length)
    show "span (set fs) = carrier_vec n" using span C by auto
  qed
  thus "lin_indpt (set fs)" unfolding basis_def by auto  
  show "distinct fs" 
  proof (rule ccontr)
    assume "¬ distinct fs" 
    hence "card (set fs) < length fs" using antisym_conv1 card_distinct card_length by auto
    also have " = dim" unfolding len dim_is_n ..
    finally have "card (set fs) < dim" by auto
    also have "  card (set fs)" using span finite_set[of fs] 
      using b basis_def gen_ge_dim by auto
    finally show False by simp
  qed
qed

lemma basis_list_imp_lin_indpt_list: assumes "basis_list fs" shows "lin_indpt_list fs" 
  using basis_list_basis[OF assms] assms unfolding lin_indpt_list_def basis_list_def by auto

lemma basis_det_nonzero:
  assumes db:"basis (set G)" and len:"length G = n"
  shows "det (mat_of_rows n G)  0"
proof -
  have M_car1:"mat_of_rows n G  carrier_mat n n" using assms by auto
  hence M_car:"(mat_of_rows n G)T  carrier_mat n n" by auto
  have li:"lin_indpt (set G)"
   and inc_2:"set G  carrier_vec n"
   and issp:"carrier_vec n = span (set G)"
   and RG_in_carr:"i. i < length G  G ! i  carrier_vec n"
    using assms[unfolded basis_def] by auto
  hence "basis_list G" unfolding basis_list_def using len by auto
  from basis_list_basis[OF this] have di:"distinct G" by auto
  have "det ((mat_of_rows n G)T)  0" unfolding det_0_iff_vec_prod_zero[OF M_car] 
  proof
    assume "v. v  carrier_vec n  v  0v n  (mat_of_rows n G)T *v v = 0v n"
    then obtain v where v:"v  span (set G)"
                          "v  0v n" "(mat_of_rows n G)T *v v = 0v n"
      unfolding issp by blast
    from finite_in_span[OF finite_set inc_2 v(1)] obtain a
      where aA: "v = lincomb a (set G)" by blast
    from v(1,2)[folded issp] obtain i where i:"v $ i  0" "i < n" by fastforce
    hence inG:"G ! i  set G" using len by auto
    have di2: "distinct [0..<length G]" by auto
    define f where "f = (λl. i  set [0..<length G]. if l = G ! i then v $ i else 0)"
    hence f':"f (G ! i) = (ia[0..<n]. if G ! ia = G ! i then v $ ia else 0)"
      unfolding f_def sum.distinct_set_conv_list[OF di2] unfolding len by metis
    from v have "mat_of_cols n G *v v = 0v n"
      unfolding transpose_mat_of_rows by auto
    with mat_of_cols_mult_as_finsum[OF v(1)[folded issp len] RG_in_carr]
    have f:"lincomb f (set G) = 0v n" unfolding len f_def by auto
    note [simp] = list_trisect[OF i(2)[folded len],unfolded len]
    note x = i(2)[folded len]
    have [simp]:"(x[0..<i]. if G ! x = G ! i then v $ x else 0) = 0"
      by (rule sum_list_0,auto simp: nth_eq_iff_index_eq[OF di less_trans[OF _ x] x])
    have [simp]:"(x[Suc i..<n]. if G ! x = G ! i then v $ x else 0) = 0"
      apply (rule sum_list_0) using nth_eq_iff_index_eq[OF di _ x] len by auto
    from i(1) have "f (G ! i)  0" unfolding f' by auto
  from lin_dep_crit[OF finite_set subset_refl TrueI inG this f]
    have "lin_dep (set G)".
    thus False using li by auto
  qed
  thus det0:"det (mat_of_rows n G)  0" by (unfold det_transpose[OF M_car1])
qed

lemma lin_indpt_list_add_vec: assumes  
      i: "j < length us" "i < length us" "i  j" 
   and indep: "lin_indpt_list  us" 
shows "lin_indpt_list (us [i := us ! i + c v us ! j])" (is "lin_indpt_list ?V")
proof -
  from indep[unfolded lin_indpt_list_def] have us: "set us  carrier_vec n" 
    and dist: "distinct us" and indep: "lin_indpt (set us)" by auto
  let ?E = "set us - {us ! i}" 
  let ?us = "insert (us ! i) ?E"
  let ?v = "us ! i + c v us ! j"     
  from us i have usi: "us ! i  carrier_vec n" "us ! i  ?E" "us ! i  set us" 
    and usj: "us ! j  carrier_vec n" by auto
  from usi usj have v: "?v  carrier_vec n" by auto      
  have fin: "finite ?E" by auto
  have id: "set us = insert (us ! i) (set us - {us ! i})" using i(2) by auto
  from dist i have diff': "us ! i  us ! j" unfolding distinct_conv_nth by auto
  from subset_li_is_li[OF indep] have indepE: "lin_indpt ?E" by auto
  have Vid: "set ?V = insert ?v ?E" using set_update_distinct[OF dist i(2)] by auto
  have E: "?E  carrier_vec n" using us by auto
  have V: "set ?V  carrier_vec n" using us v unfolding Vid by auto
  from dist i have diff: "us ! i  us ! j" unfolding distinct_conv_nth by auto
  have vspan: "?v  span ?E"
  proof
    assume mem: "?v  span ?E" 
    from diff i have "us ! j  ?E" by auto
    hence "us ! j  span ?E" using E by (metis span_mem)
    hence "- c v us ! j  span ?E" using smult_in_span[OF E] by auto
    from span_add1[OF E mem this] have "?v + (- c v us ! j)  span ?E" .
    also have "?v + (- c v us ! j) = us ! i" using usi usj by auto
    finally have mem: "us ! i  span ?E" .
    from in_spanE[OF this] obtain a A where lc: "us ! i = lincomb a A" and A: "finite A" 
      "A  set us - {us ! i}" 
      by auto
    let ?a = "a (us ! i := -1)" let ?A = "insert (us ! i) A" 
    from A have fin: "finite ?A" by auto
    have lc: "lincomb ?a A = us ! i" unfolding lc
      by (rule lincomb_cong, insert A us lc, auto)
    have "lincomb ?a ?A = 0v n" 
      by (subst lincomb_insert2[OF A(1)], insert A us lc usi diff, auto)
    from not_lindepD[OF indep _ _ _ this] A usi 
    show False by auto
  qed
  hence vmem: "?v  ?E" using span_mem[OF E, of ?v] by auto
  from lin_dep_iff_in_span[OF E indepE v this] vspan 
  have indep1: "lin_indpt (set ?V)" unfolding Vid by auto
  from vmem dist have "distinct ?V" by (metis distinct_list_update)
  with indep1 V show ?thesis unfolding lin_indpt_list_def by auto
qed

lemma scalar_prod_lincomb_orthogonal: assumes ortho: "orthogonal gs" and gs: "set gs  carrier_vec n"
  shows "k  length gs  sumlist (map (λ i. g i v gs ! i) [0 ..< k])  sumlist (map (λ i. h i v gs ! i) [0 ..< k])
  = sum_list (map (λ i. g i * h i * (gs ! i  gs ! i)) [0 ..< k])"
proof (induct k)
  case (Suc k)
  note ortho = orthogonalD[OF ortho]
  let ?m = "length gs" 
  from gs Suc(2) have gsi[simp]: " i. i  k  gs ! i  carrier_vec n" by auto
  from Suc have kn: "k  ?m" and k: "k < ?m" by auto
  let ?v1 = "sumlist (map (λi. g i v gs ! i) [0..<k])" 
  let ?v2 = "(g k v gs ! k)" 
  let ?w1 = "sumlist (map (λi. h i v gs ! i) [0..<k])" 
  let ?w2 = "(h k v gs ! k)" 
  from Suc have id: "[0 ..< Suc k] = [0 ..< k] @ [k]" by simp
  have id: "sumlist (map (λi. g i v gs ! i) [0..<Suc k]) = ?v1 + ?v2"
     "sumlist (map (λi. h i v gs ! i) [0..<Suc k]) = ?w1 + ?w2"
    unfolding id map_append
    by (subst sumlist_append, insert Suc(2), auto)+
  have v1: "?v1  carrier_vec n" by (rule sumlist_carrier, insert Suc(2), auto)
  have v2: "?v2  carrier_vec n" by (insert Suc(2), auto)
  have w1: "?w1  carrier_vec n" by (rule sumlist_carrier, insert Suc(2), auto)
  have w2: "?w2  carrier_vec n" by (insert Suc(2), auto)
  have gsk: "gs ! k  carrier_vec n" by simp
  have v12: "?v1 + ?v2  carrier_vec n" using v1 v2 by auto
  have w12: "?w1 + ?w2  carrier_vec n" using w1 w2 by auto
  have 0: " g h. i < k  (g v gs ! i)  (h v gs ! k) = 0" for i
    by (subst scalar_prod_smult_distrib[OF _ gsk], (insert k, auto)[1],
    subst smult_scalar_prod_distrib[OF _ gsk], (insert k, auto)[1], insert ortho[of i k] k, auto)
  have 1: "?v1  ?w2 = 0" 
    by (subst scalar_prod_left_sum_distrib[OF _ w2], (insert Suc(2), auto)[1], rule sum_list_neutral, 
        insert 0, auto)   
  have 2: "?v2  ?w1 = 0" unfolding comm_scalar_prod[OF v2 w1]
    apply (subst scalar_prod_left_sum_distrib[OF _ v2])
     apply ((insert gs, force)[1])
    apply (rule sum_list_neutral)
    by (insert 0, auto)
  show ?case unfolding id
    unfolding scalar_prod_add_distrib[OF v12 w1 w2]
      add_scalar_prod_distrib[OF v1 v2 w1]
      add_scalar_prod_distrib[OF v1 v2 w2]
      scalar_prod_smult_distrib[OF w2 gsk]
      smult_scalar_prod_distrib[OF gsk gsk]
    unfolding Suc(1)[OF kn]
    by (simp add: 1 2 comm_scalar_prod[OF v2 w1])
qed auto
end


locale gram_schmidt = cof_vec_space n f_ty
  for n :: nat and f_ty :: "'a :: {trivial_conjugatable_linordered_field} itself"
begin

definition Gramian_matrix where
  "Gramian_matrix G k = (let M = mat k n (λ (i,j). (G ! i) $ j) in M * MT)"

lemma Gramian_matrix_alt_def: "k  length G  
  Gramian_matrix G k = (let M = mat_of_rows n (take k G) in M * MT)"
  unfolding Gramian_matrix_def Let_def
  by (rule arg_cong[of _ _ "λ x. x * xT"], unfold mat_of_rows_def, intro eq_matI, auto)

definition Gramian_determinant where
  "Gramian_determinant G k = det (Gramian_matrix G k)"

lemma Gramian_determinant_0 [simp]: "Gramian_determinant G 0 = 1"
  unfolding Gramian_determinant_def Gramian_matrix_def Let_def
  by (simp add: times_mat_def)

lemma orthogonal_imp_lin_indpt_list: 
  assumes ortho: "orthogonal gs" and gs: "set gs  carrier_vec n"
  shows "lin_indpt_list gs" 
proof -
  from corthogonal_distinct[of gs] ortho have dist: "distinct gs" by simp
  show ?thesis unfolding lin_indpt_list_def
  proof (intro conjI gs dist finite_lin_indpt2 finite_set)
    fix lc
    assume 0: "lincomb lc (set gs) = 0v n" (is "?lc = _") 
    have lc: "?lc  carrier_vec n" by (rule lincomb_closed[OF gs])
    let ?m = "length gs" 
    from 0 have "0 = ?lc  ?lc" by simp
    also have "?lc = lincomb_list (λi. lc (gs ! i)) gs" 
      unfolding lincomb_as_lincomb_list_distinct[OF gs dist] ..
    also have " = sumlist (map (λi. lc (gs ! i) v gs ! i) [0..< ?m])" 
      unfolding lincomb_list_def by auto 
    also have "   = (i[0..<?m]. (lc (gs ! i) * lc (gs ! i)) * sq_norm (gs ! i))" (is "_ = sum_list ?sum")
      unfolding scalar_prod_lincomb_orthogonal[OF ortho gs le_refl]
      by (auto simp: sq_norm_vec_as_cscalar_prod power2_eq_square)
    finally have sum_0: "sum_list ?sum = 0" ..
    have nonneg: " x. x  set ?sum  x  0" 
      using zero_le_square[of "lc (gs ! i)" for i] sq_norm_vec_ge_0[of "gs ! i" for i] by auto  
    {
      fix x
      assume x: "x  set gs" 
      then obtain i where i: "i < ?m" and x: "x = gs ! i" unfolding set_conv_nth 
        by auto
      hence "lc x * lc x * sq_norm x  set ?sum" by auto
      with sum_list_nonneg_eq_0_iff[of ?sum, OF nonneg] sum_0 
      have "lc x = 0  sq_norm x = 0" by auto
      with orthogonalD[OF ortho, OF i i, folded x]
      have "lc x = 0" by (auto simp: sq_norm_vec_as_cscalar_prod)
    }
    thus "vset gs. lc v = 0" by auto
  qed
qed

lemma orthocompl_span:
  assumes " x. x  S  v  x = 0" "S  carrier_vec n" and [intro]: "v  carrier_vec n"
  and "y  span S" 
  shows "v  y = 0"
proof -
  {fix a A
   assume "y = lincomb a A" "finite A" "A  S"
   note assms = assms this
   hence [intro!]:"lincomb a A  carrier_vec n" "(λv. a v v v)  A  carrier_vec n" by auto
   have "xA. (a x v x)  v = 0" proof fix x assume "x  A" note assms = assms this
     hence x:"x  S" by auto
     with assms have [intro]:"x  carrier_vec n" by auto
     from assms(1)[OF x] have "x  v = 0" by(subst comm_scalar_prod) force+
     thus "(a x v x)  v = 0"
       apply(subst smult_scalar_prod_distrib) by force+
   qed
   hence "v  lincomb a A = 0" apply(subst comm_scalar_prod) apply force+ unfolding lincomb_def
     apply(subst finsum_scalar_prod_sum) by force+
  }
  thus ?thesis using y  span S unfolding span_def by auto
qed

lemma orthogonal_sumlist:
  assumes ortho: " x. x  set S  v  x = 0" and S: "set S  carrier_vec n" and v: "v  carrier_vec n"
  shows "v  sumlist S = 0"
  by (rule orthocompl_span[OF ortho S v sumlist_in_span[OF S span_mem[OF S]]])

lemma oc_projection_alt_def:
  assumes carr:"(W::'a vec set)  carrier_vec n" "x  carrier_vec n"
      and alt1:"y1  W" "x - y1  orthogonal_complement W"
      and alt2:"y2  W" "x - y2  orthogonal_complement W"
  shows  "y1 = y2"
proof -
  have carr:"y1  carrier_vec n" "y2  carrier_vec n" "x  carrier_vec n" "- y1  carrier_vec n" 
    "0v n  carrier_vec n"
    using alt1 alt2 carr by auto
  hence "y1 - y2  carrier_vec n" by auto
  note carr = this carr
  from alt1 have "yaW  (x - y1)  ya = 0" for ya
    unfolding orthogonal_complement_def by blast
  hence "(x - y1)  y2 = 0" "(x - y1)  y1 = 0" using alt2 alt1 by auto
  hence eq1:"y1  y2 = x  y2" "y1  y1 = x  y1" using carr minus_scalar_prod_distrib by force+
  from this(1) have eq2:"y2  y1 = x  y2" using carr comm_scalar_prod by force
  from alt2 have "yaW  (x - y2)  ya = 0" for ya
    unfolding orthogonal_complement_def by blast
  hence "(x - y2)  y1 = 0" "(x - y2)  y2 = 0" using alt2 alt1 by auto
  hence eq3:"y2  y2 = x  y2" "y2  y1 = x  y1" using carr minus_scalar_prod_distrib by force+
  with eq2 have eq4:"x  y1 = x  y2" by auto
  have "(y1 - y2)2 = 0" unfolding sq_norm_vec_as_cscalar_prod cscalar_prod_is_scalar_prod using carr
    apply(subst minus_scalar_prod_distrib) apply force+
    apply(subst (0 0) scalar_prod_minus_distrib) apply force+
    unfolding eq1 eq2 eq3 eq4 by auto
  with sq_norm_vec_eq_0[of "(y1 - y2)"] carr have "y1 - y2 = 0v n" by fastforce
  hence "y1 - y2 + y2 = y2" using carr by fastforce
  also have "y1 - y2 + y2 = y1" using carr by auto
  finally show "y1 = y2" .
qed

definition
  "is_oc_projection w S v = (w  carrier_vec n  v - w  span S  ( u. u  S  w  u = 0))"

lemma is_oc_projection_sq_norm: assumes "is_oc_projection w S v"
  and S: "S  carrier_vec n" 
  and v: "v  carrier_vec n" 
shows "sq_norm w  sq_norm v" 
proof -
  from assms[unfolded is_oc_projection_def]
  have w: "w  carrier_vec n" 
    and vw: "v - w  span S" and ortho: " u. u  S  w  u = 0" by auto
  have "sq_norm v = sq_norm ((v - w) + w)" using v w 
    by (intro arg_cong[of _ _ sq_norm_vec], auto)
  also have " = ((v - w) + w)  ((v - w) + w)" unfolding sq_norm_vec_as_cscalar_prod
    by simp
  also have " = (v - w)  ((v - w) + w) + w  ((v - w) + w)" 
    by (rule add_scalar_prod_distrib, insert v w, auto)
  also have " = ((v - w)  (v - w) + (v - w)  w) + (w  (v - w) + w  w)" 
    by (subst (1 2) scalar_prod_add_distrib, insert v w, auto)
  also have " = sq_norm (v - w) + 2 * (w  (v - w)) + sq_norm w" 
    unfolding sq_norm_vec_as_cscalar_prod using v w by (auto simp: comm_scalar_prod[of w _ "v - w"])
  also have "  2 * (w  (v - w)) + sq_norm w" using sq_norm_vec_ge_0[of "v - w"] by auto
  also have "w  (v - w) = 0" using orthocompl_span[OF ortho S w vw] by auto
  finally show ?thesis by auto
qed

definition oc_projection where
"oc_projection S fi  (SOME v. is_oc_projection v S fi)"

lemma inv_in_span:
  assumes incarr[intro]:"U  carrier_vec n" and insp:"a  span U"
  shows "- a  span U"
proof -
  from insp[THEN in_spanE] obtain aa A where a:"a = lincomb aa A" "finite A" "A  U" by auto
  with assms have [intro!]:"(λv. aa v v v)  A  carrier_vec n" by auto
  from a(1) have e1:"- a = lincomb (λ x. - 1 * aa x) A" unfolding smult_smult_assoc[symmetric] lincomb_def
    by(subst finsum_smult[symmetric]) force+
  show ?thesis using e1 a span_def by blast
qed

lemma non_span_det_zero:
  assumes len: "length G = n"
  and nonb:"¬ (carrier_vec n  span (set G))"
  and carr:"set G  carrier_vec n"
  shows "det (mat_of_rows n G) = 0" unfolding det_0_iff_vec_prod_zero
proof -
  let ?A = "(mat_of_rows n G)T" let ?B = "1m n"
  from carr have carr_mat:"?A  carrier_mat n n" "?B  carrier_mat n n" "mat_of_rows n G  carrier_mat n n"
    using len mat_of_rows_carrier(1) by auto
  from carr have g_len:" i. i < length G  G ! i  carrier_vec n" by auto
  from nonb obtain v where v:"v  carrier_vec n" "v  span (set G)" by fast
  hence "v  0v n" using span_zero by auto
  obtain B C where gj:"gauss_jordan ?A ?B = (B,C)" by force
  note gj = carr_mat(1,2) gj
  hence B:"B = fst (gauss_jordan ?A ?B)" by auto
  from gauss_jordan[OF gj] have BC:"B  carrier_mat n n" by auto
  from gauss_jordan_transform[OF gj] obtain P where
   P:"PUnits (ring_mat TYPE('a) n ?B)"  "B = P * ?A" by fast
  hence PC:"P  carrier_mat n n" unfolding Units_def by (simp add: ring_mat_simps)
  from mat_inverse[OF PC] P obtain PI where "mat_inverse P = Some PI" by fast
  from mat_inverse(2)[OF PC this]
  have PI:"P * PI = 1m n" "PI * P = 1m n" "PI  carrier_mat n n" by auto
  have "B  1m n" proof
    assume "B = ?B"
    hence "?A * P = ?B" unfolding P
      using PC P(2) carr_mat(1) mat_mult_left_right_inverse by blast
    hence "?A * P *v v = v" using v by auto
    hence "?A *v (P *v v) = v" unfolding assoc_mult_mat_vec[OF carr_mat(1) PC v(1)].
    hence v_eq:"mat_of_cols n G *v (P *v v) = v"
      unfolding transpose_mat_of_rows by auto
    have pvc:"P *v v  carrier_vec (length G)" using PC v len by auto
    from mat_of_cols_mult_as_finsum[OF pvc g_len,unfolded v_eq] obtain a where
      "v = lincomb a (set G)" by auto
    hence "v  span (set G)" by (intro in_spanI[OF _ finite_set subset_refl])
    thus False using v by auto
  qed
  with det_non_zero_imp_unit[OF carr_mat(1)] show ?thesis
    unfolding gauss_jordan_check_invertable[OF carr_mat(1,2)] B det_transpose[OF carr_mat(3)]
    by metis
qed

lemma span_basis_det_zero_iff:
assumes "length G = n" "set G  carrier_vec n"
shows "carrier_vec n  span (set G)  det (mat_of_rows n G)  0" (is ?q1)
      "carrier_vec n  span (set G)  basis (set G)" (is ?q2)
      "det (mat_of_rows n G)  0  basis (set G)" (is ?q3)
proof -
  have dc:"det (mat_of_rows n G)  0  carrier_vec n  span (set G)"
    using assms non_span_det_zero by auto
  have cb:"carrier_vec n  span (set G)  basis (set G)" using assms basis_list_basis 
    by (auto simp: basis_list_def)
  have bd:"basis (set G)  det (mat_of_rows n G)  0" using assms basis_det_nonzero by auto
  show ?q1 ?q2 ?q3 using dc cb bd by metis+
qed

lemma lin_indpt_list_nonzero:
  assumes "lin_indpt_list G" 
  shows "0v n  set G"
proof-
  from assms[unfolded lin_indpt_list_def] have "lin_indpt (set G)" by auto
  from vs_zero_lin_dep[OF _ this] assms[unfolded lin_indpt_list_def] show zero: "0v n  set G" by auto
qed

lemma is_oc_projection_eq:
  assumes ispr:"is_oc_projection a S v" "is_oc_projection b S v" 
    and carr: "S  carrier_vec n" "v  carrier_vec n"
  shows "a = b"
proof -
  from carr have c2:"span S  carrier_vec n" "v  carrier_vec n" by auto
  have a:"v - (v - a) = a" using carr ispr by auto
  have b:"v - (v - b) = b" using carr ispr by auto
  have "(v - a) = (v - b)" 
    apply(rule oc_projection_alt_def[OF c2])
    using ispr a b unfolding in_orthogonal_complement_span[OF carr(1)]
    unfolding orthogonal_complement_def is_oc_projection_def by auto
  hence "v - (v - a) = v - (v - b)" by metis
  thus ?thesis unfolding a b.
qed



fun adjuster_wit :: "'a list  'a vec  'a vec list  'a list × 'a vec"
  where "adjuster_wit wits w [] = (wits, 0v n)"
  |  "adjuster_wit wits w (u#us) = (let a = (w  u)/ sq_norm u in 
            case adjuster_wit (a # wits) w us of (wit, v)
          (wit, -a v u + v))"

fun sub2_wit where
    "sub2_wit us [] = ([], [])"
  | "sub2_wit us (w # ws) =
     (case adjuster_wit [] w us of (wit,aw)  let u = aw + w in
      case sub2_wit (u # us) ws of (wits, vvs)  (wit # wits, u # vvs))"  
    
definition main :: "'a vec list  'a list list × 'a vec list" where 
  "main us = sub2_wit [] us"
end


locale gram_schmidt_fs = 
  fixes n :: nat and fs :: "'a :: {trivial_conjugatable_linordered_field} vec list"
begin

sublocale gram_schmidt n "TYPE('a)" .

fun gso and μ where
  "gso i = fs ! i + sumlist (map (λ j. - μ i j v gso j) [0 ..< i])" 
| "μ i j = (if j < i then (fs ! i  gso j)/ sq_norm (gso j) else if i = j then 1 else 0)" 
    
declare gso.simps[simp del]
declare μ.simps[simp del]


lemma gso_carrier'[intro]:
  assumes " i. i  j  fs ! i  carrier_vec n"
  shows "gso j  carrier_vec n"
using assms proof(induct j rule:nat_less_induct[rule_format])
  case (1 j)
  then show ?case unfolding gso.simps[of j] by (auto intro!:sumlist_carrier add_carrier_vec)
qed

lemma adjuster_wit: assumes res: "adjuster_wit wits w us = (wits',a)"
  and w: "w  carrier_vec n"
    and us: " i. i  j  fs ! i  carrier_vec n"
    and us_gs: "us = map gso (rev [0 ..< j])" 
    and wits: "wits = map (μ i) [j ..< i]" 
    and j: "j  n" "j  i" 
    and wi: "w = fs ! i" 
  shows "adjuster n w us = a  a  carrier_vec n  wits' = map (μ i) [0 ..< i] 
      (a = sumlist (map (λj. - μ i j v gso j) [0..<j]))"
  using res us us_gs wits j
proof (induct us arbitrary: wits wits' a j)
  case (Cons u us wits wits' a j)
  note us_gs = Cons(4)
  note wits = Cons(5)
  note jn = Cons(6-7)
  from us_gs obtain jj where j: "j = Suc jj" by (cases j, auto)
  from jn j have jj: "jj  n" "jj < n" "jj  i" "jj < i" by auto
  have zj: "[0 ..< j] = [0 ..< jj] @ [jj]" unfolding j by simp
  have jjn: "[jj ..< i] = jj # [j ..< i]" using jj unfolding j by (metis upt_conv_Cons)
  from us_gs[unfolded zj] have ugs: "u = gso jj" and us: "us = map gso (rev [0..<jj])" by auto
  let ?w = "w  u / (u  u)" 
  have muij: "?w = μ i jj" unfolding μ.simps[of i jj] ugs wi sq_norm_vec_as_cscalar_prod using jj by auto
  have wwits: "?w # wits = map (μ i) [jj..<i]" unfolding jjn wits muij by simp
  obtain wwits b where rec: "adjuster_wit (?w # wits) w us = (wwits,b)" by force
  from Cons(1)[OF this Cons(3) us wwits jj(1,3),unfolded j] have IH: 
     "adjuster n w us = b" "wwits = map (μ i) [0..<i]"
     "b = sumlist (map (λj. - μ i j v gso j) [0..<jj])"
      and b: "b  carrier_vec n" by auto
  from Cons(2)[simplified, unfolded Let_def rec split sq_norm_vec_as_cscalar_prod 
      cscalar_prod_is_scalar_prod]
  have id: "wits' = wwits" and a: "a = - ?w v u + b" by auto
  have 1: "adjuster n w (u # us) = a" unfolding a IH(1)[symmetric] by auto     
  from id IH(2) have wits': "wits' =  map (μ i) [0..<i]" by simp
  have carr:"set (map (λj. - μ i j v gso j) [0..<j])  carrier_vec n"
            "set (map (λj. - μ i j v gso j) [0..<jj])  carrier_vec n" and u:"u  carrier_vec n" 
    using Cons j by (auto intro!:gso_carrier')
  from u b a have ac: "a  carrier_vec n" "dim_vec (-?w v u) = n" "dim_vec b = n" "dim_vec u = n" by auto
  show ?case
    apply (intro conjI[OF 1] ac exI conjI wits')
    unfolding carr a IH zj muij ugs[symmetric] map_append
    apply (subst sumlist_append)
    using Cons.prems j apply force
    using b u ugs IH(3) by auto
qed auto

lemma sub2_wit:
  assumes "set us  carrier_vec n" "set ws  carrier_vec n" "length us + length ws = m" 
    and "ws = map (λ i. fs ! i) [i ..< m]"
    and "us = map gso (rev [0 ..< i])" 
    and us: " j. j < m  fs ! j  carrier_vec n"
    and mn: "m  n" 
  shows "sub2_wit us ws = (wits,vvs)  gram_schmidt_sub2 n us ws = vvs 
     vvs = map gso [i ..< m]  wits = map (λ i. map (μ i) [0..<i]) [i ..< m]"
  using assms(1-6)
proof (induct ws arbitrary: us vvs i wits)
  case (Cons w ws us vs)  
  note us = Cons(3) note wws = Cons(4)
  note wsf' = Cons(6)
  note us_gs = Cons(7)
  from wsf' have "i < m" "i  m" by (cases "i < m", auto)+
  hence i_m: "[i ..< m] = i # [Suc i ..< m]" by (metis upt_conv_Cons)
  from i < m mn have "i < n" "i  n" "i  m" by auto
  hence i_n: "[i ..< n] = i # [Suc i ..< n]" by (metis upt_conv_Cons)
  from wsf' i_m have wsf: "ws = map (λ i. fs ! i) [Suc i ..< m]" 
    and fiw: "fs !  i = w" by auto
  from wws have w: "w  carrier_vec n" and ws: "set ws  carrier_vec n" by auto
  have list: "map (μ i) [i ..< i] = []" by auto
  let ?a = "adjuster_wit [] w us" 
  obtain wit a where a: "?a = (wit,a)" by force
  obtain wits' vv where gs: "sub2_wit ((a + w) # us) ws = (wits',vv)" by force      
  from adjuster_wit[OF a w Cons(8) us_gs list[symmetric] i  n _ fiw[symmetric]] us wws i < m
  have awus: "set ((a + w) # us)  carrier_vec n"  
     and aa: "adjuster n w us = a" "a  carrier_vec n" 
     and aaa: "a = sumlist (map (λj. - μ i j v gso j) [0..<i])"  
     and wit: "wit = map (μ i) [0..<i]" 
    by auto
  have aw_gs: "a + w = gso i" unfolding gso.simps[of i] fiw aaa[symmetric] using aa(2) w by auto
  with us_gs have us_gs': "(a + w) # us = map gso (rev [0..<Suc i])" by auto
  from Cons(1)[OF gs awus ws _ wsf us_gs' Cons(8)] Cons(5) 
  have IH: "gram_schmidt_sub2 n ((a + w) # us) ws = vv"  
    and vv: "vv = map gso [Suc i..<m]" 
    and wits': "wits' = map (λi. map (μ i) [0..<i]) [Suc i ..< m]" by auto
  from gs a aa IH Cons(5) 
  have gs_vs: "gram_schmidt_sub2 n us (w # ws) = vs" and vs: "vs = (a + w) # vv" using Cons(2)
    by (auto simp add: Let_def snd_def split:prod.splits)
  from Cons(2)[unfolded sub2_wit.simps a split Let_def gs] have wits: "wits = wit # wits'" by auto
  from vs vv aw_gs have vs: "vs = map gso [i ..< m]" unfolding i_m by auto
  with gs_vs show ?case unfolding wits wit wits' by (auto simp: i_m)
qed auto
  
lemma partial_connect: fixes vs
  assumes "length fs = m" "k  m" "m  n" "set us  carrier_vec n" "snd (main us) = vs" 
  "us = take k fs" "set fs  carrier_vec n"
shows "gram_schmidt n us = vs" 
    "vs = map gso [0..<k]" 
proof -
  have [simp]: "map ((!) fs) [0..<k] = take k fs" using assms(1,2) by (intro nth_equalityI, auto)
  have carr: "j < m  fs ! j  carrier_vec n" for j using assms by auto
  note assms(5)[unfolded main_def]
  have "gram_schmidt_sub2 n [] (take k fs) = vvs  vvs = map gso [0..<k]  wits = map (λi. map (μ i) [0..<i]) [0..<k]"
    if "vvs = snd (sub2_wit [] (take k fs))" "wits = fst (sub2_wit [] (take k fs))" for vvs wits
    using assms that by (intro sub2_wit) (auto)
  with assms main_def
  show "gram_schmidt n us = vs" "vs = map gso [0..<k]" unfolding gram_schmidt_code
    by (auto simp add: main_def case_prod_beta')
qed

lemma adjuster_wit_small:
  "(adjuster_wit v a xs) = (x1,x2)
   (fst (adjuster_wit v a xs) = x1  x2 = adjuster n a xs)"
proof(induct xs arbitrary: a v x1 x2)
  case (Cons a xs)
  then show ?case
    by (auto simp:Let_def sq_norm_vec_as_cscalar_prod split:prod.splits) 
qed auto

lemma sub2: "rev xs @ snd (sub2_wit xs us) = rev (gram_schmidt_sub n xs us)"
proof -
  have "sub2_wit xs us = (x1, x2)  rev xs @ x2 = rev (gram_schmidt_sub n xs us)"
    for x1 x2 xs us
    apply(induct us arbitrary: xs x1 x2)
    by (auto simp:Let_def rev_unsimp adjuster_wit_small split:prod.splits simp del:rev.simps)
  thus ?thesis 
    apply (cases us)
    by (auto simp:Let_def rev_unsimp adjuster_wit_small split:prod.splits simp del:rev.simps)
qed

lemma gso_connect: "snd (main us) = gram_schmidt n us" unfolding main_def gram_schmidt_def
  using sub2[of Nil us] by auto

definition weakly_reduced :: "'a  nat  bool" 
  (* for k = n, this is reduced according to "Modern Computer Algebra" *)
  where "weakly_reduced α k = ( i. Suc i < k  
    sq_norm (gso i)  α * sq_norm (gso (Suc i)))" 
  
definition reduced :: "'a  nat  bool" 
  (* this is reduced according to LLL original paper *)
  where "reduced α k = (weakly_reduced α k  
    ( i j. i < k  j < i  abs (μ i j)  1/2))"


end (* gram_schmidt_fs *)


locale gram_schmidt_fs_Rn = gram_schmidt_fs +
  assumes fs_carrier: "set fs  carrier_vec n"
begin

abbreviation (input) m where "m  length fs"

definition M where "M k = mat k k (λ (i,j). μ i j)"

lemma f_carrier[simp]: "i < m  fs ! i  carrier_vec n" 
  using fs_carrier unfolding set_conv_nth by force

lemma gso_carrier[simp]: "i < m  gso i  carrier_vec n" 
  using gso_carrier' f_carrier by auto

lemma gso_dim[simp]: "i < m  dim_vec (gso i) = n" by auto
lemma f_dim[simp]: "i < m  dim_vec (fs ! i) = n" by auto

lemma fs0_gso0: "0 < m  fs ! 0 = gso 0" 
  unfolding gso.simps[of 0] using f_dim[of 0] 
  by (cases fs, auto simp add: upt_rec)

lemma fs_by_gso_def : 
assumes i: "i < m"
shows "fs ! i = gso i + M.sumlist (map (λja. μ i ja v gso ja) [0..<i])" (is "_ = _ + ?sum")
proof -
  {
    fix f
    have a: "M.sumlist (map (λja. f ja v gso ja) [0..<i])  carrier_vec n" 
      using gso_carrier i by (intro M.sumlist_carrier, auto)
    hence "dim_vec (M.sumlist (map (λja. f ja v gso ja) [0..<i])) = n" by auto
    note a this
  } note sum_carrier = this
  note [simp] = sum_carrier(2)
  have f: "fs ! i  carrier_vec n" using i by simp
  have "gso i + ?sum = fs ! i + M.sumlist (map (λj. - μ i j v gso j) [0..<i]) + ?sum " 
    (is "_ = _ + ?minus_sum + _")
    unfolding gso.simps[of i] by simp
  also have "?minus_sum = - ?sum"
    using gso_carrier i sum_carrier
    by (intro eq_vecI, auto simp: sumlist_nth sum_negf)
  also have "fs ! i + (-?sum) + ?sum = fs ! i"
    using sum_carrier fs_carrier f by simp
  finally show ?thesis by auto
qed


lemma main_connect:
  assumes "m  n"
  shows "gram_schmidt n fs = map gso [0..<m]"
proof -
  obtain vs where snd_main: "snd (main fs) = vs" by auto
  have "gram_schmidt_sub2 n [] fs = snd (sub2_wit [] fs)  snd (sub2_wit [] fs) = map gso [0..<length fs]
         wits = map (λi. map (μ i) [0..<i]) [0..<length fs]" 
    if "wits = fst (sub2_wit [] fs)" for wits
    using assms that fs_carrier by (intro  sub2_wit) (auto simp add: map_nth) 
  then have "gram_schmidt_sub2 n [] fs = vs  vs = map gso [0..<m]"
    using snd_main main_def by auto
  thus "gram_schmidt n fs = map gso [0..<m]" by (auto simp: gram_schmidt_code)
qed


lemma reduced_gso_E: "weakly_reduced α k  k  m  Suc i < k  
  sq_norm (gso i)  α * sq_norm (gso (Suc i))" 
  unfolding weakly_reduced_def by auto
      
abbreviation (input) FF where "FF  mat_of_rows n fs"
abbreviation (input) Fs where "Fs  mat_of_rows n (map gso [0..<m])" 
  
lemma FF_dim[simp]: "dim_row FF = m" "dim_col FF = n" "FF  carrier_mat m n" 
  unfolding mat_of_rows_def by (auto)

lemma Fs_dim[simp]: "dim_row Fs = m" "dim_col Fs = n" "Fs  carrier_mat m n" 
  unfolding mat_of_rows_def by (auto simp: main_connect)

lemma M_dim[simp]: "dim_row (M m) = m" "dim_col (M m) = m" "(M m)  carrier_mat m m"
  unfolding M_def by auto
    
lemma FF_index[simp]: "i < m  j < n  FF $$ (i,j) = fs ! i $ j" 
  unfolding mat_of_rows_def by auto

lemma M_index[simp]:"i < m  j < m  (M m) $$ (i,j) = μ i j"
  unfolding M_def by auto
    
(* equation 2 on page 463 of textbook *)      
lemma matrix_equality: "FF = (M m) * Fs" 
proof - 
  let ?P = "(M m) * Fs" 
  have dim: "dim_row FF = m" "dim_col FF = n" "dim_row ?P = m" "dim_col ?P = n" "dim_row (M m) = m" "dim_col (M m) = m" 
      "dim_row Fs = m" "dim_col Fs = n" 
    by (auto simp: mat_of_rows_def mat_of_rows_list_def main_connect)
  show ?thesis 
  proof (rule eq_matI; unfold dim)
    fix i j
    assume i: "i < m" and j: "j < n" 
    from i have split: "[0 ..< m] = [0 ..< i] @ [i] @ [Suc i ..< m]"
      by (metis append_Cons append_self_conv2 less_Suc_eq_le less_imp_add_positive upt_add_eq_append upt_rec zero_less_Suc)
    let ?prod = "λ k. μ i k * gso k $ j" 
    have dim2: "dim_vec (col Fs j) = m" using j dim by auto
    define idx where "idx = [0..<i]" 
    have idx: "set idx  {0 ..< i}" unfolding idx_def using i by auto
    let ?vec = "sumlist (map (λj. - μ i j v gso j) idx)" 
    have vec: "?vec  carrier_vec n" by (rule sumlist_carrier, insert idx gso_carrier i, auto)
    hence dimv: "dim_vec ?vec = n" by auto
    have "?P $$ (i,j) = row (M m) i  col Fs j" using dim i j by auto
    also have " = ( k = 0..<m. row (M m) i $ k * col Fs j $ k)" 
      unfolding scalar_prod_def dim2 by auto
    also have " = ( k = 0..<m. ?prod k)" 
      by (rule sum.cong[OF refl], insert i j dim, auto simp: mat_of_rows_list_def mat_of_rows_def)
    also have " = sum_list (map ?prod [0 ..< m])"       
      by (subst sum_list_distinct_conv_sum_set, auto)
    also have " = sum_list (map ?prod idx) + ?prod i + sum_list (map ?prod [Suc i ..< m])" 
      unfolding split idx_def by auto
    also have "?prod i = gso i $ j" unfolding μ.simps by simp
    also have " = fs ! i $ j + sum_list (map (λk. - μ i k * gso k $ j) idx)" unfolding gso.simps[of i] idx_def[symmetric]
      by (subst index_add_vec, unfold dimv, rule j, subst sumlist_vec_index[OF _ j], insert idx gso_carrier i j, 
      auto simp: o_def intro!: arg_cong[OF map_cong])
    also have "sum_list (map (λk. - μ i k * gso k $ j) idx) = - sum_list (map (λk. μ i k * gso k $ j) idx)" 
      by (induct idx, auto)
    also have "sum_list (map ?prod [Suc i ..< m]) = 0"
      by (rule sum_list_neutral, auto simp: μ.simps)
    finally have "?P $$ (i,j) = fs ! i $ j" by simp
    with FF_index[OF i j]
    show "FF $$ (i,j) = ?P $$ (i,j)" by simp
  qed auto
qed
  
lemma fi_is_sum_of_mu_gso: assumes i: "i < m" 
  shows "fs ! i = sumlist (map (λ j. μ i j v gso j) [0 ..< Suc i])" 
proof -
  let ?l = "sumlist (map (λ j. μ i j v gso j) [0 ..< Suc i])" 
  have "?l  carrier_vec n" by (rule sumlist_carrier, insert gso_carrier i, auto)
  hence dim: "dim_vec ?l = n" by (rule carrier_vecD)
  show ?thesis 
  proof (rule eq_vecI, unfold dim f_dim[OF i])
    fix j
    assume j: "j < n"     
    from i have split: "[0 ..< m] = [0 ..< Suc i] @ [Suc i ..< m]"
      by (metis Suc_lessI append.assoc append_same_eq less_imp_add_positive order_refl upt_add_eq_append zero_le)
    let ?prod = "λ k. μ i k * gso k $ j" 
    have "fs ! i $ j = FF $$ (i,j)" using i j by simp
    also have " = ((M m) * Fs) $$ (i,j)" using matrix_equality by simp
    also have " = row (M m) i  col Fs j" using i j by auto
    also have " = ( k = 0..<m. row (M m) i $ k * col Fs j $ k)" 
      unfolding scalar_prod_def by auto
    also have " = ( k = 0..<m. ?prod k)" 
      by (rule sum.cong[OF refl], insert i j dim, auto simp: mat_of_rows_list_def mat_of_rows_def)
    also have " = sum_list (map ?prod [0 ..< m])"       
      by (subst sum_list_distinct_conv_sum_set, auto)
    also have " = sum_list (map ?prod [0 ..< Suc i]) + sum_list (map ?prod [Suc i ..< m])" 
      unfolding split by auto
    also have "sum_list (map ?prod [Suc i ..< m]) = 0" 
      by (rule sum_list_neutral, auto simp: μ.simps)
    also have "sum_list (map ?prod [0 ..< Suc i]) = ?l $ j" 
      by (subst sumlist_vec_index[OF _ j], (insert i, auto simp: intro!: gso_carrier)[1], 
        rule arg_cong[of _ _ sum_list], insert i j, auto)
    finally show "fs ! i $ j = ?l $ j" by simp
  qed simp
qed

lemma gi_is_fi_minus_sum_mu_gso:
  assumes i: "i < m" 
  shows "gso i = fs ! i - sumlist (map (λ j. μ i j v gso j) [0 ..< i])" (is "_ = _ - ?sum")
proof -
  have sum: "?sum  carrier_vec n" 
    by (rule sumlist_carrier, insert gso_carrier i, auto)
  show ?thesis unfolding fs_by_gso_def[OF i]
    by (intro eq_vecI, insert gso_carrier[OF i] sum, auto)
qed

(* Theorem 16.5 (iv) *)  
lemma det: assumes m: "m = n" shows "det FF = det Fs" 
  unfolding matrix_equality
  apply (subst det_mult[OF M_dim(3)], (insert Fs_dim(3) m, auto)[1])
  apply (subst det_lower_triangular[OF _ M_dim(3)]) 
  by (subst M_index, (auto simp: μ.simps)[3], unfold prod_list_diag_prod, auto simp: μ.simps) 
end

locale gram_schmidt_fs_lin_indpt = gram_schmidt_fs_Rn +
  assumes lin_indpt: "lin_indpt (set fs)" and dist: "distinct fs"
begin

lemmas loc_assms = lin_indpt dist

lemma mn:
  shows "m  n"
proof -
  have n: "n = dim" by (simp add: dim_is_n)
  have m: "m = card (set fs)"
    using distinct_card loc_assms by metis
  from m n have mn: "m  n  card (set fs)  dim" by simp
  show ?thesis unfolding mn
    by (rule li_le_dim, use loc_assms fs_carrier in auto)
qed

lemma
shows span_gso: "span (gso ` {0..<m}) = span (set fs)"
  and orthogonal_gso: "orthogonal (map gso [0..<m])" 
  and dist_gso: "distinct (map gso [0..<m])"
  using gram_schmidt_result[OF fs_carrier _ _ main_connect[symmetric]] loc_assms mn by auto

lemma gso_inj[intro]:
  assumes "i < m"
  shows "inj_on gso {0..<i}"
proof -
  { fix x y assume assms': "i < m" "x  {0..<i}" "y  {0..<i}" "gso x = gso y"
  have "distinct (map gso [0..<m])" "x < length (map gso [0..<m])" "y < length (map gso [0..<m])" 
    using dist_gso assms mn assms' by (auto intro!: dist_gso)
  from nth_eq_iff_index_eq[OF this] assms' have "x = y" by auto }
  then show ?thesis
    using assms by (intro inj_onI) auto
qed

lemma partial_span:
  assumes i: "i  m" 
  shows "span (gso ` {0 ..< i}) = span (set (take i fs))" 
proof -
  let ?f = "λ i. fs ! i" 
  let ?us = "take i fs" 
  have len: "length ?us = i" using i by auto
  from fs_carrier i have us: "set ?us  carrier_vec n" 
    by (meson set_take_subset subset_trans)
  obtain vi where main: "snd (main ?us) = vi" by force
  from dist have dist: "distinct ?us" by auto
  from lin_indpt have indpt: "lin_indpt (set ?us)" 
    using supset_ld_is_ld[of "set ?us", of "set (?us @ drop i fs)"] 
    by (auto simp: set_take_subset)
  from partial_connect[OF _ i mn us main refl fs_carrier] assms
  have gso: "vi = gram_schmidt n ?us" and vi: "vi = map gso [0 ..< i]" by auto
  from cof_vec_space.gram_schmidt_result(1)[OF us dist indpt gso, unfolded vi]
  show ?thesis by auto
qed

lemma partial_span': 
  assumes i: "i  m" 
  shows "span (gso ` {0 ..< i}) = span ((λ j. fs ! j) ` {0 ..< i})"
  unfolding partial_span[OF i]
  by (rule arg_cong[of _ _ span], subst nth_image, insert i loc_assms, auto)

(* Theorem 16.5 (iii) *)
lemma orthogonal:
  assumes "i < m" "j < m" "i  j"
  shows "gso i  gso j = 0"
  using assms mn orthogonal_gso[unfolded orthogonal_def] by auto

(* Theorem 16.5 (i) not in full general form *)  
lemma same_base:
  shows "span (set fs) = span (gso ` {0..<m})" 
  using span_gso loc_assms by simp

(* Theorem 16.5 (ii), second half *)
lemma sq_norm_gso_le_f:
  assumes i: "i < m"
  shows "sq_norm (gso i)  sq_norm (fs ! i)"
proof -
  have id: "[0 ..< Suc i] = [0 ..< i] @ [i]" by simp
  let ?sum = "sumlist (map (λj. μ i j v gso j) [0..<i])" 
  have sum: "?sum  carrier_vec n" and gsoi: "gso i  carrier_vec n" using i
    by (auto intro!: sumlist_carrier gso_carrier)
  from fi_is_sum_of_mu_gso[OF i, unfolded id]
  have "sq_norm (fs ! i) = sq_norm (sumlist (map (λj. μ i j v gso j) [0..<i] @ [gso i]))" by (simp add: μ.simps)
  also have " = sq_norm (?sum + gso i)" 
    by (subst sumlist_append, insert gso_carrier i, auto)
  also have " = (?sum + gso i)  (?sum + gso i)" by (simp add: sq_norm_vec_as_cscalar_prod)
  also have " = ?sum  (?sum + gso i) + gso i  (?sum + gso i)" 
    by (rule add_scalar_prod_distrib[OF sum gsoi], insert sum gsoi, auto)
  also have " = (?sum  ?sum + ?sum  gso i) + (gso i  ?sum + gso i  gso i)" 
    by (subst (1 2) scalar_prod_add_distrib[of _ n], insert sum gsoi, auto)
  also have "?sum  ?sum = sq_norm ?sum" by (simp add: sq_norm_vec_as_cscalar_prod)
  also have "gso i  gso i = sq_norm (gso i)" by (simp add: sq_norm_vec_as_cscalar_prod)
  also have "gso i  ?sum = ?sum  gso i" using gsoi sum by (simp add: comm_scalar_prod)
  finally have "sq_norm (fs ! i) = sq_norm ?sum + 2 * (?sum  gso i) + sq_norm (gso i)" by simp
  also have "  2 * (?sum  gso i) + sq_norm (gso i)" using sq_norm_vec_ge_0[of ?sum] by simp
  also have "?sum  gso i = (vmap (λj. μ i j v gso j) [0..<i]. v  gso i)" 
    by (subst scalar_prod_left_sum_distrib[OF _ gsoi], insert i gso_carrier, auto)
  also have " = 0" 
  proof (rule sum_list_neutral, goal_cases)
    case (1 x)
    then obtain j where j: "j < i" and x: "x = (μ i j v gso j)  gso i" by auto
    from j i have gsoj: "gso j  carrier_vec n" by auto
    have "x = μ i j * (gso j  gso i)" using gsoi gsoj unfolding x by simp
    also have "gso j  gso i = 0" 
      by (rule orthogonal, insert j i assms, auto)
    finally show "x = 0" by simp
  qed
  finally show ?thesis by simp
qed

(* Theorem 16.5 (ii), first half *)
lemma oc_projection_exist:
  assumes i: "i < m" 
  shows "fs ! i - gso i  span (gso ` {0..<i})"
proof
  let ?A = "gso ` {0..<i}"
  show finA:"finite ?A" by auto
  have carA[intro!]:"?A  carrier_vec n" using gso_dim assms by auto
  let "?a v" = "n[0..<i]. if v = gso n then μ i n else 0"
  have d:"(sumlist (map (λj. - μ i j v gso j) [0..<i]))  carrier_vec n"
    using gso.simps[of i] gso_dim[OF i] unfolding carrier_vec_def by auto
  note [intro] = f_carrier[OF i] gso_carrier[OF i] d
  have [intro!]:"(λv. ?a v v v)  gso ` {0..<i}  carrier_vec n"
     using gso_carrier assms by auto
  {fix ia assume ia[intro]:"ia < n"
    have "(xgso ` {0..<i}. (?a x v x) $ ia) =
      - (xmap (λj. - μ i j v gso j) [0..<i]. x $ ia)"
    unfolding map_map comm_monoid_add_class.sum.reindex[OF gso_inj[OF assms]]
    unfolding atLeastLessThan_upt sum_set_upt_conv_sum_list_nat uminus_sum_list_map o_def
    proof(rule arg_cong[OF map_cong, OF refl],goal_cases)
      case (1 x) hence x:"x < m" "x < i" using assms by auto
      hence d:"insert x (set [0..<i]) = {0..<i}"
              "count (mset [0..<i]) x = 1" by auto
      hence "inj_on gso (insert x (set [0..<i]))" using gso_inj[OF assms] by auto
      from inj_on_filter_key_eq[OF this,folded replicate_count_mset_eq_filter_eq]
      have "[n[0..<i] . gso x = gso n] = [x]" using x assms d replicate.simps(2)[of 0] by auto
      hence "(n[0..<i]. if gso x = gso n then μ i n else 0) = μ i x"
        unfolding sum_list_map_filter'[symmetric] by auto
      with ia gso_dim x show ?case apply(subst index_smult_vec) by force+
    qed
    hence "(Vvgso ` {0..<i}. ?a v v v) $ ia =
          (- local.sumlist (map (λj. - μ i j v gso j) [0..<i])) $ ia"
      using d assms
      apply (subst (0 0) finsum_index index_uminus_vec) apply force+
      apply (subst sumlist_vec_index) by force+
  }
  hence id: "(Vv?A. ?a v v v) = - sumlist (map (λj. - μ i j v gso j) [0..<i])"
    using d lincomb_dim[OF finA carA,unfolded lincomb_def] by(intro eq_vecI,auto)
  show "fs ! i - gso i = lincomb ?a ?A" unfolding lincomb_def gso.simps[of i] id
    by (rule eq_vecI, auto)
qed auto

lemma oc_projection_unique:
  assumes "i < m" 
          "v  carrier_vec n"
          " x. x  gso ` {0..<i}  v  x = 0"
          "fs ! i - v  span (gso ` {0..<i})"
  shows "v = gso i"
proof -
  from assms have carr_span:"span (gso ` {0..<i})  carrier_vec n" by(intro span_is_subset2) auto
  from assms have carr: "gso ` {0..<i}  carrier_vec n" by auto
  from assms have eq:"fs ! i - (fs ! i - v) = v" for v by auto
  from orthocompl_span[OF _ carr] assms
  have "y  span (gso ` {0..<i})  v  y = 0" for y by auto
  hence oc1:"fs ! i - (fs ! i - v)  orthogonal_complement (span (gso ` {0..< i}))"
    unfolding eq orthogonal_complement_def using assms by auto
  have "x  gso ` {0..<i}  gso i  x = 0" for x using assms orthogonal by auto
  hence "y  span (gso ` {0..<i})  gso i  y = 0" for y
    by (rule orthocompl_span) (use carr gso_carrier assms in auto)
  hence oc2:"fs ! i - (fs ! i - gso i)  orthogonal_complement (span (gso ` {0..< i}))"
    unfolding eq orthogonal_complement_def using assms by auto
  note pe= oc_projection_exist[OF assms(1)]
  note prerec = carr_span f_carrier[OF assms(1)] assms(4) oc1 oc_projection_exist[OF assms(1)] oc2
  note prerec = carr_span f_carrier[OF assms(1)] assms(4) oc1 oc_projection_exist[OF assms(1)] oc2
  have gsoi: "gso i  carrier_vec n" "fs ! i  carrier_vec n"
    by (rule gso_carrier[OF i < m], rule f_carrier[OF i < m])
  note main = arg_cong[OF oc_projection_alt_def[OF carr_span f_carrier[OF assms(1)] assms(4) oc1 pe oc2], 
     of "λ v. - v $ j + fs ! i $ j" for j]
  show "v = gso i" 
  proof (intro eq_vecI)
    fix j
    show "j < dim_vec (gso i)  v $ j = gso i $ j" 
      using assms gsoi main[of j] by (auto)
  qed (insert assms gsoi, auto)
qed

lemma gso_oc_projection:
  assumes "i < m"
  shows "gso i = oc_projection (gso ` {0..<i}) (fs ! i)"
  unfolding oc_projection_def is_oc_projection_def
proof (rule some_equality[symmetric,OF _ oc_projection_unique[OF assms]])
  have orthogonal:" xa. xa < i  gso i  gso xa = 0" by (rule orthogonal,insert assms, auto)
  show "gso i  carrier_vec n 
        fs ! i - gso i  span (gso ` {0..<i}) 
        (x. x  gso ` {0..<i}  gso i  x = 0)"
    using gso_carrier oc_projection_exist assms orthogonal by auto
qed auto

lemma gso_oc_projection_span:
  assumes "i < m"
  shows "gso i = oc_projection (span (gso ` {0..<i})) (fs ! i)"
    and "is_oc_projection (gso i) (span (gso ` {0..<i})) (fs ! i)"
  unfolding oc_projection_def is_oc_projection_def
proof (rule some_equality[symmetric,OF _ oc_projection_unique[OF assms]])
  let ?P = "λv. v  carrier_vec n  fs ! i - v  span (span (gso ` {0..<i}))
     (x. x  span (gso ` {0..<i})  v  x = 0)"
  have carr:"gso ` {0..<i}  carrier_vec n" using assms by auto
  have *:  " xa. xa < i  gso i  gso xa = 0" by (rule orthogonal,insert assms, auto)
  have orthogonal:"x. x  span (gso ` {0..<i})  gso i  x = 0"
    apply(rule orthocompl_span) using assms * by auto
  show "?P (gso i)" "?P (gso i)" unfolding span_span[OF carr]
    using gso_carrier oc_projection_exist assms orthogonal by auto
  fix v assume p:"?P v"
  then show "v  carrier_vec n" by auto
  from p show "fs ! i - v  span (gso ` {0..<i})" unfolding span_span[OF carr] by auto
  fix xa assume "xa  gso ` {0..<i}"
  hence "xa  span (gso ` {0..<i})" using in_own_span[OF carr] by auto
  thus "v  xa = 0" using p by auto
qed

lemma gso_is_oc_projection:
  assumes "i < m"
  shows "is_oc_projection (gso i) (set (take i fs)) (fs ! i)"
proof -
  have [simp]: "v  carrier_vec n" if "v  set (take i fs)" for v
    using that by (meson contra_subsetD fs_carrier in_set_takeD)
  have "span (gso ` {0..<i}) = span (set (take i fs))"
    by (rule partial_span) (auto simp add: assms less_or_eq_imp_le)
  moreover have "is_oc_projection (gso i) (span (gso ` {0..<i})) (fs ! i)"
    by (rule gso_oc_projection_span) (auto simp add: assms less_or_eq_imp_le)
  ultimately have "is_oc_projection (gso i) (span (set (take i fs))) (fs ! i)"
    by auto
  moreover have "set (take i fs)  span (set (take i fs))"
    by (auto intro!: span_mem)
  ultimately show ?thesis
    unfolding is_oc_projection_def by (subst (asm) span_span) (auto)
qed

lemma fi_scalar_prod_gso:
  assumes i: "i < m" and j: "j < m" 
  shows "fs ! i  gso j = μ i j * gso j2" 
proof -
  let ?mu = "λj. μ i j v gso j" 
  from i have list1: "[0..< m] = [0..< Suc i] @ [Suc i ..< m]" 
    by (intro nth_equalityI, auto simp: nth_append, rename_tac j, case_tac "j - i", auto)
  from j have list2: "[0..< m] = [0..< j] @ [j] @ [Suc j ..< m]" 
    by (intro nth_equalityI, auto simp: nth_append, rename_tac k, case_tac "k - j", auto)
  have "fs ! i  gso j = sumlist (map ?mu [0..<Suc i])  gso j" 
    unfolding fi_is_sum_of_mu_gso[OF i] by simp
  also have " = (vmap ?mu [0..<Suc i]. v  gso j) + 0" 
    by (subst scalar_prod_left_sum_distrib, insert gso_carrier assms, auto)
  also have " = (vmap ?mu [0..<Suc i]. v  gso j) + (vmap ?mu [Suc i..<m]. v  gso j)" 
    by (subst (3) sum_list_neutral, insert assms gso_carrier, auto intro!: orthogonal simp: μ.simps)
  also have " = (vmap ?mu [0..< m]. v  gso j)" 
    unfolding list1 by simp
  also have " = (vmap ?mu [0..< j]. v  gso j) + ?mu j  gso j + (vmap ?mu [Suc j..< m]. v  gso j)" 
    unfolding list2 by simp
  also have "(vmap ?mu [0..< j]. v  gso j) = 0" 
    by (rule sum_list_neutral, insert assms gso_carrier, auto intro!: orthogonal)
  also have "(vmap ?mu [Suc j..< m]. v  gso j) = 0" 
    by (rule sum_list_neutral, insert assms gso_carrier, auto intro!: orthogonal)
  also have "?mu j  gso j = μ i j * sq_norm (gso j)" 
    using gso_carrier[OF j] by (simp add: sq_norm_vec_as_cscalar_prod)  
  finally show ?thesis by simp
qed

lemma gso_scalar_zero:
  assumes "k < m" "i < k"
  shows "(gso k)  (fs ! i) = 0"
  by (subst comm_scalar_prod[OF gso_carrier]; (subst fi_scalar_prod_gso)?,
  insert assms, auto simp: μ.simps)

lemma scalar_prod_lincomb_gso:
  assumes k: "k  m"
  shows "sumlist (map (λ i. g i v gso i) [0 ..< k])  sumlist (map (λ i. h i v gso i) [0 ..< k])
    = sum_list (map (λ i. g i * h i * (gso i  gso i)) [0 ..< k])" 
proof -
  have id1: "map (λi. g i v map (gso) [0..<m] ! i) [0..<k] = map (λi. g i v gso i) [0..<k]" for g using k
    by auto
  have id2: "(i[0..<k]. g i * h i * (map (gso) [0..<m] ! i  map (gso) [0..<m] ! i)) 
    = (i[0..<k]. g i * h i * (gso i  gso i))" using k
    by (intro arg_cong[OF map_cong], auto)
  define gs where "gs = map (gso) [0..<m]"
  have gs_gso: "gs ! i = gso i" if "i < k" for i
    using that assms unfolding gs_def by auto
  have "M.sumlist (map (λi. g i v gs ! i) [0..<k])  M.sumlist (map (λi. h i v gs ! i) [0..<k]) = 
        (i[0..<k]. g i * h i * (gs ! i  gs ! i))"
    unfolding gs_def using  assms  orthogonal_gso 
    by (intro scalar_prod_lincomb_orthogonal) auto
  also have "map (λi. g i v gs ! i) [0..<k] = map (λi. g i v gso i) [0..<k]"
    using gs_gso by (intro map_cong) (auto)
  also have "map (λi. h i v gs ! i) [0..<k] = map (λi. h i v gso i) [0..<k]"
    using gs_gso by (intro map_cong) (auto)
  also have "map (λi. g i * h i * (gs ! i  gs ! i)) [0..<k] = map (λi. g i * h i * (gso i  gso i)) [0..<k]"
    using gs_gso by (intro map_cong) (auto)
  finally show ?thesis by simp
qed

lemma gso_times_self_is_norm:
  assumes "j < m"
  shows "fs ! j  gso j = sq_norm (gso j)"
  by (subst fi_scalar_prod_gso, insert assms, auto simp: μ.simps)

(* Lemma 16.7 *)
lemma gram_schmidt_short_vector: 
  assumes in_L: "h  lattice_of fs - {0v n}" 
  shows " i < m. h2  gso i2"
proof -
  from in_L have non_0: "h  0v n" by auto
  from in_L[unfolded lattice_of_def] obtain lam where 
    h: "h =  sumlist (map (λ i. of_int (lam i) v fs ! i) [0 ..< length fs])" 
    by auto
  have in_L: "h = sumlist (map (λ i. of_int (lam i) v fs ! i) [0 ..< m])" unfolding length_map h
    by (rule arg_cong[of _ _ sumlist], rule map_cong, auto)
  let ?n = "[0 ..< m]" 
  let ?f = "(λ i. of_int (lam i) v fs ! i)" 
  let ?vs = "map ?f ?n" 
  let ?P = "λ k. k < m  lam k  0" 
  define k where "k = (GREATEST kk. ?P kk)" 
  { 
    assume *: " i < m. lam i = 0" 
    have vs: "?vs = map (λ i. 0v n) ?n"
      by (rule map_cong, insert f_dim *, auto)
    have "h = 0v n" unfolding in_L vs
      by (rule sumlist_neutral, auto)
    with non_0 have False by auto
  }  
  then obtain kk where "?P kk" by auto
  from GreatestI_nat[of ?P, OF this, of m] have Pk: "?P k" unfolding k_def by auto      
  hence kn: "k < m" by auto
  let ?gso = "(λi j. μ i j v gso j)" 
  have k: "k < i  i < m  lam i = 0" for i
    using Greatest_le_nat[of ?P i m, folded k_def] by auto
  define l where "l = lam k" 
  from Pk have l: "l  0" unfolding l_def by auto
  define idx where "idx = [0 ..< k]" 
  have idx: " i. i  set idx  i < k" " i. i  set idx  i < m"  unfolding idx_def using kn by auto
  from Pk have split: "[0 ..< m] = idx @ [k] @ [Suc k ..< m]" unfolding idx_def
    by (metis append_Cons append_self_conv2 less_Suc_eq_le less_imp_add_positive upt_add_eq_append 
        upt_rec zero_less_Suc)  
  define gg where "gg = sumlist 
    (map (λi. of_int (lam i) v fs ! i) idx) + of_int l v sumlist (map (λj. μ k j v gso j) idx)" 
  have "h = sumlist ?vs" unfolding in_L ..
  also have " = sumlist ((map ?f idx @ [?f k]) @ map ?f [Suc k ..< m])" unfolding split by auto
  also have " = sumlist (map ?f idx @ [?f k]) + sumlist (map ?f [Suc k ..< m])" 
    by (rule sumlist_append, auto intro!: f_carrier, insert Pk idx, auto)
  also have "sumlist (map ?f [Suc k ..< m]) = 0v n" by (rule sumlist_neutral, auto simp: k)
  also have "sumlist (map ?f idx @ [?f k]) = sumlist (map ?f idx) + ?f k" 
    by (subst sumlist_append, auto intro!: f_carrier, insert Pk idx, auto)
  also have "fs ! k = sumlist (map (?gso k) [0..<Suc k])" using fi_is_sum_of_mu_gso[OF kn] by simp
  also have " = sumlist (map (?gso k) idx @ [gso k])" by (simp add: μ.simps[of k k] idx_def)
  also have " = sumlist (map (?gso k) idx) + gso k" 
    by (subst sumlist_append, auto intro!: f_carrier, insert Pk idx, auto)
  also have "of_int (lam k) v  = of_int (lam k) v (sumlist (map (?gso k) idx)) 
    + of_int (lam k) v gso k" 
    unfolding idx_def
    by (rule smult_add_distrib_vec[OF sumlist_carrier], auto intro!: gso_carrier, insert kn, auto)
  finally have "h = sumlist (map ?f idx) +
       (of_int (lam k) v sumlist (map (?gso k) idx) + of_int (lam k) v gso k) + 0v n " by simp 
  also have " = gg + of_int l v gso k" unfolding gg_def l_def
    by (rule eq_vecI, insert idx kn, auto simp: sumlist_vec_index,
      subst index_add_vec, auto simp: sumlist_dim kn, subst sumlist_dim, auto)
  finally have hgg: "h = gg + of_int l v gso k" .      
  let ?k = "[0 ..< k]" 
  define R where "R = {gg.  nu. gg = sumlist (map (λ i. nu i v gso i) idx)}" 
  {
    fix nu
    have "dim_vec (sumlist (map (λ i. nu i v gso i) idx)) = n" 
      by (rule sumlist_dim, insert kn, auto simp: idx_def)
  } note dim_nu[simp] = this
  define kk where "kk = ?k" 
  {
    fix v
    assume "v  R"
    then obtain nu where v: "v = sumlist (map (λ i. nu i v gso i) idx)" unfolding R_def by auto
    have "dim_vec v = n" unfolding gg_def v by simp
  } note dim_R = this
  {
    fix v1 v2
    assume "v1  R" "v2  R" 
    then obtain nu1 nu2 where v1: "v1 = sumlist (map (λ i. nu1 i v gso i) idx)" and
      v2: "v2 = sumlist (map (λ i. nu2 i v gso i) idx)"
      unfolding R_def by auto
    have "v1 + v2  R" unfolding R_def
      by (standard, rule exI[of _ "λ i. nu1 i + nu2 i"], unfold v1 v2, rule eq_vecI, 
        (subst sumlist_vec_index, insert idx, auto intro!: gso_carrier simp: o_def)+, 
        unfold sum_list_addf[symmetric], induct idx, auto simp: algebra_simps)
  } note add_R = this
  have "gg  R" unfolding gg_def
  proof (rule add_R)
    show "of_int l v sumlist (map (λj. μ k j v gso j) idx)  R" 
      unfolding R_def
      by (standard, rule exI[of _ "λi. of_int l * μ k i"], rule eq_vecI,
       (subst sumlist_vec_index, insert idx, auto intro!: gso_carrier simp: o_def)+, 
       induct idx, auto simp: algebra_simps)
    show "sumlist (map ?f idx)  R" using idx
    proof (induct idx)
      case Nil
      show ?case by (simp add: R_def, intro exI[of _ "λ i. 0"], rule eq_vecI,
        (subst sumlist_vec_index, insert idx, auto intro!: gso_carrier simp: o_def)+, 
        induct idx, auto)
    next      
      case (Cons i idxs)
      have "sumlist (map ?f (i # idxs)) = sumlist ([?f i] @ map ?f idxs)" by simp
      also have " = ?f i + sumlist (map ?f idxs)" 
        by (subst sumlist_append, insert Cons(3), auto intro!: f_carrier)
      finally have id: "sumlist (map ?f (i # idxs)) = ?f i + sumlist (map ?f idxs)" .
      show ?case unfolding id
      proof (rule add_R[OF _ Cons(1)[OF Cons(2-3)]])
        from Cons(2-3) have i: "i < m" "i < k" by auto
        hence idx_split: "idx = [0 ..< Suc i] @ [Suc i ..< k]" unfolding idx_def 
          by (metis Suc_lessI append_Nil2 less_imp_add_positive upt_add_eq_append upt_rec zero_le)
        {
          fix j
          assume j: "j < n" 
          define idxs where "idxs = [0 ..< Suc i]"
          let ?f = "λ x. ((if x < Suc i then of_int (lam i) * μ i x else 0) v gso x) $ j" 
          have "(xidx. ?f x) = (x[0 ..< Suc i]. ?f x) + (x [Suc i ..< k]. ?f x)" 
            unfolding idx_split by auto
          also have "(x [Suc i ..< k]. ?f x) = 0" by (rule sum_list_neutral, insert j kn, auto)          
          also have "(x[0 ..< Suc i]. ?f x) = (xidxs. of_int (lam i) * (μ i x v gso x) $ j)" 
            unfolding idxs_def by (rule arg_cong[of _ _ sum_list], rule map_cong[OF refl], 
                subst index_smult_vec, insert j i kn, auto)
          also have " = of_int (lam i) * ((x[0..<Suc i]. (μ i x v gso x) $ j))" 
            unfolding idxs_def[symmetric] by (induct idxs, auto simp: algebra_simps)
          finally have "(xidx. ?f x) = of_int (lam i) * ((x[0..<Suc i]. (μ i x v gso x) $ j))" 
            by simp
        } note main = this
        show "?f i  R" unfolding fi_is_sum_of_mu_gso[OF i(1)] R_def
          apply (standard, rule exI[of _ "λ j. if j < Suc i then of_int (lam i) * μ i j else 0"], rule eq_vecI)
           apply (subst sumlist_vec_index, insert idx i, auto intro!: gso_carrier sumlist_dim simp: o_def)
          apply (subst index_smult_vec, subst sumlist_dim, auto) 
          apply (subst sumlist_vec_index, auto, insert idx i main, auto simp: o_def)
        done
      qed auto
    qed
  qed
  then obtain nu where gg: "gg = sumlist (map (λ i. nu i v gso i) idx)" unfolding R_def by auto
  let ?ff = "sumlist (map (λi. nu i v gso i) idx) + of_int l v gso k" 
  define hh where "hh = (λ i. (if i < k then nu i else of_int l))" 
  let ?hh = "sumlist (map (λ i. hh i v gso i) [0 ..< Suc k])" 
  have ffhh: "?hh = sumlist (map (λ i. hh i v gso i) [0 ..< k] @ [hh k v gso k])" 
    by simp
  also have " = sumlist (map (λ i. hh i v gso i) [0 ..< k]) + sumlist [hh k v gso k]" 
    by (rule sumlist_append, insert kn, auto)
  also have "sumlist [hh k v gso k] = hh k v gso k" using kn by auto
  also have " = of_int l v gso k" unfolding hh_def by auto
  also have "map (λ i. hh i v gso i) [0 ..< k] = map (λ i. nu i v gso i) [0 ..< k]" 
    by (rule map_cong, auto simp: hh_def)
  finally have ffhh: "?ff = ?hh" by (simp add: idx_def)
  from hgg[unfolded gg] 
  have h: "h = ?ff" by auto
  have "gso k  gso k  1 * (gso k  gso k)" by simp
  also have "  of_int (l * l) * (gso k  gso k)" 
  proof (rule mult_right_mono)
    from l have "l * l  1" by (meson eq_iff int_one_le_iff_zero_less mult_le_0_iff not_le)
    thus "1  (of_int (l * l) :: 'a)" by presburger     
    show "0  gso k  gso k" by (rule scalar_prod_ge_0)
  qed
  also have " = 0 + of_int (l * l) * (gso k  gso k)" by simp
  also have "  sum_list (map (λ i. (nu i * nu i) * (gso i  gso i)) idx) + of_int (l * l) * (gso k  gso k)" 
    by (rule add_right_mono, rule sum_list_nonneg, auto, rule mult_nonneg_nonneg, auto simp: scalar_prod_ge_0)
  also have "map (λ i. (nu i * nu i) * (gso i  gso i)) idx = map (λ i. hh i * hh i * (gso i  gso i)) [0..<k]" 
    unfolding idx_def by (rule map_cong, auto simp: hh_def) 
  also have "of_int (l * l) = hh k * hh k" unfolding hh_def by auto
  also have "(i[0..<k]. hh i * hh i * (gso i  gso i)) + hh k * hh k * (gso k  gso k)
     = (i[0..<Suc k]. hh i * hh i * (gso i  gso i))" by simp
  also have " = ?hh  ?hh" by (rule sym, rule scalar_prod_lincomb_gso, insert kn assms, auto)
  also have " = ?ff  ?ff" by (simp add: ffhh)
  also have " = h  h" unfolding h ..
  finally show ?thesis using kn unfolding sq_norm_vec_as_cscalar_prod by auto
qed

   
(* Theorem 16.9 
  (bound in textbook looks better as it uses 2^((n-1)/2), but this difference
  is caused by the fact that we here we look at the squared norms) *)
lemma weakly_reduced_imp_short_vector: 
  assumes "weakly_reduced α m"
    and in_L: "h  lattice_of fs - {0v n}" and α_pos:"α  1"
  shows "fs  []  sq_norm (fs ! 0)  α^(m-1) * sq_norm h"
proof -
  from gram_schmidt_short_vector assms obtain i where 
    i: "i < m" and le: "sq_norm (gso i)  sq_norm h" by auto
  have small: "sq_norm (fs ! 0)  α^i * sq_norm (gso i)" using i
  proof (induct i)
    case 0
    show ?case unfolding fs0_gso0[OF 0] by auto
  next
    case (Suc i)
    hence "sq_norm (fs ! 0)  α^i * sq_norm (gso i)" by auto
    also have "  α^i * (α * (sq_norm (gso (Suc i))))" 
      using reduced_gso_E[OF assms(1) le_refl Suc(2)] α_pos by auto
    finally show ?case unfolding class_semiring.nat_pow_Suc[of α i] by auto
  qed
  also have "  α^(m-1) * sq_norm h" 
    by (rule mult_mono[OF power_increasing le], insert i α_pos, auto)
  finally show ?thesis using i by (cases fs, auto)
qed


lemma sq_norm_pos: 
  assumes j: "j < m" 
  shows "sq_norm (gso j) > 0"
proof -
  from j have jj: "j < m - 0" by simp
  from orthogonalD[OF orthogonal_gso, unfolded length_map length_upt, OF jj jj] assms
  have "sq_norm (gso j)  0" using j by (simp add: sq_norm_vec_as_cscalar_prod)    
  moreover have "sq_norm (gso j)  0" by auto
  ultimately show "0 < sq_norm (gso j)" by auto
qed

lemma Gramian_determinant: 
  assumes k: "k  m" 
  shows "Gramian_determinant fs k = ( j<k. sq_norm (gso j))"
    "Gramian_determinant fs k > 0" 
proof -
  define Gk where "Gk = mat k n (λ (i,j). fs ! i $ j)" 
  have Gk: "Gk  carrier_mat k n" unfolding Gk_def by auto
  define Mk where "Mk = mat k k (λ (i,j). μ i j)" 
  have Mk_μ: "i < k  j < k  Mk $$ (i,j) = μ i j" for i j
    unfolding Mk_def using k by auto
  have Mk: "Mk  carrier_mat k k" and [simp]: "dim_row Mk = k" "dim_col Mk = k" unfolding Mk_def by auto
  have "det Mk = prod_list (diag_mat Mk)" 
    by (rule det_lower_triangular[OF _ Mk], auto simp: Mk_μ μ.simps)
  also have " = 1" 
    by (rule prod_list_neutral, auto simp: diag_mat_def Mk_μ μ.simps)
  finally have detMk: "det Mk = 1" .
  define Gsk where "Gsk = mat k n (λ (i,j). gso i $ j)" 
  have Gsk: "Gsk  carrier_mat k n" unfolding Gsk_def by auto
  have Gsk': "GskT  carrier_mat n k" using Gsk by auto
  let ?Rn = "carrier_vec n" 
  have id: "Gk = Mk * Gsk" 
  proof (rule eq_matI)
    from Gk Mk Gsk 
    have dim: "dim_row Gk = k" "dim_row (Mk * Gsk) = k" "dim_col Gk = n" "dim_col (Mk * Gsk) = n" by auto
    from dim show "dim_row Gk = dim_row (Mk * Gsk)" "dim_col Gk = dim_col (Mk * Gsk)" by auto
    fix i j
    assume "i < dim_row (Mk * Gsk)" "j < dim_col (Mk * Gsk)"     
    hence ij: "i < k" "j < n" and i: "i < m" using dim k by auto    
    have Gi: "fs ! i  ?Rn" using i by simp
    have "Gk $$ (i, j) = fs ! i $ j" unfolding Gk_def using ij k Gi by auto
    also have "... = FF $$ (i,j)" using ij i by simp
    also have "FF = (M m) * Fs" by (rule matrix_equality)
    also have " $$ (i,j) = row (M m) i  col Fs j" 
      by (rule index_mult_mat(1), insert i ij, auto simp: mat_of_rows_list_def)
    also have "row (M m) i = vec m (λ j. if j < k then Mk $$ (i,j) else 0)" 
      (is "_ = vec m ?Mk") 
      unfolding Mk_def using ij i
      by (auto simp: mat_of_rows_list_def μ.simps)
    also have "col Fs j = vec m (λ i'. if i' < k then Gsk $$ (i',j) else (Fs $$ (i',j)))" 
      (is "_ = vec m ?Gsk") 
      unfolding Gsk_def using ij i by (auto simp: mat_of_rows_def)
    also have "vec m ?Mk  vec m ?Gsk = ( i  {0 ..< m}. ?Mk i * ?Gsk i)" 
      unfolding scalar_prod_def by auto
    also have " = ( i  {0 ..< k}  {k ..< m}. ?Mk i * ?Gsk i)"
      by (rule sum.cong, insert k, auto)
    also have " = ( i  {0 ..< k}. ?Mk i * ?Gsk i) + ( i  {k ..< m}. ?Mk i * ?Gsk i)" 
      by (rule sum.union_disjoint, auto)
    also have "( i  {k ..< m}. ?Mk i * ?Gsk i) = 0" 
      by (rule sum.neutral, auto)
    also have "( i  {0 ..< k}. ?Mk i * ?Gsk i) = ( i'  {0 ..< k}. Mk $$ (i,i') * Gsk $$ (i',j))"
      by (rule sum.cong, auto)
    also have " = row Mk i  col Gsk j" unfolding scalar_prod_def using ij 
      by (auto simp: Gsk_def Mk_def)
    also have " = (Mk * Gsk) $$ (i, j)" using ij Mk Gsk by simp
    finally show "Gk $$ (i, j) = (Mk * Gsk) $$ (i, j)" by simp
  qed
  have cong: " a b c d. a = b  c = d  a * c = b * d" by auto
  have "Gramian_determinant fs k = det (Gk * GkT)" 
    unfolding Gramian_determinant_def Gramian_matrix_def Let_def
    by (rule arg_cong[of _ _ det], rule cong, insert k, auto simp: Gk_def) 
  also have "GkT = GskT * MkT" (is "_ = ?TGsk * ?TMk") unfolding id 
    by (rule transpose_mult[OF Mk Gsk])
  also have "Gk = Mk * Gsk" by fact
  also have " * (?TGsk * ?TMk) = Mk * (Gsk * (?TGsk * ?TMk))" 
    by (rule assoc_mult_mat[OF Mk Gsk, of _ k], insert Gsk Mk, auto)
  also have "det  = det Mk * det (Gsk * (?TGsk * ?TMk))" 
    by (rule det_mult[OF Mk], insert Gsk Mk, auto)
  also have " = det (Gsk * (?TGsk * ?TMk))" using detMk by simp
  also have "Gsk * (?TGsk * ?TMk) = (Gsk * ?TGsk) * ?TMk" 
    by (rule assoc_mult_mat[symmetric, OF Gsk], insert Gsk Mk, auto)
  also have "det  = det (Gsk * ?TGsk) * det ?TMk" 
    by (rule det_mult, insert Gsk Mk, auto)
  also have " = det (Gsk * ?TGsk)" using detMk det_transpose[OF Mk] by simp
  also have "Gsk * ?TGsk = mat k k (λ (i,j). if i = j then sq_norm (gso j) else 0)" (is "_ = ?M")
  proof (rule eq_matI)
    show "dim_row (Gsk * ?TGsk) = dim_row ?M" unfolding Gsk_def by auto
    show "dim_col (Gsk * ?TGsk) = dim_col ?M" unfolding Gsk_def by auto
    fix i j
    assume "i < dim_row ?M" "j < dim_col ?M" 
    hence ij: "i < k" "j < k" and ijn: "i < m" "j < m" using k by auto
    {
      fix i
      assume "i < k" 
      hence "i < m" using k by auto
      hence Gs: "gso i  ?Rn" by auto
      have "row Gsk i = gso i" unfolding row_def Gsk_def
        by (rule eq_vecI, insert Gs i < k, auto)
    } note row = this
    have "(Gsk * ?TGsk) $$ (i,j) = row Gsk i  row Gsk j" using ij Gsk by auto
    also have " = gso i  gso j" using row ij by simp
    also have " = (if i = j then sq_norm (gso j) else 0)" 
    proof (cases "i = j")
      assume "i = j" 
      thus ?thesis by (simp add: sq_norm_vec_as_cscalar_prod) 
    next
      assume "i  j" 
      from i  j orthogonalD[OF orthogonal_gso] ijn assms
      show ?thesis by auto
    qed
    also have " = ?M $$ (i,j)" using ij by simp
    finally show "(Gsk * ?TGsk) $$ (i,j) = ?M $$ (i,j)" .
  qed
  also have "det ?M = prod_list (diag_mat ?M)" 
    by (rule det_upper_triangular, auto)
  also have "diag_mat ?M = map (λ j. sq_norm (gso j)) [0 ..< k]" unfolding diag_mat_def by auto
  also have "prod_list  = ( j < k. sq_norm (gso j))"
    by (subst prod.distinct_set_conv_list[symmetric], force, rule prod.cong, auto) 
  finally show "Gramian_determinant fs k = (j<k. gso j2)" .
  also have " > 0" 
    by (rule prod_pos, intro ballI sq_norm_pos, insert k assms, auto)
  finally show "0 < Gramian_determinant fs k" by auto
qed

lemma Gramian_determinant_div:
  assumes "l < m"
  shows "Gramian_determinant fs (Suc l) / Gramian_determinant fs l = gso l2"
proof -
  note gram = Gramian_determinant(1)[symmetric]
  from assms have le: "Suc l  m" "l  m" by auto
  have "(j<Suc l. gso j2) = (j  {0..<l}  {l}. gso j2)"
    using assms by (intro prod.cong) (auto)
  also have " = (j<l. gso j2) * gso l2"
    using assms by (subst prod_Un) (auto simp add: atLeast0LessThan)
  finally show ?thesis unfolding gram[OF le(1)] gram[OF le(2)]
    using Gramian_determinant(2)[OF le(2)] assms by auto 
qed

end

lemma (in gram_schmidt_fs_Rn) Gramian_determinant_Ints:
  assumes "k  m" "i j. i < n  j < m  fs ! j $ i  "
  shows "Gramian_determinant fs k  "
proof -
  let ?oi = "of_int :: int  'a" 
  from assms have " i. i < n  j.  c. j < m  fs ! j $ i = ?oi c" unfolding Ints_def by auto
  from choice[OF this] have " i.  c.  j. i < n  j < m  fs ! j $ i = ?oi (c j)" by blast
  from choice[OF this] obtain c where c: " i j. i < n  j < m  fs ! j $ i = ?oi (c i j)" by blast
  define d where "d = map (λ j. vec n (λ i. c i j)) [0..<m]" 
  have fs: "fs = map (map_vec ?oi) d" 
    unfolding d_def by (rule nth_equalityI, auto intro!: eq_vecI c)
  have id: "mat k n (λ(i, y). map (map_vec ?oi) d ! i $ y) = map_mat of_int (mat k n (λ(i, y). d ! i $ y))" 
    by (rule eq_matI, insert k  m, auto simp: d_def o_def)
  show ?thesis unfolding fs Gramian_determinant_def Gramian_matrix_def Let_def id
    map_mat_transpose
    by (subst of_int_hom.mat_hom_mult[symmetric], auto)
qed

locale gram_schmidt_fs_int = gram_schmidt_fs_lin_indpt +
  assumes fs_int: "i j. i < n  j < m  fs ! j $ i  "
begin

lemma Gramian_determinant_ge1:
  assumes "k  m"
  shows "1  Gramian_determinant fs k"
proof -
  have "0 < Gramian_determinant fs k"
    by (simp add: assms Gramian_determinant(2) less_or_eq_imp_le)
  moreover have "Gramian_determinant fs k  "
    by (simp add: Gramian_determinant_Ints assms fs_int)
  ultimately show ?thesis
    using Ints_nonzero_abs_ge1 by fastforce
qed

lemma mu_bound_Gramian_determinant:
  assumes "l < k" "k < m"
  shows "(μ k l)2  Gramian_determinant fs l * fs ! k2"
proof -
  have "(μ k l)2  = (fs ! k  gso l)2 / (gso l2)2"
    using assms by (simp add: power_divide μ.simps)
  also have "  (fs ! k2 * gso l2) / (gso l2)2"
    using assms by (auto intro!: scalar_prod_Cauchy divide_right_mono)
  also have " = fs ! k2 / gso l2"
    by (auto simp add: field_simps power2_eq_square)
  also have " =  fs ! k2 / (Gramian_determinant fs (Suc l) / Gramian_determinant fs l)"
    using assms by (subst Gramian_determinant_div[symmetric]) auto
  also have " =  Gramian_determinant fs l * fs ! k2 / Gramian_determinant fs (Suc l)"
    by (auto simp add: field_simps)
  also have "  Gramian_determinant fs l * fs ! k2 / 1"
    by (rule divide_left_mono, insert Gramian_determinant_ge1[of l] Gramian_determinant_ge1[of "Suc l"] assms,
    auto intro!: mult_nonneg_nonneg) 
  finally show ?thesis
    by simp
qed

end (* gram_schmidt_fs_int *)

context gram_schmidt
begin

lemma gso_cong:
  fixes f1 f2 :: "'a vec list"
  assumes " i. i  x  f1 ! i = f2 ! i"
  shows "gram_schmidt_fs.gso n f1 x = gram_schmidt_fs.gso n f2 x"
  using assms
proof(induct x rule:nat_less_induct[rule_format])
  case (1 x)
  interpret f1: gram_schmidt_fs n f1 .
  interpret f2: gram_schmidt_fs n f2 .
  have *: "map (λj. - f1.μ x j v f1.gso j) [0..<x] = map (λj. - f2.μ x j v f2.gso j) [0..<x]"
    using 1 by (intro map_cong) (auto simp add: f1.μ.simps f2.μ.simps)
  show ?case
    using 1 by (subst f1.gso.simps, subst f2.gso.simps, subst *) auto
qed

lemma μ_cong:
  fixes f1 f2 :: "'a vec list"
  assumes " k. j < i  k  j  f1 ! k = f2 ! k"
    and "j < i  f1 ! i = f2 ! i" 
  shows "gram_schmidt_fs.μ n f1 i j = gram_schmidt_fs.μ n f2 i j"
proof -
  interpret f1: gram_schmidt_fs n f1 .
  interpret f2: gram_schmidt_fs n f2 .
  from gso_cong[of j f1 f2] assms have id: "j < i  f1.gso j = f2.gso j" by auto
  show ?thesis unfolding f1.μ.simps f2.μ.simps using assms id by auto
qed

end

lemma prod_list_le_mono: fixes us :: "'a :: {linordered_nonzero_semiring,ordered_ring} list" 
  assumes "length us = length vs" 
  and " i. i < length vs  0  us ! i  us ! i  vs ! i" 
shows "0  prod_list us  prod_list us  prod_list vs" 
  using assms 
proof (induction us vs rule: list_induct2)
  case (Cons u us v vs)
  have "0  prod_list us  prod_list us  prod_list vs" 
    by (rule Cons.IH, insert Cons.prems[of "Suc i" for i], auto)
  moreover have "0  u  u  v" using Cons.prems[of 0] by auto
  ultimately show ?case by (auto intro: mult_mono)
qed simp

lemma lattice_of_of_int: assumes G: "set F  carrier_vec n" 
  and "f  vec_module.lattice_of n F"     
shows "map_vec rat_of_int f  vec_module.lattice_of n (map (map_vec of_int) F)" 
  (is "?f  vec_module.lattice_of _ ?F")
proof -
  let ?sl = "abelian_monoid.sumlist (module_vec TYPE('a::semiring_1) n)" 
  note d = vec_module.lattice_of_def
  note dim = vec_module.sumlist_dim
  note sumlist_vec_index = vec_module.sumlist_vec_index
  from G have Gi: " i. i < length F  F ! i  carrier_vec n" by auto
  from Gi have Gid: " i. i < length F  dim_vec (F ! i) = n" by auto
  from assms(2)[unfolded d]
  obtain c where 
    ffc: "f = ?sl (map (λi. of_int (c i) v F ! i) [0..<length F])" (is "_ = ?g") by auto   
  have "?f = ?sl (map (λi. of_int (c i) v ?F ! i) [0..<length ?F])" (is "_ = ?gg")
  proof -
    have d1[simp]: "dim_vec ?g = n" by (subst dim, auto simp: Gi)
    have d2[simp]: "dim_vec ?gg = n" unfolding length_map by (subst vec_module.sumlist_dim, auto simp: Gi G)
    show ?thesis
      unfolding ffc length_map
      apply (rule eq_vecI)
       apply (insert d1 d2, auto)[2]
      apply (subst (1 2) sumlist_vec_index, auto simp: o_def Gi G)
      apply (unfold of_int_hom.hom_sum_list)
      apply (intro arg_cong[of _ _ sum_list] map_cong)
        by (auto simp: G Gi, (subst index_smult_vec, simp add: Gid)+,
         subst index_map_vec, auto simp: Gid)
  qed
  thus "?f  vec_module.lattice_of n ?F" unfolding d by auto
qed


(* Theorem 16.6, difficult part *)
lemma Hadamard's_inequality: 
  fixes A::"real mat"
  assumes A: "A  carrier_mat n n" 
  shows  "abs (det A)  sqrt (prod_list (map sq_norm (rows A)))" 
proof -
  let ?us = "map (row A) [0 ..< n]"
  interpret gso: gram_schmidt_fs n ?us .
  have len: "length ?us = n" by simp
  have us: "set ?us  carrier_vec n" using A by auto
  let ?vs = "map gso.gso [0..<n]" 
  show ?thesis
  proof (cases "carrier_vec n  gso.span (set ?us)")
    case True
    with us len have basis: "gso.basis_list ?us" unfolding gso.basis_list_def by auto
    note in_dep = gso.basis_list_imp_lin_indpt_list[OF basis]
    interpret gso: gram_schmidt_fs_lin_indpt n ?us
      by (standard) (use in_dep gso.lin_indpt_list_def in auto)
    have last: "0  prod_list (map sq_norm ?vs)  prod_list (map sq_norm ?vs)  prod_list (map sq_norm ?us)" 
    proof (rule prod_list_le_mono, force, unfold length_map length_upt)
      fix i
      assume "i < n - 0" 
      hence i: "i < n" by simp
      have vsi: "map sq_norm ?vs ! i = sq_norm (?vs ! i)" using i by simp
      have usi: "map sq_norm ?us ! i = sq_norm (row A i)" using i by simp
      have zero: "0  sq_norm (?vs ! i)" by auto
      have le: "sq_norm (?vs ! i)  sq_norm (row A i)"
        using gso.sq_norm_gso_le_f i by simp
      show "0  map sq_norm ?vs ! i  map sq_norm ?vs ! i  map sq_norm ?us ! i" 
        unfolding vsi usi using zero le by auto
    qed
    have Fs: "gso.FF  carrier_mat n n" by auto
    have A_Fs: "A = gso.FF" 
      by (rule eq_matI, subst gso.FF_index, insert A, auto)
    hence "abs (det A) = abs (det (gso.FF))" by simp
    (* the following three steps are based on a discussion with Bertram Felgenhauer *)
    also have " = abs (sqrt (det (gso.FF) * det (gso.FF)))" by simp
    also have "det (gso.FF) * det (gso.FF) = det (gso.FF) * det (gso.FF)T" 
      unfolding det_transpose[OF Fs] ..
    also have " = det (gso.FF * (gso.FF)T)" 
      by (subst det_mult[OF Fs], insert Fs, auto)
    also have " = gso.Gramian_determinant ?us n" 
      unfolding gso.Gramian_matrix_def gso.Gramian_determinant_def Let_def A_Fs[symmetric]
      by (rule arg_cong[of _ _ det], rule arg_cong2[of _ _ _ _ "(*)"], insert A, auto)
    also have " = (j  set [0 ..< n]. ?vs ! j2)"
      by (subst gso.Gramian_determinant) (auto intro!: prod.cong)
    also have " = prod_list (map (λ i. sq_norm (?vs ! i)) [0 ..< n])"
      by (subst prod.distinct_set_conv_list, auto)
    also have "map (λ i. sq_norm (?vs ! i)) [0 ..< n] = map sq_norm ?vs" 
      by (intro nth_equalityI, auto)
    also have "abs (sqrt (prod_list ))  sqrt (prod_list (map sq_norm ?us))" 
      using last by simp
    also have "?us = rows A" unfolding rows_def using A by simp
    finally show ?thesis .
  next
    case False
    from mat_of_rows_rows[unfolded rows_def,of A] A gram_schmidt.non_span_det_zero[OF len False us]
    have zero: "det A = 0" by auto
    have ge: "prod_list (map sq_norm (rows A))  0" 
      by (rule prod_list_nonneg, auto simp: sq_norm_vec_ge_0)
    show ?thesis unfolding zero using ge by simp
  qed
qed


definition "gram_schmidt_wit = gram_schmidt.main" 

declare gram_schmidt.adjuster_wit.simps[code]
declare gram_schmidt.sub2_wit.simps[code]
declare gram_schmidt.main_def[code]
      
definition gram_schmidt_int :: "nat  int vec list  rat list list × rat vec list" where
  "gram_schmidt_int n us = gram_schmidt_wit n (map (map_vec of_int) us)" 

lemma snd_gram_schmidt_int : "snd (gram_schmidt_int n us) = gram_schmidt n (map (map_vec of_int) us)"
  unfolding gram_schmidt_int_def gram_schmidt_wit_def gram_schmidt_fs.gso_connect by metis

text ‹Faster implementation for rational vectors which also avoid recomputations
  of square-norms›

fun adjuster_triv :: "nat  rat vec  (rat vec × rat) list  rat vec"
  where "adjuster_triv n w [] = 0v n"
    |  "adjuster_triv n w ((u,nu)#us) = -(w  u)/ nu v u + adjuster_triv n w us"

fun gram_schmidt_sub_triv
  where "gram_schmidt_sub_triv n us [] = us"
  | "gram_schmidt_sub_triv n us (w # ws) = (let u = adjuster_triv n w us + w in
     gram_schmidt_sub_triv n ((u, sq_norm_vec_rat u) # us) ws)"

definition gram_schmidt_triv :: "nat  rat vec list  (rat vec × rat) list"
  where "gram_schmidt_triv n ws = rev (gram_schmidt_sub_triv n [] ws)"

lemma adjuster_triv: "adjuster_triv n w (map (λ x. (x,sq_norm x)) us) = adjuster n w us" 
  by (induct us, auto simp: sq_norm_vec_as_cscalar_prod) 

lemma gram_schmidt_sub_triv: "gram_schmidt_sub_triv n ((map (λ x. (x,sq_norm x)) us)) ws = 
  map (λ x. (x, sq_norm x)) (gram_schmidt_sub n us ws)" 
  by (rule sym, induct ws arbitrary: us, auto simp: adjuster_triv o_def Let_def)

lemma gram_schmidt_triv[simp]: "gram_schmidt_triv n ws = map (λ x. (x,sq_norm x)) (gram_schmidt n ws)" 
  unfolding gram_schmidt_def gram_schmidt_triv_def rev_map[symmetric] 
  by (auto simp: gram_schmidt_sub_triv[symmetric])

context gram_schmidt
begin

fun mus_adjuster :: "'a vec  ('a vec × 'a) list  'a list  'a vec  'a list × 'a vec"
  where
  "mus_adjuster f []           mus g' = (mus, g')" |
  "mus_adjuster f ((g, ng)#n_gs) mus g' = (let a = (f  g) / ng in
                                             mus_adjuster f n_gs (a # mus) (-a v g + g'))"

fun norms_mus' where
  "norms_mus' []       n_gs mus = (map snd n_gs, mus)" |
  "norms_mus' (f # fs) n_gs mus =
    (let (mus_row, g') = mus_adjuster f n_gs [] (0v n);
                     g = g' + f in
      norms_mus' fs ((g, sq_norm_vec g) # n_gs) (mus_row#mus))"

lemma adjuster_wit_carrier_vec:
  assumes "f  carrier_vec n" "set gs  carrier_vec n"
  shows "snd (adjuster_wit mus f gs)  carrier_vec n"
  using assms
  by (induction mus f gs rule: adjuster_wit.induct) (auto simp add: Let_def case_prod_beta')

lemma adjuster_wit'':
  assumes "adjuster_wit mus_acc f gs = (mus, g')" "n_gs = map (λx. (x, sq_norm_vec x)) gs"
 "f  carrier_vec n" "acc  carrier_vec n" "set gs  carrier_vec n"
  shows "mus_adjuster f n_gs mus_acc acc = (mus, acc + g')"
  using assms proof(induction f n_gs mus_acc acc arbitrary: g' gs mus rule: mus_adjuster.induct)
  case (1 mus' f acc g)
  then show ?case
    by auto
next
  case (2 f g n_g n_gs mus_acc acc g' gs mus)
  let ?gg = "snd (adjuster_wit (f  g / n_g # mus_acc) f (tl gs))"
  from 2 have l: "gs = g # tl gs"
    by auto
  have gg: "?gg  carrier_vec n"
    using 2 by (auto intro!: adjuster_wit_carrier_vec)
  then have [simp]: "g' = (- (f  g / g2) v g + ?gg)"
    using 2 by (auto simp add: Let_def case_prod_beta')
  have "mus_adjuster f ((g, n_g) # n_gs) mus_acc acc =
        mus_adjuster f n_gs (f  g / n_g # mus_acc) (- (f  g / n_g) v g + acc)"
    by (auto simp add: Let_def)
  also have " = (mus, - (f  g / n_g) v g + acc + ?gg)"
  proof -
    have "adjuster_wit (f  g / n_g # mus_acc) f (tl gs) = (mus, ?gg)"
      using 2 by (subst (asm) l) (auto simp add: Let_def case_prod_beta')
    then show ?thesis
      using 2 by (subst 2(1)[of _ "tl gs"]) (auto simp add: Let_def case_prod_beta')
  qed
  finally show ?case
    using 2 gg by auto
qed

lemma adjuster_wit':
  assumes "n_gs = map (λx. (x, sq_norm_vec x)) gs" "f  carrier_vec n" "set gs  carrier_vec n"
  shows "mus_adjuster f n_gs mus_acc (0v n) = adjuster_wit mus_acc f gs"
proof -
  let ?g = "snd (adjuster_wit mus_acc f gs)"
  let ?mus = "fst (adjuster_wit mus_acc f gs)"
  have "?g  carrier_vec n"
    using assms by (auto intro!: adjuster_wit_carrier_vec)
  then show ?thesis
    using assms by (subst adjuster_wit''[of _ _ gs ?mus ?g]) (auto simp add: case_prod_beta')
qed

lemma sub2_wit_norms_mus':
  assumes "n_gs' = map (λv. (v, sq_norm_vec v)) gs'"
   "sub2_wit gs' fs = (mus, gs)" "set fs  carrier_vec n" "set gs'  carrier_vec n"
 shows "norms_mus' fs n_gs' mus_acc = (map sq_norm_vec (rev gs @ gs'), rev mus @ mus_acc)"
  using assms proof (induction fs n_gs' mus_acc arbitrary: gs' mus gs rule: norms_mus'.induct)
  case (1 n_gs mus_acc)
  then show ?case by (auto simp add: rev_map)
next
  case (2  f fs n_gs mus_acc)
  note aw1 = conjunct1[OF conjunct2[OF gram_schmidt_fs.adjuster_wit]]
  let ?aw = "mus_adjuster f n_gs [] (0v n)"
  have aw: "?aw = adjuster_wit [] f gs'"
    apply(subst adjuster_wit') using 2 by auto
  have "sub2_wit ((snd ?aw + f) # gs') fs = sub2_wit ((snd (adjuster_wit [] f gs') + f) # gs') fs"
    apply(subst adjuster_wit') using 2 by auto
  also have " = (tl mus, tl gs)"
    using 2 by (auto simp add: Let_def case_prod_beta')
  finally have sub_tl: "sub2_wit ((snd ?aw + f) # gs') fs = (tl mus, tl gs)"
    by simp
  have aw_c: "snd ?aw  carrier_vec n"
    apply(subst adjuster_wit'[of _ gs'])
     using 2 adjuster_wit_carrier_vec by (auto)
  have gs: "gs = (snd ?aw + f) # tl gs"
    apply(subst aw) using 2 by (auto simp add: Let_def case_prod_beta')
  have mus: "mus = fst ?aw # tl mus"
    apply(subst aw) using 2 by (auto simp add: Let_def case_prod_beta')
  show ?case apply(simp add: Let_def case_prod_beta')
    apply(subst 2(1)[of _ _ _ _ "(snd ?aw + f)#gs'"  "tl mus" "tl gs"]) apply(simp) defer apply(simp)
         apply (simp add: "2.prems"(1))
    using sub_tl apply(simp)
    using 2 apply(simp)
    subgoal using 2 aw_c by (auto)
     defer
     apply(simp)
    apply(auto)
    using gs 
     apply(subst gs) apply(subst (2) gs)
     apply (metis list.simps(9) rev.simps(2) rev_map)
    using mus
    by (metis rev.simps(2))
qed

lemma sub2_wit_gram_schmidt_sub_triv'':
  assumes "sub2_wit [] fs = (mus, gs)" "set fs  carrier_vec n"
  shows "norms_mus' fs [] [] = (map sq_norm_vec (rev gs), rev mus)"
  using assms by (subst sub2_wit_norms_mus') (simp)+

definition norms_mus where
  "norms_mus fs = (let (n_gs, mus) = norms_mus' fs [] [] in (rev n_gs, rev mus))"

lemma sub2_wit_gram_schmidt_norm_mus:
  assumes "sub2_wit [] fs = (mus, gs)" "set fs  carrier_vec n"
  shows "norms_mus fs = (map sq_norm_vec gs, mus)"
  unfolding norms_mus_def using assms sub2_wit_gram_schmidt_sub_triv''
  by (auto simp add: Let_def case_prod_beta' rev_map)

lemma (in gram_schmidt_fs_Rn) norms_mus: assumes "set fs  carrier_vec n" "length fs  n"
  shows "norms_mus fs = (map (λj. gso j2) [0..<length fs], map (λi. map (μ i) [0..<i]) [0..<length fs])" 
proof -
  let ?s = "sub2_wit [] fs"
  have "gram_schmidt_sub2 n [] fs = snd ?s  snd ?s = map (gso) [0..<length fs]  fst ?s = map (λi. map (μ i) [0..<i]) [0..<length fs]"
    using assms by (intro sub2_wit) (auto simp add: map_nth)
  then have 1: "snd ?s = map (gso) [0..<length fs]" and 2: "fst ?s = map (λi. map (μ i) [0..<i]) [0..<length fs]" 
    by auto
  have s: "?s = (fst ?s, snd ?s)" by auto
  show ?thesis
    unfolding sub2_wit_gram_schmidt_norm_mus[OF s assms(1)]
    unfolding 1 2 o_def map_map by auto
qed

end

fun mus_adjuster_rat :: "rat vec  (rat vec × rat) list  rat list  rat vec  rat list × rat vec"
  where
  "mus_adjuster_rat f []           mus g' = (mus, g')" |
  "mus_adjuster_rat f ((g, ng)#n_gs) mus g' = (let a = (f  g) / ng in
                                             mus_adjuster_rat f n_gs (a # mus) (-a v g + g'))"

fun norms_mus_rat' where
  "norms_mus_rat' n []       n_gs mus = (map snd n_gs, mus)" |
  "norms_mus_rat' n (f # fs) n_gs mus =
    (let (mus_row, g') = mus_adjuster_rat f n_gs [] (0v n);
                     g = g' + f in
      norms_mus_rat' n fs ((g, sq_norm_vec g) # n_gs) (mus_row#mus))"

definition norms_mus_rat where
  "norms_mus_rat n fs = (let (n_gs, mus) = norms_mus_rat' n fs [] [] in (rev n_gs, rev mus))"

lemma norms_mus_rat_norms_mus:
  "norms_mus_rat n fs = gram_schmidt.norms_mus n fs"
proof -
  have "mus_adjuster_rat f n_gs mus_acc g_acc = gram_schmidt.mus_adjuster f n_gs mus_acc g_acc"
    for f n_gs mus_acc g_acc
    by(induction f n_gs mus_acc g_acc rule: mus_adjuster_rat.induct)
      (auto simp add: gram_schmidt.mus_adjuster.simps)
  then have "norms_mus_rat' n fs n_gs mus = gram_schmidt.norms_mus' n fs n_gs mus" for n fs n_gs mus
    by(induction n fs n_gs mus rule: norms_mus_rat'.induct)
      (auto simp add: gram_schmidt.norms_mus'.simps case_prod_beta')
  then show ?thesis
    unfolding norms_mus_rat_def gram_schmidt.norms_mus_def by auto
qed

lemma of_int_dvd:
  "b dvd a" if "of_int a / (of_int b :: 'a :: field_char_0)  " "b  0"
  using that by (cases rule: Ints_cases)
    (simp add: field_simps flip: of_int_mult)

lemma denom_dvd_ints:
  fixes i::int
  assumes "quotient_of r = (z, n)" "of_int i * r  "
  shows "n dvd i"
proof -
  have "rat_of_int i * (rat_of_int z / rat_of_int n)  "
    using assms quotient_of_div by blast
  then have "n dvd i * z"
    using quotient_of_denom_pos assms by (auto intro!: of_int_dvd)
  then show "n dvd i"
    using assms algebraic_semidom_class.coprime_commute 
      quotient_of_coprime coprime_dvd_mult_left_iff by blast
qed

lemma quotient_of_bounds: 
  assumes "quotient_of r = (n, d)" "rat_of_int i * r  " "0 < i" "¦r¦  b"
  shows "of_int ¦n¦  of_int i * b" "d  i" 
proof -
  show ni: "d  i"
    using assms denom_dvd_ints  by (intro zdvd_imp_le) blast+
  have "¦r¦ = ¦rat_of_int n / rat_of_int d¦"
    using assms quotient_of_div by blast
  also have " = rat_of_int ¦n¦ / rat_of_int d"
    using assms using quotient_of_denom_pos by force
  finally have "of_int ¦n¦ = rat_of_int d * ¦r¦"
    using assms by auto
  also have "  rat_of_int d * b"
    using assms quotient_of_denom_pos by auto
  also have "  rat_of_int i * b"
    using ni assms of_int_le_iff by (auto intro!: mult_right_mono)
  finally show "rat_of_int ¦n¦  rat_of_int i * b" 
    by simp
qed

context gram_schmidt_fs_Rn
begin

(* Lemma 16.17 *) 

lemma ex_κ:
  assumes "i < length fs" "l  i"
  shows "κ. sumlist (map (λj. - μ i j v gso j) [0 ..< l]) =
             sumlist (map (λj. κ j v fs ! j) [0 ..< l])" (is "κ. ?Prop l i κ")
  using assms 
proof (induction l arbitrary: i)
  case (Suc l)
  then obtain κi where κi_def: "?Prop l i κi"
    by force
  from Suc obtain κl where κl_def: "?Prop l l κl"
    by force
  have [simp]: "dim_vec (M.sumlist (map (λj. f j v fs ! j) [0..<y])) = n" if "y  Suc l" for f y
    using Suc that by (auto intro!: dim_sumlist)
  define κ where "κ = (λx. (if x < l then κi x - κl x * μ i l else  - μ i l))"
  let ?sum = "λi. sumlist (map (λj. - μ i j v gso j) [0..<l])"
  have "M.sumlist (map (λj. - μ i j v gso j) [0..<Suc l]) = 
        M.sumlist (map (λj. κi j v fs ! j) [0..<l]) + - μ i l v gso l"
    using Suc by (subst κi_def[symmetric], subst sumlist_snoc[symmetric]) (auto)
  also have "gso l = fs ! l + M.sumlist (map (λj. κl j v fs ! j) [0..<l])"
    by (subst gso.simps) (auto simp add: κl_def)
  also have "M.sumlist (map (λj. κi j v fs ! j) [0..<l]) +
             - μ i l v (fs ! l + M.sumlist (map (λj. κl j v fs ! j) [0..<l]))
             = M.sumlist (map (λj. κ j v fs ! j) [0..<Suc l])" (is "?lhs = ?rhs")
  proof -
    have "?lhs $ k = ?rhs $ k" if "k < n" for k
    proof -
      have "(M.sumlist (map (λj. κi j v fs ! j) [0..<l]) + 
                - μ i l v (fs ! l + M.sumlist (map (λj. κl j v fs ! j) [0..<l]))) $ k
          = (M.sumlist (map (λj. κi j v fs ! j) [0..<l]) $ k + 
                - μ i l * (fs ! l $ k + M.sumlist (map (λj. κl j v fs ! j) [0..<l]) $ k))"
        using that by auto
      also have " = (j = 0..<l. κi j * fs ! j $ k) 
                 + (- μ i l * (j = 0..<l. κl j * fs ! j $ k)) - μ i l * fs ! l $ k"
        using that Suc by (auto simp add: algebra_simps sumlist_nth)
      also have "- μ i l * (j = 0..<l. κl j * fs ! j $ k) 
               = (j = 0..<l. - μ i l * (κl j * fs ! j $ k))"
        using sum_distrib_left by blast
      also have "(j = 0..<l. κi j * fs ! j $ k) + (j = 0..<l. - μ i l * (κl j * fs ! j $ k)) =
               (x = 0..<l. (κi x - κl x * μ i l) * fs ! x $ k)"
        by (subst sum.distrib[symmetric]) (simp add: algebra_simps)
      also have " = (x = 0..<l. κ x * fs ! x $ k)"
        unfolding κ_def by (rule sum.cong) (auto)
      also have "(x = 0..<l. κ x * fs ! x $ k) - μ i l * fs ! l $ k =
                 (x = 0..<l. κ x * fs ! x $ k) + (x = l..<Suc l. κ x * fs ! x $ k)"
        unfolding κ_def by auto
      also have " = (x = 0..<Suc l. κ x * fs ! x $ k)"
        by (subst sum.union_disjoint[symmetric]) auto
      also have " = (x = 0..<Suc l. (κ x v fs ! x) $ k)"
        using that Suc by auto
      also have " = M.sumlist (map (λj. κ j v fs ! j) [0..<Suc l]) $ k"
        by (subst sumlist_nth, insert that Suc, auto simp: nth_append)
      finally show ?thesis by simp
    qed
    then show ?thesis
      using Suc by (auto simp add: dim_sumlist)
  qed
  finally show ?case by (intro exI[of _ κ]) simp
qed auto


definition κ_SOME_def:
  "κ = (SOME κ. i l. i < length fs  l  i 
        sumlist (map (λj. - μ i j v gso j) [0..<l]) =
        sumlist (map (λj. κ i l j v fs ! j) [0..<l]))"

lemma κ_def:
  assumes "i < length fs" "l  i"
  shows "sumlist (map (λj. - μ i j v gso j) [0..<l]) =
         sumlist (map (λj. κ i l j v fs ! j) [0..<l])"
proof -
  let ?P = "λ i l κ. (i < length fs  l  i 
                  sumlist (map (λj. - μ i j v gso j) [0..<l]) =
                  sumlist (map (λj. κ j v fs ! j) [0..<l]))" 
  from ex_κ have " i.  l. κ. ?P i l κ" by blast
  from choice[OF this] have "i. κ.  l. ?P i l (κ l)" by blast
  from choice[OF this] have "κ. i l. ?P i l (κ i l)" by blast
  from someI_ex[OF this] show ?thesis
    unfolding κ_SOME_def using assms by blast
qed

lemma (in gram_schmidt_fs_lin_indpt) 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 (* gram_schmidt_fs_Rn *)

lemma Ints_sum:
  assumes "a. a  A  f a  "
  shows "sum f A  "
  using assms by (induction A rule: infinite_finite_induct) auto

lemma Ints_prod:
  assumes "a. a  A  f a  "
  shows "prod f A  "
using assms by (induction A rule: infinite_finite_induct) auto

lemma Ints_scalar_prod: 
  "v  carrier_vec n  w  carrier_vec n
    ( i. i < n  v $ i  )  ( i. i < n  w $ i  )  v  w  " 
  unfolding scalar_prod_def by (intro Ints_sum Ints_mult, auto)

lemma Ints_det: assumes " i j. i < dim_row A  j < dim_col A 
   A $$ (i,j)  "
  shows "det A  " 
proof (cases "dim_row A = dim_col A")
  case True
  show ?thesis unfolding Determinant.det_def using True assms
    by (auto intro!: Ints_mult Ints_prod)
next
  case False
  show ?thesis unfolding Determinant.det_def using False by simp
qed


lemma (in gram_schmidt_fs_Rn) Gramian_matrix_alt_alt_def:
  assumes "k  m"
  shows "Gramian_matrix fs k = mat k k (λ(i,j). fs ! i  fs ! j)"
proof -
  have *: "vec n (($) (fs ! i)) = fs ! i" if "i < m" for i
    using that by auto
  then show ?thesis
    unfolding Gramian_matrix_def using assms
    by (intro eq_matI) (auto simp add: Let_def)
qed

lemma (in gram_schmidt_fs_int) fs_scalar_Ints:
  assumes "i < m" "j < m"
  shows "fs ! i  fs ! j  "
  by (rule Ints_scalar_prod[of _ n], insert fs_int assms, auto)

abbreviation (in gram_schmidt_fs_lin_indpt) d where "d  Gramian_determinant fs" 


lemma (in gram_schmidt_fs_lin_indpt) fs_i_fs_j_sum_κ :
  assumes "i < m" "l  i" "j < l"
  shows "- (fs ! i  fs ! j) = (t = 0..<l. fs ! t  fs ! j * κ i l t)"
proof -
  have [simp]: "M.sumlist (map (λj. κ i l j v fs ! j) [0..<l])  carrier_vec n"
    using assms by (auto intro!: sumlist_carrier simp add: dim_sumlist)
  have "0  = (fs ! i + M.sumlist (map (λj. κ i l j v fs ! j) [0..<l]))  fs ! j"
    using fs_i_sumlist_κ assms by simp
  also have " = fs ! i  fs ! j + M.sumlist (map (λj. κ i l j v fs ! j) [0..<l])  fs ! j"
    using assms by (subst add_scalar_prod_distrib[of _ n]) (auto)
  also have "M.sumlist (map (λj. κ i l j v fs ! j) [0..<l])  fs ! j =
             (vmap (λj. κ i l j v fs ! j) [0..<l]. v  fs ! j)"
    using assms by (intro scalar_prod_left_sum_distrib) (auto)
  also have " = (t[0..<l]. (κ i l t v fs ! t)  fs ! j)"
    by (rule arg_cong[where f=sum_list]) (auto)
  also have " =  (t = 0..<l. (κ i l t v fs ! t)  fs ! j) "
    by (subst interv_sum_list_conv_sum_set_nat) (auto)
  also have " = (t = 0..<l. fs ! t  fs ! j * κ i l t)"
    using assms by (intro sum.cong) auto
  finally show ?thesis by (simp add: field_simps)
qed

lemma (in gram_schmidt_fs_lin_indpt) Gramian_matrix_times_κ :
  assumes "i < m" "l  i"
  shows "Gramian_matrix fs l *v (vec l (λt. κ i l t)) = (vec l (λj. - (fs ! i  fs ! j)))"
proof -
  have "- (fs ! i  fs ! j) = (t = 0..<l. fs ! t  fs ! j * κ i l t)" if "j < l" for j
    using fs_i_fs_j_sum_κ assms that by simp
  then show ?thesis using assms
    by (subst Gramian_matrix_alt_alt_def) (auto simp add: scalar_prod_def algebra_simps)
qed

lemma (in gram_schmidt_fs_int) d_κ_Ints :
  assumes "i < m" "l  i" "t < l"
  shows "d l * κ i l t  "
proof -
  let ?A = "Gramian_matrix fs l"
  let ?B = "replace_col ?A (Gramian_matrix fs l *v vec l (κ i l)) t" 
  have deteq: "d l = det ?A"
    unfolding Gramian_determinant_def
    using Gramian_determinant_Ints
    by auto

  have **: "Gramian_matrix fs l  carrier_mat l l" unfolding Gramian_matrix_def Let_def  using fs_carrier by auto
      
  then have " κ i l t * det ?A = det ?B"
    using assms fs_carrier cramer_lemma_mat[of ?A l " (vec l (λt. κ i l t))" t]
    by auto

  also have " ...   "
  proof -
    have *: "t<l  (?A *v vec l (κ i l)) $ t  " for t
      using assms
      apply(subst Gramian_matrix_times_κ, force, force)
      using fs_int fs_carrier
      by (auto intro!: fs_scalar_Ints Ints_minus)

    define B where "B = ?B"

    have Bint: "t1<l  s1 < l  B $$ (t1,s1)  " for t1 s1
    proof (cases "s1 = t")
      case True
      from * ** this show ?thesis 
        unfolding replace_col_def B_def
        by auto
    next
      case False
      from * ** Gramian_matrix_def this fs_carrier assms show ?thesis
        unfolding replace_col_def B_def
        by (auto simp: Gramian_matrix_def Let_def scalar_prod_def intro!: Ints_sum Ints_mult fs_int)
    qed
    have B: "B  carrier_mat l l"
      using ** replace_col_def unfolding B_def
      by (auto simp: replace_col_def)
    have "det B  "
      using B Bint assms  det_col[of B l]
      by (auto intro!: Ints_sum Ints_mult Ints_prod)
    thus ?thesis unfolding B_def.
  qed
  finally show ?thesis using deteq by (auto simp add: algebra_simps)
qed

lemma (in gram_schmidt_fs_int) d_gso_Ints:
  assumes "i < n" "k < m"
  shows "(d k v (gso k)) $ i  "
proof -
  note d_κ_Ints[intro!]
  then have "(d k * κ k k j) * fs ! j $ i  " if "j < k" for j
    using that fs_int assms by (auto intro: Ints_mult )
  moreover have "(d k * κ k k j) * fs ! j $ i = d k * κ k k j * fs ! j $ i" for j
    by (auto simp add: field_simps)
  ultimately have "d k * (j = 0..<k. κ k k j * fs ! j $ i)  "
     by (subst sum_distrib_left) (auto simp add: field_simps intro!: Ints_sum)
  moreover have "(gso k) $ i = fs ! k $ i + sum (λj. (κ k k j v fs ! j) $ i) {0..<k}"
  proof -
    have " i < dim_vec (M.sumlist (map (λj. κ k k j v fs ! j) [0..<k]))"
      using assms by (subst sumlist_dim) auto
    then show ?thesis
      using assms by (subst gso.simps) (auto simp add: sumlist_nth sumlist_dim κ_def)
  qed
  ultimately show ?thesis
    using assms
    by (auto simp add: distrib_left Gramian_determinant_Ints fs_int intro!: Ints_mult Ints_add)
qed

lemma (in gram_schmidt_fs_int) d_mu_Ints:
  assumes "l  k" "k < m"
  shows "d (Suc l) * μ k l  "
proof (cases "l < k")
  case True
  have ll: "d l * gso l $ i = (d l v gso l) $ i" if "i < n" for i
    using that assms by auto
  have "d (Suc l) * μ k l =d (Suc l) * (fs ! k  gso l) / gso l2 "
    using assms True unfolding μ.simps by simp
  also have " = fs ! k  (d l v gso l)"
    using assms Gramian_determinant(2)[of "Suc l"]
    by (subst Gramian_determinant_div[symmetric]) (auto)
  also have "  "
  proof -
    have "d l * gso l $ i  " if "i < n" for i
      using assms d_gso_Ints that ll by (simp)
    then show ?thesis
      using assms by (auto intro!: Ints_sum simp add: fs_int scalar_prod_def)
 qed
 finally show ?thesis
   by simp
next
  case False
  with assms have l: "l = k" by auto
  show ?thesis unfolding l μ.simps using Gramian_determinant_Ints fs_int assms by simp
qed


lemma max_list_Max: "ls  []  max_list ls = Max (set ls)"
  by (induction ls) (auto simp add: max_list_Cons)

subsection ‹Explicit Bounds for Size of Numbers that Occur During GSO Algorithm ›

context gram_schmidt_fs_lin_indpt
begin

definition "N = Max (sq_norm ` set fs)"



lemma N_ge_0:
  assumes "0 < m"
  shows "0  N"
proof -
  have "x  sq_norm ` set fs  0  x" for x
    by auto
  then show ?thesis
  using assms unfolding N_def by auto
qed

lemma N_fs:
  assumes "i < m"
  shows "fs ! i2  N"
    using assms unfolding N_def by (auto)

lemma N_gso:
  assumes "i < m"
  shows "gso i2  N"
  using assms N_fs sq_norm_gso_le_f by fastforce

lemma N_d:
  assumes "i  m"
  shows "Gramian_determinant fs i  N ^ i"
proof -
  have "(j<i. gso j2)  (j<i. N)"
      using assms N_gso by (intro prod_mono) auto
    then show ?thesis
      using assms Gramian_determinant by auto
  qed


end

lemma ex_MAXIMUM: assumes "finite A" "A  {}"
  shows "a  A. Max (f ` A) = f a"
proof -
  have "Max (f ` A)  f ` A"
    using assms by (auto intro!: Max_in)
  then show ?thesis
    using assms imageE by blast
qed

context gram_schmidt_fs_int
begin

lemma fs_int': "k < n  f  set fs  f $ k  "
  by (metis fs_int in_set_conv_nth)

lemma
  assumes "i < m"
  shows fs_sq_norm_Ints: "fs ! i2  " and fs_sq_norm_ge_1: "1  fs ! i2"
proof -
  show fs_Ints: "fs ! i2  "
    using assms fs_int' carrier_vecD fs_carrier
    by (auto simp add: sq_norm_vec_as_cscalar_prod scalar_prod_def intro!: Ints_sum Ints_mult)
  have "fs ! i  0v n"
    using assms fs_carrier loc_assms nth_mem vs_zero_lin_dep by force
  then have *: "0  fs ! i2"
    using assms sq_norm_vec_eq_0 f_carrier by metis
  show "1  fs ! i2"
    by (rule Ints_cases[OF fs_Ints]) (use * sq_norm_vec_ge_0[of "fs ! i"] assms in auto)
qed

lemma
  assumes "set fs  {}"
  shows N_Ints: "N  " and N_1: "1  N"  
proof -
  have "vm  set fs. N = sq_norm vm"
    unfolding N_def using assms by (auto intro!: ex_MAXIMUM)
  then obtain vm::"'a vec" where vm_def: "vm  set fs" "N = sq_norm vm"
    by blast
  then show N_Ints: "N  "
    using fs_int' carrier_vecD fs_carrier
    by (auto simp add: sq_norm_vec_as_cscalar_prod scalar_prod_def intro!: Ints_sum Ints_mult)
  have *: "0  N"
    using N_gso sq_norm_pos assms by fastforce
  show "1  N"
    by (rule Ints_cases[OF N_Ints]) (use * N_ge_0 assms in force)+
qed

lemma N_mu:
  assumes "i < m" "j  i"
  shows "(μ i j)2  N ^ (Suc j)"
proof -
  { assume ji: "j < i"
    have "(μ i j)2  Gramian_determinant fs j * fs ! i2"
      using assms ji by (intro mu_bound_Gramian_determinant) auto
    also have "  N ^ j * fs ! i2"
      using assms N_d N_ge_0 by (intro mult_mono) fastforce+
    also have "N ^ j * fs ! i2  N ^ j * N"
      using assms N_fs N_ge_0 by (intro mult_mono) fastforce+
    also have " = N ^ (Suc j)"
      by auto
    finally have ?thesis
      by simp }
  moreover 
  { assume ji: "j = i"
    have "(μ i j)2 = 1"
      using ji by (simp add: μ.simps)
    also have "  N"
      using assms N_1 by fastforce
    also have "  N ^ (Suc j)"
      using assms N_1 by fastforce
    finally have ?thesis
      by simp }
  ultimately show ?thesis
    using assms by fastforce
qed

end


lemma vec_hom_Ints:
  assumes "i < n" "xs  carrier_vec n"
  shows "of_int_hom.vec_hom xs $ i  "
  using assms by auto

lemma division_to_div: "(of_int x  :: 'a :: floor_ceiling) = of_int y / of_int z  x = y div z" 
  by (metis floor_divide_of_int_eq floor_of_int)

lemma exact_division: assumes "of_int x / (of_int y  :: 'a :: floor_ceiling)  "
  shows "of_int (x div y) = of_int x / (of_int y :: 'a)" 
  using assms by (metis Ints_cases division_to_div)

lemma int_via_rat_eqI: "rat_of_int x = rat_of_int y  x = y" by auto

locale fs_int =
  fixes
    n :: nat (* n-dimensional vectors, *) and
    fs_init :: "int vec list" (* initial basis *)
begin

sublocale vec_module "TYPE(int)" n .

abbreviation RAT where "RAT  map (map_vec rat_of_int)" 
abbreviation (input) m where "m  length fs_init"

sublocale gs: gram_schmidt_fs n "RAT fs_init" .

definition d :: "int vec list  nat  int" where "d fs k = gs.Gramian_determinant fs k"
definition D :: "int vec list  nat" where "D fs = nat ( i < length fs. d fs i)" 

lemma of_int_Gramian_determinant:
  assumes "k  length F" "i. i < length F  dim_vec (F ! i) = n"
  shows "gs.Gramian_determinant (map of_int_hom.vec_hom F) k = of_int (gs.Gramian_determinant F k)"
  unfolding gs.Gramian_determinant_def of_int_hom.hom_det[symmetric]
proof (rule arg_cong[of _ _ det])
  let ?F = "map of_int_hom.vec_hom F"
  have cong: " a b c d. a = b  c = d  a * c = b * d" by auto
  show "gs.Gramian_matrix ?F k = map_mat of_int (gs.Gramian_matrix F k)" 
    unfolding gs.Gramian_matrix_def Let_def
  proof (subst of_int_hom.mat_hom_mult[of _ k n _ k], (auto)[2], rule cong)
    show id: "mat k n (λ (i,j). ?F ! i $ j) = map_mat of_int (mat k n (λ (i, j). F ! i $ j))" (is "?L = map_mat _ ?R")
    proof (rule eq_matI, goal_cases)
      case (1 i j)
      hence ij: "i < k" "j < n" "i < length F" "dim_vec (F ! i) = n" using assms by auto
      show ?case using ij by simp 
    qed auto
    show "?LT = map_mat of_int ?RT" unfolding id by (rule eq_matI, auto)
  qed
qed

end

locale fs_int_indpt = fs_int n fs for n fs +
  assumes lin_indep: "gs.lin_indpt_list (RAT fs)"
begin

sublocale gs: gram_schmidt_fs_lin_indpt n "RAT fs"
  by (standard) (use lin_indep gs.lin_indpt_list_def in auto)

sublocale gs: gram_schmidt_fs_int n "RAT fs"
  by (standard) (use gs.f_carrier lin_indep gs.lin_indpt_list_def in auto intro!: vec_hom_Ints)

lemma f_carrier[dest]: "i < m  fs ! i  carrier_vec n"
  and fs_carrier [simp]: "set fs  carrier_vec n"
  using lin_indep gs.f_carrier gs.gso_carrier unfolding gs.lin_indpt_list_def by auto

lemma Gramian_determinant:
  assumes k: "k  m" 
  shows "of_int (gs.Gramian_determinant fs k) = ( j<k. sq_norm (gs.gso j))" (is ?g1)
    "gs.Gramian_determinant fs k > 0" (is ?g2)
proof -
  have hom: "gs.Gramian_determinant (RAT fs) k = of_int (gs.Gramian_determinant fs k)"
    using k by (intro of_int_Gramian_determinant) auto
  show ?g1
    unfolding hom[symmetric] using gs.Gramian_determinant assms by auto
  show ?g2
    using hom gs.Gramian_determinant assms by fastforce
qed

lemma fs_int_d_pos [intro]:
  assumes k: "k  m" 
shows "d fs k > 0"
  unfolding d_def using Gramian_determinant[OF k] by auto

lemma fs_int_d_Suc:
  assumes k: "k < m" 
shows "of_int (d fs (Suc k)) = sq_norm (gs.gso k) * of_int (d fs k)" 
proof -
  from k have k: "k  m" "Suc k  m" by auto
  show ?thesis unfolding Gramian_determinant[OF k(1)] Gramian_determinant[OF k(2)] d_def
    by (subst prod.remove[of _ k], force+, rule arg_cong[of _ _ "λ x. _ * x"], rule prod.cong, auto)
qed

lemma fs_int_D_pos:
shows "D fs > 0"
proof -
  have "( j < m. d fs j) > 0"
    by (rule prod_pos, insert fs_int_d_pos, auto)
  thus ?thesis unfolding D_def by auto
qed

definition " i j = int_of_rat (of_int (d fs (Suc j)) * gs.μ i j)" 

lemma fs_int_mu_d_Z:
  assumes j: "j  ii" and ii: "ii < m" 
  shows "of_int (d fs (Suc j)) * gs.μ ii j  "
proof -
  have id: "of_int (d fs (Suc j)) = gs.Gramian_determinant (RAT fs) (Suc j)" 
    unfolding d_def
    by (rule of_int_Gramian_determinant[symmetric], insert j ii , auto)
  have "of_int_hom.vec_hom (fs ! j) $ i  " if "i < n" "j < length fs" for i j
     using that by (intro vec_hom_Ints) auto
  then show ?thesis
    unfolding id using j ii unfolding gs.lin_indpt_list_def 
    by (intro gs.d_mu_Ints) (auto)
qed

lemma fs_int_mu_d_Z_m_m:
  assumes j: "j < m" and ii: "ii < m" 
  shows "of_int (d fs (Suc j)) * gs.μ ii j  "
proof (cases "j  ii")
  case True
  thus ?thesis using fs_int_mu_d_Z[OF True ii] by auto
next
  case False thus ?thesis by (simp add: gs.μ.simps)
qed


lemma sq_norm_fs_via_sum_mu_gso: assumes i: "i < m" 
  shows "of_int fs ! i2 = (j[0..<Suc i]. (gs.μ i j)2 * gs.gso j2)" 
proof -
  let ?G = "map (gs.gso) [0 ..< m]" 
  let ?gso = "λ fs j. ?G ! j"
  have "of_int fs ! i2 = RAT fs ! i2" unfolding sq_norm_of_int[symmetric] using insert i by auto
  also have "RAT fs ! i = gs.sumlist (map (λj. gs.μ i j v gs.gso j) [0..<Suc i])" 
    using gs.fi_is_sum_of_mu_gso i by auto
  also have id: "map (λj. gs.μ i j v gs.gso j) [0..<Suc i] = map (λj. gs.μ i j v ?gso fs j) [0..<Suc i]" 
    by (rule nth_equalityI, insert i, auto simp: nth_append)
  also have "sq_norm (gs.sumlist ) = sum_list (map sq_norm (map (λj. gs.μ i j v gs.gso j) [0..<Suc i]))" 
    unfolding map_map o_def sq_norm_smult_vec
    unfolding sq_norm_vec_as_cscalar_prod cscalar_prod_is_scalar_prod conjugate_id
  proof (subst gs.scalar_prod_lincomb_orthogonal)
    show "Suc i  length ?G" using i by auto
    show "set ?G  carrier_vec n" using gs.gso_carrier by auto
    show "orthogonal ?G" using gs.orthogonal_gso by auto
  qed (rule arg_cong[of _ _ sum_list], intro nth_equalityI, insert i, auto simp: nth_append)
  also have "map sq_norm (map (λj. gs.μ i j v gs.gso j) [0..<Suc i]) = map (λj. (gs.μ i j)^2 * sq_norm (gs.gso j)) [0..<Suc i]" 
    unfolding map_map o_def sq_norm_smult_vec by (rule map_cong, auto simp: power2_eq_square)
  finally show ?thesis . 
qed

lemma : assumes "j < m" "ii < m" 
  shows "of_int ( ii j) = of_int (d fs (Suc j)) * gs.μ ii j" 
  unfolding dμ_def using fs_int_mu_d_Z_m_m assms by auto

end

end