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

Reply via email to