equal
deleted
inserted
replaced
604 thus False using 1 by (metis ANTISYM antisymD) |
604 thus False using 1 by (metis ANTISYM antisymD) |
605 qed |
605 qed |
606 |
606 |
607 lemma not_isSucc_zero: "\<not> isSucc zero" |
607 lemma not_isSucc_zero: "\<not> isSucc zero" |
608 proof |
608 proof |
609 assume "isSucc zero" |
609 assume *: "isSucc zero" |
610 moreover |
|
611 then obtain i where "aboveS i \<noteq> {}" and 1: "minim (Field r) = succ i" |
610 then obtain i where "aboveS i \<noteq> {}" and 1: "minim (Field r) = succ i" |
612 unfolding isSucc_def zero_def by auto |
611 unfolding isSucc_def zero_def by auto |
613 hence "succ i \<in> Field r" by auto |
612 hence "succ i \<in> Field r" by auto |
614 ultimately show False by (metis REFL isSucc_def minim_least refl_on_domain |
613 with * show False |
615 subset_refl succ_in succ_not_in zero_def) |
614 by (metis REFL isSucc_def minim_least refl_on_domain |
|
615 subset_refl succ_in succ_not_in zero_def) |
616 qed |
616 qed |
617 |
617 |
618 lemma isLim_zero[simp]: "isLim zero" |
618 lemma isLim_zero[simp]: "isLim zero" |
619 by (metis isLim_def not_isSucc_zero) |
619 by (metis isLim_def not_isSucc_zero) |
620 |
620 |