Re: [isabelle] Why is 'auto' slow here?



For your lemma to be true, ax1 should assert that the set Z is non-empty.

Stephan

On 22 Feb 2010, at 09:35, Tobias Nipkow wrote:

> I'm afraid your formulae are not well-formed. Never mind the "fx", but
> "EX Z < S. ALL x : Z" doesnt make sense. Pls send an actual theory that
> Isabelle is prepared to accept.
> 
> Tobias
> 
> munddr at googlemail.com wrote:
>> Hi,
>> 
>> I have the following and somehow 'auto' spends a lot of time and not
>> doesn't terminate:
>> 
>> consts
>> f :: "real => real"
>> g :: "real => real"
>> S :: "real set"
>> 
>> types S = "real set"
>> 
>> axioms
>> a1: "EX Z < S. ALL x : Z. fx ~= g x"
>> 
>> lemma lem: "EX Z < S. EX x : Z. fx ~= g x"
>> using a1
>> apply auto
>> 
>> For some reason, auto doesn't terminate. Shouldn't the lemma be
>> straightforward to prove given a1?
>> 
>> Thanks
>> John
> 
> 






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