--- 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];
-
-
--- 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 \<le>) *)
+
+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 (\<le>) **)
+
+lemma le_number_of_eq_not_less: "(number_of x \<le> (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
--- 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)"
-apply (auto simp add: zless_iff_Suc_zadd int_Suc gr0_conv_Suc zero_reorient)
-apply (rule_tac x = "Suc n" in exI)
-apply (simp add: int_Suc)
-done
-
-lemma add1_zle_eq: "(w + (1::int) \<le> z) = (w<z)"
-apply (simp add: zle_def zless_add1_eq)
-apply (auto intro: zless_asym zle_anti_sym
- simp add: order_less_imp_le symmetric zle_def)
-done
-
-lemma add1_left_zle_eq: "((1::int) + w \<le> z) = (w<z)"
-apply (subst zadd_commute)
-apply (rule add1_zle_eq)
-done
-
-
-
-
ML
{*
val zless_eq_neg = thm "zless_eq_neg";
val eq_eq_iszero = thm "eq_eq_iszero";
val zle_eq_not_neg = thm "zle_eq_not_neg";
-val zless_add1_eq = thm "zless_add1_eq";
-val add1_zle_eq = thm "add1_zle_eq";
-val add1_left_zle_eq = thm "add1_left_zle_eq";
val zadd_right_cancel_zless = thm "zadd_right_cancel_zless";
val zadd_left_cancel_zless = thm "zadd_left_cancel_zless";
val zadd_right_cancel_zle = thm "zadd_right_cancel_zle";
--- a/src/HOL/Integ/IntArith.thy Wed Dec 03 10:49:34 2003 +0100
+++ b/src/HOL/Integ/IntArith.thy Thu Dec 04 10:29:17 2003 +0100
@@ -8,13 +8,34 @@
theory IntArith = Bin
files ("int_arith1.ML"):
+subsection{*Inequality Reasoning for the Arithmetic Simproc*}
+
+lemma zless_imp_add1_zle: "w<z ==> w + (1::int) \<le> 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)"
by arith
-lemma zle_add1_eq_le [simp]: "(w < z + 1) = (w<=(z::int))"
+lemma add1_zle_eq: "(w + (1::int) \<le> z) = (w<z)"
+by arith
+
+lemma zle_diff1_eq [simp]: "(w \<le> z - (1::int)) = (w<(z::int))"
+by arith
+
+lemma zle_add1_eq_le [simp]: "(w < z + 1) = (w\<le>(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 \<le> 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 \<le> 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 \<le> 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 \<le> 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 \<le> 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<z)"
+lemma nat_less_eq_zless: "0 \<le> w ==> (nat w < nat z) = (w<z)"
apply (case_tac "neg z")
apply (auto simp add: nat_less_iff)
apply (auto intro: zless_trans simp add: neg_eq_less_0 zle_def)
done
-lemma nat_le_eq_zle: "0 < w | 0 <= z ==> (nat w <= nat z) = (w<=z)"
+lemma nat_le_eq_zle: "0 < w | 0 \<le> z ==> (nat w \<le> nat z) = (w\<le>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 \<le> 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 \<le> 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 \<and> 0 <= z \<or> z = -w \<and> z < 0)"
+ "(abs (z::int) = w) = (z = w \<and> 0 \<le> z \<or> z = -w \<and> z < 0)"
by (auto simp add: zabs_def)
lemma int_nat_eq [simp]: "int (nat z) = (if 0 \<le> z then z else 0)"
@@ -117,7 +138,7 @@
step: "\<And>i. \<lbrakk>k \<le> i; P i\<rbrakk> \<Longrightarrow> P(i+1)"
shows "P i"
proof -
- { fix n have "\<And>i::int. n = nat(i-k) \<Longrightarrow> k <= i \<Longrightarrow> P i"
+ { fix n have "\<And>i::int. n = nat(i-k) \<Longrightarrow> k \<le> i \<Longrightarrow> P i"
proof (induct n)
case 0
hence "i = k" by arith
@@ -153,7 +174,7 @@
step: "\<And>i. \<lbrakk>i \<le> k; P i\<rbrakk> \<Longrightarrow> P(i - 1)"
shows "P i"
proof -
- { fix n have "\<And>i::int. n = nat(k-i) \<Longrightarrow> i <= k \<Longrightarrow> P i"
+ { fix n have "\<And>i::int. n = nat(k-i) \<Longrightarrow> i \<le> k \<Longrightarrow> 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) \<le> abs(x) + abs(y::int)"
by arith
--- 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<n; 0<m |] ==> 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 {*
--- 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)";
--- 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]}),
--- 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<n; 0<m |] ==> 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]);
-
--- 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 \
--- 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 \<le> - b) = (b \<le> - (a::'a::ordered_ring))"
+apply (simp add: linorder_not_less [symmetric])
+apply (rule minus_less_iff)
+done
+
+lemma minus_le_iff: "(- a \<le> b) = (- b \<le> (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 \<le> b) = (a-b \<le> (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 \<le> b*e + d) = ((a-b)*e + c \<le> (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 \<le> b*e + d) = (c \<le> (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: