[isabelle] Tactic Emulation



An offline discussion revealed that the problem was due to 
non-existing ML-bindings for theorems one proves in ones own 
theories. While theorems, like conjI from HOL, have an ML-binding 
with the same name, ones own theorems must be fetched from 
the theorem-database. This can be done with the functions 
"thm" and "get_thm".

Christian

Peter Chapman writes:
 > Thanks Christian
 > 
 > This sounds like the kind of thing I want to do, but I've hit a snag  
 > in implementing your suggestion of writing the tactics in ML and then  
 > using this directly in Isar.
 > 
 > Say I have a lemma " |- A --> A --> A --> A", then using the Isar  
 > method of doing things, I use
 > 
 > apply ((rule impr)+)?
 > 
 > which returns
 > 
 > Subgoal:
 > 
 > A, A, A |- A
 > 
 > as expected.  However, if I use the direct tactic from Isabelle
 > 
 > apply (tactic {* REPEAT (rtac impr 1) *} )
 > 
 > I simply get back the original goal; the rule fails to be applied  
 > even once.  This was confirmed when I tried
 > 
 > apply (tactic {* rtac impr 1 *} )
 > 
 > which fails.  After scouring the manuals for both Isar (Appendix B:  
 > Converting between Isabelle and Isar) and Isabelle (Chapters 3 and  
 > 4), I cannot figure out why the two representations do not have the  
 > same behaviour.  If it is important, the theorems are declared in a  
 > file called G3cp.thy, which is included in the file where I am  
 > actually performing the calculations, G3cpExamples.thy.
 > 
 > Thanks
 > 
 > Peter
 >   





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