Re: [isabelle] Creating simple tactics



Greg Bronevetsky wrote:
I'm trying to write tactics that are more complex than the basic constructs supported by Isar. In particular, I'd like to be able to use the ALLGOALS tactic. The first thing I tried was embedding ML code into tactics like in the following example:
   apply(tactic {* Addsimps[Let_def]; ALLGOALS(Simp_tac) *})
While more basic versions of the above seem to work, the above example does not. It appears that Simp_tac does not unfold my let definitions, meaning that my call to Addsimps[Let_def] fails to add Let_def to the simp set. Why not? How else would I do this?



Addsimps modifies the simpset associated with the current theory,
and Simp_tac uses it (as does simpset ()).
First point: Is the above really what you want, or rather
ALLGOALS (simp_tac (simpset () addsimps [Let_def])) ?

Second point:
In translating Isabelle proofs into Isar I've found that things depending on the notion of the current theory are liable to misbehave
(including what I've written above).

In Isar I would have to write (in place of my version above),
SIMPSET (fn ss => ALLGOALS (simp_tac (ss addsimps [Let_def]))).

See 10.2.3 of the reference manual.

However I have found in Isar that
ML {*
Addsimps [xxx] ;
*}
seems to work as expected.

Regards,

Jeremy





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