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

41561 d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	1	(* Title: HOL/SPARK/Examples/RIPEMD-160/F.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 F
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	8	imports RMD_Specification
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/f"
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_f_2
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	14	using assms by simp_all
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	15
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	16	spark_vc function_f_3
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	17	using assms by simp_all
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	18
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	19	spark_vc function_f_4
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	20	using assms by simp_all
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	21
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	22	spark_vc function_f_5
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	23	using assms by simp_all
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	24
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	25	spark_vc function_f_6
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	26	proof -
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	27	from H8 have "nat j <= 15" by simp
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	28	with assms show ?thesis
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	29	by (simp add: f_def bwsimps int_word_uint int_mod_eq')
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	30	qed
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	31
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	32	spark_vc function_f_7
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	33	proof -
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	34	from H7 have "16 <= nat j" by simp
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	35	moreover from H8 have "nat j <= 31" by simp
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	36	ultimately show ?thesis using assms
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	37	by (simp add: f_def bwsimps int_word_uint int_mod_eq')
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	38	qed
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	39
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	40	spark_vc function_f_8
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	41	proof -
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	42	from H7 have "32 <= nat j" by simp
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	43	moreover from H8 have "nat j <= 47" by simp
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	44	ultimately show ?thesis using assms
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	45	by (simp add: f_def bwsimps int_word_uint int_mod_eq')
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	46	qed
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	47
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	48	spark_vc function_f_9
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	49	proof -
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	50	from H7 have "48 <= nat j" by simp
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	51	moreover from H8 have "nat j <= 63" by simp
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	52	ultimately show ?thesis using assms
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	53	by (simp add: f_def bwsimps int_word_uint int_mod_eq')
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	54	qed
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	55
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	56	spark_vc function_f_10
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	57	proof -
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	58	from H2 have "nat j <= 79" by simp
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	59	moreover from H12 have "64 <= nat j" by simp
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	60	ultimately show ?thesis using assms
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	61	by (simp add: f_def bwsimps int_word_uint int_mod_eq')
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	62	qed
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	63
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	64	spark_end
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	65
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	66	end

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