I think I got it, it’s F(R) = {(0,0)} in this case ...
> Il giorno 04 mag 2017, alle ore 14:53, Chun Tian (binghe)
> <binghe.l...@gmail.com> ha scritto:
>
> Hi Michael,
>
> Thanks for quick response. I want to further ask, if I have the following
> mini relation:
>
> val (R_rules, R_coind, R_cases) = Hol_coreln `
> (!(m:num) (n:num). R 0 0) `;
>
> which generates a cases theorem:
>
> val R_cases =
> |- ∀a0 a1. R a0 a1 ⇔ ∃m n. (a0 = 0) ∧ (a1 = 0):
> thm
>
> How can I convince someone (who doesn't know and trust anything from HOL)
> that, {(0, 0)} is the only fixed point of above relation R. Thus, no matter I
> define it with Hol_reln or Hol_coreln, I get exactly the same relation?
>
> In another word, what's the exact definition of the function F in this case,
> such that R is the fixed point of F, e.g. F (R) = R ?
>
> Regards,
>
> Chun
>
>
>
> On 4 May 2017 at 14:17, <michael.norr...@data61.csiro.au> wrote:
> As with the cases theorem returned by Hol_reln, the cases theorem is
> effectively an assertion that the relation is indeed a fix-point.
>
>
>
> Michael
>
>
>
> From: "Chun Tian (binghe)" <binghe.l...@gmail.com>
> Date: Thursday, 4 May 2017 at 14:07
> To: hol-info <hol-info@lists.sourceforge.net>
> Subject: [Hol-info] Documentation for Hol_coreln?
>
>
>
> Hi,
>
>
>
> Currently the "Hol_coreln" command in HOL4 seems undocumented. I wonder, is
> there any related paper or notes when this facility was added?
>
>
>
> I mainly want to know the purpose of the "cases" theorem returned by
> Hol_coreln (beside looking at source code).
>
>
>
> Thanks,
>
>
>
> --
>
> 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
>
>
>
>
> --
> 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
