Q:

how to discover new lemma or guess or search the next lemma which want to be proved in Isabelle

i do not have example, but i googled some people can 
use Isabelle to search lemma and discover new lemma with Isabelle
do not know where give hints to discover or search next lemma after current lemma proved automatically
can you give examples that how to discover lemmas?

A:

Johansson et al. have recently presented a system for theory exploration, that is, coming up with lemmas based on your definitions. You can find their implementation on GitHub and the paper on arXiv. In the paper, you will also find a lot of examples. The only drawback is that, as far as I can tell, their implementation only works with Isabelle2013-2.
Johansson, Moa, et al. "Hipster: Integrating Theory Exploration in a Proof Assistant." Intelligent Computer Mathematics. Springer International Publishing, 2014. 108-122.

