Re: [isabelle] using HOL.contrapos_pp



On Tue, 28 Jul 2015, Gergely Buday wrote:

lemma "A â B"
proof (erule_tac Q="A" in HOL.contrapos_pp)

ends up in

goal (1 subgoal):
1. Â B â Â A

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"

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


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.