|
41561
|
1 |
(* Title: HOL/SPARK/Examples/RIPEMD-160/RMD_Lemmas.thy
|
|
|
2 |
Author: Fabian Immler, TU Muenchen
|
|
|
3 |
|
|
|
4 |
Verification of the RIPEMD-160 hash function
|
|
|
5 |
*)
|
|
|
6 |
|
|
|
7 |
theory RMD_Lemmas
|
|
|
8 |
imports Main
|
|
|
9 |
begin
|
|
|
10 |
|
|
|
11 |
definition "fun_of_list i xs g j =
|
|
|
12 |
(if j < i \<or> i + int (length xs) \<le> j then g j else xs ! nat (j - i))"
|
|
|
13 |
|
|
|
14 |
lemma fun_of_list_Nil [simp]: "fun_of_list i [] g = g"
|
|
|
15 |
by (auto simp add: fun_eq_iff fun_of_list_def)
|
|
|
16 |
|
|
|
17 |
lemma fun_of_list_Cons [simp]:
|
|
|
18 |
"fun_of_list i (x # xs) g = fun_of_list (i + 1) xs (g(i:=x))"
|
|
|
19 |
by (auto simp add: fun_eq_iff fun_of_list_def nth_Cons'
|
|
|
20 |
nat_diff_distrib [of "int (Suc 0)", simplified, symmetric]
|
|
|
21 |
diff_diff_eq)
|
|
|
22 |
|
|
|
23 |
lemma nth_fun_of_list_eq:
|
|
|
24 |
"0 \<le> i \<Longrightarrow> i < int (length xs) \<Longrightarrow> xs ! nat i = fun_of_list 0 xs g i"
|
|
|
25 |
by (simp add: fun_of_list_def)
|
|
|
26 |
|
|
|
27 |
end
|