Re: [isabelle] Trouble with the Int Theory



Hi,

try 
      note [[ show_sorts]]
      thm of_int_eq_0_iff

here, you will see that the of_int_eq_0_iff lemma only works
if the right hand side is in the ring_char_0 typeclass. 

So make sure that your 0 on the RHS also is in this typeclass.

--
  Peter




On Fr, 2014-10-31 at 17:38 -0400, Scott Constable wrote:
> I am working on a proof which I was able to reduce to “of_int i = 0 ==> i = 0”. This seemed like a simple application of the rule “of_int_eq_0_iff” however I was unable to successfully apply this rule.
> On further probing I found that I was unable to prove the following lemma
> 
> lemma of_int_eq_0_imp1: “of_int i = 0 ==> i = 0”
> 
> by any means whatsoever. That is, unless I declare the lemma within the context ring_char_0. Then the lemma can easily be proved as follows:
> 
> context ring_char_0 begin
> lemma of_int_eq_0_imp1: “of_int i = 0 ==> i = 0”
> using of_int_eq_iff [of i 0] by simp
> end
> 
> But then I cannot apply this lemma outside of this context, which is what my main theorem requires (it resides within a different context).
> 
> Any help would be greatly appreciated.






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