author | paulson |
Thu, 30 Oct 2003 16:21:50 +0100 | |
changeset 14251 | b91f632a1d37 |
parent 13837 | 8dd150d36c65 |
permissions | -rw-r--r-- |
13588
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
1 |
(* Title: HOL/Integ/Int_lemmas.ML |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
2 |
ID: $Id$ |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
4 |
Copyright 1998 University of Cambridge |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
5 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
6 |
Type "int" is a linear order |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
7 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
8 |
And many further lemmas |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
9 |
*) |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
10 |
|
14251
b91f632a1d37
Got rid of the structure "Int", which was obsolete and which obscured the
paulson
parents:
13837
diff
changeset
|
11 |
(*Legacy ML bindings, but no longer the structure Int.*) |
b91f632a1d37
Got rid of the structure "Int", which was obsolete and which obscured the
paulson
parents:
13837
diff
changeset
|
12 |
val Int_thy = the_context (); |
b91f632a1d37
Got rid of the structure "Int", which was obsolete and which obscured the
paulson
parents:
13837
diff
changeset
|
13 |
val zabs_def = thm "zabs_def"; |
b91f632a1d37
Got rid of the structure "Int", which was obsolete and which obscured the
paulson
parents:
13837
diff
changeset
|
14 |
val nat_def = thm "nat_def"; |
13588
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
15 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
16 |
Goal "int 0 = (0::int)"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
17 |
by (simp_tac (simpset() addsimps [Zero_int_def]) 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
18 |
qed "int_0"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
19 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
20 |
Goal "int 1 = 1"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
21 |
by (simp_tac (simpset() addsimps [One_int_def]) 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
22 |
qed "int_1"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
23 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
24 |
Goal "int (Suc 0) = 1"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
25 |
by (simp_tac (simpset() addsimps [One_int_def, One_nat_def]) 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
26 |
qed "int_Suc0_eq_1"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
27 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
28 |
Goalw [zdiff_def,zless_def] "neg x = (x < 0)"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
29 |
by Auto_tac; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
30 |
qed "neg_eq_less_0"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
31 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
32 |
Goalw [zle_def] "(~neg x) = (0 <= x)"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
33 |
by (simp_tac (simpset() addsimps [neg_eq_less_0]) 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
34 |
qed "not_neg_eq_ge_0"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
35 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
36 |
(** Needed to simplify inequalities when Numeral1 can get simplified to 1 **) |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
37 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
38 |
Goal "~ neg 0"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
39 |
by (simp_tac (simpset() addsimps [One_int_def, neg_eq_less_0]) 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
40 |
qed "not_neg_0"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
41 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
42 |
Goal "~ neg 1"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
43 |
by (simp_tac (simpset() addsimps [One_int_def, neg_eq_less_0]) 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
44 |
qed "not_neg_1"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
45 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
46 |
Goal "iszero 0"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
47 |
by (simp_tac (simpset() addsimps [iszero_def]) 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
48 |
qed "iszero_0"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
49 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
50 |
Goal "~ iszero 1"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
51 |
by (simp_tac (simpset() addsimps [Zero_int_def, One_int_def, One_nat_def, |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
52 |
iszero_def]) 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
53 |
qed "not_iszero_1"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
54 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
55 |
Goal "0 < (1::int)"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
56 |
by (simp_tac (simpset() addsimps [Zero_int_def, One_int_def, One_nat_def]) 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
57 |
qed "int_0_less_1"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
58 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
59 |
Goal "0 \\<noteq> (1::int)"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
60 |
by (simp_tac (simpset() addsimps [Zero_int_def, One_int_def, One_nat_def]) 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
61 |
qed "int_0_neq_1"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
62 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
63 |
Addsimps [int_0, int_1, int_0_neq_1]; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
64 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
65 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
66 |
(*** Abel_Cancel simproc on the integers ***) |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
67 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
68 |
(* Lemmas needed for the simprocs *) |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
69 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
70 |
(*Deletion of other terms in the formula, seeking the -x at the front of z*) |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
71 |
Goal "((x::int) + (y + z) = y + u) = ((x + z) = u)"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
72 |
by (stac zadd_left_commute 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
73 |
by (rtac zadd_left_cancel 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
74 |
qed "zadd_cancel_21"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
75 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
76 |
(*A further rule to deal with the case that |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
77 |
everything gets cancelled on the right.*) |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
78 |
Goal "((x::int) + (y + z) = y) = (x = -z)"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
79 |
by (stac zadd_left_commute 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
80 |
by (res_inst_tac [("t", "y")] (zadd_0_right RS subst) 1 |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
81 |
THEN stac zadd_left_cancel 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
82 |
by (simp_tac (simpset() addsimps [eq_zdiff_eq RS sym]) 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
83 |
qed "zadd_cancel_end"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
84 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
85 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
86 |
structure Int_Cancel_Data = |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
87 |
struct |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
88 |
val ss = HOL_ss |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
89 |
val eq_reflection = eq_reflection |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
90 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
91 |
val sg_ref = Sign.self_ref (Theory.sign_of (the_context ())) |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
92 |
val T = HOLogic.intT |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
93 |
val zero = Const ("0", HOLogic.intT) |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
94 |
val restrict_to_left = restrict_to_left |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
95 |
val add_cancel_21 = zadd_cancel_21 |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
96 |
val add_cancel_end = zadd_cancel_end |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
97 |
val add_left_cancel = zadd_left_cancel |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
98 |
val add_assoc = zadd_assoc |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
99 |
val add_commute = zadd_commute |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
100 |
val add_left_commute = zadd_left_commute |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
101 |
val add_0 = zadd_0 |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
102 |
val add_0_right = zadd_0_right |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
103 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
104 |
val eq_diff_eq = eq_zdiff_eq |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
105 |
val eqI_rules = [zless_eqI, zeq_eqI, zle_eqI] |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
106 |
fun dest_eqI th = |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
107 |
#1 (HOLogic.dest_bin "op =" HOLogic.boolT |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
108 |
(HOLogic.dest_Trueprop (concl_of th))) |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
109 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
110 |
val diff_def = zdiff_def |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
111 |
val minus_add_distrib = zminus_zadd_distrib |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
112 |
val minus_minus = zminus_zminus |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
113 |
val minus_0 = zminus_0 |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
114 |
val add_inverses = [zadd_zminus_inverse, zadd_zminus_inverse2] |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
115 |
val cancel_simps = [zadd_zminus_cancel, zminus_zadd_cancel] |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
116 |
end; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
117 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
118 |
structure Int_Cancel = Abel_Cancel (Int_Cancel_Data); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
119 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
120 |
Addsimprocs [Int_Cancel.sum_conv, Int_Cancel.rel_conv]; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
121 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
122 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
123 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
124 |
(*** misc ***) |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
125 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
126 |
Goal "- (z - y) = y - (z::int)"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
127 |
by (Simp_tac 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
128 |
qed "zminus_zdiff_eq"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
129 |
Addsimps [zminus_zdiff_eq]; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
130 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
131 |
Goal "(w<z) = neg(w-z)"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
132 |
by (simp_tac (simpset() addsimps [zless_def]) 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
133 |
qed "zless_eq_neg"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
134 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
135 |
Goal "(w=z) = iszero(w-z)"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
136 |
by (simp_tac (simpset() addsimps [iszero_def, zdiff_eq_eq]) 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
137 |
qed "eq_eq_iszero"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
138 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
139 |
Goal "(w<=z) = (~ neg(z-w))"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
140 |
by (simp_tac (simpset() addsimps [zle_def, zless_def]) 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
141 |
qed "zle_eq_not_neg"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
142 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
143 |
(** Inequality reasoning **) |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
144 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
145 |
Goal "(w < z + (1::int)) = (w<z | w=z)"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
146 |
by (auto_tac (claset(), |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
147 |
simpset() addsimps [zless_iff_Suc_zadd, int_Suc, |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
148 |
gr0_conv_Suc, zero_reorient])); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
149 |
by (res_inst_tac [("x","Suc n")] exI 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
150 |
by (simp_tac (simpset() addsimps [int_Suc]) 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
151 |
qed "zless_add1_eq"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
152 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
153 |
Goal "(w + (1::int) <= z) = (w<z)"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
154 |
by (asm_full_simp_tac (simpset() addsimps [zle_def, zless_add1_eq]) 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
155 |
by (auto_tac (claset() addIs [zle_anti_sym], |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
156 |
simpset() addsimps [order_less_imp_le, symmetric zle_def])); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
157 |
qed "add1_zle_eq"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
158 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
159 |
Goal "((1::int) + w <= z) = (w<z)"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
160 |
by (stac zadd_commute 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
161 |
by (rtac add1_zle_eq 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
162 |
qed "add1_left_zle_eq"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
163 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
164 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
165 |
(*** Monotonicity results ***) |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
166 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
167 |
Goal "(v+z < w+z) = (v < (w::int))"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
168 |
by (Simp_tac 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
169 |
qed "zadd_right_cancel_zless"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
170 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
171 |
Goal "(z+v < z+w) = (v < (w::int))"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
172 |
by (Simp_tac 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
173 |
qed "zadd_left_cancel_zless"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
174 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
175 |
Addsimps [zadd_right_cancel_zless, zadd_left_cancel_zless]; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
176 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
177 |
Goal "(v+z <= w+z) = (v <= (w::int))"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
178 |
by (Simp_tac 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
179 |
qed "zadd_right_cancel_zle"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
180 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
181 |
Goal "(z+v <= z+w) = (v <= (w::int))"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
182 |
by (Simp_tac 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
183 |
qed "zadd_left_cancel_zle"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
184 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
185 |
Addsimps [zadd_right_cancel_zle, zadd_left_cancel_zle]; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
186 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
187 |
(*"v<=w ==> v+z <= w+z"*) |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
188 |
bind_thm ("zadd_zless_mono1", zadd_right_cancel_zless RS iffD2); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
189 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
190 |
(*"v<=w ==> z+v <= z+w"*) |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
191 |
bind_thm ("zadd_zless_mono2", zadd_left_cancel_zless RS iffD2); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
192 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
193 |
(*"v<=w ==> v+z <= w+z"*) |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
194 |
bind_thm ("zadd_zle_mono1", zadd_right_cancel_zle RS iffD2); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
195 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
196 |
(*"v<=w ==> z+v <= z+w"*) |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
197 |
bind_thm ("zadd_zle_mono2", zadd_left_cancel_zle RS iffD2); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
198 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
199 |
Goal "[| w'<=w; z'<=z |] ==> w' + z' <= w + (z::int)"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
200 |
by (etac (zadd_zle_mono1 RS zle_trans) 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
201 |
by (Simp_tac 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
202 |
qed "zadd_zle_mono"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
203 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
204 |
Goal "[| w'<w; z'<=z |] ==> w' + z' < w + (z::int)"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
205 |
by (etac (zadd_zless_mono1 RS order_less_le_trans) 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
206 |
by (Simp_tac 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
207 |
qed "zadd_zless_mono"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
208 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
209 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
210 |
(*** Comparison laws ***) |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
211 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
212 |
Goal "(- x < - y) = (y < (x::int))"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
213 |
by (simp_tac (simpset() addsimps [zless_def, zdiff_def] @ zadd_ac) 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
214 |
qed "zminus_zless_zminus"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
215 |
Addsimps [zminus_zless_zminus]; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
216 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
217 |
Goal "(- x <= - y) = (y <= (x::int))"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
218 |
by (simp_tac (simpset() addsimps [zle_def]) 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
219 |
qed "zminus_zle_zminus"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
220 |
Addsimps [zminus_zle_zminus]; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
221 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
222 |
(** The next several equations can make the simplifier loop! **) |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
223 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
224 |
Goal "(x < - y) = (y < - (x::int))"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
225 |
by (simp_tac (simpset() addsimps [zless_def, zdiff_def] @ zadd_ac) 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
226 |
qed "zless_zminus"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
227 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
228 |
Goal "(- x < y) = (- y < (x::int))"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
229 |
by (simp_tac (simpset() addsimps [zless_def, zdiff_def] @ zadd_ac) 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
230 |
qed "zminus_zless"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
231 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
232 |
Goal "(x <= - y) = (y <= - (x::int))"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
233 |
by (simp_tac (simpset() addsimps [zle_def, zminus_zless]) 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
234 |
qed "zle_zminus"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
235 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
236 |
Goal "(- x <= y) = (- y <= (x::int))"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
237 |
by (simp_tac (simpset() addsimps [zle_def, zless_zminus]) 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
238 |
qed "zminus_zle"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
239 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
240 |
Goal "(x = - y) = (y = - (x::int))"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
241 |
by Auto_tac; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
242 |
qed "equation_zminus"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
243 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
244 |
Goal "(- x = y) = (- (y::int) = x)"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
245 |
by Auto_tac; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
246 |
qed "zminus_equation"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
247 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
248 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
249 |
(** Instances of the equations above, for zero **) |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
250 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
251 |
(*instantiate a variable to zero and simplify*) |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
252 |
fun zero_instance v th = simplify (simpset()) (inst v "0" th); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
253 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
254 |
Addsimps [zero_instance "x" zless_zminus, |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
255 |
zero_instance "y" zminus_zless, |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
256 |
zero_instance "x" zle_zminus, |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
257 |
zero_instance "y" zminus_zle, |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
258 |
zero_instance "x" equation_zminus, |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
259 |
zero_instance "y" zminus_equation]; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
260 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
261 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
262 |
Goal "- (int (Suc n)) < 0"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
263 |
by (simp_tac (simpset() addsimps [zless_def]) 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
264 |
qed "negative_zless_0"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
265 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
266 |
Goal "- (int (Suc n)) < int m"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
267 |
by (rtac (negative_zless_0 RS order_less_le_trans) 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
268 |
by (Simp_tac 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
269 |
qed "negative_zless"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
270 |
AddIffs [negative_zless]; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
271 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
272 |
Goal "- int n <= 0"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
273 |
by (simp_tac (simpset() addsimps [zminus_zle]) 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
274 |
qed "negative_zle_0"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
275 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
276 |
Goal "- int n <= int m"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
277 |
by (simp_tac (simpset() addsimps [zless_def, zle_def, zdiff_def, zadd_int]) 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
278 |
qed "negative_zle"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
279 |
AddIffs [negative_zle]; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
280 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
281 |
Goal "~(0 <= - (int (Suc n)))"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
282 |
by (stac zle_zminus 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
283 |
by (Simp_tac 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
284 |
qed "not_zle_0_negative"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
285 |
Addsimps [not_zle_0_negative]; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
286 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
287 |
Goal "(int n <= - int m) = (n = 0 & m = 0)"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
288 |
by Safe_tac; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
289 |
by (Simp_tac 3); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
290 |
by (dtac (zle_zminus RS iffD1) 2); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
291 |
by (ALLGOALS (dtac (negative_zle_0 RSN(2,zle_trans)))); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
292 |
by (ALLGOALS Asm_full_simp_tac); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
293 |
qed "int_zle_neg"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
294 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
295 |
Goal "~(int n < - int m)"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
296 |
by (simp_tac (simpset() addsimps [symmetric zle_def]) 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
297 |
qed "not_int_zless_negative"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
298 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
299 |
Goal "(- int n = int m) = (n = 0 & m = 0)"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
300 |
by (rtac iffI 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
301 |
by (rtac (int_zle_neg RS iffD1) 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
302 |
by (dtac sym 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
303 |
by (ALLGOALS Asm_simp_tac); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
304 |
qed "negative_eq_positive"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
305 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
306 |
Addsimps [negative_eq_positive, not_int_zless_negative]; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
307 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
308 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
309 |
Goal "(w <= z) = (EX n. z = w + int n)"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
310 |
by (auto_tac (claset() addIs [inst "x" "0::nat" exI] |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
311 |
addSIs [not_sym RS not0_implies_Suc], |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
312 |
simpset() addsimps [zless_iff_Suc_zadd, int_le_less])); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
313 |
qed "zle_iff_zadd"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
314 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
315 |
Goal "abs (int m) = int m"; |
14251
b91f632a1d37
Got rid of the structure "Int", which was obsolete and which obscured the
paulson
parents:
13837
diff
changeset
|
316 |
by (simp_tac (simpset() addsimps [zabs_def]) 1); |
13588
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
317 |
qed "abs_int_eq"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
318 |
Addsimps [abs_int_eq]; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
319 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
320 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
321 |
(**** nat: magnitide of an integer, as a natural number ****) |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
322 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
323 |
Goalw [nat_def] "nat(int n) = n"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
324 |
by Auto_tac; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
325 |
qed "nat_int"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
326 |
Addsimps [nat_int]; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
327 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
328 |
Goalw [nat_def] "nat(- (int n)) = 0"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
329 |
by (auto_tac (claset(), |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
330 |
simpset() addsimps [neg_eq_less_0, zero_reorient, zminus_zless])); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
331 |
qed "nat_zminus_int"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
332 |
Addsimps [nat_zminus_int]; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
333 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
334 |
Goalw [Zero_int_def] "nat 0 = 0"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
335 |
by (rtac nat_int 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
336 |
qed "nat_zero"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
337 |
Addsimps [nat_zero]; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
338 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
339 |
Goal "~ neg z ==> int (nat z) = z"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
340 |
by (dtac (not_neg_eq_ge_0 RS iffD1) 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
341 |
by (dtac zle_imp_zless_or_eq 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
342 |
by (auto_tac (claset(), simpset() addsimps [zless_iff_Suc_zadd])); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
343 |
qed "not_neg_nat"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
344 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
345 |
Goal "neg x ==> EX n. x = - (int (Suc n))"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
346 |
by (auto_tac (claset(), |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
347 |
simpset() addsimps [neg_eq_less_0, zless_iff_Suc_zadd, |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
348 |
zdiff_eq_eq RS sym, zdiff_def])); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
349 |
qed "negD"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
350 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
351 |
Goalw [nat_def] "neg z ==> nat z = 0"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
352 |
by Auto_tac; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
353 |
qed "neg_nat"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
354 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
355 |
Goal "(m < nat z) = (int m < z)"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
356 |
by (case_tac "neg z" 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
357 |
by (etac (not_neg_nat RS subst) 2); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
358 |
by (auto_tac (claset(), simpset() addsimps [neg_nat])); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
359 |
by (auto_tac (claset() addDs [order_less_trans], |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
360 |
simpset() addsimps [neg_eq_less_0])); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
361 |
qed "zless_nat_eq_int_zless"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
362 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
363 |
Goal "0 <= z ==> int (nat z) = z"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
364 |
by (asm_full_simp_tac |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
365 |
(simpset() addsimps [neg_eq_less_0, zle_def, not_neg_nat]) 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
366 |
qed "nat_0_le"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
367 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
368 |
Goal "z <= 0 ==> nat z = 0"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
369 |
by (auto_tac (claset(), |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
370 |
simpset() addsimps [order_le_less, neg_eq_less_0, |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
371 |
zle_def, neg_nat])); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
372 |
qed "nat_le_0"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
373 |
Addsimps [nat_0_le, nat_le_0]; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
374 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
375 |
(*An alternative condition is 0 <= w *) |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
376 |
Goal "0 < z ==> (nat w < nat z) = (w < z)"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
377 |
by (stac (zless_int RS sym) 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
378 |
by (asm_simp_tac (simpset() addsimps [not_neg_nat, not_neg_eq_ge_0, |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
379 |
order_le_less]) 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
380 |
by (case_tac "neg w" 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
381 |
by (asm_simp_tac (simpset() addsimps [not_neg_nat]) 2); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
382 |
by (asm_full_simp_tac (simpset() addsimps [neg_eq_less_0, neg_nat]) 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
383 |
by (blast_tac (claset() addIs [order_less_trans]) 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
384 |
val lemma = result(); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
385 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
386 |
Goal "(nat w < nat z) = (0 < z & w < z)"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
387 |
by (case_tac "0 < z" 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
388 |
by (auto_tac (claset(), simpset() addsimps [lemma, linorder_not_less])); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
389 |
qed "zless_nat_conj"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
390 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
391 |
(* a case theorem distinguishing non-negative and negative int *) |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
392 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
393 |
val prems = Goal |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
394 |
"[|!! n. z = int n ==> P; !! n. z = - (int (Suc n)) ==> P |] ==> P"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
395 |
by (case_tac "neg z" 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
396 |
by (fast_tac (claset() addSDs [negD] addSEs prems) 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
397 |
by (dtac (not_neg_nat RS sym) 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
398 |
by (eresolve_tac prems 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
399 |
qed "int_cases"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
400 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
401 |
fun int_case_tac x = res_inst_tac [("z",x)] int_cases; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
402 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
403 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
404 |
(*** Monotonicity of Multiplication ***) |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
405 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
406 |
Goal "i <= (j::int) ==> i * int k <= j * int k"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
407 |
by (induct_tac "k" 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
408 |
by (stac int_Suc 2); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
409 |
by (ALLGOALS |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
410 |
(asm_simp_tac (simpset() addsimps [zadd_zmult_distrib2, zadd_zle_mono, |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
411 |
int_Suc0_eq_1]))); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
412 |
val lemma = result(); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
413 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
414 |
Goal "[| i <= j; (0::int) <= k |] ==> i*k <= j*k"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
415 |
by (res_inst_tac [("t", "k")] (not_neg_nat RS subst) 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
416 |
by (etac lemma 2); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
417 |
by (full_simp_tac (simpset() addsimps [not_neg_eq_ge_0]) 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
418 |
qed "zmult_zle_mono1"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
419 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
420 |
Goal "[| i <= j; k <= (0::int) |] ==> j*k <= i*k"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
421 |
by (rtac (zminus_zle_zminus RS iffD1) 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
422 |
by (asm_simp_tac (simpset() addsimps [zmult_zminus_right RS sym, |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
423 |
zmult_zle_mono1, zle_zminus]) 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
424 |
qed "zmult_zle_mono1_neg"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
425 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
426 |
Goal "[| i <= j; (0::int) <= k |] ==> k*i <= k*j"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
427 |
by (dtac zmult_zle_mono1 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
428 |
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [zmult_commute]))); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
429 |
qed "zmult_zle_mono2"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
430 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
431 |
Goal "[| i <= j; k <= (0::int) |] ==> k*j <= k*i"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
432 |
by (dtac zmult_zle_mono1_neg 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
433 |
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [zmult_commute]))); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
434 |
qed "zmult_zle_mono2_neg"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
435 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
436 |
(* <= monotonicity, BOTH arguments*) |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
437 |
Goal "[| i <= j; k <= l; (0::int) <= j; (0::int) <= k |] ==> i*k <= j*l"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
438 |
by (etac (zmult_zle_mono1 RS order_trans) 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
439 |
by (assume_tac 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
440 |
by (etac zmult_zle_mono2 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
441 |
by (assume_tac 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
442 |
qed "zmult_zle_mono"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
443 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
444 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
445 |
(** strict, in 1st argument; proof is by induction on k>0 **) |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
446 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
447 |
Goal "i<j ==> 0<k --> int k * i < int k * j"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
448 |
by (induct_tac "k" 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
449 |
by (stac int_Suc 2); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
450 |
by (case_tac "n=0" 2); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
451 |
by (ALLGOALS (asm_full_simp_tac |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
452 |
(simpset() addsimps [zadd_zmult_distrib, zadd_zless_mono, |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
453 |
int_Suc0_eq_1, order_le_less]))); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
454 |
val lemma = result(); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
455 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
456 |
Goal "[| i<j; (0::int) < k |] ==> k*i < k*j"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
457 |
by (res_inst_tac [("t", "k")] (not_neg_nat RS subst) 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
458 |
by (etac (lemma RS mp) 2); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
459 |
by (asm_simp_tac (simpset() addsimps [not_neg_eq_ge_0, |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
460 |
order_le_less]) 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
461 |
by (forward_tac [conjI RS (zless_nat_conj RS iffD2)] 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
462 |
by Auto_tac; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
463 |
qed "zmult_zless_mono2"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
464 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
465 |
Goal "[| i<j; (0::int) < k |] ==> i*k < j*k"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
466 |
by (dtac zmult_zless_mono2 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
467 |
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [zmult_commute]))); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
468 |
qed "zmult_zless_mono1"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
469 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
470 |
(* < monotonicity, BOTH arguments*) |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
471 |
Goal "[| i < j; k < l; (0::int) < j; (0::int) < k |] ==> i*k < j*l"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
472 |
by (etac (zmult_zless_mono1 RS order_less_trans) 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
473 |
by (assume_tac 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
474 |
by (etac zmult_zless_mono2 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
475 |
by (assume_tac 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
476 |
qed "zmult_zless_mono"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
477 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
478 |
Goal "[| i<j; k < (0::int) |] ==> j*k < i*k"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
479 |
by (rtac (zminus_zless_zminus RS iffD1) 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
480 |
by (asm_simp_tac (simpset() addsimps [zmult_zminus_right RS sym, |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
481 |
zmult_zless_mono1, zless_zminus]) 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
482 |
qed "zmult_zless_mono1_neg"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
483 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
484 |
Goal "[| i<j; k < (0::int) |] ==> k*j < k*i"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
485 |
by (rtac (zminus_zless_zminus RS iffD1) 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
486 |
by (asm_simp_tac (simpset() addsimps [zmult_zminus RS sym, |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
487 |
zmult_zless_mono2, zless_zminus]) 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
488 |
qed "zmult_zless_mono2_neg"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
489 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
490 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
491 |
Goal "(m*n = (0::int)) = (m = 0 | n = 0)"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
492 |
by (case_tac "m < (0::int)" 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
493 |
by (auto_tac (claset(), |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
494 |
simpset() addsimps [linorder_not_less, order_le_less, |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
495 |
linorder_neq_iff])); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
496 |
by (REPEAT |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
497 |
(force_tac (claset() addDs [zmult_zless_mono1_neg, zmult_zless_mono1], |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
498 |
simpset()) 1)); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
499 |
qed "zmult_eq_0_iff"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
500 |
AddIffs [zmult_eq_0_iff]; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
501 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
502 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
503 |
(** Cancellation laws for k*m < k*n and m*k < n*k, also for <= and =, |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
504 |
but not (yet?) for k*m < n*k. **) |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
505 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
506 |
Goal "(m*k < n*k) = (((0::int) < k & m<n) | (k < 0 & n<m))"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
507 |
by (case_tac "k = (0::int)" 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
508 |
by (auto_tac (claset(), simpset() addsimps [linorder_neq_iff, |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
509 |
zmult_zless_mono1, zmult_zless_mono1_neg])); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
510 |
by (auto_tac (claset(), |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
511 |
simpset() addsimps [linorder_not_less, |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
512 |
inst "y1" "m*k" (linorder_not_le RS sym), |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
513 |
inst "y1" "m" (linorder_not_le RS sym)])); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
514 |
by (ALLGOALS (etac notE)); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
515 |
by (auto_tac (claset(), simpset() addsimps [order_less_imp_le, zmult_zle_mono1, |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
516 |
zmult_zle_mono1_neg])); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
517 |
qed "zmult_zless_cancel2"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
518 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
519 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
520 |
Goal "(k*m < k*n) = (((0::int) < k & m<n) | (k < 0 & n<m))"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
521 |
by (simp_tac (simpset() addsimps [inst "z" "k" zmult_commute, |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
522 |
zmult_zless_cancel2]) 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
523 |
qed "zmult_zless_cancel1"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
524 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
525 |
Goal "(m*k <= n*k) = (((0::int) < k --> m<=n) & (k < 0 --> n<=m))"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
526 |
by (simp_tac (simpset() addsimps [linorder_not_less RS sym, |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
527 |
zmult_zless_cancel2]) 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
528 |
qed "zmult_zle_cancel2"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
529 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
530 |
Goal "(k*m <= k*n) = (((0::int) < k --> m<=n) & (k < 0 --> n<=m))"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
531 |
by (simp_tac (simpset() addsimps [linorder_not_less RS sym, |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
532 |
zmult_zless_cancel1]) 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
533 |
qed "zmult_zle_cancel1"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
534 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
535 |
Goal "(m*k = n*k) = (k = (0::int) | m=n)"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
536 |
by (cut_facts_tac [linorder_less_linear] 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
537 |
by Safe_tac; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
538 |
by Auto_tac; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
539 |
by (REPEAT |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
540 |
(force_tac (claset() addD2 ("mono_neg", zmult_zless_mono1_neg) |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
541 |
addD2 ("mono_pos", zmult_zless_mono1), |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
542 |
simpset() addsimps [linorder_neq_iff]) 1)); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
543 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
544 |
qed "zmult_cancel2"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
545 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
546 |
Goal "(k*m = k*n) = (k = (0::int) | m=n)"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
547 |
by (simp_tac (simpset() addsimps [inst "z" "k" zmult_commute, |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
548 |
zmult_cancel2]) 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
549 |
qed "zmult_cancel1"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
550 |
Addsimps [zmult_cancel1, zmult_cancel2]; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
551 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
552 |
|
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
553 |
(*Analogous to zadd_int*) |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
554 |
Goal "n<=m --> int m - int n = int (m-n)"; |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
555 |
by (induct_thm_tac diff_induct "m n" 1); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
556 |
by (auto_tac (claset(), simpset() addsimps [int_Suc, symmetric zdiff_def])); |
07b66a557487
Renamed Integ/int.ML to Integ/Int_lemmas.ML to prevent confusion with Int.ML
paulson
parents:
diff
changeset
|
557 |
qed_spec_mp "zdiff_int"; |