# HG changeset patch
# User berghofe
# Date 1296071469 -3600
# Node ID f938a6022d2edfe18c034916276b498de0f59e97
# Parent 28d94383249c8506284669674a1d9baba3526730
Replaced smod by standard mod operator to reflect actual behaviour
of the SPARK tools.
diff -r 28d94383249c -r f938a6022d2e src/HOL/SPARK/Examples/RIPEMD-160/Round.thy
--- 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
diff -r 28d94383249c -r f938a6022d2e src/HOL/SPARK/SPARK_Setup.thy
--- 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.
diff -r 28d94383249c -r f938a6022d2e src/HOL/SPARK/Tools/spark_vcs.ML
--- 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])) =