Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isar shortcut

Email Gateway (Aug 18 2022 at 09:56):

From: Gabriele Pozzani <gabriele.pozzani@gmail.com>
Hello everybody,
in many ML level demonstrations I seen that is possible to define a variable
containing a theorem list and so use it as simp's parameter.

val sels = [sbit_def, sq_def, ssending_def, rbit_def, rq_def, rsending_def];
Goal ...
by (asm_simp_tac (simpset() addsimps sels) 1);
...

Is there a way to do a same thing in Isar proofs?

Thanks
Gabriele Pozzani

Email Gateway (Aug 18 2022 at 09:56):

From: Norbert Schirmer <norbert.schirmer@web.de>
Hello Gavriele,

Yes indeed

lemmas sels = sbit_def sq_def ...

apply (simp add: sels)

Norbert

Email Gateway (Aug 18 2022 at 09:57):

From: Peter Lammich <peter.lammich@uni-muenster.de>
Gabriele Pozzani wrote:

You could use

lemmas sels = sbit_def sq_def ssending_def rbit_def rq_def rsending_def
...
show ?thesis by (simp add: sels)
...

Last updated: May 03 2024 at 04:19 UTC