--- a/src/HOL/Integ/NatBin.ML Tue Apr 18 15:51:59 2000 +0200
+++ b/src/HOL/Integ/NatBin.ML Tue Apr 18 15:53:50 2000 +0200
@@ -55,13 +55,19 @@
nat_number_of_def, int_Suc,
Suc_nat_eq_nat_zadd1, number_of_succ]) 1);
qed "Suc_nat_number_of";
+Addsimps [Suc_nat_number_of];
+
+Goal "Suc (number_of v + n) = \
+\ (if neg (number_of v) then #1+n else number_of (bin_succ v) + n)";
+by (Simp_tac 1);
+qed "Suc_nat_number_of_add";
Goal "Suc #0 = #1";
-by (simp_tac (simpset() addsimps [Suc_nat_number_of]) 1);
+by (Simp_tac 1);
qed "Suc_numeral_0_eq_1";
Goal "Suc #1 = #2";
-by (simp_tac (simpset() addsimps [Suc_nat_number_of]) 1);
+by (Simp_tac 1);
qed "Suc_numeral_1_eq_2";
(** Addition **)
@@ -256,7 +262,6 @@
Addsimps [le_nat_number_of_eq_not_less];
-
(*** New versions of existing theorems involving 0, 1, 2 ***)
fun change_theory thy th =
@@ -282,7 +287,6 @@
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');
@@ -300,7 +304,7 @@
(** Arith **)
Addsimps (map (rename_numerals thy)
- [diff_0_eq_0, add_0, add_0_right, add_pred,
+ [diff_0, diff_0_eq_0, add_0, add_0_right, add_pred,
diff_is_0_eq, zero_is_diff_eq, zero_less_diff,
mult_0, mult_0_right, mult_1, mult_1_right,
mult_is_0, zero_is_mult, zero_less_mult_iff,
@@ -462,6 +466,242 @@
(* Push int(.) inwards: *)
Addsimps [int_Suc,zadd_int RS sym];
+
+(*** Simprocs for nat numerals ***)
+
+(*Lemma used for cancel_numerals to prove #n <= i + ... + #m + ... j *)
+Goal "!!k::nat. k<=i | k <= j ==> k <= i+j";
+by Auto_tac;
+qed "disj_imp_le_add";
+
+
+structure Nat_Numeral_Simprocs =
+struct
+
+(*Utilities for simproc inverse_fold*)
+
+fun mk_numeral n = HOLogic.number_of_const $ NumeralSyntax.mk_bin n;
+
+(*Decodes a numeral to a NATURAL NUMBER*)
+fun dest_numeral (Const("Numeral.number_of", _) $ w) =
+ BasisLibrary.Int.max (0, NumeralSyntax.dest_bin w)
+ | dest_numeral t = raise TERM("dest_numeral", [t]);
+
+fun find_first_numeral past (t::terms) =
+ (dest_numeral t, t, rev past @ terms)
+ handle _ => find_first_numeral (t::past) terms;
+
+val zero = mk_numeral 0;
+val one = mk_numeral 1;
+val mk_plus = HOLogic.mk_binop "op +";
+
+fun mk_sum [] = HOLogic.zero
+ | mk_sum [t] = t
+ | mk_sum (t :: ts) = if t = zero then mk_sum ts
+ else mk_plus (t, mk_sum ts);
+
+val dest_plus = HOLogic.dest_bin "op +" HOLogic.natT;
+
+(*extract the outer Sucs from a term and convert them to a binary numeral*)
+fun dest_Sucs (k, Const ("Suc", _) $ t) = dest_Sucs (k+1, t)
+ | dest_Sucs (0, t) = t
+ | dest_Sucs (k, t) = mk_plus (mk_numeral k, t);
+
+fun dest_sum (Const ("0", _)) = []
+ | dest_sum t =
+ let val (t,u) = dest_plus t
+ in dest_sum t @ dest_sum u end
+ handle _ => [t];
+
+fun dest_Sucs_sum t = dest_sum (dest_Sucs (0,t));
+
+val mk_diff = HOLogic.mk_binop "op -";
+val dest_diff = HOLogic.dest_bin "op -" HOLogic.natT;
+
+val mk_eqv = HOLogic.mk_Trueprop o HOLogic.mk_eq;
+
+fun prove_conv tacs sg (t, u) =
+ if t aconv u then None
+ else
+ Some
+ (mk_meta_eq (prove_goalw_cterm [] (cterm_of sg (mk_eqv (t, u)))
+ (K tacs))
+ handle ERROR => error
+ ("The error(s) above occurred while trying to prove " ^
+ (string_of_cterm (cterm_of sg (mk_eqv (t, u))))));
+
+fun all_simp_tac ss rules = ALLGOALS (simp_tac (ss addsimps rules));
+
+val add_norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps add_ac));
+
+
+structure InverseFoldData =
+ struct
+ val mk_numeral = mk_numeral
+ val dest_numeral = dest_numeral
+ val find_first_numeral = find_first_numeral []
+ val mk_sum = mk_sum
+ val dest_sum = dest_Sucs_sum
+ val mk_diff = HOLogic.mk_binop "op -"
+ val dest_diff = HOLogic.dest_bin "op -" HOLogic.natT
+ val double_diff_eq = diff_add_assoc_diff
+ val move_diff_eq = diff_add_assoc2
+ val prove_conv = prove_conv
+ val numeral_simp_tac = all_simp_tac (simpset())
+ val add_norm_tac = ALLGOALS (simp_tac (simpset() addsimps Suc_eq_add_numeral_1::add_ac))
+ end;
+
+structure InverseFold = InverseFoldFun (InverseFoldData);
+
+structure FoldSuc = FoldSucFun
+ (open InverseFoldData
+ val dest_Suc = HOLogic.dest_Suc
+ val numeral_simp_tac = all_simp_tac (simpset()
+ addsimps [Suc_nat_number_of_add]));
+
+fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc;
+fun prep_pat s = Thm.read_cterm (Theory.sign_of Arith.thy) (s, HOLogic.termT);
+val prep_pats = map prep_pat;
+
+val inverse =
+ prep_simproc ("inverse_fold",
+ (map prep_pat ["((i::nat) + j) - number_of v",
+ "Suc i - number_of v"]),
+ InverseFold.proc);
+
+val fold_Suc =
+ prep_simproc ("fold_Suc",
+ [prep_pat "Suc (i + j)"],
+ FoldSuc.proc);
+
+(*To instantiate "k" in theorems such as eq_diff_iff*)
+fun subst_inst_tac th t =
+ instantiate' [None] [Some (cterm_of (sign_of thy) t)] th;
+
+fun mk_subst_tac th k = rtac (subst_inst_tac (th RS sym RS trans) k) 1;
+
+structure CommonData =
+ struct
+ val mk_numeral = mk_numeral
+ val find_first_numeral = find_first_numeral []
+ val mk_sum = mk_sum
+ val dest_sum = dest_Sucs_sum
+ val prove_conv = prove_conv
+ val all_simp_tac = all_simp_tac
+ (simpset() addsimprocs [inverse]) [disj_imp_le_add]
+ end;
+
+
+(* nat eq *)
+structure EqCancelNumerals = CancelNumeralsFun
+ (open CommonData
+ val mk_bal = HOLogic.mk_eq
+ val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
+ val subst_tac = mk_subst_tac eq_diff_iff);
+
+(* nat less *)
+structure LessCancelNumerals = CancelNumeralsFun
+ (open CommonData
+ val mk_bal = HOLogic.mk_binrel "op <"
+ val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT
+ val subst_tac = mk_subst_tac less_diff_iff);
+
+(* nat le *)
+structure LeCancelNumerals = CancelNumeralsFun
+ (open CommonData
+ val mk_bal = HOLogic.mk_binrel "op <="
+ val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT
+ val subst_tac = mk_subst_tac le_diff_iff);
+
+(* nat diff *)
+structure DiffCancelNumerals = CancelNumeralsFun
+ (open CommonData
+ val mk_bal = HOLogic.mk_binop "op -"
+ val dest_bal = HOLogic.dest_bin "op -" HOLogic.natT
+ val subst_tac = mk_subst_tac diff_diff_eq);
+
+val eq_pats = prep_pats ["(l::nat) + m = n", "(l::nat) = m + n"];
+val less_pats = prep_pats ["(l::nat) + m < n", "(l::nat) < m + n"];
+val le_pats = prep_pats ["(l::nat) + m <= n", "(l::nat) <= m + n"];
+
+val diff_pat = prep_pat "(l::nat) - (m + n)";
+ (*but ((l::nat) + m) - n" is covered by inverse_fold*)
+
+val cancel =
+ map prep_simproc
+ [("nateq_cancel_numerals", eq_pats, EqCancelNumerals.proc),
+ ("natless_cancel_numerals", less_pats, LessCancelNumerals.proc),
+ ("natle_cancel_numerals", le_pats, LeCancelNumerals.proc),
+ ("natdiff_cancel_numerals", [diff_pat], DiffCancelNumerals.proc)];
+
+end;
+
+
+Addsimprocs [Nat_Numeral_Simprocs.inverse, Nat_Numeral_Simprocs.fold_Suc];
+Addsimprocs Nat_Numeral_Simprocs.cancel;
+
+(*examples:
+print_depth 22;
+set proof_timing;
+fun try s = (Goal s; by (simp_tac (simpset()
+ addsimprocs Nat_Numeral_Simprocs.cancel @
+ [Nat_Numeral_Simprocs.inverse, Nat_Numeral_Simprocs.fold_Suc]) 1));
+
+(*inverse*)
+try "((i + j) + #12 + (k::nat)) - #15 = y";
+try "((i + j) + #-12 + (k::nat)) - #15 = y";
+try "((i + j) + #12 + (k::nat)) - #-15 = y";
+try "(i + j + #22 + (k::nat)) - #15 = y";
+try "((i + j) + #-12 + (k::nat)) - #-15 = y";
+try "#7 + u - #5 = (yy::nat)";
+try "#2 + u - #5 = (yy::nat)";
+
+(*cancel*)
+try "((i + j) + #12 + (k::nat)) = u + #15 + y";
+try "((i + j) + #12 + (k::nat)) <= u + #15 + y";
+try "((i + j) + #32 + (k::nat)) - (u + #15 + y) = zz";
+try "((i + j) + #12 + (k::nat)) = u + #5 + y";
+(*negative numerals*)
+try "((i + j) + #-23 + (k::nat)) < u + #15 + y";
+try "((i + j) + #3 + (k::nat)) < u + #-15 + y";
+
+(*fold_Suc*)
+try "Suc (i + j + #3 + k) = u";
+try "Suc (i + j + #-3 + k) = u";
+
+
+try "Suc u - #2 = y";
+try "Suc (Suc (Suc u)) - #2 = y";
+
+
+try "((i + j) + #12 + k) = Suc (u + y)";
+try "(i + #2) = Suc u";
+try "Suc (Suc (Suc (Suc (Suc (u + y))))) <= ((i + j) + #41 + k)";
+
+try "((i + j) + #5 + k) = Suc (Suc (Suc (Suc (Suc (u + y)))))";
+(*SLOW because of Addsimps [less_SucI, le_SucI];*)
+try "((i + j) + #5 + k) < Suc (Suc (Suc (Suc (Suc (u + y)))))";
+try "((i + j) + #5 + k) <= Suc (Suc (Suc (Suc (Suc (u + y)))))";
+try "((i + j) + #5 + k) = Suc (Suc (Suc (Suc (Suc (u + y)))))";
+
+
+(*so why is this fast?*)
+try "((i + j) + #41 + k) < (#5::nat) + (u + y)";
+
+
+try "((i + j) + #1 + k) = Suc (Suc (u + y))";
+
+
+try "((i + j) + #1 + k) - #1 = (yy::nat)";
+try "Suc (Suc (u + y)) - #1 = (yy::nat)";
+
+try "((i + j) + #41 + k) - #5 = 0";
+try "Suc (Suc (Suc (Suc (Suc (u + y))))) - #5 = 0";
+
+try "((i + j) + #5 + k) = Suc (Suc (Suc (Suc (Suc (Suc (Suc (u + y)))))))";
+*)
+
+
(*** Prepare linear arithmetic for nat numerals ***)
let
@@ -482,3 +722,43 @@
LA_Data_Ref.ss_ref := !LA_Data_Ref.ss_ref addsimps add_rules
addsimprocs simprocs
end;
+
+
+
+(** For simplifying Suc m - #n **)
+
+Goal "#0 < n ==> Suc m - n = m - (n - #1)";
+by (asm_full_simp_tac (numeral_ss 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)";
+by (subgoal_tac "neg (number_of (bin_pred v)) = (number_of v < 1)" 1);
+by (Asm_simp_tac 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
+ (simpset_of Int.thy addsimps [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]; *)
+
+
+(** 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";
+
+Addsimps [inst "m" "number_of ?v" diff_Suc_eq_diff_pred];