538 apply (erule cons_lepoll_consD) |
538 apply (erule cons_lepoll_consD) |
539 apply (rule mem_not_refl)+ |
539 apply (rule mem_not_refl)+ |
540 done |
540 done |
541 |
541 |
542 |
542 |
543 lemma nat_lepoll_imp_le [rule_format]: |
543 lemma nat_lepoll_imp_le: |
544 "m \<in> nat ==> \<forall>n\<in>nat. m \<lesssim> n \<longrightarrow> m \<le> n" |
544 "m \<in> nat ==> n \<in> nat \<Longrightarrow> m \<lesssim> n \<Longrightarrow> m \<le> n" |
545 apply (induct_tac m) |
545 proof (induct m arbitrary: n rule: nat_induct) |
546 apply (blast intro!: nat_0_le) |
546 case 0 thus ?case by (blast intro!: nat_0_le) |
547 apply (rule ballI) |
547 next |
548 apply (erule_tac n = n in natE) |
548 case (succ m) |
549 apply (simp (no_asm_simp) add: lepoll_def inj_def) |
549 show ?case using `n \<in> nat` |
550 apply (blast intro!: succ_leI dest!: succ_lepoll_succD) |
550 proof (cases rule: natE) |
551 done |
551 case 0 thus ?thesis using succ |
|
552 by (simp add: lepoll_def inj_def) |
|
553 next |
|
554 case (succ n') thus ?thesis using succ.hyps ` succ(m) \<lesssim> n` |
|
555 by (blast intro!: succ_leI dest!: succ_lepoll_succD) |
|
556 qed |
|
557 qed |
552 |
558 |
553 lemma nat_eqpoll_iff: "[| m \<in> nat; n: nat |] ==> m \<approx> n \<longleftrightarrow> m = n" |
559 lemma nat_eqpoll_iff: "[| m \<in> nat; n: nat |] ==> m \<approx> n \<longleftrightarrow> m = n" |
554 apply (rule iffI) |
560 apply (rule iffI) |
555 apply (blast intro: nat_lepoll_imp_le le_anti_sym elim!: eqpollE) |
561 apply (blast intro: nat_lepoll_imp_le le_anti_sym elim!: eqpollE) |
556 apply (simp add: eqpoll_refl) |
562 apply (simp add: eqpoll_refl) |