That was a happy mistake: I wanted to write `x < omega \/ y < omega`
because there're really four different cases to consider, but HOL's
FULL_SIMP_TAC is so strong, it automatically resolved the cases when x and
y were at different sides of omega ... I didn't realize until I go over the
proof again to replace several tacticals with the ones I learnt from Ramana
Kumar.
--Chun
On 13 July 2017 at 02:50, <michael.norr...@data61.csiro.au> wrote:
> I’m confused by the Cases_on `x < omega \/ x < omega`. Surely one copy of
> x < omega would be enough.
>
>
>
> Michael
>
>
>
> *From: *"Chun Tian (binghe)" <binghe.l...@gmail.com>
> *Date: *Thursday, 13 July 2017 at 09:50
> *To: *Ramana Kumar <ramana.ku...@cl.cam.ac.uk>
> *Cc: *hol-info <hol-info@lists.sourceforge.net>
> *Subject: *Re: [Hol-info] A question about ordinals
>
>
>
> Hi Ramana,
>
>
>
> Thanks for your suggestions, I'll keep these things in mind for next
> project (or next time when I send pull requests to modify HOL's official
> code base)
>
>
>
> My current project is still based on a porting of old Hol88 proof scripts
> written by others, then I added lots of new theorems, and basically that's
> how I learnt HOL4's command set:)
>
>
>
> Regards,
>
>
>
> Chun
>
>
> Il giorno 13 lug 2017, alle ore 01:39, Ramana Kumar <
> ramana.ku...@cl.cam.ac.uk> ha scritto:
>
> 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
>
>
--
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
