1 (* Title: HOL/Integ/IntArith.ML
3 Authors: Larry Paulson and Tobias Nipkow
7 Goal "abs(abs(x::int)) = abs(x)";
12 Goal "abs(-(x::int)) = abs(x)";
17 Goal "abs(x+y) <= abs(x) + abs(y::int)";
22 (*** Intermediate value theorems ***)
24 Goal "(ALL i<n::nat. abs(f(i+1) - f i) <= 1) --> \
25 \ f 0 <= k --> k <= f n --> (EX i <= n. f i = (k::int))";
30 by(Asm_full_simp_tac 1);
31 by(eres_inst_tac [("x","n")] allE 1);
32 by(Asm_full_simp_tac 1);
33 by(case_tac "k = f(n+1)" 1);
36 by(asm_full_simp_tac (simpset() addsimps [zabs_def]
37 addsplits [split_if_asm]) 1);
39 by(blast_tac (claset() addIs [le_SucI]) 1);
42 bind_thm("nat0_intermed_int_val", ObjectLogic.rulify_no_asm lemma);
44 Goal "[| !i. m <= i & i < n --> abs(f(i + 1::nat) - f i) <= 1; m < n; \
45 \ f m <= k; k <= f n |] ==> ? i. m <= i & i <= n & f i = (k::int)";
46 by(cut_inst_tac [("n","n-m"),("f", "%i. f(i+m)"),("k","k")]lemma 1);
47 by(Asm_full_simp_tac 1);
50 by(eres_inst_tac [("x","i+m")] allE 1);
53 by(res_inst_tac [("x","i+m")] exI 1);
55 qed "nat_intermed_int_val";
58 (*** Some convenient biconditionals for products of signs ***)
60 Goal "[| (0::int) < i; 0 < j |] ==> 0 < i*j";
61 by (dtac zmult_zless_mono1 1);
65 Goal "[| i < (0::int); j < 0 |] ==> 0 < i*j";
66 by (dtac zmult_zless_mono1_neg 1);
70 Goal "[| (0::int) < i; j < 0 |] ==> i*j < 0";
71 by (dtac zmult_zless_mono1_neg 1);
75 Goal "((0::int) < x*y) = (0 < x & 0 < y | x < 0 & y < 0)";
76 by (auto_tac (claset(),
77 simpset() addsimps [order_le_less, linorder_not_less,
78 zmult_pos, zmult_neg]));
79 by (ALLGOALS (rtac ccontr));
80 by (auto_tac (claset(),
81 simpset() addsimps [order_le_less, linorder_not_less]));
82 by (ALLGOALS (etac rev_mp));
83 by (ALLGOALS (dtac zmult_pos_neg THEN' assume_tac));
84 by (auto_tac (claset() addDs [order_less_not_sym],
85 simpset() addsimps [zmult_commute]));
86 qed "int_0_less_mult_iff";
88 Goal "((0::int) <= x*y) = (0 <= x & 0 <= y | x <= 0 & y <= 0)";
89 by (auto_tac (claset(),
90 simpset() addsimps [order_le_less, linorder_not_less,
91 int_0_less_mult_iff]));
92 qed "int_0_le_mult_iff";
94 Goal "(x*y < (0::int)) = (0 < x & y < 0 | x < 0 & 0 < y)";
95 by (auto_tac (claset(),
96 simpset() addsimps [int_0_le_mult_iff,
97 linorder_not_le RS sym]));
98 by (auto_tac (claset() addDs [order_less_not_sym],
99 simpset() addsimps [linorder_not_le]));
100 qed "zmult_less_0_iff";
102 Goal "(x*y <= (0::int)) = (0 <= x & y <= 0 | x <= 0 & 0 <= y)";
103 by (auto_tac (claset() addDs [order_less_not_sym],
104 simpset() addsimps [int_0_less_mult_iff,
105 linorder_not_less RS sym]));
106 qed "zmult_le_0_iff";
108 Goal "abs (x * y) = abs x * abs (y::int)";
109 by (simp_tac (simpset () delsimps [thm "number_of_reorient"] addsplits [zabs_split]
110 addsplits [zabs_split]
111 addsimps [zmult_less_0_iff, zle_def]) 1);
114 Goal "(abs x = 0) = (x = (0::int))";
115 by (simp_tac (simpset () addsplits [zabs_split]) 1);
119 Goal "(0 < abs x) = (x ~= (0::int))";
120 by (simp_tac (simpset () addsplits [zabs_split]) 1);
122 qed "zero_less_abs_iff";
123 AddIffs [zero_less_abs_iff];
125 Goal "0 <= x * (x::int)";
126 by (subgoal_tac "(- x) * x <= 0" 1);
127 by (Asm_full_simp_tac 1);
128 by (simp_tac (HOL_basic_ss addsimps [zmult_le_0_iff]) 1);
130 qed "square_nonzero";
131 Addsimps [square_nonzero];
132 AddIs [square_nonzero];
135 (*** Products and 1, by T. M. Rasmussen ***)
137 Goal "(m = m*(n::int)) = (n = 1 | m = 0)";
139 by (subgoal_tac "m*1 = m*n" 1);
140 by (dtac (zmult_cancel1 RS iffD1) 1);
142 qed "zmult_eq_self_iff";
144 Goal "[| 1 < m; 1 < n |] ==> 1 < m*(n::int)";
145 by (res_inst_tac [("y","1*n")] order_less_trans 1);
146 by (rtac zmult_zless_mono1 2);
147 by (ALLGOALS Asm_simp_tac);
150 Goal "[| 0 < n; n ~= 1 |] ==> 1 < (n::int)";
152 val lemma = result();
154 Goal "0 < (m::int) ==> (m * n = 1) = (m = 1 & n = 1)";
156 by (case_tac "m=1" 1);
157 by (case_tac "n=1" 2);
158 by (case_tac "m=1" 4);
159 by (case_tac "n=1" 5);
161 by distinct_subgoals_tac;
162 by (subgoal_tac "1<m*n" 1);
163 by (Asm_full_simp_tac 1);
164 by (rtac zless_1_zmult 1);
165 by (ALLGOALS (rtac lemma));
167 by (subgoal_tac "0<m*n" 1);
169 by (dtac (int_0_less_mult_iff RS iffD1) 1);
171 qed "pos_zmult_eq_1_iff";
173 Goal "(m*n = (1::int)) = ((m = 1 & n = 1) | (m = -1 & n = -1))";
174 by (case_tac "0<m" 1);
175 by (asm_simp_tac (simpset() addsimps [pos_zmult_eq_1_iff]) 1);
176 by (case_tac "m=0" 1);
177 by (asm_simp_tac (simpset () delsimps [thm "number_of_reorient"]) 1);
178 by (subgoal_tac "0 < -m" 1);
180 by (dres_inst_tac [("n","-n")] pos_zmult_eq_1_iff 1);
182 qed "zmult_eq_1_iff";