Re: [isabelle] A simple lemma



Hi John,

Am 08.05.2012 um 00:01 schrieb John Munroe:

> axiomatization
> T :: "real set" and
> S :: "real set" where
> ax1: "T = {1,2}" and
> ax2: "S = {1,2,3}"
> 
> lemma "ALL t:T. EX s : S. even t <-> s*t=6"

The problem appears to be that the above formula does not type check without coercions (since "even" is not supported for "real"s) and that the implicit coercions are not necessarily those you want. (In fact, the example is rejected by the repository version of Isabelle, which appears to be more conservative here.)

You can solve the problem by adding an explicit conversion from "real" to "int", such as "floor" below:

    lemma "ALL t:T. EX s : S. even (floor t) <-> s*t=6"

Then the proof is a piece of cake:

    by (simp add: ax1 ax2)

Coercions are a recent addition to Isabelle (cf. Traytel, Berghofer, Nipkow APLAS 2011), and they can be very useful for some kinds of formalization, but their potential for confusing users remains largely unexplored. ;)

Cheers,

Jasmin






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.