Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Replaced smod by standard mod operator to reflect actual behaviour
authorberghofe
Wed, 26 Jan 2011 20:51:09 +0100
changeset 41635 f938a6022d2e
parent 41634 28d94383249c
child 41636 934b4ad9b611
Replaced smod by standard mod operator to reflect actual behaviour of the SPARK tools.
src/HOL/SPARK/Examples/RIPEMD-160/Round.thy file | annotate | diff | comparison | revisions
src/HOL/SPARK/SPARK_Setup.thy file | annotate | diff | comparison | revisions
src/HOL/SPARK/Tools/spark_vcs.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/SPARK/Examples/RIPEMD-160/Round.thy	Thu Jan 27 12:24:00 2011 +0100
+++ b/src/HOL/SPARK/Examples/RIPEMD-160/Round.thy	Wed Jan 26 20:51:09 2011 +0100
@@ -282,11 +282,11 @@
       uint_word_of_int_id[OF `0 <= cd` `cd <= ?M`]
       uint_word_of_int_id[OF `0 <= ce` `ce <= ?M`])
   let ?rotate_arg_l =
-    "((((ca + f 0 cb cc cd) smod 4294967296 +
-        x (r_l 0)) smod 4294967296 + k_l 0) smod 4294967296)"
+    "((((ca + f 0 cb cc cd) mod 4294967296 +
+        x (r_l 0)) mod 4294967296 + k_l 0) mod 4294967296)"
   let ?rotate_arg_r =
-    "((((ca + f 79 cb cc cd) smod 4294967296 +
-        x (r_r 0)) smod 4294967296 + k_r 0) smod 4294967296)"
+    "((((ca + f 79 cb cc cd) mod 4294967296 +
+        x (r_r 0)) mod 4294967296 + k_r 0) mod 4294967296)"
   note returns =
     `wordops__rotate (s_l 0) ?rotate_arg_l =
      rotate_left (s_l 0) ?rotate_arg_l`
@@ -330,20 +330,20 @@
   from this[OF x_lower x_upper x_lower' x_upper' `0 <= 0` `0 <= 79`]
     `0 \<le> ca` `0 \<le> ce` x_lower x_lower'
   show ?thesis unfolding returns(1) returns(2) unfolding returns
-    by (simp add: smod_pos_pos)
+    by simp
 qed
 
 spark_vc procedure_round_62
 proof -
   let ?M = "4294967295::int"
   let ?rotate_arg_l =
-    "((((cla + f (loop__1__j + 1) clb clc cld) smod 4294967296 +
-         x (r_l (loop__1__j + 1))) smod 4294967296 +
-         k_l (loop__1__j + 1)) smod 4294967296)"
+    "((((cla + f (loop__1__j + 1) clb clc cld) mod 4294967296 +
+         x (r_l (loop__1__j + 1))) mod 4294967296 +
+         k_l (loop__1__j + 1)) mod 4294967296)"
   let ?rotate_arg_r =
-    "((((cra + f (79 - (loop__1__j + 1)) crb crc crd) smod
-         4294967296 + x (r_r (loop__1__j + 1))) smod 4294967296 +
-         k_r (loop__1__j + 1)) smod 4294967296)"
+    "((((cra + f (79 - (loop__1__j + 1)) crb crc crd) mod
+         4294967296 + x (r_r (loop__1__j + 1))) mod 4294967296 +
+         k_r (loop__1__j + 1)) mod 4294967296)"
 
   have s: "78 - loop__1__j = (79 - (loop__1__j + 1))" by simp
   note returns =
@@ -415,7 +415,7 @@
     `0 \<le> cla` `0 \<le> cle` `0 \<le> cra` `0 \<le> cre` x_lower x_lower'
   show ?thesis unfolding `loop__1__j + 1 + 1 = loop__1__j + 2`
     unfolding returns(1) returns(2) unfolding returns
-    by (simp add: smod_pos_pos)
+    by simp
 qed
 
 spark_vc procedure_round_76
@@ -456,7 +456,7 @@
     unfolding round_def
     unfolding steps_to_steps'
     unfolding H1[symmetric]
-    by (simp add: uint_word_ariths(2) rdmods smod_pos_pos
+    by (simp add: uint_word_ariths(2) rdmods
       uint_word_of_int_id)
 qed
 
--- a/src/HOL/SPARK/SPARK_Setup.thy	Thu Jan 27 12:24:00 2011 +0100
+++ b/src/HOL/SPARK/SPARK_Setup.thy	Wed Jan 26 20:51:09 2011 +0100
@@ -15,7 +15,7 @@
 begin
 
 text {*
-SPARK versions of div and mod, see section 4.4.1.1 of SPARK Proof Manual
+SPARK version of div, see section 4.4.1.1 of SPARK Proof Manual
 *}
 
 definition sdiv :: "int \<Rightarrow> int \<Rightarrow> int" (infixl "sdiv" 70) where
@@ -27,23 +27,14 @@
         if 0 \<le> b then - (- a div b)
         else - a div - b)"
 
-definition smod :: "int \<Rightarrow> int \<Rightarrow> int" (infixl "smod" 70) where
-  "a smod b = a - ((a sdiv b) * b)"
-
 lemma sdiv_minus_dividend: "- a sdiv b = - (a sdiv b)"
   by (simp add: sdiv_def)
 
 lemma sdiv_minus_divisor: "a sdiv - b = - (a sdiv b)"
   by (simp add: sdiv_def)
 
-lemma smod_minus_dividend: "- a smod b = - (a smod b)"
-  by (simp add: smod_def sdiv_minus_dividend)
-
-lemma smod_minus_divisor: "a smod - b = a smod b"
-  by (simp add: smod_def sdiv_minus_divisor)
-
 text {*
-Correspondence between HOL's and SPARK's versions of div and mod
+Correspondence between HOL's and SPARK's version of div
 *}
 
 lemma sdiv_pos_pos: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> a sdiv b = a div b"
@@ -58,18 +49,6 @@
 lemma sdiv_neg_neg: "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> a sdiv b = - a div - b"
   by (simp add: sdiv_def)
 
-lemma smod_pos_pos: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> a smod b = a mod b"
-  by (simp add: smod_def sdiv_pos_pos zmod_zdiv_equality')
-
-lemma smod_pos_neg: "0 \<le> a \<Longrightarrow> b < 0 \<Longrightarrow> a smod b = a mod - b"
-  by (simp add: smod_def sdiv_pos_neg zmod_zdiv_equality')
-
-lemma smod_neg_pos: "a < 0 \<Longrightarrow> 0 \<le> b \<Longrightarrow> a smod b = - (- a mod b)"
-  by (simp add: smod_def sdiv_neg_pos zmod_zdiv_equality')
-
-lemma smod_neg_neg: "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> a smod b = - (- a mod - b)"
-  by (simp add: smod_def sdiv_neg_neg zmod_zdiv_equality')
-
 
 text {*
 Updating a function at a set of points. Useful for building arrays.
--- a/src/HOL/SPARK/Tools/spark_vcs.ML	Thu Jan 27 12:24:00 2011 +0100
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Wed Jan 26 20:51:09 2011 +0100
@@ -287,7 +287,7 @@
       | tm_of vs (Funct ("div", [e, e'])) = (HOLogic.mk_binop @{const_name sdiv}
           (fst (tm_of vs e), fst (tm_of vs e')), integerN)
 
-      | tm_of vs (Funct ("mod", [e, e'])) = (HOLogic.mk_binop @{const_name smod}
+      | tm_of vs (Funct ("mod", [e, e'])) = (HOLogic.mk_binop @{const_name mod}
           (fst (tm_of vs e), fst (tm_of vs e')), integerN)
 
       | tm_of vs (Funct ("-", [e])) =
isabelle