# HG changeset patch # User paulson # Date 1003744462 -7200 # Node ID 56db9f3a6b3ecca721a1e16a7f4f7be1e973a68b # Parent 76401b2ee871d8b5095be22e4d1aedeea3b82d1e Numerals now work for the integers: the binary numerals for 0 and 1 rewrite to their abstract counterparts, while other binary numerals work correctly. diff -r 76401b2ee871 -r 56db9f3a6b3e src/HOL/Integ/Bin.ML --- a/src/HOL/Integ/Bin.ML Mon Oct 22 11:01:30 2001 +0200 +++ b/src/HOL/Integ/Bin.ML Mon Oct 22 11:54:22 2001 +0200 @@ -98,7 +98,7 @@ (**** The carry/borrow functions, bin_succ and bin_pred ****) -(**** number_of ****) +(** number_of **) Goal "number_of(NCons w b) = (number_of(w BIT b)::int)"; by (induct_tac "w" 1); @@ -107,12 +107,12 @@ Addsimps [number_of_NCons]; -Goal "number_of(bin_succ w) = int 1 + number_of w"; +Goal "number_of(bin_succ w) = (1 + number_of w :: int)"; by (induct_tac "w" 1); by (ALLGOALS (asm_simp_tac (simpset() addsimps zadd_ac))); qed "number_of_succ"; -Goal "number_of(bin_pred w) = - (int 1) + number_of w"; +Goal "number_of(bin_pred w) = (- 1 + number_of w :: int)"; by (induct_tac "w" 1); by (ALLGOALS (asm_simp_tac (simpset() addsimps zadd_ac))); qed "number_of_pred"; @@ -127,17 +127,15 @@ zadd_assoc]) 1); qed "number_of_minus"; - -bind_thms ("bin_add_simps", [bin_add_BIT_BIT, number_of_succ, number_of_pred]); - (*This proof is complicated by the mutual recursion*) Goal "! w. number_of(bin_add v w) = (number_of v + number_of w::int)"; -by (induct_tac "v" 1); -by (simp_tac (simpset() addsimps bin_add_simps) 1); -by (simp_tac (simpset() addsimps bin_add_simps) 1); +by (induct_tac "v" 1); +by (Simp_tac 1); +by (simp_tac (simpset() addsimps [number_of_pred]) 1); by (rtac allI 1); by (induct_tac "w" 1); -by (ALLGOALS (asm_simp_tac (simpset() addsimps bin_add_simps @ zadd_ac))); +by (ALLGOALS (asm_simp_tac (simpset() addsimps + [bin_add_BIT_BIT, number_of_succ, number_of_pred] @ zadd_ac))); qed_spec_mp "number_of_add"; @@ -147,7 +145,8 @@ by (simp_tac (simpset() addsimps [number_of_add, number_of_minus]) 1); qed "diff_number_of_eq"; -bind_thms ("bin_mult_simps", [zmult_zminus, number_of_minus, number_of_add]); +bind_thms ("bin_mult_simps", + [int_Suc0_eq_1, zmult_zminus, number_of_minus, number_of_add]); Goal "number_of(bin_mult v w) = (number_of v * number_of w::int)"; by (induct_tac "v" 1); @@ -167,54 +166,15 @@ qed "double_number_of_BIT"; -(** Simplification rules with integer constants **) - -Goal "Numeral0 + z = (z::int)"; -by (Simp_tac 1); -qed "zadd_0"; - -Goal "z + Numeral0 = (z::int)"; -by (Simp_tac 1); -qed "zadd_0_right"; - -Addsimps [zadd_0, zadd_0_right]; - - -(** Converting simple cases of (int n) to numerals **) - -Goal "int 0 = Numeral0"; -by (rtac sym 1); -by (rtac number_of_Pls 1); -qed "int_0"; - -Goal "int 1 = Numeral1"; -by (Simp_tac 1); -qed "int_1"; +(** Converting numerals 0 and 1 to their abstract versions **) -Goal "int (Suc n) = Numeral1 + int n"; -by (simp_tac (simpset() addsimps [zadd_int]) 1); -qed "int_Suc"; - -Goal "- (Numeral0) = (Numeral0::int)"; +Goal "Numeral0 = (0::int)"; by (Simp_tac 1); -qed "zminus_0"; - -Addsimps [zminus_0]; - +qed "int_numeral_0_eq_0"; -Goal "(Numeral0::int) - x = -x"; -by (simp_tac (simpset() addsimps [zdiff_def]) 1); -qed "zdiff0"; - -Goal "x - (Numeral0::int) = x"; -by (simp_tac (simpset() addsimps [zdiff_def]) 1); -qed "zdiff0_right"; - -Goal "x - x = (Numeral0::int)"; -by (simp_tac (simpset() addsimps [zdiff_def]) 1); -qed "zdiff_self"; - -Addsimps [zdiff0, zdiff0_right, zdiff_self]; +Goal "Numeral1 = (1::int)"; +by (simp_tac (simpset() addsimps [int_1, int_Suc0_eq_1]) 1); +qed "int_numeral_1_eq_1"; (** Special simplification, for constants only **) @@ -240,99 +200,30 @@ (** Special-case simplification for small constants **) -Goal "Numeral0 * z = (Numeral0::int)"; -by (Simp_tac 1); -qed "zmult_0"; - -Goal "z * Numeral0 = (Numeral0::int)"; -by (Simp_tac 1); -qed "zmult_0_right"; - -Goal "Numeral1 * z = (z::int)"; -by (Simp_tac 1); -qed "zmult_1"; - -Goal "z * Numeral1 = (z::int)"; -by (Simp_tac 1); -qed "zmult_1_right"; - Goal "-1 * z = -(z::int)"; -by (simp_tac (simpset() addsimps zcompare_rls@[zmult_zminus]) 1); +by (simp_tac (simpset() addsimps zcompare_rls@[int_Suc0_eq_1, zmult_zminus]) 1); qed "zmult_minus1"; Goal "z * -1 = -(z::int)"; -by (simp_tac (simpset() addsimps zcompare_rls@[zmult_zminus_right]) 1); +by (stac zmult_commute 1 THEN rtac zmult_minus1 1); qed "zmult_minus1_right"; -Addsimps [zmult_0, zmult_0_right, - zmult_1, zmult_1_right, - zmult_minus1, zmult_minus1_right]; +Addsimps [zmult_minus1, zmult_minus1_right]; (*Negation of a coefficient*) Goal "- (number_of w) * z = number_of(bin_minus w) * (z::int)"; by (simp_tac (simpset() addsimps [number_of_minus, zmult_zminus]) 1); qed "zminus_number_of_zmult"; - Addsimps [zminus_number_of_zmult]; - -(** Inequality reasoning **) - -Goal "(m*n = (Numeral0::int)) = (m = Numeral0 | n = Numeral0)"; -by (stac (int_0 RS sym) 1 THEN rtac zmult_eq_int0_iff 1); -qed "zmult_eq_0_iff"; -AddIffs [zmult_eq_0_iff]; - -Goal "(w < z + (Numeral1::int)) = (w error + ("The error(s) above occurred while trying to prove " ^ + string_of_cterm ct ^ "\nInternal failure of simproc " ^ name)) + end + + (*version without the hyps argument*) + fun prove_conv_nohyps name tacs sg = prove_conv name tacs sg [] + + fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc + fun prep_pat s = Thm.read_cterm (Theory.sign_of (the_context())) (s, HOLogic.termT) + val prep_pats = map prep_pat + + fun is_numeral (Const("Numeral.number_of", _) $ w) = true + | is_numeral _ = false + + fun simplify_meta_eq f_number_of_eq f_eq = + mk_meta_eq ([f_eq, f_number_of_eq] MRS trans) + + structure IntAbstractNumeralsData = + struct + val dest_eq = HOLogic.dest_eq o HOLogic.dest_Trueprop o concl_of + val is_numeral = is_numeral + val numeral_0_eq_0 = int_numeral_0_eq_0 + val numeral_1_eq_1 = int_numeral_1_eq_1 + val prove_conv = prove_conv_nohyps "int_abstract_numerals" + fun norm_tac simps = ALLGOALS (simp_tac (HOL_ss addsimps simps)) + val simplify_meta_eq = simplify_meta_eq + end + + structure IntAbstractNumerals = AbstractNumeralsFun (IntAbstractNumeralsData) + + + (*For addition, we already have rules for the operand 0. + Multiplication is omitted because there are already special rules for + both 0 and 1 as operands. Unary minus is trivial, just have - 1 = -1. + For the others, having three patterns is a compromise between just having + one (many spurious calls) and having nine (just too many!) *) + val eval_numerals = + map prep_simproc + [("int_add_eval_numerals", + prep_pats ["(m::int) + 1", "(m::int) + number_of v"], + IntAbstractNumerals.proc (number_of_add RS sym)), + ("int_diff_eval_numerals", + prep_pats ["(m::int) - 1", "(m::int) - number_of v"], + IntAbstractNumerals.proc diff_number_of_eq), + ("int_eq_eval_numerals", + prep_pats ["(m::int) = 0", "(m::int) = 1", "(m::int) = number_of v"], + IntAbstractNumerals.proc eq_number_of_eq), + ("int_less_eval_numerals", + prep_pats ["(m::int) < 0", "(m::int) < 1", "(m::int) < number_of v"], + IntAbstractNumerals.proc less_number_of_eq_neg), + ("int_le_eval_numerals", + prep_pats ["(m::int) <= 0", "(m::int) <= 1", "(m::int) <= number_of v"], + IntAbstractNumerals.proc le_number_of_eq_not_less)] + + (*reorientation simprules using ==, for the following simproc*) + val meta_zero_reorient = zero_reorient RS eq_reflection + val meta_one_reorient = one_reorient RS eq_reflection + val meta_number_of_reorient = number_of_reorient RS eq_reflection + + (*reorientation simplification procedure: reorients (polymorphic) + 0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a numeral.*) + fun reorient_proc sg _ (_ $ t $ u) = + case u of + Const("0", _) => None + | Const("1", _) => None + | Const("Numeral.number_of", _) $ _ => None + | _ => Some (case t of + Const("0", _) => meta_zero_reorient + | Const("1", _) => meta_one_reorient + | Const("Numeral.number_of", _) $ _ => meta_number_of_reorient) + + val reorient_simproc = + prep_simproc ("reorient_simproc", + prep_pats ["0=x", "1=x", "number_of w = x"], + reorient_proc) + + end; + + +Addsimprocs Bin_Simprocs.eval_numerals; +Addsimprocs [Bin_Simprocs.reorient_simproc]; (*Delete the original rewrites, with their clumsy conditional expressions*) @@ -423,21 +425,24 @@ (*Hide the binary representation of integer constants*) Delsimps [number_of_Pls, number_of_Min, number_of_BIT]; + + (*Simplification of arithmetic operations on integer constants. Note that bin_pred_Pls, etc. were added to the simpset by primrec.*) -bind_thms ("NCons_simps", [NCons_Pls_0, NCons_Pls_1, NCons_Min_0, NCons_Min_1, NCons_BIT]); +bind_thms ("NCons_simps", + [NCons_Pls_0, NCons_Pls_1, NCons_Min_0, NCons_Min_1, NCons_BIT]); bind_thms ("bin_arith_extra_simps", [number_of_add RS sym, - number_of_minus RS sym, + number_of_minus RS sym, zminus_1_eq_m1, number_of_mult RS sym, bin_succ_1, bin_succ_0, bin_pred_1, bin_pred_0, bin_minus_1, bin_minus_0, bin_add_Pls_right, bin_add_Min_right, bin_add_BIT_0, bin_add_BIT_10, bin_add_BIT_11, - diff_number_of_eq, abs_number_of, + diff_number_of_eq, zabs_number_of, zabs_0, zabs_1, bin_mult_1, bin_mult_0] @ NCons_simps); (*For making a minimal simpset, one must include these default simprules @@ -454,7 +459,8 @@ [eq_number_of_eq, iszero_number_of_Pls, nonzero_number_of_Min, iszero_number_of_0, iszero_number_of_1, less_number_of_eq_neg, - not_neg_number_of_Pls, neg_number_of_Min, neg_number_of_BIT, + not_neg_number_of_Pls, not_neg_0, not_neg_1, not_iszero_1, + neg_number_of_Min, neg_number_of_BIT, le_number_of_eq_not_less]); Addsimps bin_arith_extra_simps; @@ -484,3 +490,14 @@ Addsimps [add_number_of_left, mult_number_of_left, add_number_of_diff1, add_number_of_diff2]; + + +(** Inserting these natural simprules earlier would break many proofs! **) + +(* int (Suc n) = 1 + int n *) +Addsimps [int_Suc]; + +(* Numeral0 -> 0 and Numeral1 -> 1 *) +Addsimps [int_numeral_0_eq_0, int_numeral_1_eq_1]; + + diff -r 76401b2ee871 -r 56db9f3a6b3e src/HOL/Integ/Bin.thy --- a/src/HOL/Integ/Bin.thy Mon Oct 22 11:01:30 2001 +0200 +++ b/src/HOL/Integ/Bin.thy Mon Oct 22 11:54:22 2001 +0200 @@ -15,12 +15,7 @@ for the numerical interpretation. The representation expects that (m mod 2) is 0 or 1, even if m is negative; -For instance, ~5 div 2 = ~3 and ~5 mod 2 = 1; thus ~5 = (~3)*2 + 1 - -Division is not defined yet! To do it efficiently requires computing the -quotient and remainder using ML and checking the answer using multiplication -by proof. Then uniqueness of the quotient and remainder yields theorems -quoting the previously computed values. (Or code an oracle...) +For instance, -5 div 2 = -3 and -5 mod 2 = 1; thus -5 = (-3)*2 + 1 *) Bin = Int + Numeral + @@ -41,11 +36,11 @@ instance int :: number -primrec - number_of_Pls "number_of Pls = int 0" - number_of_Min "number_of Min = - (int 1)" - number_of_BIT "number_of(w BIT x) = (if x then int 1 else int 0) + - (number_of w) + (number_of w)" +primrec (*the type constraint is essential!*) + number_of_Pls "number_of Pls = 0" + number_of_Min "number_of Min = - (1::int)" + number_of_BIT "number_of(w BIT x) = (if x then 1 else 0) + + (number_of w) + (number_of w)" primrec bin_succ_Pls "bin_succ Pls = Pls BIT True" @@ -86,5 +81,4 @@ (if x then (bin_add (NCons (bin_mult v w) False) w) else (NCons (bin_mult v w) False))" - end diff -r 76401b2ee871 -r 56db9f3a6b3e src/HOL/Integ/Int.ML --- a/src/HOL/Integ/Int.ML Mon Oct 22 11:01:30 2001 +0200 +++ b/src/HOL/Integ/Int.ML Mon Oct 22 11:54:22 2001 +0200 @@ -9,6 +9,56 @@ *) +Goal "int 0 = (0::int)"; +by (simp_tac (simpset() addsimps [Zero_int_def]) 1); +qed "int_0"; + +Goal "int 1 = 1"; +by (simp_tac (simpset() addsimps [One_int_def]) 1); +qed "int_1"; + +Goal "int (Suc 0) = 1"; +by (simp_tac (simpset() addsimps [One_int_def, One_nat_def]) 1); +qed "int_Suc0_eq_1"; + +Goalw [zdiff_def,zless_def] "neg x = (x < 0)"; +by Auto_tac; +qed "neg_eq_less_0"; + +Goalw [zle_def] "(~neg x) = (0 <= x)"; +by (simp_tac (simpset() addsimps [neg_eq_less_0]) 1); +qed "not_neg_eq_ge_0"; + +(** Needed to simplify inequalities when Numeral1 can get simplified to 1 **) + +Goal "~ neg 0"; +by (simp_tac (simpset() addsimps [One_int_def, neg_eq_less_0]) 1); +qed "not_neg_0"; + +Goal "~ neg 1"; +by (simp_tac (simpset() addsimps [One_int_def, neg_eq_less_0]) 1); +qed "not_neg_1"; + +Goal "iszero 0"; +by (simp_tac (simpset() addsimps [iszero_def]) 1); +qed "iszero_0"; + +Goal "~ iszero 1"; +by (simp_tac (simpset() addsimps [Zero_int_def, One_int_def, One_nat_def, + iszero_def]) 1); +qed "not_iszero_1"; + +Goal "0 < (1::int)"; +by (simp_tac (simpset() addsimps [Zero_int_def, One_int_def, One_nat_def]) 1); +qed "int_0_less_1"; + +Goal "0 \\ (1::int)"; +by (simp_tac (simpset() addsimps [Zero_int_def, One_int_def, One_nat_def]) 1); +qed "int_0_neq_1"; + +Addsimps [int_0, int_1, int_0_neq_1]; + + (*** Abel_Cancel simproc on the integers ***) (* Lemmas needed for the simprocs *) @@ -23,7 +73,7 @@ everything gets cancelled on the right.*) Goal "((x::int) + (y + z) = y) = (x = -z)"; by (stac zadd_left_commute 1); -by (res_inst_tac [("t", "y")] (zadd_int0_right RS subst) 1 +by (res_inst_tac [("t", "y")] (zadd_0_right RS subst) 1 THEN stac zadd_left_cancel 1); by (simp_tac (simpset() addsimps [eq_zdiff_eq RS sym]) 1); qed "zadd_cancel_end"; @@ -36,7 +86,7 @@ val sg_ref = Sign.self_ref (Theory.sign_of (the_context ())) val T = HOLogic.intT - val zero = Const ("IntDef.int", HOLogic.natT --> T) $ HOLogic.zero + val zero = Const ("0", HOLogic.intT) val restrict_to_left = restrict_to_left val add_cancel_21 = zadd_cancel_21 val add_cancel_end = zadd_cancel_end @@ -44,8 +94,8 @@ val add_assoc = zadd_assoc val add_commute = zadd_commute val add_left_commute = zadd_left_commute - val add_0 = zadd_int0 - val add_0_right = zadd_int0_right + val add_0 = zadd_0 + val add_0_right = zadd_0_right val eq_diff_eq = eq_zdiff_eq val eqI_rules = [zless_eqI, zeq_eqI, zle_eqI] @@ -56,8 +106,8 @@ val diff_def = zdiff_def val minus_add_distrib = zminus_zadd_distrib val minus_minus = zminus_zminus - val minus_0 = zminus_int0 - val add_inverses = [zadd_zminus_inverse, zadd_zminus_inverse2]; + val minus_0 = zminus_0 + val add_inverses = [zadd_zminus_inverse, zadd_zminus_inverse2] val cancel_simps = [zadd_zminus_cancel, zminus_zadd_cancel] end; @@ -86,29 +136,26 @@ by (simp_tac (simpset() addsimps [zle_def, zless_def]) 1); qed "zle_eq_not_neg"; +(** Inequality reasoning **) -(*** Inequality lemmas involving int (Suc m) ***) - -Goal "(w < z + int (Suc m)) = (w < z + int m | w = z + int m)"; +Goal "(w < z + (1::int)) = (w int (nat z) = z"; -by (dtac (not_neg_eq_ge_int0 RS iffD1) 1); +by (dtac (not_neg_eq_ge_0 RS iffD1) 1); by (dtac zle_imp_zless_or_eq 1); by (auto_tac (claset(), simpset() addsimps [zless_iff_Suc_zadd])); qed "not_neg_nat"; Goal "neg x ==> EX n. x = - (int (Suc n))"; by (auto_tac (claset(), - simpset() addsimps [neg_eq_less_int0, zless_iff_Suc_zadd, + simpset() addsimps [neg_eq_less_0, zless_iff_Suc_zadd, zdiff_eq_eq RS sym, zdiff_def])); qed "negD"; @@ -295,28 +353,28 @@ by (etac (not_neg_nat RS subst) 2); by (auto_tac (claset(), simpset() addsimps [neg_nat])); by (auto_tac (claset() addDs [order_less_trans], - simpset() addsimps [neg_eq_less_int0])); + simpset() addsimps [neg_eq_less_0])); qed "zless_nat_eq_int_zless"; -Goal "z <= int 0 ==> nat z = 0"; +Goal "z <= 0 ==> nat z = 0"; by (auto_tac (claset(), - simpset() addsimps [order_le_less, neg_eq_less_int0, + simpset() addsimps [order_le_less, neg_eq_less_0, zle_def, neg_nat])); qed "nat_le_int0"; -(*An alternative condition is int 0 <= w *) -Goal "int 0 < z ==> (nat w < nat z) = (w < z)"; +(*An alternative condition is 0 <= w *) +Goal "0 < z ==> (nat w < nat z) = (w < z)"; by (stac (zless_int RS sym) 1); -by (asm_simp_tac (simpset() addsimps [not_neg_nat, not_neg_eq_ge_int0, +by (asm_simp_tac (simpset() addsimps [not_neg_nat, not_neg_eq_ge_0, order_le_less]) 1); by (case_tac "neg w" 1); by (asm_simp_tac (simpset() addsimps [not_neg_nat]) 2); -by (asm_full_simp_tac (simpset() addsimps [neg_eq_less_int0, neg_nat]) 1); +by (asm_full_simp_tac (simpset() addsimps [neg_eq_less_0, neg_nat]) 1); by (blast_tac (claset() addIs [order_less_trans]) 1); val lemma = result(); -Goal "(nat w < nat z) = (int 0 < z & w < z)"; -by (case_tac "int 0 < z" 1); +Goal "(nat w < nat z) = (0 < z & w < z)"; +by (case_tac "0 < z" 1); by (auto_tac (claset(), simpset() addsimps [lemma, nat_le_int0, linorder_not_less])); qed "zless_nat_conj"; @@ -339,35 +397,36 @@ Goal "i <= (j::int) ==> i * int k <= j * int k"; by (induct_tac "k" 1); -by (stac int_Suc_int_1 2); +by (stac int_Suc 2); by (ALLGOALS - (asm_simp_tac (simpset() addsimps [zadd_zmult_distrib2, zadd_zle_mono]))); + (asm_simp_tac (simpset() addsimps [zadd_zmult_distrib2, zadd_zle_mono, + int_Suc0_eq_1]))); val lemma = result(); -Goal "[| i <= j; int 0 <= k |] ==> i*k <= j*k"; +Goal "[| i <= j; (0::int) <= k |] ==> i*k <= j*k"; by (res_inst_tac [("t", "k")] (not_neg_nat RS subst) 1); by (etac lemma 2); -by (full_simp_tac (simpset() addsimps [not_neg_eq_ge_int0]) 1); +by (full_simp_tac (simpset() addsimps [not_neg_eq_ge_0]) 1); qed "zmult_zle_mono1"; -Goal "[| i <= j; k <= int 0 |] ==> j*k <= i*k"; +Goal "[| i <= j; k <= (0::int) |] ==> j*k <= i*k"; by (rtac (zminus_zle_zminus RS iffD1) 1); by (asm_simp_tac (simpset() addsimps [zmult_zminus_right RS sym, zmult_zle_mono1, zle_zminus]) 1); qed "zmult_zle_mono1_neg"; -Goal "[| i <= j; int 0 <= k |] ==> k*i <= k*j"; +Goal "[| i <= j; (0::int) <= k |] ==> k*i <= k*j"; by (dtac zmult_zle_mono1 1); by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [zmult_commute]))); qed "zmult_zle_mono2"; -Goal "[| i <= j; k <= int 0 |] ==> k*j <= k*i"; +Goal "[| i <= j; k <= (0::int) |] ==> k*j <= k*i"; by (dtac zmult_zle_mono1_neg 1); by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [zmult_commute]))); qed "zmult_zle_mono2_neg"; (* <= monotonicity, BOTH arguments*) -Goal "[| i <= j; k <= l; int 0 <= j; int 0 <= k |] ==> i*k <= j*l"; +Goal "[| i <= j; k <= l; (0::int) <= j; (0::int) <= k |] ==> i*k <= j*l"; by (etac (zmult_zle_mono1 RS order_trans) 1); by (assume_tac 1); by (etac zmult_zle_mono2 1); @@ -379,64 +438,65 @@ Goal "i 0 int k * i < int k * j"; by (induct_tac "k" 1); -by (stac int_Suc_int_1 2); +by (stac int_Suc 2); by (case_tac "n=0" 2); by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [zadd_zmult_distrib, zadd_zless_mono, - order_le_less]))); -val lemma = result() RS mp; + int_Suc0_eq_1, order_le_less]))); +val lemma = result(); -Goal "[| i k*i < k*j"; +Goal "[| i k*i < k*j"; by (res_inst_tac [("t", "k")] (not_neg_nat RS subst) 1); -by (etac lemma 2); -by (asm_simp_tac (simpset() addsimps [not_neg_eq_ge_int0, +by (etac (lemma RS mp) 2); +by (asm_simp_tac (simpset() addsimps [not_neg_eq_ge_0, order_le_less]) 1); by (forward_tac [conjI RS (zless_nat_conj RS iffD2)] 1); by Auto_tac; qed "zmult_zless_mono2"; -Goal "[| i i*k < j*k"; +Goal "[| i i*k < j*k"; by (dtac zmult_zless_mono2 1); by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [zmult_commute]))); qed "zmult_zless_mono1"; (* < monotonicity, BOTH arguments*) -Goal "[| i < j; k < l; int 0 < j; int 0 < k |] ==> i*k < j*l"; +Goal "[| i < j; k < l; (0::int) < j; (0::int) < k |] ==> i*k < j*l"; by (etac (zmult_zless_mono1 RS order_less_trans) 1); by (assume_tac 1); by (etac zmult_zless_mono2 1); by (assume_tac 1); qed "zmult_zless_mono"; -Goal "[| i j*k < i*k"; +Goal "[| i j*k < i*k"; by (rtac (zminus_zless_zminus RS iffD1) 1); by (asm_simp_tac (simpset() addsimps [zmult_zminus_right RS sym, zmult_zless_mono1, zless_zminus]) 1); qed "zmult_zless_mono1_neg"; -Goal "[| i k*j < k*i"; +Goal "[| i k*j < k*i"; by (rtac (zminus_zless_zminus RS iffD1) 1); by (asm_simp_tac (simpset() addsimps [zmult_zminus RS sym, zmult_zless_mono2, zless_zminus]) 1); qed "zmult_zless_mono2_neg"; -Goal "(m*n = int 0) = (m = int 0 | n = int 0)"; -by (case_tac "m < int 0" 1); +Goal "(m*n = (0::int)) = (m = 0 | n = 0)"; +by (case_tac "m < (0::int)" 1); by (auto_tac (claset(), simpset() addsimps [linorder_not_less, order_le_less, linorder_neq_iff])); by (REPEAT (force_tac (claset() addDs [zmult_zless_mono1_neg, zmult_zless_mono1], simpset()) 1)); -qed "zmult_eq_int0_iff"; +qed "zmult_eq_0_iff"; +AddIffs [zmult_eq_0_iff]; (** Cancellation laws for k*m < k*n and m*k < n*k, also for <= and =, but not (yet?) for k*m < n*k. **) -Goal "(m*k < n*k) = ((int 0 < k & m m<=n) & (k < int 0 --> n<=m))"; +Goal "(m*k <= n*k) = (((0::int) < k --> m<=n) & (k < 0 --> n<=m))"; by (simp_tac (simpset() addsimps [linorder_not_less RS sym, zmult_zless_cancel2]) 1); qed "zmult_zle_cancel2"; -Goal "(k*m <= k*n) = ((int 0 < k --> m<=n) & (k < int 0 --> n<=m))"; +Goal "(k*m <= k*n) = (((0::int) < k --> m<=n) & (k < 0 --> n<=m))"; by (simp_tac (simpset() addsimps [linorder_not_less RS sym, zmult_zless_cancel1]) 1); qed "zmult_zle_cancel1"; -Goal "(m*k = n*k) = (k = int 0 | m=n)"; +Goal "(m*k = n*k) = (k = (0::int) | m=n)"; by (cut_facts_tac [linorder_less_linear] 1); by Safe_tac; by Auto_tac; @@ -475,8 +535,15 @@ qed "zmult_cancel2"; -Goal "(k*m = k*n) = (k = int 0 | m=n)"; +Goal "(k*m = k*n) = (k = (0::int) | m=n)"; by (simp_tac (simpset() addsimps [inst "z" "k" zmult_commute, zmult_cancel2]) 1); qed "zmult_cancel1"; Addsimps [zmult_cancel1, zmult_cancel2]; + + +(*Analogous to zadd_int*) +Goal "n<=m --> int m - int n = int (m-n)"; +by (induct_thm_tac diff_induct "m n" 1); +by (auto_tac (claset(), simpset() addsimps [int_Suc, symmetric zdiff_def])); +qed_spec_mp "zdiff_int"; diff -r 76401b2ee871 -r 56db9f3a6b3e src/HOL/Integ/Int.thy --- a/src/HOL/Integ/Int.thy Mon Oct 22 11:01:30 2001 +0200 +++ b/src/HOL/Integ/Int.thy Mon Oct 22 11:54:22 2001 +0200 @@ -9,7 +9,7 @@ Int = IntDef + instance int :: order (zle_refl,zle_trans,zle_anti_sym,int_less_le) -instance int :: plus_ac0 (zadd_commute,zadd_assoc,zadd_zero) +instance int :: plus_ac0 (zadd_commute,zadd_assoc,zadd_0) instance int :: linorder (zle_linear) constdefs diff -r 76401b2ee871 -r 56db9f3a6b3e src/HOL/Integ/IntArith.ML --- a/src/HOL/Integ/IntArith.ML Mon Oct 22 11:01:30 2001 +0200 +++ b/src/HOL/Integ/IntArith.ML Mon Oct 22 11:54:22 2001 +0200 @@ -3,6 +3,7 @@ Authors: Larry Paulson and Tobias Nipkow *) + Goal "abs(abs(x::int)) = abs(x)"; by(arith_tac 1); qed "abs_abs"; @@ -20,7 +21,7 @@ (*** Intermediate value theorems ***) -Goal "(ALL i \ +Goal "(ALL i \ \ f 0 <= k --> k <= f n --> (EX i <= n. f i = (k::int))"; by(induct_tac "n" 1); by(Asm_simp_tac 1); @@ -40,7 +41,7 @@ bind_thm("nat0_intermed_int_val", ObjectLogic.rulify_no_asm lemma); -Goal "[| !i. m <= i & i < n --> abs(f(i + 1::nat) - f i) <= Numeral1; m < n; \ +Goal "[| !i. m <= i & i < n --> abs(f(i + 1::nat) - f i) <= 1; m < n; \ \ f m <= k; k <= f n |] ==> ? i. m <= i & i <= n & f i = (k::int)"; by(cut_inst_tac [("n","n-m"),("f", "%i. f(i+m)"),("k","k")]lemma 1); by(Asm_full_simp_tac 1); @@ -56,22 +57,22 @@ (*** Some convenient biconditionals for products of signs ***) -Goal "[| (Numeral0::int) < i; Numeral0 < j |] ==> Numeral0 < i*j"; +Goal "[| (0::int) < i; 0 < j |] ==> 0 < i*j"; by (dtac zmult_zless_mono1 1); by Auto_tac; qed "zmult_pos"; -Goal "[| i < (Numeral0::int); j < Numeral0 |] ==> Numeral0 < i*j"; +Goal "[| i < (0::int); j < 0 |] ==> 0 < i*j"; by (dtac zmult_zless_mono1_neg 1); by Auto_tac; qed "zmult_neg"; -Goal "[| (Numeral0::int) < i; j < Numeral0 |] ==> i*j < Numeral0"; +Goal "[| (0::int) < i; j < 0 |] ==> i*j < 0"; by (dtac zmult_zless_mono1_neg 1); by Auto_tac; qed "zmult_pos_neg"; -Goal "((Numeral0::int) < x*y) = (Numeral0 < x & Numeral0 < y | x < Numeral0 & y < Numeral0)"; +Goal "((0::int) < x*y) = (0 < x & 0 < y | x < 0 & y < 0)"; by (auto_tac (claset(), simpset() addsimps [order_le_less, linorder_not_less, zmult_pos, zmult_neg])); @@ -84,13 +85,13 @@ simpset() addsimps [zmult_commute])); qed "int_0_less_mult_iff"; -Goal "((Numeral0::int) <= x*y) = (Numeral0 <= x & Numeral0 <= y | x <= Numeral0 & y <= Numeral0)"; +Goal "((0::int) <= x*y) = (0 <= x & 0 <= y | x <= 0 & y <= 0)"; by (auto_tac (claset(), simpset() addsimps [order_le_less, linorder_not_less, int_0_less_mult_iff])); qed "int_0_le_mult_iff"; -Goal "(x*y < (Numeral0::int)) = (Numeral0 < x & y < Numeral0 | x < Numeral0 & Numeral0 < y)"; +Goal "(x*y < (0::int)) = (0 < x & y < 0 | x < 0 & 0 < y)"; by (auto_tac (claset(), simpset() addsimps [int_0_le_mult_iff, linorder_not_le RS sym])); @@ -98,30 +99,31 @@ simpset() addsimps [linorder_not_le])); qed "zmult_less_0_iff"; -Goal "(x*y <= (Numeral0::int)) = (Numeral0 <= x & y <= Numeral0 | x <= Numeral0 & Numeral0 <= y)"; +Goal "(x*y <= (0::int)) = (0 <= x & y <= 0 | x <= 0 & 0 <= y)"; by (auto_tac (claset() addDs [order_less_not_sym], simpset() addsimps [int_0_less_mult_iff, linorder_not_less RS sym])); qed "zmult_le_0_iff"; Goal "abs (x * y) = abs x * abs (y::int)"; -by (simp_tac (simpset () addsplits [zabs_split] +by (simp_tac (simpset () delsimps [thm "number_of_reorient"] addsplits [zabs_split] + addsplits [zabs_split] addsimps [zmult_less_0_iff, zle_def]) 1); qed "abs_mult"; -Goal "(abs x = Numeral0) = (x = (Numeral0::int))"; +Goal "(abs x = 0) = (x = (0::int))"; by (simp_tac (simpset () addsplits [zabs_split]) 1); qed "abs_eq_0"; AddIffs [abs_eq_0]; -Goal "(Numeral0 < abs x) = (x ~= (Numeral0::int))"; +Goal "(0 < abs x) = (x ~= (0::int))"; by (simp_tac (simpset () addsplits [zabs_split]) 1); by (arith_tac 1); qed "zero_less_abs_iff"; AddIffs [zero_less_abs_iff]; -Goal "Numeral0 <= x * (x::int)"; -by (subgoal_tac "(- x) * x <= Numeral0" 1); +Goal "0 <= x * (x::int)"; +by (subgoal_tac "(- x) * x <= 0" 1); by (Asm_full_simp_tac 1); by (simp_tac (HOL_basic_ss addsimps [zmult_le_0_iff]) 1); by Auto_tac; @@ -132,48 +134,48 @@ (*** Products and 1, by T. M. Rasmussen ***) -Goal "(m = m*(n::int)) = (n = Numeral1 | m = Numeral0)"; +Goal "(m = m*(n::int)) = (n = 1 | m = 0)"; by Auto_tac; -by (subgoal_tac "m*Numeral1 = m*n" 1); +by (subgoal_tac "m*1 = m*n" 1); by (dtac (zmult_cancel1 RS iffD1) 1); by Auto_tac; qed "zmult_eq_self_iff"; -Goal "[| Numeral1 < m; Numeral1 < n |] ==> Numeral1 < m*(n::int)"; -by (res_inst_tac [("y","Numeral1*n")] order_less_trans 1); +Goal "[| 1 < m; 1 < n |] ==> 1 < m*(n::int)"; +by (res_inst_tac [("y","1*n")] order_less_trans 1); by (rtac zmult_zless_mono1 2); by (ALLGOALS Asm_simp_tac); qed "zless_1_zmult"; -Goal "[| Numeral0 < n; n ~= Numeral1 |] ==> Numeral1 < (n::int)"; +Goal "[| 0 < n; n ~= 1 |] ==> 1 < (n::int)"; by (arith_tac 1); val lemma = result(); -Goal "Numeral0 < (m::int) ==> (m * n = Numeral1) = (m = Numeral1 & n = Numeral1)"; +Goal "0 < (m::int) ==> (m * n = 1) = (m = 1 & n = 1)"; by Auto_tac; -by (case_tac "m=Numeral1" 1); -by (case_tac "n=Numeral1" 2); -by (case_tac "m=Numeral1" 4); -by (case_tac "n=Numeral1" 5); +by (case_tac "m=1" 1); +by (case_tac "n=1" 2); +by (case_tac "m=1" 4); +by (case_tac "n=1" 5); by Auto_tac; by distinct_subgoals_tac; -by (subgoal_tac "Numeral1 z < w | z=(w::int)"; by (cut_facts_tac [zless_linear] 1); by (blast_tac (claset() addEs [zless_asym]) 1); @@ -506,11 +525,13 @@ qed "zle_zdiff_eq"; Goalw [zdiff_def] "(x-y = z) = (x = z + (y::int))"; -by (auto_tac (claset(), simpset() addsimps [zadd_assoc])); +by (auto_tac (claset(), + simpset() addsimps [zadd_assoc, symmetric Zero_int_def])); qed "zdiff_eq_eq"; Goalw [zdiff_def] "(x = z-y) = (x + (y::int) = z)"; -by (auto_tac (claset(), simpset() addsimps [zadd_assoc])); +by (auto_tac (claset(), + simpset() addsimps [zadd_assoc, symmetric Zero_int_def])); qed "eq_zdiff_eq"; (*This list of rewrites simplifies (in)equalities by bringing subtractions @@ -528,7 +549,8 @@ Goal "!!w::int. (z + w' = z + w) = (w' = w)"; by Safe_tac; by (dres_inst_tac [("f", "%x. x + (-z)")] arg_cong 1); -by (asm_full_simp_tac (simpset() addsimps zadd_ac) 1); +by (asm_full_simp_tac (simpset() addsimps symmetric Zero_int_def :: + zadd_ac) 1); qed "zadd_left_cancel"; Addsimps [zadd_left_cancel]; diff -r 76401b2ee871 -r 56db9f3a6b3e src/HOL/Integ/IntDef.thy --- a/src/HOL/Integ/IntDef.thy Mon Oct 22 11:01:30 2001 +0200 +++ b/src/HOL/Integ/IntDef.thy Mon Oct 22 11:54:22 2001 +0200 @@ -31,7 +31,7 @@ (*For simplifying equalities*) iszero :: int => bool - "iszero z == z = int 0" + "iszero z == z = (0::int)" defs (*of overloaded constants*) 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"; diff -r 76401b2ee871 -r 56db9f3a6b3e src/HOL/Integ/IntDiv.thy --- a/src/HOL/Integ/IntDiv.thy Mon Oct 22 11:01:30 2001 +0200 +++ b/src/HOL/Integ/IntDiv.thy Mon Oct 22 11:54:22 2001 +0200 @@ -12,27 +12,27 @@ quorem :: "(int*int) * (int*int) => bool" "quorem == %((a,b), (q,r)). a = b*q + r & - (if Numeral0 < b then Numeral0<=r & r int*int" - "adjust a b == %(q,r). if Numeral0 <= r-b then (2*q + Numeral1, r-b) - else (2*q, r)" + adjust :: "[int, int*int] => int*int" + "adjust b == %(q,r). if 0 <= r-b then (2*q + 1, r-b) + else (2*q, r)" (** the division algorithm **) (*for the case a>=0, b>0*) consts posDivAlg :: "int*int => int*int" -recdef posDivAlg "inv_image less_than (%(a,b). nat(a - b + Numeral1))" +recdef posDivAlg "inv_image less_than (%(a,b). nat(a - b + 1))" "posDivAlg (a,b) = - (if (a0*) consts negDivAlg :: "int*int => int*int" recdef negDivAlg "inv_image less_than (%(a,b). nat(- a - b))" "negDivAlg (a,b) = - (if (Numeral0<=a+b | b<=Numeral0) then (-1,a+b) - else adjust a b (negDivAlg(a, 2*b)))" + (if (0<=a+b | b<=0) then (-1,a+b) + else adjust b (negDivAlg(a, 2*b)))" (*for the general case b~=0*) @@ -44,12 +44,12 @@ including the special case a=0, b<0, because negDivAlg requires a<0*) divAlg :: "int*int => int*int" "divAlg == - %(a,b). if Numeral0<=a then - if Numeral0<=b then posDivAlg (a,b) - else if a=Numeral0 then (Numeral0,Numeral0) + %(a,b). if 0<=a then + if 0<=b then posDivAlg (a,b) + else if a=0 then (0,0) else negateSnd (negDivAlg (-a,-b)) else - if Numeral0 Suc m - n = m - (n - Numeral1)"; -by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1); +by (asm_simp_tac (simpset() addsimps [numeral_0_eq_0, numeral_1_eq_1] + addsplits [nat_diff_split]) 1); qed "Suc_diff_eq_diff_pred"; (*Now just instantiating n to (number_of v) does the right simplification, @@ -48,8 +49,8 @@ by (stac add_eq_if 1); by (asm_simp_tac (simpset() addsplits [nat.split] - addsimps [Let_def, neg_imp_number_of_eq_0, - neg_number_of_bin_pred_iff_0]) 1); + addsimps [numeral_1_eq_Suc_0 RS sym, Let_def, + neg_imp_number_of_eq_0, neg_number_of_bin_pred_iff_0]) 1); qed "nat_case_add_eq_if"; Addsimps [nat_case_number_of, nat_case_add_eq_if]; @@ -71,8 +72,8 @@ by (stac add_eq_if 1); by (asm_simp_tac (simpset() addsplits [nat.split] - addsimps [Let_def, neg_imp_number_of_eq_0, - neg_number_of_bin_pred_iff_0]) 1); + addsimps [numeral_1_eq_Suc_0 RS sym, Let_def, + neg_imp_number_of_eq_0, neg_number_of_bin_pred_iff_0]) 1); qed "nat_rec_add_eq_if"; Addsimps [nat_rec_number_of, nat_rec_add_eq_if]; @@ -80,7 +81,7 @@ (** For simplifying # m - Suc n **) -Goal "m - Suc n = (m - Numeral1) - n"; +Goal "m - Suc n = (m - 1) - n"; by (simp_tac (numeral_ss addsplits [nat_diff_split]) 1); qed "diff_Suc_eq_diff_pred"; @@ -93,7 +94,7 @@ (** Evens and Odds, for Mutilated Chess Board **) (*Case analysis on b<2*) -Goal "(n::nat) < 2 ==> n = Numeral0 | n = Numeral1"; +Goal "(n::nat) < 2 ==> n = 0 | n = Suc 0"; by (arith_tac 1); qed "less_2_cases"; @@ -101,16 +102,16 @@ by (subgoal_tac "m mod 2 < 2" 1); by (Asm_simp_tac 2); be (less_2_cases RS disjE) 1; -by (ALLGOALS (asm_simp_tac (simpset() addsimps [mod_Suc]))); +by (ALLGOALS (asm_simp_tac (simpset() addsimps [Let_def, mod_Suc, nat_1]))); qed "mod2_Suc_Suc"; Addsimps [mod2_Suc_Suc]; -Goal "!!m::nat. (0 < m mod 2) = (m mod 2 = Numeral1)"; +Goal "!!m::nat. (0 < m mod 2) = (m mod 2 = 1)"; by (subgoal_tac "m mod 2 < 2" 1); by (Asm_simp_tac 2); by (auto_tac (claset(), simpset() delsimps [mod_less_divisor])); qed "mod2_gr_0"; -Addsimps [mod2_gr_0, rename_numerals mod2_gr_0]; +Addsimps [mod2_gr_0]; (** Removal of small numerals: Numeral0, Numeral1 and (in additive positions) 2 **) diff -r 76401b2ee871 -r 56db9f3a6b3e src/HOL/Integ/int_arith1.ML --- a/src/HOL/Integ/int_arith1.ML Mon Oct 22 11:01:30 2001 +0200 +++ b/src/HOL/Integ/int_arith1.ML Mon Oct 22 11:54:22 2001 +0200 @@ -5,19 +5,21 @@ Simprocs and decision procedure for linear arithmetic. *) +Addsimps [int_numeral_0_eq_0, int_numeral_1_eq_1]; + (*** Simprocs for numeric literals ***) (** Combining of literal coefficients in sums of products **) -Goal "(x < y) = (x-y < (Numeral0::int))"; +Goal "(x < y) = (x-y < (0::int))"; by (simp_tac (simpset() addsimps zcompare_rls) 1); qed "zless_iff_zdiff_zless_0"; -Goal "(x = y) = (x-y = (Numeral0::int))"; +Goal "(x = y) = (x-y = (0::int))"; by (simp_tac (simpset() addsimps zcompare_rls) 1); qed "eq_iff_zdiff_eq_0"; -Goal "(x <= y) = (x-y <= (Numeral0::int))"; +Goal "(x <= y) = (x-y <= (0::int))"; by (simp_tac (simpset() addsimps zcompare_rls) 1); qed "zle_iff_zdiff_zle_0"; @@ -77,12 +79,22 @@ structure Int_Numeral_Simprocs = struct +(*Maps 0 to Numeral0 and 1 to Numeral1 so that arithmetic in simprocs + isn't complicated by the abstract 0 and 1.*) +val numeral_syms = [int_numeral_0_eq_0 RS sym, int_numeral_1_eq_1 RS sym]; +val numeral_sym_ss = HOL_ss addsimps numeral_syms; + +fun rename_numerals th = + simplify numeral_sym_ss (Thm.transfer (the_context ()) th); + (*Utilities*) fun mk_numeral n = HOLogic.number_of_const HOLogic.intT $ HOLogic.mk_bin n; (*Decodes a binary INTEGER*) -fun dest_numeral (Const("Numeral.number_of", _) $ w) = +fun dest_numeral (Const("0", _)) = 0 + | dest_numeral (Const("1", _)) = 1 + | dest_numeral (Const("Numeral.number_of", _) $ w) = (HOLogic.dest_binum w handle TERM _ => raise TERM("Int_Numeral_Simprocs.dest_numeral:1", [w])) | dest_numeral t = raise TERM("Int_Numeral_Simprocs.dest_numeral:2", [t]); @@ -97,7 +109,7 @@ val uminus_const = Const ("uminus", HOLogic.intT --> HOLogic.intT); -(*Thus mk_sum[t] yields t+Numeral0; longer sums don't have a trailing zero*) +(*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*) fun mk_sum [] = zero | mk_sum [t,u] = mk_plus (t, u) | mk_sum (t :: ts) = mk_plus (t, mk_sum ts); @@ -157,16 +169,20 @@ handle TERM _ => find_first_coeff (t::past) u terms; -(*Simplify Numeral1*n and n*Numeral1 to n*) -val add_0s = [zadd_0, zadd_0_right]; -val mult_1s = [zmult_1, zmult_1_right, zmult_minus1, zmult_minus1_right]; +(*Simplify Numeral0+n, n+Numeral0, Numeral1*n, n*Numeral1*) +val add_0s = map rename_numerals [zadd_0, zadd_0_right]; +val mult_1s = map rename_numerals [zmult_1, zmult_1_right] @ + [zmult_minus1, zmult_minus1_right]; -(*To perform binary arithmetic*) -val bin_simps = [add_number_of_left] @ bin_arith_simps @ bin_rel_simps; +(*To perform binary arithmetic. The "left" rewriting handles patterns + created by the simprocs, such as 3 * (5 * x). *) +val bin_simps = [int_numeral_0_eq_0 RS sym, int_numeral_1_eq_1 RS sym, + add_number_of_left, mult_number_of_left] @ + bin_arith_simps @ bin_rel_simps; (*To evaluate binary negations of coefficients*) val zminus_simps = NCons_simps @ - [number_of_minus RS sym, + [zminus_1_eq_m1, number_of_minus RS sym, bin_minus_1, bin_minus_0, bin_minus_Pls, bin_minus_Min, bin_pred_1, bin_pred_0, bin_pred_Pls, bin_pred_Min]; @@ -189,28 +205,10 @@ fun trans_tac None = all_tac | trans_tac (Some th) = ALLGOALS (rtac (th RS trans)); -fun prove_conv name tacs sg (hyps: thm list) (t,u) = - if t aconv u then None - else - let val ct = cterm_of sg (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u))) - in Some - (prove_goalw_cterm [] ct (K tacs) - handle ERROR => error - ("The error(s) above occurred while trying to prove " ^ - string_of_cterm ct ^ "\nInternal failure of simproc " ^ name)) - end; - -(*version without the hyps argument*) -fun prove_conv_nohyps name tacs sg = prove_conv name tacs sg []; - fun simplify_meta_eq rules = mk_meta_eq o simplify (HOL_basic_ss addeqcongs[eq_cong2] addsimps rules) -fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc; -fun prep_pat s = Thm.read_cterm (Theory.sign_of (the_context())) (s, HOLogic.termT); -val prep_pats = map prep_pat; - structure CancelNumeralsCommon = struct val mk_sum = mk_sum @@ -220,8 +218,8 @@ val find_first_coeff = find_first_coeff [] val trans_tac = trans_tac val norm_tac = - ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@ - zminus_simps@zadd_ac)) + ALLGOALS (simp_tac (HOL_ss addsimps numeral_syms@add_0s@mult_1s@ + diff_simps@zminus_simps@zadd_ac)) THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@int_mult_minus_simps)) THEN ALLGOALS (simp_tac (HOL_ss addsimps int_minus_from_mult_simps@ zadd_ac@zmult_ac)) @@ -232,7 +230,7 @@ structure EqCancelNumerals = CancelNumeralsFun (open CancelNumeralsCommon - val prove_conv = prove_conv "inteq_cancel_numerals" + val prove_conv = Bin_Simprocs.prove_conv "inteq_cancel_numerals" val mk_bal = HOLogic.mk_eq val dest_bal = HOLogic.dest_bin "op =" HOLogic.intT val bal_add1 = eq_add_iff1 RS trans @@ -241,7 +239,7 @@ structure LessCancelNumerals = CancelNumeralsFun (open CancelNumeralsCommon - val prove_conv = prove_conv "intless_cancel_numerals" + val prove_conv = Bin_Simprocs.prove_conv "intless_cancel_numerals" val mk_bal = HOLogic.mk_binrel "op <" val dest_bal = HOLogic.dest_bin "op <" HOLogic.intT val bal_add1 = less_add_iff1 RS trans @@ -250,7 +248,7 @@ structure LeCancelNumerals = CancelNumeralsFun (open CancelNumeralsCommon - val prove_conv = prove_conv "intle_cancel_numerals" + val prove_conv = Bin_Simprocs.prove_conv "intle_cancel_numerals" val mk_bal = HOLogic.mk_binrel "op <=" val dest_bal = HOLogic.dest_bin "op <=" HOLogic.intT val bal_add1 = le_add_iff1 RS trans @@ -258,19 +256,22 @@ ); val cancel_numerals = - map prep_simproc + map Bin_Simprocs.prep_simproc [("inteq_cancel_numerals", - prep_pats ["(l::int) + m = n", "(l::int) = m + n", + Bin_Simprocs.prep_pats + ["(l::int) + m = n", "(l::int) = m + n", "(l::int) - m = n", "(l::int) = m - n", "(l::int) * m = n", "(l::int) = m * n"], EqCancelNumerals.proc), ("intless_cancel_numerals", - prep_pats ["(l::int) + m < n", "(l::int) < m + n", + Bin_Simprocs.prep_pats + ["(l::int) + m < n", "(l::int) < m + n", "(l::int) - m < n", "(l::int) < m - n", "(l::int) * m < n", "(l::int) < m * n"], LessCancelNumerals.proc), ("intle_cancel_numerals", - prep_pats ["(l::int) + m <= n", "(l::int) <= m + n", + Bin_Simprocs.prep_pats + ["(l::int) + m <= n", "(l::int) <= m + n", "(l::int) - m <= n", "(l::int) <= m - n", "(l::int) * m <= n", "(l::int) <= m * n"], LeCancelNumerals.proc)]; @@ -284,11 +285,11 @@ val mk_coeff = mk_coeff val dest_coeff = dest_coeff 1 val left_distrib = left_zadd_zmult_distrib RS trans - val prove_conv = prove_conv_nohyps "int_combine_numerals" + val prove_conv = Bin_Simprocs.prove_conv_nohyps "int_combine_numerals" val trans_tac = trans_tac val norm_tac = - ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@ - zminus_simps@zadd_ac)) + ALLGOALS (simp_tac (HOL_ss addsimps numeral_syms@add_0s@mult_1s@ + diff_simps@zminus_simps@zadd_ac)) THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@int_mult_minus_simps)) THEN ALLGOALS (simp_tac (HOL_ss addsimps int_minus_from_mult_simps@ zadd_ac@zmult_ac)) @@ -299,9 +300,9 @@ structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData); -val combine_numerals = - prep_simproc ("int_combine_numerals", - prep_pats ["(i::int) + j", "(i::int) - j"], +val combine_numerals = Bin_Simprocs.prep_simproc + ("int_combine_numerals", + Bin_Simprocs.prep_pats ["(i::int) + j", "(i::int) - j"], CombineNumerals.proc); end; @@ -316,7 +317,7 @@ print_depth 22; set timing; set trace_simp; -fun test s = (Goal s; by (Simp_tac 1)); +fun test s = (Goal s, by (Simp_tac 1)); test "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::int)"; @@ -403,17 +404,20 @@ local (* reduce contradictory <= to False *) -val add_rules = simp_thms @ bin_arith_simps @ bin_rel_simps @ - [zadd_0, zadd_0_right, zdiff_def, - zadd_zminus_inverse, zadd_zminus_inverse2, - zmult_0, zmult_0_right, - zmult_1, zmult_1_right, - zmult_minus1, zmult_minus1_right, - zminus_zadd_distrib, zminus_zminus, zmult_assoc, - Zero_int_def, One_int_def, int_0, int_1, zadd_int RS sym, int_Suc]; +val add_rules = + simp_thms @ bin_arith_simps @ bin_rel_simps @ + [int_numeral_0_eq_0, int_numeral_1_eq_1, + zadd_0, zadd_0_right, zdiff_def, + zadd_zminus_inverse, zadd_zminus_inverse2, + zmult_0, zmult_0_right, + zmult_1, zmult_1_right, + zmult_minus1, zmult_minus1_right, + zminus_zadd_distrib, zminus_zminus, zmult_assoc, + int_0, int_1, zadd_int RS sym, int_Suc]; val simprocs = [Int_Times_Assoc.conv, Int_Numeral_Simprocs.combine_numerals]@ - Int_Numeral_Simprocs.cancel_numerals; + Int_Numeral_Simprocs.cancel_numerals @ + Bin_Simprocs.eval_numerals; val add_mono_thms_int = map (fn s => prove_goal (the_context ()) s @@ -457,7 +461,7 @@ by (fast_arith_tac 1); Goal "!!a::int. [| a < b; c < d |] ==> a-d+ 2 <= b+(-c)"; by (fast_arith_tac 1); -Goal "!!a::int. [| a < b; c < d |] ==> a+c+ Numeral1 < b+d"; +Goal "!!a::int. [| a < b; c < d |] ==> a+c+ 1 < b+d"; by (fast_arith_tac 1); Goal "!!a::int. [| a <= b; b+b <= c |] ==> a+a <= c"; by (fast_arith_tac 1); diff -r 76401b2ee871 -r 56db9f3a6b3e src/HOL/Integ/int_arith2.ML --- a/src/HOL/Integ/int_arith2.ML Mon Oct 22 11:01:30 2001 +0200 +++ b/src/HOL/Integ/int_arith2.ML Mon Oct 22 11:54:22 2001 +0200 @@ -3,19 +3,17 @@ Authors: Larry Paulson and Tobias Nipkow *) -(** Simplification of inequalities involving numerical constants **) - -Goal "(w <= z - (Numeral1::int)) = (w<(z::int))"; +Goal "(w <= z - (1::int)) = (w<(z::int))"; by (arith_tac 1); qed "zle_diff1_eq"; Addsimps [zle_diff1_eq]; -Goal "(w < z + Numeral1) = (w<=(z::int))"; +Goal "(w < z + 1) = (w<=(z::int))"; by (arith_tac 1); qed "zle_add1_eq_le"; Addsimps [zle_add1_eq_le]; -Goal "(z = z + w) = (w = (Numeral0::int))"; +Goal "(z = z + w) = (w = (0::int))"; by (arith_tac 1); qed "zadd_left_cancel0"; Addsimps [zadd_left_cancel0]; @@ -23,13 +21,13 @@ (* nat *) -Goal "Numeral0 <= z ==> int (nat z) = z"; +Goal "0 <= z ==> int (nat z) = z"; by (asm_full_simp_tac (simpset() addsimps [neg_eq_less_0, zle_def, not_neg_nat]) 1); qed "nat_0_le"; -Goal "z <= Numeral0 ==> nat z = 0"; -by (case_tac "z = Numeral0" 1); +Goal "z <= 0 ==> nat z = 0"; +by (case_tac "z = 0" 1); by (asm_simp_tac (simpset() addsimps [nat_le_int0]) 1); by (asm_full_simp_tac (simpset() addsimps [neg_eq_less_0, neg_nat, linorder_neq_iff]) 1); @@ -37,19 +35,19 @@ Addsimps [nat_0_le, nat_le_0]; -val [major,minor] = Goal "[| Numeral0 <= z; !!m. z = int m ==> P |] ==> P"; +val [major,minor] = Goal "[| 0 <= z; !!m. z = int m ==> P |] ==> P"; by (rtac (major RS nat_0_le RS sym RS minor) 1); qed "nonneg_eq_int"; -Goal "(nat w = m) = (if Numeral0 <= w then w = int m else m=0)"; +Goal "(nat w = m) = (if 0 <= w then w = int m else m=0)"; by Auto_tac; qed "nat_eq_iff"; -Goal "(m = nat w) = (if Numeral0 <= w then w = int m else m=0)"; +Goal "(m = nat w) = (if 0 <= w then w = int m else m=0)"; by Auto_tac; qed "nat_eq_iff2"; -Goal "Numeral0 <= w ==> (nat w < m) = (w < int m)"; +Goal "0 <= w ==> (nat w < m) = (w < int m)"; by (rtac iffI 1); by (asm_full_simp_tac (simpset() delsimps [zless_int] addsimps [zless_int RS sym]) 2); @@ -57,48 +55,41 @@ by (Simp_tac 1); qed "nat_less_iff"; -Goal "(int m = z) = (m = nat z & Numeral0 <= z)"; +Goal "(int m = z) = (m = nat z & 0 <= z)"; by (auto_tac (claset(), simpset() addsimps [nat_eq_iff2])); qed "int_eq_iff"; -Addsimps [inst "z" "number_of ?v" int_eq_iff]; - (*Users don't want to see (int 0), int(Suc 0) or w + - z*) -Addsimps [int_0, int_Suc, symmetric zdiff_def]; +Addsimps (map symmetric [Zero_int_def, One_int_def, zdiff_def]); -Goal "nat Numeral0 = 0"; +Goal "nat 0 = 0"; by (simp_tac (simpset() addsimps [nat_eq_iff]) 1); qed "nat_0"; -Goal "nat Numeral1 = Suc 0"; -by (simp_tac (simpset() addsimps [nat_eq_iff]) 1); +Goal "nat 1 = Suc 0"; +by (stac nat_eq_iff 1); +by (Simp_tac 1); qed "nat_1"; Goal "nat 2 = Suc (Suc 0)"; -by (simp_tac (simpset() addsimps [nat_eq_iff]) 1); +by (stac nat_eq_iff 1); +by (Simp_tac 1); qed "nat_2"; -Goal "Numeral0 <= w ==> (nat w < nat z) = (w (nat w < nat z) = (w (nat w <= nat z) = (w<=z)"; +Goal "0 < w | 0 <= z ==> (nat w <= nat z) = (w<=z)"; by (auto_tac (claset(), simpset() addsimps [linorder_not_less RS sym, zless_nat_conj])); qed "nat_le_eq_zle"; -(*Analogous to zadd_int, but more easily provable using the arithmetic in Bin*) -Goal "n<=m --> int m - int n = int (m-n)"; -by (induct_thm_tac diff_induct "m n" 1); -by Auto_tac; -qed_spec_mp "zdiff_int"; - - (*** abs: absolute value, as an integer ****) (* Simpler: use zabs_def as rewrite rule; @@ -106,13 +97,17 @@ *) Goalw [zabs_def] - "P(abs(i::int)) = ((Numeral0 <= i --> P i) & (i < Numeral0 --> P(-i)))"; + "P(abs(i::int)) = ((0 <= i --> P i) & (i < 0 --> P(-i)))"; by(Simp_tac 1); qed "zabs_split"; -Goal "Numeral0 <= abs (z::int)"; +Goal "0 <= abs (z::int)"; by (simp_tac (simpset() addsimps [zabs_def]) 1); qed "zero_le_zabs"; AddIffs [zero_le_zabs]; + +(*Not sure why this simprule is required!*) +Addsimps [inst "z" "number_of ?v" int_eq_iff]; + (*continued in IntArith.ML ...*) diff -r 76401b2ee871 -r 56db9f3a6b3e src/HOL/Integ/int_factor_simprocs.ML --- a/src/HOL/Integ/int_factor_simprocs.ML Mon Oct 22 11:01:30 2001 +0200 +++ b/src/HOL/Integ/int_factor_simprocs.ML Mon Oct 22 11:54:22 2001 +0200 @@ -10,27 +10,27 @@ (** Factor cancellation theorems for "int" **) -Goal "!!k::int. (k*m <= k*n) = ((Numeral0 < k --> m<=n) & (k < Numeral0 --> n<=m))"; +Goal "!!k::int. (k*m <= k*n) = ((0 < k --> m<=n) & (k < 0 --> n<=m))"; by (stac zmult_zle_cancel1 1); by Auto_tac; qed "int_mult_le_cancel1"; -Goal "!!k::int. (k*m < k*n) = ((Numeral0 < k & m (k*m) div (k*n) = (m div n)"; +Goal "!!k::int. k~=0 ==> (k*m) div (k*n) = (m div n)"; by (stac zdiv_zmult_zmult1 1); by Auto_tac; qed "int_mult_div_cancel1"; (*For ExtractCommonTermFun, cancelling common factors*) -Goal "(k*m) div (k*n) = (if k = (Numeral0::int) then Numeral0 else m div n)"; +Goal "(k*m) div (k*n) = (if k = (0::int) then 0 else m div n)"; by (simp_tac (simpset() addsimps [int_mult_div_cancel1]) 1); qed "int_mult_div_cancel_disj"; @@ -54,7 +54,7 @@ structure DivCancelNumeralFactor = CancelNumeralFactorFun (open CancelNumeralFactorCommon - val prove_conv = prove_conv "intdiv_cancel_numeral_factor" + val prove_conv = Bin_Simprocs.prove_conv "intdiv_cancel_numeral_factor" val mk_bal = HOLogic.mk_binop "Divides.op div" val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.intT val cancel = int_mult_div_cancel1 RS trans @@ -63,7 +63,7 @@ structure EqCancelNumeralFactor = CancelNumeralFactorFun (open CancelNumeralFactorCommon - val prove_conv = prove_conv "inteq_cancel_numeral_factor" + val prove_conv = Bin_Simprocs.prove_conv "inteq_cancel_numeral_factor" val mk_bal = HOLogic.mk_eq val dest_bal = HOLogic.dest_bin "op =" HOLogic.intT val cancel = int_mult_eq_cancel1 RS trans @@ -72,7 +72,7 @@ structure LessCancelNumeralFactor = CancelNumeralFactorFun (open CancelNumeralFactorCommon - val prove_conv = prove_conv "intless_cancel_numeral_factor" + val prove_conv = Bin_Simprocs.prove_conv "intless_cancel_numeral_factor" val mk_bal = HOLogic.mk_binrel "op <" val dest_bal = HOLogic.dest_bin "op <" HOLogic.intT val cancel = int_mult_less_cancel1 RS trans @@ -81,7 +81,7 @@ structure LeCancelNumeralFactor = CancelNumeralFactorFun (open CancelNumeralFactorCommon - val prove_conv = prove_conv "intle_cancel_numeral_factor" + val prove_conv = Bin_Simprocs.prove_conv "intle_cancel_numeral_factor" val mk_bal = HOLogic.mk_binrel "op <=" val dest_bal = HOLogic.dest_bin "op <=" HOLogic.intT val cancel = int_mult_le_cancel1 RS trans @@ -89,18 +89,18 @@ ) val int_cancel_numeral_factors = - map prep_simproc + map Bin_Simprocs.prep_simproc [("inteq_cancel_numeral_factors", - prep_pats ["(l::int) * m = n", "(l::int) = m * n"], + Bin_Simprocs.prep_pats ["(l::int) * m = n", "(l::int) = m * n"], EqCancelNumeralFactor.proc), ("intless_cancel_numeral_factors", - prep_pats ["(l::int) * m < n", "(l::int) < m * n"], + Bin_Simprocs.prep_pats ["(l::int) * m < n", "(l::int) < m * n"], LessCancelNumeralFactor.proc), ("intle_cancel_numeral_factors", - prep_pats ["(l::int) * m <= n", "(l::int) <= m * n"], + Bin_Simprocs.prep_pats ["(l::int) * m <= n", "(l::int) <= m * n"], LeCancelNumeralFactor.proc), ("intdiv_cancel_numeral_factors", - prep_pats ["((l::int) * m) div n", "(l::int) div (m * n)"], + Bin_Simprocs.prep_pats ["((l::int) * m) div n", "(l::int) div (m * n)"], DivCancelNumeralFactor.proc)]; end; @@ -181,7 +181,7 @@ structure EqCancelFactor = ExtractCommonTermFun (open CancelFactorCommon - val prove_conv = prove_conv "int_eq_cancel_factor" + val prove_conv = Bin_Simprocs.prove_conv "int_eq_cancel_factor" val mk_bal = HOLogic.mk_eq val dest_bal = HOLogic.dest_bin "op =" HOLogic.intT val simplify_meta_eq = cancel_simplify_meta_eq int_mult_eq_cancel1 @@ -189,19 +189,19 @@ structure DivideCancelFactor = ExtractCommonTermFun (open CancelFactorCommon - val prove_conv = prove_conv "int_divide_cancel_factor" + val prove_conv = Bin_Simprocs.prove_conv "int_divide_cancel_factor" val mk_bal = HOLogic.mk_binop "Divides.op div" val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.intT val simplify_meta_eq = cancel_simplify_meta_eq int_mult_div_cancel_disj ); val int_cancel_factor = - map prep_simproc + map Bin_Simprocs.prep_simproc [("int_eq_cancel_factor", - prep_pats ["(l::int) * m = n", "(l::int) = m * n"], + Bin_Simprocs.prep_pats ["(l::int) * m = n", "(l::int) = m * n"], EqCancelFactor.proc), ("int_divide_cancel_factor", - prep_pats ["((l::int) * m) div n", "(l::int) div (m * n)"], + Bin_Simprocs.prep_pats ["((l::int) * m) div n", "(l::int) div (m * n)"], DivideCancelFactor.proc)]; end; diff -r 76401b2ee871 -r 56db9f3a6b3e src/HOL/Integ/nat_bin.ML --- a/src/HOL/Integ/nat_bin.ML Mon Oct 22 11:01:30 2001 +0200 +++ b/src/HOL/Integ/nat_bin.ML Mon Oct 22 11:54:22 2001 +0200 @@ -13,29 +13,29 @@ Goal "nat (number_of w) = number_of w"; by (simp_tac (simpset() addsimps [nat_number_of_def]) 1); qed "nat_number_of"; -Addsimps [nat_number_of]; - -(*These rewrites should one day be re-oriented...*) +Addsimps [nat_number_of, nat_0, nat_1]; Goal "Numeral0 = (0::nat)"; -by (simp_tac (HOL_basic_ss addsimps [nat_0, nat_number_of_def]) 1); +by (simp_tac (simpset() addsimps [nat_number_of_def]) 1); qed "numeral_0_eq_0"; Goal "Numeral1 = (1::nat)"; -by (simp_tac (HOL_basic_ss addsimps [nat_1, nat_number_of_def, One_nat_def]) 1); +by (simp_tac (simpset() addsimps [nat_1, nat_number_of_def]) 1); qed "numeral_1_eq_1"; -Goal "2 = Suc 1"; -by (simp_tac (HOL_basic_ss addsimps [nat_2, nat_number_of_def, One_nat_def]) 1); +Goal "Numeral1 = Suc 0"; +by (simp_tac (simpset() addsimps [numeral_1_eq_1]) 1); +qed "numeral_1_eq_Suc_0"; + +Goalw [nat_number_of_def, One_nat_def] "2 = Suc 1"; +by (rtac nat_2 1); qed "numeral_2_eq_2"; -bind_thm ("zero_eq_numeral_0", numeral_0_eq_0 RS sym); - (** int (coercion from nat to int) **) (*"neg" is used in rewrite rules for binary comparisons*) Goal "int (number_of v :: nat) = \ -\ (if neg (number_of v) then Numeral0 \ +\ (if neg (number_of v) then 0 \ \ else (number_of v :: int))"; by (simp_tac (simpset_of Int.thy addsimps [neg_nat, nat_number_of_def, @@ -45,45 +45,39 @@ val nat_bin_arith_setup = - [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} => - {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, - inj_thms = inj_thms, - lessD = lessD, - simpset = simpset addsimps [int_nat_number_of, - not_neg_number_of_Pls,neg_number_of_Min,neg_number_of_BIT]})]; + [Fast_Arith.map_data + (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} => + {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, + inj_thms = inj_thms, + lessD = lessD, + simpset = simpset addsimps [int_nat_number_of, not_neg_number_of_Pls, + neg_number_of_Min,neg_number_of_BIT]})]; (** Successor **) -Goal "(Numeral0::int) <= z ==> Suc (nat z) = nat (Numeral1 + z)"; +Goal "(0::int) <= z ==> Suc (nat z) = nat (1 + z)"; by (rtac sym 1); -by (asm_simp_tac (simpset() addsimps [nat_eq_iff]) 1); +by (asm_simp_tac (simpset() addsimps [nat_eq_iff, int_Suc]) 1); qed "Suc_nat_eq_nat_zadd1"; -Goal "Suc (number_of v) = \ -\ (if neg (number_of v) then Numeral1 else number_of (bin_succ v))"; +Goal "Suc (number_of v + n) = \ +\ (if neg (number_of v) then 1+n else number_of (bin_succ v) + n)"; by (simp_tac (simpset_of Int.thy addsimps [neg_nat, nat_1, not_neg_eq_ge_0, nat_number_of_def, int_Suc, Suc_nat_eq_nat_zadd1, number_of_succ]) 1); +qed "Suc_nat_number_of_add"; + +Goal "Suc (number_of v) = \ +\ (if neg (number_of v) then 1 else number_of (bin_succ v))"; +by (cut_inst_tac [("n","0")] Suc_nat_number_of_add 1); +by (asm_full_simp_tac (simpset() delcongs [if_weak_cong]) 1); qed "Suc_nat_number_of"; Addsimps [Suc_nat_number_of]; -Goal "Suc (number_of v + n) = \ -\ (if neg (number_of v) then Numeral1+n else number_of (bin_succ v) + n)"; -by (Simp_tac 1); -qed "Suc_nat_number_of_add"; - -Goal "Suc Numeral0 = Numeral1"; -by (Simp_tac 1); -qed "Suc_numeral_0_eq_1"; - -Goal "Suc Numeral1 = 2"; -by (Simp_tac 1); -qed "Suc_numeral_1_eq_2"; - (** Addition **) -Goal "[| (Numeral0::int) <= z; Numeral0 <= z' |] ==> nat (z+z') = nat z + nat z'"; +Goal "[| (0::int) <= z; 0 <= z' |] ==> nat (z+z') = nat z + nat z'"; by (rtac (inj_int RS injD) 1); by (asm_simp_tac (simpset() addsimps [zadd_int RS sym]) 1); qed "nat_add_distrib"; @@ -103,7 +97,7 @@ (** Subtraction **) -Goal "[| (Numeral0::int) <= z'; z' <= z |] ==> nat (z-z') = nat z - nat z'"; +Goal "[| (0::int) <= z'; z' <= z |] ==> nat (z-z') = nat z - nat z'"; by (rtac (inj_int RS injD) 1); by (asm_simp_tac (simpset() addsimps [zdiff_int RS sym, nat_le_eq_zle]) 1); qed "nat_diff_distrib"; @@ -122,7 +116,7 @@ "(number_of v :: nat) - number_of v' = \ \ (if neg (number_of v') then number_of v \ \ else let d = number_of (bin_add v (bin_minus v')) in \ -\ if neg d then Numeral0 else nat d)"; +\ if neg d then 0 else nat d)"; by (simp_tac (simpset_of Int.thy delcongs [if_weak_cong] addsimps [not_neg_eq_ge_0, nat_0, @@ -134,22 +128,22 @@ (** Multiplication **) -Goal "(Numeral0::int) <= z ==> nat (z*z') = nat z * nat z'"; -by (case_tac "Numeral0 <= z'" 1); +Goal "(0::int) <= z ==> nat (z*z') = nat z * nat z'"; +by (case_tac "0 <= z'" 1); by (asm_full_simp_tac (simpset() addsimps [zmult_le_0_iff]) 2); by (rtac (inj_int RS injD) 1); by (asm_simp_tac (simpset() addsimps [zmult_int RS sym, int_0_le_mult_iff]) 1); qed "nat_mult_distrib"; -Goal "z <= (Numeral0::int) ==> nat(z*z') = nat(-z) * nat(-z')"; +Goal "z <= (0::int) ==> nat(z*z') = nat(-z) * nat(-z')"; by (rtac trans 1); by (rtac nat_mult_distrib 2); by Auto_tac; qed "nat_mult_distrib_neg"; Goal "(number_of v :: nat) * number_of v' = \ -\ (if neg (number_of v) then Numeral0 else number_of (bin_mult v v'))"; +\ (if neg (number_of v) then 0 else number_of (bin_mult v v'))"; by (simp_tac (simpset_of Int.thy addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def, nat_mult_distrib RS sym, number_of_mult, @@ -161,15 +155,15 @@ (** Quotient **) -Goal "(Numeral0::int) <= z ==> nat (z div z') = nat z div nat z'"; -by (case_tac "Numeral0 <= z'" 1); +Goal "(0::int) <= z ==> nat (z div z') = nat z div nat z'"; +by (case_tac "0 <= z'" 1); by (auto_tac (claset(), simpset() addsimps [div_nonneg_neg_le0, DIVISION_BY_ZERO_DIV])); -by (zdiv_undefined_case_tac "z' = Numeral0" 1); +by (zdiv_undefined_case_tac "z' = 0" 1); by (simp_tac (simpset() addsimps [numeral_0_eq_0, DIVISION_BY_ZERO_DIV]) 1); by (auto_tac (claset() addSEs [nonneg_eq_int], simpset())); by (rename_tac "m m'" 1); -by (subgoal_tac "Numeral0 <= int m div int m'" 1); +by (subgoal_tac "0 <= int m div int m'" 1); by (asm_full_simp_tac (simpset() addsimps [numeral_0_eq_0, pos_imp_zdiv_nonneg_iff]) 2); by (rtac (inj_int RS injD) 1); @@ -184,7 +178,7 @@ qed "nat_div_distrib"; Goal "(number_of v :: nat) div number_of v' = \ -\ (if neg (number_of v) then Numeral0 \ +\ (if neg (number_of v) then 0 \ \ else nat (number_of v div number_of v'))"; by (simp_tac (simpset_of Int.thy addsimps [not_neg_eq_ge_0, nat_number_of_def, neg_nat, @@ -197,12 +191,12 @@ (** Remainder **) (*Fails if z'<0: the LHS collapses to (nat z) but the RHS doesn't*) -Goal "[| (Numeral0::int) <= z; Numeral0 <= z' |] ==> nat (z mod z') = nat z mod nat z'"; -by (zdiv_undefined_case_tac "z' = Numeral0" 1); +Goal "[| (0::int) <= z; 0 <= z' |] ==> nat (z mod z') = nat z mod nat z'"; +by (zdiv_undefined_case_tac "z' = 0" 1); by (simp_tac (simpset() addsimps [numeral_0_eq_0, DIVISION_BY_ZERO_MOD]) 1); by (auto_tac (claset() addSEs [nonneg_eq_int], simpset())); by (rename_tac "m m'" 1); -by (subgoal_tac "Numeral0 <= int m mod int m'" 1); +by (subgoal_tac "0 <= int m mod int m'" 1); by (asm_full_simp_tac (simpset() addsimps [nat_less_iff, numeral_0_eq_0, pos_mod_sign]) 2); by (rtac (inj_int RS injD) 1); @@ -217,7 +211,7 @@ qed "nat_mod_distrib"; Goal "(number_of v :: nat) mod number_of v' = \ -\ (if neg (number_of v) then Numeral0 \ +\ (if neg (number_of v) then 0 \ \ else if neg (number_of v') then number_of v \ \ else nat (number_of v mod number_of v'))"; by (simp_tac @@ -228,12 +222,36 @@ Addsimps [mod_nat_number_of]; +structure NatAbstractNumeralsData = + struct + val dest_eq = HOLogic.dest_eq o HOLogic.dest_Trueprop o concl_of + val is_numeral = Bin_Simprocs.is_numeral + val numeral_0_eq_0 = numeral_0_eq_0 + val numeral_1_eq_1 = numeral_1_eq_Suc_0 + val prove_conv = Bin_Simprocs.prove_conv_nohyps "nat_abstract_numerals" + fun norm_tac simps = ALLGOALS (simp_tac (HOL_ss addsimps simps)) + val simplify_meta_eq = Bin_Simprocs.simplify_meta_eq + end + +structure NatAbstractNumerals = AbstractNumeralsFun (NatAbstractNumeralsData) + +val nat_eval_numerals = + map Bin_Simprocs.prep_simproc + [("nat_div_eval_numerals", + Bin_Simprocs.prep_pats ["(Suc 0) div m"], + NatAbstractNumerals.proc div_nat_number_of), + ("nat_mod_eval_numerals", + Bin_Simprocs.prep_pats ["(Suc 0) mod m"], + NatAbstractNumerals.proc mod_nat_number_of)]; + +Addsimprocs nat_eval_numerals; + (*** Comparisons ***) (** Equals (=) **) -Goal "[| (Numeral0::int) <= z; Numeral0 <= z' |] ==> (nat z = nat z') = (z=z')"; +Goal "[| (0::int) <= z; 0 <= z' |] ==> (nat z = nat z') = (z=z')"; by (auto_tac (claset() addSEs [nonneg_eq_int], simpset())); qed "eq_nat_nat_iff"; @@ -262,7 +280,7 @@ (simpset_of Int.thy addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def, nat_less_eq_zless, less_number_of_eq_neg, nat_0]) 1); -by (simp_tac (simpset_of Int.thy addsimps [neg_eq_less_int0, zminus_zless, +by (simp_tac (simpset_of Int.thy addsimps [neg_eq_less_0, zminus_zless, number_of_minus, zless_nat_eq_int_zless]) 1); qed "less_nat_number_of"; @@ -278,24 +296,14 @@ Addsimps [le_nat_number_of_eq_not_less]; -(*** New versions of existing theorems involving 0, 1, 2 ***) -(*Maps n to # n for n = 0, 1, 2*) -val numeral_sym_ss = - HOL_ss addsimps [numeral_0_eq_0 RS sym, - numeral_1_eq_1 RS sym, - numeral_2_eq_2 RS sym, - Suc_numeral_1_eq_2, Suc_numeral_0_eq_1]; - -fun rename_numerals th = simplify numeral_sym_ss (Thm.transfer (the_context ()) th); - -(*Maps # n to n for n = 0, 1, 2*) +(*Maps #n to n for n = 0, 1, 2*) bind_thms ("numerals", [numeral_0_eq_0, numeral_1_eq_1, numeral_2_eq_2]); val numeral_ss = simpset() addsimps numerals; (** Nat **) -Goal "Numeral0 < n ==> n = Suc(n - Numeral1)"; +Goal "0 < n ==> n = Suc(n - 1)"; by (asm_full_simp_tac numeral_ss 1); qed "Suc_pred'"; @@ -303,111 +311,48 @@ NOT suitable for rewriting because n recurs in the condition.*) bind_thm ("expand_Suc", inst "n" "number_of ?v" Suc_pred'); -(** NatDef & Nat **) - -Addsimps (map rename_numerals [min_0L, min_0R, max_0L, max_0R]); - -AddIffs (map rename_numerals - [Suc_not_Zero, Zero_not_Suc, zero_less_Suc, not_less0, less_one, - le0, le_0_eq, neq0_conv, not_gr0]); - (** Arith **) -(*Identity laws for + - * *) -val basic_renamed_arith_simps = - map rename_numerals - [diff_0, diff_0_eq_0, add_0, add_0_right, - mult_0, mult_0_right, mult_1, mult_1_right]; - -(*Non-trivial simplifications*) -val other_renamed_arith_simps = - map rename_numerals - [diff_is_0_eq, zero_less_diff, - mult_is_0, zero_less_mult_iff, mult_eq_1_iff]; - -Addsimps (basic_renamed_arith_simps @ other_renamed_arith_simps); - -AddIffs (map rename_numerals [add_is_0, add_gr_0]); - -Goal "Suc n = n + Numeral1"; +Goal "Suc n = n + 1"; by (asm_simp_tac numeral_ss 1); qed "Suc_eq_add_numeral_1"; (* These two can be useful when m = number_of... *) -Goal "(m::nat) + n = (if m=Numeral0 then n else Suc ((m - Numeral1) + n))"; +Goal "(m::nat) + n = (if m=0 then n else Suc ((m - 1) + n))"; by (case_tac "m" 1); by (ALLGOALS (asm_simp_tac numeral_ss)); qed "add_eq_if"; -Goal "(m::nat) * n = (if m=Numeral0 then Numeral0 else n + ((m - Numeral1) * n))"; +Goal "(m::nat) * n = (if m=0 then 0 else n + ((m - 1) * n))"; by (case_tac "m" 1); by (ALLGOALS (asm_simp_tac numeral_ss)); qed "mult_eq_if"; -Goal "(p ^ m :: nat) = (if m=Numeral0 then Numeral1 else p * (p ^ (m - Numeral1)))"; +Goal "(p ^ m :: nat) = (if m=0 then 1 else p * (p ^ (m - 1)))"; by (case_tac "m" 1); by (ALLGOALS (asm_simp_tac numeral_ss)); qed "power_eq_if"; -Goal "[| Numeral0 m - n < (m::nat)"; +Goal "[| 0 m - n < (m::nat)"; by (asm_full_simp_tac (numeral_ss addsimps [diff_less]) 1); qed "diff_less'"; Addsimps [inst "n" "number_of ?v" diff_less']; -(*various theorems that aren't in the default simpset*) -bind_thm ("add_is_one'", rename_numerals add_is_1); -bind_thm ("zero_induct'", rename_numerals zero_induct); -bind_thm ("diff_self_eq_0'", rename_numerals diff_self_eq_0); -bind_thm ("mult_eq_self_implies_10'", rename_numerals mult_eq_self_implies_10); - -(** Divides **) - -Addsimps (map rename_numerals [mod_1, mod_0, div_1, div_0]); -AddIffs (map rename_numerals [dvd_1_left, dvd_0_right]); - -(*useful?*) -bind_thm ("mod_self'", rename_numerals mod_self); -bind_thm ("div_self'", rename_numerals div_self); -bind_thm ("div_less'", rename_numerals div_less); -bind_thm ("mod_mult_self_is_zero'", rename_numerals mod_mult_self_is_0); - (** Power **) -Goal "(p::nat) ^ Numeral0 = Numeral1"; -by (simp_tac numeral_ss 1); -qed "power_zero"; - -Goal "(p::nat) ^ Numeral1 = p"; -by (simp_tac numeral_ss 1); -qed "power_one"; -Addsimps [power_zero, power_one]; - Goal "(p::nat) ^ 2 = p*p"; by (simp_tac numeral_ss 1); qed "power_two"; -Goal "Numeral0 < (i::nat) ==> Numeral0 < i^n"; -by (asm_simp_tac numeral_ss 1); -qed "zero_less_power'"; -Addsimps [zero_less_power']; - -bind_thm ("binomial_zero", rename_numerals binomial_0); -bind_thm ("binomial_Suc'", rename_numerals binomial_Suc); -bind_thm ("binomial_n_n'", rename_numerals binomial_n_n); - -(*binomial_0_Suc doesn't work well on numerals*) -Addsimps (map rename_numerals [binomial_n_0, binomial_zero, binomial_1]); - -Addsimps [rename_numerals card_Pow]; (*** Comparisons involving (0::nat) ***) Goal "(number_of v = (0::nat)) = \ \ (if neg (number_of v) then True else iszero (number_of v))"; -by (simp_tac (simpset() addsimps [numeral_0_eq_0 RS sym]) 1); -qed "eq_number_of_0"; +by (simp_tac (simpset() addsimps [numeral_0_eq_0 RS sym, iszero_0]) 1); +qed "eq_number_of_0"; Goal "((0::nat) = number_of v) = \ \ (if neg (number_of v) then True else iszero (number_of v))"; @@ -422,7 +367,7 @@ Addsimps [eq_number_of_0, eq_0_number_of, less_0_number_of]; Goal "neg (number_of v) ==> number_of v = (0::nat)"; -by (asm_simp_tac (simpset() addsimps [numeral_0_eq_0 RS sym]) 1); +by (asm_simp_tac (simpset() addsimps [numeral_0_eq_0 RS sym, iszero_0]) 1); qed "neg_imp_number_of_eq_0"; @@ -489,13 +434,13 @@ le_number_of_Suc, le_Suc_number_of]; (* Push int(.) inwards: *) -Addsimps [int_Suc,zadd_int RS sym]; +Addsimps [zadd_int RS sym]; Goal "(m+m = n+n) = (m = (n::int))"; by Auto_tac; val lemma1 = result(); -Goal "m+m ~= int (Suc 0) + n + n"; +Goal "m+m ~= (1::int) + n + n"; by Auto_tac; by (dres_inst_tac [("f", "%x. x mod 2")] arg_cong 1); by (full_simp_tac (simpset() addsimps [zmod_zadd1_eq]) 1); @@ -536,7 +481,7 @@ (*** Further lemmas about "nat" ***) Goal "nat (abs (w * z)) = nat (abs w) * nat (abs z)"; -by (case_tac "z=Numeral0 | w=Numeral0" 1); +by (case_tac "z=0 | w=0" 1); by Auto_tac; by (simp_tac (simpset() addsimps [zabs_def, nat_mult_distrib RS sym, nat_mult_distrib_neg RS sym, zmult_less_0_iff]) 1); diff -r 76401b2ee871 -r 56db9f3a6b3e src/HOL/Integ/nat_simprocs.ML --- a/src/HOL/Integ/nat_simprocs.ML Mon Oct 22 11:01:30 2001 +0200 +++ b/src/HOL/Integ/nat_simprocs.ML Mon Oct 22 11:54:22 2001 +0200 @@ -66,19 +66,19 @@ (** For cancel_numeral_factors **) -Goal "(Numeral0::nat) < k ==> (k*m <= k*n) = (m<=n)"; +Goal "(0::nat) < k ==> (k*m <= k*n) = (m<=n)"; by Auto_tac; qed "nat_mult_le_cancel1"; -Goal "(Numeral0::nat) < k ==> (k*m < k*n) = (m (k*m < k*n) = (m (k*m = k*n) = (m=n)"; +Goal "(0::nat) < k ==> (k*m = k*n) = (m=n)"; by Auto_tac; qed "nat_mult_eq_cancel1"; -Goal "(Numeral0::nat) < k ==> (k*m) div (k*n) = (m div n)"; +Goal "(0::nat) < k ==> (k*m) div (k*n) = (m div n)"; by Auto_tac; qed "nat_mult_div_cancel1"; @@ -105,6 +105,14 @@ structure Nat_Numeral_Simprocs = struct +(*Maps n to #n for n = 0, 1, 2*) +val numeral_syms = + [numeral_0_eq_0 RS sym, numeral_1_eq_1 RS sym, numeral_2_eq_2 RS sym]; +val numeral_sym_ss = HOL_ss addsimps numeral_syms; + +fun rename_numerals th = + simplify numeral_sym_ss (Thm.transfer (the_context ()) th); + (*Utilities*) fun mk_numeral n = HOLogic.number_of_const HOLogic.natT $ HOLogic.mk_bin n; @@ -125,13 +133,13 @@ val zero = mk_numeral 0; val mk_plus = HOLogic.mk_binop "op +"; -(*Thus mk_sum[t] yields t+Numeral0; longer sums don't have a trailing zero*) +(*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*) fun mk_sum [] = zero | mk_sum [t,u] = mk_plus (t, u) | mk_sum (t :: ts) = mk_plus (t, mk_sum ts); (*this version ALWAYS includes a trailing zero*) -fun long_mk_sum [] = zero +fun long_mk_sum [] = HOLogic.zero | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts); val dest_plus = HOLogic.dest_bin "op +" HOLogic.natT; @@ -153,9 +161,8 @@ val trans_tac = Int_Numeral_Simprocs.trans_tac; -val prove_conv = Int_Numeral_Simprocs.prove_conv; - -val bin_simps = [add_nat_number_of, nat_number_of_add_left, +val bin_simps = [numeral_0_eq_0 RS sym, numeral_1_eq_1 RS sym, + add_nat_number_of, nat_number_of_add_left, diff_nat_number_of, le_nat_number_of_eq_not_less, less_nat_number_of, mult_nat_number_of, thm "Let_number_of", nat_number_of] @ @@ -204,14 +211,14 @@ handle TERM _ => find_first_coeff (t::past) u terms; -(*Simplify Numeral1*n and n*Numeral1 to n*) -val add_0s = map rename_numerals [add_0, add_0_right]; +(*Simplify 1*n and n*1 to n*) +val add_0s = map rename_numerals [add_0, add_0_right]; val mult_1s = map rename_numerals [mult_1, mult_1_right]; (*Final simplification: cancel + and *; replace Numeral0 by 0 and Numeral1 by 1*) val simplify_meta_eq = Int_Numeral_Simprocs.simplify_meta_eq - [numeral_0_eq_0, numeral_1_eq_1, add_0, add_0_right, + [numeral_0_eq_0, numeral_1_eq_Suc_0, add_0, add_0_right, mult_0, mult_0_right, mult_1, mult_1_right]; @@ -243,19 +250,19 @@ val find_first_coeff = find_first_coeff [] val trans_tac = trans_tac val norm_tac = ALLGOALS - (simp_tac (HOL_ss addsimps add_0s@mult_1s@ - [add_0, Suc_eq_add_numeral_1]@add_ac)) + (simp_tac (HOL_ss addsimps numeral_syms@add_0s@mult_1s@ + [Suc_eq_add_numeral_1] @ add_ac)) THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@add_ac@mult_ac)) val numeral_simp_tac = ALLGOALS - (simp_tac (HOL_ss addsimps [numeral_0_eq_0 RS sym]@add_0s@bin_simps)) + (simp_tac (HOL_ss addsimps add_0s@bin_simps)) val simplify_meta_eq = simplify_meta_eq end; structure EqCancelNumerals = CancelNumeralsFun (open CancelNumeralsCommon - val prove_conv = prove_conv "nateq_cancel_numerals" + val prove_conv = Bin_Simprocs.prove_conv "nateq_cancel_numerals" val mk_bal = HOLogic.mk_eq val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT val bal_add1 = nat_eq_add_iff1 RS trans @@ -264,7 +271,7 @@ structure LessCancelNumerals = CancelNumeralsFun (open CancelNumeralsCommon - val prove_conv = prove_conv "natless_cancel_numerals" + val prove_conv = Bin_Simprocs.prove_conv "natless_cancel_numerals" val mk_bal = HOLogic.mk_binrel "op <" val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT val bal_add1 = nat_less_add_iff1 RS trans @@ -273,7 +280,7 @@ structure LeCancelNumerals = CancelNumeralsFun (open CancelNumeralsCommon - val prove_conv = prove_conv "natle_cancel_numerals" + val prove_conv = Bin_Simprocs.prove_conv "natle_cancel_numerals" val mk_bal = HOLogic.mk_binrel "op <=" val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT val bal_add1 = nat_le_add_iff1 RS trans @@ -282,7 +289,7 @@ structure DiffCancelNumerals = CancelNumeralsFun (open CancelNumeralsCommon - val prove_conv = prove_conv "natdiff_cancel_numerals" + val prove_conv = Bin_Simprocs.prove_conv "natdiff_cancel_numerals" val mk_bal = HOLogic.mk_binop "op -" val dest_bal = HOLogic.dest_bin "op -" HOLogic.natT val bal_add1 = nat_diff_add_eq1 RS trans @@ -324,16 +331,15 @@ val mk_coeff = mk_coeff val dest_coeff = dest_coeff val left_distrib = left_add_mult_distrib RS trans - val prove_conv = - Int_Numeral_Simprocs.prove_conv_nohyps "nat_combine_numerals" + val prove_conv = Bin_Simprocs.prove_conv_nohyps "nat_combine_numerals" val trans_tac = trans_tac val norm_tac = ALLGOALS - (simp_tac (HOL_ss addsimps add_0s@mult_1s@ - [add_0, Suc_eq_add_numeral_1]@add_ac)) + (simp_tac (HOL_ss addsimps numeral_syms@add_0s@mult_1s@ + [Suc_eq_add_numeral_1] @ add_ac)) THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@add_ac@mult_ac)) val numeral_simp_tac = ALLGOALS - (simp_tac (HOL_ss addsimps [numeral_0_eq_0 RS sym]@add_0s@bin_simps)) + (simp_tac (HOL_ss addsimps add_0s@bin_simps)) val simplify_meta_eq = simplify_meta_eq end; @@ -352,8 +358,8 @@ val mk_coeff = mk_coeff val dest_coeff = dest_coeff val trans_tac = trans_tac - val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps - [Suc_eq_add_numeral_1]@mult_1s)) + val norm_tac = ALLGOALS + (simp_tac (HOL_ss addsimps [Suc_eq_add_numeral_1]@mult_1s)) THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@mult_ac)) val numeral_simp_tac = ALLGOALS (simp_tac (HOL_ss addsimps bin_simps)) val simplify_meta_eq = simplify_meta_eq @@ -361,7 +367,7 @@ structure DivCancelNumeralFactor = CancelNumeralFactorFun (open CancelNumeralFactorCommon - val prove_conv = prove_conv "natdiv_cancel_numeral_factor" + val prove_conv = Bin_Simprocs.prove_conv "natdiv_cancel_numeral_factor" val mk_bal = HOLogic.mk_binop "Divides.op div" val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.natT val cancel = nat_mult_div_cancel1 RS trans @@ -370,7 +376,7 @@ structure EqCancelNumeralFactor = CancelNumeralFactorFun (open CancelNumeralFactorCommon - val prove_conv = prove_conv "nateq_cancel_numeral_factor" + val prove_conv = Bin_Simprocs.prove_conv "nateq_cancel_numeral_factor" val mk_bal = HOLogic.mk_eq val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT val cancel = nat_mult_eq_cancel1 RS trans @@ -379,7 +385,7 @@ structure LessCancelNumeralFactor = CancelNumeralFactorFun (open CancelNumeralFactorCommon - val prove_conv = prove_conv "natless_cancel_numeral_factor" + val prove_conv = Bin_Simprocs.prove_conv "natless_cancel_numeral_factor" val mk_bal = HOLogic.mk_binrel "op <" val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT val cancel = nat_mult_less_cancel1 RS trans @@ -388,7 +394,7 @@ structure LeCancelNumeralFactor = CancelNumeralFactorFun (open CancelNumeralFactorCommon - val prove_conv = prove_conv "natle_cancel_numeral_factor" + val prove_conv = Bin_Simprocs.prove_conv "natle_cancel_numeral_factor" val mk_bal = HOLogic.mk_binrel "op <=" val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT val cancel = nat_mult_le_cancel1 RS trans @@ -443,7 +449,7 @@ structure EqCancelFactor = ExtractCommonTermFun (open CancelFactorCommon - val prove_conv = prove_conv "nat_eq_cancel_factor" + val prove_conv = Bin_Simprocs.prove_conv "nat_eq_cancel_factor" val mk_bal = HOLogic.mk_eq val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT val simplify_meta_eq = cancel_simplify_meta_eq nat_mult_eq_cancel_disj @@ -451,7 +457,7 @@ structure LessCancelFactor = ExtractCommonTermFun (open CancelFactorCommon - val prove_conv = prove_conv "nat_less_cancel_factor" + val prove_conv = Bin_Simprocs.prove_conv "nat_less_cancel_factor" val mk_bal = HOLogic.mk_binrel "op <" val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT val simplify_meta_eq = cancel_simplify_meta_eq nat_mult_less_cancel_disj @@ -459,7 +465,7 @@ structure LeCancelFactor = ExtractCommonTermFun (open CancelFactorCommon - val prove_conv = prove_conv "nat_leq_cancel_factor" + val prove_conv = Bin_Simprocs.prove_conv "nat_leq_cancel_factor" val mk_bal = HOLogic.mk_binrel "op <=" val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT val simplify_meta_eq = cancel_simplify_meta_eq nat_mult_le_cancel_disj @@ -467,7 +473,7 @@ structure DivideCancelFactor = ExtractCommonTermFun (open CancelFactorCommon - val prove_conv = prove_conv "nat_divide_cancel_factor" + val prove_conv = Bin_Simprocs.prove_conv "nat_divide_cancel_factor" val mk_bal = HOLogic.mk_binop "Divides.op div" val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.natT val simplify_meta_eq = cancel_simplify_meta_eq nat_mult_div_cancel_disj @@ -514,7 +520,7 @@ test "Suc u - 2 = y"; test "Suc (Suc (Suc u)) - 2 = y"; test "(i + j + 2 + (k::nat)) - 1 = y"; -test "(i + j + Numeral1 + (k::nat)) - 2 = y"; +test "(i + j + 1 + (k::nat)) - 2 = y"; test "(2*x + (u*v) + y) - v*3*u = (w::nat)"; test "(2*x*u*v + 5 + (u*v)*4 + y) - v*u*4 = (w::nat)"; @@ -590,7 +596,8 @@ (* reduce contradictory <= to False *) val add_rules = - [add_nat_number_of, diff_nat_number_of, mult_nat_number_of, + [thm "Let_number_of", thm "Let_0", thm "Let_1", nat_0, nat_1, + add_nat_number_of, diff_nat_number_of, mult_nat_number_of, eq_nat_number_of, less_nat_number_of, le_nat_number_of_eq_not_less, le_Suc_number_of,le_number_of_Suc, less_Suc_number_of,less_number_of_Suc, @@ -610,7 +617,6 @@ {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = inj_thms, lessD = lessD, simpset = simpset addsimps add_rules - addsimps basic_renamed_arith_simps addsimprocs simprocs})]; end; diff -r 76401b2ee871 -r 56db9f3a6b3e src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Mon Oct 22 11:01:30 2001 +0200 +++ b/src/HOL/Library/Multiset.thy Mon Oct 22 11:54:22 2001 +0200 @@ -274,18 +274,8 @@ apply (simp (no_asm) add: expand_fun_eq) apply (rule conjI) apply force - apply clarify - apply (rule conjI) - apply blast - apply clarify - apply (rule iffI) - apply (rule conjI) - apply clarify - apply (rule conjI) - apply (simp add: eq_sym_conv) (* FIXME blast fails !? *) - apply fast - apply simp - apply force + apply safe + apply (simp_all add: eq_sym_conv) done (* diff -r 76401b2ee871 -r 56db9f3a6b3e src/HOL/List.ML --- a/src/HOL/List.ML Mon Oct 22 11:01:30 2001 +0200 +++ b/src/HOL/List.ML Mon Oct 22 11:54:22 2001 +0200 @@ -232,23 +232,23 @@ local val list_eq_pattern = - Thm.read_cterm (Theory.sign_of (the_context ())) ("(xs::'a list) = ys",HOLogic.boolT); + Thm.read_cterm (Theory.sign_of (the_context ())) ("(xs::'a list) = ys",HOLogic.boolT) fun last (cons as Const("List.list.Cons",_) $ _ $ xs) = (case xs of Const("List.list.Nil",_) => cons | _ => last xs) | last (Const("List.op @",_) $ _ $ ys) = last ys - | last t = t; + | last t = t fun list1 (Const("List.list.Cons",_) $ _ $ Const("List.list.Nil",_)) = true - | list1 _ = false; + | list1 _ = false fun butlast ((cons as Const("List.list.Cons",_) $ x) $ xs) = (case xs of Const("List.list.Nil",_) => xs | _ => cons $ butlast xs) | butlast ((app as Const("List.op @",_) $ xs) $ ys) = app $ butlast ys - | butlast xs = Const("List.list.Nil",fastype_of xs); + | butlast xs = Const("List.list.Nil",fastype_of xs) val rearr_tac = - simp_tac (HOL_basic_ss addsimps [append_assoc,append_Nil,append_Cons]); + simp_tac (HOL_basic_ss addsimps [append_assoc,append_Nil,append_Cons]) fun list_eq sg _ (F as (eq as Const(_,eqT)) $ lhs $ rhs) = let @@ -272,9 +272,9 @@ if lastl aconv lastr then rearr append_same_eq else None - end; + end in -val list_eq_simproc = mk_simproc "list_eq" [list_eq_pattern] list_eq; +val list_eq_simproc = mk_simproc "list_eq" [list_eq_pattern] list_eq end; Addsimprocs [list_eq_simproc]; @@ -1501,24 +1501,19 @@ Addsimps [sublist_upt_eq_take]; -(*** Versions of some theorems above using binary numerals ***) - -AddIffs (map rename_numerals - [length_0_conv, length_greater_0_conv, sum_eq_0_conv]); - -Goal "take n (x#xs) = (if n = Numeral0 then [] else x # take (n - Numeral1) xs)"; +Goal "take n (x#xs) = (if n=0 then [] else x # take (n - 1) xs)"; by (case_tac "n" 1); by (ALLGOALS (asm_simp_tac (simpset() addsimps [numeral_0_eq_0, numeral_1_eq_1]))); qed "take_Cons'"; -Goal "drop n (x#xs) = (if n = Numeral0 then x#xs else drop (n - Numeral1) xs)"; +Goal "drop n (x#xs) = (if n=0 then x#xs else drop (n - 1) xs)"; by (case_tac "n" 1); by (ALLGOALS (asm_simp_tac (simpset() addsimps [numeral_0_eq_0, numeral_1_eq_1]))); qed "drop_Cons'"; -Goal "(x#xs)!n = (if n = Numeral0 then x else xs!(n - Numeral1))"; +Goal "(x#xs)!n = (if n=0 then x else xs!(n - 1))"; by (case_tac "n" 1); by (ALLGOALS (asm_simp_tac (simpset() addsimps [numeral_0_eq_0, numeral_1_eq_1]))); diff -r 76401b2ee871 -r 56db9f3a6b3e src/HOL/Nat.ML --- a/src/HOL/Nat.ML Mon Oct 22 11:01:30 2001 +0200 +++ b/src/HOL/Nat.ML Mon Oct 22 11:54:22 2001 +0200 @@ -243,9 +243,8 @@ by (Auto_tac); qed "add_is_1"; -Goal "(Suc 0 = m+n) = (m=Suc 0 & n=0 | m=0 & n= Suc 0)"; -by (case_tac "m" 1); -by (Auto_tac); +Goal "(Suc 0 = m+n) = (m = Suc 0 & n=0 | m=0 & n = Suc 0)"; +by (rtac ([eq_commute, add_is_1] MRS trans) 1); qed "one_is_add"; Goal "!!m::nat. (0 (0 = x) = (x = 0)"; +Goal "(0 = x) = (x = 0)"; by Auto_tac; qed "zero_reorient"; -Addsimps [zero_reorient]; -(*Polymorphic, not just for "nat"*) -Goal "True ==> (1 = x) = (x = 1)"; +Goal "(1 = x) = (x = 1)"; by Auto_tac; qed "one_reorient"; -Addsimps [one_reorient]; - -Goal "True ==> (Suc (Suc 0) = x) = (x = Suc (Suc 0))"; (* FIXME !? *) -by Auto_tac; -qed "two_reorient"; -Addsimps [two_reorient]; diff -r 76401b2ee871 -r 56db9f3a6b3e src/HOL/NumberTheory/Chinese.thy --- a/src/HOL/NumberTheory/Chinese.thy Mon Oct 22 11:01:30 2001 +0200 +++ b/src/HOL/NumberTheory/Chinese.thy Mon Oct 22 11:54:22 2001 +0200 @@ -45,11 +45,11 @@ defs m_cond_def: "m_cond n mf == - (\i. i \ n --> Numeral0 < mf i) \ - (\i j. i \ n \ j \ n \ i \ j --> zgcd (mf i, mf j) = Numeral1)" + (\i. i \ n --> 0 < mf i) \ + (\i j. i \ n \ j \ n \ i \ j --> zgcd (mf i, mf j) = 1)" km_cond_def: - "km_cond n kf mf == \i. i \ n --> zgcd (kf i, mf i) = Numeral1" + "km_cond n kf mf == \i. i \ n --> zgcd (kf i, mf i) = 1" lincong_sol_def: "lincong_sol n kf bf mf x == \i. i \ n --> zcong (kf i * x) (bf i) (mf i)" @@ -63,8 +63,8 @@ xilin_sol_def: "xilin_sol i n kf bf mf == if 0 < n \ i \ n \ m_cond n mf \ km_cond n kf mf then - (SOME x. Numeral0 \ x \ x < mf i \ zcong (kf i * mhf mf n i * x) (bf i) (mf i)) - else Numeral0" + (SOME x. 0 \ x \ x < mf i \ zcong (kf i * mhf mf n i * x) (bf i) (mf i)) + else 0" x_sol_def: "x_sol n kf bf mf == funsum (\i. xilin_sol i n kf bf mf * mhf mf n i) 0 n" @@ -72,15 +72,15 @@ text {* \medskip @{term funprod} and @{term funsum} *} -lemma funprod_pos: "(\i. i \ n --> Numeral0 < mf i) ==> Numeral0 < funprod mf 0 n" +lemma funprod_pos: "(\i. i \ n --> 0 < mf i) ==> 0 < funprod mf 0 n" apply (induct n) apply auto apply (simp add: int_0_less_mult_iff) done lemma funprod_zgcd [rule_format (no_asm)]: - "(\i. k \ i \ i \ k + l --> zgcd (mf i, mf m) = Numeral1) --> - zgcd (funprod mf k l, mf m) = Numeral1" + "(\i. k \ i \ i \ k + l --> zgcd (mf i, mf m) = 1) --> + zgcd (funprod mf k l, mf m) = 1" apply (induct l) apply simp_all apply (rule impI)+ @@ -110,14 +110,14 @@ done lemma funsum_zero [rule_format (no_asm)]: - "(\i. k \ i \ i \ k + l --> f i = Numeral0) --> (funsum f k l) = Numeral0" + "(\i. k \ i \ i \ k + l --> f i = 0) --> (funsum f k l) = 0" apply (induct l) apply auto done lemma funsum_oneelem [rule_format (no_asm)]: "k \ j --> j \ k + l --> - (\i. k \ i \ i \ k + l \ i \ j --> f i = Numeral0) --> + (\i. k \ i \ i \ k + l \ i \ j --> f i = 0) --> funsum f k l = f j" apply (induct l) prefer 2 @@ -127,9 +127,9 @@ apply (subgoal_tac "k = j") apply (simp_all (no_asm_simp)) apply (case_tac "Suc (k + n) = j") - apply (subgoal_tac "funsum f k n = Numeral0") + apply (subgoal_tac "funsum f k n = 0") apply (rule_tac [2] funsum_zero) - apply (subgoal_tac [3] "f (Suc (k + n)) = Numeral0") + apply (subgoal_tac [3] "f (Suc (k + n)) = 0") apply (subgoal_tac [3] "j \ k + n") prefer 4 apply arith @@ -175,7 +175,7 @@ lemma unique_xi_sol: "0 < n ==> i \ n ==> m_cond n mf ==> km_cond n kf mf - ==> \!x. Numeral0 \ x \ x < mf i \ [kf i * mhf mf n i * x = bf i] (mod mf i)" + ==> \!x. 0 \ x \ x < mf i \ [kf i * mhf mf n i * x = bf i] (mod mf i)" apply (rule zcong_lineq_unique) apply (tactic {* stac (thm "zgcd_zmult_cancel") 2 *}) apply (unfold m_cond_def km_cond_def mhf_def) @@ -227,7 +227,7 @@ lemma chinese_remainder: "0 < n ==> m_cond n mf ==> km_cond n kf mf - ==> \!x. Numeral0 \ x \ x < funprod mf 0 n \ lincong_sol n kf bf mf x" + ==> \!x. 0 \ x \ x < funprod mf 0 n \ lincong_sol n kf bf mf x" apply safe apply (rule_tac [2] m = "funprod mf 0 n" in zcong_zless_imp_eq) apply (rule_tac [6] zcong_funprod) @@ -242,7 +242,7 @@ apply (tactic {* stac (thm "zmod_zmult_distrib" RS sym) 7 *}) apply (tactic {* stac (thm "zcong_zmod" RS sym) 7 *}) apply (subgoal_tac [7] - "Numeral0 \ xilin_sol i n kf bf mf \ xilin_sol i n kf bf mf < mf i + "0 \ xilin_sol i n kf bf mf \ xilin_sol i n kf bf mf < mf i \ [kf i * mhf mf n i * xilin_sol i n kf bf mf = bf i] (mod mf i)") prefer 7 apply (simp add: zmult_ac) diff -r 76401b2ee871 -r 56db9f3a6b3e src/HOL/NumberTheory/EulerFermat.thy --- a/src/HOL/NumberTheory/EulerFermat.thy Mon Oct 22 11:01:30 2001 +0200 +++ b/src/HOL/NumberTheory/EulerFermat.thy Mon Oct 22 11:54:22 2001 +0200 @@ -29,33 +29,33 @@ inductive "RsetR m" intros empty [simp]: "{} \ RsetR m" - insert: "A \ RsetR m ==> zgcd (a, m) = Numeral1 ==> + insert: "A \ RsetR m ==> zgcd (a, m) = 1 ==> \a'. a' \ A --> \ zcong a a' m ==> insert a A \ RsetR m" recdef BnorRset "measure ((\(a, m). nat a) :: int * int => nat)" "BnorRset (a, m) = - (if Numeral0 < a then - let na = BnorRset (a - Numeral1, m) - in (if zgcd (a, m) = Numeral1 then insert a na else na) + (if 0 < a then + let na = BnorRset (a - 1, m) + in (if zgcd (a, m) = 1 then insert a na else na) else {})" defs - norRRset_def: "norRRset m == BnorRset (m - Numeral1, m)" + norRRset_def: "norRRset m == BnorRset (m - 1, m)" noXRRset_def: "noXRRset m x == (\a. a * x) ` norRRset m" phi_def: "phi m == card (norRRset m)" is_RRset_def: "is_RRset A m == A \ RsetR m \ card A = phi m" RRset2norRR_def: "RRset2norRR A m a == - (if Numeral1 < m \ is_RRset A m \ a \ A then + (if 1 < m \ is_RRset A m \ a \ A then SOME b. zcong a b m \ b \ norRRset m - else Numeral0)" + else 0)" constdefs zcongm :: "int => int => int => bool" "zcongm m == \a b. zcong a b m" -lemma abs_eq_1_iff [iff]: "(abs z = (Numeral1::int)) = (z = Numeral1 \ z = -1)" +lemma abs_eq_1_iff [iff]: "(abs z = (1::int)) = (z = 1 \ z = -1)" -- {* LCP: not sure why this lemma is needed now *} apply (auto simp add: zabs_def) done @@ -67,7 +67,7 @@ lemma BnorRset_induct: "(!!a m. P {} a m) ==> - (!!a m. Numeral0 < (a::int) ==> P (BnorRset (a - Numeral1, m::int)) (a - Numeral1) m + (!!a m. 0 < (a::int) ==> P (BnorRset (a - 1, m::int)) (a - 1) m ==> P (BnorRset(a,m)) a m) ==> P (BnorRset(u,v)) u v" proof - @@ -75,7 +75,7 @@ show ?thesis apply (rule BnorRset.induct) apply safe - apply (case_tac [2] "Numeral0 < a") + apply (case_tac [2] "0 < a") apply (rule_tac [2] rule_context) apply simp_all apply (simp_all add: BnorRset.simps rule_context) @@ -94,7 +94,7 @@ apply (auto dest: Bnor_mem_zle) done -lemma Bnor_mem_zg [rule_format]: "b \ BnorRset (a, m) --> Numeral0 < b" +lemma Bnor_mem_zg [rule_format]: "b \ BnorRset (a, m) --> 0 < b" apply (induct a m rule: BnorRset_induct) prefer 2 apply (subst BnorRset.simps) @@ -103,7 +103,7 @@ done lemma Bnor_mem_if [rule_format]: - "zgcd (b, m) = Numeral1 --> Numeral0 < b --> b \ a --> b \ BnorRset (a, m)" + "zgcd (b, m) = 1 --> 0 < b --> b \ a --> b \ BnorRset (a, m)" apply (induct a m rule: BnorRset.induct) apply auto apply (case_tac "a = b") @@ -128,7 +128,7 @@ apply (rule_tac [3] allI) apply (rule_tac [3] impI) apply (rule_tac [3] zcong_not) - apply (subgoal_tac [6] "a' \ a - Numeral1") + apply (subgoal_tac [6] "a' \ a - 1") apply (rule_tac [7] Bnor_mem_zle) apply (rule_tac [5] Bnor_mem_zg) apply auto @@ -142,13 +142,13 @@ apply auto done -lemma aux: "a \ b - Numeral1 ==> a < (b::int)" +lemma aux: "a \ b - 1 ==> a < (b::int)" apply auto done lemma norR_mem_unique: - "Numeral1 < m ==> - zgcd (a, m) = Numeral1 ==> \!b. [a = b] (mod m) \ b \ norRRset m" + "1 < m ==> + zgcd (a, m) = 1 ==> \!b. [a = b] (mod m) \ b \ norRRset m" apply (unfold norRRset_def) apply (cut_tac a = a and m = m in zcong_zless_unique) apply auto @@ -158,7 +158,7 @@ apply (rule_tac "x" = "b" in exI) apply safe apply (rule Bnor_mem_if) - apply (case_tac [2] "b = Numeral0") + apply (case_tac [2] "b = 0") apply (auto intro: order_less_le [THEN iffD2]) prefer 2 apply (simp only: zcong_def) @@ -173,7 +173,7 @@ text {* \medskip @{term noXRRset} *} lemma RRset_gcd [rule_format]: - "is_RRset A m ==> a \ A --> zgcd (a, m) = Numeral1" + "is_RRset A m ==> a \ A --> zgcd (a, m) = 1" apply (unfold is_RRset_def) apply (rule RsetR.induct) apply auto @@ -181,7 +181,7 @@ lemma RsetR_zmult_mono: "A \ RsetR m ==> - Numeral0 < m ==> zgcd (x, m) = Numeral1 ==> (\a. a * x) ` A \ RsetR m" + 0 < m ==> zgcd (x, m) = 1 ==> (\a. a * x) ` A \ RsetR m" apply (erule RsetR.induct) apply simp_all apply (rule RsetR.insert) @@ -191,8 +191,8 @@ done lemma card_nor_eq_noX: - "Numeral0 < m ==> - zgcd (x, m) = Numeral1 ==> card (noXRRset m x) = card (norRRset m)" + "0 < m ==> + zgcd (x, m) = 1 ==> card (noXRRset m x) = card (norRRset m)" apply (unfold norRRset_def noXRRset_def) apply (rule card_image) apply (auto simp add: inj_on_def Bnor_fin) @@ -200,7 +200,7 @@ done lemma noX_is_RRset: - "Numeral0 < m ==> zgcd (x, m) = Numeral1 ==> is_RRset (noXRRset m x) m" + "0 < m ==> zgcd (x, m) = 1 ==> is_RRset (noXRRset m x) m" apply (unfold is_RRset_def phi_def) apply (auto simp add: card_nor_eq_noX) apply (unfold noXRRset_def norRRset_def) @@ -210,7 +210,7 @@ done lemma aux_some: - "Numeral1 < m ==> is_RRset A m ==> a \ A + "1 < m ==> is_RRset A m ==> a \ A ==> zcong a (SOME b. [a = b] (mod m) \ b \ norRRset m) m \ (SOME b. [a = b] (mod m) \ b \ norRRset m) \ norRRset m" apply (rule norR_mem_unique [THEN ex1_implies_ex, THEN someI_ex]) @@ -219,7 +219,7 @@ done lemma RRset2norRR_correct: - "Numeral1 < m ==> is_RRset A m ==> a \ A ==> + "1 < m ==> is_RRset A m ==> a \ A ==> [a = RRset2norRR A m a] (mod m) \ RRset2norRR A m a \ norRRset m" apply (unfold RRset2norRR_def) apply simp @@ -238,7 +238,7 @@ done lemma RRset_zcong_eq [rule_format]: - "Numeral1 < m ==> + "1 < m ==> is_RRset A m ==> [a = b] (mod m) ==> a \ A --> b \ A --> a = b" apply (unfold is_RRset_def) apply (rule RsetR.induct) @@ -252,7 +252,7 @@ done lemma RRset2norRR_inj: - "Numeral1 < m ==> is_RRset A m ==> inj_on (RRset2norRR A m) A" + "1 < m ==> is_RRset A m ==> inj_on (RRset2norRR A m) A" apply (unfold RRset2norRR_def inj_on_def) apply auto apply (subgoal_tac "\b. ([x = b] (mod m) \ b \ norRRset m) \ @@ -267,7 +267,7 @@ done lemma RRset2norRR_eq_norR: - "Numeral1 < m ==> is_RRset A m ==> RRset2norRR A m ` A = norRRset m" + "1 < m ==> is_RRset A m ==> RRset2norRR A m ` A = norRRset m" apply (rule card_seteq) prefer 3 apply (subst card_image) @@ -286,7 +286,7 @@ done lemma Bnor_prod_power [rule_format]: - "x \ Numeral0 ==> a < m --> setprod ((\a. a * x) ` BnorRset (a, m)) = + "x \ 0 ==> a < m --> setprod ((\a. a * x) ` BnorRset (a, m)) = setprod (BnorRset(a, m)) * x^card (BnorRset (a, m))" apply (induct a m rule: BnorRset_induct) prefer 2 @@ -313,7 +313,7 @@ done lemma Bnor_prod_zgcd [rule_format]: - "a < m --> zgcd (setprod (BnorRset (a, m)), m) = Numeral1" + "a < m --> zgcd (setprod (BnorRset (a, m)), m) = 1" apply (induct a m rule: BnorRset_induct) prefer 2 apply (subst BnorRset.simps) @@ -324,12 +324,12 @@ done theorem Euler_Fermat: - "Numeral0 < m ==> zgcd (x, m) = Numeral1 ==> [x^(phi m) = Numeral1] (mod m)" + "0 < m ==> zgcd (x, m) = 1 ==> [x^(phi m) = 1] (mod m)" apply (unfold norRRset_def phi_def) - apply (case_tac "x = Numeral0") - apply (case_tac [2] "m = Numeral1") + apply (case_tac "x = 0") + apply (case_tac [2] "m = 1") apply (rule_tac [3] iffD1) - apply (rule_tac [3] k = "setprod (BnorRset (m - Numeral1, m))" + apply (rule_tac [3] k = "setprod (BnorRset (m - 1, m))" in zcong_cancel2) prefer 5 apply (subst Bnor_prod_power [symmetric]) @@ -352,7 +352,7 @@ lemma Bnor_prime [rule_format (no_asm)]: "p \ zprime ==> - a < p --> (\b. Numeral0 < b \ b \ a --> zgcd (b, p) = Numeral1) + a < p --> (\b. 0 < b \ b \ a --> zgcd (b, p) = 1) --> card (BnorRset (a, p)) = nat a" apply (unfold zprime_def) apply (induct a p rule: BnorRset.induct) @@ -361,7 +361,7 @@ apply auto done -lemma phi_prime: "p \ zprime ==> phi p = nat (p - Numeral1)" +lemma phi_prime: "p \ zprime ==> phi p = nat (p - 1)" apply (unfold phi_def norRRset_def) apply (rule Bnor_prime) apply auto @@ -370,7 +370,7 @@ done theorem Little_Fermat: - "p \ zprime ==> \ p dvd x ==> [x^(nat (p - Numeral1)) = Numeral1] (mod p)" + "p \ zprime ==> \ p dvd x ==> [x^(nat (p - 1)) = 1] (mod p)" apply (subst phi_prime [symmetric]) apply (rule_tac [2] Euler_Fermat) apply (erule_tac [3] zprime_imp_zrelprime) diff -r 76401b2ee871 -r 56db9f3a6b3e src/HOL/NumberTheory/Fib.thy --- a/src/HOL/NumberTheory/Fib.thy Mon Oct 22 11:01:30 2001 +0200 +++ b/src/HOL/NumberTheory/Fib.thy Mon Oct 22 11:54:22 2001 +0200 @@ -67,8 +67,8 @@ *} lemma fib_Cassini: "int (fib (Suc (Suc n)) * fib n) = - (if n mod 2 = 0 then int (fib (Suc n) * fib (Suc n)) - Numeral1 - else int (fib (Suc n) * fib (Suc n)) + Numeral1)" + (if n mod 2 = 0 then int (fib (Suc n) * fib (Suc n)) - 1 + else int (fib (Suc n) * fib (Suc n)) + 1)" apply (induct n rule: fib.induct) apply (simp add: fib.Suc_Suc) apply (simp add: fib.Suc_Suc mod_Suc) diff -r 76401b2ee871 -r 56db9f3a6b3e src/HOL/NumberTheory/IntFact.thy --- a/src/HOL/NumberTheory/IntFact.thy Mon Oct 22 11:01:30 2001 +0200 +++ b/src/HOL/NumberTheory/IntFact.thy Mon Oct 22 11:54:22 2001 +0200 @@ -22,18 +22,18 @@ d22set :: "int => int set" recdef zfact "measure ((\n. nat n) :: int => nat)" - "zfact n = (if n \ Numeral0 then Numeral1 else n * zfact (n - Numeral1))" + "zfact n = (if n \ 0 then 1 else n * zfact (n - 1))" defs - setprod_def: "setprod A == (if finite A then fold (op *) Numeral1 A else Numeral1)" + setprod_def: "setprod A == (if finite A then fold (op *) 1 A else 1)" recdef d22set "measure ((\a. nat a) :: int => nat)" - "d22set a = (if Numeral1 < a then insert a (d22set (a - Numeral1)) else {})" + "d22set a = (if 1 < a then insert a (d22set (a - 1)) else {})" text {* \medskip @{term setprod} --- product of finite set *} -lemma setprod_empty [simp]: "setprod {} = Numeral1" +lemma setprod_empty [simp]: "setprod {} = 1" apply (simp add: setprod_def) done @@ -54,7 +54,7 @@ lemma d22set_induct: "(!!a. P {} a) ==> - (!!a. Numeral1 < (a::int) ==> P (d22set (a - Numeral1)) (a - Numeral1) + (!!a. 1 < (a::int) ==> P (d22set (a - 1)) (a - 1) ==> P (d22set a) a) ==> P (d22set u) u" proof - @@ -62,14 +62,14 @@ show ?thesis apply (rule d22set.induct) apply safe - apply (case_tac [2] "Numeral1 < a") + apply (case_tac [2] "1 < a") apply (rule_tac [2] rule_context) apply (simp_all (no_asm_simp)) apply (simp_all (no_asm_simp) add: d22set.simps rule_context) done qed -lemma d22set_g_1 [rule_format]: "b \ d22set a --> Numeral1 < b" +lemma d22set_g_1 [rule_format]: "b \ d22set a --> 1 < b" apply (induct a rule: d22set_induct) prefer 2 apply (subst d22set.simps) @@ -87,7 +87,7 @@ apply (auto dest: d22set_le) done -lemma d22set_mem [rule_format]: "Numeral1 < b --> b \ a --> b \ d22set a" +lemma d22set_mem [rule_format]: "1 < b --> b \ a --> b \ d22set a" apply (induct a rule: d22set.induct) apply auto apply (simp_all add: d22set.simps) @@ -109,7 +109,7 @@ apply (simp add: d22set.simps zfact.simps) apply (subst d22set.simps) apply (subst zfact.simps) - apply (case_tac "Numeral1 < a") + apply (case_tac "1 < a") prefer 2 apply (simp add: d22set.simps zfact.simps) apply (simp add: d22set_fin d22set_le_swap) diff -r 76401b2ee871 -r 56db9f3a6b3e src/HOL/NumberTheory/IntPrimes.thy --- a/src/HOL/NumberTheory/IntPrimes.thy Mon Oct 22 11:01:30 2001 +0200 +++ b/src/HOL/NumberTheory/IntPrimes.thy Mon Oct 22 11:54:22 2001 +0200 @@ -29,7 +29,7 @@ "measure ((\(m, n, r', r, s', s, t', t). nat r) :: int * int * int * int *int * int * int * int => nat)" "xzgcda (m, n, r', r, s', s, t', t) = - (if r \ Numeral0 then (r', s', t') + (if r \ 0 then (r', s', t') else xzgcda (m, n, r, r' mod r, s, s' - (r' div r) * s, t, t' - (r' div r) * t))" (hints simp: pos_mod_bound) @@ -38,13 +38,13 @@ "zgcd == \(x,y). int (gcd (nat (abs x), nat (abs y)))" defs - xzgcd_def: "xzgcd m n == xzgcda (m, n, m, n, Numeral1, Numeral0, Numeral0, Numeral1)" - zprime_def: "zprime == {p. Numeral1 < p \ (\m. m dvd p --> m = Numeral1 \ m = p)}" + xzgcd_def: "xzgcd m n == xzgcda (m, n, m, n, 1, 0, 0, 1)" + zprime_def: "zprime == {p. 1 < p \ (\m. m dvd p --> m = 1 \ m = p)}" zcong_def: "[a = b] (mod m) == m dvd (a - b)" lemma zabs_eq_iff: - "(abs (z::int) = w) = (z = w \ Numeral0 <= z \ z = -w \ z < Numeral0)" + "(abs (z::int) = w) = (z = w \ 0 <= z \ z = -w \ z < 0)" apply (auto simp add: zabs_def) done @@ -64,17 +64,17 @@ subsection {* Divides relation *} -lemma zdvd_0_right [iff]: "(m::int) dvd Numeral0" +lemma zdvd_0_right [iff]: "(m::int) dvd 0" apply (unfold dvd_def) apply (blast intro: zmult_0_right [symmetric]) done -lemma zdvd_0_left [iff]: "(Numeral0 dvd (m::int)) = (m = Numeral0)" +lemma zdvd_0_left [iff]: "(0 dvd (m::int)) = (m = 0)" apply (unfold dvd_def) apply auto done -lemma zdvd_1_left [iff]: "Numeral1 dvd (m::int)" +lemma zdvd_1_left [iff]: "1 dvd (m::int)" apply (unfold dvd_def) apply simp done @@ -104,7 +104,7 @@ done lemma zdvd_anti_sym: - "Numeral0 < m ==> Numeral0 < n ==> m dvd n ==> n dvd m ==> m = (n::int)" + "0 < m ==> 0 < n ==> m dvd n ==> n dvd m ==> m = (n::int)" apply (unfold dvd_def) apply auto apply (simp add: zmult_assoc zmult_eq_self_iff int_0_less_mult_iff zmult_eq_1_iff) @@ -186,19 +186,19 @@ apply (simp add: zdvd_zadd zdvd_zmult2) done -lemma zdvd_iff_zmod_eq_0: "(k dvd n) = (n mod (k::int) = Numeral0)" +lemma zdvd_iff_zmod_eq_0: "(k dvd n) = (n mod (k::int) = 0)" apply (unfold dvd_def) apply auto done -lemma zdvd_not_zless: "Numeral0 < m ==> m < n ==> \ n dvd (m::int)" +lemma zdvd_not_zless: "0 < m ==> m < n ==> \ n dvd (m::int)" apply (unfold dvd_def) apply auto - apply (subgoal_tac "Numeral0 < n") + apply (subgoal_tac "0 < n") prefer 2 apply (blast intro: zless_trans) apply (simp add: int_0_less_mult_iff) - apply (subgoal_tac "n * k < n * Numeral1") + apply (subgoal_tac "n * k < n * 1") apply (drule zmult_zless_cancel1 [THEN iffD1]) apply auto done @@ -221,7 +221,7 @@ nat_mult_distrib [symmetric] nat_eq_iff2) done -lemma nat_dvd_iff: "(nat z dvd m) = (if Numeral0 \ z then (z dvd int m) else m = 0)" +lemma nat_dvd_iff: "(nat z dvd m) = (if 0 \ z then (z dvd int m) else m = 0)" apply (auto simp add: dvd_def zmult_int [symmetric]) apply (rule_tac x = "nat k" in exI) apply (cut_tac k = m in int_less_0_conv) @@ -245,11 +245,11 @@ subsection {* Euclid's Algorithm and GCD *} -lemma zgcd_0 [simp]: "zgcd (m, Numeral0) = abs m" +lemma zgcd_0 [simp]: "zgcd (m, 0) = abs m" apply (simp add: zgcd_def zabs_def) done -lemma zgcd_0_left [simp]: "zgcd (Numeral0, m) = abs m" +lemma zgcd_0_left [simp]: "zgcd (0, m) = abs m" apply (simp add: zgcd_def zabs_def) done @@ -261,7 +261,7 @@ apply (simp add: zgcd_def) done -lemma zgcd_non_0: "Numeral0 < n ==> zgcd (m, n) = zgcd (n, m mod n)" +lemma zgcd_non_0: "0 < n ==> zgcd (m, n) = zgcd (n, m mod n)" apply (frule_tac b = n and a = m in pos_mod_sign) apply (simp add: zgcd_def zabs_def nat_mod_distrib) apply (cut_tac a = "-m" and b = n in zmod_zminus1_eq_if) @@ -273,17 +273,17 @@ done lemma zgcd_eq: "zgcd (m, n) = zgcd (n, m mod n)" - apply (tactic {* zdiv_undefined_case_tac "n = Numeral0" 1 *}) + apply (tactic {* zdiv_undefined_case_tac "n = 0" 1 *}) apply (auto simp add: linorder_neq_iff zgcd_non_0) apply (cut_tac m = "-m" and n = "-n" in zgcd_non_0) apply auto done -lemma zgcd_1 [simp]: "zgcd (m, Numeral1) = Numeral1" +lemma zgcd_1 [simp]: "zgcd (m, 1) = 1" apply (simp add: zgcd_def zabs_def) done -lemma zgcd_0_1_iff [simp]: "(zgcd (Numeral0, m) = Numeral1) = (abs m = Numeral1)" +lemma zgcd_0_1_iff [simp]: "(zgcd (0, m) = 1) = (abs m = 1)" apply (simp add: zgcd_def zabs_def) done @@ -303,7 +303,7 @@ apply (simp add: zgcd_def gcd_commute) done -lemma zgcd_1_left [simp]: "zgcd (Numeral1, m) = Numeral1" +lemma zgcd_1_left [simp]: "zgcd (1, m) = 1" apply (simp add: zgcd_def gcd_1_left) done @@ -320,7 +320,7 @@ lemmas zgcd_ac = zgcd_assoc zgcd_commute zgcd_left_commute -- {* addition is an AC-operator *} -lemma zgcd_zmult_distrib2: "Numeral0 \ k ==> k * zgcd (m, n) = zgcd (k * m, k * n)" +lemma zgcd_zmult_distrib2: "0 \ k ==> k * zgcd (m, n) = zgcd (k * m, k * n)" apply (simp del: zmult_zminus_right add: zmult_zminus_right [symmetric] nat_mult_distrib zgcd_def zabs_def zmult_less_0_iff gcd_mult_distrib2 [symmetric] zmult_int [symmetric]) @@ -330,29 +330,29 @@ apply (simp add: zabs_def zgcd_zmult_distrib2) done -lemma zgcd_self [simp]: "Numeral0 \ m ==> zgcd (m, m) = m" - apply (cut_tac k = m and m = "Numeral1" and n = "Numeral1" in zgcd_zmult_distrib2) +lemma zgcd_self [simp]: "0 \ m ==> zgcd (m, m) = m" + apply (cut_tac k = m and m = "1" and n = "1" in zgcd_zmult_distrib2) apply simp_all done -lemma zgcd_zmult_eq_self [simp]: "Numeral0 \ k ==> zgcd (k, k * n) = k" - apply (cut_tac k = k and m = "Numeral1" and n = n in zgcd_zmult_distrib2) +lemma zgcd_zmult_eq_self [simp]: "0 \ k ==> zgcd (k, k * n) = k" + apply (cut_tac k = k and m = "1" and n = n in zgcd_zmult_distrib2) apply simp_all done -lemma zgcd_zmult_eq_self2 [simp]: "Numeral0 \ k ==> zgcd (k * n, k) = k" - apply (cut_tac k = k and m = n and n = "Numeral1" in zgcd_zmult_distrib2) +lemma zgcd_zmult_eq_self2 [simp]: "0 \ k ==> zgcd (k * n, k) = k" + apply (cut_tac k = k and m = n and n = "1" in zgcd_zmult_distrib2) apply simp_all done -lemma aux: "zgcd (n, k) = Numeral1 ==> k dvd m * n ==> Numeral0 \ m ==> k dvd m" +lemma aux: "zgcd (n, k) = 1 ==> k dvd m * n ==> 0 \ m ==> k dvd m" apply (subgoal_tac "m = zgcd (m * n, m * k)") apply (erule ssubst, rule zgcd_greatest_iff [THEN iffD2]) apply (simp_all add: zgcd_zmult_distrib2 [symmetric] int_0_le_mult_iff) done -lemma zrelprime_zdvd_zmult: "zgcd (n, k) = Numeral1 ==> k dvd m * n ==> k dvd m" - apply (case_tac "Numeral0 \ m") +lemma zrelprime_zdvd_zmult: "zgcd (n, k) = 1 ==> k dvd m * n ==> k dvd m" + apply (case_tac "0 \ m") apply (blast intro: aux) apply (subgoal_tac "k dvd -m") apply (rule_tac [2] aux) @@ -360,20 +360,20 @@ done lemma zprime_imp_zrelprime: - "p \ zprime ==> \ p dvd n ==> zgcd (n, p) = Numeral1" + "p \ zprime ==> \ p dvd n ==> zgcd (n, p) = 1" apply (unfold zprime_def) apply auto done lemma zless_zprime_imp_zrelprime: - "p \ zprime ==> Numeral0 < n ==> n < p ==> zgcd (n, p) = Numeral1" + "p \ zprime ==> 0 < n ==> n < p ==> zgcd (n, p) = 1" apply (erule zprime_imp_zrelprime) apply (erule zdvd_not_zless) apply assumption done lemma zprime_zdvd_zmult: - "Numeral0 \ (m::int) ==> p \ zprime ==> p dvd m * n ==> p dvd m \ p dvd n" + "0 \ (m::int) ==> p \ zprime ==> p dvd m * n ==> p dvd m \ p dvd n" apply safe apply (rule zrelprime_zdvd_zmult) apply (rule zprime_imp_zrelprime) @@ -392,7 +392,7 @@ done lemma zgcd_zmult_zdvd_zgcd: - "zgcd (k, n) = Numeral1 ==> zgcd (k * m, n) dvd zgcd (m, n)" + "zgcd (k, n) = 1 ==> zgcd (k * m, n) dvd zgcd (m, n)" apply (simp add: zgcd_greatest_iff) apply (rule_tac n = k in zrelprime_zdvd_zmult) prefer 2 @@ -402,16 +402,16 @@ apply (simp (no_asm) add: zgcd_ac) done -lemma zgcd_zmult_cancel: "zgcd (k, n) = Numeral1 ==> zgcd (k * m, n) = zgcd (m, n)" +lemma zgcd_zmult_cancel: "zgcd (k, n) = 1 ==> zgcd (k * m, n) = zgcd (m, n)" apply (simp add: zgcd_def nat_abs_mult_distrib gcd_mult_cancel) done lemma zgcd_zgcd_zmult: - "zgcd (k, m) = Numeral1 ==> zgcd (n, m) = Numeral1 ==> zgcd (k * n, m) = Numeral1" + "zgcd (k, m) = 1 ==> zgcd (n, m) = 1 ==> zgcd (k * n, m) = 1" apply (simp (no_asm_simp) add: zgcd_zmult_cancel) done -lemma zdvd_iff_zgcd: "Numeral0 < m ==> (m dvd n) = (zgcd (n, m) = m)" +lemma zdvd_iff_zgcd: "0 < m ==> (m dvd n) = (zgcd (n, m) = m)" apply safe apply (rule_tac [2] n = "zgcd (n, m)" in zdvd_trans) apply (rule_tac [3] zgcd_zdvd1) @@ -423,7 +423,7 @@ subsection {* Congruences *} -lemma zcong_1 [simp]: "[a = b] (mod Numeral1)" +lemma zcong_1 [simp]: "[a = b] (mod 1)" apply (unfold zcong_def) apply auto done @@ -494,19 +494,19 @@ done lemma zcong_square: - "p \ zprime ==> Numeral0 < a ==> [a * a = Numeral1] (mod p) - ==> [a = Numeral1] (mod p) \ [a = p - Numeral1] (mod p)" + "p \ zprime ==> 0 < a ==> [a * a = 1] (mod p) + ==> [a = 1] (mod p) \ [a = p - 1] (mod p)" apply (unfold zcong_def) apply (rule zprime_zdvd_zmult) - apply (rule_tac [3] s = "a * a - Numeral1 + p * (Numeral1 - a)" in subst) + apply (rule_tac [3] s = "a * a - 1 + p * (1 - a)" in subst) prefer 4 apply (simp add: zdvd_reduce) apply (simp_all add: zdiff_zmult_distrib zmult_commute zdiff_zmult_distrib2) done lemma zcong_cancel: - "Numeral0 \ m ==> - zgcd (k, m) = Numeral1 ==> [a * k = b * k] (mod m) = [a = b] (mod m)" + "0 \ m ==> + zgcd (k, m) = 1 ==> [a * k = b * k] (mod m) = [a = b] (mod m)" apply safe prefer 2 apply (blast intro: zcong_scalar) @@ -523,19 +523,19 @@ done lemma zcong_cancel2: - "Numeral0 \ m ==> - zgcd (k, m) = Numeral1 ==> [k * a = k * b] (mod m) = [a = b] (mod m)" + "0 \ m ==> + zgcd (k, m) = 1 ==> [k * a = k * b] (mod m) = [a = b] (mod m)" apply (simp add: zmult_commute zcong_cancel) done lemma zcong_zgcd_zmult_zmod: - "[a = b] (mod m) ==> [a = b] (mod n) ==> zgcd (m, n) = Numeral1 + "[a = b] (mod m) ==> [a = b] (mod n) ==> zgcd (m, n) = 1 ==> [a = b] (mod m * n)" apply (unfold zcong_def dvd_def) apply auto apply (subgoal_tac "m dvd n * ka") apply (subgoal_tac "m dvd ka") - apply (case_tac [2] "Numeral0 \ ka") + apply (case_tac [2] "0 \ ka") prefer 3 apply (subst zdvd_zminus_iff [symmetric]) apply (rule_tac n = n in zrelprime_zdvd_zmult) @@ -550,8 +550,8 @@ done lemma zcong_zless_imp_eq: - "Numeral0 \ a ==> - a < m ==> Numeral0 \ b ==> b < m ==> [a = b] (mod m) ==> a = b" + "0 \ a ==> + a < m ==> 0 \ b ==> b < m ==> [a = b] (mod m) ==> a = b" apply (unfold zcong_def dvd_def) apply auto apply (drule_tac f = "\z. z mod m" in arg_cong) @@ -566,38 +566,38 @@ done lemma zcong_square_zless: - "p \ zprime ==> Numeral0 < a ==> a < p ==> - [a * a = Numeral1] (mod p) ==> a = Numeral1 \ a = p - Numeral1" + "p \ zprime ==> 0 < a ==> a < p ==> + [a * a = 1] (mod p) ==> a = 1 \ a = p - 1" apply (cut_tac p = p and a = a in zcong_square) apply (simp add: zprime_def) apply (auto intro: zcong_zless_imp_eq) done lemma zcong_not: - "Numeral0 < a ==> a < m ==> Numeral0 < b ==> b < a ==> \ [a = b] (mod m)" + "0 < a ==> a < m ==> 0 < b ==> b < a ==> \ [a = b] (mod m)" apply (unfold zcong_def) apply (rule zdvd_not_zless) apply auto done lemma zcong_zless_0: - "Numeral0 \ a ==> a < m ==> [a = Numeral0] (mod m) ==> a = Numeral0" + "0 \ a ==> a < m ==> [a = 0] (mod m) ==> a = 0" apply (unfold zcong_def dvd_def) apply auto - apply (subgoal_tac "Numeral0 < m") + apply (subgoal_tac "0 < m") apply (rotate_tac -1) apply (simp add: int_0_le_mult_iff) - apply (subgoal_tac "m * k < m * Numeral1") + apply (subgoal_tac "m * k < m * 1") apply (drule zmult_zless_cancel1 [THEN iffD1]) apply (auto simp add: linorder_neq_iff) done lemma zcong_zless_unique: - "Numeral0 < m ==> (\!b. Numeral0 \ b \ b < m \ [a = b] (mod m))" + "0 < m ==> (\!b. 0 \ b \ b < m \ [a = b] (mod m))" apply auto apply (subgoal_tac [2] "[b = y] (mod m)") - apply (case_tac [2] "b = Numeral0") - apply (case_tac [3] "y = Numeral0") + apply (case_tac [2] "b = 0") + apply (case_tac [3] "y = 0") apply (auto intro: zcong_trans zcong_zless_0 zcong_zless_imp_eq order_less_le simp add: zcong_sym) apply (unfold zcong_def dvd_def) @@ -616,8 +616,8 @@ done lemma zgcd_zcong_zgcd: - "Numeral0 < m ==> - zgcd (a, m) = Numeral1 ==> [a = b] (mod m) ==> zgcd (b, m) = Numeral1" + "0 < m ==> + zgcd (a, m) = 1 ==> [a = b] (mod m) ==> zgcd (b, m) = 1" apply (auto simp add: zcong_iff_lin) done @@ -643,7 +643,7 @@ apply (simp add: zadd_commute) done -lemma zcong_zmod_eq: "Numeral0 < m ==> [a = b] (mod m) = (a mod m = b mod m)" +lemma zcong_zmod_eq: "0 < m ==> [a = b] (mod m) = (a mod m = b mod m)" apply auto apply (rule_tac m = m in zcong_zless_imp_eq) prefer 5 @@ -659,13 +659,13 @@ apply (auto simp add: zcong_def) done -lemma zcong_zero [iff]: "[a = b] (mod Numeral0) = (a = b)" +lemma zcong_zero [iff]: "[a = b] (mod 0) = (a = b)" apply (auto simp add: zcong_def) done lemma "[a = b] (mod m) = (a mod m = b mod m)" - apply (tactic {* zdiv_undefined_case_tac "m = Numeral0" 1 *}) - apply (case_tac "Numeral0 < m") + apply (tactic {* zdiv_undefined_case_tac "m = 0" 1 *}) + apply (case_tac "0 < m") apply (simp add: zcong_zmod_eq) apply (rule_tac t = m in zminus_zminus [THEN subst]) apply (subst zcong_zminus) @@ -677,7 +677,7 @@ subsection {* Modulo *} lemma zmod_zdvd_zmod: - "Numeral0 < (m::int) ==> m dvd b ==> (a mod b mod m) = (a mod m)" + "0 < (m::int) ==> m dvd b ==> (a mod b mod m) = (a mod m)" apply (unfold dvd_def) apply auto apply (subst zcong_zmod_eq [symmetric]) @@ -696,14 +696,14 @@ declare xzgcda.simps [simp del] lemma aux1: - "zgcd (r', r) = k --> Numeral0 < r --> + "zgcd (r', r) = k --> 0 < r --> (\sn tn. xzgcda (m, n, r', r, s', s, t', t) = (k, sn, tn))" apply (rule_tac u = m and v = n and w = r' and x = r and y = s' and z = s and aa = t' and ab = t in xzgcda.induct) apply (subst zgcd_eq) apply (subst xzgcda.simps) apply auto - apply (case_tac "r' mod r = Numeral0") + apply (case_tac "r' mod r = 0") prefer 2 apply (frule_tac a = "r'" in pos_mod_sign) apply auto @@ -716,14 +716,14 @@ done lemma aux2: - "(\sn tn. xzgcda (m, n, r', r, s', s, t', t) = (k, sn, tn)) --> Numeral0 < r --> + "(\sn tn. xzgcda (m, n, r', r, s', s, t', t) = (k, sn, tn)) --> 0 < r --> zgcd (r', r) = k" apply (rule_tac u = m and v = n and w = r' and x = r and y = s' and z = s and aa = t' and ab = t in xzgcda.induct) apply (subst zgcd_eq) apply (subst xzgcda.simps) apply (auto simp add: linorder_not_le) - apply (case_tac "r' mod r = Numeral0") + apply (case_tac "r' mod r = 0") prefer 2 apply (frule_tac a = "r'" in pos_mod_sign) apply auto @@ -735,7 +735,7 @@ done lemma xzgcd_correct: - "Numeral0 < n ==> (zgcd (m, n) = k) = (\s t. xzgcd m n = (k, s, t))" + "0 < n ==> (zgcd (m, n) = k) = (\s t. xzgcd m n = (k, s, t))" apply (unfold xzgcd_def) apply (rule iffI) apply (rule_tac [2] aux2 [THEN mp, THEN mp]) @@ -768,17 +768,17 @@ by (rule iffD2 [OF order_less_le conjI]) lemma xzgcda_linear [rule_format]: - "Numeral0 < r --> xzgcda (m, n, r', r, s', s, t', t) = (rn, sn, tn) --> + "0 < r --> xzgcda (m, n, r', r, s', s, t', t) = (rn, sn, tn) --> r' = s' * m + t' * n --> r = s * m + t * n --> rn = sn * m + tn * n" apply (rule_tac u = m and v = n and w = r' and x = r and y = s' and z = s and aa = t' and ab = t in xzgcda.induct) apply (subst xzgcda.simps) apply (simp (no_asm)) apply (rule impI)+ - apply (case_tac "r' mod r = Numeral0") + apply (case_tac "r' mod r = 0") apply (simp add: xzgcda.simps) apply clarify - apply (subgoal_tac "Numeral0 < r' mod r") + apply (subgoal_tac "0 < r' mod r") apply (rule_tac [2] order_le_neq_implies_less) apply (rule_tac [2] pos_mod_sign) apply (cut_tac m = m and n = n and r' = r' and r = r and s' = s' and @@ -787,7 +787,7 @@ done lemma xzgcd_linear: - "Numeral0 < n ==> xzgcd m n = (r, s, t) ==> r = s * m + t * n" + "0 < n ==> xzgcd m n = (r, s, t) ==> r = s * m + t * n" apply (unfold xzgcd_def) apply (erule xzgcda_linear) apply assumption @@ -795,7 +795,7 @@ done lemma zgcd_ex_linear: - "Numeral0 < n ==> zgcd (m, n) = k ==> (\s t. k = s * m + t * n)" + "0 < n ==> zgcd (m, n) = k ==> (\s t. k = s * m + t * n)" apply (simp add: xzgcd_correct) apply safe apply (rule exI)+ @@ -804,8 +804,8 @@ done lemma zcong_lineq_ex: - "Numeral0 < n ==> zgcd (a, n) = Numeral1 ==> \x. [a * x = Numeral1] (mod n)" - apply (cut_tac m = a and n = n and k = "Numeral1" in zgcd_ex_linear) + "0 < n ==> zgcd (a, n) = 1 ==> \x. [a * x = 1] (mod n)" + apply (cut_tac m = a and n = n and k = "1" in zgcd_ex_linear) apply safe apply (rule_tac x = s in exI) apply (rule_tac b = "s * a + t * n" in zcong_trans) @@ -816,8 +816,8 @@ done lemma zcong_lineq_unique: - "Numeral0 < n ==> - zgcd (a, n) = Numeral1 ==> \!x. Numeral0 \ x \ x < n \ [a * x = b] (mod n)" + "0 < n ==> + zgcd (a, n) = 1 ==> \!x. 0 \ x \ x < n \ [a * x = b] (mod n)" apply auto apply (rule_tac [2] zcong_zless_imp_eq) apply (tactic {* stac (thm "zcong_cancel2" RS sym) 6 *}) @@ -833,7 +833,7 @@ apply (subst zcong_zmod) apply (subst zmod_zmult1_eq [symmetric]) apply (subst zcong_zmod [symmetric]) - apply (subgoal_tac "[a * x * b = Numeral1 * b] (mod n)") + apply (subgoal_tac "[a * x * b = 1 * b] (mod n)") apply (rule_tac [2] zcong_zmult) apply (simp_all add: zmult_assoc) done diff -r 76401b2ee871 -r 56db9f3a6b3e src/HOL/NumberTheory/WilsonBij.thy --- a/src/HOL/NumberTheory/WilsonBij.thy Mon Oct 22 11:01:30 2001 +0200 +++ b/src/HOL/NumberTheory/WilsonBij.thy Mon Oct 22 11:54:22 2001 +0200 @@ -20,19 +20,19 @@ constdefs reciR :: "int => int => int => bool" "reciR p == - \a b. zcong (a * b) Numeral1 p \ Numeral1 < a \ a < p - Numeral1 \ Numeral1 < b \ b < p - Numeral1" + \a b. zcong (a * b) 1 p \ 1 < a \ a < p - 1 \ 1 < b \ b < p - 1" inv :: "int => int => int" "inv p a == - if p \ zprime \ Numeral0 < a \ a < p then - (SOME x. Numeral0 \ x \ x < p \ zcong (a * x) Numeral1 p) - else Numeral0" + if p \ zprime \ 0 < a \ a < p then + (SOME x. 0 \ x \ x < p \ zcong (a * x) 1 p) + else 0" text {* \medskip Inverse *} lemma inv_correct: - "p \ zprime ==> Numeral0 < a ==> a < p - ==> Numeral0 \ inv p a \ inv p a < p \ [a * inv p a = Numeral1] (mod p)" + "p \ zprime ==> 0 < a ==> a < p + ==> 0 \ inv p a \ inv p a < p \ [a * inv p a = 1] (mod p)" apply (unfold inv_def) apply (simp (no_asm_simp)) apply (rule zcong_lineq_unique [THEN ex1_implies_ex, THEN someI_ex]) @@ -46,53 +46,53 @@ lemmas inv_is_inv = inv_correct [THEN conjunct2, THEN conjunct2, standard] lemma inv_not_0: - "p \ zprime ==> Numeral1 < a ==> a < p - Numeral1 ==> inv p a \ Numeral0" + "p \ zprime ==> 1 < a ==> a < p - 1 ==> inv p a \ 0" -- {* same as @{text WilsonRuss} *} apply safe apply (cut_tac a = a and p = p in inv_is_inv) apply (unfold zcong_def) apply auto - apply (subgoal_tac "\ p dvd Numeral1") + apply (subgoal_tac "\ p dvd 1") apply (rule_tac [2] zdvd_not_zless) - apply (subgoal_tac "p dvd Numeral1") + apply (subgoal_tac "p dvd 1") prefer 2 apply (subst zdvd_zminus_iff [symmetric]) apply auto done lemma inv_not_1: - "p \ zprime ==> Numeral1 < a ==> a < p - Numeral1 ==> inv p a \ Numeral1" + "p \ zprime ==> 1 < a ==> a < p - 1 ==> inv p a \ 1" -- {* same as @{text WilsonRuss} *} apply safe apply (cut_tac a = a and p = p in inv_is_inv) prefer 4 apply simp - apply (subgoal_tac "a = Numeral1") + apply (subgoal_tac "a = 1") apply (rule_tac [2] zcong_zless_imp_eq) apply auto done -lemma aux: "[a * (p - Numeral1) = Numeral1] (mod p) = [a = p - Numeral1] (mod p)" +lemma aux: "[a * (p - 1) = 1] (mod p) = [a = p - 1] (mod p)" -- {* same as @{text WilsonRuss} *} apply (unfold zcong_def) apply (simp add: zdiff_zdiff_eq zdiff_zdiff_eq2 zdiff_zmult_distrib2) - apply (rule_tac s = "p dvd -((a + Numeral1) + (p * -a))" in trans) + apply (rule_tac s = "p dvd -((a + 1) + (p * -a))" in trans) apply (simp add: zmult_commute zminus_zdiff_eq) apply (subst zdvd_zminus_iff) apply (subst zdvd_reduce) - apply (rule_tac s = "p dvd (a + Numeral1) + (p * -Numeral1)" in trans) + apply (rule_tac s = "p dvd (a + 1) + (p * -1)" in trans) apply (subst zdvd_reduce) apply auto done lemma inv_not_p_minus_1: - "p \ zprime ==> Numeral1 < a ==> a < p - Numeral1 ==> inv p a \ p - Numeral1" + "p \ zprime ==> 1 < a ==> a < p - 1 ==> inv p a \ p - 1" -- {* same as @{text WilsonRuss} *} apply safe apply (cut_tac a = a and p = p in inv_is_inv) apply auto apply (simp add: aux) - apply (subgoal_tac "a = p - Numeral1") + apply (subgoal_tac "a = p - 1") apply (rule_tac [2] zcong_zless_imp_eq) apply auto done @@ -102,9 +102,9 @@ but use ``@{text correct}'' theorems. *} -lemma inv_g_1: "p \ zprime ==> Numeral1 < a ==> a < p - Numeral1 ==> Numeral1 < inv p a" - apply (subgoal_tac "inv p a \ Numeral1") - apply (subgoal_tac "inv p a \ Numeral0") +lemma inv_g_1: "p \ zprime ==> 1 < a ==> a < p - 1 ==> 1 < inv p a" + apply (subgoal_tac "inv p a \ 1") + apply (subgoal_tac "inv p a \ 0") apply (subst order_less_le) apply (subst zle_add1_eq_le [symmetric]) apply (subst order_less_le) @@ -116,7 +116,7 @@ done lemma inv_less_p_minus_1: - "p \ zprime ==> Numeral1 < a ==> a < p - Numeral1 ==> inv p a < p - Numeral1" + "p \ zprime ==> 1 < a ==> a < p - 1 ==> inv p a < p - 1" -- {* ditto *} apply (subst order_less_le) apply (simp add: inv_not_p_minus_1 inv_less) @@ -125,11 +125,11 @@ text {* \medskip Bijection *} -lemma aux1: "Numeral1 < x ==> Numeral0 \ (x::int)" +lemma aux1: "1 < x ==> 0 \ (x::int)" apply auto done -lemma aux2: "Numeral1 < x ==> Numeral0 < (x::int)" +lemma aux2: "1 < x ==> 0 < (x::int)" apply auto done @@ -137,7 +137,7 @@ apply auto done -lemma aux4: "x \ p - 2 ==> x < (p::int)-Numeral1" +lemma aux4: "x \ p - 2 ==> x < (p::int) - 1" apply auto done @@ -167,7 +167,7 @@ apply auto apply (rule d22set_mem) apply (erule inv_g_1) - apply (subgoal_tac [3] "inv p xa < p - Numeral1") + apply (subgoal_tac [3] "inv p xa < p - 1") apply (erule_tac [4] inv_less_p_minus_1) apply (auto intro: d22set_g_1 d22set_le aux4) done @@ -229,28 +229,28 @@ subsection {* Wilson *} lemma bijER_zcong_prod_1: - "p \ zprime ==> A \ bijER (reciR p) ==> [setprod A = Numeral1] (mod p)" + "p \ zprime ==> A \ bijER (reciR p) ==> [setprod A = 1] (mod p)" apply (unfold reciR_def) apply (erule bijER.induct) - apply (subgoal_tac [2] "a = Numeral1 \ a = p - Numeral1") + apply (subgoal_tac [2] "a = 1 \ a = p - 1") apply (rule_tac [3] zcong_square_zless) apply auto apply (subst setprod_insert) prefer 3 apply (subst setprod_insert) apply (auto simp add: fin_bijER) - apply (subgoal_tac "zcong ((a * b) * setprod A) (Numeral1 * Numeral1) p") + apply (subgoal_tac "zcong ((a * b) * setprod A) (1 * 1) p") apply (simp add: zmult_assoc) apply (rule zcong_zmult) apply auto done -theorem Wilson_Bij: "p \ zprime ==> [zfact (p - Numeral1) = -1] (mod p)" - apply (subgoal_tac "zcong ((p - Numeral1) * zfact (p - 2)) (-1 * Numeral1) p") +theorem Wilson_Bij: "p \ zprime ==> [zfact (p - 1) = -1] (mod p)" + apply (subgoal_tac "zcong ((p - 1) * zfact (p - 2)) (-1 * 1) p") apply (rule_tac [2] zcong_zmult) apply (simp add: zprime_def) apply (subst zfact.simps) - apply (rule_tac t = "p - Numeral1 - Numeral1" and s = "p - 2" in subst) + apply (rule_tac t = "p - 1 - 1" and s = "p - 2" in subst) apply auto apply (simp add: zcong_def) apply (subst d22set_prod_zfact [symmetric]) diff -r 76401b2ee871 -r 56db9f3a6b3e src/HOL/NumberTheory/WilsonRuss.thy --- a/src/HOL/NumberTheory/WilsonRuss.thy Mon Oct 22 11:01:30 2001 +0200 +++ b/src/HOL/NumberTheory/WilsonRuss.thy Mon Oct 22 11:54:22 2001 +0200 @@ -25,20 +25,20 @@ recdef wset "measure ((\(a, p). nat a) :: int * int => nat)" "wset (a, p) = - (if Numeral1 < a then - let ws = wset (a - Numeral1, p) + (if 1 < a then + let ws = wset (a - 1, p) in (if a \ ws then ws else insert a (insert (inv p a) ws)) else {})" text {* \medskip @{term [source] inv} *} -lemma aux: "Numeral1 < m ==> Suc (nat (m - 2)) = nat (m - Numeral1)" +lemma aux: "1 < m ==> Suc (nat (m - 2)) = nat (m - 1)" apply (subst int_int_eq [symmetric]) apply auto done lemma inv_is_inv: - "p \ zprime \ Numeral0 < a \ a < p ==> [a * inv p a = Numeral1] (mod p)" + "p \ zprime \ 0 < a \ a < p ==> [a * inv p a = 1] (mod p)" apply (unfold inv_def) apply (subst zcong_zmod) apply (subst zmod_zmult1_eq [symmetric]) @@ -52,71 +52,71 @@ done lemma inv_distinct: - "p \ zprime \ Numeral1 < a \ a < p - Numeral1 ==> a \ inv p a" + "p \ zprime \ 1 < a \ a < p - 1 ==> a \ inv p a" apply safe apply (cut_tac a = a and p = p in zcong_square) apply (cut_tac [3] a = a and p = p in inv_is_inv) apply auto - apply (subgoal_tac "a = Numeral1") + apply (subgoal_tac "a = 1") apply (rule_tac [2] m = p in zcong_zless_imp_eq) - apply (subgoal_tac [7] "a = p - Numeral1") + apply (subgoal_tac [7] "a = p - 1") apply (rule_tac [8] m = p in zcong_zless_imp_eq) apply auto done lemma inv_not_0: - "p \ zprime \ Numeral1 < a \ a < p - Numeral1 ==> inv p a \ Numeral0" + "p \ zprime \ 1 < a \ a < p - 1 ==> inv p a \ 0" apply safe apply (cut_tac a = a and p = p in inv_is_inv) apply (unfold zcong_def) apply auto - apply (subgoal_tac "\ p dvd Numeral1") + apply (subgoal_tac "\ p dvd 1") apply (rule_tac [2] zdvd_not_zless) - apply (subgoal_tac "p dvd Numeral1") + apply (subgoal_tac "p dvd 1") prefer 2 apply (subst zdvd_zminus_iff [symmetric]) apply auto done lemma inv_not_1: - "p \ zprime \ Numeral1 < a \ a < p - Numeral1 ==> inv p a \ Numeral1" + "p \ zprime \ 1 < a \ a < p - 1 ==> inv p a \ 1" apply safe apply (cut_tac a = a and p = p in inv_is_inv) prefer 4 apply simp - apply (subgoal_tac "a = Numeral1") + apply (subgoal_tac "a = 1") apply (rule_tac [2] zcong_zless_imp_eq) apply auto done -lemma aux: "[a * (p - Numeral1) = Numeral1] (mod p) = [a = p - Numeral1] (mod p)" +lemma aux: "[a * (p - 1) = 1] (mod p) = [a = p - 1] (mod p)" apply (unfold zcong_def) apply (simp add: zdiff_zdiff_eq zdiff_zdiff_eq2 zdiff_zmult_distrib2) - apply (rule_tac s = "p dvd -((a + Numeral1) + (p * -a))" in trans) + apply (rule_tac s = "p dvd -((a + 1) + (p * -a))" in trans) apply (simp add: zmult_commute zminus_zdiff_eq) apply (subst zdvd_zminus_iff) apply (subst zdvd_reduce) - apply (rule_tac s = "p dvd (a + Numeral1) + (p * -Numeral1)" in trans) + apply (rule_tac s = "p dvd (a + 1) + (p * -1)" in trans) apply (subst zdvd_reduce) apply auto done lemma inv_not_p_minus_1: - "p \ zprime \ Numeral1 < a \ a < p - Numeral1 ==> inv p a \ p - Numeral1" + "p \ zprime \ 1 < a \ a < p - 1 ==> inv p a \ p - 1" apply safe apply (cut_tac a = a and p = p in inv_is_inv) apply auto apply (simp add: aux) - apply (subgoal_tac "a = p - Numeral1") + apply (subgoal_tac "a = p - 1") apply (rule_tac [2] zcong_zless_imp_eq) apply auto done lemma inv_g_1: - "p \ zprime \ Numeral1 < a \ a < p - Numeral1 ==> Numeral1 < inv p a" - apply (case_tac "Numeral0\ inv p a") - apply (subgoal_tac "inv p a \ Numeral1") - apply (subgoal_tac "inv p a \ Numeral0") + "p \ zprime \ 1 < a \ a < p - 1 ==> 1 < inv p a" + apply (case_tac "0\ inv p a") + apply (subgoal_tac "inv p a \ 1") + apply (subgoal_tac "inv p a \ 0") apply (subst order_less_le) apply (subst zle_add1_eq_le [symmetric]) apply (subst order_less_le) @@ -128,7 +128,7 @@ done lemma inv_less_p_minus_1: - "p \ zprime \ Numeral1 < a \ a < p - Numeral1 ==> inv p a < p - Numeral1" + "p \ zprime \ 1 < a \ a < p - 1 ==> inv p a < p - 1" apply (case_tac "inv p a < p") apply (subst order_less_le) apply (simp add: inv_not_p_minus_1) @@ -138,23 +138,23 @@ done lemma aux: "5 \ p ==> - nat (p - 2) * nat (p - 2) = Suc (nat (p - Numeral1) * nat (p - 3))" + nat (p - 2) * nat (p - 2) = Suc (nat (p - 1) * nat (p - 3))" apply (subst int_int_eq [symmetric]) apply (simp add: zmult_int [symmetric]) apply (simp add: zdiff_zmult_distrib zdiff_zmult_distrib2) done lemma zcong_zpower_zmult: - "[x^y = Numeral1] (mod p) \ [x^(y * z) = Numeral1] (mod p)" + "[x^y = 1] (mod p) \ [x^(y * z) = 1] (mod p)" apply (induct z) apply (auto simp add: zpower_zadd_distrib) - apply (subgoal_tac "zcong (x^y * x^(y * n)) (Numeral1 * Numeral1) p") + apply (subgoal_tac "zcong (x^y * x^(y * n)) (1 * 1) p") apply (rule_tac [2] zcong_zmult) apply simp_all done lemma inv_inv: "p \ zprime \ - 5 \ p \ Numeral0 < a \ a < p ==> inv p (inv p a) = a" + 5 \ p \ 0 < a \ a < p ==> inv p (inv p a) = a" apply (unfold inv_def) apply (subst zpower_zmod) apply (subst zpower_zpower) @@ -165,7 +165,7 @@ apply (subst zcong_zmod [symmetric]) apply (subst aux) apply (subgoal_tac [2] - "zcong (a * a^(nat (p - Numeral1) * nat (p - 3))) (a * Numeral1) p") + "zcong (a * a^(nat (p - 1) * nat (p - 3))) (a * 1) p") apply (rule_tac [3] zcong_zmult) apply (rule_tac [4] zcong_zpower_zmult) apply (erule_tac [4] Little_Fermat) @@ -180,7 +180,7 @@ lemma wset_induct: "(!!a p. P {} a p) \ - (!!a p. Numeral1 < (a::int) \ P (wset (a - Numeral1, p)) (a - Numeral1) p + (!!a p. 1 < (a::int) \ P (wset (a - 1, p)) (a - 1) p ==> P (wset (a, p)) a p) ==> P (wset (u, v)) u v" proof - @@ -188,7 +188,7 @@ show ?thesis apply (rule wset.induct) apply safe - apply (case_tac [2] "Numeral1 < a") + apply (case_tac [2] "1 < a") apply (rule_tac [2] rule_context) apply simp_all apply (simp_all add: wset.simps rule_context) @@ -196,27 +196,27 @@ qed lemma wset_mem_imp_or [rule_format]: - "Numeral1 < a \ b \ wset (a - Numeral1, p) + "1 < a \ b \ wset (a - 1, p) ==> b \ wset (a, p) --> b = a \ b = inv p a" apply (subst wset.simps) apply (unfold Let_def) apply simp done -lemma wset_mem_mem [simp]: "Numeral1 < a ==> a \ wset (a, p)" +lemma wset_mem_mem [simp]: "1 < a ==> a \ wset (a, p)" apply (subst wset.simps) apply (unfold Let_def) apply simp done -lemma wset_subset: "Numeral1 < a \ b \ wset (a - Numeral1, p) ==> b \ wset (a, p)" +lemma wset_subset: "1 < a \ b \ wset (a - 1, p) ==> b \ wset (a, p)" apply (subst wset.simps) apply (unfold Let_def) apply auto done lemma wset_g_1 [rule_format]: - "p \ zprime --> a < p - Numeral1 --> b \ wset (a, p) --> Numeral1 < b" + "p \ zprime --> a < p - 1 --> b \ wset (a, p) --> 1 < b" apply (induct a p rule: wset_induct) apply auto apply (case_tac "b = a") @@ -230,7 +230,7 @@ done lemma wset_less [rule_format]: - "p \ zprime --> a < p - Numeral1 --> b \ wset (a, p) --> b < p - Numeral1" + "p \ zprime --> a < p - 1 --> b \ wset (a, p) --> b < p - 1" apply (induct a p rule: wset_induct) apply auto apply (case_tac "b = a") @@ -245,7 +245,7 @@ lemma wset_mem [rule_format]: "p \ zprime --> - a < p - Numeral1 --> Numeral1 < b --> b \ a --> b \ wset (a, p)" + a < p - 1 --> 1 < b --> b \ a --> b \ wset (a, p)" apply (induct a p rule: wset.induct) apply auto apply (subgoal_tac "b = a") @@ -256,7 +256,7 @@ done lemma wset_mem_inv_mem [rule_format]: - "p \ zprime --> 5 \ p --> a < p - Numeral1 --> b \ wset (a, p) + "p \ zprime --> 5 \ p --> a < p - 1 --> b \ wset (a, p) --> inv p b \ wset (a, p)" apply (induct a p rule: wset_induct) apply auto @@ -274,7 +274,7 @@ done lemma wset_inv_mem_mem: - "p \ zprime \ 5 \ p \ a < p - Numeral1 \ Numeral1 < b \ b < p - Numeral1 + "p \ zprime \ 5 \ p \ a < p - 1 \ 1 < b \ b < p - 1 \ inv p b \ wset (a, p) \ b \ wset (a, p)" apply (rule_tac s = "inv p (inv p b)" and t = b in subst) apply (rule_tac [2] wset_mem_inv_mem) @@ -292,7 +292,7 @@ lemma wset_zcong_prod_1 [rule_format]: "p \ zprime --> - 5 \ p --> a < p - Numeral1 --> [setprod (wset (a, p)) = Numeral1] (mod p)" + 5 \ p --> a < p - 1 --> [setprod (wset (a, p)) = 1] (mod p)" apply (induct a p rule: wset_induct) prefer 2 apply (subst wset.simps) @@ -301,13 +301,13 @@ apply (subst setprod_insert) apply (tactic {* stac (thm "setprod_insert") 3 *}) apply (subgoal_tac [5] - "zcong (a * inv p a * setprod (wset (a - Numeral1, p))) (Numeral1 * Numeral1) p") + "zcong (a * inv p a * setprod (wset (a - 1, p))) (1 * 1) p") prefer 5 apply (simp add: zmult_assoc) apply (rule_tac [5] zcong_zmult) apply (rule_tac [5] inv_is_inv) apply (tactic "Clarify_tac 4") - apply (subgoal_tac [4] "a \ wset (a - Numeral1, p)") + apply (subgoal_tac [4] "a \ wset (a - 1, p)") apply (rule_tac [5] wset_inv_mem_mem) apply (simp_all add: wset_fin) apply (rule inv_distinct) @@ -323,7 +323,7 @@ apply (erule_tac [4] wset_g_1) prefer 6 apply (subst zle_add1_eq_le [symmetric]) - apply (subgoal_tac "p - 2 + Numeral1 = p - Numeral1") + apply (subgoal_tac "p - 2 + 1 = p - 1") apply (simp (no_asm_simp)) apply (erule wset_less) apply auto @@ -348,12 +348,12 @@ done theorem Wilson_Russ: - "p \ zprime ==> [zfact (p - Numeral1) = -1] (mod p)" - apply (subgoal_tac "[(p - Numeral1) * zfact (p - 2) = -1 * Numeral1] (mod p)") + "p \ zprime ==> [zfact (p - 1) = -1] (mod p)" + apply (subgoal_tac "[(p - 1) * zfact (p - 2) = -1 * 1] (mod p)") apply (rule_tac [2] zcong_zmult) apply (simp only: zprime_def) apply (subst zfact.simps) - apply (rule_tac t = "p - Numeral1 - Numeral1" and s = "p - 2" in subst) + apply (rule_tac t = "p - 1 - 1" and s = "p - 2" in subst) apply auto apply (simp only: zcong_def) apply (simp (no_asm_simp)) diff -r 76401b2ee871 -r 56db9f3a6b3e src/HOL/Numeral.thy --- a/src/HOL/Numeral.thy Mon Oct 22 11:01:30 2001 +0200 +++ b/src/HOL/Numeral.thy Mon Oct 22 11:54:22 2001 +0200 @@ -40,10 +40,10 @@ lemma Let_number_of [simp]: "Let (number_of v) f == f (number_of v)" by (simp add: Let_def) -(*The condition "True" is a hack to prevent looping. - Conditional rewrite rules are tried after unconditional ones, so a rule - like eq_nat_number_of will be tried first to eliminate #mm=#nn. *) -lemma number_of_reorient [simp]: "True ==> (number_of w = x) = (x = number_of w)" - by auto +lemma Let_0 [simp]: "Let 0 f == f 0" + by (simp add: Let_def) + +lemma Let_1 [simp]: "Let 1 f == f 1" + by (simp add: Let_def) end diff -r 76401b2ee871 -r 56db9f3a6b3e src/HOL/ROOT.ML --- a/src/HOL/ROOT.ML Mon Oct 22 11:01:30 2001 +0200 +++ b/src/HOL/ROOT.ML Mon Oct 22 11:54:22 2001 +0200 @@ -29,6 +29,7 @@ use "~~/src/Provers/Arith/abel_cancel.ML"; use "~~/src/Provers/Arith/assoc_fold.ML"; use "~~/src/Provers/quantifier1.ML"; +use "~~/src/Provers/Arith/abstract_numerals.ML"; use "~~/src/Provers/Arith/cancel_numerals.ML"; use "~~/src/Provers/Arith/combine_numerals.ML"; use "~~/src/Provers/Arith/cancel_numeral_factor.ML"; diff -r 76401b2ee871 -r 56db9f3a6b3e src/HOL/Real/ex/Sqrt_Irrational.thy --- a/src/HOL/Real/ex/Sqrt_Irrational.thy Mon Oct 22 11:01:30 2001 +0200 +++ b/src/HOL/Real/ex/Sqrt_Irrational.thy Mon Oct 22 11:54:22 2001 +0200 @@ -119,7 +119,7 @@ { fix m :: nat assume dvd: "m dvd 2" hence "m \ 2" by (simp add: dvd_imp_le) - moreover from dvd have "m \ 0" by (auto dest: dvd_0_left iff del: neq0_conv) + moreover from dvd have "m \ 0" by (auto iff del: neq0_conv) ultimately have "m = 1 \ m = 2" by arith } thus "2 \ prime" by (simp add: prime_def) diff -r 76401b2ee871 -r 56db9f3a6b3e src/HOL/SVC_Oracle.ML --- a/src/HOL/SVC_Oracle.ML Mon Oct 22 11:01:30 2001 +0200 +++ b/src/HOL/SVC_Oracle.ML Mon Oct 22 11:54:22 2001 +0200 @@ -41,30 +41,29 @@ | _ => (case gen_assoc Pattern.aeconv (!pairs, t) of Some v => v | None => insert t) + (*abstraction of a numeric literal*) + fun lit (t as Const("0", _)) = t + | lit (t as Const("1", _)) = t + | lit (t as Const("Numeral.number_of", _) $ w) = t + | lit t = replace t (*abstraction of a real/rational expression*) fun rat ((c as Const("op +", _)) $ x $ y) = c $ (rat x) $ (rat y) | rat ((c as Const("op -", _)) $ x $ y) = c $ (rat x) $ (rat y) | rat ((c as Const("op /", _)) $ x $ y) = c $ (rat x) $ (rat y) | rat ((c as Const("op *", _)) $ x $ y) = c $ (rat x) $ (rat y) | rat ((c as Const("uminus", _)) $ x) = c $ (rat x) - | rat ((c as Const("0", _))) = c - | rat ((c as Const("1", _))) = c - | rat (t as Const("Numeral.number_of", _) $ w) = t - | rat t = replace t + | rat t = lit t (*abstraction of an integer expression: no div, mod*) fun int ((c as Const("op +", _)) $ x $ y) = c $ (int x) $ (int y) | int ((c as Const("op -", _)) $ x $ y) = c $ (int x) $ (int y) | int ((c as Const("op *", _)) $ x $ y) = c $ (int x) $ (int y) | int ((c as Const("uminus", _)) $ x) = c $ (int x) - | int (t as Const("Numeral.number_of", _) $ w) = t - | int t = replace t + | int t = lit t (*abstraction of a natural number expression: no minus*) fun nat ((c as Const("op +", _)) $ x $ y) = c $ (nat x) $ (nat y) | nat ((c as Const("op *", _)) $ x $ y) = c $ (nat x) $ (nat y) | nat ((c as Const("Suc", _)) $ x) = c $ (nat x) - | nat (t as Const("0", _)) = t - | nat (t as Const("Numeral.number_of", _) $ w) = t - | nat t = replace t + | nat t = lit t (*abstraction of a relation: =, <, <=*) fun rel (T, c $ x $ y) = if T = HOLogic.realT then c $ (rat x) $ (rat y) diff -r 76401b2ee871 -r 56db9f3a6b3e src/HOL/UNITY/Comp/Counter.ML --- a/src/HOL/UNITY/Comp/Counter.ML Mon Oct 22 11:01:30 2001 +0200 +++ b/src/HOL/UNITY/Comp/Counter.ML Mon Oct 22 11:54:22 2001 +0200 @@ -100,7 +100,7 @@ (* Compositional Proof *) -Goal "(ALL i. i < I --> s (c i) = Numeral0) --> sum I s = Numeral0"; +Goal "(ALL i. i < I --> s (c i) = 0) --> sum I s = 0"; by (induct_tac "I" 1); by Auto_tac; qed "sum_0'"; diff -r 76401b2ee871 -r 56db9f3a6b3e src/HOL/UNITY/Comp/Counter.thy --- a/src/HOL/UNITY/Comp/Counter.thy Mon Oct 22 11:01:30 2001 +0200 +++ b/src/HOL/UNITY/Comp/Counter.thy Mon Oct 22 11:54:22 2001 +0200 @@ -21,21 +21,21 @@ sumj :: "[nat, nat, state]=>int" primrec (* sum I s = sigma_{icommand" - "a i == {(s, s'). s'=s(c i:= s (c i) + Numeral1, C:= s C + Numeral1)}" + "a i == {(s, s'). s'=s(c i:= s (c i) + 1, C:= s C + 1)}" Component :: "nat => state program" "Component i == - mk_program({s. s C = Numeral0 & s (c i) = Numeral0}, {a i}, + mk_program({s. s C = 0 & s (c i) = 0}, {a i}, UN G: preserves (%s. s (c i)). Acts G)" end diff -r 76401b2ee871 -r 56db9f3a6b3e src/HOL/UNITY/Comp/Counterc.ML --- a/src/HOL/UNITY/Comp/Counterc.ML Mon Oct 22 11:01:30 2001 +0200 +++ b/src/HOL/UNITY/Comp/Counterc.ML Mon Oct 22 11:54:22 2001 +0200 @@ -38,7 +38,7 @@ qed_spec_mp "sumj_ext"; -Goal "(ALL i. i c s i = Numeral0) --> sum I s = Numeral0"; +Goal "(ALL i. i c s i = 0) --> sum I s = 0"; by (induct_tac "I" 1); by Auto_tac; qed "sum0"; diff -r 76401b2ee871 -r 56db9f3a6b3e src/HOL/UNITY/Comp/Counterc.thy --- a/src/HOL/UNITY/Comp/Counterc.thy Mon Oct 22 11:01:30 2001 +0200 +++ b/src/HOL/UNITY/Comp/Counterc.thy Mon Oct 22 11:54:22 2001 +0200 @@ -24,20 +24,20 @@ sumj :: "[nat, nat, state]=>int" primrec (* sum I s = sigma_{icommand" - "a i == {(s, s'). (c s') i = (c s) i + Numeral1 & (C s') = (C s) + Numeral1}" + "a i == {(s, s'). (c s') i = (c s) i + 1 & (C s') = (C s) + 1}" Component :: "nat => state program" - "Component i == mk_program({s. C s = Numeral0 & (c s) i = Numeral0}, {a i}, + "Component i == mk_program({s. C s = 0 & (c s) i = 0}, {a i}, UN G: preserves (%s. (c s) i). Acts G)" end diff -r 76401b2ee871 -r 56db9f3a6b3e src/HOL/UNITY/Simple/Lift.ML --- a/src/HOL/UNITY/Simple/Lift.ML Mon Oct 22 11:01:30 2001 +0200 +++ b/src/HOL/UNITY/Simple/Lift.ML Mon Oct 22 11:54:22 2001 +0200 @@ -142,7 +142,7 @@ (*lem_lift_4_1 *) -Goal "Numeral0 < N ==> \ +Goal "0 < N ==> \ \ Lift : (moving Int Req n Int {s. metric n s = N} Int \ \ {s. floor s ~: req s} Int {s. up s}) \ \ LeadsTo \ @@ -157,7 +157,7 @@ (*lem_lift_4_3 *) -Goal "Numeral0 < N ==> \ +Goal "0 < N ==> \ \ Lift : (moving Int Req n Int {s. metric n s = N} Int \ \ {s. floor s ~: req s} - {s. up s}) \ \ LeadsTo (moving Int Req n Int {s. metric n s < N})"; @@ -170,7 +170,7 @@ qed "E_thm12b"; (*lift_4*) -Goal "Numeral0 Lift : (moving Int Req n Int {s. metric n s = N} Int \ +Goal "0 Lift : (moving Int Req n Int {s. metric n s = N} Int \ \ {s. floor s ~: req s}) LeadsTo \ \ (moving Int Req n Int {s. metric n s < N})"; by (rtac ([subset_imp_LeadsTo, [E_thm12a, E_thm12b] MRS LeadsTo_Un] @@ -182,7 +182,7 @@ (** towards lift_5 **) (*lem_lift_5_3*) -Goal "Numeral0 Lift : (closed Int Req n Int {s. metric n s = N} Int goingup) LeadsTo \ \ (moving Int Req n Int {s. metric n s < N})"; by (cut_facts_tac [bounded] 1); @@ -192,7 +192,7 @@ (*lem_lift_5_1 has ~goingup instead of goingdown*) -Goal "Numeral0 \ +Goal "0 \ \ Lift : (closed Int Req n Int {s. metric n s = N} Int goingdown) LeadsTo \ \ (moving Int Req n Int {s. metric n s < N})"; by (cut_facts_tac [bounded] 1); @@ -203,14 +203,14 @@ (*lem_lift_5_0 proves an intersection involving ~goingup and goingup, i.e. the trivial disjunction, leading to an asymmetrical proof.*) -Goal "Numeral0 Req n Int {s. metric n s = N} <= goingup Un goingdown"; +Goal "0 Req n Int {s. metric n s = N} <= goingup Un goingdown"; by (Clarify_tac 1); by (auto_tac (claset(), metric_ss)); qed "E_thm16c"; (*lift_5*) -Goal "Numeral0 Lift : (closed Int Req n Int {s. metric n s = N}) LeadsTo \ +Goal "0 Lift : (closed Int Req n Int {s. metric n s = N}) LeadsTo \ \ (moving Int Req n Int {s. metric n s < N})"; by (rtac ([subset_imp_LeadsTo, [E_thm16a, E_thm16b] MRS LeadsTo_Un] MRS LeadsTo_Trans) 1); @@ -222,7 +222,7 @@ (** towards lift_3 **) (*lemma used to prove lem_lift_3_1*) -Goal "[| metric n s = Numeral0; Min <= floor s; floor s <= Max |] ==> floor s = n"; +Goal "[| metric n s = 0; Min <= floor s; floor s <= Max |] ==> floor s = n"; by (auto_tac (claset(), metric_ss)); qed "metric_eq_0D"; @@ -230,7 +230,7 @@ (*lem_lift_3_1*) -Goal "Lift : (moving Int Req n Int {s. metric n s = Numeral0}) LeadsTo \ +Goal "Lift : (moving Int Req n Int {s. metric n s = 0}) LeadsTo \ \ (stopped Int atFloor n)"; by (cut_facts_tac [bounded] 1); by (ensures_tac "request_act" 1); @@ -246,7 +246,7 @@ qed "E_thm13"; (*lem_lift_3_6*) -Goal "Numeral0 < N ==> \ +Goal "0 < N ==> \ \ Lift : \ \ (stopped Int Req n Int {s. metric n s = N} Int {s. floor s : req s}) \ \ LeadsTo (opened Int Req n Int {s. metric n s = N})"; @@ -264,7 +264,7 @@ (** the final steps **) -Goal "Numeral0 < N ==> \ +Goal "0 < N ==> \ \ Lift : \ \ (moving Int Req n Int {s. metric n s = N} Int {s. floor s : req s}) \ \ LeadsTo (moving Int Req n Int {s. metric n s < N})"; @@ -274,7 +274,7 @@ (*Now we observe that our integer metric is really a natural number*) -Goal "Lift : Always {s. Numeral0 <= metric n s}"; +Goal "Lift : Always {s. 0 <= metric n s}"; by (rtac (bounded RS Always_weaken) 1); by (auto_tac (claset(), metric_ss)); qed "Always_nonneg"; @@ -283,8 +283,8 @@ Goal "Lift : (moving Int Req n) LeadsTo (stopped Int atFloor n)"; by (rtac (Always_nonneg RS integ_0_le_induct) 1); -by (case_tac "Numeral0 < z" 1); -(*If z <= Numeral0 then actually z = Numeral0*) +by (case_tac "0 < z" 1); +(*If z <= 0 then actually z = 0*) by (force_tac (claset() addIs [R_thm11, order_antisym], simpset() addsimps [linorder_not_less]) 2); by (rtac ([asm_rl, Un_upper1] MRS LeadsTo_weaken_R) 1); diff -r 76401b2ee871 -r 56db9f3a6b3e src/HOL/UNITY/Simple/Lift.thy --- a/src/HOL/UNITY/Simple/Lift.thy Mon Oct 22 11:01:30 2001 +0200 +++ b/src/HOL/UNITY/Simple/Lift.thy Mon Oct 22 11:54:22 2001 +0200 @@ -87,25 +87,25 @@ req_up :: "(state*state) set" "req_up == {(s,s'). s' = s (|stop :=False, - floor := floor s + Numeral1, + floor := floor s + 1, up := True|) & s : (ready Int goingup)}" req_down :: "(state*state) set" "req_down == {(s,s'). s' = s (|stop :=False, - floor := floor s - Numeral1, + floor := floor s - 1, up := False|) & s : (ready Int goingdown)}" move_up :: "(state*state) set" "move_up == - {(s,s'). s' = s (|floor := floor s + Numeral1|) + {(s,s'). s' = s (|floor := floor s + 1|) & ~ stop s & up s & floor s ~: req s}" move_down :: "(state*state) set" "move_down == - {(s,s'). s' = s (|floor := floor s - Numeral1|) + {(s,s'). s' = s (|floor := floor s - 1|) & ~ stop s & ~ up s & floor s ~: req s}" (*This action is omitted from prior treatments, which therefore are @@ -156,7 +156,7 @@ else if n < floor s then (if up s then (Max - floor s) + (Max-n) else floor s - n) - else Numeral0" + else 0" locale floor = fixes diff -r 76401b2ee871 -r 56db9f3a6b3e src/HOL/UNITY/Simple/Mutex.ML --- a/src/HOL/UNITY/Simple/Mutex.ML Mon Oct 22 11:01:30 2001 +0200 +++ b/src/HOL/UNITY/Simple/Mutex.ML Mon Oct 22 11:54:22 2001 +0200 @@ -42,7 +42,7 @@ getgoal 1; -Goal "((Numeral1::int) <= i & i <= 3) = (i = Numeral1 | i = 2 | i = 3)"; +Goal "((1::int) <= i & i <= 3) = (i = 1 | i = 2 | i = 3)"; by (arith_tac 1); qed "eq_123"; @@ -53,7 +53,7 @@ by (constrains_tac 1); qed "U_F0"; -Goal "Mutex : {s. m s=Numeral1} LeadsTo {s. p s = v s & m s = 2}"; +Goal "Mutex : {s. m s=1} LeadsTo {s. p s = v s & m s = 2}"; by (ensures_tac "U1" 1); qed "U_F1"; @@ -75,12 +75,12 @@ by (auto_tac (claset() addSEs [less_SucE], simpset())); val U_lemma2 = result(); -Goal "Mutex : {s. m s = Numeral1} LeadsTo {s. p s}"; +Goal "Mutex : {s. m s = 1} LeadsTo {s. p s}"; by (rtac ([U_F1 RS LeadsTo_weaken_R, U_lemma2] MRS LeadsTo_Trans) 1); by (Blast_tac 1); val U_lemma1 = result(); -Goal "Mutex : {s. Numeral1 <= m s & m s <= 3} LeadsTo {s. p s}"; +Goal "Mutex : {s. 1 <= m s & m s <= 3} LeadsTo {s. p s}"; by (simp_tac (simpset() addsimps [eq_123, Collect_disj_eq, LeadsTo_Un_distrib, U_lemma1, U_lemma2, U_F3] ) 1); val U_lemma123 = result(); @@ -99,7 +99,7 @@ by (constrains_tac 1); qed "V_F0"; -Goal "Mutex : {s. n s=Numeral1} LeadsTo {s. p s = (~ u s) & n s = 2}"; +Goal "Mutex : {s. n s=1} LeadsTo {s. p s = (~ u s) & n s = 2}"; by (ensures_tac "V1" 1); qed "V_F1"; @@ -121,12 +121,12 @@ by (auto_tac (claset() addSEs [less_SucE], simpset())); val V_lemma2 = result(); -Goal "Mutex : {s. n s = Numeral1} LeadsTo {s. ~ p s}"; +Goal "Mutex : {s. n s = 1} LeadsTo {s. ~ p s}"; by (rtac ([V_F1 RS LeadsTo_weaken_R, V_lemma2] MRS LeadsTo_Trans) 1); by (Blast_tac 1); val V_lemma1 = result(); -Goal "Mutex : {s. Numeral1 <= n s & n s <= 3} LeadsTo {s. ~ p s}"; +Goal "Mutex : {s. 1 <= n s & n s <= 3} LeadsTo {s. ~ p s}"; by (simp_tac (simpset() addsimps [eq_123, Collect_disj_eq, LeadsTo_Un_distrib, V_lemma1, V_lemma2, V_F3] ) 1); val V_lemma123 = result(); @@ -142,7 +142,7 @@ (** Absence of starvation **) (*Misra's F6*) -Goal "Mutex : {s. m s = Numeral1} LeadsTo {s. m s = 3}"; +Goal "Mutex : {s. m s = 1} LeadsTo {s. m s = 3}"; by (rtac (LeadsTo_cancel2 RS LeadsTo_Un_duplicate) 1); by (rtac U_F2 2); by (simp_tac (simpset() addsimps [Collect_conj_eq] ) 1); @@ -154,7 +154,7 @@ qed "m1_Leadsto_3"; (*The same for V*) -Goal "Mutex : {s. n s = Numeral1} LeadsTo {s. n s = 3}"; +Goal "Mutex : {s. n s = 1} LeadsTo {s. n s = 3}"; by (rtac (LeadsTo_cancel2 RS LeadsTo_Un_duplicate) 1); by (rtac V_F2 2); by (simp_tac (simpset() addsimps [Collect_conj_eq] ) 1); diff -r 76401b2ee871 -r 56db9f3a6b3e src/HOL/UNITY/Simple/Mutex.thy --- a/src/HOL/UNITY/Simple/Mutex.thy Mon Oct 22 11:01:30 2001 +0200 +++ b/src/HOL/UNITY/Simple/Mutex.thy Mon Oct 22 11:54:22 2001 +0200 @@ -22,10 +22,10 @@ (** The program for process U **) U0 :: command - "U0 == {(s,s'). s' = s (|u:=True, m:=Numeral1|) & m s = Numeral0}" + "U0 == {(s,s'). s' = s (|u:=True, m:=1|) & m s = 0}" U1 :: command - "U1 == {(s,s'). s' = s (|p:= v s, m:=2|) & m s = Numeral1}" + "U1 == {(s,s'). s' = s (|p:= v s, m:=2|) & m s = 1}" U2 :: command "U2 == {(s,s'). s' = s (|m:=3|) & ~ p s & m s = 2}" @@ -34,15 +34,15 @@ "U3 == {(s,s'). s' = s (|u:=False, m:=4|) & m s = 3}" U4 :: command - "U4 == {(s,s'). s' = s (|p:=True, m:=Numeral0|) & m s = 4}" + "U4 == {(s,s'). s' = s (|p:=True, m:=0|) & m s = 4}" (** The program for process V **) V0 :: command - "V0 == {(s,s'). s' = s (|v:=True, n:=Numeral1|) & n s = Numeral0}" + "V0 == {(s,s'). s' = s (|v:=True, n:=1|) & n s = 0}" V1 :: command - "V1 == {(s,s'). s' = s (|p:= ~ u s, n:=2|) & n s = Numeral1}" + "V1 == {(s,s'). s' = s (|p:= ~ u s, n:=2|) & n s = 1}" V2 :: command "V2 == {(s,s'). s' = s (|n:=3|) & p s & n s = 2}" @@ -51,10 +51,10 @@ "V3 == {(s,s'). s' = s (|v:=False, n:=4|) & n s = 3}" V4 :: command - "V4 == {(s,s'). s' = s (|p:=False, n:=Numeral0|) & n s = 4}" + "V4 == {(s,s'). s' = s (|p:=False, n:=0|) & n s = 4}" Mutex :: state program - "Mutex == mk_program ({s. ~ u s & ~ v s & m s = Numeral0 & n s = Numeral0}, + "Mutex == mk_program ({s. ~ u s & ~ v s & m s = 0 & n s = 0}, {U0, U1, U2, U3, U4, V0, V1, V2, V3, V4}, UNIV)" @@ -62,15 +62,15 @@ (** The correct invariants **) IU :: state set - "IU == {s. (u s = (Numeral1 <= m s & m s <= 3)) & (m s = 3 --> ~ p s)}" + "IU == {s. (u s = (1 <= m s & m s <= 3)) & (m s = 3 --> ~ p s)}" IV :: state set - "IV == {s. (v s = (Numeral1 <= n s & n s <= 3)) & (n s = 3 --> p s)}" + "IV == {s. (v s = (1 <= n s & n s <= 3)) & (n s = 3 --> p s)}" (** The faulty invariant (for U alone) **) bad_IU :: state set - "bad_IU == {s. (u s = (Numeral1 <= m s & m s <= 3)) & + "bad_IU == {s. (u s = (1 <= m s & m s <= 3)) & (3 <= m s & m s <= 4 --> ~ p s)}" end diff -r 76401b2ee871 -r 56db9f3a6b3e src/HOL/UNITY/SubstAx.ML --- a/src/HOL/UNITY/SubstAx.ML Mon Oct 22 11:01:30 2001 +0200 +++ b/src/HOL/UNITY/SubstAx.ML Mon Oct 22 11:54:22 2001 +0200 @@ -341,9 +341,9 @@ by (auto_tac (claset() addIs prems, simpset())); qed "LessThan_induct"; -(*Integer version. Could generalize from Numeral0 to any lower bound*) +(*Integer version. Could generalize from 0 to any lower bound*) val [reach, prem] = -Goal "[| F : Always {s. (Numeral0::int) <= f s}; \ +Goal "[| F : Always {s. (0::int) <= f s}; \ \ !! z. F : (A Int {s. f s = z}) LeadsTo \ \ ((A Int {s. f s < z}) Un B) |] \ \ ==> F : A LeadsTo B"; diff -r 76401b2ee871 -r 56db9f3a6b3e src/HOL/UNITY/Union.ML --- a/src/HOL/UNITY/Union.ML Mon Oct 22 11:01:30 2001 +0200 +++ b/src/HOL/UNITY/Union.ML Mon Oct 22 11:54:22 2001 +0200 @@ -352,7 +352,7 @@ bind_thm ("ok_sym", ok_commute RS iffD1); -Goal "OK {(Numeral0::int,F),(Numeral1,G),(2,H)} snd = (F ok G & (F Join G) ok H)"; +Goal "OK {(0::int,F),(1,G),(2,H)} snd = (F ok G & (F Join G) ok H)"; by (asm_full_simp_tac (simpset() addsimps [Ball_def, conj_disj_distribR, ok_def, Join_def, OK_def, insert_absorb, all_conj_distrib, eq_commute]) 1); diff -r 76401b2ee871 -r 56db9f3a6b3e src/HOL/ex/BinEx.thy --- a/src/HOL/ex/BinEx.thy Mon Oct 22 11:01:30 2001 +0200 +++ b/src/HOL/ex/BinEx.thy Mon Oct 22 11:54:22 2001 +0200 @@ -60,7 +60,7 @@ lemma "(13557456::int) < 18678654" by simp -lemma "(999999::int) \ (1000001 + Numeral1) - 2" +lemma "(999999::int) \ (1000001 + 1) - 2" by simp lemma "(1234567::int) \ 1234567" @@ -72,7 +72,7 @@ lemma "(10::int) div 3 = 3" by simp -lemma "(10::int) mod 3 = Numeral1" +lemma "(10::int) mod 3 = 1" by simp text {* A negative divisor *} @@ -104,7 +104,7 @@ text {* A few bigger examples *} -lemma "(8452::int) mod 3 = Numeral1" +lemma "(8452::int) mod 3 = 1" by simp lemma "(59485::int) div 434 = 137" @@ -119,7 +119,7 @@ lemma "10000000 div 2 = (5000000::int)" by simp -lemma "10000001 mod 2 = (Numeral1::int)" +lemma "10000001 mod 2 = (1::int)" by simp lemma "10000055 div 32 = (312501::int)" @@ -161,10 +161,10 @@ lemma "(32::nat) - 14 = 18" by simp -lemma "(14::nat) - 15 = Numeral0" +lemma "(14::nat) - 15 = 0" by simp -lemma "(14::nat) - 1576644 = Numeral0" +lemma "(14::nat) - 1576644 = 0" by simp lemma "(48273776::nat) - 3873737 = 44400039" @@ -185,49 +185,49 @@ lemma "(10::nat) div 3 = 3" by simp -lemma "(10::nat) mod 3 = Numeral1" +lemma "(10::nat) mod 3 = 1" by simp lemma "(10000::nat) div 9 = 1111" by simp -lemma "(10000::nat) mod 9 = Numeral1" +lemma "(10000::nat) mod 9 = 1" by simp lemma "(10000::nat) div 16 = 625" by simp -lemma "(10000::nat) mod 16 = Numeral0" +lemma "(10000::nat) mod 16 = 0" by simp text {* \medskip Testing the cancellation of complementary terms *} -lemma "y + (x + -x) = (Numeral0::int) + y" +lemma "y + (x + -x) = (0::int) + y" by simp -lemma "y + (-x + (- y + x)) = (Numeral0::int)" +lemma "y + (-x + (- y + x)) = (0::int)" by simp -lemma "-x + (y + (- y + x)) = (Numeral0::int)" +lemma "-x + (y + (- y + x)) = (0::int)" by simp -lemma "x + (x + (- x + (- x + (- y + - z)))) = (Numeral0::int) - y - z" +lemma "x + (x + (- x + (- x + (- y + - z)))) = (0::int) - y - z" by simp -lemma "x + x - x - x - y - z = (Numeral0::int) - y - z" +lemma "x + x - x - x - y - z = (0::int) - y - z" by simp -lemma "x + y + z - (x + z) = y - (Numeral0::int)" +lemma "x + y + z - (x + z) = y - (0::int)" by simp -lemma "x + (y + (y + (y + (-x + -x)))) = (Numeral0::int) + y - x + y + y" +lemma "x + (y + (y + (y + (-x + -x)))) = (0::int) + y - x + y + y" by simp -lemma "x + (y + (y + (y + (-y + -x)))) = y + (Numeral0::int) + y" +lemma "x + (y + (y + (y + (-y + -x)))) = y + (0::int) + y" by simp -lemma "x + y - x + z - x - y - z + x < (Numeral1::int)" +lemma "x + y - x + z - x - y - z + x < (1::int)" by simp @@ -302,7 +302,7 @@ apply simp_all done -lemma normal_Pls_eq_0: "w \ normal ==> (w = Pls) = (number_of w = (Numeral0::int))" +lemma normal_Pls_eq_0: "w \ normal ==> (w = Pls) = (number_of w = (0::int))" apply (erule normal.induct) apply auto done @@ -313,7 +313,7 @@ apply (rule normal.intros) apply assumption apply (simp add: normal_Pls_eq_0) - apply (simp only: number_of_minus iszero_def zminus_equation [of _ "int 0"]) + apply (simp only: number_of_minus iszero_def zminus_equation [of _ "0"]) apply (rule not_sym) apply simp done diff -r 76401b2ee871 -r 56db9f3a6b3e src/HOL/ex/IntRing.thy --- a/src/HOL/ex/IntRing.thy Mon Oct 22 11:01:30 2001 +0200 +++ b/src/HOL/ex/IntRing.thy Mon Oct 22 11:54:22 2001 +0200 @@ -10,7 +10,7 @@ IntRing = Ring + Lagrange + instance int :: add_semigroup (zadd_assoc) -instance int :: add_monoid (Zero_int_def,zadd_int0,zadd_int0_right) +instance int :: add_monoid (zadd_0,zadd_0_right) instance int :: add_group {|Auto_tac|} instance int :: add_agroup (zadd_commute) instance int :: ring (zmult_assoc,zadd_zmult_distrib2,zadd_zmult_distrib) diff -r 76401b2ee871 -r 56db9f3a6b3e src/HOL/ex/svc_test.ML --- a/src/HOL/ex/svc_test.ML Mon Oct 22 11:01:30 2001 +0200 +++ b/src/HOL/ex/svc_test.ML Mon Oct 22 11:54:22 2001 +0200 @@ -233,12 +233,12 @@ Goal "x ~= 14 & x ~= 13 & x ~= 12 & x ~= 11 & x ~= 10 & x ~= 9 & \ \ x ~= 8 & x ~= 7 & x ~= 6 & x ~= 5 & x ~= 4 & x ~= 3 & \ -\ x ~= 2 & x ~= Numeral1 & Numeral0 < x & x < 16 --> 15 = (x::int)"; +\ x ~= 2 & x ~= 1 & 0 < x & x < 16 --> 15 = (x::int)"; by (svc_tac 1); qed ""; (*merely to test polarity handling in the presence of biconditionals*) -Goal "(x < (y::int)) = (x+Numeral1 <= y)"; +Goal "(x < (y::int)) = (x+1 <= y)"; by (svc_tac 1); qed ""; @@ -249,6 +249,6 @@ by (svc_tac 1); qed ""; -Goal "(n::nat) < 2 ==> (n = Numeral0) | (n = Numeral1)"; +Goal "(n::nat) < 2 ==> (n = 0) | (n = 1)"; by (svc_tac 1); qed "";