equal
deleted
inserted
replaced
216 apply(rule Quotient_rel_abs[OF Quotient_int]) |
216 apply(rule Quotient_rel_abs[OF Quotient_int]) |
217 apply(rule plus_raw_rsp_aux) |
217 apply(rule plus_raw_rsp_aux) |
218 apply(simp_all add: rep_abs_rsp_left[OF Quotient_int]) |
218 apply(simp_all add: rep_abs_rsp_left[OF Quotient_int]) |
219 done |
219 done |
220 |
220 |
221 lemma int_def: |
221 definition int_of_nat_raw: "int_of_nat_raw m = (m :: nat, 0 :: nat)" |
222 shows "of_nat m = ABS_int (m, 0)" |
222 |
223 by (induct m) (simp_all add: zero_int_def one_int_def add) |
223 quotient_def |
|
224 int_of_nat :: "int_of_nat :: nat \<Rightarrow> int" where "int_of_nat_raw" |
|
225 |
|
226 lemma[quot_respect]: "(op = ===> op \<approx>) int_of_nat_raw int_of_nat_raw" |
|
227 by (simp add: equivp_reflp[OF int_equivp]) |
|
228 |
|
229 lemma int_def: |
|
230 shows "of_nat m = int_of_nat m" |
|
231 apply (induct m) |
|
232 apply (simp_all add: zero_int_def one_int_def int_of_nat_def int_of_nat_raw add) |
|
233 done |
224 |
234 |
225 lemma le_antisym_raw: |
235 lemma le_antisym_raw: |
226 shows "less_eq_raw i j \<Longrightarrow> less_eq_raw j i \<Longrightarrow> i \<approx> j" |
236 shows "less_eq_raw i j \<Longrightarrow> less_eq_raw j i \<Longrightarrow> i \<approx> j" |
227 by (cases i, cases j) (simp) |
237 by (cases i, cases j) (simp) |
228 |
238 |
295 done |
305 done |
296 |
306 |
297 lemma int_induct_raw: |
307 lemma int_induct_raw: |
298 assumes a: "P (0::nat, 0)" |
308 assumes a: "P (0::nat, 0)" |
299 and b: "\<And>i. P i \<Longrightarrow> P (plus_raw i (1,0))" |
309 and b: "\<And>i. P i \<Longrightarrow> P (plus_raw i (1,0))" |
300 and c: "\<And>i. P i \<Longrightarrow> P (plus_raw i (minus_raw (1,0)))" |
310 and c: "\<And>i. P i \<Longrightarrow> P (plus_raw i (uminus_raw (1,0)))" |
301 shows "P x" |
311 shows "P x" |
302 apply(case_tac x) apply(simp) |
312 apply(case_tac x) apply(simp) |
303 apply(rule_tac x="b" in spec) |
313 apply(rule_tac x="b" in spec) |
304 apply(rule_tac Nat.induct) |
314 apply(rule_tac Nat.induct) |
305 apply(rule allI) |
315 apply(rule allI) |
312 and b: "\<And>i. P i \<Longrightarrow> P (i + 1)" |
322 and b: "\<And>i. P i \<Longrightarrow> P (i + 1)" |
313 and c: "\<And>i. P i \<Longrightarrow> P (i + (- 1))" |
323 and c: "\<And>i. P i \<Longrightarrow> P (i + (- 1))" |
314 shows "P x" |
324 shows "P x" |
315 using a b c by (lifting int_induct_raw) |
325 using a b c by (lifting int_induct_raw) |
316 |
326 |
317 lemma zero_le_imp_eq_int: |
327 lemma zero_le_imp_eq_int_raw: |
|
328 fixes k::"(nat \<times> nat)" |
|
329 shows "less_raw (0,0) k \<Longrightarrow> (\<exists>n > 0. k \<approx> int_of_nat_raw n)" |
|
330 apply(cases k) |
|
331 apply(simp add:int_of_nat_raw) |
|
332 apply(auto) |
|
333 apply(rule_tac i="b" and j="a" in less_Suc_induct) |
|
334 apply(auto) |
|
335 done |
|
336 |
|
337 lemma zero_le_imp_eq_int: |
318 fixes k::int |
338 fixes k::int |
319 shows "0 < k \<Longrightarrow> \<exists>n > 0. k = of_nat n" |
339 shows "0 < k \<Longrightarrow> \<exists>n > 0. k = int_of_nat n" |
320 sorry |
340 unfolding less_int_def by (lifting zero_le_imp_eq_int_raw) |
321 |
341 |
322 lemma zmult_zless_mono2: |
342 lemma zmult_zless_mono2: |
323 fixes i j k::int |
343 fixes i j k::int |
324 assumes a: "i < j" "0 < k" |
344 assumes a: "i < j" "0 < k" |
325 shows "k * i < k * j" |
345 shows "k * i < k * j" |