interim working version: more improvements to the integers
authorpaulson
Fri Aug 11 10:34:02 2000 +0200 (2000-08-11)
changeset 95763df14e0a3a51
parent 9575 af71f5f4ca6b
child 9577 9e66e8ed8237
interim working version: more improvements to the integers
src/ZF/Integ/Bin.ML
src/ZF/Integ/Int.ML
src/ZF/Integ/int_arith.ML
     1.1 --- a/src/ZF/Integ/Bin.ML	Thu Aug 10 14:55:21 2000 +0200
     1.2 +++ b/src/ZF/Integ/Bin.ML	Fri Aug 11 10:34:02 2000 +0200
     1.3 @@ -260,6 +260,16 @@
     1.4  by (Simp_tac 1);
     1.5  qed "int_of_0";
     1.6  
     1.7 +Goal "$# succ(n) = #1 $+ $#n";
     1.8 +by (simp_tac (simpset() addsimps [int_of_add RS sym, natify_succ]) 1);
     1.9 +qed "int_of_succ";
    1.10 +
    1.11 +Goal "$- #0 = #0";
    1.12 +by (Simp_tac 1);
    1.13 +qed "zminus_0";
    1.14 +
    1.15 +Addsimps [zminus_0];
    1.16 +
    1.17  Goal "#0 $+ z = intify(z)";
    1.18  by (Simp_tac 1);
    1.19  qed "zadd_0_intify";
    1.20 @@ -303,6 +313,11 @@
    1.21  
    1.22  Addsimps [zmult_minus1, zmult_minus1_right];
    1.23  
    1.24 +(*beware!  LOOPS with int_combine_numerals simproc*)
    1.25 +Goal "#2 $* z = z $+ z";
    1.26 +by (simp_tac (simpset() addsimps [zadd_zmult_distrib]) 1);
    1.27 +qed "zmult_2";
    1.28 +
    1.29  
    1.30  (*** Simplification rules for comparison of binary numbers (N Voelker) ***)
    1.31  
    1.32 @@ -470,3 +485,31 @@
    1.33  
    1.34  Addsimps [add_integ_of_left, mult_integ_of_left,
    1.35  	  add_integ_of_diff1, add_integ_of_diff2]; 
    1.36 +
    1.37 +
    1.38 +(** More for integer constants **)
    1.39 +
    1.40 +Addsimps [int_of_0, int_of_succ];
    1.41 +
    1.42 +Goal "#0 $- x = $-x";
    1.43 +by (simp_tac (simpset() addsimps [zdiff_def]) 1);
    1.44 +qed "zdiff0";
    1.45 +
    1.46 +Goal "x $- #0 = intify(x)";
    1.47 +by (simp_tac (simpset() addsimps [zdiff_def]) 1);
    1.48 +qed "zdiff0_right";
    1.49 +
    1.50 +Goal "x $- x = #0";
    1.51 +by (simp_tac (simpset() addsimps [zdiff_def]) 1);
    1.52 +qed "zdiff_self";
    1.53 +
    1.54 +Addsimps [zdiff0, zdiff0_right, zdiff_self];
    1.55 +
    1.56 +Goal "[| znegative(k); k: int |] ==> k $< #0";
    1.57 +by (asm_simp_tac (simpset() addsimps [zless_def]) 1);
    1.58 +qed "znegative_imp_zless_0";
    1.59 +
    1.60 +Goal "[| #0 $< k; k: int |] ==> znegative($-k)";
    1.61 +by (asm_full_simp_tac (simpset() addsimps [zless_def]) 1);
    1.62 +qed "zero_zless_imp_znegative_zminus";
    1.63 +
     2.1 --- a/src/ZF/Integ/Int.ML	Thu Aug 10 14:55:21 2000 +0200
     2.2 +++ b/src/ZF/Integ/Int.ML	Fri Aug 11 10:34:02 2000 +0200
     2.3 @@ -8,7 +8,6 @@
     2.4  Could also prove...
     2.5  "znegative(z) ==> $# zmagnitude(z) = $- z"
     2.6  "~ znegative(z) ==> $# zmagnitude(z) = z"
     2.7 -$+ and $* are monotonic wrt $<
     2.8  *)
     2.9  
    2.10  AddSEs [quotientE];
    2.11 @@ -241,9 +240,9 @@
    2.12  
    2.13  Goalw [int_of_def] "$- ($#0) = $#0";
    2.14  by (simp_tac (simpset() addsimps [zminus]) 1);
    2.15 -qed "zminus_0";
    2.16 +qed "zminus_int0";
    2.17  
    2.18 -Addsimps [zminus_zminus_intify, zminus_0];
    2.19 +Addsimps [zminus_zminus_intify, zminus_int0];
    2.20  
    2.21  Goal "z : int ==> $- ($- z) = z";
    2.22  by (Asm_simp_tac 1);
    2.23 @@ -327,12 +326,12 @@
    2.24  Addsimps [not_zneg_mag];
    2.25  
    2.26  Goalw [int_def, znegative_def, int_of_def]
    2.27 -     "[| z: int; znegative(z) |] ==> EX n:nat. z = $- ($# succ(n))"; 
    2.28 +     "[| znegative(z); z: int |] ==> EX n:nat. z = $- ($# succ(n))"; 
    2.29  by (auto_tac(claset() addSDs [less_imp_succ_add], 
    2.30  	     simpset() addsimps [zminus, image_singleton_iff]));
    2.31  qed "zneg_int_of";
    2.32  
    2.33 -Goal "[| z: int; znegative(z) |] ==> $# (zmagnitude(z)) = $- z"; 
    2.34 +Goal "[| znegative(z); z: int |] ==> $# (zmagnitude(z)) = $- z"; 
    2.35  by (dtac zneg_int_of 1);
    2.36  by Auto_tac;
    2.37  qed "zneg_mag"; 
    2.38 @@ -618,7 +617,7 @@
    2.39  Goal "w $* (z1 $+ z2) = (w $* z1) $+ (w $* z2)";
    2.40  by (simp_tac (simpset() addsimps [inst "z" "w" zmult_commute,
    2.41                                    zadd_zmult_distrib]) 1);
    2.42 -qed "zadd_zmult_distrib_left";
    2.43 +qed "zadd_zmult_distrib2";
    2.44  
    2.45  val int_typechecks =
    2.46      [int_of_type, zminus_type, zmagnitude_type, zadd_type, zmult_type];
    2.47 @@ -631,20 +630,6 @@
    2.48  qed "zdiff_type";
    2.49  AddIffs [zdiff_type];  AddTCs [zdiff_type];
    2.50  
    2.51 -Goal "$#0 $- x = $-x";
    2.52 -by (simp_tac (simpset() addsimps [zdiff_def]) 1);
    2.53 -qed "zdiff_int0";
    2.54 -
    2.55 -Goal "x $- $#0 = intify(x)";
    2.56 -by (simp_tac (simpset() addsimps [zdiff_def]) 1);
    2.57 -qed "zdiff_int0_right";
    2.58 -
    2.59 -Goal "x $- x = $#0";
    2.60 -by (simp_tac (simpset() addsimps [zdiff_def]) 1);
    2.61 -qed "zdiff_self";
    2.62 -
    2.63 -Addsimps [zdiff_int0, zdiff_int0_right, zdiff_self];
    2.64 -
    2.65  Goal "$- (z $- y) = y $- z";
    2.66  by (simp_tac (simpset() addsimps [zdiff_def, zadd_commute])1);
    2.67  qed "zminus_zdiff_eq";
    2.68 @@ -695,12 +680,26 @@
    2.69  
    2.70  Goal "~ (z$<z)";
    2.71  by (auto_tac (claset(), 
    2.72 -              simpset() addsimps  [zless_def, znegative_def, int_of_def]));  
    2.73 +              simpset() addsimps  [zless_def, znegative_def, int_of_def,
    2.74 +                                   zdiff_def]));  
    2.75  by (rotate_tac 2 1);
    2.76  by Auto_tac;  
    2.77  qed "zless_not_refl";
    2.78  AddIffs [zless_not_refl];
    2.79  
    2.80 +Goal "[| x: int; y: int |] ==> (x ~= y) <-> (x $< y | y $< x)";
    2.81 +by (cut_inst_tac [("z","x"),("w","y")] zless_linear 1);
    2.82 +by Auto_tac;  
    2.83 +qed "neq_iff_zless";
    2.84 +
    2.85 +Goal "w $< z ==> intify(w) ~= intify(z)";
    2.86 +by Auto_tac;  
    2.87 +by (subgoal_tac "~ (intify(w) $< intify(z))" 1);
    2.88 +by (etac ssubst 2);
    2.89 +by (Full_simp_tac 1);
    2.90 +by Auto_tac;  
    2.91 +qed "zless_imp_intify_neq";
    2.92 +
    2.93  (*This lemma allows direct proofs of other <-properties*)
    2.94  Goalw [zless_def, znegative_def, zdiff_def, int_def] 
    2.95      "[| w $< z; w: int; z: int |] ==> (EX n. z = w $+ $#(succ(n)))";
    2.96 @@ -709,11 +708,11 @@
    2.97  by (res_inst_tac [("x","k")] exI 1);
    2.98  by (etac add_left_cancel 1);
    2.99  by Auto_tac;  
   2.100 -qed "zless_imp_succ_zadd_lemma";
   2.101 +val lemma = result();
   2.102  
   2.103  Goal "w $< z ==> (EX n. w $+ $#(succ(n)) = intify(z))";
   2.104  by (subgoal_tac "intify(w) $< intify(z)" 1);
   2.105 -by (dres_inst_tac [("w","intify(w)")] zless_imp_succ_zadd_lemma 1);
   2.106 +by (dres_inst_tac [("w","intify(w)")] lemma 1);
   2.107  by Auto_tac;  
   2.108  qed "zless_imp_succ_zadd";
   2.109  
   2.110 @@ -723,10 +722,10 @@
   2.111                simpset() addsimps [zadd, zminus, int_of_def, image_iff]));  
   2.112  by (res_inst_tac [("x","0")] exI 1);
   2.113  by Auto_tac;  
   2.114 -qed "zless_succ_zadd_lemma";
   2.115 +val lemma = result();
   2.116  
   2.117  Goal "w $< w $+ $# succ(n)";
   2.118 -by (cut_facts_tac [intify_in_int RS zless_succ_zadd_lemma] 1);
   2.119 +by (cut_facts_tac [intify_in_int RS lemma] 1);
   2.120  by Auto_tac;  
   2.121  qed "zless_succ_zadd";
   2.122  
   2.123 @@ -757,6 +756,14 @@
   2.124  by Auto_tac;  
   2.125  qed "zless_trans";
   2.126  
   2.127 +Goal "z $< w ==> ~ (w $< z)";
   2.128 +by (blast_tac (claset() addDs [zless_trans]) 1);
   2.129 +qed "zless_not_sym";
   2.130 +
   2.131 +(* [| z $< w; ~ P ==> w $< z |] ==> P *)
   2.132 +bind_thm ("zless_asym", zless_not_sym RS swap);
   2.133 +
   2.134 +
   2.135  (*** "Less Than or Equals", $<= ***)
   2.136  
   2.137  Goalw [zle_def] "z $<= z";
   2.138 @@ -795,10 +802,7 @@
   2.139  Goal "~ (z $< w) <-> (w $<= z)";
   2.140  by (cut_inst_tac [("z","z"),("w","w")] zless_linear 1);
   2.141  by (auto_tac (claset() addDs [zless_trans], simpset() addsimps [zle_def]));  
   2.142 -by (auto_tac (claset(), 
   2.143 -            simpset() addsimps [zless_def, zdiff_def, zadd_def, zminus_def]));
   2.144 -by (fold_tac [zless_def, zdiff_def, zadd_def, zminus_def]);
   2.145 -by Auto_tac;  
   2.146 +by (auto_tac (claset() addSDs [zless_imp_intify_neq],  simpset()));
   2.147  qed "not_zless_iff_zle";
   2.148  
   2.149  Goal "~ (z $<= w) <-> (w $< z)";
   2.150 @@ -806,7 +810,6 @@
   2.151  qed "not_zle_iff_zless";
   2.152  
   2.153  
   2.154 -
   2.155  (*** More subtraction laws (for zcompare_rls) ***)
   2.156  
   2.157  Goal "(x $- y) $- z = x $- (y $+ z)";
   2.158 @@ -919,6 +922,19 @@
   2.159  Addsimps [zadd_right_cancel_zle, zadd_left_cancel_zle];
   2.160  
   2.161  
   2.162 +(*** Comparison laws ***)
   2.163 +
   2.164 +Goal "($- x $< $- y) <-> (y $< x)";
   2.165 +by (simp_tac (simpset() addsimps [zless_def, zdiff_def] @ zadd_ac) 1);
   2.166 +qed "zminus_zless_zminus"; 
   2.167 +Addsimps [zminus_zless_zminus];
   2.168 +
   2.169 +Goal "($- x $<= $- y) <-> (y $<= x)";
   2.170 +by (simp_tac (simpset() addsimps [not_zless_iff_zle RS iff_sym]) 1);
   2.171 +qed "zminus_zle_zminus"; 
   2.172 +Addsimps [zminus_zle_zminus];
   2.173 +
   2.174 +
   2.175  (*** More inequality lemmas ***)
   2.176  
   2.177  Goal "[| x: int;  y: int |] ==> (x = $- y) <-> (y = $- x)";
   2.178 @@ -928,3 +944,34 @@
   2.179  Goal "[| x: int;  y: int |] ==> ($- x = y) <-> ($- y = x)";
   2.180  by Auto_tac;
   2.181  qed "zminus_equation";
   2.182 +
   2.183 +Goal "(intify(x) = $- y) <-> (intify(y) = $- x)";
   2.184 +by (cut_inst_tac [("x","intify(x)"), ("y","intify(y)")] equation_zminus 1);
   2.185 +by Auto_tac;
   2.186 +qed "equation_zminus_intify";
   2.187 +
   2.188 +Goal "($- x = intify(y)) <-> ($- y = intify(x))";
   2.189 +by (cut_inst_tac [("x","intify(x)"), ("y","intify(y)")] zminus_equation 1);
   2.190 +by Auto_tac;
   2.191 +qed "zminus_equation_intify";
   2.192 +
   2.193 +
   2.194 +(** The next several equations are permutative: watch out! **)
   2.195 +
   2.196 +Goal "(x $< $- y) <-> (y $< $- x)";
   2.197 +by (simp_tac (simpset() addsimps [zless_def, zdiff_def] @ zadd_ac) 1);
   2.198 +qed "zless_zminus"; 
   2.199 +
   2.200 +Goal "($- x $< y) <-> ($- y $< x)";
   2.201 +by (simp_tac (simpset() addsimps [zless_def, zdiff_def] @ zadd_ac) 1);
   2.202 +qed "zminus_zless"; 
   2.203 +
   2.204 +Goal "(x $<= $- y) <-> (y $<= $- x)";
   2.205 +by (simp_tac (simpset() addsimps [not_zless_iff_zle RS iff_sym, 
   2.206 +                                  zminus_zless]) 1);
   2.207 +qed "zle_zminus"; 
   2.208 +
   2.209 +Goal "($- x $<= y) <-> ($- y $<= x)";
   2.210 +by (simp_tac (simpset() addsimps [not_zless_iff_zle RS iff_sym, 
   2.211 +                                  zless_zminus]) 1);
   2.212 +qed "zminus_zle"; 
     3.1 --- a/src/ZF/Integ/int_arith.ML	Thu Aug 10 14:55:21 2000 +0200
     3.2 +++ b/src/ZF/Integ/int_arith.ML	Fri Aug 11 10:34:02 2000 +0200
     3.3 @@ -315,7 +315,7 @@
     3.4    
     3.5  val combine_numerals_prod = 
     3.6      prep_simproc ("int_combine_numerals_prod",
     3.7 -		  prep_pats ["i $* j", "i $* j"],
     3.8 +		  prep_pats ["i $* j"],
     3.9  		  CombineNumeralsProd.proc);
    3.10  
    3.11  end;