# HG changeset patch # User huffman # Date 1332841276 -7200 # Node ID 98bddfa0f717ed8e05c8d3b49536c763541a7714 # Parent f8cf96545eed670dc23720e64a55817e51d55afc extend definition of divmod_int_rel to handle denominator=0 case diff -r f8cf96545eed -r 98bddfa0f717 src/HOL/Divides.thy --- a/src/HOL/Divides.thy Tue Mar 27 11:02:18 2012 +0200 +++ b/src/HOL/Divides.thy Tue Mar 27 11:41:16 2012 +0200 @@ -1133,8 +1133,8 @@ definition divmod_int_rel :: "int \ int \ int \ int \ bool" where --{*definition of quotient and remainder*} - "divmod_int_rel a b = (\(q, r). a = b * q + r \ - (if 0 < b then 0 \ r \ r < b else b < r \ r \ 0))" + "divmod_int_rel a b = (\(q, r). a = b * q + r \ + (if 0 < b then 0 \ r \ r < b else if b < 0 then b < r \ r \ 0 else q = 0))" definition adjust :: "int \ int \ int \ int \ int" where --{*for the division algorithm*} @@ -1332,19 +1332,23 @@ subsubsection {* Existence Shown by Proving the Division Algorithm to be Correct *} (*the case a=0*) -lemma divmod_int_rel_0: "b \ 0 ==> divmod_int_rel 0 b (0, 0)" +lemma divmod_int_rel_0: "divmod_int_rel 0 b (0, 0)" by (auto simp add: divmod_int_rel_def linorder_neq_iff) lemma posDivAlg_0 [simp]: "posDivAlg 0 b = (0, 0)" by (subst posDivAlg.simps, auto) +lemma posDivAlg_0_right [simp]: "posDivAlg a 0 = (0, a)" +by (subst posDivAlg.simps, auto) + lemma negDivAlg_minus1 [simp]: "negDivAlg -1 b = (-1, b - 1)" by (subst negDivAlg.simps, auto) lemma divmod_int_rel_neg: "divmod_int_rel (-a) (-b) qr ==> divmod_int_rel a b (apsnd uminus qr)" -by (auto simp add: split_ifs divmod_int_rel_def) - -lemma divmod_int_correct: "b \ 0 ==> divmod_int_rel a b (divmod_int a b)" +by (auto simp add: divmod_int_rel_def) + +lemma divmod_int_correct: "divmod_int_rel a b (divmod_int a b)" +apply (cases "b = 0", simp add: divmod_int_def divmod_int_rel_def) by (force simp add: linorder_neq_iff divmod_int_rel_0 divmod_int_def divmod_int_rel_neg posDivAlg_correct negDivAlg_correct) @@ -1411,19 +1415,15 @@ subsubsection {* General Properties of div and mod *} -lemma divmod_int_rel_div_mod: "b \ 0 ==> divmod_int_rel a b (a div b, a mod b)" +lemma divmod_int_rel_div_mod: "divmod_int_rel a b (a div b, a mod b)" apply (cut_tac a = a and b = b in zmod_zdiv_equality) apply (force simp add: divmod_int_rel_def linorder_neq_iff) done lemma divmod_int_rel_div: "[| divmod_int_rel a b (q, r) |] ==> a div b = q" -apply (cases "b = 0") -apply (simp add: divmod_int_rel_def) by (simp add: divmod_int_rel_div_mod [THEN unique_quotient]) lemma divmod_int_rel_mod: "[| divmod_int_rel a b (q, r) |] ==> a mod b = r" -apply (cases "b = 0") -apply (simp add: divmod_int_rel_def) by (simp add: divmod_int_rel_div_mod [THEN unique_remainder]) lemma div_pos_pos_trivial: "[| (0::int) \ a; a < b |] ==> a div b = 0" @@ -1463,7 +1463,6 @@ (*Simpler laws such as -a div b = -(a div b) FAIL, but see just below*) lemma zdiv_zminus_zminus [simp]: "(-a) div (-b) = a div (b::int)" -apply (case_tac "b = 0", simp) apply (simp add: divmod_int_rel_div_mod [THEN divmod_int_rel_neg, simplified, THEN divmod_int_rel_div, THEN sym]) @@ -1471,7 +1470,6 @@ (*Simpler laws such as -a mod b = -(a mod b) FAIL, but see just below*) lemma zmod_zminus_zminus [simp]: "(-a) mod (-b) = - (a mod (b::int))" -apply (case_tac "b = 0", simp) apply (subst divmod_int_rel_div_mod [THEN divmod_int_rel_neg, simplified, THEN divmod_int_rel_mod], auto) done @@ -1480,7 +1478,7 @@ subsubsection {* Laws for div and mod with Unary Minus *} lemma zminus1_lemma: - "divmod_int_rel a b (q, r) + "divmod_int_rel a b (q, r) ==> b \ 0 ==> divmod_int_rel (-a) b (if r=0 then -q else -q - 1, if r=0 then 0 else b-r)" by (force simp add: split_ifs divmod_int_rel_def linorder_neq_iff right_diff_distrib) @@ -1538,7 +1536,7 @@ apply (simp add: right_diff_distrib) done -lemma self_quotient: "[| divmod_int_rel a a (q, r) |] ==> q = 1" +lemma self_quotient: "[| divmod_int_rel a a (q, r); a \ 0 |] ==> q = 1" apply (simp add: split_ifs divmod_int_rel_def linorder_neq_iff) apply (rule order_antisym, safe, simp_all) apply (rule_tac [3] a = "-a" and r = "-r" in self_quotient_aux1) @@ -1546,8 +1544,8 @@ apply (force intro: self_quotient_aux1 self_quotient_aux2 simp add: add_commute)+ done -lemma self_remainder: "[| divmod_int_rel a a (q, r) |] ==> r = 0" -apply (frule self_quotient) +lemma self_remainder: "[| divmod_int_rel a a (q, r); a \ 0 |] ==> r = 0" +apply (frule (1) self_quotient) apply (simp add: divmod_int_rel_def) done @@ -1853,9 +1851,9 @@ case True then have "b \ 0" and "c \ 0" by auto with `a \ 0` have "\q r. divmod_int_rel b c (q, r) \ divmod_int_rel (a * b) (a * c) (q, a * r)" - apply (auto simp add: divmod_int_rel_def) + apply (auto simp add: divmod_int_rel_def split: split_if_asm) apply (auto simp add: algebra_simps) - apply (auto simp add: zero_less_mult_iff zero_le_mult_iff mult_le_0_iff mult_commute [of a] mult_less_cancel_right) + 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) done moreover with `c \ 0` divmod_int_rel_div_mod have "divmod_int_rel b c (b div c, b mod c)" by auto ultimately have "divmod_int_rel (a * b) (a * c) (b div c, a * (b mod c))" . @@ -1949,7 +1947,7 @@ ==> divmod_int_rel a (b * c) (q div c, b*(q mod c) + r)" by (auto simp add: mult_ac divmod_int_rel_def linorder_neq_iff zero_less_mult_iff right_distrib [symmetric] - zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4) + zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4 mult_less_0_iff split: split_if_asm) lemma zdiv_zmult2_eq: "(0::int) < c ==> a div (b*c) = (a div b) div c" apply (case_tac "b = 0", simp)