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
