equal
deleted
inserted
replaced
21 |
21 |
22 definition |
22 definition |
23 choicefun :: "'a set => 'a" where |
23 choicefun :: "'a set => 'a" where |
24 "choicefun E = (@x. \<exists>X \<in> Pow(E) -{{}}. x : X)" |
24 "choicefun E = (@x. \<exists>X \<in> Pow(E) -{{}}. x : X)" |
25 |
25 |
26 consts injf_max :: "nat => ('a::{order} set) => 'a" |
26 primrec injf_max :: "nat => ('a::{order} set) => 'a" |
27 primrec |
27 where |
28 injf_max_zero: "injf_max 0 E = choicefun E" |
28 injf_max_zero: "injf_max 0 E = choicefun E" |
29 injf_max_Suc: "injf_max (Suc n) E = choicefun({e. e:E & injf_max n E < e})" |
29 | injf_max_Suc: "injf_max (Suc n) E = choicefun({e. e:E & injf_max n E < e})" |
30 |
30 |
31 |
31 |
32 lemma dvd_by_all: "\<forall>M. \<exists>N. 0 < N & (\<forall>m. 0 < m & (m::nat) <= M --> m dvd N)" |
32 lemma dvd_by_all: "\<forall>M. \<exists>N. 0 < N & (\<forall>m. 0 < m & (m::nat) <= M --> m dvd N)" |
33 apply (rule allI) |
33 apply (rule allI) |
34 apply (induct_tac "M", auto) |
34 apply (induct_tac "M", auto) |