Re: [isabelle] old methods



On Mon, 15 Apr 2013, Paqui Lucio Carrasco wrote:

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?

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


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.