Vincent, you gave me a nice exercise which I'll try to work, but it dawned on me that we can't use that unless we permanently change the parser. E.g. every time I use miz3, I have to change the parser for that entire HOL Light session. The same thing goes for your nice hack of quotexpander: it hold for the entire HOL Light session. Is that right? In that case, I think it would not be a good idea to install that in HOL Light, I think, as the benefit so far (improving case & consider a bit) is too low. I think the benefit of changing the parser permanently would be high enough if we could always infer the type of a variable in the scope of a variable binding.
Petros, I have some understanding now of your X_MATCH_CHOOSE_TAC: the variable x' doesn't need a type annotation that X_CHOOSE_TAC would need, because it infers the type from the existential statement xth by xtm = concl xth x,bod = dest_exists xtm (type_of x) Is that more or less correct? I know I'm missing a lot of details. I couldn't understand how rule_tac worked. I didn't understand much of your Isabelle Light paper, so I wonder if you can try to apply your skills to my problems. First, I'd like to be able to pluck the type of a variable out of the "environment". I don't think you're doing that. I think you can only infer the type of a variable in very specific circumstances. Let's fix the manual example for X_CHOOSE_TAC: g `(?y. x = y + 2) ==> x < x * x`;; e(DISCH_THEN(X_CHOOSE_TAC `d:num`));; e(ASM_REWRITE_TAC[] THEN ARITH_TAC);; needs "IsabelleLight/make.ml";; g `(?y. x = y + 2) ==> x < x * x`;; e(DISCH_THEN(X_MATCH_CHOOSE_TAC `d`));; e(ASM_REWRITE_TAC[] THEN ARITH_TAC);; So we got rid of a type annotation :num, but we inferred it from something nearby, the (?y. x = y + 2) that we just discharged. Is that right? Well, how about something else nearby. How about we try to define a function consider of type term -> string -> term -> term so that consider `x` "such that" `t`;; would evaluate to the term `?x. t` and x would not be typed, but would infer its type from the term `t`. Can you do that? If we know that a variable x occurs free in a term, can you access the type of x by IsabelleLight techniques? -- 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
