author | paulson |
Wed, 13 Sep 2000 18:47:30 +0200 | |
changeset 9945 | a0efbd7c88dc |
parent 9747 | 043098ba5098 |
child 10139 | 9fa7d3890488 |
permissions | -rw-r--r-- |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
1 |
(* Title: HOL/Integ/int_arith2.ML |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
2 |
ID: $Id$ |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
3 |
Authors: Larry Paulson and Tobias Nipkow |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
4 |
*) |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
5 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
6 |
(** Simplification of inequalities involving numerical constants **) |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
7 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
8 |
Goal "(w <= z - (#1::int)) = (w<(z::int))"; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
9 |
by (arith_tac 1); |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
10 |
qed "zle_diff1_eq"; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
11 |
Addsimps [zle_diff1_eq]; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
12 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
13 |
Goal "(w < z + #1) = (w<=(z::int))"; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
14 |
by (arith_tac 1); |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
15 |
qed "zle_add1_eq_le"; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
16 |
Addsimps [zle_add1_eq_le]; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
17 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
18 |
Goal "(z = z + w) = (w = (#0::int))"; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
19 |
by (arith_tac 1); |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
20 |
qed "zadd_left_cancel0"; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
21 |
Addsimps [zadd_left_cancel0]; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
22 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
23 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
24 |
(* nat *) |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
25 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
26 |
Goal "#0 <= z ==> int (nat z) = z"; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
27 |
by (asm_full_simp_tac |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
28 |
(simpset() addsimps [neg_eq_less_0, zle_def, not_neg_nat]) 1); |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
29 |
qed "nat_0_le"; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
30 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
31 |
Goal "z <= #0 ==> nat z = 0"; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
32 |
by (case_tac "z = #0" 1); |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
33 |
by (asm_simp_tac (simpset() addsimps [nat_le_int0]) 1); |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
34 |
by (asm_full_simp_tac |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
35 |
(simpset() addsimps [neg_eq_less_0, neg_nat, linorder_neq_iff]) 1); |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
36 |
qed "nat_le_0"; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
37 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
38 |
Addsimps [nat_0_le, nat_le_0]; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
39 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
40 |
val [major,minor] = Goal "[| #0 <= z; !!m. z = int m ==> P |] ==> P"; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
41 |
by (rtac (major RS nat_0_le RS sym RS minor) 1); |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
42 |
qed "nonneg_eq_int"; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
43 |
|
9945 | 44 |
Goal "(nat w = m) = (if #0 <= w then w = int m else m=0)"; |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
45 |
by Auto_tac; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
46 |
qed "nat_eq_iff"; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
47 |
|
9945 | 48 |
Goal "(m = nat w) = (if #0 <= w then w = int m else m=0)"; |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
49 |
by Auto_tac; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
50 |
qed "nat_eq_iff2"; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
51 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
52 |
Goal "#0 <= w ==> (nat w < m) = (w < int m)"; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
53 |
by (rtac iffI 1); |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
54 |
by (asm_full_simp_tac |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
55 |
(simpset() delsimps [zless_int] addsimps [zless_int RS sym]) 2); |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
56 |
by (etac (nat_0_le RS subst) 1); |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
57 |
by (Simp_tac 1); |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
58 |
qed "nat_less_iff"; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
59 |
|
9945 | 60 |
Goal "(int m = z) = (m = nat z & #0 \\<le> z)"; |
61 |
by (auto_tac (claset(), simpset() addsimps [nat_eq_iff2])); |
|
62 |
qed "int_eq_iff"; |
|
63 |
||
64 |
Addsimps [inst "z" "number_of ?v" int_eq_iff]; |
|
65 |
||
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
66 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
67 |
(*Users don't want to see (int 0), int(Suc 0) or w + - z*) |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
68 |
Addsimps [int_0, int_Suc, symmetric zdiff_def]; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
69 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
70 |
Goal "nat #0 = 0"; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
71 |
by (simp_tac (simpset() addsimps [nat_eq_iff]) 1); |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
72 |
qed "nat_0"; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
73 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
74 |
Goal "nat #1 = 1"; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
75 |
by (simp_tac (simpset() addsimps [nat_eq_iff]) 1); |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
76 |
qed "nat_1"; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
77 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
78 |
Goal "nat #2 = 2"; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
79 |
by (simp_tac (simpset() addsimps [nat_eq_iff]) 1); |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
80 |
qed "nat_2"; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
81 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
82 |
Goal "#0 <= w ==> (nat w < nat z) = (w<z)"; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
83 |
by (case_tac "neg z" 1); |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
84 |
by (auto_tac (claset(), simpset() addsimps [nat_less_iff])); |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
85 |
by (auto_tac (claset() addIs [zless_trans], |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
86 |
simpset() addsimps [neg_eq_less_0, zle_def])); |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
87 |
qed "nat_less_eq_zless"; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
88 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
89 |
Goal "#0 < w | #0 <= z ==> (nat w <= nat z) = (w<=z)"; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
90 |
by (auto_tac (claset(), |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
91 |
simpset() addsimps [linorder_not_less RS sym, |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
92 |
zless_nat_conj])); |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
93 |
qed "nat_le_eq_zle"; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
94 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
95 |
(*Analogous to zadd_int, but more easily provable using the arithmetic in Bin*) |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
96 |
Goal "n<=m --> int m - int n = int (m-n)"; |
9747 | 97 |
by (induct_thm_tac diff_induct "m n" 1); |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
98 |
by Auto_tac; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
99 |
qed_spec_mp "zdiff_int"; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
100 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
101 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
102 |
(*** abs: absolute value, as an integer ****) |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
103 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
104 |
(* Simpler: use zabs_def as rewrite rule; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
105 |
but arith_tac is not parameterized by such simp rules |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
106 |
*) |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
107 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
108 |
Goalw [zabs_def] |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
109 |
"P(abs(i::int)) = ((#0 <= i --> P i) & (i < #0 --> P(-i)))"; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
110 |
by(Simp_tac 1); |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
111 |
qed "zabs_split"; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
112 |
|
9945 | 113 |
Goal "#0 <= abs (z::int)"; |
114 |
by (simp_tac (simpset() addsimps [zabs_def]) 1); |
|
115 |
qed "zero_le_zabs"; |
|
116 |
AddIffs [zero_le_zabs]; |
|
117 |
||
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
118 |
(*continued in IntArith.ML ...*) |