Rob, I learned a lot from your post! My conclusion is that in both HOL Light and HOL4, {f x | R x} = λa. ∃x. R x ∧ a = f x for some variable a than is not free in R x or f x. I judge both HOL approaches to have pluses & minuses, and can't rate one above the other:
1) In HOL Light, the proof of this equation is immediate, as parser defines {f x | R x} to be the RHS. However, we always generate a fresh variable, ones with odd-sounding (although unseen) names like GEN%PVAR%1066. 2) In HOL4, the parser's definition of {f x | R x} involves no fresh variables, but calculating a in the above equation was beyond my skill/patience here, as there are many cases to consider. # dest_comb `{f x | R x}`;; val it : term * term = (`GSPEC`, `\GEN%PVAR%1066. ?x. SETSPEC GEN%PVAR%1066 (R x) (f x)`) I like this approach for its simplicity: ``Let's choose a fresh variable, whether we need it or not, without studying the free & bound variables.'' The HOL4 approach, as you explained it, looks more elegant, but if you want to understand what alpha-conversions take place, you need a serious investigation that I couldn't complete here. Let me make a two minor changes to your code: # let HOL4_GSPEC = new_definition `HOL4_GSPEC = (\f. (\v. ?r. f r = (v, T)))`;; Let's study your {f x | R x} = HOL4_GSPEC (λx. (f x, R x)) : HOL4_GSPEC (λx. (f x, R x)) = (λf. (λv. ∃r. f r = (v, T))) (λx. (f x, R x)) = λv. ∃r. (λx. (f x, R x)) r = (v, T) as long as v and r are not free in (λx. (f x, R x)). Assuming this, and that r is not a bound variable in (f x, R x), we have = λv. ∃r. (f r, R r) = (v, T) = λv. ∃r. f r = v ∧ R r and that's correct! But if any of the assumptions above don't hold, we'll have to alpha-convert if we want to make it this far. I couldn't figure the whole story out, but here are three alpha-conversion examples, the first when r is bound in (f x, R x). needs "RichterHilbertAxiomGeometry/readable.ml";; (* extensively commented *) let HOL4_GSPEC = NewDefinition `; HOL4_GSPEC = (λf. (λv. ∃r. f r = (v, T)))`;; interactive_goal `; f = (λx. (λr. r + x)) ⇒ {f x | R x} = HOL4_GSPEC (\x. (f x, R x)) `;; interactive_proof `; intro_TAC fDef; rewrite SETSPEC GSPEC HOL4_GSPEC PAIR_EQ; `;; `(\GEN%PVAR%479. ?x. R x /\ GEN%PVAR%479 = f x) = (\v. ?r. f r = v /\ R r)` The whole point is the next step, where I expected alpha-conversion of the outer (existential) r: interactive_proof `; rewrite fDef; `;; `(\GEN%PVAR%479. ?x. R x /\ GEN%PVAR%479 = (\r. r + x)) = (\v. ?r. (\r'. r' + r) = v /\ R r)` I was wrong; it was the inner (abstraction) r that was alpha-converted. Here's an example with ¬(r = x) and r free in (f x, R x): interactive_goal `; f = (λx. r + x) ⇒ {f x | R x} = HOL4_GSPEC (\v. (f v, R v)) `;; interactive_proof `; intro_TAC fDef; rewrite fDef; rewrite HOL4_GSPEC PAIR_EQ; `;; `{r + x | R x} = (\v. ?r'. r + r' = v /\ R r')` Now the outer (existential) r was alpha-converted. Here's an example where ¬(v = x), v is free in (f x, R x), and r is not free in (λx. (f x, R x)). interactive_goal `; f = (λx. v + x) ⇒ {f x | R x} = HOL4_GSPEC (\x. (f x, R x)) `;; interactive_proof `; intro_TAC fDef; rewrite fDef HOL4_GSPEC PAIR_EQ ; `;; `{v + x | R x} = (\v'. ?r. v + r = v' /\ R r)` I finally got what I wanted, and HOL Light-type alpha-conversion. Let's make it look even nicer: interactive_proof `; ∀y. v + y = f y [fApplied] by fol fDef; rewrite fApplied; `;; `{f x | R x} = (\v'. ?r. f r = v' /\ R r)` Let me address my lack of skill/patience. Alpha-conversion will be needed iff ¬(v = x) and v is free in (f x, R x) \/ ¬(r = x) and r is free in (f x, R x) \/ r is bound in (f x, R x). I guess that's only 4 cases, as the 2nd and 3rd disjuncts are disjoint, and my 3 examples touched on all 4. I should try to work this exercise. I suppose after all this I should re-prove your theorem: let thm1 = theorem `; {f x | R x} = HOL4_GSPEC (\x. (f x, R x)) proof rewrite HOL4_GSPEC PAIR_EQ EXTENSION IN_ELIM_THM; fol; qed; `;; val thm1 : thm = |- {f x | R x} = HOL4_GSPEC (\x. f x,R x) The HOL4 design sees two abstractions here: `\(x, y, z). f x y z` and `\(x, y, z). R x y z` and combines them together into one abstraction `\(x, y, z). (f x y z, R x y z)`. This contains all the information needed to construct the set comprehension and the HOL4 formulation of GSPEC captures that construction. Wow, that's cool! Is this due to Konrad and Michael, or does it go way back? I never would have thought of such stunts. Here's two proof: HOL4_GSPEC (λ(x, y, z). (f x y z, R x y z)) = (λv. ∃r. (λ(x, y, z). (f x y z, R x y z)) r = (v, T)) = Now r must be a triple r = (a, b, c), and then = (λv. ∃a b c. v = f a b c ∧ R a b c) = {f x y z | R x y z} let thm3 = theorem `; {f x y z | R x y z} = HOL4_GSPEC (λ(x, y, z). (f x y z, R x y z)) proof rewrite HOL4_GSPEC PAIR_EQ IN_ELIM_THM EXISTS_PAIR_THM EXTENSION IN_ELIM_THM; fol; qed; `;; Warning: inventing type variables 0..0..0..solved at 3 0..0..0..solved at 3 val thm3 : thm = |- {f x y z | R x y z} = HOL4_GSPEC (\(x,y,z). f x y z,R x y z) Actually I got a pretty-printer error that seems serious enough to switch to standard usage: let HOL4_GSPEC = new_definition `HOL4_GSPEC = (\f. (\v. ?r. f r = (v, T)))`;; g `{f x y z | R x y z} = HOL4_GSPEC (\(x, y, z). (f x y z, R x y z))`;; e(REWRITE_TAC [HOL4_GSPEC; PAIR_EQ; IN_ELIM_THM; EXISTS_PAIR_THM; EXTENSION; IN_ELIM_THM]);; `!x. (?x y z. R x y z /\ x = f x y z) <=> (?p1 p1 p2. f p1 p1 p2 = x /\ R p1 p1 p2)` That looks like a variable capture error (on top of the repeated p1), one that we know (since the theorem was proved) didn't actually take place. The pretty-printer ought to have printed `!x'. (?x y z. R x y z /\ x' = f x y z) <=> (?p1 p1 p2. f p1 p1 p2 = x /\ R p1 p1 p2)` I see the same pretty-printer error occurred in your theorem: interactive_goal `; {f x | R x} = HOL4_GSPEC (\x. (f x, R x)) `;; interactive_proof `; rewrite HOL4_GSPEC PAIR_EQ EXTENSION IN_ELIM_THM; `;; # val it : goalstack = 1 subgoal (1 total) `!x. (?x. R x /\ x = f x) <=> (?r. f r = x /\ R r)` Does anyone understand the HOL Light pretty-printing of freshly generated variables, or know where it's done? -- Best, Bill ------------------------------------------------------------------------------ Rapidly troubleshoot problems before they affect your business. Most IT organizations don't have a clear picture of how application performance affects their revenue. With AppDynamics, you get 100% visibility into your Java,.NET, & PHP application. Start your 15-day FREE TRIAL of AppDynamics Pro! http://pubads.g.doubleclick.net/gampad/clk?id=84349831&iu=/4140/ostg.clktrk _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info