I wrote my type annotation reducing versions of EXISTS_TAC and X_GEN_TAC, and
cleaned up the code, with
let (make_env: goal -> (string * pretype) list) =
fun (asl,w) -> map ((fun (s,ty) -> s,pretype_of_type ty) o dest_var)
(freesl (w::(map (concl o snd) asl)));;
let parse_env_string env s = (term_of_preterm o retypecheck env)
((fst o parse_preterm o lex o explode) s);;
let (subgoal_THEN: string -> thm_tactic -> tactic) =
fun stm ttac (asl,w) ->
let wa = parse_env_string (make_env (asl,w)) stm in
let meta,gl,just = ttac (ASSUME wa) (asl,w) in
meta,(asl,wa)::gl,fun i l -> PROVE_HYP (hd l) (just i (tl l));;
let (exists_TAC: string -> tactic) =
fun stm (asl,w) -> let env = make_env (asl,w) in
EXISTS_TAC (parse_env_string env stm) (asl,w);;
let (X_gen_TAC: string -> tactic) =
fun svar (asl,w) ->
let vartype = (snd o dest_var o fst o dest_forall) w in
X_GEN_TAC (mk_var (svar,vartype)) (asl,w);;
Mark, let me try again with mathematicians and free variables. Suppose we're
trying to prove a math theorem with quantifiers, say a result that Rob
formalized:
Theorem:
For all all topological spaces X and Y and for all covering space
projections p: X ---> Y, p is a fibration.
Proof:
Let X and Y be topological spaces, and let p: X ---> Y be a covering space
projection.
[...]
I've always thought of the math-proof "let" as binding a variable, so the three
"let * be * " phrases above bind the variables X, Y and p. These bindings have
scope, and it feels exactly like variable bindings and scope just like in a
programming language. In ML, variable bindings are given by "let" and scope is
indicated by "in". So I just assumed that the ML/math-proof "let" variable
binding as the same idea as GEN_TAC, X_GEN_TAC, and my favorite, INTRO_TAC,
which in miz3 is actually written as "let".
But I now think I was completely mistaken. GEN_TAC is not like the ML "let"
variable binding. Instead, GEN_TAC turns the goal from a universal statement
to a statement with free variables, the statement given by getting rid of the
quantifier. Which means that HOL is based on statement with free variables.
Somehow I never realized this obvious fact. I know John pointed out in his
purple book that he was using free variables more often than is often customary
in Math Logic texts, but I didn't pick up on that. I'm not thinking this is
something that's poorly explained in the HOL dox. I think it's just something
I missed this all along.
Once I realized that my binding/scope was all contained in free variables, I
knew all I had to do to build my environment is just to access the statements
in the assumption list that I refer to in the proof of the SUBGOAL_TAC
statement. But it was easier to just grab the entire assumption list and the
goal.
Petros, the very first thing I did was to rewrite the function BuildExist you
wrote for me in Examples/inverse_bug_puzzle_tac.ml as the much shorter (uh,
without any of your error checking)
let buildexist xs t =
let env = map ((fun (s,ty) -> s,pretype_of_type ty) o dest_var) (frees t) in
let x = (term_of_preterm o retypecheck env)
((fst o parse_preterm o lex o explode) xs) in
mk_exists (x,t);;
--
Best,
Bill
------------------------------------------------------------------------------
Introducing AppDynamics Lite, a free troubleshooting tool for Java/.NET
Get 100% visibility into your production application - at no cost.
Code-level diagnostics for performance bottlenecks with <2% overhead
Download for free and get started troubleshooting in minutes.
http://p.sf.net/sfu/appdyn_d2d_ap1
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
