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