Re: [isabelle] Partial Linear Arithmetic

P.S.: I still did not find the correct formula for the modular case, sample2.html. Isabelle declines to solve the lemma. Does anyone know, what's wrong there?

The "lemma" on your web page

lemma sample2: "(EX j::nat.(ALL r::int.(r-2*j<=1)))"

is not even syntactically well-formed, has a type problem (nat/int) and is definitely false. Your purported solution "j=2 dvd (r)" does not make sense because your quantifiers are in the wrong order. If you swap them and correct all the mistakes, it works:

lemma sample2: "ALL r::int. EX j. r - 2*j<=1"
by arith

Thanks to Amine.


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