author paulson Fri, 12 May 2000 15:14:08 +0200 changeset 8865 06d842030c11 parent 8864 a12ccd629e2c child 8866 9ac6a18d363b
new simprules for nat_case and nat_rec simplify_meta_eq now maps #0 to 0 and #1 to 1 in its result
```--- 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)";

Goal "i <= (j::nat) ==> ((i*u + m) - (j*u + n)) = (m - ((j-i)*u + n))";

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]

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]

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]

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]

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]

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]

@@ -115,8 +115,6 @@

val prove_conv = Int_Numeral_Simprocs.prove_conv;

-val simplify_meta_eq = Int_Numeral_Simprocs.simplify_meta_eq;
-
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 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
+	 mult_0, mult_0_right, mult_1, mult_1_right];
+
structure CancelNumeralsCommon =
struct
val mk_sum    	= mk_sum
@@ -183,7 +187,7 @@
val numeral_simp_tac	= ALLGOALS
-  val simplify_meta_eq  = simplify_meta_eq (add_0s@mult_1s)
+  val simplify_meta_eq  = simplify_meta_eq
end;

@@ -264,7 +268,7 @@
val numeral_simp_tac	= ALLGOALS
-  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 @@

-(*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";
-
-
(*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

+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
+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 (asm_simp_tac
+			 neg_number_of_bin_pred_iff_0]) 1);
+
+
+
+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
+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 (asm_simp_tac
+			 neg_number_of_bin_pred_iff_0]) 1);