isabelle: src/HOL/SPARK/Examples/RIPEMD-160/F.thy@7ddae44464d4 (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
74496 807b094a9b78 avoid overaggressive contraction of conversions haftmann parents: 72292 diff changeset	29	by (simp add: f_def bwsimps take_bit_int_eq_self unsigned_of_int)
41561 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
72292 4a58c38b85ff factored out typedef material haftmann parents: 72262 diff changeset	37	by (simp only: f_def bwsimps)
74496 807b094a9b78 avoid overaggressive contraction of conversions haftmann parents: 72292 diff changeset	38	(simp add: take_bit_int_eq_self take_bit_not_eq_mask_diff mask_eq_exp_minus_1 unsigned_of_int)
41561 d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	39	qed
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	40
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	41	spark_vc function_f_8
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	42	proof -
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	43	from H7 have "32 <= nat j" by simp
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	44	moreover from H8 have "nat j <= 47" by simp
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	45	ultimately show ?thesis using assms
74496 807b094a9b78 avoid overaggressive contraction of conversions haftmann parents: 72292 diff changeset	46	by (simp only: f_def bwsimps) (simp add: take_bit_int_eq_self take_bit_not_eq_mask_diff mask_eq_exp_minus_1 unsigned_of_int)
41561 d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	47	qed
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	48
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	49	spark_vc function_f_9
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	50	proof -
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	51	from H7 have "48 <= nat j" by simp
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	52	moreover from H8 have "nat j <= 63" by simp
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	53	ultimately show ?thesis using assms
74496 807b094a9b78 avoid overaggressive contraction of conversions haftmann parents: 72292 diff changeset	54	by (simp only: f_def bwsimps) (simp add: take_bit_int_eq_self take_bit_not_eq_mask_diff mask_eq_exp_minus_1 unsigned_of_int)
41561 d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	55	qed
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	56
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	57	spark_vc function_f_10
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	58	proof -
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	59	from H2 have "nat j <= 79" by simp
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	60	moreover from H12 have "64 <= nat j" by simp
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	61	ultimately show ?thesis using assms
74496 807b094a9b78 avoid overaggressive contraction of conversions haftmann parents: 72292 diff changeset	62	by (simp only: f_def bwsimps) (simp add: take_bit_int_eq_self take_bit_not_eq_mask_diff mask_eq_exp_minus_1 unsigned_of_int)
41561 d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	63	qed
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	64
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	65	spark_end
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	66
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	67	end

author	haftmann
	Tue, 08 Jul 2025 19:13:44 +0200
changeset 82824	7ddae44464d4
parent 74496	807b094a9b78
permissions	-rw-r--r--