Re: [isabelle] using HOL.contrapos_pp



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

> On 28 Jul 2015, at 19:40, Gergely Buday <gbuday at gmail.com> wrote:
> 
> 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.