1(*  Title:      HOL/SPARK/Examples/RIPEMD-160/K_L.thy
2    Author:     Fabian Immler, TU Muenchen
3
4Verification of the RIPEMD-160 hash function
5*)
6
7theory K_L
8imports RMD_Specification
9begin
10
11spark_open \<open>rmd/k_l\<close>
12
13spark_vc function_k_l_6
14  using assms by (simp add: K_def)
15
16spark_vc function_k_l_7
17proof -
18  from H1 have "16 <= nat j" by simp
19  moreover from H2 have "nat j <= 31" by simp
20  ultimately show ?thesis by (simp add: K_def)
21qed
22
23spark_vc function_k_l_8
24proof -
25  from H1 have "32 <= nat j" by simp
26  moreover from H2 have "nat j <= 47" by simp
27  ultimately show ?thesis by (simp add: K_def)
28qed
29
30spark_vc function_k_l_9
31proof -
32  from H1 have "48 <= nat j" by simp
33  moreover from H2 have "nat j <= 63" by simp
34  ultimately show ?thesis by (simp add: K_def)
35qed
36
37spark_vc function_k_l_10
38proof -
39  from H6 have "64 <= nat j" by simp
40  moreover from H2 have "nat j <= 79" by simp
41  ultimately show ?thesis by (simp add: K_def)
42qed
43
44spark_end
45
46end
47