I have nothing to add here about the proof content, but I thought I'd
mention that there are lowercase versions of many tactics which could be
easier to type.
For example, your proof could start like this: "rpt gen_tac >> mp_tac
univ_ord_greater_cardinal".
The other style thing I'd say is to prefer qpat_x_assum over pat_x_assum,
and qspec_then over (Q.)SPEC, since the quotation gets parsed in the
context of the goal that way.
For example, I'd replace your first PAT_X_ASSUM line with:
qpat_x_assum`!g. P`(qspec_then`...`mp_tac)
(or probably first_x_assum(qspec_then`...`mp_tac), since the pattern match
there isn't doing much)
On 13 July 2017 at 09:26, Chun Tian (binghe) <binghe.l...@gmail.com> wrote:
> 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)
> >
>
>
> ------------------------------------------------------------
> ------------------
> 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
>
>
------------------------------------------------------------------------------
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
