Re: [isabelle] tactic being executed twice

On 05/06/18 16:34, Jeremy Dawson wrote:
> I have a (part) theory file, with goal and tactic as follows
> theory Scratch imports ZF begin
> lemma oracle_test: "A ⟶ A & B"
>   apply (rule impI)
>   apply (rule conjI)
> apply (tactic {* fn thm =>
>   let
>     val _ = writeln "aaa" ;
>     val _ = writeln (@{make_string} thm) ;
>     val cps = Drule.cprems_of thm ;
>     val _ = writeln "ccc" ;
>     val _ = writeln (@{make_string} cps) ;
>     val _ = writeln "ddd" ;
>   in Seq.succeed thm end ; *})
> At this point it seems clear that the tactic is executed twice, the
> first time seemingly with an argument thm which gets printed out as
> "TERM _", and the second time with the actual goal state.
> Why is this?  What's going on here?  Is this how apply tactic ... should
> be used?

Since tactics are by definition lazy and value-oriented, the system is
free to run them many times. Here it happens to be twice, because of an
additional stage to "intern" the proof method expression; in other
situations it might be more than twice.

The writeln invocations above are not value-oriented, thus you see such
implementation details in the experiment. In production use, you would
never emit such messages from a tactic.

If you want to experiment with Isar goal states, it works better via the
ML_val command with the @{Isar.state} antiquotation. You can put various
auxiliary ML val bindings into ML_val, but cannot export a modified
proof state.

Anyway, can you generally say what you are trying to do? So far I merely
see attempts to fit the mindset of a different proof assistant
(Isabelle98) to Isabelle2017. There is a common name prefix, but almost
everything else has changed since then.

To get started with Isabelle2017, I recommend to ignore Isabelle/ML
altogether, and do definitions, statements, proofs in the Isar source
language. Then maybe get acquainted with Eisbach for user-defined proof


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