Isabelle
theorem proverのひとつ