Re: [isabelle] Questios about evaluation and code extraction



(1) Is it possible to evaluate, or normalize, terms inside Isabelle? I
know that one can exract executable specifications to ML ("Isabelle's
Logics: HOL", Section 2.9). I also know that in the proof mode I can
say apply(simp) to simplify, say, the goal "(12 :: int) div 5 = 2" to
True. But can I make Isabelle compute the result of "(12 :: int) div
5"?

Try the Isar command
value  "...."
which does just that. Preview: the development version provides the new command `normal_form' which even normalizes terms containing variables.

(2) Is it possible to extract code from fragments that use rational
numbers? When I tried the following code:

Rational numbers are defined as quotient types, which are not directly executable. The development version contains a manual implementation of the rationals - Stefan Berghofer or Florian Haftmann should be able to provide the details.

Tobias





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