[isabelle] Creating simple tactics



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?

I also tried following the directions laid out in a post by Lucas Dixon from last year but am having trouble. He points to src/Provers/simplifier.ML as an example of what to do but I can't seem to get a simple enough subset of the code in this file or other files to work and I don't understand enough of what's happening in these files to figure out why my simple examples break. Is there any documentation on how to create simple tactics and make them available in Isar? Is there a simple example that just creates a basic tactic?

--
                            Greg Bronevetsky






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