Email Gateway (Aug 18 2022 at 10:03): Email Gateway (Aug 18 2022 at 10:03):From: Yevgeniy Makarov <emakarov@gmail.com>
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
Email Gateway (Aug 18 2022 at 10:03):From: Tobias Nipkow <nipkow@in.tum.de>
(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
Last updated: May 03 2024 at 08:18 UTC