Re: [isabelle] tactic being executed twice





On 06/06/2018 12:45 AM, Makarius wrote:
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
methods.


	Makarius

Hi Makarius,

Well, if the system is going to run a tactic twice, one with a phoney goal "TERM _", and then once with the actual goal, and it fails the first time (because the subgoal list is empty), that's not going to be much use. Under what conditions is apply (tactic ...) usable?

No, I realise that in production use I wouldn't be printing "aaa", "bbb", etc. They're there for the purpose of debugging. Without them I wouldn't have realised that the system was running the tactic twice, and that "TERM _" must refer to what it uses as the goal state the first time.

What I'm doing right now is trying to code up an absurdly trivial example of a tactic which should succeed using an absurdly trivial oracle, which isn't included in the code I showed, but fails in the same way (at least, the same, in that the tactic gets applied to a goal which does not have the requisite number of subgoals).

Like printing "aaa", etc, using apply (tactic ...) was for the purpose of debugging - ie exploring why it doesn't work.

Jeremy





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