isabelle: src/HOL/SPARK/Examples/RIPEMD-160/F.thy@a96320074298 (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
69605 a96320074298 isabelle update -u path_cartouches; wenzelm parents: 56798 diff changeset	11	spark_open \<open>rmd/f\<close>
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
	Sun, 06 Jan 2019 15:04:34 +0100
changeset 69605	a96320074298
parent 56798	939e88e79724
child 71997	4a013c92a091
permissions	-rw-r--r--