Re: [isabelle] can't prove "True => True"



On Mon, 2008-11-10 at 00:57 +0900, Duraid Madina wrote:
> [...] I am not sure why, for example,
> 
> lemma doh:
>  "1+1=(3::nat) --> 1+1=(4::nat)"
> apply(eval)
> done
> 
> works, but
> 
> lemma doh:
>  "1+1=(3::nat) ==> 1+1=(4::nat)"
> apply(eval)
> done
> 
> fails. Is this exception the intended behaviour for the latter case?

I don't know if the above is the intended behavior, but in any case you 
can replace the meta implication ==> by a HOL implication --> using

  apply (erule rev_mp)

More generally, you can replace meta connectives by HOL connectives
using

  apply (atomize (full))

(See page 107 of the Isabelle/Isar Reference Manual for details.)

Best,

    Tjark






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