author | wenzelm |
Tue, 31 May 2016 19:51:01 +0200 | |
changeset 63197 | af562e976038 |
parent 63145 | 703edebd1d92 |
child 63561 | fba08009ff3e |
permissions | -rw-r--r-- |
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 |
|
57952 | 14 |
named_theorems arith "arith facts -- only ground formulas" |
48891 | 15 |
ML_file "Tools/arith_data.ML" |
16 |
||
17 |
||
61799 | 18 |
subsection \<open>Type \<open>ind\<close>\<close> |
13449 | 19 |
|
20 |
typedecl ind |
|
21 |
||
63110 | 22 |
axiomatization Zero_Rep :: ind and Suc_Rep :: "ind \<Rightarrow> ind" |
23 |
\<comment> \<open>The axiom of infinity in 2 parts:\<close> |
|
24 |
where Suc_Rep_inject: "Suc_Rep x = Suc_Rep y \<Longrightarrow> x = y" |
|
25 |
and Suc_Rep_not_Zero_Rep: "Suc_Rep x \<noteq> Zero_Rep" |
|
19573 | 26 |
|
60758 | 27 |
subsection \<open>Type nat\<close> |
28 |
||
29 |
text \<open>Type definition\<close> |
|
13449 | 30 |
|
44325 | 31 |
inductive Nat :: "ind \<Rightarrow> bool" where |
32 |
Zero_RepI: "Nat Zero_Rep" |
|
33 |
| Suc_RepI: "Nat i \<Longrightarrow> Nat (Suc_Rep i)" |
|
13449 | 34 |
|
49834 | 35 |
typedef nat = "{n. Nat n}" |
45696 | 36 |
morphisms Rep_Nat Abs_Nat |
44278
1220ecb81e8f
observe distinction between sets and predicates more properly
haftmann
parents:
43595
diff
changeset
|
37 |
using Nat.Zero_RepI by auto |
1220ecb81e8f
observe distinction between sets and predicates more properly
haftmann
parents:
43595
diff
changeset
|
38 |
|
1220ecb81e8f
observe distinction between sets and predicates more properly
haftmann
parents:
43595
diff
changeset
|
39 |
lemma Nat_Rep_Nat: |
1220ecb81e8f
observe distinction between sets and predicates more properly
haftmann
parents:
43595
diff
changeset
|
40 |
"Nat (Rep_Nat n)" |
1220ecb81e8f
observe distinction between sets and predicates more properly
haftmann
parents:
43595
diff
changeset
|
41 |
using Rep_Nat by simp |
13449 | 42 |
|
44278
1220ecb81e8f
observe distinction between sets and predicates more properly
haftmann
parents:
43595
diff
changeset
|
43 |
lemma Nat_Abs_Nat_inverse: |
1220ecb81e8f
observe distinction between sets and predicates more properly
haftmann
parents:
43595
diff
changeset
|
44 |
"Nat n \<Longrightarrow> Rep_Nat (Abs_Nat n) = n" |
1220ecb81e8f
observe distinction between sets and predicates more properly
haftmann
parents:
43595
diff
changeset
|
45 |
using Abs_Nat_inverse by simp |
1220ecb81e8f
observe distinction between sets and predicates more properly
haftmann
parents:
43595
diff
changeset
|
46 |
|
1220ecb81e8f
observe distinction between sets and predicates more properly
haftmann
parents:
43595
diff
changeset
|
47 |
lemma Nat_Abs_Nat_inject: |
1220ecb81e8f
observe distinction between sets and predicates more properly
haftmann
parents:
43595
diff
changeset
|
48 |
"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
|
49 |
using Abs_Nat_inject by simp |
13449 | 50 |
|
25510 | 51 |
instantiation nat :: zero |
52 |
begin |
|
53 |
||
37767 | 54 |
definition Zero_nat_def: |
25510 | 55 |
"0 = Abs_Nat Zero_Rep" |
56 |
||
57 |
instance .. |
|
58 |
||
59 |
end |
|
24995 | 60 |
|
44278
1220ecb81e8f
observe distinction between sets and predicates more properly
haftmann
parents:
43595
diff
changeset
|
61 |
definition Suc :: "nat \<Rightarrow> nat" where |
1220ecb81e8f
observe distinction between sets and predicates more properly
haftmann
parents:
43595
diff
changeset
|
62 |
"Suc n = Abs_Nat (Suc_Rep (Rep_Nat n))" |
1220ecb81e8f
observe distinction between sets and predicates more properly
haftmann
parents:
43595
diff
changeset
|
63 |
|
27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
26748
diff
changeset
|
64 |
lemma Suc_not_Zero: "Suc m \<noteq> 0" |
44278
1220ecb81e8f
observe distinction between sets and predicates more properly
haftmann
parents:
43595
diff
changeset
|
65 |
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 | 66 |
|
27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
26748
diff
changeset
|
67 |
lemma Zero_not_Suc: "0 \<noteq> Suc m" |
13449 | 68 |
by (rule not_sym, rule Suc_not_Zero not_sym) |
69 |
||
34208
a7acd6c68d9b
more regular axiom of infinity, with no (indirect) reference to overloaded constants
krauss
parents:
33657
diff
changeset
|
70 |
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
|
71 |
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
|
72 |
|
55417
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
55415
diff
changeset
|
73 |
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
|
74 |
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
|
75 |
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
|
76 |
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
|
77 |
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
|
78 |
apply (unfold Zero_nat_def Suc_def) |
61799 | 79 |
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
|
80 |
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
|
81 |
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
|
82 |
done |
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
55415
diff
changeset
|
83 |
|
55469
b19dd108f0c2
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
blanchet
parents:
55468
diff
changeset
|
84 |
free_constructors case_nat for |
61076 | 85 |
"0 :: nat" |
55469
b19dd108f0c2
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
blanchet
parents:
55468
diff
changeset
|
86 |
| Suc pred |
57200
aab87ffa60cc
use 'where' clause for selector default value syntax
blanchet
parents:
57091
diff
changeset
|
87 |
where |
61076 | 88 |
"pred (0 :: nat) = (0 :: nat)" |
58189
9d714be4f028
added 'plugins' option to control which hooks are enabled
blanchet
parents:
57983
diff
changeset
|
89 |
apply atomize_elim |
9d714be4f028
added 'plugins' option to control which hooks are enabled
blanchet
parents:
57983
diff
changeset
|
90 |
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
|
91 |
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
|
92 |
Rep_Nat_inject) |
9d714be4f028
added 'plugins' option to control which hooks are enabled
blanchet
parents:
57983
diff
changeset
|
93 |
apply (simp only: Suc_not_Zero) |
9d714be4f028
added 'plugins' option to control which hooks are enabled
blanchet
parents:
57983
diff
changeset
|
94 |
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
|
95 |
|
61799 | 96 |
\<comment> \<open>Avoid name clashes by prefixing the output of \<open>old_rep_datatype\<close> with \<open>old\<close>.\<close> |
60758 | 97 |
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
|
98 |
|
61076 | 99 |
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
|
100 |
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
|
101 |
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
|
102 |
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
|
103 |
done |
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
55415
diff
changeset
|
104 |
|
60758 | 105 |
setup \<open>Sign.parent_path\<close> |
106 |
||
61799 | 107 |
\<comment> \<open>But erase the prefix for properties that are not generated by \<open>free_constructors\<close>.\<close> |
60758 | 108 |
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
|
109 |
|
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
55415
diff
changeset
|
110 |
declare |
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
55415
diff
changeset
|
111 |
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
|
112 |
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
|
113 |
|
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
55415
diff
changeset
|
114 |
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
|
115 |
lemmas inducts = old.nat.inducts |
55642
63beb38e9258
adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
blanchet
parents:
55575
diff
changeset
|
116 |
lemmas rec = old.nat.rec |
63beb38e9258
adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
blanchet
parents:
55575
diff
changeset
|
117 |
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
|
118 |
|
60758 | 119 |
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
|
120 |
|
63110 | 121 |
abbreviation rec_nat :: "'a \<Rightarrow> (nat \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a" |
122 |
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
|
123 |
|
55424
9ab4129a76a3
remove hidden fact about hidden constant from code generator setup
blanchet
parents:
55423
diff
changeset
|
124 |
declare nat.sel[code del] |
9ab4129a76a3
remove hidden fact about hidden constant from code generator setup
blanchet
parents:
55423
diff
changeset
|
125 |
|
61799 | 126 |
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
|
127 |
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
|
128 |
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
|
129 |
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
|
130 |
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
|
131 |
nat.sel |
57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57952
diff
changeset
|
132 |
nat.exhaust_sel |
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57952
diff
changeset
|
133 |
nat.split_sel |
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57952
diff
changeset
|
134 |
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
|
135 |
|
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
55415
diff
changeset
|
136 |
lemma nat_exhaust [case_names 0 Suc, cases type: nat]: |
61799 | 137 |
\<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
|
138 |
"(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
|
139 |
by (rule old.nat.exhaust) |
13449 | 140 |
|
27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
26748
diff
changeset
|
141 |
lemma nat_induct [case_names 0 Suc, induct type: nat]: |
61799 | 142 |
\<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
|
143 |
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
|
144 |
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
|
145 |
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
|
146 |
using assms by (rule nat.induct) |
13449 | 147 |
|
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 |
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
|
149 |
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
|
150 |
nat_induct0 |
24995 | 151 |
|
60758 | 152 |
ML \<open> |
58389 | 153 |
val nat_basic_lfp_sugar = |
154 |
let |
|
155 |
val ctr_sugar = the (Ctr_Sugar.ctr_sugar_of_global @{theory} @{type_name nat}); |
|
156 |
val recx = Logic.varify_types_global @{term rec_nat}; |
|
157 |
val C = body_type (fastype_of recx); |
|
158 |
in |
|
159 |
{T = HOLogic.natT, fp_res_index = 0, C = C, fun_arg_Tsss = [[], [[HOLogic.natT, C]]], |
|
160 |
ctr_sugar = ctr_sugar, recx = recx, rec_thms = @{thms nat.rec}} |
|
161 |
end; |
|
60758 | 162 |
\<close> |
163 |
||
164 |
setup \<open> |
|
58389 | 165 |
let |
166 |
fun basic_lfp_sugars_of _ [@{typ nat}] _ _ ctxt = |
|
62326
3cf7a067599c
allow predicator instead of map function in 'primrec'
blanchet
parents:
62217
diff
changeset
|
167 |
([], [0], [nat_basic_lfp_sugar], [], [], [], TrueI (*dummy*), [], false, ctxt) |
58389 | 168 |
| basic_lfp_sugars_of bs arg_Ts callers callssss ctxt = |
169 |
BNF_LFP_Rec_Sugar.default_basic_lfp_sugars_of bs arg_Ts callers callssss ctxt; |
|
170 |
in |
|
171 |
BNF_LFP_Rec_Sugar.register_lfp_rec_extension |
|
172 |
{nested_simps = [], is_new_datatype = K (K true), basic_lfp_sugars_of = basic_lfp_sugars_of, |
|
173 |
rewrite_nested_rec_call = NONE} |
|
174 |
end |
|
60758 | 175 |
\<close> |
176 |
||
177 |
text \<open>Injectiveness and distinctness lemmas\<close> |
|
24995 | 178 |
|
27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
26748
diff
changeset
|
179 |
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
|
180 |
by (simp add: inj_on_def) |
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
26748
diff
changeset
|
181 |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
182 |
lemma Suc_neq_Zero: "Suc m = 0 \<Longrightarrow> R" |
25162 | 183 |
by (rule notE, rule Suc_not_Zero) |
24995 | 184 |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
185 |
lemma Zero_neq_Suc: "0 = Suc m \<Longrightarrow> R" |
25162 | 186 |
by (rule Suc_neq_Zero, erule sym) |
24995 | 187 |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
188 |
lemma Suc_inject: "Suc x = Suc y \<Longrightarrow> x = y" |
25162 | 189 |
by (rule inj_Suc [THEN injD]) |
24995 | 190 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
191 |
lemma n_not_Suc_n: "n \<noteq> Suc n" |
25162 | 192 |
by (induct n) simp_all |
13449 | 193 |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
194 |
lemma Suc_n_not_n: "Suc n \<noteq> n" |
25162 | 195 |
by (rule not_sym, rule n_not_Suc_n) |
13449 | 196 |
|
60758 | 197 |
text \<open>A special form of induction for reasoning |
198 |
about @{term "m < n"} and @{term "m - n"}\<close> |
|
13449 | 199 |
|
63110 | 200 |
lemma diff_induct: |
201 |
assumes "\<And>x. P x 0" |
|
202 |
and "\<And>y. P 0 (Suc y)" |
|
203 |
and "\<And>x y. P x y \<Longrightarrow> P (Suc x) (Suc y)" |
|
204 |
shows "P m n" |
|
205 |
using assms |
|
14208 | 206 |
apply (rule_tac x = m in spec) |
15251 | 207 |
apply (induct n) |
13449 | 208 |
prefer 2 |
209 |
apply (rule allI) |
|
17589 | 210 |
apply (induct_tac x, iprover+) |
13449 | 211 |
done |
212 |
||
24995 | 213 |
|
60758 | 214 |
subsection \<open>Arithmetic operators\<close> |
24995 | 215 |
|
49388 | 216 |
instantiation nat :: comm_monoid_diff |
25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25563
diff
changeset
|
217 |
begin |
24995 | 218 |
|
55575
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55534
diff
changeset
|
219 |
primrec plus_nat where |
63110 | 220 |
add_0: "0 + n = (n::nat)" |
221 |
| add_Suc: "Suc m + n = Suc (m + n)" |
|
222 |
||
223 |
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
|
224 |
by (induct m) simp_all |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
225 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
226 |
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
|
227 |
by (induct m) simp_all |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
228 |
|
28514 | 229 |
declare add_0 [code] |
230 |
||
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
231 |
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
|
232 |
by simp |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
233 |
|
55575
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55534
diff
changeset
|
234 |
primrec minus_nat where |
61076 | 235 |
diff_0 [code]: "m - 0 = (m::nat)" |
63110 | 236 |
| diff_Suc: "m - Suc n = (case m - n of 0 \<Rightarrow> 0 | Suc k \<Rightarrow> k)" |
24995 | 237 |
|
28514 | 238 |
declare diff_Suc [simp del] |
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
239 |
|
63110 | 240 |
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
|
241 |
by (induct n) (simp_all add: diff_Suc) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
242 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
243 |
lemma diff_Suc_Suc [simp, code]: "Suc m - Suc n = m - n" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
244 |
by (induct n) (simp_all add: diff_Suc) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
245 |
|
63110 | 246 |
instance |
247 |
proof |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
248 |
fix n m q :: nat |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
249 |
show "(n + m) + q = n + (m + q)" by (induct n) simp_all |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
250 |
show "n + m = m + n" by (induct n) simp_all |
59815
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59582
diff
changeset
|
251 |
show "m + n - m = n" by (induct m) simp_all |
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59582
diff
changeset
|
252 |
show "n - m - q = n - (m + q)" by (induct q) (simp_all add: diff_Suc) |
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
253 |
show "0 + n = n" by simp |
49388 | 254 |
show "0 - n = 0" by simp |
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
255 |
qed |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
256 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
257 |
end |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
258 |
|
36176
3fe7e97ccca8
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
wenzelm
parents:
35828
diff
changeset
|
259 |
hide_fact (open) add_0 add_0_right diff_0 |
35047
1b2bae06c796
hide fact Nat.add_0_right; make add_0_right from Groups priority
haftmann
parents:
35028
diff
changeset
|
260 |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
261 |
instantiation nat :: comm_semiring_1_cancel |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
262 |
begin |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
263 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
264 |
definition |
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46351
diff
changeset
|
265 |
One_nat_def [simp]: "1 = Suc 0" |
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
266 |
|
55575
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55534
diff
changeset
|
267 |
primrec times_nat where |
61076 | 268 |
mult_0: "0 * n = (0::nat)" |
44325 | 269 |
| mult_Suc: "Suc m * n = n + (m * n)" |
25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25563
diff
changeset
|
270 |
|
63110 | 271 |
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
|
272 |
by (induct m) simp_all |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
273 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
274 |
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
|
275 |
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
|
276 |
|
63110 | 277 |
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
|
278 |
by (induct m) (simp_all add: add.assoc) |
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
279 |
|
63110 | 280 |
instance |
281 |
proof |
|
282 |
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
|
283 |
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
|
284 |
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
|
285 |
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
|
286 |
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
|
287 |
show "(n + m) * q = n * q + m * q" by (rule add_mult_distrib) |
63110 | 288 |
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
|
289 |
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
|
290 |
qed |
25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25563
diff
changeset
|
291 |
|
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25563
diff
changeset
|
292 |
end |
24995 | 293 |
|
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
|
294 |
|
60758 | 295 |
subsubsection \<open>Addition\<close> |
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
296 |
|
61799 | 297 |
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
|
298 |
|
63110 | 299 |
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
|
300 |
by (cases m) simp_all |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
301 |
|
63110 | 302 |
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
|
303 |
by (cases m) simp_all |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
304 |
|
63110 | 305 |
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
|
306 |
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
|
307 |
|
63110 | 308 |
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
|
309 |
by (induct m) simp_all |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
310 |
|
63110 | 311 |
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
|
312 |
apply (induct k) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
313 |
apply simp |
63110 | 314 |
apply (drule comp_inj_on[OF _ inj_Suc]) |
315 |
apply (simp add: o_def) |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
316 |
done |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
317 |
|
47208 | 318 |
lemma Suc_eq_plus1: "Suc n = n + 1" |
319 |
unfolding One_nat_def by simp |
|
320 |
||
321 |
lemma Suc_eq_plus1_left: "Suc n = 1 + n" |
|
322 |
unfolding One_nat_def by simp |
|
323 |
||
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
324 |
|
60758 | 325 |
subsubsection \<open>Difference\<close> |
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
326 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
327 |
lemma Suc_diff_diff [simp]: "(Suc m - n) - Suc k = m - n - k" |
62365 | 328 |
by (simp add: diff_diff_add) |
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
329 |
|
30093 | 330 |
lemma diff_Suc_1 [simp]: "Suc n - 1 = n" |
331 |
unfolding One_nat_def by simp |
|
332 |
||
60758 | 333 |
subsubsection \<open>Multiplication\<close> |
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
334 |
|
63110 | 335 |
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
|
336 |
by (induct m) auto |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
337 |
|
63110 | 338 |
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
|
339 |
apply (induct m) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
340 |
apply simp |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
341 |
apply (induct n) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
342 |
apply auto |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
343 |
done |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
344 |
|
63110 | 345 |
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
|
346 |
apply (rule trans) |
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
44848
diff
changeset
|
347 |
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
|
348 |
done |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
349 |
|
63110 | 350 |
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
|
351 |
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
|
352 |
|
63110 | 353 |
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
|
354 |
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
|
355 |
|
63110 | 356 |
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
|
357 |
proof - |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
358 |
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
|
359 |
proof (induct n arbitrary: m) |
63110 | 360 |
case 0 |
361 |
then show "m = 0" by simp |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
362 |
next |
63110 | 363 |
case (Suc n) |
364 |
then show "m = Suc n" |
|
365 |
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
|
366 |
qed |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
367 |
then show ?thesis by auto |
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 |
|
63110 | 370 |
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
|
371 |
by (simp add: mult.commute) |
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
372 |
|
63110 | 373 |
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
|
374 |
by (subst mult_cancel1) simp |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
375 |
|
24995 | 376 |
|
60758 | 377 |
subsection \<open>Orders on @{typ nat}\<close> |
378 |
||
379 |
subsubsection \<open>Operation definition\<close> |
|
24995 | 380 |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
381 |
instantiation nat :: linorder |
25510 | 382 |
begin |
383 |
||
55575
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55534
diff
changeset
|
384 |
primrec less_eq_nat where |
61076 | 385 |
"(0::nat) \<le> n \<longleftrightarrow> True" |
44325 | 386 |
| "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
|
387 |
|
28514 | 388 |
declare less_eq_nat.simps [simp del] |
63110 | 389 |
|
390 |
lemma le0 [iff]: "0 \<le> n" for n :: nat |
|
391 |
by (simp add: less_eq_nat.simps) |
|
392 |
||
393 |
lemma [code]: "0 \<le> n \<longleftrightarrow> True" for n :: nat |
|
394 |
by simp |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
395 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
396 |
definition less_nat where |
28514 | 397 |
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
|
398 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
399 |
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
|
400 |
by (simp add: less_eq_nat.simps(2)) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
401 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
402 |
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
|
403 |
unfolding less_eq_Suc_le .. |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
404 |
|
63110 | 405 |
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
|
406 |
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
|
407 |
|
63110 | 408 |
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
|
409 |
by (simp add: less_eq_Suc_le) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
410 |
|
63110 | 411 |
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
|
412 |
by simp |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
413 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
414 |
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
|
415 |
by (simp add: less_eq_Suc_le) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
416 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
417 |
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
|
418 |
by (simp add: less_eq_Suc_le) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
419 |
|
56194 | 420 |
lemma Suc_less_eq2: "Suc n < m \<longleftrightarrow> (\<exists>m'. m = Suc m' \<and> n < m')" |
421 |
by (cases m) auto |
|
422 |
||
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
423 |
lemma le_SucI: "m \<le> n \<Longrightarrow> m \<le> Suc n" |
63110 | 424 |
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
|
425 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
426 |
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
|
427 |
by (cases n) (auto intro: le_SucI) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
428 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
429 |
lemma less_SucI: "m < n \<Longrightarrow> m < Suc n" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
430 |
by (simp add: less_eq_Suc_le) (erule Suc_leD) |
24995 | 431 |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
432 |
lemma Suc_lessD: "Suc m < n \<Longrightarrow> m < n" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
433 |
by (simp add: less_eq_Suc_le) (erule Suc_leD) |
25510 | 434 |
|
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
|
435 |
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
|
436 |
proof |
63110 | 437 |
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
|
438 |
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
|
439 |
proof (induct n arbitrary: m) |
63110 | 440 |
case 0 |
441 |
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
|
442 |
next |
63110 | 443 |
case (Suc n) |
444 |
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
|
445 |
qed |
63110 | 446 |
show "n \<le> n" by (induct n) simp_all |
447 |
then show "n = m" if "n \<le> m" and "m \<le> n" |
|
448 |
using that by (induct n arbitrary: m) |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
449 |
(simp_all add: less_eq_nat.simps(2) split: nat.splits) |
63110 | 450 |
show "n \<le> q" if "n \<le> m" and "m \<le> q" |
451 |
using that |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
452 |
proof (induct n arbitrary: m q) |
63110 | 453 |
case 0 |
454 |
show ?case by simp |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
455 |
next |
63110 | 456 |
case (Suc n) |
457 |
then show ?case |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
458 |
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
|
459 |
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
|
460 |
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
|
461 |
qed |
63110 | 462 |
show "n \<le> m \<or> m \<le> n" |
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
463 |
by (induct n arbitrary: m) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
464 |
(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
|
465 |
qed |
25510 | 466 |
|
467 |
end |
|
13449 | 468 |
|
52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
52435
diff
changeset
|
469 |
instantiation nat :: order_bot |
29652 | 470 |
begin |
471 |
||
63110 | 472 |
definition bot_nat :: nat where "bot_nat = 0" |
473 |
||
474 |
instance by standard (simp add: bot_nat_def) |
|
29652 | 475 |
|
476 |
end |
|
477 |
||
51329
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51263
diff
changeset
|
478 |
instance nat :: no_top |
61169 | 479 |
by standard (auto intro: less_Suc_eq_le [THEN iffD2]) |
52289 | 480 |
|
51329
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51263
diff
changeset
|
481 |
|
60758 | 482 |
subsubsection \<open>Introduction properties\<close> |
13449 | 483 |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
484 |
lemma lessI [iff]: "n < Suc n" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
485 |
by (simp add: less_Suc_eq_le) |
13449 | 486 |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
487 |
lemma zero_less_Suc [iff]: "0 < Suc n" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
488 |
by (simp add: less_Suc_eq_le) |
13449 | 489 |
|
490 |
||
60758 | 491 |
subsubsection \<open>Elimination properties\<close> |
13449 | 492 |
|
63110 | 493 |
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
|
494 |
by (rule order_less_irrefl) |
13449 | 495 |
|
63110 | 496 |
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
|
497 |
by (rule not_sym) (rule less_imp_neq) |
13449 | 498 |
|
63110 | 499 |
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
|
500 |
by (rule less_imp_neq) |
13449 | 501 |
|
63110 | 502 |
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
|
503 |
by (rule notE, rule less_not_refl) |
13449 | 504 |
|
63110 | 505 |
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
|
506 |
by (rule notE) (rule not_less0) |
13449 | 507 |
|
63110 | 508 |
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
|
509 |
unfolding less_Suc_eq_le le_less .. |
13449 | 510 |
|
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
|
511 |
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
|
512 |
by (simp add: less_Suc_eq) |
13449 | 513 |
|
63110 | 514 |
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
|
515 |
unfolding One_nat_def by (rule less_Suc0) |
13449 | 516 |
|
63110 | 517 |
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
|
518 |
by simp |
13449 | 519 |
|
60758 | 520 |
text \<open>"Less than" is antisymmetric, sort of\<close> |
14302 | 521 |
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
|
522 |
unfolding not_less less_Suc_eq_le by (rule antisym) |
14302 | 523 |
|
63110 | 524 |
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
|
525 |
by (rule linorder_neq_iff) |
13449 | 526 |
|
527 |
||
60758 | 528 |
subsubsection \<open>Inductive (?) properties\<close> |
13449 | 529 |
|
63110 | 530 |
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
|
531 |
unfolding less_eq_Suc_le [of m] le_less by simp |
13449 | 532 |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
533 |
lemma lessE: |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
534 |
assumes major: "i < k" |
63110 | 535 |
and 1: "k = Suc i \<Longrightarrow> P" |
536 |
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
|
537 |
shows P |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
538 |
proof - |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
539 |
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
|
540 |
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
|
541 |
then have "(\<exists>j. i < j \<and> k = Suc j) \<or> k = Suc i" |
63110 | 542 |
by (auto simp add: less_le) |
543 |
with 1 2 show P by auto |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
544 |
qed |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
545 |
|
63110 | 546 |
lemma less_SucE: |
547 |
assumes major: "m < Suc n" |
|
548 |
and less: "m < n \<Longrightarrow> P" |
|
549 |
and eq: "m = n \<Longrightarrow> P" |
|
550 |
shows P |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
551 |
apply (rule major [THEN lessE]) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
552 |
apply (rule eq, blast) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
553 |
apply (rule less, blast) |
13449 | 554 |
done |
555 |
||
63110 | 556 |
lemma Suc_lessE: |
557 |
assumes major: "Suc i < k" |
|
558 |
and minor: "\<And>j. i < j \<Longrightarrow> k = Suc j \<Longrightarrow> P" |
|
559 |
shows P |
|
13449 | 560 |
apply (rule major [THEN lessE]) |
561 |
apply (erule lessI [THEN minor]) |
|
14208 | 562 |
apply (erule Suc_lessD [THEN minor], assumption) |
13449 | 563 |
done |
564 |
||
63110 | 565 |
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
|
566 |
by simp |
13449 | 567 |
|
568 |
lemma less_trans_Suc: |
|
63110 | 569 |
assumes le: "i < j" |
570 |
shows "j < k \<Longrightarrow> Suc i < k" |
|
14208 | 571 |
apply (induct k, simp_all) |
63110 | 572 |
using le |
13449 | 573 |
apply (simp add: less_Suc_eq) |
574 |
apply (blast dest: Suc_lessD) |
|
575 |
done |
|
576 |
||
63110 | 577 |
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
|
578 |
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
|
579 |
unfolding not_less less_Suc_eq_le .. |
13449 | 580 |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
581 |
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
|
582 |
unfolding not_le Suc_le_eq .. |
21243 | 583 |
|
60758 | 584 |
text \<open>Properties of "less than or equal"\<close> |
13449 | 585 |
|
63110 | 586 |
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
|
587 |
unfolding less_Suc_eq_le . |
13449 | 588 |
|
63110 | 589 |
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
|
590 |
unfolding not_le less_Suc_eq_le .. |
13449 | 591 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
592 |
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
|
593 |
by (simp add: less_Suc_eq_le [symmetric] less_Suc_eq) |
13449 | 594 |
|
63110 | 595 |
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
|
596 |
by (drule le_Suc_eq [THEN iffD1], iprover+) |
13449 | 597 |
|
63110 | 598 |
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
|
599 |
unfolding Suc_le_eq . |
13449 | 600 |
|
61799 | 601 |
text \<open>Stronger version of \<open>Suc_leD\<close>\<close> |
63110 | 602 |
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
|
603 |
unfolding Suc_le_eq . |
13449 | 604 |
|
63110 | 605 |
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
|
606 |
unfolding less_eq_Suc_le by (rule Suc_leD) |
13449 | 607 |
|
61799 | 608 |
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
|
609 |
lemmas le_simps = less_imp_le_nat less_Suc_eq_le Suc_le_eq |
13449 | 610 |
|
611 |
||
63110 | 612 |
text \<open>Equivalence of \<open>m \<le> n\<close> and \<open>m < n \<or> m = n\<close>\<close> |
613 |
||
614 |
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
|
615 |
unfolding le_less . |
13449 | 616 |
|
63110 | 617 |
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
|
618 |
by (rule le_less) |
13449 | 619 |
|
61799 | 620 |
text \<open>Useful with \<open>blast\<close>.\<close> |
63110 | 621 |
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
|
622 |
by auto |
13449 | 623 |
|
63110 | 624 |
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
|
625 |
by simp |
13449 | 626 |
|
63110 | 627 |
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
|
628 |
by (rule order_trans) |
13449 | 629 |
|
63110 | 630 |
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
|
631 |
by (rule antisym) |
13449 | 632 |
|
63110 | 633 |
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
|
634 |
by (rule less_le) |
13449 | 635 |
|
63110 | 636 |
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
|
637 |
unfolding less_le .. |
13449 | 638 |
|
63110 | 639 |
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
|
640 |
by (rule linear) |
14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset
|
641 |
|
22718 | 642 |
lemmas linorder_neqE_nat = linorder_neqE [where 'a = nat] |
15921 | 643 |
|
63110 | 644 |
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
|
645 |
unfolding less_Suc_eq_le by auto |
13449 | 646 |
|
63110 | 647 |
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
|
648 |
unfolding not_less by (rule le_less_Suc_eq) |
13449 | 649 |
|
650 |
lemmas not_less_simps = not_less_less_Suc_eq le_less_Suc_eq |
|
651 |
||
63110 | 652 |
lemma not0_implies_Suc: "n \<noteq> 0 \<Longrightarrow> \<exists>m. n = Suc m" |
653 |
by (cases n) simp_all |
|
654 |
||
655 |
lemma gr0_implies_Suc: "n > 0 \<Longrightarrow> \<exists>m. n = Suc m" |
|
656 |
by (cases n) simp_all |
|
657 |
||
658 |
lemma gr_implies_not0: "m < n \<Longrightarrow> n \<noteq> 0" for m n :: nat |
|
659 |
by (cases n) simp_all |
|
660 |
||
661 |
lemma neq0_conv[iff]: "n \<noteq> 0 \<longleftrightarrow> 0 < n" for n :: nat |
|
662 |
by (cases n) simp_all |
|
25140 | 663 |
|
61799 | 664 |
text \<open>This theorem is useful with \<open>blast\<close>\<close> |
63110 | 665 |
lemma gr0I: "(n = 0 \<Longrightarrow> False) \<Longrightarrow> 0 < n" for n :: nat |
666 |
by (rule neq0_conv[THEN iffD1], iprover) |
|
667 |
||
668 |
lemma gr0_conv_Suc: "0 < n \<longleftrightarrow> (\<exists>m. n = Suc m)" |
|
669 |
by (fast intro: not0_implies_Suc) |
|
670 |
||
671 |
lemma not_gr0 [iff]: "\<not> 0 < n \<longleftrightarrow> n = 0" for n :: nat |
|
672 |
using neq0_conv by blast |
|
673 |
||
674 |
lemma Suc_le_D: "Suc n \<le> m' \<Longrightarrow> \<exists>m. m' = Suc m" |
|
675 |
by (induct m') simp_all |
|
13449 | 676 |
|
60758 | 677 |
text \<open>Useful in certain inductive arguments\<close> |
63110 | 678 |
lemma less_Suc_eq_0_disj: "m < Suc n \<longleftrightarrow> m = 0 \<or> (\<exists>j. m = Suc j \<and> j < n)" |
679 |
by (cases m) simp_all |
|
13449 | 680 |
|
681 |
||
60758 | 682 |
subsubsection \<open>Monotonicity of Addition\<close> |
13449 | 683 |
|
63110 | 684 |
lemma Suc_pred [simp]: "n > 0 \<Longrightarrow> Suc (n - Suc 0) = n" |
685 |
by (simp add: diff_Suc split: nat.split) |
|
686 |
||
687 |
lemma Suc_diff_1 [simp]: "0 < n \<Longrightarrow> Suc (n - 1) = n" |
|
688 |
unfolding One_nat_def by (rule Suc_pred) |
|
689 |
||
690 |
lemma nat_add_left_cancel_le [simp]: "k + m \<le> k + n \<longleftrightarrow> m \<le> n" for k m n :: nat |
|
691 |
by (induct k) simp_all |
|
692 |
||
693 |
lemma nat_add_left_cancel_less [simp]: "k + m < k + n \<longleftrightarrow> m < n" for k m n :: nat |
|
694 |
by (induct k) simp_all |
|
695 |
||
696 |
lemma add_gr_0 [iff]: "m + n > 0 \<longleftrightarrow> m > 0 \<or> n > 0" for m n :: nat |
|
697 |
by (auto dest: gr0_implies_Suc) |
|
13449 | 698 |
|
60758 | 699 |
text \<open>strict, in 1st argument\<close> |
63110 | 700 |
lemma add_less_mono1: "i < j \<Longrightarrow> i + k < j + k" for i j k :: nat |
701 |
by (induct k) simp_all |
|
14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset
|
702 |
|
60758 | 703 |
text \<open>strict, in both arguments\<close> |
63110 | 704 |
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
|
705 |
apply (rule add_less_mono1 [THEN less_trans], assumption+) |
15251 | 706 |
apply (induct j, simp_all) |
14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset
|
707 |
done |
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset
|
708 |
|
61799 | 709 |
text \<open>Deleted \<open>less_natE\<close>; use \<open>less_imp_Suc_add RS exE\<close>\<close> |
63110 | 710 |
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
|
711 |
apply (induct n) |
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset
|
712 |
apply (simp_all add: order_le_less) |
22718 | 713 |
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
|
714 |
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
|
715 |
done |
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset
|
716 |
|
63110 | 717 |
lemma le_Suc_ex: "k \<le> l \<Longrightarrow> (\<exists>n. l = k + n)" for k l :: nat |
56194 | 718 |
by (auto simp: less_Suc_eq_le[symmetric] dest: less_imp_Suc_add) |
719 |
||
61799 | 720 |
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
|
721 |
lemma mult_less_mono2: |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
722 |
fixes i j :: nat |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
723 |
assumes "i < j" and "0 < k" |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
724 |
shows "k * i < k * j" |
63110 | 725 |
using \<open>0 < k\<close> |
726 |
proof (induct k) |
|
727 |
case 0 |
|
728 |
then show ?case by simp |
|
62481
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
729 |
next |
63110 | 730 |
case (Suc k) |
731 |
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
|
732 |
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
|
733 |
qed |
14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset
|
734 |
|
60758 | 735 |
text \<open>Addition is the inverse of subtraction: |
736 |
if @{term "n \<le> m"} then @{term "n + (m - n) = m"}.\<close> |
|
63110 | 737 |
lemma add_diff_inverse_nat: "\<not> m < n \<Longrightarrow> n + (m - n) = m" for m n :: nat |
738 |
by (induct m n rule: diff_induct) simp_all |
|
739 |
||
740 |
lemma nat_le_iff_add: "m \<le> n \<longleftrightarrow> (\<exists>k. n = m + k)" for m n :: nat |
|
741 |
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
|
742 |
|
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
|
743 |
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
|
744 |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34208
diff
changeset
|
745 |
instance nat :: linordered_semidom |
14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14331
diff
changeset
|
746 |
proof |
63110 | 747 |
fix m n q :: nat |
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14341
diff
changeset
|
748 |
show "0 < (1::nat)" by simp |
63110 | 749 |
show "m \<le> n \<Longrightarrow> q + m \<le> q + n" by simp |
750 |
show "m < n \<Longrightarrow> 0 < q \<Longrightarrow> q * m < q * n" by (simp add: mult_less_mono2) |
|
751 |
show "m \<noteq> 0 \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> m * n \<noteq> 0" by simp |
|
752 |
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
|
753 |
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
|
754 |
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
|
755 |
|
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
|
756 |
instance nat :: dioid |
63110 | 757 |
by standard (rule nat_le_iff_add) |
63145 | 758 |
declare le0[simp del] \<comment> \<open>This is now @{thm zero_le}\<close> |
759 |
declare le_0_eq[simp del] \<comment> \<open>This is now @{thm le_zero_eq}\<close> |
|
760 |
declare not_less0[simp del] \<comment> \<open>This is now @{thm not_less_zero}\<close> |
|
761 |
declare not_gr0[simp del] \<comment> \<open>This is now @{thm not_gr_zero}\<close> |
|
62376
85f38d5f8807
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents:
62365
diff
changeset
|
762 |
|
63110 | 763 |
instance nat :: ordered_cancel_comm_monoid_add .. |
764 |
instance nat :: ordered_cancel_comm_monoid_diff .. |
|
765 |
||
44817 | 766 |
|
60758 | 767 |
subsubsection \<open>@{term min} and @{term max}\<close> |
44817 | 768 |
|
769 |
lemma mono_Suc: "mono Suc" |
|
63110 | 770 |
by (rule monoI) simp |
771 |
||
772 |
lemma min_0L [simp]: "min 0 n = 0" for n :: nat |
|
773 |
by (rule min_absorb1) simp |
|
774 |
||
775 |
lemma min_0R [simp]: "min n 0 = 0" for n :: nat |
|
776 |
by (rule min_absorb2) simp |
|
44817 | 777 |
|
778 |
lemma min_Suc_Suc [simp]: "min (Suc m) (Suc n) = Suc (min m n)" |
|
63110 | 779 |
by (simp add: mono_Suc min_of_mono) |
780 |
||
781 |
lemma min_Suc1: "min (Suc n) m = (case m of 0 \<Rightarrow> 0 | Suc m' \<Rightarrow> Suc(min n m'))" |
|
782 |
by (simp split: nat.split) |
|
783 |
||
784 |
lemma min_Suc2: "min m (Suc n) = (case m of 0 \<Rightarrow> 0 | Suc m' \<Rightarrow> Suc(min m' n))" |
|
785 |
by (simp split: nat.split) |
|
786 |
||
787 |
lemma max_0L [simp]: "max 0 n = n" for n :: nat |
|
788 |
by (rule max_absorb2) simp |
|
789 |
||
790 |
lemma max_0R [simp]: "max n 0 = n" for n :: nat |
|
791 |
by (rule max_absorb1) simp |
|
792 |
||
793 |
lemma max_Suc_Suc [simp]: "max (Suc m) (Suc n) = Suc (max m n)" |
|
794 |
by (simp add: mono_Suc max_of_mono) |
|
795 |
||
796 |
lemma max_Suc1: "max (Suc n) m = (case m of 0 \<Rightarrow> Suc n | Suc m' \<Rightarrow> Suc (max n m'))" |
|
797 |
by (simp split: nat.split) |
|
798 |
||
799 |
lemma max_Suc2: "max m (Suc n) = (case m of 0 \<Rightarrow> Suc n | Suc m' \<Rightarrow> Suc (max m' n))" |
|
800 |
by (simp split: nat.split) |
|
801 |
||
802 |
lemma nat_mult_min_left: "min m n * q = min (m * q) (n * q)" for m n q :: nat |
|
803 |
by (simp add: min_def not_le) |
|
804 |
(auto dest: mult_right_le_imp_le mult_right_less_imp_less le_less_trans) |
|
805 |
||
806 |
lemma nat_mult_min_right: "m * min n q = min (m * n) (m * q)" for m n q :: nat |
|
807 |
by (simp add: min_def not_le) |
|
808 |
(auto dest: mult_left_le_imp_le mult_left_less_imp_less le_less_trans) |
|
809 |
||
810 |
lemma nat_add_max_left: "max m n + q = max (m + q) (n + q)" for m n q :: nat |
|
44817 | 811 |
by (simp add: max_def) |
812 |
||
63110 | 813 |
lemma nat_add_max_right: "m + max n q = max (m + n) (m + q)" for m n q :: nat |
44817 | 814 |
by (simp add: max_def) |
815 |
||
63110 | 816 |
lemma nat_mult_max_left: "max m n * q = max (m * q) (n * q)" for m n q :: nat |
817 |
by (simp add: max_def not_le) |
|
818 |
(auto dest: mult_right_le_imp_le mult_right_less_imp_less le_less_trans) |
|
819 |
||
820 |
lemma nat_mult_max_right: "m * max n q = max (m * n) (m * q)" for m n q :: nat |
|
821 |
by (simp add: max_def not_le) |
|
822 |
(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
|
823 |
|
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
824 |
|
60758 | 825 |
subsubsection \<open>Additional theorems about @{term "op \<le>"}\<close> |
826 |
||
827 |
text \<open>Complete induction, aka course-of-values induction\<close> |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset
|
828 |
|
63110 | 829 |
instance nat :: wellorder |
830 |
proof |
|
27823 | 831 |
fix P and n :: nat |
63110 | 832 |
assume step: "(\<And>m. m < n \<Longrightarrow> P m) \<Longrightarrow> P n" for n :: nat |
27823 | 833 |
have "\<And>q. q \<le> n \<Longrightarrow> P q" |
834 |
proof (induct n) |
|
835 |
case (0 n) |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset
|
836 |
have "P 0" by (rule step) auto |
63110 | 837 |
then show ?case using 0 by auto |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset
|
838 |
next |
27823 | 839 |
case (Suc m n) |
840 |
then have "n \<le> m \<or> n = Suc m" by (simp add: le_Suc_eq) |
|
63110 | 841 |
then show ?case |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset
|
842 |
proof |
63110 | 843 |
assume "n \<le> m" |
844 |
then show "P n" by (rule Suc(1)) |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset
|
845 |
next |
27823 | 846 |
assume n: "n = Suc m" |
63110 | 847 |
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
|
848 |
qed |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset
|
849 |
qed |
27823 | 850 |
then show "P n" by auto |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset
|
851 |
qed |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset
|
852 |
|
57015 | 853 |
|
63110 | 854 |
lemma Least_eq_0[simp]: "P 0 \<Longrightarrow> Least P = 0" for P :: "nat \<Rightarrow> bool" |
855 |
by (rule Least_equality[OF _ le0]) |
|
856 |
||
857 |
lemma Least_Suc: "P n \<Longrightarrow> \<not> P 0 \<Longrightarrow> (LEAST n. P n) = Suc (LEAST m. P (Suc m))" |
|
47988 | 858 |
apply (cases n, auto) |
27823 | 859 |
apply (frule LeastI) |
63110 | 860 |
apply (drule_tac P = "\<lambda>x. P (Suc x) " in LeastI) |
27823 | 861 |
apply (subgoal_tac " (LEAST x. P x) \<le> Suc (LEAST x. P (Suc x))") |
862 |
apply (erule_tac [2] Least_le) |
|
47988 | 863 |
apply (cases "LEAST x. P x", auto) |
63110 | 864 |
apply (drule_tac P = "\<lambda>x. P (Suc x) " in Least_le) |
27823 | 865 |
apply (blast intro: order_antisym) |
866 |
done |
|
867 |
||
63110 | 868 |
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 | 869 |
apply (erule (1) Least_Suc [THEN ssubst]) |
870 |
apply simp |
|
871 |
done |
|
872 |
||
63110 | 873 |
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 | 874 |
apply (cases n) |
875 |
apply blast |
|
63110 | 876 |
apply (rule_tac x="LEAST k. P k" in exI) |
27823 | 877 |
apply (blast intro: Least_le dest: not_less_Least intro: LeastI_ex) |
878 |
done |
|
879 |
||
63110 | 880 |
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
|
881 |
unfolding One_nat_def |
27823 | 882 |
apply (cases n) |
883 |
apply blast |
|
884 |
apply (frule (1) ex_least_nat_le) |
|
885 |
apply (erule exE) |
|
886 |
apply (case_tac k) |
|
887 |
apply simp |
|
888 |
apply (rename_tac k1) |
|
889 |
apply (rule_tac x=k1 in exI) |
|
890 |
apply (auto simp add: less_eq_Suc_le) |
|
891 |
done |
|
892 |
||
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset
|
893 |
lemma nat_less_induct: |
63110 | 894 |
fixes P :: "nat \<Rightarrow> bool" |
895 |
assumes "\<And>n. \<forall>m. m < n \<longrightarrow> P m \<Longrightarrow> P n" |
|
896 |
shows "P n" |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset
|
897 |
using assms less_induct by blast |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset
|
898 |
|
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset
|
899 |
lemma measure_induct_rule [case_names less]: |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset
|
900 |
fixes f :: "'a \<Rightarrow> nat" |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset
|
901 |
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
|
902 |
shows "P a" |
63110 | 903 |
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
|
904 |
|
60758 | 905 |
text \<open>old style induction rules:\<close> |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset
|
906 |
lemma measure_induct: |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset
|
907 |
fixes f :: "'a \<Rightarrow> nat" |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset
|
908 |
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
|
909 |
by (rule measure_induct_rule [of f P a]) iprover |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset
|
910 |
|
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset
|
911 |
lemma full_nat_induct: |
63110 | 912 |
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
|
913 |
shows "P n" |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset
|
914 |
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
|
915 |
|
63110 | 916 |
text\<open>An induction rule for establishing binary relations\<close> |
62683 | 917 |
lemma less_Suc_induct [consumes 1]: |
63110 | 918 |
assumes less: "i < j" |
919 |
and step: "\<And>i. P i (Suc i)" |
|
920 |
and trans: "\<And>i j k. i < j \<Longrightarrow> j < k \<Longrightarrow> P i j \<Longrightarrow> P j k \<Longrightarrow> P i k" |
|
19870 | 921 |
shows "P i j" |
922 |
proof - |
|
63110 | 923 |
from less obtain k where j: "j = Suc (i + k)" |
924 |
by (auto dest: less_imp_Suc_add) |
|
22718 | 925 |
have "P i (Suc (i + k))" |
19870 | 926 |
proof (induct k) |
22718 | 927 |
case 0 |
928 |
show ?case by (simp add: step) |
|
19870 | 929 |
next |
930 |
case (Suc k) |
|
31714 | 931 |
have "0 + i < Suc k + i" by (rule add_less_mono1) simp |
63110 | 932 |
then have "i < Suc (i + k)" by (simp add: add.commute) |
31714 | 933 |
from trans[OF this lessI Suc step] |
934 |
show ?case by simp |
|
19870 | 935 |
qed |
63110 | 936 |
then show "P i j" by (simp add: j) |
19870 | 937 |
qed |
938 |
||
63111 | 939 |
text \<open> |
940 |
The method of infinite descent, frequently used in number theory. |
|
941 |
Provided by Roelof Oosterhuis. |
|
942 |
\<open>P n\<close> is true for all natural numbers if |
|
943 |
\<^item> case ``0'': given \<open>n = 0\<close> prove \<open>P n\<close> |
|
944 |
\<^item> case ``smaller'': given \<open>n > 0\<close> and \<open>\<not> P n\<close> prove there exists |
|
945 |
a smaller natural number \<open>m\<close> such that \<open>\<not> P m\<close>. |
|
946 |
\<close> |
|
947 |
||
63110 | 948 |
lemma infinite_descent: "(\<And>n. \<not> P n \<Longrightarrow> \<exists>m<n. \<not> P m) \<Longrightarrow> P n" for P :: "nat \<Rightarrow> bool" |
63111 | 949 |
\<comment> \<open>compact version without explicit base case\<close> |
63110 | 950 |
by (induct n rule: less_induct) auto |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset
|
951 |
|
63111 | 952 |
lemma infinite_descent0 [case_names 0 smaller]: |
63110 | 953 |
fixes P :: "nat \<Rightarrow> bool" |
63111 | 954 |
assumes "P 0" |
955 |
and "\<And>n. n > 0 \<Longrightarrow> \<not> P n \<Longrightarrow> \<exists>m. m < n \<and> \<not> P m" |
|
63110 | 956 |
shows "P n" |
957 |
apply (rule infinite_descent) |
|
958 |
using assms |
|
959 |
apply (case_tac "n > 0") |
|
960 |
apply auto |
|
961 |
done |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset
|
962 |
|
60758 | 963 |
text \<open> |
63111 | 964 |
Infinite descent using a mapping to \<open>nat\<close>: |
965 |
\<open>P x\<close> is true for all \<open>x \<in> D\<close> if there exists a \<open>V \<in> D \<Rightarrow> nat\<close> and |
|
966 |
\<^item> case ``0'': given \<open>V x = 0\<close> prove \<open>P x\<close> |
|
967 |
\<^item> ``smaller'': given \<open>V x > 0\<close> and \<open>\<not> P x\<close> prove |
|
968 |
there exists a \<open>y \<in> D\<close> such that \<open>V y < V x\<close> and \<open>\<not> P y\<close>. |
|
969 |
\<close> |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset
|
970 |
corollary infinite_descent0_measure [case_names 0 smaller]: |
63110 | 971 |
fixes V :: "'a \<Rightarrow> nat" |
972 |
assumes 1: "\<And>x. V x = 0 \<Longrightarrow> P x" |
|
973 |
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
|
974 |
shows "P x" |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset
|
975 |
proof - |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset
|
976 |
obtain n where "n = V x" by auto |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset
|
977 |
moreover have "\<And>x. V x = n \<Longrightarrow> P x" |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset
|
978 |
proof (induct n rule: infinite_descent0) |
63110 | 979 |
case 0 |
980 |
with 1 show "P x" by auto |
|
981 |
next |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset
|
982 |
case (smaller n) |
63110 | 983 |
then obtain x where *: "V x = n " and "V x > 0 \<and> \<not> P x" by auto |
984 |
with 2 obtain y where "V y < V x \<and> \<not> P y" by auto |
|
63111 | 985 |
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
|
986 |
then show ?case by auto |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset
|
987 |
qed |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset
|
988 |
ultimately show "P x" by auto |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset
|
989 |
qed |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset
|
990 |
|
60758 | 991 |
text\<open>Again, without explicit base case:\<close> |
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset
|
992 |
lemma infinite_descent_measure: |
63110 | 993 |
fixes V :: "'a \<Rightarrow> nat" |
994 |
assumes "\<And>x. \<not> P x \<Longrightarrow> \<exists>y. V y < V x \<and> \<not> P y" |
|
995 |
shows "P x" |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset
|
996 |
proof - |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset
|
997 |
from assms obtain n where "n = V x" by auto |
63110 | 998 |
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
|
999 |
proof (induct n rule: infinite_descent, auto) |
63111 | 1000 |
show "\<exists>m < V x. \<exists>y. V y = m \<and> \<not> P y" if "\<not> P x" for x |
1001 |
using assms and that by auto |
|
26748
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset
|
1002 |
qed |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset
|
1003 |
ultimately show "P x" by auto |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset
|
1004 |
qed |
4d51ddd6aa5c
Merged theories about wellfoundedness into one: Wellfounded.thy
krauss
parents:
26335
diff
changeset
|
1005 |
|
63111 | 1006 |
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
|
1007 |
lemma less_mono_imp_le_mono: |
63110 | 1008 |
fixes f :: "nat \<Rightarrow> nat" |
1009 |
and i j :: nat |
|
1010 |
assumes "\<And>i j::nat. i < j \<Longrightarrow> f i < f j" |
|
1011 |
and "i \<le> j" |
|
1012 |
shows "f i \<le> f j" |
|
1013 |
using assms by (auto simp add: order_le_less) |
|
24438 | 1014 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
1015 |
|
60758 | 1016 |
text \<open>non-strict, in 1st argument\<close> |
63110 | 1017 |
lemma add_le_mono1: "i \<le> j \<Longrightarrow> i + k \<le> j + k" for i j k :: nat |
1018 |
by (rule add_right_mono) |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
1019 |
|
60758 | 1020 |
text \<open>non-strict, in both arguments\<close> |
63110 | 1021 |
lemma add_le_mono: "i \<le> j \<Longrightarrow> k \<le> l \<Longrightarrow> i + k \<le> j + l" for i j k l :: nat |
1022 |
by (rule add_mono) |
|
1023 |
||
1024 |
lemma le_add2: "n \<le> m + n" for m n :: nat |
|
62608 | 1025 |
by simp |
13449 | 1026 |
|
63110 | 1027 |
lemma le_add1: "n \<le> n + m" for m n :: nat |
62608 | 1028 |
by simp |
13449 | 1029 |
|
1030 |
lemma less_add_Suc1: "i < Suc (i + m)" |
|
63110 | 1031 |
by (rule le_less_trans, rule le_add1, rule lessI) |
13449 | 1032 |
|
1033 |
lemma less_add_Suc2: "i < Suc (m + i)" |
|
63110 | 1034 |
by (rule le_less_trans, rule le_add2, rule lessI) |
1035 |
||
1036 |
lemma less_iff_Suc_add: "m < n \<longleftrightarrow> (\<exists>k. n = Suc (m + k))" |
|
1037 |
by (iprover intro!: less_add_Suc1 less_imp_Suc_add) |
|
1038 |
||
1039 |
lemma trans_le_add1: "i \<le> j \<Longrightarrow> i \<le> j + m" for i j m :: nat |
|
1040 |
by (rule le_trans, assumption, rule le_add1) |
|
1041 |
||
1042 |
lemma trans_le_add2: "i \<le> j \<Longrightarrow> i \<le> m + j" for i j m :: nat |
|
1043 |
by (rule le_trans, assumption, rule le_add2) |
|
1044 |
||
1045 |
lemma trans_less_add1: "i < j \<Longrightarrow> i < j + m" for i j m :: nat |
|
1046 |
by (rule less_le_trans, assumption, rule le_add1) |
|
1047 |
||
1048 |
lemma trans_less_add2: "i < j \<Longrightarrow> i < m + j" for i j m :: nat |
|
1049 |
by (rule less_le_trans, assumption, rule le_add2) |
|
1050 |
||
1051 |
lemma add_lessD1: "i + j < k \<Longrightarrow> i < k" for i j k :: nat |
|
1052 |
by (rule le_less_trans [of _ "i+j"]) (simp_all add: le_add1) |
|
1053 |
||
1054 |
lemma not_add_less1 [iff]: "\<not> i + j < i" for i j :: nat |
|
1055 |
apply (rule notI) |
|
1056 |
apply (drule add_lessD1) |
|
1057 |
apply (erule less_irrefl [THEN notE]) |
|
1058 |
done |
|
1059 |
||
1060 |
lemma not_add_less2 [iff]: "\<not> j + i < i" for i j :: nat |
|
1061 |
by (simp add: add.commute) |
|
1062 |
||
1063 |
lemma add_leD1: "m + k \<le> n \<Longrightarrow> m \<le> n" for k m n :: nat |
|
1064 |
by (rule order_trans [of _ "m+k"]) (simp_all add: le_add1) |
|
1065 |
||
1066 |
lemma add_leD2: "m + k \<le> n \<Longrightarrow> k \<le> n" for k m n :: nat |
|
1067 |
apply (simp add: add.commute) |
|
1068 |
apply (erule add_leD1) |
|
1069 |
done |
|
1070 |
||
1071 |
lemma add_leE: "m + k \<le> n \<Longrightarrow> (m \<le> n \<Longrightarrow> k \<le> n \<Longrightarrow> R) \<Longrightarrow> R" for k m n :: nat |
|
1072 |
by (blast dest: add_leD1 add_leD2) |
|
1073 |
||
1074 |
text \<open>needs \<open>\<And>k\<close> for \<open>ac_simps\<close> to work\<close> |
|
1075 |
lemma less_add_eq_less: "\<And>k::nat. k < l \<Longrightarrow> m + l = k + n \<Longrightarrow> m < n" |
|
1076 |
by (force simp del: add_Suc_right simp add: less_iff_Suc_add add_Suc_right [symmetric] ac_simps) |
|
13449 | 1077 |
|
1078 |
||
60758 | 1079 |
subsubsection \<open>More results about difference\<close> |
13449 | 1080 |
|
63110 | 1081 |
lemma Suc_diff_le: "n \<le> m \<Longrightarrow> Suc m - n = Suc (m - n)" |
1082 |
by (induct m n rule: diff_induct) simp_all |
|
13449 | 1083 |
|
1084 |
lemma diff_less_Suc: "m - n < Suc m" |
|
24438 | 1085 |
apply (induct m n rule: diff_induct) |
1086 |
apply (erule_tac [3] less_SucE) |
|
1087 |
apply (simp_all add: less_Suc_eq) |
|
1088 |
done |
|
13449 | 1089 |
|
63110 | 1090 |
lemma diff_le_self [simp]: "m - n \<le> m" for m n :: nat |
1091 |
by (induct m n rule: diff_induct) (simp_all add: le_SucI) |
|
1092 |
||
1093 |
lemma less_imp_diff_less: "j < k \<Longrightarrow> j - n < k" for j k n :: nat |
|
1094 |
by (rule le_less_trans, rule diff_le_self) |
|
1095 |
||
1096 |
lemma diff_Suc_less [simp]: "0 < n \<Longrightarrow> n - Suc i < n" |
|
1097 |
by (cases n) (auto simp add: le_simps) |
|
1098 |
||
1099 |
lemma diff_add_assoc: "k \<le> j \<Longrightarrow> (i + j) - k = i + (j - k)" for i j k :: nat |
|
1100 |
by (induct j k rule: diff_induct) simp_all |
|
1101 |
||
1102 |
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
|
1103 |
by (fact diff_add_assoc [symmetric]) |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1104 |
|
63110 | 1105 |
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
|
1106 |
by (simp add: ac_simps) |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1107 |
|
63110 | 1108 |
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
|
1109 |
by (fact diff_add_assoc2 [symmetric]) |
13449 | 1110 |
|
63110 | 1111 |
lemma le_imp_diff_is_add: "i \<le> j \<Longrightarrow> (j - i = k) = (j = k + i)" for i j k :: nat |
1112 |
by auto |
|
1113 |
||
1114 |
lemma diff_is_0_eq [simp]: "m - n = 0 \<longleftrightarrow> m \<le> n" for m n :: nat |
|
1115 |
by (induct m n rule: diff_induct) simp_all |
|
1116 |
||
1117 |
lemma diff_is_0_eq' [simp]: "m \<le> n \<Longrightarrow> m - n = 0" for m n :: nat |
|
1118 |
by (rule iffD2, rule diff_is_0_eq) |
|
1119 |
||
1120 |
lemma zero_less_diff [simp]: "0 < n - m \<longleftrightarrow> m < n" for m n :: nat |
|
1121 |
by (induct m n rule: diff_induct) simp_all |
|
13449 | 1122 |
|
22718 | 1123 |
lemma less_imp_add_positive: |
1124 |
assumes "i < j" |
|
63110 | 1125 |
shows "\<exists>k::nat. 0 < k \<and> i + k = j" |
22718 | 1126 |
proof |
63110 | 1127 |
from assms show "0 < j - i \<and> i + (j - i) = j" |
23476 | 1128 |
by (simp add: order_less_imp_le) |
22718 | 1129 |
qed |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
7702
diff
changeset
|
1130 |
|
60758 | 1131 |
text \<open>a nice rewrite for bounded subtraction\<close> |
63110 | 1132 |
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
|
1133 |
by (simp add: max_def not_le order_less_imp_le) |
13449 | 1134 |
|
63110 | 1135 |
lemma nat_diff_split: "P (a - b) \<longleftrightarrow> (a < b \<longrightarrow> P 0) \<and> (\<forall>d. a = b + d \<longrightarrow> P d)" |
1136 |
for a b :: nat |
|
61799 | 1137 |
\<comment> \<open>elimination of \<open>-\<close> on \<open>nat\<close>\<close> |
62365 | 1138 |
by (cases "a < b") |
1139 |
(auto simp add: not_less le_less dest!: add_eq_self_zero [OF sym]) |
|
13449 | 1140 |
|
63110 | 1141 |
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))" |
1142 |
for a b :: nat |
|
61799 | 1143 |
\<comment> \<open>elimination of \<open>-\<close> on \<open>nat\<close> in assumptions\<close> |
62365 | 1144 |
by (auto split: nat_diff_split) |
13449 | 1145 |
|
63110 | 1146 |
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
|
1147 |
by simp |
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47208
diff
changeset
|
1148 |
|
63110 | 1149 |
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
|
1150 |
unfolding One_nat_def by (cases m) simp_all |
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47208
diff
changeset
|
1151 |
|
63110 | 1152 |
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
|
1153 |
unfolding One_nat_def by (cases m) simp_all |
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47208
diff
changeset
|
1154 |
|
63110 | 1155 |
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
|
1156 |
unfolding One_nat_def by (cases n) simp_all |
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47208
diff
changeset
|
1157 |
|
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47208
diff
changeset
|
1158 |
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
|
1159 |
unfolding One_nat_def by (cases m) simp_all |
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47208
diff
changeset
|
1160 |
|
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47208
diff
changeset
|
1161 |
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
|
1162 |
by (fact Let_def) |
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47208
diff
changeset
|
1163 |
|
13449 | 1164 |
|
60758 | 1165 |
subsubsection \<open>Monotonicity of multiplication\<close> |
13449 | 1166 |
|
63110 | 1167 |
lemma mult_le_mono1: "i \<le> j \<Longrightarrow> i * k \<le> j * k" for i j k :: nat |
1168 |
by (simp add: mult_right_mono) |
|
1169 |
||
1170 |
lemma mult_le_mono2: "i \<le> j \<Longrightarrow> k * i \<le> k * j" for i j k :: nat |
|
1171 |
by (simp add: mult_left_mono) |
|
13449 | 1172 |
|
61799 | 1173 |
text \<open>\<open>\<le>\<close> monotonicity, BOTH arguments\<close> |
63110 | 1174 |
lemma mult_le_mono: "i \<le> j \<Longrightarrow> k \<le> l \<Longrightarrow> i * k \<le> j * l" for i j k l :: nat |
1175 |
by (simp add: mult_mono) |
|
1176 |
||
1177 |
lemma mult_less_mono1: "i < j \<Longrightarrow> 0 < k \<Longrightarrow> i * k < j * k" for i j k :: nat |
|
1178 |
by (simp add: mult_strict_right_mono) |
|
13449 | 1179 |
|
61799 | 1180 |
text\<open>Differs from the standard \<open>zero_less_mult_iff\<close> in that |
60758 | 1181 |
there are no negative numbers.\<close> |
63110 | 1182 |
lemma nat_0_less_mult_iff [simp]: "0 < m * n \<longleftrightarrow> 0 < m \<and> 0 < n" for m n :: nat |
13449 | 1183 |
apply (induct m) |
22718 | 1184 |
apply simp |
1185 |
apply (case_tac n) |
|
1186 |
apply simp_all |
|
13449 | 1187 |
done |
1188 |
||
63110 | 1189 |
lemma one_le_mult_iff [simp]: "Suc 0 \<le> m * n \<longleftrightarrow> Suc 0 \<le> m \<and> Suc 0 \<le> n" |
13449 | 1190 |
apply (induct m) |
22718 | 1191 |
apply simp |
1192 |
apply (case_tac n) |
|
1193 |
apply simp_all |
|
13449 | 1194 |
done |
1195 |
||
63110 | 1196 |
lemma mult_less_cancel2 [simp]: "m * k < n * k \<longleftrightarrow> 0 < k \<and> m < n" for k m n :: nat |
13449 | 1197 |
apply (safe intro!: mult_less_mono1) |
47988 | 1198 |
apply (cases k, auto) |
63110 | 1199 |
apply (simp add: linorder_not_le [symmetric]) |
13449 | 1200 |
apply (blast intro: mult_le_mono1) |
1201 |
done |
|
1202 |
||
63110 | 1203 |
lemma mult_less_cancel1 [simp]: "k * m < k * n \<longleftrightarrow> 0 < k \<and> m < n" for k m n :: nat |
1204 |
by (simp add: mult.commute [of k]) |
|
1205 |
||
1206 |
lemma mult_le_cancel1 [simp]: "k * m \<le> k * n \<longleftrightarrow> (0 < k \<longrightarrow> m \<le> n)" for k m n :: nat |
|
1207 |
by (simp add: linorder_not_less [symmetric], auto) |
|
1208 |
||
1209 |
lemma mult_le_cancel2 [simp]: "m * k \<le> n * k \<longleftrightarrow> (0 < k \<longrightarrow> m \<le> n)" for k m n :: nat |
|
1210 |
by (simp add: linorder_not_less [symmetric], auto) |
|
1211 |
||
1212 |
lemma Suc_mult_less_cancel1: "Suc k * m < Suc k * n \<longleftrightarrow> m < n" |
|
1213 |
by (subst mult_less_cancel1) simp |
|
1214 |
||
1215 |
lemma Suc_mult_le_cancel1: "Suc k * m \<le> Suc k * n \<longleftrightarrow> m \<le> n" |
|
1216 |
by (subst mult_le_cancel1) simp |
|
1217 |
||
1218 |
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
|
1219 |
by (cases m) (auto intro: le_add1) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1220 |
|
63110 | 1221 |
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
|
1222 |
by (cases m) (auto intro: le_add1) |
13449 | 1223 |
|
61799 | 1224 |
text \<open>Lemma for \<open>gcd\<close>\<close> |
63110 | 1225 |
lemma mult_eq_self_implies_10: "m = m * n \<Longrightarrow> n = 1 \<or> m = 0" for m n :: nat |
13449 | 1226 |
apply (drule sym) |
1227 |
apply (rule disjCI) |
|
63113 | 1228 |
apply (rule linorder_cases, erule_tac [2] _) |
25157 | 1229 |
apply (drule_tac [2] mult_less_mono2) |
25162 | 1230 |
apply (auto) |
13449 | 1231 |
done |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
7702
diff
changeset
|
1232 |
|
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51173
diff
changeset
|
1233 |
lemma mono_times_nat: |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51173
diff
changeset
|
1234 |
fixes n :: nat |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51173
diff
changeset
|
1235 |
assumes "n > 0" |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51173
diff
changeset
|
1236 |
shows "mono (times n)" |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51173
diff
changeset
|
1237 |
proof |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51173
diff
changeset
|
1238 |
fix m q :: nat |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51173
diff
changeset
|
1239 |
assume "m \<le> q" |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51173
diff
changeset
|
1240 |
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
|
1241 |
qed |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51173
diff
changeset
|
1242 |
|
60758 | 1243 |
text \<open>the lattice order on @{typ nat}\<close> |
24995 | 1244 |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1245 |
instantiation nat :: distrib_lattice |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1246 |
begin |
24995 | 1247 |
|
63110 | 1248 |
definition "(inf :: nat \<Rightarrow> nat \<Rightarrow> nat) = min" |
1249 |
||
1250 |
definition "(sup :: nat \<Rightarrow> nat \<Rightarrow> nat) = max" |
|
1251 |
||
1252 |
instance |
|
1253 |
by intro_classes |
|
1254 |
(auto simp add: inf_nat_def sup_nat_def max_def not_le min_def |
|
1255 |
intro: order_less_imp_le antisym elim!: order_trans order_less_trans) |
|
24995 | 1256 |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1257 |
end |
24995 | 1258 |
|
1259 |
||
60758 | 1260 |
subsection \<open>Natural operation of natural numbers on functions\<close> |
1261 |
||
1262 |
text \<open> |
|
30971 | 1263 |
We use the same logical constant for the power operations on |
1264 |
functions and relations, in order to share the same syntax. |
|
60758 | 1265 |
\<close> |
30971 | 1266 |
|
45965
2af982715e5c
generalized type signature to permit overloading on `set`
haftmann
parents:
45933
diff
changeset
|
1267 |
consts compow :: "nat \<Rightarrow> 'a \<Rightarrow> 'a" |
30971 | 1268 |
|
63110 | 1269 |
abbreviation compower :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixr "^^" 80) |
1270 |
where "f ^^ n \<equiv> compow n f" |
|
30971 | 1271 |
|
1272 |
notation (latex output) |
|
1273 |
compower ("(_\<^bsup>_\<^esup>)" [1000] 1000) |
|
1274 |
||
61799 | 1275 |
text \<open>\<open>f ^^ n = f o ... o f\<close>, the n-fold composition of \<open>f\<close>\<close> |
30971 | 1276 |
|
1277 |
overloading |
|
63110 | 1278 |
funpow \<equiv> "compow :: nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a)" |
30971 | 1279 |
begin |
30954
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30686
diff
changeset
|
1280 |
|
55575
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55534
diff
changeset
|
1281 |
primrec funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where |
44325 | 1282 |
"funpow 0 f = id" |
1283 |
| "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
changeset
|
1284 |
|
30971 | 1285 |
end |
1286 |
||
62217 | 1287 |
lemma funpow_0 [simp]: "(f ^^ 0) x = x" |
1288 |
by simp |
|
1289 |
||
63110 | 1290 |
lemma funpow_Suc_right: "f ^^ Suc n = f ^^ n \<circ> f" |
49723
bbc2942ba09f
alternative simplification of ^^ to the righthand side;
haftmann
parents:
49388
diff
changeset
|
1291 |
proof (induct n) |
63110 | 1292 |
case 0 |
1293 |
then show ?case by simp |
|
49723
bbc2942ba09f
alternative simplification of ^^ to the righthand side;
haftmann
parents:
49388
diff
changeset
|
1294 |
next |
bbc2942ba09f
alternative simplification of ^^ to the righthand side;
haftmann
parents:
49388
diff
changeset
|
1295 |
fix n |
bbc2942ba09f
alternative simplification of ^^ to the righthand side;
haftmann
parents:
49388
diff
changeset
|
1296 |
assume "f ^^ Suc n = f ^^ n \<circ> f" |
bbc2942ba09f
alternative simplification of ^^ to the righthand side;
haftmann
parents:
49388
diff
changeset
|
1297 |
then show "f ^^ Suc (Suc n) = f ^^ Suc n \<circ> f" |
bbc2942ba09f
alternative simplification of ^^ to the righthand side;
haftmann
parents:
49388
diff
changeset
|
1298 |
by (simp add: o_assoc) |
bbc2942ba09f
alternative simplification of ^^ to the righthand side;
haftmann
parents:
49388
diff
changeset
|
1299 |
qed |
bbc2942ba09f
alternative simplification of ^^ to the righthand side;
haftmann
parents:
49388
diff
changeset
|
1300 |
|
bbc2942ba09f
alternative simplification of ^^ to the righthand side;
haftmann
parents:
49388
diff
changeset
|
1301 |
lemmas funpow_simps_right = funpow.simps(1) funpow_Suc_right |
bbc2942ba09f
alternative simplification of ^^ to the righthand side;
haftmann
parents:
49388
diff
changeset
|
1302 |
|
60758 | 1303 |
text \<open>for code generation\<close> |
30971 | 1304 |
|
63110 | 1305 |
definition funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" |
1306 |
where funpow_code_def [code_abbrev]: "funpow = compow" |
|
30954
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30686
diff
changeset
|
1307 |
|
30971 | 1308 |
lemma [code]: |
63110 | 1309 |
"funpow (Suc n) f = f \<circ> funpow n f" |
30971 | 1310 |
"funpow 0 f = id" |
37430 | 1311 |
by (simp_all add: funpow_code_def) |
30971 | 1312 |
|
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
|
1313 |
hide_const (open) funpow |
30954
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30686
diff
changeset
|
1314 |
|
63110 | 1315 |
lemma funpow_add: "f ^^ (m + n) = f ^^ m \<circ> f ^^ n" |
30954
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30686
diff
changeset
|
1316 |
by (induct m) simp_all |
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30686
diff
changeset
|
1317 |
|
63110 | 1318 |
lemma funpow_mult: "(f ^^ m) ^^ n = f ^^ (m * n)" for f :: "'a \<Rightarrow> 'a" |
37430 | 1319 |
by (induct n) (simp_all add: funpow_add) |
1320 |
||
63110 | 1321 |
lemma funpow_swap1: "f ((f ^^ n) x) = (f ^^ n) (f x)" |
30954
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30686
diff
changeset
|
1322 |
proof - |
30971 | 1323 |
have "f ((f ^^ n) x) = (f ^^ (n + 1)) x" by simp |
1324 |
also have "\<dots> = (f ^^ n o f ^^ 1) x" by (simp only: funpow_add) |
|
1325 |
also have "\<dots> = (f ^^ n) (f x)" by simp |
|
30954
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30686
diff
changeset
|
1326 |
finally show ?thesis . |
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30686
diff
changeset
|
1327 |
qed |
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30686
diff
changeset
|
1328 |
|
63110 | 1329 |
lemma comp_funpow: "comp f ^^ n = comp (f ^^ n)" for f :: "'a \<Rightarrow> 'a" |
38621
d6cb7e625d75
more concise characterization of of_nat operation and class semiring_char_0
haftmann
parents:
37767
diff
changeset
|
1330 |
by (induct n) simp_all |
30954
cf50e67bc1d1
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
haftmann
parents:
30686
diff
changeset
|
1331 |
|
54496
178922b63b58
add lemmas Suc_funpow and id_funpow to simpset; add lemma map_add_upt
hoelzl
parents:
54411
diff
changeset
|
1332 |
lemma Suc_funpow[simp]: "Suc ^^ n = (op + n)" |
178922b63b58
add lemmas Suc_funpow and id_funpow to simpset; add lemma map_add_upt
hoelzl
parents:
54411
diff
changeset
|
1333 |
by (induct n) simp_all |
178922b63b58
add lemmas Suc_funpow and id_funpow to simpset; add lemma map_add_upt
hoelzl
parents:
54411
diff
changeset
|
1334 |
|
178922b63b58
add lemmas Suc_funpow and id_funpow to simpset; add lemma map_add_upt
hoelzl
parents:
54411
diff
changeset
|
1335 |
lemma id_funpow[simp]: "id ^^ n = id" |
178922b63b58
add lemmas Suc_funpow and id_funpow to simpset; add lemma map_add_upt
hoelzl
parents:
54411
diff
changeset
|
1336 |
by (induct n) simp_all |
38621
d6cb7e625d75
more concise characterization of of_nat operation and class semiring_char_0
haftmann
parents:
37767
diff
changeset
|
1337 |
|
63110 | 1338 |
lemma funpow_mono: "mono f \<Longrightarrow> A \<le> B \<Longrightarrow> (f ^^ n) A \<le> (f ^^ n) B" |
1339 |
for f :: "'a \<Rightarrow> ('a::lattice)" |
|
59000 | 1340 |
by (induct n arbitrary: A B) |
1341 |
(auto simp del: funpow.simps(2) simp add: funpow_Suc_right mono_def) |
|
1342 |
||
63110 | 1343 |
|
60758 | 1344 |
subsection \<open>Kleene iteration\<close> |
45833 | 1345 |
|
52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
52435
diff
changeset
|
1346 |
lemma Kleene_iter_lpfp: |
63110 | 1347 |
assumes "mono f" |
1348 |
and "f p \<le> p" |
|
1349 |
shows "(f^^k) (bot::'a::order_bot) \<le> p" |
|
45833 | 1350 |
proof(induction k) |
63110 | 1351 |
case 0 |
1352 |
show ?case by simp |
|
45833 | 1353 |
next |
1354 |
case Suc |
|
63110 | 1355 |
from monoD[OF assms(1) Suc] assms(2) show ?case by simp |
45833 | 1356 |
qed |
1357 |
||
63110 | 1358 |
lemma lfp_Kleene_iter: |
1359 |
assumes "mono f" |
|
1360 |
and "(f^^Suc k) bot = (f^^k) bot" |
|
1361 |
shows "lfp f = (f^^k) bot" |
|
1362 |
proof (rule antisym) |
|
45833 | 1363 |
show "lfp f \<le> (f^^k) bot" |
63110 | 1364 |
proof (rule lfp_lowerbound) |
1365 |
show "f ((f^^k) bot) \<le> (f^^k) bot" |
|
1366 |
using assms(2) by simp |
|
45833 | 1367 |
qed |
1368 |
show "(f^^k) bot \<le> lfp f" |
|
1369 |
using Kleene_iter_lpfp[OF assms(1)] lfp_unfold[OF assms(1)] by simp |
|
1370 |
qed |
|
1371 |
||
63110 | 1372 |
lemma mono_pow: "mono f \<Longrightarrow> mono (f ^^ n)" for f :: "'a \<Rightarrow> 'a::complete_lattice" |
1373 |
by (induct n) (auto simp: mono_def) |
|
60636
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60562
diff
changeset
|
1374 |
|
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60562
diff
changeset
|
1375 |
lemma lfp_funpow: |
63110 | 1376 |
assumes f: "mono f" |
1377 |
shows "lfp (f ^^ Suc n) = lfp f" |
|
60636
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60562
diff
changeset
|
1378 |
proof (rule antisym) |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60562
diff
changeset
|
1379 |
show "lfp f \<le> lfp (f ^^ Suc n)" |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60562
diff
changeset
|
1380 |
proof (rule lfp_lowerbound) |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60562
diff
changeset
|
1381 |
have "f (lfp (f ^^ Suc n)) = lfp (\<lambda>x. f ((f ^^ n) x))" |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60562
diff
changeset
|
1382 |
unfolding funpow_Suc_right by (simp add: lfp_rolling f mono_pow comp_def) |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60562
diff
changeset
|
1383 |
then show "f (lfp (f ^^ Suc n)) \<le> lfp (f ^^ Suc n)" |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60562
diff
changeset
|
1384 |
by (simp add: comp_def) |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60562
diff
changeset
|
1385 |
qed |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60562
diff
changeset
|
1386 |
have "(f^^n) (lfp f) = lfp f" for n |
63110 | 1387 |
by (induct n) (auto intro: f lfp_unfold[symmetric]) |
60636
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60562
diff
changeset
|
1388 |
then show "lfp (f^^Suc n) \<le> lfp f" |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60562
diff
changeset
|
1389 |
by (intro lfp_lowerbound) (simp del: funpow.simps) |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60562
diff
changeset
|
1390 |
qed |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60562
diff
changeset
|
1391 |
|
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60562
diff
changeset
|
1392 |
lemma gfp_funpow: |
63110 | 1393 |
assumes f: "mono f" |
1394 |
shows "gfp (f ^^ Suc n) = gfp f" |
|
60636
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60562
diff
changeset
|
1395 |
proof (rule antisym) |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60562
diff
changeset
|
1396 |
show "gfp f \<ge> gfp (f ^^ Suc n)" |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60562
diff
changeset
|
1397 |
proof (rule gfp_upperbound) |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60562
diff
changeset
|
1398 |
have "f (gfp (f ^^ Suc n)) = gfp (\<lambda>x. f ((f ^^ n) x))" |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60562
diff
changeset
|
1399 |
unfolding funpow_Suc_right by (simp add: gfp_rolling f mono_pow comp_def) |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60562
diff
changeset
|
1400 |
then show "f (gfp (f ^^ Suc n)) \<ge> gfp (f ^^ Suc n)" |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60562
diff
changeset
|
1401 |
by (simp add: comp_def) |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60562
diff
changeset
|
1402 |
qed |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60562
diff
changeset
|
1403 |
have "(f^^n) (gfp f) = gfp f" for n |
63110 | 1404 |
by (induct n) (auto intro: f gfp_unfold[symmetric]) |
60636
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60562
diff
changeset
|
1405 |
then show "gfp (f^^Suc n) \<ge> gfp f" |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60562
diff
changeset
|
1406 |
by (intro gfp_upperbound) (simp del: funpow.simps) |
ee18efe9b246
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
hoelzl
parents:
60562
diff
changeset
|
1407 |
qed |
45833 | 1408 |
|
63110 | 1409 |
|
61799 | 1410 |
subsection \<open>Embedding of the naturals into any \<open>semiring_1\<close>: @{term of_nat}\<close> |
24196 | 1411 |
|
1412 |
context semiring_1 |
|
1413 |
begin |
|
1414 |
||
63110 | 1415 |
definition of_nat :: "nat \<Rightarrow> 'a" |
1416 |
where "of_nat n = (plus 1 ^^ n) 0" |
|
38621
d6cb7e625d75
more concise characterization of of_nat operation and class semiring_char_0
haftmann
parents:
37767
diff
changeset
|
1417 |
|
d6cb7e625d75
more concise characterization of of_nat operation and class semiring_char_0
haftmann
parents:
37767
diff
changeset
|
1418 |
lemma of_nat_simps [simp]: |
d6cb7e625d75
more concise characterization of of_nat operation and class semiring_char_0
haftmann
parents:
37767
diff
changeset
|
1419 |
shows of_nat_0: "of_nat 0 = 0" |
d6cb7e625d75
more concise characterization of of_nat operation and class semiring_char_0
haftmann
parents:
37767
diff
changeset
|
1420 |
and of_nat_Suc: "of_nat (Suc m) = 1 + of_nat m" |
d6cb7e625d75
more concise characterization of of_nat operation and class semiring_char_0
haftmann
parents:
37767
diff
changeset
|
1421 |
by (simp_all add: of_nat_def) |
25193 | 1422 |
|
1423 |
lemma of_nat_1 [simp]: "of_nat 1 = 1" |
|
38621
d6cb7e625d75
more concise characterization of of_nat operation and class semiring_char_0
haftmann
parents:
37767
diff
changeset
|
1424 |
by (simp add: of_nat_def) |
25193 | 1425 |
|
1426 |
lemma of_nat_add [simp]: "of_nat (m + n) = of_nat m + of_nat n" |
|
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset
|
1427 |
by (induct m) (simp_all add: ac_simps) |
25193 | 1428 |
|
61649
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61531
diff
changeset
|
1429 |
lemma of_nat_mult [simp]: "of_nat (m * n) = of_nat m * of_nat n" |
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset
|
1430 |
by (induct m) (simp_all add: ac_simps distrib_right) |
25193 | 1431 |
|
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61378
diff
changeset
|
1432 |
lemma mult_of_nat_commute: "of_nat x * y = y * of_nat x" |
63110 | 1433 |
by (induct x) (simp_all add: algebra_simps) |
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61378
diff
changeset
|
1434 |
|
55575
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55534
diff
changeset
|
1435 |
primrec of_nat_aux :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where |
28514 | 1436 |
"of_nat_aux inc 0 i = i" |
61799 | 1437 |
| "of_nat_aux inc (Suc n) i = of_nat_aux inc n (inc i)" \<comment> \<open>tail recursive\<close> |
25928 | 1438 |
|
63110 | 1439 |
lemma of_nat_code: "of_nat n = of_nat_aux (\<lambda>i. i + 1) n 0" |
28514 | 1440 |
proof (induct n) |
63110 | 1441 |
case 0 |
1442 |
then show ?case by simp |
|
28514 | 1443 |
next |
1444 |
case (Suc n) |
|
1445 |
have "\<And>i. of_nat_aux (\<lambda>i. i + 1) n (i + 1) = of_nat_aux (\<lambda>i. i + 1) n i + 1" |
|
1446 |
by (induct n) simp_all |
|
1447 |
from this [of 0] have "of_nat_aux (\<lambda>i. i + 1) n 1 = of_nat_aux (\<lambda>i. i + 1) n 0 + 1" |
|
1448 |
by simp |
|
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57492
diff
changeset
|
1449 |
with Suc show ?case by (simp add: add.commute) |
28514 | 1450 |
qed |
30966 | 1451 |
|
24196 | 1452 |
end |
1453 |
||
45231
d85a2fdc586c
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
bulwahn
parents:
44890
diff
changeset
|
1454 |
declare of_nat_code [code] |
30966 | 1455 |
|
62481
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1456 |
context ring_1 |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1457 |
begin |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1458 |
|
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1459 |
lemma of_nat_diff: "n \<le> m \<Longrightarrow> of_nat (m - n) = of_nat m - of_nat n" |
63110 | 1460 |
by (simp add: algebra_simps of_nat_add [symmetric]) |
62481
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1461 |
|
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1462 |
end |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1463 |
|
63110 | 1464 |
text \<open>Class for unital semirings with characteristic zero. |
60758 | 1465 |
Includes non-ordered rings like the complex numbers.\<close> |
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1466 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1467 |
class semiring_char_0 = semiring_1 + |
38621
d6cb7e625d75
more concise characterization of of_nat operation and class semiring_char_0
haftmann
parents:
37767
diff
changeset
|
1468 |
assumes inj_of_nat: "inj of_nat" |
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1469 |
begin |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1470 |
|
38621
d6cb7e625d75
more concise characterization of of_nat operation and class semiring_char_0
haftmann
parents:
37767
diff
changeset
|
1471 |
lemma of_nat_eq_iff [simp]: "of_nat m = of_nat n \<longleftrightarrow> m = n" |
d6cb7e625d75
more concise characterization of of_nat operation and class semiring_char_0
haftmann
parents:
37767
diff
changeset
|
1472 |
by (auto intro: inj_of_nat injD) |
d6cb7e625d75
more concise characterization of of_nat operation and class semiring_char_0
haftmann
parents:
37767
diff
changeset
|
1473 |
|
63110 | 1474 |
text \<open>Special cases where either operand is zero\<close> |
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1475 |
|
54147
97a8ff4e4ac9
killed most "no_atp", to make Sledgehammer more complete
blanchet
parents:
53986
diff
changeset
|
1476 |
lemma of_nat_0_eq_iff [simp]: "0 = of_nat n \<longleftrightarrow> 0 = n" |
38621
d6cb7e625d75
more concise characterization of of_nat operation and class semiring_char_0
haftmann
parents:
37767
diff
changeset
|
1477 |
by (fact of_nat_eq_iff [of 0 n, unfolded of_nat_0]) |
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1478 |
|
54147
97a8ff4e4ac9
killed most "no_atp", to make Sledgehammer more complete
blanchet
parents:
53986
diff
changeset
|
1479 |
lemma of_nat_eq_0_iff [simp]: "of_nat m = 0 \<longleftrightarrow> m = 0" |
38621
d6cb7e625d75
more concise characterization of of_nat operation and class semiring_char_0
haftmann
parents:
37767
diff
changeset
|
1480 |
by (fact of_nat_eq_iff [of m 0, unfolded of_nat_0]) |
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1481 |
|
60353
838025c6e278
implicit partial divison operation in integral domains
haftmann
parents:
60175
diff
changeset
|
1482 |
lemma of_nat_neq_0 [simp]: |
838025c6e278
implicit partial divison operation in integral domains
haftmann
parents:
60175
diff
changeset
|
1483 |
"of_nat (Suc n) \<noteq> 0" |
838025c6e278
implicit partial divison operation in integral domains
haftmann
parents:
60175
diff
changeset
|
1484 |
unfolding of_nat_eq_0_iff by simp |
838025c6e278
implicit partial divison operation in integral domains
haftmann
parents:
60175
diff
changeset
|
1485 |
|
838025c6e278
implicit partial divison operation in integral domains
haftmann
parents:
60175
diff
changeset
|
1486 |
lemma of_nat_0_neq [simp]: |
838025c6e278
implicit partial divison operation in integral domains
haftmann
parents:
60175
diff
changeset
|
1487 |
"0 \<noteq> of_nat (Suc 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
|
1488 |
unfolding of_nat_0_eq_iff by simp |
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
|
1489 |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1490 |
end |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1491 |
|
62481
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1492 |
class ring_char_0 = ring_1 + semiring_char_0 |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1493 |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34208
diff
changeset
|
1494 |
context linordered_semidom |
25193 | 1495 |
begin |
1496 |
||
47489 | 1497 |
lemma of_nat_0_le_iff [simp]: "0 \<le> of_nat n" |
1498 |
by (induct n) simp_all |
|
25193 | 1499 |
|
47489 | 1500 |
lemma of_nat_less_0_iff [simp]: "\<not> of_nat m < 0" |
1501 |
by (simp add: not_less) |
|
25193 | 1502 |
|
1503 |
lemma of_nat_less_iff [simp]: "of_nat m < of_nat n \<longleftrightarrow> m < n" |
|
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
|
1504 |
by (induct m n rule: diff_induct) (simp_all add: add_pos_nonneg) |
25193 | 1505 |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1506 |
lemma of_nat_le_iff [simp]: "of_nat m \<le> of_nat n \<longleftrightarrow> m \<le> n" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1507 |
by (simp add: not_less [symmetric] linorder_not_less [symmetric]) |
25193 | 1508 |
|
47489 | 1509 |
lemma less_imp_of_nat_less: "m < n \<Longrightarrow> of_nat m < of_nat n" |
1510 |
by simp |
|
1511 |
||
1512 |
lemma of_nat_less_imp_less: "of_nat m < of_nat n \<Longrightarrow> m < n" |
|
1513 |
by simp |
|
1514 |
||
63110 | 1515 |
text \<open>Every \<open>linordered_semidom\<close> has characteristic zero.\<close> |
1516 |
||
1517 |
subclass semiring_char_0 |
|
1518 |
by standard (auto intro!: injI simp add: eq_iff) |
|
1519 |
||
1520 |
text \<open>Special cases where either operand is zero\<close> |
|
25193 | 1521 |
|
54147
97a8ff4e4ac9
killed most "no_atp", to make Sledgehammer more complete
blanchet
parents:
53986
diff
changeset
|
1522 |
lemma of_nat_le_0_iff [simp]: "of_nat m \<le> 0 \<longleftrightarrow> m = 0" |
25193 | 1523 |
by (rule of_nat_le_iff [of _ 0, simplified]) |
1524 |
||
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1525 |
lemma of_nat_0_less_iff [simp]: "0 < of_nat n \<longleftrightarrow> 0 < n" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1526 |
by (rule of_nat_less_iff [of 0, simplified]) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1527 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1528 |
end |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1529 |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
34208
diff
changeset
|
1530 |
context linordered_idom |
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1531 |
begin |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1532 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1533 |
lemma abs_of_nat [simp]: "\<bar>of_nat n\<bar> = of_nat n" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1534 |
unfolding abs_if by auto |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1535 |
|
25193 | 1536 |
end |
1537 |
||
1538 |
lemma of_nat_id [simp]: "of_nat n = n" |
|
35216 | 1539 |
by (induct n) simp_all |
25193 | 1540 |
|
1541 |
lemma of_nat_eq_id [simp]: "of_nat = id" |
|
39302
d7728f65b353
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents:
39198
diff
changeset
|
1542 |
by (auto simp add: fun_eq_iff) |
25193 | 1543 |
|
1544 |
||
60758 | 1545 |
subsection \<open>The set of natural numbers\<close> |
25193 | 1546 |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1547 |
context semiring_1 |
25193 | 1548 |
begin |
1549 |
||
61070 | 1550 |
definition Nats :: "'a set" ("\<nat>") |
1551 |
where "\<nat> = range of_nat" |
|
25193 | 1552 |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1553 |
lemma of_nat_in_Nats [simp]: "of_nat n \<in> \<nat>" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1554 |
by (simp add: Nats_def) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1555 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1556 |
lemma Nats_0 [simp]: "0 \<in> \<nat>" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1557 |
apply (simp add: Nats_def) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1558 |
apply (rule range_eqI) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1559 |
apply (rule of_nat_0 [symmetric]) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1560 |
done |
25193 | 1561 |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1562 |
lemma Nats_1 [simp]: "1 \<in> \<nat>" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1563 |
apply (simp add: Nats_def) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1564 |
apply (rule range_eqI) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1565 |
apply (rule of_nat_1 [symmetric]) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1566 |
done |
25193 | 1567 |
|
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1568 |
lemma Nats_add [simp]: "a \<in> \<nat> \<Longrightarrow> b \<in> \<nat> \<Longrightarrow> a + b \<in> \<nat>" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1569 |
apply (auto simp add: Nats_def) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1570 |
apply (rule range_eqI) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1571 |
apply (rule of_nat_add [symmetric]) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1572 |
done |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1573 |
|
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1574 |
lemma Nats_mult [simp]: "a \<in> \<nat> \<Longrightarrow> b \<in> \<nat> \<Longrightarrow> a * b \<in> \<nat>" |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1575 |
apply (auto simp add: Nats_def) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1576 |
apply (rule range_eqI) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1577 |
apply (rule of_nat_mult [symmetric]) |
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25928
diff
changeset
|
1578 |
done |
25193 | 1579 |
|
35633 | 1580 |
lemma Nats_cases [cases set: Nats]: |
1581 |
assumes "x \<in> \<nat>" |
|
1582 |
obtains (of_nat) n where "x = of_nat n" |
|
1583 |
unfolding Nats_def |
|
1584 |
proof - |
|
60758 | 1585 |
from \<open>x \<in> \<nat>\<close> have "x \<in> range of_nat" unfolding Nats_def . |
35633 | 1586 |
then obtain n where "x = of_nat n" .. |
1587 |
then show thesis .. |
|
1588 |
qed |
|
1589 |
||
1590 |
lemma Nats_induct [case_names of_nat, induct set: Nats]: |
|
1591 |
"x \<in> \<nat> \<Longrightarrow> (\<And>n. P (of_nat n)) \<Longrightarrow> P x" |
|
1592 |
by (rule Nats_cases) auto |
|
1593 |
||
25193 | 1594 |
end |
1595 |
||
1596 |
||
60758 | 1597 |
subsection \<open>Further arithmetic facts concerning the natural numbers\<close> |
21243 | 1598 |
|
22845 | 1599 |
lemma subst_equals: |
63110 | 1600 |
assumes "t = s" and "u = t" |
22845 | 1601 |
shows "u = s" |
63110 | 1602 |
using assms(2,1) by (rule trans) |
22845 | 1603 |
|
48891 | 1604 |
ML_file "Tools/nat_arith.ML" |
48559
686cc7c47589
give Nat_Arith simprocs proper name bindings by using simproc_setup
huffman
parents:
47988
diff
changeset
|
1605 |
|
686cc7c47589
give Nat_Arith simprocs proper name bindings by using simproc_setup
huffman
parents:
47988
diff
changeset
|
1606 |
simproc_setup nateq_cancel_sums |
686cc7c47589
give Nat_Arith simprocs proper name bindings by using simproc_setup
huffman
parents:
47988
diff
changeset
|
1607 |
("(l::nat) + m = n" | "(l::nat) = m + n" | "Suc m = n" | "m = Suc n") = |
60758 | 1608 |
\<open>fn phi => try o Nat_Arith.cancel_eq_conv\<close> |
48559
686cc7c47589
give Nat_Arith simprocs proper name bindings by using simproc_setup
huffman
parents:
47988
diff
changeset
|
1609 |
|
686cc7c47589
give Nat_Arith simprocs proper name bindings by using simproc_setup
huffman
parents:
47988
diff
changeset
|
1610 |
simproc_setup natless_cancel_sums |
686cc7c47589
give Nat_Arith simprocs proper name bindings by using simproc_setup
huffman
parents:
47988
diff
changeset
|
1611 |
("(l::nat) + m < n" | "(l::nat) < m + n" | "Suc m < n" | "m < Suc n") = |
60758 | 1612 |
\<open>fn phi => try o Nat_Arith.cancel_less_conv\<close> |
48559
686cc7c47589
give Nat_Arith simprocs proper name bindings by using simproc_setup
huffman
parents:
47988
diff
changeset
|
1613 |
|
686cc7c47589
give Nat_Arith simprocs proper name bindings by using simproc_setup
huffman
parents:
47988
diff
changeset
|
1614 |
simproc_setup natle_cancel_sums |
686cc7c47589
give Nat_Arith simprocs proper name bindings by using simproc_setup
huffman
parents:
47988
diff
changeset
|
1615 |
("(l::nat) + m \<le> n" | "(l::nat) \<le> m + n" | "Suc m \<le> n" | "m \<le> Suc n") = |
60758 | 1616 |
\<open>fn phi => try o Nat_Arith.cancel_le_conv\<close> |
48559
686cc7c47589
give Nat_Arith simprocs proper name bindings by using simproc_setup
huffman
parents:
47988
diff
changeset
|
1617 |
|
686cc7c47589
give Nat_Arith simprocs proper name bindings by using simproc_setup
huffman
parents:
47988
diff
changeset
|
1618 |
simproc_setup natdiff_cancel_sums |
686cc7c47589
give Nat_Arith simprocs proper name bindings by using simproc_setup
huffman
parents:
47988
diff
changeset
|
1619 |
("(l::nat) + m - n" | "(l::nat) - (m + n)" | "Suc m - n" | "m - Suc n") = |
60758 | 1620 |
\<open>fn phi => try o Nat_Arith.cancel_diff_conv\<close> |
24091 | 1621 |
|
27625 | 1622 |
context order |
1623 |
begin |
|
1624 |
||
1625 |
lemma lift_Suc_mono_le: |
|
53986 | 1626 |
assumes mono: "\<And>n. f n \<le> f (Suc n)" and "n \<le> n'" |
27627 | 1627 |
shows "f n \<le> f n'" |
1628 |
proof (cases "n < n'") |
|
1629 |
case True |
|
53986 | 1630 |
then show ?thesis |
62683 | 1631 |
by (induct n n' rule: less_Suc_induct) (auto intro: mono) |
63110 | 1632 |
next |
1633 |
case False |
|
1634 |
with \<open>n \<le> n'\<close> show ?thesis by auto |
|
1635 |
qed |
|
27625 | 1636 |
|
56020
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
55642
diff
changeset
|
1637 |
lemma lift_Suc_antimono_le: |
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
55642
diff
changeset
|
1638 |
assumes mono: "\<And>n. f n \<ge> f (Suc n)" and "n \<le> n'" |
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
55642
diff
changeset
|
1639 |
shows "f n \<ge> f n'" |
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
55642
diff
changeset
|
1640 |
proof (cases "n < n'") |
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
55642
diff
changeset
|
1641 |
case True |
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
55642
diff
changeset
|
1642 |
then show ?thesis |
62683 | 1643 |
by (induct n n' rule: less_Suc_induct) (auto intro: mono) |
63110 | 1644 |
next |
1645 |
case False |
|
1646 |
with \<open>n \<le> n'\<close> show ?thesis by auto |
|
1647 |
qed |
|
56020
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
55642
diff
changeset
|
1648 |
|
27625 | 1649 |
lemma lift_Suc_mono_less: |
53986 | 1650 |
assumes mono: "\<And>n. f n < f (Suc n)" and "n < n'" |
27627 | 1651 |
shows "f n < f n'" |
63110 | 1652 |
using \<open>n < n'\<close> by (induct n n' rule: less_Suc_induct) (auto intro: mono) |
1653 |
||
1654 |
lemma lift_Suc_mono_less_iff: "(\<And>n. f n < f (Suc n)) \<Longrightarrow> f n < f m \<longleftrightarrow> n < m" |
|
53986 | 1655 |
by (blast intro: less_asym' lift_Suc_mono_less [of f] |
1656 |
dest: linorder_not_less[THEN iffD1] le_eq_less_or_eq [THEN iffD1]) |
|
27789 | 1657 |
|
27625 | 1658 |
end |
1659 |
||
63110 | 1660 |
lemma mono_iff_le_Suc: "mono f \<longleftrightarrow> (\<forall>n. f n \<le> f (Suc n))" |
37387
3581483cca6c
qualified types "+" and nat; qualified constants Ball, Bex, Suc, curry; modernized some specifications
haftmann
parents:
36977
diff
changeset
|
1661 |
unfolding mono_def by (auto intro: lift_Suc_mono_le [of f]) |
27625 | 1662 |
|
63110 | 1663 |
lemma antimono_iff_le_Suc: "antimono f \<longleftrightarrow> (\<forall>n. f (Suc n) \<le> f n)" |
56020
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
55642
diff
changeset
|
1664 |
unfolding antimono_def by (auto intro: lift_Suc_antimono_le [of f]) |
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
55642
diff
changeset
|
1665 |
|
27789 | 1666 |
lemma mono_nat_linear_lb: |
53986 | 1667 |
fixes f :: "nat \<Rightarrow> nat" |
1668 |
assumes "\<And>m n. m < n \<Longrightarrow> f m < f n" |
|
1669 |
shows "f m + k \<le> f (m + k)" |
|
1670 |
proof (induct k) |
|
63110 | 1671 |
case 0 |
1672 |
then show ?case by simp |
|
53986 | 1673 |
next |
1674 |
case (Suc k) |
|
1675 |
then have "Suc (f m + k) \<le> Suc (f (m + k))" by simp |
|
1676 |
also from assms [of "m + k" "Suc (m + k)"] have "Suc (f (m + k)) \<le> f (Suc (m + k))" |
|
1677 |
by (simp add: Suc_le_eq) |
|
1678 |
finally show ?case by simp |
|
1679 |
qed |
|
27789 | 1680 |
|
1681 |
||
63110 | 1682 |
text \<open>Subtraction laws, mostly by Clemens Ballarin\<close> |
21243 | 1683 |
|
62481
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1684 |
lemma diff_less_mono: |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1685 |
fixes a b c :: nat |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1686 |
assumes "a < b" and "c \<le> a" |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1687 |
shows "a - c < b - c" |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1688 |
proof - |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1689 |
from assms obtain d e where "b = c + (d + e)" and "a = c + e" and "d > 0" |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1690 |
by (auto dest!: le_Suc_ex less_imp_Suc_add simp add: ac_simps) |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1691 |
then show ?thesis by simp |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1692 |
qed |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1693 |
|
63110 | 1694 |
lemma less_diff_conv: "i < j - k \<longleftrightarrow> i + k < j" for i j k :: nat |
1695 |
by (cases "k \<le> j") (auto simp add: not_le dest: less_imp_Suc_add le_Suc_ex) |
|
1696 |
||
1697 |
lemma less_diff_conv2: "k \<le> j \<Longrightarrow> j - k < i \<longleftrightarrow> j < i + k" for j k i :: nat |
|
62481
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1698 |
by (auto dest: le_Suc_ex) |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1699 |
|
63110 | 1700 |
lemma le_diff_conv: "j - k \<le> i \<longleftrightarrow> j \<le> i + k" for j k i :: nat |
1701 |
by (cases "k \<le> j") (auto simp add: not_le dest!: less_imp_Suc_add le_Suc_ex) |
|
1702 |
||
1703 |
lemma diff_diff_cancel [simp]: "i \<le> n \<Longrightarrow> n - (n - i) = i" for i n :: nat |
|
1704 |
by (auto dest: le_Suc_ex) |
|
1705 |
||
1706 |
lemma diff_less [simp]: "0 < n \<Longrightarrow> 0 < m \<Longrightarrow> m - n < m" for i n :: nat |
|
62481
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1707 |
by (auto dest: less_imp_Suc_add) |
21243 | 1708 |
|
60758 | 1709 |
text \<open>Simplification of relational expressions involving subtraction\<close> |
21243 | 1710 |
|
63110 | 1711 |
lemma diff_diff_eq: "k \<le> m \<Longrightarrow> k \<le> n \<Longrightarrow> m - k - (n - k) = m - n" for m n k :: nat |
62481
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1712 |
by (auto dest!: le_Suc_ex) |
21243 | 1713 |
|
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
|
1714 |
hide_fact (open) diff_diff_eq |
35064
1bdef0c013d3
hide fact names clashing with fact names from Group.thy
haftmann
parents:
35047
diff
changeset
|
1715 |
|
63110 | 1716 |
lemma eq_diff_iff: "k \<le> m \<Longrightarrow> k \<le> n \<Longrightarrow> m - k = n - k \<longleftrightarrow> m = n" for m n k :: nat |
62481
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1717 |
by (auto dest: le_Suc_ex) |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1718 |
|
63110 | 1719 |
lemma less_diff_iff: "k \<le> m \<Longrightarrow> k \<le> n \<Longrightarrow> m - k < n - k \<longleftrightarrow> m < n" for m n k :: nat |
62481
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1720 |
by (auto dest!: le_Suc_ex) |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1721 |
|
63110 | 1722 |
lemma le_diff_iff: "k \<le> m \<Longrightarrow> k \<le> n \<Longrightarrow> m - k \<le> n - k \<longleftrightarrow> m \<le> n" for m n k :: nat |
62481
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1723 |
by (auto dest!: le_Suc_ex) |
21243 | 1724 |
|
63110 | 1725 |
lemma le_diff_iff': "a \<le> c \<Longrightarrow> b \<le> c \<Longrightarrow> c - a \<le> c - b \<longleftrightarrow> b \<le> a" for a b c :: nat |
63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
63040
diff
changeset
|
1726 |
by (force dest: le_Suc_ex) |
63110 | 1727 |
|
1728 |
||
1729 |
text \<open>(Anti)Monotonicity of subtraction -- by Stephan Merz\<close> |
|
1730 |
||
1731 |
lemma diff_le_mono: "m \<le> n \<Longrightarrow> m - l \<le> n - l" for m n l :: nat |
|
62481
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1732 |
by (auto dest: less_imp_le less_imp_Suc_add split add: nat_diff_split) |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1733 |
|
63110 | 1734 |
lemma diff_le_mono2: "m \<le> n \<Longrightarrow> l - n \<le> l - m" for m n l :: nat |
62481
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1735 |
by (auto dest: less_imp_le le_Suc_ex less_imp_Suc_add less_le_trans split add: nat_diff_split) |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1736 |
|
63110 | 1737 |
lemma diff_less_mono2: "m < n \<Longrightarrow> m < l \<Longrightarrow> l - n < l - m" for m n l :: nat |
62481
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1738 |
by (auto dest: less_imp_Suc_add split add: nat_diff_split) |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1739 |
|
63110 | 1740 |
lemma diffs0_imp_equal: "m - n = 0 \<Longrightarrow> n - m = 0 \<Longrightarrow> m = n" for m n :: nat |
62481
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1741 |
by (simp split add: nat_diff_split) |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1742 |
|
63110 | 1743 |
lemma min_diff: "min (m - i) (n - i) = min m n - i" for m n i :: nat |
62481
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1744 |
by (cases m n rule: le_cases) |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1745 |
(auto simp add: not_le min.absorb1 min.absorb2 min.absorb_iff1 [symmetric] diff_le_mono) |
26143
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26101
diff
changeset
|
1746 |
|
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
|
1747 |
lemma inj_on_diff_nat: |
63110 | 1748 |
fixes k :: nat |
1749 |
assumes "\<forall>n \<in> N. k \<le> n" |
|
26143
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26101
diff
changeset
|
1750 |
shows "inj_on (\<lambda>n. n - k) N" |
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26101
diff
changeset
|
1751 |
proof (rule inj_onI) |
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26101
diff
changeset
|
1752 |
fix x y |
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26101
diff
changeset
|
1753 |
assume a: "x \<in> N" "y \<in> N" "x - k = y - k" |
63110 | 1754 |
with assms have "x - k + k = y - k + k" by auto |
1755 |
with a assms show "x = y" by (auto simp add: eq_diff_iff) |
|
26143
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26101
diff
changeset
|
1756 |
qed |
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26101
diff
changeset
|
1757 |
|
63110 | 1758 |
text \<open>Rewriting to pull differences out\<close> |
1759 |
||
1760 |
lemma diff_diff_right [simp]: "k \<le> j \<Longrightarrow> i - (j - k) = i + k - j" for i j k :: nat |
|
62481
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1761 |
by (fact diff_diff_right) |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1762 |
|
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1763 |
lemma diff_Suc_diff_eq1 [simp]: |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1764 |
assumes "k \<le> j" |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1765 |
shows "i - Suc (j - k) = i + k - Suc j" |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1766 |
proof - |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1767 |
from assms have *: "Suc (j - k) = Suc j - k" |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1768 |
by (simp add: Suc_diff_le) |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1769 |
from assms have "k \<le> Suc j" |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1770 |
by (rule order_trans) simp |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1771 |
with diff_diff_right [of k "Suc j" i] * show ?thesis |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1772 |
by simp |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1773 |
qed |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1774 |
|
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1775 |
lemma diff_Suc_diff_eq2 [simp]: |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1776 |
assumes "k \<le> j" |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1777 |
shows "Suc (j - k) - i = Suc j - (k + i)" |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1778 |
proof - |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1779 |
from assms obtain n where "j = k + n" |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1780 |
by (auto dest: le_Suc_ex) |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1781 |
moreover have "Suc n - i = (k + Suc n) - (k + i)" |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1782 |
using add_diff_cancel_left [of k "Suc n" i] by simp |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1783 |
ultimately show ?thesis by simp |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1784 |
qed |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1785 |
|
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1786 |
lemma Suc_diff_Suc: |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1787 |
assumes "n < m" |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1788 |
shows "Suc (m - Suc n) = m - n" |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1789 |
proof - |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1790 |
from assms obtain q where "m = n + Suc q" |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1791 |
by (auto dest: less_imp_Suc_add) |
63040 | 1792 |
moreover define r where "r = Suc q" |
62481
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1793 |
ultimately have "Suc (m - Suc n) = r" and "m = n + r" |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1794 |
by simp_all |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1795 |
then show ?thesis by simp |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1796 |
qed |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1797 |
|
63110 | 1798 |
lemma one_less_mult: "Suc 0 < n \<Longrightarrow> Suc 0 < m \<Longrightarrow> Suc 0 < m * n" |
62481
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1799 |
using less_1_mult [of n m] by (simp add: ac_simps) |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1800 |
|
63110 | 1801 |
lemma n_less_m_mult_n: "0 < n \<Longrightarrow> Suc 0 < m \<Longrightarrow> n < m * n" |
62481
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1802 |
using mult_strict_right_mono [of 1 m n] by simp |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1803 |
|
63110 | 1804 |
lemma n_less_n_mult_m: "0 < n \<Longrightarrow> Suc 0 < m \<Longrightarrow> n < n * m" |
62481
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1805 |
using mult_strict_left_mono [of 1 m n] by simp |
21243 | 1806 |
|
63110 | 1807 |
|
60758 | 1808 |
text \<open>Specialized induction principles that work "backwards":\<close> |
23001
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1809 |
|
62481
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1810 |
lemma inc_induct [consumes 1, case_names base step]: |
54411 | 1811 |
assumes less: "i \<le> j" |
63110 | 1812 |
and base: "P j" |
1813 |
and step: "\<And>n. i \<le> n \<Longrightarrow> n < j \<Longrightarrow> P (Suc n) \<Longrightarrow> P n" |
|
23001
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1814 |
shows "P i" |
54411 | 1815 |
using less step |
62481
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1816 |
proof (induct "j - i" arbitrary: i) |
23001
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1817 |
case (0 i) |
62481
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1818 |
then have "i = j" by simp |
23001
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1819 |
with base show ?case by simp |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1820 |
next |
54411 | 1821 |
case (Suc d n) |
62481
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1822 |
from Suc.hyps have "n \<noteq> j" by auto |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1823 |
with Suc have "n < j" by (simp add: less_le) |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1824 |
from \<open>Suc d = j - n\<close> have "d + 1 = j - n" by simp |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1825 |
then have "d + 1 - 1 = j - n - 1" by simp |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1826 |
then have "d = j - n - 1" by simp |
63110 | 1827 |
then have "d = j - (n + 1)" |
62481
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1828 |
by (simp add: diff_diff_eq) |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1829 |
then have "d = j - Suc n" |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1830 |
by simp |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1831 |
moreover from \<open>n < j\<close> have "Suc n \<le> j" |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1832 |
by (simp add: Suc_le_eq) |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1833 |
ultimately have "P (Suc n)" |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1834 |
proof (rule Suc.hyps) |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1835 |
fix q |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1836 |
assume "Suc n \<le> q" |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1837 |
then have "n \<le> q" by (simp add: Suc_le_eq less_imp_le) |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1838 |
moreover assume "q < j" |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1839 |
moreover assume "P (Suc q)" |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1840 |
ultimately show "P q" |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1841 |
by (rule Suc.prems) |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1842 |
qed |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1843 |
with order_refl \<open>n < j\<close> show "P n" |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1844 |
by (rule Suc.prems) |
23001
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1845 |
qed |
63110 | 1846 |
|
62481
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1847 |
lemma strict_inc_induct [consumes 1, case_names base step]: |
23001
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1848 |
assumes less: "i < j" |
63110 | 1849 |
and base: "\<And>i. j = Suc i \<Longrightarrow> P i" |
1850 |
and step: "\<And>i. i < j \<Longrightarrow> P (Suc i) \<Longrightarrow> P i" |
|
23001
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1851 |
shows "P i" |
62481
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1852 |
using less proof (induct "j - i - 1" arbitrary: i) |
23001
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1853 |
case (0 i) |
62481
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1854 |
from \<open>i < j\<close> obtain n where "j = i + n" and "n > 0" |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1855 |
by (auto dest!: less_imp_Suc_add) |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1856 |
with 0 have "j = Suc i" |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1857 |
by (auto intro: order_antisym simp add: Suc_le_eq) |
23001
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1858 |
with base show ?case by simp |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1859 |
next |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1860 |
case (Suc d i) |
62481
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1861 |
from \<open>Suc d = j - i - 1\<close> have *: "Suc d = j - Suc i" |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1862 |
by (simp add: diff_diff_add) |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1863 |
then have "Suc d - 1 = j - Suc i - 1" |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1864 |
by simp |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1865 |
then have "d = j - Suc i - 1" |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1866 |
by simp |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1867 |
moreover from * have "j - Suc i \<noteq> 0" |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1868 |
by auto |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1869 |
then have "Suc i < j" |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1870 |
by (simp add: not_le) |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1871 |
ultimately have "P (Suc i)" |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1872 |
by (rule Suc.hyps) |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1873 |
with \<open>i < j\<close> show "P i" by (rule step) |
23001
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1874 |
qed |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1875 |
|
63110 | 1876 |
lemma zero_induct_lemma: "P k \<Longrightarrow> (\<And>n. P (Suc n) \<Longrightarrow> P n) \<Longrightarrow> P (k - i)" |
23001
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1877 |
using inc_induct[of "k - i" k P, simplified] by blast |
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1878 |
|
63110 | 1879 |
lemma zero_induct: "P k \<Longrightarrow> (\<And>n. P (Suc n) \<Longrightarrow> P n) \<Longrightarrow> P 0" |
23001
3608f0362a91
added induction principles for induction "backwards": P (Suc n) ==> P n
krauss
parents:
22920
diff
changeset
|
1880 |
using inc_induct[of 0 k P] by blast |
21243 | 1881 |
|
60758 | 1882 |
text \<open>Further induction rule similar to @{thm inc_induct}\<close> |
27625 | 1883 |
|
62481
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1884 |
lemma dec_induct [consumes 1, case_names base step]: |
54411 | 1885 |
"i \<le> j \<Longrightarrow> P i \<Longrightarrow> (\<And>n. i \<le> n \<Longrightarrow> n < j \<Longrightarrow> P n \<Longrightarrow> P (Suc n)) \<Longrightarrow> P j" |
62481
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1886 |
proof (induct j arbitrary: i) |
63110 | 1887 |
case 0 |
1888 |
then show ?case by simp |
|
62481
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1889 |
next |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1890 |
case (Suc j) |
63110 | 1891 |
from Suc.prems consider "i \<le> j" | "i = Suc j" |
1892 |
by (auto simp add: le_Suc_eq) |
|
1893 |
then show ?case |
|
1894 |
proof cases |
|
1895 |
case 1 |
|
62481
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1896 |
moreover have "j < Suc j" by simp |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1897 |
moreover have "P j" using \<open>i \<le> j\<close> \<open>P i\<close> |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1898 |
proof (rule Suc.hyps) |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1899 |
fix q |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1900 |
assume "i \<le> q" |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1901 |
moreover assume "q < j" then have "q < Suc j" |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1902 |
by (simp add: less_Suc_eq) |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1903 |
moreover assume "P q" |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1904 |
ultimately show "P (Suc q)" |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1905 |
by (rule Suc.prems) |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1906 |
qed |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1907 |
ultimately show "P (Suc j)" |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1908 |
by (rule Suc.prems) |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1909 |
next |
63110 | 1910 |
case 2 |
62481
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1911 |
with \<open>P i\<close> show "P (Suc j)" by simp |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1912 |
qed |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1913 |
qed |
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1914 |
|
59000 | 1915 |
|
63110 | 1916 |
subsection \<open>Monotonicity of \<open>funpow\<close>\<close> |
59000 | 1917 |
|
1918 |
lemma funpow_increasing: |
|
63110 | 1919 |
fixes f :: "'a \<Rightarrow> 'a::{lattice,order_top}" |
59000 | 1920 |
shows "m \<le> n \<Longrightarrow> mono f \<Longrightarrow> (f ^^ n) \<top> \<le> (f ^^ m) \<top>" |
1921 |
by (induct rule: inc_induct) |
|
1922 |
(auto simp del: funpow.simps(2) simp add: funpow_Suc_right |
|
1923 |
intro: order_trans[OF _ funpow_mono]) |
|
1924 |
||
1925 |
lemma funpow_decreasing: |
|
63110 | 1926 |
fixes f :: "'a \<Rightarrow> 'a::{lattice,order_bot}" |
59000 | 1927 |
shows "m \<le> n \<Longrightarrow> mono f \<Longrightarrow> (f ^^ m) \<bottom> \<le> (f ^^ n) \<bottom>" |
1928 |
by (induct rule: dec_induct) |
|
1929 |
(auto simp del: funpow.simps(2) simp add: funpow_Suc_right |
|
1930 |
intro: order_trans[OF _ funpow_mono]) |
|
1931 |
||
1932 |
lemma mono_funpow: |
|
63110 | 1933 |
fixes Q :: "'a::{lattice,order_bot} \<Rightarrow> 'a" |
59000 | 1934 |
shows "mono Q \<Longrightarrow> mono (\<lambda>i. (Q ^^ i) \<bottom>)" |
1935 |
by (auto intro!: funpow_decreasing simp: mono_def) |
|
58377
c6f93b8d2d8e
moved old 'size' generator together with 'old_datatype'
blanchet
parents:
58306
diff
changeset
|
1936 |
|
60175 | 1937 |
lemma antimono_funpow: |
63110 | 1938 |
fixes Q :: "'a::{lattice,order_top} \<Rightarrow> 'a" |
60175 | 1939 |
shows "mono Q \<Longrightarrow> antimono (\<lambda>i. (Q ^^ i) \<top>)" |
1940 |
by (auto intro!: funpow_increasing simp: antimono_def) |
|
1941 |
||
63110 | 1942 |
|
60758 | 1943 |
subsection \<open>The divides relation on @{typ nat}\<close> |
33274
b6ff7db522b5
moved lemmas for dvd on nat to theories Nat and Power
haftmann
parents:
32772
diff
changeset
|
1944 |
|
63110 | 1945 |
lemma dvd_1_left [iff]: "Suc 0 dvd k" |
62365 | 1946 |
by (simp add: dvd_def) |
1947 |
||
63110 | 1948 |
lemma dvd_1_iff_1 [simp]: "m dvd Suc 0 \<longleftrightarrow> m = Suc 0" |
62365 | 1949 |
by (simp add: dvd_def) |
1950 |
||
63110 | 1951 |
lemma nat_dvd_1_iff_1 [simp]: "m dvd 1 \<longleftrightarrow> m = 1" for m :: nat |
62365 | 1952 |
by (simp add: dvd_def) |
1953 |
||
63110 | 1954 |
lemma dvd_antisym: "m dvd n \<Longrightarrow> n dvd m \<Longrightarrow> m = n" for m n :: nat |
1955 |
unfolding dvd_def by (force dest: mult_eq_self_implies_10 simp add: mult.assoc) |
|
1956 |
||
1957 |
lemma dvd_diff_nat [simp]: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd (m - n)" for k m n :: nat |
|
1958 |
unfolding dvd_def by (blast intro: right_diff_distrib' [symmetric]) |
|
1959 |
||
1960 |
lemma dvd_diffD: "k dvd m - n \<Longrightarrow> k dvd n \<Longrightarrow> n \<le> m \<Longrightarrow> k dvd m" for k m n :: nat |
|
33274
b6ff7db522b5
moved lemmas for dvd on nat to theories Nat and Power
haftmann
parents:
32772
diff
changeset
|
1961 |
apply (erule linorder_not_less [THEN iffD2, THEN add_diff_inverse, THEN subst]) |
b6ff7db522b5
moved lemmas for dvd on nat to theories Nat and Power
haftmann
parents:
32772
diff
changeset
|
1962 |
apply (blast intro: dvd_add) |
b6ff7db522b5
moved lemmas for dvd on nat to theories Nat and Power
haftmann
parents:
32772
diff
changeset
|
1963 |
done |
b6ff7db522b5
moved lemmas for dvd on nat to theories Nat and Power
haftmann
parents:
32772
diff
changeset
|
1964 |
|
63110 | 1965 |
lemma dvd_diffD1: "k dvd m - n \<Longrightarrow> k dvd m \<Longrightarrow> n \<le> m \<Longrightarrow> k dvd n" for k m n :: nat |
62365 | 1966 |
by (drule_tac m = m in dvd_diff_nat) auto |
1967 |
||
1968 |
lemma dvd_mult_cancel: |
|
1969 |
fixes m n k :: nat |
|
1970 |
assumes "k * m dvd k * n" and "0 < k" |
|
1971 |
shows "m dvd n" |
|
1972 |
proof - |
|
1973 |
from assms(1) obtain q where "k * n = (k * m) * q" .. |
|
1974 |
then have "k * n = k * (m * q)" by (simp add: ac_simps) |
|
62481
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
1975 |
with \<open>0 < k\<close> have "n = m * q" by (auto simp add: mult_left_cancel) |
62365 | 1976 |
then show ?thesis .. |
1977 |
qed |
|
63110 | 1978 |
|
1979 |
lemma dvd_mult_cancel1: "0 < m \<Longrightarrow> m * n dvd m \<longleftrightarrow> n = 1" for m n :: nat |
|
33274
b6ff7db522b5
moved lemmas for dvd on nat to theories Nat and Power
haftmann
parents:
32772
diff
changeset
|
1980 |
apply auto |
63110 | 1981 |
apply (subgoal_tac "m * n dvd m * 1") |
33274
b6ff7db522b5
moved lemmas for dvd on nat to theories Nat and Power
haftmann
parents:
32772
diff
changeset
|
1982 |
apply (drule dvd_mult_cancel, auto) |
b6ff7db522b5
moved lemmas for dvd on nat to theories Nat and Power
haftmann
parents:
32772
diff
changeset
|
1983 |
done |
b6ff7db522b5
moved lemmas for dvd on nat to theories Nat and Power
haftmann
parents:
32772
diff
changeset
|
1984 |
|
63110 | 1985 |
lemma dvd_mult_cancel2: "0 < m \<Longrightarrow> n * m dvd m \<longleftrightarrow> n = 1" for m n :: nat |
62365 | 1986 |
using dvd_mult_cancel1 [of m n] by (simp add: ac_simps) |
1987 |
||
63110 | 1988 |
lemma dvd_imp_le: "k dvd n \<Longrightarrow> 0 < n \<Longrightarrow> k \<le> n" for k n :: nat |
62365 | 1989 |
by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc) |
33274
b6ff7db522b5
moved lemmas for dvd on nat to theories Nat and Power
haftmann
parents:
32772
diff
changeset
|
1990 |
|
63110 | 1991 |
lemma nat_dvd_not_less: "0 < m \<Longrightarrow> m < n \<Longrightarrow> \<not> n dvd m" for m n :: nat |
62365 | 1992 |
by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc) |
33274
b6ff7db522b5
moved lemmas for dvd on nat to theories Nat and Power
haftmann
parents:
32772
diff
changeset
|
1993 |
|
54222 | 1994 |
lemma less_eq_dvd_minus: |
51173 | 1995 |
fixes m n :: nat |
54222 | 1996 |
assumes "m \<le> n" |
1997 |
shows "m dvd n \<longleftrightarrow> m dvd n - m" |
|
51173 | 1998 |
proof - |
54222 | 1999 |
from assms have "n = m + (n - m)" by simp |
51173 | 2000 |
then obtain q where "n = m + q" .. |
58647 | 2001 |
then show ?thesis by (simp add: add.commute [of m]) |
51173 | 2002 |
qed |
2003 |
||
63110 | 2004 |
lemma dvd_minus_self: "m dvd n - m \<longleftrightarrow> n < m \<or> m dvd n" for m n :: nat |
62481
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62378
diff
changeset
|
2005 |
by (cases "n < m") (auto elim!: dvdE simp add: not_less le_imp_diff_is_add dest: less_imp_le) |
51173 | 2006 |
|
2007 |
lemma dvd_minus_add: |
|
2008 |
fixes m n q r :: nat |
|
2009 |
assumes "q \<le> n" "q \<le> r * m" |
|
2010 |
shows "m dvd n - q \<longleftrightarrow> m dvd n + (r * m - q)" |
|
2011 |
proof - |
|
2012 |
have "m dvd n - q \<longleftrightarrow> m dvd r * m + (n - q)" |
|
58649
a62065b5e1e2
generalized and consolidated some theorems concerning divisibility
haftmann
parents:
58647
diff
changeset
|
2013 |
using dvd_add_times_triv_left_iff [of m r] by simp |
53374
a14d2a854c02
tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents:
52729
diff
changeset
|
2014 |
also from assms have "\<dots> \<longleftrightarrow> m dvd r * m + n - q" by simp |
a14d2a854c02
tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents:
52729
diff
changeset
|
2015 |
also from assms have "\<dots> \<longleftrightarrow> m dvd (r * m - q) + n" by simp |
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57492
diff
changeset
|
2016 |
also have "\<dots> \<longleftrightarrow> m dvd n + (r * m - q)" by (simp add: add.commute) |
51173 | 2017 |
finally show ?thesis . |
2018 |
qed |
|
2019 |
||
33274
b6ff7db522b5
moved lemmas for dvd on nat to theories Nat and Power
haftmann
parents:
32772
diff
changeset
|
2020 |
|
62365 | 2021 |
subsection \<open>Aliasses\<close> |
44817 | 2022 |
|
63110 | 2023 |
lemma nat_mult_1: "1 * n = n" for n :: nat |
58647 | 2024 |
by (fact mult_1_left) |
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
|
2025 |
|
63110 | 2026 |
lemma nat_mult_1_right: "n * 1 = n" for n :: nat |
58647 | 2027 |
by (fact mult_1_right) |
2028 |
||
63110 | 2029 |
lemma nat_add_left_cancel: "k + m = k + n \<longleftrightarrow> m = n" for k m n :: nat |
62365 | 2030 |
by (fact add_left_cancel) |
2031 |
||
63110 | 2032 |
lemma nat_add_right_cancel: "m + k = n + k \<longleftrightarrow> m = n" for k m n :: nat |
62365 | 2033 |
by (fact add_right_cancel) |
2034 |
||
63110 | 2035 |
lemma diff_mult_distrib: "(m - n) * k = (m * k) - (n * k)" for k m n :: nat |
62365 | 2036 |
by (fact left_diff_distrib') |
2037 |
||
63110 | 2038 |
lemma diff_mult_distrib2: "k * (m - n) = (k * m) - (k * n)" for k m n :: nat |
62365 | 2039 |
by (fact right_diff_distrib') |
2040 |
||
63110 | 2041 |
lemma le_add_diff: "k \<le> n \<Longrightarrow> m \<le> n + m - k" for k m n :: nat |
2042 |
by (fact le_add_diff) (* FIXME delete *) |
|
2043 |
||
2044 |
lemma le_diff_conv2: "k \<le> j \<Longrightarrow> (i \<le> j - k) = (i + k \<le> j)" for i j k :: nat |
|
2045 |
by (fact le_diff_conv2) (* FIXME delete *) |
|
2046 |
||
2047 |
lemma diff_self_eq_0 [simp]: "m - m = 0" for m :: nat |
|
62365 | 2048 |
by (fact diff_cancel) |
2049 |
||
63110 | 2050 |
lemma diff_diff_left [simp]: "i - j - k = i - (j + k)" for i j k :: nat |
62365 | 2051 |
by (fact diff_diff_add) |
2052 |
||
63110 | 2053 |
lemma diff_commute: "i - j - k = i - k - j" for i j k :: nat |
62365 | 2054 |
by (fact diff_right_commute) |
2055 |
||
63110 | 2056 |
lemma diff_add_inverse: "(n + m) - n = m" for m n :: nat |
62365 | 2057 |
by (fact add_diff_cancel_left') |
2058 |
||
63110 | 2059 |
lemma diff_add_inverse2: "(m + n) - n = m" for m n :: nat |
62365 | 2060 |
by (fact add_diff_cancel_right') |
2061 |
||
63110 | 2062 |
lemma diff_cancel: "(k + m) - (k + n) = m - n" for k m n :: nat |
62365 | 2063 |
by (fact add_diff_cancel_left) |
2064 |
||
63110 | 2065 |
lemma diff_cancel2: "(m + k) - (n + k) = m - n" for k m n :: nat |
62365 | 2066 |
by (fact add_diff_cancel_right) |
2067 |
||
63110 | 2068 |
lemma diff_add_0: "n - (n + m) = 0" for m n :: nat |
62365 | 2069 |
by (fact diff_add_zero) |
2070 |
||
63110 | 2071 |
lemma add_mult_distrib2: "k * (m + n) = (k * m) + (k * n)" for k m n :: nat |
62365 | 2072 |
by (fact distrib_left) |
2073 |
||
2074 |
lemmas nat_distrib = |
|
2075 |
add_mult_distrib distrib_left diff_mult_distrib diff_mult_distrib2 |
|
2076 |
||
44817 | 2077 |
|
60758 | 2078 |
subsection \<open>Size of a datatype value\<close> |
25193 | 2079 |
|
29608 | 2080 |
class size = |
61799 | 2081 |
fixes size :: "'a \<Rightarrow> nat" \<comment> \<open>see further theory \<open>Wellfounded\<close>\<close> |
23852 | 2082 |
|
58377
c6f93b8d2d8e
moved old 'size' generator together with 'old_datatype'
blanchet
parents:
58306
diff
changeset
|
2083 |
instantiation nat :: size |
c6f93b8d2d8e
moved old 'size' generator together with 'old_datatype'
blanchet
parents:
58306
diff
changeset
|
2084 |
begin |
c6f93b8d2d8e
moved old 'size' generator together with 'old_datatype'
blanchet
parents:
58306
diff
changeset
|
2085 |
|
63110 | 2086 |
definition size_nat where [simp, code]: "size (n::nat) = n" |
58377
c6f93b8d2d8e
moved old 'size' generator together with 'old_datatype'
blanchet
parents:
58306
diff
changeset
|
2087 |
|
c6f93b8d2d8e
moved old 'size' generator together with 'old_datatype'
blanchet
parents:
58306
diff
changeset
|
2088 |
instance .. |
c6f93b8d2d8e
moved old 'size' generator together with 'old_datatype'
blanchet
parents:
58306
diff
changeset
|
2089 |
|
c6f93b8d2d8e
moved old 'size' generator together with 'old_datatype'
blanchet
parents:
58306
diff
changeset
|
2090 |
end |
c6f93b8d2d8e
moved old 'size' generator together with 'old_datatype'
blanchet
parents:
58306
diff
changeset
|
2091 |
|
c6f93b8d2d8e
moved old 'size' generator together with 'old_datatype'
blanchet
parents:
58306
diff
changeset
|
2092 |
|
60758 | 2093 |
subsection \<open>Code module namespace\<close> |
33364 | 2094 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52289
diff
changeset
|
2095 |
code_identifier |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
52289
diff
changeset
|
2096 |
code_module Nat \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith |
33364 | 2097 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46351
diff
changeset
|
2098 |
hide_const (open) of_nat_aux |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46351
diff
changeset
|
2099 |
|
25193 | 2100 |
end |