|
41561
|
1 |
(* Title: HOL/SPARK/Examples/RIPEMD-160/R_R.thy
|
|
|
2 |
Author: Fabian Immler, TU Muenchen
|
|
|
3 |
|
|
|
4 |
Verification of the RIPEMD-160 hash function
|
|
|
5 |
*)
|
|
|
6 |
|
|
|
7 |
theory R_R
|
|
|
8 |
imports RMD_Specification RMD_Lemmas
|
|
|
9 |
begin
|
|
|
10 |
|
|
|
11 |
spark_open "rmd/r_r.siv"
|
|
|
12 |
|
|
|
13 |
spark_vc function_r_r_2
|
|
|
14 |
proof -
|
|
|
15 |
from `0 \<le> j` `j \<le> 79`
|
|
|
16 |
show C: ?C1
|
|
|
17 |
by (simp add: r'_def r'_list_def nth_map [symmetric, of _ _ int] del: fun_upd_apply)
|
|
|
18 |
(simp add: nth_fun_of_list_eq [of _ _ undefined] del: fun_upd_apply)
|
|
|
19 |
from C show ?C2 by simp
|
|
|
20 |
have "list_all (\<lambda>n. int n \<le> 15) r'_list"
|
|
|
21 |
by (simp add: r'_list_def)
|
|
|
22 |
moreover have "length r'_list = 80"
|
|
|
23 |
by (simp add: r'_list_def)
|
|
|
24 |
ultimately show ?C3 unfolding C using `j \<le> 79`
|
|
|
25 |
by (simp add: r'_def list_all_length)
|
|
|
26 |
qed
|
|
|
27 |
|
|
|
28 |
spark_end
|
|
|
29 |
|
|
|
30 |
end
|