src/ZF/Integ/Int.ML
changeset 9883 c1c8647af477
parent 9578 ab26d6c8ebfe
child 9909 111ccda5009b
     1.1 --- a/src/ZF/Integ/Int.ML	Thu Sep 07 15:31:09 2000 +0200
     1.2 +++ b/src/ZF/Integ/Int.ML	Thu Sep 07 17:36:37 2000 +0200
     1.3 @@ -278,6 +278,32 @@
     1.4               simpset() addsimps [nat_into_Ord RS Ord_0_lt_iff RS iff_sym]));
     1.5  qed "not_znegative_imp_zero";
     1.6  
     1.7 +(**** nat_of: coercion of an integer to a natural number ****)
     1.8 +
     1.9 +Goalw [nat_of_def] "nat_of(intify(z)) = nat_of(z)";
    1.10 +by Auto_tac;  
    1.11 +qed "nat_of_intify";
    1.12 +Addsimps [nat_of_intify];
    1.13 +
    1.14 +Goalw [nat_of_def, raw_nat_of_def] "nat_of($# n) = natify(n)";
    1.15 +by (auto_tac (claset(), simpset() addsimps [int_of_eq]));  
    1.16 +qed "nat_of_int_of";
    1.17 +Addsimps [nat_of_int_of];
    1.18 +
    1.19 +Goalw [raw_nat_of_def] "raw_nat_of(z) : nat";
    1.20 +by Auto_tac;
    1.21 +by (case_tac "EX! m. m: nat & z = int_of(m)" 1);
    1.22 +by (asm_simp_tac (simpset() addsimps [the_0]) 2); 
    1.23 +by (rtac theI2 1);
    1.24 +by Auto_tac;  
    1.25 +qed "raw_nat_of_type";
    1.26 +
    1.27 +Goalw [nat_of_def] "nat_of(z) : nat";
    1.28 +by (simp_tac (simpset() addsimps [raw_nat_of_type]) 1); 
    1.29 +qed "nat_of_type";
    1.30 +AddIffs [nat_of_type];
    1.31 +AddTCs [nat_of_type];
    1.32 +
    1.33  (**** zmagnitude: magnitide of an integer, as a natural number ****)
    1.34  
    1.35  Goalw [zmagnitude_def] "zmagnitude($# n) = natify(n)";
    1.36 @@ -344,6 +370,25 @@
    1.37  by (blast_tac (claset() addDs [zneg_int_of]) 1);
    1.38  qed "int_cases"; 
    1.39  
    1.40 +Goal "[| ~ znegative(z); z: int |] ==> $# (raw_nat_of(z)) = z";  
    1.41 +by (dtac not_zneg_int_of 1);
    1.42 +by (auto_tac (claset(), simpset() addsimps [raw_nat_of_type]));
    1.43 +by (auto_tac (claset(), simpset() addsimps [raw_nat_of_def]));
    1.44 +qed "not_zneg_raw_nat_of"; 
    1.45 +
    1.46 +Goal "~ znegative(intify(z)) ==> $# (nat_of(z)) = intify(z)";  
    1.47 +by (asm_simp_tac (simpset() addsimps [nat_of_def, not_zneg_raw_nat_of]) 1);
    1.48 +qed "not_zneg_nat_of_intify"; 
    1.49 +
    1.50 +Goal "[| ~ znegative(z); z: int |] ==> $# (nat_of(z)) = z";  
    1.51 +by (asm_simp_tac (simpset() addsimps [not_zneg_nat_of_intify]) 1);
    1.52 +qed "not_zneg_nat_of"; 
    1.53 +
    1.54 +Goalw [nat_of_def, raw_nat_of_def] "znegative(intify(z)) ==> nat_of(z) = 0"; 
    1.55 +by Auto_tac;  
    1.56 +qed "zneg_nat_of"; 
    1.57 +Addsimps [zneg_nat_of];
    1.58 +
    1.59  
    1.60  (**** zadd: addition on int ****)
    1.61  
    1.62 @@ -738,10 +783,16 @@
    1.63  by Auto_tac;  
    1.64  qed "zless_iff_succ_zadd";
    1.65  
    1.66 +Goal "[| m: nat; n: nat |] ==> ($#m $< $#n) <-> (m<n)";
    1.67 +by (asm_simp_tac (simpset() addsimps [less_iff_succ_add, zless_iff_succ_zadd, 
    1.68 +	 		  	      int_of_add RS sym]) 1);
    1.69 +by (blast_tac (claset() addIs [sym]) 1); 
    1.70 +qed "zless_int_of";
    1.71 +Addsimps [zless_int_of];
    1.72 +
    1.73  Goalw [zless_def, znegative_def, zdiff_def, int_def] 
    1.74      "[| x $< y; y $< z; x: int; y : int; z: int |] ==> x $< z"; 
    1.75 -by (auto_tac (claset(), 
    1.76 -              simpset() addsimps [zadd, zminus, int_of_def, image_iff]));
    1.77 +by (auto_tac (claset(), simpset() addsimps [zadd, zminus, image_iff]));
    1.78  by (rename_tac "x1 x2 y1 y2" 1);
    1.79  by (res_inst_tac [("x","x1#+x2")] exI 1);  
    1.80  by (res_inst_tac [("x","y1#+y2")] exI 1);