tests/PGCD/PGCD_PGCD_gcd_a_b_1.thy

   1 theory PGCD_PGCD_gcd_a_b_1
   2 imports Why3
   3 begin
   4
   5 why3_open "PGCD_PGCD_gcd_a_b_1.xml"
   6
   7 why3_vc gcd_a_b
   8 proof -
   9   from assms have "common_div (a-b) b k" using is_gcd_def by simp
  10   then have 1: "common_div a b k" using common_div_a_b by simp
  11   (* show that any other common divisor of a and b divides k *)
  12   { fix p
  13     assume h: "common_div a b p"
  14     hence "\<exists>ka kb::int. (a = ka * p) \<and> (b = kb * p)" using common_div_def and divides_def by simp
  15     then obtain ka kb where "a = ka * p" and "b = kb * p" by auto
  16     hence "a - b = (ka - kb) * p" using int_distrib by simp
  17     hence "divides p (a-b)"  using divides_def by simp
  18     hence "common_div (a-b) b p" using h and common_div_def by simp
  19     hence "divides p k" using assms and is_gcd_def by simp
  20   }
  21   hence "\<forall>p::int. common_div a b p \<longrightarrow> divides p k" by simp
  22   thus "is_gcd a b k" using 1 and is_gcd_def by simp
  23 qed
  24
  25 why3_end
  26
  27 end