Session LLL_Basis_Reduction

Theory Missing_Lemmas

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

section ‹Missing lemmas›

text ‹This theory contains many results that are important but not specific for our development. 
      They could be moved to the stardard library and some other AFP entries.› 

theory Missing_Lemmas
  imports
    Berlekamp_Zassenhaus.Sublist_Iteration (* for thm upt_append *)
    Berlekamp_Zassenhaus.Square_Free_Int_To_Square_Free_GFp (* for thm large_mod_0 *)
    Algebraic_Numbers.Resultant
    Jordan_Normal_Form.Conjugate
    Jordan_Normal_Form.Missing_VectorSpace
    Jordan_Normal_Form.VS_Connect
    Berlekamp_Zassenhaus.Finite_Field_Factorization_Record_Based (* for transfer rules for thm vec_of_list_Nil *)
    Berlekamp_Zassenhaus.Berlekamp_Hensel (* for unique_factorization_m_factor *)
begin

no_notation test_bit (infixl "!!" 100)

hide_const(open) module.smult up_ring.monom up_ring.coeff

(**** Could be merged to HOL/Rings.thy ****)

class ordered_semiring_1 = Rings.ordered_semiring_0 + monoid_mult + zero_less_one
begin

subclass semiring_1..

lemma of_nat_ge_zero[intro!]: "of_nat n  0"
  using add_right_mono[of _ _ 1] by (induct n, auto)

(* Following lemmas are moved from @{class ordered_idom}. *)
lemma zero_le_power [simp]: "0  a  0  a ^ n"
  by (induct n) simp_all

lemma power_mono: "a  b  0  a  a ^ n  b ^ n"
  by (induct n) (auto intro: mult_mono order_trans [of 0 a b])

lemma one_le_power [simp]: "1  a  1  a ^ n"
  using power_mono [of 1 a n] by simp

lemma power_le_one: "0  a  a  1  a ^ n  1"
  using power_mono [of a 1 n] by simp

lemma power_gt1_lemma:
  assumes gt1: "1 < a"
  shows "1 < a * a ^ n"
proof -
  from gt1 have "0  a"
    by (fact order_trans [OF zero_le_one less_imp_le])
  from gt1 have "1 * 1 < a * 1" by simp
  also from gt1 have "  a * a ^ n"
    by (simp only: mult_mono 0  a one_le_power order_less_imp_le zero_le_one order_refl)
  finally show ?thesis by simp
qed

lemma power_gt1: "1 < a  1 < a ^ Suc n"
  by (simp add: power_gt1_lemma)

lemma one_less_power [simp]: "1 < a  0 < n  1 < a ^ n"
  by (cases n) (simp_all add: power_gt1_lemma)

lemma power_decreasing: "n  N  0  a  a  1  a ^ N  a ^ n"
proof (induction N)
  case (Suc N)
  then have "a * a^N  1 * a^n" if "n  N"
    using that by (intro mult_mono) auto
  then show ?case
    using Suc by (auto simp add: le_Suc_eq)
qed (auto)

lemma power_increasing: "n  N  1  a  a ^ n  a ^ N"
proof (induction N)
  case (Suc N)
  then have "1 * a^n  a * a^N" if "n  N"
    using that by (intro mult_mono) (auto simp add: order_trans[OF zero_le_one])
  then show ?case
    using Suc by (auto simp add: le_Suc_eq)
qed (auto)

lemma power_Suc_le_self: "0  a  a  1  a ^ Suc n  a"
  using power_decreasing [of 1 "Suc n" a] by simp

end

lemma prod_list_nonneg: "( x. (x :: 'a :: ordered_semiring_1)  set xs  x  0)  prod_list xs  0"
  by (induct xs, auto)

subclass (in ordered_idom) ordered_semiring_1 by unfold_locales auto

(**** End of lemmas that could be moved to HOL/Rings.thy ****)

(* missing lemma on logarithms *)
lemma log_prod: assumes "0 < a" "a  1" " x. x  X  0 < f x" 
  shows "log a (prod f X) = sum (log a o f) X" 
  using assms(3)
proof (induct X rule: infinite_finite_induct)
  case (insert x F)
  have "log a (prod f (insert x F)) = log a (f x * prod f F)" using insert by simp
  also have " = log a (f x) + log a (prod f F)" 
    by (rule log_mult[OF assms(1-2) insert(4) prod_pos], insert insert, auto)
  finally show ?case using insert by auto
qed auto

(* TODO: Jordan_Normal_Form/Missing_Ring.ordered_idom should be redefined *)
subclass (in ordered_idom) zero_less_one by (unfold_locales, auto)
hide_fact Missing_Ring.zero_less_one

(**** The following lemmas could be part of the standard library ****)

instance real :: ordered_semiring_strict by (intro_classes, auto)
instance real :: linordered_idom..

(*This is a generalisation of thm less_1_mult*) 
lemma less_1_mult': 
  fixes a::"'a::linordered_semidom"
  shows "1 < a  1  b  1 < a * b"
  by (metis le_less less_1_mult mult.right_neutral)

lemma upt_minus_eq_append: "ij  ij-k  [i..<j] = [i..<j-k] @ [j-k..<j]"
proof (induct k)
  case (Suc k)
  have hyp: "[i..<j] = [i..<j - k] @ [j - k..<j]" using Suc.hyps Suc.prems by auto
  then show ?case
    by (metis Suc.prems(2) append.simps(1) diff_Suc_less nat_less_le neq0_conv upt_append upt_rec zero_diff)
qed auto

lemma list_trisect: "x < length lst  [0..<length lst] = [0..<x]@x#[Suc x..<length lst]"
  by (induct lst, force, rename_tac a lst, case_tac "x = length lst", auto)

lemma id_imp_bij_betw:
  assumes f: "f : A  A"
      and ff: "a. a  A  f (f a) = a"
  shows "bij_betw f A A"
  by (intro bij_betwI[OF f f], simp_all add: ff)

lemma range_subsetI:
  assumes "x. f x = g (h x)" shows "range f  range g"
  using assms by auto

lemma Gcd_uminus: 
  fixes A::"int set"
  assumes "finite A"
  shows "Gcd A = Gcd (uminus ` A)"
  using assms
  by (induct A, auto)

lemma aux_abs_int: fixes c :: int
  assumes "c  0" 
  shows "¦x¦  ¦x * c¦"
proof -
  have "abs x = abs x * 1" by simp
  also have "  abs x * abs c" 
    by (rule mult_left_mono, insert assms, auto)
  finally show ?thesis unfolding abs_mult by auto
qed

lemma mod_0_abs_less_imp_0:
  fixes a::int
  assumes a1: "[a = 0] (mod m)"
  and a2: "abs(a)<m"
  shows "a = 0"
proof -
  have "m0" using assms by auto
  thus ?thesis  
    using assms unfolding cong_def
    using int_mod_pos_eq large_mod_0 zless_imp_add1_zle 
      by (metis abs_of_nonneg le_less not_less zabs_less_one_iff zmod_trivial_iff)
qed

(* an intro version of sum_list_0 *)
lemma sum_list_zero:
  assumes "set xs  {0}" shows "sum_list xs = 0"
  using assms by (induct xs, auto)

(* About @{const max} *)
lemma max_idem [simp]: shows "max a a = a" by (simp add: max_def)

lemma hom_max:
  assumes "a  b  f a  f b"
  shows "f (max a b) = max (f a) (f b)" using assms by (auto simp: max_def)

lemma le_max_self:
  fixes a b :: "'a :: preorder"
  assumes "a  b  b  a" shows "a  max a b" and "b  max a b"
  using assms by (auto simp: max_def)

lemma le_max:
  fixes a b :: "'a :: preorder"
  assumes "c  a  c  b" and "a  b  b  a" shows "c  max a b"
  using assms(1) le_max_self[OF assms(2)] by (auto dest: order_trans)

fun max_list where
  "max_list [] = (THE x. False)" (* more convenient than "undefined" *)
| "max_list [x] = x"
| "max_list (x # y # xs) = max x (max_list (y # xs))"

declare max_list.simps(1) [simp del]
declare max_list.simps(2-3)[code]

lemma max_list_Cons: "max_list (x#xs) = (if xs = [] then x else max x (max_list xs))"
  by (cases xs, auto)

lemma max_list_mem: "xs  []  max_list xs  set xs"
  by (induct xs, auto simp: max_list_Cons max_def)

lemma mem_set_imp_le_max_list:
  fixes xs :: "'a :: preorder list"
  assumes "a b. a  set xs  b  set xs  a  b  b  a"
      and "a  set xs"
  shows "a  max_list xs"
proof (insert assms, induct xs arbitrary:a)
  case Nil
  with assms show ?case by auto
next
  case (Cons x xs)
  show ?case
  proof (cases "xs = []")
    case False
    have "x  max_list xs  max_list xs  x"
      apply (rule Cons(2)) using max_list_mem[of xs] False by auto
    note 1 = le_max_self[OF this]
    from Cons have "a = x  a  set xs" by auto
    then show ?thesis
    proof (elim disjE)
      assume a: "a = x"
      show ?thesis by (unfold a max_list_Cons, auto simp: False intro!: 1)
    next
      assume "a  set xs"
      then have "a  max_list xs" by (intro Cons, auto)
      with 1 have "a  max x (max_list xs)" by (auto dest: order_trans)
      then show ?thesis by (unfold max_list_Cons, auto simp: False)
    qed
  qed (insert Cons, auto)
qed

lemma le_max_list:
  fixes xs :: "'a :: preorder list"
  assumes ord: "a b. a  set xs  b  set xs  a  b  b  a"
      and ab: "a  b"
      and b: "b  set xs"
  shows "a  max_list xs"
proof-
  note ab
  also have "b  max_list xs"
    by (rule mem_set_imp_le_max_list, fact ord, fact b)
  finally show ?thesis.
qed

lemma max_list_le:
  fixes xs :: "'a :: preorder list"
  assumes a: "x. x  set xs  x  a"
      and xs: "xs  []"
  shows "max_list xs  a"
  using max_list_mem[OF xs] a by auto

lemma max_list_as_Greatest:
  assumes "x y. x  set xs  y  set xs  x  y  y  x"
  shows "max_list xs = (GREATEST a. a  set xs)"
proof (cases "xs = []")
  case True
  then show ?thesis by (unfold Greatest_def, auto simp: max_list.simps(1))
next
  case False
  from assms have 1: "x  set xs  x  max_list xs" for x
    by (auto intro: le_max_list)
  have 2: "max_list xs  set xs" by (fact max_list_mem[OF False])
  have "∃!x. x  set xs  (y. y  set xs  y  x)" (is "∃!x. ?P x")
  proof (intro ex1I)
    from 1 2
    show "?P (max_list xs)" by auto
  next
    fix x assume 3: "?P x"
    with 1 have "x  max_list xs" by auto
    moreover from 2 3 have "max_list xs  x" by auto
    ultimately show "x = max_list xs" by auto
  qed
  note 3 = theI_unique[OF this,symmetric]
  from 1 2 show ?thesis
    by (unfold Greatest_def Cons 3, auto)
qed

lemma hom_max_list_commute:
  assumes "xs  []"
      and "x y. x  set xs  y  set xs  h (max x y) = max (h x) (h y)"
  shows "h (max_list xs) = max_list (map h xs)"
  by (insert assms, induct xs, auto simp: max_list_Cons max_list_mem)


(*Efficient rev [i..<j]*)
primrec rev_upt :: "nat  nat  nat list" ("(1[_>.._])") where
rev_upt_0: "[0>..j] = []" |
rev_upt_Suc: "[(Suc i)>..j] = (if i  j then i # [i>..j] else [])"

lemma rev_upt_rec: "[i>..j] = (if i>j then [i>..Suc j] @ [j] else [])"
  by (induct i, auto)    

definition rev_upt_aux :: "nat  nat  nat list  nat list" where
  "rev_upt_aux i j js = [i>..j] @ js"

lemma upt_aux_rec [code]:
  "rev_upt_aux i j js = (if ji then js else rev_upt_aux i (Suc j) (j#js))"
  by (induct j, auto simp add: rev_upt_aux_def rev_upt_rec)

lemma rev_upt_code[code]: "[i>..j] = rev_upt_aux i j []"
  by(simp add: rev_upt_aux_def)    
  
lemma upt_rev_upt:
  "rev [j>..i] = [i..<j]"
  by (induct j, auto)
    
lemma rev_upt_upt:
  "rev [i..<j] = [j>..i]"
  by (induct j, auto) 

lemma length_rev_upt [simp]: "length [i>..j] = i - j"
  by (induct i) (auto simp add: Suc_diff_le)
    
lemma nth_rev_upt [simp]: "j + k < i  [i>..j] ! k = i - 1 - k"
proof -
  assume jk_i: "j + k < i"
  have "[i>..j] = rev [j..<i]" using rev_upt_upt by simp
  also have "... ! k = [j..<i] ! (length [j..<i] - 1 - k)"
    using jk_i by (simp add: rev_nth)
  also have "... = [j..<i] ! (i - j - 1 - k)" by auto
  also have "... = j + (i - j - 1 - k)" by (rule nth_upt, insert jk_i, auto)
  finally show ?thesis using jk_i by auto
qed    
  
lemma nth_map_rev_upt: 
  assumes i: "i < m-n"
  shows "(map f [m>..n]) ! i = f (m - 1 - i)"
proof -
  have "(map f [m>..n]) ! i = f ([m>..n] ! i)" by (rule nth_map, auto simp add: i)
  also have "... = f (m - 1 - i)"
  proof (rule arg_cong[of _ _ f], rule nth_rev_upt)
    show "n + i < m" using i by linarith
  qed
  finally show ?thesis .
qed

lemma coeff_mult_monom:
 "coeff (p * monom a d) i = (if d  i then a * coeff p (i - d) else 0)"
  using coeff_monom_mult[of a d p] by (simp add: ac_simps)

(**** End of the lemmas which may be part of the standard library ****)

(**** The following lemmas could be moved to Algebraic_Numbers/Resultant.thy ****)
lemma vec_of_poly_0 [simp]: "vec_of_poly 0 = 0v 1" by (auto simp: vec_of_poly_def)

lemma vec_index_vec_of_poly [simp]: "i  degree p  vec_of_poly p $ i = coeff p (degree p - i)"
  by (simp add: vec_of_poly_def Let_def)

lemma poly_of_vec_vec: "poly_of_vec (vec n f) = Poly (rev (map f [0..<n]))"
proof (induct n arbitrary:f)
  case 0
  then show ?case by auto
next
  case (Suc n)
  have "map f [0..<Suc n] = f 0 # map (f  Suc) [0..<n]" by (simp add: map_upt_Suc del: upt_Suc)
  also have "Poly (rev ) = Poly (rev (map (f  Suc) [0..<n])) + monom (f 0) n"
    by (simp add: Poly_snoc smult_monom)
  also have " = poly_of_vec (vec n (f  Suc)) + monom (f 0) n"
    by (fold Suc, simp)
  also have " = poly_of_vec (vec (Suc n) f)"
    apply (unfold poly_of_vec_def Let_def dim_vec sum.lessThan_Suc)
    by (auto simp add: Suc_diff_Suc)
  finally show ?case..
qed

lemma sum_list_map_dropWhile0:
  assumes f0: "f 0 = 0"
  shows "sum_list (map f (dropWhile ((=) 0) xs)) = sum_list (map f xs)"
  by (induct xs, auto simp add: f0)

lemma coeffs_poly_of_vec:
  "coeffs (poly_of_vec v) = rev (dropWhile ((=) 0) (list_of_vec v))"
proof-
  obtain n f where v: "v = vec n f" by transfer auto
  show ?thesis by (simp add: v poly_of_vec_vec)
qed

lemma poly_of_vec_vCons:
 "poly_of_vec (vCons a v) = monom a (dim_vec v) + poly_of_vec v" (is "?l = ?r")
  by (auto intro: poly_eqI simp: coeff_poly_of_vec vec_index_vCons)

lemma poly_of_vec_as_Poly: "poly_of_vec v = Poly (rev (list_of_vec v))"
  by (induct v, auto simp:poly_of_vec_vCons Poly_snoc ac_simps)

lemma poly_of_vec_add:
  assumes "dim_vec a = dim_vec b"
  shows "poly_of_vec (a + b) = poly_of_vec a + poly_of_vec b"
  using assms
  by (auto simp add: poly_eq_iff coeff_poly_of_vec)

(*TODO: replace the one in Resultant.thy*)
lemma degree_poly_of_vec_less:
  assumes "0 < dim_vec v" and "dim_vec v  n" shows "degree (poly_of_vec v) < n"
  using degree_poly_of_vec_less assms by (auto dest: less_le_trans)

lemma (in vec_module) poly_of_vec_finsum:
  assumes "f  X  carrier_vec n"
  shows "poly_of_vec (finsum V f X) = (iX. poly_of_vec (f i))"
proof (cases "finite X")
  case False then show ?thesis by auto
next
  case True show ?thesis
  proof (insert True assms, induct X rule: finite_induct)
    case IH: (insert a X)
    have [simp]: "f x  carrier_vec n" if x: "x  X" for x 
      using x IH.prems unfolding Pi_def by auto
    have [simp]: "f a  carrier_vec n" using IH.prems unfolding Pi_def by auto
    have [simp]: "dim_vec (finsum V f X) = n" by simp
    have [simp]: "dim_vec (f a) = n" by simp
    show ?case
    proof (cases "a  X")
      case True then show ?thesis by (auto simp: insert_absorb IH)
    next
      case False
      then have "(finsum V f (insert a X)) = f a + (finsum V f X)" 
        by (auto intro: finsum_insert IH)
      also have "poly_of_vec ... = poly_of_vec (f a) + poly_of_vec (finsum V f X)"
        by (rule poly_of_vec_add, simp)
      also have "... = (iinsert a X. poly_of_vec (f i))"
        using IH False by (subst sum.insert, auto)
      finally show ?thesis .
    qed
  qed auto
qed

(*This function transforms a polynomial to a vector of dimension n*)  
definition "vec_of_poly_n p n =
  vec n (λi. if i < n - degree p - 1 then 0 else coeff p (n - i - 1))"

(* TODO: make it abbreviation? *)
lemma vec_of_poly_as: "vec_of_poly_n p (Suc (degree p)) = vec_of_poly p"
  by (induct p, auto simp: vec_of_poly_def vec_of_poly_n_def)

lemma vec_of_poly_n_0 [simp]: "vec_of_poly_n p 0 = vNil"
  by (auto simp: vec_of_poly_n_def)

lemma vec_dim_vec_of_poly_n [simp]:
  "dim_vec (vec_of_poly_n p n) = n"
  "vec_of_poly_n p n  carrier_vec n"
  unfolding vec_of_poly_n_def by auto

lemma dim_vec_of_poly [simp]: "dim_vec (vec_of_poly f) = degree f + 1"
  by (simp add: vec_of_poly_as[symmetric])

lemma vec_index_of_poly_n:
  assumes "i < n"
  shows "vec_of_poly_n p n $ i =
    (if i < n - Suc (degree p) then 0 else coeff p (n - i - 1))"
  using assms by (auto simp: vec_of_poly_n_def Let_def)

lemma vec_of_poly_n_pCons[simp]:
  shows "vec_of_poly_n (pCons a p) (Suc n) = vec_of_poly_n p n @v vec_of_list [a]" (is "?l = ?r")
proof (unfold vec_eq_iff, intro conjI allI impI)
  show "dim_vec ?l = dim_vec ?r" by auto
  show "i < dim_vec ?r  ?l $ i = ?r $ i" for i
    by (cases "n - i", auto simp: coeff_pCons less_Suc_eq_le vec_index_of_poly_n)
qed

lemma vec_of_poly_pCons:
  shows "vec_of_poly (pCons a p) =
   (if p = 0 then vec_of_list [a] else vec_of_poly p @v vec_of_list [a])"
  by (cases "degree p", auto simp: vec_of_poly_as[symmetric])

lemma list_of_vec_of_poly [simp]:
  "list_of_vec (vec_of_poly p) = (if p = 0 then [0] else rev (coeffs p))"
  by (induct p, auto simp: vec_of_poly_pCons)

lemma poly_of_vec_of_poly_n:
  assumes p: "degree p<n"
  shows "poly_of_vec (vec_of_poly_n p n) = p"
proof - 
  have "vec_of_poly_n p n $ (n - Suc i) = coeff p i" if i: "i < n" for i    
  proof -
    have n: "n - Suc i < n" using i by auto
    have "vec_of_poly_n p n $ (n - Suc i) = 
      (if n - Suc i < n - Suc (degree p) then 0 else coeff p (n - (n - Suc i) - 1))"
      using vec_index_of_poly_n[OF n, of p] .
    also have "... = coeff p i" using i n le_degree by fastforce
    finally show ?thesis .
  qed
  moreover have "coeff p i = 0" if i2: "i  n" for i
    by (rule coeff_eq_0, insert i2 p, simp)
  ultimately show ?thesis
  using assms
  unfolding poly_eq_iff
  unfolding coeff_poly_of_vec by auto
qed

lemma vec_of_poly_n0[simp]: "vec_of_poly_n 0 n = 0v n" 
  unfolding vec_of_poly_n_def by auto

lemma vec_of_poly_n_add: "vec_of_poly_n (a + b) n = vec_of_poly_n a n + vec_of_poly_n b n"
proof (induct n arbitrary: a b)
  case 0
  then show ?case by auto
next
  case (Suc n)
  then show ?case by (cases a, cases b, auto)
qed

lemma vec_of_poly_n_poly_of_vec:
  assumes n: "dim_vec g = n"
  shows "vec_of_poly_n (poly_of_vec g) n = g"
proof (auto simp add: poly_of_vec_def vec_of_poly_n_def assms vec_eq_iff Let_def)
  have d: "degree (i<n. monom (g $ (n - Suc i)) i) = degree (poly_of_vec g)" 
    unfolding poly_of_vec_def Let_def n by auto
  fix i assume i1: "i < n - Suc (degree (i<n. monom (g $ (n - Suc i)) i))" 
    and i2: "i < n"
  have i3: "i < n - Suc (degree (poly_of_vec g))" 
    using i1 unfolding d by auto
  hence "dim_vec g - Suc i > degree (poly_of_vec g)"
    using n by linarith
  then show "g $ i = 0" using i1 i2 i3    
    by (metis (no_types, lifting) Suc_diff_Suc coeff_poly_of_vec diff_Suc_less 
        diff_diff_cancel leD le_degree less_imp_le_nat n neq0_conv)
next
  fix i assume "i < n"
  thus "coeff (i<n. monom (g $ (n - Suc i)) i) (n - Suc i) = g $ i"    
    by (metis (no_types) Suc_diff_Suc coeff_poly_of_vec diff_diff_cancel 
        diff_less_Suc less_imp_le_nat n not_less_eq poly_of_vec_def)
qed

lemma poly_of_vec_scalar_mult:
  assumes "degree b<n"
  shows "poly_of_vec (a v (vec_of_poly_n b n)) = smult a b"
  using assms
  by (auto simp add: poly_eq_iff coeff_poly_of_vec vec_of_poly_n_def coeff_eq_0)

(*TODO: replace the one in Resultant.thy*)
definition vec_of_poly_rev_shifted where
  "vec_of_poly_rev_shifted p n s j 
   vec n (λi. if i  j  j  s + i then coeff p (s + i - j) else 0)"

lemma vec_of_poly_rev_shifted_dim[simp]: "dim_vec (vec_of_poly_rev_shifted p n s j) = n"
  unfolding vec_of_poly_rev_shifted_def by auto

lemma col_sylvester_sub: (* TODO: from this directly derive col_sylvester *)
  assumes j: "j < m + n"
  shows "col (sylvester_mat_sub m n p q) j =
    vec_of_poly_rev_shifted p n m j @v vec_of_poly_rev_shifted q m n j" (is "?l = ?r")
proof
  show "dim_vec ?l = dim_vec ?r" by simp
  fix i assume "i < dim_vec ?r" then have i: "i < m+n" by auto
  show "?l $ i = ?r $ i"
    unfolding vec_of_poly_rev_shifted_def
    apply (subst index_col) using i apply simp using j apply simp
    apply (subst sylvester_mat_sub_index) using i apply simp using j apply simp
    apply (cases "i < n") using i apply force using i
    apply (auto simp: not_less not_le intro!: coeff_eq_0)
    done
qed

lemma vec_of_poly_rev_shifted_scalar_prod:
  fixes p v
  defines "q  poly_of_vec v"
  assumes m: "degree p  m" and n: "dim_vec v = n"
  assumes j: "j < m+n"
  shows "vec_of_poly_rev_shifted p n m (n+m-Suc j)  v = coeff (p * q) j" (is "?l = ?r")
proof -
  have id1: " i. m + i - (n + m - Suc j) = i + Suc j - n"
    using j by auto
  let ?g = "λ i. if i  n + m - Suc j  n - Suc j  i then coeff p (i + Suc j - n) *  v $ i else 0"
  have "?thesis = ((i = 0..<n. ?g i) =          
        (ij. coeff p i * (if j - i < n then v $ (n - Suc (j - i)) else 0)))" (is "_ = (?l = ?r)")
    unfolding vec_of_poly_rev_shifted_def coeff_mult m scalar_prod_def n q_def
      coeff_poly_of_vec 
    by (subst sum.cong, insert id1, auto)
  also have "..." 
  proof -
    have "?r = (ij. (if j - i < n then coeff p i * v $ (n - Suc (j - i)) else 0))" (is "_ = sum ?f _")
      by (rule sum.cong, auto)
    also have "sum ?f {..j} = sum ?f ({i. i  j  j - i < n}  {i. i  j  ¬ j - i < n})" 
      (is "_ = sum _ (?R1  ?R2)")
      by (rule sum.cong, auto)
    also have " = sum ?f ?R1 + sum ?f ?R2"
      by (subst sum.union_disjoint, auto)
    also have "sum ?f ?R2 = 0"
      by (rule sum.neutral, auto)
    also have "sum ?f ?R1 + 0 = sum (λ i. coeff p i * v $ (i + n - Suc j)) ?R1"
      (is "_ = sum ?F _")
      by (subst sum.cong, auto simp: ac_simps)
    also have " = sum ?F ((?R1  {..m})  (?R1 - {..m}))"
      (is "_ = sum _ (?R  ?R')")
      by (rule sum.cong, auto)
    also have " = sum ?F ?R + sum ?F ?R'"
      by (subst sum.union_disjoint, auto)
    also have "sum ?F ?R' = 0"
    proof -
      { 
        fix x
        assume "x > m" 
        with m
        have "?F x = 0" by (subst coeff_eq_0, auto)
      }
      thus ?thesis
        by (subst sum.neutral, auto)
    qed
    finally have r: "?r = sum ?F ?R" by simp

    have "?l = sum ?g ({i. i < n  i  n + m - Suc j  n - Suc j  i} 
       {i. i < n  ¬ (i  n + m - Suc j  n - Suc j  i)})" 
      (is "_ = sum _ (?L1  ?L2)")
      by (rule sum.cong, auto)
    also have " = sum ?g ?L1 + sum ?g ?L2"
      by (subst sum.union_disjoint, auto)
    also have "sum ?g ?L2 = 0"
      by (rule sum.neutral, auto)
    also have "sum ?g ?L1 + 0 = sum (λ i. coeff p (i + Suc j - n) * v $ i) ?L1"
      (is "_ = sum ?G _")
      by (subst sum.cong, auto)
    also have " = sum ?G (?L1  {i. i + Suc j - n  m}  (?L1 - {i. i + Suc j - n  m}))"
      (is "_ = sum _ (?L  ?L')")
      by (subst sum.cong, auto)
    also have " = sum ?G ?L + sum ?G ?L'"
      by (subst sum.union_disjoint, auto)
    also have "sum ?G ?L' = 0"
    proof -
      {
        fix x
        assume "x + Suc j - n > m" 
        with m
        have "?G x = 0" by (subst coeff_eq_0, auto)
      }
      thus ?thesis
        by (subst sum.neutral, auto)
    qed
    finally have l: "?l = sum ?G ?L" by simp

    let ?bij = "λ i. i + n - Suc j"
    {
      fix x
      assume x: "j < m + n" "Suc (x + j) - n  m" "x < n" "n - Suc j  x" 
      define y where "y = x + Suc j - n"
      from x have "x + Suc j  n" by auto
      with x have xy: "x = ?bij y" unfolding y_def by auto
      from x have y: "y  ?R" unfolding y_def by auto
      have "x  ?bij ` ?R" unfolding xy using y by blast
    } note tedious = this
    show ?thesis unfolding l r
      by (rule sum.reindex_cong[of ?bij], insert j, auto simp: inj_on_def tedious)
  qed
  finally show ?thesis by simp
qed

lemma sylvester_sub_poly:
  fixes p q :: "'a :: comm_semiring_0 poly"
  assumes m: "degree p  m"
  assumes n: "degree q  n"
  assumes v: "v  carrier_vec (m+n)"
  shows "poly_of_vec ((sylvester_mat_sub m n p q)T *v v) =
    poly_of_vec (vec_first v n) * p + poly_of_vec (vec_last v m) * q" (is "?l = ?r")
proof (rule poly_eqI)
  fix i
  let ?Tv = "(sylvester_mat_sub m n p q)T *v v"
  have dim: "dim_vec (vec_first v n) = n" "dim_vec (vec_last v m) = m" "dim_vec ?Tv = n + m" 
    using v by auto
  have if_distrib: " x y z. (if x then y else (0 :: 'a)) * z = (if x then y * z else 0)" 
    by auto
  show "coeff ?l i = coeff ?r i"
  proof (cases "i < m+n")
    case False
      hence i_mn: "i  m+n"
        and i_n: "x. x  i  x < n  x < n"
        and i_m: "x. x  i  x < m  x < m" by auto
      have "coeff ?r i =
            ( x < n. vec_first v n $ (n - Suc x) * coeff p (i - x)) +
            ( x < m. vec_last v m $ (m - Suc x) * coeff q (i - x))"
        (is "_ = sum ?f _ + sum ?g _")
        unfolding coeff_add coeff_mult Let_def 
        unfolding coeff_poly_of_vec dim if_distrib
        unfolding atMost_def
        apply(subst sum.inter_filter[symmetric],simp)
        apply(subst sum.inter_filter[symmetric],simp)
        unfolding mem_Collect_eq
        unfolding i_n i_m
        unfolding lessThan_def by simp
      also { fix x assume x: "x < n"
        have "coeff p (i-x) = 0"
          apply(rule coeff_eq_0) using i_mn x m by auto
        hence "?f x = 0" by auto
      } hence "sum ?f {..<n} = 0" by auto
      also { fix x assume x: "x < m"
        have "coeff q (i-x) = 0"
          apply(rule coeff_eq_0) using i_mn x n by auto
        hence "?g x = 0" by auto
      } hence "sum ?g {..<m} = 0" by auto
      finally have "coeff ?r i = 0" by auto
      also from False have "0 = coeff ?l i"
        unfolding coeff_poly_of_vec dim sum.distrib[symmetric] by auto
      finally show ?thesis by auto
    next case True
      hence "coeff ?l i = ((sylvester_mat_sub m n p q)T *v v) $ (n + m - Suc i)"
        unfolding coeff_poly_of_vec dim sum.distrib[symmetric] by auto
      also have "... = coeff (p * poly_of_vec (vec_first v n) + q * poly_of_vec (vec_last v m)) i"
        apply(subst index_mult_mat_vec) using True apply simp
        apply(subst row_transpose) using True apply simp
        apply(subst col_sylvester_sub)
        using True apply simp
        apply(subst vec_first_last_append[of v n m,symmetric]) using v apply(simp add: add.commute)
        apply(subst scalar_prod_append)
        apply (rule carrier_vecI,simp)+
        apply (subst vec_of_poly_rev_shifted_scalar_prod[OF m],simp) using True apply simp
        apply (subst add.commute[of n m])
        apply (subst vec_of_poly_rev_shifted_scalar_prod[OF n]) apply simp using True apply simp
        by simp
      also have "... =
        (xi. (if x < n then vec_first v n $ (n - Suc x) else 0) * coeff p (i - x)) +
        (xi. (if x < m then vec_last v m $ (m - Suc x) else 0) * coeff q (i - x))"
        unfolding coeff_poly_of_vec[of "vec_first v n",unfolded dim_vec_first,symmetric]
        unfolding coeff_poly_of_vec[of "vec_last v m",unfolded dim_vec_last,symmetric]
        unfolding coeff_mult[symmetric] by (simp add: mult.commute)
      also have "... = coeff ?r i"
        unfolding coeff_add coeff_mult Let_def
        unfolding coeff_poly_of_vec dim..
      finally show ?thesis.
  qed
qed

(**** End of the lemmas which could be moved to Algebraic_Numbers/Resultant.thy ****)

(**** The following lemmas could be moved to Computational_Algebra/Polynomial.thy ****)

lemma normalize_field [simp]: "normalize (a :: 'a :: {field, semiring_gcd}) = (if a = 0 then 0 else 1)"
  using unit_factor_normalize by fastforce

lemma content_field [simp]: "content (p :: 'a :: {field,semiring_gcd} poly) = (if p = 0 then 0 else 1)"
  by (induct p, auto simp: content_def)

lemma primitive_part_field [simp]: "primitive_part (p :: 'a :: {field,semiring_gcd} poly) = p"
  by (cases "p = 0", auto intro!: primitive_part_prim)

lemma primitive_part_dvd: "primitive_part a dvd a"
  by (metis content_times_primitive_part dvd_def dvd_refl mult_smult_right)

lemma degree_abs [simp]:
  "degree ¦p¦ = degree p" by (auto simp: abs_poly_def)

lemma degree_gcd1:
  assumes a_not0: "a  0" 
  shows "degree (gcd a b)  degree a"
proof -
  let ?g = "gcd a b"
  have gcd_dvd_b: "?g dvd a" by simp
  from this obtain c where a_gc: "a = ?g * c" unfolding dvd_def by auto
  have g_not0: "?g 0" using a_not0 a_gc by auto
  have c0: "c  0" using a_not0 a_gc by auto
  have "degree ?g  degree (?g * c)" by (rule degree_mult_right_le[OF c0])
  also have "... = degree a" using a_gc by auto
  finally show ?thesis .  
qed

lemma primitive_part_neg [simp]:
  fixes a::"'a :: {factorial_ring_gcd,factorial_semiring_multiplicative} poly"
  shows "primitive_part (-a) = - primitive_part a"
proof -
  have "primitive_part (-a) = primitive_part (smult (-1) a)" by auto
  then show ?thesis unfolding primitive_part_smult
    by (simp add: is_unit_unit_factor)
qed

lemma content_uminus[simp]: 
  fixes f::"int poly"
  shows "content (-f) = content f"
proof -
  have "-f = - (smult 1 f)" by auto
  also have "... = smult (-1) f" using smult_minus_left by auto
  finally have "content (-f) = content (smult (-1) f)" by auto
  also have "... = normalize (- 1) * content f" unfolding content_smult ..
  finally show ?thesis by auto  
qed

lemma pseudo_mod_monic:
  fixes f g :: "'a::{comm_ring_1,semiring_1_no_zero_divisors} poly"
  defines "r  pseudo_mod f g"
  assumes monic_g: "monic g"
  shows "q.  f = g * q + r" "r = 0  degree r < degree g"
proof -
  let ?cg = "coeff g (degree g)"
  let ?cge = "?cg ^ (Suc (degree f) - degree g)"
  define a where "a = ?cge"
  from r_def[unfolded pseudo_mod_def] obtain q where pdm: "pseudo_divmod f g = (q, r)"
    by (cases "pseudo_divmod f g") auto
  have g: "g  0" using monic_g by auto
  from pseudo_divmod[OF g pdm] have id: "smult a f = g * q + r" and "r = 0  degree r < degree g"
    by (auto simp: a_def)
  have a1: "a = 1" unfolding a_def using monic_g by auto
  hence id2: "f = g * q + r" using id by auto  
  show "r = 0  degree r < degree g" by fact  
  from g have "a  0"
    by (auto simp: a_def)  
  with id2 show "q. f = g * q + r"
    by auto
qed

lemma monic_imp_div_mod_int_poly_degree: 
  fixes p :: "'a::{comm_ring_1,semiring_1_no_zero_divisors} poly"
  assumes m: "monic u"
  shows "q r. p = q*u + r  (r = 0  degree r < degree u)" 
  using pseudo_mod_monic[OF m] using mult.commute by metis

corollary monic_imp_div_mod_int_poly_degree2: 
  fixes p :: "'a::{comm_ring_1,semiring_1_no_zero_divisors} poly"
  assumes m: "monic u" and deg_u: "degree u > 0"
  shows "q r. p = q*u + r  (degree r < degree u)"
proof -  
  obtain q r where "p = q * u + r" and r: "(r = 0  degree r < degree u)" 
      using monic_imp_div_mod_int_poly_degree[OF m, of p] by auto
    moreover have "degree r < degree u" using deg_u r by auto  
  ultimately show ?thesis by auto
qed
(**** End of the lemmas that could be moved to Computational_Algebra/Polynomial.thy ****)


(* To be categorized *)
lemma (in zero_hom) hom_upper_triangular:
  "A  carrier_mat n n  upper_triangular A  upper_triangular (map_mat hom A)"
  by (auto simp: upper_triangular_def)

end

Theory More_IArray

(*
    Authors:    Ralph Bottesch
                Maximilian Haslbeck
                René Thiemann
    License:    BSD
*)
section ‹Auxiliary Lemmas and Definitions for Immutable Arrays›

text ‹We define some definitions on immutable arrays, and modify the simplication
  rules so that IArrays will mainly operate pointwise, and not as lists.
  To be more precise, IArray.of-fun will become the main constructor.›
theory More_IArray
  imports "HOL-Library.IArray" 
begin

definition iarray_update :: "'a iarray  nat  'a  'a iarray" where
  "iarray_update a i x = IArray.of_fun (λ j. if j = i then x else a !! j) (IArray.length a)" 

lemma iarray_cong: "n = m  ( i. i < m  f i = g i)  IArray.of_fun f n = IArray.of_fun g m" 
  by auto

lemma iarray_cong': "( i. i < n  f i = g i)  IArray.of_fun f n = IArray.of_fun g n" 
  by (rule iarray_cong, auto)

lemma iarray_update_length[simp]: "IArray.length (iarray_update a i x) = IArray.length a" 
  unfolding iarray_update_def by simp

lemma iarray_length_of_fun[simp]: "IArray.length (IArray.of_fun f n) = n" by simp

lemma iarray_update_of_fun[simp]: "iarray_update (IArray.of_fun f n) i x = IArray.of_fun (f (i := x)) n" 
  unfolding iarray_update_def iarray_length_of_fun
  by (rule iarray_cong, auto)

fun iarray_append where "iarray_append (IArray xs) x = IArray (xs @ [x])" 

lemma iarray_append_code[code]: "iarray_append xs x = IArray (IArray.list_of xs @ [x])"
  by (cases xs, auto)

lemma iarray_append_of_fun[simp]: "iarray_append (IArray.of_fun f n) x = IArray.of_fun (f (n := x)) (Suc n)" 
  by auto

declare iarray_append.simps[simp del]

lemma iarray_of_fun_sub[simp]: "i < n  IArray.of_fun f n !! i = f i" 
  by auto

lemma IArray_of_fun_conv: "IArray xs = IArray.of_fun (λ i. xs ! i) (length xs)" 
  by (auto intro!: nth_equalityI)

declare IArray.of_fun_def[simp del]
declare IArray.sub_def[simp del]

lemmas iarray_simps = iarray_update_of_fun iarray_append_of_fun IArray_of_fun_conv iarray_of_fun_sub

end

Theory Norms

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

section ‹Norms›

text ‹In this theory we provide the basic definitions and properties of several 
  norms of vectors and polynomials.
› 

theory Norms
  imports "HOL-Computational_Algebra.Polynomial" 
    "HOL-Library.Adhoc_Overloading"
    "Jordan_Normal_Form.Conjugate"
    "Algebraic_Numbers.Resultant" (* only for poly_of_vec *)
    Missing_Lemmas
begin

subsection ‹L-∞› Norms›

consts linf_norm :: "'a  'b" ("(_)")

definition linf_norm_vec where "linf_norm_vec v  max_list (map abs (list_of_vec v) @ [0])"
adhoc_overloading linf_norm linf_norm_vec

definition linf_norm_poly where "linf_norm_poly f  max_list (map abs (coeffs f) @ [0])"
adhoc_overloading linf_norm linf_norm_poly

lemma linf_norm_vec: "vec n f = max_list (map (abs  f) [0..<n] @ [0])"
  by (simp add: linf_norm_vec_def)

lemma linf_norm_vec_vCons[simp]: "vCons a v = max ¦a¦ v"
  by (auto simp: linf_norm_vec_def max_list_Cons)

lemma linf_norm_vec_0 [simp]: "vec 0 f = 0" by (simp add: linf_norm_vec_def)

lemma linf_norm_zero_vec [simp]: "0v n :: 'a :: ordered_ab_group_add_abs vec = 0"
  by (induct n, simp add: zero_vec_def, auto simp: zero_vec_Suc)

lemma linf_norm_vec_ge_0 [intro!]:
  fixes v :: "'a :: ordered_ab_group_add_abs vec"
  shows "v  0"
  by (induct v, auto simp: max_def)

lemma linf_norm_vec_eq_0 [simp]:
  fixes v :: "'a :: ordered_ab_group_add_abs vec"
  assumes "v  carrier_vec n"
  shows "v = 0  v = 0v n"
  by (insert assms, induct rule: carrier_vec_induct, auto simp: zero_vec_Suc max_def)

lemma linf_norm_vec_greater_0 [simp]:
  fixes v :: "'a :: ordered_ab_group_add_abs vec"
  assumes "v  carrier_vec n"
  shows "v > 0  v  0v n"
  by (insert assms, induct rule: carrier_vec_induct, auto simp: zero_vec_Suc max_def)

lemma linf_norm_poly_0 [simp]: "0::_ poly = 0"
  by (simp add: linf_norm_poly_def)

lemma linf_norm_pCons [simp]:
  fixes p :: "'a :: ordered_ab_group_add_abs poly"
  shows "pCons a p = max ¦a¦ p"
  by (cases "p = 0", cases "a = 0", auto simp: linf_norm_poly_def max_list_Cons)

lemma linf_norm_poly_ge_0 [intro!]:
  fixes f :: "'a :: ordered_ab_group_add_abs poly"
  shows "f  0"
  by (induct f, auto simp: max_def)

lemma linf_norm_poly_eq_0 [simp]:
  fixes f :: "'a :: ordered_ab_group_add_abs poly"
  shows "f = 0  f = 0"
  by (induct f, auto simp: max_def)

lemma linf_norm_poly_greater_0 [simp]:
  fixes f :: "'a :: ordered_ab_group_add_abs poly"
  shows "f > 0  f  0"
  by (induct f, auto simp: max_def)

subsection ‹Square Norms›

consts sq_norm :: "'a  'b" ("(_)2")

abbreviation "sq_norm_conjugate x  x * conjugate x"
adhoc_overloading sq_norm sq_norm_conjugate

subsubsection ‹Square norms for vectors›

text ‹We prefer sum\_list over sum because it is not essentially dependent on commutativity,
  and easier for proving.
›
definition "sq_norm_vec v  x  list_of_vec v. x2"
adhoc_overloading sq_norm sq_norm_vec

lemma sq_norm_vec_vCons[simp]: "vCons a v2 = a2 + v2"
  by (simp add: sq_norm_vec_def)

lemma sq_norm_vec_0[simp]: "vec 0 f2 = 0"
  by (simp add: sq_norm_vec_def)

lemma sq_norm_vec_as_cscalar_prod:
  fixes v :: "'a :: conjugatable_ring vec"
  shows "v2 = v ∙c v"
  by (induct v, simp_all add: sq_norm_vec_def)

lemma sq_norm_zero_vec[simp]: "0v n :: 'a :: conjugatable_ring vec2 = 0"
  by (simp add: sq_norm_vec_as_cscalar_prod)

lemmas sq_norm_vec_ge_0 [intro!] = conjugate_square_ge_0_vec[folded sq_norm_vec_as_cscalar_prod]

lemmas sq_norm_vec_eq_0 [simp] = conjugate_square_eq_0_vec[folded sq_norm_vec_as_cscalar_prod]

lemmas sq_norm_vec_greater_0 [simp] = conjugate_square_greater_0_vec[folded sq_norm_vec_as_cscalar_prod]

subsubsection ‹Square norm for polynomials›

definition sq_norm_poly where "sq_norm_poly p  acoeffs p. a2"

adhoc_overloading sq_norm sq_norm_poly

lemma sq_norm_poly_0 [simp]: "0::_poly2 = 0"
  by (auto simp: sq_norm_poly_def)

lemma sq_norm_poly_pCons [simp]:
  fixes a :: "'a :: conjugatable_ring"
  shows "pCons a p2 = a2 + p2"
  by (cases "p = 0"; cases "a = 0", auto simp: sq_norm_poly_def)

lemma sq_norm_poly_ge_0 [intro!]:
  fixes p :: "'a :: conjugatable_ordered_ring poly"
  shows "p2  0"
  by (unfold sq_norm_poly_def, rule sum_list_nonneg, auto intro!:conjugate_square_positive)

lemma sq_norm_poly_eq_0 [simp]:
  fixes p :: "'a :: {conjugatable_ordered_ring,ring_no_zero_divisors} poly"
  shows "p2 = 0  p = 0"
proof (induct p)
  case IH: (pCons a p)
  show ?case
  proof (cases "a = 0")
    case True
    with IH show ?thesis by simp
  next
    case False
    then have "a2 + p2 > 0" by (intro add_pos_nonneg, auto)
    then show ?thesis by auto
  qed
qed simp

lemma sq_norm_poly_pos [simp]:
  fixes p :: "'a :: {conjugatable_ordered_ring,ring_no_zero_divisors} poly"
  shows "p2 > 0  p  0"
  by (auto simp: less_le)

lemma sq_norm_vec_of_poly [simp]:
  fixes p :: "'a :: conjugatable_ring poly"
  shows "vec_of_poly p2 = p2"
  apply (unfold sq_norm_poly_def sq_norm_vec_def)
  apply (fold sum_mset_sum_list)
  apply auto.

lemma sq_norm_poly_of_vec [simp]:
  fixes v :: "'a :: conjugatable_ring vec"
  shows "poly_of_vec v2 = v2"
  apply (unfold sq_norm_poly_def sq_norm_vec_def coeffs_poly_of_vec)
  apply (fold rev_map)
  apply (fold sum_mset_sum_list)
  apply (unfold mset_rev)
  apply (unfold sum_mset_sum_list)
  by (auto intro: sum_list_map_dropWhile0)

subsection ‹Relating Norms›

text ‹A class where ordering around 0 is linear.›
abbreviation (in ordered_semiring) is_real where "is_real a  a < 0  a = 0  0 < a"

class semiring_real_line = ordered_semiring_strict + ordered_semiring_0 +
  assumes add_pos_neg_is_real: "a > 0  b < 0  is_real (a + b)"
      and mult_neg_neg: "a < 0  b < 0  0 < a * b"
      and pos_pos_linear: "0 < a  0 < b  a < b  a = b  b < a"
      and neg_neg_linear: "a < 0  b < 0  a < b  a = b  b < a"
begin

lemma add_neg_pos_is_real: "a < 0  b > 0  is_real (a + b)"
  using add_pos_neg_is_real[of b a] by (simp add: ac_simps)

lemma nonneg_linorder_cases [consumes 2, case_names less eq greater]:
  assumes "0  a" and "0  b"
      and "a < b  thesis" "a = b  thesis" "b < a  thesis"
  shows thesis
  using assms pos_pos_linear by (auto simp: le_less)

lemma nonpos_linorder_cases [consumes 2, case_names less eq greater]:
  assumes "a  0" "b  0"
      and "a < b  thesis" "a = b  thesis" "b < a  thesis"
  shows thesis
  using assms neg_neg_linear by (auto simp: le_less)

lemma real_linear:
  assumes "is_real a" and "is_real b" shows "a < b  a = b  b < a"
  using pos_pos_linear neg_neg_linear assms by (auto dest: less_trans[of _ 0])

lemma real_linorder_cases [consumes 2, case_names less eq greater]:
  assumes real: "is_real a" "is_real b"
      and cases: "a < b  thesis" "a = b  thesis" "b < a  thesis"
  shows thesis
  using real_linear[OF real] cases by auto

lemma
  assumes a: "is_real a" and b: "is_real b"
  shows real_add_le_cancel_left_pos: "c + a  c + b  a  b"
    and real_add_less_cancel_left_pos: "c + a < c + b  a < b"
    and real_add_le_cancel_right_pos: "a + c  b + c  a  b"
    and real_add_less_cancel_right_pos: "a + c < b + c  a < b"
  using add_strict_left_mono[of b a c] add_strict_left_mono[of a b c]
  using add_strict_right_mono[of b a c] add_strict_right_mono[of a b c]
  by (atomize(full), cases rule: real_linorder_cases[OF a b], auto)

lemma
  assumes a: "is_real a" and b: "is_real b" and c: "0 < c"
  shows real_mult_le_cancel_left_pos: "c * a  c * b  a  b"
    and real_mult_less_cancel_left_pos: "c * a < c * b  a < b"
    and real_mult_le_cancel_right_pos: "a * c  b * c  a  b"
    and real_mult_less_cancel_right_pos: "a * c < b * c  a < b"
  using mult_strict_left_mono[of b a c] mult_strict_left_mono[of a b c] c
  using mult_strict_right_mono[of b a c] mult_strict_right_mono[of a b c] c
  by (atomize(full), cases rule: real_linorder_cases[OF a b], auto)

lemma
  assumes a: "is_real a" and b: "is_real b"
  shows not_le_real: "¬ a  b  a < b"
    and not_less_real: "¬ a > b  a  b"
  by (atomize(full), cases rule: real_linorder_cases[OF a b], auto simp: less_imp_le)

lemma real_mult_eq_0_iff:
  assumes a: "is_real a" and b: "is_real b"
  shows "a * b = 0  a = 0  b = 0"
proof-
  { assume l: "a * b = 0" and "a  0" and "b  0"
    with a b have "a < 0  0 < a" and "b < 0  0 < b" by auto
    then have "False" using mult_pos_pos[of a b] mult_pos_neg[of a b] mult_neg_pos[of a b] mult_neg_neg[of a b]
      by (auto simp:l)
  } then show ?thesis by auto
qed

end

lemma real_pos_mult_max:
  fixes a b c :: "'a :: semiring_real_line"
  assumes c: "c > 0" and a: "is_real a" and b: "is_real b"
  shows "c * max a b = max (c * a) (c * b)"
  by (rule hom_max, simp add: real_mult_le_cancel_left_pos[OF a b c])

class ring_abs_real_line = ordered_ring_abs + semiring_real_line

class semiring_1_real_line = semiring_real_line + monoid_mult + zero_less_one
begin

subclass ordered_semiring_1 by (unfold_locales, auto)

lemma power_both_mono: "1  a  m  n  a  b  a ^ m  b ^ n"
  using power_mono[of a b n] power_increasing[of m n a]
  by (auto simp: order.trans[OF zero_le_one])

lemma power_pos:
  assumes a0: "0 < a" shows "0 < a ^ n"
  by (induct n, insert mult_strict_mono[OF a0] a0, auto)

lemma power_neg:
  assumes a0: "a < 0" shows "odd n  a ^ n < 0" and "even n  a ^ n > 0"
  by (atomize(full), induct n, insert a0, auto simp add: mult_pos_neg2 mult_neg_neg)

lemma power_ge_0_iff:
  assumes a: "is_real a"
  shows "0  a ^ n  0  a  even n"
using a proof (elim disjE)
  assume "a < 0"
  with power_neg[OF this, of n] show ?thesis by(cases "even n", auto)
next
  assume "0 < a"
  with power_pos[OF this] show ?thesis by auto
next
  assume "a = 0"
  then show ?thesis by (auto simp:power_0_left)
qed

lemma nonneg_power_less:
  assumes "0  a" and "0  b" shows "a^n < b^n  n > 0  a < b"
proof (insert assms, induct n arbitrary: a b)
  case 0
  then show ?case by auto
next
  case (Suc n)
  note a = 0  a
  note b = 0  b
  show ?case
  proof (cases "n > 0")
    case True
    from a b show ?thesis
    proof (cases rule: nonneg_linorder_cases)
      case less
      then show ?thesis by (auto simp: Suc.hyps[OF a b] True intro!:mult_strict_mono' a b zero_le_power)
    next
      case eq
      then show ?thesis by simp
    next
      case greater
      with Suc.hyps[OF b a] True have "b ^ n < a ^ n" by auto
      with mult_strict_mono'[OF greater this] b greater
      show ?thesis by auto
    qed
  qed auto
qed

lemma power_strict_mono:
  shows "a < b  0  a  0 < n  a ^ n < b ^ n"
  by (subst nonneg_power_less, auto)

lemma nonneg_power_le:
  assumes "0  a" and "0  b" shows "a^n  b^n  n = 0  a  b"
using assms proof (cases rule: nonneg_linorder_cases)
  case less
  with power_strict_mono[OF this, of n] assms show ?thesis by (cases n, auto)
next
  case eq
  then show ?thesis by auto
next
  case greater
  with power_strict_mono[OF this, of n] assms show ?thesis by (cases n, auto)
qed

end

subclass (in linordered_idom) semiring_1_real_line
  apply unfold_locales
  by (auto simp: mult_strict_left_mono mult_strict_right_mono mult_neg_neg)

class ring_1_abs_real_line = ring_abs_real_line + semiring_1_real_line
begin

subclass ring_1..

lemma abs_cases:
  assumes "a = 0  thesis" and "¦a¦ > 0  thesis" shows thesis
  using assms by auto

lemma abs_linorder_cases[case_names less eq greater]:
  assumes "¦a¦ < ¦b¦  thesis" and "¦a¦ = ¦b¦  thesis" and "¦b¦ < ¦a¦  thesis"
  shows thesis
  apply (cases rule: nonneg_linorder_cases[of "¦a¦" "¦b¦"])
  using assms by auto

lemma [simp]:
  shows not_le_abs_abs: "¬ ¦a¦  ¦b¦  ¦a¦ < ¦b¦"
    and not_less_abs_abs: "¬ ¦a¦ > ¦b¦  ¦a¦  ¦b¦"
  by (atomize(full), cases a b rule: abs_linorder_cases, auto simp: less_imp_le)

lemma abs_power_less [simp]: "¦a¦^n < ¦b¦^n  n > 0  ¦a¦ < ¦b¦"
  by (subst nonneg_power_less, auto)

lemma abs_power_le [simp]: "¦a¦^n  ¦b¦^n  n = 0  ¦a¦  ¦b¦"
  by (subst nonneg_power_le, auto)

lemma abs_power_pos [simp]: "¦a¦^n > 0  a  0  n = 0"
  using power_pos[of "¦a¦"] by (cases "n", auto)

lemma abs_power_nonneg [intro!]: "¦a¦^n  0" by auto

lemma abs_power_eq_0 [simp]: "¦a¦^n = 0  a = 0  n  0"
  apply (induct n, force)
  apply (unfold power_Suc)
  apply (subst real_mult_eq_0_iff, auto).

end

instance nat :: semiring_1_real_line by (intro_classes, auto)
instance int :: ring_1_abs_real_line..

lemma vec_index_vec_of_list [simp]: "vec_of_list xs $ i = xs ! i"
  by transfer (auto simp: mk_vec_def undef_vec_def dest: empty_nth)

lemma vec_of_list_append: "vec_of_list (xs @ ys) = vec_of_list xs @v vec_of_list ys"
  by (auto simp: nth_append)

lemma linf_norm_vec_of_list:
  "vec_of_list xs = max_list (map abs xs @ [0])"
  by (simp add: linf_norm_vec_def)

lemma linf_norm_vec_as_Greatest:
  fixes v :: "'a :: ring_1_abs_real_line vec"
  shows "v = (GREATEST a. a  abs ` set (list_of_vec v)  {0})"
  unfolding linf_norm_vec_of_list[of "list_of_vec v", simplified]
  by (subst max_list_as_Greatest, auto)

lemma vec_of_poly_pCons:
  assumes "f  0"
  shows "vec_of_poly (pCons a f) = vec_of_poly f @v vec_of_list [a]"
  using assms
  by (auto simp: vec_eq_iff Suc_diff_le)

lemma vec_of_poly_as_vec_of_list:
  assumes "f  0"
  shows "vec_of_poly f = vec_of_list (rev (coeffs f))"
proof (insert assms, induct f)
  case 0
  then show ?case by auto
next
  case (pCons a f)
  then show ?case
    by (cases "f = 0", auto simp: vec_of_list_append vec_of_poly_pCons)
qed

lemma linf_norm_vec_of_poly [simp]:
  fixes f :: "'a :: ring_1_abs_real_line poly"
  shows "vec_of_poly f = f"
proof (cases "f = 0")
  case False
  then show ?thesis
    apply (unfold vec_of_poly_as_vec_of_list linf_norm_vec_of_list linf_norm_poly_def)
    apply (subst (1 2) max_list_as_Greatest, auto).
qed simp

lemma linf_norm_poly_as_Greatest:
  fixes f :: "'a :: ring_1_abs_real_line poly"
  shows "f = (GREATEST a. a  abs ` set (coeffs f)  {0})"
  using linf_norm_vec_as_Greatest[of "vec_of_poly f"]
  by simp

lemma vec_index_le_linf_norm:
  fixes v :: "'a :: ring_1_abs_real_line vec"
  assumes "i < dim_vec v"
  shows "¦v$i¦  v"
apply (unfold linf_norm_vec_def, rule le_max_list) using assms
apply (auto simp:  in_set_conv_nth intro!: imageI exI[of _ i]).

lemma coeff_le_linf_norm:
  fixes f :: "'a :: ring_1_abs_real_line poly"
  shows "¦coeff f i¦  f"
  using vec_index_le_linf_norm[of "degree f - i" "vec_of_poly f"]
  by (cases "i  degree f", auto simp: coeff_eq_0)

class conjugatable_ring_1_abs_real_line = conjugatable_ring + ring_1_abs_real_line + power +
  assumes sq_norm_as_sq_abs [simp]: "a2 = ¦a¦2"
begin
subclass conjugatable_ordered_ring by (unfold_locales, simp)
end

instance int :: conjugatable_ring_1_abs_real_line
  by (intro_classes, simp add: numeral_2_eq_2)

instance rat :: conjugatable_ring_1_abs_real_line
  by (intro_classes, simp add: numeral_2_eq_2)

instance real :: conjugatable_ring_1_abs_real_line
  by (intro_classes, simp add: numeral_2_eq_2)

instance complex :: semiring_1_real_line
  apply intro_classes
  by (auto simp: complex_eq_iff mult_le_cancel_left mult_le_cancel_right mult_neg_neg)

text ‹
  Due to the assumption @{thm abs_ge_self} from Groups.thy,
  @{type complex} cannot be @{class ring_1_abs_real_line}!
›
instance complex :: ordered_ab_group_add_abs oops

lemma sq_norm_as_sq_abs [simp]: "(sq_norm :: 'a :: conjugatable_ring_1_abs_real_line  'a) = power2  abs"
  by auto

lemma sq_norm_vec_le_linf_norm:
  fixes v :: "'a :: {conjugatable_ring_1_abs_real_line} vec"
  assumes "v  carrier_vec n"
  shows "v2  of_nat n * v2"
proof (insert assms, induct rule: carrier_vec_induct)
  case (Suc n a v)
  have [dest!]: "¬ ¦a¦  v  of_nat n * v2  of_nat n * ¦a¦2"
    by (rule real_linorder_cases[of "¦a¦" "v"], insert Suc, auto simp: less_le intro!: power_mono mult_left_mono)
  from Suc show ?case
    by (auto simp: ring_distribs max_def intro!:add_mono power_mono)
qed simp
 
lemma sq_norm_poly_le_linf_norm:
  fixes p :: "'a :: {conjugatable_ring_1_abs_real_line} poly"
  shows "p2  of_nat (degree p + 1) * p2"
  using sq_norm_vec_le_linf_norm[of "vec_of_poly p" "degree p + 1"]
    by (auto simp: carrier_dim_vec)

lemma coeff_le_sq_norm:
  fixes f :: "'a :: {conjugatable_ring_1_abs_real_line} poly"
  shows "¦coeff f i¦2  f2"
proof (induct f arbitrary: i)
  case (pCons a f)
  show ?case
  proof (cases i)
    case (Suc ii)
    note pCons(2)[of ii]
    also have "f2  ¦a¦2 + f2" by auto
    finally show ?thesis unfolding Suc by auto
  qed auto
qed simp

lemma max_norm_witness:
  fixes f :: "'a :: ordered_ring_abs poly"
  shows " i. f = ¦coeff f i¦"
  by (induct f, auto simp add: max_def intro: exI[of _ "Suc _"] exI[of _ 0])

lemma max_norm_le_sq_norm:
  fixes f ::  "'a :: conjugatable_ring_1_abs_real_line poly"
shows "f2  f2" 
proof -
  from max_norm_witness[of f] obtain i where id: "f = ¦coeff f i¦" by auto
  show ?thesis unfolding id using coeff_le_sq_norm[of f i] by auto
qed

(*TODO MOVE*)
lemma (in conjugatable_ring) conjugate_minus: "conjugate (x - y) = conjugate x - conjugate y"
  by (unfold diff_conv_add_uminus conjugate_dist_add conjugate_neg, rule)

lemma conjugate_1[simp]: "(conjugate 1 :: 'a :: {conjugatable_ring, ring_1}) = 1"
proof-
  have "conjugate 1 * 1 = (conjugate 1 :: 'a)" by simp
  also have "conjugate  = 1" by simp
  finally show ?thesis by (unfold conjugate_dist_mul, simp)
qed

lemma conjugate_of_int [simp]:
  "(conjugate (of_int x) :: 'a :: {conjugatable_ring,ring_1}) = of_int x"
proof (induct x)
  case (nonneg n)
  then show ?case by (induct n, auto simp: conjugate_dist_add)
next
  case (neg n)
  then show ?case apply (induct n, auto simp: conjugate_minus conjugate_neg)
    by (metis conjugate_1 conjugate_dist_add one_add_one)
qed


lemma sq_norm_of_int: "map_vec of_int v :: 'a :: {conjugatable_ring,ring_1} vec2 = of_int v2" 
  unfolding sq_norm_vec_as_cscalar_prod scalar_prod_def
  unfolding hom_distribs
  by (rule sum.cong, auto)

definition "norm1 p = sum_list (map abs (coeffs p))"

lemma norm1_ge_0: "norm1 (f :: 'a :: {abs,ordered_semiring_0,ordered_ab_group_add_abs}poly)  0" 
  unfolding norm1_def by (rule sum_list_nonneg, auto)

lemma norm2_norm1_main_equality: fixes f :: "nat  'a :: linordered_idom" 
  shows "(i = 0..<n. ¦f i¦)2 = (i = 0..<n. f i * f i)
      + (i = 0..<n. j = 0..<n. if i = j then 0 else ¦f i¦ * ¦f j¦)"  
proof (induct n)
  case (Suc n)
  have id: "{0 ..< Suc n} = insert n {0 ..< n}" by auto
  have id: "sum f {0 ..< Suc n} = f n + sum f {0 ..< n}" for f :: "nat  'a" 
    unfolding id by (rule sum.insert, auto)
  show ?case unfolding id power2_sum unfolding Suc
    by (auto simp: power2_eq_square sum_distrib_left sum.distrib ac_simps)
qed auto

lemma norm2_norm1_main_inequality: fixes f :: "nat  'a :: linordered_idom" 
  shows "(i = 0..<n. f i * f i)  (i = 0..<n. ¦f i¦)2"  
  unfolding norm2_norm1_main_equality 
  by (auto intro!: sum_nonneg)  

lemma norm2_le_norm1_int: "f :: int poly2  (norm1 f)^2" 
proof -
  define F where "F = (!) (coeffs f)" 
  define n where "n = length (coeffs f)" 
  have 1: "f2 = (i = 0..<n. F i * F i)" 
    unfolding norm1_def sq_norm_poly_def sum_list_sum_nth F_def n_def
    by (subst sum.cong, auto simp: power2_eq_square)
  have 2: "norm1 f = (i = 0..<n. ¦F i¦)" 
    unfolding norm1_def sq_norm_poly_def sum_list_sum_nth F_def n_def
    by (subst sum.cong, auto)
  show ?thesis unfolding 1 2 by (rule norm2_norm1_main_inequality)
qed

lemma sq_norm_smult_vec: "sq_norm ((c :: 'a :: {conjugatable_ring,comm_semiring_0}) v v) = (c * conjugate c) * sq_norm v" 
  unfolding sq_norm_vec_as_cscalar_prod 
  by (subst scalar_prod_smult_left, force, unfold conjugate_smult_vec, 
    subst scalar_prod_smult_right, force, simp add: ac_simps)

lemma vec_le_sq_norm:
  fixes v :: "'a :: conjugatable_ring_1_abs_real_line vec"
  assumes "v  carrier_vec n" "i < n"
  shows "¦v $ i¦2  v2"
using assms proof (induction v arbitrary: i)
  case (Suc n a v i)
  note IH = Suc
  show ?case 
  proof (cases i)
    case (Suc ii)
    then show ?thesis
      using IH IH(2)[of ii] le_add_same_cancel2 order_trans by fastforce
  qed auto
qed auto

class trivial_conjugatable =
  conjugate +
  assumes conjugate_id [simp]: "conjugate x = x"

class trivial_conjugatable_ordered_field = 
  conjugatable_ordered_field + trivial_conjugatable

class trivial_conjugatable_linordered_field = 
  trivial_conjugatable_ordered_field + linordered_field
begin
subclass conjugatable_ring_1_abs_real_line
  by (standard) (auto simp add: semiring_normalization_rules)
end

instance rat :: trivial_conjugatable_linordered_field 
  by (standard, auto)

instance real :: trivial_conjugatable_linordered_field 
  by (standard, auto)

lemma scalar_prod_ge_0: "(x :: 'a :: linordered_idom vec)  x  0" 
  unfolding scalar_prod_def
  by (rule sum_nonneg, auto)

lemma cscalar_prod_is_scalar_prod[simp]: "(x :: 'a :: trivial_conjugatable_ordered_field vec) ∙c y = x  y"
  unfolding conjugate_id
  by (rule arg_cong[of _ _ "scalar_prod x"], auto)


lemma scalar_prod_Cauchy:
  fixes u v::"'a :: {trivial_conjugatable_linordered_field} Matrix.vec"
  assumes "u  carrier_vec n" "v  carrier_vec n"
  shows "(u  v)2  u2 * v2 "
proof -
  { assume v_0: "v  0v n"
    have "0  (u - r v v)  (u - r v v)" for r
      by (simp add: scalar_prod_ge_0)
    also have "(u - r v v)  (u - r v v) = u  u - r * (u  v) - r * (u  v) + r * r * (v  v)" for r::'a
    proof -
      have "(u - r v v)  (u - r v v) = (u - r v v)  u - (u - r v v)  (r v v)"
        using assms by (subst scalar_prod_minus_distrib) auto
      also have " = u  u - (r v v)  u - r * ((u - r v v)  v)"
        using assms by (subst minus_scalar_prod_distrib) auto
      also have " = u  u - r * (v  u) - r * (u  v - r * (v  v))"
        using assms by (subst minus_scalar_prod_distrib) auto
      also have " = u  u - r * (u  v) - r * (u  v) + r * r * (v  v)"
        using assms comm_scalar_prod by (auto simp add: field_simps)
      finally show ?thesis
        by simp
    qed
    also have "u  u - r * (u  v) - r * (u  v) + r * r * (v  v) = sq_norm u - (u  v)2 / sq_norm v"
      if "r = (u  v) / (v  v)" for r
      unfolding that by (auto simp add: sq_norm_vec_as_cscalar_prod power2_eq_square)
    finally have "0  u2 - (u  v)2 / v2"
      by auto
    then have "(u  v)2 / v2  u2"
      by auto
    then have "(u  v)2  u2 * v2"
      using pos_divide_le_eq[of "v2"] v_0 assms by (auto)
  }
  then show ?thesis
    by (fastforce simp add: assms)
qed

end

Theory Int_Rat_Operations

(*
    Authors:    René Thiemann
    License:    BSD
*)
section ‹Optimized Code for Integer-Rational Operations›

theory Int_Rat_Operations
imports 
  Sqrt_Babylonian.Sqrt_Babylonian_Auxiliary
  Norms
begin

definition int_times_rat :: "int  rat  rat" where "int_times_rat i x = of_int i * x" 

declare int_times_rat_def[simp]

lemma int_times_rat_code[code abstract]: "quotient_of (int_times_rat i x) =
  (case quotient_of x of (n,d)  Rat.normalize (i * n, d))"  
  unfolding int_times_rat_def rat_times_code by auto

definition square_rat :: "rat  rat" where [simp]: "square_rat x = x * x" 

lemma quotient_of_square: assumes "quotient_of x = (a,b)"
  shows "quotient_of (x * x) = (a * a, b * b)"
proof -
  have b0: "b > 0" "b  0" using quotient_of_denom_pos[OF assms] by auto
  hence b: "(b * b > 0) = True" by auto
  show ?thesis
    unfolding rat_times_code assms Let_def split Rat.normalize_def fst_conv snd_conv b if_True
    using quotient_of_coprime[OF assms] b0 by simp
qed

lemma square_rat_code[code abstract]: "quotient_of (square_rat x) = (case quotient_of x of (n,d)
   (n * n, d * d))" using quotient_of_square[of x] unfolding square_rat_def 
  by (cases "quotient_of x", auto)


definition scalar_prod_int_rat :: "int vec  rat vec  rat" (infix "∙i" 70) where
  "x ∙i y = (y  map_vec rat_of_int x)"

lemma scalar_prod_int_rat_code[code]: "v ∙i w = (i = 0..<dim_vec v. int_times_rat (v $ i) (w $ i))"  
  unfolding scalar_prod_int_rat_def Let_def scalar_prod_def int_times_rat_def
  by (rule sum.cong, auto)

lemma scalar_prod_int_rat[simp]: "dim_vec x = dim_vec y  x ∙i y = map_vec of_int x  y" 
  unfolding scalar_prod_int_rat_def by (intro comm_scalar_prod[of _ "dim_vec x"], auto intro: carrier_vecI) 

definition sq_norm_vec_rat :: "rat vec  rat" where [simp]: "sq_norm_vec_rat x = sq_norm_vec x" 

lemma sq_norm_vec_rat_code[code]: "sq_norm_vec_rat x = (xlist_of_vec x. square_rat x)" 
  unfolding sq_norm_vec_rat_def sq_norm_vec_def square_rat_def by auto

end

Theory Cost

(*
    Authors:    Maximilian Haslbeck
                René Thiemann
    License:    BSD
*)
section ‹Representing Computation Costs as Pairs of Results and Costs›
theory Cost
  imports Main
begin

type_synonym 'a cost = "'a × nat" 

definition cost :: "'a cost  nat" where "cost = snd" 
definition result :: "'a cost  'a" where "result = fst" 

lemma cost_simps: "cost (a,c) = c" "result (a,c) = a" 
  unfolding cost_def result_def by auto

lemma result_costD: assumes "result f_c = f" 
  "cost f_c  b"
  "f_c = (a,c)"
shows "a = f" "c  b" using assms by (auto simp: cost_simps)

lemma result_costD': assumes "result f_c = f  cost f_c  b"
  "f_c = (a,c)"
  shows "a = f" "c  b" using assms by (auto simp: cost_simps)

end

Theory List_Representation

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

section ‹List representation›

theory List_Representation
  imports Main
begin

lemma rev_take_Suc: assumes j: "j < length xs"
  shows "rev (take (Suc j) xs) = xs ! j # rev (take j xs)" 
proof -
  from j have xs: "xs = take j xs @ xs ! j # drop (Suc j) xs" by (rule id_take_nth_drop)
  show ?thesis unfolding arg_cong[OF xs, of "λ xs. rev (take (Suc j) xs)"] 
    by (simp add: min_def)
qed
    
type_synonym 'a list_repr = "'a list × 'a list"   

definition list_repr :: "nat  'a list_repr  'a list  bool" where
  "list_repr i ba xs = (i  length xs  fst ba = rev (take i xs)  snd ba = drop i xs)"  

definition of_list_repr :: "'a list_repr  'a list" where
  "of_list_repr ba = (rev (fst ba) @ snd ba)" 
  
lemma of_list_repr: "list_repr i ba xs  of_list_repr ba = xs" 
  unfolding of_list_repr_def list_repr_def by auto
    
definition get_nth_i :: "'a list_repr  'a" where
  "get_nth_i ba = hd (snd ba)" 

definition get_nth_im1 :: "'a list_repr  'a" where
  "get_nth_im1 ba = hd (fst ba)" 
  
lemma get_nth_i: "list_repr i ba xs  i < length xs  get_nth_i ba = xs ! i" 
  unfolding list_repr_def get_nth_i_def 
  by (auto simp: hd_drop_conv_nth) 

lemma get_nth_im1: "list_repr i ba xs  i  0  get_nth_im1 ba = xs ! (i - 1)" 
  unfolding list_repr_def get_nth_im1_def 
  by (cases i, auto simp: rev_take_Suc) 
    
definition update_i :: "'a list_repr  'a  'a list_repr" where
  "update_i ba x = (fst ba, x # tl (snd ba))" 
  
lemma Cons_tl_drop_update: "i < length xs  x # tl (drop i xs) = drop i (xs[i := x])"
proof (induct i arbitrary: xs)
  case (0 xs)
  thus ?case by (cases xs, auto)
next
  case (Suc i xs)
  thus ?case by (cases xs, auto)
qed
  
lemma update_i: "list_repr i ba xs  i < length xs  list_repr i (update_i ba x) (xs [i := x])" 
  unfolding update_i_def list_repr_def 
  by (auto simp: Cons_tl_drop_update)
    
definition update_im1 :: "'a list_repr  'a  'a list_repr" where
  "update_im1 ba x = (x # tl (fst ba), snd ba)" 

lemma update_im1: "list_repr i ba xs  i  0  list_repr i (update_im1 ba x) (xs [i - 1 := x])" 
  unfolding update_im1_def list_repr_def 
  by (cases i, auto simp: rev_take_Suc)
  
lemma tl_drop_Suc: "tl (drop i xs) = drop (Suc i) xs"
proof (induct i arbitrary: xs)
  case (0 xs) thus ?case by (cases xs, auto)
next
  case (Suc i xs) thus ?case by (cases xs, auto)
qed
    
definition inc_i :: "'a list_repr  'a list_repr" where
  "inc_i ba = (case ba of (b,a)  (hd a # b, tl a))" 
    
lemma inc_i: "list_repr i ba xs  i < length xs  list_repr (Suc i) (inc_i ba) xs" 
  unfolding list_repr_def inc_i_def by (cases ba, auto simp: rev_take_Suc hd_drop_conv_nth tl_drop_Suc) 

definition dec_i :: "'a list_repr  'a list_repr" where
  "dec_i ba = (case ba of (b,a)  (tl b, hd b # a))" 
    
lemma dec_i: "list_repr i ba xs  i  0  list_repr (i - 1) (dec_i ba) xs" 
  unfolding list_repr_def dec_i_def 
  by (cases ba; cases i, auto simp: rev_take_Suc hd_drop_conv_nth Cons_nth_drop_Suc) 

lemma dec_i_Suc: "list_repr (Suc i) ba xs  list_repr i (dec_i ba) xs" 
  using dec_i[of "Suc i" ba xs] by auto

end

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 *)

no_notation Group.m_inv  ("invı _" [81] 80)

(* TODO: Is a function like this already in the library
   find_index is used to rewrite the sumlists in the lattice_of definition to finsums *)

fun find_index :: "'b list  'b  nat" where
  "find_index [] _ = 0" |
  "find_index (x#xs) y = (if x = y then 0 else find_index xs y + 1)"

lemma find_index_not_in_set: "x  set xs  find_index xs x = length xs"
  by (induction xs) auto

lemma find_index_in_set: "x  set xs  xs ! (find_index xs x) = x"
  by (induction xs) auto

lemma find_index_inj: "inj_on (find_index xs) (set xs)"
  by (induction xs) (auto simp add: inj_on_def)

lemma find_index_leq_length: "find_index xs x < length xs  x  set xs"
  by (induction xs) (auto)


(* TODO: move *)

lemma rev_unsimp: "rev xs @ (r # rs) = rev (r#xs) @ rs" by(induct xs,auto)


(* 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


(* TODO: move *)

context vec_module begin

definition lattice_of :: "'a vec list  'a vec set" where
  "lattice_of fs = range (λ c. sumlist (map (λ i. of_int (c i) v fs ! i) [0 ..< length fs]))"

lemma lattice_of_finsum:
  assumes "set fs  carrier_vec n"
  shows "lattice_of fs = range (λ c. finsum V (λ i. of_int (c i) v fs ! i) {0 ..< length fs})"
proof -
  have "sumlist (map (λ i. of_int (c i) v fs ! i) [0 ..< length fs])
        = finsum V (λ i. of_int (c i) v fs ! i) {0 ..< length fs}" for c
    using  assms by (subst sumlist_map_as_finsum) (fastforce)+
  then show ?thesis
    unfolding lattice_of_def by auto
qed

lemma in_latticeE: assumes "f  lattice_of fs" obtains c where
    "f = sumlist (map (λ i. of_int (c i) v fs ! i) [0 ..< length fs])" 
  using assms unfolding lattice_of_def by auto
    
lemma in_latticeI: assumes "f = sumlist (map (λ i. of_int (c i) v fs ! i) [0 ..< length fs])" 
  shows "f  lattice_of fs" 
  using assms unfolding lattice_of_def by auto

lemma finsum_over_indexes_to_vectors:
  assumes "set vs  carrier_vec n" "l = length vs"
  shows "c. (Vx{0..<l}. of_int (g x) v vs ! x) = (Vvset vs. of_int (c v) v v)"
  using assms proof (induction l arbitrary: vs)
  case (Suc l)
  then obtain vs' v where vs'_def: "vs = vs' @ [v]"
    by (metis Zero_not_Suc length_0_conv rev_exhaust)
  have c: "c. (Vi{0..<l}. of_int (g i) v vs' ! i) = (Vvset vs'. of_int (c v) v v)"
    using Suc vs'_def by (auto)
  then obtain c 
    where c_def: "(Vx{0..<l}. of_int (g x) v vs' ! x) = (Vvset vs'. of_int (c v) v v)"
    by blast
  have "(Vx{0..<Suc l}. of_int (g x) v vs ! x) 
        = of_int (g l) v vs ! l + (Vx{0..<l}. of_int (g x) v vs ! x)"
     using Suc by (subst finsum_insert[symmetric]) (fastforce intro!: finsum_cong')+
  also have "vs = vs' @ [v]"
    using vs'_def by simp
  also have "(Vx{0..<l}. of_int (g x) v (vs' @ [v]) ! x) = (Vx{0..<l}. of_int (g x) v vs' ! x)"
    using Suc vs'_def by (intro finsum_cong') (auto simp add: in_mono append_Cons_nth_left)
  also note c_def
  also have "(vs' @ [v]) ! l = v"
    using Suc vs'_def by auto
  also have "d'. of_int (g l) v v + (Vvset vs'. of_int (c v) v v) = (Vvset vs. of_int (d' v) v v)"
  proof (cases "v  set vs'")
    case True
    then have I: "set vs' = insert v (set vs' - {v})"
      by blast
    define c' where "c' x = (if x = v then c x + g l else c x)" for x
    have "of_int (g l) v v + (Vvset vs'. of_int (c v) v v)
          = of_int (g l) v v + (of_int (c v) v v + (Vvset vs' - {v}. of_int (c v) v v))"
      using Suc vs'_def by (subst I, subst finsum_insert) fastforce+
    also have " = of_int (g l) v v + of_int (c v) v v + (Vvset vs' - {v}. of_int (c v) v v)"
      using Suc vs'_def by (subst a_assoc) (auto intro!: finsum_closed)
    also have "of_int (g l) v v + of_int (c v) v v = of_int (c' v)  v v"
      unfolding c'_def by (auto simp add: add_smult_distrib_vec)
    also have "(Vvset vs' - {v}. of_int (c v) v v) = (Vvset vs' - {v}. of_int (c' v) v v)"
      using Suc vs'_def unfolding c'_def by (intro finsum_cong') (auto)
    also have "of_int (c' v) v v + (Vvset vs' - {v}. of_int (c' v) v v)
               = (Vvinsert v (set vs'). of_int (c' v) v v)"
      using Suc vs'_def by (subst finsum_insert[symmetric]) (auto)
    finally show ?thesis
      using vs'_def by force
  next
    case False
    define c' where "c' x = (if x = v then g l else c x)" for x
    have "of_int (g l) v v + (Vvset vs'. of_int (c v) v v)
          = of_int (c' v) v v + (Vvset vs'. of_int (c v) v v)"
      unfolding c'_def by simp
    also have "(Vvset vs'. of_int (c v) v v) = (Vvset vs'. of_int (c' v) v v)"
      unfolding c'_def using Suc False vs'_def by (auto intro!: finsum_cong')
    also have "of_int (c' v) v v + (Vvset vs'. of_int (c' v) v v)
               = (Vvinsert v (set vs'). of_int (c' v) v v)"
      using False Suc vs'_def by (subst finsum_insert[symmetric]) (auto)
    also have "(Vvset vs'. of_int (c' v) v v) = (Vvset vs'. of_int (c v) v v)"
      unfolding c'_def using False Suc vs'_def by (auto intro!: finsum_cong')
    finally show ?thesis
      using vs'_def by auto
  qed
  finally show ?case
    unfolding vs'_def by blast
qed (auto)

lemma lattice_of_altdef:
  assumes "set vs  carrier_vec n"
  shows "lattice_of vs = range (λc. Vvset vs. of_int (c v) v v)"
proof -
  have "v  lattice_of vs" if "v  range (λc. Vvset vs. of_int (c v) v v)" for v
  proof -
    obtain c where v: "v = (Vvset vs. of_int (c v) v v)"
      using v  range (λc. Vvset vs. of_int (c v) v v) by (auto)
    define c' where "c' i = (if find_index vs (vs ! i) = i then c (vs ! i) else 0)" for i
    have "v = (Vvset vs. of_int (c' (find_index vs v)) v vs ! (find_index vs v))"
      unfolding v
      using assms by (auto intro!: finsum_cong' simp add: c'_def find_index_in_set in_mono)
    also have " = (Vifind_index vs ` (set vs). of_int (c' i) v vs ! i)"
      using assms find_index_in_set find_index_inj by (subst finsum_reindex) fastforce+
    also have " = (Viset [0..<length vs]. of_int (c' i) v vs ! i)"
    proof -
      have "i  find_index vs ` set vs" if "i < length vs" "find_index vs (vs ! i) = i" for i
        using that by (metis imageI nth_mem)
      then show ?thesis
        unfolding c'_def using find_index_leq_length assms 
        by (intro add.finprod_mono_neutral_cong_left) (auto simp add: in_mono find_index_leq_length)
    qed
    also have " = sumlist (map (λi. of_int (c' i) v vs ! i) [0..<length vs])"
      using assms by (subst sumlist_map_as_finsum) (fastforce)+
    finally show ?thesis
      unfolding lattice_of_def by blast
  qed
  moreover have "v  range (λc. Vvset vs. of_int (c v) v v)" if "v  lattice_of vs" for v
  proof -
    obtain c where "v = sumlist (map (λi. of_int (c i) v vs ! i) [0..<length vs])"
      using v  lattice_of vs unfolding lattice_of_def by (auto)
    also have " = (Vx{0..<length vs}. of_int (c x) v vs ! x)"
      using that assms by (subst sumlist_map_as_finsum) fastforce+
    also obtain d where  " = (Vvset vs. of_int (d v) v v)"
      using finsum_over_indexes_to_vectors assms by blast
    finally show ?thesis
      by blast
  qed
  ultimately show ?thesis
    by fastforce
qed

lemma basis_in_latticeI:
  assumes fs: "set fs  carrier_vec n" and "f  set fs" 
  shows "f  lattice_of fs"
proof -
  define c :: "'a vec  int" where "c v = (if v = f then 1 else 0)" for v
  have "f = (Vv{f}. of_int (c v) v v)"
    using assms by (auto simp add: c_def)
  also have " = (Vvset fs. of_int (c v) v v)"
    using assms by (intro add.finprod_mono_neutral_cong_left) (auto simp add: c_def)
  finally show ?thesis
    using assms lattice_of_altdef by blast
qed

lemma lattice_of_eq_set:
  assumes "set fs = set gs" "set fs  carrier_vec n"
  shows "lattice_of fs = lattice_of gs"
  using assms lattice_of_altdef by simp

lemma lattice_of_swap: assumes fs: "set fs  carrier_vec n" 
  and ij: "i < length fs" "j < length fs" "i  j" 
  and gs: "gs = fs[ i := fs ! j, j := fs ! i]" 
shows "lattice_of gs = lattice_of fs"
  using assms mset_swap by (intro lattice_of_eq_set) auto

lemma lattice_of_add: assumes fs: "set fs  carrier_vec n" 
  and ij: "i < length fs" "j < length fs" "i  j" 
  and gs: "gs = fs[ i := fs ! i + of_int l v fs ! j]" 
shows "lattice_of gs = lattice_of fs"
proof -
  {
    fix i j l and fs :: "'a vec list" 
    assume *: "i < j" "j < length fs" and fs: "set fs  carrier_vec n"
    note * = ij(1) *
    let ?gs = "fs[ i := fs ! i + of_int l v fs ! j]"
    let ?len = "[0..<i] @ [i] @ [Suc i..<j] @ [j] @ [Suc j..<length fs]" 
    have "[0 ..< length fs] = [0 ..< j] @ [j] @ [Suc j ..< length fs]" using *
      by (metis append_Cons append_self_conv2 less_Suc_eq_le less_imp_add_positive upt_add_eq_append 
          upt_conv_Cons zero_less_Suc)
    also have "[0 ..< j] = [0 ..< i] @ [i] @ [Suc i ..< j]" using *
      by (metis append_Cons append_self_conv2 less_Suc_eq_le less_imp_add_positive upt_add_eq_append 
          upt_conv_Cons zero_less_Suc)
    finally have len: "[0..<length fs] = ?len" by simp
    from fs have fs: " i. i < length fs  fs ! i  carrier_vec n" unfolding set_conv_nth by auto
    from fs have fsd: " i. i < length fs  dim_vec (fs ! i) = n" by auto
    from fsd[of i] fsd[of j] * have fsd: "dim_vec (fs ! i) = n" "dim_vec (fs ! j) = n" by auto
    {
      fix f
      assume "f  lattice_of fs" 
      from in_latticeE[OF this, unfolded len] obtain c where
        f: "f = sumlist (map (λi. of_int (c i) v fs ! i) ?len)" by auto
      define sc where "sc = (λ xs. sumlist (map (λi. of_int (c i) v fs ! i) xs))"
      define d where "d = (λ k. if k = j then c j - c i * l else c k)"
      define sd where "sd = (λ xs. sumlist (map (λi. of_int (d i) v ?gs ! i) xs))"
      have isc: "set is  {0 ..< length fs}  sc is  carrier_vec n" for "is" 
        unfolding sc_def by (intro sumlist_carrier, auto simp: fs)
      have isd: "set is  {0 ..< length fs}  sd is  carrier_vec n" for "is" 
        unfolding sd_def using * by (intro sumlist_carrier, auto, rename_tac k,
        case_tac "k = i", auto simp: fs)
      let ?a = "sc [0..<i]" let ?b = "sc [i]" let ?c = "sc [Suc i ..< j]" let ?d = "sc [j]" 
      let ?e = "sc [Suc j ..< length fs]" 
      let ?A = "sd [0..<i]" let ?B = "sd [i]" let ?C = "sd [Suc i ..< j]" let ?D = "sd [j]" 
      let ?E = "sd [Suc j ..< length fs]" 
      let ?CC = "carrier_vec n" 
      have ae: "?a  ?CC" "?b  ?CC" "?c  ?CC" "?d  ?CC" "?e  ?CC"  
        using * by (auto intro: isc)
      have AE: "?A  ?CC" "?B  ?CC" "?C  ?CC" "?D  ?CC" "?E  ?CC"  
        using * by (auto intro: isd)
      have sc_sd: "{i,j}  set is  {}  sc is = sd is" for "is" 
        unfolding sc_def sd_def by (rule arg_cong[of _ _ sumlist], rule map_cong, auto simp: d_def,
        rename_tac k, case_tac "i = k", auto)
      have "f = ?a + (?b + (?c + (?d + ?e)))"         
        unfolding f map_append sc_def using fs *
        by ((subst sumlist_append, force, force)+, simp)
      also have " = ?a + ((?b + ?d) + (?c + ?e))" using ae by auto          
      also have " = ?A + ((?b + ?d) + (?C + ?E))" 
        using * by (auto simp: sc_sd)
      also have "?b + ?d = ?B + ?D" unfolding sd_def sc_def d_def sumlist_def
        by (rule eq_vecI, insert * fsd, auto simp: algebra_simps)
      finally have "f = ?A + (?B + (?C + (?D + ?E)))" using AE by auto
      also have " = sumlist (map (λi. of_int (d i) v ?gs ! i) ?len)" 
        unfolding f map_append sd_def using fs *
        by ((subst sumlist_append, force, force)+, simp)
      also have " = sumlist (map (λi. of_int (d i) v ?gs ! i) [0 ..< length ?gs])"
        unfolding len[symmetric] by simp
      finally have "f = sumlist (map (λi. of_int (d i) v ?gs ! i) [0 ..< length ?gs])" .
      from in_latticeI[OF this] have "f  lattice_of ?gs" .
    }
    hence "lattice_of fs  lattice_of ?gs" by blast
  } note main = this 
  {
    fix i j and fs :: "'a vec list" 
    assume *: "i < j" "j < length fs" and fs: "set fs  carrier_vec n"
    let ?gs = "fs[ i := fs ! i + of_int l v fs ! j]"
    define gs where "gs = ?gs" 
    from main[OF * fs, of l, folded gs_def]
    have one: "lattice_of fs  lattice_of gs" .
    have *: "i < j" "j < length gs" "set gs  carrier_vec n" using * fs unfolding gs_def set_conv_nth
      by (auto, rename_tac k, case_tac "k = i", (force intro!: add_carrier_vec)+)
    from fs have fs: " i. i < length fs  fs ! i  carrier_vec n" unfolding set_conv_nth by auto
    from fs have fsd: " i. i < length fs  dim_vec (fs ! i) = n" by auto
    from fsd[of i] fsd[of j] * have fsd: "dim_vec (fs ! i) = n" "dim_vec (fs ! j) = n" by (auto simp: gs_def)
    from main[OF *, of "-l"]
    have "lattice_of gs  lattice_of (gs[i := gs ! i + of_int (- l) v gs ! j])" .
    also have "gs[i := gs ! i + of_int (- l) v gs ! j] = fs" unfolding gs_def
      by (rule nth_equalityI, auto, insert * fsd, rename_tac k, case_tac "k = i", auto)
    ultimately have "lattice_of fs = lattice_of ?gs" using one unfolding gs_def by auto
  } note main = this
  show ?thesis
  proof (cases "i < j")
    case True
    from main[OF this ij(2) fs] show ?thesis unfolding gs by simp
  next
    case False
    with ij have ji: "j < i" by auto
    define hs where "hs = fs[i := fs ! j, j := fs ! i]" 
    define ks where "ks = hs[j := hs ! j + of_int l v hs ! i]" 
    from ij fs have ij': "i < length hs" "set hs  carrier_vec n" unfolding hs_def by auto
    hence ij'': "set ks  carrier_vec n" "i < length ks" "j < length ks" "i  j" 
      using ji unfolding ks_def set_conv_nth by (auto, rename_tac k, case_tac "k = i", 
        force, case_tac "k = j", (force intro!: add_carrier_vec)+)
    from lattice_of_swap[OF fs ij refl] 
    have "lattice_of fs = lattice_of hs" unfolding hs_def by auto
    also have " = lattice_of ks" 
      using main[OF ji ij'] unfolding ks_def .
    also have " = lattice_of (ks[i := ks ! j, j := ks ! i])" 
      by (rule sym, rule lattice_of_swap[OF ij'' refl])
    also have "ks[i := ks ! j, j := ks ! i] = gs" unfolding gs ks_def hs_def
      by (rule nth_equalityI, insert ij, auto, 
       rename_tac k, case_tac "k = i", force, case_tac "k = j", auto)
    finally show ?thesis by simp
  qed
qed

definition "orthogonal_complement W = {x. x  carrier_vec n  (y  W. x  y = 0)}"

lemma orthogonal_complement_subset:
  assumes "A  B"
  shows "orthogonal_complement B  orthogonal_complement A"
unfolding orthogonal_complement_def using assms by auto

end

context vec_space
begin


lemma in_orthogonal_complement_span[simp]:
  assumes [intro]:"S  carrier_vec n"
  shows "orthogonal_complement (span S) = orthogonal_complement S"
proof
  show "orthogonal_complement (span S)  orthogonal_complement S"
    by(fact orthogonal_complement_subset[OF in_own_span[OF assms]])
  {fix x :: "'a vec"
    fix a fix A :: "'a vec set"
    assume x [intro]:"x  carrier_vec n" and f: "finite A" and S:"A  S"
    assume i0:"yS. x  y = 0"
    have "x  lincomb a A = 0"
      unfolding comm_scalar_prod[OF x lincomb_closed[OF subset_trans[OF S assms]]]
    proof(insert S,atomize(full),rule finite_induct[OF f],goal_cases)
      case 1 thus ?case using assms x by force
    next
      case (2 f F)
      { assume i:"insert f F  S"
        hence F:"F  S" and f: "f  S" by auto
        from F f assms
        have [intro]:"F  carrier_vec n"
          and fc[intro]:"f  carrier_vec n"
          and [intro]:"x  F  x  carrier_vec n" for x by auto
        have laf:"lincomb a F  x = 0" using F 2 by auto
        have [simp]:"(uF. (a u v u)  x) = 0"
          by(insert laf[unfolded lincomb_def],atomize(full),subst finsum_scalar_prod_sum) auto
        from f i0 have [simp]:"f  x = 0" by (subst comm_scalar_prod) auto
        from lincomb_closed[OF subset_trans[OF i assms]]
        have "lincomb a (insert f F)  x = 0" unfolding lincomb_def
          apply(subst finsum_scalar_prod_sum,force,force)
          using 2(1,2) smult_scalar_prod_distrib[OF fc x] by auto
      } thus ?case by auto
      qed
  }
  thus "orthogonal_complement S  orthogonal_complement (span S)"
    unfolding orthogonal_complement_def span_def by auto
qed

end

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