Theory HOL-SPARK-Examples.Greatest_Common_Divisor

(*  Title:      HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy
    Author:     Stefan Berghofer
    Copyright:  secunet Security Networks AG
*)

theory Greatest_Common_Divisor
imports "HOL-SPARK.SPARK"
begin

spark_proof_functions
  gcd = "gcd :: int ⇒ int ⇒ int"

spark_open ‹greatest_common_divisor/g_c_d›

spark_vc procedure_g_c_d_4
proof -
  from ‹0 < d› have "0 ≤ c mod d" by (rule pos_mod_sign)
  with ‹0 ≤ c› ‹0 < d› ‹c - c sdiv d * d ≠ 0› show ?C1
    by (simp add: sdiv_pos_pos minus_div_mult_eq_mod [symmetric])
next
  from ‹0 ≤ c› ‹0 < d› ‹gcd c d = gcd m n› show ?C2
    by (simp add: sdiv_pos_pos minus_div_mult_eq_mod [symmetric] gcd_non_0_int)
qed

spark_vc procedure_g_c_d_11
proof -
  from ‹0 ≤ c› ‹0 < d› ‹c - c sdiv d * d = 0›
  have "d dvd c"
    by (auto simp add: sdiv_pos_pos dvd_def ac_simps)
  with ‹0 < d› ‹gcd c d = gcd m n› show ?C1
    by simp
qed

spark_end

end