# [isabelle] using HOL.contrapos_pp

Hi,
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"
Failed to meet type constraint:
Term: âthesis. (ân. Q n â thesis) â thesis :: prop
Type: bool
http://stackoverflow.com/questions/29032644/proving-a-simple-arithmetic-statement-with-rewriting-in-isabelle
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?
- Gergely

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