gcd.thy

theory gcd
  imports Main
begin

fun gcd :: "nat ⇒ nat ⇒ nat" where
  "gcd a 0 = a" |
  "gcd a b = gcd b (a mod b)"

lemma div_mod_eq:
  fixes a b :: nat
  shows "int b * int (a div b) + int (a mod b) = int a"
  using zdiv_int [of a b] zmod_int [of a b]
  using mult_div_mod_eq [of "int b" "int a"]
  by simp

lemma gcd_dvd_sum:
  fixes a b :: nat and m n :: int
  shows "int (gcd a b) dvd (m * int a + n * int b)"
proof (induction a b arbitrary: m n rule: gcd.induct)
  case (1 a) show ?case by simp
next
  case (2 a c)
  let ?b = "Suc c"
  from "2.IH" [of "n + m * int (a div ?b)" m]
  have "int (gcd a ?b) dvd
      (n + m * int (a div ?b)) * int ?b + m * int (a mod ?b)"
    by simp
  hence "int (gcd a ?b) dvd
      m * (int ?b * int (a div ?b) + int (a mod ?b)) +
      n * int ?b"
    by (simp add: algebra_simps)
  thus ?case using div_mod_eq [of ?b a] by simp
qed

lemma gcd_eq_sum:
  fixes a b :: nat
  shows "∃m n :: int.
    int (gcd a b) = m * int a + n * int b"
proof (induction a b rule: gcd.induct)
  case (1 a) show ?case by auto
next
  case (2 a c)
  let ?b = "Suc c"
  have "int (a mod ?b) = int a - int ?b * int (a div ?b)"
    using div_mod_eq [of ?b a]
    by (simp add: algebra_simps)
  moreover
  from "2.IH" obtain n m :: int where
    "int (gcd a ?b) = m * int ?b + n * int (a mod ?b)"
    by auto
  ultimately
  have "int (gcd a ?b) = m * int ?b +
      n * (int a - int ?b * int (a div ?b))"
    by simp
  hence "int (gcd a ?b) = n * int a +
      (m - n * int (a div ?b)) * int ?b"
    by (simp add: algebra_simps)
  then show ?case by blast
qed

lemma dvd_mult:
  fixes a b r k :: nat
  assumes "a ≠ 0" and "r dvd (a * b)" and "r = (gcd r a) * k"
  shows "k dvd b"
proof (cases "r = 0")
  case True
  thus ?thesis using assms by simp
next
  case False
  note c = False
  obtain l :: nat
    where "a * b = r * l" using assms by blast
  hence "int a * int b = int r * int l"
    using int_ops(7) [of a b] by simp
  moreover obtain n m :: int
    where "int (gcd r a) = n * int r + m * int a"
    using gcd_eq_sum [of r a] by blast
  ultimately have
    "int (gcd r a) * int b = int r * (n * int b + m * int l)"
    by (simp add: algebra_simps)
  hence "int b = int k * (n * int b + m * int l)"
    using assms c int_ops(7) [of "gcd r a" k] by auto
  hence "(int k) dvd (int b)"
    unfolding dvd_def
    by (rule_tac x = "n * int b + m * int l" in exI)
  thus ?thesis by simp
qed

definition dvd_set :: "nat ⇒ nat set" where
  "dvd_set n = {d. d dvd n}"

lemma dvd_set_mult:
  fixes a b :: nat
  assumes "A = dvd_set a"
    and "B = dvd_set b"
    and "AB = {a * b | a b. a ∈ A ∧ b ∈ B}"
  shows "AB = dvd_set (a * b)"
proof -
  have "⋀d. d ∈ AB ⟹ d dvd (a * b)" sorry
  moreover
  have "⋀d. d dvd (a * b) ⟹ d ∈ AB" sorry
  ultimately
  show ?thesis unfolding dvd_set_def by blast
qed

definition sigma :: "nat ⇒ nat" where
  "sigma n = (let
     ds = filter (λd. d dvd n) [1 ..< Suc n] in
     foldr (+) ds 0)"

lemma sigma_prod:
  fixes a b :: nat
  assumes "gcd a b = 1"
  shows "sigma (a * b) = sigma a * sigma b"
  sorry

end

gcd_1.thy

theory gcd_1
  imports Main
begin

fun gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
  "gcd a 0 = a" |
  "gcd a b = gcd b (a mod b)"

lemma div_mod_eq:
  fixes a b :: nat
  shows "int b * int (a div b) + int (a mod b) = int a"
  using zdiv_int [of a b] zmod_int [of a b]
  using mult_div_mod_eq [of "int b" "int a"]
  by simp

lemma gcd_dvd_sum:
  fixes a b :: nat and m n :: int
  shows "int (gcd a b) dvd (m * int a + n * int b)"
proof (induction a b arbitrary: m n rule: gcd.induct)
  case (1 a) show ?case by simp
next
  case (2 a c)
  let ?b = "Suc c"
  from "2.IH" [of "n + m * int (a div ?b)" m]
  have "int (gcd a ?b) dvd
      (n + m * int (a div ?b)) * int ?b + m * int (a mod ?b)"
    by simp
  hence "int (gcd a ?b) dvd
      m * (int ?b * int (a div ?b) + int (a mod ?b)) +
      n * int ?b"
    by (simp add: algebra_simps)
  thus ?case using div_mod_eq [of ?b a] by simp
qed

lemma gcd_eq_sum:
  fixes a b :: nat
  shows "\<exists>m n :: int.
    int (gcd a b) = m * int a + n * int b"
proof (induction a b rule: gcd.induct)
  case (1 a) show ?case by auto
next
  case (2 a c)
  let ?b = "Suc c"
  have "int (a mod ?b) = int a - int ?b * int (a div ?b)"
    using div_mod_eq [of ?b a]
    by (simp add: algebra_simps)
  moreover
  from "2.IH" obtain n m :: int where
    "int (gcd a ?b) = m * int ?b + n * int (a mod ?b)"
    by auto
  ultimately
  have "int (gcd a ?b) = m * int ?b +
      n * (int a - int ?b * int (a div ?b))"
    by simp
  hence "int (gcd a ?b) = n * int a +
      (m - n * int (a div ?b)) * int ?b"
    by (simp add: algebra_simps)
  then show ?case by blast
qed

lemma dvd_mult:
  fixes a b r k :: nat
  assumes "a \<noteq> 0" and "r dvd (a * b)" and "r = (gcd r a) * k"
  shows "k dvd b"
proof (cases "r = 0")
  case True
  thus ?thesis using assms by simp
next
  case False
  note c = False
  obtain l :: nat
    where "a * b = r * l" using assms by blast
  hence "int a * int b = int r * int l"
    using int_ops(7) [of a b] by simp
  moreover obtain n m :: int
    where "int (gcd r a) = n * int r + m * int a"
    using gcd_eq_sum [of r a] by blast
  ultimately have
    "int (gcd r a) * int b = int r * (n * int b + m * int l)"
    by (simp add: algebra_simps)
  hence "int b = int k * (n * int b + m * int l)"
    using assms c int_ops(7) [of "gcd r a" k] by auto
  hence "(int k) dvd (int b)"
    unfolding dvd_def
    by (rule_tac x = "n * int b + m * int l" in exI)
  thus ?thesis by simp
qed

definition dvd_set :: "nat \<Rightarrow> nat set" where
  "dvd_set n = {d. d dvd n}"

lemma dvd_set_mult:
  fixes a b :: nat
  assumes "A = dvd_set a"
    and "B = dvd_set b"
    and "AB = {a * b | a b. a \<in> A \<and> b \<in> B}"
  shows "AB = dvd_set (a * b)"
proof -
  have "\<And>d. d \<in> AB \<Longrightarrow> d dvd (a * b)" sorry
  moreover
  have "\<And>d. d dvd (a * b) \<Longrightarrow> d \<in> AB" sorry
  ultimately
  show ?thesis unfolding dvd_set_def by blast
qed

definition sigma :: "nat \<Rightarrow> nat" where
  "sigma n = (let
     ds = filter (\<lambda>d. d dvd n) [1 ..< Suc n] in
     foldr (+) ds 0)"

lemma sigma_prod:
  fixes a b :: nat
  assumes "gcd a b = 1"
  shows "sigma (a * b) = sigma a * sigma b"
  sorry

end