Можно ли написать неавтоматизированные c формализации в Изаре?

Question

У меня есть следующее:

lemma 
  assumes p: "P"
  assumes pimpq: "P⟶Q"
  shows "P∧Q"
proof -
  from pimpq p have q: "Q" by (rule impE)
  from p q show ?thesis by (rule conjI)
qed

Я думал, что это до базовых c правил вывода, но читал документацию по rule в разделе 9.4.3 Structured Methods Справочного руководства по Изару. Оказалось, что он использует Классический Разумник с различными правилами. Кроме того, замена предложений by на .. также решает задачи, поэтому упоминание об исключении подтекстов и введении конъюнкции не является обязательным.

Можно ли написать строгую формализацию здесь, в Изаре, то есть не использовать какая-нибудь автоматизация и дополнительные правила, которые не указаны в тексте программы? Что-то вроде прямого доказательства в HOL4.

Answer 1

Вы можете использовать Pure.rule, если не хотите использовать модуль classical.

lemma 
  assumes p: "P"
  assumes pimpq: "P⟶Q"
  shows "P∧Q"
proof -
  from pimpq p have q: "Q" by (Pure.rule impE)
  from p q show ?thesis by (Pure.rule conjI)
qed

Если вы напишите .. Изабель автоматически выберет правило на основе отмеченных лемм с атрибутом [intro] или [elim].

Может быть, вы также можете поделиться своим доказательством HOL4, которое вы хотите воспроизвести в Изабель, чтобы мы могли предложить эквивалент в Изабель / HOL.