# HG changeset patch
# User berghofe
# Date 1296142263 -3600
# Node ID 55a45051b22050454984f9665065f4ef1bde0a66
# Parent  934b4ad9b61120d457e62429cb3a3dc95e8bb0e2
Tuned definition of sdiv.

diff -r 934b4ad9b611 -r 55a45051b220 src/HOL/SPARK/SPARK_Setup.thy
--- a/src/HOL/SPARK/SPARK_Setup.thy	Thu Jan 27 16:24:29 2011 +0100
+++ b/src/HOL/SPARK/SPARK_Setup.thy	Thu Jan 27 16:31:03 2011 +0100
@@ -19,35 +19,29 @@
 *}
 
 definition sdiv :: "int \<Rightarrow> int \<Rightarrow> int" (infixl "sdiv" 70) where
-  "a sdiv b =
-     (if 0 \<le> a then
-        if 0 \<le> b then a div b
-        else - (a div - b)
-      else
-        if 0 \<le> b then - (- a div b)
-        else - a div - b)"
+  "a sdiv b = sgn a * sgn b * (\<bar>a\<bar> div \<bar>b\<bar>)"
 
 lemma sdiv_minus_dividend: "- a sdiv b = - (a sdiv b)"
-  by (simp add: sdiv_def)
+  by (simp add: sdiv_def sgn_if)
 
 lemma sdiv_minus_divisor: "a sdiv - b = - (a sdiv b)"
-  by (simp add: sdiv_def)
+  by (simp add: sdiv_def sgn_if)
 
 text {*
 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"
-  by (simp add: sdiv_def)
+  by (simp add: sdiv_def sgn_if)
 
 lemma sdiv_pos_neg: "0 \<le> a \<Longrightarrow> b < 0 \<Longrightarrow> a sdiv b = - (a div - b)"
-  by (simp add: sdiv_def)
+  by (simp add: sdiv_def sgn_if)
 
 lemma sdiv_neg_pos: "a < 0 \<Longrightarrow> 0 \<le> b \<Longrightarrow> a sdiv b = - (- a div b)"
-  by (simp add: sdiv_def)
+  by (simp add: sdiv_def sgn_if)
 
 lemma sdiv_neg_neg: "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> a sdiv b = - a div - b"
-  by (simp add: sdiv_def)
+  by (simp add: sdiv_def sgn_if)
 
 
 text {*