src/HOL/SPARK/Examples/RIPEMD-160/K_R.thy
changeset 41561 d1318f3c86ba
child 56798 939e88e79724
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/SPARK/Examples/RIPEMD-160/K_R.thy	Sat Jan 15 12:35:29 2011 +0100
     1.3 @@ -0,0 +1,46 @@
     1.4 +(*  Title:      HOL/SPARK/Examples/RIPEMD-160/K_R.thy
     1.5 +    Author:     Fabian Immler, TU Muenchen
     1.6 +
     1.7 +Verification of the RIPEMD-160 hash function
     1.8 +*)
     1.9 +
    1.10 +theory K_R
    1.11 +imports RMD_Specification
    1.12 +begin
    1.13 +
    1.14 +spark_open "rmd/k_r.siv"
    1.15 +
    1.16 +spark_vc function_k_r_6
    1.17 +  using assms by (simp add: K'_def)
    1.18 +
    1.19 +spark_vc function_k_r_7
    1.20 +proof-
    1.21 +  from H1 have "16 <= nat j" by simp
    1.22 +  moreover from H2 have "nat j <= 31" by simp
    1.23 +  ultimately show ?thesis by (simp add: K'_def)
    1.24 +qed
    1.25 +
    1.26 +spark_vc function_k_r_8
    1.27 +proof -
    1.28 +  from H1 have "32 <= nat j" by simp
    1.29 +  moreover from H2 have "nat j <= 47" by simp
    1.30 +  ultimately show ?thesis by (simp add: K'_def)
    1.31 +qed
    1.32 +
    1.33 +spark_vc function_k_r_9
    1.34 +proof -
    1.35 +  from H1 have "48 <= nat j" by simp
    1.36 +  moreover from H2 have "nat j <= 63" by simp
    1.37 +  ultimately show ?thesis by (simp add: K'_def)
    1.38 +qed
    1.39 +
    1.40 +spark_vc function_k_r_10
    1.41 +proof -
    1.42 +  from H6 have "64 <= nat j" by simp
    1.43 +  moreover from H2 have "nat j <= 79" by simp
    1.44 +  ultimately show ?thesis by (simp add: K'_def)
    1.45 +qed
    1.46 +
    1.47 +spark_end
    1.48 +
    1.49 +end