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)