src/HOL/Integ/NatSimprocs.ML
changeset 8865 06d842030c11
parent 8850 03cb6625c4a5
child 8877 9d6514fcd584
--- a/src/HOL/Integ/NatSimprocs.ML	Fri May 12 15:11:42 2000 +0200
+++ b/src/HOL/Integ/NatSimprocs.ML	Fri May 12 15:14:08 2000 +0200
@@ -24,42 +24,42 @@
 (** For cancel_numerals **)
 
 Goal "j <= (i::nat) ==> ((i*u + m) - (j*u + n)) = (((i-j)*u + m) - n)";
-by (asm_simp_tac (simpset() addsplits [nat_diff_split'] 
+by (asm_simp_tac (simpset() addsplits [nat_diff_split] 
 		            addsimps [add_mult_distrib]) 1);
 qed "nat_diff_add_eq1";
 
 Goal "i <= (j::nat) ==> ((i*u + m) - (j*u + n)) = (m - ((j-i)*u + n))";
-by (asm_simp_tac (simpset() addsplits [nat_diff_split'] 
+by (asm_simp_tac (simpset() addsplits [nat_diff_split] 
 		            addsimps [add_mult_distrib]) 1);
 qed "nat_diff_add_eq2";
 
 Goal "j <= (i::nat) ==> (i*u + m = j*u + n) = ((i-j)*u + m = n)";
-by (auto_tac (claset(), simpset() addsplits [nat_diff_split'] 
+by (auto_tac (claset(), simpset() addsplits [nat_diff_split] 
                                   addsimps [add_mult_distrib]));
 qed "nat_eq_add_iff1";
 
 Goal "i <= (j::nat) ==> (i*u + m = j*u + n) = (m = (j-i)*u + n)";
-by (auto_tac (claset(), simpset() addsplits [nat_diff_split'] 
+by (auto_tac (claset(), simpset() addsplits [nat_diff_split] 
                                   addsimps [add_mult_distrib]));
 qed "nat_eq_add_iff2";
 
 Goal "j <= (i::nat) ==> (i*u + m < j*u + n) = ((i-j)*u + m < n)";
-by (auto_tac (claset(), simpset() addsplits [nat_diff_split'] 
+by (auto_tac (claset(), simpset() addsplits [nat_diff_split] 
                                   addsimps [add_mult_distrib]));
 qed "nat_less_add_iff1";
 
 Goal "i <= (j::nat) ==> (i*u + m < j*u + n) = (m < (j-i)*u + n)";
-by (auto_tac (claset(), simpset() addsplits [nat_diff_split'] 
+by (auto_tac (claset(), simpset() addsplits [nat_diff_split] 
                                   addsimps [add_mult_distrib]));
 qed "nat_less_add_iff2";
 
 Goal "j <= (i::nat) ==> (i*u + m <= j*u + n) = ((i-j)*u + m <= n)";
-by (auto_tac (claset(), simpset() addsplits [nat_diff_split'] 
+by (auto_tac (claset(), simpset() addsplits [nat_diff_split] 
                                   addsimps [add_mult_distrib]));
 qed "nat_le_add_iff1";
 
 Goal "i <= (j::nat) ==> (i*u + m <= j*u + n) = (m <= (j-i)*u + n)";
-by (auto_tac (claset(), simpset() addsplits [nat_diff_split'] 
+by (auto_tac (claset(), simpset() addsplits [nat_diff_split] 
                                   addsimps [add_mult_distrib]));
 qed "nat_le_add_iff2";
 
@@ -115,8 +115,6 @@
 
 val prove_conv = Int_Numeral_Simprocs.prove_conv;
 
-val simplify_meta_eq = Int_Numeral_Simprocs.simplify_meta_eq;
-
 val bin_simps = [add_nat_number_of, nat_number_of_add_left,
 		 diff_nat_number_of, le_nat_number_of_eq_not_less, 
 		 less_nat_number_of, Let_number_of, nat_number_of] @ 
@@ -168,6 +166,12 @@
 val add_0s = map (rename_numerals NatBin.thy) [add_0, add_0_right];
 val mult_1s = map (rename_numerals NatBin.thy) [mult_1, mult_1_right];
 
+(*Final simplification: cancel + and *; replace #0 by 0 and #1 by 1*)
+val simplify_meta_eq = 
+    Int_Numeral_Simprocs.simplify_meta_eq
+         [numeral_0_eq_0, numeral_1_eq_1, add_0, add_0_right,
+	 mult_0, mult_0_right, mult_1, mult_1_right];
+
 structure CancelNumeralsCommon =
   struct
   val mk_sum    	= mk_sum
@@ -183,7 +187,7 @@
 				(HOL_ss addsimps bin_simps@add_ac@mult_ac))
   val numeral_simp_tac	= ALLGOALS
                 (simp_tac (HOL_ss addsimps [numeral_0_eq_0 RS sym]@add_0s@bin_simps))
-  val simplify_meta_eq  = simplify_meta_eq (add_0s@mult_1s)
+  val simplify_meta_eq  = simplify_meta_eq
   end;
 
 
@@ -264,7 +268,7 @@
 				(HOL_ss addsimps bin_simps@add_ac@mult_ac))
   val numeral_simp_tac	= ALLGOALS
                 (simp_tac (HOL_ss addsimps [numeral_0_eq_0 RS sym]@add_0s@bin_simps))
-  val simplify_meta_eq  = simplify_meta_eq (add_0s@mult_1s)
+  val simplify_meta_eq  = simplify_meta_eq
   end;
 
 structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
@@ -281,14 +285,6 @@
 Addsimprocs [Nat_Numeral_Simprocs.combine_numerals];
 
 
-(*If the result is just #1 + ..., replace it by Suc so that primrecs, etc.
-  will work.*)
-Goal "#1 + n = Suc n";
-by Auto_tac;
-qed "one_plus_eq_Suc";
-Addsimps [one_plus_eq_Suc];
-
-
 (*examples:
 print_depth 22;
 set proof_timing;
@@ -305,12 +301,11 @@
 test "(i + j + #12 + (k::nat)) - #5 = y";
 test "Suc u - #2 = y";
 test "Suc (Suc (Suc u)) - #2 = y";
-(*Unary*)
 test "(i + j + #2 + (k::nat)) - 1 = y";
 test "(i + j + #1 + (k::nat)) - 2 = y";
 
 test "(#2*x + (u*v) + y) - v*#3*u = (w::nat)";
-test "(#2*x*u*v + (u*v)*#4 + y) - v*u*#4 = (w::nat)";
+test "(#2*x*u*v + #5 + (u*v)*#4 + y) - v*u*#4 = (w::nat)";
 test "(#2*x*u*v + (u*v)*#4 + y) - v*u = (w::nat)";
 test "Suc (Suc (#2*x*u*v + u*#4 + y)) - u = w";
 test "Suc ((u*v)*#4) - v*#3*u = w";
@@ -379,7 +374,7 @@
 (** 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);
+by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1);
 qed "Suc_diff_eq_diff_pred";
 
 (*Now just instantiating n to (number_of v) does the right simplification,
@@ -398,18 +393,61 @@
 by (Simp_tac 1);
 by (Simp_tac 1);
 by (asm_full_simp_tac
-    (simpset_of Int.thy addsimps [less_0_number_of RS sym, 
+    (simpset_of Int.thy 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 [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 [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);
+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];