Found a proof: open cardinalTheory ordinalTheory sumTheory;
val ONE_ONE_IMP_EXISTS = store_thm ((* NEW *)
"ONE_ONE_IMP_EXISTS",
``!(A :'a set) (f :'a ordinal -> 'a). ONE_ONE f ==> ?n. !x. x IN A ==> x <> f
n``,
REPEAT GEN_TAC
>> MP_TAC univ_ord_greater_cardinal
>> RW_TAC std_ss [ONE_ONE_DEF, cardleq_def, INJ_DEF, IN_UNIV]
>> CCONTR_TAC
>> PAT_X_ASSUM ``!g. P``
(MP_TAC o (Q.SPEC `\n. if n < omega then INL (@m. &m = n) else INR (f
n)`))
>> BETA_TAC
>> REPEAT STRIP_TAC
>> Cases_on `x < omega \/ x < omega` (* 2 sub-goals here *)
>| [ (* goal 1 (of 2) *)
FULL_SIMP_TAC std_ss [] \\
PAT_X_ASSUM ``(@m. &m = x) = @m. &m = y`` MP_TAC \\
REWRITE_TAC [] \\
NTAC 2 SELECT_ELIM_TAC \\
REPEAT STRIP_TAC >| (* 3 sub-goals here *)
[ (* goal 1.1 (of 3) *)
PAT_X_ASSUM ``y < omega`` (ASSUME_TAC o (REWRITE_RULE [lt_omega])) \\
PROVE_TAC [],
(* goal 1.2 (of 3) *)
PAT_X_ASSUM ``x < omega`` (ASSUME_TAC o (REWRITE_RULE [lt_omega])) \\
PROVE_TAC [],
(* goal 1.3 (of 3) *)
FULL_SIMP_TAC std_ss [] ],
(* goal 2 (of 2) *)
FULL_SIMP_TAC std_ss [EXTENSION, GSPECIFICATION] \\
PROVE_TAC [] ]);
> Il giorno 12 lug 2017, alle ore 23:32, Chun Tian (binghe)
> <binghe.l...@gmail.com> ha scritto:
>
> *my initial proposition IS NOT TRUE unless the infinite set B has the same
> type variable with the ordinals ...
>
> On 12 July 2017 at 23:21, Chun Tian (binghe) <binghe.l...@gmail.com> wrote:
> Hi Konrad,
>
> Simply because the domain of f is the universe of some ordinals. Actually I
> think my initial proposition unless the infinite set B has the same type
> variable with the ordinals: ('a ordinal) and ('a set). Now there's a theorem
> in ordinalTheory saying that:
>
> [univ_ord_greater_cardinal] Theorem
>
> |- 𝕌(:'a inf) ≺ 𝕌(:'a ordinal)
>
> where (:'a inf) means the sum type: ``:num + 'a``. Reading from right to
> left, it says there's no injection from 𝕌(:'a ordinal) to 𝕌(:'a inf). In
> another words, for all mappings g, there're x, y IN 𝕌(:'a ordinal) such that
> g(x) = g(y) but x <> y.
>
> If my original goal is not true, i.e. for all x IN 𝕌(:'a ordinal), f(x) in B.
> then the following mapping:
>
> g(x) = if x < omega then INL (@n. n = &x) else INR f(x)
>
> will map each ('a ordinal) ordinals into B UNION univ(:num), and the part
> from non-limit ordinals to univ(:num) is actually a bijection. Now the
> result I got from univ_ord_greater_cardinal and the assumption (ONE_ONE f)
> are conflict, thus my original goal must be true.
>
> Do you agree?
>
> Regards,
>
> Chun
>
>
> On 12 July 2017 at 22:53, Konrad Slind <konrad.sl...@gmail.com> wrote:
> I don't know a lot about this (even though I am responsible for
> ordinalTheory) but
> the Axiom of Infinity in HOL asserts the existence of an infinite set without
> saying how big it is. How do you know that B is not the same size as the
> domain of f?
>
> Konrad.
>
>
> On Wed, Jul 12, 2017 at 12:50 PM, Chun Tian (binghe) <binghe.l...@gmail.com>
> wrote:
> Hi,
>
> I’m using the ordinalTheory and cardinalTheory (in
> "examples/set-theory/hol_sets”) with the following proposition unprovable:
>
> Suppose I have a ONE_ONE function (f :’a ordinal -> ‘b), and an infinite set
> (B: ‘b set), how can I assert the existence of an ordinal ``n`` such that
> ``(f n) NOTIN B``?
>
> Regards,
>
> Chun Tian
>
>
> ------------------------------------------------------------------------------
> Check out the vibrant tech community on one of the world's most
> engaging tech sites, Slashdot.org! http://sdm.link/slashdot
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
>
>
>
> --
> Chun Tian (binghe)
> University of Bologna (Italy)
>
>
>
>
> --
> Chun Tian (binghe)
> University of Bologna (Italy)
>
signature.asc
Description: Message signed with OpenPGP using GPGMail
------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
