src/HOL/SPARK/Manual/Simple_Greatest_Common_Divisor.thy
author huffman
Sun Apr 01 16:09:58 2012 +0200 (2012-04-01)
changeset 47255 30a1692557b0
parent 45610 11095c312709
child 56798 939e88e79724
permissions -rw-r--r--
removed Nat_Numeral.thy, moving all theorems elsewhere
wenzelm@45610
     1
(*  Title:      HOL/SPARK/Manual/Simple_Greatest_Common_Divisor.thy
berghofe@45044
     2
    Author:     Stefan Berghofer
berghofe@45044
     3
    Copyright:  secunet Security Networks AG
berghofe@45044
     4
*)
berghofe@45044
     5
berghofe@45044
     6
theory Simple_Greatest_Common_Divisor
berghofe@45044
     7
imports SPARK GCD
berghofe@45044
     8
begin
berghofe@45044
     9
berghofe@45044
    10
spark_proof_functions
berghofe@45044
    11
  gcd = "gcd :: int \<Rightarrow> int \<Rightarrow> int"
berghofe@45044
    12
berghofe@45044
    13
spark_open "simple_greatest_common_divisor/g_c_d.siv"
berghofe@45044
    14
berghofe@45044
    15
spark_vc procedure_g_c_d_4
berghofe@45044
    16
  using `0 < d` `gcd c d = gcd m n`
berghofe@45044
    17
  by (simp add: gcd_non_0_int)
berghofe@45044
    18
berghofe@45044
    19
spark_vc procedure_g_c_d_9
berghofe@45044
    20
  using `0 \<le> c` `gcd c 0 = gcd m n`
berghofe@45044
    21
  by simp
berghofe@45044
    22
berghofe@45044
    23
spark_end
berghofe@45044
    24
berghofe@45044
    25
end