diff -r 76401b2ee871 -r 56db9f3a6b3e src/HOL/Integ/IntDiv.ML --- a/src/HOL/Integ/IntDiv.ML Mon Oct 22 11:01:30 2001 +0200 +++ b/src/HOL/Integ/IntDiv.ML Mon Oct 22 11:54:22 2001 +0200 @@ -34,21 +34,21 @@ (*** Uniqueness and monotonicity of quotients and remainders ***) -Goal "[| b*q' + r' <= b*q + r; Numeral0 <= r'; Numeral0 < b; r < b |] \ +Goal "[| b*q' + r' <= b*q + r; 0 <= r'; 0 < b; r < b |] \ \ ==> q' <= (q::int)"; by (subgoal_tac "r' + b * (q'-q) <= r" 1); by (simp_tac (simpset() addsimps [zdiff_zmult_distrib2]) 2); -by (subgoal_tac "Numeral0 < b * (Numeral1 + q - q')" 1); +by (subgoal_tac "0 < b * (1 + q - q')" 1); by (etac order_le_less_trans 2); by (full_simp_tac (simpset() addsimps [zdiff_zmult_distrib2, zadd_zmult_distrib2]) 2); -by (subgoal_tac "b * q' < b * (Numeral1 + q)" 1); +by (subgoal_tac "b * q' < b * (1 + q)" 1); by (full_simp_tac (simpset() addsimps [zdiff_zmult_distrib2, zadd_zmult_distrib2]) 2); by (asm_full_simp_tac (simpset() addsimps [zmult_zless_cancel1]) 1); qed "unique_quotient_lemma"; -Goal "[| b*q' + r' <= b*q + r; r <= Numeral0; b < Numeral0; b < r' |] \ +Goal "[| b*q' + r' <= b*q + r; r <= 0; b < 0; b < r' |] \ \ ==> q <= (q'::int)"; by (res_inst_tac [("b", "-b"), ("r", "-r'"), ("r'", "-r")] unique_quotient_lemma 1); @@ -57,7 +57,7 @@ qed "unique_quotient_lemma_neg"; -Goal "[| quorem ((a,b), (q,r)); quorem ((a,b), (q',r')); b ~= Numeral0 |] \ +Goal "[| quorem ((a,b), (q,r)); quorem ((a,b), (q',r')); b ~= 0 |] \ \ ==> q = q'"; by (asm_full_simp_tac (simpset() addsimps split_ifs@ @@ -72,7 +72,7 @@ qed "unique_quotient"; -Goal "[| quorem ((a,b), (q,r)); quorem ((a,b), (q',r')); b ~= Numeral0 |] \ +Goal "[| quorem ((a,b), (q,r)); quorem ((a,b), (q',r')); b ~= 0 |] \ \ ==> r = r'"; by (subgoal_tac "q = q'" 1); by (blast_tac (claset() addIs [unique_quotient]) 2); @@ -83,9 +83,9 @@ (*** Correctness of posDivAlg, the division algorithm for a>=0 and b>0 ***) -Goal "adjust a b (q,r) = (let diff = r-b in \ -\ if Numeral0 <= diff then (2*q + Numeral1, diff) \ -\ else (2*q, r))"; +Goal "adjust b (q,r) = (let diff = r-b in \ +\ if 0 <= diff then (2*q + 1, diff) \ +\ else (2*q, r))"; by (simp_tac (simpset() addsimps [Let_def,adjust_def]) 1); qed "adjust_eq"; Addsimps [adjust_eq]; @@ -101,9 +101,9 @@ bind_thm ("posDivAlg_raw_eqn", lemma RS hd posDivAlg.simps); (**use with simproc to avoid re-proving the premise*) -Goal "Numeral0 < b ==> \ +Goal "0 < b ==> \ \ posDivAlg (a,b) = \ -\ (if a Numeral0 < b --> quorem ((a, b), posDivAlg (a, b))"; +Goal "0 <= a --> 0 < b --> quorem ((a, b), posDivAlg (a, b))"; by (induct_thm_tac posDivAlg_induct "a b" 1); by Auto_tac; by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [quorem_def]))); @@ -139,9 +139,9 @@ bind_thm ("negDivAlg_raw_eqn", lemma RS hd negDivAlg.simps); (**use with simproc to avoid re-proving the premise*) -Goal "Numeral0 < b ==> \ +Goal "0 < b ==> \ \ negDivAlg (a,b) = \ -\ (if Numeral0<=a+b then (-1,a+b) else adjust a b (negDivAlg(a, 2*b)))"; +\ (if 0<=a+b then (-1,a+b) else adjust b (negDivAlg(a, 2*b)))"; by (rtac (negDivAlg_raw_eqn RS trans) 1); by (Asm_simp_tac 1); qed "negDivAlg_eqn"; @@ -151,7 +151,7 @@ (*Correctness of negDivAlg: it computes quotients correctly It doesn't work if a=0 because the 0/b=0 rather than -1*) -Goal "a < Numeral0 --> Numeral0 < b --> quorem ((a, b), negDivAlg (a, b))"; +Goal "a < 0 --> 0 < b --> quorem ((a, b), negDivAlg (a, b))"; by (induct_thm_tac negDivAlg_induct "a b" 1); by Auto_tac; by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [quorem_def]))); @@ -168,18 +168,18 @@ (*** Existence shown by proving the division algorithm to be correct ***) (*the case a=0*) -Goal "b ~= Numeral0 ==> quorem ((Numeral0,b), (Numeral0,Numeral0))"; +Goal "b ~= 0 ==> quorem ((0,b), (0,0))"; by (auto_tac (claset(), simpset() addsimps [quorem_def, linorder_neq_iff])); qed "quorem_0"; -Goal "posDivAlg (Numeral0, b) = (Numeral0, Numeral0)"; +Goal "posDivAlg (0, b) = (0, 0)"; by (stac posDivAlg_raw_eqn 1); by Auto_tac; qed "posDivAlg_0"; Addsimps [posDivAlg_0]; -Goal "negDivAlg (-1, b) = (-1, b-Numeral1)"; +Goal "negDivAlg (-1, b) = (-1, b - 1)"; by (stac negDivAlg_raw_eqn 1); by Auto_tac; qed "negDivAlg_minus1"; @@ -194,7 +194,7 @@ by (auto_tac (claset(), simpset() addsimps split_ifs@[quorem_def])); qed "quorem_neg"; -Goal "b ~= Numeral0 ==> quorem ((a,b), divAlg(a,b))"; +Goal "b ~= 0 ==> quorem ((a,b), divAlg(a,b))"; by (auto_tac (claset(), simpset() addsimps [quorem_0, divAlg_def])); by (REPEAT_FIRST (resolve_tac [quorem_neg, posDivAlg_correct, @@ -206,11 +206,11 @@ (** Arbitrary definitions for division by zero. Useful to simplify certain equations **) -Goal "a div (Numeral0::int) = Numeral0"; +Goal "a div (0::int) = 0"; by (simp_tac (simpset() addsimps [div_def, divAlg_def, posDivAlg_raw_eqn]) 1); qed "DIVISION_BY_ZERO_ZDIV"; (*NOT for adding to default simpset*) -Goal "a mod (Numeral0::int) = a"; +Goal "a mod (0::int) = a"; by (simp_tac (simpset() addsimps [mod_def, divAlg_def, posDivAlg_raw_eqn]) 1); qed "DIVISION_BY_ZERO_ZMOD"; (*NOT for adding to default simpset*) @@ -222,20 +222,20 @@ (** Basic laws about division and remainder **) Goal "(a::int) = b * (a div b) + (a mod b)"; -by (zdiv_undefined_case_tac "b = Numeral0" 1); +by (zdiv_undefined_case_tac "b = 0" 1); by (cut_inst_tac [("a","a"),("b","b")] divAlg_correct 1); by (auto_tac (claset(), simpset() addsimps [quorem_def, div_def, mod_def])); qed "zmod_zdiv_equality"; -Goal "(Numeral0::int) < b ==> Numeral0 <= a mod b & a mod b < b"; +Goal "(0::int) < b ==> 0 <= a mod b & a mod b < b"; by (cut_inst_tac [("a","a"),("b","b")] divAlg_correct 1); by (auto_tac (claset(), simpset() addsimps [quorem_def, mod_def])); bind_thm ("pos_mod_sign", result() RS conjunct1); bind_thm ("pos_mod_bound", result() RS conjunct2); -Goal "b < (Numeral0::int) ==> a mod b <= Numeral0 & b < a mod b"; +Goal "b < (0::int) ==> a mod b <= 0 & b < a mod b"; by (cut_inst_tac [("a","a"),("b","b")] divAlg_correct 1); by (auto_tac (claset(), simpset() addsimps [quorem_def, div_def, mod_def])); @@ -245,7 +245,7 @@ (** proving general properties of div and mod **) -Goal "b ~= Numeral0 ==> quorem ((a, b), (a div b, a mod b))"; +Goal "b ~= 0 ==> quorem ((a, b), (a div b, a mod b))"; by (cut_inst_tac [("a","a"),("b","b")] zmod_zdiv_equality 1); by (auto_tac (claset(), @@ -254,42 +254,42 @@ neg_mod_sign, neg_mod_bound])); qed "quorem_div_mod"; -Goal "[| quorem((a,b),(q,r)); b ~= Numeral0 |] ==> a div b = q"; +Goal "[| quorem((a,b),(q,r)); b ~= 0 |] ==> a div b = q"; by (asm_simp_tac (simpset() addsimps [quorem_div_mod RS unique_quotient]) 1); qed "quorem_div"; -Goal "[| quorem((a,b),(q,r)); b ~= Numeral0 |] ==> a mod b = r"; +Goal "[| quorem((a,b),(q,r)); b ~= 0 |] ==> a mod b = r"; by (asm_simp_tac (simpset() addsimps [quorem_div_mod RS unique_remainder]) 1); qed "quorem_mod"; -Goal "[| (Numeral0::int) <= a; a < b |] ==> a div b = Numeral0"; +Goal "[| (0::int) <= a; a < b |] ==> a div b = 0"; by (rtac quorem_div 1); by (auto_tac (claset(), simpset() addsimps [quorem_def])); qed "div_pos_pos_trivial"; -Goal "[| a <= (Numeral0::int); b < a |] ==> a div b = Numeral0"; +Goal "[| a <= (0::int); b < a |] ==> a div b = 0"; by (rtac quorem_div 1); by (auto_tac (claset(), simpset() addsimps [quorem_def])); qed "div_neg_neg_trivial"; -Goal "[| (Numeral0::int) < a; a+b <= Numeral0 |] ==> a div b = -1"; +Goal "[| (0::int) < a; a+b <= 0 |] ==> a div b = -1"; by (rtac quorem_div 1); by (auto_tac (claset(), simpset() addsimps [quorem_def])); qed "div_pos_neg_trivial"; -(*There is no div_neg_pos_trivial because Numeral0 div b = Numeral0 would supersede it*) +(*There is no div_neg_pos_trivial because 0 div b = 0 would supersede it*) -Goal "[| (Numeral0::int) <= a; a < b |] ==> a mod b = a"; -by (res_inst_tac [("q","Numeral0")] quorem_mod 1); +Goal "[| (0::int) <= a; a < b |] ==> a mod b = a"; +by (res_inst_tac [("q","0")] quorem_mod 1); by (auto_tac (claset(), simpset() addsimps [quorem_def])); qed "mod_pos_pos_trivial"; -Goal "[| a <= (Numeral0::int); b < a |] ==> a mod b = a"; -by (res_inst_tac [("q","Numeral0")] quorem_mod 1); +Goal "[| a <= (0::int); b < a |] ==> a mod b = a"; +by (res_inst_tac [("q","0")] quorem_mod 1); by (auto_tac (claset(), simpset() addsimps [quorem_def])); qed "mod_neg_neg_trivial"; -Goal "[| (Numeral0::int) < a; a+b <= Numeral0 |] ==> a mod b = a+b"; +Goal "[| (0::int) < a; a+b <= 0 |] ==> a mod b = a+b"; by (res_inst_tac [("q","-1")] quorem_mod 1); by (auto_tac (claset(), simpset() addsimps [quorem_def])); qed "mod_pos_neg_trivial"; @@ -299,7 +299,7 @@ (*Simpler laws such as -a div b = -(a div b) FAIL, but see just below*) Goal "(-a) div (-b) = a div (b::int)"; -by (zdiv_undefined_case_tac "b = Numeral0" 1); +by (zdiv_undefined_case_tac "b = 0" 1); by (stac ((simplify(simpset()) (quorem_div_mod RS quorem_neg)) RS quorem_div) 1); by Auto_tac; @@ -308,7 +308,7 @@ (*Simpler laws such as -a mod b = -(a mod b) FAIL, but see just below*) Goal "(-a) mod (-b) = - (a mod (b::int))"; -by (zdiv_undefined_case_tac "b = Numeral0" 1); +by (zdiv_undefined_case_tac "b = 0" 1); by (stac ((simplify(simpset()) (quorem_div_mod RS quorem_neg)) RS quorem_mod) 1); by Auto_tac; @@ -319,8 +319,8 @@ (*** div, mod and unary minus ***) Goal "quorem((a,b),(q,r)) \ -\ ==> quorem ((-a,b), (if r=Numeral0 then -q else -q-Numeral1), \ -\ (if r=Numeral0 then Numeral0 else b-r))"; +\ ==> quorem ((-a,b), (if r=0 then -q else -q - 1), \ +\ (if r=0 then 0 else b-r))"; by (auto_tac (claset(), simpset() addsimps split_ifs@ @@ -328,14 +328,14 @@ zdiff_zmult_distrib2])); val lemma = result(); -Goal "b ~= (Numeral0::int) \ +Goal "b ~= (0::int) \ \ ==> (-a) div b = \ -\ (if a mod b = Numeral0 then - (a div b) else - (a div b) - Numeral1)"; +\ (if a mod b = 0 then - (a div b) else - (a div b) - 1)"; by (blast_tac (claset() addIs [quorem_div_mod RS lemma RS quorem_div]) 1); qed "zdiv_zminus1_eq_if"; -Goal "(-a::int) mod b = (if a mod b = Numeral0 then Numeral0 else b - (a mod b))"; -by (zdiv_undefined_case_tac "b = Numeral0" 1); +Goal "(-a::int) mod b = (if a mod b = 0 then 0 else b - (a mod b))"; +by (zdiv_undefined_case_tac "b = 0" 1); by (blast_tac (claset() addIs [quorem_div_mod RS lemma RS quorem_mod]) 1); qed "zmod_zminus1_eq_if"; @@ -349,32 +349,32 @@ by Auto_tac; qed "zmod_zminus2"; -Goal "b ~= (Numeral0::int) \ +Goal "b ~= (0::int) \ \ ==> a div (-b) = \ -\ (if a mod b = Numeral0 then - (a div b) else - (a div b) - Numeral1)"; +\ (if a mod b = 0 then - (a div b) else - (a div b) - 1)"; by (asm_simp_tac (simpset() addsimps [zdiv_zminus1_eq_if, zdiv_zminus2]) 1); qed "zdiv_zminus2_eq_if"; -Goal "a mod (-b::int) = (if a mod b = Numeral0 then Numeral0 else (a mod b) - b)"; +Goal "a mod (-b::int) = (if a mod b = 0 then 0 else (a mod b) - b)"; by (asm_simp_tac (simpset() addsimps [zmod_zminus1_eq_if, zmod_zminus2]) 1); qed "zmod_zminus2_eq_if"; (*** division of a number by itself ***) -Goal "[| (Numeral0::int) < a; a = r + a*q; r < a |] ==> Numeral1 <= q"; -by (subgoal_tac "Numeral0 < a*q" 1); +Goal "[| (0::int) < a; a = r + a*q; r < a |] ==> 1 <= q"; +by (subgoal_tac "0 < a*q" 1); by (arith_tac 2); by (asm_full_simp_tac (simpset() addsimps [int_0_less_mult_iff]) 1); val lemma1 = result(); -Goal "[| (Numeral0::int) < a; a = r + a*q; Numeral0 <= r |] ==> q <= Numeral1"; -by (subgoal_tac "Numeral0 <= a*(Numeral1-q)" 1); +Goal "[| (0::int) < a; a = r + a*q; 0 <= r |] ==> q <= 1"; +by (subgoal_tac "0 <= a*(1-q)" 1); by (asm_simp_tac (simpset() addsimps [zdiff_zmult_distrib2]) 2); by (asm_full_simp_tac (simpset() addsimps [int_0_le_mult_iff]) 1); val lemma2 = result(); -Goal "[| quorem((a,a),(q,r)); a ~= (Numeral0::int) |] ==> q = Numeral1"; +Goal "[| quorem((a,a),(q,r)); a ~= (0::int) |] ==> q = 1"; by (asm_full_simp_tac (simpset() addsimps split_ifs@[quorem_def, linorder_neq_iff]) 1); by (rtac order_antisym 1); @@ -386,20 +386,20 @@ simpset() addsimps [zadd_commute, zmult_zminus]) 1)); qed "self_quotient"; -Goal "[| quorem((a,a),(q,r)); a ~= (Numeral0::int) |] ==> r = Numeral0"; +Goal "[| quorem((a,a),(q,r)); a ~= (0::int) |] ==> r = 0"; by (ftac self_quotient 1); by (assume_tac 1); by (asm_full_simp_tac (simpset() addsimps [quorem_def]) 1); qed "self_remainder"; -Goal "a ~= Numeral0 ==> a div a = (Numeral1::int)"; +Goal "a ~= 0 ==> a div a = (1::int)"; by (asm_simp_tac (simpset() addsimps [quorem_div_mod RS self_quotient]) 1); qed "zdiv_self"; Addsimps [zdiv_self]; (*Here we have 0 mod 0 = 0, also assumed by Knuth (who puts m mod 0 = 0) *) -Goal "a mod a = (Numeral0::int)"; -by (zdiv_undefined_case_tac "a = Numeral0" 1); +Goal "a mod a = (0::int)"; +by (zdiv_undefined_case_tac "a = 0" 1); by (asm_simp_tac (simpset() addsimps [quorem_div_mod RS self_remainder]) 1); qed "zmod_self"; Addsimps [zmod_self]; @@ -407,65 +407,65 @@ (*** Computation of division and remainder ***) -Goal "(Numeral0::int) div b = Numeral0"; +Goal "(0::int) div b = 0"; by (simp_tac (simpset() addsimps [div_def, divAlg_def]) 1); qed "zdiv_zero"; -Goal "(Numeral0::int) < b ==> -1 div b = -1"; +Goal "(0::int) < b ==> -1 div b = -1"; by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1); qed "div_eq_minus1"; -Goal "(Numeral0::int) mod b = Numeral0"; +Goal "(0::int) mod b = 0"; by (simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1); qed "zmod_zero"; Addsimps [zdiv_zero, zmod_zero]; -Goal "(Numeral0::int) < b ==> -1 div b = -1"; +Goal "(0::int) < b ==> -1 div b = -1"; by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1); qed "zdiv_minus1"; -Goal "(Numeral0::int) < b ==> -1 mod b = b-Numeral1"; +Goal "(0::int) < b ==> -1 mod b = b - 1"; by (asm_simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1); qed "zmod_minus1"; (** a positive, b positive **) -Goal "[| Numeral0 < a; Numeral0 <= b |] ==> a div b = fst (posDivAlg(a,b))"; +Goal "[| 0 < a; 0 <= b |] ==> a div b = fst (posDivAlg(a,b))"; by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1); qed "div_pos_pos"; -Goal "[| Numeral0 < a; Numeral0 <= b |] ==> a mod b = snd (posDivAlg(a,b))"; +Goal "[| 0 < a; 0 <= b |] ==> a mod b = snd (posDivAlg(a,b))"; by (asm_simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1); qed "mod_pos_pos"; (** a negative, b positive **) -Goal "[| a < Numeral0; Numeral0 < b |] ==> a div b = fst (negDivAlg(a,b))"; +Goal "[| a < 0; 0 < b |] ==> a div b = fst (negDivAlg(a,b))"; by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1); qed "div_neg_pos"; -Goal "[| a < Numeral0; Numeral0 < b |] ==> a mod b = snd (negDivAlg(a,b))"; +Goal "[| a < 0; 0 < b |] ==> a mod b = snd (negDivAlg(a,b))"; by (asm_simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1); qed "mod_neg_pos"; (** a positive, b negative **) -Goal "[| Numeral0 < a; b < Numeral0 |] ==> a div b = fst (negateSnd(negDivAlg(-a,-b)))"; +Goal "[| 0 < a; b < 0 |] ==> a div b = fst (negateSnd(negDivAlg(-a,-b)))"; by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1); qed "div_pos_neg"; -Goal "[| Numeral0 < a; b < Numeral0 |] ==> a mod b = snd (negateSnd(negDivAlg(-a,-b)))"; +Goal "[| 0 < a; b < 0 |] ==> a mod b = snd (negateSnd(negDivAlg(-a,-b)))"; by (asm_simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1); qed "mod_pos_neg"; (** a negative, b negative **) -Goal "[| a < Numeral0; b <= Numeral0 |] ==> a div b = fst (negateSnd(posDivAlg(-a,-b)))"; +Goal "[| a < 0; b <= 0 |] ==> a div b = fst (negateSnd(posDivAlg(-a,-b)))"; by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1); qed "div_neg_neg"; -Goal "[| a < Numeral0; b <= Numeral0 |] ==> a mod b = snd (negateSnd(posDivAlg(-a,-b)))"; +Goal "[| a < 0; b <= 0 |] ==> a mod b = snd (negateSnd(posDivAlg(-a,-b)))"; by (asm_simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1); qed "mod_neg_neg"; @@ -478,20 +478,20 @@ (** Special-case simplification **) -Goal "a mod (Numeral1::int) = Numeral0"; -by (cut_inst_tac [("a","a"),("b","Numeral1")] pos_mod_sign 1); -by (cut_inst_tac [("a","a"),("b","Numeral1")] pos_mod_bound 2); +Goal "a mod (1::int) = 0"; +by (cut_inst_tac [("a","a"),("b","1")] pos_mod_sign 1); +by (cut_inst_tac [("a","a"),("b","1")] pos_mod_bound 2); by Auto_tac; qed "zmod_1"; Addsimps [zmod_1]; -Goal "a div (Numeral1::int) = a"; -by (cut_inst_tac [("a","a"),("b","Numeral1")] zmod_zdiv_equality 1); +Goal "a div (1::int) = a"; +by (cut_inst_tac [("a","a"),("b","1")] zmod_zdiv_equality 1); by Auto_tac; qed "zdiv_1"; Addsimps [zdiv_1]; -Goal "a mod (-1::int) = Numeral0"; +Goal "a mod (-1::int) = 0"; by (cut_inst_tac [("a","a"),("b","-1")] neg_mod_sign 1); by (cut_inst_tac [("a","a"),("b","-1")] neg_mod_bound 2); by Auto_tac; @@ -504,10 +504,19 @@ qed "zdiv_minus1_right"; Addsimps [zdiv_minus1_right]; +(** The last remaining cases: 1 div z and 1 mod z **) + +Addsimps (map (fn th => int_0_less_1 RS inst "b" "number_of ?w" th) + [div_pos_pos, div_pos_neg, mod_pos_pos, mod_pos_neg]); + +Addsimps (map (read_instantiate_sg (sign_of (the_context ())) + [("a", "1"), ("b", "number_of ?w")]) + [posDivAlg_eqn, negDivAlg_eqn]); + (*** Monotonicity in the first argument (divisor) ***) -Goal "[| a <= a'; Numeral0 < (b::int) |] ==> a div b <= a' div b"; +Goal "[| a <= a'; 0 < (b::int) |] ==> a div b <= a' div b"; by (cut_inst_tac [("a","a"),("b","b")] zmod_zdiv_equality 1); by (cut_inst_tac [("a","a'"),("b","b")] zmod_zdiv_equality 1); by (rtac unique_quotient_lemma 1); @@ -516,7 +525,7 @@ by (ALLGOALS (asm_simp_tac (simpset() addsimps [pos_mod_sign,pos_mod_bound]))); qed "zdiv_mono1"; -Goal "[| a <= a'; (b::int) < Numeral0 |] ==> a' div b <= a div b"; +Goal "[| a <= a'; (b::int) < 0 |] ==> a' div b <= a div b"; by (cut_inst_tac [("a","a"),("b","b")] zmod_zdiv_equality 1); by (cut_inst_tac [("a","a'"),("b","b")] zmod_zdiv_equality 1); by (rtac unique_quotient_lemma_neg 1); @@ -528,14 +537,14 @@ (*** Monotonicity in the second argument (dividend) ***) -Goal "[| b*q + r = b'*q' + r'; Numeral0 <= b'*q' + r'; \ -\ r' < b'; Numeral0 <= r; Numeral0 < b'; b' <= b |] \ +Goal "[| b*q + r = b'*q' + r'; 0 <= b'*q' + r'; \ +\ r' < b'; 0 <= r; 0 < b'; b' <= b |] \ \ ==> q <= (q'::int)"; -by (subgoal_tac "Numeral0 <= q'" 1); - by (subgoal_tac "Numeral0 < b'*(q' + Numeral1)" 2); +by (subgoal_tac "0 <= q'" 1); + by (subgoal_tac "0 < b'*(q' + 1)" 2); by (asm_simp_tac (simpset() addsimps [zadd_zmult_distrib2]) 3); by (asm_full_simp_tac (simpset() addsimps [int_0_less_mult_iff]) 2); -by (subgoal_tac "b*q < b*(q' + Numeral1)" 1); +by (subgoal_tac "b*q < b*(q' + 1)" 1); by (asm_full_simp_tac (simpset() addsimps [zmult_zless_cancel1]) 1); by (subgoal_tac "b*q = r' - r + b'*q'" 1); by (Simp_tac 2); @@ -545,9 +554,9 @@ by Auto_tac; qed "zdiv_mono2_lemma"; -Goal "[| (Numeral0::int) <= a; Numeral0 < b'; b' <= b |] \ +Goal "[| (0::int) <= a; 0 < b'; b' <= b |] \ \ ==> a div b <= a div b'"; -by (subgoal_tac "b ~= Numeral0" 1); +by (subgoal_tac "b ~= 0" 1); by (arith_tac 2); by (cut_inst_tac [("a","a"),("b","b")] zmod_zdiv_equality 1); by (cut_inst_tac [("a","a"),("b","b'")] zmod_zdiv_equality 1); @@ -557,14 +566,14 @@ by (ALLGOALS (asm_simp_tac (simpset() addsimps [pos_mod_sign,pos_mod_bound]))); qed "zdiv_mono2"; -Goal "[| b*q + r = b'*q' + r'; b'*q' + r' < Numeral0; \ -\ r < b; Numeral0 <= r'; Numeral0 < b'; b' <= b |] \ +Goal "[| b*q + r = b'*q' + r'; b'*q' + r' < 0; \ +\ r < b; 0 <= r'; 0 < b'; b' <= b |] \ \ ==> q' <= (q::int)"; -by (subgoal_tac "q' < Numeral0" 1); - by (subgoal_tac "b'*q' < Numeral0" 2); +by (subgoal_tac "q' < 0" 1); + by (subgoal_tac "b'*q' < 0" 2); by (arith_tac 3); by (asm_full_simp_tac (simpset() addsimps [zmult_less_0_iff]) 2); -by (subgoal_tac "b*q' < b*(q + Numeral1)" 1); +by (subgoal_tac "b*q' < b*(q + 1)" 1); by (asm_full_simp_tac (simpset() addsimps [zmult_zless_cancel1]) 1); by (asm_simp_tac (simpset() addsimps [zadd_zmult_distrib2]) 1); by (subgoal_tac "b*q' <= b'*q'" 1); @@ -574,7 +583,7 @@ by (arith_tac 1); qed "zdiv_mono2_neg_lemma"; -Goal "[| a < (Numeral0::int); Numeral0 < b'; b' <= b |] \ +Goal "[| a < (0::int); 0 < b'; b' <= b |] \ \ ==> a div b' <= a div b"; by (cut_inst_tac [("a","a"),("b","b")] zmod_zdiv_equality 1); by (cut_inst_tac [("a","a"),("b","b'")] zmod_zdiv_equality 1); @@ -589,7 +598,7 @@ (** proving (a*b) div c = a * (b div c) + a * (b mod c) **) -Goal "[| quorem((b,c),(q,r)); c ~= Numeral0 |] \ +Goal "[| quorem((b,c),(q,r)); c ~= 0 |] \ \ ==> quorem ((a*b, c), (a*q + a*r div c, a*r mod c))"; by (auto_tac (claset(), @@ -602,12 +611,12 @@ val lemma = result(); Goal "(a*b) div c = a*(b div c) + a*(b mod c) div (c::int)"; -by (zdiv_undefined_case_tac "c = Numeral0" 1); +by (zdiv_undefined_case_tac "c = 0" 1); by (blast_tac (claset() addIs [quorem_div_mod RS lemma RS quorem_div]) 1); qed "zdiv_zmult1_eq"; Goal "(a*b) mod c = a*(b mod c) mod (c::int)"; -by (zdiv_undefined_case_tac "c = Numeral0" 1); +by (zdiv_undefined_case_tac "c = 0" 1); by (blast_tac (claset() addIs [quorem_div_mod RS lemma RS quorem_mod]) 1); qed "zmod_zmult1_eq"; @@ -623,27 +632,27 @@ by (rtac zmod_zmult1_eq 1); qed "zmod_zmult_distrib"; -Goal "b ~= (Numeral0::int) ==> (a*b) div b = a"; +Goal "b ~= (0::int) ==> (a*b) div b = a"; by (asm_simp_tac (simpset() addsimps [zdiv_zmult1_eq]) 1); qed "zdiv_zmult_self1"; -Goal "b ~= (Numeral0::int) ==> (b*a) div b = a"; +Goal "b ~= (0::int) ==> (b*a) div b = a"; by (stac zmult_commute 1 THEN etac zdiv_zmult_self1 1); qed "zdiv_zmult_self2"; Addsimps [zdiv_zmult_self1, zdiv_zmult_self2]; -Goal "(a*b) mod b = (Numeral0::int)"; +Goal "(a*b) mod b = (0::int)"; by (simp_tac (simpset() addsimps [zmod_zmult1_eq]) 1); qed "zmod_zmult_self1"; -Goal "(b*a) mod b = (Numeral0::int)"; +Goal "(b*a) mod b = (0::int)"; by (simp_tac (simpset() addsimps [zmult_commute, zmod_zmult1_eq]) 1); qed "zmod_zmult_self2"; Addsimps [zmod_zmult_self1, zmod_zmult_self2]; -Goal "(m mod d = Numeral0) = (EX q::int. m = d*q)"; +Goal "(m mod d = 0) = (EX q::int. m = d*q)"; by (cut_inst_tac [("a","m"),("b","d")] zmod_zdiv_equality 1); by Auto_tac; qed "zmod_eq_0_iff"; @@ -652,7 +661,7 @@ (** proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) **) -Goal "[| quorem((a,c),(aq,ar)); quorem((b,c),(bq,br)); c ~= Numeral0 |] \ +Goal "[| quorem((a,c),(aq,ar)); quorem((b,c),(bq,br)); c ~= 0 |] \ \ ==> quorem ((a+b, c), (aq + bq + (ar+br) div c, (ar+br) mod c))"; by (auto_tac (claset(), @@ -666,19 +675,19 @@ (*NOT suitable for rewriting: the RHS has an instance of the LHS*) Goal "(a+b) div (c::int) = a div c + b div c + ((a mod c + b mod c) div c)"; -by (zdiv_undefined_case_tac "c = Numeral0" 1); +by (zdiv_undefined_case_tac "c = 0" 1); by (blast_tac (claset() addIs [[quorem_div_mod,quorem_div_mod] MRS lemma RS quorem_div]) 1); qed "zdiv_zadd1_eq"; Goal "(a+b) mod (c::int) = (a mod c + b mod c) mod c"; -by (zdiv_undefined_case_tac "c = Numeral0" 1); +by (zdiv_undefined_case_tac "c = 0" 1); by (blast_tac (claset() addIs [[quorem_div_mod,quorem_div_mod] MRS lemma RS quorem_mod]) 1); qed "zmod_zadd1_eq"; -Goal "(a mod b) div b = (Numeral0::int)"; -by (zdiv_undefined_case_tac "b = Numeral0" 1); +Goal "(a mod b) div b = (0::int)"; +by (zdiv_undefined_case_tac "b = 0" 1); by (auto_tac (claset(), simpset() addsimps [linorder_neq_iff, pos_mod_sign, pos_mod_bound, div_pos_pos_trivial, @@ -687,7 +696,7 @@ Addsimps [mod_div_trivial]; Goal "(a mod b) mod b = a mod (b::int)"; -by (zdiv_undefined_case_tac "b = Numeral0" 1); +by (zdiv_undefined_case_tac "b = 0" 1); by (auto_tac (claset(), simpset() addsimps [linorder_neq_iff, pos_mod_sign, pos_mod_bound, mod_pos_pos_trivial, @@ -710,22 +719,22 @@ qed "zmod_zadd_right_eq"; -Goal "a ~= (Numeral0::int) ==> (a+b) div a = b div a + Numeral1"; +Goal "a ~= (0::int) ==> (a+b) div a = b div a + 1"; by (asm_simp_tac (simpset() addsimps [zdiv_zadd1_eq]) 1); qed "zdiv_zadd_self1"; -Goal "a ~= (Numeral0::int) ==> (b+a) div a = b div a + Numeral1"; +Goal "a ~= (0::int) ==> (b+a) div a = b div a + 1"; by (asm_simp_tac (simpset() addsimps [zdiv_zadd1_eq]) 1); qed "zdiv_zadd_self2"; Addsimps [zdiv_zadd_self1, zdiv_zadd_self2]; Goal "(a+b) mod a = b mod (a::int)"; -by (zdiv_undefined_case_tac "a = Numeral0" 1); +by (zdiv_undefined_case_tac "a = 0" 1); by (asm_simp_tac (simpset() addsimps [zmod_zadd1_eq]) 1); qed "zmod_zadd_self1"; Goal "(b+a) mod a = b mod (a::int)"; -by (zdiv_undefined_case_tac "a = Numeral0" 1); +by (zdiv_undefined_case_tac "a = 0" 1); by (asm_simp_tac (simpset() addsimps [zmod_zadd1_eq]) 1); qed "zmod_zadd_self2"; Addsimps [zmod_zadd_self1, zmod_zadd_self2]; @@ -739,8 +748,8 @@ (** first, four lemmas to bound the remainder for the cases b<0 and b>0 **) -Goal "[| (Numeral0::int) < c; b < r; r <= Numeral0 |] ==> b*c < b*(q mod c) + r"; -by (subgoal_tac "b * (c - q mod c) < r * Numeral1" 1); +Goal "[| (0::int) < c; b < r; r <= 0 |] ==> b*c < b*(q mod c) + r"; +by (subgoal_tac "b * (c - q mod c) < r * 1" 1); by (asm_full_simp_tac (simpset() addsimps [zdiff_zmult_distrib2]) 1); by (rtac order_le_less_trans 1); by (etac zmult_zless_mono1 2); @@ -748,23 +757,24 @@ by (auto_tac (claset(), simpset() addsimps zcompare_rls@ - [zadd_commute, add1_zle_eq, pos_mod_bound])); + [inst "z" "1" zadd_commute, add1_zle_eq, + pos_mod_bound])); val lemma1 = result(); -Goal "[| (Numeral0::int) < c; b < r; r <= Numeral0 |] ==> b * (q mod c) + r <= Numeral0"; -by (subgoal_tac "b * (q mod c) <= Numeral0" 1); +Goal "[| (0::int) < c; b < r; r <= 0 |] ==> b * (q mod c) + r <= 0"; +by (subgoal_tac "b * (q mod c) <= 0" 1); by (arith_tac 1); by (asm_simp_tac (simpset() addsimps [zmult_le_0_iff, pos_mod_sign]) 1); val lemma2 = result(); -Goal "[| (Numeral0::int) < c; Numeral0 <= r; r < b |] ==> Numeral0 <= b * (q mod c) + r"; -by (subgoal_tac "Numeral0 <= b * (q mod c)" 1); +Goal "[| (0::int) < c; 0 <= r; r < b |] ==> 0 <= b * (q mod c) + r"; +by (subgoal_tac "0 <= b * (q mod c)" 1); by (arith_tac 1); by (asm_simp_tac (simpset() addsimps [int_0_le_mult_iff, pos_mod_sign]) 1); val lemma3 = result(); -Goal "[| (Numeral0::int) < c; Numeral0 <= r; r < b |] ==> b * (q mod c) + r < b * c"; -by (subgoal_tac "r * Numeral1 < b * (c - q mod c)" 1); +Goal "[| (0::int) < c; 0 <= r; r < b |] ==> b * (q mod c) + r < b * c"; +by (subgoal_tac "r * 1 < b * (c - q mod c)" 1); by (asm_full_simp_tac (simpset() addsimps [zdiff_zmult_distrib2]) 1); by (rtac order_less_le_trans 1); by (etac zmult_zless_mono1 1); @@ -772,10 +782,11 @@ by (auto_tac (claset(), simpset() addsimps zcompare_rls@ - [zadd_commute, add1_zle_eq, pos_mod_bound])); + [inst "z" "1" zadd_commute, add1_zle_eq, + pos_mod_bound])); val lemma4 = result(); -Goal "[| quorem ((a,b), (q,r)); b ~= Numeral0; Numeral0 < c |] \ +Goal "[| quorem ((a,b), (q,r)); b ~= 0; 0 < c |] \ \ ==> quorem ((a, b*c), (q div c, b*(q mod c) + r))"; by (auto_tac (claset(), @@ -786,15 +797,15 @@ lemma1, lemma2, lemma3, lemma4])); val lemma = result(); -Goal "(Numeral0::int) < c ==> a div (b*c) = (a div b) div c"; -by (zdiv_undefined_case_tac "b = Numeral0" 1); +Goal "(0::int) < c ==> a div (b*c) = (a div b) div c"; +by (zdiv_undefined_case_tac "b = 0" 1); by (force_tac (claset(), simpset() addsimps [quorem_div_mod RS lemma RS quorem_div, zmult_eq_0_iff]) 1); qed "zdiv_zmult2_eq"; -Goal "(Numeral0::int) < c ==> a mod (b*c) = b*(a div b mod c) + a mod b"; -by (zdiv_undefined_case_tac "b = Numeral0" 1); +Goal "(0::int) < c ==> a mod (b*c) = b*(a div b mod c) + a mod b"; +by (zdiv_undefined_case_tac "b = 0" 1); by (force_tac (claset(), simpset() addsimps [quorem_div_mod RS lemma RS quorem_mod, zmult_eq_0_iff]) 1); @@ -803,26 +814,26 @@ (*** Cancellation of common factors in "div" ***) -Goal "[| (Numeral0::int) < b; c ~= Numeral0 |] ==> (c*a) div (c*b) = a div b"; +Goal "[| (0::int) < b; c ~= 0 |] ==> (c*a) div (c*b) = a div b"; by (stac zdiv_zmult2_eq 1); by Auto_tac; val lemma1 = result(); -Goal "[| b < (Numeral0::int); c ~= Numeral0 |] ==> (c*a) div (c*b) = a div b"; +Goal "[| b < (0::int); c ~= 0 |] ==> (c*a) div (c*b) = a div b"; by (subgoal_tac "(c * (-a)) div (c * (-b)) = (-a) div (-b)" 1); by (rtac lemma1 2); by Auto_tac; val lemma2 = result(); -Goal "c ~= (Numeral0::int) ==> (c*a) div (c*b) = a div b"; -by (zdiv_undefined_case_tac "b = Numeral0" 1); +Goal "c ~= (0::int) ==> (c*a) div (c*b) = a div b"; +by (zdiv_undefined_case_tac "b = 0" 1); by (auto_tac (claset(), simpset() addsimps [read_instantiate [("x", "b")] linorder_neq_iff, lemma1, lemma2])); qed "zdiv_zmult_zmult1"; -Goal "c ~= (Numeral0::int) ==> (a*c) div (b*c) = a div b"; +Goal "c ~= (0::int) ==> (a*c) div (b*c) = a div b"; by (dtac zdiv_zmult_zmult1 1); by (auto_tac (claset(), simpset() addsimps [zmult_commute])); qed "zdiv_zmult_zmult2"; @@ -831,20 +842,20 @@ (*** Distribution of factors over "mod" ***) -Goal "[| (Numeral0::int) < b; c ~= Numeral0 |] ==> (c*a) mod (c*b) = c * (a mod b)"; +Goal "[| (0::int) < b; c ~= 0 |] ==> (c*a) mod (c*b) = c * (a mod b)"; by (stac zmod_zmult2_eq 1); by Auto_tac; val lemma1 = result(); -Goal "[| b < (Numeral0::int); c ~= Numeral0 |] ==> (c*a) mod (c*b) = c * (a mod b)"; +Goal "[| b < (0::int); c ~= 0 |] ==> (c*a) mod (c*b) = c * (a mod b)"; by (subgoal_tac "(c * (-a)) mod (c * (-b)) = c * ((-a) mod (-b))" 1); by (rtac lemma1 2); by Auto_tac; val lemma2 = result(); Goal "(c*a) mod (c*b) = (c::int) * (a mod b)"; -by (zdiv_undefined_case_tac "b = Numeral0" 1); -by (zdiv_undefined_case_tac "c = Numeral0" 1); +by (zdiv_undefined_case_tac "b = 0" 1); +by (zdiv_undefined_case_tac "c = 0" 1); by (auto_tac (claset(), simpset() addsimps [read_instantiate [("x", "b")] linorder_neq_iff, @@ -861,16 +872,16 @@ (** computing "div" by shifting **) -Goal "(Numeral0::int) <= a ==> (Numeral1 + 2*b) div (2*a) = b div a"; -by (zdiv_undefined_case_tac "a = Numeral0" 1); -by (subgoal_tac "Numeral1 <= a" 1); +Goal "(0::int) <= a ==> (1 + 2*b) div (2*a) = b div a"; +by (zdiv_undefined_case_tac "a = 0" 1); +by (subgoal_tac "1 <= a" 1); by (arith_tac 2); -by (subgoal_tac "Numeral1 < a * 2" 1); +by (subgoal_tac "1 < a * 2" 1); by (arith_tac 2); -by (subgoal_tac "2*(Numeral1 + b mod a) <= 2*a" 1); +by (subgoal_tac "2*(1 + b mod a) <= 2*a" 1); by (rtac zmult_zle_mono2 2); by (auto_tac (claset(), - simpset() addsimps [zadd_commute, zmult_commute, + simpset() addsimps [inst "z" "1" zadd_commute, zmult_commute, add1_zle_eq, pos_mod_bound])); by (stac zdiv_zadd1_eq 1); by (asm_simp_tac (simpset() addsimps [zdiv_zmult_zmult2, zmod_zmult_zmult2, @@ -881,18 +892,18 @@ pos_mod_sign RS zadd_zle_mono1 RSN (2,order_trans)]) 1); by (auto_tac (claset(), simpset() addsimps [mod_pos_pos_trivial])); -by (subgoal_tac "Numeral0 <= b mod a" 1); +by (subgoal_tac "0 <= b mod a" 1); by (asm_simp_tac (simpset() addsimps [pos_mod_sign]) 2); by (arith_tac 1); qed "pos_zdiv_mult_2"; -Goal "a <= (Numeral0::int) ==> (Numeral1 + 2*b) div (2*a) = (b+Numeral1) div a"; -by (subgoal_tac "(Numeral1 + 2*(-b-Numeral1)) div (2 * (-a)) = (-b-Numeral1) div (-a)" 1); +Goal "a <= (0::int) ==> (1 + 2*b) div (2*a) = (b+1) div a"; +by (subgoal_tac "(1 + 2*(-b - 1)) div (2 * (-a)) = (-b - 1) div (-a)" 1); by (rtac pos_zdiv_mult_2 2); by (auto_tac (claset(), simpset() addsimps [zmult_zminus_right])); -by (subgoal_tac "(-1 - (2 * b)) = - (Numeral1 + (2 * b))" 1); +by (subgoal_tac "(-1 - (2 * b)) = - (1 + (2 * b))" 1); by (Simp_tac 2); by (asm_full_simp_tac (HOL_ss addsimps [zdiv_zminus_zminus, zdiff_def, @@ -902,17 +913,19 @@ (*Not clear why this must be proved separately; probably number_of causes simplification problems*) -Goal "~ Numeral0 <= x ==> x <= (Numeral0::int)"; +Goal "~ 0 <= x ==> x <= (0::int)"; by Auto_tac; val lemma = result(); Goal "number_of (v BIT b) div number_of (w BIT False) = \ -\ (if ~b | (Numeral0::int) <= number_of w \ +\ (if ~b | (0::int) <= number_of w \ \ then number_of v div (number_of w) \ -\ else (number_of v + (Numeral1::int)) div (number_of w))"; +\ else (number_of v + (1::int)) div (number_of w))"; by (simp_tac (simpset_of Int.thy addsimps [zadd_assoc, number_of_BIT]) 1); +by (subgoal_tac "2 ~= (0::int)" 1); + by (Simp_tac 2); (*we do this because the next step can't simplify numerals*) by (asm_simp_tac (simpset() - delsimps [thm "number_of_reorient"]@bin_arith_extra_simps@bin_rel_simps + delsimps bin_arith_extra_simps addsimps [zdiv_zmult_zmult1, pos_zdiv_mult_2, lemma, neg_zdiv_mult_2]) 1); qed "zdiv_number_of_BIT"; @@ -921,16 +934,16 @@ (** computing "mod" by shifting (proofs resemble those for "div") **) -Goal "(Numeral0::int) <= a ==> (Numeral1 + 2*b) mod (2*a) = Numeral1 + 2 * (b mod a)"; -by (zdiv_undefined_case_tac "a = Numeral0" 1); -by (subgoal_tac "Numeral1 <= a" 1); +Goal "(0::int) <= a ==> (1 + 2*b) mod (2*a) = 1 + 2 * (b mod a)"; +by (zdiv_undefined_case_tac "a = 0" 1); +by (subgoal_tac "1 <= a" 1); by (arith_tac 2); -by (subgoal_tac "Numeral1 < a * 2" 1); +by (subgoal_tac "1 < a * 2" 1); by (arith_tac 2); -by (subgoal_tac "2*(Numeral1 + b mod a) <= 2*a" 1); +by (subgoal_tac "2*(1 + b mod a) <= 2*a" 1); by (rtac zmult_zle_mono2 2); by (auto_tac (claset(), - simpset() addsimps [zadd_commute, zmult_commute, + simpset() addsimps [inst "z" "1" zadd_commute, zmult_commute, add1_zle_eq, pos_mod_bound])); by (stac zmod_zadd1_eq 1); by (asm_simp_tac (simpset() addsimps [zmod_zmult_zmult2, @@ -941,19 +954,18 @@ pos_mod_sign RS zadd_zle_mono1 RSN (2,order_trans)]) 1); by (auto_tac (claset(), simpset() addsimps [mod_pos_pos_trivial])); -by (subgoal_tac "Numeral0 <= b mod a" 1); +by (subgoal_tac "0 <= b mod a" 1); by (asm_simp_tac (simpset() addsimps [pos_mod_sign]) 2); by (arith_tac 1); qed "pos_zmod_mult_2"; -Goal "a <= (Numeral0::int) ==> (Numeral1 + 2*b) mod (2*a) = 2 * ((b+Numeral1) mod a) - Numeral1"; +Goal "a <= (0::int) ==> (1 + 2*b) mod (2*a) = 2 * ((b+1) mod a) - 1"; by (subgoal_tac - "(Numeral1 + 2*(-b-Numeral1)) mod (2*(-a)) = Numeral1 + 2*((-b-Numeral1) mod (-a))" 1); + "(1 + 2*(-b - 1)) mod (2*(-a)) = 1 + 2*((-b - 1) mod (-a))" 1); by (rtac pos_zmod_mult_2 2); -by (auto_tac (claset(), - simpset() addsimps [zmult_zminus_right])); -by (subgoal_tac "(-1 - (2 * b)) = - (Numeral1 + (2 * b))" 1); +by (auto_tac (claset(), simpset() addsimps [zmult_zminus_right])); +by (subgoal_tac "(-1 - (2 * b)) = - (1 + (2 * b))" 1); by (Simp_tac 2); by (asm_full_simp_tac (HOL_ss addsimps [zmod_zminus_zminus, zdiff_def, @@ -964,15 +976,16 @@ Goal "number_of (v BIT b) mod number_of (w BIT False) = \ \ (if b then \ -\ if (Numeral0::int) <= number_of w \ -\ then 2 * (number_of v mod number_of w) + Numeral1 \ -\ else 2 * ((number_of v + (Numeral1::int)) mod number_of w) - Numeral1 \ +\ if (0::int) <= number_of w \ +\ then 2 * (number_of v mod number_of w) + 1 \ +\ else 2 * ((number_of v + (1::int)) mod number_of w) - 1 \ \ else 2 * (number_of v mod number_of w))"; by (simp_tac (simpset_of Int.thy addsimps [zadd_assoc, number_of_BIT]) 1); by (asm_simp_tac (simpset() delsimps bin_arith_extra_simps@bin_rel_simps addsimps [zmod_zmult_zmult1, pos_zmod_mult_2, lemma, neg_zmod_mult_2]) 1); +by (Simp_tac 1); qed "zmod_number_of_BIT"; Addsimps [zmod_number_of_BIT]; @@ -980,7 +993,7 @@ (** Quotients of signs **) -Goal "[| a < (Numeral0::int); Numeral0 < b |] ==> a div b < Numeral0"; +Goal "[| a < (0::int); 0 < b |] ==> a div b < 0"; by (subgoal_tac "a div b <= -1" 1); by (Force_tac 1); by (rtac order_trans 1); @@ -988,12 +1001,12 @@ by (auto_tac (claset(), simpset() addsimps [zdiv_minus1])); qed "div_neg_pos_less0"; -Goal "[| (Numeral0::int) <= a; b < Numeral0 |] ==> a div b <= Numeral0"; +Goal "[| (0::int) <= a; b < 0 |] ==> a div b <= 0"; by (dtac zdiv_mono1_neg 1); by Auto_tac; qed "div_nonneg_neg_le0"; -Goal "(Numeral0::int) < b ==> (Numeral0 <= a div b) = (Numeral0 <= a)"; +Goal "(0::int) < b ==> (0 <= a div b) = (0 <= a)"; by Auto_tac; by (dtac zdiv_mono1 2); by (auto_tac (claset(), simpset() addsimps [linorder_neq_iff])); @@ -1001,20 +1014,20 @@ by (blast_tac (claset() addIs [div_neg_pos_less0]) 1); qed "pos_imp_zdiv_nonneg_iff"; -Goal "b < (Numeral0::int) ==> (Numeral0 <= a div b) = (a <= (Numeral0::int))"; +Goal "b < (0::int) ==> (0 <= a div b) = (a <= (0::int))"; by (stac (zdiv_zminus_zminus RS sym) 1); by (stac pos_imp_zdiv_nonneg_iff 1); by Auto_tac; qed "neg_imp_zdiv_nonneg_iff"; (*But not (a div b <= 0 iff a<=0); consider a=1, b=2 when a div b = 0.*) -Goal "(Numeral0::int) < b ==> (a div b < Numeral0) = (a < Numeral0)"; +Goal "(0::int) < b ==> (a div b < 0) = (a < 0)"; by (asm_simp_tac (simpset() addsimps [linorder_not_le RS sym, pos_imp_zdiv_nonneg_iff]) 1); qed "pos_imp_zdiv_neg_iff"; (*Again the law fails for <=: consider a = -1, b = -2 when a div b = 0*) -Goal "b < (Numeral0::int) ==> (a div b < Numeral0) = (Numeral0 < a)"; +Goal "b < (0::int) ==> (a div b < 0) = (0 < a)"; by (asm_simp_tac (simpset() addsimps [linorder_not_le RS sym, neg_imp_zdiv_nonneg_iff]) 1); qed "neg_imp_zdiv_neg_iff";