# HG changeset patch
# User wenzelm
# Date 1515764586 -3600
# Node ID dbaa38bd223a380e8cd3fe22bf35c2a42884a552
# Parent  23307fd339067a3d11fecf188d9de74fc7399d36
prefer formal comments;

diff -r 23307fd33906 -r dbaa38bd223a src/HOL/SPARK/Examples/RIPEMD-160/RMD.thy
--- a/src/HOL/SPARK/Examples/RIPEMD-160/RMD.thy	Fri Jan 12 14:08:53 2018 +0100
+++ b/src/HOL/SPARK/Examples/RIPEMD-160/RMD.thy	Fri Jan 12 14:43:06 2018 +0100
@@ -9,7 +9,7 @@
 begin
 
 
-(* all operations are defined on 32-bit words *)
+\<comment> \<open>all operations are defined on 32-bit words\<close>
 
 type_synonym word32 = "32 word"
 type_synonym byte = "8 word"
@@ -18,7 +18,7 @@
 type_synonym block = "nat \<Rightarrow> word32"
 type_synonym message = "nat \<Rightarrow> block"
 
-(* nonlinear functions at bit level *)
+\<comment> \<open>nonlinear functions at bit level\<close>
 
 definition f::"[nat, word32, word32, word32] => word32"
 where
@@ -31,7 +31,7 @@
   else 0)"
 
 
-(* added constants (hexadecimal) *)
+\<comment> \<open>added constants (hexadecimal)\<close>
 
 definition K::"nat => word32"
 where
@@ -54,7 +54,7 @@
   else 0)"
 
 
-(* selection of message word *)
+\<comment> \<open>selection of message word\<close>
 
 definition r_list :: "nat list"
   where "r_list = [
@@ -81,7 +81,7 @@
   where "r' j = r'_list ! j"
 
 
-(* amount for rotate left (rol) *)
+\<comment> \<open>amount for rotate left (rol)\<close>
 
 definition s_list :: "nat list"
   where "s_list = [
@@ -108,7 +108,7 @@
   where "s' j = s'_list ! j"
 
 
-(* Initial value (hexadecimal *)
+\<comment> \<open>Initial value (hexadecimal)\<close>
 
 definition h0_0::word32 where "h0_0 = 0x67452301"
 definition h1_0::word32 where "h1_0 = 0xEFCDAB89"
@@ -126,11 +126,11 @@
   where
   "step_l X c j =
     (let (A, B, C, D, E) = c in
-    ((* A *) E,
-     (* B *) word_rotl (s j) (A + f j B C D + X (r j) + K j) + E,
-     (* C *) B,
-     (* D *) word_rotl 10 C,
-     (* E *) D))"
+    (\<comment> \<open>\<open>A:\<close>\<close> E,
+     \<comment> \<open>\<open>B:\<close>\<close> word_rotl (s j) (A + f j B C D + X (r j) + K j) + E,
+     \<comment> \<open>\<open>C:\<close>\<close> B,
+     \<comment> \<open>\<open>D:\<close>\<close> word_rotl 10 C,
+     \<comment> \<open>\<open>E:\<close>\<close> D))"
 
 definition step_r ::
   "[ block,
@@ -140,11 +140,11 @@
 where
   "step_r X c' j =
     (let (A', B', C', D', E') = c' in
-    ((* A' *) E',
-     (* B' *) word_rotl (s' j) (A' + f (79 - j) B' C' D' + X (r' j) + K' j) + E',
-     (* C' *) B',
-     (* D' *) word_rotl 10 C',
-     (* E' *) D'))"
+    (\<comment> \<open>\<open>A':\<close>\<close> E',
+     \<comment> \<open>\<open>B':\<close>\<close> word_rotl (s' j) (A' + f (79 - j) B' C' D' + X (r' j) + K' j) + E',
+     \<comment> \<open>\<open>C':\<close>\<close> B',
+     \<comment> \<open>\<open>D':\<close>\<close> word_rotl 10 C',
+     \<comment> \<open>\<open>E':\<close>\<close> D'))"
 
 definition step_both ::
   "[ block, chain * chain, nat ] \<Rightarrow> chain * chain"
@@ -159,11 +159,11 @@
   where "round X h =
     (let (h0, h1, h2, h3, h4) = h in
      let ((A, B, C, D, E), (A', B', C', D', E')) = steps X (h, h) 80 in
-      ((* h0 *) h1 + C + D',
-       (* h1 *) h2 + D + E',
-       (* h2 *) h3 + E + A',
-       (* h3 *) h4 + A + B',
-       (* h4 *) h0 + B + C'))"
+      (\<comment> \<open>\<open>h0:\<close>\<close> h1 + C + D',
+       \<comment> \<open>\<open>h1:\<close>\<close> h2 + D + E',
+       \<comment> \<open>\<open>h2:\<close>\<close> h3 + E + A',
+       \<comment> \<open>\<open>h3:\<close>\<close> h4 + A + B',
+       \<comment> \<open>\<open>h4:\<close>\<close> h0 + B + C'))"
 
 definition rmd_body::"[ message, chain, nat ] => chain"
 where
diff -r 23307fd33906 -r dbaa38bd223a src/HOL/SPARK/Examples/RIPEMD-160/RMD_Specification.thy
--- a/src/HOL/SPARK/Examples/RIPEMD-160/RMD_Specification.thy	Fri Jan 12 14:08:53 2018 +0100
+++ b/src/HOL/SPARK/Examples/RIPEMD-160/RMD_Specification.thy	Fri Jan 12 14:43:06 2018 +0100
@@ -8,7 +8,7 @@
 imports RMD "HOL-SPARK.SPARK"
 begin
 
-(* bit operations *)
+\<comment> \<open>bit operations\<close>
 
 abbreviation rotate_left :: "int \<Rightarrow> int \<Rightarrow> int" where
   "rotate_left i w == uint (word_rotl (nat i) (word_of_int w::word32))"
@@ -17,7 +17,7 @@
   wordops__rotate_left = rotate_left
 
 
-(* Conversions for proof functions *)
+\<comment> \<open>Conversions for proof functions\<close>
 abbreviation k_l_spec :: " int => int " where
   "k_l_spec j == uint (K (nat j))"
 abbreviation k_r_spec :: " int => int " where
diff -r 23307fd33906 -r dbaa38bd223a src/HOL/SPARK/Examples/RIPEMD-160/Round.thy
--- a/src/HOL/SPARK/Examples/RIPEMD-160/Round.thy	Fri Jan 12 14:08:53 2018 +0100
+++ b/src/HOL/SPARK/Examples/RIPEMD-160/Round.thy	Fri Jan 12 14:43:06 2018 +0100
@@ -324,8 +324,8 @@
   have "0 <= (79::int)" by simp
   note step_from_hyp [OF
     step_hyp
-    H2 H4 H6 H8 H10 H2 H4 H6 H8 H10 (* upper bounds *)
-    H1 H3 H5 H7 H9  H1 H3 H5 H7 H9  (* lower bounds *)
+    H2 H4 H6 H8 H10 H2 H4 H6 H8 H10 \<comment> \<open>upper bounds\<close>
+    H1 H3 H5 H7 H9  H1 H3 H5 H7 H9  \<comment> \<open>lower bounds\<close>
   ]
   from this[OF x_lower x_upper x_lower' x_upper' \<open>0 <= 0\<close> \<open>0 <= 79\<close>]
     \<open>0 \<le> ca\<close> \<open>0 \<le> ce\<close> x_lower x_lower'