--- a/src/HOL/Integ/Bin.ML Fri Sep 18 16:04:44 1998 +0200
+++ b/src/HOL/Integ/Bin.ML Fri Sep 18 16:05:08 1998 +0200
@@ -102,21 +102,19 @@
qed_goal "integ_of_norm_Bcons" Bin.thy
"integ_of(norm_Bcons w b) = integ_of(Bcons w b)"
(fn _ =>[(induct_tac "w" 1),
- (ALLGOALS (asm_simp_tac
- (simpset() addsimps [zadd_zminus_inverse_nat]))) ]);
+ (ALLGOALS Asm_simp_tac) ]);
-val integ_of_norm_Cons_simps =
- [zadd_zminus_inverse_nat, integ_of_norm_Bcons] @ zadd_ac;
+Addsimps [integ_of_norm_Bcons];
qed_goal "integ_of_succ" Bin.thy
"integ_of(bin_succ w) = $#1 + integ_of w"
(fn _ =>[(rtac bin.induct 1),
- (ALLGOALS(asm_simp_tac (simpset() addsimps integ_of_norm_Cons_simps))) ]);
+ (ALLGOALS(asm_simp_tac (simpset() addsimps zadd_ac))) ]);
qed_goal "integ_of_pred" Bin.thy
"integ_of(bin_pred w) = - ($#1) + integ_of w"
(fn _ =>[(rtac bin.induct 1),
- (ALLGOALS(asm_simp_tac (simpset() addsimps integ_of_norm_Cons_simps))) ]);
+ (ALLGOALS(asm_simp_tac (simpset() addsimps zadd_ac))) ]);
Goal "integ_of(bin_minus w) = - (integ_of w)";
by (rtac bin.induct 1);
@@ -129,11 +127,8 @@
qed "integ_of_minus";
-val bin_add_simps = [zadd_zminus_inverse_nat, zadd_zminus_inverse_nat2,
- bin_add_Bcons_Plus,
- bin_add_Bcons_Minus,bin_add_Bcons_Bcons,
- integ_of_succ, integ_of_pred,
- integ_of_norm_Bcons];
+val bin_add_simps = [bin_add_Bcons_Bcons,
+ integ_of_succ, integ_of_pred];
Goal "! w. integ_of(bin_add v w) = integ_of v + integ_of w";
by (induct_tac "v" 1);
@@ -144,8 +139,7 @@
by (ALLGOALS (asm_simp_tac (simpset() addsimps (bin_add_simps @ zadd_ac))));
qed_spec_mp "integ_of_add";
-val bin_mult_simps = [zmult_zminus,
- integ_of_minus, integ_of_add,
+val bin_mult_simps = [zmult_zminus, integ_of_minus, integ_of_add,
integ_of_norm_Bcons];
@@ -158,17 +152,6 @@
zadd_ac)) 1);
qed "integ_of_mult";
-(* #0 = $# 0 *)
-bind_thm ("int_eq_nat0", integ_of_Plus);
-
-Goal "$# 1 = #1";
-by (Simp_tac 1);
-qed "int_eq_nat1";
-
-Goal "$# 2 = #2";
-by (simp_tac (simpset() addsimps [add_znat]) 1);
-qed "int_eq_nat2";
-
(** Simplification rules with integer constants **)
@@ -181,13 +164,16 @@
qed "zadd_0_right";
Goal "z + (- z) = #0";
-by (simp_tac (simpset() addsimps [zadd_zminus_inverse_nat]) 1);
+by (Simp_tac 1);
qed "zadd_zminus_inverse";
Goal "(- z) + z = #0";
-by (simp_tac (simpset() addsimps [zadd_zminus_inverse_nat2]) 1);
+by (Simp_tac 1);
qed "zadd_zminus_inverse2";
+(*These rewrite to $# 0. Henceforth we should rewrite to #0 *)
+Delsimps [zadd_zminus_inverse_nat, zadd_zminus_inverse_nat2];
+
Addsimps [zadd_0, zadd_0_right, zadd_zminus_inverse, zadd_zminus_inverse2];
Goal "- (#0) = #0";
@@ -233,6 +219,15 @@
qed "add1_zle_eq";
Addsimps [add1_zle_eq];
+Goal "znegative x = (x < #0)";
+by (simp_tac (simpset() addsimps [znegative_eq_less_nat0]) 1);
+qed "znegative_eq_less_0";
+
+Goal "(~znegative x) = ($# 0 <= x)";
+by (simp_tac (simpset() addsimps [not_znegative_eq_ge_nat0]) 1);
+qed "not_znegative_eq_ge_0";
+
+
(** Simplification rules for comparison of binary numbers (Norbert Voelker) **)
@@ -284,7 +279,7 @@
by (Asm_simp_tac 1);
by (int_case_tac "integ_of w" 1);
by (ALLGOALS (asm_simp_tac
- (simpset() addsimps ([add_znat, znegative_eq_less_0,
+ (simpset() addsimps ([add_znat, znegative_eq_less_nat0,
symmetric zdiff_def] @
zcompare_rls))));
qed "neg_integ_of_Bcons";
@@ -306,14 +301,14 @@
Addsimps [integ_of_add RS sym,
integ_of_minus RS sym,
integ_of_mult RS sym,
- bin_succ_Bcons1,bin_succ_Bcons0,
- bin_pred_Bcons1,bin_pred_Bcons0,
- bin_minus_Bcons1,bin_minus_Bcons0,
- bin_add_Bcons_Plus,bin_add_Bcons_Minus,
- bin_add_Bcons_Bcons0,bin_add_Bcons_Bcons10,bin_add_Bcons_Bcons11,
- bin_mult_Bcons1,bin_mult_Bcons0,
- norm_Bcons_Plus_0,norm_Bcons_Plus_1,
- norm_Bcons_Minus_0,norm_Bcons_Minus_1,
+ bin_succ_Bcons1, bin_succ_Bcons0,
+ bin_pred_Bcons1, bin_pred_Bcons0,
+ bin_minus_Bcons1, bin_minus_Bcons0,
+ bin_add_Bcons_Plus, bin_add_Bcons_Minus,
+ bin_add_Bcons_Bcons0, bin_add_Bcons_Bcons10, bin_add_Bcons_Bcons11,
+ bin_mult_Bcons1, bin_mult_Bcons0,
+ norm_Bcons_Plus_0, norm_Bcons_Plus_1,
+ norm_Bcons_Minus_0, norm_Bcons_Minus_1,
norm_Bcons_Bcons];
(*... and simplification of relational operations*)
@@ -330,3 +325,65 @@
(*... and finally subtraction*)
Addsimps [diff_integ_of_eq];
+
+
+(** Simplification of inequalities involving numerical constants **)
+
+Goal "(w <= z + #1) = (w<=z | w = z + #1)";
+by (simp_tac (simpset() addsimps [zle_eq_zless_or_eq, zless_add1_eq]) 1);
+qed "zle_add1_eq";
+
+Goal "(w <= z - #1) = (w<z)";
+by (simp_tac (simpset() addsimps zcompare_rls) 1);
+qed "zle_diff1_eq";
+Addsimps [zle_diff1_eq];
+
+(*2nd premise can be proved automatically if v is a literal*)
+Goal "[| w <= z; #0 <= v |] ==> w <= z + v";
+by (dtac zadd_zle_mono 1);
+by (assume_tac 1);
+by (Full_simp_tac 1);
+qed "zle_imp_zle_zadd";
+
+Goal "w <= z ==> w <= z + #1";
+by (asm_simp_tac (simpset() addsimps [zle_imp_zle_zadd]) 1);
+qed "zle_imp_zle_zadd1";
+
+(*2nd premise can be proved automatically if v is a literal*)
+Goal "[| w < z; #0 <= v |] ==> w < z + v";
+by (dtac zadd_zless_mono 1);
+by (assume_tac 1);
+by (Full_simp_tac 1);
+qed "zless_imp_zless_zadd";
+
+Goal "w < z ==> w < z + #1";
+by (asm_simp_tac (simpset() addsimps [zless_imp_zless_zadd]) 1);
+qed "zless_imp_zless_zadd1";
+
+Goal "(w < z + #1) = (w<=z)";
+by (simp_tac (simpset() addsimps [zless_add1_eq, zle_eq_zless_or_eq]) 1);
+qed "zle_add1_eq_le";
+Addsimps [zle_add1_eq_le];
+
+Goal "(z = z + w) = (w = #0)";
+by (rtac trans 1);
+by (rtac zadd_left_cancel 2);
+by (simp_tac (simpset() addsimps [eq_sym_conv]) 1);
+qed "zadd_left_cancel0";
+Addsimps [zadd_left_cancel0];
+
+(*LOOPS as a simprule!*)
+Goal "[| w + v < z; #0 <= v |] ==> w < z";
+by (dtac zadd_zless_mono 1);
+by (assume_tac 1);
+by (full_simp_tac (simpset() addsimps zadd_ac) 1);
+qed "zless_zadd_imp_zless";
+
+(*LOOPS as a simprule!*)
+Goal "w + #1 < z ==> w < z";
+bd zless_zadd_imp_zless 1;
+ba 2;
+by (Simp_tac 1);
+qed "zless_zadd1_imp_zless";
+
+