Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] old methods


view this post on Zulip Email Gateway (Aug 19 2022 at 10:53):

From: Paqui Lucio Carrasco <paqui.lucio@ehu.es>
Hi,
The following “old” method is not correct for Isabelle2013

method_setup unnext_method = {* Method.thms_args (fn thms =>
Method.METHOD (fn facts =>
(REPEAT (resolve_tac [thm
"unnext1",thm "unnext2"] 1
ORELSE
(resolve_tac [thm "unnext0"] 1))))) *}

¿Could you tell how to “renew” this king of methods for
Isabelle2013?

Thanks,
Paqui


Paqui Lucio
Dpto de Lenguajes y Sistemas Informáticos
Facultad de Informática
Paseo Manuel de Lardizabal, 1
20018-San Sebastián
SPAIN


e-mail: paqui.lucio@ehu.es
Tfn: (+34) (9)43 015049
Fax: (+34) (9)43 015590
Web: http://www.sc.ehu.es/paqui


view this post on Zulip Email Gateway (Aug 19 2022 at 10:53):

From: Makarius <makarius@sketis.net>
I guess that this was for Isabelle2008. To warp it forwards in time to
Isabelle2013, see also
http://isabelle.in.tum.de/dist/Isabelle2013/doc/isar-ref.pdf section 6.3.5
on 'method_setup'.

Here is your slighty reworked example, according to the my_method3 example
from there.

theorem unnext1: True and unnext2: True and unnext0: True by auto

method_setup unnext = {*
Attrib.thms >> (fn thms => fn ctxt =>
SIMPLE_METHOD' (fn i =>
(REPEAT (resolve_tac @{thms unnext1 unnext2} i
ORELSE (resolve_tac @{thms unnext0} i)))))
*}

Since this does not use the "thms" argument at all, you might also
consider the my_method1 or my_method2 template from the manual.

After 2009 all this has become much simpler than before: you should search
for method_setup or Method.setup in existing Isabelle applications to get
further ideas.

ML antiquotations like @{thms} above are explained in
http://isabelle.in.tum.de/dist/Isabelle2013/doc/implementation.pdf

Makarius


Last updated: Mar 29 2024 at 04:18 UTC