# HG changeset patch
# User paulson
# Date 993567849 -7200
# Node ID 4ab3b7b0938fe71bfa602adfe5ebd5548549f332
# Parent  e76366922751ffaa6fad8d6b96fb65c9f9d6f189
tidying and consolidating files

diff -r e76366922751 -r 4ab3b7b0938f src/ZF/Integ/Bin.ML
--- a/src/ZF/Integ/Bin.ML	Tue Jun 26 16:54:39 2001 +0200
+++ b/src/ZF/Integ/Bin.ML	Tue Jun 26 17:04:09 2001 +0200
@@ -396,10 +396,6 @@
 by (asm_simp_tac (simpset() addsimps [equation_zminus, int_of_diff RS sym])1);
 qed "neg_integ_of_BIT"; 
 
-Goal "w: bin ==> iszero (integ_of (w BIT 0)) <-> iszero (integ_of(w))"; 
-by (asm_simp_tac (ZF_ss addsimps [iszero_integ_of_BIT]) 1); 
-qed "iszero_integ_of_0"; 
-
 (** Less-than-or-equals (<=) **)
 
 Goal "(integ_of(x) $<= (integ_of(w))) <-> ~ (integ_of(w) $< (integ_of(x)))";
diff -r e76366922751 -r 4ab3b7b0938f src/ZF/Integ/Bin.thy
--- a/src/ZF/Integ/Bin.thy	Tue Jun 26 16:54:39 2001 +0200
+++ b/src/ZF/Integ/Bin.thy	Tue Jun 26 17:04:09 2001 +0200
@@ -14,8 +14,6 @@
 
 The representation expects that (m mod 2) is 0 or 1, even if m is negative;
 For instance, ~5 div 2 = ~3 and ~5 mod 2 = 1; thus ~5 = (~3)*2 + 1
-
-Division is not defined yet!
 *)
 
 Bin = Int + Datatype +
diff -r e76366922751 -r 4ab3b7b0938f src/ZF/Integ/Int.ML
--- a/src/ZF/Integ/Int.ML	Tue Jun 26 16:54:39 2001 +0200
+++ b/src/ZF/Integ/Int.ML	Tue Jun 26 17:04:09 2001 +0200
@@ -986,6 +986,29 @@
 Addsimps [zadd_right_cancel_zle, zadd_left_cancel_zle];
 
 
+(*"v $<= w ==> v$+z $<= w$+z"*)
+bind_thm ("zadd_zless_mono1", zadd_right_cancel_zless RS iffD2);
+
+(*"v $<= w ==> z$+v $<= z$+w"*)
+bind_thm ("zadd_zless_mono2", zadd_left_cancel_zless RS iffD2);
+
+(*"v $<= w ==> v$+z $<= w$+z"*)
+bind_thm ("zadd_zle_mono1", zadd_right_cancel_zle RS iffD2);
+
+(*"v $<= w ==> z$+v $<= z$+w"*)
+bind_thm ("zadd_zle_mono2", zadd_left_cancel_zle RS iffD2);
+
+Goal "[| w' $<= w; z' $<= z |] ==> w' $+ z' $<= w $+ z";
+by (etac (zadd_zle_mono1 RS zle_trans) 1);
+by (Simp_tac 1);
+qed "zadd_zle_mono";
+
+Goal "[| w' $< w; z' $<= z |] ==> w' $+ z' $< w $+ z";
+by (etac (zadd_zless_mono1 RS zless_zle_trans) 1);
+by (Simp_tac 1);
+qed "zadd_zless_mono";
+
+
 (*** Comparison laws ***)
 
 Goal "($- x $< $- y) <-> (y $< x)";
diff -r e76366922751 -r 4ab3b7b0938f src/ZF/Integ/IntDiv.ML
--- a/src/ZF/Integ/IntDiv.ML	Tue Jun 26 16:54:39 2001 +0200
+++ b/src/ZF/Integ/IntDiv.ML	Tue Jun 26 17:04:09 2001 +0200
@@ -90,51 +90,6 @@
 qed "add1_left_zle_iff";
 
 
-(*** Monotonicity results ***)
-
-Goal "(v$+z $< w$+z) <-> (v $< w)";
-by (Simp_tac 1);
-qed "zadd_right_cancel_zless";
-
-Goal "(z$+v $< z$+w) <-> (v $< w)";
-by (Simp_tac 1);
-qed "zadd_left_cancel_zless";
-
-Addsimps [zadd_right_cancel_zless, zadd_left_cancel_zless];
-
-Goal "(v$+z $<= w$+z) <-> (v $<= w)";
-by (Simp_tac 1);
-qed "zadd_right_cancel_zle";
-
-Goal "(z$+v $<= z$+w) <-> (v $<= w)";
-by (Simp_tac 1);
-qed "zadd_left_cancel_zle";
-
-Addsimps [zadd_right_cancel_zle, zadd_left_cancel_zle];
-
-(*"v $<= w ==> v$+z $<= w$+z"*)
-bind_thm ("zadd_zless_mono1", zadd_right_cancel_zless RS iffD2);
-
-(*"v $<= w ==> z$+v $<= z$+w"*)
-bind_thm ("zadd_zless_mono2", zadd_left_cancel_zless RS iffD2);
-
-(*"v $<= w ==> v$+z $<= w$+z"*)
-bind_thm ("zadd_zle_mono1", zadd_right_cancel_zle RS iffD2);
-
-(*"v $<= w ==> z$+v $<= z$+w"*)
-bind_thm ("zadd_zle_mono2", zadd_left_cancel_zle RS iffD2);
-
-Goal "[| w' $<= w; z' $<= z |] ==> w' $+ z' $<= w $+ z";
-by (etac (zadd_zle_mono1 RS zle_trans) 1);
-by (Simp_tac 1);
-qed "zadd_zle_mono";
-
-Goal "[| w' $< w; z' $<= z |] ==> w' $+ z' $< w $+ z";
-by (etac (zadd_zless_mono1 RS zless_zle_trans) 1);
-by (Simp_tac 1);
-qed "zadd_zless_mono";
-
-
 (*** Monotonicity of Multiplication ***)
 
 Goal "k \\<in> nat ==> i $<= j ==> i $* $#k $<= j $* $#k";
@@ -235,6 +190,9 @@
 				      zmult_zless_mono2, zless_zminus]) 1);
 qed "zmult_zless_mono2_neg";
 
+
+(** Products of zeroes **)
+
 Goal "[| m \\<in> int; n \\<in> int |] ==> (m$*n = #0) <-> (m = #0 | n = #0)";
 by (case_tac "m $< #0" 1);
 by (auto_tac (claset(), 
@@ -247,6 +205,7 @@
 Goal "(m$*n = #0) <-> (intify(m) = #0 | intify(n) = #0)";
 by (asm_full_simp_tac (simpset() addsimps [lemma RS iff_sym]) 1);
 qed "zmult_eq_0_iff";
+AddIffs [zmult_eq_0_iff];
 
 
 (** Cancellation laws for k*m < k*n and m*k < n*k, also for <= and =,
@@ -437,27 +396,6 @@
 qed "intify_eq_0_iff_zle";
 
 
-
-(*** Products of zeroes ***)
-
-Goal "[| x \\<in> int; y \\<in> int |] \
-\     ==> (x $* y = #0) <-> (intify(x) = #0 | intify(y) = #0)";
-by (case_tac "x $< #0" 1);
-by (auto_tac (claset(), 
-      simpset() addsimps [not_zless_iff_zle, zle_def, neq_iff_zless]));
-by (REPEAT
-    (force_tac (claset() addDs [zmult_zless_mono1_neg, zmult_zless_mono1], 
-		simpset()) 1));
-qed "zmult_eq_0_iff_lemma";
-
-Goal "(x $* y = #0) <-> (intify(x) = #0 | intify(y) = #0)";
-by (cut_inst_tac [("x","intify(x)"),("y","intify(y)")] 
-                 zmult_eq_0_iff_lemma 1);
-by Auto_tac; 
-qed "zmult_eq_0_iff";
-AddIffs [zmult_eq_0_iff];
-
-
 (*** Some convenient biconditionals for products of signs ***)
 
 Goal "[| #0 $< i; #0 $< j |] ==> #0 $< i $* j";