[isabelle] Questios about evaluation and code extraction



Hello,

I am a beginner in Isabelle, and I have two (hopefully)
straightforward questions.

(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"?

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

constdefs f :: "rat => rat"
 "f x == 1 / x + x"

code_module Inc file "rat.ml"
contains f

I got this error:

*** Unable to generate code for type:
*** 'a set
*** required by:
*** Quotient.quot (type), Rational.rat (type), <Top>
*** At command "code_module".

Thank you,
Yevgeniy





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