author  nipkow 
Thu, 14 May 2020 23:44:01 +0200  
changeset 71841  f4626b1f1b96 
parent 71836  c095d3143047 
child 71851  34ecb540a079 
permissions  rwrr 
923  1 
(* Title: HOL/Nat.thy 
63588  2 
Author: Tobias Nipkow 
3 
Author: Lawrence C Paulson 

4 
Author: Markus Wenzel 

923  5 
*) 
6 

60758  7 
section \<open>Natural numbers\<close> 
13449  8 

15131  9 
theory Nat 
64447  10 
imports Inductive Typedef Fun Rings 
15131  11 
begin 
13449  12 

61799  13 
subsection \<open>Type \<open>ind\<close>\<close> 
13449  14 

15 
typedecl ind 

16 

63110  17 
axiomatization Zero_Rep :: ind and Suc_Rep :: "ind \<Rightarrow> ind" 
18 
\<comment> \<open>The axiom of infinity in 2 parts:\<close> 

63588  19 
where Suc_Rep_inject: "Suc_Rep x = Suc_Rep y \<Longrightarrow> x = y" 
20 
and Suc_Rep_not_Zero_Rep: "Suc_Rep x \<noteq> Zero_Rep" 

21 

19573  22 

60758  23 
subsection \<open>Type nat\<close> 
24 

25 
text \<open>Type definition\<close> 

13449  26 

63588  27 
inductive Nat :: "ind \<Rightarrow> bool" 
28 
where 

29 
Zero_RepI: "Nat Zero_Rep" 

30 
 Suc_RepI: "Nat i \<Longrightarrow> Nat (Suc_Rep i)" 

13449  31 

49834  32 
typedef nat = "{n. Nat n}" 
45696  33 
morphisms Rep_Nat Abs_Nat 
44278
1220ecb81e8f
observe distinction between sets and predicates more properly
haftmann
parents:
43595
diff
changeset

34 
using Nat.Zero_RepI by auto 
1220ecb81e8f
observe distinction between sets and predicates more properly
haftmann
parents:
43595
diff
changeset

35 

63588  36 
lemma Nat_Rep_Nat: "Nat (Rep_Nat n)" 
44278
1220ecb81e8f
observe distinction between sets and predicates more properly
haftmann
parents:
43595
diff
changeset

37 
using Rep_Nat by simp 
13449  38 

63588  39 
lemma Nat_Abs_Nat_inverse: "Nat n \<Longrightarrow> Rep_Nat (Abs_Nat n) = n" 
44278
1220ecb81e8f
observe distinction between sets and predicates more properly
haftmann
parents:
43595
diff
changeset

40 
using Abs_Nat_inverse by simp 
1220ecb81e8f
observe distinction between sets and predicates more properly
haftmann
parents:
43595
diff
changeset

41 

63588  42 
lemma Nat_Abs_Nat_inject: "Nat n \<Longrightarrow> Nat m \<Longrightarrow> Abs_Nat n = Abs_Nat m \<longleftrightarrow> n = m" 
44278
1220ecb81e8f
observe distinction between sets and predicates more properly
haftmann
parents:
43595
diff
changeset

43 
using Abs_Nat_inject by simp 
13449  44 

25510  45 
instantiation nat :: zero 
46 
begin 

47 

63588  48 
definition Zero_nat_def: "0 = Abs_Nat Zero_Rep" 
25510  49 

50 
instance .. 

51 

52 
end 

24995  53 

63588  54 
definition Suc :: "nat \<Rightarrow> nat" 
55 
where "Suc n = Abs_Nat (Suc_Rep (Rep_Nat n))" 

44278
1220ecb81e8f
observe distinction between sets and predicates more properly
haftmann
parents:
43595
diff
changeset

56 

27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
26748
diff
changeset

57 
lemma Suc_not_Zero: "Suc m \<noteq> 0" 
63588  58 
by (simp add: Zero_nat_def Suc_def Suc_RepI Zero_RepI 
59 
Nat_Abs_Nat_inject Suc_Rep_not_Zero_Rep Nat_Rep_Nat) 

13449  60 

27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
26748
diff
changeset

61 
lemma Zero_not_Suc: "0 \<noteq> Suc m" 
63588  62 
by (rule not_sym) (rule Suc_not_Zero) 
13449  63 

34208
a7acd6c68d9b
more regular axiom of infinity, with no (indirect) reference to overloaded constants
krauss
parents:
33657
diff
changeset

64 
lemma Suc_Rep_inject': "Suc_Rep x = Suc_Rep y \<longleftrightarrow> x = y" 
a7acd6c68d9b
more regular axiom of infinity, with no (indirect) reference to overloaded constants
krauss
parents:
33657
diff
changeset

65 
by (rule iffI, rule Suc_Rep_inject) simp_all 
a7acd6c68d9b
more regular axiom of infinity, with no (indirect) reference to overloaded constants
krauss
parents:
33657
diff
changeset

66 

55417
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
55415
diff
changeset

67 
lemma nat_induct0: 
71585  68 
assumes "P 0" and "\<And>n. P n \<Longrightarrow> P (Suc n)" 
55417
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
55415
diff
changeset

69 
shows "P n" 
71585  70 
proof  
71 
have "P (Abs_Nat (Rep_Nat n))" 

72 
using assms unfolding Zero_nat_def Suc_def 

73 
by (iprover intro: Nat_Rep_Nat [THEN Nat.induct] elim: Nat_Abs_Nat_inverse [THEN subst]) 

74 
then show ?thesis 

75 
by (simp add: Rep_Nat_inverse) 

76 
qed 

63588  77 

78 
free_constructors case_nat for "0 :: nat"  Suc pred 

79 
where "pred (0 :: nat) = (0 :: nat)" 

58189
9d714be4f028
added 'plugins' option to control which hooks are enabled
blanchet
parents:
57983
diff
changeset

80 
apply atomize_elim 
9d714be4f028
added 'plugins' option to control which hooks are enabled
blanchet
parents:
57983
diff
changeset

81 
apply (rename_tac n, induct_tac n rule: nat_induct0, auto) 
63588  82 
apply (simp add: Suc_def Nat_Abs_Nat_inject Nat_Rep_Nat Suc_RepI Suc_Rep_inject' Rep_Nat_inject) 
58189
9d714be4f028
added 'plugins' option to control which hooks are enabled
blanchet
parents:
57983
diff
changeset

83 
apply (simp only: Suc_not_Zero) 
9d714be4f028
added 'plugins' option to control which hooks are enabled
blanchet
parents:
57983
diff
changeset

84 
done 
55417
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
55415
diff
changeset

85 

61799  86 
\<comment> \<open>Avoid name clashes by prefixing the output of \<open>old_rep_datatype\<close> with \<open>old\<close>.\<close> 
60758  87 
setup \<open>Sign.mandatory_path "old"\<close> 
55417
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
55415
diff
changeset

88 

61076  89 
old_rep_datatype "0 :: nat" Suc 
71585  90 
by (erule nat_induct0) auto 
55417
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
55415
diff
changeset

91 

60758  92 
setup \<open>Sign.parent_path\<close> 
93 

61799  94 
\<comment> \<open>But erase the prefix for properties that are not generated by \<open>free_constructors\<close>.\<close> 
60758  95 
setup \<open>Sign.mandatory_path "nat"\<close> 
55417
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
55415
diff
changeset

96 

63588  97 
declare old.nat.inject[iff del] 
98 
and old.nat.distinct(1)[simp del, induct_simp del] 

55417
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
55415
diff
changeset

99 

01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
55415
diff
changeset

100 
lemmas induct = old.nat.induct 
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
55415
diff
changeset

101 
lemmas inducts = old.nat.inducts 
55642
63beb38e9258
adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
blanchet
parents:
55575
diff
changeset

102 
lemmas rec = old.nat.rec 
63beb38e9258
adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
blanchet
parents:
55575
diff
changeset

103 
lemmas simps = nat.inject nat.distinct nat.case nat.rec 
55417
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
55415
diff
changeset

104 

60758  105 
setup \<open>Sign.parent_path\<close> 
55417
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
55415
diff
changeset

106 

63110  107 
abbreviation rec_nat :: "'a \<Rightarrow> (nat \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a" 
108 
where "rec_nat \<equiv> old.rec_nat" 

55417
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
55415
diff
changeset

109 

55424
9ab4129a76a3
remove hidden fact about hidden constant from code generator setup
blanchet
parents:
55423
diff
changeset

110 
declare nat.sel[code del] 
9ab4129a76a3
remove hidden fact about hidden constant from code generator setup
blanchet
parents:
55423
diff
changeset

111 

61799  112 
hide_const (open) Nat.pred \<comment> \<open>hide everything related to the selector\<close> 
55417
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
55415
diff
changeset

113 
hide_fact 
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
55415
diff
changeset

114 
nat.case_eq_if 
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
55415
diff
changeset

115 
nat.collapse 
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
55415
diff
changeset

116 
nat.expand 
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
55415
diff
changeset

117 
nat.sel 
57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57952
diff
changeset

118 
nat.exhaust_sel 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57952
diff
changeset

119 
nat.split_sel 
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57952
diff
changeset

120 
nat.split_sel_asm 
55417
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
55415
diff
changeset

121 

01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
55415
diff
changeset

122 
lemma nat_exhaust [case_names 0 Suc, cases type: nat]: 
63588  123 
"(y = 0 \<Longrightarrow> P) \<Longrightarrow> (\<And>nat. y = Suc nat \<Longrightarrow> P) \<Longrightarrow> P" 
61799  124 
\<comment> \<open>for backward compatibility  names of variables differ\<close> 
63588  125 
by (rule old.nat.exhaust) 
13449  126 

27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
26748
diff
changeset

127 
lemma nat_induct [case_names 0 Suc, induct type: nat]: 
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
26748
diff
changeset

128 
fixes n 
55417
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
55415
diff
changeset

129 
assumes "P 0" and "\<And>n. P n \<Longrightarrow> P (Suc n)" 
27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
26748
diff
changeset

130 
shows "P n" 
63588  131 
\<comment> \<open>for backward compatibility  names of variables differ\<close> 
132 
using assms by (rule nat.induct) 

13449  133 

55417
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
55415
diff
changeset

134 
hide_fact 
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
55415
diff
changeset

135 
nat_exhaust 
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
55415
diff
changeset

136 
nat_induct0 
24995  137 

60758  138 
ML \<open> 
58389  139 
val nat_basic_lfp_sugar = 
140 
let 

69593  141 
val ctr_sugar = the (Ctr_Sugar.ctr_sugar_of_global \<^theory> \<^type_name>\<open>nat\<close>); 
142 
val recx = Logic.varify_types_global \<^term>\<open>rec_nat\<close>; 

58389  143 
val C = body_type (fastype_of recx); 
144 
in 

145 
{T = HOLogic.natT, fp_res_index = 0, C = C, fun_arg_Tsss = [[], [[HOLogic.natT, C]]], 

146 
ctr_sugar = ctr_sugar, recx = recx, rec_thms = @{thms nat.rec}} 

147 
end; 

60758  148 
\<close> 
149 

150 
setup \<open> 

58389  151 
let 
69593  152 
fun basic_lfp_sugars_of _ [\<^typ>\<open>nat\<close>] _ _ ctxt = 
62326
3cf7a067599c
allow predicator instead of map function in 'primrec'
blanchet
parents:
62217
diff
changeset

153 
([], [0], [nat_basic_lfp_sugar], [], [], [], TrueI (*dummy*), [], false, ctxt) 
58389  154 
 basic_lfp_sugars_of bs arg_Ts callers callssss ctxt = 
155 
BNF_LFP_Rec_Sugar.default_basic_lfp_sugars_of bs arg_Ts callers callssss ctxt; 

156 
in 

157 
BNF_LFP_Rec_Sugar.register_lfp_rec_extension 

66290  158 
{nested_simps = [], special_endgame_tac = K (K (K (K no_tac))), is_new_datatype = K (K true), 
159 
basic_lfp_sugars_of = basic_lfp_sugars_of, rewrite_nested_rec_call = NONE} 

58389  160 
end 
60758  161 
\<close> 
162 

163 
text \<open>Injectiveness and distinctness lemmas\<close> 

24995  164 

66936  165 
lemma inj_Suc [simp]: 
166 
"inj_on Suc N" 

27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
26748
diff
changeset

167 
by (simp add: inj_on_def) 
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
26748
diff
changeset

168 

66936  169 
lemma bij_betw_Suc [simp]: 
170 
"bij_betw Suc M N \<longleftrightarrow> Suc ` M = N" 

171 
by (simp add: bij_betw_def) 

172 

26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

173 
lemma Suc_neq_Zero: "Suc m = 0 \<Longrightarrow> R" 
63588  174 
by (rule notE) (rule Suc_not_Zero) 
24995  175 

26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

176 
lemma Zero_neq_Suc: "0 = Suc m \<Longrightarrow> R" 
63588  177 
by (rule Suc_neq_Zero) (erule sym) 
24995  178 

26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

179 
lemma Suc_inject: "Suc x = Suc y \<Longrightarrow> x = y" 
63588  180 
by (rule inj_Suc [THEN injD]) 
24995  181 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

182 
lemma n_not_Suc_n: "n \<noteq> Suc n" 
63588  183 
by (induct n) simp_all 
13449  184 

26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

185 
lemma Suc_n_not_n: "Suc n \<noteq> n" 
63588  186 
by (rule not_sym) (rule n_not_Suc_n) 
187 

69593  188 
text \<open>A special form of induction for reasoning about \<^term>\<open>m < n\<close> and \<^term>\<open>m  n\<close>.\<close> 
63110  189 
lemma diff_induct: 
190 
assumes "\<And>x. P x 0" 

191 
and "\<And>y. P 0 (Suc y)" 

192 
and "\<And>x y. P x y \<Longrightarrow> P (Suc x) (Suc y)" 

193 
shows "P m n" 

63588  194 
proof (induct n arbitrary: m) 
195 
case 0 

196 
show ?case by (rule assms(1)) 

197 
next 

198 
case (Suc n) 

199 
show ?case 

200 
proof (induct m) 

201 
case 0 

202 
show ?case by (rule assms(2)) 

203 
next 

204 
case (Suc m) 

205 
from \<open>P m n\<close> show ?case by (rule assms(3)) 

206 
qed 

207 
qed 

13449  208 

24995  209 

60758  210 
subsection \<open>Arithmetic operators\<close> 
24995  211 

49388  212 
instantiation nat :: comm_monoid_diff 
25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25563
diff
changeset

213 
begin 
24995  214 

63588  215 
primrec plus_nat 
216 
where 

217 
add_0: "0 + n = (n::nat)" 

218 
 add_Suc: "Suc m + n = Suc (m + n)" 

219 

220 
lemma add_0_right [simp]: "m + 0 = m" 

221 
for m :: nat 

26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

222 
by (induct m) simp_all 
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_Suc_right [simp]: "m + Suc n = Suc (m + n)" 
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

225 
by (induct m) simp_all 
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

226 

28514  227 
declare add_0 [code] 
228 

26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

229 
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

230 
by simp 
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

231 

63588  232 
primrec minus_nat 
233 
where 

234 
diff_0 [code]: "m  0 = (m::nat)" 

235 
 diff_Suc: "m  Suc n = (case m  n of 0 \<Rightarrow> 0  Suc k \<Rightarrow> k)" 

24995  236 

28514  237 
declare diff_Suc [simp del] 
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

238 

63588  239 
lemma diff_0_eq_0 [simp, code]: "0  n = 0" 
240 
for n :: nat 

26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

241 
by (induct n) (simp_all add: diff_Suc) 
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

242 

f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

243 
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

244 
by (induct n) (simp_all add: diff_Suc) 
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

245 

63110  246 
instance 
247 
proof 

26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

248 
fix n m q :: nat 
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

249 
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

250 
show "n + m = m + n" by (induct n) simp_all 
59815
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59582
diff
changeset

251 
show "m + n  m = n" by (induct m) simp_all 
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59582
diff
changeset

252 
show "n  m  q = n  (m + q)" by (induct q) (simp_all add: diff_Suc) 
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

253 
show "0 + n = n" by simp 
49388  254 
show "0  n = 0" by simp 
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

255 
qed 
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

256 

f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

257 
end 
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

258 

36176
3fe7e97ccca8
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact'  frees some popular keywords;
wenzelm
parents:
35828
diff
changeset

259 
hide_fact (open) add_0 add_0_right diff_0 
35047
1b2bae06c796
hide fact Nat.add_0_right; make add_0_right from Groups priority
haftmann
parents:
35028
diff
changeset

260 

26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

261 
instantiation nat :: comm_semiring_1_cancel 
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

262 
begin 
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

263 

63588  264 
definition One_nat_def [simp]: "1 = Suc 0" 
265 

266 
primrec times_nat 

267 
where 

268 
mult_0: "0 * n = (0::nat)" 

269 
 mult_Suc: "Suc m * n = n + (m * n)" 

270 

271 
lemma mult_0_right [simp]: "m * 0 = 0" 

272 
for m :: nat 

26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

273 
by (induct m) simp_all 
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

274 

f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

275 
lemma mult_Suc_right [simp]: "m * Suc n = m + (m * n)" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57492
diff
changeset

276 
by (induct m) (simp_all add: add.left_commute) 
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

277 

63588  278 
lemma add_mult_distrib: "(m + n) * k = (m * k) + (n * k)" 
279 
for m n k :: nat 

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57492
diff
changeset

280 
by (induct m) (simp_all add: add.assoc) 
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

281 

63110  282 
instance 
283 
proof 

284 
fix k n m q :: nat 

63588  285 
show "0 \<noteq> (1::nat)" 
286 
by simp 

287 
show "1 * n = n" 

288 
by simp 

289 
show "n * m = m * n" 

290 
by (induct n) simp_all 

291 
show "(n * m) * q = n * (m * q)" 

292 
by (induct n) (simp_all add: add_mult_distrib) 

293 
show "(n + m) * q = n * q + m * q" 

294 
by (rule add_mult_distrib) 

63110  295 
show "k * (m  n) = (k * m)  (k * n)" 
60562
24af00b010cf
Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
paulson <lp15@cam.ac.uk>
parents:
60427
diff
changeset

296 
by (induct m n rule: diff_induct) simp_all 
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

297 
qed 
25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25563
diff
changeset

298 

c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25563
diff
changeset

299 
end 
24995  300 

60562
24af00b010cf
Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
paulson <lp15@cam.ac.uk>
parents:
60427
diff
changeset

301 

60758  302 
subsubsection \<open>Addition\<close> 
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

303 

61799  304 
text \<open>Reasoning about \<open>m + 0 = 0\<close>, etc.\<close> 
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

305 

63588  306 
lemma add_is_0 [iff]: "m + n = 0 \<longleftrightarrow> m = 0 \<and> n = 0" 
307 
for m n :: nat 

26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

308 
by (cases m) simp_all 
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

309 

67091  310 
lemma add_is_1: "m + n = Suc 0 \<longleftrightarrow> m = Suc 0 \<and> n = 0 \<or> m = 0 \<and> n = Suc 0" 
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

311 
by (cases m) simp_all 
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

312 

67091  313 
lemma one_is_add: "Suc 0 = m + n \<longleftrightarrow> m = Suc 0 \<and> n = 0 \<or> m = 0 \<and> n = Suc 0" 
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

314 
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

315 

63588  316 
lemma add_eq_self_zero: "m + n = m \<Longrightarrow> n = 0" 
317 
for m n :: nat 

26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

318 
by (induct m) simp_all 
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

319 

66936  320 
lemma plus_1_eq_Suc: 
321 
"plus 1 = Suc" 

322 
by (simp add: fun_eq_iff) 

26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

323 

47208  324 
lemma Suc_eq_plus1: "Suc n = n + 1" 
63588  325 
by simp 
47208  326 

327 
lemma Suc_eq_plus1_left: "Suc n = 1 + n" 

63588  328 
by simp 
47208  329 

26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

330 

60758  331 
subsubsection \<open>Difference\<close> 
26072
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_diff_diff [simp]: "(Suc m  n)  Suc k = m  n  k" 
62365  334 
by (simp add: diff_diff_add) 
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

335 

30093  336 
lemma diff_Suc_1 [simp]: "Suc n  1 = n" 
63588  337 
by simp 
338 

30093  339 

60758  340 
subsubsection \<open>Multiplication\<close> 
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

341 

63110  342 
lemma mult_is_0 [simp]: "m * n = 0 \<longleftrightarrow> m = 0 \<or> n = 0" for m n :: nat 
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

343 
by (induct m) auto 
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

344 

63110  345 
lemma mult_eq_1_iff [simp]: "m * n = Suc 0 \<longleftrightarrow> m = Suc 0 \<and> n = Suc 0" 
63588  346 
proof (induct m) 
347 
case 0 

348 
then show ?case by simp 

349 
next 

350 
case (Suc m) 

351 
then show ?case by (induct n) auto 

352 
qed 

26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

353 

63110  354 
lemma one_eq_mult_iff [simp]: "Suc 0 = m * n \<longleftrightarrow> m = Suc 0 \<and> n = Suc 0" 
71585  355 
by (simp add: eq_commute flip: mult_eq_1_iff) 
356 

357 
lemma nat_mult_eq_1_iff [simp]: "m * n = 1 \<longleftrightarrow> m = 1 \<and> n = 1" 

358 
and nat_1_eq_mult_iff [simp]: "1 = m * n \<longleftrightarrow> m = 1 \<and> n = 1" for m n :: nat 

359 
by auto 

30079
293b896b9c25
make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules
huffman
parents:
30056
diff
changeset

360 

63588  361 
lemma mult_cancel1 [simp]: "k * m = k * n \<longleftrightarrow> m = n \<or> k = 0" 
362 
for k m n :: nat 

26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

363 
proof  
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

364 
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

365 
proof (induct n arbitrary: m) 
63110  366 
case 0 
367 
then show "m = 0" by simp 

26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

368 
next 
63110  369 
case (Suc n) 
370 
then show "m = Suc n" 

371 
by (cases m) (simp_all add: eq_commute [of 0]) 

26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

372 
qed 
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

373 
then show ?thesis by auto 
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

374 
qed 
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

375 

63588  376 
lemma mult_cancel2 [simp]: "m * k = n * k \<longleftrightarrow> m = n \<or> k = 0" 
377 
for k m n :: nat 

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57492
diff
changeset

378 
by (simp add: mult.commute) 
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

379 

63110  380 
lemma Suc_mult_cancel1: "Suc k * m = Suc k * n \<longleftrightarrow> m = n" 
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

381 
by (subst mult_cancel1) simp 
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

382 

24995  383 

69593  384 
subsection \<open>Orders on \<^typ>\<open>nat\<close>\<close> 
60758  385 

386 
subsubsection \<open>Operation definition\<close> 

24995  387 

26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

388 
instantiation nat :: linorder 
25510  389 
begin 
390 

63588  391 
primrec less_eq_nat 
392 
where 

393 
"(0::nat) \<le> n \<longleftrightarrow> True" 

394 
 "Suc m \<le> n \<longleftrightarrow> (case n of 0 \<Rightarrow> False  Suc n \<Rightarrow> m \<le> n)" 

26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

395 

28514  396 
declare less_eq_nat.simps [simp del] 
63110  397 

63588  398 
lemma le0 [iff]: "0 \<le> n" for 
399 
n :: nat 

63110  400 
by (simp add: less_eq_nat.simps) 
401 

63588  402 
lemma [code]: "0 \<le> n \<longleftrightarrow> True" 
403 
for n :: nat 

63110  404 
by simp 
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

405 

63588  406 
definition less_nat 
407 
where less_eq_Suc_le: "n < m \<longleftrightarrow> Suc n \<le> m" 

26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

408 

f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

409 
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

410 
by (simp add: less_eq_nat.simps(2)) 
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

411 

f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

412 
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

413 
unfolding less_eq_Suc_le .. 
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

414 

63588  415 
lemma le_0_eq [iff]: "n \<le> 0 \<longleftrightarrow> n = 0" 
416 
for n :: nat 

26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

417 
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

418 

63588  419 
lemma not_less0 [iff]: "\<not> n < 0" 
420 
for n :: nat 

26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

421 
by (simp add: less_eq_Suc_le) 
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

422 

63588  423 
lemma less_nat_zero_code [code]: "n < 0 \<longleftrightarrow> False" 
424 
for n :: nat 

26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

425 
by simp 
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

426 

f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

427 
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

428 
by (simp add: less_eq_Suc_le) 
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

429 

f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

430 
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

431 
by (simp add: less_eq_Suc_le) 
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

432 

56194  433 
lemma Suc_less_eq2: "Suc n < m \<longleftrightarrow> (\<exists>m'. m = Suc m' \<and> n < m')" 
434 
by (cases m) auto 

435 

26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

436 
lemma le_SucI: "m \<le> n \<Longrightarrow> m \<le> Suc n" 
63110  437 
by (induct m arbitrary: n) (simp_all add: less_eq_nat.simps(2) split: nat.splits) 
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

438 

f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

439 
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

440 
by (cases n) (auto intro: le_SucI) 
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

441 

f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

442 
lemma less_SucI: "m < n \<Longrightarrow> m < Suc n" 
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

443 
by (simp add: less_eq_Suc_le) (erule Suc_leD) 
24995  444 

26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

445 
lemma Suc_lessD: "Suc m < n \<Longrightarrow> m < n" 
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

446 
by (simp add: less_eq_Suc_le) (erule Suc_leD) 
25510  447 

26315
cb3badaa192e
removed redundant less_trans, less_linear, le_imp_less_or_eq, le_less_trans, less_le_trans (cf. Orderings.thy);
wenzelm
parents:
26300
diff
changeset

448 
instance 
cb3badaa192e
removed redundant less_trans, less_linear, le_imp_less_or_eq, le_less_trans, less_le_trans (cf. Orderings.thy);
wenzelm
parents:
26300
diff
changeset

449 
proof 
63110  450 
fix n m q :: nat 
60562
24af00b010cf
Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
paulson <lp15@cam.ac.uk>
parents:
60427
diff
changeset

451 
show "n < m \<longleftrightarrow> n \<le> m \<and> \<not> m \<le> n" 
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

452 
proof (induct n arbitrary: m) 
63110  453 
case 0 
63588  454 
then show ?case 
455 
by (cases m) (simp_all add: less_eq_Suc_le) 

26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

456 
next 
63110  457 
case (Suc n) 
63588  458 
then show ?case 
459 
by (cases m) (simp_all add: less_eq_Suc_le) 

26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

460 
qed 
63588  461 
show "n \<le> n" 
462 
by (induct n) simp_all 

63110  463 
then show "n = m" if "n \<le> m" and "m \<le> n" 
464 
using that by (induct n arbitrary: m) 

26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

465 
(simp_all add: less_eq_nat.simps(2) split: nat.splits) 
63110  466 
show "n \<le> q" if "n \<le> m" and "m \<le> q" 
467 
using that 

26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

468 
proof (induct n arbitrary: m q) 
63110  469 
case 0 
470 
show ?case by simp 

26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

471 
next 
63110  472 
case (Suc n) 
473 
then show ?case 

26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

474 
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

475 
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

476 
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

477 
qed 
63110  478 
show "n \<le> m \<or> m \<le> n" 
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

479 
by (induct n arbitrary: m) 
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

480 
(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

481 
qed 
25510  482 

483 
end 

13449  484 

52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
52435
diff
changeset

485 
instantiation nat :: order_bot 
29652  486 
begin 
487 

63588  488 
definition bot_nat :: nat 
489 
where "bot_nat = 0" 

490 

491 
instance 

492 
by standard (simp add: bot_nat_def) 

29652  493 

494 
end 

495 

51329
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51263
diff
changeset

496 
instance nat :: no_top 
61169  497 
by standard (auto intro: less_Suc_eq_le [THEN iffD2]) 
52289  498 

51329
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51263
diff
changeset

499 

60758  500 
subsubsection \<open>Introduction properties\<close> 
13449  501 

26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

502 
lemma lessI [iff]: "n < Suc n" 
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

503 
by (simp add: less_Suc_eq_le) 
13449  504 

26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

505 
lemma zero_less_Suc [iff]: "0 < Suc n" 
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

506 
by (simp add: less_Suc_eq_le) 
13449  507 

508 

60758  509 
subsubsection \<open>Elimination properties\<close> 
13449  510 

63588  511 
lemma less_not_refl: "\<not> n < n" 
512 
for n :: nat 

26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

513 
by (rule order_less_irrefl) 
13449  514 

63588  515 
lemma less_not_refl2: "n < m \<Longrightarrow> m \<noteq> n" 
516 
for m n :: nat 

60562
24af00b010cf
Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
paulson <lp15@cam.ac.uk>
parents:
60427
diff
changeset

517 
by (rule not_sym) (rule less_imp_neq) 
13449  518 

63588  519 
lemma less_not_refl3: "s < t \<Longrightarrow> s \<noteq> t" 
520 
for s t :: nat 

26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

521 
by (rule less_imp_neq) 
13449  522 

63588  523 
lemma less_irrefl_nat: "n < n \<Longrightarrow> R" 
524 
for n :: nat 

26335
961bbcc9d85b
removed redundant Nat.less_not_sym, Nat.less_asym;
wenzelm
parents:
26315
diff
changeset

525 
by (rule notE, rule less_not_refl) 
13449  526 

63588  527 
lemma less_zeroE: "n < 0 \<Longrightarrow> R" 
528 
for n :: nat 

26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

529 
by (rule notE) (rule not_less0) 
13449  530 

63110  531 
lemma less_Suc_eq: "m < Suc n \<longleftrightarrow> m < n \<or> m = n" 
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

532 
unfolding less_Suc_eq_le le_less .. 
13449  533 

30079
293b896b9c25
make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules
huffman
parents:
30056
diff
changeset

534 
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

535 
by (simp add: less_Suc_eq) 
13449  536 

63588  537 
lemma less_one [iff]: "n < 1 \<longleftrightarrow> n = 0" 
538 
for n :: nat 

30079
293b896b9c25
make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules
huffman
parents:
30056
diff
changeset

539 
unfolding One_nat_def by (rule less_Suc0) 
13449  540 

63110  541 
lemma Suc_mono: "m < n \<Longrightarrow> Suc m < Suc n" 
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

542 
by simp 
13449  543 

63588  544 
text \<open>"Less than" is antisymmetric, sort of.\<close> 
545 
lemma less_antisym: "\<not> n < m \<Longrightarrow> n < Suc m \<Longrightarrow> m = n" 

26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

546 
unfolding not_less less_Suc_eq_le by (rule antisym) 
14302  547 

63588  548 
lemma nat_neq_iff: "m \<noteq> n \<longleftrightarrow> m < n \<or> n < m" 
549 
for m n :: nat 

26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

550 
by (rule linorder_neq_iff) 
13449  551 

552 

60758  553 
subsubsection \<open>Inductive (?) properties\<close> 
13449  554 

63110  555 
lemma Suc_lessI: "m < n \<Longrightarrow> Suc m \<noteq> n \<Longrightarrow> Suc m < n" 
60562
24af00b010cf
Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
paulson <lp15@cam.ac.uk>
parents:
60427
diff
changeset

556 
unfolding less_eq_Suc_le [of m] le_less by simp 
13449  557 

26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

558 
lemma lessE: 
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

559 
assumes major: "i < k" 
63110  560 
and 1: "k = Suc i \<Longrightarrow> P" 
561 
and 2: "\<And>j. i < j \<Longrightarrow> k = Suc j \<Longrightarrow> P" 

26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

562 
shows P 
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

563 
proof  
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

564 
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

565 
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

566 
then have "(\<exists>j. i < j \<and> k = Suc j) \<or> k = Suc i" 
63110  567 
by (auto simp add: less_le) 
568 
with 1 2 show P by auto 

26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

569 
qed 
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

570 

63110  571 
lemma less_SucE: 
572 
assumes major: "m < Suc n" 

573 
and less: "m < n \<Longrightarrow> P" 

574 
and eq: "m = n \<Longrightarrow> P" 

575 
shows P 

71585  576 
proof (rule major [THEN lessE]) 
577 
show "Suc n = Suc m \<Longrightarrow> P" 

578 
using eq by blast 

579 
show "\<And>j. \<lbrakk>m < j; Suc n = Suc j\<rbrakk> \<Longrightarrow> P" 

580 
by (blast intro: less) 

581 
qed 

13449  582 

63110  583 
lemma Suc_lessE: 
584 
assumes major: "Suc i < k" 

585 
and minor: "\<And>j. i < j \<Longrightarrow> k = Suc j \<Longrightarrow> P" 

586 
shows P 

71585  587 
proof (rule major [THEN lessE]) 
588 
show "k = Suc (Suc i) \<Longrightarrow> P" 

589 
using lessI minor by iprover 

590 
show "\<And>j. \<lbrakk>Suc i < j; k = Suc j\<rbrakk> \<Longrightarrow> P" 

591 
using Suc_lessD minor by iprover 

592 
qed 

13449  593 

63110  594 
lemma Suc_less_SucD: "Suc m < Suc n \<Longrightarrow> m < n" 
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

595 
by simp 
13449  596 

597 
lemma less_trans_Suc: 

63110  598 
assumes le: "i < j" 
599 
shows "j < k \<Longrightarrow> Suc i < k" 

63588  600 
proof (induct k) 
601 
case 0 

602 
then show ?case by simp 

603 
next 

604 
case (Suc k) 

605 
with le show ?case 

606 
by simp (auto simp add: less_Suc_eq dest: Suc_lessD) 

607 
qed 

608 

69593  609 
text \<open>Can be used with \<open>less_Suc_eq\<close> to get \<^prop>\<open>n = m \<or> n < m\<close>.\<close> 
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

610 
lemma not_less_eq: "\<not> m < n \<longleftrightarrow> n < Suc m" 
63588  611 
by (simp only: not_less less_Suc_eq_le) 
13449  612 

26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

613 
lemma not_less_eq_eq: "\<not> m \<le> n \<longleftrightarrow> Suc n \<le> m" 
63588  614 
by (simp only: not_le Suc_le_eq) 
615 

616 
text \<open>Properties of "less than or equal".\<close> 

13449  617 

63110  618 
lemma le_imp_less_Suc: "m \<le> n \<Longrightarrow> m < Suc n" 
63588  619 
by (simp only: less_Suc_eq_le) 
13449  620 

63110  621 
lemma Suc_n_not_le_n: "\<not> Suc n \<le> n" 
63588  622 
by (simp add: not_le less_Suc_eq_le) 
623 

624 
lemma le_Suc_eq: "m \<le> Suc n \<longleftrightarrow> m \<le> n \<or> m = Suc n" 

26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

625 
by (simp add: less_Suc_eq_le [symmetric] less_Suc_eq) 
13449  626 

63110  627 
lemma le_SucE: "m \<le> Suc n \<Longrightarrow> (m \<le> n \<Longrightarrow> R) \<Longrightarrow> (m = Suc n \<Longrightarrow> R) \<Longrightarrow> R" 
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

628 
by (drule le_Suc_eq [THEN iffD1], iprover+) 
13449  629 

63588  630 
lemma Suc_leI: "m < n \<Longrightarrow> Suc m \<le> n" 
631 
by (simp only: Suc_le_eq) 

632 

633 
text \<open>Stronger version of \<open>Suc_leD\<close>.\<close> 

63110  634 
lemma Suc_le_lessD: "Suc m \<le> n \<Longrightarrow> m < n" 
63588  635 
by (simp only: Suc_le_eq) 
13449  636 

63110  637 
lemma less_imp_le_nat: "m < n \<Longrightarrow> m \<le> n" for m n :: nat 
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

638 
unfolding less_eq_Suc_le by (rule Suc_leD) 
13449  639 

61799  640 
text \<open>For instance, \<open>(Suc m < Suc n) = (Suc m \<le> n) = (m < n)\<close>\<close> 
26315
cb3badaa192e
removed redundant less_trans, less_linear, le_imp_less_or_eq, le_less_trans, less_le_trans (cf. Orderings.thy);
wenzelm
parents:
26300
diff
changeset

641 
lemmas le_simps = less_imp_le_nat less_Suc_eq_le Suc_le_eq 
13449  642 

643 

63110  644 
text \<open>Equivalence of \<open>m \<le> n\<close> and \<open>m < n \<or> m = n\<close>\<close> 
645 

63588  646 
lemma less_or_eq_imp_le: "m < n \<or> m = n \<Longrightarrow> m \<le> n" 
647 
for m n :: nat 

26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

648 
unfolding le_less . 
13449  649 

63588  650 
lemma le_eq_less_or_eq: "m \<le> n \<longleftrightarrow> m < n \<or> m = n" 
651 
for m n :: nat 

26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

652 
by (rule le_less) 
13449  653 

61799  654 
text \<open>Useful with \<open>blast\<close>.\<close> 
63588  655 
lemma eq_imp_le: "m = n \<Longrightarrow> m \<le> n" 
656 
for m n :: nat 

26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

657 
by auto 
13449  658 

63588  659 
lemma le_refl: "n \<le> n" 
660 
for n :: nat 

26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

661 
by simp 
13449  662 

63588  663 
lemma le_trans: "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> i \<le> k" 
664 
for i j k :: nat 

26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

665 
by (rule order_trans) 
13449  666 

63588  667 
lemma le_antisym: "m \<le> n \<Longrightarrow> n \<le> m \<Longrightarrow> m = n" 
668 
for m n :: nat 

26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

669 
by (rule antisym) 
13449  670 

63588  671 
lemma nat_less_le: "m < n \<longleftrightarrow> m \<le> n \<and> m \<noteq> n" 
672 
for m n :: nat 

26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

673 
by (rule less_le) 
13449  674 

63588  675 
lemma le_neq_implies_less: "m \<le> n \<Longrightarrow> m \<noteq> n \<Longrightarrow> m < n" 
676 
for m n :: nat 

26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

677 
unfolding less_le .. 
13449  678 

67091  679 
lemma nat_le_linear: "m \<le> n \<or> n \<le> m" 
63588  680 
for m n :: nat 
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

681 
by (rule linear) 
14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset

682 

22718  683 
lemmas linorder_neqE_nat = linorder_neqE [where 'a = nat] 
15921  684 

63110  685 
lemma le_less_Suc_eq: "m \<le> n \<Longrightarrow> n < Suc m \<longleftrightarrow> n = m" 
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

686 
unfolding less_Suc_eq_le by auto 
13449  687 

63110  688 
lemma not_less_less_Suc_eq: "\<not> n < m \<Longrightarrow> n < Suc m \<longleftrightarrow> n = m" 
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

689 
unfolding not_less by (rule le_less_Suc_eq) 
13449  690 

691 
lemmas not_less_simps = not_less_less_Suc_eq le_less_Suc_eq 

692 

63110  693 
lemma not0_implies_Suc: "n \<noteq> 0 \<Longrightarrow> \<exists>m. n = Suc m" 
694 
by (cases n) simp_all 

695 

696 
lemma gr0_implies_Suc: "n > 0 \<Longrightarrow> \<exists>m. n = Suc m" 

697 
by (cases n) simp_all 

698 

63588  699 
lemma gr_implies_not0: "m < n \<Longrightarrow> n \<noteq> 0" 
700 
for m n :: nat 

63110  701 
by (cases n) simp_all 
702 

63588  703 
lemma neq0_conv[iff]: "n \<noteq> 0 \<longleftrightarrow> 0 < n" 
704 
for n :: nat 

63110  705 
by (cases n) simp_all 
25140  706 

61799  707 
text \<open>This theorem is useful with \<open>blast\<close>\<close> 
63588  708 
lemma gr0I: "(n = 0 \<Longrightarrow> False) \<Longrightarrow> 0 < n" 
709 
for n :: nat 

710 
by (rule neq0_conv[THEN iffD1]) iprover 

63110  711 

712 
lemma gr0_conv_Suc: "0 < n \<longleftrightarrow> (\<exists>m. n = Suc m)" 

713 
by (fast intro: not0_implies_Suc) 

714 

63588  715 
lemma not_gr0 [iff]: "\<not> 0 < n \<longleftrightarrow> n = 0" 
716 
for n :: nat 

63110  717 
using neq0_conv by blast 
718 

719 
lemma Suc_le_D: "Suc n \<le> m' \<Longrightarrow> \<exists>m. m' = Suc m" 

720 
by (induct m') simp_all 

13449  721 

60758  722 
text \<open>Useful in certain inductive arguments\<close> 
63110  723 
lemma less_Suc_eq_0_disj: "m < Suc n \<longleftrightarrow> m = 0 \<or> (\<exists>j. m = Suc j \<and> j < n)" 
724 
by (cases m) simp_all 

13449  725 

64447  726 
lemma All_less_Suc: "(\<forall>i < Suc n. P i) = (P n \<and> (\<forall>i < n. P i))" 
71404
f2b783abfbe7
A few lemmas connected with orderings
paulson <lp15@cam.ac.uk>
parents:
70490
diff
changeset

727 
by (auto simp: less_Suc_eq) 
13449  728 

66386  729 
lemma All_less_Suc2: "(\<forall>i < Suc n. P i) = (P 0 \<and> (\<forall>i < n. P(Suc i)))" 
71404
f2b783abfbe7
A few lemmas connected with orderings
paulson <lp15@cam.ac.uk>
parents:
70490
diff
changeset

730 
by (auto simp: less_Suc_eq_0_disj) 
66386  731 

732 
lemma Ex_less_Suc: "(\<exists>i < Suc n. P i) = (P n \<or> (\<exists>i < n. P i))" 

71404
f2b783abfbe7
A few lemmas connected with orderings
paulson <lp15@cam.ac.uk>
parents:
70490
diff
changeset

733 
by (auto simp: less_Suc_eq) 
66386  734 

735 
lemma Ex_less_Suc2: "(\<exists>i < Suc n. P i) = (P 0 \<or> (\<exists>i < n. P(Suc i)))" 

71404
f2b783abfbe7
A few lemmas connected with orderings
paulson <lp15@cam.ac.uk>
parents:
70490
diff
changeset

736 
by (auto simp: less_Suc_eq_0_disj) 
f2b783abfbe7
A few lemmas connected with orderings
paulson <lp15@cam.ac.uk>
parents:
70490
diff
changeset

737 

f2b783abfbe7
A few lemmas connected with orderings
paulson <lp15@cam.ac.uk>
parents:
70490
diff
changeset

738 
text \<open>@{term mono} (nonstrict) doesn't imply increasing, as the function could be constant\<close> 
f2b783abfbe7
A few lemmas connected with orderings
paulson <lp15@cam.ac.uk>
parents:
70490
diff
changeset

739 
lemma strict_mono_imp_increasing: 
f2b783abfbe7
A few lemmas connected with orderings
paulson <lp15@cam.ac.uk>
parents:
70490
diff
changeset

740 
fixes n::nat 
f2b783abfbe7
A few lemmas connected with orderings
paulson <lp15@cam.ac.uk>
parents:
70490
diff
changeset

741 
assumes "strict_mono f" shows "f n \<ge> n" 
f2b783abfbe7
A few lemmas connected with orderings
paulson <lp15@cam.ac.uk>
parents:
70490
diff
changeset

742 
proof (induction n) 
f2b783abfbe7
A few lemmas connected with orderings
paulson <lp15@cam.ac.uk>
parents:
70490
diff
changeset

743 
case 0 
f2b783abfbe7
A few lemmas connected with orderings
paulson <lp15@cam.ac.uk>
parents:
70490
diff
changeset

744 
then show ?case 
f2b783abfbe7
A few lemmas connected with orderings
paulson <lp15@cam.ac.uk>
parents:
70490
diff
changeset

745 
by auto 
f2b783abfbe7
A few lemmas connected with orderings
paulson <lp15@cam.ac.uk>
parents:
70490
diff
changeset

746 
next 
f2b783abfbe7
A few lemmas connected with orderings
paulson <lp15@cam.ac.uk>
parents:
70490
diff
changeset

747 
case (Suc n) 
f2b783abfbe7
A few lemmas connected with orderings
paulson <lp15@cam.ac.uk>
parents:
70490
diff
changeset

748 
then show ?case 
f2b783abfbe7
A few lemmas connected with orderings
paulson <lp15@cam.ac.uk>
parents:
70490
diff
changeset

749 
unfolding not_less_eq_eq [symmetric] 
f2b783abfbe7
A few lemmas connected with orderings
paulson <lp15@cam.ac.uk>
parents:
70490
diff
changeset

750 
using Suc_n_not_le_n assms order_trans strict_mono_less_eq by blast 
f2b783abfbe7
A few lemmas connected with orderings
paulson <lp15@cam.ac.uk>
parents:
70490
diff
changeset

751 
qed 
66386  752 

60758  753 
subsubsection \<open>Monotonicity of Addition\<close> 
13449  754 

63110  755 
lemma Suc_pred [simp]: "n > 0 \<Longrightarrow> Suc (n  Suc 0) = n" 
756 
by (simp add: diff_Suc split: nat.split) 

757 

758 
lemma Suc_diff_1 [simp]: "0 < n \<Longrightarrow> Suc (n  1) = n" 

759 
unfolding One_nat_def by (rule Suc_pred) 

760 

63588  761 
lemma nat_add_left_cancel_le [simp]: "k + m \<le> k + n \<longleftrightarrow> m \<le> n" 
762 
for k m n :: nat 

63110  763 
by (induct k) simp_all 
764 

63588  765 
lemma nat_add_left_cancel_less [simp]: "k + m < k + n \<longleftrightarrow> m < n" 
766 
for k m n :: nat 

63110  767 
by (induct k) simp_all 
768 

63588  769 
lemma add_gr_0 [iff]: "m + n > 0 \<longleftrightarrow> m > 0 \<or> n > 0" 
770 
for m n :: nat 

63110  771 
by (auto dest: gr0_implies_Suc) 
13449  772 

60758  773 
text \<open>strict, in 1st argument\<close> 
63588  774 
lemma add_less_mono1: "i < j \<Longrightarrow> i + k < j + k" 
775 
for i j k :: nat 

63110  776 
by (induct k) simp_all 
14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset

777 

60758  778 
text \<open>strict, in both arguments\<close> 
71585  779 
lemma add_less_mono: 
780 
fixes i j k l :: nat 

781 
assumes "i < j" "k < l" shows "i + k < j + l" 

782 
proof  

783 
have "i + k < j + k" 

784 
by (simp add: add_less_mono1 assms) 

785 
also have "... < j + l" 

786 
using \<open>i < j\<close> by (induction j) (auto simp: assms) 

787 
finally show ?thesis . 

788 
qed 

14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset

789 

63110  790 
lemma less_imp_Suc_add: "m < n \<Longrightarrow> \<exists>k. n = Suc (m + k)" 
63588  791 
proof (induct n) 
792 
case 0 

793 
then show ?case by simp 

794 
next 

795 
case Suc 

796 
then show ?case 

797 
by (simp add: order_le_less) 

798 
(blast elim!: less_SucE intro!: Nat.add_0_right [symmetric] add_Suc_right [symmetric]) 

799 
qed 

800 

801 
lemma le_Suc_ex: "k \<le> l \<Longrightarrow> (\<exists>n. l = k + n)" 

802 
for k l :: nat 

56194  803 
by (auto simp: less_Suc_eq_le[symmetric] dest: less_imp_Suc_add) 
804 

71425
f2da99316b86
more rules for natural deduction from inequalities
haftmann
parents:
71407
diff
changeset

805 
lemma less_natE: 
f2da99316b86
more rules for natural deduction from inequalities
haftmann
parents:
71407
diff
changeset

806 
assumes \<open>m < n\<close> 
f2da99316b86
more rules for natural deduction from inequalities
haftmann
parents:
71407
diff
changeset

807 
obtains q where \<open>n = Suc (m + q)\<close> 
f2da99316b86
more rules for natural deduction from inequalities
haftmann
parents:
71407
diff
changeset

808 
using assms by (auto dest: less_imp_Suc_add intro: that) 
f2da99316b86
more rules for natural deduction from inequalities
haftmann
parents:
71407
diff
changeset

809 

61799  810 
text \<open>strict, in 1st argument; proof is by induction on \<open>k > 0\<close>\<close> 
62481
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset

811 
lemma mult_less_mono2: 
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset

812 
fixes i j :: nat 
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset

813 
assumes "i < j" and "0 < k" 
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset

814 
shows "k * i < k * j" 
63110  815 
using \<open>0 < k\<close> 
816 
proof (induct k) 

817 
case 0 

818 
then show ?case by simp 

62481
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset

819 
next 
63110  820 
case (Suc k) 
821 
with \<open>i < j\<close> show ?case 

62481
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset

822 
by (cases k) (simp_all add: add_less_mono) 
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset

823 
qed 
14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset

824 

60758  825 
text \<open>Addition is the inverse of subtraction: 
69593  826 
if \<^term>\<open>n \<le> m\<close> then \<^term>\<open>n + (m  n) = m\<close>.\<close> 
63588  827 
lemma add_diff_inverse_nat: "\<not> m < n \<Longrightarrow> n + (m  n) = m" 
828 
for m n :: nat 

63110  829 
by (induct m n rule: diff_induct) simp_all 
830 

63588  831 
lemma nat_le_iff_add: "m \<le> n \<longleftrightarrow> (\<exists>k. n = m + k)" 
832 
for m n :: nat 

63110  833 
using nat_add_left_cancel_le[of m 0] by (auto dest: le_Suc_ex) 
62376
85f38d5f8807
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents:
62365
diff
changeset

834 

63588  835 
text \<open>The naturals form an ordered \<open>semidom\<close> and a \<open>dioid\<close>.\<close> 
62376
85f38d5f8807
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents:
62365
diff
changeset

836 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34208
diff
changeset

837 
instance nat :: linordered_semidom 
14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset

838 
proof 
63110  839 
fix m n q :: nat 
63588  840 
show "0 < (1::nat)" 
841 
by simp 

842 
show "m \<le> n \<Longrightarrow> q + m \<le> q + n" 

843 
by simp 

844 
show "m < n \<Longrightarrow> 0 < q \<Longrightarrow> q * m < q * n" 

845 
by (simp add: mult_less_mono2) 

846 
show "m \<noteq> 0 \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> m * n \<noteq> 0" 

847 
by simp 

63110  848 
show "n \<le> m \<Longrightarrow> (m  n) + n = m" 
60562
24af00b010cf
Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
paulson <lp15@cam.ac.uk>
parents:
60427
diff
changeset

849 
by (simp add: add_diff_inverse_nat add.commute linorder_not_less) 
62376
85f38d5f8807
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents:
62365
diff
changeset

850 
qed 
85f38d5f8807
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents:
62365
diff
changeset

851 

85f38d5f8807
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents:
62365
diff
changeset

852 
instance nat :: dioid 
63110  853 
by standard (rule nat_le_iff_add) 
63588  854 

63145  855 
declare le0[simp del] \<comment> \<open>This is now @{thm zero_le}\<close> 
856 
declare le_0_eq[simp del] \<comment> \<open>This is now @{thm le_zero_eq}\<close> 

857 
declare not_less0[simp del] \<comment> \<open>This is now @{thm not_less_zero}\<close> 

858 
declare not_gr0[simp del] \<comment> \<open>This is now @{thm not_gr_zero}\<close> 

62376
85f38d5f8807
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents:
62365
diff
changeset

859 

63110  860 
instance nat :: ordered_cancel_comm_monoid_add .. 
861 
instance nat :: ordered_cancel_comm_monoid_diff .. 

862 

44817  863 

69593  864 
subsubsection \<open>\<^term>\<open>min\<close> and \<^term>\<open>max\<close>\<close> 
44817  865 

866 
lemma mono_Suc: "mono Suc" 

63110  867 
by (rule monoI) simp 
868 

63588  869 
lemma min_0L [simp]: "min 0 n = 0" 
870 
for n :: nat 

63110  871 
by (rule min_absorb1) simp 
872 

63588  873 
lemma min_0R [simp]: "min n 0 = 0" 
874 
for n :: nat 

63110  875 
by (rule min_absorb2) simp 
44817  876 

877 
lemma min_Suc_Suc [simp]: "min (Suc m) (Suc n) = Suc (min m n)" 

63110  878 
by (simp add: mono_Suc min_of_mono) 
879 

880 
lemma min_Suc1: "min (Suc n) m = (case m of 0 \<Rightarrow> 0  Suc m' \<Rightarrow> Suc(min n m'))" 

881 
by (simp split: nat.split) 

882 

883 
lemma min_Suc2: "min m (Suc n) = (case m of 0 \<Rightarrow> 0  Suc m' \<Rightarrow> Suc(min m' n))" 

884 
by (simp split: nat.split) 

885 

63588  886 
lemma max_0L [simp]: "max 0 n = n" 
887 
for n :: nat 

63110  888 
by (rule max_absorb2) simp 
889 

63588  890 
lemma max_0R [simp]: "max n 0 = n" 
891 
for n :: nat 

63110  892 
by (rule max_absorb1) simp 
893 

894 
lemma max_Suc_Suc [simp]: "max (Suc m) (Suc n) = Suc (max m n)" 

895 
by (simp add: mono_Suc max_of_mono) 

896 

897 
lemma max_Suc1: "max (Suc n) m = (case m of 0 \<Rightarrow> Suc n  Suc m' \<Rightarrow> Suc (max n m'))" 

898 
by (simp split: nat.split) 

899 

900 
lemma max_Suc2: "max m (Suc n) = (case m of 0 \<Rightarrow> Suc n  Suc m' \<Rightarrow> Suc (max m' n))" 

901 
by (simp split: nat.split) 

902 

71841  903 
lemma max_0_iff[simp]: "max m n = (0::nat) \<longleftrightarrow> m = 0 \<and> n = 0" 
904 
by(cases m, auto simp: max_Suc1 split: nat.split) 

905 

63588  906 
lemma nat_mult_min_left: "min m n * q = min (m * q) (n * q)" 
907 
for m n q :: nat 

63110  908 
by (simp add: min_def not_le) 
909 
(auto dest: mult_right_le_imp_le mult_right_less_imp_less le_less_trans) 

910 

63588  911 
lemma nat_mult_min_right: "m * min n q = min (m * n) (m * q)" 
912 
for m n q :: nat 

63110  913 
by (simp add: min_def not_le) 
914 
(auto dest: mult_left_le_imp_le mult_left_less_imp_less le_less_trans) 

915 

63588  916 
lemma nat_add_max_left: "max m n + q = max (m + q) (n + q)" 
917 
for m n q :: nat 

44817  918 
by (simp add: max_def) 
919 

63588  920 
lemma nat_add_max_right: "m + max n q = max (m + n) (m + q)" 
921 
for m n q :: nat 

44817  922 
by (simp add: max_def) 
923 

63588  924 
lemma nat_mult_max_left: "max m n * q = max (m * q) (n * q)" 
925 
for m n q :: nat 

63110  926 
by (simp add: max_def not_le) 
927 
(auto dest: mult_right_le_imp_le mult_right_less_imp_less le_less_trans) 

928 

63588  929 
lemma nat_mult_max_right: "m * max n q = max (m * n) (m * q)" 
930 
for m n q :: nat 

63110  931 
by (simp add: max_def not_le) 
932 
(auto dest: mult_left_le_imp_le mult_left_less_imp_less le_less_trans) 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

933 

b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

934 

69593  935 
subsubsection \<open>Additional theorems about \<^term>\<open>(\<le>)\<close>\<close> 
60758  936 

937 
text \<open>Complete induction, aka courseofvalues induction\<close> 

26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset

938 

63110  939 
instance nat :: wellorder 
940 
proof 

27823  941 
fix P and n :: nat 
63110  942 
assume step: "(\<And>m. m < n \<Longrightarrow> P m) \<Longrightarrow> P n" for n :: nat 
27823  943 
have "\<And>q. q \<le> n \<Longrightarrow> P q" 
944 
proof (induct n) 

945 
case (0 n) 

26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset

946 
have "P 0" by (rule step) auto 
63588  947 
with 0 show ?case by auto 
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset

948 
next 
27823  949 
case (Suc m n) 
63588  950 
then have "n \<le> m \<or> n = Suc m" 
951 
by (simp add: le_Suc_eq) 

63110  952 
then show ?case 
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset

953 
proof 
63110  954 
assume "n \<le> m" 
955 
then show "P n" by (rule Suc(1)) 

26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset

956 
next 
27823  957 
assume n: "n = Suc m" 
63110  958 
show "P n" by (rule step) (rule Suc(1), simp add: n le_simps) 
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset

959 
qed 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset

960 
qed 
27823  961 
then show "P n" by auto 
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset

962 
qed 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset

963 

57015  964 

63588  965 
lemma Least_eq_0[simp]: "P 0 \<Longrightarrow> Least P = 0" 
966 
for P :: "nat \<Rightarrow> bool" 

63110  967 
by (rule Least_equality[OF _ le0]) 
968 

71585  969 
lemma Least_Suc: 
970 
assumes "P n" "\<not> P 0" 

971 
shows "(LEAST n. P n) = Suc (LEAST m. P (Suc m))" 

972 
proof (cases n) 

973 
case (Suc m) 

974 
show ?thesis 

975 
proof (rule antisym) 

976 
show "(LEAST x. P x) \<le> Suc (LEAST x. P (Suc x))" 

977 
using assms Suc by (force intro: LeastI Least_le) 

978 
have \<section>: "P (LEAST x. P x)" 

979 
by (blast intro: LeastI assms) 

980 
show "Suc (LEAST m. P (Suc m)) \<le> (LEAST n. P n)" 

981 
proof (cases "(LEAST n. P n)") 

982 
case 0 

983 
then show ?thesis 

984 
using \<section> by (simp add: assms) 

985 
next 

986 
case Suc 

987 
with \<section> show ?thesis 

988 
by (auto simp: Least_le) 

989 
qed 

990 
qed 

991 
qed (use assms in auto) 

27823  992 

63110  993 
lemma Least_Suc2: "P n \<Longrightarrow> Q m \<Longrightarrow> \<not> P 0 \<Longrightarrow> \<forall>k. P (Suc k) = Q k \<Longrightarrow> Least P = Suc (Least Q)" 
63588  994 
by (erule (1) Least_Suc [THEN ssubst]) simp 
995 

71585  996 
lemma ex_least_nat_le: 
997 
fixes P :: "nat \<Rightarrow> bool" 

998 
assumes "P n" "\<not> P 0" 

999 
shows "\<exists>k\<le>n. (\<forall>i<k. \<not> P i) \<and> P k" 

1000 
proof (cases n) 

1001 
case (Suc m) 

1002 
with assms show ?thesis 

1003 
by (blast intro: Least_le LeastI_ex dest: not_less_Least) 

1004 
qed (use assms in auto) 

1005 

1006 
lemma ex_least_nat_less: 

1007 
fixes P :: "nat \<Rightarrow> bool" 

1008 
assumes "P n" "\<not> P 0" 

1009 
shows "\<exists>k<n. (\<forall>i\<le>k. \<not> P i) \<and> P (Suc k)" 

1010 
proof (cases n) 

1011 
case (Suc m) 

1012 
then obtain k where k: "k \<le> n" "\<forall>i<k. \<not> P i" "P k" 

1013 
using ex_least_nat_le [OF assms] by blast 

1014 
show ?thesis 

1015 
by (cases k) (use assms k less_eq_Suc_le in auto) 

1016 
qed (use assms in auto) 

1017 

27823  1018 

26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset

1019 
lemma nat_less_induct: 
63110  1020 
fixes P :: "nat \<Rightarrow> bool" 
1021 
assumes "\<And>n. \<forall>m. m < n \<longrightarrow> P m \<Longrightarrow> P n" 

1022 
shows "P n" 

26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset

1023 
using assms less_induct by blast 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset

1024 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset

1025 
lemma measure_induct_rule [case_names less]: 
64876  1026 
fixes f :: "'a \<Rightarrow> 'b::wellorder" 
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset

1027 
assumes step: "\<And>x. (\<And>y. f y < f x \<Longrightarrow> P y) \<Longrightarrow> P x" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset

1028 
shows "P a" 
63110  1029 
by (induct m \<equiv> "f a" arbitrary: a rule: less_induct) (auto intro: step) 
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset

1030 

60758  1031 
text \<open>old style induction rules:\<close> 
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset

1032 
lemma measure_induct: 
64876  1033 
fixes f :: "'a \<Rightarrow> 'b::wellorder" 
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset

1034 
shows "(\<And>x. \<forall>y. f y < f x \<longrightarrow> P y \<Longrightarrow> P x) \<Longrightarrow> P a" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset

1035 
by (rule measure_induct_rule [of f P a]) iprover 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset

1036 

4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset

1037 
lemma full_nat_induct: 
63110  1038 
assumes step: "\<And>n. (\<forall>m. Suc m \<le> n \<longrightarrow> P m) \<Longrightarrow> P n" 
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset

1039 
shows "P n" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset

1040 
by (rule less_induct) (auto intro: step simp:le_simps) 
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

1041 

63110  1042 
text\<open>An induction rule for establishing binary relations\<close> 
62683  1043 
lemma less_Suc_induct [consumes 1]: 
63110  1044 
assumes less: "i < j" 
1045 
and step: "\<And>i. P i (Suc i)" 

1046 
and trans: "\<And>i j k. i < j \<Longrightarrow> j < k \<Longrightarrow> P i j \<Longrightarrow> P j k \<Longrightarrow> P i k" 

19870  1047 
shows "P i j" 
1048 
proof  

63110  1049 
from less obtain k where j: "j = Suc (i + k)" 
1050 
by (auto dest: less_imp_Suc_add) 

22718  1051 
have "P i (Suc (i + k))" 
19870  1052 
proof (induct k) 
22718  1053 
case 0 
1054 
show ?case by (simp add: step) 

19870  1055 
next 
1056 
case (Suc k) 

31714  1057 
have "0 + i < Suc k + i" by (rule add_less_mono1) simp 
63110  1058 
then have "i < Suc (i + k)" by (simp add: add.commute) 
31714  1059 
from trans[OF this lessI Suc step] 
1060 
show ?case by simp 

19870  1061 
qed 
63110  1062 
then show "P i j" by (simp add: j) 
19870  1063 
qed 
1064 

63111  1065 
text \<open> 
1066 
The method of infinite descent, frequently used in number theory. 

1067 
Provided by Roelof Oosterhuis. 

1068 
\<open>P n\<close> is true for all natural numbers if 

1069 
\<^item> case ``0'': given \<open>n = 0\<close> prove \<open>P n\<close> 

1070 
\<^item> case ``smaller'': given \<open>n > 0\<close> and \<open>\<not> P n\<close> prove there exists 

1071 
a smaller natural number \<open>m\<close> such that \<open>\<not> P m\<close>. 

1072 
\<close> 

1073 

63110  1074 
lemma infinite_descent: "(\<And>n. \<not> P n \<Longrightarrow> \<exists>m<n. \<not> P m) \<Longrightarrow> P n" for P :: "nat \<Rightarrow> bool" 
63111  1075 
\<comment> \<open>compact version without explicit base case\<close> 
63110  1076 
by (induct n rule: less_induct) auto 
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset

1077 

63111  1078 
lemma infinite_descent0 [case_names 0 smaller]: 
63110  1079 
fixes P :: "nat \<Rightarrow> bool" 
63111  1080 
assumes "P 0" 
1081 
and "\<And>n. n > 0 \<Longrightarrow> \<not> P n \<Longrightarrow> \<exists>m. m < n \<and> \<not> P m" 

63110  1082 
shows "P n" 
71585  1083 
proof (rule infinite_descent) 
1084 
show "\<And>n. \<not> P n \<Longrightarrow> \<exists>m<n. \<not> P m" 

1085 
using assms by (case_tac "n > 0") auto 

1086 
qed 

26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset

1087 

60758  1088 
text \<open> 
63111  1089 
Infinite descent using a mapping to \<open>nat\<close>: 
1090 
\<open>P x\<close> is true for all \<open>x \<in> D\<close> if there exists a \<open>V \<in> D \<Rightarrow> nat\<close> and 

1091 
\<^item> case ``0'': given \<open>V x = 0\<close> prove \<open>P x\<close> 

1092 
\<^item> ``smaller'': given \<open>V x > 0\<close> and \<open>\<not> P x\<close> prove 

1093 
there exists a \<open>y \<in> D\<close> such that \<open>V y < V x\<close> and \<open>\<not> P y\<close>. 

1094 
\<close> 

26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset

1095 
corollary infinite_descent0_measure [case_names 0 smaller]: 
63110  1096 
fixes V :: "'a \<Rightarrow> nat" 
1097 
assumes 1: "\<And>x. V x = 0 \<Longrightarrow> P x" 

1098 
and 2: "\<And>x. V x > 0 \<Longrightarrow> \<not> P x \<Longrightarrow> \<exists>y. V y < V x \<and> \<not> P y" 

26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset

1099 
shows "P x" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset

1100 
proof  
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset

1101 
obtain n where "n = V x" by auto 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset

1102 
moreover have "\<And>x. V x = n \<Longrightarrow> P x" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset

1103 
proof (induct n rule: infinite_descent0) 
63110  1104 
case 0 
1105 
with 1 show "P x" by auto 

1106 
next 

26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset

1107 
case (smaller n) 
63110  1108 
then obtain x where *: "V x = n " and "V x > 0 \<and> \<not> P x" by auto 
1109 
with 2 obtain y where "V y < V x \<and> \<not> P y" by auto 

63111  1110 
with * obtain m where "m = V y \<and> m < n \<and> \<not> P y" by auto 
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset

1111 
then show ?case by auto 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset

1112 
qed 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset

1113 
ultimately show "P x" by auto 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset

1114 
qed 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset

1115 

63588  1116 
text \<open>Again, without explicit base case:\<close> 
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset

1117 
lemma infinite_descent_measure: 
63110  1118 
fixes V :: "'a \<Rightarrow> nat" 
1119 
assumes "\<And>x. \<not> P x \<Longrightarrow> \<exists>y. V y < V x \<and> \<not> P y" 

1120 
shows "P x" 

26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset

1121 
proof  
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset

1122 
from assms obtain n where "n = V x" by auto 
63110  1123 
moreover have "\<And>x. V x = n \<Longrightarrow> P x" 
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset

1124 
proof (induct n rule: infinite_descent, auto) 
63111  1125 
show "\<exists>m < V x. \<exists>y. V y = m \<and> \<not> P y" if "\<not> P x" for x 
1126 
using assms and that by auto 

26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset

1127 
qed 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset

1128 
ultimately show "P x" by auto 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset

1129 
qed 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset

1130 

63111  1131 
text \<open>A (clumsy) way of lifting \<open><\<close> monotonicity to \<open>\<le>\<close> monotonicity\<close> 
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

1132 
lemma less_mono_imp_le_mono: 
63110  1133 
fixes f :: "nat \<Rightarrow> nat" 
1134 
and i j :: nat 

1135 
assumes "\<And>i j::nat. i < j \<Longrightarrow> f i < f j" 

1136 
and "i \<le> j" 

1137 
shows "f i \<le> f j" 

1138 
using assms by (auto simp add: order_le_less) 

24438  1139 

14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

1140 

60758  1141 
text \<open>nonstrict, in 1st argument\<close> 
63588  1142 
lemma add_le_mono1: "i \<le> j \<Longrightarrow> i + k \<le> j + k" 
1143 
for i j k :: nat 

63110  1144 
by (rule add_right_mono) 
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset

1145 

60758  1146 
text \<open>nonstrict, in both arguments\<close> 
63588  1147 
lemma add_le_mono: "i \<le> j \<Longrightarrow> k \<le> l \<Longrightarrow> i + k \<le> j + l" 
1148 
for i j k l :: nat 

63110  1149 
by (rule add_mono) 
1150 

63588  1151 
lemma le_add2: "n \<le> m + n" 
1152 
for m n :: nat 

62608  1153 
by simp 
13449  1154 

63588  1155 
lemma le_add1: "n \<le> n + m" 
1156 
for m n :: nat 

62608  1157 
by simp 
13449  1158 

1159 
lemma less_add_Suc1: "i < Suc (i + m)" 

63110  1160 
by (rule le_less_trans, rule le_add1, rule lessI) 
13449  1161 

1162 
lemma less_add_Suc2: "i < Suc (m + i)" 

63110  1163 
by (rule le_less_trans, rule le_add2, rule lessI) 
1164 

1165 
lemma less_iff_Suc_add: "m < n \<longleftrightarrow> (\<exists>k. n = Suc (m + k))" 

1166 
by (iprover intro!: less_add_Suc1 less_imp_Suc_add) 

1167 

63588  1168 
lemma trans_le_add1: "i \<le> j \<Longrightarrow> i \<le> j + m" 
1169 
for i j m :: nat 

63110  1170 
by (rule le_trans, assumption, rule le_add1) 
1171 

63588  1172 
lemma trans_le_add2: "i \<le> j \<Longrightarrow> i \<le> m + j" 
1173 
for i j m :: nat 

63110  1174 
by (rule le_trans, assumption, rule le_add2) 
1175 

63588  1176 
lemma trans_less_add1: "i < j \<Longrightarrow> i < j + m" 
1177 
for i j m :: nat 

63110  1178 
by (rule less_le_trans, assumption, rule le_add1) 
1179 

63588  1180 
lemma trans_less_add2: "i < j \<Longrightarrow> i < m + j" 
1181 
for i j m :: nat 

63110  1182 
by (rule less_le_trans, assumption, rule le_add2) 
1183 

63588  1184 
lemma add_lessD1: "i + j < k \<Longrightarrow> i < k" 
1185 
for i j k :: nat 

63110  1186 
by (rule le_less_trans [of _ "i+j"]) (simp_all add: le_add1) 
1187 

63588  1188 
lemma not_add_less1 [iff]: "\<not> i + j < i" 
1189 
for i j :: nat 

71585  1190 
by simp 
63110  1191 

63588  1192 
lemma not_add_less2 [iff]: "\<not> j + i < i" 
1193 
for i j :: nat 

71585  1194 
by simp 
63110  1195 

63588  1196 
lemma add_leD1: "m + k \<le> n \<Longrightarrow> m \<le> n" 
1197 
for k m n :: nat 

1198 
by (rule order_trans [of _ "m + k"]) (simp_all add: le_add1) 

1199 

1200 
lemma add_leD2: "m + k \<le> n \<Longrightarrow> k \<le> n" 

1201 
for k m n :: nat 

71585  1202 
by (force simp add: add.commute dest: add_leD1) 
63110  1203 

63588  1204 
lemma add_leE: "m + k \<le> n \<Longrightarrow> (m \<le> n \<Longrightarrow> k \<le> n \<Longrightarrow> R) \<Longrightarrow> R" 
1205 
for k m n :: nat 

63110  1206 
by (blast dest: add_leD1 add_leD2) 
1207 

1208 
text \<open>needs \<open>\<And>k\<close> for \<open>ac_simps\<close> to work\<close> 

63588  1209 
lemma less_add_eq_less: "\<And>k. k < l \<Longrightarrow> m + l = k + n \<Longrightarrow> m < n" 
1210 
for l m n :: nat 

63110  1211 
by (force simp del: add_Suc_right simp add: less_iff_Suc_add add_Suc_right [symmetric] ac_simps) 
13449  1212 

1213 

60758  1214 
subsubsection \<open>More results about difference\<close> 
13449  1215 

63110  1216 
lemma Suc_diff_le: "n \<le> m \<Longrightarrow> Suc m  n = Suc (m  n)" 
1217 
by (induct m n rule: diff_induct) simp_all 

13449  1218 

1219 
lemma diff_less_Suc: "m  n < Suc m" 

71585  1220 
by (induct m n rule: diff_induct) (auto simp: less_Suc_eq) 
63588  1221 

1222 
lemma diff_le_self [simp]: "m  n \<le> m" 

1223 
for m n :: nat 

63110  1224 
by (induct m n rule: diff_induct) (simp_all add: le_SucI) 
1225 

63588  1226 
lemma less_imp_diff_less: "j < k \<Longrightarrow> j  n < k" 
1227 
for j k n :: nat 

63110  1228 
by (rule le_less_trans, rule diff_le_self) 
1229 

1230 
lemma diff_Suc_less [simp]: "0 < n \<Longrightarrow> n  Suc i < n" 

1231 
by (cases n) (auto simp add: le_simps) 

1232 

63588  1233 
lemma diff_add_assoc: "k \<le> j \<Longrightarrow> (i + j)  k = i + (j  k)" 
1234 
for i j k :: nat 

71404
f2b783abfbe7
A few lemmas connected with orderings
paulson <lp15@cam.ac.uk>
parents:
70490
diff
changeset

1235 
by (fact ordered_cancel_comm_monoid_diff_class.diff_add_assoc) 
63110  1236 

63588  1237 
lemma add_diff_assoc [simp]: "k \<le> j \<Longrightarrow> i + (j  k) = i + j  k" 
1238 
for i j k :: nat 

71404
f2b783abfbe7
A few lemmas connected with orderings
paulson <lp15@cam.ac.uk>
parents:
70490
diff
changeset

1239 
by (fact ordered_cancel_comm_monoid_diff_class.add_diff_assoc) 
62481
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset

1240 

63588  1241 
lemma diff_add_assoc2: "k \<le> j \<Longrightarrow> (j + i)  k = (j  k) + i" 
1242 
for i j k :: nat 

71404
f2b783abfbe7
A few lemmas connected with orderings
paulson <lp15@cam.ac.uk>
parents:
70490
diff
changeset

1243 
by (fact ordered_cancel_comm_monoid_diff_class.diff_add_assoc2) 
62481
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset

1244 

63588  1245 
lemma add_diff_assoc2 [simp]: "k \<le> j \<Longrightarrow> j  k + i = j + i  k" 
1246 
for i j k :: nat 

71404
f2b783abfbe7
A few lemmas connected with orderings
paulson <lp15@cam.ac.uk>
parents:
70490
diff
changeset

1247 
by (fact ordered_cancel_comm_monoid_diff_class.add_diff_assoc2) 
13449  1248 

63588  1249 
lemma le_imp_diff_is_add: "i \<le> j \<Longrightarrow> (j  i = k) = (j = k + i)" 
1250 
for i j k :: nat 

63110  1251 
by auto 
1252 

63588  1253 
lemma diff_is_0_eq [simp]: "m  n = 0 \<longleftrightarrow> m \<le> n" 
1254 
for m n :: nat 

63110  1255 
by (induct m n rule: diff_induct) simp_all 
1256 

63588  1257 
lemma diff_is_0_eq' [simp]: "m \<le> n \<Longrightarrow> m  n = 0" 
1258 
for m n :: nat 

63110  1259 
by (rule iffD2, rule diff_is_0_eq) 
1260 

63588  1261 
lemma zero_less_diff [simp]: "0 < n  m \<longleftrightarrow> m < n" 
1262 
for m n :: nat 

63110  1263 
by (induct m n rule: diff_induct) simp_all 
13449  1264 

22718  1265 
lemma less_imp_add_positive: 
1266 
assumes "i < j" 

63110  1267 
shows "\<exists>k::nat. 0 < k \<and> i + k = j" 
22718  1268 
proof 
63110  1269 
from assms show "0 < j  i \<and> i + (j  i) = j" 
23476  1270 
by (simp add: order_less_imp_le) 
22718  1271 
qed 
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
7702
diff
changeset

1272 

60758  1273 
text \<open>a nice rewrite for bounded subtraction\<close> 
63588  1274 
lemma nat_minus_add_max: "n  m + m = max n m" 
1275 
for m n :: nat 

1276 
by (simp add: max_def not_le order_less_imp_le) 

13449  1277 

63110  1278 
lemma nat_diff_split: "P (a  b) \<longleftrightarrow> (a < b \<longrightarrow> P 0) \<and> (\<forall>d. a = b + d \<longrightarrow> P d)" 
1279 
for a b :: nat 

63588  1280 
\<comment> \<open>elimination of \<open>\<close> on \<open>nat\<close>\<close> 
1281 
by (cases "a < b") (auto simp add: not_less le_less dest!: add_eq_self_zero [OF sym]) 

13449  1282 

63110  1283 
lemma nat_diff_split_asm: "P (a  b) \<longleftrightarrow> \<not> (a < b \<and> \<not> P 0 \<or> (\<exists>d. a = b + d \<and> \<not> P d))" 
1284 
for a b :: nat 

63588  1285 
\<comment> \<open>elimination of \<open>\<close> on \<open>nat\<close> in assumptions\<close> 
62365  1286 
by (auto split: nat_diff_split) 
13449  1287 

63110  1288 
lemma Suc_pred': "0 < n \<Longrightarrow> n = Suc(n  1)" 
47255
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47208
diff
changeset

1289 
by simp 
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47208
diff
changeset

1290 

63110  1291 
lemma add_eq_if: "m + n = (if m = 0 then n else Suc ((m  1) + n))" 
47255
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47208
diff
changeset

1292 
unfolding One_nat_def by (cases m) simp_all 
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47208
diff
changeset

1293 

63588  1294 
lemma mult_eq_if: "m * n = (if m = 0 then 0 else n + ((m  1) * n))" 
1295 
for m n :: nat 

1296 
by (cases m) simp_all 

47255
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47208
diff
changeset

1297 

63110  1298 
lemma Suc_diff_eq_diff_pred: "0 < n \<Longrightarrow> Suc m  n = m  (n  1)" 
63588  1299 
by (cases n) simp_all 
47255
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47208
diff
changeset

1300 

30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47208
diff
changeset

1301 
lemma diff_Suc_eq_diff_pred: "m  Suc n = (m  1)  n" 
63588  1302 
by (cases m) simp_all 
1303 
