author | wenzelm |
Fri, 18 Aug 2017 20:47:47 +0200 | |
changeset 66453 | cc19f7ca2ed6 |
parent 63167 | 0909deb8059b |
child 69605 | a96320074298 |
permissions | -rw-r--r-- |
41561 | 1 |
(* Title: HOL/SPARK/Examples/RIPEMD-160/R_L.thy |
2 |
Author: Fabian Immler, TU Muenchen |
|
3 |
||
4 |
Verification of the RIPEMD-160 hash function |
|
5 |
*) |
|
6 |
||
7 |
theory R_L |
|
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/r_l" |
41561 | 12 |
|
13 |
spark_vc function_r_l_2 |
|
14 |
proof - |
|
63167 | 15 |
from \<open>0 \<le> j\<close> \<open>j \<le> 79\<close> |
41561 | 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) |
|
63167 | 24 |
ultimately show ?C3 unfolding C using \<open>j \<le> 79\<close> |
41561 | 25 |
by (simp add: r_def list_all_length) |
26 |
qed |
|
27 |
||
28 |
spark_end |
|
29 |
||
30 |
end |