Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Problem with abstract types

view this post on Zulip Email Gateway (Jul 04 2026 at 09:19):

From: Nicolas FRANCOIS <cl-isabelle-users@lists.cam.ac.uk>

Hi.

I have a function which adds an Atom (a "sign" and a variable name) to a
Cube (a Cube being an Atom list). The function has to compare the
variables to see if it has to mix the Atoms or transfer them. Namely :

fun AtomAndCube :: "('a Atom) => ('a Cube)" where
"AtomAndCube (Atom a) (Cube []) = Cube [a]"
| "AtomAndCube (Atom (sa,va)) (Cube ((sa',va') # c')) =
(if va=va' then ... else ...)

I hope you see the idea. My problem is, I can't test this function on
abstract data. For example,

AtomAndCube (Atom (Plus,1::nat)) (Cube [(Minus,2),(Plus,1),(Plus,3)])

works, but

AtomAndCube (Atom (Plus,a)) (Cube [(Plus,b),(Minus,a),(Minus,c)])

doesn't (the computation returns the question), and I think it is
because Isabelle has no way to know that a and b are different.

Is there a way I can make this true for an example, or, even better,
for the entire theory ?

I'm quite new to Isabelle, sorry if I'm not very clear...

Thanks in advance.

--

Nicolas FRANCOIS | /\
http://nicolas.francois.free.fr | |__|
X--/\\
We are the Micro$oft. _\_V
Resistance is futile.
You will be assimilated. darthvader penguin

view this post on Zulip Email Gateway (Jul 04 2026 at 09:36):

From: Stepan Holub <cl-isabelle-users@lists.cam.ac.uk>

I think it is because Isabelle has no way to know that a and b are different.

How do /YOU /know they are different?

More generally:
If you refer to the "value" command, it is crucial to realize that not
all expressions can be evaluated.
You need some kind of executable code to be available for the expression.
For example
while
value "(1::nat) + 1"
works
value "1+1"
does not.

Stepan

On 04-Jul-26 10:55 AM, Nicolas FRANCOIS (via cl-isabelle-users Mailing
List) wrote:

Hi.

I have a function which adds an Atom (a "sign" and a variable name) to a
Cube (a Cube being an Atom list). The function has to compare the
variables to see if it has to mix the Atoms or transfer them. Namely :

fun AtomAndCube :: "('a Atom) => ('a Cube)" where
"AtomAndCube (Atom a) (Cube []) = Cube [a]"
| "AtomAndCube (Atom (sa,va)) (Cube ((sa',va') # c')) =
(if va=va' then ... else ...)

I hope you see the idea. My problem is, I can't test this function on
abstract data. For example,

AtomAndCube (Atom (Plus,1::nat)) (Cube [(Minus,2),(Plus,1),(Plus,3)])

works, but

AtomAndCube (Atom (Plus,a)) (Cube [(Plus,b),(Minus,a),(Minus,c)])

doesn't (the computation returns the question), and I think it is
because Isabelle has no way to know that a and b are different.

Is there a way I can make this true for an example, or, even better,
for the entire theory ?

I'm quite new to Isabelle, sorry if I'm not very clear...

Thanks in advance.

Last updated: Jul 22 2026 at 14:00 UTC