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<mailto: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<mailto: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<mailto: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<mailto: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<mailto: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<mailto: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://Slashdot.org>!
> http://sdm.link/slashdot
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net<mailto: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://Slashdot.org>! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net<mailto: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
