theory a3q1_2010
imports Main
begin

-- "Question 1"

fun gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat"
where
  "gcd x 0 = x"
| "gcd 0 y = y"
| "gcd (Suc x) (Suc y) = (if x < y then gcd (Suc x) (y - x)
                                   else gcd (x - y) (Suc y))"

-- "1 (a)"

thm mod_if 
thm dvd_mod_iff
thm algebra_simps

lemma gcd_divides:
  "gcd a b dvd b \<and> gcd a b dvd a"
thm gcd.induct
  apply (induct a b  rule:gcd.induct)
    apply simp
   apply simp
  apply simp
  apply (rule conjI)
  apply clarsimp
  apply (simp add: dvd_def)
  apply clarsimp
  apply (rule_tac x="k+ka"  in exI)
  apply (clarsimp simp: algebra_simps)
 apply clarsimp
 apply (clarsimp  simp: dvd_def)
 apply (rule_tac x="k + ka" in exI)
 apply (clarsimp simp: algebra_simps)
done


-- "1 (b)"

fun gcd2 :: "nat \<Rightarrow> nat \<Rightarrow> nat"
where
  "gcd2 x 0 = x"
| "gcd2 x y = gcd2 y (x mod y)"

lemma gcd_zero [simp]:
  "gcd 0 x = x"
  by (cases x, auto)


lemma gcd_commute:
  "gcd a b = gcd b a"
  by (induct a b rule:gcd.induct, auto)

lemma gcd_mod:
  "gcd a (b mod a) = gcd a b"
  apply (induct a b rule:gcd.induct)
    apply simp
   apply simp
  apply simp
  apply (rule conjI) 
   apply clarsimp thm mod_if
   apply (simp add: mod_if)
  apply (clarsimp simp: mod_if)
done


lemma gcd_equiv:
  "gcd2 a b = gcd a b"
  apply (induct a b rule:gcd2.induct) 
   apply simp
  apply (simp add: gcd_mod gcd_commute)
done



lemma gcd_greatest:
  "\<lbrakk> z dvd a; z dvd b \<rbrakk> \<Longrightarrow> z dvd gcd a b" thm gcd_equiv thm gcd_equiv[symmetric]
  apply (simp add: gcd_equiv[symmetric])
  apply (induct a b rule: gcd2.induct)
   apply simp
  apply simp thm dvd_mod_iff
  apply (simp add: dvd_mod_iff)
done


value "gcd 9 12"
value "gcd2 9 12"

value "gcd 139328 1262968"
value "gcd2 139328 1262968"

end