--- a/src/HOL/Integ/Bin.ML Mon Oct 22 11:01:30 2001 +0200
+++ b/src/HOL/Integ/Bin.ML Mon Oct 22 11:54:22 2001 +0200
@@ -98,7 +98,7 @@
(**** The carry/borrow functions, bin_succ and bin_pred ****)
-(**** number_of ****)
+(** number_of **)
Goal "number_of(NCons w b) = (number_of(w BIT b)::int)";
by (induct_tac "w" 1);
@@ -107,12 +107,12 @@
Addsimps [number_of_NCons];
-Goal "number_of(bin_succ w) = int 1 + number_of w";
+Goal "number_of(bin_succ w) = (1 + number_of w :: int)";
by (induct_tac "w" 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps zadd_ac)));
qed "number_of_succ";
-Goal "number_of(bin_pred w) = - (int 1) + number_of w";
+Goal "number_of(bin_pred w) = (- 1 + number_of w :: int)";
by (induct_tac "w" 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps zadd_ac)));
qed "number_of_pred";
@@ -127,17 +127,15 @@
zadd_assoc]) 1);
qed "number_of_minus";
-
-bind_thms ("bin_add_simps", [bin_add_BIT_BIT, number_of_succ, number_of_pred]);
-
(*This proof is complicated by the mutual recursion*)
Goal "! w. number_of(bin_add v w) = (number_of v + number_of w::int)";
-by (induct_tac "v" 1);
-by (simp_tac (simpset() addsimps bin_add_simps) 1);
-by (simp_tac (simpset() addsimps bin_add_simps) 1);
+by (induct_tac "v" 1);
+by (Simp_tac 1);
+by (simp_tac (simpset() addsimps [number_of_pred]) 1);
by (rtac allI 1);
by (induct_tac "w" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps bin_add_simps @ zadd_ac)));
+by (ALLGOALS (asm_simp_tac (simpset() addsimps
+ [bin_add_BIT_BIT, number_of_succ, number_of_pred] @ zadd_ac)));
qed_spec_mp "number_of_add";
@@ -147,7 +145,8 @@
by (simp_tac (simpset() addsimps [number_of_add, number_of_minus]) 1);
qed "diff_number_of_eq";
-bind_thms ("bin_mult_simps", [zmult_zminus, number_of_minus, number_of_add]);
+bind_thms ("bin_mult_simps",
+ [int_Suc0_eq_1, zmult_zminus, number_of_minus, number_of_add]);
Goal "number_of(bin_mult v w) = (number_of v * number_of w::int)";
by (induct_tac "v" 1);
@@ -167,54 +166,15 @@
qed "double_number_of_BIT";
-(** Simplification rules with integer constants **)
-
-Goal "Numeral0 + z = (z::int)";
-by (Simp_tac 1);
-qed "zadd_0";
-
-Goal "z + Numeral0 = (z::int)";
-by (Simp_tac 1);
-qed "zadd_0_right";
-
-Addsimps [zadd_0, zadd_0_right];
-
-
-(** Converting simple cases of (int n) to numerals **)
-
-Goal "int 0 = Numeral0";
-by (rtac sym 1);
-by (rtac number_of_Pls 1);
-qed "int_0";
-
-Goal "int 1 = Numeral1";
-by (Simp_tac 1);
-qed "int_1";
+(** Converting numerals 0 and 1 to their abstract versions **)
-Goal "int (Suc n) = Numeral1 + int n";
-by (simp_tac (simpset() addsimps [zadd_int]) 1);
-qed "int_Suc";
-
-Goal "- (Numeral0) = (Numeral0::int)";
+Goal "Numeral0 = (0::int)";
by (Simp_tac 1);
-qed "zminus_0";
-
-Addsimps [zminus_0];
-
+qed "int_numeral_0_eq_0";
-Goal "(Numeral0::int) - x = -x";
-by (simp_tac (simpset() addsimps [zdiff_def]) 1);
-qed "zdiff0";
-
-Goal "x - (Numeral0::int) = x";
-by (simp_tac (simpset() addsimps [zdiff_def]) 1);
-qed "zdiff0_right";
-
-Goal "x - x = (Numeral0::int)";
-by (simp_tac (simpset() addsimps [zdiff_def]) 1);
-qed "zdiff_self";
-
-Addsimps [zdiff0, zdiff0_right, zdiff_self];
+Goal "Numeral1 = (1::int)";
+by (simp_tac (simpset() addsimps [int_1, int_Suc0_eq_1]) 1);
+qed "int_numeral_1_eq_1";
(** Special simplification, for constants only **)
@@ -240,99 +200,30 @@
(** Special-case simplification for small constants **)
-Goal "Numeral0 * z = (Numeral0::int)";
-by (Simp_tac 1);
-qed "zmult_0";
-
-Goal "z * Numeral0 = (Numeral0::int)";
-by (Simp_tac 1);
-qed "zmult_0_right";
-
-Goal "Numeral1 * z = (z::int)";
-by (Simp_tac 1);
-qed "zmult_1";
-
-Goal "z * Numeral1 = (z::int)";
-by (Simp_tac 1);
-qed "zmult_1_right";
-
Goal "-1 * z = -(z::int)";
-by (simp_tac (simpset() addsimps zcompare_rls@[zmult_zminus]) 1);
+by (simp_tac (simpset() addsimps zcompare_rls@[int_Suc0_eq_1, zmult_zminus]) 1);
qed "zmult_minus1";
Goal "z * -1 = -(z::int)";
-by (simp_tac (simpset() addsimps zcompare_rls@[zmult_zminus_right]) 1);
+by (stac zmult_commute 1 THEN rtac zmult_minus1 1);
qed "zmult_minus1_right";
-Addsimps [zmult_0, zmult_0_right,
- zmult_1, zmult_1_right,
- zmult_minus1, zmult_minus1_right];
+Addsimps [zmult_minus1, zmult_minus1_right];
(*Negation of a coefficient*)
Goal "- (number_of w) * z = number_of(bin_minus w) * (z::int)";
by (simp_tac (simpset() addsimps [number_of_minus, zmult_zminus]) 1);
qed "zminus_number_of_zmult";
-
Addsimps [zminus_number_of_zmult];
-
-(** Inequality reasoning **)
-
-Goal "(m*n = (Numeral0::int)) = (m = Numeral0 | n = Numeral0)";
-by (stac (int_0 RS sym) 1 THEN rtac zmult_eq_int0_iff 1);
-qed "zmult_eq_0_iff";
-AddIffs [zmult_eq_0_iff];
-
-Goal "(w < z + (Numeral1::int)) = (w<z | w=z)";
-by (simp_tac (simpset() addsimps [zless_add_int_Suc_eq]) 1);
-qed "zless_add1_eq";
-
-Goal "(w + (Numeral1::int) <= z) = (w<z)";
-by (simp_tac (simpset() addsimps [add_int_Suc_zle_eq]) 1);
-qed "add1_zle_eq";
-
-Goal "((Numeral1::int) + w <= z) = (w<z)";
-by (stac zadd_commute 1);
-by (rtac add1_zle_eq 1);
-qed "add1_left_zle_eq";
-
-Goal "neg x = (x < Numeral0)";
-by (simp_tac (simpset() addsimps [neg_eq_less_int0]) 1);
-qed "neg_eq_less_0";
-
-Goal "(~neg x) = (Numeral0 <= x)";
-by (simp_tac (simpset() addsimps [not_neg_eq_ge_int0]) 1);
-qed "not_neg_eq_ge_0";
+(*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 "Numeral0 <= int m";
-by (Simp_tac 1);
-qed "zero_zle_int";
-AddIffs [zero_zle_int];
-
-
-(** Needed because (int 0) rewrites to Numeral0. (* FIXME !? *)
- Can these be generalized without evaluating large numbers?**)
-
-Goal "~ (int k < Numeral0)";
-by (Simp_tac 1);
-qed "int_less_0_conv";
-
-Goal "(int k <= Numeral0) = (k=0)";
-by (Simp_tac 1);
-qed "int_le_0_conv";
-
-Goal "(int k = Numeral0) = (k=0)";
-by (Simp_tac 1);
-qed "int_eq_0_conv";
-
-Goal "(Numeral0 < int k) = (0<k)";
-by (Simp_tac 1);
-qed "zero_less_int_conv";
-
-Addsimps [int_less_0_conv, int_le_0_conv, int_eq_0_conv, zero_less_int_conv];
-
-Goal "(0 < nat z) = (Numeral0 < z)";
-by (cut_inst_tac [("w","Numeral0")] zless_nat_conj 1);
+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];
@@ -345,7 +236,7 @@
Goalw [iszero_def]
"((number_of x::int) = number_of y) = \
\ iszero (number_of (bin_add x (bin_minus y)))";
-by (simp_tac (simpset() delsimps [thm "number_of_reorient"]
+by (simp_tac (simpset()
addsimps zcompare_rls @ [number_of_add, number_of_minus]) 1);
qed "eq_number_of_eq";
@@ -360,9 +251,11 @@
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 zcompare_rls @
- [zminus_zadd_distrib RS sym, zadd_int])));
+by (ALLGOALS
+ (asm_simp_tac
+ (simpset() addsimps zcompare_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)";
@@ -383,20 +276,22 @@
by (simp_tac (simpset() addsimps bin_mult_simps) 1);
qed "less_number_of_eq_neg";
-Goal "~ neg (number_of Pls)";
-by (Simp_tac 1);
+(*But if Numeral0 is rewritten to 0 then this rule can't be applied:
+ Numeral0 IS (number_of Pls) *)
+Goal "~ neg (number_of Pls)";
+by (simp_tac (simpset() addsimps [neg_eq_less_0]) 1);
qed "not_neg_number_of_Pls";
Goal "neg (number_of Min)";
-by (Simp_tac 1);
+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 [zadd_int, neg_eq_less_int0,
- symmetric zdiff_def] @ zcompare_rls)));
+ (simpset() addsimps [int_Suc0_eq_1 RS sym, zadd_int,
+ neg_eq_less_0, symmetric zdiff_def] @ zcompare_rls)));
qed "neg_number_of_BIT";
@@ -413,7 +308,114 @@
"abs(number_of x::int) = \
\ (if number_of x < (0::int) then -number_of x else number_of x)";
by(rtac refl 1);
-qed "abs_number_of";
+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 name tacs sg (hyps: thm list) (t,u) =
+ if t aconv u then None
+ else
+ let val ct = cterm_of sg (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u)))
+ in Some
+ (prove_goalw_cterm [] ct (K tacs)
+ handle ERROR => error
+ ("The error(s) above occurred while trying to prove " ^
+ string_of_cterm ct ^ "\nInternal failure of simproc " ^ name))
+ end
+
+ (*version without the hyps argument*)
+ fun prove_conv_nohyps name tacs sg = prove_conv name tacs sg []
+
+ fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc
+ fun prep_pat s = Thm.read_cterm (Theory.sign_of (the_context())) (s, HOLogic.termT)
+ val prep_pats = map prep_pat
+
+ fun is_numeral (Const("Numeral.number_of", _) $ w) = true
+ | is_numeral _ = false
+
+ fun simplify_meta_eq f_number_of_eq f_eq =
+ mk_meta_eq ([f_eq, f_number_of_eq] MRS trans)
+
+ structure IntAbstractNumeralsData =
+ struct
+ val dest_eq = HOLogic.dest_eq o HOLogic.dest_Trueprop o concl_of
+ val is_numeral = is_numeral
+ val numeral_0_eq_0 = int_numeral_0_eq_0
+ val numeral_1_eq_1 = int_numeral_1_eq_1
+ val prove_conv = prove_conv_nohyps "int_abstract_numerals"
+ fun norm_tac simps = ALLGOALS (simp_tac (HOL_ss addsimps simps))
+ val simplify_meta_eq = simplify_meta_eq
+ end
+
+ structure IntAbstractNumerals = AbstractNumeralsFun (IntAbstractNumeralsData)
+
+
+ (*For addition, we already have rules for the operand 0.
+ Multiplication is omitted because there are already special rules for
+ both 0 and 1 as operands. Unary minus is trivial, just have - 1 = -1.
+ For the others, having three patterns is a compromise between just having
+ one (many spurious calls) and having nine (just too many!) *)
+ val eval_numerals =
+ map prep_simproc
+ [("int_add_eval_numerals",
+ prep_pats ["(m::int) + 1", "(m::int) + number_of v"],
+ IntAbstractNumerals.proc (number_of_add RS sym)),
+ ("int_diff_eval_numerals",
+ prep_pats ["(m::int) - 1", "(m::int) - number_of v"],
+ IntAbstractNumerals.proc diff_number_of_eq),
+ ("int_eq_eval_numerals",
+ prep_pats ["(m::int) = 0", "(m::int) = 1", "(m::int) = number_of v"],
+ IntAbstractNumerals.proc eq_number_of_eq),
+ ("int_less_eval_numerals",
+ prep_pats ["(m::int) < 0", "(m::int) < 1", "(m::int) < number_of v"],
+ IntAbstractNumerals.proc less_number_of_eq_neg),
+ ("int_le_eval_numerals",
+ prep_pats ["(m::int) <= 0", "(m::int) <= 1", "(m::int) <= number_of v"],
+ IntAbstractNumerals.proc le_number_of_eq_not_less)]
+
+ (*reorientation simprules using ==, for the following simproc*)
+ val meta_zero_reorient = zero_reorient RS eq_reflection
+ val meta_one_reorient = one_reorient RS eq_reflection
+ val meta_number_of_reorient = number_of_reorient RS eq_reflection
+
+ (*reorientation simplification procedure: reorients (polymorphic)
+ 0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a numeral.*)
+ fun reorient_proc sg _ (_ $ t $ u) =
+ case u of
+ Const("0", _) => None
+ | Const("1", _) => None
+ | Const("Numeral.number_of", _) $ _ => None
+ | _ => Some (case t of
+ Const("0", _) => meta_zero_reorient
+ | Const("1", _) => meta_one_reorient
+ | Const("Numeral.number_of", _) $ _ => meta_number_of_reorient)
+
+ val reorient_simproc =
+ prep_simproc ("reorient_simproc",
+ prep_pats ["0=x", "1=x", "number_of w = x"],
+ reorient_proc)
+
+ end;
+
+
+Addsimprocs Bin_Simprocs.eval_numerals;
+Addsimprocs [Bin_Simprocs.reorient_simproc];
(*Delete the original rewrites, with their clumsy conditional expressions*)
@@ -423,21 +425,24 @@
(*Hide the binary representation of integer constants*)
Delsimps [number_of_Pls, number_of_Min, number_of_BIT];
+
+
(*Simplification of arithmetic operations on integer constants.
Note that bin_pred_Pls, etc. were added to the simpset by primrec.*)
-bind_thms ("NCons_simps", [NCons_Pls_0, NCons_Pls_1, NCons_Min_0, NCons_Min_1, NCons_BIT]);
+bind_thms ("NCons_simps",
+ [NCons_Pls_0, NCons_Pls_1, NCons_Min_0, NCons_Min_1, NCons_BIT]);
bind_thms ("bin_arith_extra_simps",
[number_of_add RS sym,
- number_of_minus RS sym,
+ number_of_minus RS sym, zminus_1_eq_m1,
number_of_mult RS sym,
bin_succ_1, bin_succ_0,
bin_pred_1, bin_pred_0,
bin_minus_1, bin_minus_0,
bin_add_Pls_right, bin_add_Min_right,
bin_add_BIT_0, bin_add_BIT_10, bin_add_BIT_11,
- diff_number_of_eq, abs_number_of,
+ diff_number_of_eq, zabs_number_of, zabs_0, zabs_1,
bin_mult_1, bin_mult_0] @ NCons_simps);
(*For making a minimal simpset, one must include these default simprules
@@ -454,7 +459,8 @@
[eq_number_of_eq, iszero_number_of_Pls, nonzero_number_of_Min,
iszero_number_of_0, iszero_number_of_1,
less_number_of_eq_neg,
- not_neg_number_of_Pls, neg_number_of_Min, neg_number_of_BIT,
+ not_neg_number_of_Pls, not_neg_0, not_neg_1, not_iszero_1,
+ neg_number_of_Min, neg_number_of_BIT,
le_number_of_eq_not_less]);
Addsimps bin_arith_extra_simps;
@@ -484,3 +490,14 @@
Addsimps [add_number_of_left, mult_number_of_left,
add_number_of_diff1, add_number_of_diff2];
+
+
+(** Inserting these natural simprules earlier would break many proofs! **)
+
+(* int (Suc n) = 1 + int n *)
+Addsimps [int_Suc];
+
+(* Numeral0 -> 0 and Numeral1 -> 1 *)
+Addsimps [int_numeral_0_eq_0, int_numeral_1_eq_1];
+
+