src/HOL/SPARK/Examples/RIPEMD-160/RMD_Lemmas.thy
changeset 41561 d1318f3c86ba
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/SPARK/Examples/RIPEMD-160/RMD_Lemmas.thy	Sat Jan 15 12:35:29 2011 +0100
     1.3 @@ -0,0 +1,27 @@
     1.4 +(*  Title:      HOL/SPARK/Examples/RIPEMD-160/RMD_Lemmas.thy
     1.5 +    Author:     Fabian Immler, TU Muenchen
     1.6 +
     1.7 +Verification of the RIPEMD-160 hash function
     1.8 +*)
     1.9 +
    1.10 +theory RMD_Lemmas
    1.11 +imports Main
    1.12 +begin
    1.13 +
    1.14 +definition "fun_of_list i xs g j =
    1.15 +  (if j < i \<or> i + int (length xs) \<le> j then g j else xs ! nat (j - i))"
    1.16 +
    1.17 +lemma fun_of_list_Nil [simp]: "fun_of_list i [] g = g"
    1.18 +  by (auto simp add: fun_eq_iff fun_of_list_def)
    1.19 +
    1.20 +lemma fun_of_list_Cons [simp]:
    1.21 +  "fun_of_list i (x # xs) g = fun_of_list (i + 1) xs (g(i:=x))"
    1.22 +  by (auto simp add: fun_eq_iff fun_of_list_def nth_Cons'
    1.23 +    nat_diff_distrib [of "int (Suc 0)", simplified, symmetric]
    1.24 +    diff_diff_eq)
    1.25 +
    1.26 +lemma nth_fun_of_list_eq:
    1.27 +  "0 \<le> i \<Longrightarrow> i < int (length xs) \<Longrightarrow> xs ! nat i = fun_of_list 0 xs g i"
    1.28 +  by (simp add: fun_of_list_def)
    1.29 +
    1.30 +end