Re: [isabelle] Definition in jEdit

On Mon, 21 May 2012, Abdullah wrote:

I tried to definition the *consts * but it give me error and I do not know
where is it.,,

Const1:: "type => type"

const_def : " Const1 A = Const1 B ==> A = B"

And the error message is

(((Not a meta-equality (==)
The error(s) above occurred in definition "injective_publicKey":
 "A = B" ))))

I am not sure what you are trying to do. The above is not a definition, it is a statement about injectivity of Const1.

You can achieve that as follows:

  datatype 'a test = Const1 'a
  lemma "Const1 A = Const1 B ==> A = B" by simp

Const1 as datatype constructor is injective, as demonstrated here, and a bit more according to the meaning of datatype.

Anyway, if you want to make plain definitions, use 'definition' or 'fun' as described in the Isabelle/Isar reference manual.


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