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)
------------------------------------------------------------------------------
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
