Re: [isabelle] About auto-method





jwang whu.edu.cn (jwang) wrote:
   Hi:
    I want to know how to print the proof procedure of auto-method in  Isabelle ,for example the theroy or lemmas used by auto-method ,so I have a good understanding of the proof procedure of some theroy used in verifying security protocol.
    Thanks a lot.
                                                                     Jean
The procedure is found in src/Provers/clasimp.ML, under mk_auto_tac;
it contains the use of the "blast" tactics (see blast.ML) which are very complex.

But as for the lemmas used, auto_tac uses a "claset" and a "simpset", the reference manual (chapters 10 and 11) tell you about these. Most commonly you would use the default ones, possibly adding rules useful for your particular goal. So if you need to make it work better,
first try adding relevant rules.  Second try alternatives - eg force_tac

Jeremy








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