[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.