Petros, I think this is a pretty good exercise for a novice (unless they use MESON_TAC[], which solves it instantly):
g `P ==> (P==>Q) ==> Q`;; e (REPEAT DISCH_TAC);; e (FIRST_ASSUM (fun x -> FIRST_ASSUM (fun y -> ACCEPT_TAC (MP x y))));; I'm still kind of a novice myself, so I tried to solve it using John and Marco's readable code ideas: let USE2THEN a b thm2tactic = USE_THEN a (fun x -> (USE_THEN b (fun y -> thm2tactic x y)));; g `P ==> (P==>Q) ==> Q`;; e(INTRO_TAC "p; pq");; e(USE2THEN "pq" "p" (fun x y -> ACCEPT_TAC (MP x y)));; I'd say this is simpler because my fun x y -> ACCEPT_TAC (MP x y) is pretty simple, just a version of ACCEPT_TAC o MP, and we can write USE2THEN ourselves, and explain to the novice how to use USE2THEN and that USE_THEN is explained in the HOL Light reference manual. Probably your fix is even simpler. Thanks for your explanation of the 4 * rule tactics, but I'm sorry to say that I'm not really getting it. I'll try to read your paper with Jacques An Isabelle-Like Procedural Mode for HOL Light more carefully, but it would really help if I had an example that I already understood. I wonder if you could translate part of Examples/inverse_bug_puzzle_tac.ml from the latest subversion (159) into you IsabelleLight framework. That is, I've been using the readable code framework of John, Freek and Marco, but I think you and Jacques are working in a very different framework. I'm already sold on your code (that's great how you can remove type annotations), so I expect to benefit from understanding your framework as well. -- Best, Bill ------------------------------------------------------------------------------ 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
