author | wenzelm |
Sat, 02 Sep 2000 21:51:14 +0200 | |
changeset 9805 | 10b617bdd028 |
parent 9648 | 35d761c7d934 |
child 9883 | c1c8647af477 |
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; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
153 |
by (dtac znegative_imp_zless_0 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
154 |
by (dtac zless_zle_trans 2); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
155 |
by Auto_tac; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
156 |
qed "zmult_zle_mono1"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
157 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
158 |
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
|
159 |
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
|
160 |
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
|
161 |
addsimps [zmult_zminus_right RS sym, |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
162 |
zmult_zle_mono1, zle_zminus]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
163 |
qed "zmult_zle_mono1_neg"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
164 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
165 |
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
|
166 |
by (dtac zmult_zle_mono1 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
167 |
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
|
168 |
qed "zmult_zle_mono2"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
169 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
170 |
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
|
171 |
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
|
172 |
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
|
173 |
qed "zmult_zle_mono2_neg"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
174 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
175 |
(* $<= monotonicity, BOTH arguments*) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
176 |
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
|
177 |
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
|
178 |
by (assume_tac 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
179 |
by (etac zmult_zle_mono2 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
180 |
by (assume_tac 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
181 |
qed "zmult_zle_mono"; |
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 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
184 |
(** 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
|
185 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
186 |
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
|
187 |
by (induct_tac "k" 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
188 |
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
|
189 |
by (etac natE 2); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
190 |
by (ALLGOALS (asm_full_simp_tac |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
191 |
(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
|
192 |
zle_def]))); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
193 |
by (ftac nat_0_le 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
194 |
by (mp_tac 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
195 |
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
|
196 |
by (Full_simp_tac 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
197 |
by (rtac zadd_zless_mono 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
198 |
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
|
199 |
val lemma = result() RS mp; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
200 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
201 |
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
|
202 |
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
|
203 |
by (Full_simp_tac 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
204 |
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
|
205 |
by (rtac lemma 3); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
206 |
by Auto_tac; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
207 |
by (dtac znegative_imp_zless_0 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
208 |
by (dtac zless_trans 2 THEN assume_tac 2); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
209 |
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
|
210 |
qed "zmult_zless_mono2"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
211 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
212 |
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
|
213 |
by (dtac zmult_zless_mono2 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
214 |
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
|
215 |
qed "zmult_zless_mono1"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
216 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
217 |
(* < monotonicity, BOTH arguments*) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
218 |
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
|
219 |
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
|
220 |
by (assume_tac 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
221 |
by (etac zmult_zless_mono2 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
222 |
by (assume_tac 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
223 |
qed "zmult_zless_mono"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
224 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
225 |
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
|
226 |
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
|
227 |
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
|
228 |
addsimps [zmult_zminus_right RS sym, |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
229 |
zmult_zless_mono1, zless_zminus]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
230 |
qed "zmult_zless_mono1_neg"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
231 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
232 |
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
|
233 |
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
|
234 |
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
|
235 |
addsimps [zmult_zminus RS sym, |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
236 |
zmult_zless_mono2, zless_zminus]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
237 |
qed "zmult_zless_mono2_neg"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
238 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
239 |
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
|
240 |
by (case_tac "m $< #0" 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
241 |
by (auto_tac (claset(), |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
242 |
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
|
243 |
by (REPEAT |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
244 |
(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
|
245 |
simpset()) 1)); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
246 |
val lemma = result(); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
247 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
248 |
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
|
249 |
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
|
250 |
qed "zmult_eq_0_iff"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
251 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
252 |
|
9648
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
253 |
(** 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
|
254 |
but not (yet?) for k*m < n*k. **) |
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
255 |
|
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
256 |
Goal "[| k: int; m: int; n: int |] \ |
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
257 |
\ ==> (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
|
258 |
by (case_tac "k = #0" 1); |
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
259 |
by (auto_tac (claset(), simpset() addsimps [neq_iff_zless, |
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
260 |
zmult_zless_mono1, zmult_zless_mono1_neg])); |
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
261 |
by (auto_tac (claset(), |
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
262 |
simpset() addsimps [not_zless_iff_zle, |
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
263 |
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
|
264 |
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
|
265 |
by (ALLGOALS (etac notE)); |
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
266 |
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
|
267 |
zmult_zle_mono1_neg])); |
9578
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
268 |
val lemma = result(); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
269 |
|
9648
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
270 |
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
|
271 |
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
|
272 |
lemma 1); |
9578
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
273 |
by Auto_tac; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
274 |
qed "zmult_zless_cancel2"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
275 |
|
9648
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
276 |
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
|
277 |
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
|
278 |
zmult_zless_cancel2]) 1); |
9578
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
279 |
qed "zmult_zless_cancel1"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
280 |
|
9648
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
281 |
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
|
282 |
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
|
283 |
zmult_zless_cancel2]) 1); |
9578
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
284 |
by Auto_tac; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
285 |
qed "zmult_zle_cancel2"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
286 |
|
9648
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
287 |
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
|
288 |
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
|
289 |
zmult_zless_cancel1]) 1); |
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
290 |
by Auto_tac; |
9578
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
291 |
qed "zmult_zle_cancel1"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
292 |
|
9648
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
293 |
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
|
294 |
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
|
295 |
qed "int_eq_iff_zle"; |
9578
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
296 |
|
9648
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
297 |
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
|
298 |
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
|
299 |
inst "m" "m" int_eq_iff_zle]) 1); |
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
300 |
by (auto_tac (claset(), |
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
301 |
simpset() addsimps [zmult_zle_cancel2, neq_iff_zless])); |
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
302 |
val lemma = result(); |
9578
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
303 |
|
9648
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
304 |
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
|
305 |
by (rtac iff_trans 1); |
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
306 |
by (rtac lemma 2); |
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
307 |
by Auto_tac; |
9578
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
308 |
qed "zmult_cancel2"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
309 |
|
9648
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
310 |
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
|
311 |
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
|
312 |
zmult_cancel2]) 1); |
9578
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
313 |
qed "zmult_cancel1"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
314 |
Addsimps [zmult_cancel1, zmult_cancel2]; |
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 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
317 |
(*** 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
|
318 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
319 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
320 |
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
|
321 |
\ ==> q' $<= q"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
322 |
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
|
323 |
by (full_simp_tac |
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
324 |
(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
|
325 |
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
|
326 |
by (etac zle_zless_trans 2); |
9648
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
327 |
by (full_simp_tac |
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
328 |
(simpset() addsimps [zdiff_zmult_distrib2, |
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
329 |
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
|
330 |
by (etac zle_zless_trans 2); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
331 |
by (Asm_simp_tac 2); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
332 |
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
|
333 |
by (full_simp_tac |
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
334 |
(simpset() addsimps [zdiff_zmult_distrib2, |
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
335 |
zadd_zmult_distrib2]@zadd_ac@zcompare_rls) 2); |
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
336 |
by (auto_tac (claset() addEs [zless_asym], |
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
337 |
simpset() addsimps [zmult_zless_cancel1, zless_add1_iff_zle]@ |
35d761c7d934
better rules for cancellation of common factors across comparisons
paulson
parents:
9578
diff
changeset
|
338 |
zadd_ac@zcompare_rls)); |
9578
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
339 |
qed "unique_quotient_lemma"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
340 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
341 |
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
|
342 |
\ ==> q $<= q'"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
343 |
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
|
344 |
unique_quotient_lemma 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
345 |
by (auto_tac (claset(), |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
346 |
simpset() delsimps [zminus_zadd_distrib] |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
347 |
addsimps [zminus_zadd_distrib RS sym, |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
348 |
zle_zminus, zless_zminus])); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
349 |
qed "unique_quotient_lemma_neg"; |
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 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
352 |
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
|
353 |
\ q: int; q' : int |] ==> q = q'"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
354 |
by (asm_full_simp_tac |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
355 |
(simpset() addsimps split_ifs@ |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
356 |
[quorem_def, neq_iff_zless]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
357 |
by Safe_tac; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
358 |
by (ALLGOALS Asm_full_simp_tac); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
359 |
by (REPEAT |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
360 |
(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
|
361 |
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
|
362 |
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
|
363 |
sym]) 1)); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
364 |
qed "unique_quotient"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
365 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
366 |
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
|
367 |
\ q: int; q' : int; \ |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
368 |
\ r: int; r' : int |] ==> r = r'"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
369 |
by (subgoal_tac "q = q'" 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
370 |
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
|
371 |
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
|
372 |
by Auto_tac; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
373 |
qed "unique_remainder"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
374 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
375 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
376 |
(*** THE REST TO PORT LATER. The division algorithm can wait; most properties |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
377 |
of division flow from the uniqueness properties proved above... |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
378 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
379 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
380 |
(*** Correctness of posDivAlg, the division algorithm for a>=0 and b>0 ***) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
381 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
382 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
383 |
Goal "adjust a b <q,r> = (let diff = r$-b in \ |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
384 |
\ if #0 $<= diff then <#2$*q $+ #1,diff> \ |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
385 |
\ else <#2$*q,r>)"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
386 |
by (simp_tac (simpset() addsimps [Let_def,adjust_def]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
387 |
qed "adjust_eq"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
388 |
Addsimps [adjust_eq]; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
389 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
390 |
(*Proving posDivAlg's termination condition*) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
391 |
val [tc] = posDivAlg.tcs; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
392 |
goalw_cterm [] (cterm_of (sign_of (the_context ())) (HOLogic.mk_Trueprop tc)); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
393 |
by Auto_tac; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
394 |
val lemma = result(); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
395 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
396 |
(* removing the termination condition from the generated theorems *) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
397 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
398 |
bind_thm ("posDivAlg_raw_eqn", lemma RS hd posDivAlg.simps); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
399 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
400 |
(**use with simproc to avoid re-proving the premise*) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
401 |
Goal "#0 $< b ==> \ |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
402 |
\ posDivAlg <a,b> = \ |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
403 |
\ (if a$<b then <#0,a> else adjust a b (posDivAlg<a,#2$*b>))"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
404 |
by (rtac (posDivAlg_raw_eqn RS trans) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
405 |
by (Asm_simp_tac 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
406 |
qed "posDivAlg_eqn"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
407 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
408 |
bind_thm ("posDivAlg_induct", lemma RS posDivAlg.induct); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
409 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
410 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
411 |
(*Correctness of posDivAlg: it computes quotients correctly*) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
412 |
Goal "#0 $<= a --> #0 $< b --> quorem (<a,b>, posDivAlg <a,b>)"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
413 |
by (res_inst_tac [("u", "a"), ("v", "b")] posDivAlg_induct 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
414 |
by Auto_tac; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
415 |
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [quorem_def]))); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
416 |
(*base case: a<b*) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
417 |
by (asm_full_simp_tac (simpset() addsimps [posDivAlg_eqn]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
418 |
(*main argument*) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
419 |
by (stac posDivAlg_eqn 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
420 |
by (ALLGOALS Asm_simp_tac); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
421 |
by (etac splitE 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
422 |
by (auto_tac (claset(), simpset() addsimps [zadd_zmult_distrib2, Let_def])); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
423 |
qed_spec_mp "posDivAlg_correct"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
424 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
425 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
426 |
(*** Correctness of negDivAlg, the division algorithm for a<0 and b>0 ***) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
427 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
428 |
(*Proving negDivAlg's termination condition*) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
429 |
val [tc] = negDivAlg.tcs; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
430 |
goalw_cterm [] (cterm_of (sign_of (the_context ())) (HOLogic.mk_Trueprop tc)); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
431 |
by Auto_tac; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
432 |
val lemma = result(); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
433 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
434 |
(* removing the termination condition from the generated theorems *) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
435 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
436 |
bind_thm ("negDivAlg_raw_eqn", lemma RS hd negDivAlg.simps); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
437 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
438 |
(**use with simproc to avoid re-proving the premise*) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
439 |
Goal "#0 $< b ==> \ |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
440 |
\ negDivAlg <a,b> = \ |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
441 |
\ (if #0$<=a$+b then <#-1,a$+b> else adjust a b (negDivAlg<a,#2$*b>))"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
442 |
by (rtac (negDivAlg_raw_eqn RS trans) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
443 |
by (Asm_simp_tac 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
444 |
qed "negDivAlg_eqn"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
445 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
446 |
bind_thm ("negDivAlg_induct", lemma RS negDivAlg.induct); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
447 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
448 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
449 |
(*Correctness of negDivAlg: it computes quotients correctly |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
450 |
It doesn't work if a=0 because the 0/b=0 rather than -1*) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
451 |
Goal "a $< #0 --> #0 $< b --> quorem (<a,b>, negDivAlg <a,b>)"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
452 |
by (res_inst_tac [("u", "a"), ("v", "b")] negDivAlg_induct 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
453 |
by Auto_tac; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
454 |
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [quorem_def]))); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
455 |
(*base case: 0$<=a$+b*) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
456 |
by (asm_full_simp_tac (simpset() addsimps [negDivAlg_eqn]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
457 |
(*main argument*) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
458 |
by (stac negDivAlg_eqn 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
459 |
by (ALLGOALS Asm_simp_tac); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
460 |
by (etac splitE 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
461 |
by (auto_tac (claset(), simpset() addsimps [zadd_zmult_distrib2, Let_def])); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
462 |
qed_spec_mp "negDivAlg_correct"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
463 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
464 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
465 |
(*** Existence shown by proving the division algorithm to be correct ***) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
466 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
467 |
(*the case a=0*) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
468 |
Goal "b ~= #0 ==> quorem (<#0,b>, <#0,#0>)"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
469 |
by (auto_tac (claset(), |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
470 |
simpset() addsimps [quorem_def, neq_iff_zless])); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
471 |
qed "quorem_0"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
472 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
473 |
Goal "posDivAlg <#0,b> = <#0,#0>"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
474 |
by (stac posDivAlg_raw_eqn 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
475 |
by Auto_tac; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
476 |
qed "posDivAlg_0"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
477 |
Addsimps [posDivAlg_0]; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
478 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
479 |
Goal "negDivAlg <#-1,b> = <#-1,b-#1>"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
480 |
by (stac negDivAlg_raw_eqn 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
481 |
by Auto_tac; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
482 |
qed "negDivAlg_minus1"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
483 |
Addsimps [negDivAlg_minus1]; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
484 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
485 |
Goalw [negateSnd_def] "negateSnd<q,r> = <q,-r>"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
486 |
by Auto_tac; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
487 |
qed "negateSnd_eq"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
488 |
Addsimps [negateSnd_eq]; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
489 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
490 |
Goal "quorem (<-a,-b>, qr) ==> quorem (<a,b>, negateSnd qr)"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
491 |
by (auto_tac (claset(), simpset() addsimps split_ifs@[quorem_def])); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
492 |
qed "quorem_neg"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
493 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
494 |
Goal "b ~= #0 ==> quorem (<a,b>, divAlg<a,b>)"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
495 |
by (auto_tac (claset(), |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
496 |
simpset() addsimps [quorem_0, divAlg_def])); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
497 |
by (REPEAT_FIRST (resolve_tac [quorem_neg, posDivAlg_correct, |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
498 |
negDivAlg_correct])); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
499 |
by (auto_tac (claset(), |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
500 |
simpset() addsimps [quorem_def, neq_iff_zless])); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
501 |
qed "divAlg_correct"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
502 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
503 |
(** Aribtrary definitions for division by zero. Useful to simplify |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
504 |
certain equations **) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
505 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
506 |
Goal "a div (#0::int) = #0"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
507 |
by (simp_tac (simpset() addsimps [div_def, divAlg_def, posDivAlg_raw_eqn]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
508 |
qed "DIVISION_BY_ZERO_ZDIV"; (*NOT for adding to default simpset*) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
509 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
510 |
Goal "a mod (#0::int) = a"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
511 |
by (simp_tac (simpset() addsimps [mod_def, divAlg_def, posDivAlg_raw_eqn]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
512 |
qed "DIVISION_BY_ZERO_ZMOD"; (*NOT for adding to default simpset*) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
513 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
514 |
fun zdiv_undefined_case_tac s i = |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
515 |
case_tac s i THEN |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
516 |
asm_simp_tac (simpset() addsimps [DIVISION_BY_ZERO_ZDIV, |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
517 |
DIVISION_BY_ZERO_ZMOD]) i; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
518 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
519 |
(** Basic laws about division and remainder **) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
520 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
521 |
Goal "a = b $* (a div b) $+ (a mod b)"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
522 |
by (zdiv_undefined_case_tac "b = #0" 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
523 |
by (cut_inst_tac [("a","a"),("b","b")] divAlg_correct 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
524 |
by (auto_tac (claset(), |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
525 |
simpset() addsimps [quorem_def, div_def, mod_def])); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
526 |
qed "zmod_zdiv_equality"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
527 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
528 |
Goal "(#0::int) $< b ==> #0 $<= a mod b & a mod b $< b"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
529 |
by (cut_inst_tac [("a","a"),("b","b")] divAlg_correct 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
530 |
by (auto_tac (claset(), |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
531 |
simpset() addsimps [quorem_def, mod_def])); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
532 |
bind_thm ("pos_mod_sign", result() RS conjunct1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
533 |
bind_thm ("pos_mod_bound", result() RS conjunct2); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
534 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
535 |
Goal "b $< (#0::int) ==> a mod b $<= #0 & b $< a mod b"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
536 |
by (cut_inst_tac [("a","a"),("b","b")] divAlg_correct 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
537 |
by (auto_tac (claset(), |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
538 |
simpset() addsimps [quorem_def, div_def, mod_def])); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
539 |
bind_thm ("neg_mod_sign", result() RS conjunct1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
540 |
bind_thm ("neg_mod_bound", result() RS conjunct2); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
541 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
542 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
543 |
(** proving general properties of div and mod **) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
544 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
545 |
Goal "b ~= #0 ==> quorem (<a,b>, <a div b,a mod b>)"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
546 |
by (cut_inst_tac [("a","a"),("b","b")] zmod_zdiv_equality 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
547 |
by (auto_tac |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
548 |
(claset(), |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
549 |
simpset() addsimps [quorem_def, neq_iff_zless, |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
550 |
pos_mod_sign,pos_mod_bound, |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
551 |
neg_mod_sign, neg_mod_bound])); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
552 |
qed "quorem_div_mod"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
553 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
554 |
Goal "[| quorem(<a,b>,<q,r>); b ~= #0 |] ==> a div b = q"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
555 |
by (asm_simp_tac (simpset() addsimps [quorem_div_mod RS unique_quotient]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
556 |
qed "quorem_div"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
557 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
558 |
Goal "[| quorem(<a,b>,<q,r>); b ~= #0 |] ==> a mod b = r"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
559 |
by (asm_simp_tac (simpset() addsimps [quorem_div_mod RS unique_remainder]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
560 |
qed "quorem_mod"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
561 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
562 |
Goal "[| (#0::int) $<= a; a $< b |] ==> a div b = #0"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
563 |
by (rtac quorem_div 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
564 |
by (auto_tac (claset(), simpset() addsimps [quorem_def])); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
565 |
qed "div_pos_pos_trivial"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
566 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
567 |
Goal "[| a $<= (#0::int); b $< a |] ==> a div b = #0"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
568 |
by (rtac quorem_div 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
569 |
by (auto_tac (claset(), simpset() addsimps [quorem_def])); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
570 |
qed "div_neg_neg_trivial"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
571 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
572 |
Goal "[| (#0::int) $< a; a$+b $<= #0 |] ==> a div b = #-1"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
573 |
by (rtac quorem_div 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
574 |
by (auto_tac (claset(), simpset() addsimps [quorem_def])); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
575 |
qed "div_pos_neg_trivial"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
576 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
577 |
(*There is no div_neg_pos_trivial because #0 div b = #0 would supersede it*) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
578 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
579 |
Goal "[| (#0::int) $<= a; a $< b |] ==> a mod b = a"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
580 |
by (res_inst_tac [("q","#0")] quorem_mod 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
581 |
by (auto_tac (claset(), simpset() addsimps [quorem_def])); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
582 |
qed "mod_pos_pos_trivial"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
583 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
584 |
Goal "[| a $<= (#0::int); b $< a |] ==> a mod b = a"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
585 |
by (res_inst_tac [("q","#0")] quorem_mod 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
586 |
by (auto_tac (claset(), simpset() addsimps [quorem_def])); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
587 |
qed "mod_neg_neg_trivial"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
588 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
589 |
Goal "[| (#0::int) $< a; a$+b $<= #0 |] ==> a mod b = a$+b"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
590 |
by (res_inst_tac [("q","#-1")] quorem_mod 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
591 |
by (auto_tac (claset(), simpset() addsimps [quorem_def])); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
592 |
qed "mod_pos_neg_trivial"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
593 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
594 |
(*There is no mod_neg_pos_trivial...*) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
595 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
596 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
597 |
(*Simpler laws such as -a div b = -(a div b) FAIL*) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
598 |
Goal "(-a) div (-b) = a div b"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
599 |
by (zdiv_undefined_case_tac "b = #0" 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
600 |
by (stac ((simplify(simpset()) (quorem_div_mod RS quorem_neg)) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
601 |
RS quorem_div) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
602 |
by Auto_tac; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
603 |
qed "zdiv_zminus_zminus"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
604 |
Addsimps [zdiv_zminus_zminus]; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
605 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
606 |
(*Simpler laws such as -a mod b = -(a mod b) FAIL*) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
607 |
Goal "(-a) mod (-b) = - (a mod b)"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
608 |
by (zdiv_undefined_case_tac "b = #0" 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
609 |
by (stac ((simplify(simpset()) (quorem_div_mod RS quorem_neg)) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
610 |
RS quorem_mod) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
611 |
by Auto_tac; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
612 |
qed "zmod_zminus_zminus"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
613 |
Addsimps [zmod_zminus_zminus]; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
614 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
615 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
616 |
(*** division of a number by itself ***) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
617 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
618 |
Goal "[| (#0::int) $< a; a = r $+ a$*q; r $< a |] ==> #1 $<= q"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
619 |
by (subgoal_tac "#0 $< a$*q" 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
620 |
by (arith_tac 2); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
621 |
by (asm_full_simp_tac (simpset() addsimps [int_0_less_mult_iff]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
622 |
val lemma1 = result(); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
623 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
624 |
Goal "[| (#0::int) $< a; a = r $+ a$*q; #0 $<= r |] ==> q $<= #1"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
625 |
by (subgoal_tac "#0 $<= a$*(#1$-q)" 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
626 |
by (asm_simp_tac (simpset() addsimps [zdiff_zmult_distrib2]) 2); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
627 |
by (asm_full_simp_tac (simpset() addsimps [int_0_le_mult_iff]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
628 |
val lemma2 = result(); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
629 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
630 |
Goal "[| quorem(<a,a>,<q,r>); a ~= (#0::int) |] ==> q = #1"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
631 |
by (asm_full_simp_tac |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
632 |
(simpset() addsimps split_ifs@[quorem_def, neq_iff_zless]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
633 |
by (rtac order_antisym 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
634 |
by Safe_tac; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
635 |
by Auto_tac; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
636 |
by (res_inst_tac [("a", "-a"),("r", "-r")] lemma1 3); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
637 |
by (res_inst_tac [("a", "-a"),("r", "-r")] lemma2 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
638 |
by (REPEAT (force_tac (claset() addIs [lemma1,lemma2], |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
639 |
simpset() addsimps [zadd_commute, zmult_zminus]) 1)); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
640 |
qed "self_quotient"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
641 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
642 |
Goal "[| quorem(<a,a>,<q,r>); a ~= (#0::int) |] ==> r = #0"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
643 |
by (ftac self_quotient 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
644 |
by (assume_tac 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
645 |
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
|
646 |
qed "self_remainder"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
647 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
648 |
Goal "a ~= #0 ==> a div a = (#1::int)"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
649 |
by (asm_simp_tac (simpset() addsimps [quorem_div_mod RS self_quotient]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
650 |
qed "zdiv_self"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
651 |
Addsimps [zdiv_self]; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
652 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
653 |
(*Here we have 0 mod 0 = 0, also assumed by Knuth (who puts m mod 0 = 0) *) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
654 |
Goal "a mod a = (#0::int)"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
655 |
by (zdiv_undefined_case_tac "a = #0" 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
656 |
by (asm_simp_tac (simpset() addsimps [quorem_div_mod RS self_remainder]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
657 |
qed "zmod_self"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
658 |
Addsimps [zmod_self]; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
659 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
660 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
661 |
(*** Computation of division and remainder ***) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
662 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
663 |
Goal "(#0::int) div b = #0"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
664 |
by (simp_tac (simpset() addsimps [div_def, divAlg_def]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
665 |
qed "zdiv_zero"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
666 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
667 |
Goal "(#0::int) $< b ==> #-1 div b = #-1"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
668 |
by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
669 |
qed "div_eq_minus1"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
670 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
671 |
Goal "(#0::int) mod b = #0"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
672 |
by (simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
673 |
qed "zmod_zero"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
674 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
675 |
Addsimps [zdiv_zero, zmod_zero]; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
676 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
677 |
Goal "(#0::int) $< b ==> #-1 div b = #-1"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
678 |
by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
679 |
qed "zdiv_minus1"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
680 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
681 |
Goal "(#0::int) $< b ==> #-1 mod b = b-#1"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
682 |
by (asm_simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
683 |
qed "zmod_minus1"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
684 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
685 |
(** a positive, b positive **) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
686 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
687 |
Goal "[| #0 $< a; #0 $<= b |] ==> a div b = fst (posDivAlg<a,b>)"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
688 |
by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
689 |
qed "div_pos_pos"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
690 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
691 |
Goal "[| #0 $< a; #0 $<= b |] ==> a mod b = snd (posDivAlg<a,b>)"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
692 |
by (asm_simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
693 |
qed "mod_pos_pos"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
694 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
695 |
(** a negative, b positive **) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
696 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
697 |
Goal "[| a $< #0; #0 $< b |] ==> a div b = fst (negDivAlg<a,b>)"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
698 |
by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
699 |
qed "div_neg_pos"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
700 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
701 |
Goal "[| a $< #0; #0 $< b |] ==> a mod b = snd (negDivAlg<a,b>)"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
702 |
by (asm_simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
703 |
qed "mod_neg_pos"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
704 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
705 |
(** a positive, b negative **) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
706 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
707 |
Goal "[| #0 $< a; b $< #0 |] ==> a div b = fst (negateSnd(negDivAlg<-a,-b>))"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
708 |
by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
709 |
qed "div_pos_neg"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
710 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
711 |
Goal "[| #0 $< a; b $< #0 |] ==> a mod b = snd (negateSnd(negDivAlg<-a,-b>))"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
712 |
by (asm_simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
713 |
qed "mod_pos_neg"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
714 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
715 |
(** a negative, b negative **) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
716 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
717 |
Goal "[| a $< #0; b $<= #0 |] ==> a div b = fst (negateSnd(posDivAlg<-a,-b>))"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
718 |
by (asm_simp_tac (simpset() addsimps [div_def, divAlg_def]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
719 |
qed "div_neg_neg"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
720 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
721 |
Goal "[| a $< #0; b $<= #0 |] ==> a mod b = snd (negateSnd(posDivAlg<-a,-b>))"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
722 |
by (asm_simp_tac (simpset() addsimps [mod_def, divAlg_def]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
723 |
qed "mod_neg_neg"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
724 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
725 |
Addsimps (map (read_instantiate_sg (sign_of (the_context ())) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
726 |
[("a", "number_of ?v"), ("b", "number_of ?w")]) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
727 |
[div_pos_pos, div_neg_pos, div_pos_neg, div_neg_neg, |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
728 |
mod_pos_pos, mod_neg_pos, mod_pos_neg, mod_neg_neg, |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
729 |
posDivAlg_eqn, negDivAlg_eqn]); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
730 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
731 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
732 |
(** Special-case simplification **) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
733 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
734 |
Goal "a mod (#1::int) = #0"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
735 |
by (cut_inst_tac [("a","a"),("b","#1")] pos_mod_sign 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
736 |
by (cut_inst_tac [("a","a"),("b","#1")] pos_mod_bound 2); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
737 |
by Auto_tac; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
738 |
qed "zmod_1"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
739 |
Addsimps [zmod_1]; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
740 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
741 |
Goal "a div (#1::int) = a"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
742 |
by (cut_inst_tac [("a","a"),("b","#1")] zmod_zdiv_equality 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
743 |
by Auto_tac; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
744 |
qed "zdiv_1"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
745 |
Addsimps [zdiv_1]; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
746 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
747 |
Goal "a mod (#-1::int) = #0"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
748 |
by (cut_inst_tac [("a","a"),("b","#-1")] neg_mod_sign 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
749 |
by (cut_inst_tac [("a","a"),("b","#-1")] neg_mod_bound 2); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
750 |
by Auto_tac; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
751 |
qed "zmod_minus1_right"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
752 |
Addsimps [zmod_minus1_right]; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
753 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
754 |
Goal "a div (#-1::int) = -a"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
755 |
by (cut_inst_tac [("a","a"),("b","#-1")] zmod_zdiv_equality 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
756 |
by Auto_tac; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
757 |
qed "zdiv_minus1_right"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
758 |
Addsimps [zdiv_minus1_right]; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
759 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
760 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
761 |
(*** Monotonicity in the first argument (divisor) ***) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
762 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
763 |
Goal "[| a $<= a'; #0 $< b |] ==> a div b $<= a' div b"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
764 |
by (cut_inst_tac [("a","a"),("b","b")] zmod_zdiv_equality 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
765 |
by (cut_inst_tac [("a","a'"),("b","b")] zmod_zdiv_equality 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
766 |
by (rtac unique_quotient_lemma 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
767 |
by (etac subst 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
768 |
by (etac subst 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
769 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [pos_mod_sign,pos_mod_bound]))); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
770 |
qed "zdiv_mono1"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
771 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
772 |
Goal "[| a $<= a'; b $< #0 |] ==> a' div b $<= a div b"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
773 |
by (cut_inst_tac [("a","a"),("b","b")] zmod_zdiv_equality 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
774 |
by (cut_inst_tac [("a","a'"),("b","b")] zmod_zdiv_equality 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
775 |
by (rtac unique_quotient_lemma_neg 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
776 |
by (etac subst 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
777 |
by (etac subst 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
778 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [neg_mod_sign,neg_mod_bound]))); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
779 |
qed "zdiv_mono1_neg"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
780 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
781 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
782 |
(*** Monotonicity in the second argument (dividend) ***) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
783 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
784 |
Goal "[| b$*q $+ r = b'$*q' $+ r'; #0 $<= b'$*q' $+ r'; \ |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
785 |
\ r' $< b'; #0 $<= r; #0 $< b'; b' $<= b |] \ |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
786 |
\ ==> q $<= q'"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
787 |
by (subgoal_tac "#0 $<= q'" 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
788 |
by (subgoal_tac "#0 $< b'$*(q' $+ #1)" 2); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
789 |
by (asm_simp_tac (simpset() addsimps [zadd_zmult_distrib2]) 3); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
790 |
by (asm_full_simp_tac (simpset() addsimps [int_0_less_mult_iff]) 2); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
791 |
by (subgoal_tac "b$*q $< b$*(q' $+ #1)" 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
792 |
by (Asm_full_simp_tac 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
793 |
by (subgoal_tac "b$*q = r' $- r $+ b'$*q'" 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
794 |
by (Simp_tac 2); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
795 |
by (asm_simp_tac (simpset() addsimps [zadd_zmult_distrib2]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
796 |
by (stac zadd_commute 1 THEN rtac zadd_zless_mono 1 THEN arith_tac 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
797 |
by (rtac zmult_zle_mono1 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
798 |
by Auto_tac; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
799 |
qed "zdiv_mono2_lemma"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
800 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
801 |
Goal "[| (#0::int) $<= a; #0 $< b'; b' $<= b |] \ |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
802 |
\ ==> a div b $<= a div b'"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
803 |
by (subgoal_tac "b ~= #0" 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
804 |
by (arith_tac 2); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
805 |
by (cut_inst_tac [("a","a"),("b","b")] zmod_zdiv_equality 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
806 |
by (cut_inst_tac [("a","a"),("b","b'")] zmod_zdiv_equality 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
807 |
by (rtac zdiv_mono2_lemma 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
808 |
by (etac subst 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
809 |
by (etac subst 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
810 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [pos_mod_sign,pos_mod_bound]))); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
811 |
qed "zdiv_mono2"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
812 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
813 |
Goal "[| b$*q $+ r = b'$*q' $+ r'; b'$*q' $+ r' $< #0; \ |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
814 |
\ r $< b; #0 $<= r'; #0 $< b'; b' $<= b |] \ |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
815 |
\ ==> q' $<= q"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
816 |
by (subgoal_tac "q' $< #0" 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
817 |
by (subgoal_tac "b'$*q' $< #0" 2); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
818 |
by (arith_tac 3); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
819 |
by (asm_full_simp_tac (simpset() addsimps [zmult_less_0_iff]) 2); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
820 |
by (subgoal_tac "b$*q' $< b$*(q $+ #1)" 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
821 |
by (Asm_full_simp_tac 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
822 |
by (asm_simp_tac (simpset() addsimps [zadd_zmult_distrib2]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
823 |
by (subgoal_tac "b$*q' $<= b'$*q'" 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
824 |
by (asm_simp_tac (simpset() addsimps [zmult_zle_mono1_neg]) 2); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
825 |
by (subgoal_tac "b'$*q' $< b $+ b$*q" 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
826 |
by (Asm_simp_tac 2); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
827 |
by (arith_tac 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
828 |
qed "zdiv_mono2_neg_lemma"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
829 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
830 |
Goal "[| a $< (#0::int); #0 $< b'; b' $<= b |] \ |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
831 |
\ ==> a div b' $<= a div b"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
832 |
by (cut_inst_tac [("a","a"),("b","b")] zmod_zdiv_equality 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
833 |
by (cut_inst_tac [("a","a"),("b","b'")] zmod_zdiv_equality 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
834 |
by (rtac zdiv_mono2_neg_lemma 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
835 |
by (etac subst 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
836 |
by (etac subst 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
837 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [pos_mod_sign,pos_mod_bound]))); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
838 |
qed "zdiv_mono2_neg"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
839 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
840 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
841 |
(*** More algebraic laws for div and mod ***) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
842 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
843 |
(** proving (a*b) div c = a $* (b div c) $+ a * (b mod c) **) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
844 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
845 |
Goal "[| quorem(<b,c>,<q,r>); c ~= #0 |] \ |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
846 |
\ ==> quorem (<a$*b,c>, <a$*q $+ a$*r div c,a$*r mod c>)"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
847 |
by (auto_tac |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
848 |
(claset(), |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
849 |
simpset() addsimps split_ifs@ |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
850 |
[quorem_def, neq_iff_zless, |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
851 |
zadd_zmult_distrib2, |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
852 |
pos_mod_sign,pos_mod_bound, |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
853 |
neg_mod_sign, neg_mod_bound])); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
854 |
by (ALLGOALS(rtac zmod_zdiv_equality)); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
855 |
val lemma = result(); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
856 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
857 |
Goal "(a$*b) div c = a$*(b div c) $+ a$*(b mod c) div c"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
858 |
by (zdiv_undefined_case_tac "c = #0" 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
859 |
by (blast_tac (claset() addIs [quorem_div_mod RS lemma RS quorem_div]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
860 |
qed "zdiv_zmult1_eq"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
861 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
862 |
Goal "(a$*b) mod c = a$*(b mod c) mod c"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
863 |
by (zdiv_undefined_case_tac "c = #0" 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
864 |
by (blast_tac (claset() addIs [quorem_div_mod RS lemma RS quorem_mod]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
865 |
qed "zmod_zmult1_eq"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
866 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
867 |
Goal "(a$*b) mod c = ((a mod c) $* b) mod c"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
868 |
by (rtac trans 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
869 |
by (res_inst_tac [("s","b$*a mod c")] trans 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
870 |
by (rtac zmod_zmult1_eq 2); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
871 |
by (ALLGOALS (simp_tac (simpset() addsimps [zmult_commute]))); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
872 |
qed "zmod_zmult1_eq'"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
873 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
874 |
Goal "(a$*b) mod c = ((a mod c) $* (b mod c)) mod c"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
875 |
by (rtac (zmod_zmult1_eq' RS trans) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
876 |
by (rtac zmod_zmult1_eq 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
877 |
qed "zmod_zmult_distrib"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
878 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
879 |
Goal "b ~= (#0::int) ==> (a$*b) div b = a"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
880 |
by (asm_simp_tac (simpset() addsimps [zdiv_zmult1_eq]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
881 |
qed "zdiv_zmult_self1"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
882 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
883 |
Goal "b ~= (#0::int) ==> (b$*a) div b = a"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
884 |
by (stac zmult_commute 1 THEN etac zdiv_zmult_self1 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
885 |
qed "zdiv_zmult_self2"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
886 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
887 |
Addsimps [zdiv_zmult_self1, zdiv_zmult_self2]; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
888 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
889 |
Goal "(a$*b) mod b = (#0::int)"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
890 |
by (simp_tac (simpset() addsimps [zmod_zmult1_eq]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
891 |
qed "zmod_zmult_self1"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
892 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
893 |
Goal "(b$*a) mod b = (#0::int)"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
894 |
by (simp_tac (simpset() addsimps [zmult_commute, zmod_zmult1_eq]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
895 |
qed "zmod_zmult_self2"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
896 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
897 |
Addsimps [zmod_zmult_self1, zmod_zmult_self2]; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
898 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
899 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
900 |
(** proving (a$+b) div c = a div c $+ b div c $+ ((a mod c $+ b mod c) div c) **) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
901 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
902 |
Goal "[| quorem(<a,c>,<aq,ar>); quorem(<b,c>,<bq,br>); c ~= #0 |] \ |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
903 |
\ ==> quorem (<a$+b,c>, (aq $+ bq $+ (ar$+br) div c, (ar$+br) mod c))"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
904 |
by (auto_tac |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
905 |
(claset(), |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
906 |
simpset() addsimps split_ifs@ |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
907 |
[quorem_def, neq_iff_zless, |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
908 |
zadd_zmult_distrib2, |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
909 |
pos_mod_sign,pos_mod_bound, |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
910 |
neg_mod_sign, neg_mod_bound])); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
911 |
by (ALLGOALS(rtac zmod_zdiv_equality)); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
912 |
val lemma = result(); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
913 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
914 |
(*NOT suitable for rewriting: the RHS has an instance of the LHS*) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
915 |
Goal "(a$+b) div c = a div c $+ b div c $+ ((a mod c $+ b mod c) div c)"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
916 |
by (zdiv_undefined_case_tac "c = #0" 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
917 |
by (blast_tac (claset() addIs [[quorem_div_mod,quorem_div_mod] |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
918 |
MRS lemma RS quorem_div]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
919 |
qed "zdiv_zadd1_eq"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
920 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
921 |
Goal "(a$+b) mod c = (a mod c $+ b mod c) mod c"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
922 |
by (zdiv_undefined_case_tac "c = #0" 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
923 |
by (blast_tac (claset() addIs [[quorem_div_mod,quorem_div_mod] |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
924 |
MRS lemma RS quorem_mod]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
925 |
qed "zmod_zadd1_eq"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
926 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
927 |
Goal "(a mod b) div b = (#0::int)"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
928 |
by (zdiv_undefined_case_tac "b = #0" 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
929 |
by (auto_tac (claset(), |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
930 |
simpset() addsimps [neq_iff_zless, |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
931 |
pos_mod_sign, pos_mod_bound, div_pos_pos_trivial, |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
932 |
neg_mod_sign, neg_mod_bound, div_neg_neg_trivial])); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
933 |
qed "mod_div_trivial"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
934 |
Addsimps [mod_div_trivial]; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
935 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
936 |
Goal "(a mod b) mod b = a mod b"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
937 |
by (zdiv_undefined_case_tac "b = #0" 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
938 |
by (auto_tac (claset(), |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
939 |
simpset() addsimps [neq_iff_zless, |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
940 |
pos_mod_sign, pos_mod_bound, mod_pos_pos_trivial, |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
941 |
neg_mod_sign, neg_mod_bound, mod_neg_neg_trivial])); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
942 |
qed "mod_mod_trivial"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
943 |
Addsimps [mod_mod_trivial]; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
944 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
945 |
Goal "(a$+b) mod c = ((a mod c) $+ b) mod c"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
946 |
by (rtac (trans RS sym) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
947 |
by (rtac zmod_zadd1_eq 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
948 |
by (Simp_tac 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
949 |
by (rtac (zmod_zadd1_eq RS sym) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
950 |
qed "zmod_zadd_left_eq"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
951 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
952 |
Goal "(a$+b) mod c = (a $+ (b mod c)) mod c"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
953 |
by (rtac (trans RS sym) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
954 |
by (rtac zmod_zadd1_eq 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
955 |
by (Simp_tac 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
956 |
by (rtac (zmod_zadd1_eq RS sym) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
957 |
qed "zmod_zadd_right_eq"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
958 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
959 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
960 |
Goal "a ~= (#0::int) ==> (a$+b) div a = b div a $+ #1"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
961 |
by (asm_simp_tac (simpset() addsimps [zdiv_zadd1_eq]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
962 |
qed "zdiv_zadd_self1"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
963 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
964 |
Goal "a ~= (#0::int) ==> (b$+a) div a = b div a $+ #1"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
965 |
by (asm_simp_tac (simpset() addsimps [zdiv_zadd1_eq]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
966 |
qed "zdiv_zadd_self2"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
967 |
Addsimps [zdiv_zadd_self1, zdiv_zadd_self2]; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
968 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
969 |
Goal "(a$+b) mod a = b mod a"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
970 |
by (zdiv_undefined_case_tac "a = #0" 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
971 |
by (asm_simp_tac (simpset() addsimps [zmod_zadd1_eq]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
972 |
qed "zmod_zadd_self1"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
973 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
974 |
Goal "(b$+a) mod a = b mod a"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
975 |
by (zdiv_undefined_case_tac "a = #0" 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
976 |
by (asm_simp_tac (simpset() addsimps [zmod_zadd1_eq]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
977 |
qed "zmod_zadd_self2"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
978 |
Addsimps [zmod_zadd_self1, zmod_zadd_self2]; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
979 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
980 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
981 |
(*** proving a div (b*c) = (a div b) div c ***) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
982 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
983 |
(*The condition c>0 seems necessary. Consider that 7 div ~6 = ~2 but |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
984 |
7 div 2 div ~3 = 3 div ~3 = ~1. The subcase (a div b) mod c = 0 seems |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
985 |
to cause particular problems.*) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
986 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
987 |
(** first, four lemmas to bound the remainder for the cases b<0 and b>0 **) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
988 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
989 |
Goal "[| (#0::int) $< c; b $< r; r $<= #0 |] ==> b$*c $< b$*(q mod c) $+ r"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
990 |
by (subgoal_tac "b $* (c $- q mod c) $< r $* #1" 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
991 |
by (asm_full_simp_tac (simpset() addsimps [zdiff_zmult_distrib2]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
992 |
by (rtac order_le_less_trans 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
993 |
by (etac zmult_zless_mono1 2); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
994 |
by (rtac zmult_zle_mono2_neg 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
995 |
by (auto_tac |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
996 |
(claset(), |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
997 |
simpset() addsimps zcompare_rls@ |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
998 |
[zadd_commute, add1_zle_eq, pos_mod_bound])); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
999 |
val lemma1 = result(); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1000 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1001 |
Goal "[| (#0::int) $< c; b $< r; r $<= #0 |] ==> b $* (q mod c) $+ r $<= #0"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1002 |
by (subgoal_tac "b $* (q mod c) $<= #0" 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1003 |
by (arith_tac 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1004 |
by (asm_simp_tac (simpset() addsimps [zmult_le_0_iff, pos_mod_sign]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1005 |
val lemma2 = result(); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1006 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1007 |
Goal "[| (#0::int) $< c; #0 $<= r; r $< b |] ==> #0 $<= b $* (q mod c) $+ r"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1008 |
by (subgoal_tac "#0 $<= b $* (q mod c)" 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1009 |
by (arith_tac 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1010 |
by (asm_simp_tac (simpset() addsimps [int_0_le_mult_iff, pos_mod_sign]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1011 |
val lemma3 = result(); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1012 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1013 |
Goal "[| (#0::int) $< c; #0 $<= r; r $< b |] ==> b $* (q mod c) $+ r $< b $* c"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1014 |
by (subgoal_tac "r $* #1 $< b $* (c $- q mod c)" 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1015 |
by (asm_full_simp_tac (simpset() addsimps [zdiff_zmult_distrib2]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1016 |
by (rtac order_less_le_trans 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1017 |
by (etac zmult_zless_mono1 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1018 |
by (rtac zmult_zle_mono2 2); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1019 |
by (auto_tac |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1020 |
(claset(), |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1021 |
simpset() addsimps zcompare_rls@ |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1022 |
[zadd_commute, add1_zle_eq, pos_mod_bound])); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1023 |
val lemma4 = result(); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1024 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1025 |
Goal "[| quorem (<a,b>, <q,r>); b ~= #0; #0 $< c |] \ |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1026 |
\ ==> quorem (<a,b$*c>, (q div c, b$*(q mod c) $+ r))"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1027 |
by (auto_tac |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1028 |
(claset(), |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1029 |
simpset() addsimps zmult_ac@ |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1030 |
[zmod_zdiv_equality, quorem_def, neq_iff_zless, |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1031 |
int_0_less_mult_iff, |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1032 |
zadd_zmult_distrib2 RS sym, |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1033 |
lemma1, lemma2, lemma3, lemma4])); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1034 |
val lemma = result(); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1035 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1036 |
Goal "(#0::int) $< c ==> a div (b$*c) = (a div b) div c"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1037 |
by (zdiv_undefined_case_tac "b = #0" 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1038 |
by (force_tac (claset(), |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1039 |
simpset() addsimps [quorem_div_mod RS lemma RS quorem_div, |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1040 |
zmult_eq_0_iff]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1041 |
qed "zdiv_zmult2_eq"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1042 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1043 |
Goal "(#0::int) $< c ==> a mod (b$*c) = b$*(a div b mod c) $+ a mod b"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1044 |
by (zdiv_undefined_case_tac "b = #0" 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1045 |
by (force_tac (claset(), |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1046 |
simpset() addsimps [quorem_div_mod RS lemma RS quorem_mod, |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1047 |
zmult_eq_0_iff]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1048 |
qed "zmod_zmult2_eq"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1049 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1050 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1051 |
(*** Cancellation of common factors in "div" ***) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1052 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1053 |
Goal "[| (#0::int) $< b; c ~= #0 |] ==> (c$*a) div (c$*b) = a div b"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1054 |
by (stac zdiv_zmult2_eq 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1055 |
by Auto_tac; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1056 |
val lemma1 = result(); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1057 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1058 |
Goal "[| b $< (#0::int); c ~= #0 |] ==> (c$*a) div (c$*b) = a div b"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1059 |
by (subgoal_tac "(c $* (-a)) div (c $* (-b)) = (-a) div (-b)" 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1060 |
by (rtac lemma1 2); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1061 |
by Auto_tac; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1062 |
val lemma2 = result(); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1063 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1064 |
Goal "c ~= (#0::int) ==> (c$*a) div (c$*b) = a div b"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1065 |
by (zdiv_undefined_case_tac "b = #0" 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1066 |
by (auto_tac |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1067 |
(claset(), |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1068 |
simpset() addsimps [read_instantiate [("x", "b")] neq_iff_zless, |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1069 |
lemma1, lemma2])); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1070 |
qed "zdiv_zmult_zmult1"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1071 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1072 |
Goal "c ~= (#0::int) ==> (a$*c) div (b$*c) = a div b"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1073 |
by (dtac zdiv_zmult_zmult1 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1074 |
by (auto_tac (claset(), simpset() addsimps [zmult_commute])); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1075 |
qed "zdiv_zmult_zmult2"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1076 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1077 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1078 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1079 |
(*** Distribution of factors over "mod" ***) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1080 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1081 |
Goal "[| (#0::int) $< b; c ~= #0 |] ==> (c$*a) mod (c$*b) = c $* (a mod b)"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1082 |
by (stac zmod_zmult2_eq 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1083 |
by Auto_tac; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1084 |
val lemma1 = result(); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1085 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1086 |
Goal "[| b $< (#0::int); c ~= #0 |] ==> (c$*a) mod (c$*b) = c $* (a mod b)"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1087 |
by (subgoal_tac "(c $* (-a)) mod (c $* (-b)) = c $* ((-a) mod (-b))" 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1088 |
by (rtac lemma1 2); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1089 |
by Auto_tac; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1090 |
val lemma2 = result(); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1091 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1092 |
Goal "(c$*a) mod (c$*b) = c $* (a mod b)"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1093 |
by (zdiv_undefined_case_tac "b = #0" 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1094 |
by (zdiv_undefined_case_tac "c = #0" 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1095 |
by (auto_tac |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1096 |
(claset(), |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1097 |
simpset() addsimps [read_instantiate [("x", "b")] neq_iff_zless, |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1098 |
lemma1, lemma2])); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1099 |
qed "zmod_zmult_zmult1"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1100 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1101 |
Goal "(a$*c) mod (b$*c) = (a mod b) $* c"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1102 |
by (cut_inst_tac [("c","c")] zmod_zmult_zmult1 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1103 |
by (auto_tac (claset(), simpset() addsimps [zmult_commute])); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1104 |
qed "zmod_zmult_zmult2"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1105 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1106 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1107 |
(*** Speeding up the division algorithm with shifting ***) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1108 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1109 |
(** computing "div" by shifting **) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1110 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1111 |
Goal "(#0::int) $<= a ==> (#1 $+ #2$*b) div (#2$*a) = b div a"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1112 |
by (zdiv_undefined_case_tac "a = #0" 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1113 |
by (subgoal_tac "#1 $<= a" 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1114 |
by (arith_tac 2); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1115 |
by (subgoal_tac "#1 $< a $* #2" 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1116 |
by (arith_tac 2); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1117 |
by (subgoal_tac "#2$*(#1 $+ b mod a) $<= #2$*a" 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1118 |
by (rtac zmult_zle_mono2 2); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1119 |
by (auto_tac (claset(), |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1120 |
simpset() addsimps [zadd_commute, zmult_commute, |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1121 |
add1_zle_eq, pos_mod_bound])); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1122 |
by (stac zdiv_zadd1_eq 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1123 |
by (asm_simp_tac (simpset() addsimps [zdiv_zmult_zmult2, zmod_zmult_zmult2, |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1124 |
div_pos_pos_trivial]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1125 |
by (stac div_pos_pos_trivial 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1126 |
by (asm_simp_tac (simpset() |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1127 |
addsimps [mod_pos_pos_trivial, |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1128 |
pos_mod_sign RS zadd_zle_mono1 RSN (2,order_trans)]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1129 |
by (auto_tac (claset(), |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1130 |
simpset() addsimps [mod_pos_pos_trivial])); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1131 |
by (subgoal_tac "#0 $<= b mod a" 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1132 |
by (asm_simp_tac (simpset() addsimps [pos_mod_sign]) 2); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1133 |
by (arith_tac 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1134 |
qed "pos_zdiv_mult_2"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1135 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1136 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1137 |
Goal "a $<= (#0::int) ==> (#1 $+ #2$*b) div (#2$*a) = (b$+#1) div a"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1138 |
by (subgoal_tac "(#1 $+ #2$*(-b-#1)) div (#2 $* (-a)) = (-b-#1) div (-a)" 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1139 |
by (rtac pos_zdiv_mult_2 2); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1140 |
by (auto_tac (claset(), |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1141 |
simpset() addsimps [zmult_zminus_right])); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1142 |
by (subgoal_tac "(#-1 - (#2 $* b)) = - (#1 $+ (#2 $* b))" 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1143 |
by (Simp_tac 2); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1144 |
by (asm_full_simp_tac (HOL_ss |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1145 |
addsimps [zdiv_zminus_zminus, zdiff_def, |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1146 |
zminus_zadd_distrib RS sym]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1147 |
qed "neg_zdiv_mult_2"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1148 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1149 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1150 |
(*Not clear why this must be proved separately; probably number_of causes |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1151 |
simplification problems*) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1152 |
Goal "~ #0 $<= x ==> x $<= (#0::int)"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1153 |
by Auto_tac; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1154 |
val lemma = result(); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1155 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1156 |
Goal "number_of (v BIT b) div number_of (w BIT False) = \ |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1157 |
\ (if ~b | (#0::int) $<= number_of w \ |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1158 |
\ then number_of v div (number_of w) \ |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1159 |
\ else (number_of v $+ (#1::int)) div (number_of w))"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1160 |
by (simp_tac (simpset_of Int.thy addsimps [zadd_assoc, number_of_BIT]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1161 |
by (asm_simp_tac (simpset() |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1162 |
delsimps bin_arith_extra_simps@bin_rel_simps |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1163 |
addsimps [zdiv_zmult_zmult1, |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1164 |
pos_zdiv_mult_2, lemma, neg_zdiv_mult_2]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1165 |
qed "zdiv_number_of_BIT"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1166 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1167 |
Addsimps [zdiv_number_of_BIT]; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1168 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1169 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1170 |
(** computing "mod" by shifting (proofs resemble those for "div") **) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1171 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1172 |
Goal "(#0::int) $<= a ==> (#1 $+ #2$*b) mod (#2$*a) = #1 $+ #2 $* (b mod a)"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1173 |
by (zdiv_undefined_case_tac "a = #0" 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1174 |
by (subgoal_tac "#1 $<= a" 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1175 |
by (arith_tac 2); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1176 |
by (subgoal_tac "#1 $< a $* #2" 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1177 |
by (arith_tac 2); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1178 |
by (subgoal_tac "#2$*(#1 $+ b mod a) $<= #2$*a" 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1179 |
by (rtac zmult_zle_mono2 2); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1180 |
by (auto_tac (claset(), |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1181 |
simpset() addsimps [zadd_commute, zmult_commute, |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1182 |
add1_zle_eq, pos_mod_bound])); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1183 |
by (stac zmod_zadd1_eq 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1184 |
by (asm_simp_tac (simpset() addsimps [zmod_zmult_zmult2, |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1185 |
mod_pos_pos_trivial]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1186 |
by (rtac mod_pos_pos_trivial 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1187 |
by (asm_simp_tac (simpset() |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1188 |
addsimps [mod_pos_pos_trivial, |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1189 |
pos_mod_sign RS zadd_zle_mono1 RSN (2,order_trans)]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1190 |
by (auto_tac (claset(), |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1191 |
simpset() addsimps [mod_pos_pos_trivial])); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1192 |
by (subgoal_tac "#0 $<= b mod a" 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1193 |
by (asm_simp_tac (simpset() addsimps [pos_mod_sign]) 2); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1194 |
by (arith_tac 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1195 |
qed "pos_zmod_mult_2"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1196 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1197 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1198 |
Goal "a $<= (#0::int) ==> (#1 $+ #2$*b) mod (#2$*a) = #2 $* ((b$+#1) mod a) - #1"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1199 |
by (subgoal_tac |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1200 |
"(#1 $+ #2$*(-b-#1)) mod (#2$*(-a)) = #1 $+ #2$*((-b-#1) mod (-a))" 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1201 |
by (rtac pos_zmod_mult_2 2); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1202 |
by (auto_tac (claset(), |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1203 |
simpset() addsimps [zmult_zminus_right])); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1204 |
by (subgoal_tac "(#-1 - (#2 $* b)) = - (#1 $+ (#2 $* b))" 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1205 |
by (Simp_tac 2); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1206 |
by (asm_full_simp_tac (HOL_ss |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1207 |
addsimps [zmod_zminus_zminus, zdiff_def, |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1208 |
zminus_zadd_distrib RS sym]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1209 |
by (dtac (zminus_equation RS iffD1 RS sym) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1210 |
by Auto_tac; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1211 |
qed "neg_zmod_mult_2"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1212 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1213 |
Goal "number_of (v BIT b) mod number_of (w BIT False) = \ |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1214 |
\ (if b then \ |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1215 |
\ if (#0::int) $<= number_of w \ |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1216 |
\ then #2 $* (number_of v mod number_of w) $+ #1 \ |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1217 |
\ else #2 $* ((number_of v $+ (#1::int)) mod number_of w) - #1 \ |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1218 |
\ else #2 $* (number_of v mod number_of w))"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1219 |
by (simp_tac (simpset_of Int.thy addsimps [zadd_assoc, number_of_BIT]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1220 |
by (asm_simp_tac (simpset() |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1221 |
delsimps bin_arith_extra_simps@bin_rel_simps |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1222 |
addsimps [zmod_zmult_zmult1, |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1223 |
pos_zmod_mult_2, lemma, neg_zmod_mult_2]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1224 |
qed "zmod_number_of_BIT"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1225 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1226 |
Addsimps [zmod_number_of_BIT]; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1227 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1228 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1229 |
(** Quotients of signs **) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1230 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1231 |
Goal "[| a $< (#0::int); #0 $< b |] ==> a div b $< #0"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1232 |
by (subgoal_tac "a div b $<= #-1" 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1233 |
by (Force_tac 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1234 |
by (rtac order_trans 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1235 |
by (res_inst_tac [("a'","#-1")] zdiv_mono1 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1236 |
by (auto_tac (claset(), simpset() addsimps [zdiv_minus1])); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1237 |
qed "div_neg_pos_less0"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1238 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1239 |
Goal "[| (#0::int) $<= a; b $< #0 |] ==> a div b $<= #0"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1240 |
by (dtac zdiv_mono1_neg 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1241 |
by Auto_tac; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1242 |
qed "div_nonneg_neg_le0"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1243 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1244 |
Goal "(#0::int) $< b ==> (#0 $<= a div b) = (#0 $<= a)"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1245 |
by Auto_tac; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1246 |
by (dtac zdiv_mono1 2); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1247 |
by (auto_tac (claset(), simpset() addsimps [neq_iff_zless])); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1248 |
by (full_simp_tac (simpset() addsimps [not_zless_iff_zle RS sym]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1249 |
by (blast_tac (claset() addIs [div_neg_pos_less0]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1250 |
qed "pos_imp_zdiv_nonneg_iff"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1251 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1252 |
Goal "b $< (#0::int) ==> (#0 $<= a div b) = (a $<= (#0::int))"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1253 |
by (stac (zdiv_zminus_zminus RS sym) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1254 |
by (stac pos_imp_zdiv_nonneg_iff 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1255 |
by Auto_tac; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1256 |
qed "neg_imp_zdiv_nonneg_iff"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1257 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1258 |
(*But not (a div b $<= 0 iff a$<=0); consider a=1, b=2 when a div b = 0.*) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1259 |
Goal "(#0::int) $< b ==> (a div b $< #0) = (a $< #0)"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1260 |
by (asm_simp_tac (simpset() addsimps [linorder_not_le RS sym, |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1261 |
pos_imp_zdiv_nonneg_iff]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1262 |
qed "pos_imp_zdiv_neg_iff"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1263 |
|
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1264 |
(*Again the law fails for $<=: consider a = -1, b = -2 when a div b = 0*) |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1265 |
Goal "b $< (#0::int) ==> (a div b $< #0) = (#0 $< a)"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1266 |
by (asm_simp_tac (simpset() addsimps [linorder_not_le RS sym, |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1267 |
neg_imp_zdiv_nonneg_iff]) 1); |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1268 |
qed "neg_imp_zdiv_neg_iff"; |
ab26d6c8ebfe
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
paulson
parents:
diff
changeset
|
1269 |
*) |