Re: [isabelle] evaluation of expressions

Hi Viorel,

Thanks for clarifying the requirements w.r.t. efficiency. I indeed misread your "quick" as efficient instead of "easy to do".


On 02/03/2019 11:23, viorel.preoteasa at wrote:

Thank you for your messages. code_unfold is exactly what I was looking for. Probably my message was  a bit confusing.
By "a quick way" I did not mean necessarily efficient, but easy way to evaluate that kind of expressions.

Before I would define a function F = g (S f), then introduce a lemma [code]: "F = f", but to introduce this lemma, I would need
to obtain f first which could be a very long expression.


-----Original Message-----
From: Manuel Eberl <eberlm at>
Sent: Friday, March 1, 2019 11:23 PM
To: Andreas Lochbihler <mail at>; Viorel Preoteasa <viorel.preoteasa at>; cl-isabelle-users at
Subject: Re: [isabelle] evaluation of expressions

I don't see what "code_unfold" has to do with performance. Are you perhaps confusing it with code_simp/"value [simp]"?

As far as I know, "code_unfold" is just a code generator preprocessing option that allows you to tweak the input before the code generator is invoked. Viorel seems to want to use something as a "code equation" that does not fulfil the syntactic prerequisites to be a code equation, and code_unfold works pretty well for that. I don't see why it should be slow.


On 01/03/2019 22:18, Andreas Lochbihler wrote:
Hi Manuel,

Thanks for the suggestion. I briefly had thought about this, but then
dismissed it because Viorel wrote that a "quick way" to evaluate such
expressions, and code-unfold is not quick as it is done by the simplifier.


On 01/03/2019 21:48, Manuel Eberl wrote:

there is one possible solution that Andreas may have missed. Whether
this works for you depends a bit on your application, but at least in
the case you presented, you can simply use "g_S_simp" as a "code_unfold"
rule instead of a "code" rule, and then "value" works on your example:

lemma g_S_simp[code_unfold, simp]: "g (S f) = f"

You can read up on what "code_unfold" does in the code generator
manual; very briefly, if I recall correctly, it just rewrites the
input expression with the unfold rules before attempting to generate
code for it. I often use it to generate code for "non-executable"
constructs that can be rewritten into a more palatable form, or to
introduce optimisations.


On 01/03/2019 21:25, Andreas Lochbihler wrote:
Dear Viorel,

value "..." tries to generate SML code for the given expression and
evaluate it in the run-time system. In your example, the lemma
g_S_simp is not a code equation, because in a code equation, you can
only pattern match on constructors. This is also what the warning tells you.
Accordingly, the code generator ignores this equation and tries to
generate code for g using its definition. This definition contains
SOME and that's where the well-sortedness error comes from.

So there's no way to get to this behaviour for any of the evaluator.
The reason is that the code generator simply does not allow such
non-constructor pattern, although the symbolic evaluators code_simp
and normalization could deal with such equations.


On 01/03/2019 09:54, Viorel Preoteasa wrote:

I have a lemma of the following form: "g (S f) = f" and I would
like to use it evaluate for example "g (S Suc) 3" using

value "g (S Suc) 3"

Is it possible to achieve this behavior? Simplification works OK,
but I need also a quick way to calculate this kind of expressions.

Next is the complete example

definition "S f x = f x"

lemma S_simp: "S f = f"

     by (simp add: S_def fun_eq_iff)

definition "g A = (SOME f . A = S f)"

lemma g_S_simp[code,simp]: "g (S f) = f"
     by (simp add: g_def S_simp)

lemma "g (S Suc) 3 = 4"
     by (simp) (*this works OK*)

value "g (S Suc) 3" (*this gives Wellsortedness error*)

Best regards,

Viorel Preoteasa

On 19/02/2019 15.14, Thomas Sewell wrote:

I recall the addition of the signed words, and maybe I can add
some information.

I think that "'a signed word" and "'a word" are equivalent for all
key operations. The signed variant was added as part of an
adjustment of the C-to-Isabelle parser, so that in the resulting
code it was possible to tell whether the variables were designated
signed or unsigned in C. Note that most arithmetic is exactly the same.

Also note that the outer type constructor is word, that is, "32
signed word" is an instance of "'a word" where the length
parameter is "32 signed". To make use of this, I think you want to
define some kind of is_signed class with a class constant of type
bool, and ensure that "32 signed" is signed, and that each numeral
type counts as unsigned. Finally, you can lift that to a query on
the outer word type.

I think that all might work, but I haven't tried any of it.




*From:* cl-isabelle-users-bounces at
<cl-isabelle-users-bounces at> on behalf of Viorel
Preoteasa <viorel.preoteasa at>
*Sent:* Tuesday, February 19, 2019 10:40:26 AM
*To:* Thiemann, René
*Cc:* cl-isabelle-users at
*Subject:* Re: [isabelle] signed and unsigned words Dear René,

Thank you for your message.

On 18/02/2019 15.18, Thiemann, René wrote:
Dear Viorel,

it is difficult to test your problem, since the “signed” and
“usigned” types are something that I do neither find in the
distribution nor in the AFP.

The definition of the signed type is here:

and the definition of unsigned is identical.

Hence, I can only blindly guess:

There might be a problem in your definition of “overflow_add”
uses the generic “to_int”, not a specific implementation.
This will work if “to_int” is defined as a class-constant (class
some_name = fixes to_int :: …), but I’m not sure whether your
approach via “consts to_int” is supported with code-generation.

So, you might try to reformulate the definition of to_int via
and instantiation.

This was my first attempt, but I did not manage the instantiation
of class overflow as 'a signed word .

Now I have implemented a different solution. I created a new copy
of the type 'a word:

typedef (overloaded) 'a::len sword = "UNIV::'a word set"
     morphisms sword_to_word word_to_sword by auto

and I lifted all operations from word to sword. This seems to
work, but I am interested to find the best possible solution.

Best regards,


Best regards,

I need new types of signed and unsigned words with operations
-, ...) identical with the operations on words, but with a new

overflow_add a b which is defined differently for signed and
unsigned words.

Basically I need the two types to be instantiations of the
following class:

class overflow = plus +
     fixes overflow_add::  "'a ⇒ 'a ⇒ bool"

I tried something inspired from the AFP entry "Finite Machine

type_synonym 'a sword = "'a signed word"
type_synonym 'a uword = "'a usigned word"

consts to_int :: "'a word ⇒ int"

     to_int_sword ≡ "to_int:: 'a sword ⇒ int"
     to_int_uword ≡ "to_int::'a uword ⇒ int"
     definition "to_int_sword (a:: 'a::len sword) = sint a"
     definition "to_int_uword (a:: 'a::len uword) = uint a"

instantiation  word :: (len0)  overflow begin
     definition "overflow_add a b = (to_int (a::'a word) + to_int
b =
to_int (a + b))"
instance ..

this seems to work, but I don't know how to get code generation
for overflow_add:

value "overflow_add (-2::4 sword) (-3)"

gives the error:

No code equations for to_int

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