# HG changeset patch
# User paulson
# Date 906649644 -7200
# Node ID ed5e19bc7e324e5ba20294172418ff489298f7a1
# Parent  8375188ae9b0682d1313ad68bfaf29f4fe5ad90c
renamed some axioms; some new theorems

diff -r 8375188ae9b0 -r ed5e19bc7e32 src/HOL/Integ/Bin.ML
--- a/src/HOL/Integ/Bin.ML	Thu Sep 24 16:53:14 1998 +0200
+++ b/src/HOL/Integ/Bin.ML	Thu Sep 24 17:07:24 1998 +0200
@@ -65,9 +65,10 @@
     "bin_add (v BIT False) (w BIT y) = NCons (bin_add v w) y"
  (fn _ => [Auto_tac]);
 
-qed_goal "bin_add_BIT_Pls" Bin.thy
-    "bin_add (v BIT x) Pls = v BIT x"
- (fn _ => [(Simp_tac 1)]);
+Goal "bin_add w Pls = w";
+by (induct_tac "w" 1);
+by Auto_tac;
+qed "bin_add_Pls_right";
 
 qed_goal "bin_add_BIT_Min" Bin.thy
     "bin_add (v BIT x) Min = bin_pred (v BIT x)"
@@ -117,7 +118,7 @@
 by (Simp_tac 1);
 by (Simp_tac 1);
 by (asm_simp_tac (simpset()
-		  delsimps [pred_Pls,pred_Min,pred_BIT]
+		  delsimps [bin_pred_Pls, bin_pred_Min, bin_pred_BIT]
 		  addsimps [integ_of_succ,integ_of_pred,
 			    zadd_assoc]) 1);
 qed "integ_of_minus";
@@ -285,8 +286,8 @@
 qed "le_integ_of_eq_not_less"; 
 
 (*Delete the original rewrites, with their clumsy conditional expressions*)
-Delsimps [succ_BIT, pred_BIT, minus_BIT, 
-          NCons_Pls, NCons_Min, add_BIT, mult_BIT];
+Delsimps [bin_succ_BIT, bin_pred_BIT, bin_minus_BIT, 
+          NCons_Pls, NCons_Min, bin_add_BIT, bin_mult_BIT];
 
 (*Hide the binary representation of integer constants*)
 Delsimps [integ_of_Pls, integ_of_Min, integ_of_BIT];
@@ -298,7 +299,7 @@
           bin_succ_1, bin_succ_0, 
           bin_pred_1, bin_pred_0, 
           bin_minus_1, bin_minus_0,  
-          bin_add_BIT_Pls, bin_add_BIT_Min,
+          bin_add_Pls_right, bin_add_BIT_Min,
           bin_add_BIT_0, bin_add_BIT_10, bin_add_BIT_11,
           bin_mult_1, bin_mult_0, 
           NCons_Pls_0, NCons_Pls_1, 
@@ -380,4 +381,47 @@
 by (Simp_tac 1);
 qed "zless_zadd1_imp_zless";
 
+Goal "w + #-1 = w - #1";
+by (simp_tac (simpset() addsimps zadd_ac@zcompare_0_rls) 1);
+qed "zplus_minus1_conv";
 
+(*Eliminates neg from the subgoal, introduced e.g. by zcompare_0_rls*)
+val no_neg_ss = 
+    simpset()
+      delsimps [less_integ_of_eq_neg]  (*loops: it introduces neg*)
+      addsimps [zadd_assoc RS sym, zplus_minus1_conv,
+		neg_eq_less_0, iszero_def] @ zcompare_rls;
+
+
+(*** nat_of ***)
+
+Goal "#0 <= z ==> $# (nat_of z) = z"; 
+by (asm_full_simp_tac
+    (simpset() addsimps [neg_eq_less_0, zle_def, not_neg_nat_of]) 1); 
+qed "nat_of_0_le"; 
+
+Goal "z < #0 ==> nat_of z = 0"; 
+by (asm_full_simp_tac
+    (simpset() addsimps [neg_eq_less_0, zle_def, neg_nat_of]) 1); 
+qed "nat_of_less_0"; 
+
+Addsimps [nat_of_0_le, nat_of_less_0];
+
+Goal "#0 <= w ==> (nat_of w = m) = (w = $# m)";
+by Auto_tac;
+qed "nat_of_eq_iff";
+
+Goal "#0 <= w ==> (nat_of w < m) = (w < $# m)";
+by (rtac iffI 1);
+by (asm_full_simp_tac 
+    (simpset() delsimps [zless_eq_less] addsimps [zless_eq_less RS sym]) 2);
+by (etac (nat_of_0_le RS subst) 1);
+by (Simp_tac 1);
+qed "nat_of_less_iff";
+
+Goal "#0 <= w ==> (nat_of w < nat_of z) = (w<z)";
+by (case_tac "neg z" 1);
+by (auto_tac (claset(), simpset() addsimps [nat_of_less_iff]));
+by (auto_tac (claset() addIs [zless_trans], 
+	      simpset() addsimps [neg_eq_less_0, integ_of_Pls, zle_def]));
+qed "nat_of_less_eq_zless";