Существуют простые правила, которые позволяют упрощающему делать это автоматически:
lemma "prime (5 :: nat)"
by simp
Для больших чисел (например, 137) это займет несколько секунд, а для гораздо больших чисел этополностью непригоден для использования.
Вы также можете использовать eval вместо simp, который проходит через оракула оценки Изабель для оценки утверждения внутри стандарта ML, а затем переосмысливает результат как теорему в Изабель.В зависимости от того, кого вы спрашиваете, это может показаться немного менее заслуживающим доверия, чем simp.
Наконец, есть запись о Сертификатах Pratt в Архив формальных доказательств также предоставляет метод проверки под названием pratt, который может автоматически доказать простоту числа с помощью сертификатов Pratt.Это немного более эффективно, чем использование simp, но все же не подходит для действительно больших чисел.
В любом случае, для небольших чисел, таких как 5 и 7, by simp - это путь.
Обратите внимание, что вы должны указать тип, то есть prime (5 :: nat) или prime (7 :: int).Если вы просто напишите prime 5, тип, который выводится для 5, является слишком общим.Например, prime (5 :: real) - это , а не true, поскольку поля не содержат простых чисел.