src/HOL/Divides.thy
 changeset 47139 98bddfa0f717 parent 47138 f8cf96545eed child 47140 97c3676c5c94
```     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.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.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.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.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.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)
```