# HG changeset patch
# User paulson
# Date 956066030 -7200
# Node ID f9733879ff25928923591bc514099d0468ad840f
# Parent  0bfd6678a5fa6a880ef16bec0e8522cb1bf1281a
instantiates new simprocs for numerals of type "nat"

diff -r 0bfd6678a5fa -r f9733879ff25 src/HOL/Integ/NatBin.ML
--- 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];