Theory Affine_Arithmetic_Auxiliarities

theory Affine_Arithmetic_Auxiliarities
imports "HOL-Analysis.Multivariate_Analysis"
begin

subsection ‹@{term sum_list}›

lemma sum_list_nth_eqI:
  fixes xs ys::"'a::monoid_add list"
  shows
    "length xs = length ys ⟹ (⋀x y. (x, y) ∈ set (zip xs ys) ⟹ x = y) ⟹
      sum_list xs = sum_list ys"
  by (induct xs ys rule: list_induct2) auto

lemma fst_sum_list: "fst (sum_list xs) = sum_list (map fst xs)"
  by (induct xs) auto

lemma snd_sum_list: "snd (sum_list xs) = sum_list (map snd xs)"
  by (induct xs) auto

lemma take_greater_eqI: "take c xs = take c ys ⟹ c ≥ a ⟹ take a xs = take a ys"
proof (induct xs arbitrary: a c ys)
  case (Cons x xs) note ICons = Cons
  thus ?case
  proof (cases a)
    case (Suc b)
    thus ?thesis using Cons(2,3)
    proof (cases ys)
      case (Cons z zs)
      from ICons obtain d where c: "c = Suc d"
        by (auto simp: Cons Suc dest!: Suc_le_D)
      show ?thesis
        using ICons(2,3)
        by (auto simp: Suc Cons c intro: ICons(1))
    qed simp
  qed simp
qed (metis le_0_eq take_eq_Nil)

lemma take_max_eqD:
  "take (max a b) xs = take (max a b) ys ⟹ take a xs = take a ys ∧ take b xs = take b ys"
  by (metis max.cobounded1 max.cobounded2 take_greater_eqI)

lemma take_Suc_eq: "take (Suc n) xs = (if n < length xs then take n xs @ [xs ! n] else xs)"
  by (auto simp: take_Suc_conv_app_nth)


subsection ‹Radiant and Degree›

definition "rad_of w = w * pi / 180"

definition "deg_of w = 180 * w / pi"

lemma rad_of_inverse[simp]: "deg_of (rad_of w) = w"
  and deg_of_inverse[simp]: "rad_of (deg_of w) = w"
  by (auto simp: deg_of_def rad_of_def)

lemma deg_of_monoI: "x ≤ y ⟹ deg_of x ≤ deg_of y"
  by (auto simp: deg_of_def intro!: divide_right_mono)

lemma rad_of_monoI: "x ≤ y ⟹ rad_of x ≤ rad_of y"
  by (auto simp: rad_of_def)

lemma deg_of_strict_monoI: "x < y ⟹ deg_of x < deg_of y"
  by (auto simp: deg_of_def intro!: divide_strict_right_mono)

lemma rad_of_strict_monoI: "x < y ⟹ rad_of x < rad_of y"
  by (auto simp: rad_of_def)

lemma deg_of_mono[simp]: "deg_of x ≤ deg_of y ⟷ x ≤ y"
  using rad_of_monoI
  by (fastforce intro!: deg_of_monoI)

lemma rad_of_mono[simp]: "rad_of x ≤ rad_of y ⟷ x ≤ y"
  using rad_of_monoI
  by (fastforce intro!: deg_of_monoI)

lemma deg_of_strict_mono[simp]: "deg_of x < deg_of y ⟷ x < y"
  using rad_of_strict_monoI
  by (fastforce intro!: deg_of_strict_monoI)

lemma rad_of_strict_mono[simp]: "rad_of x < rad_of y ⟷ x < y"
  using rad_of_strict_monoI
  by (fastforce intro!: deg_of_strict_monoI)

lemma rad_of_lt_iff: "rad_of d < r ⟷ d < deg_of r"
  and rad_of_gt_iff: "rad_of d > r ⟷ d > deg_of r"
  and rad_of_le_iff: "rad_of d ≤ r ⟷ d ≤ deg_of r"
  and rad_of_ge_iff: "rad_of d ≥ r ⟷ d ≥ deg_of r"
  using rad_of_strict_mono[of d "deg_of r"] rad_of_mono[of d "deg_of r"]
  by auto

end