Re: [isabelle] A simple lemma



On Mon, 7 May 2012, John Munroe wrote:

I'm having trouble proving the following, could someone please help?

axiomatization
T :: "real set" and
S :: "real set" where
ax1: "T = {1,2}" and
ax2: "S = {1,2,3}"

lemma "ALL t:T. EX s : S. even t <-> s*t=6"

I expect it to be true since only 2 in T is even.

Axiomatizations are bad by default; better use a local context.

In Isabelle2012 (e.g. RC2) you can do it like this:

  context
    fixes T :: "real set"
      and S :: "real set"
    assumes ax1: "T = {1,2}"
      and ax2: "S = {1,2,3}"
  begin

  lemma "ALL t:T. EX s : S. even t <-> s*t=6"

Incidently, this then reveals a more explicit type error than in Isabelle2011-1, as Jasmin has already pointed out.


	Makarius





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