author | bulwahn |
Tue, 26 Feb 2008 11:18:43 +0100 | |
changeset 26143 | 314c0bcb7df7 |
parent 26101 | a657683e902a |
child 26149 | 6094349a4de9 |
permissions | -rw-r--r-- |
923 | 1 |
(* Title: HOL/Nat.thy |
2 |
ID: $Id$ |
|
21243 | 3 |
Author: Tobias Nipkow and Lawrence C Paulson and Markus Wenzel |
923 | 4 |
|
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
7702
diff
changeset
|
5 |
Type "nat" is a linear order, and a datatype; arithmetic operators + - |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
7702
diff
changeset
|
6 |
and * (for div, mod and dvd, see theory Divides). |
923 | 7 |
*) |
8 |
||
13449 | 9 |
header {* Natural numbers *} |
10 |
||
15131 | 11 |
theory Nat |
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
12 |
imports Inductive Ring_and_Field |
23263 | 13 |
uses |
14 |
"~~/src/Tools/rat.ML" |
|
15 |
"~~/src/Provers/Arith/cancel_sums.ML" |
|
16 |
("arith_data.ML") |
|
24091 | 17 |
"~~/src/Provers/Arith/fast_lin_arith.ML" |
18 |
("Tools/lin_arith.ML") |
|
15131 | 19 |
begin |
13449 | 20 |
|
21 |
subsection {* Type @{text ind} *} |
|
22 |
||
23 |
typedecl ind |
|
24 |
||
19573 | 25 |
axiomatization |
26 |
Zero_Rep :: ind and |
|
27 |
Suc_Rep :: "ind => ind" |
|
28 |
where |
|
13449 | 29 |
-- {* the axiom of infinity in 2 parts *} |
19573 | 30 |
inj_Suc_Rep: "inj Suc_Rep" and |
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
31 |
Suc_Rep_not_Zero_Rep: "Suc_Rep x \<noteq> Zero_Rep" |
19573 | 32 |
|
13449 | 33 |
|
34 |
subsection {* Type nat *} |
|
35 |
||
36 |
text {* Type definition *} |
|
37 |
||
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
38 |
inductive Nat :: "ind \<Rightarrow> bool" |
22262 | 39 |
where |
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
40 |
Zero_RepI: "Nat Zero_Rep" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
41 |
| Suc_RepI: "Nat i \<Longrightarrow> Nat (Suc_Rep i)" |
13449 | 42 |
|
43 |
global |
|
44 |
||
45 |
typedef (open Nat) |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
46 |
nat = "Collect Nat" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
47 |
by (rule exI, rule CollectI, rule Nat.Zero_RepI) |
13449 | 48 |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
49 |
constdefs |
13449 | 50 |
Suc :: "nat => nat" |
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
51 |
Suc_def: "Suc == (%n. Abs_Nat (Suc_Rep (Rep_Nat n)))" |
13449 | 52 |
|
53 |
local |
|
54 |
||
25510 | 55 |
instantiation nat :: zero |
56 |
begin |
|
57 |
||
58 |
definition Zero_nat_def [code func del]: |
|
59 |
"0 = Abs_Nat Zero_Rep" |
|
60 |
||
61 |
instance .. |
|
62 |
||
63 |
end |
|
24995 | 64 |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
65 |
lemma nat_induct: "P 0 ==> (!!n. P n ==> P (Suc n)) ==> P n" |
13449 | 66 |
apply (unfold Zero_nat_def Suc_def) |
67 |
apply (rule Rep_Nat_inverse [THEN subst]) -- {* types force good instantiation *} |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
68 |
apply (erule Rep_Nat [THEN CollectD, THEN Nat.induct]) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
69 |
apply (iprover elim: Abs_Nat_inverse [OF CollectI, THEN subst]) |
13449 | 70 |
done |
71 |
||
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
72 |
lemma Suc_not_Zero [iff]: "Suc m \<noteq> 0" |
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
73 |
by (simp add: Zero_nat_def Suc_def |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
74 |
Abs_Nat_inject Rep_Nat [THEN CollectD] Suc_RepI Zero_RepI |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
75 |
Suc_Rep_not_Zero_Rep) |
13449 | 76 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
77 |
lemma Zero_not_Suc [iff]: "0 \<noteq> Suc m" |
13449 | 78 |
by (rule not_sym, rule Suc_not_Zero not_sym) |
79 |
||
16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16635
diff
changeset
|
80 |
lemma inj_Suc[simp]: "inj_on Suc N" |
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
81 |
by (simp add: Suc_def inj_on_def Abs_Nat_inject Rep_Nat [THEN CollectD] Suc_RepI |
22718 | 82 |
inj_Suc_Rep [THEN inj_eq] Rep_Nat_inject) |
13449 | 83 |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
84 |
lemma Suc_Suc_eq [iff]: "Suc m = Suc n \<longleftrightarrow> m = n" |
15413 | 85 |
by (rule inj_Suc [THEN inj_eq]) |
13449 | 86 |
|
5188
633ec5f6c155
Declaration of type 'nat' as a datatype (this allows usage of
berghofe
parents:
4640
diff
changeset
|
87 |
rep_datatype nat |
13449 | 88 |
distinct Suc_not_Zero Zero_not_Suc |
89 |
inject Suc_Suc_eq |
|
21411 | 90 |
induction nat_induct |
91 |
||
92 |
declare nat.induct [case_names 0 Suc, induct type: nat] |
|
93 |
declare nat.exhaust [case_names 0 Suc, cases type: nat] |
|
13449 | 94 |
|
21672 | 95 |
lemmas nat_rec_0 = nat.recs(1) |
96 |
and nat_rec_Suc = nat.recs(2) |
|
97 |
||
98 |
lemmas nat_case_0 = nat.cases(1) |
|
99 |
and nat_case_Suc = nat.cases(2) |
|
100 |
||
24995 | 101 |
|
102 |
text {* Injectiveness and distinctness lemmas *} |
|
103 |
||
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
104 |
lemma Suc_neq_Zero: "Suc m = 0 \<Longrightarrow> R" |
25162 | 105 |
by (rule notE, rule Suc_not_Zero) |
24995 | 106 |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
107 |
lemma Zero_neq_Suc: "0 = Suc m \<Longrightarrow> R" |
25162 | 108 |
by (rule Suc_neq_Zero, erule sym) |
24995 | 109 |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
110 |
lemma Suc_inject: "Suc x = Suc y \<Longrightarrow> x = y" |
25162 | 111 |
by (rule inj_Suc [THEN injD]) |
24995 | 112 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
113 |
lemma n_not_Suc_n: "n \<noteq> Suc n" |
25162 | 114 |
by (induct n) simp_all |
13449 | 115 |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
116 |
lemma Suc_n_not_n: "Suc n \<noteq> n" |
25162 | 117 |
by (rule not_sym, rule n_not_Suc_n) |
13449 | 118 |
|
119 |
text {* A special form of induction for reasoning |
|
120 |
about @{term "m < n"} and @{term "m - n"} *} |
|
121 |
||
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
122 |
lemma diff_induct: "(!!x. P x 0) ==> (!!y. P 0 (Suc y)) ==> |
13449 | 123 |
(!!x y. P x y ==> P (Suc x) (Suc y)) ==> P m n" |
14208 | 124 |
apply (rule_tac x = m in spec) |
15251 | 125 |
apply (induct n) |
13449 | 126 |
prefer 2 |
127 |
apply (rule allI) |
|
17589 | 128 |
apply (induct_tac x, iprover+) |
13449 | 129 |
done |
130 |
||
24995 | 131 |
|
132 |
subsection {* Arithmetic operators *} |
|
133 |
||
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
134 |
instantiation nat :: "{minus, comm_monoid_add}" |
25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25563
diff
changeset
|
135 |
begin |
24995 | 136 |
|
25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25563
diff
changeset
|
137 |
primrec plus_nat |
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25563
diff
changeset
|
138 |
where |
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25563
diff
changeset
|
139 |
add_0: "0 + n = (n\<Colon>nat)" |
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25563
diff
changeset
|
140 |
| add_Suc: "Suc m + n = Suc (m + n)" |
24995 | 141 |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
142 |
lemma add_0_right [simp]: "m + 0 = (m::nat)" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
143 |
by (induct m) simp_all |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
144 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
145 |
lemma add_Suc_right [simp]: "m + Suc n = Suc (m + n)" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
146 |
by (induct m) simp_all |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
147 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
148 |
lemma add_Suc_shift [code]: "Suc m + n = m + Suc n" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
149 |
by simp |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
150 |
|
25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25563
diff
changeset
|
151 |
primrec minus_nat |
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25563
diff
changeset
|
152 |
where |
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25563
diff
changeset
|
153 |
diff_0: "m - 0 = (m\<Colon>nat)" |
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25563
diff
changeset
|
154 |
| diff_Suc: "m - Suc n = (case m - n of 0 => 0 | Suc k => k)" |
24995 | 155 |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
156 |
declare diff_Suc [simp del, code del] |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
157 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
158 |
lemma diff_0_eq_0 [simp, code]: "0 - n = (0::nat)" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
159 |
by (induct n) (simp_all add: diff_Suc) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
160 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
161 |
lemma diff_Suc_Suc [simp, code]: "Suc m - Suc n = m - n" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
162 |
by (induct n) (simp_all add: diff_Suc) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
163 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
164 |
instance proof |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
165 |
fix n m q :: nat |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
166 |
show "(n + m) + q = n + (m + q)" by (induct n) simp_all |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
167 |
show "n + m = m + n" by (induct n) simp_all |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
168 |
show "0 + n = n" by simp |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
169 |
qed |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
170 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
171 |
end |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
172 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
173 |
instantiation nat :: comm_semiring_1_cancel |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
174 |
begin |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
175 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
176 |
definition |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
177 |
One_nat_def [simp]: "1 = Suc 0" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
178 |
|
25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25563
diff
changeset
|
179 |
primrec times_nat |
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25563
diff
changeset
|
180 |
where |
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25563
diff
changeset
|
181 |
mult_0: "0 * n = (0\<Colon>nat)" |
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25563
diff
changeset
|
182 |
| mult_Suc: "Suc m * n = n + (m * n)" |
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25563
diff
changeset
|
183 |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
184 |
lemma mult_0_right [simp]: "(m::nat) * 0 = 0" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
185 |
by (induct m) simp_all |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
186 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
187 |
lemma mult_Suc_right [simp]: "m * Suc n = m + (m * n)" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
188 |
by (induct m) (simp_all add: add_left_commute) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
189 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
190 |
lemma add_mult_distrib: "(m + n) * k = (m * k) + ((n * k)::nat)" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
191 |
by (induct m) (simp_all add: add_assoc) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
192 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
193 |
instance proof |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
194 |
fix n m q :: nat |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
195 |
show "0 \<noteq> (1::nat)" by simp |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
196 |
show "1 * n = n" by simp |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
197 |
show "n * m = m * n" by (induct n) simp_all |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
198 |
show "(n * m) * q = n * (m * q)" by (induct n) (simp_all add: add_mult_distrib) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
199 |
show "(n + m) * q = n * q + m * q" by (rule add_mult_distrib) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
200 |
assume "n + m = n + q" thus "m = q" by (induct n) simp_all |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
201 |
qed |
25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25563
diff
changeset
|
202 |
|
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25563
diff
changeset
|
203 |
end |
24995 | 204 |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
205 |
subsubsection {* Addition *} |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
206 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
207 |
lemma nat_add_assoc: "(m + n) + k = m + ((n + k)::nat)" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
208 |
by (rule add_assoc) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
209 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
210 |
lemma nat_add_commute: "m + n = n + (m::nat)" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
211 |
by (rule add_commute) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
212 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
213 |
lemma nat_add_left_commute: "x + (y + z) = y + ((x + z)::nat)" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
214 |
by (rule add_left_commute) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
215 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
216 |
lemma nat_add_left_cancel [simp]: "(k + m = k + n) = (m = (n::nat))" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
217 |
by (rule add_left_cancel) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
218 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
219 |
lemma nat_add_right_cancel [simp]: "(m + k = n + k) = (m=(n::nat))" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
220 |
by (rule add_right_cancel) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
221 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
222 |
text {* Reasoning about @{text "m + 0 = 0"}, etc. *} |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
223 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
224 |
lemma add_is_0 [iff]: |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
225 |
fixes m n :: nat |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
226 |
shows "(m + n = 0) = (m = 0 & n = 0)" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
227 |
by (cases m) simp_all |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
228 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
229 |
lemma add_is_1: |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
230 |
"(m+n= Suc 0) = (m= Suc 0 & n=0 | m=0 & n= Suc 0)" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
231 |
by (cases m) simp_all |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
232 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
233 |
lemma one_is_add: |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
234 |
"(Suc 0 = m + n) = (m = Suc 0 & n = 0 | m = 0 & n = Suc 0)" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
235 |
by (rule trans, rule eq_commute, rule add_is_1) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
236 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
237 |
lemma add_eq_self_zero: |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
238 |
fixes m n :: nat |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
239 |
shows "m + n = m \<Longrightarrow> n = 0" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
240 |
by (induct m) simp_all |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
241 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
242 |
lemma inj_on_add_nat[simp]: "inj_on (%n::nat. n+k) N" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
243 |
apply (induct k) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
244 |
apply simp |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
245 |
apply(drule comp_inj_on[OF _ inj_Suc]) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
246 |
apply (simp add:o_def) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
247 |
done |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
248 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
249 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
250 |
subsubsection {* Difference *} |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
251 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
252 |
lemma diff_self_eq_0 [simp]: "(m\<Colon>nat) - m = 0" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
253 |
by (induct m) simp_all |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
254 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
255 |
lemma diff_diff_left: "(i::nat) - j - k = i - (j + k)" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
256 |
by (induct i j rule: diff_induct) simp_all |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
257 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
258 |
lemma Suc_diff_diff [simp]: "(Suc m - n) - Suc k = m - n - k" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
259 |
by (simp add: diff_diff_left) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
260 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
261 |
lemma diff_commute: "(i::nat) - j - k = i - k - j" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
262 |
by (simp add: diff_diff_left add_commute) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
263 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
264 |
lemma diff_add_inverse: "(n + m) - n = (m::nat)" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
265 |
by (induct n) simp_all |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
266 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
267 |
lemma diff_add_inverse2: "(m + n) - n = (m::nat)" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
268 |
by (simp add: diff_add_inverse add_commute [of m n]) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
269 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
270 |
lemma diff_cancel: "(k + m) - (k + n) = m - (n::nat)" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
271 |
by (induct k) simp_all |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
272 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
273 |
lemma diff_cancel2: "(m + k) - (n + k) = m - (n::nat)" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
274 |
by (simp add: diff_cancel add_commute) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
275 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
276 |
lemma diff_add_0: "n - (n + m) = (0::nat)" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
277 |
by (induct n) simp_all |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
278 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
279 |
text {* Difference distributes over multiplication *} |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
280 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
281 |
lemma diff_mult_distrib: "((m::nat) - n) * k = (m * k) - (n * k)" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
282 |
by (induct m n rule: diff_induct) (simp_all add: diff_cancel) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
283 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
284 |
lemma diff_mult_distrib2: "k * ((m::nat) - n) = (k * m) - (k * n)" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
285 |
by (simp add: diff_mult_distrib mult_commute [of k]) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
286 |
-- {* NOT added as rewrites, since sometimes they are used from right-to-left *} |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
287 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
288 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
289 |
subsubsection {* Multiplication *} |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
290 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
291 |
lemma nat_mult_assoc: "(m * n) * k = m * ((n * k)::nat)" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
292 |
by (rule mult_assoc) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
293 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
294 |
lemma nat_mult_commute: "m * n = n * (m::nat)" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
295 |
by (rule mult_commute) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
296 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
297 |
lemma add_mult_distrib2: "k * (m + n) = (k * m) + ((k * n)::nat)" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
298 |
by (rule right_distrib) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
299 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
300 |
lemma mult_is_0 [simp]: "((m::nat) * n = 0) = (m=0 | n=0)" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
301 |
by (induct m) auto |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
302 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
303 |
lemmas nat_distrib = |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
304 |
add_mult_distrib add_mult_distrib2 diff_mult_distrib diff_mult_distrib2 |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
305 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
306 |
lemma mult_eq_1_iff [simp]: "(m * n = Suc 0) = (m = 1 & n = 1)" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
307 |
apply (induct m) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
308 |
apply simp |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
309 |
apply (induct n) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
310 |
apply auto |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
311 |
done |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
312 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
313 |
lemma one_eq_mult_iff [simp,noatp]: "(Suc 0 = m * n) = (m = 1 & n = 1)" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
314 |
apply (rule trans) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
315 |
apply (rule_tac [2] mult_eq_1_iff, fastsimp) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
316 |
done |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
317 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
318 |
lemma mult_cancel1 [simp]: "(k * m = k * n) = (m = n | (k = (0::nat)))" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
319 |
proof - |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
320 |
have "k \<noteq> 0 \<Longrightarrow> k * m = k * n \<Longrightarrow> m = n" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
321 |
proof (induct n arbitrary: m) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
322 |
case 0 then show "m = 0" by simp |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
323 |
next |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
324 |
case (Suc n) then show "m = Suc n" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
325 |
by (cases m) (simp_all add: eq_commute [of "0"]) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
326 |
qed |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
327 |
then show ?thesis by auto |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
328 |
qed |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
329 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
330 |
lemma mult_cancel2 [simp]: "(m * k = n * k) = (m = n | (k = (0::nat)))" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
331 |
by (simp add: mult_commute) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
332 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
333 |
lemma Suc_mult_cancel1: "(Suc k * m = Suc k * n) = (m = n)" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
334 |
by (subst mult_cancel1) simp |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
335 |
|
24995 | 336 |
|
337 |
subsection {* Orders on @{typ nat} *} |
|
338 |
||
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
339 |
subsubsection {* Operation definition *} |
24995 | 340 |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
341 |
instantiation nat :: linorder |
25510 | 342 |
begin |
343 |
||
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
344 |
primrec less_eq_nat where |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
345 |
"(0\<Colon>nat) \<le> n \<longleftrightarrow> True" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
346 |
| "Suc m \<le> n \<longleftrightarrow> (case n of 0 \<Rightarrow> False | Suc n \<Rightarrow> m \<le> n)" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
347 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
348 |
declare less_eq_nat.simps [simp del, code del] |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
349 |
lemma [code]: "(0\<Colon>nat) \<le> n \<longleftrightarrow> True" by (simp add: less_eq_nat.simps) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
350 |
lemma le0 [iff]: "0 \<le> (n\<Colon>nat)" by (simp add: less_eq_nat.simps) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
351 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
352 |
definition less_nat where |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
353 |
less_eq_Suc_le [code func del]: "n < m \<longleftrightarrow> Suc n \<le> m" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
354 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
355 |
lemma Suc_le_mono [iff]: "Suc n \<le> Suc m \<longleftrightarrow> n \<le> m" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
356 |
by (simp add: less_eq_nat.simps(2)) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
357 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
358 |
lemma Suc_le_eq [code]: "Suc m \<le> n \<longleftrightarrow> m < n" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
359 |
unfolding less_eq_Suc_le .. |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
360 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
361 |
lemma le_0_eq [iff]: "(n\<Colon>nat) \<le> 0 \<longleftrightarrow> n = 0" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
362 |
by (induct n) (simp_all add: less_eq_nat.simps(2)) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
363 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
364 |
lemma not_less0 [iff]: "\<not> n < (0\<Colon>nat)" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
365 |
by (simp add: less_eq_Suc_le) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
366 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
367 |
lemma less_nat_zero_code [code]: "n < (0\<Colon>nat) \<longleftrightarrow> False" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
368 |
by simp |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
369 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
370 |
lemma Suc_less_eq [iff]: "Suc m < Suc n \<longleftrightarrow> m < n" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
371 |
by (simp add: less_eq_Suc_le) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
372 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
373 |
lemma less_Suc_eq_le [code]: "m < Suc n \<longleftrightarrow> m \<le> n" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
374 |
by (simp add: less_eq_Suc_le) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
375 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
376 |
lemma le_SucI: "m \<le> n \<Longrightarrow> m \<le> Suc n" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
377 |
by (induct m arbitrary: n) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
378 |
(simp_all add: less_eq_nat.simps(2) split: nat.splits) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
379 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
380 |
lemma Suc_leD: "Suc m \<le> n \<Longrightarrow> m \<le> n" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
381 |
by (cases n) (auto intro: le_SucI) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
382 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
383 |
lemma less_SucI: "m < n \<Longrightarrow> m < Suc n" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
384 |
by (simp add: less_eq_Suc_le) (erule Suc_leD) |
24995 | 385 |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
386 |
lemma Suc_lessD: "Suc m < n \<Longrightarrow> m < n" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
387 |
by (simp add: less_eq_Suc_le) (erule Suc_leD) |
25510 | 388 |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
389 |
instance proof |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
390 |
fix n m :: nat |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
391 |
have less_imp_le: "n < m \<Longrightarrow> n \<le> m" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
392 |
unfolding less_eq_Suc_le by (erule Suc_leD) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
393 |
have irrefl: "\<not> m < m" by (induct m) auto |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
394 |
have strict: "n \<le> m \<Longrightarrow> n \<noteq> m \<Longrightarrow> n < m" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
395 |
proof (induct n arbitrary: m) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
396 |
case 0 then show ?case |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
397 |
by (cases m) (simp_all add: less_eq_Suc_le) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
398 |
next |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
399 |
case (Suc n) then show ?case |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
400 |
by (cases m) (simp_all add: less_eq_Suc_le) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
401 |
qed |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
402 |
show "n < m \<longleftrightarrow> n \<le> m \<and> n \<noteq> m" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
403 |
by (auto simp add: irrefl intro: less_imp_le strict) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
404 |
next |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
405 |
fix n :: nat show "n \<le> n" by (induct n) simp_all |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
406 |
next |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
407 |
fix n m :: nat assume "n \<le> m" and "m \<le> n" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
408 |
then show "n = m" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
409 |
by (induct n arbitrary: m) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
410 |
(simp_all add: less_eq_nat.simps(2) split: nat.splits) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
411 |
next |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
412 |
fix n m q :: nat assume "n \<le> m" and "m \<le> q" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
413 |
then show "n \<le> q" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
414 |
proof (induct n arbitrary: m q) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
415 |
case 0 show ?case by simp |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
416 |
next |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
417 |
case (Suc n) then show ?case |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
418 |
by (simp_all (no_asm_use) add: less_eq_nat.simps(2) split: nat.splits, clarify, |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
419 |
simp_all (no_asm_use) add: less_eq_nat.simps(2) split: nat.splits, clarify, |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
420 |
simp_all (no_asm_use) add: less_eq_nat.simps(2) split: nat.splits) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
421 |
qed |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
422 |
next |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
423 |
fix n m :: nat show "n \<le> m \<or> m \<le> n" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
424 |
by (induct n arbitrary: m) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
425 |
(simp_all add: less_eq_nat.simps(2) split: nat.splits) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
426 |
qed |
25510 | 427 |
|
428 |
end |
|
13449 | 429 |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
430 |
subsubsection {* Introduction properties *} |
13449 | 431 |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
432 |
lemma lessI [iff]: "n < Suc n" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
433 |
by (simp add: less_Suc_eq_le) |
13449 | 434 |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
435 |
lemma zero_less_Suc [iff]: "0 < Suc n" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
436 |
by (simp add: less_Suc_eq_le) |
13449 | 437 |
|
438 |
lemma less_trans: "i < j ==> j < k ==> i < (k::nat)" |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
439 |
by (rule order_less_trans) |
13449 | 440 |
|
441 |
subsubsection {* Elimination properties *} |
|
442 |
||
443 |
lemma less_not_sym: "n < m ==> ~ m < (n::nat)" |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
444 |
by (rule order_less_not_sym) |
13449 | 445 |
|
446 |
lemma less_asym: |
|
447 |
assumes h1: "(n::nat) < m" and h2: "~ P ==> m < n" shows P |
|
448 |
apply (rule contrapos_np) |
|
449 |
apply (rule less_not_sym) |
|
450 |
apply (rule h1) |
|
451 |
apply (erule h2) |
|
452 |
done |
|
453 |
||
454 |
lemma less_not_refl: "~ n < (n::nat)" |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
455 |
by (rule order_less_irrefl) |
13449 | 456 |
|
457 |
lemma less_irrefl [elim!]: "(n::nat) < n ==> R" |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
458 |
by (rule notE, rule less_not_refl) |
13449 | 459 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
460 |
lemma less_not_refl3: "(s::nat) < t ==> s \<noteq> t" |
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
461 |
by (rule less_imp_neq) |
13449 | 462 |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
463 |
lemma less_not_refl2: "n < m ==> m \<noteq> (n::nat)" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
464 |
by (rule not_sym) (rule less_imp_neq) |
13449 | 465 |
|
466 |
lemma less_zeroE: "(n::nat) < 0 ==> R" |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
467 |
by (rule notE) (rule not_less0) |
13449 | 468 |
|
469 |
lemma less_Suc_eq: "(m < Suc n) = (m < n | m = n)" |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
470 |
unfolding less_Suc_eq_le le_less .. |
13449 | 471 |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
472 |
lemma less_one [iff, noatp]: "(n < (1::nat)) = (n = 0)" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
473 |
by (simp add: less_Suc_eq) |
13449 | 474 |
|
475 |
lemma less_Suc0 [iff]: "(n < Suc 0) = (n = 0)" |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
476 |
by (simp add: less_Suc_eq) |
13449 | 477 |
|
478 |
lemma Suc_mono: "m < n ==> Suc m < Suc n" |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
479 |
by simp |
13449 | 480 |
|
481 |
lemma less_linear: "m < n | m = n | n < (m::nat)" |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
482 |
by (rule less_linear) |
13449 | 483 |
|
14302 | 484 |
text {* "Less than" is antisymmetric, sort of *} |
485 |
lemma less_antisym: "\<lbrakk> \<not> n < m; n < Suc m \<rbrakk> \<Longrightarrow> m = n" |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
486 |
unfolding not_less less_Suc_eq_le by (rule antisym) |
14302 | 487 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
488 |
lemma nat_neq_iff: "((m::nat) \<noteq> n) = (m < n | n < m)" |
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
489 |
by (rule linorder_neq_iff) |
13449 | 490 |
|
491 |
lemma nat_less_cases: assumes major: "(m::nat) < n ==> P n m" |
|
492 |
and eqCase: "m = n ==> P n m" and lessCase: "n<m ==> P n m" |
|
493 |
shows "P n m" |
|
494 |
apply (rule less_linear [THEN disjE]) |
|
495 |
apply (erule_tac [2] disjE) |
|
496 |
apply (erule lessCase) |
|
497 |
apply (erule sym [THEN eqCase]) |
|
498 |
apply (erule major) |
|
499 |
done |
|
500 |
||
501 |
||
502 |
subsubsection {* Inductive (?) properties *} |
|
503 |
||
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
504 |
lemma Suc_lessI: "m < n ==> Suc m \<noteq> n ==> Suc m < n" |
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
505 |
unfolding less_eq_Suc_le [of m] le_less by simp |
13449 | 506 |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
507 |
lemma lessE: |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
508 |
assumes major: "i < k" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
509 |
and p1: "k = Suc i ==> P" and p2: "!!j. i < j ==> k = Suc j ==> P" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
510 |
shows P |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
511 |
proof - |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
512 |
from major have "\<exists>j. i \<le> j \<and> k = Suc j" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
513 |
unfolding less_eq_Suc_le by (induct k) simp_all |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
514 |
then have "(\<exists>j. i < j \<and> k = Suc j) \<or> k = Suc i" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
515 |
by (clarsimp simp add: less_le) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
516 |
with p1 p2 show P by auto |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
517 |
qed |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
518 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
519 |
lemma less_SucE: assumes major: "m < Suc n" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
520 |
and less: "m < n ==> P" and eq: "m = n ==> P" shows P |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
521 |
apply (rule major [THEN lessE]) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
522 |
apply (rule eq, blast) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
523 |
apply (rule less, blast) |
13449 | 524 |
done |
525 |
||
526 |
lemma Suc_lessE: assumes major: "Suc i < k" |
|
527 |
and minor: "!!j. i < j ==> k = Suc j ==> P" shows P |
|
528 |
apply (rule major [THEN lessE]) |
|
529 |
apply (erule lessI [THEN minor]) |
|
14208 | 530 |
apply (erule Suc_lessD [THEN minor], assumption) |
13449 | 531 |
done |
532 |
||
533 |
lemma Suc_less_SucD: "Suc m < Suc n ==> m < n" |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
534 |
by simp |
13449 | 535 |
|
536 |
lemma less_trans_Suc: |
|
537 |
assumes le: "i < j" shows "j < k ==> Suc i < k" |
|
14208 | 538 |
apply (induct k, simp_all) |
13449 | 539 |
apply (insert le) |
540 |
apply (simp add: less_Suc_eq) |
|
541 |
apply (blast dest: Suc_lessD) |
|
542 |
done |
|
543 |
||
544 |
text {* Can be used with @{text less_Suc_eq} to get @{term "n = m | n < m"} *} |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
545 |
lemma not_less_eq: "\<not> m < n \<longleftrightarrow> n < Suc m" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
546 |
unfolding not_less less_Suc_eq_le .. |
13449 | 547 |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
548 |
lemma not_less_eq_eq: "\<not> m \<le> n \<longleftrightarrow> Suc n \<le> m" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
549 |
unfolding not_le Suc_le_eq .. |
21243 | 550 |
|
24995 | 551 |
text {* Properties of "less than or equal" *} |
13449 | 552 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
553 |
lemma le_imp_less_Suc: "m \<le> n ==> m < Suc n" |
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
554 |
unfolding less_Suc_eq_le . |
13449 | 555 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
556 |
lemma Suc_n_not_le_n: "~ Suc n \<le> n" |
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
557 |
unfolding not_le less_Suc_eq_le .. |
13449 | 558 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
559 |
lemma le_Suc_eq: "(m \<le> Suc n) = (m \<le> n | m = Suc n)" |
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
560 |
by (simp add: less_Suc_eq_le [symmetric] less_Suc_eq) |
13449 | 561 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
562 |
lemma le_SucE: "m \<le> Suc n ==> (m \<le> n ==> R) ==> (m = Suc n ==> R) ==> R" |
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
563 |
by (drule le_Suc_eq [THEN iffD1], iprover+) |
13449 | 564 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
565 |
lemma Suc_leI: "m < n ==> Suc(m) \<le> n" |
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
566 |
unfolding Suc_le_eq . |
13449 | 567 |
|
568 |
text {* Stronger version of @{text Suc_leD} *} |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
569 |
lemma Suc_le_lessD: "Suc m \<le> n ==> m < n" |
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
570 |
unfolding Suc_le_eq . |
13449 | 571 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
572 |
lemma less_imp_le: "m < n ==> m \<le> (n::nat)" |
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
573 |
unfolding less_eq_Suc_le by (rule Suc_leD) |
13449 | 574 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
575 |
text {* For instance, @{text "(Suc m < Suc n) = (Suc m \<le> n) = (m < n)"} *} |
13449 | 576 |
lemmas le_simps = less_imp_le less_Suc_eq_le Suc_le_eq |
577 |
||
578 |
||
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
579 |
text {* Equivalence of @{term "m \<le> n"} and @{term "m < n | m = n"} *} |
13449 | 580 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
581 |
lemma le_imp_less_or_eq: "m \<le> n ==> m < n | m = (n::nat)" |
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
582 |
unfolding le_less . |
13449 | 583 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
584 |
lemma less_or_eq_imp_le: "m < n | m = n ==> m \<le> (n::nat)" |
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
585 |
unfolding le_less . |
13449 | 586 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
587 |
lemma le_eq_less_or_eq: "(m \<le> (n::nat)) = (m < n | m=n)" |
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
588 |
by (rule le_less) |
13449 | 589 |
|
22718 | 590 |
text {* Useful with @{text blast}. *} |
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
591 |
lemma eq_imp_le: "(m::nat) = n ==> m \<le> n" |
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
592 |
by auto |
13449 | 593 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
594 |
lemma le_refl: "n \<le> (n::nat)" |
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
595 |
by simp |
13449 | 596 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
597 |
lemma le_less_trans: "[| i \<le> j; j < k |] ==> i < (k::nat)" |
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
598 |
by (rule order_le_less_trans) |
13449 | 599 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
600 |
lemma less_le_trans: "[| i < j; j \<le> k |] ==> i < (k::nat)" |
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
601 |
by (rule order_less_le_trans) |
13449 | 602 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
603 |
lemma le_trans: "[| i \<le> j; j \<le> k |] ==> i \<le> (k::nat)" |
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
604 |
by (rule order_trans) |
13449 | 605 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
606 |
lemma le_anti_sym: "[| m \<le> n; n \<le> m |] ==> m = (n::nat)" |
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
607 |
by (rule antisym) |
13449 | 608 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
609 |
lemma nat_less_le: "((m::nat) < n) = (m \<le> n & m \<noteq> n)" |
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
610 |
by (rule less_le) |
13449 | 611 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
612 |
lemma le_neq_implies_less: "(m::nat) \<le> n ==> m \<noteq> n ==> m < n" |
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
613 |
unfolding less_le .. |
13449 | 614 |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
615 |
lemma nat_le_linear: "(m::nat) \<le> n | n \<le> m" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
616 |
by (rule linear) |
14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset
|
617 |
|
22718 | 618 |
lemmas linorder_neqE_nat = linorder_neqE [where 'a = nat] |
15921 | 619 |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
620 |
lemma le_less_Suc_eq: "m \<le> n ==> (n < Suc m) = (n = m)" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
621 |
unfolding less_Suc_eq_le by auto |
13449 | 622 |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
623 |
lemma not_less_less_Suc_eq: "~ n < m ==> (n < Suc m) = (n = m)" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
624 |
unfolding not_less by (rule le_less_Suc_eq) |
13449 | 625 |
|
626 |
lemmas not_less_simps = not_less_less_Suc_eq le_less_Suc_eq |
|
627 |
||
22718 | 628 |
text {* These two rules ease the use of primitive recursion. |
14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset
|
629 |
NOTE USE OF @{text "=="} *} |
13449 | 630 |
lemma def_nat_rec_0: "(!!n. f n == nat_rec c h n) ==> f 0 = c" |
25162 | 631 |
by simp |
13449 | 632 |
|
633 |
lemma def_nat_rec_Suc: "(!!n. f n == nat_rec c h n) ==> f (Suc n) = h n (f n)" |
|
25162 | 634 |
by simp |
13449 | 635 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
636 |
lemma not0_implies_Suc: "n \<noteq> 0 ==> \<exists>m. n = Suc m" |
25162 | 637 |
by (cases n) simp_all |
638 |
||
639 |
lemma gr0_implies_Suc: "n > 0 ==> \<exists>m. n = Suc m" |
|
640 |
by (cases n) simp_all |
|
13449 | 641 |
|
22718 | 642 |
lemma gr_implies_not0: fixes n :: nat shows "m<n ==> n \<noteq> 0" |
25162 | 643 |
by (cases n) simp_all |
13449 | 644 |
|
25162 | 645 |
lemma neq0_conv[iff]: fixes n :: nat shows "(n \<noteq> 0) = (0 < n)" |
646 |
by (cases n) simp_all |
|
25140 | 647 |
|
13449 | 648 |
text {* This theorem is useful with @{text blast} *} |
649 |
lemma gr0I: "((n::nat) = 0 ==> False) ==> 0 < n" |
|
25162 | 650 |
by (rule neq0_conv[THEN iffD1], iprover) |
13449 | 651 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
652 |
lemma gr0_conv_Suc: "(0 < n) = (\<exists>m. n = Suc m)" |
25162 | 653 |
by (fast intro: not0_implies_Suc) |
13449 | 654 |
|
24286
7619080e49f0
ATP blacklisting is now in theory data, attribute noatp
paulson
parents:
24196
diff
changeset
|
655 |
lemma not_gr0 [iff,noatp]: "!!n::nat. (~ (0 < n)) = (n = 0)" |
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25111
diff
changeset
|
656 |
using neq0_conv by blast |
13449 | 657 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
658 |
lemma Suc_le_D: "(Suc n \<le> m') ==> (? m. m' = Suc m)" |
25162 | 659 |
by (induct m') simp_all |
13449 | 660 |
|
661 |
text {* Useful in certain inductive arguments *} |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
662 |
lemma less_Suc_eq_0_disj: "(m < Suc n) = (m = 0 | (\<exists>j. m = Suc j & j < n))" |
25162 | 663 |
by (cases m) simp_all |
13449 | 664 |
|
665 |
||
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
666 |
subsubsection {* @{term min} and @{term max} *} |
13449 | 667 |
|
25076 | 668 |
lemma mono_Suc: "mono Suc" |
25162 | 669 |
by (rule monoI) simp |
25076 | 670 |
|
13449 | 671 |
lemma min_0L [simp]: "min 0 n = (0::nat)" |
25162 | 672 |
by (rule min_leastL) simp |
13449 | 673 |
|
674 |
lemma min_0R [simp]: "min n 0 = (0::nat)" |
|
25162 | 675 |
by (rule min_leastR) simp |
13449 | 676 |
|
677 |
lemma min_Suc_Suc [simp]: "min (Suc m) (Suc n) = Suc (min m n)" |
|
25162 | 678 |
by (simp add: mono_Suc min_of_mono) |
13449 | 679 |
|
22191 | 680 |
lemma min_Suc1: |
681 |
"min (Suc n) m = (case m of 0 => 0 | Suc m' => Suc(min n m'))" |
|
25162 | 682 |
by (simp split: nat.split) |
22191 | 683 |
|
684 |
lemma min_Suc2: |
|
685 |
"min m (Suc n) = (case m of 0 => 0 | Suc m' => Suc(min m' n))" |
|
25162 | 686 |
by (simp split: nat.split) |
22191 | 687 |
|
13449 | 688 |
lemma max_0L [simp]: "max 0 n = (n::nat)" |
25162 | 689 |
by (rule max_leastL) simp |
13449 | 690 |
|
691 |
lemma max_0R [simp]: "max n 0 = (n::nat)" |
|
25162 | 692 |
by (rule max_leastR) simp |
13449 | 693 |
|
694 |
lemma max_Suc_Suc [simp]: "max (Suc m) (Suc n) = Suc(max m n)" |
|
25162 | 695 |
by (simp add: mono_Suc max_of_mono) |
13449 | 696 |
|
22191 | 697 |
lemma max_Suc1: |
698 |
"max (Suc n) m = (case m of 0 => Suc n | Suc m' => Suc(max n m'))" |
|
25162 | 699 |
by (simp split: nat.split) |
22191 | 700 |
|
701 |
lemma max_Suc2: |
|
702 |
"max m (Suc n) = (case m of 0 => Suc n | Suc m' => Suc(max m' n))" |
|
25162 | 703 |
by (simp split: nat.split) |
22191 | 704 |
|
13449 | 705 |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
706 |
subsubsection {* Monotonicity of Addition *} |
13449 | 707 |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
708 |
lemma Suc_pred [simp]: "n>0 ==> Suc (n - Suc 0) = n" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
709 |
by (simp add: diff_Suc split: nat.split) |
13449 | 710 |
|
14331 | 711 |
lemma nat_add_left_cancel_le [simp]: "(k + m \<le> k + n) = (m\<le>(n::nat))" |
25162 | 712 |
by (induct k) simp_all |
13449 | 713 |
|
14331 | 714 |
lemma nat_add_left_cancel_less [simp]: "(k + m < k + n) = (m<(n::nat))" |
25162 | 715 |
by (induct k) simp_all |
13449 | 716 |
|
25162 | 717 |
lemma add_gr_0 [iff]: "!!m::nat. (m + n > 0) = (m>0 | n>0)" |
718 |
by(auto dest:gr0_implies_Suc) |
|
13449 | 719 |
|
14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset
|
720 |
text {* strict, in 1st argument *} |
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset
|
721 |
lemma add_less_mono1: "i < j ==> i + k < j + (k::nat)" |
25162 | 722 |
by (induct k) simp_all |
14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset
|
723 |
|
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset
|
724 |
text {* strict, in both arguments *} |
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset
|
725 |
lemma add_less_mono: "[|i < j; k < l|] ==> i + k < j + (l::nat)" |
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset
|
726 |
apply (rule add_less_mono1 [THEN less_trans], assumption+) |
15251 | 727 |
apply (induct j, simp_all) |
14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset
|
728 |
done |
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset
|
729 |
|
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset
|
730 |
text {* Deleted @{text less_natE}; use @{text "less_imp_Suc_add RS exE"} *} |
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset
|
731 |
lemma less_imp_Suc_add: "m < n ==> (\<exists>k. n = Suc (m + k))" |
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset
|
732 |
apply (induct n) |
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset
|
733 |
apply (simp_all add: order_le_less) |
22718 | 734 |
apply (blast elim!: less_SucE |
14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset
|
735 |
intro!: add_0_right [symmetric] add_Suc_right [symmetric]) |
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset
|
736 |
done |
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset
|
737 |
|
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset
|
738 |
text {* strict, in 1st argument; proof is by induction on @{text "k > 0"} *} |
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25111
diff
changeset
|
739 |
lemma mult_less_mono2: "(i::nat) < j ==> 0<k ==> k * i < k * j" |
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25111
diff
changeset
|
740 |
apply(auto simp: gr0_conv_Suc) |
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25111
diff
changeset
|
741 |
apply (induct_tac m) |
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25111
diff
changeset
|
742 |
apply (simp_all add: add_less_mono) |
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25111
diff
changeset
|
743 |
done |
14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset
|
744 |
|
14740 | 745 |
text{*The naturals form an ordered @{text comm_semiring_1_cancel}*} |
14738 | 746 |
instance nat :: ordered_semidom |
14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset
|
747 |
proof |
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset
|
748 |
fix i j k :: nat |
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14341
diff
changeset
|
749 |
show "0 < (1::nat)" by simp |
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
750 |
show "i \<le> j ==> k + i \<le> k + j" by simp |
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
751 |
show "i < j ==> 0 < k ==> k * i < k * j" by (simp add: mult_less_mono2) |
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
752 |
qed |
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
753 |
|
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
754 |
lemma nat_mult_1: "(1::nat) * n = n" |
25162 | 755 |
by simp |
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
756 |
|
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
757 |
lemma nat_mult_1_right: "n * (1::nat) = n" |
25162 | 758 |
by simp |
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
759 |
|
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
760 |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
761 |
subsubsection {* Additional theorems about "less than" *} |
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
762 |
|
19870 | 763 |
text{*An induction rule for estabilishing binary relations*} |
22718 | 764 |
lemma less_Suc_induct: |
19870 | 765 |
assumes less: "i < j" |
766 |
and step: "!!i. P i (Suc i)" |
|
767 |
and trans: "!!i j k. P i j ==> P j k ==> P i k" |
|
768 |
shows "P i j" |
|
769 |
proof - |
|
22718 | 770 |
from less obtain k where j: "j = Suc(i+k)" by (auto dest: less_imp_Suc_add) |
771 |
have "P i (Suc (i + k))" |
|
19870 | 772 |
proof (induct k) |
22718 | 773 |
case 0 |
774 |
show ?case by (simp add: step) |
|
19870 | 775 |
next |
776 |
case (Suc k) |
|
22718 | 777 |
thus ?case by (auto intro: assms) |
19870 | 778 |
qed |
22718 | 779 |
thus "P i j" by (simp add: j) |
19870 | 780 |
qed |
781 |
||
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
782 |
text {* A [clumsy] way of lifting @{text "<"} |
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
783 |
monotonicity to @{text "\<le>"} monotonicity *} |
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
784 |
lemma less_mono_imp_le_mono: |
24438 | 785 |
"\<lbrakk> !!i j::nat. i < j \<Longrightarrow> f i < f j; i \<le> j \<rbrakk> \<Longrightarrow> f i \<le> ((f j)::nat)" |
786 |
by (simp add: order_le_less) (blast) |
|
787 |
||
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
788 |
|
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
789 |
text {* non-strict, in 1st argument *} |
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
790 |
lemma add_le_mono1: "i \<le> j ==> i + k \<le> j + (k::nat)" |
24438 | 791 |
by (rule add_right_mono) |
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
792 |
|
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
793 |
text {* non-strict, in both arguments *} |
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
794 |
lemma add_le_mono: "[| i \<le> j; k \<le> l |] ==> i + k \<le> j + (l::nat)" |
24438 | 795 |
by (rule add_mono) |
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
796 |
|
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
797 |
lemma le_add2: "n \<le> ((m + n)::nat)" |
24438 | 798 |
by (insert add_right_mono [of 0 m n], simp) |
13449 | 799 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
800 |
lemma le_add1: "n \<le> ((n + m)::nat)" |
24438 | 801 |
by (simp add: add_commute, rule le_add2) |
13449 | 802 |
|
803 |
lemma less_add_Suc1: "i < Suc (i + m)" |
|
24438 | 804 |
by (rule le_less_trans, rule le_add1, rule lessI) |
13449 | 805 |
|
806 |
lemma less_add_Suc2: "i < Suc (m + i)" |
|
24438 | 807 |
by (rule le_less_trans, rule le_add2, rule lessI) |
13449 | 808 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
809 |
lemma less_iff_Suc_add: "(m < n) = (\<exists>k. n = Suc (m + k))" |
24438 | 810 |
by (iprover intro!: less_add_Suc1 less_imp_Suc_add) |
13449 | 811 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
812 |
lemma trans_le_add1: "(i::nat) \<le> j ==> i \<le> j + m" |
24438 | 813 |
by (rule le_trans, assumption, rule le_add1) |
13449 | 814 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
815 |
lemma trans_le_add2: "(i::nat) \<le> j ==> i \<le> m + j" |
24438 | 816 |
by (rule le_trans, assumption, rule le_add2) |
13449 | 817 |
|
818 |
lemma trans_less_add1: "(i::nat) < j ==> i < j + m" |
|
24438 | 819 |
by (rule less_le_trans, assumption, rule le_add1) |
13449 | 820 |
|
821 |
lemma trans_less_add2: "(i::nat) < j ==> i < m + j" |
|
24438 | 822 |
by (rule less_le_trans, assumption, rule le_add2) |
13449 | 823 |
|
824 |
lemma add_lessD1: "i + j < (k::nat) ==> i < k" |
|
24438 | 825 |
apply (rule le_less_trans [of _ "i+j"]) |
826 |
apply (simp_all add: le_add1) |
|
827 |
done |
|
13449 | 828 |
|
829 |
lemma not_add_less1 [iff]: "~ (i + j < (i::nat))" |
|
24438 | 830 |
apply (rule notI) |
831 |
apply (erule add_lessD1 [THEN less_irrefl]) |
|
832 |
done |
|
13449 | 833 |
|
834 |
lemma not_add_less2 [iff]: "~ (j + i < (i::nat))" |
|
24438 | 835 |
by (simp add: add_commute not_add_less1) |
13449 | 836 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
837 |
lemma add_leD1: "m + k \<le> n ==> m \<le> (n::nat)" |
24438 | 838 |
apply (rule order_trans [of _ "m+k"]) |
839 |
apply (simp_all add: le_add1) |
|
840 |
done |
|
13449 | 841 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
842 |
lemma add_leD2: "m + k \<le> n ==> k \<le> (n::nat)" |
24438 | 843 |
apply (simp add: add_commute) |
844 |
apply (erule add_leD1) |
|
845 |
done |
|
13449 | 846 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
847 |
lemma add_leE: "(m::nat) + k \<le> n ==> (m \<le> n ==> k \<le> n ==> R) ==> R" |
24438 | 848 |
by (blast dest: add_leD1 add_leD2) |
13449 | 849 |
|
850 |
text {* needs @{text "!!k"} for @{text add_ac} to work *} |
|
851 |
lemma less_add_eq_less: "!!k::nat. k < l ==> m + l = k + n ==> m < n" |
|
24438 | 852 |
by (force simp del: add_Suc_right |
13449 | 853 |
simp add: less_iff_Suc_add add_Suc_right [symmetric] add_ac) |
854 |
||
855 |
||
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
856 |
subsubsection {* More results about difference *} |
13449 | 857 |
|
858 |
lemma diff_self_eq_0 [simp]: "(m::nat) - m = 0" |
|
24438 | 859 |
by (induct m) simp_all |
13449 | 860 |
|
861 |
text {* Addition is the inverse of subtraction: |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
862 |
if @{term "n \<le> m"} then @{term "n + (m - n) = m"}. *} |
13449 | 863 |
lemma add_diff_inverse: "~ m < n ==> n + (m - n) = (m::nat)" |
24438 | 864 |
by (induct m n rule: diff_induct) simp_all |
13449 | 865 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
866 |
lemma le_add_diff_inverse [simp]: "n \<le> m ==> n + (m - n) = (m::nat)" |
24438 | 867 |
by (simp add: add_diff_inverse linorder_not_less) |
13449 | 868 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
869 |
lemma le_add_diff_inverse2 [simp]: "n \<le> m ==> (m - n) + n = (m::nat)" |
24438 | 870 |
by (simp add: le_add_diff_inverse add_commute) |
13449 | 871 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
872 |
lemma Suc_diff_le: "n \<le> m ==> Suc m - n = Suc (m - n)" |
24438 | 873 |
by (induct m n rule: diff_induct) simp_all |
13449 | 874 |
|
875 |
lemma diff_less_Suc: "m - n < Suc m" |
|
24438 | 876 |
apply (induct m n rule: diff_induct) |
877 |
apply (erule_tac [3] less_SucE) |
|
878 |
apply (simp_all add: less_Suc_eq) |
|
879 |
done |
|
13449 | 880 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
881 |
lemma diff_le_self [simp]: "m - n \<le> (m::nat)" |
24438 | 882 |
by (induct m n rule: diff_induct) (simp_all add: le_SucI) |
13449 | 883 |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
884 |
lemma le_iff_add: "(m::nat) \<le> n = (\<exists>k. n = m + k)" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
885 |
by (auto simp: le_add1 dest!: le_add_diff_inverse sym [of _ n]) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
886 |
|
13449 | 887 |
lemma less_imp_diff_less: "(j::nat) < k ==> j - n < k" |
24438 | 888 |
by (rule le_less_trans, rule diff_le_self) |
13449 | 889 |
|
890 |
lemma diff_Suc_less [simp]: "0<n ==> n - Suc i < n" |
|
24438 | 891 |
by (cases n) (auto simp add: le_simps) |
13449 | 892 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
893 |
lemma diff_add_assoc: "k \<le> (j::nat) ==> (i + j) - k = i + (j - k)" |
24438 | 894 |
by (induct j k rule: diff_induct) simp_all |
13449 | 895 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
896 |
lemma diff_add_assoc2: "k \<le> (j::nat) ==> (j + i) - k = (j - k) + i" |
24438 | 897 |
by (simp add: add_commute diff_add_assoc) |
13449 | 898 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
899 |
lemma le_imp_diff_is_add: "i \<le> (j::nat) ==> (j - i = k) = (j = k + i)" |
24438 | 900 |
by (auto simp add: diff_add_inverse2) |
13449 | 901 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
902 |
lemma diff_is_0_eq [simp]: "((m::nat) - n = 0) = (m \<le> n)" |
24438 | 903 |
by (induct m n rule: diff_induct) simp_all |
13449 | 904 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
905 |
lemma diff_is_0_eq' [simp]: "m \<le> n ==> (m::nat) - n = 0" |
24438 | 906 |
by (rule iffD2, rule diff_is_0_eq) |
13449 | 907 |
|
908 |
lemma zero_less_diff [simp]: "(0 < n - (m::nat)) = (m < n)" |
|
24438 | 909 |
by (induct m n rule: diff_induct) simp_all |
13449 | 910 |
|
22718 | 911 |
lemma less_imp_add_positive: |
912 |
assumes "i < j" |
|
913 |
shows "\<exists>k::nat. 0 < k & i + k = j" |
|
914 |
proof |
|
915 |
from assms show "0 < j - i & i + (j - i) = j" |
|
23476 | 916 |
by (simp add: order_less_imp_le) |
22718 | 917 |
qed |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
7702
diff
changeset
|
918 |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
919 |
text {* a nice rewrite for bounded subtraction *} |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
920 |
lemma nat_minus_add_max: |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
921 |
fixes n m :: nat |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
922 |
shows "n - m + m = max n m" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
923 |
by (simp add: max_def not_le order_less_imp_le) |
13449 | 924 |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
925 |
lemma nat_diff_split: |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
926 |
"P(a - b::nat) = ((a<b --> P 0) & (ALL d. a = b + d --> P d))" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
927 |
-- {* elimination of @{text -} on @{text nat} *} |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
928 |
by (cases "a < b") |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
929 |
(auto simp add: diff_is_0_eq [THEN iffD2] diff_add_inverse |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
930 |
not_less le_less dest!: sym [of a] sym [of b] add_eq_self_zero) |
13449 | 931 |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
932 |
lemma nat_diff_split_asm: |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
933 |
"P(a - b::nat) = (~ (a < b & ~ P 0 | (EX d. a = b + d & ~ P d)))" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
934 |
-- {* elimination of @{text -} on @{text nat} in assumptions *} |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
935 |
by (auto split: nat_diff_split) |
13449 | 936 |
|
937 |
||
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
938 |
subsubsection {* Monotonicity of Multiplication *} |
13449 | 939 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
940 |
lemma mult_le_mono1: "i \<le> (j::nat) ==> i * k \<le> j * k" |
24438 | 941 |
by (simp add: mult_right_mono) |
13449 | 942 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
943 |
lemma mult_le_mono2: "i \<le> (j::nat) ==> k * i \<le> k * j" |
24438 | 944 |
by (simp add: mult_left_mono) |
13449 | 945 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
946 |
text {* @{text "\<le>"} monotonicity, BOTH arguments *} |
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
947 |
lemma mult_le_mono: "i \<le> (j::nat) ==> k \<le> l ==> i * k \<le> j * l" |
24438 | 948 |
by (simp add: mult_mono) |
13449 | 949 |
|
950 |
lemma mult_less_mono1: "(i::nat) < j ==> 0 < k ==> i * k < j * k" |
|
24438 | 951 |
by (simp add: mult_strict_right_mono) |
13449 | 952 |
|
14266 | 953 |
text{*Differs from the standard @{text zero_less_mult_iff} in that |
954 |
there are no negative numbers.*} |
|
955 |
lemma nat_0_less_mult_iff [simp]: "(0 < (m::nat) * n) = (0 < m & 0 < n)" |
|
13449 | 956 |
apply (induct m) |
22718 | 957 |
apply simp |
958 |
apply (case_tac n) |
|
959 |
apply simp_all |
|
13449 | 960 |
done |
961 |
||
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
962 |
lemma one_le_mult_iff [simp]: "(Suc 0 \<le> m * n) = (1 \<le> m & 1 \<le> n)" |
13449 | 963 |
apply (induct m) |
22718 | 964 |
apply simp |
965 |
apply (case_tac n) |
|
966 |
apply simp_all |
|
13449 | 967 |
done |
968 |
||
14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset
|
969 |
lemma mult_less_cancel2 [simp]: "((m::nat) * k < n * k) = (0 < k & m < n)" |
13449 | 970 |
apply (safe intro!: mult_less_mono1) |
14208 | 971 |
apply (case_tac k, auto) |
13449 | 972 |
apply (simp del: le_0_eq add: linorder_not_le [symmetric]) |
973 |
apply (blast intro: mult_le_mono1) |
|
974 |
done |
|
975 |
||
976 |
lemma mult_less_cancel1 [simp]: "(k * (m::nat) < k * n) = (0 < k & m < n)" |
|
24438 | 977 |
by (simp add: mult_commute [of k]) |
13449 | 978 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
979 |
lemma mult_le_cancel1 [simp]: "(k * (m::nat) \<le> k * n) = (0 < k --> m \<le> n)" |
24438 | 980 |
by (simp add: linorder_not_less [symmetric], auto) |
13449 | 981 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
982 |
lemma mult_le_cancel2 [simp]: "((m::nat) * k \<le> n * k) = (0 < k --> m \<le> n)" |
24438 | 983 |
by (simp add: linorder_not_less [symmetric], auto) |
13449 | 984 |
|
985 |
lemma Suc_mult_less_cancel1: "(Suc k * m < Suc k * n) = (m < n)" |
|
24438 | 986 |
by (subst mult_less_cancel1) simp |
13449 | 987 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
988 |
lemma Suc_mult_le_cancel1: "(Suc k * m \<le> Suc k * n) = (m \<le> n)" |
24438 | 989 |
by (subst mult_le_cancel1) simp |
13449 | 990 |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
991 |
lemma le_square: "m \<le> m * (m::nat)" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
992 |
by (cases m) (auto intro: le_add1) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
993 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
994 |
lemma le_cube: "(m::nat) \<le> m * (m * m)" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
995 |
by (cases m) (auto intro: le_add1) |
13449 | 996 |
|
997 |
text {* Lemma for @{text gcd} *} |
|
998 |
lemma mult_eq_self_implies_10: "(m::nat) = m * n ==> n = 1 | m = 0" |
|
999 |
apply (drule sym) |
|
1000 |
apply (rule disjCI) |
|
1001 |
apply (rule nat_less_cases, erule_tac [2] _) |
|
25157 | 1002 |
apply (drule_tac [2] mult_less_mono2) |
25162 | 1003 |
apply (auto) |
13449 | 1004 |
done |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
7702
diff
changeset
|
1005 |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1006 |
text {* the lattice order on @{typ nat} *} |
24995 | 1007 |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1008 |
instantiation nat :: distrib_lattice |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1009 |
begin |
24995 | 1010 |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1011 |
definition |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1012 |
"(inf \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat) = min" |
24995 | 1013 |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1014 |
definition |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1015 |
"(sup \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat) = max" |
24995 | 1016 |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1017 |
instance by intro_classes |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1018 |
(auto simp add: inf_nat_def sup_nat_def max_def not_le min_def |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1019 |
intro: order_less_imp_le antisym elim!: order_trans order_less_trans) |
24995 | 1020 |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1021 |
end |
24995 | 1022 |
|
1023 |
||
25193 | 1024 |
subsection {* Embedding of the Naturals into any |
1025 |
@{text semiring_1}: @{term of_nat} *} |
|
24196 | 1026 |
|
1027 |
context semiring_1 |
|
1028 |
begin |
|
1029 |
||
25559 | 1030 |
primrec |
1031 |
of_nat :: "nat \<Rightarrow> 'a" |
|
1032 |
where |
|
1033 |
of_nat_0: "of_nat 0 = 0" |
|
1034 |
| of_nat_Suc: "of_nat (Suc m) = 1 + of_nat m" |
|
25193 | 1035 |
|
1036 |
lemma of_nat_1 [simp]: "of_nat 1 = 1" |
|
1037 |
by simp |
|
1038 |
||
1039 |
lemma of_nat_add [simp]: "of_nat (m + n) = of_nat m + of_nat n" |
|
1040 |
by (induct m) (simp_all add: add_ac) |
|
1041 |
||
1042 |
lemma of_nat_mult: "of_nat (m * n) = of_nat m * of_nat n" |
|
1043 |
by (induct m) (simp_all add: add_ac left_distrib) |
|
1044 |
||
25928 | 1045 |
definition |
1046 |
of_nat_aux :: "nat \<Rightarrow> 'a \<Rightarrow> 'a" |
|
1047 |
where |
|
1048 |
[code func del]: "of_nat_aux n i = of_nat n + i" |
|
1049 |
||
1050 |
lemma of_nat_aux_code [code]: |
|
1051 |
"of_nat_aux 0 i = i" |
|
1052 |
"of_nat_aux (Suc n) i = of_nat_aux n (i + 1)" -- {* tail recursive *} |
|
1053 |
by (simp_all add: of_nat_aux_def add_ac) |
|
1054 |
||
1055 |
lemma of_nat_code [code]: |
|
1056 |
"of_nat n = of_nat_aux n 0" |
|
1057 |
by (simp add: of_nat_aux_def) |
|
1058 |
||
24196 | 1059 |
end |
1060 |
||
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1061 |
text{*Class for unital semirings with characteristic zero. |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1062 |
Includes non-ordered rings like the complex numbers.*} |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1063 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1064 |
class semiring_char_0 = semiring_1 + |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1065 |
assumes of_nat_eq_iff [simp]: "of_nat m = of_nat n \<longleftrightarrow> m = n" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1066 |
begin |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1067 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1068 |
text{*Special cases where either operand is zero*} |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1069 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1070 |
lemma of_nat_0_eq_iff [simp, noatp]: "0 = of_nat n \<longleftrightarrow> 0 = n" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1071 |
by (rule of_nat_eq_iff [of 0, simplified]) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1072 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1073 |
lemma of_nat_eq_0_iff [simp, noatp]: "of_nat m = 0 \<longleftrightarrow> m = 0" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1074 |
by (rule of_nat_eq_iff [of _ 0, simplified]) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1075 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1076 |
lemma inj_of_nat: "inj of_nat" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1077 |
by (simp add: inj_on_def) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1078 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1079 |
end |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1080 |
|
25193 | 1081 |
context ordered_semidom |
1082 |
begin |
|
1083 |
||
1084 |
lemma zero_le_imp_of_nat: "0 \<le> of_nat m" |
|
1085 |
apply (induct m, simp_all) |
|
1086 |
apply (erule order_trans) |
|
1087 |
apply (rule ord_le_eq_trans [OF _ add_commute]) |
|
1088 |
apply (rule less_add_one [THEN less_imp_le]) |
|
1089 |
done |
|
1090 |
||
1091 |
lemma less_imp_of_nat_less: "m < n \<Longrightarrow> of_nat m < of_nat n" |
|
1092 |
apply (induct m n rule: diff_induct, simp_all) |
|
1093 |
apply (insert add_less_le_mono [OF zero_less_one zero_le_imp_of_nat], force) |
|
1094 |
done |
|
1095 |
||
1096 |
lemma of_nat_less_imp_less: "of_nat m < of_nat n \<Longrightarrow> m < n" |
|
1097 |
apply (induct m n rule: diff_induct, simp_all) |
|
1098 |
apply (insert zero_le_imp_of_nat) |
|
1099 |
apply (force simp add: not_less [symmetric]) |
|
1100 |
done |
|
1101 |
||
1102 |
lemma of_nat_less_iff [simp]: "of_nat m < of_nat n \<longleftrightarrow> m < n" |
|
1103 |
by (blast intro: of_nat_less_imp_less less_imp_of_nat_less) |
|
1104 |
||
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1105 |
lemma of_nat_le_iff [simp]: "of_nat m \<le> of_nat n \<longleftrightarrow> m \<le> n" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1106 |
by (simp add: not_less [symmetric] linorder_not_less [symmetric]) |
25193 | 1107 |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1108 |
text{*Every @{text ordered_semidom} has characteristic zero.*} |
25193 | 1109 |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1110 |
subclass semiring_char_0 |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1111 |
by unfold_locales (simp add: eq_iff order_eq_iff) |
25193 | 1112 |
|
1113 |
text{*Special cases where either operand is zero*} |
|
1114 |
||
1115 |
lemma of_nat_0_le_iff [simp]: "0 \<le> of_nat n" |
|
1116 |
by (rule of_nat_le_iff [of 0, simplified]) |
|
1117 |
||
1118 |
lemma of_nat_le_0_iff [simp, noatp]: "of_nat m \<le> 0 \<longleftrightarrow> m = 0" |
|
1119 |
by (rule of_nat_le_iff [of _ 0, simplified]) |
|
1120 |
||
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1121 |
lemma of_nat_0_less_iff [simp]: "0 < of_nat n \<longleftrightarrow> 0 < n" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1122 |
by (rule of_nat_less_iff [of 0, simplified]) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1123 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1124 |
lemma of_nat_less_0_iff [simp]: "\<not> of_nat m < 0" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1125 |
by (rule of_nat_less_iff [of _ 0, simplified]) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1126 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1127 |
end |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1128 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1129 |
context ring_1 |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1130 |
begin |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1131 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1132 |
lemma of_nat_diff: "n \<le> m \<Longrightarrow> of_nat (m - n) = of_nat m - of_nat n" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1133 |
by (simp add: compare_rls of_nat_add [symmetric]) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1134 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1135 |
end |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1136 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1137 |
context ordered_idom |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1138 |
begin |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1139 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1140 |
lemma abs_of_nat [simp]: "\<bar>of_nat n\<bar> = of_nat n" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1141 |
unfolding abs_if by auto |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1142 |
|
25193 | 1143 |
end |
1144 |
||
1145 |
lemma of_nat_id [simp]: "of_nat n = n" |
|
1146 |
by (induct n) auto |
|
1147 |
||
1148 |
lemma of_nat_eq_id [simp]: "of_nat = id" |
|
1149 |
by (auto simp add: expand_fun_eq) |
|
1150 |
||
1151 |
||
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1152 |
subsection {*The Set of Natural Numbers*} |
25193 | 1153 |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1154 |
context semiring_1 |
25193 | 1155 |
begin |
1156 |
||
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1157 |
definition |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1158 |
Nats :: "'a set" where |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1159 |
"Nats = range of_nat" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1160 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1161 |
notation (xsymbols) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1162 |
Nats ("\<nat>") |
25193 | 1163 |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1164 |
lemma of_nat_in_Nats [simp]: "of_nat n \<in> \<nat>" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1165 |
by (simp add: Nats_def) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1166 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1167 |
lemma Nats_0 [simp]: "0 \<in> \<nat>" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1168 |
apply (simp add: Nats_def) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1169 |
apply (rule range_eqI) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1170 |
apply (rule of_nat_0 [symmetric]) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1171 |
done |
25193 | 1172 |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1173 |
lemma Nats_1 [simp]: "1 \<in> \<nat>" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1174 |
apply (simp add: Nats_def) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1175 |
apply (rule range_eqI) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1176 |
apply (rule of_nat_1 [symmetric]) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1177 |
done |
25193 | 1178 |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1179 |
lemma Nats_add [simp]: "a \<in> \<nat> \<Longrightarrow> b \<in> \<nat> \<Longrightarrow> a + b \<in> \<nat>" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1180 |
apply (auto simp add: Nats_def) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1181 |
apply (rule range_eqI) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1182 |
apply (rule of_nat_add [symmetric]) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1183 |
done |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1184 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1185 |
lemma Nats_mult [simp]: "a \<in> \<nat> \<Longrightarrow> b \<in> \<nat> \<Longrightarrow> a * b \<in> \<nat>" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1186 |
apply (auto simp add: Nats_def) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1187 |
apply (rule range_eqI) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1188 |
apply (rule of_nat_mult [symmetric]) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1189 |
done |
25193 | 1190 |
|
1191 |
end |
|
1192 |
||
1193 |
||
21243 | 1194 |
subsection {* Further Arithmetic Facts Concerning the Natural Numbers *} |
1195 |
||
22845 | 1196 |
lemma subst_equals: |
1197 |
assumes 1: "t = s" and 2: "u = t" |
|
1198 |
shows "u = s" |
|
1199 |
using 2 1 by (rule trans) |
|
1200 |
||
21243 | 1201 |
use "arith_data.ML" |
26101 | 1202 |
declaration {* K ArithData.setup *} |
24091 | 1203 |
|
1204 |
use "Tools/lin_arith.ML" |
|
1205 |
declaration {* K LinArith.setup *} |
|
1206 |
||
21243 | 1207 |
lemmas [arith_split] = nat_diff_split split_min split_max |
1208 |
||
1209 |
text{*Subtraction laws, mostly by Clemens Ballarin*} |
|
1210 |
||
1211 |
lemma diff_less_mono: "[| a < (b::nat); c \<le> a |] ==> a-c < b-c" |
|
24438 | 1212 |
by arith |
21243 | 1213 |
|
1214 |
lemma less_diff_conv: "(i < j-k) = (i+k < (j::nat))" |
|
24438 | 1215 |
by arith |
21243 | 1216 |
|
1217 |
lemma le_diff_conv: "(j-k \<le> (i::nat)) = (j \<le> i+k)" |
|
24438 | 1218 |
by arith |
21243 | 1219 |
|
1220 |
lemma le_diff_conv2: "k \<le> j ==> (i \<le> j-k) = (i+k \<le> (j::nat))" |
|
24438 | 1221 |
by arith |
21243 | 1222 |
|
1223 |
lemma diff_diff_cancel [simp]: "i \<le> (n::nat) ==> n - (n - i) = i" |
|
24438 | 1224 |
by arith |
21243 | 1225 |
|
1226 |
lemma le_add_diff: "k \<le> (n::nat) ==> m \<le> n + m - k" |
|
24438 | 1227 |
by arith |
21243 | 1228 |
|
1229 |
(*Replaces the previous diff_less and le_diff_less, which had the stronger |
|
1230 |
second premise n\<le>m*) |
|
1231 |
lemma diff_less[simp]: "!!m::nat. [| 0<n; 0<m |] ==> m - n < m" |
|
24438 | 1232 |
by arith |
21243 | 1233 |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1234 |
text {* Simplification of relational expressions involving subtraction *} |
21243 | 1235 |
|
1236 |
lemma diff_diff_eq: "[| k \<le> m; k \<le> (n::nat) |] ==> ((m-k) - (n-k)) = (m-n)" |
|
24438 | 1237 |
by (simp split add: nat_diff_split) |
21243 | 1238 |
|
1239 |
lemma eq_diff_iff: "[| k \<le> m; k \<le> (n::nat) |] ==> (m-k = n-k) = (m=n)" |
|
24438 | 1240 |
by (auto split add: nat_diff_split) |
21243 | 1241 |
|
1242 |
lemma less_diff_iff: "[| k \<le> m; k \<le> (n::nat) |] ==> (m-k < n-k) = (m<n)" |
|
24438 | 1243 |
by (auto split add: nat_diff_split) |
21243 | 1244 |
|
1245 |
lemma le_diff_iff: "[| k \<le> m; k \<le> (n::nat) |] ==> (m-k \<le> n-k) = (m\<le>n)" |
|
24438 | 1246 |
by (auto split add: nat_diff_split) |
21243 | 1247 |
|
1248 |
text{*(Anti)Monotonicity of subtraction -- by Stephan Merz*} |
|
1249 |
||
1250 |
(* Monotonicity of subtraction in first argument *) |
|
1251 |
lemma diff_le_mono: "m \<le> (n::nat) ==> (m-l) \<le> (n-l)" |
|
24438 | 1252 |
by (simp split add: nat_diff_split) |
21243 | 1253 |
|
1254 |
lemma diff_le_mono2: "m \<le> (n::nat) ==> (l-n) \<le> (l-m)" |
|
24438 | 1255 |
by (simp split add: nat_diff_split) |
21243 | 1256 |
|
1257 |
lemma diff_less_mono2: "[| m < (n::nat); m<l |] ==> (l-n) < (l-m)" |
|
24438 | 1258 |
by (simp split add: nat_diff_split) |
21243 | 1259 |
|
1260 |
lemma diffs0_imp_equal: "!!m::nat. [| m-n = 0; n-m = 0 |] ==> m=n" |
|
24438 | 1261 |
by (simp split add: nat_diff_split) |
21243 | 1262 |
|
26143
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26101
diff
changeset
|
1263 |
lemma min_diff: "min (m - (i::nat)) (n - i) = min m n - i" |
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26101
diff
changeset
|
1264 |
unfolding min_def by auto |
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26101
diff
changeset
|
1265 |
|
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26101
diff
changeset
|
1266 |
lemma inj_on_diff_nat: |
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26101
diff
changeset
|
1267 |
assumes k_le_n: "\<forall>n \<in> N. k \<le> (n::nat)" |
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26101
diff
changeset
|
1268 |
shows "inj_on (\<lambda>n. n - k) N" |
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26101
diff
changeset
|
1269 |
proof (rule inj_onI) |
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26101
diff
changeset
|
1270 |
fix x y |
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26101
diff
changeset
|
1271 |
assume a: "x \<in> N" "y \<in> N" "x - k = y - k" |
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26101
diff
changeset
|
1272 |
with k_le_n have "x - k + k = y - k + k" by auto |
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26101
diff
changeset
|
1273 |
with a k_le_n show "x = y" by auto |
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26101
diff
changeset
|
1274 |
qed |
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26101
diff
changeset
|
1275 |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1276 |
text{*Rewriting to pull differences out*} |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1277 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1278 |
lemma diff_diff_right [simp]: "k\<le>j --> i - (j - k) = i + (k::nat) - j" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1279 |
by arith |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1280 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1281 |
lemma diff_Suc_diff_eq1 [simp]: "k \<le> j ==> m - Suc (j - k) = m + k - Suc j" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1282 |
by arith |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1283 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1284 |
lemma diff_Suc_diff_eq2 [simp]: "k \<le> j ==> Suc (j - k) - m = Suc j - (k + m)" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1285 |
by arith |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1286 |
|
21243 | 1287 |
text{*Lemmas for ex/Factorization*} |
1288 |
||
1289 |
lemma one_less_mult: "[| Suc 0 < n; Suc 0 < m |] ==> Suc 0 < m*n" |
|
24438 | 1290 |
by (cases m) auto |
21243 | 1291 |
|
1292 |
lemma n_less_m_mult_n: "[| Suc 0 < n; Suc 0 < m |] ==> n<m*n" |
|
24438 | 1293 |
by (cases m) auto |
21243 | 1294 |
|
1295 |
lemma n_less_n_mult_m: "[| Suc 0 < n; Suc 0 < m |] ==> n<n*m" |
|
24438 | 1296 |
by (cases m) auto |
21243 | 1297 |
|
23001
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1298 |
text {* Specialized induction principles that work "backwards": *} |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1299 |
|
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1300 |
lemma inc_induct[consumes 1, case_names base step]: |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1301 |
assumes less: "i <= j" |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1302 |
assumes base: "P j" |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1303 |
assumes step: "!!i. [| i < j; P (Suc i) |] ==> P i" |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1304 |
shows "P i" |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1305 |
using less |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1306 |
proof (induct d=="j - i" arbitrary: i) |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1307 |
case (0 i) |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1308 |
hence "i = j" by simp |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1309 |
with base show ?case by simp |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1310 |
next |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1311 |
case (Suc d i) |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1312 |
hence "i < j" "P (Suc i)" |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1313 |
by simp_all |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1314 |
thus "P i" by (rule step) |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1315 |
qed |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1316 |
|
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1317 |
lemma strict_inc_induct[consumes 1, case_names base step]: |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1318 |
assumes less: "i < j" |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1319 |
assumes base: "!!i. j = Suc i ==> P i" |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1320 |
assumes step: "!!i. [| i < j; P (Suc i) |] ==> P i" |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1321 |
shows "P i" |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1322 |
using less |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1323 |
proof (induct d=="j - i - 1" arbitrary: i) |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1324 |
case (0 i) |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1325 |
with `i < j` have "j = Suc i" by simp |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1326 |
with base show ?case by simp |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1327 |
next |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1328 |
case (Suc d i) |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1329 |
hence "i < j" "P (Suc i)" |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1330 |
by simp_all |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1331 |
thus "P i" by (rule step) |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1332 |
qed |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1333 |
|
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1334 |
lemma zero_induct_lemma: "P k ==> (!!n. P (Suc n) ==> P n) ==> P (k - i)" |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1335 |
using inc_induct[of "k - i" k P, simplified] by blast |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1336 |
|
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1337 |
lemma zero_induct: "P k ==> (!!n. P (Suc n) ==> P n) ==> P 0" |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1338 |
using inc_induct[of 0 k P] by blast |
21243 | 1339 |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1340 |
lemma nat_not_singleton: "(\<forall>x. x = (0::nat)) = False" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1341 |
by auto |
21243 | 1342 |
|
1343 |
(*The others are |
|
1344 |
i - j - k = i - (j + k), |
|
1345 |
k \<le> j ==> j - k + i = j + i - k, |
|
1346 |
k \<le> j ==> i + (j - k) = i + j - k *) |
|
1347 |
lemmas add_diff_assoc = diff_add_assoc [symmetric] |
|
1348 |
lemmas add_diff_assoc2 = diff_add_assoc2[symmetric] |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1349 |
declare diff_diff_left [simp] add_diff_assoc [simp] add_diff_assoc2[simp] |
21243 | 1350 |
|
1351 |
text{*At present we prove no analogue of @{text not_less_Least} or @{text |
|
1352 |
Least_Suc}, since there appears to be no need.*} |
|
1353 |
||
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1354 |
subsection {* size of a datatype value *} |
25193 | 1355 |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1356 |
class size = type + |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1357 |
fixes size :: "'a \<Rightarrow> nat" -- {* see further theory @{text Wellfounded_Recursion} *} |
23852 | 1358 |
|
25193 | 1359 |
end |