theory Brojevi
  imports Complex_Main
begin

(*
complex C
real    R
rat     Q
int     Z
nat     N0
*)

thm power2_eq_square
lemma
  fixes x y :: real
  shows "(x + y)\<^sup>2 = x * x + 2 * x * y + y * y"
  by (auto simp add: power2_eq_square algebra_simps)


lemma
  fixes x y z w :: real
  shows "(x + y) * (x + z) = x\<^sup>2 + x * (y + z) + y * z"
proof-
  have "(x + y) * (x + z) = x * (x + z) + y * (x + z)"
    using [[show_types]]
    by (subst distrib_right, rule refl)
  also have "\<dots> = (x * x + x * z) + y * (x + z)"
    by (subst distrib_left, rule refl)
  also have "\<dots> = (x * x + x * z) + (y * x + y * z)"
    by (subst distrib_left, rule refl)
  also have "\<dots> = x * x + (x * z + (y * x + y * z))"
    by (subst add.assoc, rule refl)
  also have "\<dots> = x * x + ((x * z + y * x) + y * z)"
    by (subst add.assoc, rule refl)
  also have "\<dots> = x * x + ((x * z + x * y) + y * z)"
    by (subst mult.commute[where a=y and b=x], rule refl)
  also have "\<dots> = x * x + (x * (z + y) + y * z)"
    by (subst distrib_left, rule refl)
  also have "\<dots> = x * x + x * (z + y) + y * z"
    by (subst add.assoc, rule refl)
  also have "\<dots> = x\<^sup>2 + x * (z + y) + y * z"
    by (subst power2_eq_square, rule refl)
  also have "\<dots> = x\<^sup>2 + x * (y + z) + y * z"
    by (subst add.commute[of z y], rule refl)
  finally
  show ?thesis
    .
qed

thm distrib_left
thm distrib_left[symmetric]

thm field_simps
lemma
  fixes a b c d :: real
  assumes "a / b = c / d" "b \<noteq> 0" "d \<noteq> 0"
  shows "a*d = b*c"
  using assms
  by (auto simp add: field_simps)

(* Paziti se operacije - kada se radi sa prirodnim brojevima *)

value "(5::nat) - (3::nat)"
value "(3::nat) - (5::nat)"

lemma 
  fixes x y z :: nat
  assumes "x \<ge> y" "y \<ge> z"
  shows "(x - y) + (y - z) = x - z"
  using assms
  by auto


(* Indukcija nad prirodnim brojevima *)
(* 1 + 2 + ... + n = n * (n + 1) / 2 *)

value "(13::nat) div (5::nat)"
value "(13::nat) mod (5::nat)" 
(* 13 = 5 * 2 + 3 *)

value "[1..<11]"

value "sum_list ([1..<11]::nat list)"

lemma "sum_list [1..<n+1] = n * (n + 1) div 2"
proof (induction n)
  case 0
  then show ?case
    by auto
next
  case (Suc n)
  have "sum_list [1..<Suc n + 1] = sum_list [1..<n + 1] + Suc n"
    by auto
  also have "\<dots> = n * (n + 1) div 2 + (n + 1)"
    by (subst Suc, auto)
  also have "\<dots> = (n * (n + 1) + 2 * (n + 1)) div 2"
    by auto
  also have "\<dots> = (n + 1) * (n + 2) div 2"
    by auto
  finally    
  show ?case
    by auto
qed


end