Mercurial Mercurial > repos > isabelle / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/SPARK/Examples/RIPEMD-160/K_R.thy
author wenzelm
Sat, 23 May 2015 17:19:37 +0200
changeset 60299 5ae2a2e74c93
parent 56798 939e88e79724
child 69605 a96320074298
permissions -rw-r--r--
clarified NEWS: document_files are officially required since Isabelle2014, but the absence was tolerated as legacy feature;

(*  Title:      HOL/SPARK/Examples/RIPEMD-160/K_R.thy
    Author:     Fabian Immler, TU Muenchen

Verification of the RIPEMD-160 hash function
*)

theory K_R
imports RMD_Specification
begin

spark_open "rmd/k_r"

spark_vc function_k_r_6
  using assms by (simp add: K'_def)

spark_vc function_k_r_7
proof-
  from H1 have "16 <= nat j" by simp
  moreover from H2 have "nat j <= 31" by simp
  ultimately show ?thesis by (simp add: K'_def)
qed

spark_vc function_k_r_8
proof -
  from H1 have "32 <= nat j" by simp
  moreover from H2 have "nat j <= 47" by simp
  ultimately show ?thesis by (simp add: K'_def)
qed

spark_vc function_k_r_9
proof -
  from H1 have "48 <= nat j" by simp
  moreover from H2 have "nat j <= 63" by simp
  ultimately show ?thesis by (simp add: K'_def)
qed

spark_vc function_k_r_10
proof -
  from H6 have "64 <= nat j" by simp
  moreover from H2 have "nat j <= 79" by simp
  ultimately show ?thesis by (simp add: K'_def)
qed

spark_end

end
isabelle