1.1 --- a/src/HOL/Divides.thy	Tue Mar 27 11:02:18 2012 +0200
     1.2 +++ b/src/HOL/Divides.thy	Tue Mar 27 11:41:16 2012 +0200
     1.3 @@ -1133,8 +1133,8 @@
     1.4  
     1.5  definition divmod_int_rel :: "int \<Rightarrow> int \<Rightarrow> int \<times> int \<Rightarrow> bool" where
     1.6      --{*definition of quotient and remainder*}
     1.7 -    "divmod_int_rel a b = (\<lambda>(q, r). a = b * q + r \<and>
     1.8 -               (if 0 < b then 0 \<le> r \<and> r < b else b < r \<and> r \<le> 0))"
     1.9 +  "divmod_int_rel a b = (\<lambda>(q, r). a = b * q + r \<and>
    1.10 +    (if 0 < b then 0 \<le> r \<and> r < b else if b < 0 then b < r \<and> r \<le> 0 else q = 0))"
    1.11  
    1.12  definition adjust :: "int \<Rightarrow> int \<times> int \<Rightarrow> int \<times> int" where
    1.13      --{*for the division algorithm*}
    1.14 @@ -1332,19 +1332,23 @@
    1.15  subsubsection {* Existence Shown by Proving the Division Algorithm to be Correct *}
    1.16  
    1.17  (*the case a=0*)
    1.18 -lemma divmod_int_rel_0: "b \<noteq> 0 ==> divmod_int_rel 0 b (0, 0)"
    1.19 +lemma divmod_int_rel_0: "divmod_int_rel 0 b (0, 0)"
    1.20  by (auto simp add: divmod_int_rel_def linorder_neq_iff)
    1.21  
    1.22  lemma posDivAlg_0 [simp]: "posDivAlg 0 b = (0, 0)"
    1.23  by (subst posDivAlg.simps, auto)
    1.24  
    1.25 +lemma posDivAlg_0_right [simp]: "posDivAlg a 0 = (0, a)"
    1.26 +by (subst posDivAlg.simps, auto)
    1.27 +
    1.28  lemma negDivAlg_minus1 [simp]: "negDivAlg -1 b = (-1, b - 1)"
    1.29  by (subst negDivAlg.simps, auto)
    1.30  
    1.31  lemma divmod_int_rel_neg: "divmod_int_rel (-a) (-b) qr ==> divmod_int_rel a b (apsnd uminus qr)"
    1.32 -by (auto simp add: split_ifs divmod_int_rel_def)
    1.33 -
    1.34 -lemma divmod_int_correct: "b \<noteq> 0 ==> divmod_int_rel a b (divmod_int a b)"
    1.35 +by (auto simp add: divmod_int_rel_def)
    1.36 +
    1.37 +lemma divmod_int_correct: "divmod_int_rel a b (divmod_int a b)"
    1.38 +apply (cases "b = 0", simp add: divmod_int_def divmod_int_rel_def)
    1.39  by (force simp add: linorder_neq_iff divmod_int_rel_0 divmod_int_def divmod_int_rel_neg
    1.40                      posDivAlg_correct negDivAlg_correct)
    1.41  
    1.42 @@ -1411,19 +1415,15 @@
    1.43  
    1.44  subsubsection {* General Properties of div and mod *}
    1.45  
    1.46 -lemma divmod_int_rel_div_mod: "b \<noteq> 0 ==> divmod_int_rel a b (a div b, a mod b)"
    1.47 +lemma divmod_int_rel_div_mod: "divmod_int_rel a b (a div b, a mod b)"
    1.48  apply (cut_tac a = a and b = b in zmod_zdiv_equality)
    1.49  apply (force simp add: divmod_int_rel_def linorder_neq_iff)
    1.50  done
    1.51  
    1.52  lemma divmod_int_rel_div: "[| divmod_int_rel a b (q, r) |] ==> a div b = q"
    1.53 -apply (cases "b = 0")
    1.54 -apply (simp add: divmod_int_rel_def)
    1.55  by (simp add: divmod_int_rel_div_mod [THEN unique_quotient])
    1.56  
    1.57  lemma divmod_int_rel_mod: "[| divmod_int_rel a b (q, r) |] ==> a mod b = r"
    1.58 -apply (cases "b = 0")
    1.59 -apply (simp add: divmod_int_rel_def)
    1.60  by (simp add: divmod_int_rel_div_mod [THEN unique_remainder])
    1.61  
    1.62  lemma div_pos_pos_trivial: "[| (0::int) \<le> a;  a < b |] ==> a div b = 0"
    1.63 @@ -1463,7 +1463,6 @@
    1.64  
    1.65  (*Simpler laws such as -a div b = -(a div b) FAIL, but see just below*)
    1.66  lemma zdiv_zminus_zminus [simp]: "(-a) div (-b) = a div (b::int)"
    1.67 -apply (case_tac "b = 0", simp)
    1.68  apply (simp add: divmod_int_rel_div_mod [THEN divmod_int_rel_neg, simplified, 
    1.69                                   THEN divmod_int_rel_div, THEN sym])
    1.70  
    1.71 @@ -1471,7 +1470,6 @@
    1.72  
    1.73  (*Simpler laws such as -a mod b = -(a mod b) FAIL, but see just below*)
    1.74  lemma zmod_zminus_zminus [simp]: "(-a) mod (-b) = - (a mod (b::int))"
    1.75 -apply (case_tac "b = 0", simp)
    1.76  apply (subst divmod_int_rel_div_mod [THEN divmod_int_rel_neg, simplified, THEN divmod_int_rel_mod],
    1.77         auto)
    1.78  done
    1.79 @@ -1480,7 +1478,7 @@
    1.80  subsubsection {* Laws for div and mod with Unary Minus *}
    1.81  
    1.82  lemma zminus1_lemma:
    1.83 -     "divmod_int_rel a b (q, r)
    1.84 +     "divmod_int_rel a b (q, r) ==> b \<noteq> 0
    1.85        ==> divmod_int_rel (-a) b (if r=0 then -q else -q - 1,  
    1.86                            if r=0 then 0 else b-r)"
    1.87  by (force simp add: split_ifs divmod_int_rel_def linorder_neq_iff right_diff_distrib)
    1.88 @@ -1538,7 +1536,7 @@
    1.89  apply (simp add: right_diff_distrib)
    1.90  done
    1.91  
    1.92 -lemma self_quotient: "[| divmod_int_rel a a (q, r) |] ==> q = 1"
    1.93 +lemma self_quotient: "[| divmod_int_rel a a (q, r); a \<noteq> 0 |] ==> q = 1"
    1.94  apply (simp add: split_ifs divmod_int_rel_def linorder_neq_iff)
    1.95  apply (rule order_antisym, safe, simp_all)
    1.96  apply (rule_tac [3] a = "-a" and r = "-r" in self_quotient_aux1)
    1.97 @@ -1546,8 +1544,8 @@
    1.98  apply (force intro: self_quotient_aux1 self_quotient_aux2 simp add: add_commute)+
    1.99  done
   1.100  
   1.101 -lemma self_remainder: "[| divmod_int_rel a a (q, r) |] ==> r = 0"
   1.102 -apply (frule self_quotient)
   1.103 +lemma self_remainder: "[| divmod_int_rel a a (q, r); a \<noteq> 0 |] ==> r = 0"
   1.104 +apply (frule (1) self_quotient)
   1.105  apply (simp add: divmod_int_rel_def)
   1.106  done
   1.107  
   1.108 @@ -1853,9 +1851,9 @@
   1.109      case True then have "b \<noteq> 0" and "c \<noteq> 0" by auto
   1.110      with `a \<noteq> 0`
   1.111      have "\<And>q r. divmod_int_rel b c (q, r) \<Longrightarrow> divmod_int_rel (a * b) (a * c) (q, a * r)"
   1.112 -      apply (auto simp add: divmod_int_rel_def) 
   1.113 +      apply (auto simp add: divmod_int_rel_def split: split_if_asm)
   1.114        apply (auto simp add: algebra_simps)
   1.115 -      apply (auto simp add: zero_less_mult_iff zero_le_mult_iff mult_le_0_iff mult_commute [of a] mult_less_cancel_right)
   1.116 +      apply (auto simp add: zero_less_mult_iff zero_le_mult_iff mult_le_0_iff mult_commute [of a] mult_less_cancel_right mult_less_0_iff)
   1.117        done
   1.118      moreover with `c \<noteq> 0` divmod_int_rel_div_mod have "divmod_int_rel b c (b div c, b mod c)" by auto
   1.119      ultimately have "divmod_int_rel (a * b) (a * c) (b div c, a * (b mod c))" .
   1.120 @@ -1949,7 +1947,7 @@
   1.121        ==> divmod_int_rel a (b * c) (q div c, b*(q mod c) + r)"
   1.122  by (auto simp add: mult_ac divmod_int_rel_def linorder_neq_iff
   1.123                     zero_less_mult_iff right_distrib [symmetric] 
   1.124 -                   zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4)
   1.125 +                   zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4 mult_less_0_iff split: split_if_asm)
   1.126  
   1.127  lemma zdiv_zmult2_eq: "(0::int) < c ==> a div (b*c) = (a div b) div c"
   1.128  apply (case_tac "b = 0", simp)