author  wenzelm 
Mon, 23 May 2016 14:43:14 +0200  
changeset 63110  ccbdce905fca 
parent 63099  af0e964aad7b 
child 63111  caa0c513bbca 
permissions  rwrr 
923  1 
(* Title: HOL/Nat.thy 
21243  2 
Author: Tobias Nipkow and Lawrence C Paulson and Markus Wenzel 
923  3 

9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
7702
diff
changeset

4 
Type "nat" is a linear order, and a datatype; arithmetic operators +  
30496
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
30242
diff
changeset

5 
and * (for div and mod, see theory Divides). 
923  6 
*) 
7 

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

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

11 
imports Inductive Typedef Fun Rings 
15131  12 
begin 
13449  13 

48891  14 
ML_file "~~/src/Tools/rat.ML" 
57952  15 

16 
named_theorems arith "arith facts  only ground formulas" 

48891  17 
ML_file "Tools/arith_data.ML" 
18 

19 

61799  20 
subsection \<open>Type \<open>ind\<close>\<close> 
13449  21 

22 
typedecl ind 

23 

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

26 
where Suc_Rep_inject: "Suc_Rep x = Suc_Rep y \<Longrightarrow> x = y" 

27 
and Suc_Rep_not_Zero_Rep: "Suc_Rep x \<noteq> Zero_Rep" 

19573  28 

60758  29 
subsection \<open>Type nat\<close> 
30 

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

13449  32 

44325  33 
inductive Nat :: "ind \<Rightarrow> bool" where 
34 
Zero_RepI: "Nat Zero_Rep" 

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

13449  36 

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

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

40 

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

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

42 
"Nat (Rep_Nat n)" 
1220ecb81e8f
observe distinction between sets and predicates more properly
haftmann
parents:
43595
diff
changeset

43 
using Rep_Nat by simp 
13449  44 

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

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

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

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

48 

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

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

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

51 
using Abs_Nat_inject by simp 
13449  52 

25510  53 
instantiation nat :: zero 
54 
begin 

55 

37767  56 
definition Zero_nat_def: 
25510  57 
"0 = Abs_Nat Zero_Rep" 
58 

59 
instance .. 

60 

61 
end 

24995  62 

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

63 
definition Suc :: "nat \<Rightarrow> nat" where 
1220ecb81e8f
observe distinction between sets and predicates more properly
haftmann
parents:
43595
diff
changeset

64 
"Suc n = Abs_Nat (Suc_Rep (Rep_Nat n))" 
1220ecb81e8f
observe distinction between sets and predicates more properly
haftmann
parents:
43595
diff
changeset

65 

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

66 
lemma Suc_not_Zero: "Suc m \<noteq> 0" 
44278
1220ecb81e8f
observe distinction between sets and predicates more properly
haftmann
parents:
43595
diff
changeset

67 
by (simp add: Zero_nat_def Suc_def Suc_RepI Zero_RepI Nat_Abs_Nat_inject Suc_Rep_not_Zero_Rep Nat_Rep_Nat) 
13449  68 

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

69 
lemma Zero_not_Suc: "0 \<noteq> Suc m" 
13449  70 
by (rule not_sym, rule Suc_not_Zero not_sym) 
71 

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

72 
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

73 
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

74 

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

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

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

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

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

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

80 
apply (unfold Zero_nat_def Suc_def) 
61799  81 
apply (rule Rep_Nat_inverse [THEN subst]) \<comment> \<open>types force good instantiation\<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

82 
apply (erule Nat_Rep_Nat [THEN 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

83 
apply (iprover elim: Nat_Abs_Nat_inverse [THEN subst]) 
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
55415
diff
changeset

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

85 

55469
b19dd108f0c2
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
blanchet
parents:
55468
diff
changeset

86 
free_constructors case_nat for 
61076  87 
"0 :: nat" 
55469
b19dd108f0c2
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
blanchet
parents:
55468
diff
changeset

88 
 Suc pred 
57200
aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57091
diff
changeset

89 
where 
61076  90 
"pred (0 :: nat) = (0 :: nat)" 
58189
9d714be4f028
added 'plugins' option to control which hooks are enabled
blanchet
parents:
57983
diff
changeset

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

92 
apply (rename_tac n, induct_tac n rule: nat_induct0, auto) 
9d714be4f028
added 'plugins' option to control which hooks are enabled
blanchet
parents:
57983
diff
changeset

93 
apply (simp add: Suc_def Nat_Abs_Nat_inject Nat_Rep_Nat Suc_RepI Suc_Rep_inject' 
9d714be4f028
added 'plugins' option to control which hooks are enabled
blanchet
parents:
57983
diff
changeset

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

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

96 
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

97 

61799  98 
\<comment> \<open>Avoid name clashes by prefixing the output of \<open>old_rep_datatype\<close> with \<open>old\<close>.\<close> 
60758  99 
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

100 

61076  101 
old_rep_datatype "0 :: nat" Suc 
55417
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
55415
diff
changeset

102 
apply (erule nat_induct0, assumption) 
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
55415
diff
changeset

103 
apply (rule nat.inject) 
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
55415
diff
changeset

104 
apply (rule nat.distinct(1)) 
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
55415
diff
changeset

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

106 

60758  107 
setup \<open>Sign.parent_path\<close> 
108 

61799  109 
\<comment> \<open>But erase the prefix for properties that are not generated by \<open>free_constructors\<close>.\<close> 
60758  110 
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

111 

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

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

113 
old.nat.inject[iff del] 
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
55415
diff
changeset

114 
old.nat.distinct(1)[simp del, induct_simp del] 
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
55415
diff
changeset

115 

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

116 
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

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

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

119 
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

120 

60758  121 
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

122 

63110  123 
abbreviation rec_nat :: "'a \<Rightarrow> (nat \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a" 
124 
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

125 

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

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

127 

61799  128 
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

129 
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

130 
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

131 
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

132 
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

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

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

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

136 
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

137 

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

138 
lemma nat_exhaust [case_names 0 Suc, cases type: nat]: 
61799  139 
\<comment> \<open>for backward compatibility  names of variables differ\<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

140 
"(y = 0 \<Longrightarrow> P) \<Longrightarrow> (\<And>nat. y = Suc nat \<Longrightarrow> P) \<Longrightarrow> P" 
55423
07dea66779f3
for extraction  use the exhaust rule that's registered with 'datatype_realizer.ML'
blanchet
parents:
55417
diff
changeset

141 
by (rule old.nat.exhaust) 
13449  142 

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

143 
lemma nat_induct [case_names 0 Suc, induct type: nat]: 
61799  144 
\<comment> \<open>for backward compatibility  names of variables differ\<close> 
27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
26748
diff
changeset

145 
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

146 
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

147 
shows "P 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

148 
using assms by (rule nat.induct) 
13449  149 

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

150 
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

151 
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

152 
nat_induct0 
24995  153 

60758  154 
ML \<open> 
58389  155 
val nat_basic_lfp_sugar = 
156 
let 

157 
val ctr_sugar = the (Ctr_Sugar.ctr_sugar_of_global @{theory} @{type_name nat}); 

158 
val recx = Logic.varify_types_global @{term rec_nat}; 

159 
val C = body_type (fastype_of recx); 

160 
in 

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

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

163 
end; 

60758  164 
\<close> 
165 

166 
setup \<open> 

58389  167 
let 
168 
fun basic_lfp_sugars_of _ [@{typ nat}] _ _ ctxt = 

62326
3cf7a067599c
allow predicator instead of map function in 'primrec'
blanchet
parents:
62217
diff
changeset

169 
([], [0], [nat_basic_lfp_sugar], [], [], [], TrueI (*dummy*), [], false, ctxt) 
58389  170 
 basic_lfp_sugars_of bs arg_Ts callers callssss ctxt = 
171 
BNF_LFP_Rec_Sugar.default_basic_lfp_sugars_of bs arg_Ts callers callssss ctxt; 

172 
in 

173 
BNF_LFP_Rec_Sugar.register_lfp_rec_extension 

174 
{nested_simps = [], is_new_datatype = K (K true), basic_lfp_sugars_of = basic_lfp_sugars_of, 

175 
rewrite_nested_rec_call = NONE} 

176 
end 

60758  177 
\<close> 
178 

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

24995  180 

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

181 
lemma inj_Suc[simp]: "inj_on Suc N" 
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
26748
diff
changeset

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

183 

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

184 
lemma Suc_neq_Zero: "Suc m = 0 \<Longrightarrow> R" 
25162  185 
by (rule notE, rule Suc_not_Zero) 
24995  186 

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

187 
lemma Zero_neq_Suc: "0 = Suc m \<Longrightarrow> R" 
25162  188 
by (rule Suc_neq_Zero, erule sym) 
24995  189 

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

190 
lemma Suc_inject: "Suc x = Suc y \<Longrightarrow> x = y" 
25162  191 
by (rule inj_Suc [THEN injD]) 
24995  192 

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

193 
lemma n_not_Suc_n: "n \<noteq> Suc n" 
25162  194 
by (induct n) simp_all 
13449  195 

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

196 
lemma Suc_n_not_n: "Suc n \<noteq> n" 
25162  197 
by (rule not_sym, rule n_not_Suc_n) 
13449  198 

60758  199 
text \<open>A special form of induction for reasoning 
200 
about @{term "m < n"} and @{term "m  n"}\<close> 

13449  201 

63110  202 
lemma diff_induct: 
203 
assumes "\<And>x. P x 0" 

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

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

206 
shows "P m n" 

207 
using assms 

14208  208 
apply (rule_tac x = m in spec) 
15251  209 
apply (induct n) 
13449  210 
prefer 2 
211 
apply (rule allI) 

17589  212 
apply (induct_tac x, iprover+) 
13449  213 
done 
214 

24995  215 

60758  216 
subsection \<open>Arithmetic operators\<close> 
24995  217 

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

219 
begin 
24995  220 

55575
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55534
diff
changeset

221 
primrec plus_nat where 
63110  222 
add_0: "0 + n = (n::nat)" 
223 
 add_Suc: "Suc m + n = Suc (m + n)" 

224 

225 
lemma add_0_right [simp]: "m + 0 = m" for m :: nat 

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

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

227 

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

228 
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

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

230 

28514  231 
declare add_0 [code] 
232 

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

233 
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

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

235 

55575
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55534
diff
changeset

236 
primrec minus_nat where 
61076  237 
diff_0 [code]: "m  0 = (m::nat)" 
63110  238 
 diff_Suc: "m  Suc n = (case m  n of 0 \<Rightarrow> 0  Suc k \<Rightarrow> k)" 
24995  239 

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

241 

63110  242 
lemma diff_0_eq_0 [simp, code]: "0  n = 0" for n :: nat 
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

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

244 

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

245 
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

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

247 

63110  248 
instance 
249 
proof 

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

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

251 
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

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

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

254 
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

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

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

258 

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

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

260 

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

261 
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

262 

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

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

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

265 

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

266 
definition 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46351
diff
changeset

267 
One_nat_def [simp]: "1 = Suc 0" 
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

268 

55575
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55534
diff
changeset

269 
primrec times_nat where 
61076  270 
mult_0: "0 * n = (0::nat)" 
44325  271 
 mult_Suc: "Suc m * n = n + (m * n)" 
25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25563
diff
changeset

272 

63110  273 
lemma mult_0_right [simp]: "m * 0 = 0" for m :: nat 
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

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

275 

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

276 
lemma 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

277 
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

278 

63110  279 
lemma add_mult_distrib: "(m + n) * k = (m * k) + (n * k)" 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 

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

285 
show "0 \<noteq> (1::nat)" unfolding One_nat_def by simp 
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

286 
show "1 * n = n" unfolding One_nat_def by simp 
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

287 
show "n * m = m * n" by (induct n) simp_all 
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

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

289 
show "(n + m) * q = n * q + m * q" by (rule add_mult_distrib) 
63110  290 
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

291 
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

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

293 

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

294 
end 
24995  295 

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 

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

298 

61799  299 
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

300 

63110  301 
lemma add_is_0 [iff]: "(m + n = 0) = (m = 0 \<and> n = 0)" for m n :: nat 
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

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

303 

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

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

306 

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

308 
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

309 

63110  310 
lemma add_eq_self_zero: "m + n = m \<Longrightarrow> n = 0" for m n :: nat 
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

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

312 

63110  313 
lemma inj_on_add_nat[simp]: "inj_on (\<lambda>n. n + k) N" for k :: nat 
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

314 
apply (induct k) 
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

315 
apply simp 
63110  316 
apply (drule comp_inj_on[OF _ inj_Suc]) 
317 
apply (simp add: o_def) 

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

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

319 

47208  320 
lemma Suc_eq_plus1: "Suc n = n + 1" 
321 
unfolding One_nat_def by simp 

322 

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

324 
unfolding One_nat_def by simp 

325 

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

326 

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

328 

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

329 
lemma Suc_diff_diff [simp]: "(Suc m  n)  Suc k = m  n  k" 
62365  330 
by (simp add: diff_diff_add) 
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

331 

30093  332 
lemma diff_Suc_1 [simp]: "Suc n  1 = n" 
333 
unfolding One_nat_def by simp 

334 

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

336 

63110  337 
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

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

339 

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

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

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

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

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

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

346 

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

348 
apply (rule trans) 
44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44848
diff
changeset

349 
apply (rule_tac [2] mult_eq_1_iff, fastforce) 
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

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

351 

63110  352 
lemma nat_mult_eq_1_iff [simp]: "m * n = 1 \<longleftrightarrow> m = 1 \<and> n = 1" for m 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

353 
unfolding One_nat_def by (rule mult_eq_1_iff) 
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

354 

63110  355 
lemma nat_1_eq_mult_iff [simp]: "1 = m * n \<longleftrightarrow> m = 1 \<and> n = 1" for m 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

356 
unfolding One_nat_def by (rule one_eq_mult_iff) 
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

357 

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

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

360 
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

361 
proof (induct n arbitrary: m) 
63110  362 
case 0 
363 
then show "m = 0" by simp 

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

364 
next 
63110  365 
case (Suc n) 
366 
then show "m = Suc n" 

367 
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

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

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

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

371 

63110  372 
lemma mult_cancel2 [simp]: "m * k = n * k \<longleftrightarrow> m = n \<or> k = 0" for k m n :: nat 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57492
diff
changeset

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

374 

63110  375 
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

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

377 

24995  378 

60758  379 
subsection \<open>Orders on @{typ nat}\<close> 
380 

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

24995  382 

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

383 
instantiation nat :: linorder 
25510  384 
begin 
385 

55575
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55534
diff
changeset

386 
primrec less_eq_nat where 
61076  387 
"(0::nat) \<le> n \<longleftrightarrow> True" 
44325  388 
 "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

389 

28514  390 
declare less_eq_nat.simps [simp del] 
63110  391 

392 
lemma le0 [iff]: "0 \<le> n" for n :: nat 

393 
by (simp add: less_eq_nat.simps) 

394 

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

396 
by simp 

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

397 

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

398 
definition less_nat where 
28514  399 
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

400 

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

401 
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

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

403 

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

404 
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

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

406 

63110  407 
lemma le_0_eq [iff]: "n \<le> 0 \<longleftrightarrow> n = 0" for n :: nat 
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

408 
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

409 

63110  410 
lemma not_less0 [iff]: "\<not> n < 0" for n :: nat 
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

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

412 

63110  413 
lemma less_nat_zero_code [code]: "n < 0 \<longleftrightarrow> False" for n :: nat 
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

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

415 

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

416 
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

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

418 

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

419 
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

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

421 

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

424 

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

425 
lemma le_SucI: "m \<le> n \<Longrightarrow> m \<le> Suc n" 
63110  426 
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

427 

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

428 
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

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

430 

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

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

432 
by (simp add: less_eq_Suc_le) (erule Suc_leD) 
24995  433 

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

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

435 
by (simp add: less_eq_Suc_le) (erule Suc_leD) 
25510  436 

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

437 
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

438 
proof 
63110  439 
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

440 
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

441 
proof (induct n arbitrary: m) 
63110  442 
case 0 
443 
then show ?case 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

444 
next 
63110  445 
case (Suc n) 
446 
then show ?case 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

447 
qed 
63110  448 
show "n \<le> n" by (induct n) simp_all 
449 
then show "n = m" if "n \<le> m" and "m \<le> n" 

450 
using that by (induct n arbitrary: m) 

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

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

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

454 
proof (induct n arbitrary: m q) 
63110  455 
case 0 
456 
show ?case by simp 

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

457 
next 
63110  458 
case (Suc n) 
459 
then show ?case 

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

460 
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

461 
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

462 
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

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

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

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

467 
qed 
25510  468 

469 
end 

13449  470 

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

471 
instantiation nat :: order_bot 
29652  472 
begin 
473 

63110  474 
definition bot_nat :: nat where "bot_nat = 0" 
475 

476 
instance by standard (simp add: bot_nat_def) 

29652  477 

478 
end 

479 

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

480 
instance nat :: no_top 
61169  481 
by standard (auto intro: less_Suc_eq_le [THEN iffD2]) 
52289  482 

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

483 

60758  484 
subsubsection \<open>Introduction properties\<close> 
13449  485 

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

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

487 
by (simp add: less_Suc_eq_le) 
13449  488 

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

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

490 
by (simp add: less_Suc_eq_le) 
13449  491 

492 

60758  493 
subsubsection \<open>Elimination properties\<close> 
13449  494 

63110  495 
lemma less_not_refl: "\<not> n < n" for n :: nat 
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

496 
by (rule order_less_irrefl) 
13449  497 

63110  498 
lemma less_not_refl2: "n < m \<Longrightarrow> m \<noteq> n" 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

499 
by (rule not_sym) (rule less_imp_neq) 
13449  500 

63110  501 
lemma less_not_refl3: "s < t \<Longrightarrow> s \<noteq> t" for s t :: nat 
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

502 
by (rule less_imp_neq) 
13449  503 

63110  504 
lemma less_irrefl_nat: "n < n \<Longrightarrow> R" for n :: nat 
26335
961bbcc9d85b
removed redundant Nat.less_not_sym, Nat.less_asym;
wenzelm
parents:
26315
diff
changeset

505 
by (rule notE, rule less_not_refl) 
13449  506 

63110  507 
lemma less_zeroE: "n < 0 \<Longrightarrow> R" for n :: nat 
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

508 
by (rule notE) (rule not_less0) 
13449  509 

63110  510 
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

511 
unfolding less_Suc_eq_le le_less .. 
13449  512 

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

513 
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

514 
by (simp add: less_Suc_eq) 
13449  515 

63110  516 
lemma less_one [iff]: "n < 1 \<longleftrightarrow> n = 0" 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

517 
unfolding One_nat_def by (rule less_Suc0) 
13449  518 

63110  519 
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

520 
by simp 
13449  521 

60758  522 
text \<open>"Less than" is antisymmetric, sort of\<close> 
14302  523 
lemma less_antisym: "\<lbrakk> \<not> n < m; n < Suc m \<rbrakk> \<Longrightarrow> m = n" 
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

524 
unfolding not_less less_Suc_eq_le by (rule antisym) 
14302  525 

63110  526 
lemma nat_neq_iff: "m \<noteq> n \<longleftrightarrow> m < n \<or> n < m" for m n :: nat 
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

527 
by (rule linorder_neq_iff) 
13449  528 

63110  529 
lemma nat_less_cases: 
530 
fixes m n :: nat 

531 
assumes major: "m < n \<Longrightarrow> P n m" 

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

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

13449  534 
shows "P n m" 
535 
apply (rule less_linear [THEN disjE]) 

536 
apply (erule_tac [2] disjE) 

63110  537 
apply (erule less) 
538 
apply (erule sym [THEN eq]) 

13449  539 
apply (erule major) 
540 
done 

541 

542 

60758  543 
subsubsection \<open>Inductive (?) properties\<close> 
13449  544 

63110  545 
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

546 
unfolding less_eq_Suc_le [of m] le_less by simp 
13449  547 

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

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

549 
assumes major: "i < k" 
63110  550 
and 1: "k = Suc i \<Longrightarrow> P" 
551 
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

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

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

554 
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

555 
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

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

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

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

560 

63110  561 
lemma less_SucE: 
562 
assumes major: "m < Suc n" 

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

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

565 
shows P 

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

566 
apply (rule major [THEN lessE]) 
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

567 
apply (rule eq, blast) 
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

568 
apply (rule less, blast) 
13449  569 
done 
570 

63110  571 
lemma Suc_lessE: 
572 
assumes major: "Suc i < k" 

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

574 
shows P 

13449  575 
apply (rule major [THEN lessE]) 
576 
apply (erule lessI [THEN minor]) 

14208  577 
apply (erule Suc_lessD [THEN minor], assumption) 
13449  578 
done 
579 

63110  580 
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

581 
by simp 
13449  582 

583 
lemma less_trans_Suc: 

63110  584 
assumes le: "i < j" 
585 
shows "j < k \<Longrightarrow> Suc i < k" 

14208  586 
apply (induct k, simp_all) 
63110  587 
using le 
13449  588 
apply (simp add: less_Suc_eq) 
589 
apply (blast dest: Suc_lessD) 

590 
done 

591 

63110  592 
text \<open>Can be used with \<open>less_Suc_eq\<close> to get @{prop "n = m \<or> n < m"}\<close> 
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

593 
lemma not_less_eq: "\<not> m < n \<longleftrightarrow> n < Suc m" 
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

594 
unfolding not_less less_Suc_eq_le .. 
13449  595 

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

596 
lemma not_less_eq_eq: "\<not> m \<le> n \<longleftrightarrow> Suc n \<le> m" 
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

597 
unfolding not_le Suc_le_eq .. 
21243  598 

60758  599 
text \<open>Properties of "less than or equal"\<close> 
13449  600 

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

602 
unfolding less_Suc_eq_le . 
13449  603 

63110  604 
lemma Suc_n_not_le_n: "\<not> Suc n \<le> n" 
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

605 
unfolding not_le less_Suc_eq_le .. 
13449  606 

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

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

608 
by (simp add: less_Suc_eq_le [symmetric] less_Suc_eq) 
13449  609 

63110  610 
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

611 
by (drule le_Suc_eq [THEN iffD1], iprover+) 
13449  612 

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

614 
unfolding Suc_le_eq . 
13449  615 

61799  616 
text \<open>Stronger version of \<open>Suc_leD\<close>\<close> 
63110  617 
lemma Suc_le_lessD: "Suc m \<le> n \<Longrightarrow> m < n" 
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

618 
unfolding Suc_le_eq . 
13449  619 

63110  620 
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

621 
unfolding less_eq_Suc_le by (rule Suc_leD) 
13449  622 

61799  623 
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

624 
lemmas le_simps = less_imp_le_nat less_Suc_eq_le Suc_le_eq 
13449  625 

626 

63110  627 
text \<open>Equivalence of \<open>m \<le> n\<close> and \<open>m < n \<or> m = n\<close>\<close> 
628 

629 
lemma less_or_eq_imp_le: "m < n \<or> 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

630 
unfolding le_less . 
13449  631 

63110  632 
lemma le_eq_less_or_eq: "m \<le> n \<longleftrightarrow> m < n \<or> m = n" for m n :: nat 
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

633 
by (rule le_less) 
13449  634 

61799  635 
text \<open>Useful with \<open>blast\<close>.\<close> 
63110  636 
lemma eq_imp_le: "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

637 
by auto 
13449  638 

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

640 
by simp 
13449  641 

63110  642 
lemma le_trans: "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> i \<le> k" for i j k :: nat 
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

643 
by (rule order_trans) 
13449  644 

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

646 
by (rule antisym) 
13449  647 

63110  648 
lemma nat_less_le: "m < n \<longleftrightarrow> m \<le> n \<and> m \<noteq> n" for m n :: nat 
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

649 
by (rule less_le) 
13449  650 

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

652 
unfolding less_le .. 
13449  653 

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

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

656 

22718  657 
lemmas linorder_neqE_nat = linorder_neqE [where 'a = nat] 
15921  658 

63110  659 
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

660 
unfolding less_Suc_eq_le by auto 
13449  661 

63110  662 
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

663 
unfolding not_less by (rule le_less_Suc_eq) 
13449  664 

665 
lemmas not_less_simps = not_less_less_Suc_eq le_less_Suc_eq 

666 

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

669 

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

671 
by (cases n) simp_all 

672 

673 
lemma gr_implies_not0: "m < n \<Longrightarrow> n \<noteq> 0" for m n :: nat 

674 
by (cases n) simp_all 

675 

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

677 
by (cases n) simp_all 

25140  678 

61799  679 
text \<open>This theorem is useful with \<open>blast\<close>\<close> 
63110  680 
lemma gr0I: "(n = 0 \<Longrightarrow> False) \<Longrightarrow> 0 < n" for n :: nat 
681 
by (rule neq0_conv[THEN iffD1], iprover) 

682 

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

684 
by (fast intro: not0_implies_Suc) 

685 

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

687 
using neq0_conv by blast 

688 

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

690 
by (induct m') simp_all 

13449  691 

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

13449  695 

696 

60758  697 
subsubsection \<open>Monotonicity of Addition\<close> 
13449  698 

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

701 

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

703 
unfolding One_nat_def by (rule Suc_pred) 

704 

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

706 
by (induct k) simp_all 

707 

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

709 
by (induct k) simp_all 

710 

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

712 
by (auto dest: gr0_implies_Suc) 

13449  713 

60758  714 
text \<open>strict, in 1st argument\<close> 
63110  715 
lemma add_less_mono1: "i < j \<Longrightarrow> i + k < j + k" for i j k :: nat 
716 
by (induct k) simp_all 

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

717 

60758  718 
text \<open>strict, in both arguments\<close> 
63110  719 
lemma add_less_mono: "i < j \<Longrightarrow> k < l \<Longrightarrow> i + k < j + l" for i j k l :: nat 
14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset

720 
apply (rule add_less_mono1 [THEN less_trans], assumption+) 
15251  721 
apply (induct j, simp_all) 
14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset

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

723 

61799  724 
text \<open>Deleted \<open>less_natE\<close>; use \<open>less_imp_Suc_add RS exE\<close>\<close> 
63110  725 
lemma less_imp_Suc_add: "m < n \<Longrightarrow> \<exists>k. n = Suc (m + k)" 
14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset

726 
apply (induct n) 
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset

727 
apply (simp_all add: order_le_less) 
22718  728 
apply (blast elim!: less_SucE 
35047
1b2bae06c796
hide fact Nat.add_0_right; make add_0_right from Groups priority
haftmann
parents:
35028
diff
changeset

729 
intro!: Nat.add_0_right [symmetric] add_Suc_right [symmetric]) 
14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset

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

731 

63110  732 
lemma le_Suc_ex: "k \<le> l \<Longrightarrow> (\<exists>n. l = k + n)" for k l :: nat 
56194  733 
by (auto simp: less_Suc_eq_le[symmetric] dest: less_imp_Suc_add) 
734 

61799  735 
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

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

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

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

739 
shows "k * i < k * j" 
63110  740 
using \<open>0 < k\<close> 
741 
proof (induct k) 

742 
case 0 

743 
then show ?case by simp 

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

744 
next 
63110  745 
case (Suc k) 
746 
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

747 
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

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

749 

60758  750 
text \<open>Addition is the inverse of subtraction: 
751 
if @{term "n \<le> m"} then @{term "n + (m  n) = m"}.\<close> 

63110  752 
lemma add_diff_inverse_nat: "\<not> m < n \<Longrightarrow> n + (m  n) = m" for m n :: nat 
753 
by (induct m n rule: diff_induct) simp_all 

754 

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

756 
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

757 

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

758 
text\<open>The naturals form an ordered \<open>semidom\<close> and a \<open>dioid\<close>\<close> 
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

759 

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

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

761 
proof 
63110  762 
fix m n q :: nat 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14341
diff
changeset

763 
show "0 < (1::nat)" by simp 
63110  764 
show "m \<le> n \<Longrightarrow> q + m \<le> q + n" by simp 
765 
show "m < n \<Longrightarrow> 0 < q \<Longrightarrow> q * m < q * n" by (simp add: mult_less_mono2) 

766 
show "m \<noteq> 0 \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> m * n \<noteq> 0" by simp 

767 
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

768 
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

769 
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

770 

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

771 
instance nat :: dioid 
63110  772 
by standard (rule nat_le_iff_add) 
62378
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62376
diff
changeset

773 
declare le0[simp del]  \<open>This is now @{thm zero_le}\<close> 
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62376
diff
changeset

774 
declare le_0_eq[simp del]  \<open>This is now @{thm le_zero_eq}\<close> 
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62376
diff
changeset

775 
declare not_less0[simp del]  \<open>This is now @{thm not_less_zero}\<close> 
85ed00c1fe7c
generalize more theorems to support enat and ennreal
hoelzl
parents:
62376
diff
changeset

776 
declare not_gr0[simp del]  \<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

777 

63110  778 
instance nat :: ordered_cancel_comm_monoid_add .. 
779 
instance nat :: ordered_cancel_comm_monoid_diff .. 

780 

44817  781 

60758  782 
subsubsection \<open>@{term min} and @{term max}\<close> 
44817  783 

784 
lemma mono_Suc: "mono Suc" 

63110  785 
by (rule monoI) simp 
786 

787 
lemma min_0L [simp]: "min 0 n = 0" for n :: nat 

788 
by (rule min_absorb1) simp 

789 

790 
lemma min_0R [simp]: "min n 0 = 0" for n :: nat 

791 
by (rule min_absorb2) simp 

44817  792 

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

63110  794 
by (simp add: mono_Suc min_of_mono) 
795 

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

797 
by (simp split: nat.split) 

798 

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

800 
by (simp split: nat.split) 

801 

802 
lemma max_0L [simp]: "max 0 n = n" for n :: nat 

803 
by (rule max_absorb2) simp 

804 

805 
lemma max_0R [simp]: "max n 0 = n" for n :: nat 

806 
by (rule max_absorb1) simp 

807 

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

809 
by (simp add: mono_Suc max_of_mono) 

810 

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

812 
by (simp split: nat.split) 

813 

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

815 
by (simp split: nat.split) 

816 

817 
lemma nat_mult_min_left: "min m n * q = min (m * q) (n * q)" for m n q :: nat 

818 
by (simp add: min_def not_le) 

819 
(auto dest: mult_right_le_imp_le mult_right_less_imp_less le_less_trans) 

820 

821 
lemma nat_mult_min_right: "m * min n q = min (m * n) (m * q)" for m n q :: nat 

822 
by (simp add: min_def not_le) 

823 
(auto dest: mult_left_le_imp_le mult_left_less_imp_less le_less_trans) 

824 

825 
lemma nat_add_max_left: "max m n + q = max (m + q) (n + q)" for m n q :: nat 

44817  826 
by (simp add: max_def) 
827 

63110  828 
lemma nat_add_max_right: "m + max n q = max (m + n) (m + q)" for m n q :: nat 
44817  829 
by (simp add: max_def) 
830 

63110  831 
lemma nat_mult_max_left: "max m n * q = max (m * q) (n * q)" for m n q :: nat 
832 
by (simp add: max_def not_le) 

833 
(auto dest: mult_right_le_imp_le mult_right_less_imp_less le_less_trans) 

834 

835 
lemma nat_mult_max_right: "m * max n q = max (m * n) (m * q)" for m n q :: nat 

836 
by (simp add: max_def not_le) 

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

838 

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

839 

60758  840 
subsubsection \<open>Additional theorems about @{term "op \<le>"}\<close> 
841 

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

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

843 

63110  844 
instance nat :: wellorder 
845 
proof 

27823  846 
fix P and n :: nat 
63110  847 
assume step: "(\<And>m. m < n \<Longrightarrow> P m) \<Longrightarrow> P n" for n :: nat 
27823  848 
have "\<And>q. q \<le> n \<Longrightarrow> P q" 
849 
proof (induct n) 

850 
case (0 n) 

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

851 
have "P 0" by (rule step) auto 
63110  852 
then show ?case using 0 by auto 
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset

853 
next 
27823  854 
case (Suc m n) 
855 
then have "n \<le> m \<or> n = Suc m" by (simp add: le_Suc_eq) 

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

857 
proof 
63110  858 
assume "n \<le> m" 
859 
then show "P n" by (rule Suc(1)) 

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

860 
next 
27823  861 
assume n: "n = Suc m" 
63110  862 
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

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

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

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

867 

57015  868 

63110  869 
lemma Least_eq_0[simp]: "P 0 \<Longrightarrow> Least P = 0" for P :: "nat \<Rightarrow> bool" 
870 
by (rule Least_equality[OF _ le0]) 

871 

872 
lemma Least_Suc: "P n \<Longrightarrow> \<not> P 0 \<Longrightarrow> (LEAST n. P n) = Suc (LEAST m. P (Suc m))" 

47988  873 
apply (cases n, auto) 
27823  874 
apply (frule LeastI) 
63110  875 
apply (drule_tac P = "\<lambda>x. P (Suc x) " in LeastI) 
27823  876 
apply (subgoal_tac " (LEAST x. P x) \<le> Suc (LEAST x. P (Suc x))") 
877 
apply (erule_tac [2] Least_le) 

47988  878 
apply (cases "LEAST x. P x", auto) 
63110  879 
apply (drule_tac P = "\<lambda>x. P (Suc x) " in Least_le) 
27823  880 
apply (blast intro: order_antisym) 
881 
done 

882 

63110  883 
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)" 
27823  884 
apply (erule (1) Least_Suc [THEN ssubst]) 
885 
apply simp 

886 
done 

887 

63110  888 
lemma ex_least_nat_le: "\<not> P 0 \<Longrightarrow> P n \<Longrightarrow> \<exists>k\<le>n. (\<forall>i<k. \<not> P i) \<and> P k" for P :: "nat \<Rightarrow> bool" 
27823  889 
apply (cases n) 
890 
apply blast 

63110  891 
apply (rule_tac x="LEAST k. P k" in exI) 
27823  892 
apply (blast intro: Least_le dest: not_less_Least intro: LeastI_ex) 
893 
done 

894 

63110  895 
lemma ex_least_nat_less: "\<not> P 0 \<Longrightarrow> P n \<Longrightarrow> \<exists>k<n. (\<forall>i\<le>k. \<not> P i) \<and> P (k + 1)" for P :: "nat \<Rightarrow> bool" 
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

896 
unfolding One_nat_def 
27823  897 
apply (cases n) 
898 
apply blast 

899 
apply (frule (1) ex_least_nat_le) 

900 
apply (erule exE) 

901 
apply (case_tac k) 

902 
apply simp 

903 
apply (rename_tac k1) 

904 
apply (rule_tac x=k1 in exI) 

905 
apply (auto simp add: less_eq_Suc_le) 

906 
done 

907 

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

908 
lemma nat_less_induct: 
63110  909 
fixes P :: "nat \<Rightarrow> bool" 
910 
assumes "\<And>n. \<forall>m. m < n \<longrightarrow> P m \<Longrightarrow> P n" 

911 
shows "P n" 

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

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

913 

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

914 
lemma measure_induct_rule [case_names less]: 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset

915 
fixes f :: "'a \<Rightarrow> nat" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset

916 
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

917 
shows "P a" 
63110  918 
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

919 

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

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

922 
fixes f :: "'a \<Rightarrow> nat" 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset

923 
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

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

925 

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

926 
lemma full_nat_induct: 
63110  927 
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

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

929 
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

930 

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

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

19870  936 
shows "P i j" 
937 
proof  

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

22718  940 
have "P i (Suc (i + k))" 
19870  941 
proof (induct k) 
22718  942 
case 0 
943 
show ?case by (simp add: step) 

19870  944 
next 
945 
case (Suc k) 

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

19870  950 
qed 
63110  951 
then show "P i j" by (simp add: j) 
19870  952 
qed 
953 

60758  954 
text \<open>The method of infinite descent, frequently used in number theory. 
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset

955 
Provided by Roelof Oosterhuis. 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset

956 
$P(n)$ is true for all $n\in\mathbb{N}$ if 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset

957 
\begin{itemize} 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset

958 
\item case ``0'': given $n=0$ prove $P(n)$, 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset

959 
\item case ``smaller'': given $n>0$ and $\neg P(n)$ prove there exists 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset

960 
a smaller integer $m$ such that $\neg P(m)$. 
60758  961 
\end{itemize}\<close> 
962 

963 
text\<open>A compact version without explicit base case:\<close> 

63110  964 
lemma infinite_descent: "(\<And>n. \<not> P n \<Longrightarrow> \<exists>m<n. \<not> P m) \<Longrightarrow> P n" for P :: "nat \<Rightarrow> bool" 
965 
by (induct n rule: less_induct) auto 

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

966 

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

967 
lemma infinite_descent0[case_names 0 smaller]: 
63110  968 
fixes P :: "nat \<Rightarrow> bool" 
969 
assumes "P 0" and "\<And>n. n > 0 \<Longrightarrow> \<not> P n \<Longrightarrow> (\<exists>m. m < n \<and> \<not> P m)" 

970 
shows "P n" 

971 
apply (rule infinite_descent) 

972 
using assms 

973 
apply (case_tac "n > 0") 

974 
apply auto 

975 
done 

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

976 

60758  977 
text \<open> 
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset

978 
Infinite descent using a mapping to $\mathbb{N}$: 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset

979 
$P(x)$ is true for all $x\in D$ if there exists a $V: D \to \mathbb{N}$ and 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset

980 
\begin{itemize} 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset

981 
\item case ``0'': given $V(x)=0$ prove $P(x)$, 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset

982 
\item case ``smaller'': given $V(x)>0$ and $\neg P(x)$ prove there exists a $y \in D$ such that $V(y)<V(x)$ and $~\neg P(y)$. 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset

983 
\end{itemize} 
60758  984 
NB: the proof also shows how to use the previous lemma.\<close> 
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset

985 

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

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

989 
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

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

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

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

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

994 
proof (induct n rule: infinite_descent0) 
63110  995 
case 0 
996 
with 1 show "P x" by auto 

997 
next 

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

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

1001 
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

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

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

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

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

1006 

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

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

1011 
shows "P x" 

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

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

1013 
from assms obtain n where "n = V x" by auto 
63110  1014 
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

1015 
proof (induct n rule: infinite_descent, auto) 
63110  1016 
fix x 
1017 
assume "\<not> P x" 

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

1018 
with assms show "\<exists>m < V x. \<exists>y. V y = m \<and> \<not> P y" by auto 
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset

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

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

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

1022 

63110  1023 
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

1024 
lemma less_mono_imp_le_mono: 
63110  1025 
fixes f :: "nat \<Rightarrow> nat" 
1026 
and i j :: nat 

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

1028 
and "i \<le> j" 

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

1030 
using assms by (auto simp add: order_le_less) 

24438  1031 

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

1032 

60758  1033 
text \<open>nonstrict, in 1st argument\<close> 
63110  1034 
lemma add_le_mono1: "i \<le> j \<Longrightarrow> i + k \<le> j + k" for i j k :: nat 
1035 
by (rule add_right_mono) 

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

1036 

60758  1037 
text \<open>nonstrict, in both arguments\<close> 
63110  1038 
lemma add_le_mono: "i \<le> j \<Longrightarrow> k \<le> l \<Longrightarrow> i + k \<le> j + l" for i j k l :: nat 
1039 
by (rule add_mono) 

1040 

1041 
lemma le_add2: "n \<le> m + n" for m n :: nat 

62608  1042 
by simp 
13449  1043 

63110  1044 
lemma le_add1: "n \<le> n + m" for m n :: nat 
62608  1045 
by simp 
13449  1046 

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

63110  1048 
by (rule le_less_trans, rule le_add1, rule lessI) 
13449  1049 

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

63110  1051 
by (rule le_less_trans, rule le_add2, rule lessI) 
1052 

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

1054 
by (iprover intro!: less_add_Suc1 less_imp_Suc_add) 

1055 

1056 
lemma trans_le_add1: "i \<le> j \<Longrightarrow> i \<le> j + m" for i j m :: nat 

1057 
by (rule le_trans, assumption, rule le_add1) 

1058 

1059 
lemma trans_le_add2: "i \<le> j \<Longrightarrow> i \<le> m + j" for i j m :: nat 

1060 
by (rule le_trans, assumption, rule le_add2) 

1061 

1062 
lemma trans_less_add1: "i < j \<Longrightarrow> i < j + m" for i j m :: nat 

1063 
by (rule less_le_trans, assumption, rule le_add1) 

1064 

1065 
lemma trans_less_add2: "i < j \<Longrightarrow> i < m + j" for i j m :: nat 

1066 
by (rule less_le_trans, assumption, rule le_add2) 

1067 

1068 
lemma add_lessD1: "i + j < k \<Longrightarrow> i < k" for i j k :: nat 

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

1070 

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

1072 
apply (rule notI) 

1073 
apply (drule add_lessD1) 

1074 
apply (erule less_irrefl [THEN notE]) 

1075 
done 

1076 

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

1078 
by (simp add: add.commute) 

1079 

1080 
lemma add_leD1: "m + k \<le> n \<Longrightarrow> m \<le> n" for k m n :: nat 

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

1082 

1083 
lemma add_leD2: "m + k \<le> n \<Longrightarrow> k \<le> n" for k m n :: nat 

1084 
apply (simp add: add.commute) 

1085 
apply (erule add_leD1) 

1086 
done 

1087 

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

1089 
by (blast dest: add_leD1 add_leD2) 

1090 

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

1092 
lemma less_add_eq_less: "\<And>k::nat. k < l \<Longrightarrow> m + l = k + n \<Longrightarrow> m < n" 

1093 
by (force simp del: add_Suc_right simp add: less_iff_Suc_add add_Suc_right [symmetric] ac_simps) 

13449  1094 

1095 

60758  1096 
subsubsection \<open>More results about difference\<close> 
13449  1097 

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

13449  1100 

1101 
lemma diff_less_Suc: "m  n < Suc m" 

24438  1102 
apply (induct m n rule: diff_induct) 
1103 
apply (erule_tac [3] less_SucE) 

1104 
apply (simp_all add: less_Suc_eq) 

1105 
done 

13449  1106 

63110  1107 
lemma diff_le_self [simp]: "m  n \<le> m" for m n :: nat 
1108 
by (induct m n rule: diff_induct) (simp_all add: le_SucI) 

1109 

1110 
lemma less_imp_diff_less: "j < k \<Longrightarrow> j  n < k" for j k n :: nat 

1111 
by (rule le_less_trans, rule diff_le_self) 

1112 

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

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

1115 

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

1117 
by (induct j k rule: diff_induct) simp_all 

1118 

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

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

1120 
by (fact diff_add_assoc [symmetric]) 
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset

1121 

63110  1122 
lemma diff_add_assoc2: "k \<le> j \<Longrightarrow> (j + i)  k = (j  k) + i" for i j k :: nat 
62481
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset

1123 
by (simp add: ac_simps) 
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset

1124 

63110  1125 
lemma add_diff_assoc2 [simp]: "k \<le> j \<Longrightarrow> j  k + i = j + i  k" for i j k :: nat 
62481
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset

1126 
by (fact diff_add_assoc2 [symmetric]) 
13449  1127 

63110  1128 
lemma le_imp_diff_is_add: "i \<le> j \<Longrightarrow> (j  i = k) = (j = k + i)" for i j k :: nat 
1129 
by auto 

1130 

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

1132 
by (induct m n rule: diff_induct) simp_all 

1133 

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

1135 
by (rule iffD2, rule diff_is_0_eq) 

1136 

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

1138 
by (induct m n rule: diff_induct) simp_all 

13449  1139 

22718  1140 
lemma less_imp_add_positive: 
1141 
assumes "i < j" 

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

1147 

60758  1148 
text \<open>a nice rewrite for bounded subtraction\<close> 
63110  1149 
lemma nat_minus_add_max: "n  m + m = max n m" for m n :: nat 
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

1150 
by (simp add: max_def not_le order_less_imp_le) 
13449  1151 

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

61799  1154 
\<comment> \<open>elimination of \<open>\<close> on \<open>nat\<close>\<close> 
62365  1155 
by (cases "a < b") 
1156 
(auto simp add: not_less le_less dest!: add_eq_self_zero [OF sym]) 

13449  1157 

63110  1158 
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))" 
1159 
for a b :: nat 

61799  1160 
\<comment> \<open>elimination of \<open>\<close> on \<open>nat\<close> in assumptions\<close> 
62365  1161 
by (auto split: nat_diff_split) 
13449  1162 

63110  1163 
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

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

1165 

63110  1166 
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

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

1168 

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

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

1171 

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

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

1174 

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

1175 
lemma diff_Suc_eq_diff_pred: "m  Suc n = (m  1)  n" 
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47208
diff
changeset

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

1177 

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

1178 
lemma Let_Suc [simp]: "Let (Suc n) f == f (Suc n)" 
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47208
diff
changeset

1179 
by (fact Let_def) 
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47208
diff
changeset

1180 

13449  1181 

60758  1182 
subsubsection \<open>Monotonicity of multiplication\<close> 
13449  1183 

63110  1184 
lemma mult_le_mono1: "i \<le> j \<Longrightarrow> i * k \<le> j * k" for i j k :: nat 
1185 
by (simp add: mult_right_mono) 

1186 

1187 
lemma mult_le_mono2: "i \<le> j \<Longrightarrow> k * i \<le> k * j" for i j k :: nat 

1188 
by (simp add: mult_left_mono) 

13449  1189 

61799  1190 
text \<open>\<open>\<le>\<close> monotonicity, BOTH arguments\<close> 
63110  1191 
lemma mult_le_mono: "i \<le> j \<Longrightarrow> k \<le> l \<Longrightarrow> i * k \<le> j * l" for i j k l :: nat 
1192 
by (simp add: mult_mono) 

1193 

1194 
lemma mult_less_mono1: "i < j \<Longrightarrow> 0 < k \<Longrightarrow> i * k < j * k" for i j k :: nat 

1195 
by (simp add: mult_strict_right_mono) 

13449  1196 

61799  1197 
text\<open>Differs from the standard \<open>zero_less_mult_iff\<close> in that 
60758  1198 
there are no negative numbers.\<close> 
63110  1199 
lemma nat_0_less_mult_iff [simp]: "0 < m * n \<longleftrightarrow> 0 < m \<and> 0 < n" for m n :: nat 
13449  1200 
apply (induct m) 
22718  1201 
apply simp 
1202 
apply (case_tac n) 

1203 
apply simp_all 

13449  1204 
done 
1205 

63110  1206 
lemma one_le_mult_iff [simp]: "Suc 0 \<le> m * n \<longleftrightarrow> Suc 0 \<le> m \<and> Suc 0 \<le> n" 
13449  1207 
apply (induct m) 
22718  1208 
apply simp 
1209 
apply (case_tac n) 

1210 
apply simp_all 

13449  1211 
done 
1212 

63110  1213 
lemma mult_less_cancel2 [simp]: "m * k < n * k \<longleftrightarrow> 0 < k \<and> m < n" for k m n :: nat 
13449  1214 
apply (safe intro!: mult_less_mono1) 
47988  1215 
apply (cases k, auto) 
63110  1216 
apply (simp add: linorder_not_le [symmetric]) 
13449  1217 
apply (blast intro: mult_le_mono1) 
1218 
done 

1219 

63110  1220 
lemma mult_less_cancel1 [simp]: "k * m < k * n \<longleftrightarrow> 0 < k \<and> m < n" for k m n :: nat 
1221 
by (simp add: mult.commute [of k]) 

1222 

1223 
lemma mult_le_cancel1 [simp]: "k * m \<le> k * n \<longleftrightarrow> (0 < k \<longrightarrow> m \<le> n)" for k m n :: nat 

1224 
by (simp add: linorder_not_less [symmetric], auto) 

1225 

1226 
lemma mult_le_cancel2 [simp]: "m * k \<le> n * k \<longleftrightarrow> (0 < k \<longrightarrow> m \<le> n)" for k m n :: nat 

1227 
by (simp add: linorder_not_less [symmetric], auto) 

1228 

1229 
lemma Suc_mult_less_cancel1: "Suc k * m < Suc k * n \<longleftrightarrow> m < n" 

1230 
by (subst mult_less_cancel1) simp 

1231 

1232 
lemma Suc_mult_le_cancel1: "Suc k * m \<le> Suc k * n \<longleftrightarrow> m \<le> n" 

1233 
by (subst mult_le_cancel1) simp 

1234 

1235 
lemma le_square: "m \<le> m * m" for m :: nat 

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

1236 
by (cases m) (auto intro: le_add1) 
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

1237 

63110  1238 
lemma le_cube: "m \<le> m * (m * m)" for m :: nat 
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset

1239 
by (cases m) (auto intro: le_add1) 
13449  1240 

61799  1241 
text \<open>Lemma for \<open>gcd\<close>\<close> 
63110  1242 
lemma mult_eq_self_implies_10: "m = m * n \<Longrightarrow> n = 1 \<or> m = 0" for m n :: nat 
13449  1243 
apply (drule sym) 
1244 
apply (rule disjCI) 

1245 
apply (rule nat_less_cases, erule_tac [2] _) 

25157  1246 
apply (drule_tac [2] mult_less_mono2) 
25162  1247 
apply (auto) 
13449  1248 
done 
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
7702
diff
changeset

1249 

51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51173
diff
changeset

1250 
lemma mono_times_nat: 
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51173
diff
changeset

1251 
fixes n :: nat 
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51173
diff
changeset

1252 
assumes "n > 0" 
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51173
diff
changeset

1253 
shows "mono (times n)" 
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51173
diff
changeset

1254 
proof 
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51173
diff
changeset

1255 
fix m q :: nat 
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51173
diff
changeset

1256 
assume "m \<le> q" 
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51173
diff
changeset

1257 
with assms show "n * m \<le> n * q" by simp 
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51173
diff
changeset

1258 
qed 
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51173
diff
changeset

1259 

60758  1260 
text \<open>the lattice order on @{typ nat}\<close> 
24995  1261 

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

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

1263 
begin 
24995  1264 

63110  1265 
definition "(inf :: nat \<Rightarrow> nat \<Rightarrow> nat) = min" 
1266 

1267 
definition "(sup :: nat \<Rightarrow> nat \<Rightarrow> nat) = max" 

1268 

1269 
instance 

1270 
by intro_classes 

1271 
(auto simp add: inf_nat_def sup_nat_def max_def not_le min_def 

1272 
intro: order_less_imp_le antisym elim!: order_trans order_less_trans) 

24995  1273 

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

1274 
end 
24995  1275 

1276 

60758  1277 
subsection \<open>Natural operation of natural numbers on functions\<close> 
1278 

1279 
text \<open> 

30971  1280 
We use the same logical constant for the power operations on 
1281 
functions and relations, in order to share the same syntax. 

60758  1282 
\<close> 
30971  1283 

45965
2af982715e5c
generalized type signature to permit overloading on `set`
haftmann
parents:
45933
diff
changeset

1284 
consts compow :: "nat \<Rightarrow> 'a \<Rightarrow> 'a" 
30971  1285 

63110  1286 
abbreviation compower :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixr "^^" 80) 
1287 
where "f ^^ n \<equiv> compow n f" 

30971  1288 

1289 
notation (latex output) 

1290 
compower ("(_\<^bsup>_\<^esup>)" [1000] 1000) 

1291 

61799  1292 
text \<open>\<open>f ^^ n = f o ... o f\<close>, the nfold composition of \<open>f\<close>\<close> 
30971  1293 

1294 
overloading 

63110  1295 
funpow \<equiv> "compow :: nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a)" 
30971  1296 
begin 
30954
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30686
diff
changeset

1297 

55575
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55534
diff
changeset

1298 
primrec funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where 
44325  1299 
"funpow 0 f = id" 
1300 
 "funpow (Suc n) f = f o funpow n f" 

30954
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30686
diff
