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
