Right. If you have recursive occurrences of R on the RHS, these would correspond to places where the fix-point construction does something with the set parameter (as opposed to ignoring it).
Michael On 5/5/17, 02:37, "Chun Tian (binghe)" <[email protected]> wrote: 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) <[email protected]> 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, <[email protected]> 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)" <[email protected]> > Date: Thursday, 4 May 2017 at 14:07 > To: hol-info <[email protected]> > 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 > [email protected] > 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 [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
