# HG changeset patch
# User paulson
# Date 906127508 -7200
# Node ID ad120f7c52ad009b06e0a8a5f79fa5b0c56ec4a7
# Parent  c38cc427976c6126c05a3dcc47afe6ba48dde3ab
improved (but still flawed) treatment of binary arithmetic

diff -r c38cc427976c -r ad120f7c52ad src/HOL/Integ/Bin.ML
--- 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";
+
+
diff -r c38cc427976c -r ad120f7c52ad src/HOL/Integ/Bin.thy
--- a/src/HOL/Integ/Bin.thy	Fri Sep 18 16:04:44 1998 +0200
+++ b/src/HOL/Integ/Bin.thy	Fri Sep 18 16:05:08 1998 +0200
@@ -86,11 +86,6 @@
 	            (bin_add v (if (x & y) then bin_succ w else w)) (x~=y)" 
 
 
-(*For implementing the equality test on integer constants*)
-constdefs
-  iszero :: int => bool
-  "iszero z == z = $# 0"
-  
 end
 
 ML