| author | berghofe |
| Wed, 30 Apr 2014 15:43:44 +0200 | |
| changeset 56798 | 939e88e79724 |
| parent 41561 | d1318f3c86ba |
| child 62390 | 842917225d56 |
| permissions | -rw-r--r-- |
| 41561 | 1 |
(* Title: HOL/SPARK/Examples/RIPEMD-160/S_R.thy |
2 |
Author: Fabian Immler, TU Muenchen |
|
3 |
||
4 |
Verification of the RIPEMD-160 hash function |
|
5 |
*) |
|
6 |
||
7 |
theory S_R |
|
8 |
imports RMD_Specification RMD_Lemmas |
|
9 |
begin |
|
10 |
||
|
56798
939e88e79724
Discontinued old spark_open; spark_open_siv is now spark_open
berghofe
parents:
41561
diff
changeset
|
11 |
spark_open "rmd/s_r" |
| 41561 | 12 |
|
13 |
spark_vc function_s_r_2 |
|
14 |
proof - |
|
15 |
from `0 \<le> j` `j \<le> 79` |
|
16 |
show C: ?C1 |
|
17 |
by (simp add: s'_def s'_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) s'_list" |
|
21 |
by (simp add: s'_list_def) |
|
22 |
moreover have "length s'_list = 80" |
|
23 |
by (simp add: s'_list_def) |
|
24 |
ultimately show ?C3 unfolding C using `j \<le> 79` |
|
25 |
by (simp add: s'_def list_all_length) |
|
26 |
qed |
|
27 |
||
28 |
spark_end |
|
29 |
||
30 |
end |