Правило индукции в Изаре

Question

Я хочу сделать индукцию правила в Изабель / Изаре. Я считаю, что

proof (rule_tac P="λn. f n ≥ n ∧ f n ≥ 1" in f.induct)

или

proof (rule f.induct[of "λn. f n ≥ n ∧ f n ≥ 1"])

делают именно то, что я хочу. Но как я могу написать эту строку, используя «новый стиль» Изара? Как видите, я просто пытаюсь рассказать Изабель, как создать экземпляр переменной P в правиле индукции для моей функции f.

Answer 1

Я бы сказал, что вы уже используете стиль Изар, поскольку здесь нет apply.

Вы также можете использовать синтаксис f.induct[where P="λn. f n ≥ n ∧ f n ≥ 1"].

Кроме того, часто это не нужносоздать экземпляр P вручную, так как объединение даст вам P. Может быть, вам нужно переформулировать свою цель для достижения этой цели. В стиле Isar унификация также происходит после proof, когда вы запускаете show, так что это еще один вариант, чтобы не указывать его явно.