equal
deleted
inserted
replaced
457 by (cases n) simp_all |
457 by (cases n) simp_all |
458 |
458 |
459 lemma enat_iless: "n < enat m \<Longrightarrow> \<exists>k. n = enat k" |
459 lemma enat_iless: "n < enat m \<Longrightarrow> \<exists>k. n = enat k" |
460 by (cases n) simp_all |
460 by (cases n) simp_all |
461 |
461 |
|
462 lemma iadd_le_enat_iff: |
|
463 "x + y \<le> enat n \<longleftrightarrow> (\<exists>y' x'. x = enat x' \<and> y = enat y' \<and> x' + y' \<le> n)" |
|
464 by(cases x y rule: enat.exhaust[case_product enat.exhaust]) simp_all |
|
465 |
462 lemma chain_incr: "\<forall>i. \<exists>j. Y i < Y j ==> \<exists>j. enat k < Y j" |
466 lemma chain_incr: "\<forall>i. \<exists>j. Y i < Y j ==> \<exists>j. enat k < Y j" |
463 apply (induct_tac k) |
467 apply (induct_tac k) |
464 apply (simp (no_asm) only: enat_0) |
468 apply (simp (no_asm) only: enat_0) |
465 apply (fast intro: le_less_trans [OF i0_lb]) |
469 apply (fast intro: le_less_trans [OF i0_lb]) |
466 apply (erule exE) |
470 apply (erule exE) |