20 done |
20 done |
21 |
21 |
22 (**Addition is the inverse of subtraction**) |
22 (**Addition is the inverse of subtraction**) |
23 |
23 |
24 (*We need m:nat even if we replace the RHS by natify(m), for consider e.g. |
24 (*We need m:nat even if we replace the RHS by natify(m), for consider e.g. |
25 n=2, m=omega; then n + (m-n) = 2 + (0-2) = 2 ~= 0 = natify(m).*) |
25 n=2, m=omega; then n + (m-n) = 2 + (0-2) = 2 \<noteq> 0 = natify(m).*) |
26 lemma add_diff_inverse: "[| n le m; m:nat |] ==> n #+ (m#-n) = m" |
26 lemma add_diff_inverse: "[| n \<le> m; m:nat |] ==> n #+ (m#-n) = m" |
27 apply (frule lt_nat_in_nat, erule nat_succI) |
27 apply (frule lt_nat_in_nat, erule nat_succI) |
28 apply (erule rev_mp) |
28 apply (erule rev_mp) |
29 apply (rule_tac m = m and n = n in diff_induct, auto) |
29 apply (rule_tac m = m and n = n in diff_induct, auto) |
30 done |
30 done |
31 |
31 |
32 lemma add_diff_inverse2: "[| n le m; m:nat |] ==> (m#-n) #+ n = m" |
32 lemma add_diff_inverse2: "[| n \<le> m; m:nat |] ==> (m#-n) #+ n = m" |
33 apply (frule lt_nat_in_nat, erule nat_succI) |
33 apply (frule lt_nat_in_nat, erule nat_succI) |
34 apply (simp (no_asm_simp) add: add_commute add_diff_inverse) |
34 apply (simp (no_asm_simp) add: add_commute add_diff_inverse) |
35 done |
35 done |
36 |
36 |
37 (*Proof is IDENTICAL to that of add_diff_inverse*) |
37 (*Proof is IDENTICAL to that of add_diff_inverse*) |
38 lemma diff_succ: "[| n le m; m:nat |] ==> succ(m) #- n = succ(m#-n)" |
38 lemma diff_succ: "[| n \<le> m; m:nat |] ==> succ(m) #- n = succ(m#-n)" |
39 apply (frule lt_nat_in_nat, erule nat_succI) |
39 apply (frule lt_nat_in_nat, erule nat_succI) |
40 apply (erule rev_mp) |
40 apply (erule rev_mp) |
41 apply (rule_tac m = m and n = n in diff_induct) |
41 apply (rule_tac m = m and n = n in diff_induct) |
42 apply (simp_all (no_asm_simp)) |
42 apply (simp_all (no_asm_simp)) |
43 done |
43 done |
63 |
63 |
64 |
64 |
65 subsection{*Remainder*} |
65 subsection{*Remainder*} |
66 |
66 |
67 (*We need m:nat even with natify*) |
67 (*We need m:nat even with natify*) |
68 lemma div_termination: "[| 0<n; n le m; m:nat |] ==> m #- n < m" |
68 lemma div_termination: "[| 0<n; n \<le> m; m:nat |] ==> m #- n < m" |
69 apply (frule lt_nat_in_nat, erule nat_succI) |
69 apply (frule lt_nat_in_nat, erule nat_succI) |
70 apply (erule rev_mp) |
70 apply (erule rev_mp) |
71 apply (erule rev_mp) |
71 apply (erule rev_mp) |
72 apply (rule_tac m = m and n = n in diff_induct) |
72 apply (rule_tac m = m and n = n in diff_induct) |
73 apply (simp_all (no_asm_simp) add: diff_le_self) |
73 apply (simp_all (no_asm_simp) add: diff_le_self) |
74 done |
74 done |
75 |
75 |
76 (*for mod and div*) |
76 (*for mod and div*) |
77 lemmas div_rls = |
77 lemmas div_rls = |
78 nat_typechecks Ord_transrec_type apply_funtype |
78 nat_typechecks Ord_transrec_type apply_funtype |
79 div_termination [THEN ltD] |
79 div_termination [THEN ltD] |
80 nat_into_Ord not_lt_iff_le [THEN iffD1] |
80 nat_into_Ord not_lt_iff_le [THEN iffD1] |
81 |
81 |
82 lemma raw_mod_type: "[| m:nat; n:nat |] ==> raw_mod (m, n) : nat" |
82 lemma raw_mod_type: "[| m:nat; n:nat |] ==> raw_mod (m, n) \<in> nat" |
83 apply (unfold raw_mod_def) |
83 apply (unfold raw_mod_def) |
84 apply (rule Ord_transrec_type) |
84 apply (rule Ord_transrec_type) |
85 apply (auto simp add: nat_into_Ord [THEN Ord_0_lt_iff]) |
85 apply (auto simp add: nat_into_Ord [THEN Ord_0_lt_iff]) |
86 apply (blast intro: div_rls) |
86 apply (blast intro: div_rls) |
87 done |
87 done |
88 |
88 |
89 lemma mod_type [TC,iff]: "m mod n : nat" |
89 lemma mod_type [TC,iff]: "m mod n \<in> nat" |
90 apply (unfold mod_def) |
90 apply (unfold mod_def) |
91 apply (simp (no_asm) add: mod_def raw_mod_type) |
91 apply (simp (no_asm) add: mod_def raw_mod_type) |
92 done |
92 done |
93 |
93 |
94 |
94 |
95 (** Aribtrary definitions for division by zero. Useful to simplify |
95 (** Aribtrary definitions for division by zero. Useful to simplify |
96 certain equations **) |
96 certain equations **) |
97 |
97 |
98 lemma DIVISION_BY_ZERO_DIV: "a div 0 = 0" |
98 lemma DIVISION_BY_ZERO_DIV: "a div 0 = 0" |
99 apply (unfold div_def) |
99 apply (unfold div_def) |
100 apply (rule raw_div_def [THEN def_transrec, THEN trans]) |
100 apply (rule raw_div_def [THEN def_transrec, THEN trans]) |
110 lemma raw_mod_less: "m<n ==> raw_mod (m,n) = m" |
110 lemma raw_mod_less: "m<n ==> raw_mod (m,n) = m" |
111 apply (rule raw_mod_def [THEN def_transrec, THEN trans]) |
111 apply (rule raw_mod_def [THEN def_transrec, THEN trans]) |
112 apply (simp (no_asm_simp) add: div_termination [THEN ltD]) |
112 apply (simp (no_asm_simp) add: div_termination [THEN ltD]) |
113 done |
113 done |
114 |
114 |
115 lemma mod_less [simp]: "[| m<n; n : nat |] ==> m mod n = m" |
115 lemma mod_less [simp]: "[| m<n; n \<in> nat |] ==> m mod n = m" |
116 apply (frule lt_nat_in_nat, assumption) |
116 apply (frule lt_nat_in_nat, assumption) |
117 apply (simp (no_asm_simp) add: mod_def raw_mod_less) |
117 apply (simp (no_asm_simp) add: mod_def raw_mod_less) |
118 done |
118 done |
119 |
119 |
120 lemma raw_mod_geq: |
120 lemma raw_mod_geq: |
121 "[| 0<n; n le m; m:nat |] ==> raw_mod (m, n) = raw_mod (m#-n, n)" |
121 "[| 0<n; n \<le> m; m:nat |] ==> raw_mod (m, n) = raw_mod (m#-n, n)" |
122 apply (frule lt_nat_in_nat, erule nat_succI) |
122 apply (frule lt_nat_in_nat, erule nat_succI) |
123 apply (rule raw_mod_def [THEN def_transrec, THEN trans]) |
123 apply (rule raw_mod_def [THEN def_transrec, THEN trans]) |
124 apply (simp (no_asm_simp) add: div_termination [THEN ltD] not_lt_iff_le [THEN iffD2], blast) |
124 apply (simp (no_asm_simp) add: div_termination [THEN ltD] not_lt_iff_le [THEN iffD2], blast) |
125 done |
125 done |
126 |
126 |
127 |
127 |
128 lemma mod_geq: "[| n le m; m:nat |] ==> m mod n = (m#-n) mod n" |
128 lemma mod_geq: "[| n \<le> m; m:nat |] ==> m mod n = (m#-n) mod n" |
129 apply (frule lt_nat_in_nat, erule nat_succI) |
129 apply (frule lt_nat_in_nat, erule nat_succI) |
130 apply (case_tac "n=0") |
130 apply (case_tac "n=0") |
131 apply (simp add: DIVISION_BY_ZERO_MOD) |
131 apply (simp add: DIVISION_BY_ZERO_MOD) |
132 apply (simp add: mod_def raw_mod_geq nat_into_Ord [THEN Ord_0_lt_iff]) |
132 apply (simp add: mod_def raw_mod_geq nat_into_Ord [THEN Ord_0_lt_iff]) |
133 done |
133 done |
134 |
134 |
135 |
135 |
136 subsection{*Division*} |
136 subsection{*Division*} |
137 |
137 |
138 lemma raw_div_type: "[| m:nat; n:nat |] ==> raw_div (m, n) : nat" |
138 lemma raw_div_type: "[| m:nat; n:nat |] ==> raw_div (m, n) \<in> nat" |
139 apply (unfold raw_div_def) |
139 apply (unfold raw_div_def) |
140 apply (rule Ord_transrec_type) |
140 apply (rule Ord_transrec_type) |
141 apply (auto simp add: nat_into_Ord [THEN Ord_0_lt_iff]) |
141 apply (auto simp add: nat_into_Ord [THEN Ord_0_lt_iff]) |
142 apply (blast intro: div_rls) |
142 apply (blast intro: div_rls) |
143 done |
143 done |
144 |
144 |
145 lemma div_type [TC,iff]: "m div n : nat" |
145 lemma div_type [TC,iff]: "m div n \<in> nat" |
146 apply (unfold div_def) |
146 apply (unfold div_def) |
147 apply (simp (no_asm) add: div_def raw_div_type) |
147 apply (simp (no_asm) add: div_def raw_div_type) |
148 done |
148 done |
149 |
149 |
150 lemma raw_div_less: "m<n ==> raw_div (m,n) = 0" |
150 lemma raw_div_less: "m<n ==> raw_div (m,n) = 0" |
151 apply (rule raw_div_def [THEN def_transrec, THEN trans]) |
151 apply (rule raw_div_def [THEN def_transrec, THEN trans]) |
152 apply (simp (no_asm_simp) add: div_termination [THEN ltD]) |
152 apply (simp (no_asm_simp) add: div_termination [THEN ltD]) |
153 done |
153 done |
154 |
154 |
155 lemma div_less [simp]: "[| m<n; n : nat |] ==> m div n = 0" |
155 lemma div_less [simp]: "[| m<n; n \<in> nat |] ==> m div n = 0" |
156 apply (frule lt_nat_in_nat, assumption) |
156 apply (frule lt_nat_in_nat, assumption) |
157 apply (simp (no_asm_simp) add: div_def raw_div_less) |
157 apply (simp (no_asm_simp) add: div_def raw_div_less) |
158 done |
158 done |
159 |
159 |
160 lemma raw_div_geq: "[| 0<n; n le m; m:nat |] ==> raw_div(m,n) = succ(raw_div(m#-n, n))" |
160 lemma raw_div_geq: "[| 0<n; n \<le> m; m:nat |] ==> raw_div(m,n) = succ(raw_div(m#-n, n))" |
161 apply (subgoal_tac "n ~= 0") |
161 apply (subgoal_tac "n \<noteq> 0") |
162 prefer 2 apply blast |
162 prefer 2 apply blast |
163 apply (frule lt_nat_in_nat, erule nat_succI) |
163 apply (frule lt_nat_in_nat, erule nat_succI) |
164 apply (rule raw_div_def [THEN def_transrec, THEN trans]) |
164 apply (rule raw_div_def [THEN def_transrec, THEN trans]) |
165 apply (simp (no_asm_simp) add: div_termination [THEN ltD] not_lt_iff_le [THEN iffD2] ) |
165 apply (simp (no_asm_simp) add: div_termination [THEN ltD] not_lt_iff_le [THEN iffD2] ) |
166 done |
166 done |
167 |
167 |
168 lemma div_geq [simp]: |
168 lemma div_geq [simp]: |
169 "[| 0<n; n le m; m:nat |] ==> m div n = succ ((m#-n) div n)" |
169 "[| 0<n; n \<le> m; m:nat |] ==> m div n = succ ((m#-n) div n)" |
170 apply (frule lt_nat_in_nat, erule nat_succI) |
170 apply (frule lt_nat_in_nat, erule nat_succI) |
171 apply (simp (no_asm_simp) add: div_def raw_div_geq) |
171 apply (simp (no_asm_simp) add: div_def raw_div_geq) |
172 done |
172 done |
173 |
173 |
174 declare div_less [simp] div_geq [simp] |
174 declare div_less [simp] div_geq [simp] |
181 apply (simp add: nat_into_Ord [THEN Ord_0_lt_iff]) |
181 apply (simp add: nat_into_Ord [THEN Ord_0_lt_iff]) |
182 apply (erule complete_induct) |
182 apply (erule complete_induct) |
183 apply (case_tac "x<n") |
183 apply (case_tac "x<n") |
184 txt{*case x<n*} |
184 txt{*case x<n*} |
185 apply (simp (no_asm_simp)) |
185 apply (simp (no_asm_simp)) |
186 txt{*case n le x*} |
186 txt{*case @{term"n \<le> x"}*} |
187 apply (simp add: not_lt_iff_le add_assoc mod_geq div_termination [THEN ltD] add_diff_inverse) |
187 apply (simp add: not_lt_iff_le add_assoc mod_geq div_termination [THEN ltD] add_diff_inverse) |
188 done |
188 done |
189 |
189 |
190 lemma mod_div_equality_natify: "(m div n)#*n #+ m mod n = natify(m)" |
190 lemma mod_div_equality_natify: "(m div n)#*n #+ m mod n = natify(m)" |
191 apply (subgoal_tac " (natify (m) div natify (n))#*natify (n) #+ natify (m) mod natify (n) = natify (m) ") |
191 apply (subgoal_tac " (natify (m) div natify (n))#*natify (n) #+ natify (m) mod natify (n) = natify (m) ") |
192 apply force |
192 apply force |
193 apply (subst mod_div_lemma, auto) |
193 apply (subst mod_div_lemma, auto) |
194 done |
194 done |
195 |
195 |
196 lemma mod_div_equality: "m: nat ==> (m div n)#*n #+ m mod n = m" |
196 lemma mod_div_equality: "m: nat ==> (m div n)#*n #+ m mod n = m" |
197 apply (simp (no_asm_simp) add: mod_div_equality_natify) |
197 apply (simp (no_asm_simp) add: mod_div_equality_natify) |
201 subsection{*Further Facts about Remainder*} |
201 subsection{*Further Facts about Remainder*} |
202 |
202 |
203 text{*(mainly for mutilated chess board)*} |
203 text{*(mainly for mutilated chess board)*} |
204 |
204 |
205 lemma mod_succ_lemma: |
205 lemma mod_succ_lemma: |
206 "[| 0<n; m:nat; n:nat |] |
206 "[| 0<n; m:nat; n:nat |] |
207 ==> succ(m) mod n = (if succ(m mod n) = n then 0 else succ(m mod n))" |
207 ==> succ(m) mod n = (if succ(m mod n) = n then 0 else succ(m mod n))" |
208 apply (erule complete_induct) |
208 apply (erule complete_induct) |
209 apply (case_tac "succ (x) <n") |
209 apply (case_tac "succ (x) <n") |
210 txt{* case succ(x) < n *} |
210 txt{* case succ(x) < n *} |
211 apply (simp (no_asm_simp) add: nat_le_refl [THEN lt_trans] succ_neq_self) |
211 apply (simp (no_asm_simp) add: nat_le_refl [THEN lt_trans] succ_neq_self) |
212 apply (simp add: ltD [THEN mem_imp_not_eq]) |
212 apply (simp add: ltD [THEN mem_imp_not_eq]) |
213 txt{* case n le succ(x) *} |
213 txt{* case @{term"n \<le> succ(x)"} *} |
214 apply (simp add: mod_geq not_lt_iff_le) |
214 apply (simp add: mod_geq not_lt_iff_le) |
215 apply (erule leE) |
215 apply (erule leE) |
216 apply (simp (no_asm_simp) add: mod_geq div_termination [THEN ltD] diff_succ) |
216 apply (simp (no_asm_simp) add: mod_geq div_termination [THEN ltD] diff_succ) |
217 txt{*equality case*} |
217 txt{*equality case*} |
218 apply (simp add: diff_self_eq_0) |
218 apply (simp add: diff_self_eq_0) |
262 by (cut_tac n = 0 in mod2_add_more, auto) |
262 by (cut_tac n = 0 in mod2_add_more, auto) |
263 |
263 |
264 |
264 |
265 subsection{*Additional theorems about @{text "\<le>"}*} |
265 subsection{*Additional theorems about @{text "\<le>"}*} |
266 |
266 |
267 lemma add_le_self: "m:nat ==> m le (m #+ n)" |
267 lemma add_le_self: "m:nat ==> m \<le> (m #+ n)" |
268 apply (simp (no_asm_simp)) |
268 apply (simp (no_asm_simp)) |
269 done |
269 done |
270 |
270 |
271 lemma add_le_self2: "m:nat ==> m le (n #+ m)" |
271 lemma add_le_self2: "m:nat ==> m \<le> (n #+ m)" |
272 apply (simp (no_asm_simp)) |
272 apply (simp (no_asm_simp)) |
273 done |
273 done |
274 |
274 |
275 (*** Monotonicity of Multiplication ***) |
275 (*** Monotonicity of Multiplication ***) |
276 |
276 |
277 lemma mult_le_mono1: "[| i le j; j:nat |] ==> (i#*k) le (j#*k)" |
277 lemma mult_le_mono1: "[| i \<le> j; j:nat |] ==> (i#*k) \<le> (j#*k)" |
278 apply (subgoal_tac "natify (i) #*natify (k) le j#*natify (k) ") |
278 apply (subgoal_tac "natify (i) #*natify (k) \<le> j#*natify (k) ") |
279 apply (frule_tac [2] lt_nat_in_nat) |
279 apply (frule_tac [2] lt_nat_in_nat) |
280 apply (rule_tac [3] n = "natify (k) " in nat_induct) |
280 apply (rule_tac [3] n = "natify (k) " in nat_induct) |
281 apply (simp_all add: add_le_mono) |
281 apply (simp_all add: add_le_mono) |
282 done |
282 done |
283 |
283 |
284 (* le monotonicity, BOTH arguments*) |
284 (* @{text"\<le>"} monotonicity, BOTH arguments*) |
285 lemma mult_le_mono: "[| i le j; k le l; j:nat; l:nat |] ==> i#*k le j#*l" |
285 lemma mult_le_mono: "[| i \<le> j; k \<le> l; j:nat; l:nat |] ==> i#*k \<le> j#*l" |
286 apply (rule mult_le_mono1 [THEN le_trans], assumption+) |
286 apply (rule mult_le_mono1 [THEN le_trans], assumption+) |
287 apply (subst mult_commute, subst mult_commute, rule mult_le_mono1, assumption+) |
287 apply (subst mult_commute, subst mult_commute, rule mult_le_mono1, assumption+) |
288 done |
288 done |
289 |
289 |
290 (*strict, in 1st argument; proof is by induction on k>0. |
290 (*strict, in 1st argument; proof is by induction on k>0. |
357 lemma mult_less_cancel1 [simp]: |
357 lemma mult_less_cancel1 [simp]: |
358 "(k#*m < k#*n) <-> (0 < natify(k) & natify(m) < natify(n))" |
358 "(k#*m < k#*n) <-> (0 < natify(k) & natify(m) < natify(n))" |
359 apply (simp (no_asm) add: mult_less_cancel2 mult_commute [of k]) |
359 apply (simp (no_asm) add: mult_less_cancel2 mult_commute [of k]) |
360 done |
360 done |
361 |
361 |
362 lemma mult_le_cancel2 [simp]: "(m#*k le n#*k) <-> (0 < natify(k) --> natify(m) le natify(n))" |
362 lemma mult_le_cancel2 [simp]: "(m#*k \<le> n#*k) <-> (0 < natify(k) \<longrightarrow> natify(m) \<le> natify(n))" |
363 apply (simp (no_asm_simp) add: not_lt_iff_le [THEN iff_sym]) |
363 apply (simp (no_asm_simp) add: not_lt_iff_le [THEN iff_sym]) |
364 apply auto |
364 apply auto |
365 done |
365 done |
366 |
366 |
367 lemma mult_le_cancel1 [simp]: "(k#*m le k#*n) <-> (0 < natify(k) --> natify(m) le natify(n))" |
367 lemma mult_le_cancel1 [simp]: "(k#*m \<le> k#*n) <-> (0 < natify(k) \<longrightarrow> natify(m) \<le> natify(n))" |
368 apply (simp (no_asm_simp) add: not_lt_iff_le [THEN iff_sym]) |
368 apply (simp (no_asm_simp) add: not_lt_iff_le [THEN iff_sym]) |
369 apply auto |
369 apply auto |
370 done |
370 done |
371 |
371 |
372 lemma mult_le_cancel_le1: "k : nat ==> k #* m le k \<longleftrightarrow> (0 < k \<longrightarrow> natify(m) le 1)" |
372 lemma mult_le_cancel_le1: "k \<in> nat ==> k #* m \<le> k \<longleftrightarrow> (0 < k \<longrightarrow> natify(m) \<le> 1)" |
373 by (cut_tac k = k and m = m and n = 1 in mult_le_cancel1, auto) |
373 by (cut_tac k = k and m = m and n = 1 in mult_le_cancel1, auto) |
374 |
374 |
375 lemma Ord_eq_iff_le: "[| Ord(m); Ord(n) |] ==> m=n <-> (m le n & n le m)" |
375 lemma Ord_eq_iff_le: "[| Ord(m); Ord(n) |] ==> m=n <-> (m \<le> n & n \<le> m)" |
376 by (blast intro: le_anti_sym) |
376 by (blast intro: le_anti_sym) |
377 |
377 |
378 lemma mult_cancel2_lemma: |
378 lemma mult_cancel2_lemma: |
379 "[| k: nat; m: nat; n: nat |] ==> (m#*k = n#*k) <-> (m=n | k=0)" |
379 "[| k: nat; m: nat; n: nat |] ==> (m#*k = n#*k) <-> (m=n | k=0)" |
380 apply (simp (no_asm_simp) add: Ord_eq_iff_le [of "m#*k"] Ord_eq_iff_le [of m]) |
380 apply (simp (no_asm_simp) add: Ord_eq_iff_le [of "m#*k"] Ord_eq_iff_le [of m]) |
422 apply (simp add: DIVISION_BY_ZERO_MOD) |
422 apply (simp add: DIVISION_BY_ZERO_MOD) |
423 apply (simp add: nat_into_Ord [THEN Ord_0_lt_iff]) |
423 apply (simp add: nat_into_Ord [THEN Ord_0_lt_iff]) |
424 apply (erule_tac i = m in complete_induct) |
424 apply (erule_tac i = m in complete_induct) |
425 apply (case_tac "x<n") |
425 apply (case_tac "x<n") |
426 apply (simp (no_asm_simp) add: mod_less zero_lt_mult_iff mult_lt_mono2) |
426 apply (simp (no_asm_simp) add: mod_less zero_lt_mult_iff mult_lt_mono2) |
427 apply (simp add: not_lt_iff_le zero_lt_mult_iff le_refl [THEN mult_le_mono] |
427 apply (simp add: not_lt_iff_le zero_lt_mult_iff le_refl [THEN mult_le_mono] |
428 mod_geq diff_mult_distrib2 [symmetric] div_termination [THEN ltD]) |
428 mod_geq diff_mult_distrib2 [symmetric] div_termination [THEN ltD]) |
429 done |
429 done |
430 |
430 |
431 lemma mod_mult_distrib2: "k #* (m mod n) = (k#*m) mod (k#*n)" |
431 lemma mod_mult_distrib2: "k #* (m mod n) = (k#*m) mod (k#*n)" |
432 apply (cut_tac k = "natify (k) " and m = "natify (m)" and n = "natify (n)" |
432 apply (cut_tac k = "natify (k) " and m = "natify (m)" and n = "natify (n)" |
433 in mult_mod_distrib_raw) |
433 in mult_mod_distrib_raw) |
434 apply auto |
434 apply auto |
435 done |
435 done |
436 |
436 |
437 lemma mult_mod_distrib: "(m mod n) #* k = (m#*k) mod (n#*k)" |
437 lemma mult_mod_distrib: "(m mod n) #* k = (m#*k) mod (n#*k)" |
438 apply (simp (no_asm) add: mult_commute mod_mult_distrib2) |
438 apply (simp (no_asm) add: mult_commute mod_mult_distrib2) |
439 done |
439 done |
440 |
440 |
441 lemma mod_add_self2_raw: "n \<in> nat ==> (m #+ n) mod n = m mod n" |
441 lemma mod_add_self2_raw: "n \<in> nat ==> (m #+ n) mod n = m mod n" |
442 apply (subgoal_tac " (n #+ m) mod n = (n #+ m #- n) mod n") |
442 apply (subgoal_tac " (n #+ m) mod n = (n #+ m #- n) mod n") |
443 apply (simp add: add_commute) |
443 apply (simp add: add_commute) |
444 apply (subst mod_geq [symmetric], auto) |
444 apply (subst mod_geq [symmetric], auto) |
445 done |
445 done |
446 |
446 |
447 lemma mod_add_self2 [simp]: "(m #+ n) mod n = m mod n" |
447 lemma mod_add_self2 [simp]: "(m #+ n) mod n = m mod n" |
448 apply (cut_tac n = "natify (n) " in mod_add_self2_raw) |
448 apply (cut_tac n = "natify (n) " in mod_add_self2_raw) |
449 apply auto |
449 apply auto |
468 done |
468 done |
469 |
469 |
470 (*Lemma for gcd*) |
470 (*Lemma for gcd*) |
471 lemma mult_eq_self_implies_10: "m = m#*n ==> natify(n)=1 | m=0" |
471 lemma mult_eq_self_implies_10: "m = m#*n ==> natify(n)=1 | m=0" |
472 apply (subgoal_tac "m: nat") |
472 apply (subgoal_tac "m: nat") |
473 prefer 2 |
473 prefer 2 |
474 apply (erule ssubst) |
474 apply (erule ssubst) |
475 apply simp |
475 apply simp |
476 apply (rule disjCI) |
476 apply (rule disjCI) |
477 apply (drule sym) |
477 apply (drule sym) |
478 apply (rule Ord_linear_lt [of "natify(n)" 1]) |
478 apply (rule Ord_linear_lt [of "natify(n)" 1]) |
479 apply simp_all |
479 apply simp_all |
480 apply (subgoal_tac "m #* n = 0", simp) |
480 apply (subgoal_tac "m #* n = 0", simp) |
481 apply (subst mult_natify2 [symmetric]) |
481 apply (subst mult_natify2 [symmetric]) |
482 apply (simp del: mult_natify2) |
482 apply (simp del: mult_natify2) |
483 apply (drule nat_into_Ord [THEN Ord_0_lt, THEN [2] mult_lt_mono2], auto) |
483 apply (drule nat_into_Ord [THEN Ord_0_lt, THEN [2] mult_lt_mono2], auto) |
484 done |
484 done |
485 |
485 |
486 lemma less_imp_succ_add [rule_format]: |
486 lemma less_imp_succ_add [rule_format]: |
487 "[| m<n; n: nat |] ==> EX k: nat. n = succ(m#+k)" |
487 "[| m<n; n: nat |] ==> \<exists>k\<in>nat. n = succ(m#+k)" |
488 apply (frule lt_nat_in_nat, assumption) |
488 apply (frule lt_nat_in_nat, assumption) |
489 apply (erule rev_mp) |
489 apply (erule rev_mp) |
490 apply (induct_tac "n") |
490 apply (induct_tac "n") |
491 apply (simp_all (no_asm) add: le_iff) |
491 apply (simp_all (no_asm) add: le_iff) |
492 apply (blast elim!: leE intro!: add_0_right [symmetric] add_succ_right [symmetric]) |
492 apply (blast elim!: leE intro!: add_0_right [symmetric] add_succ_right [symmetric]) |
493 done |
493 done |
494 |
494 |
495 lemma less_iff_succ_add: |
495 lemma less_iff_succ_add: |
496 "[| m: nat; n: nat |] ==> (m<n) <-> (EX k: nat. n = succ(m#+k))" |
496 "[| m: nat; n: nat |] ==> (m<n) <-> (\<exists>k\<in>nat. n = succ(m#+k))" |
497 by (auto intro: less_imp_succ_add) |
497 by (auto intro: less_imp_succ_add) |
498 |
498 |
499 lemma add_lt_elim2: |
499 lemma add_lt_elim2: |
500 "\<lbrakk>a #+ d = b #+ c; a < b; b \<in> nat; c \<in> nat; d \<in> nat\<rbrakk> \<Longrightarrow> c < d" |
500 "\<lbrakk>a #+ d = b #+ c; a < b; b \<in> nat; c \<in> nat; d \<in> nat\<rbrakk> \<Longrightarrow> c < d" |
501 by (drule less_imp_succ_add, auto) |
501 by (drule less_imp_succ_add, auto) |
502 |
502 |
503 lemma add_le_elim2: |
503 lemma add_le_elim2: |
504 "\<lbrakk>a #+ d = b #+ c; a le b; b \<in> nat; c \<in> nat; d \<in> nat\<rbrakk> \<Longrightarrow> c le d" |
504 "\<lbrakk>a #+ d = b #+ c; a \<le> b; b \<in> nat; c \<in> nat; d \<in> nat\<rbrakk> \<Longrightarrow> c \<le> d" |
505 by (drule less_imp_succ_add, auto) |
505 by (drule less_imp_succ_add, auto) |
506 |
506 |
507 |
507 |
508 subsubsection{*More Lemmas About Difference*} |
508 subsubsection{*More Lemmas About Difference*} |
509 |
509 |
510 lemma diff_is_0_lemma: |
510 lemma diff_is_0_lemma: |
511 "[| m: nat; n: nat |] ==> m #- n = 0 <-> m le n" |
511 "[| m: nat; n: nat |] ==> m #- n = 0 <-> m \<le> n" |
512 apply (rule_tac m = m and n = n in diff_induct, simp_all) |
512 apply (rule_tac m = m and n = n in diff_induct, simp_all) |
513 done |
513 done |
514 |
514 |
515 lemma diff_is_0_iff: "m #- n = 0 <-> natify(m) le natify(n)" |
515 lemma diff_is_0_iff: "m #- n = 0 <-> natify(m) \<le> natify(n)" |
516 by (simp add: diff_is_0_lemma [symmetric]) |
516 by (simp add: diff_is_0_lemma [symmetric]) |
517 |
517 |
518 lemma nat_lt_imp_diff_eq_0: |
518 lemma nat_lt_imp_diff_eq_0: |
519 "[| a:nat; b:nat; a<b |] ==> a #- b = 0" |
519 "[| a:nat; b:nat; a<b |] ==> a #- b = 0" |
520 by (simp add: diff_is_0_iff le_iff) |
520 by (simp add: diff_is_0_iff le_iff) |
521 |
521 |
522 lemma raw_nat_diff_split: |
522 lemma raw_nat_diff_split: |
523 "[| a:nat; b:nat |] ==> |
523 "[| a:nat; b:nat |] ==> |
524 (P(a #- b)) <-> ((a < b -->P(0)) & (ALL d:nat. a = b #+ d --> P(d)))" |
524 (P(a #- b)) <-> ((a < b \<longrightarrow>P(0)) & (\<forall>d\<in>nat. a = b #+ d \<longrightarrow> P(d)))" |
525 apply (case_tac "a < b") |
525 apply (case_tac "a < b") |
526 apply (force simp add: nat_lt_imp_diff_eq_0) |
526 apply (force simp add: nat_lt_imp_diff_eq_0) |
527 apply (rule iffI, force, simp) |
527 apply (rule iffI, force, simp) |
528 apply (drule_tac x="a#-b" in bspec) |
528 apply (drule_tac x="a#-b" in bspec) |
529 apply (simp_all add: Ordinal.not_lt_iff_le add_diff_inverse) |
529 apply (simp_all add: Ordinal.not_lt_iff_le add_diff_inverse) |
530 done |
530 done |
531 |
531 |
532 lemma nat_diff_split: |
532 lemma nat_diff_split: |
533 "(P(a #- b)) <-> |
533 "(P(a #- b)) <-> |
534 (natify(a) < natify(b) -->P(0)) & (ALL d:nat. natify(a) = b #+ d --> P(d))" |
534 (natify(a) < natify(b) \<longrightarrow>P(0)) & (\<forall>d\<in>nat. natify(a) = b #+ d \<longrightarrow> P(d))" |
535 apply (cut_tac P=P and a="natify(a)" and b="natify(b)" in raw_nat_diff_split) |
535 apply (cut_tac P=P and a="natify(a)" and b="natify(b)" in raw_nat_diff_split) |
536 apply simp_all |
536 apply simp_all |
537 done |
537 done |
538 |
538 |
539 text{*Difference and less-than*} |
539 text{*Difference and less-than*} |
542 apply (erule rev_mp) |
542 apply (erule rev_mp) |
543 apply (simp split add: nat_diff_split, auto) |
543 apply (simp split add: nat_diff_split, auto) |
544 apply (blast intro: add_le_self lt_trans1) |
544 apply (blast intro: add_le_self lt_trans1) |
545 apply (rule not_le_iff_lt [THEN iffD1], auto) |
545 apply (rule not_le_iff_lt [THEN iffD1], auto) |
546 apply (subgoal_tac "i #+ da < j #+ d", force) |
546 apply (subgoal_tac "i #+ da < j #+ d", force) |
547 apply (blast intro: add_le_lt_mono) |
547 apply (blast intro: add_le_lt_mono) |
548 done |
548 done |
549 |
549 |
550 lemma lt_imp_diff_lt: "[|j<i; i\<le>k; k\<in>nat|] ==> (k#-i) < (k#-j)" |
550 lemma lt_imp_diff_lt: "[|j<i; i\<le>k; k\<in>nat|] ==> (k#-i) < (k#-j)" |
551 apply (frule le_in_nat, assumption) |
551 apply (frule le_in_nat, assumption) |
552 apply (frule lt_nat_in_nat, assumption) |
552 apply (frule lt_nat_in_nat, assumption) |
553 apply (simp split add: nat_diff_split, auto) |
553 apply (simp split add: nat_diff_split, auto) |
554 apply (blast intro: lt_asym lt_trans2) |
554 apply (blast intro: lt_asym lt_trans2) |
555 apply (blast intro: lt_irrefl lt_trans2) |
555 apply (blast intro: lt_irrefl lt_trans2) |
556 apply (rule not_le_iff_lt [THEN iffD1], auto) |
556 apply (rule not_le_iff_lt [THEN iffD1], auto) |
557 apply (subgoal_tac "j #+ d < i #+ da", force) |
557 apply (subgoal_tac "j #+ d < i #+ da", force) |
558 apply (blast intro: add_lt_le_mono) |
558 apply (blast intro: add_lt_le_mono) |
559 done |
559 done |
560 |
560 |
561 |
561 |
562 lemma diff_lt_iff_lt: "[|i\<le>k; j\<in>nat; k\<in>nat|] ==> (k#-i) < (k#-j) <-> j<i" |
562 lemma diff_lt_iff_lt: "[|i\<le>k; j\<in>nat; k\<in>nat|] ==> (k#-i) < (k#-j) <-> j<i" |
563 apply (frule le_in_nat, assumption) |
563 apply (frule le_in_nat, assumption) |
564 apply (blast intro: lt_imp_diff_lt diff_lt_imp_lt) |
564 apply (blast intro: lt_imp_diff_lt diff_lt_imp_lt) |
565 done |
565 done |
566 |
566 |
567 end |
567 end |