Proving Theorems by Using Abstraction Interactively