1.1 --- a/src/HOL/SPARK/SPARK_Setup.thy	Thu Jan 27 16:24:29 2011 +0100
     1.2 +++ b/src/HOL/SPARK/SPARK_Setup.thy	Thu Jan 27 16:31:03 2011 +0100
     1.3 @@ -19,35 +19,29 @@
     1.4  *}
     1.5  
     1.6  definition sdiv :: "int \<Rightarrow> int \<Rightarrow> int" (infixl "sdiv" 70) where
     1.7 -  "a sdiv b =
     1.8 -     (if 0 \<le> a then
     1.9 -        if 0 \<le> b then a div b
    1.10 -        else - (a div - b)
    1.11 -      else
    1.12 -        if 0 \<le> b then - (- a div b)
    1.13 -        else - a div - b)"
    1.14 +  "a sdiv b = sgn a * sgn b * (\<bar>a\<bar> div \<bar>b\<bar>)"
    1.15  
    1.16  lemma sdiv_minus_dividend: "- a sdiv b = - (a sdiv b)"
    1.17 -  by (simp add: sdiv_def)
    1.18 +  by (simp add: sdiv_def sgn_if)
    1.19  
    1.20  lemma sdiv_minus_divisor: "a sdiv - b = - (a sdiv b)"
    1.21 -  by (simp add: sdiv_def)
    1.22 +  by (simp add: sdiv_def sgn_if)
    1.23  
    1.24  text {*
    1.25  Correspondence between HOL's and SPARK's version of div
    1.26  *}
    1.27  
    1.28  lemma sdiv_pos_pos: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> a sdiv b = a div b"
    1.29 -  by (simp add: sdiv_def)
    1.30 +  by (simp add: sdiv_def sgn_if)
    1.31  
    1.32  lemma sdiv_pos_neg: "0 \<le> a \<Longrightarrow> b < 0 \<Longrightarrow> a sdiv b = - (a div - b)"
    1.33 -  by (simp add: sdiv_def)
    1.34 +  by (simp add: sdiv_def sgn_if)
    1.35  
    1.36  lemma sdiv_neg_pos: "a < 0 \<Longrightarrow> 0 \<le> b \<Longrightarrow> a sdiv b = - (- a div b)"
    1.37 -  by (simp add: sdiv_def)
    1.38 +  by (simp add: sdiv_def sgn_if)
    1.39  
    1.40  lemma sdiv_neg_neg: "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> a sdiv b = - a div - b"
    1.41 -  by (simp add: sdiv_def)
    1.42 +  by (simp add: sdiv_def sgn_if)
    1.43  
    1.44  
    1.45  text {*