Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] shorter syntax?

Email Gateway (Aug 19 2022 at 15:33):

From: Vadim Zaliva <vzaliva@cmu.edu>
Hi!

I am proving things about lists of of values which have type of instances of comm_ring_1.
I have to write a lot of constructs like this:

fixes a::"'val::{comm_ring_1} list"

If there is a way to define shorter alias for this?
For example, before I was working with reals and I had
type_synonym 'vec' for 'real list' and I would use:

fixes a::"vec"

Any way to do something similar here?

Thanks!

Sincerely,
Vadim Zaliva

Email Gateway (Aug 19 2022 at 16:02):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Vadim,

fixes a::"'val::{comm_ring_1} list"

If there is a way to define shorter alias for this?

in short, nothing simple except to leave out the curly brackets:

fixes a :: "'a :: comm_ring list"

You could do fancy things on one of the type parsing/printing layers,
but this is nothing I would recommend here.

Florian

For example, before I was working with reals and I had
type_synonym 'vec' for 'real list' and I would use:

fixes a::"vec"

Any way to do something similar here?

Thanks!

Sincerely,
Vadim Zaliva

--
CMU ECE PhD student
Mobile: +1(510)220-1060
Skype: vzaliva

signature.asc

Email Gateway (Aug 19 2022 at 16:02):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Vadim

Here's another thought on this. If it is just about avoiding the ubiquitous sort
constraint for one specific type variable, you can fix the type variable locally in an
anonymous context. Here's an example:

context fixes dummy :: "'val :: comm_ring_1" begin

lemma foo
fixes a :: "'val"
assumes ...
shows ...
sorry

end

Andreas

Last updated: May 06 2024 at 12:29 UTC