isabelle: src/HOL/SPARK/Examples/RIPEMD-160/K_R.thy@939e88e79724 (annotated)

41561 d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	1	(* Title: HOL/SPARK/Examples/RIPEMD-160/K_R.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 K_R
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/k_r"
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_k_r_6
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	14	using assms by (simp add: K'_def)
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_k_r_7
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	17	proof-
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	18	from H1 have "16 <= nat j" by simp
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	19	moreover from H2 have "nat j <= 31" by simp
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	20	ultimately show ?thesis by (simp add: K'_def)
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	21	qed
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	22
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	23	spark_vc function_k_r_8
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	24	proof -
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	25	from H1 have "32 <= nat j" by simp
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	26	moreover from H2 have "nat j <= 47" by simp
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	27	ultimately show ?thesis by (simp add: K'_def)
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	28	qed
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	29
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	30	spark_vc function_k_r_9
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	31	proof -
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	32	from H1 have "48 <= nat j" by simp
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	33	moreover from H2 have "nat j <= 63" by simp
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	34	ultimately show ?thesis by (simp add: K'_def)
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	35	qed
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	36
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	37	spark_vc function_k_r_10
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	38	proof -
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	39	from H6 have "64 <= nat j" by simp
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	40	moreover from H2 have "nat j <= 79" by simp
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	41	ultimately show ?thesis by (simp add: K'_def)
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	42	qed
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	43
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	44	spark_end
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	45
d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	46	end

author	berghofe
	Wed, 30 Apr 2014 15:43:44 +0200
changeset 56798	939e88e79724
parent 41561	d1318f3c86ba
child 69605	a96320074298
permissions	-rw-r--r--