isabelle: src/HOL/SPARK/Examples/RIPEMD-160/S_L.thy@64b47495676d (annotated)

41561 d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	1	(* Title: HOL/SPARK/Examples/RIPEMD-160/S_L.thy
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	2	Author: Fabian Immler, TU Muenchen
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	3
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	4	Verification of the RIPEMD-160 hash function
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	5	*)
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	6
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	7	theory S_L
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	8	imports RMD_Specification RMD_Lemmas
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	9	begin
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	10
56798 939e88e79724 Discontinued old spark_open; spark_open_siv is now spark_open berghofe parents: 41561 diff changeset	11	spark_open "rmd/s_l"
41561 d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	12
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	13	spark_vc function_s_l_2
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	14	proof -
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 62390 diff changeset	15	from \<open>0 \<le> j\<close> \<open>j \<le> 79\<close>
41561 d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	16	show C: ?C1
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	17	by (simp add: s_def s_list_def nth_map [symmetric, of _ _ int] del: fun_upd_apply)
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	18	(simp add: nth_fun_of_list_eq [of _ _ undefined] del: fun_upd_apply)
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	19	from C show ?C2 by simp
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	20	have "list_all (\<lambda>n. int n \<le> 15) s_list"
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	21	by (simp add: s_list_def)
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	22	moreover have "length s_list = 80"
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	23	by (simp add: s_list_def)
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 62390 diff changeset	24	ultimately show ?C3 unfolding C using \<open>j \<le> 79\<close>
41561 d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	25	by (simp add: s_def list_all_length)
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	26	qed
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	27
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	28	spark_end
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	29
62390 842917225d56 more canonical names nipkow parents: 56798 diff changeset	30	end

author	wenzelm
	Wed, 04 Oct 2017 12:00:53 +0200
changeset 66787	64b47495676d
parent 63167	0909deb8059b
child 69605	a96320074298
permissions	-rw-r--r--