author | paulson |
Thu, 07 Sep 2000 17:36:37 +0200 | |
changeset 9883 | c1c8647af477 |
parent 9648 | 35d761c7d934 |
child 9955 | 6ed42bcba707 |
permissions | -rw-r--r-- |
9578
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1 |
(* Title: HOL/IntDiv.ML |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
2 |
ID: $Id$ |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
4 |
Copyright 1999 University of Cambridge |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
5 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
6 |
The division operators div, mod and the divides relation "dvd" |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
7 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
8 |
Here is the division algorithm in ML: |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
9 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
10 |
fun posDivAlg (a,b) = |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
11 |
if a<b then (0,a) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
12 |
else let val (q,r) = posDivAlg(a, 2*b) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
13 |
in if 0<=r-b then (2*q+1, r-b) else (2*q, r) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
14 |
end; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
15 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
16 |
fun negDivAlg (a,b) = |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
17 |
if 0<=a+b then (~1,a+b) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
18 |
else let val (q,r) = negDivAlg(a, 2*b) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
19 |
in if 0<=r-b then (2*q+1, r-b) else (2*q, r) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
20 |
end; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
21 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
22 |
fun negateSnd (q,r:int) = (q,~r); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
23 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
24 |
fun divAlg (a,b) = if 0<=a then |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
25 |
if b>0 then posDivAlg (a,b) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
26 |
else if a=0 then (0,0) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
27 |
else negateSnd (negDivAlg (~a,~b)) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
28 |
else |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
29 |
if 0<b then negDivAlg (a,b) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
30 |
else negateSnd (posDivAlg (~a,~b)); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
31 |
*) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
32 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
33 |
Goal "[| #0 $< k; k: int |] ==> 0 < zmagnitude(k)"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
34 |
by (dtac zero_zless_imp_znegative_zminus 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
35 |
by (dtac zneg_int_of 2); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
36 |
by (auto_tac (claset(), simpset() addsimps [inst "x" "k" zminus_equation])); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
37 |
by (subgoal_tac "0 < zmagnitude($# succ(x))" 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
38 |
by (Asm_full_simp_tac 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
39 |
by (asm_full_simp_tac (simpset_of Arith.thy addsimps [zmagnitude_int_of]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
40 |
qed "zero_lt_zmagnitude"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
41 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
42 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
43 |
(*** Inequality lemmas involving $#succ(m) ***) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
44 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
45 |
Goal "(w $< z $+ $# succ(m)) <-> (w $< z $+ $#m | intify(w) = z $+ $#m)"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
46 |
by (auto_tac (claset(), |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
47 |
simpset() addsimps [zless_iff_succ_zadd, zadd_assoc, |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
48 |
int_of_add RS sym])); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
49 |
by (res_inst_tac [("x","0")] bexI 3); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
50 |
by (TRYALL (dtac sym)); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
51 |
by (cut_inst_tac [("m","m")] int_succ_int_1 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
52 |
by (cut_inst_tac [("m","n")] int_succ_int_1 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
53 |
by (Asm_full_simp_tac 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
54 |
by (eres_inst_tac [("n","x")] natE 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
55 |
by Auto_tac; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
56 |
by (res_inst_tac [("x","succ(x)")] bexI 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
57 |
by Auto_tac; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
58 |
qed "zless_add_succ_iff"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
59 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
60 |
Goal "z : int ==> (w $+ $# succ(m) $<= z) <-> (w $+ $#m $< z)"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
61 |
by (asm_simp_tac (simpset_of Int.thy addsimps |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
62 |
[not_zless_iff_zle RS iff_sym, zless_add_succ_iff]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
63 |
by (auto_tac (claset() addIs [zle_anti_sym] addEs [zless_asym], |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
64 |
simpset() addsimps [zless_imp_zle, not_zless_iff_zle])); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
65 |
qed "lemma"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
66 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
67 |
Goal "(w $+ $# succ(m) $<= z) <-> (w $+ $#m $< z)"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
68 |
by (cut_inst_tac [("z","intify(z)")] lemma 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
69 |
by Auto_tac; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
70 |
qed "zadd_succ_zle_iff"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
71 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
72 |
(** Inequality reasoning **) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
73 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
74 |
Goal "(w $< z $+ #1) <-> (w$<=z)"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
75 |
by (subgoal_tac "#1 = $# 1" 1); |
9648
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
76 |
by (asm_simp_tac (simpset_of Int.thy |
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
77 |
addsimps [zless_add_succ_iff, zle_def]) 1); |
9578
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
78 |
by Auto_tac; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
79 |
qed "zless_add1_iff_zle"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
80 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
81 |
Goal "(w $+ #1 $<= z) <-> (w $< z)"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
82 |
by (subgoal_tac "#1 = $# 1" 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
83 |
by (asm_simp_tac (simpset_of Int.thy addsimps [zadd_succ_zle_iff]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
84 |
by Auto_tac; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
85 |
qed "add1_zle_iff"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
86 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
87 |
Goal "(#1 $+ w $<= z) <-> (w $< z)"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
88 |
by (stac zadd_commute 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
89 |
by (rtac add1_zle_iff 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
90 |
qed "add1_left_zle_iff"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
91 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
92 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
93 |
(*** Monotonicity results ***) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
94 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
95 |
Goal "(v$+z $< w$+z) <-> (v $< w)"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
96 |
by (Simp_tac 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
97 |
qed "zadd_right_cancel_zless"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
98 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
99 |
Goal "(z$+v $< z$+w) <-> (v $< w)"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
100 |
by (Simp_tac 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
101 |
qed "zadd_left_cancel_zless"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
102 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
103 |
Addsimps [zadd_right_cancel_zless, zadd_left_cancel_zless]; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
104 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
105 |
Goal "(v$+z $<= w$+z) <-> (v $<= w)"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
106 |
by (Simp_tac 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
107 |
qed "zadd_right_cancel_zle"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
108 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
109 |
Goal "(z$+v $<= z$+w) <-> (v $<= w)"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
110 |
by (Simp_tac 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
111 |
qed "zadd_left_cancel_zle"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
112 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
113 |
Addsimps [zadd_right_cancel_zle, zadd_left_cancel_zle]; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
114 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
115 |
(*"v $<= w ==> v$+z $<= w$+z"*) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
116 |
bind_thm ("zadd_zless_mono1", zadd_right_cancel_zless RS iffD2); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
117 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
118 |
(*"v $<= w ==> z$+v $<= z$+w"*) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
119 |
bind_thm ("zadd_zless_mono2", zadd_left_cancel_zless RS iffD2); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
120 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
121 |
(*"v $<= w ==> v$+z $<= w$+z"*) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
122 |
bind_thm ("zadd_zle_mono1", zadd_right_cancel_zle RS iffD2); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
123 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
124 |
(*"v $<= w ==> z$+v $<= z$+w"*) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
125 |
bind_thm ("zadd_zle_mono2", zadd_left_cancel_zle RS iffD2); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
126 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
127 |
Goal "[| w' $<= w; z' $<= z |] ==> w' $+ z' $<= w $+ z"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
128 |
by (etac (zadd_zle_mono1 RS zle_trans) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
129 |
by (Simp_tac 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
130 |
qed "zadd_zle_mono"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
131 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
132 |
Goal "[| w' $< w; z' $<= z |] ==> w' $+ z' $< w $+ z"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
133 |
by (etac (zadd_zless_mono1 RS zless_zle_trans) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
134 |
by (Simp_tac 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
135 |
qed "zadd_zless_mono"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
136 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
137 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
138 |
(*** Monotonicity of Multiplication ***) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
139 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
140 |
Goal "k : nat ==> i $<= j ==> i $* $#k $<= j $* $#k"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
141 |
by (induct_tac "k" 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
142 |
by (stac int_succ_int_1 2); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
143 |
by (ALLGOALS |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
144 |
(asm_simp_tac (simpset() addsimps [zadd_zmult_distrib2, zadd_zle_mono]))); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
145 |
val lemma = result(); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
146 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
147 |
Goal "[| i $<= j; #0 $<= k |] ==> i$*k $<= j$*k"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
148 |
by (subgoal_tac "i $* intify(k) $<= j $* intify(k)" 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
149 |
by (Full_simp_tac 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
150 |
by (res_inst_tac [("b", "intify(k)")] (not_zneg_mag RS subst) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
151 |
by (rtac lemma 3); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
152 |
by Auto_tac; |
9883 | 153 |
by (asm_full_simp_tac (simpset() addsimps [znegative_iff_zless_0, |
154 |
not_zless_iff_zle RS iff_sym]) 1); |
|
9578
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
155 |
qed "zmult_zle_mono1"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
156 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
157 |
Goal "[| i $<= j; k $<= #0 |] ==> j$*k $<= i$*k"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
158 |
by (rtac (zminus_zle_zminus RS iffD1) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
159 |
by (asm_simp_tac (simpset() delsimps [zmult_zminus_right] |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
160 |
addsimps [zmult_zminus_right RS sym, |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
161 |
zmult_zle_mono1, zle_zminus]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
162 |
qed "zmult_zle_mono1_neg"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
163 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
164 |
Goal "[| i $<= j; #0 $<= k |] ==> k$*i $<= k$*j"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
165 |
by (dtac zmult_zle_mono1 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
166 |
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [zmult_commute]))); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
167 |
qed "zmult_zle_mono2"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
168 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
169 |
Goal "[| i $<= j; k $<= #0 |] ==> k$*j $<= k$*i"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
170 |
by (dtac zmult_zle_mono1_neg 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
171 |
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [zmult_commute]))); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
172 |
qed "zmult_zle_mono2_neg"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
173 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
174 |
(* $<= monotonicity, BOTH arguments*) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
175 |
Goal "[| i $<= j; k $<= l; #0 $<= j; #0 $<= k |] ==> i$*k $<= j$*l"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
176 |
by (etac (zmult_zle_mono1 RS zle_trans) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
177 |
by (assume_tac 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
178 |
by (etac zmult_zle_mono2 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
179 |
by (assume_tac 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
180 |
qed "zmult_zle_mono"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
181 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
182 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
183 |
(** strict, in 1st argument; proof is by induction on k>0 **) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
184 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
185 |
Goal "[| i$<j; k : nat |] ==> 0<k --> $#k $* i $< $#k $* j"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
186 |
by (induct_tac "k" 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
187 |
by (stac int_succ_int_1 2); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
188 |
by (etac natE 2); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
189 |
by (ALLGOALS (asm_full_simp_tac |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
190 |
(simpset() addsimps [zadd_zmult_distrib, zadd_zless_mono, |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
191 |
zle_def]))); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
192 |
by (ftac nat_0_le 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
193 |
by (mp_tac 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
194 |
by (subgoal_tac "i $+ (i $+ $# xa $* i) $< j $+ (j $+ $# xa $* j)" 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
195 |
by (Full_simp_tac 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
196 |
by (rtac zadd_zless_mono 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
197 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [zle_def]))); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
198 |
val lemma = result() RS mp; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
199 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
200 |
Goal "[| i$<j; #0 $< k |] ==> k$*i $< k$*j"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
201 |
by (subgoal_tac "intify(k) $* i $< intify(k) $* j" 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
202 |
by (Full_simp_tac 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
203 |
by (res_inst_tac [("b", "intify(k)")] (not_zneg_mag RS subst) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
204 |
by (rtac lemma 3); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
205 |
by Auto_tac; |
9883 | 206 |
by (asm_full_simp_tac (simpset() addsimps [znegative_iff_zless_0]) 1); |
207 |
by (dtac zless_trans 1 THEN assume_tac 1); |
|
9578
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
208 |
by (auto_tac (claset(), simpset() addsimps [zero_lt_zmagnitude])); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
209 |
qed "zmult_zless_mono2"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
210 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
211 |
Goal "[| i$<j; #0 $< k |] ==> i$*k $< j$*k"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
212 |
by (dtac zmult_zless_mono2 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
213 |
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [zmult_commute]))); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
214 |
qed "zmult_zless_mono1"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
215 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
216 |
(* < monotonicity, BOTH arguments*) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
217 |
Goal "[| i $< j; k $< l; #0 $< j; #0 $< k |] ==> i$*k $< j$*l"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
218 |
by (etac (zmult_zless_mono1 RS zless_trans) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
219 |
by (assume_tac 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
220 |
by (etac zmult_zless_mono2 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
221 |
by (assume_tac 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
222 |
qed "zmult_zless_mono"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
223 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
224 |
Goal "[| i $< j; k $< #0 |] ==> j$*k $< i$*k"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
225 |
by (rtac (zminus_zless_zminus RS iffD1) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
226 |
by (asm_simp_tac (simpset() delsimps [zmult_zminus_right] |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
227 |
addsimps [zmult_zminus_right RS sym, |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
228 |
zmult_zless_mono1, zless_zminus]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
229 |
qed "zmult_zless_mono1_neg"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
230 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
231 |
Goal "[| i $< j; k $< #0 |] ==> k$*j $< k$*i"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
232 |
by (rtac (zminus_zless_zminus RS iffD1) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
233 |
by (asm_simp_tac (simpset() delsimps [zmult_zminus] |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
234 |
addsimps [zmult_zminus RS sym, |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
235 |
zmult_zless_mono2, zless_zminus]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
236 |
qed "zmult_zless_mono2_neg"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
237 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
238 |
Goal "[| m: int; n: int |] ==> (m$*n = #0) <-> (m = #0 | n = #0)"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
239 |
by (case_tac "m $< #0" 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
240 |
by (auto_tac (claset(), |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
241 |
simpset() addsimps [not_zless_iff_zle, zle_def, neq_iff_zless])); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
242 |
by (REPEAT |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
243 |
(force_tac (claset() addDs [zmult_zless_mono1_neg, zmult_zless_mono1], |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
244 |
simpset()) 1)); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
245 |
val lemma = result(); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
246 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
247 |
Goal "(m$*n = #0) <-> (intify(m) = #0 | intify(n) = #0)"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
248 |
by (asm_full_simp_tac (simpset() addsimps [lemma RS iff_sym]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
249 |
qed "zmult_eq_0_iff"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
250 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
251 |
|
9648
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
252 |
(** Cancellation laws for k*m < k*n and m*k < n*k, also for <= and =, |
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
253 |
but not (yet?) for k*m < n*k. **) |
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
254 |
|
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
255 |
Goal "[| k: int; m: int; n: int |] \ |
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
256 |
\ ==> (m$*k $< n$*k) <-> ((#0 $< k & m$<n) | (k $< #0 & n$<m))"; |
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
257 |
by (case_tac "k = #0" 1); |
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
258 |
by (auto_tac (claset(), simpset() addsimps [neq_iff_zless, |
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
259 |
zmult_zless_mono1, zmult_zless_mono1_neg])); |
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
260 |
by (auto_tac (claset(), |
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
261 |
simpset() addsimps [not_zless_iff_zle, |
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
262 |
inst "w1" "m$*k" (not_zle_iff_zless RS iff_sym), |
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
263 |
inst "w1" "m" (not_zle_iff_zless RS iff_sym)])); |
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
264 |
by (ALLGOALS (etac notE)); |
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
265 |
by (auto_tac (claset(), simpset() addsimps [zless_imp_zle, zmult_zle_mono1, |
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
266 |
zmult_zle_mono1_neg])); |
9578
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
267 |
val lemma = result(); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
268 |
|
9648
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
269 |
Goal "(m$*k $< n$*k) <-> ((#0 $< k & m$<n) | (k $< #0 & n$<m))"; |
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
270 |
by (cut_inst_tac [("k","intify(k)"),("m","intify(m)"),("n","intify(n)")] |
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
271 |
lemma 1); |
9578
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
272 |
by Auto_tac; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
273 |
qed "zmult_zless_cancel2"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
274 |
|
9648
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
275 |
Goal "(k$*m $< k$*n) <-> ((#0 $< k & m$<n) | (k $< #0 & n$<m))"; |
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
276 |
by (simp_tac (simpset() addsimps [inst "z" "k" zmult_commute, |
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
277 |
zmult_zless_cancel2]) 1); |
9578
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
278 |
qed "zmult_zless_cancel1"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
279 |
|
9648
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
280 |
Goal "(m$*k $<= n$*k) <-> ((#0 $< k --> m$<=n) & (k $< #0 --> n$<=m))"; |
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
281 |
by (simp_tac (simpset() addsimps [not_zless_iff_zle RS iff_sym, |
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
282 |
zmult_zless_cancel2]) 1); |
9578
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
283 |
by Auto_tac; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
284 |
qed "zmult_zle_cancel2"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
285 |
|
9648
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
286 |
Goal "(k$*m $<= k$*n) <-> ((#0 $< k --> m$<=n) & (k $< #0 --> n$<=m))"; |
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
287 |
by (simp_tac (simpset() addsimps [not_zless_iff_zle RS iff_sym, |
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
288 |
zmult_zless_cancel1]) 1); |
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
289 |
by Auto_tac; |
9578
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
290 |
qed "zmult_zle_cancel1"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
291 |
|
9648
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
292 |
Goal "[| m: int; n: int |] ==> m=n <-> (m $<= n & n $<= m)"; |
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
293 |
by (blast_tac (claset() addIs [zle_refl,zle_anti_sym]) 1); |
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
294 |
qed "int_eq_iff_zle"; |
9578
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
295 |
|
9648
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
296 |
Goal "[| k: int; m: int; n: int |] ==> (m$*k = n$*k) <-> (k=#0 | m=n)"; |
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
297 |
by (asm_simp_tac (simpset() addsimps [inst "m" "m$*k" int_eq_iff_zle, |
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
298 |
inst "m" "m" int_eq_iff_zle]) 1); |
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
299 |
by (auto_tac (claset(), |
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
300 |
simpset() addsimps [zmult_zle_cancel2, neq_iff_zless])); |
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
301 |
val lemma = result(); |
9578
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
302 |
|
9648
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
303 |
Goal "(m$*k = n$*k) <-> (intify(k) = #0 | intify(m) = intify(n))"; |
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
304 |
by (rtac iff_trans 1); |
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
305 |
by (rtac lemma 2); |
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
306 |
by Auto_tac; |
9578
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
307 |
qed "zmult_cancel2"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
308 |
|
9648
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
309 |
Goal "(k$*m = k$*n) <-> (intify(k) = #0 | intify(m) = intify(n))"; |
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
310 |
by (simp_tac (simpset() addsimps [inst "z" "k" zmult_commute, |
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
311 |
zmult_cancel2]) 1); |
9578
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
312 |
qed "zmult_cancel1"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
313 |
Addsimps [zmult_cancel1, zmult_cancel2]; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
314 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
315 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
316 |
(*** Uniqueness and monotonicity of quotients and remainders ***) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
317 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
318 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
319 |
Goal "[| b$*q' $+ r' $<= b$*q $+ r; #0 $<= r'; #0 $< b; r $< b |] \ |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
320 |
\ ==> q' $<= q"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
321 |
by (subgoal_tac "r' $+ b $* (q'$-q) $<= r" 1); |
9648
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
322 |
by (full_simp_tac |
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
323 |
(simpset() addsimps [zdiff_zmult_distrib2]@zadd_ac@zcompare_rls) 2); |
9578
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
324 |
by (subgoal_tac "#0 $< b $* (#1 $+ q $- q')" 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
325 |
by (etac zle_zless_trans 2); |
9648
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
326 |
by (full_simp_tac |
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
327 |
(simpset() addsimps [zdiff_zmult_distrib2, |
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
328 |
zadd_zmult_distrib2]@zadd_ac@zcompare_rls) 2); |
9578
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
329 |
by (etac zle_zless_trans 2); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
330 |
by (Asm_simp_tac 2); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
331 |
by (subgoal_tac "b $* q' $< b $* (#1 $+ q)" 1); |
9648
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
332 |
by (full_simp_tac |
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
333 |
(simpset() addsimps [zdiff_zmult_distrib2, |
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
334 |
zadd_zmult_distrib2]@zadd_ac@zcompare_rls) 2); |
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
335 |
by (auto_tac (claset() addEs [zless_asym], |
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
336 |
simpset() addsimps [zmult_zless_cancel1, zless_add1_iff_zle]@ |
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
337 |
zadd_ac@zcompare_rls)); |
9578
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
338 |
qed "unique_quotient_lemma"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
339 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
340 |
Goal "[| b$*q' $+ r' $<= b$*q $+ r; r $<= #0; b $< #0; b $< r' |] \ |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
341 |
\ ==> q $<= q'"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
342 |
by (res_inst_tac [("b", "$-b"), ("r", "$-r'"), ("r'", "$-r")] |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
343 |
unique_quotient_lemma 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
344 |
by (auto_tac (claset(), |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
345 |
simpset() delsimps [zminus_zadd_distrib] |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
346 |
addsimps [zminus_zadd_distrib RS sym, |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
347 |
zle_zminus, zless_zminus])); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
348 |
qed "unique_quotient_lemma_neg"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
349 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
350 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
351 |
Goal "[| quorem (<a,b>, <q,r>); quorem (<a,b>, <q',r'>); b: int; b ~= #0; \ |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
352 |
\ q: int; q' : int |] ==> q = q'"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
353 |
by (asm_full_simp_tac |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
354 |
(simpset() addsimps split_ifs@ |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
355 |
[quorem_def, neq_iff_zless]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
356 |
by Safe_tac; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
357 |
by (ALLGOALS Asm_full_simp_tac); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
358 |
by (REPEAT |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
359 |
(blast_tac (claset() addIs [zle_anti_sym] |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
360 |
addDs [zle_eq_refl RS unique_quotient_lemma, |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
361 |
zle_eq_refl RS unique_quotient_lemma_neg, |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
362 |
sym]) 1)); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
363 |
qed "unique_quotient"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
364 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
365 |
Goal "[| quorem (<a,b>, <q,r>); quorem (<a,b>, <q',r'>); b: int; b ~= #0; \ |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
366 |
\ q: int; q' : int; \ |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
367 |
\ r: int; r' : int |] ==> r = r'"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
368 |
by (subgoal_tac "q = q'" 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
369 |
by (blast_tac (claset() addIs [unique_quotient]) 2); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
370 |
by (asm_full_simp_tac (simpset() addsimps [quorem_def]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
371 |
by Auto_tac; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
372 |
qed "unique_remainder"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
373 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
374 |