theory GreatestCommonDivisor
imports Main
begin

fun gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
  "gcd a b =
      (if a = 0 then
         b
       else if b = 0 then
         a
       else if a > b then 
         gcd (a - b) b
       else
         gcd a (b - a))"

definition
  greatest_common_divisor :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where
  "greatest_common_divisor p m n \<equiv> p dvd m \<and> p dvd n \<and>
    (\<forall>d. d dvd m \<longrightarrow> d dvd n \<longrightarrow> d dvd p)"
declare greatest_common_divisor_def[simp]

theorem gcd_correct:
  assumes n: "n = a + b"
  shows "greatest_common_divisor (gcd a b) a b"
  using n apply (induct n arbitrary: a b rule: nat_less_induct)
proof -
  fix n a b
  assume IH: "\<forall>m<n. \<forall>x xa.
            m = x + xa \<longrightarrow> greatest_common_divisor (gcd x xa) x xa"
    and n: "n = a + b"
  show "greatest_common_divisor (gcd a b) a b"
  proof (cases "a = 0")
    assume a: "a = 0"
    hence g: "gcd a b = b" by simp
    have x: "b dvd 0" by simp  
    have y: "b dvd b" by simp
    have z: "\<forall> d. d dvd 0 \<and> d dvd b \<longrightarrow> d dvd b" by simp
    from x y z have "greatest_common_divisor b 0 b" by simp
    with a show ?thesis by simp
  next
    assume az: "a \<noteq> 0"
    show "greatest_common_divisor (gcd a b) a b"
    proof (cases "b = 0")
      assume b: "b = 0"
      with az have g: "gcd a b = a" by (case_tac a) auto
      have x: "a dvd a" by simp
      have y: "a dvd 0" by simp  
      have z: "\<forall> d. d dvd a \<and> d dvd 0 \<longrightarrow> d dvd a" by simp
      from x y z have "greatest_common_divisor a a 0" by simp
      with b g show ?thesis by simp
    next
      assume bz: "b \<noteq> 0"
      have "a > b \<or> a \<le> b" by arith
      thus "greatest_common_divisor (gcd a b) a b"
      proof
	assume ba: "b < a"
	from az bz ba have g: "gcd a b = gcd (a - b) b"
	  apply (case_tac a) apply auto done
	let ?M = "(a - b) + b"
	from bz ba n have mn: "?M < n" by simp
	from mn IH 
	have "greatest_common_divisor (gcd (a - b) b) (a - b) b"
	  by blast
	with g have d: "greatest_common_divisor (gcd a b) (a - b) b" 
          by (simp only: g)
	from d have dab: "(gcd a b) dvd (a - b)" 
          by (simp only: greatest_common_divisor_def)
	from d have db: "(gcd a b) dvd b" 
          by (simp only: greatest_common_divisor_def)
	from ba have ba2: "b \<le> a" by simp
	from dab db ba2	have x: "(gcd a b) dvd a" by (rule dvd_diffD) 
	have z: "\<forall> d. d dvd a \<and> d dvd b \<longrightarrow> d dvd (gcd a b)"
	proof clarify
	  fix d assume da: "d dvd a" and db: "d dvd b"
	  from d have gr: "\<forall> k. k dvd (a - b) \<and> k dvd b \<longrightarrow> k dvd (gcd a b)"
            by (simp only: greatest_common_divisor_def, blast)
	  from da db have dab: "d dvd (a - b)" by (rule nat_dvd_diff)
	  from gr dab db show "d dvd (gcd a b)" by simp
	qed
	from x db z show ?thesis by simp 
      next
	assume ab: "a \<le> b"
	from az bz ab have g: "gcd a b = gcd a (b - a)"by (case_tac a) auto
	let ?M = "a + (b - a)"
	from az ab n have mn: "?M < n" by simp
	from mn IH 
	have "greatest_common_divisor (gcd a (b - a)) a (b - a)" by blast
	with g have g2: "greatest_common_divisor (gcd a b) a (b - a)" 
          by (simp only: greatest_common_divisor_def) blast
        from g2 have gcd_div_a: "gcd a b dvd a"
	  by (simp only: greatest_common_divisor_def)
        from g2 ab have gcd_div_b: "gcd a b dvd b"
	  apply (simp only: greatest_common_divisor_def)
          apply (rule dvd_diffD) apply blast+ done
        have greatest: "\<forall>d. d dvd a \<longrightarrow> d dvd b \<longrightarrow> d dvd gcd a b"
        proof clarify
          fix d assume diva: "d dvd a" and divb: "d dvd b"
          from divb diva have divba: "d dvd (b - a)" by (rule nat_dvd_diff)
          from divba diva g2 show "d dvd (gcd a b)"
            by (simp only: greatest_common_divisor_def)
        qed
	from gcd_div_a gcd_div_b greatest show ?thesis
	  by (simp only: greatest_common_divisor_def) blast
      qed
    qed
  qed
qed

end