--- a/src/HOL/Integ/NatSimprocs.ML Thu Dec 04 10:29:17 2003 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,160 +0,0 @@
-(* Title: HOL/NatSimprocs.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 2000 University of Cambridge
-
-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)";
-by (asm_simp_tac (simpset() addsimps [numeral_0_eq_0, numeral_1_eq_1]
- addsplits [nat_diff_split]) 1);
-qed "Suc_diff_eq_diff_pred";
-
-(*Now just instantiating n to (number_of v) does the right simplification,
- but with some redundant inequality tests.*)
-Goal "neg (number_of (bin_pred v)) = (number_of v = (0::nat))";
-by (subgoal_tac "neg (number_of (bin_pred v)) = (number_of v < Suc 0)" 1);
-by (asm_simp_tac (HOL_ss addsimps [less_Suc_eq_le, le_0_eq]) 1);
-by (stac less_number_of_Suc 1);
-by (Simp_tac 1);
-qed "neg_number_of_bin_pred_iff_0";
-
-Goal "neg (number_of (bin_minus v)) ==> \
-\ Suc m - (number_of v) = m - (number_of (bin_pred v))";
-by (stac Suc_diff_eq_diff_pred 1);
-by (Simp_tac 1);
-by (Simp_tac 1);
-by (asm_full_simp_tac (ss_Int addsimps [diff_nat_number_of,
- less_0_number_of RS sym, neg_number_of_bin_pred_iff_0]) 1);
-qed "Suc_diff_number_of";
-
-(* now redundant because of the inverse_fold simproc
- Addsimps [Suc_diff_number_of]; *)
-
-Goal "nat_case a f (number_of v) = \
-\ (let pv = number_of (bin_pred v) in \
-\ if neg pv then a else f (nat pv))";
-by (simp_tac
- (simpset() addsplits [nat.split]
- addsimps [Let_def, neg_number_of_bin_pred_iff_0]) 1);
-qed "nat_case_number_of";
-
-Goal "nat_case a f ((number_of v) + n) = \
-\ (let pv = number_of (bin_pred v) in \
-\ if neg pv then nat_case a f n else f (nat pv + n))";
-by (stac add_eq_if 1);
-by (asm_simp_tac
- (simpset() addsplits [nat.split]
- addsimps [numeral_1_eq_Suc_0 RS sym, Let_def,
- neg_imp_number_of_eq_0, neg_number_of_bin_pred_iff_0]) 1);
-qed "nat_case_add_eq_if";
-
-Addsimps [nat_case_number_of, nat_case_add_eq_if];
-
-
-Goal "nat_rec a f (number_of v) = \
-\ (let pv = number_of (bin_pred v) in \
-\ if neg pv then a else f (nat pv) (nat_rec a f (nat pv)))";
-by (case_tac "(number_of v)::nat" 1);
-by (ALLGOALS (asm_simp_tac
- (simpset() addsimps [Let_def, neg_number_of_bin_pred_iff_0])));
-by (asm_full_simp_tac (simpset() addsplits [split_if_asm]) 1);
-qed "nat_rec_number_of";
-
-Goal "nat_rec a f (number_of v + n) = \
-\ (let pv = number_of (bin_pred v) in \
-\ if neg pv then nat_rec a f n \
-\ else f (nat pv + n) (nat_rec a f (nat pv + n)))";
-by (stac add_eq_if 1);
-by (asm_simp_tac
- (simpset() addsplits [nat.split]
- addsimps [numeral_1_eq_Suc_0 RS sym, Let_def,
- neg_imp_number_of_eq_0, neg_number_of_bin_pred_iff_0]) 1);
-qed "nat_rec_add_eq_if";
-
-Addsimps [nat_rec_number_of, nat_rec_add_eq_if];
-
-
-(** For simplifying # m - Suc n **)
-
-Goal "m - Suc n = (m - 1) - n";
-by (simp_tac (numeral_ss addsplits [nat_diff_split]) 1);
-qed "diff_Suc_eq_diff_pred";
-
-(*Obsolete because of natdiff_cancel_numerals
- Addsimps [inst "m" "number_of ?v" diff_Suc_eq_diff_pred];
- It LOOPS if Numeral1 is being replaced by 1.
-*)
-
-
-(** Evens and Odds, for Mutilated Chess Board **)
-
-(*Case analysis on b<2*)
-Goal "(n::nat) < 2 ==> n = 0 | n = Suc 0";
-by (arith_tac 1);
-qed "less_2_cases";
-
-Goal "Suc(Suc(m)) mod 2 = m mod 2";
-by (subgoal_tac "m mod 2 < 2" 1);
-by (Asm_simp_tac 2);
-by (etac (less_2_cases RS disjE) 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [Let_def, mod_Suc, nat_1])));
-qed "mod2_Suc_Suc";
-Addsimps [mod2_Suc_Suc];
-
-Goal "!!m::nat. (0 < m mod 2) = (m mod 2 = 1)";
-by (subgoal_tac "m mod 2 < 2" 1);
-by (Asm_simp_tac 2);
-by (auto_tac (claset(), simpset() delsimps [mod_less_divisor]));
-qed "mod2_gr_0";
-Addsimps [mod2_gr_0];
-
-(** Removal of small numerals: Numeral0, Numeral1 and (in additive positions) 2 **)
-
-Goal "2 + n = Suc (Suc n)";
-by (Simp_tac 1);
-qed "add_2_eq_Suc";
-
-Goal "n + 2 = Suc (Suc n)";
-by (Simp_tac 1);
-qed "add_2_eq_Suc'";
-
-Addsimps [numeral_0_eq_0, numeral_1_eq_1, add_2_eq_Suc, add_2_eq_Suc'];
-
-(*Can be used to eliminate long strings of Sucs, but not by default*)
-Goal "Suc (Suc (Suc n)) = 3 + n";
-by (Simp_tac 1);
-qed "Suc3_eq_add_3";
-
-
-(** To collapse some needless occurrences of Suc
- At least three Sucs, since two and fewer are rewritten back to Suc again!
-
- We already have some rules to simplify operands smaller than 3.
-**)
-
-Goal "m div (Suc (Suc (Suc n))) = m div (3+n)";
-by (simp_tac (simpset() addsimps [Suc3_eq_add_3]) 1);
-qed "div_Suc_eq_div_add3";
-
-Goal "m mod (Suc (Suc (Suc n))) = m mod (3+n)";
-by (simp_tac (simpset() addsimps [Suc3_eq_add_3]) 1);
-qed "mod_Suc_eq_mod_add3";
-
-Addsimps [div_Suc_eq_div_add3, mod_Suc_eq_mod_add3];
-
-Goal "(Suc (Suc (Suc m))) div n = (3+m) div n";
-by (simp_tac (simpset() addsimps [Suc3_eq_add_3]) 1);
-qed "Suc_div_eq_add3_div";
-
-Goal "(Suc (Suc (Suc m))) mod n = (3+m) mod n";
-by (simp_tac (simpset() addsimps [Suc3_eq_add_3]) 1);
-qed "Suc_mod_eq_add3_mod";
-
-Addsimps [inst "n" "number_of ?v" Suc_div_eq_add3_div,
- inst "n" "number_of ?v" Suc_mod_eq_add3_mod];