Vince, thanks for improving my code! I've implemented Freek's 1-line "by"
proofs, so I can shorten your proof a bit:
let INTERIOR_EQ = theorem `;
∀s. interior s = s ⇔ open s
by simplify interior_DEF OPEN_IN SUBSET_UNIV TOPSPACE_EUCLIDEAN InteriorEq
EQ_SYM_EQ`;;
But why does this work? Let's run my old proof interactively
interactive_goal `;
∀s. interior s = s ⇔ open s
`;;
interactive_proof `;
simplify interior_DEF OPEN_IN SUBSET_UNIV TOPSPACE_EUCLIDEAN InteriorEq;
`;;
# val it : goalstack = 1 subgoal (1 total)
`!s. Interior euclidean s = s <=> s = Interior euclidean s`
I had no idea that's what happened. I should have checked. And that's exactly
what your EQ_SYM_EQ fixes! Thanks for the nice improvement. How do you like
my readable.ml, which of course you helped me write?
That looks like a good summary of the different tactics (thmlist->tactics I
mean), and I think the only thing I didn't know was
- if you have existentials or disjunctions in the theorems you want to
use or in the goal, use MESON_TAC
By putting this after SIMP_TAC, I infer that SIMP_TAC will not handle
existentials or disjunctions.
--
Best,
Bill
------------------------------------------------------------------------------
Managing the Performance of Cloud-Based Applications
Take advantage of what the Cloud has to offer - Avoid Common Pitfalls.
Read the Whitepaper.
http://pubads.g.doubleclick.net/gampad/clk?id=121054471&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
