|
(* 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 \<open>greatest_common_divisor/g_c_d\<close>
spark_vc procedure_g_c_d_4
proof -
from \<open>0 < d\<close> have "0 \<le> c mod d" by (rule pos_mod_sign)
with \<open>0 \<le> c\<close> \<open>0 < d\<close> \<open>c - c sdiv d * d \<noteq> 0\<close> show ?C1
by (simp add: sdiv_pos_pos minus_div_mult_eq_mod [symmetric])
next
from \<open>0 \<le> c\<close> \<open>0 < d\<close> \<open>gcd c d = gcd m n\<close> 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 \<open>0 \<le> c\<close> \<open>0 < d\<close> \<open>c - c sdiv d * d = 0\<close>
have "d dvd c"
by (auto simp add: sdiv_pos_pos dvd_def ac_simps)
with \<open>0 < d\<close> \<open>gcd c d = gcd m n\<close> show ?C1
by simp
qed
spark_end
end
¤ Dauer der Verarbeitung: 0.17 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
