# Theory Affine_Arithmetic.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
```