Email Gateway (Aug 19 2022 at 10:53): 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
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: Nov 21 2024 at 12:39 UTC