# Theory Basics

```section ‹Basic Results›

theory Basics
imports
HOL.Set_Interval
HOL.Semiring_Normalization
HOL.Real_Vector_Spaces
HOL.Power
HOL.Complex
Jordan_Normal_Form.Jordan_Normal_Form
begin

subsection ‹Basic Set-Theoretic Results›

lemma set_2_atLeast0 [simp]: "{0..<2::nat} = {0,1}" by auto

lemma set_2: "{..<2::nat} = {0,1}" by auto

lemma set_4_atLeast0 [simp]:"{0..<4::nat} = {0,1,2,3}" by auto

lemma set_4: "{..<4::nat} = {0,1,2,3}" by auto

lemma set_4_disj [simp]:
fixes i:: nat
assumes "i < 4"
shows "i = 0 ∨ i = 1 ∨ i = 2 ∨ i = 3"
using assms by auto

lemma set_8_atLeast0 [simp]: "{0..<8::nat} = {0,1,2,3,4,5,6,7}" by auto

lemma index_is_2 [simp]: "∀i::nat. i ≠ Suc 0 ⟶ i ≠ 3 ⟶ 0 < i ⟶ i < 4 ⟶ i = 2" by simp

lemma index_sl_four [simp]: "∀i::nat. i < 4 ⟶ i = 0 ∨ i = 1 ∨ i = 2 ∨ i = 3" by auto

subsection ‹Basic Arithmetic Results›

lemma index_div_eq [simp]:
fixes i::nat
shows "i∈{a*b..<(a+1)*b} ⟹ i div b = a"
proof-
fix i::nat
assume a:"i∈{a*b..<(a+1)*b}"
then have "i div b ≥ a"
by (metis Suc_eq_plus1 atLeastLessThan_iff le_refl semiring_normalization_rules(7) split_div')
moreover have "i div b < a+1"
using a by (simp add: less_mult_imp_div_less)
ultimately show "i div b = a" by simp
qed

lemma index_mod_eq [simp]:
fixes i::nat
shows "i∈{a*b..<(a+1)*b} ⟹ i mod b = i-a*b"

lemma sqr_of_cmod_of_prod:
shows "(cmod (z1 * z2))⇧2 = (cmod z1)⇧2 * (cmod z2)⇧2"

fixes i m n:: nat
assumes "i < 2^(m+n)"
shows "i div 2^n < 2^m"

lemma div_mult_mod_eq_minus:
fixes i j:: nat
shows "(i div 2^n) * 2^n + i mod 2^n - (j div 2^n) * 2^n - j mod 2^n = i - j"

lemma neq_imp_neq_div_or_mod:
fixes i j:: nat
assumes "i ≠ j"
shows "i div 2^n ≠ j div 2^n ∨ i mod 2^n ≠ j mod 2^n"
using assms div_mult_mod_eq_minus

lemma index_one_mat_div_mod:
assumes "i < 2^(m+n)" and "j < 2^(m+n)"
shows "((1⇩m(2^m) \$\$ (i div 2^n, j div 2^n))::complex) * 1⇩m(2^n) \$\$ (i mod 2^n, j mod 2^n) = 1⇩m(2^(m+n)) \$\$ (i, j)"
proof (cases "i = j")
case True
then show ?thesis by(simp add: assms)
next
case c1:False
have "i div 2^n ≠ j div 2^n ∨ i mod 2^n ≠ j mod 2^n"
using c1 neq_imp_neq_div_or_mod by simp
then have "1⇩m (2^m) \$\$ (i div 2^n, j div 2^n) = 0 ∨ 1⇩m (2^n) \$\$ (i mod 2^n, j mod 2^n) = 0"
using assms by simp
then show ?thesis
using assms by (simp add: c1)
qed

lemma sqr_of_sqrt_2 [simp]:
fixes z:: "complex"
shows "z * 2 / (complex_of_real (sqrt 2) * complex_of_real (sqrt 2)) = z"
by(metis nonzero_mult_div_cancel_right norm_numeral of_real_numeral of_real_power power2_eq_square
real_norm_def real_sqrt_abs real_sqrt_power zero_neq_numeral)

lemma two_div_sqrt_two [simp]:
shows "2 * complex_of_real (sqrt (1/2)) = complex_of_real (sqrt 2)"
by (metis divide_eq_0_iff nonzero_mult_div_cancel_left sqr_of_sqrt_2)

lemma two_div_sqr_of_cmd_sqrt_two [simp]:
shows "2 * (cmod (1 / complex_of_real (sqrt 2)))⇧2 = 1"
using cmod_def by (simp add: power_divide)

lemma two_div_two [simp]:
shows "2 div Suc (Suc 0) = 1" by simp

lemma two_mod_two [simp]:
shows "2 mod Suc (Suc 0) = 0" by (simp add: numeral_2_eq_2)

lemma three_div_two [simp]:
shows "3 div Suc (Suc 0) = 1" by (simp add: numeral_3_eq_3)

lemma three_mod_two [simp]:
shows "3 mod Suc (Suc 0) = 1" by (simp add: mod_Suc numeral_3_eq_3)

subsection ‹Basic Results on Matrices›

lemma index_matrix_prod [simp]:
assumes "i < dim_row A" and "j < dim_col B" and "dim_col A = dim_row B"
shows "(A * B) \$\$ (i,j) = (∑k<dim_row B. (A \$\$ (i,k)) * (B \$\$ (k,j)))"
using assms

subsection ‹Basic Results on Sums›

lemma sum_insert [simp]:
assumes "x ∉ F" and "finite F"
shows "(∑y∈insert x F. P y) = (∑y∈F. P y) + P x"

lemma sum_of_index_diff [simp]:
shows "(∑i∈{a..<a+b}. f(i-a)) = (∑i∈{..<b}. f(i))"
proof (induction b)
case 0
then show ?case by simp
next
case (Suc b)
then show ?case by simp
qed

subsection ‹Basic Results Involving the Exponential Function.›

lemma exp_of_real_cnj:
fixes x ::real
shows "cnj (exp (𝗂 * x)) = exp (-(𝗂 * x))"
proof
show "Re (cnj (exp (𝗂 * x))) = Re (exp (-(𝗂 * x)))"
using Re_exp by simp
show "Im (cnj (exp (𝗂 * x))) = Im (exp (-(𝗂 * x)))"
using Im_exp by simp
qed

lemma exp_of_real_cnj2:
fixes x ::real
shows "cnj (exp (-(𝗂 * x))) = exp (𝗂 * x)"
proof
show "Re (cnj (exp (-(𝗂 * x)))) = Re (exp (𝗂 * x))"
using Re_exp by simp
show "Im (cnj (exp (-(𝗂 * x)))) = Im (exp (𝗂 * x))"
using Im_exp by simp
qed

lemma exp_of_half_pi:
fixes x:: real
assumes "x = pi/2"
shows "exp (𝗂 * complex_of_real x) = 𝗂"
using assms cis_conv_exp cis_pi_half by fastforce

lemma exp_of_minus_half_pi:
fixes x:: real
assumes "x = pi/2"
shows "exp (-(𝗂 * complex_of_real x)) = -𝗂"
using assms cis_conv_exp cis_minus_pi_half by fastforce

lemma exp_of_real:
fixes x:: real
shows "exp (𝗂 * x) = cos x + 𝗂 * (sin x)"
proof
show "Re (exp (𝗂 * x)) = Re ((cos x) + 𝗂 * (sin x))"
using Re_exp by simp
show "Im (exp (𝗂 * x)) = Im ((cos x) + 𝗂 * (sin x))"
using Im_exp by simp
qed

lemma exp_of_real_inv:
fixes x:: real
shows "exp (-(𝗂 * x)) = cos x - 𝗂 * (sin x)"
proof
show "Re (exp (-(𝗂 * x))) = Re ((cos x) - 𝗂 * (sin x))"
using Re_exp by simp
show "Im (exp (-(𝗂 * x))) = Im ((cos x) - 𝗂 * (sin x))"
using Im_exp by simp
qed

subsection ‹Basic Results with Trigonometric Functions.›

subsubsection ‹Basic Inequalities›

lemma sin_squared_le_one:
fixes x:: real
shows "(sin x)⇧2 ≤ 1"
using abs_sin_le_one abs_square_le_1 by blast

lemma cos_squared_le_one:
fixes x:: real
shows "(cos x)⇧2 ≤ 1"
using abs_cos_le_one abs_square_le_1 by blast

subsubsection ‹Basic Equalities›

lemma sin_of_quarter_pi:
fixes x:: real
assumes "x = pi/2"
shows "sin (x/2) = (sqrt 2)/2"
by (auto simp add: assms sin_45)

lemma cos_of_quarter_pi:
fixes x:: real
assumes "x = pi/2"
shows "cos (x/2) = (sqrt 2)/2"
by (auto simp add: assms cos_45)

end```