Thank you. Instantiating the variables worked with ISPEC and hence I
used ISPEC_THEN in my proof.
Cheers,
Heiko
On 09/08/2017 09:14 AM, Anthony Fox wrote:
The theorem float_add_relative is of the form
∀(a :(τ, χ) float) (b :(τ, χ) float). ..
and
SPEC ``(fp64_to_float v):(52, 11) float`` float_add_relative
will only try to specialise values and not types. What you need is Drule.ISPEC,
i.e.
Drule.ISPEC ``fp64_to_float v : (52, 11) float`` float_add_relative
Alternatively you could use SPEC after manually using Thm.INST_TYPE to
instantiate the type of float_add_relative.
Anthony
On 8 Sep 2017, at 08:01, Heiko Becker <hbec...@mpi-sws.org> wrote:
Hello everyone,
I am trying to prove a theorem using the IEEE floating-point formalizations of
HOL4. In a proof, I need to apply the lemma lift_ieeeTheory.float_add_relative.
However neither match_mp_tac nor irule are able to unify the lemma with the
conclusion I want to show.
I tried instantiating variables by hand to see what happens. Trying the below
code fails with an error complaining about mismatched types in the conclusion:
SPEC ``(fp64_to_float v):(52, 11) float`` float_add_relative
Can someone tell me what I a doing wrong in this case, since (52,11) float
should be unifiable with (τ, χ) float.
Thanks,
Heiko
------------------------------------------------------------------------------
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
------------------------------------------------------------------------------
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
