conversion of ML to Isar scripts
authorpaulson
Tue Nov 18 11:01:52 2003 +0100 (2003-11-18)
changeset 1425979f7d3451b1e
parent 14258 9bd184c007f0
child 14260 3862336cd4bd
conversion of ML to Isar scripts
src/HOL/Integ/Equiv.ML
src/HOL/Integ/Equiv.thy
src/HOL/Integ/IntArith.ML
src/HOL/Integ/IntArith.thy
src/HOL/Integ/IntDef.ML
src/HOL/Integ/IntDef.thy
src/HOL/Integ/IntPower.ML
src/HOL/Integ/IntPower.thy
src/HOL/Integ/cooper_proof.ML
src/HOL/Integ/int_arith2.ML
src/HOL/IsaMakefile
src/HOL/Tools/Presburger/cooper_proof.ML
     1.1 --- a/src/HOL/Integ/Equiv.ML	Tue Nov 18 09:45:45 2003 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,38 +0,0 @@
     1.4 -
     1.5 -(* legacy ML bindings *)
     1.6 -
     1.7 -val UN_UN_split_split_eq = thm "UN_UN_split_split_eq";
     1.8 -val UN_constant_eq = thm "UN_constant_eq";
     1.9 -val UN_equiv_class = thm "UN_equiv_class";
    1.10 -val UN_equiv_class2 = thm "UN_equiv_class2";
    1.11 -val UN_equiv_class_inject = thm "UN_equiv_class_inject";
    1.12 -val UN_equiv_class_type = thm "UN_equiv_class_type";
    1.13 -val UN_equiv_class_type2 = thm "UN_equiv_class_type2";
    1.14 -val Union_quotient = thm "Union_quotient";
    1.15 -val comp_equivI = thm "comp_equivI";
    1.16 -val congruent2I = thm "congruent2I";
    1.17 -val congruent2_commuteI = thm "congruent2_commuteI";
    1.18 -val congruent2_def = thm "congruent2_def";
    1.19 -val congruent2_implies_congruent = thm "congruent2_implies_congruent";
    1.20 -val congruent2_implies_congruent_UN = thm "congruent2_implies_congruent_UN";
    1.21 -val congruent_def = thm "congruent_def";
    1.22 -val eq_equiv_class = thm "eq_equiv_class";
    1.23 -val eq_equiv_class_iff = thm "eq_equiv_class_iff";
    1.24 -val equiv_class_eq = thm "equiv_class_eq";
    1.25 -val equiv_class_eq_iff = thm "equiv_class_eq_iff";
    1.26 -val equiv_class_nondisjoint = thm "equiv_class_nondisjoint";
    1.27 -val equiv_class_self = thm "equiv_class_self";
    1.28 -val equiv_class_subset = thm "equiv_class_subset";
    1.29 -val equiv_comp_eq = thm "equiv_comp_eq";
    1.30 -val equiv_def = thm "equiv_def";
    1.31 -val equiv_imp_dvd_card = thm "equiv_imp_dvd_card";
    1.32 -val equiv_type = thm "equiv_type";
    1.33 -val finite_equiv_class = thm "finite_equiv_class";
    1.34 -val finite_quotient = thm "finite_quotient";
    1.35 -val quotientE = thm "quotientE";
    1.36 -val quotientI = thm "quotientI";
    1.37 -val quotient_def = thm "quotient_def";
    1.38 -val quotient_disj = thm "quotient_disj";
    1.39 -val refl_comp_subset = thm "refl_comp_subset";
    1.40 -val subset_equiv_class = thm "subset_equiv_class";
    1.41 -val sym_trans_comp_subset = thm "sym_trans_comp_subset";
     2.1 --- a/src/HOL/Integ/Equiv.thy	Tue Nov 18 09:45:45 2003 +0100
     2.2 +++ b/src/HOL/Integ/Equiv.thy	Tue Nov 18 11:01:52 2003 +0100
     2.3 @@ -270,4 +270,46 @@
     2.4      apply (simp_all add: Union_quotient equiv_type finite_quotient)
     2.5    done
     2.6  
     2.7 +ML
     2.8 +{*
     2.9 +
    2.10 +(* legacy ML bindings *)
    2.11 +
    2.12 +val UN_UN_split_split_eq = thm "UN_UN_split_split_eq";
    2.13 +val UN_constant_eq = thm "UN_constant_eq";
    2.14 +val UN_equiv_class = thm "UN_equiv_class";
    2.15 +val UN_equiv_class2 = thm "UN_equiv_class2";
    2.16 +val UN_equiv_class_inject = thm "UN_equiv_class_inject";
    2.17 +val UN_equiv_class_type = thm "UN_equiv_class_type";
    2.18 +val UN_equiv_class_type2 = thm "UN_equiv_class_type2";
    2.19 +val Union_quotient = thm "Union_quotient";
    2.20 +val comp_equivI = thm "comp_equivI";
    2.21 +val congruent2I = thm "congruent2I";
    2.22 +val congruent2_commuteI = thm "congruent2_commuteI";
    2.23 +val congruent2_def = thm "congruent2_def";
    2.24 +val congruent2_implies_congruent = thm "congruent2_implies_congruent";
    2.25 +val congruent2_implies_congruent_UN = thm "congruent2_implies_congruent_UN";
    2.26 +val congruent_def = thm "congruent_def";
    2.27 +val eq_equiv_class = thm "eq_equiv_class";
    2.28 +val eq_equiv_class_iff = thm "eq_equiv_class_iff";
    2.29 +val equiv_class_eq = thm "equiv_class_eq";
    2.30 +val equiv_class_eq_iff = thm "equiv_class_eq_iff";
    2.31 +val equiv_class_nondisjoint = thm "equiv_class_nondisjoint";
    2.32 +val equiv_class_self = thm "equiv_class_self";
    2.33 +val equiv_class_subset = thm "equiv_class_subset";
    2.34 +val equiv_comp_eq = thm "equiv_comp_eq";
    2.35 +val equiv_def = thm "equiv_def";
    2.36 +val equiv_imp_dvd_card = thm "equiv_imp_dvd_card";
    2.37 +val equiv_type = thm "equiv_type";
    2.38 +val finite_equiv_class = thm "finite_equiv_class";
    2.39 +val finite_quotient = thm "finite_quotient";
    2.40 +val quotientE = thm "quotientE";
    2.41 +val quotientI = thm "quotientI";
    2.42 +val quotient_def = thm "quotient_def";
    2.43 +val quotient_disj = thm "quotient_disj";
    2.44 +val refl_comp_subset = thm "refl_comp_subset";
    2.45 +val subset_equiv_class = thm "subset_equiv_class";
    2.46 +val sym_trans_comp_subset = thm "sym_trans_comp_subset";
    2.47 +*}
    2.48 +
    2.49  end
     3.1 --- a/src/HOL/Integ/IntArith.ML	Tue Nov 18 09:45:45 2003 +0100
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,221 +0,0 @@
     3.4 -(*  Title:      HOL/Integ/IntArith.ML
     3.5 -    ID:         $Id$
     3.6 -    Authors:    Larry Paulson and Tobias Nipkow
     3.7 -*)
     3.8 -
     3.9 -
    3.10 -Goal "x - - y = x + (y::int)";
    3.11 -by (Simp_tac 1); 
    3.12 -qed "int_diff_minus_eq";
    3.13 -Addsimps [int_diff_minus_eq];
    3.14 -
    3.15 -Goal "abs(abs(x::int)) = abs(x)";
    3.16 -by (arith_tac 1);
    3.17 -qed "abs_abs";
    3.18 -Addsimps [abs_abs];
    3.19 -
    3.20 -Goal "abs(-(x::int)) = abs(x)";
    3.21 -by (arith_tac 1);
    3.22 -qed "abs_minus";
    3.23 -Addsimps [abs_minus];
    3.24 -
    3.25 -Goal "abs(x+y) <= abs(x) + abs(y::int)";
    3.26 -by (arith_tac 1);
    3.27 -qed "triangle_ineq";
    3.28 -
    3.29 -
    3.30 -(*** Intermediate value theorems ***)
    3.31 -
    3.32 -Goal "(ALL i<n::nat. abs(f(i+1) - f i) <= 1) --> \
    3.33 -\     f 0 <= k --> k <= f n --> (EX i <= n. f i = (k::int))";
    3.34 -by (induct_tac "n" 1);
    3.35 - by (Asm_simp_tac 1);
    3.36 -by (strip_tac 1);
    3.37 -by (etac impE 1);
    3.38 - by (Asm_full_simp_tac 1);
    3.39 -by (eres_inst_tac [("x","n")] allE 1);
    3.40 -by (Asm_full_simp_tac 1);
    3.41 -by (case_tac "k = f(n+1)" 1);
    3.42 - by (Force_tac 1);
    3.43 -by (etac impE 1);
    3.44 - by (asm_full_simp_tac (simpset() addsimps [zabs_def] 
    3.45 -                                 addsplits [split_if_asm]) 1);
    3.46 -by (blast_tac (claset() addIs [le_SucI]) 1);
    3.47 -val lemma = result();
    3.48 -
    3.49 -bind_thm("nat0_intermed_int_val", ObjectLogic.rulify_no_asm lemma);
    3.50 -
    3.51 -Goal "[| !i. m <= i & i < n --> abs(f(i + 1::nat) - f i) <= 1; m < n; \
    3.52 -\        f m <= k; k <= f n |] ==> ? i. m <= i & i <= n & f i = (k::int)";
    3.53 -by (cut_inst_tac [("n","n-m"),("f", "%i. f(i+m)"),("k","k")]lemma 1);
    3.54 -by (Asm_full_simp_tac 1);
    3.55 -by (etac impE 1);
    3.56 - by (strip_tac 1);
    3.57 - by (eres_inst_tac [("x","i+m")] allE 1);
    3.58 - by (arith_tac 1);
    3.59 -by (etac exE 1);
    3.60 -by (res_inst_tac [("x","i+m")] exI 1);
    3.61 -by (arith_tac 1);
    3.62 -qed "nat_intermed_int_val";
    3.63 -
    3.64 -
    3.65 -(*** Some convenient biconditionals for products of signs ***)
    3.66 -
    3.67 -Goal "[| (0::int) < i; 0 < j |] ==> 0 < i*j";
    3.68 -by (dtac zmult_zless_mono1 1);
    3.69 -by Auto_tac; 
    3.70 -qed "zmult_pos";
    3.71 -
    3.72 -Goal "[| i < (0::int); j < 0 |] ==> 0 < i*j";
    3.73 -by (dtac zmult_zless_mono1_neg 1);
    3.74 -by Auto_tac; 
    3.75 -qed "zmult_neg";
    3.76 -
    3.77 -Goal "[| (0::int) < i; j < 0 |] ==> i*j < 0";
    3.78 -by (dtac zmult_zless_mono1_neg 1);
    3.79 -by Auto_tac; 
    3.80 -qed "zmult_pos_neg";
    3.81 -
    3.82 -Goal "((0::int) < x*y) = (0 < x & 0 < y | x < 0 & y < 0)";
    3.83 -by (auto_tac (claset(), 
    3.84 -              simpset() addsimps [order_le_less, linorder_not_less,
    3.85 -	                          zmult_pos, zmult_neg]));
    3.86 -by (ALLGOALS (rtac ccontr)); 
    3.87 -by (auto_tac (claset(), 
    3.88 -	      simpset() addsimps [order_le_less, linorder_not_less]));
    3.89 -by (ALLGOALS (etac rev_mp)); 
    3.90 -by (ALLGOALS (dtac zmult_pos_neg THEN' assume_tac));
    3.91 -by (auto_tac (claset() addDs [order_less_not_sym], 
    3.92 -              simpset() addsimps [zmult_commute]));  
    3.93 -qed "int_0_less_mult_iff";
    3.94 -
    3.95 -Goal "((0::int) <= x*y) = (0 <= x & 0 <= y | x <= 0 & y <= 0)";
    3.96 -by (auto_tac (claset(), 
    3.97 -              simpset() addsimps [order_le_less, linorder_not_less,  
    3.98 -                                  int_0_less_mult_iff]));
    3.99 -qed "int_0_le_mult_iff";
   3.100 -
   3.101 -Goal "(x*y < (0::int)) = (0 < x & y < 0 | x < 0 & 0 < y)";
   3.102 -by (auto_tac (claset(), 
   3.103 -              simpset() addsimps [int_0_le_mult_iff, 
   3.104 -                                  linorder_not_le RS sym]));
   3.105 -by (auto_tac (claset() addDs [order_less_not_sym],  
   3.106 -              simpset() addsimps [linorder_not_le]));
   3.107 -qed "zmult_less_0_iff";
   3.108 -
   3.109 -Goal "(x*y <= (0::int)) = (0 <= x & y <= 0 | x <= 0 & 0 <= y)";
   3.110 -by (auto_tac (claset() addDs [order_less_not_sym], 
   3.111 -              simpset() addsimps [int_0_less_mult_iff, 
   3.112 -                                  linorder_not_less RS sym]));
   3.113 -qed "zmult_le_0_iff";
   3.114 -
   3.115 -Goal "abs (x * y) = abs x * abs (y::int)";
   3.116 -by (simp_tac (simpset () delsimps [thm "number_of_reorient"] addsplits [zabs_split] 
   3.117 -                         addsplits [zabs_split] 
   3.118 -                         addsimps [zmult_less_0_iff, zle_def]) 1);
   3.119 -qed "abs_mult";
   3.120 -
   3.121 -Goal "(abs x = 0) = (x = (0::int))";
   3.122 -by (simp_tac (simpset () addsplits [zabs_split]) 1);
   3.123 -qed "abs_eq_0";
   3.124 -AddIffs [abs_eq_0];
   3.125 -
   3.126 -Goal "(0 < abs x) = (x ~= (0::int))";
   3.127 -by (simp_tac (simpset () addsplits [zabs_split]) 1);
   3.128 -by (arith_tac 1);
   3.129 -qed "zero_less_abs_iff";
   3.130 -AddIffs [zero_less_abs_iff];
   3.131 -
   3.132 -Goal "0 <= x * (x::int)";
   3.133 -by (subgoal_tac "(- x) * x <= 0" 1);
   3.134 - by (Asm_full_simp_tac 1);
   3.135 -by (simp_tac (HOL_basic_ss addsimps [zmult_le_0_iff]) 1);
   3.136 -by Auto_tac;
   3.137 -qed "square_nonzero";
   3.138 -Addsimps [square_nonzero];
   3.139 -AddIs [square_nonzero];
   3.140 -
   3.141 -
   3.142 -(*** Products and 1, by T. M. Rasmussen ***)
   3.143 -
   3.144 -Goal "(m = m*(n::int)) = (n = 1 | m = 0)";
   3.145 -by Auto_tac;
   3.146 -by (subgoal_tac "m*1 = m*n" 1);
   3.147 -by (dtac (zmult_cancel1 RS iffD1) 1); 
   3.148 -by Auto_tac;
   3.149 -qed "zmult_eq_self_iff";
   3.150 -
   3.151 -Goal "[| 1 < m; 1 < n |] ==> 1 < m*(n::int)";
   3.152 -by (res_inst_tac [("y","1*n")] order_less_trans 1);
   3.153 -by (rtac zmult_zless_mono1 2);
   3.154 -by (ALLGOALS Asm_simp_tac);
   3.155 -qed "zless_1_zmult";
   3.156 -
   3.157 -Goal "[| 0 < n; n ~= 1 |] ==> 1 < (n::int)";
   3.158 -by (arith_tac 1);
   3.159 -val lemma = result();
   3.160 -
   3.161 -Goal "0 < (m::int) ==> (m * n = 1) = (m = 1 & n = 1)";
   3.162 -by Auto_tac;
   3.163 -by (case_tac "m=1" 1);
   3.164 -by (case_tac "n=1" 2);
   3.165 -by (case_tac "m=1" 4);
   3.166 -by (case_tac "n=1" 5);
   3.167 -by Auto_tac;
   3.168 -by distinct_subgoals_tac;
   3.169 -by (subgoal_tac "1<m*n" 1);
   3.170 -by (Asm_full_simp_tac 1);
   3.171 -by (rtac zless_1_zmult 1);
   3.172 -by (ALLGOALS (rtac lemma));
   3.173 -by Auto_tac;  
   3.174 -by (subgoal_tac "0<m*n" 1);
   3.175 -by (Asm_simp_tac 2);
   3.176 -by (dtac (int_0_less_mult_iff RS iffD1) 1);
   3.177 -by Auto_tac;  
   3.178 -qed "pos_zmult_eq_1_iff";
   3.179 -
   3.180 -Goal "(m*n = (1::int)) = ((m = 1 & n = 1) | (m = -1 & n = -1))";
   3.181 -by (case_tac "0<m" 1);
   3.182 -by (asm_simp_tac (simpset() addsimps [pos_zmult_eq_1_iff]) 1);
   3.183 -by (case_tac "m=0" 1);
   3.184 -by (asm_simp_tac (simpset () delsimps [thm "number_of_reorient"]) 1);
   3.185 -by (subgoal_tac "0 < -m" 1);
   3.186 -by (arith_tac 2);
   3.187 -by (dres_inst_tac [("n","-n")] pos_zmult_eq_1_iff 1); 
   3.188 -by Auto_tac;  
   3.189 -qed "zmult_eq_1_iff";
   3.190 -
   3.191 -
   3.192 -(*** More about nat ***)
   3.193 -
   3.194 -Goal "[| (0::int) <= z;  0 <= z' |] ==> nat (z+z') = nat z + nat z'";
   3.195 -by (rtac (inj_int RS injD) 1);
   3.196 -by (asm_simp_tac (simpset() addsimps [zadd_int RS sym]) 1);
   3.197 -qed "nat_add_distrib";
   3.198 -
   3.199 -Goal "[| (0::int) <= z';  z' <= z |] ==> nat (z-z') = nat z - nat z'";
   3.200 -by (rtac (inj_int RS injD) 1);
   3.201 -by (asm_simp_tac (simpset() addsimps [zdiff_int RS sym, nat_le_eq_zle]) 1);
   3.202 -qed "nat_diff_distrib";
   3.203 -
   3.204 -Goal "(0::int) <= z ==> nat (z*z') = nat z * nat z'";
   3.205 -by (case_tac "0 <= z'" 1);
   3.206 -by (asm_full_simp_tac (simpset() addsimps [zmult_le_0_iff]) 2);
   3.207 -by (rtac (inj_int RS injD) 1);
   3.208 -by (asm_simp_tac (simpset() addsimps [zmult_int RS sym,
   3.209 -				      int_0_le_mult_iff]) 1);
   3.210 -qed "nat_mult_distrib";
   3.211 -
   3.212 -Goal "z <= (0::int) ==> nat(z*z') = nat(-z) * nat(-z')"; 
   3.213 -by (rtac trans 1); 
   3.214 -by (rtac nat_mult_distrib 2); 
   3.215 -by Auto_tac;  
   3.216 -qed "nat_mult_distrib_neg";
   3.217 -
   3.218 -Goal "nat (abs (w * z)) = nat (abs w) * nat (abs z)";
   3.219 -by (case_tac "z=0 | w=0" 1);
   3.220 -by Auto_tac;  
   3.221 -by (simp_tac (simpset() addsimps [zabs_def, nat_mult_distrib RS sym, 
   3.222 -                          nat_mult_distrib_neg RS sym, zmult_less_0_iff]) 1);
   3.223 -by (arith_tac 1);
   3.224 -qed "nat_abs_mult_distrib";
     4.1 --- a/src/HOL/Integ/IntArith.thy	Tue Nov 18 09:45:45 2003 +0100
     4.2 +++ b/src/HOL/Integ/IntArith.thy	Tue Nov 18 11:01:52 2003 +0100
     4.3 @@ -1,12 +1,87 @@
     4.4 +(*  Title:      HOL/Integ/IntArith.thy
     4.5 +    ID:         $Id$
     4.6 +    Authors:    Larry Paulson and Tobias Nipkow
     4.7 +*)
     4.8  
     4.9  header {* Integer arithmetic *}
    4.10  
    4.11  theory IntArith = Bin
    4.12 -files ("int_arith1.ML") ("int_arith2.ML"):
    4.13 +files ("int_arith1.ML"):
    4.14  
    4.15  use "int_arith1.ML"
    4.16  setup int_arith_setup
    4.17 -use "int_arith2.ML"
    4.18 +
    4.19 +lemma zle_diff1_eq [simp]: "(w <= z - (1::int)) = (w<(z::int))"
    4.20 +by arith
    4.21 +
    4.22 +lemma zle_add1_eq_le [simp]: "(w < z + 1) = (w<=(z::int))"
    4.23 +by arith
    4.24 +
    4.25 +lemma zadd_left_cancel0 [simp]: "(z = z + w) = (w = (0::int))"
    4.26 +by arith
    4.27 +
    4.28 +subsection{*Results about @{term nat}*}
    4.29 +
    4.30 +lemma nonneg_eq_int: "[| 0 <= z;  !!m. z = int m ==> P |] ==> P"
    4.31 +by (blast dest: nat_0_le sym)
    4.32 +
    4.33 +lemma nat_eq_iff: "(nat w = m) = (if 0 <= w then w = int m else m=0)"
    4.34 +by auto
    4.35 +
    4.36 +lemma nat_eq_iff2: "(m = nat w) = (if 0 <= w then w = int m else m=0)"
    4.37 +by auto
    4.38 +
    4.39 +lemma nat_less_iff: "0 <= w ==> (nat w < m) = (w < int m)"
    4.40 +apply (rule iffI)
    4.41 +apply (erule nat_0_le [THEN subst])
    4.42 +apply (simp_all del: zless_int add: zless_int [symmetric]) 
    4.43 +done
    4.44 +
    4.45 +lemma int_eq_iff: "(int m = z) = (m = nat z & 0 <= z)"
    4.46 +by (auto simp add: nat_eq_iff2)
    4.47 +
    4.48 +
    4.49 +(*Users don't want to see (int 0), int(Suc 0) or w + - z*)
    4.50 +declare Zero_int_def [symmetric, simp]
    4.51 +declare One_int_def [symmetric, simp]
    4.52 +
    4.53 +text{*cooper.ML refers to this theorem*}
    4.54 +lemmas zdiff_def_symmetric = zdiff_def [symmetric, simp]
    4.55 +
    4.56 +lemma nat_0: "nat 0 = 0"
    4.57 +by (simp add: nat_eq_iff)
    4.58 +
    4.59 +lemma nat_1: "nat 1 = Suc 0"
    4.60 +by (subst nat_eq_iff, simp)
    4.61 +
    4.62 +lemma nat_2: "nat 2 = Suc (Suc 0)"
    4.63 +by (subst nat_eq_iff, simp)
    4.64 +
    4.65 +lemma nat_less_eq_zless: "0 <= w ==> (nat w < nat z) = (w<z)"
    4.66 +apply (case_tac "neg z")
    4.67 +apply (auto simp add: nat_less_iff)
    4.68 +apply (auto intro: zless_trans simp add: neg_eq_less_0 zle_def)
    4.69 +done
    4.70 +
    4.71 +lemma nat_le_eq_zle: "0 < w | 0 <= z ==> (nat w <= nat z) = (w<=z)"
    4.72 +by (auto simp add: linorder_not_less [symmetric] zless_nat_conj)
    4.73 +
    4.74 +subsection{*@{term abs}: Absolute Value, as an Integer*}
    4.75 +
    4.76 +(* Simpler: use zabs_def as rewrite rule
    4.77 +   but arith_tac is not parameterized by such simp rules
    4.78 +*)
    4.79 +
    4.80 +lemma zabs_split: "P(abs(i::int)) = ((0 <= i --> P i) & (i < 0 --> P(-i)))"
    4.81 +by (simp add: zabs_def)
    4.82 +
    4.83 +lemma zero_le_zabs [iff]: "0 <= abs (z::int)"
    4.84 +by (simp add: zabs_def)
    4.85 +
    4.86 +
    4.87 +text{*This simplifies expressions of the form @{term "int n = z"} where
    4.88 +      z is an integer literal.*}
    4.89 +declare int_eq_iff [of _ "number_of v", standard, simp]
    4.90  
    4.91  declare zabs_split [arith_split]
    4.92  
    4.93 @@ -18,7 +93,7 @@
    4.94    by simp
    4.95  
    4.96  lemma split_nat[arith_split]:
    4.97 -  "P(nat(i::int)) = ((ALL n. i = int n \<longrightarrow> P n) & (i < 0 \<longrightarrow> P 0))"
    4.98 +  "P(nat(i::int)) = ((\<forall>n. i = int n \<longrightarrow> P n) & (i < 0 \<longrightarrow> P 0))"
    4.99    (is "?P = (?L & ?R)")
   4.100  proof (cases "i < 0")
   4.101    case True thus ?thesis by simp
   4.102 @@ -69,8 +144,7 @@
   4.103  apply(rule int_ge_induct[of "k + 1"])
   4.104    using gr apply arith
   4.105   apply(rule base)
   4.106 -apply(rule step)
   4.107 - apply simp+
   4.108 +apply (rule step, simp+)
   4.109  done
   4.110  
   4.111  theorem int_le_induct[consumes 1,case_names base step]:
   4.112 @@ -105,9 +179,216 @@
   4.113  apply(rule int_le_induct[of _ "k - 1"])
   4.114    using less apply arith
   4.115   apply(rule base)
   4.116 -apply(rule step)
   4.117 - apply simp+
   4.118 +apply (rule step, simp+)
   4.119 +done
   4.120 +
   4.121 +subsection{*Simple Equations*}
   4.122 +
   4.123 +lemma int_diff_minus_eq [simp]: "x - - y = x + (y::int)"
   4.124 +by simp
   4.125 +
   4.126 +lemma abs_abs [simp]: "abs(abs(x::int)) = abs(x)"
   4.127 +by arith
   4.128 +
   4.129 +lemma abs_minus [simp]: "abs(-(x::int)) = abs(x)"
   4.130 +by arith
   4.131 +
   4.132 +lemma triangle_ineq: "abs(x+y) <= abs(x) + abs(y::int)"
   4.133 +by arith
   4.134 +
   4.135 +
   4.136 +subsection{*Intermediate value theorems*}
   4.137 +
   4.138 +lemma int_val_lemma:
   4.139 +     "(\<forall>i<n::nat. abs(f(i+1) - f i) \<le> 1) -->  
   4.140 +      f 0 \<le> k --> k \<le> f n --> (\<exists>i \<le> n. f i = (k::int))"
   4.141 +apply (induct_tac "n")
   4.142 + apply (simp (no_asm_simp))
   4.143 +apply (intro strip)
   4.144 +apply (erule impE, simp)
   4.145 +apply (erule_tac x = n in allE, simp)
   4.146 +apply (case_tac "k = f (n+1) ")
   4.147 + apply force
   4.148 +apply (erule impE)
   4.149 + apply (simp add: zabs_def split add: split_if_asm)
   4.150 +apply (blast intro: le_SucI)
   4.151 +done
   4.152 +
   4.153 +lemmas nat0_intermed_int_val = int_val_lemma [rule_format (no_asm)]
   4.154 +
   4.155 +lemma nat_intermed_int_val:
   4.156 +     "[| \<forall>i. m \<le> i & i < n --> abs(f(i + 1::nat) - f i) \<le> 1; m < n;  
   4.157 +         f m \<le> k; k \<le> f n |] ==> ? i. m \<le> i & i \<le> n & f i = (k::int)"
   4.158 +apply (cut_tac n = "n-m" and f = "%i. f (i+m) " and k = k 
   4.159 +       in int_val_lemma)
   4.160 +apply simp
   4.161 +apply (erule impE)
   4.162 + apply (intro strip)
   4.163 + apply (erule_tac x = "i+m" in allE, arith)
   4.164 +apply (erule exE)
   4.165 +apply (rule_tac x = "i+m" in exI, arith)
   4.166 +done
   4.167 +
   4.168 +
   4.169 +subsection{*Some convenient biconditionals for products of signs*}
   4.170 +
   4.171 +lemma zmult_pos: "[| (0::int) < i; 0 < j |] ==> 0 < i*j"
   4.172 +by (drule zmult_zless_mono1, auto)
   4.173 +
   4.174 +lemma zmult_neg: "[| i < (0::int); j < 0 |] ==> 0 < i*j"
   4.175 +by (drule zmult_zless_mono1_neg, auto)
   4.176 +
   4.177 +lemma zmult_pos_neg: "[| (0::int) < i; j < 0 |] ==> i*j < 0"
   4.178 +by (drule zmult_zless_mono1_neg, auto)
   4.179 +
   4.180 +lemma int_0_less_mult_iff: "((0::int) < x*y) = (0 < x & 0 < y | x < 0 & y < 0)"
   4.181 +apply (auto simp add: order_le_less linorder_not_less zmult_pos zmult_neg)
   4.182 +apply (rule_tac [!] ccontr)
   4.183 +apply (auto simp add: order_le_less linorder_not_less)
   4.184 +apply (erule_tac [!] rev_mp)
   4.185 +apply (drule_tac [!] zmult_pos_neg)
   4.186 +apply (auto dest: order_less_not_sym simp add: zmult_commute)
   4.187 +done
   4.188 +
   4.189 +lemma int_0_le_mult_iff: "((0::int) \<le> x*y) = (0 \<le> x & 0 \<le> y | x \<le> 0 & y \<le> 0)"
   4.190 +by (auto simp add: order_le_less linorder_not_less int_0_less_mult_iff)
   4.191 +
   4.192 +lemma zmult_less_0_iff: "(x*y < (0::int)) = (0 < x & y < 0 | x < 0 & 0 < y)"
   4.193 +by (auto simp add: int_0_le_mult_iff linorder_not_le [symmetric])
   4.194 +
   4.195 +lemma zmult_le_0_iff: "(x*y \<le> (0::int)) = (0 \<le> x & y \<le> 0 | x \<le> 0 & 0 \<le> y)"
   4.196 +by (auto dest: order_less_not_sym simp add: int_0_less_mult_iff linorder_not_less [symmetric])
   4.197 +
   4.198 +lemma abs_mult: "abs (x * y) = abs x * abs (y::int)"
   4.199 +by (simp del: number_of_reorient split
   4.200 +          add: zabs_split split add: zabs_split add: zmult_less_0_iff zle_def)
   4.201 +
   4.202 +lemma abs_eq_0 [iff]: "(abs x = 0) = (x = (0::int))"
   4.203 +by (simp split add: zabs_split)
   4.204 +
   4.205 +lemma zero_less_abs_iff [iff]: "(0 < abs x) = (x ~= (0::int))"
   4.206 +by (simp split add: zabs_split, arith)
   4.207 +
   4.208 +(* THIS LOOKS WRONG: [intro]*)
   4.209 +lemma square_nonzero [simp]: "0 \<le> x * (x::int)"
   4.210 +apply (subgoal_tac " (- x) * x \<le> 0")
   4.211 + apply simp
   4.212 +apply (simp only: zmult_le_0_iff, auto)
   4.213 +done
   4.214 +
   4.215 +
   4.216 +subsection{*Products and 1, by T. M. Rasmussen*}
   4.217 +
   4.218 +lemma zmult_eq_self_iff: "(m = m*(n::int)) = (n = 1 | m = 0)"
   4.219 +apply auto
   4.220 +apply (subgoal_tac "m*1 = m*n")
   4.221 +apply (drule zmult_cancel1 [THEN iffD1], auto)
   4.222  done
   4.223  
   4.224 +lemma zless_1_zmult: "[| 1 < m; 1 < n |] ==> 1 < m*(n::int)"
   4.225 +apply (rule_tac y = "1*n" in order_less_trans)
   4.226 +apply (rule_tac [2] zmult_zless_mono1)
   4.227 +apply (simp_all (no_asm_simp))
   4.228 +done
   4.229 +
   4.230 +lemma pos_zmult_eq_1_iff: "0 < (m::int) ==> (m * n = 1) = (m = 1 & n = 1)"
   4.231 +apply auto
   4.232 +apply (case_tac "m=1")
   4.233 +apply (case_tac [2] "n=1")
   4.234 +apply (case_tac [4] "m=1")
   4.235 +apply (case_tac [5] "n=1", auto)
   4.236 +apply (tactic"distinct_subgoals_tac")
   4.237 +apply (subgoal_tac "1<m*n", simp)
   4.238 +apply (rule zless_1_zmult, arith)
   4.239 +apply (subgoal_tac "0<n", arith)
   4.240 +apply (subgoal_tac "0<m*n")
   4.241 +apply (drule int_0_less_mult_iff [THEN iffD1], auto)
   4.242 +done
   4.243 +
   4.244 +lemma zmult_eq_1_iff: "(m*n = (1::int)) = ((m = 1 & n = 1) | (m = -1 & n = -1))"
   4.245 +apply (case_tac "0<m")
   4.246 +apply (simp (no_asm_simp) add: pos_zmult_eq_1_iff)
   4.247 +apply (case_tac "m=0")
   4.248 +apply (simp (no_asm_simp) del: number_of_reorient)
   4.249 +apply (subgoal_tac "0 < -m")
   4.250 +apply (drule_tac n = "-n" in pos_zmult_eq_1_iff, auto)
   4.251 +done
   4.252 +
   4.253 +
   4.254 +subsection{*More about nat*}
   4.255 +
   4.256 +lemma nat_add_distrib:
   4.257 +     "[| (0::int) \<le> z;  0 \<le> z' |] ==> nat (z+z') = nat z + nat z'"
   4.258 +apply (rule inj_int [THEN injD])
   4.259 +apply (simp (no_asm_simp) add: zadd_int [symmetric])
   4.260 +done
   4.261 +
   4.262 +lemma nat_diff_distrib:
   4.263 +     "[| (0::int) \<le> z';  z' \<le> z |] ==> nat (z-z') = nat z - nat z'"
   4.264 +apply (rule inj_int [THEN injD])
   4.265 +apply (simp (no_asm_simp) add: zdiff_int [symmetric] nat_le_eq_zle)
   4.266 +done
   4.267 +
   4.268 +lemma nat_mult_distrib: "(0::int) \<le> z ==> nat (z*z') = nat z * nat z'"
   4.269 +apply (case_tac "0 \<le> z'")
   4.270 +apply (rule inj_int [THEN injD])
   4.271 +apply (simp (no_asm_simp) add: zmult_int [symmetric] int_0_le_mult_iff)
   4.272 +apply (simp add: zmult_le_0_iff)
   4.273 +done
   4.274 +
   4.275 +lemma nat_mult_distrib_neg: "z \<le> (0::int) ==> nat(z*z') = nat(-z) * nat(-z')"
   4.276 +apply (rule trans)
   4.277 +apply (rule_tac [2] nat_mult_distrib, auto)
   4.278 +done
   4.279 +
   4.280 +lemma nat_abs_mult_distrib: "nat (abs (w * z)) = nat (abs w) * nat (abs z)"
   4.281 +apply (case_tac "z=0 | w=0")
   4.282 +apply (auto simp add: zabs_def nat_mult_distrib [symmetric] 
   4.283 +                      nat_mult_distrib_neg [symmetric] zmult_less_0_iff)
   4.284 +done
   4.285 +
   4.286 +ML
   4.287 +{*
   4.288 +val zle_diff1_eq = thm "zle_diff1_eq";
   4.289 +val zle_add1_eq_le = thm "zle_add1_eq_le";
   4.290 +val nonneg_eq_int = thm "nonneg_eq_int";
   4.291 +val nat_eq_iff = thm "nat_eq_iff";
   4.292 +val nat_eq_iff2 = thm "nat_eq_iff2";
   4.293 +val nat_less_iff = thm "nat_less_iff";
   4.294 +val int_eq_iff = thm "int_eq_iff";
   4.295 +val nat_0 = thm "nat_0";
   4.296 +val nat_1 = thm "nat_1";
   4.297 +val nat_2 = thm "nat_2";
   4.298 +val nat_less_eq_zless = thm "nat_less_eq_zless";
   4.299 +val nat_le_eq_zle = thm "nat_le_eq_zle";
   4.300 +val zabs_split = thm "zabs_split";
   4.301 +val zero_le_zabs = thm "zero_le_zabs";
   4.302 +
   4.303 +val int_diff_minus_eq = thm "int_diff_minus_eq";
   4.304 +val abs_abs = thm "abs_abs";
   4.305 +val abs_minus = thm "abs_minus";
   4.306 +val triangle_ineq = thm "triangle_ineq";
   4.307 +val nat_intermed_int_val = thm "nat_intermed_int_val";
   4.308 +val zmult_pos = thm "zmult_pos";
   4.309 +val zmult_neg = thm "zmult_neg";
   4.310 +val zmult_pos_neg = thm "zmult_pos_neg";
   4.311 +val int_0_less_mult_iff = thm "int_0_less_mult_iff";
   4.312 +val int_0_le_mult_iff = thm "int_0_le_mult_iff";
   4.313 +val zmult_less_0_iff = thm "zmult_less_0_iff";
   4.314 +val zmult_le_0_iff = thm "zmult_le_0_iff";
   4.315 +val abs_mult = thm "abs_mult";
   4.316 +val abs_eq_0 = thm "abs_eq_0";
   4.317 +val zero_less_abs_iff = thm "zero_less_abs_iff";
   4.318 +val square_nonzero = thm "square_nonzero";
   4.319 +val zmult_eq_self_iff = thm "zmult_eq_self_iff";
   4.320 +val zless_1_zmult = thm "zless_1_zmult";
   4.321 +val pos_zmult_eq_1_iff = thm "pos_zmult_eq_1_iff";
   4.322 +val zmult_eq_1_iff = thm "zmult_eq_1_iff";
   4.323 +val nat_add_distrib = thm "nat_add_distrib";
   4.324 +val nat_diff_distrib = thm "nat_diff_distrib";
   4.325 +val nat_mult_distrib = thm "nat_mult_distrib";
   4.326 +val nat_mult_distrib_neg = thm "nat_mult_distrib_neg";
   4.327 +val nat_abs_mult_distrib = thm "nat_abs_mult_distrib";
   4.328 +*}
   4.329 +
   4.330  end
   4.331 -
     5.1 --- a/src/HOL/Integ/IntDef.ML	Tue Nov 18 09:45:45 2003 +0100
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,580 +0,0 @@
     5.4 -(*  Title:      IntDef.ML
     5.5 -    ID:         $Id$
     5.6 -    Authors:    Lawrence C Paulson, Cambridge University Computer Laboratory
     5.7 -    Copyright   1993  University of Cambridge
     5.8 -
     5.9 -The integers as equivalence classes over nat*nat.
    5.10 -*)
    5.11 -
    5.12 -
    5.13 -Goalw  [intrel_def] "(((x1,y1),(x2,y2)): intrel) = (x1+y2 = x2+y1)";
    5.14 -by (Blast_tac 1);
    5.15 -qed "intrel_iff";
    5.16 -
    5.17 -Goalw [intrel_def, equiv_def, refl_def, sym_def, trans_def]
    5.18 -    "equiv UNIV intrel";
    5.19 -by Auto_tac;
    5.20 -qed "equiv_intrel";
    5.21 -
    5.22 -bind_thm ("equiv_intrel_iff", 
    5.23 -	  [equiv_intrel, UNIV_I, UNIV_I] MRS eq_equiv_class_iff);
    5.24 -
    5.25 -Goalw [Integ_def,intrel_def,quotient_def]
    5.26 -     "intrel``{(x,y)}:Integ";
    5.27 -by (Fast_tac 1);
    5.28 -qed "intrel_in_integ";
    5.29 -
    5.30 -Goal "inj_on Abs_Integ Integ";
    5.31 -by (rtac inj_on_inverseI 1);
    5.32 -by (etac Abs_Integ_inverse 1);
    5.33 -qed "inj_on_Abs_Integ";
    5.34 -
    5.35 -Addsimps [equiv_intrel_iff, inj_on_Abs_Integ RS inj_on_iff,
    5.36 -          intrel_iff, intrel_in_integ, Abs_Integ_inverse];
    5.37 -
    5.38 -Goal "inj(Rep_Integ)";
    5.39 -by (rtac inj_inverseI 1);
    5.40 -by (rtac Rep_Integ_inverse 1);
    5.41 -qed "inj_Rep_Integ";
    5.42 -
    5.43 -
    5.44 -(** int: the injection from "nat" to "int" **)
    5.45 -
    5.46 -Goal "inj int";
    5.47 -by (rtac injI 1);
    5.48 -by (rewtac int_def);
    5.49 -by (dtac (inj_on_Abs_Integ RS inj_onD) 1);
    5.50 -by (REPEAT (rtac intrel_in_integ 1));
    5.51 -by (dtac eq_equiv_class 1);
    5.52 -by (rtac equiv_intrel 1);
    5.53 -by (Fast_tac 1);
    5.54 -by (asm_full_simp_tac (simpset() addsimps [intrel_def]) 1);
    5.55 -qed "inj_int";
    5.56 -
    5.57 -
    5.58 -(**** zminus: unary negation on Integ ****)
    5.59 -
    5.60 -Goalw [congruent_def, intrel_def]
    5.61 -     "congruent intrel (%(x,y). intrel``{(y,x)})";
    5.62 -by (auto_tac (claset(), simpset() addsimps add_ac));
    5.63 -qed "zminus_congruent";
    5.64 -
    5.65 -Goalw [zminus_def]
    5.66 -      "- Abs_Integ(intrel``{(x,y)}) = Abs_Integ(intrel `` {(y,x)})";
    5.67 -by (simp_tac (simpset() addsimps 
    5.68 -	      [equiv_intrel RS UN_equiv_class, zminus_congruent]) 1);
    5.69 -qed "zminus";
    5.70 -
    5.71 -(*Every integer can be written in the form Abs_Integ(...) *)
    5.72 -val [prem] = Goal "(!!x y. z = Abs_Integ(intrel``{(x,y)}) ==> P) ==> P";
    5.73 -by (res_inst_tac [("x1","z")] 
    5.74 -    (rewrite_rule [Integ_def] Rep_Integ RS quotientE) 1);
    5.75 -by (dres_inst_tac [("f","Abs_Integ")] arg_cong 1);
    5.76 -by (res_inst_tac [("p","x")] PairE 1);
    5.77 -by (rtac prem 1);
    5.78 -by (asm_full_simp_tac (simpset() addsimps [Rep_Integ_inverse]) 1);
    5.79 -qed "eq_Abs_Integ";
    5.80 -
    5.81 -Goal "- (- z) = (z::int)";
    5.82 -by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
    5.83 -by (asm_simp_tac (simpset() addsimps [zminus]) 1);
    5.84 -qed "zminus_zminus";
    5.85 -Addsimps [zminus_zminus];
    5.86 -
    5.87 -Goal "inj(%z::int. -z)";
    5.88 -by (rtac injI 1);
    5.89 -by (dres_inst_tac [("f","uminus")] arg_cong 1);
    5.90 -by (Asm_full_simp_tac 1);
    5.91 -qed "inj_zminus";
    5.92 -
    5.93 -Goalw [int_def, Zero_int_def] "- 0 = (0::int)";
    5.94 -by (simp_tac (simpset() addsimps [zminus]) 1);
    5.95 -qed "zminus_0";
    5.96 -Addsimps [zminus_0];
    5.97 -
    5.98 -
    5.99 -(**** neg: the test for negative integers ****)
   5.100 -
   5.101 -
   5.102 -Goalw [neg_def, int_def] "~ neg(int n)";
   5.103 -by (Simp_tac 1);
   5.104 -qed "not_neg_int";
   5.105 -
   5.106 -Goalw [neg_def, int_def] "neg(- (int (Suc n)))";
   5.107 -by (simp_tac (simpset() addsimps [zminus]) 1);
   5.108 -qed "neg_zminus_int";
   5.109 -
   5.110 -Addsimps [neg_zminus_int, not_neg_int]; 
   5.111 -
   5.112 -
   5.113 -(**** zadd: addition on Integ ****)
   5.114 -
   5.115 -Goalw [zadd_def]
   5.116 -  "Abs_Integ(intrel``{(x1,y1)}) + Abs_Integ(intrel``{(x2,y2)}) = \
   5.117 -\  Abs_Integ(intrel``{(x1+x2, y1+y2)})";
   5.118 -by (asm_simp_tac (simpset() addsimps [UN_UN_split_split_eq]) 1);
   5.119 -by (stac (equiv_intrel RS UN_equiv_class2) 1);
   5.120 -by (auto_tac (claset(), simpset() addsimps [congruent2_def]));
   5.121 -qed "zadd";
   5.122 -
   5.123 -Goal "- (z + w) = (- z) + (- w::int)";
   5.124 -by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
   5.125 -by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
   5.126 -by (asm_simp_tac (simpset() addsimps [zminus,zadd]) 1);
   5.127 -qed "zminus_zadd_distrib";
   5.128 -Addsimps [zminus_zadd_distrib];
   5.129 -
   5.130 -Goal "(z::int) + w = w + z";
   5.131 -by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
   5.132 -by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
   5.133 -by (asm_simp_tac (simpset() addsimps add_ac @ [zadd]) 1);
   5.134 -qed "zadd_commute";
   5.135 -
   5.136 -Goal "((z1::int) + z2) + z3 = z1 + (z2 + z3)";
   5.137 -by (res_inst_tac [("z","z1")] eq_Abs_Integ 1);
   5.138 -by (res_inst_tac [("z","z2")] eq_Abs_Integ 1);
   5.139 -by (res_inst_tac [("z","z3")] eq_Abs_Integ 1);
   5.140 -by (asm_simp_tac (simpset() addsimps [zadd, add_assoc]) 1);
   5.141 -qed "zadd_assoc";
   5.142 -
   5.143 -(*For AC rewriting*)
   5.144 -Goal "(x::int)+(y+z)=y+(x+z)";
   5.145 -by(rtac ([zadd_assoc,zadd_commute] MRS
   5.146 -         read_instantiate[("f","op +")](thm"mk_left_commute")) 1);
   5.147 -qed "zadd_left_commute";
   5.148 -
   5.149 -(*Integer addition is an AC operator*)
   5.150 -bind_thms ("zadd_ac", [zadd_assoc,zadd_commute,zadd_left_commute]);
   5.151 -
   5.152 -Goalw [int_def] "(int m) + (int n) = int (m + n)";
   5.153 -by (simp_tac (simpset() addsimps [zadd]) 1);
   5.154 -qed "zadd_int";
   5.155 -
   5.156 -Goal "(int m) + (int n + z) = int (m + n) + z";
   5.157 -by (simp_tac (simpset() addsimps [zadd_int, zadd_assoc RS sym]) 1);
   5.158 -qed "zadd_int_left";
   5.159 -
   5.160 -Goal "int (Suc m) = 1 + (int m)";
   5.161 -by (simp_tac (simpset() addsimps [One_int_def, zadd_int]) 1);
   5.162 -qed "int_Suc";
   5.163 -
   5.164 -(*also for the instance declaration int :: plus_ac0*)
   5.165 -Goalw [Zero_int_def, int_def] "(0::int) + z = z";
   5.166 -by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
   5.167 -by (asm_simp_tac (simpset() addsimps [zadd]) 1);
   5.168 -qed "zadd_0";
   5.169 -Addsimps [zadd_0];
   5.170 -
   5.171 -Goal "z + (0::int) = z";
   5.172 -by (rtac ([zadd_commute, zadd_0] MRS trans) 1);
   5.173 -qed "zadd_0_right";
   5.174 -Addsimps [zadd_0_right];
   5.175 -
   5.176 -Goalw [int_def, Zero_int_def] "z + (- z) = (0::int)";
   5.177 -by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
   5.178 -by (asm_simp_tac (simpset() addsimps [zminus, zadd, add_commute]) 1);
   5.179 -qed "zadd_zminus_inverse";
   5.180 -
   5.181 -Goal "(- z) + z = (0::int)";
   5.182 -by (rtac (zadd_commute RS trans) 1);
   5.183 -by (rtac zadd_zminus_inverse 1);
   5.184 -qed "zadd_zminus_inverse2";
   5.185 -
   5.186 -Addsimps [zadd_zminus_inverse, zadd_zminus_inverse2];
   5.187 -
   5.188 -Goal "z + (- z + w) = (w::int)";
   5.189 -by (simp_tac (simpset() addsimps [zadd_assoc RS sym, zadd_0]) 1);
   5.190 -qed "zadd_zminus_cancel";
   5.191 -
   5.192 -Goal "(-z) + (z + w) = (w::int)";
   5.193 -by (simp_tac (simpset() addsimps [zadd_assoc RS sym, zadd_0]) 1);
   5.194 -qed "zminus_zadd_cancel";
   5.195 -
   5.196 -Addsimps [zadd_zminus_cancel, zminus_zadd_cancel];
   5.197 -
   5.198 -Goal "(0::int) - x = -x";
   5.199 -by (simp_tac (simpset() addsimps [zdiff_def]) 1);
   5.200 -qed "zdiff0";
   5.201 -
   5.202 -Goal "x - (0::int) = x";
   5.203 -by (simp_tac (simpset() addsimps [zdiff_def]) 1);
   5.204 -qed "zdiff0_right";
   5.205 -
   5.206 -Goal "x - x = (0::int)";
   5.207 -by (simp_tac (simpset() addsimps [zdiff_def, Zero_int_def]) 1);
   5.208 -qed "zdiff_self";
   5.209 -
   5.210 -Addsimps [zdiff0, zdiff0_right, zdiff_self];
   5.211 -
   5.212 -
   5.213 -(** Lemmas **)
   5.214 -
   5.215 -Goal "(z::int) + v = z' + v' ==> z + (v + w) = z' + (v' + w)";
   5.216 -by (asm_simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1);
   5.217 -qed "zadd_assoc_cong";
   5.218 -
   5.219 -Goal "(z::int) + (v + w) = v + (z + w)";
   5.220 -by (REPEAT (ares_tac [zadd_commute RS zadd_assoc_cong] 1));
   5.221 -qed "zadd_assoc_swap";
   5.222 -
   5.223 -
   5.224 -(**** zmult: multiplication on Integ ****)
   5.225 -
   5.226 -(*Congruence property for multiplication*)
   5.227 -Goal "congruent2 intrel \
   5.228 -\       (%p1 p2. (%(x1,y1). (%(x2,y2).   \
   5.229 -\                   intrel``{(x1*x2 + y1*y2, x1*y2 + y1*x2)}) p2) p1)";
   5.230 -by (rtac (equiv_intrel RS congruent2_commuteI) 1);
   5.231 -by (pair_tac "w" 2);
   5.232 -by (ALLGOALS Clarify_tac);
   5.233 -by (simp_tac (simpset() addsimps add_ac@mult_ac) 1);
   5.234 -by (asm_simp_tac (simpset() delsimps [equiv_intrel_iff]
   5.235 -                            addsimps add_ac@mult_ac) 1);
   5.236 -by (rename_tac "x1 x2 y1 y2 z1 z2" 1);
   5.237 -by (rtac ([equiv_intrel, intrel_iff RS iffD2] MRS equiv_class_eq) 1);
   5.238 -by (asm_full_simp_tac (simpset() addsimps [intrel_def]) 1);
   5.239 -by (subgoal_tac 
   5.240 -    "x1*z1 + y2*z1 = y1*z1 + x2*z1 & x1*z2 + y2*z2 = y1*z2 + x2*z2" 1);
   5.241 -by (asm_simp_tac (simpset() addsimps [add_mult_distrib RS sym]) 2);
   5.242 -by (arith_tac 1);
   5.243 -qed "zmult_congruent2";
   5.244 -
   5.245 -Goalw [zmult_def]
   5.246 -   "Abs_Integ((intrel``{(x1,y1)})) * Abs_Integ((intrel``{(x2,y2)})) =   \
   5.247 -\   Abs_Integ(intrel `` {(x1*x2 + y1*y2, x1*y2 + y1*x2)})";
   5.248 -by (asm_simp_tac
   5.249 -    (simpset() addsimps [UN_UN_split_split_eq, zmult_congruent2,
   5.250 -			 equiv_intrel RS UN_equiv_class2]) 1);
   5.251 -qed "zmult";
   5.252 -
   5.253 -Goal "(- z) * w = - (z * (w::int))";
   5.254 -by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
   5.255 -by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
   5.256 -by (asm_simp_tac (simpset() addsimps [zminus, zmult] @ add_ac) 1);
   5.257 -qed "zmult_zminus";
   5.258 -
   5.259 -Goal "(z::int) * w = w * z";
   5.260 -by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
   5.261 -by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
   5.262 -by (asm_simp_tac (simpset() addsimps [zmult] @ add_ac @ mult_ac) 1);
   5.263 -qed "zmult_commute";
   5.264 -
   5.265 -Goal "((z1::int) * z2) * z3 = z1 * (z2 * z3)";
   5.266 -by (res_inst_tac [("z","z1")] eq_Abs_Integ 1);
   5.267 -by (res_inst_tac [("z","z2")] eq_Abs_Integ 1);
   5.268 -by (res_inst_tac [("z","z3")] eq_Abs_Integ 1);
   5.269 -by (asm_simp_tac (simpset() addsimps [add_mult_distrib2,zmult] @ 
   5.270 -                                     add_ac @ mult_ac) 1);
   5.271 -qed "zmult_assoc";
   5.272 -
   5.273 -(*For AC rewriting*)
   5.274 -Goal "(z1::int)*(z2*z3) = z2*(z1*z3)";
   5.275 -by(rtac ([zmult_assoc,zmult_commute] MRS
   5.276 -         read_instantiate[("f","op *")](thm"mk_left_commute")) 1);
   5.277 -qed "zmult_left_commute";
   5.278 -
   5.279 -(*Integer multiplication is an AC operator*)
   5.280 -bind_thms ("zmult_ac", [zmult_assoc, zmult_commute, zmult_left_commute]);
   5.281 -
   5.282 -Goal "((z1::int) + z2) * w = (z1 * w) + (z2 * w)";
   5.283 -by (res_inst_tac [("z","z1")] eq_Abs_Integ 1);
   5.284 -by (res_inst_tac [("z","z2")] eq_Abs_Integ 1);
   5.285 -by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
   5.286 -by (asm_simp_tac 
   5.287 -    (simpset() addsimps [add_mult_distrib2, zadd, zmult] @ 
   5.288 -                        add_ac @ mult_ac) 1);
   5.289 -qed "zadd_zmult_distrib";
   5.290 -
   5.291 -val zmult_commute'= inst "z" "w" zmult_commute;
   5.292 -
   5.293 -Goal "w * (- z) = - (w * (z::int))";
   5.294 -by (simp_tac (simpset() addsimps [zmult_commute', zmult_zminus]) 1);
   5.295 -qed "zmult_zminus_right";
   5.296 -
   5.297 -Goal "(w::int) * (z1 + z2) = (w * z1) + (w * z2)";
   5.298 -by (simp_tac (simpset() addsimps [zmult_commute',zadd_zmult_distrib]) 1);
   5.299 -qed "zadd_zmult_distrib2";
   5.300 -
   5.301 -Goalw [zdiff_def] "((z1::int) - z2) * w = (z1 * w) - (z2 * w)";
   5.302 -by (stac zadd_zmult_distrib 1);
   5.303 -by (simp_tac (simpset() addsimps [zmult_zminus]) 1);
   5.304 -qed "zdiff_zmult_distrib";
   5.305 -
   5.306 -Goal "(w::int) * (z1 - z2) = (w * z1) - (w * z2)";
   5.307 -by (simp_tac (simpset() addsimps [zmult_commute',zdiff_zmult_distrib]) 1);
   5.308 -qed "zdiff_zmult_distrib2";
   5.309 -
   5.310 -bind_thms ("int_distrib",
   5.311 -  [zadd_zmult_distrib, zadd_zmult_distrib2, zdiff_zmult_distrib, zdiff_zmult_distrib2]);
   5.312 -
   5.313 -Goalw [int_def] "(int m) * (int n) = int (m * n)";
   5.314 -by (simp_tac (simpset() addsimps [zmult]) 1);
   5.315 -qed "zmult_int";
   5.316 -
   5.317 -Goalw [Zero_int_def, int_def] "0 * z = (0::int)";
   5.318 -by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
   5.319 -by (asm_simp_tac (simpset() addsimps [zmult]) 1);
   5.320 -qed "zmult_0";
   5.321 -Addsimps [zmult_0];
   5.322 -
   5.323 -Goalw [One_int_def, int_def] "(1::int) * z = z";
   5.324 -by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
   5.325 -by (asm_simp_tac (simpset() addsimps [zmult]) 1);
   5.326 -qed "zmult_1";
   5.327 -Addsimps [zmult_1];
   5.328 -
   5.329 -Goal "z * 0 = (0::int)";
   5.330 -by (rtac ([zmult_commute, zmult_0] MRS trans) 1);
   5.331 -qed "zmult_0_right";
   5.332 -Addsimps [zmult_0_right];
   5.333 -
   5.334 -Goal "z * (1::int) = z";
   5.335 -by (rtac ([zmult_commute, zmult_1] MRS trans) 1);
   5.336 -qed "zmult_1_right";
   5.337 -Addsimps [zmult_1_right];
   5.338 -
   5.339 -
   5.340 -(* Theorems about less and less_equal *)
   5.341 -
   5.342 -(*This lemma allows direct proofs of other <-properties*)
   5.343 -Goalw [zless_def, neg_def, zdiff_def, int_def] 
   5.344 -    "(w < z) = (EX n. z = w + int(Suc n))";
   5.345 -by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
   5.346 -by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
   5.347 -by (Clarify_tac 1);
   5.348 -by (asm_full_simp_tac (simpset() addsimps [zadd, zminus]) 1);
   5.349 -by (safe_tac (claset() addSDs [less_imp_Suc_add]));
   5.350 -by (res_inst_tac [("x","k")] exI 1);
   5.351 -by (ALLGOALS (asm_full_simp_tac (simpset() addsimps add_ac)));
   5.352 -qed "zless_iff_Suc_zadd";
   5.353 -
   5.354 -Goal "z < z + int (Suc n)";
   5.355 -by (auto_tac (claset(),
   5.356 -	      simpset() addsimps [zless_iff_Suc_zadd, zadd_assoc, 
   5.357 -				  zadd_int]));
   5.358 -qed "zless_zadd_Suc";
   5.359 -
   5.360 -Goal "[| z1<z2; z2<z3 |] ==> z1 < (z3::int)";
   5.361 -by (auto_tac (claset(),
   5.362 -	      simpset() addsimps [zless_iff_Suc_zadd, zadd_assoc, 
   5.363 -				  zadd_int]));
   5.364 -qed "zless_trans";
   5.365 -
   5.366 -Goal "!!w::int. z<w ==> ~w<z";
   5.367 -by (safe_tac (claset() addSDs [zless_iff_Suc_zadd RS iffD1]));
   5.368 -by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
   5.369 -by Safe_tac;
   5.370 -by (asm_full_simp_tac (simpset() addsimps [int_def, zadd]) 1);
   5.371 -qed "zless_not_sym";
   5.372 -
   5.373 -(* [| n<m;  ~P ==> m<n |] ==> P *)
   5.374 -bind_thm ("zless_asym", zless_not_sym RS swap);
   5.375 -
   5.376 -Goal "!!z::int. ~ z<z";
   5.377 -by (resolve_tac [zless_asym RS notI] 1);
   5.378 -by (REPEAT (assume_tac 1));
   5.379 -qed "zless_not_refl";
   5.380 -
   5.381 -(* z<z ==> R *)
   5.382 -bind_thm ("zless_irrefl", zless_not_refl RS notE);
   5.383 -AddSEs [zless_irrefl];
   5.384 -
   5.385 -
   5.386 -(*"Less than" is a linear ordering*)
   5.387 -Goalw [zless_def, neg_def, zdiff_def] 
   5.388 -    "z<w | z=w | w<(z::int)";
   5.389 -by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
   5.390 -by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
   5.391 -by Safe_tac;
   5.392 -by (asm_full_simp_tac
   5.393 -    (simpset() addsimps [zadd, zminus, Image_iff, Bex_def]) 1);
   5.394 -by (res_inst_tac [("m1", "x+ya"), ("n1", "xa+y")] (less_linear RS disjE) 1);
   5.395 -by (ALLGOALS (force_tac (claset(), simpset() addsimps add_ac)));
   5.396 -qed "zless_linear";
   5.397 -
   5.398 -Goal "!!w::int. (w ~= z) = (w<z | z<w)";
   5.399 -by (cut_facts_tac [zless_linear] 1);
   5.400 -by (Blast_tac 1);
   5.401 -qed "int_neq_iff";
   5.402 -
   5.403 -(*** eliminates ~= in premises ***)
   5.404 -bind_thm("int_neqE", int_neq_iff RS iffD1 RS disjE);
   5.405 -
   5.406 -Goal "(int m = int n) = (m = n)"; 
   5.407 -by (fast_tac (claset() addSEs [inj_int RS injD]) 1); 
   5.408 -qed "int_int_eq"; 
   5.409 -AddIffs [int_int_eq]; 
   5.410 -
   5.411 -Goal "(int n = 0) = (n = 0)";
   5.412 -by (simp_tac (simpset() addsimps [Zero_int_def]) 1);
   5.413 -qed "int_eq_0_conv";
   5.414 -Addsimps [int_eq_0_conv];
   5.415 -
   5.416 -Goal "(int m < int n) = (m<n)";
   5.417 -by (simp_tac (simpset() addsimps [less_iff_Suc_add, zless_iff_Suc_zadd, 
   5.418 -				  zadd_int]) 1);
   5.419 -qed "zless_int";
   5.420 -Addsimps [zless_int];
   5.421 -
   5.422 -Goal "~ (int k < 0)";
   5.423 -by (simp_tac (simpset() addsimps [Zero_int_def]) 1);
   5.424 -qed "int_less_0_conv";
   5.425 -Addsimps [int_less_0_conv];
   5.426 -
   5.427 -Goal "(0 < int n) = (0 < n)";
   5.428 -by (simp_tac (simpset() addsimps [Zero_int_def]) 1);
   5.429 -qed "zero_less_int_conv";
   5.430 -Addsimps [zero_less_int_conv];
   5.431 -
   5.432 -
   5.433 -(*** Properties of <= ***)
   5.434 -
   5.435 -Goalw [zle_def, le_def] "(int m <= int n) = (m<=n)";
   5.436 -by (Simp_tac 1);
   5.437 -qed "zle_int";
   5.438 -Addsimps [zle_int];
   5.439 -
   5.440 -Goal "(0 <= int n)";
   5.441 -by (simp_tac (simpset() addsimps [Zero_int_def]) 1);
   5.442 -qed "zero_zle_int";
   5.443 -Addsimps [zero_zle_int];
   5.444 -
   5.445 -Goal "(int n <= 0) = (n = 0)";
   5.446 -by (simp_tac (simpset() addsimps [Zero_int_def]) 1);
   5.447 -qed "int_le_0_conv";
   5.448 -Addsimps [int_le_0_conv];
   5.449 -
   5.450 -Goalw [zle_def] "z <= w ==> z < w | z=(w::int)";
   5.451 -by (cut_facts_tac [zless_linear] 1);
   5.452 -by (blast_tac (claset() addEs [zless_asym]) 1);
   5.453 -qed "zle_imp_zless_or_eq";
   5.454 -
   5.455 -Goalw [zle_def] "z<w | z=w ==> z <= (w::int)";
   5.456 -by (cut_facts_tac [zless_linear] 1);
   5.457 -by (blast_tac (claset() addEs [zless_asym]) 1);
   5.458 -qed "zless_or_eq_imp_zle";
   5.459 -
   5.460 -Goal "(x <= (y::int)) = (x < y | x=y)";
   5.461 -by (REPEAT(ares_tac [iffI, zless_or_eq_imp_zle, zle_imp_zless_or_eq] 1));
   5.462 -qed "int_le_less";
   5.463 -
   5.464 -Goal "w <= (w::int)";
   5.465 -by (simp_tac (simpset() addsimps [int_le_less]) 1);
   5.466 -qed "zle_refl";
   5.467 -
   5.468 -(* Axiom 'linorder_linear' of class 'linorder': *)
   5.469 -Goal "(z::int) <= w | w <= z";
   5.470 -by (simp_tac (simpset() addsimps [int_le_less]) 1);
   5.471 -by (cut_facts_tac [zless_linear] 1);
   5.472 -by (Blast_tac 1);
   5.473 -qed "zle_linear";
   5.474 -
   5.475 -(* Axiom 'order_trans of class 'order': *)
   5.476 -Goal "[| i <= j; j <= k |] ==> i <= (k::int)";
   5.477 -by (EVERY1 [dtac zle_imp_zless_or_eq, dtac zle_imp_zless_or_eq,
   5.478 -            rtac zless_or_eq_imp_zle, 
   5.479 -	    blast_tac (claset() addIs [zless_trans])]);
   5.480 -qed "zle_trans";
   5.481 -
   5.482 -Goal "[| z <= w; w <= z |] ==> z = (w::int)";
   5.483 -by (EVERY1 [dtac zle_imp_zless_or_eq, dtac zle_imp_zless_or_eq,
   5.484 -            blast_tac (claset() addEs [zless_asym])]);
   5.485 -qed "zle_anti_sym";
   5.486 -
   5.487 -(* Axiom 'order_less_le' of class 'order': *)
   5.488 -Goal "((w::int) < z) = (w <= z & w ~= z)";
   5.489 -by (simp_tac (simpset() addsimps [zle_def, int_neq_iff]) 1);
   5.490 -by (blast_tac (claset() addSEs [zless_asym]) 1);
   5.491 -qed "int_less_le";
   5.492 -
   5.493 -
   5.494 -(*** Subtraction laws ***)
   5.495 -
   5.496 -Goal "x + (y - z) = (x + y) - (z::int)";
   5.497 -by (simp_tac (simpset() addsimps zdiff_def::zadd_ac) 1);
   5.498 -qed "zadd_zdiff_eq";
   5.499 -
   5.500 -Goal "(x - y) + z = (x + z) - (y::int)";
   5.501 -by (simp_tac (simpset() addsimps zdiff_def::zadd_ac) 1);
   5.502 -qed "zdiff_zadd_eq";
   5.503 -
   5.504 -Goal "(x - y) - z = x - (y + (z::int))";
   5.505 -by (simp_tac (simpset() addsimps zdiff_def::zadd_ac) 1);
   5.506 -qed "zdiff_zdiff_eq";
   5.507 -
   5.508 -Goal "x - (y - z) = (x + z) - (y::int)";
   5.509 -by (simp_tac (simpset() addsimps zdiff_def::zadd_ac) 1);
   5.510 -qed "zdiff_zdiff_eq2";
   5.511 -
   5.512 -Goalw [zless_def, zdiff_def] "(x-y < z) = (x < z + (y::int))";
   5.513 -by (simp_tac (simpset() addsimps zadd_ac) 1);
   5.514 -qed "zdiff_zless_eq";
   5.515 -
   5.516 -Goalw [zless_def, zdiff_def] "(x < z-y) = (x + (y::int) < z)";
   5.517 -by (simp_tac (simpset() addsimps zadd_ac) 1);
   5.518 -qed "zless_zdiff_eq";
   5.519 -
   5.520 -Goalw [zle_def] "(x-y <= z) = (x <= z + (y::int))";
   5.521 -by (simp_tac (simpset() addsimps [zless_zdiff_eq]) 1);
   5.522 -qed "zdiff_zle_eq";
   5.523 -
   5.524 -Goalw [zle_def] "(x <= z-y) = (x + (y::int) <= z)";
   5.525 -by (simp_tac (simpset() addsimps [zdiff_zless_eq]) 1);
   5.526 -qed "zle_zdiff_eq";
   5.527 -
   5.528 -Goalw [zdiff_def] "(x-y = z) = (x = z + (y::int))";
   5.529 -by (auto_tac (claset(), 
   5.530 -              simpset() addsimps [zadd_assoc, symmetric Zero_int_def]));
   5.531 -qed "zdiff_eq_eq";
   5.532 -
   5.533 -Goalw [zdiff_def] "(x = z-y) = (x + (y::int) = z)";
   5.534 -by (auto_tac (claset(), 
   5.535 -              simpset() addsimps [zadd_assoc, symmetric Zero_int_def]));
   5.536 -qed "eq_zdiff_eq";
   5.537 -
   5.538 -(*This list of rewrites simplifies (in)equalities by bringing subtractions
   5.539 -  to the top and then moving negative terms to the other side.  
   5.540 -  Use with zadd_ac*)
   5.541 -bind_thms ("zcompare_rls",
   5.542 -    [symmetric zdiff_def,
   5.543 -     zadd_zdiff_eq, zdiff_zadd_eq, zdiff_zdiff_eq, zdiff_zdiff_eq2, 
   5.544 -     zdiff_zless_eq, zless_zdiff_eq, zdiff_zle_eq, zle_zdiff_eq, 
   5.545 -     zdiff_eq_eq, eq_zdiff_eq]);
   5.546 -
   5.547 -
   5.548 -(** Cancellation laws **)
   5.549 -
   5.550 -Goal "!!w::int. (z + w' = z + w) = (w' = w)";
   5.551 -by Safe_tac;
   5.552 -by (dres_inst_tac [("f", "%x. x + (-z)")] arg_cong 1);
   5.553 -by (asm_full_simp_tac (simpset() addsimps symmetric Zero_int_def :: 
   5.554 -                                          zadd_ac) 1);
   5.555 -qed "zadd_left_cancel";
   5.556 -
   5.557 -Addsimps [zadd_left_cancel];
   5.558 -
   5.559 -Goal "!!z::int. (w' + z = w + z) = (w' = w)";
   5.560 -by (asm_full_simp_tac (simpset() addsimps zadd_ac) 1);
   5.561 -qed "zadd_right_cancel";
   5.562 -
   5.563 -Addsimps [zadd_right_cancel];
   5.564 -
   5.565 -
   5.566 -(** For the cancellation simproc.
   5.567 -    The idea is to cancel like terms on opposite sides by subtraction **)
   5.568 -
   5.569 -Goal "(x::int) - y = x' - y' ==> (x<y) = (x'<y')";
   5.570 -by (asm_simp_tac (simpset() addsimps [zless_def]) 1);
   5.571 -qed "zless_eqI";
   5.572 -
   5.573 -Goal "(x::int) - y = x' - y' ==> (y<=x) = (y'<=x')";
   5.574 -by (dtac zless_eqI 1);
   5.575 -by (asm_simp_tac (simpset() addsimps [zle_def]) 1);
   5.576 -qed "zle_eqI";
   5.577 -
   5.578 -Goal "(x::int) - y = x' - y' ==> (x=y) = (x'=y')";
   5.579 -by Safe_tac;
   5.580 -by (ALLGOALS
   5.581 -    (asm_full_simp_tac (simpset() addsimps [eq_zdiff_eq, zdiff_eq_eq])));
   5.582 -qed "zeq_eqI";
   5.583 -
     6.1 --- a/src/HOL/Integ/IntDef.thy	Tue Nov 18 09:45:45 2003 +0100
     6.2 +++ b/src/HOL/Integ/IntDef.thy	Tue Nov 18 11:01:52 2003 +0100
     6.3 @@ -6,52 +6,652 @@
     6.4  The integers as equivalence classes over nat*nat.
     6.5  *)
     6.6  
     6.7 -IntDef = Equiv + NatArith + 
     6.8 +theory IntDef = Equiv + NatArith:
     6.9  constdefs
    6.10    intrel      :: "((nat * nat) * (nat * nat)) set"
    6.11    "intrel == {p. EX x1 y1 x2 y2. p=((x1::nat,y1),(x2,y2)) & x1+y2 = x2+y1}"
    6.12  
    6.13  typedef (Integ)
    6.14 -  int = "UNIV//intrel"            (quotient_def)
    6.15 +  int = "UNIV//intrel"
    6.16 +    by (auto simp add: quotient_def) 
    6.17  
    6.18 -instance
    6.19 -  int :: {ord, zero, one, plus, times, minus}
    6.20 +instance int :: ord ..
    6.21 +instance int :: zero ..
    6.22 +instance int :: one ..
    6.23 +instance int :: plus ..
    6.24 +instance int :: times ..
    6.25 +instance int :: minus ..
    6.26  
    6.27  defs
    6.28 -  zminus_def
    6.29 +  zminus_def:
    6.30      "- Z == Abs_Integ(UN (x,y):Rep_Integ(Z). intrel``{(y,x)})"
    6.31  
    6.32  constdefs
    6.33  
    6.34 -  int :: nat => int
    6.35 +  int :: "nat => int"
    6.36    "int m == Abs_Integ(intrel `` {(m,0)})"
    6.37  
    6.38 -  neg   :: int => bool
    6.39 +  neg   :: "int => bool"
    6.40    "neg(Z) == EX x y. x<y & (x,y::nat):Rep_Integ(Z)"
    6.41  
    6.42    (*For simplifying equalities*)
    6.43 -  iszero :: int => bool
    6.44 +  iszero :: "int => bool"
    6.45    "iszero z == z = (0::int)"
    6.46    
    6.47  defs (*of overloaded constants*)
    6.48    
    6.49 -  Zero_int_def "0 == int 0"
    6.50 -  One_int_def "1 == int 1"
    6.51 +  Zero_int_def:  "0 == int 0"
    6.52 +  One_int_def:  "1 == int 1"
    6.53  
    6.54 -  zadd_def
    6.55 +  zadd_def:
    6.56     "z + w == 
    6.57         Abs_Integ(UN (x1,y1):Rep_Integ(z). UN (x2,y2):Rep_Integ(w).   
    6.58  		 intrel``{(x1+x2, y1+y2)})"
    6.59  
    6.60 -  zdiff_def "z - (w::int) == z + (-w)"
    6.61 +  zdiff_def:  "z - (w::int) == z + (-w)"
    6.62  
    6.63 -  zless_def "z<w == neg(z - w)"
    6.64 +  zless_def:  "z<w == neg(z - w)"
    6.65  
    6.66 -  zle_def   "z <= (w::int) == ~(w < z)"
    6.67 +  zle_def:    "z <= (w::int) == ~(w < z)"
    6.68  
    6.69 -  zmult_def
    6.70 +  zmult_def:
    6.71     "z * w == 
    6.72         Abs_Integ(UN (x1,y1):Rep_Integ(z). UN (x2,y2):Rep_Integ(w).   
    6.73  		 intrel``{(x1*x2 + y1*y2, x1*y2 + y1*x2)})"
    6.74  
    6.75 +lemma intrel_iff [simp]: "(((x1,y1),(x2,y2)): intrel) = (x1+y2 = x2+y1)"
    6.76 +by (unfold intrel_def, blast)
    6.77 +
    6.78 +lemma equiv_intrel: "equiv UNIV intrel"
    6.79 +by (unfold intrel_def equiv_def refl_def sym_def trans_def, auto)
    6.80 +
    6.81 +lemmas equiv_intrel_iff =
    6.82 +       eq_equiv_class_iff [OF equiv_intrel UNIV_I UNIV_I, simp]
    6.83 +
    6.84 +lemma intrel_in_integ [simp]: "intrel``{(x,y)}:Integ"
    6.85 +by (unfold Integ_def intrel_def quotient_def, fast)
    6.86 +
    6.87 +lemma inj_on_Abs_Integ: "inj_on Abs_Integ Integ"
    6.88 +apply (rule inj_on_inverseI)
    6.89 +apply (erule Abs_Integ_inverse)
    6.90 +done
    6.91 +
    6.92 +declare inj_on_Abs_Integ [THEN inj_on_iff, simp] 
    6.93 +        Abs_Integ_inverse [simp]
    6.94 +
    6.95 +lemma inj_Rep_Integ: "inj(Rep_Integ)"
    6.96 +apply (rule inj_on_inverseI)
    6.97 +apply (rule Rep_Integ_inverse)
    6.98 +done
    6.99 +
   6.100 +
   6.101 +(** int: the injection from "nat" to "int" **)
   6.102 +
   6.103 +lemma inj_int: "inj int"
   6.104 +apply (rule inj_onI)
   6.105 +apply (unfold int_def)
   6.106 +apply (drule inj_on_Abs_Integ [THEN inj_onD])
   6.107 +apply (rule intrel_in_integ)+
   6.108 +apply (drule eq_equiv_class)
   6.109 +apply (rule equiv_intrel, fast)
   6.110 +apply (simp add: intrel_def)
   6.111 +done
   6.112 +
   6.113 +
   6.114 +subsection{*zminus: unary negation on Integ*}
   6.115 +
   6.116 +lemma zminus_congruent: "congruent intrel (%(x,y). intrel``{(y,x)})"
   6.117 +apply (unfold congruent_def intrel_def)
   6.118 +apply (auto simp add: add_ac)
   6.119 +done
   6.120 +
   6.121 +lemma zminus: "- Abs_Integ(intrel``{(x,y)}) = Abs_Integ(intrel `` {(y,x)})"
   6.122 +by (simp add: zminus_def equiv_intrel [THEN UN_equiv_class] zminus_congruent)
   6.123 +
   6.124 +(*Every integer can be written in the form Abs_Integ(...) *)
   6.125 +lemma eq_Abs_Integ: 
   6.126 +     "(!!x y. z = Abs_Integ(intrel``{(x,y)}) ==> P) ==> P"
   6.127 +apply (rule_tac x1=z in Rep_Integ [unfolded Integ_def, THEN quotientE]) 
   6.128 +apply (drule_tac f = Abs_Integ in arg_cong)
   6.129 +apply (rule_tac p = x in PairE)
   6.130 +apply (simp add: Rep_Integ_inverse)
   6.131 +done
   6.132 +
   6.133 +lemma zminus_zminus [simp]: "- (- z) = (z::int)"
   6.134 +apply (rule_tac z = z in eq_Abs_Integ)
   6.135 +apply (simp (no_asm_simp) add: zminus)
   6.136 +done
   6.137 +
   6.138 +lemma inj_zminus: "inj(%z::int. -z)"
   6.139 +apply (rule inj_onI)
   6.140 +apply (drule_tac f = uminus in arg_cong, simp)
   6.141 +done
   6.142 +
   6.143 +lemma zminus_0 [simp]: "- 0 = (0::int)"
   6.144 +by (simp add: int_def Zero_int_def zminus)
   6.145 +
   6.146 +
   6.147 +subsection{*neg: the test for negative integers*}
   6.148 +
   6.149 +
   6.150 +lemma not_neg_int [simp]: "~ neg(int n)"
   6.151 +by (simp add: neg_def int_def)
   6.152 +
   6.153 +lemma neg_zminus_int [simp]: "neg(- (int (Suc n)))"
   6.154 +by (simp add: neg_def int_def zminus)
   6.155 +
   6.156 +
   6.157 +subsection{*zadd: addition on Integ*}
   6.158 +
   6.159 +lemma zadd: 
   6.160 +  "Abs_Integ(intrel``{(x1,y1)}) + Abs_Integ(intrel``{(x2,y2)}) =  
   6.161 +   Abs_Integ(intrel``{(x1+x2, y1+y2)})"
   6.162 +apply (simp add: zadd_def UN_UN_split_split_eq)
   6.163 +apply (subst equiv_intrel [THEN UN_equiv_class2])
   6.164 +apply (auto simp add: congruent2_def)
   6.165 +done
   6.166 +
   6.167 +lemma zminus_zadd_distrib [simp]: "- (z + w) = (- z) + (- w::int)"
   6.168 +apply (rule_tac z = z in eq_Abs_Integ)
   6.169 +apply (rule_tac z = w in eq_Abs_Integ)
   6.170 +apply (simp (no_asm_simp) add: zminus zadd)
   6.171 +done
   6.172 +
   6.173 +lemma zadd_commute: "(z::int) + w = w + z"
   6.174 +apply (rule_tac z = z in eq_Abs_Integ)
   6.175 +apply (rule_tac z = w in eq_Abs_Integ)
   6.176 +apply (simp (no_asm_simp) add: add_ac zadd)
   6.177 +done
   6.178 +
   6.179 +lemma zadd_assoc: "((z1::int) + z2) + z3 = z1 + (z2 + z3)"
   6.180 +apply (rule_tac z = z1 in eq_Abs_Integ)
   6.181 +apply (rule_tac z = z2 in eq_Abs_Integ)
   6.182 +apply (rule_tac z = z3 in eq_Abs_Integ)
   6.183 +apply (simp (no_asm_simp) add: zadd add_assoc)
   6.184 +done
   6.185 +
   6.186 +(*For AC rewriting*)
   6.187 +lemma zadd_left_commute: "x + (y + z) = y + ((x + z)::int)"
   6.188 +  apply (rule mk_left_commute [of "op +"])
   6.189 +  apply (rule zadd_assoc)
   6.190 +  apply (rule zadd_commute)
   6.191 +  done
   6.192 +
   6.193 +(*Integer addition is an AC operator*)
   6.194 +lemmas zadd_ac = zadd_assoc zadd_commute zadd_left_commute
   6.195 +
   6.196 +lemma zadd_int: "(int m) + (int n) = int (m + n)"
   6.197 +by (simp add: int_def zadd)
   6.198 +
   6.199 +lemma zadd_int_left: "(int m) + (int n + z) = int (m + n) + z"
   6.200 +by (simp add: zadd_int zadd_assoc [symmetric])
   6.201 +
   6.202 +lemma int_Suc: "int (Suc m) = 1 + (int m)"
   6.203 +by (simp add: One_int_def zadd_int)
   6.204 +
   6.205 +(*also for the instance declaration int :: plus_ac0*)
   6.206 +lemma zadd_0 [simp]: "(0::int) + z = z"
   6.207 +apply (unfold Zero_int_def int_def)
   6.208 +apply (rule_tac z = z in eq_Abs_Integ)
   6.209 +apply (simp (no_asm_simp) add: zadd)
   6.210 +done
   6.211 +
   6.212 +lemma zadd_0_right [simp]: "z + (0::int) = z"
   6.213 +by (rule trans [OF zadd_commute zadd_0])
   6.214 +
   6.215 +lemma zadd_zminus_inverse [simp]: "z + (- z) = (0::int)"
   6.216 +apply (unfold int_def Zero_int_def)
   6.217 +apply (rule_tac z = z in eq_Abs_Integ)
   6.218 +apply (simp (no_asm_simp) add: zminus zadd add_commute)
   6.219 +done
   6.220 +
   6.221 +lemma zadd_zminus_inverse2 [simp]: "(- z) + z = (0::int)"
   6.222 +apply (rule zadd_commute [THEN trans])
   6.223 +apply (rule zadd_zminus_inverse)
   6.224 +done
   6.225 +
   6.226 +lemma zadd_zminus_cancel [simp]: "z + (- z + w) = (w::int)"
   6.227 +by (simp add: zadd_assoc [symmetric] zadd_0)
   6.228 +
   6.229 +lemma zminus_zadd_cancel [simp]: "(-z) + (z + w) = (w::int)"
   6.230 +by (simp add: zadd_assoc [symmetric] zadd_0)
   6.231 +
   6.232 +lemma zdiff0 [simp]: "(0::int) - x = -x"
   6.233 +by (simp add: zdiff_def)
   6.234 +
   6.235 +lemma zdiff0_right [simp]: "x - (0::int) = x"
   6.236 +by (simp add: zdiff_def)
   6.237 +
   6.238 +lemma zdiff_self [simp]: "x - x = (0::int)"
   6.239 +by (simp add: zdiff_def Zero_int_def)
   6.240 +
   6.241 +
   6.242 +(** Lemmas **)
   6.243 +
   6.244 +lemma zadd_assoc_cong: "(z::int) + v = z' + v' ==> z + (v + w) = z' + (v' + w)"
   6.245 +by (simp add: zadd_assoc [symmetric])
   6.246 +
   6.247 +lemma zadd_assoc_swap: "(z::int) + (v + w) = v + (z + w)"
   6.248 +by (rule zadd_commute [THEN zadd_assoc_cong])
   6.249 +
   6.250 +
   6.251 +subsection{*zmult: multiplication on Integ*}
   6.252 +
   6.253 +(*Congruence property for multiplication*)
   6.254 +lemma zmult_congruent2: "congruent2 intrel  
   6.255 +        (%p1 p2. (%(x1,y1). (%(x2,y2).    
   6.256 +                    intrel``{(x1*x2 + y1*y2, x1*y2 + y1*x2)}) p2) p1)"
   6.257 +apply (rule equiv_intrel [THEN congruent2_commuteI])
   6.258 +apply (rule_tac [2] p=w in PairE)  
   6.259 +apply (force simp add: add_ac mult_ac, clarify) 
   6.260 +apply (simp (no_asm_simp) del: equiv_intrel_iff add: add_ac mult_ac)
   6.261 +apply (rename_tac x1 x2 y1 y2 z1 z2)
   6.262 +apply (rule equiv_class_eq [OF equiv_intrel intrel_iff [THEN iffD2]])
   6.263 +apply (simp add: intrel_def)
   6.264 +apply (subgoal_tac "x1*z1 + y2*z1 = y1*z1 + x2*z1 & x1*z2 + y2*z2 = y1*z2 + x2*z2", arith)
   6.265 +apply (simp add: add_mult_distrib [symmetric])
   6.266 +done
   6.267 +
   6.268 +lemma zmult: 
   6.269 +   "Abs_Integ((intrel``{(x1,y1)})) * Abs_Integ((intrel``{(x2,y2)})) =    
   6.270 +    Abs_Integ(intrel `` {(x1*x2 + y1*y2, x1*y2 + y1*x2)})"
   6.271 +apply (unfold zmult_def)
   6.272 +apply (simp (no_asm_simp) add: UN_UN_split_split_eq zmult_congruent2 equiv_intrel [THEN UN_equiv_class2])
   6.273 +done
   6.274 +
   6.275 +lemma zmult_zminus: "(- z) * w = - (z * (w::int))"
   6.276 +apply (rule_tac z = z in eq_Abs_Integ)
   6.277 +apply (rule_tac z = w in eq_Abs_Integ)
   6.278 +apply (simp (no_asm_simp) add: zminus zmult add_ac)
   6.279 +done
   6.280 +
   6.281 +lemma zmult_commute: "(z::int) * w = w * z"
   6.282 +apply (rule_tac z = z in eq_Abs_Integ)
   6.283 +apply (rule_tac z = w in eq_Abs_Integ)
   6.284 +apply (simp (no_asm_simp) add: zmult add_ac mult_ac)
   6.285 +done
   6.286 +
   6.287 +lemma zmult_assoc: "((z1::int) * z2) * z3 = z1 * (z2 * z3)"
   6.288 +apply (rule_tac z = z1 in eq_Abs_Integ)
   6.289 +apply (rule_tac z = z2 in eq_Abs_Integ)
   6.290 +apply (rule_tac z = z3 in eq_Abs_Integ)
   6.291 +apply (simp (no_asm_simp) add: add_mult_distrib2 zmult add_ac mult_ac)
   6.292 +done
   6.293 +
   6.294 +(*For AC rewriting*)
   6.295 +lemma zmult_left_commute: "x * (y * z) = y * ((x * z)::int)"
   6.296 +  apply (rule mk_left_commute [of "op *"])
   6.297 +  apply (rule zmult_assoc)
   6.298 +  apply (rule zmult_commute)
   6.299 +  done
   6.300 +
   6.301 +(*Integer multiplication is an AC operator*)
   6.302 +lemmas zmult_ac = zmult_assoc zmult_commute zmult_left_commute
   6.303 +
   6.304 +lemma zadd_zmult_distrib: "((z1::int) + z2) * w = (z1 * w) + (z2 * w)"
   6.305 +apply (rule_tac z = z1 in eq_Abs_Integ)
   6.306 +apply (rule_tac z = z2 in eq_Abs_Integ)
   6.307 +apply (rule_tac z = w in eq_Abs_Integ)
   6.308 +apply (simp add: add_mult_distrib2 zadd zmult add_ac mult_ac)
   6.309 +done
   6.310 +
   6.311 +lemma zmult_zminus_right: "w * (- z) = - (w * (z::int))"
   6.312 +by (simp add: zmult_commute [of w] zmult_zminus)
   6.313 +
   6.314 +lemma zadd_zmult_distrib2: "(w::int) * (z1 + z2) = (w * z1) + (w * z2)"
   6.315 +by (simp add: zmult_commute [of w] zadd_zmult_distrib)
   6.316 +
   6.317 +lemma zdiff_zmult_distrib: "((z1::int) - z2) * w = (z1 * w) - (z2 * w)"
   6.318 +apply (unfold zdiff_def)
   6.319 +apply (subst zadd_zmult_distrib)
   6.320 +apply (simp add: zmult_zminus)
   6.321 +done
   6.322 +
   6.323 +lemma zdiff_zmult_distrib2: "(w::int) * (z1 - z2) = (w * z1) - (w * z2)"
   6.324 +by (simp add: zmult_commute [of w] zdiff_zmult_distrib)
   6.325 +
   6.326 +lemmas int_distrib =
   6.327 +  zadd_zmult_distrib zadd_zmult_distrib2 
   6.328 +  zdiff_zmult_distrib zdiff_zmult_distrib2
   6.329 +
   6.330 +lemma zmult_int: "(int m) * (int n) = int (m * n)"
   6.331 +by (simp add: int_def zmult)
   6.332 +
   6.333 +lemma zmult_0 [simp]: "0 * z = (0::int)"
   6.334 +apply (unfold Zero_int_def int_def)
   6.335 +apply (rule_tac z = z in eq_Abs_Integ)
   6.336 +apply (simp (no_asm_simp) add: zmult)
   6.337 +done
   6.338 +
   6.339 +lemma zmult_1 [simp]: "(1::int) * z = z"
   6.340 +apply (unfold One_int_def int_def)
   6.341 +apply (rule_tac z = z in eq_Abs_Integ)
   6.342 +apply (simp (no_asm_simp) add: zmult)
   6.343 +done
   6.344 +
   6.345 +lemma zmult_0_right [simp]: "z * 0 = (0::int)"
   6.346 +by (rule trans [OF zmult_commute zmult_0])
   6.347 +
   6.348 +lemma zmult_1_right [simp]: "z * (1::int) = z"
   6.349 +by (rule trans [OF zmult_commute zmult_1])
   6.350 +
   6.351 +
   6.352 +(* Theorems about less and less_equal *)
   6.353 +
   6.354 +(*This lemma allows direct proofs of other <-properties*)
   6.355 +lemma zless_iff_Suc_zadd: 
   6.356 +    "(w < z) = (EX n. z = w + int(Suc n))"
   6.357 +apply (unfold zless_def neg_def zdiff_def int_def)
   6.358 +apply (rule_tac z = z in eq_Abs_Integ)
   6.359 +apply (rule_tac z = w in eq_Abs_Integ, clarify)
   6.360 +apply (simp add: zadd zminus)
   6.361 +apply (safe dest!: less_imp_Suc_add)
   6.362 +apply (rule_tac x = k in exI)
   6.363 +apply (simp_all add: add_ac)
   6.364 +done
   6.365 +
   6.366 +lemma zless_zadd_Suc: "z < z + int (Suc n)"
   6.367 +by (auto simp add: zless_iff_Suc_zadd zadd_assoc zadd_int)
   6.368 +
   6.369 +lemma zless_trans: "[| z1<z2; z2<z3 |] ==> z1 < (z3::int)"
   6.370 +by (auto simp add: zless_iff_Suc_zadd zadd_assoc zadd_int)
   6.371 +
   6.372 +lemma zless_not_sym: "!!w::int. z<w ==> ~w<z"
   6.373 +apply (safe dest!: zless_iff_Suc_zadd [THEN iffD1])
   6.374 +apply (rule_tac z = z in eq_Abs_Integ, safe)
   6.375 +apply (simp add: int_def zadd)
   6.376 +done
   6.377 +
   6.378 +(* [| n<m;  ~P ==> m<n |] ==> P *)
   6.379 +lemmas zless_asym = zless_not_sym [THEN swap, standard]
   6.380 +
   6.381 +lemma zless_not_refl: "!!z::int. ~ z<z"
   6.382 +apply (rule zless_asym [THEN notI])
   6.383 +apply (assumption+)
   6.384 +done
   6.385 +
   6.386 +(* z<z ==> R *)
   6.387 +lemmas zless_irrefl = zless_not_refl [THEN notE, standard, elim!]
   6.388 +
   6.389 +
   6.390 +(*"Less than" is a linear ordering*)
   6.391 +lemma zless_linear: 
   6.392 +    "z<w | z=w | w<(z::int)"
   6.393 +apply (unfold zless_def neg_def zdiff_def)
   6.394 +apply (rule_tac z = z in eq_Abs_Integ)
   6.395 +apply (rule_tac z = w in eq_Abs_Integ, safe)
   6.396 +apply (simp add: zadd zminus Image_iff Bex_def)
   6.397 +apply (rule_tac m1 = "x+ya" and n1 = "xa+y" in less_linear [THEN disjE])
   6.398 +apply (force simp add: add_ac)+
   6.399 +done
   6.400 +
   6.401 +lemma int_neq_iff: "!!w::int. (w ~= z) = (w<z | z<w)"
   6.402 +by (cut_tac zless_linear, blast)
   6.403 +
   6.404 +(*** eliminates ~= in premises ***)
   6.405 +lemmas int_neqE = int_neq_iff [THEN iffD1, THEN disjE, standard]
   6.406 +
   6.407 +lemma int_int_eq [iff]: "(int m = int n) = (m = n)"
   6.408 +by (fast elim!: inj_int [THEN injD])
   6.409 +
   6.410 +lemma int_eq_0_conv [simp]: "(int n = 0) = (n = 0)"
   6.411 +by (simp add: Zero_int_def)
   6.412 +
   6.413 +lemma zless_int [simp]: "(int m < int n) = (m<n)"
   6.414 +by (simp add: less_iff_Suc_add zless_iff_Suc_zadd zadd_int)
   6.415 +
   6.416 +lemma int_less_0_conv [simp]: "~ (int k < 0)"
   6.417 +by (simp add: Zero_int_def)
   6.418 +
   6.419 +lemma zero_less_int_conv [simp]: "(0 < int n) = (0 < n)"
   6.420 +by (simp add: Zero_int_def)
   6.421 +
   6.422 +
   6.423 +(*** Properties of <= ***)
   6.424 +
   6.425 +lemma zle_int [simp]: "(int m <= int n) = (m<=n)"
   6.426 +by (simp add: zle_def le_def)
   6.427 +
   6.428 +lemma zero_zle_int [simp]: "(0 <= int n)"
   6.429 +by (simp add: Zero_int_def)
   6.430 +
   6.431 +lemma int_le_0_conv [simp]: "(int n <= 0) = (n = 0)"
   6.432 +by (simp add: Zero_int_def)
   6.433 +
   6.434 +lemma zle_imp_zless_or_eq: "z <= w ==> z < w | z=(w::int)"
   6.435 +apply (unfold zle_def)
   6.436 +apply (cut_tac zless_linear)
   6.437 +apply (blast elim: zless_asym)
   6.438 +done
   6.439 +
   6.440 +lemma zless_or_eq_imp_zle: "z<w | z=w ==> z <= (w::int)"
   6.441 +apply (unfold zle_def)
   6.442 +apply (cut_tac zless_linear)
   6.443 +apply (blast elim: zless_asym)
   6.444 +done
   6.445 +
   6.446 +lemma int_le_less: "(x <= (y::int)) = (x < y | x=y)"
   6.447 +apply (rule iffI) 
   6.448 +apply (erule zle_imp_zless_or_eq) 
   6.449 +apply (erule zless_or_eq_imp_zle) 
   6.450 +done
   6.451 +
   6.452 +lemma zle_refl: "w <= (w::int)"
   6.453 +by (simp add: int_le_less)
   6.454 +
   6.455 +(* Axiom 'linorder_linear' of class 'linorder': *)
   6.456 +lemma zle_linear: "(z::int) <= w | w <= z"
   6.457 +apply (simp add: int_le_less)
   6.458 +apply (cut_tac zless_linear, blast)
   6.459 +done
   6.460 +
   6.461 +(* Axiom 'order_trans of class 'order': *)
   6.462 +lemma zle_trans: "[| i <= j; j <= k |] ==> i <= (k::int)"
   6.463 +apply (drule zle_imp_zless_or_eq) 
   6.464 +apply (drule zle_imp_zless_or_eq) 
   6.465 +apply (rule zless_or_eq_imp_zle) 
   6.466 +apply (blast intro: zless_trans) 
   6.467 +done
   6.468 +
   6.469 +lemma zle_anti_sym: "[| z <= w; w <= z |] ==> z = (w::int)"
   6.470 +apply (drule zle_imp_zless_or_eq) 
   6.471 +apply (drule zle_imp_zless_or_eq) 
   6.472 +apply (blast elim: zless_asym) 
   6.473 +done
   6.474 +
   6.475 +(* Axiom 'order_less_le' of class 'order': *)
   6.476 +lemma int_less_le: "((w::int) < z) = (w <= z & w ~= z)"
   6.477 +apply (simp add: zle_def int_neq_iff)
   6.478 +apply (blast elim!: zless_asym)
   6.479 +done
   6.480 +
   6.481 +
   6.482 +(*** Subtraction laws ***)
   6.483 +
   6.484 +lemma zadd_zdiff_eq: "x + (y - z) = (x + y) - (z::int)"
   6.485 +by (simp add: zdiff_def zadd_ac)
   6.486 +
   6.487 +lemma zdiff_zadd_eq: "(x - y) + z = (x + z) - (y::int)"
   6.488 +by (simp add: zdiff_def zadd_ac)
   6.489 +
   6.490 +lemma zdiff_zdiff_eq: "(x - y) - z = x - (y + (z::int))"
   6.491 +by (simp add: zdiff_def zadd_ac)
   6.492 +
   6.493 +lemma zdiff_zdiff_eq2: "x - (y - z) = (x + z) - (y::int)"
   6.494 +by (simp add: zdiff_def zadd_ac)
   6.495 +
   6.496 +lemma zdiff_zless_eq: "(x-y < z) = (x < z + (y::int))"
   6.497 +apply (unfold zless_def zdiff_def)
   6.498 +apply (simp add: zadd_ac)
   6.499 +done
   6.500 +
   6.501 +lemma zless_zdiff_eq: "(x < z-y) = (x + (y::int) < z)"
   6.502 +apply (unfold zless_def zdiff_def)
   6.503 +apply (simp add: zadd_ac)
   6.504 +done
   6.505 +
   6.506 +lemma zdiff_zle_eq: "(x-y <= z) = (x <= z + (y::int))"
   6.507 +apply (unfold zle_def)
   6.508 +apply (simp add: zless_zdiff_eq)
   6.509 +done
   6.510 +
   6.511 +lemma zle_zdiff_eq: "(x <= z-y) = (x + (y::int) <= z)"
   6.512 +apply (unfold zle_def)
   6.513 +apply (simp add: zdiff_zless_eq)
   6.514 +done
   6.515 +
   6.516 +lemma zdiff_eq_eq: "(x-y = z) = (x = z + (y::int))"
   6.517 +by (auto simp add: zdiff_def zadd_assoc Zero_int_def [symmetric])
   6.518 +
   6.519 +lemma eq_zdiff_eq: "(x = z-y) = (x + (y::int) = z)"
   6.520 +by (auto simp add: zdiff_def zadd_assoc Zero_int_def [symmetric])
   6.521 +
   6.522 +(*This list of rewrites simplifies (in)equalities by bringing subtractions
   6.523 +  to the top and then moving negative terms to the other side.  
   6.524 +  Use with zadd_ac*)
   6.525 +lemmas zcompare_rls =
   6.526 +     zdiff_def [symmetric]
   6.527 +     zadd_zdiff_eq zdiff_zadd_eq zdiff_zdiff_eq zdiff_zdiff_eq2 
   6.528 +     zdiff_zless_eq zless_zdiff_eq zdiff_zle_eq zle_zdiff_eq 
   6.529 +     zdiff_eq_eq eq_zdiff_eq
   6.530 +
   6.531 +
   6.532 +(** Cancellation laws **)
   6.533 +
   6.534 +lemma zadd_left_cancel [simp]: "!!w::int. (z + w' = z + w) = (w' = w)"
   6.535 +apply safe
   6.536 +apply (drule_tac f = "%x. x + (-z) " in arg_cong)
   6.537 +apply (simp add: Zero_int_def [symmetric] zadd_ac)
   6.538 +done
   6.539 +
   6.540 +lemma zadd_right_cancel [simp]: "!!z::int. (w' + z = w + z) = (w' = w)"
   6.541 +by (simp add: zadd_ac)
   6.542 +
   6.543 +
   6.544 +(** For the cancellation simproc.
   6.545 +    The idea is to cancel like terms on opposite sides by subtraction **)
   6.546 +
   6.547 +lemma zless_eqI: "(x::int) - y = x' - y' ==> (x<y) = (x'<y')"
   6.548 +by (simp add: zless_def)
   6.549 +
   6.550 +lemma zle_eqI: "(x::int) - y = x' - y' ==> (y<=x) = (y'<=x')"
   6.551 +apply (drule zless_eqI)
   6.552 +apply (simp (no_asm_simp) add: zle_def)
   6.553 +done
   6.554 +
   6.555 +lemma zeq_eqI: "(x::int) - y = x' - y' ==> (x=y) = (x'=y')"
   6.556 +apply safe
   6.557 +apply (simp_all add: eq_zdiff_eq zdiff_eq_eq)
   6.558 +done
   6.559 +
   6.560 +ML
   6.561 +{*
   6.562 +val int_def = thm "int_def";
   6.563 +val neg_def = thm "neg_def";
   6.564 +val iszero_def = thm "iszero_def";
   6.565 +val Zero_int_def = thm "Zero_int_def";
   6.566 +val One_int_def = thm "One_int_def";
   6.567 +val zadd_def = thm "zadd_def";
   6.568 +val zdiff_def = thm "zdiff_def";
   6.569 +val zless_def = thm "zless_def";
   6.570 +val zle_def = thm "zle_def";
   6.571 +val zmult_def = thm "zmult_def";
   6.572 +
   6.573 +val intrel_iff = thm "intrel_iff";
   6.574 +val equiv_intrel = thm "equiv_intrel";
   6.575 +val equiv_intrel_iff = thm "equiv_intrel_iff";
   6.576 +val intrel_in_integ = thm "intrel_in_integ";
   6.577 +val inj_on_Abs_Integ = thm "inj_on_Abs_Integ";
   6.578 +val inj_Rep_Integ = thm "inj_Rep_Integ";
   6.579 +val inj_int = thm "inj_int";
   6.580 +val zminus_congruent = thm "zminus_congruent";
   6.581 +val zminus = thm "zminus";
   6.582 +val eq_Abs_Integ = thm "eq_Abs_Integ";
   6.583 +val zminus_zminus = thm "zminus_zminus";
   6.584 +val inj_zminus = thm "inj_zminus";
   6.585 +val zminus_0 = thm "zminus_0";
   6.586 +val not_neg_int = thm "not_neg_int";
   6.587 +val neg_zminus_int = thm "neg_zminus_int";
   6.588 +val zadd = thm "zadd";
   6.589 +val zminus_zadd_distrib = thm "zminus_zadd_distrib";
   6.590 +val zadd_commute = thm "zadd_commute";
   6.591 +val zadd_assoc = thm "zadd_assoc";
   6.592 +val zadd_left_commute = thm "zadd_left_commute";
   6.593 +val zadd_ac = thms "zadd_ac";
   6.594 +val zadd_int = thm "zadd_int";
   6.595 +val zadd_int_left = thm "zadd_int_left";
   6.596 +val int_Suc = thm "int_Suc";
   6.597 +val zadd_0 = thm "zadd_0";
   6.598 +val zadd_0_right = thm "zadd_0_right";
   6.599 +val zadd_zminus_inverse = thm "zadd_zminus_inverse";
   6.600 +val zadd_zminus_inverse2 = thm "zadd_zminus_inverse2";
   6.601 +val zadd_zminus_cancel = thm "zadd_zminus_cancel";
   6.602 +val zminus_zadd_cancel = thm "zminus_zadd_cancel";
   6.603 +val zdiff0 = thm "zdiff0";
   6.604 +val zdiff0_right = thm "zdiff0_right";
   6.605 +val zdiff_self = thm "zdiff_self";
   6.606 +val zadd_assoc_cong = thm "zadd_assoc_cong";
   6.607 +val zadd_assoc_swap = thm "zadd_assoc_swap";
   6.608 +val zmult_congruent2 = thm "zmult_congruent2";
   6.609 +val zmult = thm "zmult";
   6.610 +val zmult_zminus = thm "zmult_zminus";
   6.611 +val zmult_commute = thm "zmult_commute";
   6.612 +val zmult_assoc = thm "zmult_assoc";
   6.613 +val zmult_left_commute = thm "zmult_left_commute";
   6.614 +val zmult_ac = thms "zmult_ac";
   6.615 +val zadd_zmult_distrib = thm "zadd_zmult_distrib";
   6.616 +val zmult_zminus_right = thm "zmult_zminus_right";
   6.617 +val zadd_zmult_distrib2 = thm "zadd_zmult_distrib2";
   6.618 +val zdiff_zmult_distrib = thm "zdiff_zmult_distrib";
   6.619 +val zdiff_zmult_distrib2 = thm "zdiff_zmult_distrib2";
   6.620 +val int_distrib = thms "int_distrib";
   6.621 +val zmult_int = thm "zmult_int";
   6.622 +val zmult_0 = thm "zmult_0";
   6.623 +val zmult_1 = thm "zmult_1";
   6.624 +val zmult_0_right = thm "zmult_0_right";
   6.625 +val zmult_1_right = thm "zmult_1_right";
   6.626 +val zless_iff_Suc_zadd = thm "zless_iff_Suc_zadd";
   6.627 +val zless_zadd_Suc = thm "zless_zadd_Suc";
   6.628 +val zless_trans = thm "zless_trans";
   6.629 +val zless_not_sym = thm "zless_not_sym";
   6.630 +val zless_asym = thm "zless_asym";
   6.631 +val zless_not_refl = thm "zless_not_refl";
   6.632 +val zless_irrefl = thm "zless_irrefl";
   6.633 +val zless_linear = thm "zless_linear";
   6.634 +val int_neq_iff = thm "int_neq_iff";
   6.635 +val int_neqE = thm "int_neqE";
   6.636 +val int_int_eq = thm "int_int_eq";
   6.637 +val int_eq_0_conv = thm "int_eq_0_conv";
   6.638 +val zless_int = thm "zless_int";
   6.639 +val int_less_0_conv = thm "int_less_0_conv";
   6.640 +val zero_less_int_conv = thm "zero_less_int_conv";
   6.641 +val zle_int = thm "zle_int";
   6.642 +val zero_zle_int = thm "zero_zle_int";
   6.643 +val int_le_0_conv = thm "int_le_0_conv";
   6.644 +val zle_imp_zless_or_eq = thm "zle_imp_zless_or_eq";
   6.645 +val zless_or_eq_imp_zle = thm "zless_or_eq_imp_zle";
   6.646 +val int_le_less = thm "int_le_less";
   6.647 +val zle_refl = thm "zle_refl";
   6.648 +val zle_linear = thm "zle_linear";
   6.649 +val zle_trans = thm "zle_trans";
   6.650 +val zle_anti_sym = thm "zle_anti_sym";
   6.651 +val int_less_le = thm "int_less_le";
   6.652 +val zadd_zdiff_eq = thm "zadd_zdiff_eq";
   6.653 +val zdiff_zadd_eq = thm "zdiff_zadd_eq";
   6.654 +val zdiff_zdiff_eq = thm "zdiff_zdiff_eq";
   6.655 +val zdiff_zdiff_eq2 = thm "zdiff_zdiff_eq2";
   6.656 +val zdiff_zless_eq = thm "zdiff_zless_eq";
   6.657 +val zless_zdiff_eq = thm "zless_zdiff_eq";
   6.658 +val zdiff_zle_eq = thm "zdiff_zle_eq";
   6.659 +val zle_zdiff_eq = thm "zle_zdiff_eq";
   6.660 +val zdiff_eq_eq = thm "zdiff_eq_eq";
   6.661 +val eq_zdiff_eq = thm "eq_zdiff_eq";
   6.662 +val zcompare_rls = thms "zcompare_rls";
   6.663 +val zadd_left_cancel = thm "zadd_left_cancel";
   6.664 +val zadd_right_cancel = thm "zadd_right_cancel";
   6.665 +val zless_eqI = thm "zless_eqI";
   6.666 +val zle_eqI = thm "zle_eqI";
   6.667 +val zeq_eqI = thm "zeq_eqI";
   6.668 +*}
   6.669 +
   6.670  end
     7.1 --- a/src/HOL/Integ/IntPower.ML	Tue Nov 18 09:45:45 2003 +0100
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,61 +0,0 @@
     7.4 -(*  Title:	IntPower.thy
     7.5 -    ID:         $Id$
     7.6 -    Author:	Thomas M. Rasmussen
     7.7 -    Copyright	2000  University of Cambridge
     7.8 -
     7.9 -Integer powers 
    7.10 -*)
    7.11 -
    7.12 -
    7.13 -Goal "((x::int) mod m)^y mod m = x^y mod m";
    7.14 -by (induct_tac "y" 1);
    7.15 -by Auto_tac;
    7.16 -by (rtac (zmod_zmult1_eq RS trans) 1);
    7.17 -by (Asm_simp_tac 1);
    7.18 -by (rtac (zmod_zmult_distrib RS sym) 1);
    7.19 -qed "zpower_zmod";
    7.20 -
    7.21 -Goal "1^y = (1::int)";
    7.22 -by (induct_tac "y" 1);
    7.23 -by Auto_tac;
    7.24 -qed "zpower_1";
    7.25 -Addsimps [zpower_1];
    7.26 -
    7.27 -Goal "(x*z)^y = ((x^y)*(z^y)::int)";
    7.28 -by (induct_tac "y" 1);
    7.29 -by Auto_tac;
    7.30 -qed "zpower_zmult_distrib";
    7.31 -
    7.32 -Goal "x^(y+z) = ((x^y)*(x^z)::int)";
    7.33 -by (induct_tac "y" 1);
    7.34 -by Auto_tac;
    7.35 -qed "zpower_zadd_distrib";
    7.36 -
    7.37 -Goal "(x^y)^z = (x^(y*z)::int)";
    7.38 -by (induct_tac "y" 1);
    7.39 -by Auto_tac;
    7.40 -by (stac zpower_zmult_distrib 1);
    7.41 -by (stac zpower_zadd_distrib 1);
    7.42 -by (Asm_simp_tac 1);
    7.43 -qed "zpower_zpower";
    7.44 -
    7.45 -
    7.46 -(*** Logical equivalences for inequalities ***)
    7.47 -
    7.48 -Goal "(x^n = 0) = (x = (0::int) & 0<n)";
    7.49 -by (induct_tac "n" 1);
    7.50 -by Auto_tac; 
    7.51 -qed "zpower_eq_0_iff";
    7.52 -Addsimps [zpower_eq_0_iff];
    7.53 -
    7.54 -Goal "(0 < (abs x)^n) = (x ~= (0::int) | n=0)";
    7.55 -by (induct_tac "n" 1);
    7.56 -by (auto_tac (claset(), simpset() addsimps [int_0_less_mult_iff]));  
    7.57 -qed "zero_less_zpower_abs_iff";
    7.58 -Addsimps [zero_less_zpower_abs_iff];
    7.59 -
    7.60 -Goal "(0::int) <= (abs x)^n";
    7.61 -by (induct_tac "n" 1);
    7.62 -by (auto_tac (claset(), simpset() addsimps [int_0_le_mult_iff]));  
    7.63 -qed "zero_le_zpower_abs";
    7.64 -Addsimps [zero_le_zpower_abs];
     8.1 --- a/src/HOL/Integ/IntPower.thy	Tue Nov 18 09:45:45 2003 +0100
     8.2 +++ b/src/HOL/Integ/IntPower.thy	Tue Nov 18 11:01:52 2003 +0100
     8.3 @@ -6,13 +6,66 @@
     8.4  Integer powers 
     8.5  *)
     8.6  
     8.7 -IntPower = IntDiv + 
     8.8 +theory IntPower = IntDiv:
     8.9  
    8.10 -instance
    8.11 -  int :: {power}
    8.12 +instance int :: power ..
    8.13  
    8.14  primrec
    8.15 -  power_0   "p ^ 0 = 1"
    8.16 -  power_Suc "p ^ (Suc n) = (p::int) * (p ^ n)"
    8.17 +  power_0:   "p ^ 0 = 1"
    8.18 +  power_Suc: "p ^ (Suc n) = (p::int) * (p ^ n)"
    8.19 +
    8.20 +
    8.21 +lemma zpower_zmod: "((x::int) mod m)^y mod m = x^y mod m"
    8.22 +apply (induct_tac "y", auto)
    8.23 +apply (rule zmod_zmult1_eq [THEN trans])
    8.24 +apply (simp (no_asm_simp))
    8.25 +apply (rule zmod_zmult_distrib [symmetric])
    8.26 +done
    8.27 +
    8.28 +lemma zpower_1 [simp]: "1^y = (1::int)"
    8.29 +by (induct_tac "y", auto)
    8.30 +
    8.31 +lemma zpower_zmult_distrib: "(x*z)^y = ((x^y)*(z^y)::int)"
    8.32 +by (induct_tac "y", auto)
    8.33 +
    8.34 +lemma zpower_zadd_distrib: "x^(y+z) = ((x^y)*(x^z)::int)"
    8.35 +by (induct_tac "y", auto)
    8.36 +
    8.37 +lemma zpower_zpower: "(x^y)^z = (x^(y*z)::int)"
    8.38 +apply (induct_tac "y", auto)
    8.39 +apply (subst zpower_zmult_distrib)
    8.40 +apply (subst zpower_zadd_distrib)
    8.41 +apply (simp (no_asm_simp))
    8.42 +done
    8.43 +
    8.44 +
    8.45 +(*** Logical equivalences for inequalities ***)
    8.46 +
    8.47 +lemma zpower_eq_0_iff [simp]: "(x^n = 0) = (x = (0::int) & 0<n)"
    8.48 +by (induct_tac "n", auto)
    8.49 +
    8.50 +lemma zero_less_zpower_abs_iff [simp]:
    8.51 +     "(0 < (abs x)^n) = (x \<noteq> (0::int) | n=0)"
    8.52 +apply (induct_tac "n")
    8.53 +apply (auto simp add: int_0_less_mult_iff)
    8.54 +done
    8.55 +
    8.56 +lemma zero_le_zpower_abs [simp]: "(0::int) <= (abs x)^n"
    8.57 +apply (induct_tac "n")
    8.58 +apply (auto simp add: int_0_le_mult_iff)
    8.59 +done
    8.60 +
    8.61 +ML
    8.62 +{*
    8.63 +val zpower_zmod = thm "zpower_zmod";
    8.64 +val zpower_1 = thm "zpower_1";
    8.65 +val zpower_zmult_distrib = thm "zpower_zmult_distrib";
    8.66 +val zpower_zadd_distrib = thm "zpower_zadd_distrib";
    8.67 +val zpower_zpower = thm "zpower_zpower";
    8.68 +val zpower_eq_0_iff = thm "zpower_eq_0_iff";
    8.69 +val zero_less_zpower_abs_iff = thm "zero_less_zpower_abs_iff";
    8.70 +val zero_le_zpower_abs = thm "zero_le_zpower_abs";
    8.71 +*}
    8.72  
    8.73  end
    8.74 +
     9.1 --- a/src/HOL/Integ/cooper_proof.ML	Tue Nov 18 09:45:45 2003 +0100
     9.2 +++ b/src/HOL/Integ/cooper_proof.ML	Tue Nov 18 11:01:52 2003 +0100
     9.3 @@ -44,7 +44,7 @@
     9.4  (*-----------------------------------------------------------------*)
     9.5  
     9.6  val presburger_ss = simpset_of (theory "Presburger")
     9.7 -  addsimps [zdiff_def] delsimps [symmetric zdiff_def];
     9.8 +  addsimps [zdiff_def] delsimps [thm"zdiff_def_symmetric"];
     9.9  val cboolT = ctyp_of (sign_of HOL.thy) HOLogic.boolT;
    9.10  
    9.11  (*Theorems that will be used later for the proofgeneration*)
    9.12 @@ -52,7 +52,7 @@
    9.13  val zdvd_iff_zmod_eq_0 = thm "zdvd_iff_zmod_eq_0";
    9.14  val unity_coeff_ex = thm "unity_coeff_ex";
    9.15  
    9.16 -(* Thorems for proving the adjustment of the coeffitients*)
    9.17 +(* Theorems for proving the adjustment of the coefficients*)
    9.18  
    9.19  val ac_lt_eq =  thm "ac_lt_eq";
    9.20  val ac_eq_eq = thm "ac_eq_eq";
    9.21 @@ -68,7 +68,7 @@
    9.22  val qe_exI = thm "qe_exI";
    9.23  val qe_ALLI = thm "qe_ALLI";
    9.24  
    9.25 -(*Modulo D property for Pminusinf an Plusinf *)
    9.26 +(*Modulo D property for Pminusinf and Plusinf *)
    9.27  val fm_modd_minf = thm "fm_modd_minf";
    9.28  val not_dvd_modd_minf = thm "not_dvd_modd_minf";
    9.29  val dvd_modd_minf = thm "dvd_modd_minf";
    9.30 @@ -77,7 +77,7 @@
    9.31  val not_dvd_modd_pinf = thm "not_dvd_modd_pinf";
    9.32  val dvd_modd_pinf = thm "dvd_modd_pinf";
    9.33  
    9.34 -(* the minusinfinity proprty*)
    9.35 +(* the minusinfinity property*)
    9.36  
    9.37  val fm_eq_minf = thm "fm_eq_minf";
    9.38  val neq_eq_minf = thm "neq_eq_minf";
    9.39 @@ -87,7 +87,7 @@
    9.40  val not_dvd_eq_minf = thm "not_dvd_eq_minf";
    9.41  val dvd_eq_minf = thm "dvd_eq_minf";
    9.42  
    9.43 -(* the Plusinfinity proprty*)
    9.44 +(* the Plusinfinity property*)
    9.45  
    9.46  val fm_eq_pinf = thm "fm_eq_pinf";
    9.47  val neq_eq_pinf = thm "neq_eq_pinf";
    10.1 --- a/src/HOL/Integ/int_arith2.ML	Tue Nov 18 09:45:45 2003 +0100
    10.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.3 @@ -1,99 +0,0 @@
    10.4 -(*  Title:      HOL/Integ/int_arith2.ML
    10.5 -    ID:         $Id$
    10.6 -    Authors:    Larry Paulson and Tobias Nipkow
    10.7 -*)
    10.8 -
    10.9 -Goal "(w <= z - (1::int)) = (w<(z::int))";
   10.10 -by (arith_tac 1);
   10.11 -qed "zle_diff1_eq";
   10.12 -Addsimps [zle_diff1_eq];
   10.13 -
   10.14 -Goal "(w < z + 1) = (w<=(z::int))";
   10.15 -by (arith_tac 1);
   10.16 -qed "zle_add1_eq_le";
   10.17 -Addsimps [zle_add1_eq_le];
   10.18 -
   10.19 -Goal "(z = z + w) = (w = (0::int))";
   10.20 -by (arith_tac 1);
   10.21 -qed "zadd_left_cancel0";
   10.22 -Addsimps [zadd_left_cancel0];
   10.23 -
   10.24 -
   10.25 -(* nat *)
   10.26 -
   10.27 -val [major,minor] = Goal "[| 0 <= z;  !!m. z = int m ==> P |] ==> P"; 
   10.28 -by (rtac (major RS nat_0_le RS sym RS minor) 1);
   10.29 -qed "nonneg_eq_int"; 
   10.30 -
   10.31 -Goal "(nat w = m) = (if 0 <= w then w = int m else m=0)";
   10.32 -by Auto_tac;
   10.33 -qed "nat_eq_iff";
   10.34 -
   10.35 -Goal "(m = nat w) = (if 0 <= w then w = int m else m=0)";
   10.36 -by Auto_tac;
   10.37 -qed "nat_eq_iff2";
   10.38 -
   10.39 -Goal "0 <= w ==> (nat w < m) = (w < int m)";
   10.40 -by (rtac iffI 1);
   10.41 -by (asm_full_simp_tac 
   10.42 -    (simpset() delsimps [zless_int] addsimps [zless_int RS sym]) 2);
   10.43 -by (etac (nat_0_le RS subst) 1);
   10.44 -by (Simp_tac 1);
   10.45 -qed "nat_less_iff";
   10.46 -
   10.47 -Goal "(int m = z) = (m = nat z & 0 <= z)";
   10.48 -by (auto_tac (claset(), simpset() addsimps [nat_eq_iff2]));  
   10.49 -qed "int_eq_iff";
   10.50 -
   10.51 -
   10.52 -(*Users don't want to see (int 0), int(Suc 0) or w + - z*)
   10.53 -Addsimps (map symmetric [Zero_int_def, One_int_def, zdiff_def]);
   10.54 -
   10.55 -Goal "nat 0 = 0";
   10.56 -by (simp_tac (simpset() addsimps [nat_eq_iff]) 1);
   10.57 -qed "nat_0";
   10.58 -
   10.59 -Goal "nat 1 = Suc 0";
   10.60 -by (stac nat_eq_iff 1);
   10.61 -by (Simp_tac 1);
   10.62 -qed "nat_1";
   10.63 -
   10.64 -Goal "nat 2 = Suc (Suc 0)";
   10.65 -by (stac nat_eq_iff 1);
   10.66 -by (Simp_tac 1);
   10.67 -qed "nat_2";
   10.68 -
   10.69 -Goal "0 <= w ==> (nat w < nat z) = (w<z)";
   10.70 -by (case_tac "neg z" 1);
   10.71 -by (auto_tac (claset(), simpset() addsimps [nat_less_iff]));
   10.72 -by (auto_tac (claset() addIs [zless_trans], 
   10.73 -	      simpset() addsimps [neg_eq_less_0, zle_def]));
   10.74 -qed "nat_less_eq_zless";
   10.75 -
   10.76 -Goal "0 < w | 0 <= z ==> (nat w <= nat z) = (w<=z)";
   10.77 -by (auto_tac (claset(), 
   10.78 -	      simpset() addsimps [linorder_not_less RS sym, 
   10.79 -				  zless_nat_conj]));
   10.80 -qed "nat_le_eq_zle";
   10.81 -
   10.82 -(*** abs: absolute value, as an integer ****)
   10.83 -
   10.84 -(* Simpler: use zabs_def as rewrite rule;
   10.85 -   but arith_tac is not parameterized by such simp rules
   10.86 -*)
   10.87 -
   10.88 -Goalw [zabs_def]
   10.89 - "P(abs(i::int)) = ((0 <= i --> P i) & (i < 0 --> P(-i)))";
   10.90 -by (Simp_tac 1);
   10.91 -qed "zabs_split";
   10.92 -
   10.93 -Goal "0 <= abs (z::int)";
   10.94 -by (simp_tac (simpset() addsimps [zabs_def]) 1); 
   10.95 -qed "zero_le_zabs";
   10.96 -AddIffs [zero_le_zabs];
   10.97 -
   10.98 -
   10.99 -(*Not sure why this simprule is required!*)
  10.100 -Addsimps [inst "z" "number_of ?v" int_eq_iff];
  10.101 -
  10.102 -(*continued in IntArith.ML ...*)
    11.1 --- a/src/HOL/IsaMakefile	Tue Nov 18 09:45:45 2003 +0100
    11.2 +++ b/src/HOL/IsaMakefile	Tue Nov 18 11:01:52 2003 +0100
    11.3 @@ -86,11 +86,11 @@
    11.4    Hilbert_Choice.thy Hilbert_Choice_lemmas.ML HOL.ML \
    11.5    HOL.thy HOL_lemmas.ML Inductive.thy Integ/Bin.ML Integ/Bin.thy \
    11.6    Integ/cooper_dec.ML Integ/cooper_proof.ML \
    11.7 -  Integ/Equiv.ML Integ/Equiv.thy Integ/Int_lemmas.ML Integ/Int.thy \
    11.8 -  Integ/IntArith.ML Integ/IntArith.thy Integ/IntDef.ML Integ/IntDef.thy \
    11.9 -  Integ/IntDiv.thy Integ/IntPower.ML Integ/IntPower.thy \
   11.10 +  Integ/Equiv.thy Integ/Int_lemmas.ML Integ/Int.thy \
   11.11 +  Integ/IntArith.thy Integ/IntDef.thy \
   11.12 +  Integ/IntDiv.thy Integ/IntPower.thy \
   11.13    Integ/nat_bin.ML Integ/NatBin.thy Integ/NatSimprocs.ML \
   11.14 -  Integ/NatSimprocs.thy Integ/int_arith1.ML Integ/int_arith2.ML \
   11.15 +  Integ/NatSimprocs.thy Integ/int_arith1.ML \
   11.16    Integ/int_factor_simprocs.ML Integ/nat_simprocs.ML \
   11.17    Integ/Presburger.thy Integ/presburger.ML Integ/qelim.ML \
   11.18    Lfp.ML Lfp.thy List.ML List.thy Main.ML Main.thy Map.thy Nat.ML \
    12.1 --- a/src/HOL/Tools/Presburger/cooper_proof.ML	Tue Nov 18 09:45:45 2003 +0100
    12.2 +++ b/src/HOL/Tools/Presburger/cooper_proof.ML	Tue Nov 18 11:01:52 2003 +0100
    12.3 @@ -44,7 +44,7 @@
    12.4  (*-----------------------------------------------------------------*)
    12.5  
    12.6  val presburger_ss = simpset_of (theory "Presburger")
    12.7 -  addsimps [zdiff_def] delsimps [symmetric zdiff_def];
    12.8 +  addsimps [zdiff_def] delsimps [thm"zdiff_def_symmetric"];
    12.9  val cboolT = ctyp_of (sign_of HOL.thy) HOLogic.boolT;
   12.10  
   12.11  (*Theorems that will be used later for the proofgeneration*)
   12.12 @@ -52,7 +52,7 @@
   12.13  val zdvd_iff_zmod_eq_0 = thm "zdvd_iff_zmod_eq_0";
   12.14  val unity_coeff_ex = thm "unity_coeff_ex";
   12.15  
   12.16 -(* Thorems for proving the adjustment of the coeffitients*)
   12.17 +(* Theorems for proving the adjustment of the coefficients*)
   12.18  
   12.19  val ac_lt_eq =  thm "ac_lt_eq";
   12.20  val ac_eq_eq = thm "ac_eq_eq";
   12.21 @@ -68,7 +68,7 @@
   12.22  val qe_exI = thm "qe_exI";
   12.23  val qe_ALLI = thm "qe_ALLI";
   12.24  
   12.25 -(*Modulo D property for Pminusinf an Plusinf *)
   12.26 +(*Modulo D property for Pminusinf and Plusinf *)
   12.27  val fm_modd_minf = thm "fm_modd_minf";
   12.28  val not_dvd_modd_minf = thm "not_dvd_modd_minf";
   12.29  val dvd_modd_minf = thm "dvd_modd_minf";
   12.30 @@ -77,7 +77,7 @@
   12.31  val not_dvd_modd_pinf = thm "not_dvd_modd_pinf";
   12.32  val dvd_modd_pinf = thm "dvd_modd_pinf";
   12.33  
   12.34 -(* the minusinfinity proprty*)
   12.35 +(* the minusinfinity property*)
   12.36  
   12.37  val fm_eq_minf = thm "fm_eq_minf";
   12.38  val neq_eq_minf = thm "neq_eq_minf";
   12.39 @@ -87,7 +87,7 @@
   12.40  val not_dvd_eq_minf = thm "not_dvd_eq_minf";
   12.41  val dvd_eq_minf = thm "dvd_eq_minf";
   12.42  
   12.43 -(* the Plusinfinity proprty*)
   12.44 +(* the Plusinfinity property*)
   12.45  
   12.46  val fm_eq_pinf = thm "fm_eq_pinf";
   12.47  val neq_eq_pinf = thm "neq_eq_pinf";