On 05/04/2013 04:55, Bill Richter wrote: > Petros, your consider code is a huge step toward what I need. I'll try to > finish modifying your code tonight.
I am glad you found it helpful! > > I really like your code, and I wonder if you can't do even better. I feel > that we should never have to make an explicit type annotation of a variable > that is in the scope of a typed variable. Assuming that's the right > terminology. So there ought to be an "environment" out of which variable > typing can be pulled. Obviously the values of the variables, once they're > typed correctly, can be pulled out of this "environment". Yes that would be something interesting to implement. For example, when saying "consider x such that t", perhaps "t" contains other variables that are mentioned in the current proof context. It would be nice if you didn't have to annotate them with their types either. In Isabelle Light, the proof context is merely the current goal, so I am using this function (from IsabelleLight/support.ml) to match and retrieve the types of the "environment": let gl_frees : goal -> term list = fun (asl,w) -> itlist (union o thm_frees o snd) asl (frees w);; I am not sure if this is as straightforward in a declarative style. > > BTW maybe you can post here the point of the IsabelleLight code you and > Jacques wrote. I think the MizarLight stuff doesn't require you to > understand Mizar, it's all explained in the HOL Light tutorial in the section > "Towards more readable proofs", but maybe IsabelleLight requires you to > understand Isabelle, and I don't. > I will try and do this as concisely as possible. There are two main reasons why we implemented Isabelle Light: 1) Manipulation of assumptions in traditional HOL proofs is fairly limited, especially for novice users. This is simply not the "HOL style" of proving things. For example, assume a novice user does this: g `P ==> (P==>Q) ==> Q`;; e (REPEAT DISCH_TAC);; Even though the proof is a straightforward application of modus ponens on the assumptions, it is not that straightforward how they (being a novice user) would do this in HOL Light: e (FIRST_ASSUM (fun x -> FIRST_ASSUM (fun y -> ACCEPT_TAC (MP x y))));; 2) There is *at least* one tactic (backwards) and one rule (forward) for each natural deduction inference step in HOL Light. These are too many! (I still keep a printed copy of VERYQUICK_REFERENCE.txt pinned on my office wall, and that is far from containing all the available and useful tactics.) In Isabelle's procedural mode, you can express, prove, and use any custom made inference rule, both forwards and backwards, and manipulate the assumptions in a very precise manner using the 4 *rule tactics: rule: for backward/introduction steps drule, frule: for forward/destruction steps erule: for elimination (simultaneous forward and backward) steps (for more details see Section 3.2 of our paper [1]). Each of those can be used with any custom rule described using Isabelle's meta-logic. Inspecting rules is more straightforward than remembering tactics. Even more so, proving new rules is *much* easier than creating new tactics. You only need to remember the functionality of 4 tactics and the names of the rules. Also, their *rule_tac counterparts allow you to partially instantiate a rule using expressions from the context in order to have a more precise application of the rule (for example in order to resolve ambiguity between two equally matching assumptions in a forward rule). In Isabelle Light, we emulate Isabelle's meta-logic (with a few limitations of course), the four tactics, and a few other useful features. The proof of the previous example can be completed as follows: (* mp is the modus ponens rule: |- (p ==> q) ===> p ===> q *) e (drule mp);; e (assumption);; e (assumption);; Avoiding explicit type annotations in the *rule_tac instantiations is what lead to our current discussion! As an example, in the proof above you could do: e (drule_tac [`p`,`P`] mp);; which means "instantiate variable p in the mp rule with expression P in the goal, then use it as a destruction/forward rule)". Notice the lack of typing information (`:bool`) for `p` and `P`, which would otherwise make the script much more cumbersome. The type of `p` is determined by the rule, and the type of `P` by the goal/context. Regards, Petros [1] Papapanagiotou, P. and Fleuriot, J.: An Isabelle-Like Procedural Mode for HOL Light. Logic for Programming, Artificial Intelligence, and Reasoning, pp 565-580, Springer (2010) -- 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
