Re: [isabelle] variable in Isar?



Dear Gergely,

- inside a proof you can use:

let ?elem = "..."

- in a lemma "heading" you can use:

lemma
  defines "elem == ..."
  assumes "..."
  shows "..."

with corresponding fact "elem_def"

- for a gobal definition you can use the usual "definition" command

- for a non-global definition that might span several lemmas you can use

context
  fixes elem
  assumes "elem = ..."
begin

...

end

However, your specific example does not make sense, since it is not well-typed. Maybe you wanted to have something like "SOME x. x : {x. even x}" (i.e., an arbitrary element from the set "{x. even x}").

cheers

chris

On 07/06/2012 03:43 PM, Gergely Buday wrote:
Hi,

is it possible to define a variable in Isar, like

   var elem = SOME x. {x. even x}

and then use it later?

- Gergely








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