tests/PGCD.mlw

   1 module PGCD
   2   use int.Int
   3   use ref.Refint
   4   use int.EuclideanDivision
   5
   6   predicate divides (m: int) (n: int) =
   7     exists k: int. n = k * m
   8
   9   predicate common_div (m:int) (n:int) (cd:int) =
  10     divides cd m /\ divides cd n
  11
  12   predicate is_gcd (m: int) (n: int) (gcd: int) =
  13     common_div m n gcd /\ (forall d: int. common_div m n d -> divides d gcd)
  14
  15   lemma is_gcd_self: (* Proof by iProver or Spass *)
  16     forall n: int. is_gcd n n n
  17
  18   lemma common_div_a_b:
  19     forall a b k:int. common_div (a-b) b k -> common_div a b k
  20   (* Isabelle proof
  21 proof -
  22   from assms have "\<exists>pa pb::int. (a-b) = pa * k \<and> b = pb * k" using common_div_def and divides_def by simp
  23   then obtain pa pb where "(a-b) = pa * k" and "b = pb * k" by auto
  24   hence "a-b+b = pa * k + pb * k" by simp
  25   hence "a = (pa + pb) * k" using Mul_distr_r by simp
  26   hence "divides k a" using divides_def by simp
  27   thus "common_div a b k" using assms and common_div_def by simp
  28 qed
  29   *)
  30
  31   lemma common_div_b_a: (* Proof by Alt-Ergo *)
  32     forall a b k:int. common_div a (b-a) k -> common_div a b k
  33
  34   lemma common_div_commutes: (* Proof by Alt-Ergo *)
  35     forall a b k:int. common_div a b k -> common_div b a k
  36
  37   lemma gcd_commutes: (* Proof by Alt-Ergo *)
  38     forall a b k:int. is_gcd a b k -> is_gcd b a k
  39
  40   lemma gcd_a_b:
  41     forall a b k:int. is_gcd (a-b) b k -> is_gcd a b k
  42   (* Isabelle proof
  43 proof -
  44   from assms have "common_div (a-b) b k" using is_gcd_def by simp
  45   then have 1: "common_div a b k" using common_div_a_b by simp
  46   (* show that any other common divisor of a and b divides k *)
  47   { fix p
  48     assume h: "common_div a b p"
  49     hence "\<exists>ka kb::int. (a = ka * p) \<and> (b = kb * p)" using common_div_def and divides_def by simp
  50     then obtain ka kb where "a = ka * p" and "b = kb * p" by auto
  51     hence "a - b = (ka - kb) * p" using int_distrib by simp
  52     hence "divides p (a-b)"  using divides_def by simp
  53     hence "common_div (a-b) b p" using h and common_div_def by simp
  54     hence "divides p k" using assms and is_gcd_def by simp
  55   }
  56   hence "\<forall>p::int. common_div a b p \<longrightarrow> divides p k" by simp
  57   thus "is_gcd a b k" using 1 and is_gcd_def by simp
  58 qed
  59   *)
  60
  61   lemma gcd_b_a: (* Proof by Alt-Ergo *)
  62     forall a b k:int. is_gcd a (b-a) k -> is_gcd a b k
  63
  64   (* Correctness and termination by Alt-Ergo *)
  65   let pgcd (p: int) (q: int)
  66     requires { p > 0 /\ q > 0 }
  67     ensures { is_gcd p q result }
  68   =
  69     let a = ref p in
  70     let b = ref q in
  71     while (!a <> !b) do
  72       invariant { !a > 0 /\ !b > 0 /\ forall k: int. is_gcd !a !b k -> is_gcd p q k }
  73       variant { !a + !b }
  74       if !a > !b then
  75         a := !a - !b
  76       else
  77         b := !b - !a
  78     done;
  79     !a
  80 end