1.1 --- a/src/HOL/Integ/IntDef.ML Mon Oct 22 11:01:30 2001 +0200
1.2 +++ b/src/HOL/Integ/IntDef.ML Mon Oct 22 11:54:22 2001 +0200
1.3 @@ -7,9 +7,6 @@
1.4 *)
1.5
1.6
1.7 -(*Rewrite the overloaded 0::int and 1::int*) (* FIXME *)
1.8 -Addsimps [Zero_int_def, One_int_def];
1.9 -
1.10 Goalw [intrel_def] "(((x1,y1),(x2,y2)): intrel) = (x1+y2 = x2+y1)";
1.11 by (Blast_tac 1);
1.12 qed "intrel_iff";
1.13 @@ -90,11 +87,10 @@
1.14 by (Asm_full_simp_tac 1);
1.15 qed "inj_zminus";
1.16
1.17 -Goalw [int_def] "- (int 0) = int 0";
1.18 +Goalw [int_def, Zero_int_def] "- 0 = (0::int)";
1.19 by (simp_tac (simpset() addsimps [zminus]) 1);
1.20 -qed "zminus_int0";
1.21 -
1.22 -Addsimps [zminus_int0];
1.23 +qed "zminus_0";
1.24 +Addsimps [zminus_0];
1.25
1.26
1.27 (**** neg: the test for negative integers ****)
1.28 @@ -159,61 +155,57 @@
1.29 by (simp_tac (simpset() addsimps [zadd_int, zadd_assoc RS sym]) 1);
1.30 qed "zadd_int_left";
1.31
1.32 -Goal "int (Suc m) = int 1 + (int m)";
1.33 -by (simp_tac (simpset() addsimps [zadd_int]) 1);
1.34 -qed "int_Suc_int_1";
1.35 +Goal "int (Suc m) = 1 + (int m)";
1.36 +by (simp_tac (simpset() addsimps [One_int_def, zadd_int]) 1);
1.37 +qed "int_Suc";
1.38
1.39 -Goalw [int_def] "int 0 + z = z";
1.40 +(*also for the instance declaration int :: plus_ac0*)
1.41 +Goalw [Zero_int_def, int_def] "(0::int) + z = z";
1.42 by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
1.43 by (asm_simp_tac (simpset() addsimps [zadd]) 1);
1.44 -qed "zadd_int0";
1.45 +qed "zadd_0";
1.46 +Addsimps [zadd_0];
1.47
1.48 -Goal "z + int 0 = z";
1.49 -by (rtac (zadd_commute RS trans) 1);
1.50 -by (rtac zadd_int0 1);
1.51 -qed "zadd_int0_right";
1.52 +Goal "z + (0::int) = z";
1.53 +by (rtac ([zadd_commute, zadd_0] MRS trans) 1);
1.54 +qed "zadd_0_right";
1.55 +Addsimps [zadd_0_right];
1.56
1.57 -Goalw [int_def] "z + (- z) = int 0";
1.58 +Goalw [int_def, Zero_int_def] "z + (- z) = (0::int)";
1.59 by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
1.60 by (asm_simp_tac (simpset() addsimps [zminus, zadd, add_commute]) 1);
1.61 qed "zadd_zminus_inverse";
1.62
1.63 -Goal "(- z) + z = int 0";
1.64 +Goal "(- z) + z = (0::int)";
1.65 by (rtac (zadd_commute RS trans) 1);
1.66 by (rtac zadd_zminus_inverse 1);
1.67 qed "zadd_zminus_inverse2";
1.68
1.69 -Addsimps [zadd_int0, zadd_int0_right,
1.70 - zadd_zminus_inverse, zadd_zminus_inverse2];
1.71 -
1.72 -(*for the instance declaration int :: plus_ac0*)
1.73 -Goal "0 + z = (z::int)";
1.74 -by (Simp_tac 1);
1.75 -qed "zadd_zero";
1.76 +Addsimps [zadd_zminus_inverse, zadd_zminus_inverse2];
1.77
1.78 Goal "z + (- z + w) = (w::int)";
1.79 -by (simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1);
1.80 +by (simp_tac (simpset() addsimps [zadd_assoc RS sym, zadd_0]) 1);
1.81 qed "zadd_zminus_cancel";
1.82
1.83 Goal "(-z) + (z + w) = (w::int)";
1.84 -by (simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1);
1.85 +by (simp_tac (simpset() addsimps [zadd_assoc RS sym, zadd_0]) 1);
1.86 qed "zminus_zadd_cancel";
1.87
1.88 Addsimps [zadd_zminus_cancel, zminus_zadd_cancel];
1.89
1.90 -Goal "int 0 - x = -x";
1.91 +Goal "(0::int) - x = -x";
1.92 by (simp_tac (simpset() addsimps [zdiff_def]) 1);
1.93 -qed "zdiff_int0";
1.94 +qed "zdiff0";
1.95
1.96 -Goal "x - int 0 = x";
1.97 +Goal "x - (0::int) = x";
1.98 by (simp_tac (simpset() addsimps [zdiff_def]) 1);
1.99 -qed "zdiff_int0_right";
1.100 +qed "zdiff0_right";
1.101
1.102 -Goal "x - x = int 0";
1.103 -by (simp_tac (simpset() addsimps [zdiff_def]) 1);
1.104 +Goal "x - x = (0::int)";
1.105 +by (simp_tac (simpset() addsimps [zdiff_def, Zero_int_def]) 1);
1.106 qed "zdiff_self";
1.107
1.108 -Addsimps [zdiff_int0, zdiff_int0_right, zdiff_self];
1.109 +Addsimps [zdiff0, zdiff0_right, zdiff_self];
1.110
1.111
1.112 (** Lemmas **)
1.113 @@ -321,25 +313,27 @@
1.114 by (simp_tac (simpset() addsimps [zmult]) 1);
1.115 qed "zmult_int";
1.116
1.117 -Goalw [int_def] "int 0 * z = int 0";
1.118 +Goalw [Zero_int_def, int_def] "0 * z = (0::int)";
1.119 by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
1.120 by (asm_simp_tac (simpset() addsimps [zmult]) 1);
1.121 -qed "zmult_int0";
1.122 +qed "zmult_0";
1.123 +Addsimps [zmult_0];
1.124
1.125 -Goalw [int_def] "int (Suc 0) * z = z";
1.126 +Goalw [One_int_def, int_def] "(1::int) * z = z";
1.127 by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
1.128 by (asm_simp_tac (simpset() addsimps [zmult]) 1);
1.129 -qed "zmult_int1";
1.130 +qed "zmult_1";
1.131 +Addsimps [zmult_1];
1.132
1.133 -Goal "z * int 0 = int 0";
1.134 -by (rtac ([zmult_commute, zmult_int0] MRS trans) 1);
1.135 -qed "zmult_int0_right";
1.136 +Goal "z * 0 = (0::int)";
1.137 +by (rtac ([zmult_commute, zmult_0] MRS trans) 1);
1.138 +qed "zmult_0_right";
1.139 +Addsimps [zmult_0_right];
1.140
1.141 -Goal "z * int (Suc 0) = z";
1.142 -by (rtac ([zmult_commute, zmult_int1] MRS trans) 1);
1.143 -qed "zmult_int1_right";
1.144 -
1.145 -Addsimps [zmult_int0, zmult_int0_right, zmult_int1, zmult_int1_right];
1.146 +Goal "z * (1::int) = z";
1.147 +by (rtac ([zmult_commute, zmult_1] MRS trans) 1);
1.148 +qed "zmult_1_right";
1.149 +Addsimps [zmult_1_right];
1.150
1.151
1.152 (* Theorems about less and less_equal *)
1.153 @@ -413,12 +407,27 @@
1.154 qed "int_int_eq";
1.155 AddIffs [int_int_eq];
1.156
1.157 +Goal "(int n = 0) = (n = 0)";
1.158 +by (simp_tac (simpset() addsimps [Zero_int_def]) 1);
1.159 +qed "int_eq_0_conv";
1.160 +Addsimps [int_eq_0_conv];
1.161 +
1.162 Goal "(int m < int n) = (m<n)";
1.163 by (simp_tac (simpset() addsimps [less_iff_Suc_add, zless_iff_Suc_zadd,
1.164 zadd_int]) 1);
1.165 qed "zless_int";
1.166 Addsimps [zless_int];
1.167
1.168 +Goal "~ (int k < 0)";
1.169 +by (simp_tac (simpset() addsimps [Zero_int_def]) 1);
1.170 +qed "int_less_0_conv";
1.171 +Addsimps [int_less_0_conv];
1.172 +
1.173 +Goal "(0 < int n) = (0 < n)";
1.174 +by (simp_tac (simpset() addsimps [Zero_int_def]) 1);
1.175 +qed "zero_less_int_conv";
1.176 +Addsimps [zero_less_int_conv];
1.177 +
1.178
1.179 (*** Properties of <= ***)
1.180
1.181 @@ -427,6 +436,16 @@
1.182 qed "zle_int";
1.183 Addsimps [zle_int];
1.184
1.185 +Goal "(0 <= int n)";
1.186 +by (simp_tac (simpset() addsimps [Zero_int_def]) 1);
1.187 +qed "zero_zle_int";
1.188 +Addsimps [zero_zle_int];
1.189 +
1.190 +Goal "(int n <= 0) = (n = 0)";
1.191 +by (simp_tac (simpset() addsimps [Zero_int_def]) 1);
1.192 +qed "int_le_0_conv";
1.193 +Addsimps [int_le_0_conv];
1.194 +
1.195 Goalw [zle_def] "z <= w ==> z < w | z=(w::int)";
1.196 by (cut_facts_tac [zless_linear] 1);
1.197 by (blast_tac (claset() addEs [zless_asym]) 1);
1.198 @@ -506,11 +525,13 @@
1.199 qed "zle_zdiff_eq";
1.200
1.201 Goalw [zdiff_def] "(x-y = z) = (x = z + (y::int))";
1.202 -by (auto_tac (claset(), simpset() addsimps [zadd_assoc]));
1.203 +by (auto_tac (claset(),
1.204 + simpset() addsimps [zadd_assoc, symmetric Zero_int_def]));
1.205 qed "zdiff_eq_eq";
1.206
1.207 Goalw [zdiff_def] "(x = z-y) = (x + (y::int) = z)";
1.208 -by (auto_tac (claset(), simpset() addsimps [zadd_assoc]));
1.209 +by (auto_tac (claset(),
1.210 + simpset() addsimps [zadd_assoc, symmetric Zero_int_def]));
1.211 qed "eq_zdiff_eq";
1.212
1.213 (*This list of rewrites simplifies (in)equalities by bringing subtractions
1.214 @@ -528,7 +549,8 @@
1.215 Goal "!!w::int. (z + w' = z + w) = (w' = w)";
1.216 by Safe_tac;
1.217 by (dres_inst_tac [("f", "%x. x + (-z)")] arg_cong 1);
1.218 -by (asm_full_simp_tac (simpset() addsimps zadd_ac) 1);
1.219 +by (asm_full_simp_tac (simpset() addsimps symmetric Zero_int_def ::
1.220 + zadd_ac) 1);
1.221 qed "zadd_left_cancel";
1.222
1.223 Addsimps [zadd_left_cancel];