summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/SPARK/Examples/RIPEMD-160/K_L.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_L.thy Sat Jan 15 12:35:29 2011 +0100 1.3 @@ -0,0 +1,46 @@ 1.4 +(* Title: HOL/SPARK/Examples/RIPEMD-160/K_L.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_L 1.11 +imports RMD_Specification 1.12 +begin 1.13 + 1.14 +spark_open "rmd/k_l.siv" 1.15 + 1.16 +spark_vc function_k_l_6 1.17 + using assms by (simp add: K_def) 1.18 + 1.19 +spark_vc function_k_l_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_l_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_l_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_l_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