Theory Commuting_Hermitian_Misc

(*
Author: 
  Mnacho Echenim, Université Grenoble Alpes
*)

theory Commuting_Hermitian_Misc imports "Jordan_Normal_Form.Matrix"

begin
section ‹Misc›

fun n_sum where
  "n_sum 0 l = 0"
| "n_sum (Suc n) l = (hd l) + (n_sum n (tl l))"

lemma n_sum_last:
  fixes l::"'a::{comm_monoid_add} list"
  assumes "i < length l"
  shows "n_sum (Suc i) l = n_sum i l + l!i" using assms
proof (induct i arbitrary:l)
  case 0
  hence "l = hd l # tl l" by simp
  then show ?case
    using "0.prems" hd_conv_nth by auto
next
  case (Suc i)
  hence "n_sum (Suc (Suc i)) l = hd l + n_sum (Suc i) (tl l)" by simp
  also have "... = hd l + n_sum i (tl l) + tl l!i" using Suc
    by (metis Groups.add_ac(1) drop_Suc drop_eq_Nil2 leD leI) 
  also have "... = n_sum (Suc i) l + tl l!i" by simp
  also have "... = n_sum (Suc i) l + l!(Suc i)"
    by (metis Suc(2) Suc_lessD hd_Cons_tl list.sel(2) nth_Cons_Suc nth_tl) 
  finally show ?case .
qed

lemma n_sum_last_lt:
  fixes l::"'a::{comm_monoid_add, ordered_cancel_ab_semigroup_add} list"
  assumes "j < l!i"
  and "i < length l"
  shows "n_sum i l + j < n_sum (Suc i) l"
proof -
  have "n_sum i l + j < n_sum i l + l!i" 
    using assms add_strict_left_mono[of j "l!i"] by simp
  also have "... = n_sum (Suc i) l" using n_sum_last[of i l] assms 
    by simp
  finally show ?thesis .
qed

lemma sum_list_tl_leq:
  assumes "sum_list l ≤ (n::nat)"
  and "l≠ []"
  and "hd l ≤ n"
  shows "sum_list (tl l) ≤ n - hd l"
proof -
  have "hd l + sum_list (tl l) = sum_list l" using assms
    by (metis list.exhaust_sel sum_list_simps(2))
  also have "... ≤ n" using assms by simp
  finally have "hd l + sum_list (tl l) ≤ n" .
  thus ?thesis by simp
qed

lemma diag_mat_length:
  shows "length (diag_mat A) = dim_row A" unfolding diag_mat_def by simp

lemma sum_list_geq_tl:
  fixes l::"'a::{comm_monoid_add, ordered_ab_semigroup_add_imp_le} list"
  assumes  "l≠[]"
  and "∀j < length l. 0 ≤ l!j"
shows "sum_list (tl l) ≤ sum_list l" using assms
proof (induct l)
  case Nil
  then show ?case by simp
next
  case (Cons a l)
  hence "0 ≤ a"
    by (metis length_greater_0_conv nth_Cons_0)
  have "sum_list (tl (a#l)) = sum_list l" by simp
  also have "... ≤ a + sum_list l" using ‹0 ≤ a›
    by (metis add_0 add_le_cancel_right)
  also have "... = sum_list (a#l)" by simp
  finally show ?case .
qed

lemma sum_list_geq_0:
  fixes l::"'a::{comm_monoid_add, ordered_ab_semigroup_add_imp_le} list"
  assumes  "l≠[]"
  and "∀j < length l. 0 ≤ l!j"
shows "0 ≤ sum_list l" using assms
proof (induct l)
  case Nil
  then show ?case by simp
next
  case (Cons a l)
  hence "0 ≤ a"
    by (metis length_greater_0_conv nth_Cons_0)
  show ?case
  proof (cases "l = []")
    case True
    hence "sum_list (a#l) = a" by simp
    then show ?thesis using ‹0 ≤ a› by simp
  next
    case False
    hence "0 ≤ sum_list l" using Cons by force
    also have "... = sum_list (tl (a#l))" by simp
    also have "... ≤ sum_list (a#l)" using sum_list_geq_tl Cons by metis
    finally show ?thesis .
  qed
qed

lemma sum_list_cong:
  assumes "length l = length m"
  and "∀i < length l. l!i = m!i"
shows "sum_list l = sum_list m" using assms
proof (induct l arbitrary: m)
  case Nil
  then show ?case by simp
next
  case (Cons a l)
  hence "0 < length m" by auto
  hence "m = hd m # (tl m)" by simp
  have "sum_list (a#l) = a + sum_list l" by simp
  also have "... = hd m + sum_list l" using Cons
    by (metis ‹0 < length m› ‹m = hd m # tl m› nth_Cons_0)
  also have "... = hd m + sum_list (tl m)"
    by (metis Cons.prems(1) Cons.prems(2) ‹m = hd m # tl m› 
        calculation nth_equalityI sum_list.Cons) 
  also have "... = sum_list m"
    by (metis ‹m = hd m # tl m› sum_list.Cons)
  finally show ?case .
qed

lemma n_sum_sum_list:
  fixes l::"'a::{comm_monoid_add, ordered_ab_semigroup_add_imp_le} list"
  assumes "i ≤ length l"
  and "∀j < length l. 0 ≤ l!j"
  shows "n_sum i l ≤ sum_list l" using assms
proof (induct i arbitrary: l)
  case 0
  then show ?case
    by (metis n_sum.simps(1) order.eq_iff sum_list_geq_0 sum_list_simps(1))   
next
  case (Suc i)
  hence "1 ≤ length l" by presburger
  hence "l = hd l#(tl l)"
    by (metis hd_Cons_tl list.size(3) rel_simps(45))
  have "n_sum (Suc i) l ≤ hd l + sum_list (tl l)" 
  proof -
    have "n_sum i (tl l) ≤ sum_list (tl l)"
    proof (rule Suc(1))
      show "i ≤ length (tl l)" using Suc by simp
      show "∀j<length (tl l). 0 ≤ tl l ! j" using Suc
        by (metis Nitpick.size_list_simp(2) le_simps(3) nth_tl 
            verit_comp_simplify1(3) zero_less_Suc) 
    qed
    thus ?thesis by simp
  qed
  also have "... = sum_list l"
    by (metis ‹l = hd l # tl l› sum_list.Cons) 
  finally show ?case .
qed

lemma map2_commute:
  assumes "length l = length m"
  and "∀i < length l. f (l!i) (m!i) = f (m!i) (l!i)"
shows "map2 f l m = map2 f m l" using assms
proof (induct l arbitrary: m)
  case Nil
  then show ?case by simp
next
  case (Cons a l)
  hence "0 < length m" by auto
  hence "m = hd m#(tl m)" by simp
  hence "map2 f (a#l) m = f a (hd m) # (map2 f l (tl m))"
    by (metis (no_types, lifting) list.map(2) prod.simps(2) zip_Cons_Cons) 
  also have "... = f (hd m) a # (map2 f l (tl m))" using Cons
    by (metis ‹0 < length m› ‹m = hd m # tl m› nth_Cons_0)
  also have "... = f (hd m) a # (map2 f (tl m) l)" using Cons
    by (metis Suc_less_eq ‹m = hd m # tl m› length_Cons nat.simps(1) 
        nth_Cons_Suc)
  also have "... = map2 f m (a#l)"
    by (metis (no_types, lifting) Cons_eq_map_conv ‹m = hd m # tl m› 
        prod.simps(2) zip_Cons_Cons)
  finally show ?case .
qed

lemma map2_length:
  assumes "length Al = length Bl"
  shows "length (map2 f Al Bl) = length Al" using assms by simp


end