author | paulson |
Mon, 04 Oct 2004 15:28:03 +0200 | |
changeset 15228 | 4d332d10fa3d |
parent 15140 | 322485b816ac |
child 15234 | ec91a90c604e |
permissions | -rw-r--r-- |
14128 | 1 |
(* Title: HOL/NatSimprocs.thy |
2 |
ID: $Id$ |
|
3 |
Copyright 2003 TU Muenchen |
|
4 |
*) |
|
5 |
||
6 |
header {*Simprocs for the Naturals*} |
|
7 |
||
15131 | 8 |
theory NatSimprocs |
15140 | 9 |
imports NatBin |
15131 | 10 |
files "int_factor_simprocs.ML" "nat_simprocs.ML" |
11 |
begin |
|
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
8858
diff
changeset
|
12 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
8858
diff
changeset
|
13 |
setup nat_simprocs_setup |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
8858
diff
changeset
|
14 |
|
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
15 |
subsection{*For simplifying @{term "Suc m - K"} and @{term "K - Suc m"}*} |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
16 |
|
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
17 |
text{*Where K above is a literal*} |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
18 |
|
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
19 |
lemma Suc_diff_eq_diff_pred: "Numeral0 < n ==> Suc m - n = m - (n - Numeral1)" |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
20 |
by (simp add: numeral_0_eq_0 numeral_1_eq_1 split add: nat_diff_split) |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
21 |
|
14577 | 22 |
text {*Now just instantiating @{text n} to @{text "number_of v"} does |
23 |
the right simplification, but with some redundant inequality |
|
24 |
tests.*} |
|
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
25 |
lemma neg_number_of_bin_pred_iff_0: |
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14353
diff
changeset
|
26 |
"neg (number_of (bin_pred v)::int) = (number_of v = (0::nat))" |
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
27 |
apply (subgoal_tac "neg (number_of (bin_pred v)) = (number_of v < Suc 0) ") |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
28 |
apply (simp only: less_Suc_eq_le le_0_eq) |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
29 |
apply (subst less_number_of_Suc, simp) |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
30 |
done |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
31 |
|
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
32 |
text{*No longer required as a simprule because of the @{text inverse_fold} |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
33 |
simproc*} |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
34 |
lemma Suc_diff_number_of: |
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14353
diff
changeset
|
35 |
"neg (number_of (bin_minus v)::int) ==> |
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
36 |
Suc m - (number_of v) = m - (number_of (bin_pred v))" |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
37 |
apply (subst Suc_diff_eq_diff_pred) |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
38 |
apply (simp add: ); |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
39 |
apply (simp del: nat_numeral_1_eq_1); |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
40 |
apply (auto simp only: diff_nat_number_of less_0_number_of [symmetric] |
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
41 |
neg_number_of_bin_pred_iff_0) |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
42 |
done |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
43 |
|
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
44 |
lemma diff_Suc_eq_diff_pred: "m - Suc n = (m - 1) - n" |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
45 |
by (simp add: numerals split add: nat_diff_split) |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
46 |
|
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
47 |
|
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
48 |
subsection{*For @{term nat_case} and @{term nat_rec}*} |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
49 |
|
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
50 |
lemma nat_case_number_of [simp]: |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
51 |
"nat_case a f (number_of v) = |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
52 |
(let pv = number_of (bin_pred v) in |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
53 |
if neg pv then a else f (nat pv))" |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
54 |
by (simp split add: nat.split add: Let_def neg_number_of_bin_pred_iff_0) |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
55 |
|
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
56 |
lemma nat_case_add_eq_if [simp]: |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
57 |
"nat_case a f ((number_of v) + n) = |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
58 |
(let pv = number_of (bin_pred v) in |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
59 |
if neg pv then nat_case a f n else f (nat pv + n))" |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
60 |
apply (subst add_eq_if) |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
61 |
apply (simp split add: nat.split |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
62 |
del: nat_numeral_1_eq_1 |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
63 |
add: numeral_1_eq_Suc_0 [symmetric] Let_def |
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
64 |
neg_imp_number_of_eq_0 neg_number_of_bin_pred_iff_0) |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
65 |
done |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
66 |
|
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
67 |
lemma nat_rec_number_of [simp]: |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
68 |
"nat_rec a f (number_of v) = |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
69 |
(let pv = number_of (bin_pred v) in |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
70 |
if neg pv then a else f (nat pv) (nat_rec a f (nat pv)))" |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
71 |
apply (case_tac " (number_of v) ::nat") |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
72 |
apply (simp_all (no_asm_simp) add: Let_def neg_number_of_bin_pred_iff_0) |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
73 |
apply (simp split add: split_if_asm) |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
74 |
done |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
75 |
|
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
76 |
lemma nat_rec_add_eq_if [simp]: |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
77 |
"nat_rec a f (number_of v + n) = |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
78 |
(let pv = number_of (bin_pred v) in |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
79 |
if neg pv then nat_rec a f n |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
80 |
else f (nat pv + n) (nat_rec a f (nat pv + n)))" |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
81 |
apply (subst add_eq_if) |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
82 |
apply (simp split add: nat.split |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
83 |
del: nat_numeral_1_eq_1 |
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
84 |
add: numeral_1_eq_Suc_0 [symmetric] Let_def neg_imp_number_of_eq_0 |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
85 |
neg_number_of_bin_pred_iff_0) |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
86 |
done |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
87 |
|
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
88 |
|
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
89 |
subsection{*Various Other Lemmas*} |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
90 |
|
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
91 |
subsubsection{*Evens and Odds, for Mutilated Chess Board*} |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
92 |
|
14436 | 93 |
text{*Lemmas for specialist use, NOT as default simprules*} |
94 |
lemma nat_mult_2: "2 * z = (z+z::nat)" |
|
95 |
proof - |
|
96 |
have "2*z = (1 + 1)*z" by simp |
|
97 |
also have "... = z+z" by (simp add: left_distrib) |
|
98 |
finally show ?thesis . |
|
99 |
qed |
|
100 |
||
101 |
lemma nat_mult_2_right: "z * 2 = (z+z::nat)" |
|
102 |
by (subst mult_commute, rule nat_mult_2) |
|
103 |
||
104 |
text{*Case analysis on @{term "n<2"}*} |
|
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
105 |
lemma less_2_cases: "(n::nat) < 2 ==> n = 0 | n = Suc 0" |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
106 |
by arith |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
107 |
|
14436 | 108 |
lemma div2_Suc_Suc [simp]: "Suc(Suc m) div 2 = Suc (m div 2)" |
109 |
by arith |
|
110 |
||
111 |
lemma add_self_div_2 [simp]: "(m + m) div 2 = (m::nat)" |
|
112 |
by (simp add: nat_mult_2 [symmetric]) |
|
113 |
||
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
114 |
lemma mod2_Suc_Suc [simp]: "Suc(Suc(m)) mod 2 = m mod 2" |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
115 |
apply (subgoal_tac "m mod 2 < 2") |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
116 |
apply (erule less_2_cases [THEN disjE]) |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
117 |
apply (simp_all (no_asm_simp) add: Let_def mod_Suc nat_1) |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
118 |
done |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
119 |
|
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
120 |
lemma mod2_gr_0 [simp]: "!!m::nat. (0 < m mod 2) = (m mod 2 = 1)" |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
121 |
apply (subgoal_tac "m mod 2 < 2") |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
122 |
apply (force simp del: mod_less_divisor, simp) |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
123 |
done |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
124 |
|
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
125 |
subsubsection{*Removal of Small Numerals: 0, 1 and (in additive positions) 2*} |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
126 |
|
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
127 |
lemma add_2_eq_Suc [simp]: "2 + n = Suc (Suc n)" |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
128 |
by simp |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
129 |
|
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
130 |
lemma add_2_eq_Suc' [simp]: "n + 2 = Suc (Suc n)" |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
131 |
by simp |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
132 |
|
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
133 |
text{*Can be used to eliminate long strings of Sucs, but not by default*} |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
134 |
lemma Suc3_eq_add_3: "Suc (Suc (Suc n)) = 3 + n" |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
135 |
by simp |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
136 |
|
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
137 |
|
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
138 |
text{*These lemmas collapse some needless occurrences of Suc: |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
139 |
at least three Sucs, since two and fewer are rewritten back to Suc again! |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
140 |
We already have some rules to simplify operands smaller than 3.*} |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
141 |
|
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
142 |
lemma div_Suc_eq_div_add3 [simp]: "m div (Suc (Suc (Suc n))) = m div (3+n)" |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
143 |
by (simp add: Suc3_eq_add_3) |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
144 |
|
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
145 |
lemma mod_Suc_eq_mod_add3 [simp]: "m mod (Suc (Suc (Suc n))) = m mod (3+n)" |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
146 |
by (simp add: Suc3_eq_add_3) |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
147 |
|
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
148 |
lemma Suc_div_eq_add3_div: "(Suc (Suc (Suc m))) div n = (3+m) div n" |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
149 |
by (simp add: Suc3_eq_add_3) |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
150 |
|
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
151 |
lemma Suc_mod_eq_add3_mod: "(Suc (Suc (Suc m))) mod n = (3+m) mod n" |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
152 |
by (simp add: Suc3_eq_add_3) |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
153 |
|
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
154 |
declare Suc_div_eq_add3_div [of _ "number_of v", standard, simp] |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
155 |
declare Suc_mod_eq_add3_mod [of _ "number_of v", standard, simp] |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14128
diff
changeset
|
156 |
|
14288 | 157 |
|
158 |
subsection{*Special Simplification for Constants*} |
|
159 |
||
160 |
text{*These belong here, late in the development of HOL, to prevent their |
|
161 |
interfering with proofs of abstract properties of instances of the function |
|
162 |
@{term number_of}*} |
|
163 |
||
164 |
text{*These distributive laws move literals inside sums and differences.*} |
|
165 |
declare left_distrib [of _ _ "number_of v", standard, simp] |
|
166 |
declare right_distrib [of "number_of v", standard, simp] |
|
167 |
||
168 |
declare left_diff_distrib [of _ _ "number_of v", standard, simp] |
|
169 |
declare right_diff_distrib [of "number_of v", standard, simp] |
|
170 |
||
171 |
text{*These are actually for fields, like real: but where else to put them?*} |
|
172 |
declare zero_less_divide_iff [of "number_of w", standard, simp] |
|
173 |
declare divide_less_0_iff [of "number_of w", standard, simp] |
|
174 |
declare zero_le_divide_iff [of "number_of w", standard, simp] |
|
175 |
declare divide_le_0_iff [of "number_of w", standard, simp] |
|
176 |
||
14577 | 177 |
text {*Replaces @{text "inverse #nn"} by @{text "1/#nn"}. It looks |
178 |
strange, but then other simprocs simplify the quotient.*} |
|
179 |
||
14288 | 180 |
declare inverse_eq_divide [of "number_of w", standard, simp] |
181 |
||
182 |
text{*These laws simplify inequalities, moving unary minus from a term |
|
183 |
into the literal.*} |
|
184 |
declare less_minus_iff [of "number_of v", standard, simp] |
|
185 |
declare le_minus_iff [of "number_of v", standard, simp] |
|
186 |
declare equation_minus_iff [of "number_of v", standard, simp] |
|
187 |
||
188 |
declare minus_less_iff [of _ "number_of v", standard, simp] |
|
189 |
declare minus_le_iff [of _ "number_of v", standard, simp] |
|
190 |
declare minus_equation_iff [of _ "number_of v", standard, simp] |
|
191 |
||
192 |
text{*These simplify inequalities where one side is the constant 1.*} |
|
193 |
declare less_minus_iff [of 1, simplified, simp] |
|
194 |
declare le_minus_iff [of 1, simplified, simp] |
|
195 |
declare equation_minus_iff [of 1, simplified, simp] |
|
196 |
||
197 |
declare minus_less_iff [of _ 1, simplified, simp] |
|
198 |
declare minus_le_iff [of _ 1, simplified, simp] |
|
199 |
declare minus_equation_iff [of _ 1, simplified, simp] |
|
200 |
||
14577 | 201 |
text {*Cancellation of constant factors in comparisons (@{text "<"} and @{text "\<le>"}) *} |
14288 | 202 |
|
203 |
declare mult_less_cancel_left [of "number_of v", standard, simp] |
|
204 |
declare mult_less_cancel_right [of _ "number_of v", standard, simp] |
|
205 |
declare mult_le_cancel_left [of "number_of v", standard, simp] |
|
206 |
declare mult_le_cancel_right [of _ "number_of v", standard, simp] |
|
207 |
||
14577 | 208 |
text {*Multiplying out constant divisors in comparisons (@{text "<"}, @{text "\<le>"} and @{text "="}) *} |
14288 | 209 |
|
210 |
declare le_divide_eq [of _ _ "number_of w", standard, simp] |
|
211 |
declare divide_le_eq [of _ "number_of w", standard, simp] |
|
212 |
declare less_divide_eq [of _ _ "number_of w", standard, simp] |
|
213 |
declare divide_less_eq [of _ "number_of w", standard, simp] |
|
214 |
declare eq_divide_eq [of _ _ "number_of w", standard, simp] |
|
215 |
declare divide_eq_eq [of _ "number_of w", standard, simp] |
|
216 |
||
217 |
||
15228 | 218 |
subsection{*Optional Simplification Rules Involving Constants*} |
219 |
||
220 |
text{*Simplify quotients that are compared with a literal constant.*} |
|
221 |
||
222 |
lemmas le_divide_eq_number_of = le_divide_eq [of "number_of w", standard] |
|
223 |
lemmas divide_le_eq_number_of = divide_le_eq [of _ _ "number_of w", standard] |
|
224 |
lemmas less_divide_eq_number_of = less_divide_eq [of "number_of w", standard] |
|
225 |
lemmas divide_less_eq_number_of = divide_less_eq [of _ _ "number_of w", standard] |
|
226 |
lemmas eq_divide_eq_number_of = eq_divide_eq [of "number_of w", standard] |
|
227 |
lemmas divide_eq_eq_number_of = divide_eq_eq [of _ _ "number_of w", standard] |
|
228 |
||
229 |
text{*Simplify quotients that are compared with the value 1.*} |
|
230 |
||
231 |
lemma le_divide_eq_1: |
|
232 |
fixes a :: "'a :: {ordered_field,division_by_zero}" |
|
233 |
shows "(1 \<le> b / a) = ((0 < a & a \<le> b) | (a < 0 & b \<le> a))" |
|
234 |
by (auto simp add: le_divide_eq) |
|
235 |
||
236 |
lemma divide_le_eq_1: |
|
237 |
fixes a :: "'a :: {ordered_field,division_by_zero}" |
|
238 |
shows "(b / a \<le> 1) = ((0 < a & b \<le> a) | (a < 0 & a \<le> b) | a=0)" |
|
239 |
by (auto simp add: divide_le_eq) |
|
240 |
||
241 |
lemma less_divide_eq_1: |
|
242 |
fixes a :: "'a :: {ordered_field,division_by_zero}" |
|
243 |
shows "(1 < b / a) = ((0 < a & a < b) | (a < 0 & b < a))" |
|
244 |
by (auto simp add: less_divide_eq) |
|
245 |
||
246 |
lemma divide_less_eq_1: |
|
247 |
fixes a :: "'a :: {ordered_field,division_by_zero}" |
|
248 |
shows "(b / a < 1) = ((0 < a & b < a) | (a < 0 & a < b) | a=0)" |
|
249 |
by (auto simp add: divide_less_eq) |
|
250 |
||
251 |
||
252 |
text{*Not good as automatic simprules because they cause case splits.*} |
|
253 |
lemmas divide_const_simps = |
|
254 |
le_divide_eq_number_of divide_le_eq_number_of less_divide_eq_number_of |
|
255 |
divide_less_eq_number_of eq_divide_eq_number_of divide_eq_eq_number_of |
|
256 |
le_divide_eq_1 divide_le_eq_1 less_divide_eq_1 divide_less_eq_1 |
|
257 |
||
258 |
||
259 |
subsection{*Conditional Simplification Rules: No Case Splits*} |
|
260 |
||
261 |
lemma le_divide_eq_1_pos [simp]: |
|
262 |
fixes a :: "'a :: {ordered_field,division_by_zero}" |
|
263 |
shows "0 < a \<Longrightarrow> (1 \<le> b / a) = (a \<le> b)" |
|
264 |
by (auto simp add: le_divide_eq) |
|
265 |
||
266 |
lemma le_divide_eq_1_neg [simp]: |
|
267 |
fixes a :: "'a :: {ordered_field,division_by_zero}" |
|
268 |
shows "a < 0 \<Longrightarrow> (1 \<le> b / a) = (b \<le> a)" |
|
269 |
by (auto simp add: le_divide_eq) |
|
270 |
||
271 |
lemma divide_le_eq_1_pos [simp]: |
|
272 |
fixes a :: "'a :: {ordered_field,division_by_zero}" |
|
273 |
shows "0 < a \<Longrightarrow> (b / a \<le> 1) = (b \<le> a)" |
|
274 |
by (auto simp add: divide_le_eq) |
|
275 |
||
276 |
lemma divide_le_eq_1_neg [simp]: |
|
277 |
fixes a :: "'a :: {ordered_field,division_by_zero}" |
|
278 |
shows "a < 0 \<Longrightarrow> (b / a \<le> 1) = (a \<le> b)" |
|
279 |
by (auto simp add: divide_le_eq) |
|
280 |
||
281 |
lemma less_divide_eq_1_pos [simp]: |
|
282 |
fixes a :: "'a :: {ordered_field,division_by_zero}" |
|
283 |
shows "0 < a \<Longrightarrow> (1 < b / a) = (a < b)" |
|
284 |
by (auto simp add: less_divide_eq) |
|
285 |
||
286 |
lemma less_divide_eq_1_neg [simp]: |
|
287 |
fixes a :: "'a :: {ordered_field,division_by_zero}" |
|
288 |
shows "a < 0 \<Longrightarrow> (1 < b / a) = (b < a)" |
|
289 |
by (auto simp add: less_divide_eq) |
|
290 |
||
291 |
lemma divide_less_eq_1_pos [simp]: |
|
292 |
fixes a :: "'a :: {ordered_field,division_by_zero}" |
|
293 |
shows "0 < a \<Longrightarrow> (b / a < 1) = (b < a)" |
|
294 |
by (auto simp add: divide_less_eq) |
|
295 |
||
296 |
lemma eq_divide_eq_1 [simp]: |
|
297 |
fixes a :: "'a :: {ordered_field,division_by_zero}" |
|
298 |
shows "(1 = b / a) = ((a \<noteq> 0 & a = b))" |
|
299 |
by (auto simp add: eq_divide_eq) |
|
300 |
||
301 |
lemma divide_eq_eq_1 [simp]: |
|
302 |
fixes a :: "'a :: {ordered_field,division_by_zero}" |
|
303 |
shows "(b / a = 1) = ((a \<noteq> 0 & a = b))" |
|
304 |
by (auto simp add: divide_eq_eq) |
|
305 |
||
306 |
||
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
307 |
subsubsection{*Division By @{term "-1"}*} |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
308 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
309 |
lemma divide_minus1 [simp]: |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
310 |
"x/-1 = -(x::'a::{field,division_by_zero,number_ring})" |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
311 |
by simp |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
312 |
|
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
313 |
lemma minus1_divide [simp]: |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
314 |
"-1 / (x::'a::{field,division_by_zero,number_ring}) = - (1/x)" |
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14387
diff
changeset
|
315 |
by (simp add: divide_inverse inverse_minus_eq) |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
316 |
|
14475 | 317 |
lemma half_gt_zero_iff: |
318 |
"(0 < r/2) = (0 < (r::'a::{ordered_field,division_by_zero,number_ring}))" |
|
319 |
by auto |
|
320 |
||
321 |
lemmas half_gt_zero = half_gt_zero_iff [THEN iffD2, simp] |
|
322 |
||
14436 | 323 |
|
324 |
||
325 |
||
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
326 |
ML |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
327 |
{* |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
328 |
val divide_minus1 = thm "divide_minus1"; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
329 |
val minus1_divide = thm "minus1_divide"; |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
330 |
*} |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
331 |
|
8858
b739f0ecc1fa
new dummy theory; prevents strange errors when loading NatSimprocs.ML
paulson
parents:
diff
changeset
|
332 |
end |