Email Gateway (Aug 22 2022 at 10:42): Email Gateway (Aug 22 2022 at 10:42):From: Gergely Buday <gbuday@gmail.com>
Hi,
lemma "A ⟹ B"
proof (erule_tac Q="A" in HOL.contrapos_pp)
ends up in
goal (1 subgoal):
as expected, a standard proof method.
However, on
lemma "(⋀ thesis. (⋀ n. Q n ⟹ thesis) ⟹ thesis) ⟹ (∃ n. Q n)"
proof (erule_tac Q="(⋀ thesis. (⋀ n. Q n ⟹ thesis) ⟹ thesis)" in
HOL.contrapos_pp)
the system complains that
Type unification failed: Clash of types "prop" and "bool"
Failed to meet type constraint:
Term: ⋀thesis. (⋀n. Q n ⟹ thesis) ⟹ thesis :: prop
Type: bool
gives some clue and refers to section 2.2 of the Isabelle/Isar
reference manual but it is not clear how could I use contrapos_pp on a
complex premise.
What should I do here?
Email Gateway (Aug 22 2022 at 10:43):From: Larry Paulson <lp15@cam.ac.uk>
Simply, it can’t be done, as contrapos_pp is for booleans only. No such principle exists at the meta-level, which is intuitionistic.
Larry
Email Gateway (Aug 22 2022 at 10:43):From: Makarius <makarius@sketis.net>
Larry is right that Pure does not support classical non-sense. The premise
above can be compacted, though, to fit into HOL, e.g. like this:
lemma "(⋀thesis. (⋀n. Q n ⟹ thesis) ⟹ thesis) ⟹ (∃n. Q n)"
apply atomize
apply (erule contrapos_pp)
oops
There is not much point to do this. Here is a Pure proof of the
same statement:
lemma
assumes r: "⋀thesis. (⋀n. Q n ⟹ thesis) ⟹ thesis"
shows "∃n. Q n"
proof (rule r)
fix n
assume "Q n"
then show ?thesis ..
qed
Here is the same proof with less Isar text:
lemma
assumes r: "⋀thesis. (⋀n. Q n ⟹ thesis) ⟹ thesis"
shows "∃n. Q n"
by (rule r) (rule exI)
Makarius
Last updated: Apr 20 2024 at 04:19 UTC