src/HOL/SPARK/Examples/RIPEMD-160/R_L.thy
changeset 41561 d1318f3c86ba
child 56798 939e88e79724
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/SPARK/Examples/RIPEMD-160/R_L.thy	Sat Jan 15 12:35:29 2011 +0100
     1.3 @@ -0,0 +1,30 @@
     1.4 +(*  Title:      HOL/SPARK/Examples/RIPEMD-160/R_L.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 R_L
    1.11 +imports RMD_Specification RMD_Lemmas
    1.12 +begin
    1.13 +
    1.14 +spark_open "rmd/r_l.siv"
    1.15 +
    1.16 +spark_vc function_r_l_2
    1.17 +proof -
    1.18 +  from `0 \<le> j` `j \<le> 79`
    1.19 +  show C: ?C1
    1.20 +    by (simp add: r_def r_list_def nth_map [symmetric, of _ _ int] del: fun_upd_apply)
    1.21 +      (simp add: nth_fun_of_list_eq [of _ _ undefined] del: fun_upd_apply)
    1.22 +  from C show ?C2 by simp
    1.23 +  have "list_all (\<lambda>n. int n \<le> 15) r_list"
    1.24 +    by (simp add: r_list_def)
    1.25 +  moreover have "length r_list = 80"
    1.26 +    by (simp add: r_list_def)
    1.27 +  ultimately show ?C3 unfolding C using `j \<le> 79`
    1.28 +    by (simp add: r_def list_all_length)
    1.29 +qed
    1.30 +
    1.31 +spark_end
    1.32 +
    1.33 +end