# HG changeset patch
# User paulson
# Date 849020368 -3600
# Node ID 4fc4b465be5b93e11687acc64826b3f03fe65ae3
# Parent  4b43a8d046e5fd0f96465b064e7ab09f957193b0
New material from Norbert Voelker for efficient binary comparisons

diff -r 4b43a8d046e5 -r 4fc4b465be5b src/HOL/Integ/Bin.ML
--- a/src/HOL/Integ/Bin.ML	Tue Nov 26 14:28:17 1996 +0100
+++ b/src/HOL/Integ/Bin.ML	Tue Nov 26 15:59:28 1996 +0100
@@ -1,6 +1,6 @@
-(*  Title:	HOL/Integ/Bin.ML
-    Authors:	Lawrence C Paulson, Cambridge University Computer Laboratory
-		David Spelt, University of Twente 
+(*  Title:      HOL/Integ/Bin.ML
+    Authors:    Lawrence C Paulson, Cambridge University Computer Laboratory
+                David Spelt, University of Twente 
     Copyright   1994  University of Cambridge
     Copyright   1996 University of Twente
 
@@ -11,132 +11,148 @@
 
 (** extra rules for bin_succ, bin_pred, bin_add, bin_mult **)
 
-qed_goal "norm_Bcons_Plus_0" Bin.thy "norm_Bcons Plus False = Plus"
-	(fn prem => [(Simp_tac 1)]);
+qed_goal "norm_Bcons_Plus_0" Bin.thy
+    "norm_Bcons Plus False = Plus"
+ (fn _ => [(Simp_tac 1)]);
 
-qed_goal "norm_Bcons_Plus_1" Bin.thy "norm_Bcons Plus True = Bcons Plus True"
-	(fn prem => [(Simp_tac 1)]);
+qed_goal "norm_Bcons_Plus_1" Bin.thy
+    "norm_Bcons Plus True = Bcons Plus True"
+ (fn _ => [(Simp_tac 1)]);
 
-qed_goal "norm_Bcons_Minus_0" Bin.thy "norm_Bcons Minus False = Bcons Minus False"
-	(fn prem => [(Simp_tac 1)]);
+qed_goal "norm_Bcons_Minus_0" Bin.thy
+    "norm_Bcons Minus False = Bcons Minus False"
+ (fn _ => [(Simp_tac 1)]);
 
-qed_goal "norm_Bcons_Minus_1" Bin.thy "norm_Bcons Minus True = Minus"
-	(fn prem => [(Simp_tac 1)]);
+qed_goal "norm_Bcons_Minus_1" Bin.thy
+    "norm_Bcons Minus True = Minus"
+ (fn _ => [(Simp_tac 1)]);
 
-qed_goal "norm_Bcons_Bcons" Bin.thy "norm_Bcons (Bcons w x) b = Bcons (Bcons w x) b"
-	(fn prem => [(Simp_tac 1)]);
+qed_goal "norm_Bcons_Bcons" Bin.thy
+    "norm_Bcons (Bcons w x) b = Bcons (Bcons w x) b"
+ (fn _ => [(Simp_tac 1)]);
 
-qed_goal "bin_succ_Bcons1" Bin.thy "bin_succ(Bcons w True) = Bcons (bin_succ w) False"
-	(fn prem => [(Simp_tac 1)]);
+qed_goal "bin_succ_Bcons1" Bin.thy
+    "bin_succ(Bcons w True) = Bcons (bin_succ w) False"
+ (fn _ => [(Simp_tac 1)]);
 
-qed_goal "bin_succ_Bcons0" Bin.thy "bin_succ(Bcons w False) =  norm_Bcons w True"
-	(fn prem => [(Simp_tac 1)]);
+qed_goal "bin_succ_Bcons0" Bin.thy
+    "bin_succ(Bcons w False) =  norm_Bcons w True"
+ (fn _ => [(Simp_tac 1)]);
 
-qed_goal "bin_pred_Bcons1" Bin.thy "bin_pred(Bcons w True) = norm_Bcons w False"
-	(fn prem => [(Simp_tac 1)]);
+qed_goal "bin_pred_Bcons1" Bin.thy
+    "bin_pred(Bcons w True) = norm_Bcons w False"
+ (fn _ => [(Simp_tac 1)]);
 
-qed_goal "bin_pred_Bcons0" Bin.thy "bin_pred(Bcons w False) = Bcons (bin_pred w) True"
-	(fn prem => [(Simp_tac 1)]);
+qed_goal "bin_pred_Bcons0" Bin.thy
+    "bin_pred(Bcons w False) = Bcons (bin_pred w) True"
+ (fn _ => [(Simp_tac 1)]);
 
-qed_goal "bin_minus_Bcons1" Bin.thy "bin_minus(Bcons w True) = bin_pred (Bcons(bin_minus w) False)"
-	(fn prem => [(Simp_tac 1)]);
+qed_goal "bin_minus_Bcons1" Bin.thy
+    "bin_minus(Bcons w True) = bin_pred (Bcons(bin_minus w) False)"
+ (fn _ => [(Simp_tac 1)]);
 
-qed_goal "bin_minus_Bcons0" Bin.thy "bin_minus(Bcons w False) = Bcons (bin_minus w) False"
-	(fn prem => [(Simp_tac 1)]);
+qed_goal "bin_minus_Bcons0" Bin.thy
+    "bin_minus(Bcons w False) = Bcons (bin_minus w) False"
+ (fn _ => [(Simp_tac 1)]);
 
 (*** bin_add: binary addition ***)
 
-qed_goal "bin_add_Bcons_Bcons11" Bin.thy "bin_add (Bcons v True) (Bcons w True) = norm_Bcons (bin_add v (bin_succ w)) False"
-	(fn prem => [(Simp_tac 1)]);
+qed_goal "bin_add_Bcons_Bcons11" Bin.thy
+    "bin_add (Bcons v True) (Bcons w True) = \
+\    norm_Bcons (bin_add v (bin_succ w)) False"
+ (fn _ => [(Simp_tac 1)]);
 
-qed_goal "bin_add_Bcons_Bcons10" Bin.thy "bin_add (Bcons v True) (Bcons w False) = norm_Bcons (bin_add v w) True"
-	(fn prem => [(Simp_tac 1)]);
+qed_goal "bin_add_Bcons_Bcons10" Bin.thy
+    "bin_add (Bcons v True) (Bcons w False) = norm_Bcons (bin_add v w) True"
+ (fn _ => [(Simp_tac 1)]);
 
-(* SHOULD THIS THEOREM BE ADDED TO HOL_SS ? *)
-val my = prove_goal HOL.thy "(False = (~P)) = P"
-	(fn prem => [(Fast_tac 1)]);
+val lemma = prove_goal HOL.thy "(False = (~P)) = P"
+ (fn _ => [(Fast_tac 1)]);
 
-qed_goal "bin_add_Bcons_Bcons0" Bin.thy "bin_add (Bcons v False) (Bcons w y) = norm_Bcons (bin_add v w) y"
-	(fn prem => [(simp_tac (!simpset addsimps [my]) 1)]);
+qed_goal "bin_add_Bcons_Bcons0" Bin.thy
+    "bin_add (Bcons v False) (Bcons w y) = norm_Bcons (bin_add v w) y"
+ (fn _ => [(simp_tac (!simpset addsimps [lemma]) 1)]);
 
-qed_goal "bin_add_Bcons_Plus" Bin.thy "bin_add (Bcons v x) Plus = Bcons v x"
-	(fn prems => [(Simp_tac 1)]);
+qed_goal "bin_add_Bcons_Plus" Bin.thy
+    "bin_add (Bcons v x) Plus = Bcons v x"
+ (fn _ => [(Simp_tac 1)]);
 
-qed_goal "bin_add_Bcons_Minus" Bin.thy "bin_add (Bcons v x) Minus = bin_pred (Bcons v x)"
-	(fn prems => [(Simp_tac 1)]);
+qed_goal "bin_add_Bcons_Minus" Bin.thy
+    "bin_add (Bcons v x) Minus = bin_pred (Bcons v x)"
+ (fn _ => [(Simp_tac 1)]);
 
-qed_goal "bin_add_Bcons_Bcons" Bin.thy "bin_add (Bcons v x) (Bcons w y) = norm_Bcons(bin_add v (if x & y then (bin_succ w) else w)) (x~= y)"
-	(fn prems => [(Simp_tac 1)]);
+qed_goal "bin_add_Bcons_Bcons" Bin.thy
+    "bin_add (Bcons v x) (Bcons w y) = \
+\    norm_Bcons(bin_add v (if x & y then (bin_succ w) else w)) (x~= y)"
+ (fn _ => [(Simp_tac 1)]);
 
 
 (*** bin_add: binary multiplication ***)
 
-qed_goal "bin_mult_Bcons1" Bin.thy "bin_mult (Bcons v True) w = bin_add (norm_Bcons (bin_mult v w) False) w"
-	(fn prem => [(Simp_tac 1)]);
+qed_goal "bin_mult_Bcons1" Bin.thy
+    "bin_mult (Bcons v True) w = bin_add (norm_Bcons (bin_mult v w) False) w"
+ (fn _ => [(Simp_tac 1)]);
 
-qed_goal "bin_mult_Bcons0" Bin.thy "bin_mult (Bcons v False) w = norm_Bcons (bin_mult v w) False"
-	(fn prem => [(Simp_tac 1)]);
+qed_goal "bin_mult_Bcons0" Bin.thy
+    "bin_mult (Bcons v False) w = norm_Bcons (bin_mult v w) False"
+ (fn _ => [(Simp_tac 1)]);
 
 
 (**** The carry/borrow functions, bin_succ and bin_pred ****)
 
-(** Lemmas **)
-
-qed_goal "zadd_assoc_cong" Integ.thy "(z::int) + v = z' + v' ==> z + (v + w) = z' + (v' + w)"
-  (fn prems => [(asm_simp_tac (!simpset addsimps (prems @ [zadd_assoc RS sym])) 1)]);
-
-qed_goal "zadd_assoc_swap" Integ.thy "(z::int) + (v + w) = v + (z + w)"
-   (fn prems => [(REPEAT (ares_tac [zadd_commute RS zadd_assoc_cong] 1))]);
-
-
-val my_ss = !simpset setloop (split_tac [expand_if]) ;
+val if_ss = !simpset setloop (split_tac [expand_if]) ;
 
 
 (**** integ_of_bin ****)
 
 
-qed_goal "integ_of_bin_norm_Bcons" Bin.thy "integ_of_bin(norm_Bcons w b) = integ_of_bin(Bcons w b)"
-   (fn prems=>[	(bin.induct_tac "w" 1),
-		(REPEAT(simp_tac (!simpset setloop (split_tac [expand_if])) 1)) ]);
+qed_goal "integ_of_bin_norm_Bcons" Bin.thy
+    "integ_of_bin(norm_Bcons w b) = integ_of_bin(Bcons w b)"
+ (fn _ =>[(bin.induct_tac "w" 1),
+          (ALLGOALS(simp_tac if_ss)) ]);
 
-qed_goal "integ_of_bin_succ" Bin.thy "integ_of_bin(bin_succ w) = $#1 + integ_of_bin w"
-   (fn prems=>[	(rtac bin.induct 1),
-		(REPEAT(asm_simp_tac (!simpset addsimps (integ_of_bin_norm_Bcons::zadd_ac)
-					       setloop (split_tac [expand_if])) 1)) ]);
+qed_goal "integ_of_bin_succ" Bin.thy
+    "integ_of_bin(bin_succ w) = $#1 + integ_of_bin w"
+ (fn _ =>[(rtac bin.induct 1),
+          (ALLGOALS(asm_simp_tac 
+                    (if_ss addsimps (integ_of_bin_norm_Bcons::zadd_ac)))) ]);
 
-qed_goal "integ_of_bin_pred" Bin.thy "integ_of_bin(bin_pred w) = $~ ($#1) + integ_of_bin w"
-   (fn prems=>[	(rtac bin.induct 1),
-		(REPEAT(asm_simp_tac (!simpset addsimps (integ_of_bin_norm_Bcons::zadd_ac)
-					       setloop (split_tac [expand_if])) 1)) ]);
+qed_goal "integ_of_bin_pred" Bin.thy
+    "integ_of_bin(bin_pred w) = $~ ($#1) + integ_of_bin w"
+ (fn _ =>[(rtac bin.induct 1),
+          (ALLGOALS(asm_simp_tac
+                  (if_ss addsimps (integ_of_bin_norm_Bcons::zadd_ac)))) ]);
 
-qed_goal "integ_of_bin_minus" Bin.thy "integ_of_bin(bin_minus w) = $~ (integ_of_bin w)"
-   (fn prems=>[	(rtac bin.induct 1),
-		(Simp_tac 1),
-		(Simp_tac 1),
-		(asm_simp_tac (!simpset
-				delsimps [pred_Plus,pred_Minus,pred_Bcons]
-				addsimps [integ_of_bin_succ,integ_of_bin_pred,
-					  zadd_assoc]
-				setloop (split_tac [expand_if])) 1)]);
+qed_goal "integ_of_bin_minus" Bin.thy
+    "integ_of_bin(bin_minus w) = $~ (integ_of_bin w)"
+ (fn _ =>[(rtac bin.induct 1),
+          (Simp_tac 1),
+          (Simp_tac 1),
+          (asm_simp_tac (if_ss
+                         delsimps [pred_Plus,pred_Minus,pred_Bcons]
+                         addsimps [integ_of_bin_succ,integ_of_bin_pred,
+                                   zadd_assoc]) 1)]);
 
  
-val bin_add_simps = [add_Plus,add_Minus,bin_add_Bcons_Plus,bin_add_Bcons_Minus,bin_add_Bcons_Bcons,
-		     integ_of_bin_succ, integ_of_bin_pred,
-		     integ_of_bin_norm_Bcons];
+val bin_add_simps = [add_Plus,add_Minus,bin_add_Bcons_Plus,
+                     bin_add_Bcons_Minus,bin_add_Bcons_Bcons,
+                     integ_of_bin_succ, integ_of_bin_pred,
+                     integ_of_bin_norm_Bcons];
 val bin_simps = [iob_Plus,iob_Minus,iob_Bcons];
 
-goal Bin.thy "! w. integ_of_bin(bin_add v w) = integ_of_bin v + integ_of_bin w";
+goal Bin.thy
+    "! w. integ_of_bin(bin_add v w) = integ_of_bin v + integ_of_bin w";
 by (bin.induct_tac "v" 1);
-by (simp_tac (my_ss addsimps bin_add_simps) 1);
-by (simp_tac (my_ss addsimps bin_add_simps) 1);
+by (simp_tac (if_ss addsimps bin_add_simps) 1);
+by (simp_tac (if_ss addsimps bin_add_simps) 1);
 by (rtac allI 1);
 by (bin.induct_tac "w" 1);
-by (asm_simp_tac (my_ss addsimps (bin_add_simps)) 1);
-by (asm_simp_tac (my_ss addsimps (bin_add_simps @ zadd_ac)) 1);
+by (asm_simp_tac (if_ss addsimps (bin_add_simps)) 1);
+by (asm_simp_tac (if_ss addsimps (bin_add_simps @ zadd_ac)) 1);
 by (cut_inst_tac [("P","bool")] True_or_False 1);
 by (etac disjE 1);
-by (asm_simp_tac (my_ss addsimps (bin_add_simps @ zadd_ac)) 1);
-by (asm_simp_tac (my_ss addsimps (bin_add_simps @ zadd_ac)) 1);
+by (asm_simp_tac (if_ss addsimps (bin_add_simps @ zadd_ac)) 1);
+by (asm_simp_tac (if_ss addsimps (bin_add_simps @ zadd_ac)) 1);
 val integ_of_bin_add_lemma = result();
 
 goal Bin.thy "integ_of_bin(bin_add v w) = integ_of_bin v + integ_of_bin w";
@@ -144,35 +160,129 @@
 by (Fast_tac 1);
 qed "integ_of_bin_add";
 
-val bin_mult_simps = [integ_of_bin_minus, integ_of_bin_add,integ_of_bin_norm_Bcons];
+val bin_mult_simps = [integ_of_bin_minus, integ_of_bin_add,
+                      integ_of_bin_norm_Bcons];
 
 goal Bin.thy "integ_of_bin(bin_mult v w) = integ_of_bin v * integ_of_bin w";
 by (bin.induct_tac "v" 1);
-by (simp_tac (my_ss addsimps bin_mult_simps) 1);
-by (simp_tac (my_ss addsimps bin_mult_simps) 1);
+by (simp_tac (if_ss addsimps bin_mult_simps) 1);
+by (simp_tac (if_ss addsimps bin_mult_simps) 1);
 by (cut_inst_tac [("P","bool")] True_or_False 1);
 by (etac disjE 1);
-by (asm_simp_tac (my_ss addsimps (bin_mult_simps @ [zadd_zmult_distrib])) 2);
-by (asm_simp_tac (my_ss addsimps (bin_mult_simps @ [zadd_zmult_distrib] @ zadd_ac)) 1);
+by (asm_simp_tac (if_ss addsimps (bin_mult_simps @ [zadd_zmult_distrib])) 2);
+by (asm_simp_tac (if_ss addsimps (bin_mult_simps @ [zadd_zmult_distrib] @ 
+                                  zadd_ac)) 1);
 qed "integ_of_bin_mult";
 
 
 Delsimps [succ_Bcons,pred_Bcons,min_Bcons,add_Bcons,mult_Bcons,
-	  iob_Plus,iob_Minus,iob_Bcons,
-	  norm_Plus,norm_Minus,norm_Bcons];
+          iob_Plus,iob_Minus,iob_Bcons,
+          norm_Plus,norm_Minus,norm_Bcons];
 
 Addsimps [integ_of_bin_add RS sym,
-	  integ_of_bin_minus RS sym,
-	  integ_of_bin_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,
-	  norm_Bcons_Bcons];
+          integ_of_bin_minus RS sym,
+          integ_of_bin_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,
+          norm_Bcons_Bcons];
+
+
+(** Simplification rules for comparison of binary numbers (Norbert Völker) **) 
+
+Addsimps [zadd_assoc];
+
+goal Bin.thy  
+    "(integ_of_bin x = integ_of_bin y) \ 
+\   = (integ_of_bin (bin_add x (bin_minus y)) = $# 0)"; 
+  by (simp_tac (HOL_ss addsimps
+                [integ_of_bin_add, integ_of_bin_minus,zdiff_def]) 1); 
+  by (rtac iffI 1); 
+  by (etac ssubst 1);
+  by (rtac zadd_zminus_inverse 1); 
+  by (dres_inst_tac [("f","(% z. z + integ_of_bin y)")] arg_cong 1); 
+  by (asm_full_simp_tac 
+      (HOL_ss addsimps[zadd_assoc,zadd_0,zadd_0_right, 
+                       zadd_zminus_inverse2]) 1); 
+val iob_eq_eq_diff_0 = result(); 
+
+goal Bin.thy "(integ_of_bin Plus = $# 0) = True"; 
+  by (stac iob_Plus 1); by (Simp_tac 1); 
+val iob_Plus_eq_0 = result(); 
+
+goal Bin.thy "(integ_of_bin Minus = $# 0) = False"; 
+  by (stac iob_Minus 1); 
+  by (Simp_tac 1);
+val iob_Minus_not_eq_0 = result(); 
+
+goal Bin.thy 
+    "(integ_of_bin (Bcons w x) = $# 0) = (~x & integ_of_bin w = $# 0)"; 
+  by (stac iob_Bcons 1);
+  by (case_tac "x" 1); 
+  by (ALLGOALS Asm_simp_tac); 
+  by (ALLGOALS(asm_simp_tac (HOL_ss addsimps [integ_of_bin_add]))); 
+  by (ALLGOALS(int_case_tac "integ_of_bin w")); 
+  by (ALLGOALS(asm_simp_tac 
+               (!simpset addsimps[zminus_zadd_distrib RS sym, 
+                                znat_add RS sym]))); 
+  by (stac eq_False_conv 1); 
+  by (rtac notI 1); 
+  by (dres_inst_tac [("f","(% z. z +  $# Suc (Suc (n + n)))")] arg_cong 1); 
+  by (Asm_full_simp_tac 1); 
+val iob_Bcons_eq_0 = result(); 
+
+goalw Bin.thy [zless_def,zdiff_def] 
+    "integ_of_bin x < integ_of_bin y \
+\    = (integ_of_bin (bin_add x (bin_minus y)) < $# 0)";
+  by (Simp_tac 1); 
+val iob_less_eq_diff_lt_0 = result(); 
+
+goal Bin.thy "(integ_of_bin Plus < $# 0) = False"; 
+  by (stac iob_Plus 1); by (Simp_tac 1); 
+val iob_Plus_not_lt_0 = result(); 
+
+goal Bin.thy "(integ_of_bin Minus < $# 0) = True"; 
+  by (stac iob_Minus 1); by (Simp_tac 1);
+val iob_Minus_lt_0 = result(); 
+
+goal Bin.thy 
+    "(integ_of_bin (Bcons w x) < $# 0) = (integ_of_bin w < $# 0)"; 
+  by (stac iob_Bcons 1);
+  by (case_tac "x" 1); 
+  by (ALLGOALS Asm_simp_tac); 
+  by (ALLGOALS(asm_simp_tac (HOL_ss addsimps [integ_of_bin_add]))); 
+  by (ALLGOALS(int_case_tac "integ_of_bin w")); 
+  by (ALLGOALS(asm_simp_tac 
+               (!simpset addsimps[zminus_zadd_distrib RS sym, 
+                                znat_add RS sym]))); 
+  by (stac (zadd_zminus_inverse RS sym) 1); 
+  by (rtac zadd_zless_mono1 1); 
+  by (Simp_tac 1); 
+val iob_Bcons_lt_0 = result(); 
+
+goal Bin.thy
+  "integ_of_bin x <= integ_of_bin y \
+\  = ( integ_of_bin (bin_add x (bin_minus y)) < $# 0 \
+\    | integ_of_bin (bin_add x (bin_minus y)) = $# 0)";
+by (simp_tac (HOL_ss addsimps 
+              [zle_eq_zless_or_eq,iob_less_eq_diff_lt_0,zdiff_def
+               ,iob_eq_eq_diff_0,integ_of_bin_minus,integ_of_bin_add]) 1);
+val iob_le_diff_lt_0_or_eq_0 = result(); 
+
+Delsimps [zless_eq_less, zle_eq_le, zadd_assoc, znegative_zminus_znat, 
+          not_znegative_znat, zero_zless_Suc_pos, negative_zless_0, 
+          negative_zle_0, not_zle_0_negative, not_znat_zless_negative, 
+          zminus_zless_zminus, zminus_zle_zminus, negative_eq_positive]; 
+
+Addsimps [zdiff_def, iob_eq_eq_diff_0, iob_less_eq_diff_lt_0, 
+          iob_le_diff_lt_0_or_eq_0, iob_Plus_eq_0, iob_Minus_not_eq_0, 
+          iob_Bcons_eq_0, iob_Plus_not_lt_0, iob_Minus_lt_0, iob_Bcons_lt_0];
+
 
 (*** Examples of performing binary arithmetic by simplification ***)
 
@@ -215,3 +325,27 @@
 goal Bin.thy "#1359  *  #~2468 = #~3354012";
 by (Simp_tac 1);
 result();
+
+goal Bin.thy "#89 * #10 ~= #889";  
+by (Simp_tac 1); 
+result();
+
+goal Bin.thy "#13 < #18 - #4";  
+by (Simp_tac 1); 
+result();
+
+goal Bin.thy "#~345 < #~242 + #~100";  
+by (Simp_tac 1); 
+result();
+
+goal Bin.thy "#13557456 < #18678654";  
+by (Simp_tac 1); 
+result();
+
+goal Bin.thy "#999999 <= (#1000001 + #1)-#2";  
+by (Simp_tac 1); 
+result();
+
+goal Bin.thy "#1234567 <= #1234567";  
+by (Simp_tac 1); 
+result();
diff -r 4b43a8d046e5 -r 4fc4b465be5b src/HOL/Integ/Integ.ML
--- a/src/HOL/Integ/Integ.ML	Tue Nov 26 14:28:17 1996 +0100
+++ b/src/HOL/Integ/Integ.ML	Tue Nov 26 15:59:28 1996 +0100
@@ -318,6 +318,16 @@
 qed "zadd_0_right";
 
 
+(** Lemmas **)
+
+qed_goal "zadd_assoc_cong" Integ.thy
+    "!!z. (z::int) + v = z' + v' ==> z + (v + w) = z' + (v' + w)"
+ (fn _ => [(asm_simp_tac (!simpset addsimps [zadd_assoc RS sym]) 1)]);
+
+qed_goal "zadd_assoc_swap" Integ.thy "(z::int) + (v + w) = v + (z + w)"
+ (fn _ => [(REPEAT (ares_tac [zadd_commute RS zadd_assoc_cong] 1))]);
+
+
 (*Need properties of subtraction?  Or use $- just as an abbreviation!*)
 
 (**** zmult: multiplication on Integ ****)
@@ -745,3 +755,139 @@
 by (dres_inst_tac [("z", "w")] zadd_zle_mono1 1);
 by (asm_full_simp_tac (!simpset addsimps [zadd_commute]) 1);
 qed "zadd_zle_self";
+
+
+(**** Comparisons: lemmas and proofs by Norbert Völker ****)
+
+(** One auxiliary theorem...**)
+
+goal HOL.thy "(x = False) = (~ x)";
+  by (fast_tac HOL_cs 1);
+qed "eq_False_conv";
+
+(** Additional theorems for Integ.thy **) 
+
+Addsimps [zless_eq_less, zle_eq_le,
+	  znegative_zminus_znat, not_znegative_znat]; 
+
+goal Integ.thy "!! x. (x::int) = y ==> x <= y"; 
+  by (etac subst 1); by (rtac zle_refl 1); 
+val zequalD1 = result(); 
+
+goal Integ.thy "($~ x < $~ y) = (y < x)";
+  by (rewrite_goals_tac [zless_def,zdiff_def]); 
+  by (simp_tac (!simpset addsimps zadd_ac ) 1); 
+val zminus_zless_zminus = result(); 
+
+goal Integ.thy "($~ x <= $~ y) = (y <= x)";
+  by (simp_tac (HOL_ss addsimps[zle_def, zminus_zless_zminus]) 1); 
+val zminus_zle_zminus = result(); 
+
+goal Integ.thy "(x < $~ y) = (y < $~ x)";
+  by (rewrite_goals_tac [zless_def,zdiff_def]); 
+  by (simp_tac (!simpset addsimps zadd_ac ) 1); 
+val zless_zminus = result(); 
+
+goal Integ.thy "($~ x < y) = ($~ y < x)";
+  by (rewrite_goals_tac [zless_def,zdiff_def]); 
+  by (simp_tac (!simpset addsimps zadd_ac ) 1); 
+val zminus_zless = result(); 
+
+goal Integ.thy "(x <= $~ y) = (y <=  $~ x)";
+  by (simp_tac (HOL_ss addsimps[zle_def, zminus_zless]) 1); 
+val zle_zminus = result(); 
+
+goal Integ.thy "($~ x <= y) = ($~ y <=  x)";
+  by (simp_tac (HOL_ss addsimps[zle_def, zless_zminus]) 1); 
+val zminus_zle = result(); 
+
+goal Integ.thy " $#0 < $# Suc n"; 
+  by (rtac (zero_less_Suc RS (zless_eq_less RS iffD2)) 1); 
+val zero_zless_Suc_pos = result(); 
+
+goal Integ.thy "($# n= $# m) = (n = m)"; 
+  by (fast_tac (HOL_cs addSEs[inj_znat RS injD]) 1); 
+val znat_znat_eq = result(); 
+AddIffs[znat_znat_eq]; 
+
+goal Integ.thy "$~ $# Suc n < $#0";
+  by (stac (zminus_0 RS sym) 1); 
+  by (rtac (zminus_zless_zminus RS iffD2) 1); 
+  by (rtac (zero_less_Suc RS (zless_eq_less RS iffD2)) 1); 
+val negative_zless_0 = result(); 
+Addsimps [zero_zless_Suc_pos, negative_zless_0]; 
+
+goal Integ.thy "$~ $#  n <= $#0";
+  by (rtac zless_or_eq_imp_zle 1); 
+  by (nat_ind_tac "n" 1); 
+  by (ALLGOALS Asm_simp_tac); 
+val negative_zle_0 = result(); 
+Addsimps[negative_zle_0]; 
+
+goal Integ.thy "~($#0 <= $~ $# Suc n)";
+  by (stac zle_zminus 1);
+  by (Simp_tac 1);
+val not_zle_0_negative = result(); 
+Addsimps[not_zle_0_negative]; 
+
+goal Integ.thy "($# n <= $~ $# m) = (n = 0 & m = 0)"; 
+  by (safe_tac HOL_cs); 
+  by (Simp_tac 3); 
+  by (dtac (zle_zminus RS iffD1) 2); 
+  by (ALLGOALS(dtac (negative_zle_0 RSN(2,zle_trans)))); 
+  by (ALLGOALS Asm_full_simp_tac); 
+val znat_zle_znegative = result(); 
+
+goal Integ.thy "~($# n < $~ $# Suc m)";
+  by (rtac notI 1); by (forward_tac [zless_imp_zle] 1); 
+  by (dtac (znat_zle_znegative RS iffD1) 1); 
+  by (safe_tac HOL_cs); 
+  by (dtac (zless_zminus RS iffD1) 1); 
+  by (Asm_full_simp_tac 1);
+val not_znat_zless_negative = result(); 
+
+goal Integ.thy "($~ $# n = $# m) = (n = 0 & m = 0)"; 
+  by (rtac iffI 1);
+  by (rtac  (znat_zle_znegative RS iffD1) 1); 
+  by (dtac sym 1); 
+  by (ALLGOALS Asm_simp_tac); 
+val negative_eq_positive = result(); 
+
+Addsimps [zminus_zless_zminus, zminus_zle_zminus, 
+	  negative_eq_positive, not_znat_zless_negative]; 
+
+goalw Integ.thy [zdiff_def,zless_def] "!! x. znegative x = (x < $# 0)";
+  by (Auto_tac()); 
+val znegative_less_0 = result(); 
+
+goalw Integ.thy [zdiff_def,zless_def] "!! x. (~znegative x) = ($# 0 <= x)";
+  by (stac znegative_less_0 1); 
+  by (safe_tac (HOL_cs addSDs[zleD,not_zleE,zleI]) ); 
+val not_znegative_ge_0 = result(); 
+
+goal Integ.thy "!! x. znegative x ==> ? n. x = $~ $# Suc n"; 
+  by (dtac (znegative_less_0 RS iffD1 RS zless_eq_zadd_Suc) 1); 
+  by (etac exE 1); 
+  by (rtac exI 1);
+  by (dres_inst_tac [("f","(% z. z + $~ $# Suc n )")] arg_cong 1); 
+  by (auto_tac(!claset, !simpset addsimps [zadd_assoc])); 
+val znegativeD = result(); 
+
+goal Integ.thy "!! x. ~znegative x ==> ? n. x = $# n"; 
+  by (dtac (not_znegative_ge_0 RS iffD1) 1); 
+  by (dtac zle_imp_zless_or_eq 1); 
+  by (etac disjE 1); 
+  by (dtac zless_eq_zadd_Suc 1); 
+  by (Auto_tac()); 
+val not_znegativeD = result(); 
+
+(* a case theorem distinguishing positive and negative int *)  
+
+val prems = goal Integ.thy 
+    "[|!! n. P ($# n); !! n. P ($~ $# Suc n) |] ==> P z"; 
+  by (cut_inst_tac [("P","znegative z")] excluded_middle 1); 
+  by (fast_tac (HOL_cs addSDs[znegativeD,not_znegativeD] addSIs prems) 1); 
+val int_cases = result(); 
+
+fun int_case_tac x = res_inst_tac [("z",x)] int_cases; 
+
diff -r 4b43a8d046e5 -r 4fc4b465be5b src/HOL/Integ/Integ.thy
--- a/src/HOL/Integ/Integ.thy	Tue Nov 26 14:28:17 1996 +0100
+++ b/src/HOL/Integ/Integ.thy	Tue Nov 26 15:59:28 1996 +0100
@@ -1,6 +1,6 @@
 (*  Title:      Integ.thy
     ID:         $Id$
-    Authors:    Lawrence C Paulson, Cambridge University Computer Laboratory
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1996  University of Cambridge
 
 The integers as equivalence classes over nat*nat.
@@ -35,18 +35,6 @@
   "zmagnitude(Z) == Abs_Integ(UN p:Rep_Integ(Z).
                               split (%x y. intrel^^{((y-x) + (x-y),0)}) p)"
 
-  zdiv        :: [int,int]=>int                              (infixl 70)
-  "Z1 zdiv Z2 ==   
-      Abs_Integ(UN p1:Rep_Integ(Z1). UN p2:Rep_Integ(Z2). split (%x1 y1.   
-          split (%x2 y2. intrel^^{((x1-y1)div(x2-y2)+(y1-x1)div(y2-x2),   
-          (x1-y1)div(y2-x2)+(y1-x1)div(x2-y2))}) p2) p1)"
-
-  zmod        :: [int,int]=>int                              (infixl 70)
-  "Z1 zmod Z2 ==   
-      Abs_Integ(UN p1:Rep_Integ(Z1).UN p2:Rep_Integ(Z2).split (%x1 y1.   
-          split (%x2 y2. intrel^^{((x1-y1)mod((x2-y2)+(y2-x2)),   
-          (x1-y1)mod((x2-y2)+(x2-y2)))}) p2) p1)"
-
   zpred       :: int=>int
   "zpred(Z) == Z - $# Suc(0)"