You would have to define every function in terms of “fix” and then come up with
a clause for the new constant using “Fix” as well (or prove a new “axiom” for
the type). You would also need to prove new induction and cases theorems. But
yes, this “cheap approach” might be doable.
Michael
On 28/10/17, 02:39, "Chun Tian" <binghe.l...@gmail.com> wrote:
> Il giorno 27 ott 2017, alle ore 17:35, Chun Tian <binghe.l...@gmail.com>
ha scritto:
>
> Thanks for your comments.
>
> If I quotient [1] the original CCS datatype into another one, I could
expect to have the a “fix” constructor with a finite map, right?
>
> On the the other side, what if I directly define another similar
constant, say “Fix” in this form:
>
> |- Fix fm X = fix (alist_to_fmap ls) X
Sorry, it should be:
|- Fix fm X = fix (fmap_to_alist fm) X
>
> And in all theorems I only use “Fix”. Is this possible (as a cheap
solution) for resolving the “structural congruences” issue?
>
> Regards,
>
> Chun Tian
>
> [1] Homeier, P.V.: Higher Order Quotients in Higher Order Logic.
preparation; draft available at http://www cis …. (1969).
------------------------------------------------------------------------------
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
