# HG changeset patch
# User paulson
# Date 965982842 -7200
# Node ID 3df14e0a3a5189264d5f4d706221d4ea2a358262
# Parent  af71f5f4ca6b433dcd05bd0547087a07dfc38cdd
interim working version: more improvements to the integers

diff -r af71f5f4ca6b -r 3df14e0a3a51 src/ZF/Integ/Bin.ML
--- a/src/ZF/Integ/Bin.ML	Thu Aug 10 14:55:21 2000 +0200
+++ b/src/ZF/Integ/Bin.ML	Fri Aug 11 10:34:02 2000 +0200
@@ -260,6 +260,16 @@
 by (Simp_tac 1);
 qed "int_of_0";
 
+Goal "$# succ(n) = #1 $+ $#n";
+by (simp_tac (simpset() addsimps [int_of_add RS sym, natify_succ]) 1);
+qed "int_of_succ";
+
+Goal "$- #0 = #0";
+by (Simp_tac 1);
+qed "zminus_0";
+
+Addsimps [zminus_0];
+
 Goal "#0 $+ z = intify(z)";
 by (Simp_tac 1);
 qed "zadd_0_intify";
@@ -303,6 +313,11 @@
 
 Addsimps [zmult_minus1, zmult_minus1_right];
 
+(*beware!  LOOPS with int_combine_numerals simproc*)
+Goal "#2 $* z = z $+ z";
+by (simp_tac (simpset() addsimps [zadd_zmult_distrib]) 1);
+qed "zmult_2";
+
 
 (*** Simplification rules for comparison of binary numbers (N Voelker) ***)
 
@@ -470,3 +485,31 @@
 
 Addsimps [add_integ_of_left, mult_integ_of_left,
 	  add_integ_of_diff1, add_integ_of_diff2]; 
+
+
+(** More for integer constants **)
+
+Addsimps [int_of_0, int_of_succ];
+
+Goal "#0 $- x = $-x";
+by (simp_tac (simpset() addsimps [zdiff_def]) 1);
+qed "zdiff0";
+
+Goal "x $- #0 = intify(x)";
+by (simp_tac (simpset() addsimps [zdiff_def]) 1);
+qed "zdiff0_right";
+
+Goal "x $- x = #0";
+by (simp_tac (simpset() addsimps [zdiff_def]) 1);
+qed "zdiff_self";
+
+Addsimps [zdiff0, zdiff0_right, zdiff_self];
+
+Goal "[| znegative(k); k: int |] ==> k $< #0";
+by (asm_simp_tac (simpset() addsimps [zless_def]) 1);
+qed "znegative_imp_zless_0";
+
+Goal "[| #0 $< k; k: int |] ==> znegative($-k)";
+by (asm_full_simp_tac (simpset() addsimps [zless_def]) 1);
+qed "zero_zless_imp_znegative_zminus";
+
diff -r af71f5f4ca6b -r 3df14e0a3a51 src/ZF/Integ/Int.ML
--- a/src/ZF/Integ/Int.ML	Thu Aug 10 14:55:21 2000 +0200
+++ b/src/ZF/Integ/Int.ML	Fri Aug 11 10:34:02 2000 +0200
@@ -8,7 +8,6 @@
 Could also prove...
 "znegative(z) ==> $# zmagnitude(z) = $- z"
 "~ znegative(z) ==> $# zmagnitude(z) = z"
-$+ and $* are monotonic wrt $<
 *)
 
 AddSEs [quotientE];
@@ -241,9 +240,9 @@
 
 Goalw [int_of_def] "$- ($#0) = $#0";
 by (simp_tac (simpset() addsimps [zminus]) 1);
-qed "zminus_0";
+qed "zminus_int0";
 
-Addsimps [zminus_zminus_intify, zminus_0];
+Addsimps [zminus_zminus_intify, zminus_int0];
 
 Goal "z : int ==> $- ($- z) = z";
 by (Asm_simp_tac 1);
@@ -327,12 +326,12 @@
 Addsimps [not_zneg_mag];
 
 Goalw [int_def, znegative_def, int_of_def]
-     "[| z: int; znegative(z) |] ==> EX n:nat. z = $- ($# succ(n))"; 
+     "[| znegative(z); z: int |] ==> EX n:nat. z = $- ($# succ(n))"; 
 by (auto_tac(claset() addSDs [less_imp_succ_add], 
 	     simpset() addsimps [zminus, image_singleton_iff]));
 qed "zneg_int_of";
 
-Goal "[| z: int; znegative(z) |] ==> $# (zmagnitude(z)) = $- z"; 
+Goal "[| znegative(z); z: int |] ==> $# (zmagnitude(z)) = $- z"; 
 by (dtac zneg_int_of 1);
 by Auto_tac;
 qed "zneg_mag"; 
@@ -618,7 +617,7 @@
 Goal "w $* (z1 $+ z2) = (w $* z1) $+ (w $* z2)";
 by (simp_tac (simpset() addsimps [inst "z" "w" zmult_commute,
                                   zadd_zmult_distrib]) 1);
-qed "zadd_zmult_distrib_left";
+qed "zadd_zmult_distrib2";
 
 val int_typechecks =
     [int_of_type, zminus_type, zmagnitude_type, zadd_type, zmult_type];
@@ -631,20 +630,6 @@
 qed "zdiff_type";
 AddIffs [zdiff_type];  AddTCs [zdiff_type];
 
-Goal "$#0 $- x = $-x";
-by (simp_tac (simpset() addsimps [zdiff_def]) 1);
-qed "zdiff_int0";
-
-Goal "x $- $#0 = intify(x)";
-by (simp_tac (simpset() addsimps [zdiff_def]) 1);
-qed "zdiff_int0_right";
-
-Goal "x $- x = $#0";
-by (simp_tac (simpset() addsimps [zdiff_def]) 1);
-qed "zdiff_self";
-
-Addsimps [zdiff_int0, zdiff_int0_right, zdiff_self];
-
 Goal "$- (z $- y) = y $- z";
 by (simp_tac (simpset() addsimps [zdiff_def, zadd_commute])1);
 qed "zminus_zdiff_eq";
@@ -695,12 +680,26 @@
 
 Goal "~ (z$<z)";
 by (auto_tac (claset(), 
-              simpset() addsimps  [zless_def, znegative_def, int_of_def]));  
+              simpset() addsimps  [zless_def, znegative_def, int_of_def,
+                                   zdiff_def]));  
 by (rotate_tac 2 1);
 by Auto_tac;  
 qed "zless_not_refl";
 AddIffs [zless_not_refl];
 
+Goal "[| x: int; y: int |] ==> (x ~= y) <-> (x $< y | y $< x)";
+by (cut_inst_tac [("z","x"),("w","y")] zless_linear 1);
+by Auto_tac;  
+qed "neq_iff_zless";
+
+Goal "w $< z ==> intify(w) ~= intify(z)";
+by Auto_tac;  
+by (subgoal_tac "~ (intify(w) $< intify(z))" 1);
+by (etac ssubst 2);
+by (Full_simp_tac 1);
+by Auto_tac;  
+qed "zless_imp_intify_neq";
+
 (*This lemma allows direct proofs of other <-properties*)
 Goalw [zless_def, znegative_def, zdiff_def, int_def] 
     "[| w $< z; w: int; z: int |] ==> (EX n. z = w $+ $#(succ(n)))";
@@ -709,11 +708,11 @@
 by (res_inst_tac [("x","k")] exI 1);
 by (etac add_left_cancel 1);
 by Auto_tac;  
-qed "zless_imp_succ_zadd_lemma";
+val lemma = result();
 
 Goal "w $< z ==> (EX n. w $+ $#(succ(n)) = intify(z))";
 by (subgoal_tac "intify(w) $< intify(z)" 1);
-by (dres_inst_tac [("w","intify(w)")] zless_imp_succ_zadd_lemma 1);
+by (dres_inst_tac [("w","intify(w)")] lemma 1);
 by Auto_tac;  
 qed "zless_imp_succ_zadd";
 
@@ -723,10 +722,10 @@
               simpset() addsimps [zadd, zminus, int_of_def, image_iff]));  
 by (res_inst_tac [("x","0")] exI 1);
 by Auto_tac;  
-qed "zless_succ_zadd_lemma";
+val lemma = result();
 
 Goal "w $< w $+ $# succ(n)";
-by (cut_facts_tac [intify_in_int RS zless_succ_zadd_lemma] 1);
+by (cut_facts_tac [intify_in_int RS lemma] 1);
 by Auto_tac;  
 qed "zless_succ_zadd";
 
@@ -757,6 +756,14 @@
 by Auto_tac;  
 qed "zless_trans";
 
+Goal "z $< w ==> ~ (w $< z)";
+by (blast_tac (claset() addDs [zless_trans]) 1);
+qed "zless_not_sym";
+
+(* [| z $< w; ~ P ==> w $< z |] ==> P *)
+bind_thm ("zless_asym", zless_not_sym RS swap);
+
+
 (*** "Less Than or Equals", $<= ***)
 
 Goalw [zle_def] "z $<= z";
@@ -795,10 +802,7 @@
 Goal "~ (z $< w) <-> (w $<= z)";
 by (cut_inst_tac [("z","z"),("w","w")] zless_linear 1);
 by (auto_tac (claset() addDs [zless_trans], simpset() addsimps [zle_def]));  
-by (auto_tac (claset(), 
-            simpset() addsimps [zless_def, zdiff_def, zadd_def, zminus_def]));
-by (fold_tac [zless_def, zdiff_def, zadd_def, zminus_def]);
-by Auto_tac;  
+by (auto_tac (claset() addSDs [zless_imp_intify_neq],  simpset()));
 qed "not_zless_iff_zle";
 
 Goal "~ (z $<= w) <-> (w $< z)";
@@ -806,7 +810,6 @@
 qed "not_zle_iff_zless";
 
 
-
 (*** More subtraction laws (for zcompare_rls) ***)
 
 Goal "(x $- y) $- z = x $- (y $+ z)";
@@ -919,6 +922,19 @@
 Addsimps [zadd_right_cancel_zle, zadd_left_cancel_zle];
 
 
+(*** Comparison laws ***)
+
+Goal "($- x $< $- y) <-> (y $< x)";
+by (simp_tac (simpset() addsimps [zless_def, zdiff_def] @ zadd_ac) 1);
+qed "zminus_zless_zminus"; 
+Addsimps [zminus_zless_zminus];
+
+Goal "($- x $<= $- y) <-> (y $<= x)";
+by (simp_tac (simpset() addsimps [not_zless_iff_zle RS iff_sym]) 1);
+qed "zminus_zle_zminus"; 
+Addsimps [zminus_zle_zminus];
+
+
 (*** More inequality lemmas ***)
 
 Goal "[| x: int;  y: int |] ==> (x = $- y) <-> (y = $- x)";
@@ -928,3 +944,34 @@
 Goal "[| x: int;  y: int |] ==> ($- x = y) <-> ($- y = x)";
 by Auto_tac;
 qed "zminus_equation";
+
+Goal "(intify(x) = $- y) <-> (intify(y) = $- x)";
+by (cut_inst_tac [("x","intify(x)"), ("y","intify(y)")] equation_zminus 1);
+by Auto_tac;
+qed "equation_zminus_intify";
+
+Goal "($- x = intify(y)) <-> ($- y = intify(x))";
+by (cut_inst_tac [("x","intify(x)"), ("y","intify(y)")] zminus_equation 1);
+by Auto_tac;
+qed "zminus_equation_intify";
+
+
+(** The next several equations are permutative: watch out! **)
+
+Goal "(x $< $- y) <-> (y $< $- x)";
+by (simp_tac (simpset() addsimps [zless_def, zdiff_def] @ zadd_ac) 1);
+qed "zless_zminus"; 
+
+Goal "($- x $< y) <-> ($- y $< x)";
+by (simp_tac (simpset() addsimps [zless_def, zdiff_def] @ zadd_ac) 1);
+qed "zminus_zless"; 
+
+Goal "(x $<= $- y) <-> (y $<= $- x)";
+by (simp_tac (simpset() addsimps [not_zless_iff_zle RS iff_sym, 
+                                  zminus_zless]) 1);
+qed "zle_zminus"; 
+
+Goal "($- x $<= y) <-> ($- y $<= x)";
+by (simp_tac (simpset() addsimps [not_zless_iff_zle RS iff_sym, 
+                                  zless_zminus]) 1);
+qed "zminus_zle"; 
diff -r af71f5f4ca6b -r 3df14e0a3a51 src/ZF/Integ/int_arith.ML
--- a/src/ZF/Integ/int_arith.ML	Thu Aug 10 14:55:21 2000 +0200
+++ b/src/ZF/Integ/int_arith.ML	Fri Aug 11 10:34:02 2000 +0200
@@ -315,7 +315,7 @@
   
 val combine_numerals_prod = 
     prep_simproc ("int_combine_numerals_prod",
-		  prep_pats ["i $* j", "i $* j"],
+		  prep_pats ["i $* j"],
 		  CombineNumeralsProd.proc);
 
 end;