isabelle: src/HOL/SPARK/Examples/RIPEMD-160/K_L.thy@a96320074298 (annotated)

41561 d1318f3c86ba Added new SPARK verification environment. berghofe parents: diff changeset	1	(* Title: HOL/SPARK/Examples/RIPEMD-160/K_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 K_L
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/k_l\<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_k_l_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_l_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_l_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_l_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_l_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	wenzelm
	Sun, 06 Jan 2019 15:04:34 +0100
changeset 69605	a96320074298
parent 56798	939e88e79724
permissions	-rw-r--r--