# HG changeset patch # User paulson # Date 1070530157 -3600 # Node ID 5efbb548107d491b8bb6a4e64bb508cc3036b96f # Parent 8ed6989228bb80b195a787a8c7cdc59baae4251b Tidying of the integer development; towards removing the abel_cancel simproc diff -r 8ed6989228bb -r 5efbb548107d src/HOL/Integ/Bin.ML --- a/src/HOL/Integ/Bin.ML Wed Dec 03 10:49:34 2003 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,503 +0,0 @@ -(* Title: HOL/Integ/Bin.ML - ID: $Id$ - Authors: Lawrence C Paulson, Cambridge University Computer Laboratory - David Spelt, University of Twente - Tobias Nipkow, Technical University Munich - Copyright 1994 University of Cambridge - Copyright 1996 University of Twente - Copyright 1999 TU Munich - -Arithmetic on binary integers. -*) - -(** extra rules for bin_succ, bin_pred, bin_add, bin_mult **) - -Goal "NCons bin.Pls False = bin.Pls"; -by (Simp_tac 1); -qed "NCons_Pls_0"; - -Goal "NCons bin.Pls True = bin.Pls BIT True"; -by (Simp_tac 1); -qed "NCons_Pls_1"; - -Goal "NCons bin.Min False = bin.Min BIT False"; -by (Simp_tac 1); -qed "NCons_Min_0"; - -Goal "NCons bin.Min True = bin.Min"; -by (Simp_tac 1); -qed "NCons_Min_1"; - -Goal "bin_succ(w BIT True) = (bin_succ w) BIT False"; -by (Simp_tac 1); -qed "bin_succ_1"; - -Goal "bin_succ(w BIT False) = NCons w True"; -by (Simp_tac 1); -qed "bin_succ_0"; - -Goal "bin_pred(w BIT True) = NCons w False"; -by (Simp_tac 1); -qed "bin_pred_1"; - -Goal "bin_pred(w BIT False) = (bin_pred w) BIT True"; -by (Simp_tac 1); -qed "bin_pred_0"; - -Goal "bin_minus(w BIT True) = bin_pred (NCons (bin_minus w) False)"; -by (Simp_tac 1); -qed "bin_minus_1"; - -Goal "bin_minus(w BIT False) = (bin_minus w) BIT False"; -by (Simp_tac 1); -qed "bin_minus_0"; - - -(*** bin_add: binary addition ***) - -Goal "bin_add (v BIT True) (w BIT True) = \ -\ NCons (bin_add v (bin_succ w)) False"; -by (Simp_tac 1); -qed "bin_add_BIT_11"; - -Goal "bin_add (v BIT True) (w BIT False) = NCons (bin_add v w) True"; -by (Simp_tac 1); -qed "bin_add_BIT_10"; - -Goal "bin_add (v BIT False) (w BIT y) = NCons (bin_add v w) y"; -by Auto_tac; -qed "bin_add_BIT_0"; - -Goal "bin_add w bin.Pls = w"; -by (induct_tac "w" 1); -by Auto_tac; -qed "bin_add_Pls_right"; - -Goal "bin_add w bin.Min = bin_pred w"; -by (induct_tac "w" 1); -by Auto_tac; -qed "bin_add_Min_right"; - -Goal "bin_add (v BIT x) (w BIT y) = \ -\ NCons(bin_add v (if x & y then (bin_succ w) else w)) (x~= y)"; -by (Simp_tac 1); -qed "bin_add_BIT_BIT"; - - -(*** bin_mult: binary multiplication ***) - -Goal "bin_mult (v BIT True) w = bin_add (NCons (bin_mult v w) False) w"; -by (Simp_tac 1); -qed "bin_mult_1"; - -Goal "bin_mult (v BIT False) w = NCons (bin_mult v w) False"; -by (Simp_tac 1); -qed "bin_mult_0"; - - -(**** The carry/borrow functions, bin_succ and bin_pred ****) - - -(** number_of **) - -Goal "number_of(NCons w b) = (number_of(w BIT b)::int)"; -by (induct_tac "w" 1); -by (ALLGOALS Asm_simp_tac); -qed "number_of_NCons"; - -Addsimps [number_of_NCons]; - -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) = (- 1 + number_of w :: int)"; -by (induct_tac "w" 1); -by (ALLGOALS (asm_simp_tac (simpset() addsimps zadd_ac))); -qed "number_of_pred"; - -Goal "number_of(bin_minus w) = (- (number_of w)::int)"; -by (induct_tac "w" 1); -by (Simp_tac 1); -by (Simp_tac 1); -by (asm_simp_tac (simpset() - delsimps [bin_pred_Pls, bin_pred_Min, bin_pred_BIT] - addsimps [number_of_succ,number_of_pred, - zadd_assoc]) 1); -qed "number_of_minus"; - -(*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 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_BIT_BIT, number_of_succ, number_of_pred] @ zadd_ac))); -qed_spec_mp "number_of_add"; - - -(*Subtraction*) -Goalw [zdiff_def] - "number_of v - number_of w = (number_of(bin_add v (bin_minus w))::int)"; -by (simp_tac (simpset() addsimps [number_of_add, number_of_minus]) 1); -qed "diff_number_of_eq"; - -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); -by (simp_tac (simpset() addsimps bin_mult_simps) 1); -by (simp_tac (simpset() addsimps bin_mult_simps) 1); -by (asm_simp_tac - (simpset() addsimps bin_mult_simps @ [zadd_zmult_distrib] @ zadd_ac) 1); -qed "number_of_mult"; - - -(*The correctness of shifting. But it doesn't seem to give a measurable - speed-up.*) -Goal "(2::int) * number_of w = number_of (w BIT False)"; -by (induct_tac "w" 1); -by (ALLGOALS (asm_simp_tac - (simpset() addsimps bin_mult_simps @ [zadd_zmult_distrib] @ zadd_ac))); -qed "double_number_of_BIT"; - - -(** Converting numerals 0 and 1 to their abstract versions **) - -Goal "Numeral0 = (0::int)"; -by (Simp_tac 1); -qed "int_numeral_0_eq_0"; - -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 **) - -(*Distributive laws for literals*) -Addsimps (map (inst "w" "number_of ?v") - [zadd_zmult_distrib, zadd_zmult_distrib2, - zdiff_zmult_distrib, zdiff_zmult_distrib2]); - -Addsimps (map (inst "x" "number_of ?v") - [zless_zminus, zle_zminus, equation_zminus]); -Addsimps (map (inst "y" "number_of ?v") - [zminus_zless, zminus_zle, zminus_equation]); - -(*Equations and inequations involving 1*) -Addsimps (map (simplify (simpset()) o inst "x" "1") - [zless_zminus, zle_zminus, equation_zminus]); -Addsimps (map (simplify (simpset()) o inst "y" "1") - [zminus_zless, zminus_zle, zminus_equation]); - -(*Moving negation out of products*) -Addsimps [zmult_zminus, zmult_zminus_right]; - -(*Cancellation of constant factors in comparisons (< and <=) *) -Addsimps (map (inst "k" "number_of ?v") - [zmult_zless_cancel1, zmult_zless_cancel2, - zmult_zle_cancel1, zmult_zle_cancel2]); - - -(** Special-case simplification for small constants **) - -Goal "-1 * z = -(z::int)"; -by (simp_tac (simpset() addsimps compare_rls@[int_Suc0_eq_1, zmult_zminus]) 1); -qed "zmult_minus1"; - -Goal "z * -1 = -(z::int)"; -by (stac zmult_commute 1 THEN rtac zmult_minus1 1); -qed "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]; - -(*Integer unary minus for the abstract constant 1. Cannot be inserted - as a simprule until later: it is number_of_Min re-oriented!*) -Goal "- 1 = (-1::int)"; -by (Simp_tac 1); -qed "zminus_1_eq_m1"; - -Goal "(0 < nat z) = (0 < z)"; -by (cut_inst_tac [("w","0")] zless_nat_conj 1); -by Auto_tac; -qed "zero_less_nat_eq"; -Addsimps [zero_less_nat_eq]; - - -(** Simplification rules for comparison of binary numbers (Norbert Voelker) **) - -(** Equals (=) **) - -Goalw [iszero_def] - "((number_of x::int) = number_of y) = \ -\ iszero (number_of (bin_add x (bin_minus y)))"; -by (simp_tac (simpset() - addsimps compare_rls @ [number_of_add, number_of_minus]) 1); -qed "eq_number_of_eq"; - -Goalw [iszero_def] "iszero ((number_of bin.Pls)::int)"; -by (Simp_tac 1); -qed "iszero_number_of_Pls"; - -Goalw [iszero_def] "~ iszero ((number_of bin.Min)::int)"; -by (simp_tac (simpset() addsimps [eq_commute]) 1); -qed "nonzero_number_of_Min"; - -fun int_case_tac x = res_inst_tac [("z",x)] int_cases; - -Goalw [iszero_def] - "iszero (number_of (w BIT x)) = (~x & iszero (number_of w::int))"; -by (int_case_tac "number_of w" 1); -by (ALLGOALS - (asm_simp_tac - (simpset() addsimps compare_rls @ - [zero_reorient, zminus_zadd_distrib RS sym, - int_Suc0_eq_1 RS sym, zadd_int]))); -qed "iszero_number_of_BIT"; - -Goal "iszero (number_of (w BIT False)) = iszero (number_of w::int)"; -by (simp_tac (HOL_ss addsimps [iszero_number_of_BIT]) 1); -qed "iszero_number_of_0"; - -Goal "~ iszero (number_of (w BIT True)::int)"; -by (simp_tac (HOL_ss addsimps [iszero_number_of_BIT]) 1); -qed "iszero_number_of_1"; - - - -(** Less-than (<) **) - -Goalw [zless_def,zdiff_def] - "((number_of x::int) < number_of y) \ -\ = neg (number_of (bin_add x (bin_minus y)))"; -by (simp_tac (simpset() addsimps bin_mult_simps) 1); -qed "less_number_of_eq_neg"; - -(*But if Numeral0 is rewritten to 0 then this rule can't be applied: - Numeral0 IS (number_of Pls) *) -Goal "~ neg (number_of bin.Pls)"; -by (simp_tac (simpset() addsimps [neg_eq_less_0]) 1); -qed "not_neg_number_of_Pls"; - -Goal "neg (number_of bin.Min)"; -by (simp_tac (simpset() addsimps [neg_eq_less_0, int_0_less_1]) 1); -qed "neg_number_of_Min"; - -Goal "neg (number_of (w BIT x)) = neg (number_of w)"; -by (Asm_simp_tac 1); -by (int_case_tac "number_of w" 1); -by (ALLGOALS (asm_simp_tac - (simpset() addsimps [int_Suc0_eq_1 RS sym, zadd_int, - neg_eq_less_0, symmetric zdiff_def] @ compare_rls))); -qed "neg_number_of_BIT"; - - -(** Less-than-or-equals (<=) **) - -Goal "(number_of x <= (number_of y::int)) = \ -\ (~ number_of y < (number_of x::int))"; -by (rtac (linorder_not_less RS sym) 1); -qed "le_number_of_eq_not_less"; - -(** Absolute value (abs) **) - -Goalw [zabs_def] - "abs(number_of x::int) = \ -\ (if number_of x < (0::int) then -number_of x else number_of x)"; -by (rtac refl 1); -qed "zabs_number_of"; - -(*0 and 1 require special rewrites because they aren't numerals*) -Goal "abs (0::int) = 0"; -by (simp_tac (simpset() addsimps [zabs_def]) 1); -qed "zabs_0"; - -Goal "abs (1::int) = 1"; -by (simp_tac (simpset() delsimps [int_0, int_1] - addsimps [int_0 RS sym, int_1 RS sym, zabs_def]) 1); -qed "zabs_1"; - -(*Re-orientation of the equation nnn=x*) -Goal "(number_of w = x) = (x = number_of w)"; -by Auto_tac; -qed "number_of_reorient"; - - -structure Bin_Simprocs = - struct - fun prove_conv tacs sg (hyps: thm list) xs (t, u) = - if t aconv u then None - else - let val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u)) - in Some (Tactic.prove sg xs [] eq (K (EVERY tacs))) end - - fun prove_conv_nohyps tacs sg = prove_conv tacs sg []; - fun prove_conv_nohyps_novars tacs sg = prove_conv tacs sg [] []; - - fun prep_simproc (name, pats, proc) = - Simplifier.simproc (Theory.sign_of (the_context())) name pats proc; - - 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_novars - 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", - ["(m::int) + 1", "(m::int) + number_of v"], - IntAbstractNumerals.proc (number_of_add RS sym)), - ("int_diff_eval_numerals", - ["(m::int) - 1", "(m::int) - number_of v"], - IntAbstractNumerals.proc diff_number_of_eq), - ("int_eq_eval_numerals", - ["(m::int) = 0", "(m::int) = 1", "(m::int) = number_of v"], - IntAbstractNumerals.proc eq_number_of_eq), - ("int_less_eval_numerals", - ["(m::int) < 0", "(m::int) < 1", "(m::int) < number_of v"], - IntAbstractNumerals.proc less_number_of_eq_neg), - ("int_le_eval_numerals", - ["(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", ["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*) -Delsimps [bin_succ_BIT, bin_pred_BIT, bin_minus_BIT, - NCons_Pls, NCons_Min, bin_add_BIT, bin_mult_BIT]; - -(*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 ("bin_arith_extra_simps", - [number_of_add 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, 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 - of thy. Also include simp_thms, or at least (~False)=True*) -bind_thms ("bin_arith_simps", - [bin_pred_Pls, bin_pred_Min, - bin_succ_Pls, bin_succ_Min, - bin_add_Pls, bin_add_Min, - bin_minus_Pls, bin_minus_Min, - bin_mult_Pls, bin_mult_Min] @ bin_arith_extra_simps); - -(*Simplification of relational operations*) -bind_thms ("bin_rel_simps", - [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, 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; -Addsimps bin_rel_simps; - - -(** Simplification of arithmetic when nested to the right **) - -Goal "number_of v + (number_of w + z) = (number_of(bin_add v w) + z::int)"; -by (simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1); -qed "add_number_of_left"; - -Goal "number_of v * (number_of w * z) = (number_of(bin_mult v w) * z::int)"; -by (simp_tac (simpset() addsimps [zmult_assoc RS sym]) 1); -qed "mult_number_of_left"; - -Goalw [zdiff_def] - "number_of v + (number_of w - c) = number_of(bin_add v w) - (c::int)"; -by (rtac add_number_of_left 1); -qed "add_number_of_diff1"; - -Goal "number_of v + (c - number_of w) = \ -\ number_of (bin_add v (bin_minus w)) + (c::int)"; -by (stac (diff_number_of_eq RS sym) 1); -by Auto_tac; -qed "add_number_of_diff2"; - -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 8ed6989228bb -r 5efbb548107d src/HOL/Integ/Bin.thy --- a/src/HOL/Integ/Bin.thy Wed Dec 03 10:49:34 2003 +0100 +++ b/src/HOL/Integ/Bin.thy Thu Dec 04 10:29:17 2003 +0100 @@ -1,73 +1,78 @@ (* Title: HOL/Integ/Bin.thy ID: $Id$ Authors: Lawrence C Paulson, Cambridge University Computer Laboratory - David Spelt, University of Twente + David Spelt, University of Twente Copyright 1994 University of Cambridge Copyright 1996 University of Twente +*) -Arithmetic on binary integers. +header{*Arithmetic on Binary Integers*} + +theory Bin = Int + Numeral: - The sign Pls stands for an infinite string of leading F's. - The sign Min stands for an infinite string of leading T's. +text{*The sign @{term Pls} stands for an infinite string of leading Falses.*} +text{*The sign @{term Min} stands for an infinite string of leading Trues.*} -A number can have multiple representations, namely leading F's with sign -Pls and leading T's with sign Min. See ZF/ex/twos-compl.ML/int_of_binary +text{*A number can have multiple representations, namely leading Falses with +sign @{term Pls} and leading Trues with sign @{term Min}. +See @{text "ZF/Integ/twos-compl.ML"}, function @{text int_of_binary}, 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 -*) - -Bin = Int + Numeral + +The representation expects that @{term "(m mod 2)"} is 0 or 1, +even if m is negative; +For instance, @{term "-5 div 2 = -3"} and @{term "-5 mod 2 = 1"}; thus +@{term "-5 = (-3)*2 + 1"}. +*} consts - NCons :: [bin,bool]=>bin - bin_succ :: bin=>bin - bin_pred :: bin=>bin - bin_minus :: bin=>bin - bin_add,bin_mult :: [bin,bin]=>bin + NCons :: "[bin,bool]=>bin" + bin_succ :: "bin=>bin" + bin_pred :: "bin=>bin" + bin_minus :: "bin=>bin" + bin_add :: "[bin,bin]=>bin" + bin_mult :: "[bin,bin]=>bin" (*NCons inserts a bit, suppressing leading 0s and 1s*) primrec - NCons_Pls "NCons bin.Pls b = (if b then (bin.Pls BIT b) else bin.Pls)" - NCons_Min "NCons bin.Min b = (if b then bin.Min else (bin.Min BIT b))" - NCons_BIT "NCons (w BIT x) b = (w BIT x) BIT b" + NCons_Pls: "NCons bin.Pls b = (if b then (bin.Pls BIT b) else bin.Pls)" + NCons_Min: "NCons bin.Min b = (if b then bin.Min else (bin.Min BIT b))" + NCons_BIT: "NCons (w BIT x) b = (w BIT x) BIT b" instance - int :: number + int :: number .. primrec (*the type constraint is essential!*) - number_of_Pls "number_of bin.Pls = 0" - number_of_Min "number_of bin.Min = - (1::int)" - number_of_BIT "number_of(w BIT x) = (if x then 1 else 0) + - (number_of w) + (number_of w)" + number_of_Pls: "number_of bin.Pls = 0" + number_of_Min: "number_of bin.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 bin.Pls = bin.Pls BIT True" - bin_succ_Min "bin_succ bin.Min = bin.Pls" - bin_succ_BIT "bin_succ(w BIT x) = + bin_succ_Pls: "bin_succ bin.Pls = bin.Pls BIT True" + bin_succ_Min: "bin_succ bin.Min = bin.Pls" + bin_succ_BIT: "bin_succ(w BIT x) = (if x then bin_succ w BIT False else NCons w True)" primrec - bin_pred_Pls "bin_pred bin.Pls = bin.Min" - bin_pred_Min "bin_pred bin.Min = bin.Min BIT False" - bin_pred_BIT "bin_pred(w BIT x) = + bin_pred_Pls: "bin_pred bin.Pls = bin.Min" + bin_pred_Min: "bin_pred bin.Min = bin.Min BIT False" + bin_pred_BIT: "bin_pred(w BIT x) = (if x then NCons w False else (bin_pred w) BIT True)" - + primrec - bin_minus_Pls "bin_minus bin.Pls = bin.Pls" - bin_minus_Min "bin_minus bin.Min = bin.Pls BIT True" - bin_minus_BIT "bin_minus(w BIT x) = + bin_minus_Pls: "bin_minus bin.Pls = bin.Pls" + bin_minus_Min: "bin_minus bin.Min = bin.Pls BIT True" + bin_minus_BIT: "bin_minus(w BIT x) = (if x then bin_pred (NCons (bin_minus w) False) else bin_minus w BIT False)" primrec - bin_add_Pls "bin_add bin.Pls w = w" - bin_add_Min "bin_add bin.Min w = bin_pred w" - bin_add_BIT - "bin_add (v BIT x) w = + bin_add_Pls: "bin_add bin.Pls w = w" + bin_add_Min: "bin_add bin.Min w = bin_pred w" + bin_add_BIT: + "bin_add (v BIT x) w = (case w of Pls => v BIT x | Min => bin_pred (v BIT x) | (w BIT y) => @@ -75,10 +80,384 @@ (x~=y))" primrec - bin_mult_Pls "bin_mult bin.Pls w = bin.Pls" - bin_mult_Min "bin_mult bin.Min w = bin_minus w" - bin_mult_BIT "bin_mult (v BIT x) w = + bin_mult_Pls: "bin_mult bin.Pls w = bin.Pls" + bin_mult_Min: "bin_mult bin.Min w = bin_minus w" + bin_mult_BIT: "bin_mult (v BIT x) w = (if x then (bin_add (NCons (bin_mult v w) False) w) else (NCons (bin_mult v w) False))" + +(** extra rules for bin_succ, bin_pred, bin_add, bin_mult **) + +lemma NCons_Pls_0: "NCons bin.Pls False = bin.Pls" +by simp + +lemma NCons_Pls_1: "NCons bin.Pls True = bin.Pls BIT True" +by simp + +lemma NCons_Min_0: "NCons bin.Min False = bin.Min BIT False" +by simp + +lemma NCons_Min_1: "NCons bin.Min True = bin.Min" +by simp + +lemma bin_succ_1: "bin_succ(w BIT True) = (bin_succ w) BIT False" +by simp + +lemma bin_succ_0: "bin_succ(w BIT False) = NCons w True" +by simp + +lemma bin_pred_1: "bin_pred(w BIT True) = NCons w False" +by simp + +lemma bin_pred_0: "bin_pred(w BIT False) = (bin_pred w) BIT True" +by simp + +lemma bin_minus_1: "bin_minus(w BIT True) = bin_pred (NCons (bin_minus w) False)" +by simp + +lemma bin_minus_0: "bin_minus(w BIT False) = (bin_minus w) BIT False" +by simp + + +(*** bin_add: binary addition ***) + +lemma bin_add_BIT_11: "bin_add (v BIT True) (w BIT True) = + NCons (bin_add v (bin_succ w)) False" +apply simp +done + +lemma bin_add_BIT_10: "bin_add (v BIT True) (w BIT False) = NCons (bin_add v w) True" +by simp + +lemma bin_add_BIT_0: "bin_add (v BIT False) (w BIT y) = NCons (bin_add v w) y" +by auto + +lemma bin_add_Pls_right: "bin_add w bin.Pls = w" +by (induct_tac "w", auto) + +lemma bin_add_Min_right: "bin_add w bin.Min = bin_pred w" +by (induct_tac "w", auto) + +lemma bin_add_BIT_BIT: "bin_add (v BIT x) (w BIT y) = + NCons(bin_add v (if x & y then (bin_succ w) else w)) (x~= y)" +apply simp +done + + +(*** bin_mult: binary multiplication ***) + +lemma bin_mult_1: "bin_mult (v BIT True) w = bin_add (NCons (bin_mult v w) False) w" +by simp + +lemma bin_mult_0: "bin_mult (v BIT False) w = NCons (bin_mult v w) False" +by simp + + +(**** The carry/borrow functions, bin_succ and bin_pred ****) + + +(** number_of **) + +lemma number_of_NCons [simp]: + "number_of(NCons w b) = (number_of(w BIT b)::int)" +apply (induct_tac "w") +apply (simp_all) +done + +lemma number_of_succ: "number_of(bin_succ w) = (1 + number_of w :: int)" +apply (induct_tac "w") +apply (simp_all add: zadd_ac) +done + +lemma number_of_pred: "number_of(bin_pred w) = (- 1 + number_of w :: int)" +apply (induct_tac "w") +apply (simp_all add: add_assoc [symmetric]) +apply (simp add: zadd_ac) +done + +lemma number_of_minus: "number_of(bin_minus w) = (- (number_of w)::int)" +apply (induct_tac "w", simp, simp) +apply (simp del: bin_pred_Pls bin_pred_Min bin_pred_BIT add: number_of_succ number_of_pred zadd_assoc) +done + +(*This proof is complicated by the mutual recursion*) +lemma number_of_add [rule_format (no_asm)]: "! w. number_of(bin_add v w) = (number_of v + number_of w::int)" +apply (induct_tac "v", simp) +apply (simp add: number_of_pred) +apply (rule allI) +apply (induct_tac "w") +apply (simp_all add: bin_add_BIT_BIT number_of_succ number_of_pred add_ac) +apply (simp add: add_left_commute [of "1::int"]) +done + + +(*Subtraction*) +lemma diff_number_of_eq: + "number_of v - number_of w = (number_of(bin_add v (bin_minus w))::int)" +apply (unfold zdiff_def) +apply (simp add: number_of_add number_of_minus) +done + +lemmas bin_mult_simps = + int_Suc0_eq_1 zmult_zminus number_of_minus number_of_add + +lemma number_of_mult: "number_of(bin_mult v w) = (number_of v * number_of w::int)" +apply (induct_tac "v") +apply (simp add: bin_mult_simps) +apply (simp add: bin_mult_simps) +apply (simp add: bin_mult_simps zadd_zmult_distrib zadd_ac) +done + + +(*The correctness of shifting. But it doesn't seem to give a measurable + speed-up.*) +lemma double_number_of_BIT: "(2::int) * number_of w = number_of (w BIT False)" +apply (induct_tac "w") +apply (simp_all add: bin_mult_simps zadd_zmult_distrib zadd_ac) +done + + +(** Converting numerals 0 and 1 to their abstract versions **) + +lemma int_numeral_0_eq_0: "Numeral0 = (0::int)" +by simp + +lemma int_numeral_1_eq_1: "Numeral1 = (1::int)" +by (simp add: int_1 int_Suc0_eq_1) + + +subsubsection{*Special Simplification for Constants*} + +text{*These distributive laws move literals inside sums and differences.*} +declare left_distrib [of _ _ "number_of v", standard, simp] +declare right_distrib [of "number_of v", standard, simp] + +declare left_diff_distrib [of _ _ "number_of v", standard, simp] +declare right_diff_distrib [of "number_of v", standard, simp] + +text{*These laws simplify inequalities, moving unary minus from a term +into the literal.*} +declare zless_zminus [of "number_of v", standard, simp] +declare zle_zminus [of "number_of v", standard, simp] +declare equation_zminus [of "number_of v", standard, simp] + +declare zminus_zless [of _ "number_of v", standard, simp] +declare zminus_zle [of _ "number_of v", standard, simp] +declare zminus_equation [of _ "number_of v", standard, simp] + +text{*These simplify inequalities where one side is the constant 1.*} +declare zless_zminus [of 1, simplified, simp] +declare zle_zminus [of 1, simplified, simp] +declare equation_zminus [of 1, simplified, simp] + +declare zminus_zless [of _ 1, simplified, simp] +declare zminus_zle [of _ 1, simplified, simp] +declare zminus_equation [of _ 1, simplified, simp] + + +(*Moving negation out of products*) +declare zmult_zminus [simp] zmult_zminus_right [simp] + +(*Cancellation of constant factors in comparisons (< and \) *) + +declare mult_less_cancel_left [of "number_of v", standard, simp] +declare mult_less_cancel_right [of _ "number_of v", standard, simp] +declare mult_le_cancel_left [of "number_of v", standard, simp] +declare mult_le_cancel_right [of _ "number_of v", standard, simp] + + +(** Special-case simplification for small constants **) + +lemma zmult_minus1 [simp]: "-1 * z = -(z::int)" +by (simp add: compare_rls int_Suc0_eq_1 zmult_zminus) + +lemma zmult_minus1_right [simp]: "z * -1 = -(z::int)" +by (subst zmult_commute, rule zmult_minus1) + + +(*Negation of a coefficient*) +lemma zminus_number_of_zmult [simp]: "- (number_of w) * z = number_of(bin_minus w) * (z::int)" +by (simp add: number_of_minus zmult_zminus) + +(*Integer unary minus for the abstract constant 1. Cannot be inserted + as a simprule until later: it is number_of_Min re-oriented!*) +lemma zminus_1_eq_m1: "- 1 = (-1::int)" +by simp + +lemma zero_less_nat_eq [simp]: "(0 < nat z) = (0 < z)" +by (cut_tac w = 0 in zless_nat_conj, auto) + + +(** Simplification rules for comparison of binary numbers (Norbert Voelker) **) + +(** Equals (=) **) + +lemma eq_number_of_eq: + "((number_of x::int) = number_of y) = + iszero (number_of (bin_add x (bin_minus y)))" +apply (unfold iszero_def) +apply (simp add: compare_rls number_of_add number_of_minus) +done + +lemma iszero_number_of_Pls: "iszero ((number_of bin.Pls)::int)" +by (unfold iszero_def, simp) + +lemma nonzero_number_of_Min: "~ iszero ((number_of bin.Min)::int)" +apply (unfold iszero_def) +apply (simp add: eq_commute) +done + +lemma iszero_number_of_BIT: + "iszero (number_of (w BIT x)) = (~x & iszero (number_of w::int))" +apply (unfold iszero_def) +apply (cases "(number_of w)::int" rule: int_cases) +apply (simp_all (no_asm_simp) add: compare_rls zero_reorient + zminus_zadd_distrib [symmetric] int_Suc0_eq_1 [symmetric] zadd_int) +done + +lemma iszero_number_of_0: "iszero (number_of (w BIT False)) = iszero (number_of w::int)" +by (simp only: iszero_number_of_BIT simp_thms) + +lemma iszero_number_of_1: "~ iszero (number_of (w BIT True)::int)" +by (simp only: iszero_number_of_BIT simp_thms) + + + +(** Less-than (<) **) + +lemma less_number_of_eq_neg: + "((number_of x::int) < number_of y) + = neg (number_of (bin_add x (bin_minus y)))" + +apply (unfold zless_def zdiff_def) +apply (simp add: bin_mult_simps) +done + +(*But if Numeral0 is rewritten to 0 then this rule can't be applied: + Numeral0 IS (number_of Pls) *) +lemma not_neg_number_of_Pls: "~ neg (number_of bin.Pls)" +by (simp add: neg_eq_less_0) + +lemma neg_number_of_Min: "neg (number_of bin.Min)" +by (simp add: neg_eq_less_0 int_0_less_1) + +lemma neg_number_of_BIT: "neg (number_of (w BIT x)) = neg (number_of w)" +apply simp +apply (cases "(number_of w)::int" rule: int_cases) +apply (simp_all (no_asm_simp) add: int_Suc0_eq_1 [symmetric] zadd_int neg_eq_less_0 zdiff_def [symmetric] compare_rls) +done + + +(** Less-than-or-equals (\) **) + +lemma le_number_of_eq_not_less: "(number_of x \ (number_of y::int)) = + (~ number_of y < (number_of x::int))" +apply (rule linorder_not_less [symmetric]) +done + +(** Absolute value (abs) **) + +lemma zabs_number_of: + "abs(number_of x::int) = + (if number_of x < (0::int) then -number_of x else number_of x)" + +apply (unfold zabs_def) +apply (rule refl) +done + +(*0 and 1 require special rewrites because they aren't numerals*) +lemma zabs_0: "abs (0::int) = 0" +by (simp add: zabs_def) + +lemma zabs_1: "abs (1::int) = 1" +by (simp del: int_0 int_1 add: int_0 [symmetric] int_1 [symmetric] zabs_def) + +(*Re-orientation of the equation nnn=x*) +lemma number_of_reorient: "(number_of w = x) = (x = number_of w)" +by auto + + +(*Delete the original rewrites, with their clumsy conditional expressions*) +declare bin_succ_BIT [simp del] bin_pred_BIT [simp del] + bin_minus_BIT [simp del] + +declare bin_add_BIT [simp del] bin_mult_BIT [simp del] +declare NCons_Pls [simp del] NCons_Min [simp del] + +(*Hide the binary representation of integer constants*) +declare number_of_Pls [simp del] number_of_Min [simp del] + number_of_BIT [simp del] + + + +(*Simplification of arithmetic operations on integer constants. + Note that bin_pred_Pls, etc. were added to the simpset by primrec.*) + +lemmas NCons_simps = NCons_Pls_0 NCons_Pls_1 NCons_Min_0 NCons_Min_1 NCons_BIT + +lemmas bin_arith_extra_simps = + number_of_add [symmetric] + number_of_minus [symmetric] zminus_1_eq_m1 + number_of_mult [symmetric] + 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 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 + of thy. Also include simp_thms, or at least (~False)=True*) +lemmas bin_arith_simps = + bin_pred_Pls bin_pred_Min + bin_succ_Pls bin_succ_Min + bin_add_Pls bin_add_Min + bin_minus_Pls bin_minus_Min + bin_mult_Pls bin_mult_Min bin_arith_extra_simps + +(*Simplification of relational operations*) +lemmas bin_rel_simps = + 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 not_neg_0 not_neg_1 not_iszero_1 + neg_number_of_Min neg_number_of_BIT + le_number_of_eq_not_less + +declare bin_arith_extra_simps [simp] +declare bin_rel_simps [simp] + + +(** Simplification of arithmetic when nested to the right **) + +lemma add_number_of_left [simp]: "number_of v + (number_of w + z) = (number_of(bin_add v w) + z::int)" +by (simp add: zadd_assoc [symmetric]) + +lemma mult_number_of_left [simp]: "number_of v * (number_of w * z) = (number_of(bin_mult v w) * z::int)" +by (simp add: zmult_assoc [symmetric]) + +lemma add_number_of_diff1: + "number_of v + (number_of w - c) = number_of(bin_add v w) - (c::int)" +apply (unfold zdiff_def) +apply (rule add_number_of_left) +done + +lemma add_number_of_diff2 [simp]: "number_of v + (c - number_of w) = + number_of (bin_add v (bin_minus w)) + (c::int)" +apply (subst diff_number_of_eq [symmetric]) +apply (simp only: compare_rls) +done + + + +(** Inserting these natural simprules earlier would break many proofs! **) + +(* int (Suc n) = 1 + int n *) +declare int_Suc [simp] + +(* Numeral0 -> 0 and Numeral1 -> 1 *) +declare int_numeral_0_eq_0 [simp] int_numeral_1_eq_1 [simp] + end diff -r 8ed6989228bb -r 5efbb548107d src/HOL/Integ/Int.thy --- a/src/HOL/Integ/Int.thy Wed Dec 03 10:49:34 2003 +0100 +++ b/src/HOL/Integ/Int.thy Thu Dec 04 10:29:17 2003 +0100 @@ -56,7 +56,7 @@ subsection{*Comparison laws*} -(*ring and field?*) +(*RING AND FIELD????????????????????????????????????????????????????????????*) lemma zminus_zless_zminus [simp]: "(- x < - y) = (y < (x::int))" by (simp add: zless_def zdiff_def zadd_ac) @@ -408,8 +408,6 @@ end; structure Int_Cancel = Abel_Cancel (Int_Cancel_Data); - -Addsimprocs [Int_Cancel.sum_conv, Int_Cancel.rel_conv]; *} @@ -427,37 +425,11 @@ done -subsection{*Inequality reasoning*} - -text{*Are they needed????*} -lemma zless_add1_eq: "(w < z + (1::int)) = (w z) = (w z) = (w w + (1::int) \ z" + proof (auto simp add: zle_def zless_iff_Suc_zadd) + fix m n + assume "w + 1 = w + (1 + int m) + (1 + int n)" + hence "(w + 1) + (1 + int (m + n)) = (w + 1) + 0" + by (simp add: add_ac zadd_int [symmetric]) + hence "int (Suc(m+n)) = 0" + by (simp only: Ring_and_Field.add_left_cancel int_Suc) + thus False by (simp only: int_eq_0_conv) + qed + use "int_arith1.ML" setup int_arith_setup -lemma zle_diff1_eq [simp]: "(w <= z - (1::int)) = (w<(z::int))" +subsection{*More inequality reasoning*} + +lemma zless_add1_eq: "(w < z + (1::int)) = (w z) = (w z - (1::int)) = (w<(z::int))" +by arith + +lemma zle_add1_eq_le [simp]: "(w < z + 1) = (w\(z::int))" by arith lemma zadd_left_cancel0 [simp]: "(z = z + w) = (w = (0::int))" @@ -22,22 +43,22 @@ subsection{*Results about @{term nat}*} -lemma nonneg_eq_int: "[| 0 <= z; !!m. z = int m ==> P |] ==> P" +lemma nonneg_eq_int: "[| 0 \ z; !!m. z = int m ==> P |] ==> P" by (blast dest: nat_0_le sym) -lemma nat_eq_iff: "(nat w = m) = (if 0 <= w then w = int m else m=0)" +lemma nat_eq_iff: "(nat w = m) = (if 0 \ w then w = int m else m=0)" by auto -lemma nat_eq_iff2: "(m = nat w) = (if 0 <= w then w = int m else m=0)" +lemma nat_eq_iff2: "(m = nat w) = (if 0 \ w then w = int m else m=0)" by auto -lemma nat_less_iff: "0 <= w ==> (nat w < m) = (w < int m)" +lemma nat_less_iff: "0 \ w ==> (nat w < m) = (w < int m)" apply (rule iffI) apply (erule nat_0_le [THEN subst]) apply (simp_all del: zless_int add: zless_int [symmetric]) done -lemma int_eq_iff: "(int m = z) = (m = nat z & 0 <= z)" +lemma int_eq_iff: "(int m = z) = (m = nat z & 0 \ z)" by (auto simp add: nat_eq_iff2) @@ -57,13 +78,13 @@ lemma nat_2: "nat 2 = Suc (Suc 0)" by (subst nat_eq_iff, simp) -lemma nat_less_eq_zless: "0 <= w ==> (nat w < nat z) = (w w ==> (nat w < nat z) = (w (nat w <= nat z) = (w<=z)" +lemma nat_le_eq_zle: "0 < w | 0 \ z ==> (nat w \ nat z) = (w\z)" by (auto simp add: linorder_not_less [symmetric] zless_nat_conj) subsection{*@{term abs}: Absolute Value, as an Integer*} @@ -72,10 +93,10 @@ but arith_tac is not parameterized by such simp rules *) -lemma zabs_split: "P(abs(i::int)) = ((0 <= i --> P i) & (i < 0 --> P(-i)))" +lemma zabs_split: "P(abs(i::int)) = ((0 \ i --> P i) & (i < 0 --> P(-i)))" by (simp add: zabs_def) -lemma zero_le_zabs [iff]: "0 <= abs (z::int)" +lemma zero_le_zabs [iff]: "0 \ abs (z::int)" by (simp add: zabs_def) @@ -86,7 +107,7 @@ declare zabs_split [arith_split] lemma zabs_eq_iff: - "(abs (z::int) = w) = (z = w \ 0 <= z \ z = -w \ z < 0)" + "(abs (z::int) = w) = (z = w \ 0 \ z \ z = -w \ z < 0)" by (auto simp add: zabs_def) lemma int_nat_eq [simp]: "int (nat z) = (if 0 \ z then z else 0)" @@ -117,7 +138,7 @@ step: "\i. \k \ i; P i\ \ P(i+1)" shows "P i" proof - - { fix n have "\i::int. n = nat(i-k) \ k <= i \ P i" + { fix n have "\i::int. n = nat(i-k) \ k \ i \ P i" proof (induct n) case 0 hence "i = k" by arith @@ -153,7 +174,7 @@ step: "\i. \i \ k; P i\ \ P(i - 1)" shows "P i" proof - - { fix n have "\i::int. n = nat(k-i) \ i <= k \ P i" + { fix n have "\i::int. n = nat(k-i) \ i \ k \ P i" proof (induct n) case 0 hence "i = k" by arith @@ -193,7 +214,7 @@ lemma abs_minus [simp]: "abs(-(x::int)) = abs(x)" by arith -lemma triangle_ineq: "abs(x+y) <= abs(x) + abs(y::int)" +lemma triangle_ineq: "abs(x+y) \ abs(x) + abs(y::int)" by arith diff -r 8ed6989228bb -r 5efbb548107d src/HOL/Integ/NatBin.thy --- a/src/HOL/Integ/NatBin.thy Wed Dec 03 10:49:34 2003 +0100 +++ b/src/HOL/Integ/NatBin.thy Thu Dec 04 10:29:17 2003 +0100 @@ -6,20 +6,516 @@ header {* Binary arithmetic for the natural numbers *} -theory NatBin = IntPower -files ("nat_bin.ML"): +theory NatBin = IntPower: text {* This case is simply reduced to that for the non-negative integers. *} - instance nat :: number .. defs (overloaded) nat_number_of_def: "(number_of::bin => nat) v == nat ((number_of :: bin => int) v)" -use "nat_bin.ML" + +(** nat (coercion from int to nat) **) + +lemma nat_number_of: "nat (number_of w) = number_of w" +apply (simp (no_asm) add: nat_number_of_def) +done +declare nat_number_of [simp] nat_0 [simp] nat_1 [simp] + +lemma numeral_0_eq_0: "Numeral0 = (0::nat)" +apply (simp (no_asm) add: nat_number_of_def) +done + +lemma numeral_1_eq_1: "Numeral1 = (1::nat)" +apply (simp (no_asm) add: nat_1 nat_number_of_def) +done + +lemma numeral_1_eq_Suc_0: "Numeral1 = Suc 0" +apply (simp (no_asm) add: numeral_1_eq_1) +done + +lemma numeral_2_eq_2: "2 = Suc (Suc 0)" +apply (unfold nat_number_of_def) +apply (rule nat_2) +done + + +(** Distributive laws for "nat". The others are in IntArith.ML, but these + require div and mod to be defined for type "int". They also need + some of the lemmas proved just above.**) + +lemma nat_div_distrib: "(0::int) <= z ==> nat (z div z') = nat z div nat z'" +apply (case_tac "0 <= z'") +apply (auto simp add: div_nonneg_neg_le0 DIVISION_BY_ZERO_DIV) +apply (case_tac "z' = 0" , simp (no_asm_simp) add: DIVISION_BY_ZERO) +apply (auto elim!: nonneg_eq_int) +apply (rename_tac m m') +apply (subgoal_tac "0 <= int m div int m'") + prefer 2 apply (simp add: numeral_0_eq_0 pos_imp_zdiv_nonneg_iff) +apply (rule inj_int [THEN injD]) +apply (simp (no_asm_simp)) +apply (rule_tac r = "int (m mod m') " in quorem_div) + prefer 2 apply (force) +apply (simp add: nat_less_iff [symmetric] quorem_def numeral_0_eq_0 zadd_int zmult_int) +done + +(*Fails if z'<0: the LHS collapses to (nat z) but the RHS doesn't*) +lemma nat_mod_distrib: "[| (0::int) <= z; 0 <= z' |] ==> nat (z mod z') = nat z mod nat z'" +apply (case_tac "z' = 0" , simp (no_asm_simp) add: DIVISION_BY_ZERO) +apply (auto elim!: nonneg_eq_int) +apply (rename_tac m m') +apply (subgoal_tac "0 <= int m mod int m'") + prefer 2 apply (simp add: nat_less_iff numeral_0_eq_0 pos_mod_sign) +apply (rule inj_int [THEN injD]) +apply (simp (no_asm_simp)) +apply (rule_tac q = "int (m div m') " in quorem_mod) + prefer 2 apply (force) +apply (simp add: nat_less_iff [symmetric] quorem_def numeral_0_eq_0 zadd_int zmult_int) +done + + +(** int (coercion from nat to int) **) + +(*"neg" is used in rewrite rules for binary comparisons*) +lemma int_nat_number_of: "int (number_of v :: nat) = + (if neg (number_of v) then 0 + else (number_of v :: int))" +by (simp del: nat_number_of + add: neg_nat nat_number_of_def not_neg_nat add_assoc) +declare int_nat_number_of [simp] + + +(** Successor **) + +lemma Suc_nat_eq_nat_zadd1: "(0::int) <= z ==> Suc (nat z) = nat (1 + z)" +apply (rule sym) +apply (simp (no_asm_simp) add: nat_eq_iff int_Suc) +done + +lemma Suc_nat_number_of_add: "Suc (number_of v + n) = + (if neg (number_of v) then 1+n else number_of (bin_succ v) + n)" +by (simp del: nat_number_of + add: nat_number_of_def neg_nat + Suc_nat_eq_nat_zadd1 number_of_succ) + +lemma Suc_nat_number_of: "Suc (number_of v) = + (if neg (number_of v) then 1 else number_of (bin_succ v))" +apply (cut_tac n = "0" in Suc_nat_number_of_add) +apply (simp cong del: if_weak_cong) +done +declare Suc_nat_number_of [simp] + + +(** Addition **) + +(*"neg" is used in rewrite rules for binary comparisons*) +lemma add_nat_number_of: "(number_of v :: nat) + number_of v' = + (if neg (number_of v) then number_of v' + else if neg (number_of v') then number_of v + else number_of (bin_add v v'))" +by (force dest!: neg_nat + simp del: nat_number_of + simp add: nat_number_of_def nat_add_distrib [symmetric]) + +declare add_nat_number_of [simp] + + +(** Subtraction **) + +lemma diff_nat_eq_if: "nat z - nat z' = + (if neg z' then nat z + else let d = z-z' in + if neg d then 0 else nat d)" +apply (simp (no_asm) add: Let_def nat_diff_distrib [symmetric] neg_eq_less_0 not_neg_eq_ge_0) +apply (simp (no_asm) add: diff_is_0_eq nat_le_eq_zle) +done + +lemma diff_nat_number_of: + "(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 0 else nat d)" +by (simp del: nat_number_of add: diff_nat_eq_if nat_number_of_def) + +declare diff_nat_number_of [simp] + + +(** Multiplication **) + +lemma mult_nat_number_of: "(number_of v :: nat) * number_of v' = + (if neg (number_of v) then 0 else number_of (bin_mult v v'))" +by (force dest!: neg_nat + simp del: nat_number_of + simp add: nat_number_of_def nat_mult_distrib [symmetric]) + +declare mult_nat_number_of [simp] + + +(** Quotient **) + +lemma div_nat_number_of: "(number_of v :: nat) div number_of v' = + (if neg (number_of v) then 0 + else nat (number_of v div number_of v'))" +by (force dest!: neg_nat + simp del: nat_number_of + simp add: nat_number_of_def nat_div_distrib [symmetric]) + +declare div_nat_number_of [simp] + + +(** Remainder **) + +lemma mod_nat_number_of: "(number_of v :: nat) mod number_of v' = + (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 (force dest!: neg_nat + simp del: nat_number_of + simp add: nat_number_of_def nat_mod_distrib [symmetric]) + +declare mod_nat_number_of [simp] + +ML +{* +val nat_number_of_def = thm"nat_number_of_def"; + +val nat_number_of = thm"nat_number_of"; +val numeral_0_eq_0 = thm"numeral_0_eq_0"; +val numeral_1_eq_1 = thm"numeral_1_eq_1"; +val numeral_1_eq_Suc_0 = thm"numeral_1_eq_Suc_0"; +val numeral_2_eq_2 = thm"numeral_2_eq_2"; +val nat_div_distrib = thm"nat_div_distrib"; +val nat_mod_distrib = thm"nat_mod_distrib"; +val int_nat_number_of = thm"int_nat_number_of"; +val Suc_nat_eq_nat_zadd1 = thm"Suc_nat_eq_nat_zadd1"; +val Suc_nat_number_of_add = thm"Suc_nat_number_of_add"; +val Suc_nat_number_of = thm"Suc_nat_number_of"; +val add_nat_number_of = thm"add_nat_number_of"; +val diff_nat_eq_if = thm"diff_nat_eq_if"; +val diff_nat_number_of = thm"diff_nat_number_of"; +val mult_nat_number_of = thm"mult_nat_number_of"; +val div_nat_number_of = thm"div_nat_number_of"; +val mod_nat_number_of = thm"mod_nat_number_of"; +*} + + +ML +{* +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_novars + 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", ["(Suc 0) div m"], NatAbstractNumerals.proc div_nat_number_of), + ("nat_mod_eval_numerals", ["(Suc 0) mod m"], NatAbstractNumerals.proc mod_nat_number_of)]; + +Addsimprocs nat_eval_numerals; +*} + +(*** Comparisons ***) + +(** Equals (=) **) + +lemma eq_nat_nat_iff: "[| (0::int) <= z; 0 <= z' |] ==> (nat z = nat z') = (z=z')" +apply (auto elim!: nonneg_eq_int) +done + +(*"neg" is used in rewrite rules for binary comparisons*) +lemma eq_nat_number_of: "((number_of v :: nat) = number_of v') = + (if neg (number_of v) then (iszero (number_of v') | neg (number_of v')) + else if neg (number_of v') then iszero (number_of v) + else iszero (number_of (bin_add v (bin_minus v'))))" +apply (simp only: simp_thms neg_nat not_neg_eq_ge_0 nat_number_of_def + eq_nat_nat_iff eq_number_of_eq nat_0 iszero_def + split add: split_if cong add: imp_cong); +apply (simp only: nat_eq_iff nat_eq_iff2) +apply (simp add: not_neg_eq_ge_0 [symmetric]) +done + +declare eq_nat_number_of [simp] + +(** Less-than (<) **) + +(*"neg" is used in rewrite rules for binary comparisons*) +lemma less_nat_number_of: "((number_of v :: nat) < number_of v') = + (if neg (number_of v) then neg (number_of (bin_minus v')) + else neg (number_of (bin_add v (bin_minus v'))))" +apply (simp only: simp_thms neg_nat not_neg_eq_ge_0 nat_number_of_def + nat_less_eq_zless less_number_of_eq_neg zless_nat_eq_int_zless + cong add: imp_cong); +apply (simp add: ); +done + +declare less_nat_number_of [simp] + + +(** Less-than-or-equals (<=) **) + +lemma le_nat_number_of_eq_not_less: "(number_of x <= (number_of y::nat)) = + (~ number_of y < (number_of x::nat))" +apply (rule linorder_not_less [symmetric]) +done + +declare le_nat_number_of_eq_not_less [simp] + + +(*Maps #n to n for n = 0, 1, 2*) +lemmas numerals = numeral_0_eq_0 numeral_1_eq_1 numeral_2_eq_2 + + +(** Nat **) + +lemma Suc_pred': "0 < n ==> n = Suc(n - 1)" +apply (simp add: numerals) +done + +(*Expresses a natural number constant as the Suc of another one. + NOT suitable for rewriting because n recurs in the condition.*) +lemmas expand_Suc = Suc_pred' [of "number_of v", standard] + +(** Arith **) + +lemma Suc_eq_add_numeral_1: "Suc n = n + 1" +apply (simp add: numerals) +done + +(* These two can be useful when m = number_of... *) + +lemma add_eq_if: "(m::nat) + n = (if m=0 then n else Suc ((m - 1) + n))" +apply (case_tac "m") +apply (simp_all add: numerals) +done + +lemma mult_eq_if: "(m::nat) * n = (if m=0 then 0 else n + ((m - 1) * n))" +apply (case_tac "m") +apply (simp_all add: numerals) +done + +lemma power_eq_if: "(p ^ m :: nat) = (if m=0 then 1 else p * (p ^ (m - 1)))" +apply (case_tac "m") +apply (simp_all add: numerals) +done + +lemma diff_less': "[| 0 m - n < (m::nat)" +apply (simp add: diff_less numerals) +done + +declare diff_less' [of "number_of v", standard, simp] + +(** Power **) + +lemma power_two: "(p::nat) ^ 2 = p*p" +apply (simp add: numerals) +done + + +(*** Comparisons involving (0::nat) ***) + +lemma eq_number_of_0: "(number_of v = (0::nat)) = + (if neg (number_of v) then True else iszero (number_of v))" +apply (simp (no_asm) add: numeral_0_eq_0 [symmetric] iszero_0) +done + +lemma eq_0_number_of: "((0::nat) = number_of v) = + (if neg (number_of v) then True else iszero (number_of v))" +apply (rule trans [OF eq_sym_conv eq_number_of_0]) +done + +lemma less_0_number_of: "((0::nat) < number_of v) = neg (number_of (bin_minus v))" +apply (simp (no_asm) add: numeral_0_eq_0 [symmetric]) +done + +(*Simplification already handles n<0, n<=0 and 0<=n.*) +declare eq_number_of_0 [simp] eq_0_number_of [simp] less_0_number_of [simp] + +lemma neg_imp_number_of_eq_0: "neg (number_of v) ==> number_of v = (0::nat)" +apply (simp (no_asm_simp) add: numeral_0_eq_0 [symmetric] iszero_0) +done + + + +(*** Comparisons involving Suc ***) + +lemma eq_number_of_Suc [simp]: "(number_of v = Suc n) = + (let pv = number_of (bin_pred v) in + if neg pv then False else nat pv = n)" +apply (simp only: simp_thms Let_def neg_eq_less_0 linorder_not_less + number_of_pred nat_number_of_def + split add: split_if); +apply (rule_tac x = "number_of v" in spec) +apply (auto simp add: nat_eq_iff) +done + +lemma Suc_eq_number_of [simp]: "(Suc n = number_of v) = + (let pv = number_of (bin_pred v) in + if neg pv then False else nat pv = n)" +apply (rule trans [OF eq_sym_conv eq_number_of_Suc]) +done + +lemma less_number_of_Suc [simp]: "(number_of v < Suc n) = + (let pv = number_of (bin_pred v) in + if neg pv then True else nat pv < n)" +apply (simp only: simp_thms Let_def neg_eq_less_0 linorder_not_less + number_of_pred nat_number_of_def + split add: split_if); +apply (rule_tac x = "number_of v" in spec) +apply (auto simp add: nat_less_iff) +done + +lemma less_Suc_number_of [simp]: "(Suc n < number_of v) = + (let pv = number_of (bin_pred v) in + if neg pv then False else n < nat pv)" +apply (simp only: simp_thms Let_def neg_eq_less_0 linorder_not_less + number_of_pred nat_number_of_def + split add: split_if); +apply (rule_tac x = "number_of v" in spec) +apply (auto simp add: zless_nat_eq_int_zless) +done + +lemma le_number_of_Suc [simp]: "(number_of v <= Suc n) = + (let pv = number_of (bin_pred v) in + if neg pv then True else nat pv <= n)" +apply (simp (no_asm) add: Let_def less_Suc_number_of linorder_not_less [symmetric]) +done + +lemma le_Suc_number_of [simp]: "(Suc n <= number_of v) = + (let pv = number_of (bin_pred v) in + if neg pv then False else n <= nat pv)" +apply (simp (no_asm) add: Let_def less_number_of_Suc linorder_not_less [symmetric]) +done + + +(* Push int(.) inwards: *) +declare zadd_int [symmetric, simp] + +lemma lemma1: "(m+m = n+n) = (m = (n::int))" +apply auto +done + +lemma lemma2: "m+m ~= (1::int) + (n + n)" +apply auto +apply (drule_tac f = "%x. x mod 2" in arg_cong) +apply (simp (no_asm_use) add: zmod_zadd1_eq) +done + +lemma eq_number_of_BIT_BIT: "((number_of (v BIT x) ::int) = number_of (w BIT y)) = + (x=y & (((number_of v) ::int) = number_of w))" +by (simp only: simp_thms number_of_BIT lemma1 lemma2 eq_commute + Ring_and_Field.add_left_cancel add_assoc left_zero + split add: split_if cong: imp_cong); + + +lemma eq_number_of_BIT_Pls: "((number_of (v BIT x) ::int) = number_of bin.Pls) = + (x=False & (((number_of v) ::int) = number_of bin.Pls))" +apply (simp only: simp_thms add: number_of_BIT number_of_Pls eq_commute + split add: split_if cong: imp_cong) +apply (rule_tac x = "number_of v" in spec) +apply safe +apply (simp_all (no_asm_use)) +apply (drule_tac f = "%x. x mod 2" in arg_cong) +apply (simp (no_asm_use) add: zmod_zadd1_eq) +done + +lemma eq_number_of_BIT_Min: "((number_of (v BIT x) ::int) = number_of bin.Min) = + (x=True & (((number_of v) ::int) = number_of bin.Min))" +apply (simp only: simp_thms add: number_of_BIT number_of_Min eq_commute + split add: split_if cong: imp_cong) +apply (rule_tac x = "number_of v" in spec) +apply auto +apply (drule_tac f = "%x. x mod 2" in arg_cong) +apply auto +done + +lemma eq_number_of_Pls_Min: "(number_of bin.Pls ::int) ~= number_of bin.Min" +apply auto +done + + + +(*** Literal arithmetic involving powers, type nat ***) + +lemma nat_power_eq: "(0::int) <= z ==> nat (z^n) = nat z ^ n" +apply (induct_tac "n") +apply (simp_all (no_asm_simp) add: nat_mult_distrib) +done + +lemma power_nat_number_of: "(number_of v :: nat) ^ n = + (if neg (number_of v) then 0^n else nat ((number_of v :: int) ^ n))" +by (simp only: simp_thms neg_nat not_neg_eq_ge_0 nat_number_of_def nat_power_eq + split add: split_if cong: imp_cong) + + +declare power_nat_number_of [of _ "number_of w", standard, simp] + + + +(*** Literal arithmetic involving powers, type int ***) + +lemma zpower_even: "(z::int) ^ (2*a) = (z^a)^2" +apply (simp (no_asm) add: zpower_zpower mult_commute) +done + +lemma zpower_two: "(p::int) ^ 2 = p*p" +apply (simp add: numerals) +done + +lemma zpower_odd: "(z::int) ^ (2*a + 1) = z * (z^a)^2" +apply (simp (no_asm) add: zpower_even zpower_zadd_distrib) +done + +lemma zpower_number_of_even: "(z::int) ^ number_of (w BIT False) = + (let w = z ^ (number_of w) in w*w)" +apply (simp del: nat_number_of add: nat_number_of_def number_of_BIT Let_def) +apply (simp only: number_of_add) +apply (rule_tac x = "number_of w" in spec , clarify) +apply (case_tac " (0::int) <= x") +apply (auto simp add: nat_mult_distrib zpower_even zpower_two) +done + +lemma zpower_number_of_odd: "(z::int) ^ number_of (w BIT True) = + (if (0::int) <= number_of w + then (let w = z ^ (number_of w) in z*w*w) + else 1)" +apply (simp del: nat_number_of add: nat_number_of_def number_of_BIT Let_def) +apply (simp only: number_of_add int_numeral_1_eq_1 not_neg_eq_ge_0 neg_eq_less_0) +apply (rule_tac x = "number_of w" in spec , clarify) +apply (auto simp add: nat_add_distrib nat_mult_distrib zpower_even zpower_two neg_nat) +done + +declare zpower_number_of_even [of "number_of v", standard, simp] +declare zpower_number_of_odd [of "number_of v", standard, simp] + + + +ML +{* +val numerals = thms"numerals"; +val numeral_ss = simpset() addsimps numerals; + +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 [Suc_nat_number_of, int_nat_number_of, + not_neg_number_of_Pls, + neg_number_of_Min,neg_number_of_BIT]})] +*} + setup nat_bin_arith_setup (* Enable arith to deal with div/mod k where k is a numeral: *) @@ -64,6 +560,52 @@ by (simp add: Let_def) +subsection {*More ML Bindings*} + +ML +{* +val eq_nat_nat_iff = thm"eq_nat_nat_iff"; +val eq_nat_number_of = thm"eq_nat_number_of"; +val less_nat_number_of = thm"less_nat_number_of"; +val le_nat_number_of_eq_not_less = thm"le_nat_number_of_eq_not_less"; +val Suc_pred' = thm"Suc_pred'"; +val expand_Suc = thm"expand_Suc"; +val Suc_eq_add_numeral_1 = thm"Suc_eq_add_numeral_1"; +val add_eq_if = thm"add_eq_if"; +val mult_eq_if = thm"mult_eq_if"; +val power_eq_if = thm"power_eq_if"; +val diff_less' = thm"diff_less'"; +val power_two = thm"power_two"; +val eq_number_of_0 = thm"eq_number_of_0"; +val eq_0_number_of = thm"eq_0_number_of"; +val less_0_number_of = thm"less_0_number_of"; +val neg_imp_number_of_eq_0 = thm"neg_imp_number_of_eq_0"; +val eq_number_of_Suc = thm"eq_number_of_Suc"; +val Suc_eq_number_of = thm"Suc_eq_number_of"; +val less_number_of_Suc = thm"less_number_of_Suc"; +val less_Suc_number_of = thm"less_Suc_number_of"; +val le_number_of_Suc = thm"le_number_of_Suc"; +val le_Suc_number_of = thm"le_Suc_number_of"; +val eq_number_of_BIT_BIT = thm"eq_number_of_BIT_BIT"; +val eq_number_of_BIT_Pls = thm"eq_number_of_BIT_Pls"; +val eq_number_of_BIT_Min = thm"eq_number_of_BIT_Min"; +val eq_number_of_Pls_Min = thm"eq_number_of_Pls_Min"; +val nat_power_eq = thm"nat_power_eq"; +val power_nat_number_of = thm"power_nat_number_of"; +val zpower_even = thm"zpower_even"; +val zpower_two = thm"zpower_two"; +val zpower_odd = thm"zpower_odd"; +val zpower_number_of_even = thm"zpower_number_of_even"; +val zpower_number_of_odd = thm"zpower_number_of_odd"; +val nat_number_of_Pls = thm"nat_number_of_Pls"; +val nat_number_of_Min = thm"nat_number_of_Min"; +val nat_number_of_BIT_True = thm"nat_number_of_BIT_True"; +val nat_number_of_BIT_False = thm"nat_number_of_BIT_False"; +val Let_Suc = thm"Let_Suc"; + +val nat_number = thms"nat_number"; +*} + subsection {* Configuration of the code generator *} ML {* diff -r 8ed6989228bb -r 5efbb548107d src/HOL/Integ/NatSimprocs.ML --- a/src/HOL/Integ/NatSimprocs.ML Wed Dec 03 10:49:34 2003 +0100 +++ b/src/HOL/Integ/NatSimprocs.ML Thu Dec 04 10:29:17 2003 +0100 @@ -6,6 +6,8 @@ Simprocs for nat numerals (see also nat_simprocs.ML). *) +val ss_Int = simpset_of Int_thy; + (** For simplifying Suc m - #n **) Goal "Numeral0 < n ==> Suc m - n = m - (n - Numeral1)"; diff -r 8ed6989228bb -r 5efbb548107d src/HOL/Integ/int_arith1.ML --- a/src/HOL/Integ/int_arith1.ML Wed Dec 03 10:49:34 2003 +0100 +++ b/src/HOL/Integ/int_arith1.ML Thu Dec 04 10:29:17 2003 +0100 @@ -5,74 +5,184 @@ Simprocs and decision procedure for linear arithmetic. *) -val zadd_ac = thms "Ring_and_Field.add_ac"; -val zmult_ac = thms "Ring_and_Field.mult_ac"; - - -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 < (0::int))"; -by (simp_tac (simpset() addsimps compare_rls) 1); -qed "zless_iff_zdiff_zless_0"; +val NCons_Pls = thm"NCons_Pls"; +val NCons_Min = thm"NCons_Min"; +val NCons_BIT = thm"NCons_BIT"; +val number_of_Pls = thm"number_of_Pls"; +val number_of_Min = thm"number_of_Min"; +val number_of_BIT = thm"number_of_BIT"; +val bin_succ_Pls = thm"bin_succ_Pls"; +val bin_succ_Min = thm"bin_succ_Min"; +val bin_succ_BIT = thm"bin_succ_BIT"; +val bin_pred_Pls = thm"bin_pred_Pls"; +val bin_pred_Min = thm"bin_pred_Min"; +val bin_pred_BIT = thm"bin_pred_BIT"; +val bin_minus_Pls = thm"bin_minus_Pls"; +val bin_minus_Min = thm"bin_minus_Min"; +val bin_minus_BIT = thm"bin_minus_BIT"; +val bin_add_Pls = thm"bin_add_Pls"; +val bin_add_Min = thm"bin_add_Min"; +val bin_mult_Pls = thm"bin_mult_Pls"; +val bin_mult_Min = thm"bin_mult_Min"; +val bin_mult_BIT = thm"bin_mult_BIT"; -Goal "(x = y) = (x-y = (0::int))"; -by (simp_tac (simpset() addsimps compare_rls) 1); -qed "eq_iff_zdiff_eq_0"; +val zadd_ac = thms "Ring_and_Field.add_ac" +val zmult_ac = thms "Ring_and_Field.mult_ac" +val NCons_Pls_0 = thm"NCons_Pls_0"; +val NCons_Pls_1 = thm"NCons_Pls_1"; +val NCons_Min_0 = thm"NCons_Min_0"; +val NCons_Min_1 = thm"NCons_Min_1"; +val bin_succ_1 = thm"bin_succ_1"; +val bin_succ_0 = thm"bin_succ_0"; +val bin_pred_1 = thm"bin_pred_1"; +val bin_pred_0 = thm"bin_pred_0"; +val bin_minus_1 = thm"bin_minus_1"; +val bin_minus_0 = thm"bin_minus_0"; +val bin_add_BIT_11 = thm"bin_add_BIT_11"; +val bin_add_BIT_10 = thm"bin_add_BIT_10"; +val bin_add_BIT_0 = thm"bin_add_BIT_0"; +val bin_add_Pls_right = thm"bin_add_Pls_right"; +val bin_add_Min_right = thm"bin_add_Min_right"; +val bin_add_BIT_BIT = thm"bin_add_BIT_BIT"; +val bin_mult_1 = thm"bin_mult_1"; +val bin_mult_0 = thm"bin_mult_0"; +val number_of_NCons = thm"number_of_NCons"; +val number_of_succ = thm"number_of_succ"; +val number_of_pred = thm"number_of_pred"; +val number_of_minus = thm"number_of_minus"; +val number_of_add = thm"number_of_add"; +val diff_number_of_eq = thm"diff_number_of_eq"; +val number_of_mult = thm"number_of_mult"; +val double_number_of_BIT = thm"double_number_of_BIT"; +val int_numeral_0_eq_0 = thm"int_numeral_0_eq_0"; +val int_numeral_1_eq_1 = thm"int_numeral_1_eq_1"; +val zmult_minus1 = thm"zmult_minus1"; +val zmult_minus1_right = thm"zmult_minus1_right"; +val zminus_number_of_zmult = thm"zminus_number_of_zmult"; +val zminus_1_eq_m1 = thm"zminus_1_eq_m1"; +val zero_less_nat_eq = thm"zero_less_nat_eq"; +val eq_number_of_eq = thm"eq_number_of_eq"; +val iszero_number_of_Pls = thm"iszero_number_of_Pls"; +val nonzero_number_of_Min = thm"nonzero_number_of_Min"; +val iszero_number_of_BIT = thm"iszero_number_of_BIT"; +val iszero_number_of_0 = thm"iszero_number_of_0"; +val iszero_number_of_1 = thm"iszero_number_of_1"; +val less_number_of_eq_neg = thm"less_number_of_eq_neg"; +val not_neg_number_of_Pls = thm"not_neg_number_of_Pls"; +val neg_number_of_Min = thm"neg_number_of_Min"; +val neg_number_of_BIT = thm"neg_number_of_BIT"; +val le_number_of_eq_not_less = thm"le_number_of_eq_not_less"; +val zabs_number_of = thm"zabs_number_of"; +val zabs_0 = thm"zabs_0"; +val zabs_1 = thm"zabs_1"; +val number_of_reorient = thm"number_of_reorient"; +val add_number_of_left = thm"add_number_of_left"; +val mult_number_of_left = thm"mult_number_of_left"; +val add_number_of_diff1 = thm"add_number_of_diff1"; +val add_number_of_diff2 = thm"add_number_of_diff2"; +val less_iff_diff_less_0 = thm"less_iff_diff_less_0"; +val eq_iff_diff_eq_0 = thm"eq_iff_diff_eq_0"; +val le_iff_diff_le_0 = thm"le_iff_diff_le_0"; -Goal "(x <= y) = (x-y <= (0::int))"; -by (simp_tac (simpset() addsimps compare_rls) 1); -qed "zle_iff_zdiff_zle_0"; +val bin_mult_simps = thms"bin_mult_simps"; +val NCons_simps = thms"NCons_simps"; +val bin_arith_extra_simps = thms"bin_arith_extra_simps"; +val bin_arith_simps = thms"bin_arith_simps"; +val bin_rel_simps = thms"bin_rel_simps"; +val zless_imp_add1_zle = thm "zless_imp_add1_zle"; -(** For combine_numerals **) - -Goal "i*u + (j*u + k) = (i+j)*u + (k::int)"; -by (asm_simp_tac (simpset() addsimps [zadd_zmult_distrib]) 1); -qed "left_zadd_zmult_distrib"; +val combine_common_factor = thm"combine_common_factor"; +val eq_add_iff1 = thm"eq_add_iff1"; +val eq_add_iff2 = thm"eq_add_iff2"; +val less_add_iff1 = thm"less_add_iff1"; +val less_add_iff2 = thm"less_add_iff2"; +val le_add_iff1 = thm"le_add_iff1"; +val le_add_iff2 = thm"le_add_iff2"; -(** For cancel_numerals **) +structure Bin_Simprocs = + struct + fun prove_conv tacs sg (hyps: thm list) xs (t, u) = + if t aconv u then None + else + let val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u)) + in Some (Tactic.prove sg xs [] eq (K (EVERY tacs))) end -val rel_iff_rel_0_rls = map (inst "y" "?u+?v") - [zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0, - zle_iff_zdiff_zle_0] @ - map (inst "y" "n") - [zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0, - zle_iff_zdiff_zle_0]; + fun prove_conv_nohyps tacs sg = prove_conv tacs sg []; + fun prove_conv_nohyps_novars tacs sg = prove_conv tacs sg [] []; + + fun prep_simproc (name, pats, proc) = + Simplifier.simproc (Theory.sign_of (the_context())) name pats proc; + + fun is_numeral (Const("Numeral.number_of", _) $ w) = true + | is_numeral _ = false -Goal "!!i::int. (i*u + m = j*u + n) = ((i-j)*u + m = n)"; -by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@ - zadd_ac@rel_iff_rel_0_rls) 1); -qed "eq_add_iff1"; + fun simplify_meta_eq f_number_of_eq f_eq = + mk_meta_eq ([f_eq, f_number_of_eq] MRS trans) -Goal "!!i::int. (i*u + m = j*u + n) = (m = (j-i)*u + n)"; -by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@ - zadd_ac@rel_iff_rel_0_rls) 1); -qed "eq_add_iff2"; + 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_novars + fun norm_tac simps = ALLGOALS (simp_tac (HOL_ss addsimps simps)) + val simplify_meta_eq = simplify_meta_eq + end + + structure IntAbstractNumerals = AbstractNumeralsFun (IntAbstractNumeralsData) + -Goal "!!i::int. (i*u + m < j*u + n) = ((i-j)*u + m < n)"; -by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@ - zadd_ac@rel_iff_rel_0_rls) 1); -qed "less_add_iff1"; - -Goal "!!i::int. (i*u + m < j*u + n) = (m < (j-i)*u + n)"; -by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@ - zadd_ac@rel_iff_rel_0_rls) 1); -qed "less_add_iff2"; + (*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", + ["(m::int) + 1", "(m::int) + number_of v"], + IntAbstractNumerals.proc (number_of_add RS sym)), + ("int_diff_eval_numerals", + ["(m::int) - 1", "(m::int) - number_of v"], + IntAbstractNumerals.proc diff_number_of_eq), + ("int_eq_eval_numerals", + ["(m::int) = 0", "(m::int) = 1", "(m::int) = number_of v"], + IntAbstractNumerals.proc eq_number_of_eq), + ("int_less_eval_numerals", + ["(m::int) < 0", "(m::int) < 1", "(m::int) < number_of v"], + IntAbstractNumerals.proc less_number_of_eq_neg), + ("int_le_eval_numerals", + ["(m::int) <= 0", "(m::int) <= 1", "(m::int) <= number_of v"], + IntAbstractNumerals.proc le_number_of_eq_not_less)] -Goal "!!i::int. (i*u + m <= j*u + n) = ((i-j)*u + m <= n)"; -by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@ - zadd_ac@rel_iff_rel_0_rls) 1); -qed "le_add_iff1"; + (*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 -Goal "!!i::int. (i*u + m <= j*u + n) = (m <= (j-i)*u + n)"; -by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib] - @zadd_ac@rel_iff_rel_0_rls) 1); -qed "le_add_iff2"; + (*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", ["0=x", "1=x", "number_of w = x"], reorient_proc) + + end; + + +Addsimprocs Bin_Simprocs.eval_numerals; +Addsimprocs [Bin_Simprocs.reorient_simproc]; structure Int_Numeral_Simprocs = @@ -285,7 +395,7 @@ val dest_sum = dest_sum val mk_coeff = mk_coeff val dest_coeff = dest_coeff 1 - val left_distrib = left_zadd_zmult_distrib RS trans + val left_distrib = combine_common_factor RS trans val prove_conv = Bin_Simprocs.prove_conv_nohyps val trans_tac = trans_tac val norm_tac = @@ -436,7 +546,7 @@ {add_mono_thms = add_mono_thms @ add_mono_thms_int, mult_mono_thms = mult_mono_thms, inj_thms = [zle_int RS iffD2,int_int_eq RS iffD2] @ inj_thms, - lessD = lessD @ [add1_zle_eq RS iffD2], + lessD = lessD @ [zless_imp_add1_zle], simpset = simpset addsimps add_rules addsimprocs simprocs addcongs [if_weak_cong]}), diff -r 8ed6989228bb -r 5efbb548107d src/HOL/Integ/nat_bin.ML --- a/src/HOL/Integ/nat_bin.ML Wed Dec 03 10:49:34 2003 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,500 +0,0 @@ -(* Title: HOL/nat_bin.ML - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1999 University of Cambridge - -Binary arithmetic for the natural numbers -*) - -val nat_number_of_def = thm "nat_number_of_def"; - -val ss_Int = simpset_of Int_thy; - -(** nat (coercion from int to nat) **) - -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, nat_0, nat_1]; - -Goal "Numeral0 = (0::nat)"; -by (simp_tac (simpset() addsimps [nat_number_of_def]) 1); -qed "numeral_0_eq_0"; - -Goal "Numeral1 = (1::nat)"; -by (simp_tac (simpset() addsimps [nat_1, nat_number_of_def]) 1); -qed "numeral_1_eq_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] "2 = Suc (Suc 0)"; -by (rtac nat_2 1); -qed "numeral_2_eq_2"; - - -(** Distributive laws for "nat". The others are in IntArith.ML, but these - require div and mod to be defined for type "int". They also need - some of the lemmas proved just above.**) - -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 (case_tac "z' = 0" 1 THEN asm_simp_tac (simpset() addsimps [DIVISION_BY_ZERO]) 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 "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); -by (Asm_simp_tac 1); -by (res_inst_tac [("r", "int (m mod m')")] quorem_div 1); - by (Force_tac 2); -by (asm_full_simp_tac - (simpset() addsimps [nat_less_iff RS sym, quorem_def, - numeral_0_eq_0, zadd_int, zmult_int]) 1); -qed "nat_div_distrib"; - -(*Fails if z'<0: the LHS collapses to (nat z) but the RHS doesn't*) -Goal "[| (0::int) <= z; 0 <= z' |] ==> nat (z mod z') = nat z mod nat z'"; -by (case_tac "z' = 0" 1 THEN asm_simp_tac (simpset() addsimps [DIVISION_BY_ZERO]) 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 "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); -by (Asm_simp_tac 1); -by (res_inst_tac [("q", "int (m div m')")] quorem_mod 1); - by (Force_tac 2); -by (asm_full_simp_tac - (simpset() addsimps [nat_less_iff RS sym, quorem_def, - numeral_0_eq_0, zadd_int, zmult_int]) 1); -qed "nat_mod_distrib"; - - -(** 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 0 \ -\ else (number_of v :: int))"; -by (simp_tac - (ss_Int addsimps [neg_nat, nat_number_of_def, not_neg_nat, int_0]) 1); -qed "int_nat_number_of"; -Addsimps [int_nat_number_of]; - - -(** Successor **) - -Goal "(0::int) <= z ==> Suc (nat z) = nat (1 + z)"; -by (rtac sym 1); -by (asm_simp_tac (simpset() addsimps [nat_eq_iff, int_Suc]) 1); -qed "Suc_nat_eq_nat_zadd1"; - -Goal "Suc (number_of v + n) = \ -\ (if neg (number_of v) then 1+n else number_of (bin_succ v) + n)"; -by (simp_tac (ss_Int 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]; - -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 [Suc_nat_number_of, int_nat_number_of, - not_neg_number_of_Pls, - neg_number_of_Min,neg_number_of_BIT]})]; - -(** Addition **) - -(*"neg" is used in rewrite rules for binary comparisons*) -Goal "(number_of v :: nat) + number_of v' = \ -\ (if neg (number_of v) then number_of v' \ -\ else if neg (number_of v') then number_of v \ -\ else number_of (bin_add v v'))"; -by (simp_tac (ss_Int addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def, - nat_add_distrib RS sym, number_of_add]) 1); -qed "add_nat_number_of"; - -Addsimps [add_nat_number_of]; - - -(** Subtraction **) - -Goal "nat z - nat z' = \ -\ (if neg z' then nat z \ -\ else let d = z-z' in \ -\ if neg d then 0 else nat d)"; -by (simp_tac (simpset() addsimps [Let_def, nat_diff_distrib RS sym, - neg_eq_less_0, not_neg_eq_ge_0]) 1); -by (simp_tac (simpset() addsimps [diff_is_0_eq, nat_le_eq_zle]) 1); -qed "diff_nat_eq_if"; - -Goalw [nat_number_of_def] - "(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 0 else nat d)"; -by (simp_tac (ss_Int delcongs [if_weak_cong] - addsimps [not_neg_eq_ge_0, nat_0, - diff_nat_eq_if, diff_number_of_eq]) 1); -qed "diff_nat_number_of"; - -Addsimps [diff_nat_number_of]; - - -(** Multiplication **) - -Goal "(number_of v :: nat) * number_of v' = \ -\ (if neg (number_of v) then 0 else number_of (bin_mult v v'))"; -by (simp_tac (ss_Int addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def, - nat_mult_distrib RS sym, number_of_mult, - nat_0]) 1); -qed "mult_nat_number_of"; - -Addsimps [mult_nat_number_of]; - - -(** Quotient **) - -Goal "(number_of v :: nat) div number_of v' = \ -\ (if neg (number_of v) then 0 \ -\ else nat (number_of v div number_of v'))"; -by (simp_tac (ss_Int addsimps [not_neg_eq_ge_0, nat_number_of_def, neg_nat, - nat_div_distrib RS sym, nat_0]) 1); -qed "div_nat_number_of"; - -Addsimps [div_nat_number_of]; - - -(** Remainder **) - -Goal "(number_of v :: nat) mod number_of v' = \ -\ (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 (ss_Int addsimps [not_neg_eq_ge_0, nat_number_of_def, - neg_nat, nat_0, DIVISION_BY_ZERO_MOD, - nat_mod_distrib RS sym]) 1); -qed "mod_nat_number_of"; - -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_novars - 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", ["(Suc 0) div m"], NatAbstractNumerals.proc div_nat_number_of), - ("nat_mod_eval_numerals", ["(Suc 0) mod m"], NatAbstractNumerals.proc mod_nat_number_of)]; - -Addsimprocs nat_eval_numerals; - - -(*** Comparisons ***) - -(** Equals (=) **) - -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"; - -(*"neg" is used in rewrite rules for binary comparisons*) -Goal "((number_of v :: nat) = number_of v') = \ -\ (if neg (number_of v) then (iszero (number_of v') | neg (number_of v')) \ -\ else if neg (number_of v') then iszero (number_of v) \ -\ else iszero (number_of (bin_add v (bin_minus v'))))"; -by (simp_tac (ss_Int addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def, - eq_nat_nat_iff, eq_number_of_eq, nat_0]) 1); -by (simp_tac (ss_Int addsimps [nat_eq_iff, nat_eq_iff2, iszero_def]) 1); -by (simp_tac (simpset () addsimps [not_neg_eq_ge_0 RS sym]) 1); -qed "eq_nat_number_of"; - -Addsimps [eq_nat_number_of]; - -(** Less-than (<) **) - -(*"neg" is used in rewrite rules for binary comparisons*) -Goal "((number_of v :: nat) < number_of v') = \ -\ (if neg (number_of v) then neg (number_of (bin_minus v')) \ -\ else neg (number_of (bin_add v (bin_minus v'))))"; -by (simp_tac (ss_Int 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 (ss_Int addsimps [neg_eq_less_0, zminus_zless, - number_of_minus, zless_nat_eq_int_zless]) 1); -qed "less_nat_number_of"; - -Addsimps [less_nat_number_of]; - - -(** Less-than-or-equals (<=) **) - -Goal "(number_of x <= (number_of y::nat)) = \ -\ (~ number_of y < (number_of x::nat))"; -by (rtac (linorder_not_less RS sym) 1); -qed "le_nat_number_of_eq_not_less"; - -Addsimps [le_nat_number_of_eq_not_less]; - - -(*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 "0 < n ==> n = Suc(n - 1)"; -by (asm_full_simp_tac numeral_ss 1); -qed "Suc_pred'"; - -(*Expresses a natural number constant as the Suc of another one. - NOT suitable for rewriting because n recurs in the condition.*) -bind_thm ("expand_Suc", inst "n" "number_of ?v" Suc_pred'); - -(** Arith **) - -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=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=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=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 "[| 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']; - -(** Power **) - -Goal "(p::nat) ^ 2 = p*p"; -by (simp_tac numeral_ss 1); -qed "power_two"; - - -(*** 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, 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))"; -by (rtac ([eq_sym_conv, eq_number_of_0] MRS trans) 1); -qed "eq_0_number_of"; - -Goal "((0::nat) < number_of v) = neg (number_of (bin_minus v))"; -by (simp_tac (simpset() addsimps [numeral_0_eq_0 RS sym]) 1); -qed "less_0_number_of"; - -(*Simplification already handles n<0, n<=0 and 0<=n.*) -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, iszero_0]) 1); -qed "neg_imp_number_of_eq_0"; - - - -(*** Comparisons involving Suc ***) - -Goal "(number_of v = Suc n) = \ -\ (let pv = number_of (bin_pred v) in \ -\ if neg pv then False else nat pv = n)"; -by (simp_tac (ss_Int addsimps - [Let_def, neg_eq_less_0, linorder_not_less, number_of_pred, - nat_number_of_def, zadd_0] @ zadd_ac) 1); -by (res_inst_tac [("x", "number_of v")] spec 1); -by (auto_tac (claset(), simpset() addsimps [nat_eq_iff])); -qed "eq_number_of_Suc"; - -Goal "(Suc n = number_of v) = \ -\ (let pv = number_of (bin_pred v) in \ -\ if neg pv then False else nat pv = n)"; -by (rtac ([eq_sym_conv, eq_number_of_Suc] MRS trans) 1); -qed "Suc_eq_number_of"; - -Goal "(number_of v < Suc n) = \ -\ (let pv = number_of (bin_pred v) in \ -\ if neg pv then True else nat pv < n)"; -by (simp_tac (ss_Int addsimps - [Let_def, neg_eq_less_0, linorder_not_less, number_of_pred, - nat_number_of_def, zadd_0] @ zadd_ac) 1); -by (res_inst_tac [("x", "number_of v")] spec 1); -by (auto_tac (claset(), simpset() addsimps [nat_less_iff])); -qed "less_number_of_Suc"; - -Goal "(Suc n < number_of v) = \ -\ (let pv = number_of (bin_pred v) in \ -\ if neg pv then False else n < nat pv)"; -by (simp_tac (ss_Int addsimps - [Let_def, neg_eq_less_0, linorder_not_less, number_of_pred, - nat_number_of_def, zadd_0] @ zadd_ac) 1); -by (res_inst_tac [("x", "number_of v")] spec 1); -by (auto_tac (claset(), simpset() addsimps [zless_nat_eq_int_zless])); -qed "less_Suc_number_of"; - -Goal "(number_of v <= Suc n) = \ -\ (let pv = number_of (bin_pred v) in \ -\ if neg pv then True else nat pv <= n)"; -by (simp_tac - (simpset () addsimps - [Let_def, less_Suc_number_of, linorder_not_less RS sym]) 1); -qed "le_number_of_Suc"; - -Goal "(Suc n <= number_of v) = \ -\ (let pv = number_of (bin_pred v) in \ -\ if neg pv then False else n <= nat pv)"; -by (simp_tac - (simpset () addsimps - [Let_def, less_number_of_Suc, linorder_not_less RS sym]) 1); -qed "le_Suc_number_of"; - -Addsimps [eq_number_of_Suc, Suc_eq_number_of, - less_number_of_Suc, less_Suc_number_of, - le_number_of_Suc, le_Suc_number_of]; - -(* Push int(.) inwards: *) -Addsimps [zadd_int RS sym]; - -Goal "(m+m = n+n) = (m = (n::int))"; -by Auto_tac; -val lemma1 = result(); - -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); -val lemma2 = result(); - -Goal "((number_of (v BIT x) ::int) = number_of (w BIT y)) = \ -\ (x=y & (((number_of v) ::int) = number_of w))"; -by (simp_tac (ss_Int addsimps [number_of_BIT, lemma1, lemma2, eq_commute]) 1); -qed "eq_number_of_BIT_BIT"; - -Goal "((number_of (v BIT x) ::int) = number_of bin.Pls) = \ -\ (x=False & (((number_of v) ::int) = number_of bin.Pls))"; -by (simp_tac (ss_Int addsimps [number_of_BIT, number_of_Pls, eq_commute]) 1); -by (res_inst_tac [("x", "number_of v")] spec 1); -by Safe_tac; -by (ALLGOALS Full_simp_tac); -by (dres_inst_tac [("f", "%x. x mod 2")] arg_cong 1); -by (full_simp_tac (simpset() addsimps [zmod_zadd1_eq]) 1); -qed "eq_number_of_BIT_Pls"; - -Goal "((number_of (v BIT x) ::int) = number_of bin.Min) = \ -\ (x=True & (((number_of v) ::int) = number_of bin.Min))"; -by (simp_tac (ss_Int addsimps [number_of_BIT, number_of_Min, eq_commute]) 1); -by (res_inst_tac [("x", "number_of v")] spec 1); -by Auto_tac; -by (dres_inst_tac [("f", "%x. x mod 2")] arg_cong 1); -by Auto_tac; -qed "eq_number_of_BIT_Min"; - -Goal "(number_of bin.Pls ::int) ~= number_of bin.Min"; -by Auto_tac; -qed "eq_number_of_Pls_Min"; - - -(*Distributive laws for literals*) -Addsimps (map (inst "k" "number_of ?v") - [add_mult_distrib, add_mult_distrib2, - diff_mult_distrib, diff_mult_distrib2]); - - -(*** Literal arithmetic involving powers, type nat ***) - -Goal "(0::int) <= z ==> nat (z^n) = nat z ^ n"; -by (induct_tac "n" 1); -by (ALLGOALS (asm_simp_tac (simpset() addsimps [nat_mult_distrib]))); -qed "nat_power_eq"; - -Goal "(number_of v :: nat) ^ n = \ -\ (if neg (number_of v) then 0^n else nat ((number_of v :: int) ^ n))"; -by (simp_tac (ss_Int addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def, - nat_power_eq]) 1); -qed "power_nat_number_of"; - -Addsimps [inst "n" "number_of ?w" power_nat_number_of]; - - - -(*** Literal arithmetic involving powers, type int ***) - -Goal "(z::int) ^ (2*a) = (z^a)^2"; -by (simp_tac (simpset() addsimps [zpower_zpower, mult_commute]) 1); -qed "zpower_even"; - -Goal "(p::int) ^ 2 = p*p"; -by (simp_tac numeral_ss 1); -qed "zpower_two"; - -Goal "(z::int) ^ (2*a + 1) = z * (z^a)^2"; -by (simp_tac (simpset() addsimps [zpower_even, zpower_zadd_distrib]) 1); -qed "zpower_odd"; - -Goal "(z::int) ^ number_of (w BIT False) = \ -\ (let w = z ^ (number_of w) in w*w)"; -by (simp_tac (ss_Int addsimps [nat_number_of_def, number_of_BIT, Let_def]) 1); -by (res_inst_tac [("x","number_of w")] spec 1 THEN Clarify_tac 1); -by (case_tac "(0::int) <= x" 1); -by (auto_tac (claset(), - simpset() addsimps [nat_mult_distrib, zpower_even, zpower_two])); -qed "zpower_number_of_even"; - -Goal "(z::int) ^ number_of (w BIT True) = \ -\ (if (0::int) <= number_of w \ -\ then (let w = z ^ (number_of w) in z*w*w) \ -\ else 1)"; -by (simp_tac (ss_Int addsimps [nat_number_of_def, number_of_BIT, Let_def]) 1); -by (res_inst_tac [("x","number_of w")] spec 1 THEN Clarify_tac 1); -by (case_tac "(0::int) <= x" 1); -by (auto_tac (claset(), - simpset() addsimps [nat_add_distrib, nat_mult_distrib, - zpower_even, zpower_two])); -qed "zpower_number_of_odd"; - -Addsimps (map (inst "z" "number_of ?v") - [zpower_number_of_even, zpower_number_of_odd]); - diff -r 8ed6989228bb -r 5efbb548107d src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Wed Dec 03 10:49:34 2003 +0100 +++ b/src/HOL/IsaMakefile Thu Dec 04 10:29:17 2003 +0100 @@ -84,11 +84,11 @@ Divides.thy Extraction.thy Finite_Set.ML Finite_Set.thy \ Fun.thy Gfp.ML Gfp.thy \ Hilbert_Choice.thy Hilbert_Choice_lemmas.ML HOL.ML \ - HOL.thy HOL_lemmas.ML Inductive.thy Integ/Bin.ML Integ/Bin.thy \ + HOL.thy HOL_lemmas.ML Inductive.thy Integ/Bin.thy \ Integ/cooper_dec.ML Integ/cooper_proof.ML \ Integ/Equiv.thy Integ/Int.thy Integ/IntArith.thy Integ/IntDef.thy \ Integ/IntDiv.thy Integ/IntPower.thy \ - Integ/nat_bin.ML Integ/NatBin.thy Integ/NatSimprocs.ML \ + Integ/NatBin.thy Integ/NatSimprocs.ML \ Integ/NatSimprocs.thy Integ/int_arith1.ML \ Integ/int_factor_simprocs.ML Integ/nat_simprocs.ML \ Integ/Presburger.thy Integ/presburger.ML Integ/qelim.ML \ diff -r 8ed6989228bb -r 5efbb548107d src/HOL/Ring_and_Field.thy --- a/src/HOL/Ring_and_Field.thy Wed Dec 03 10:49:34 2003 +0100 +++ b/src/HOL/Ring_and_Field.thy Thu Dec 04 10:29:17 2003 +0100 @@ -137,6 +137,20 @@ lemma neg_0_equal_iff_equal [simp]: "(0 = -a) = (0 = (a::'a::ring))" by (subst neg_equal_iff_equal [symmetric], simp) +text{*The next two equations can make the simplifier loop!*} + +lemma equation_minus_iff: "(a = - b) = (b = - (a::'a::ring))" + proof - + have "(- (-a) = - b) = (- a = b)" by (rule neg_equal_iff_equal) + thus ?thesis by (simp add: eq_commute) + qed + +lemma minus_equation_iff: "(- a = b) = (- (b::'a::ring) = a)" + proof - + have "(- a = - (-b)) = (a = -b)" by (rule neg_equal_iff_equal) + thus ?thesis by (simp add: eq_commute) + qed + subsection {* Derived rules for multiplication *} @@ -199,6 +213,10 @@ theorems ring_distrib = right_distrib left_distrib +text{*For the @{text combine_numerals} simproc*} +lemma combine_common_factor: "a*e + (b*e + c) = (a+b)*e + (c::'a::semiring)" +by (simp add: left_distrib add_ac) + lemma minus_add_distrib [simp]: "- (a + b) = -a + -(b::'a::ring)" apply (rule equals_zero_I) apply (simp add: add_ac) @@ -221,6 +239,9 @@ by (simp add: right_distrib diff_minus minus_mult_left [symmetric] minus_mult_right [symmetric]) +lemma left_diff_distrib: "(a - b) * c = a * c - b * (c::'a::ring)" +by (simp add: mult_commute [of _ c] right_diff_distrib) + lemma minus_diff_eq [simp]: "- (a - b) = b - (a::'a::ring)" by (simp add: diff_minus add_commute) @@ -330,6 +351,30 @@ lemma neg_0_less_iff_less [simp]: "(0 < -a) = (a < (0::'a::ordered_ring))" by (subst neg_less_iff_less [symmetric], simp) +text{*The next several equations can make the simplifier loop!*} + +lemma less_minus_iff: "(a < - b) = (b < - (a::'a::ordered_ring))" + proof - + have "(- (-a) < - b) = (b < - a)" by (rule neg_less_iff_less) + thus ?thesis by simp + qed + +lemma minus_less_iff: "(- a < b) = (- b < (a::'a::ordered_ring))" + proof - + have "(- a < - (-b)) = (- b < a)" by (rule neg_less_iff_less) + thus ?thesis by simp + qed + +lemma le_minus_iff: "(a \ - b) = (b \ - (a::'a::ordered_ring))" +apply (simp add: linorder_not_less [symmetric]) +apply (rule minus_less_iff) +done + +lemma minus_le_iff: "(- a \ b) = (- b \ (a::'a::ordered_ring))" +apply (simp add: linorder_not_less [symmetric]) +apply (rule less_minus_iff) +done + subsection{*Subtraction Laws*} @@ -353,7 +398,7 @@ text{*Further subtraction laws for ordered rings*} -lemma less_eq_diff: "(a < b) = (a - b < (0::'a::ordered_ring))" +lemma less_iff_diff_less_0: "(a < b) = (a - b < (0::'a::ordered_ring))" proof - have "(a < b) = (a + (- b) < b + (-b))" by (simp only: add_less_cancel_right) @@ -362,14 +407,14 @@ qed lemma diff_less_eq: "(a-b < c) = (a < c + (b::'a::ordered_ring))" -apply (subst less_eq_diff) -apply (rule less_eq_diff [of _ c, THEN ssubst]) +apply (subst less_iff_diff_less_0) +apply (rule less_iff_diff_less_0 [of _ c, THEN ssubst]) apply (simp add: diff_minus add_ac) done lemma less_diff_eq: "(a < c-b) = (a + (b::'a::ordered_ring) < c)" -apply (subst less_eq_diff) -apply (rule less_eq_diff [of _ "c-b", THEN ssubst]) +apply (subst less_iff_diff_less_0) +apply (rule less_iff_diff_less_0 [of _ "c-b", THEN ssubst]) apply (simp add: diff_minus add_ac) done @@ -389,6 +434,51 @@ diff_eq_eq eq_diff_eq +subsection{*Lemmas for the @{text cancel_numerals} simproc*} + +lemma eq_iff_diff_eq_0: "(a = b) = (a-b = (0::'a::ring))" +by (simp add: compare_rls) + +lemma le_iff_diff_le_0: "(a \ b) = (a-b \ (0::'a::ordered_ring))" +by (simp add: compare_rls) + +lemma eq_add_iff1: + "(a*e + c = b*e + d) = ((a-b)*e + c = (d::'a::ring))" +apply (simp add: diff_minus left_distrib add_ac) +apply (simp add: compare_rls minus_mult_left [symmetric]) +done + +lemma eq_add_iff2: + "(a*e + c = b*e + d) = (c = (b-a)*e + (d::'a::ring))" +apply (simp add: diff_minus left_distrib add_ac) +apply (simp add: compare_rls minus_mult_left [symmetric]) +done + +lemma less_add_iff1: + "(a*e + c < b*e + d) = ((a-b)*e + c < (d::'a::ordered_ring))" +apply (simp add: diff_minus left_distrib add_ac) +apply (simp add: compare_rls minus_mult_left [symmetric]) +done + +lemma less_add_iff2: + "(a*e + c < b*e + d) = (c < (b-a)*e + (d::'a::ordered_ring))" +apply (simp add: diff_minus left_distrib add_ac) +apply (simp add: compare_rls minus_mult_left [symmetric]) +done + +lemma le_add_iff1: + "(a*e + c \ b*e + d) = ((a-b)*e + c \ (d::'a::ordered_ring))" +apply (simp add: diff_minus left_distrib add_ac) +apply (simp add: compare_rls minus_mult_left [symmetric]) +done + +lemma le_add_iff2: + "(a*e + c \ b*e + d) = (c \ (b-a)*e + (d::'a::ordered_ring))" +apply (simp add: diff_minus left_distrib add_ac) +apply (simp add: compare_rls minus_mult_left [symmetric]) +done + + subsection {* Ordering Rules for Multiplication *} lemma mult_strict_right_mono: