[isabelle] instantiation order for a record



Dear Isabelle community,

I am having trouble instantiation the typeclass order for one of my records.
Actually, the problem exists whenever the typeclass has parameters, to
be defined.

The error message is not particularly helpful to me.
*** Bad head of lhs: existing constant "op \<le>"
*** The error(s) above occurred in definition:
*** "A \<le> B \<equiv> lesseqTESTRECORD A B"

The online manual did not help me much in this case either; I tried
unsuccessfully to translate the examples from the manual to my case.

Hopefully somebody can give me a hint on what to change to get to the
point where the proving can start.

Cheers,
Sven

==============================
TESTRECORD.thy BEGIN
==============================
theory TESTRECORD
imports
  Main

begin

record 'a TESTRECORD =
  prefix_elem :: "'a set"

definition lesseqTESTRECORD :: "'a TESTRECORD \<Rightarrow> 'a
TESTRECORD \<Rightarrow> bool" where
  "lesseqTESTRECORD D1 D2 \<equiv> (prefix_elem D1 \<subseteq>
prefix_elem D2)"

definition lessTESTRECORD :: "'a TESTRECORD \<Rightarrow> 'a TESTRECORD
\<Rightarrow> bool" where
  "lessTESTRECORD D1 D2 \<equiv> lesseqTESTRECORD D1 D2 \<and> D1\<noteq>D2"

instantiation "TESTRECORD_ext" :: (type,type) order
begin

print_context

definition
  less_eq_TESTRECORD_ext_def: "less_eq A B = lesseqTESTRECORD A B"

definition
  less_TESTRECORD_ext_def: "less A B = lessTESTRECORD A B"

instance proof
==============================
TESTRECORD.thy END
==============================




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