Hello Bill,
On 02/04/2013 03:08, Bill Richter wrote: > Suppose we bind a variable x, say with INTRO_TAC, DESTRUCT_TAC or > X_CHOOSE_THEN, to a term t with type alpha. Then if the variable x occurs > in a term (in doublequotes) that is in the scope of this variable binding, x > ought to automatically be bound to t:alpha. We should not have to repeat the > type annotation of x. > > If that's what you did, Petros, that's fabulous, and will cut down on more > type annotations than my consider/case would. Freek's miz3 does something > like this I think, and I haven't figured out how he does it. Can you comment > on your Isabelle Light code? I'll go read your paper with Jacques Fleuriot > link.springer.com/chapter/10.1007%2F978-3-642-16242-8_40 The paper gives a good overview of what this library was built for. There is also a small README file in the library folder and the code is commented throughout. The main effort was to emulate Isabelle's procedural natural deduction tactics rule, erule, drule, and frule. In this, similarly to you, I wanted to get rid of unnecessary type annotations in situations where the type of an expression that is being provided by the user can be determined by the context of the particular proof step. I am not sure to what extent this is being done in INTRO_TAC and DESTRUCT_TAC as I haven't used or seen these tactics in detail (yet). It is very easy to write versions of X_CHOOSE_TAC, X_CHOOSE_THEN, X_GEN_TAC, and EXISTS_TAC that do this kind of type instantiation using the try_type function from my previous email. Regards, Petros -- Petros Papapanagiotou CISA, School of Informatics The University of Edinburgh Email: p.papapanagio...@sms.ed.ac.uk --- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. ------------------------------------------------------------------------------ Minimize network downtime and maximize team effectiveness. Reduce network management and security costs.Learn how to hire the most talented Cisco Certified professionals. Visit the Employer Resources Portal http://www.cisco.com/web/learning/employer_resources/index.html _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
