*To*: Sven Schneider <Sven.Schneider at TU-Berlin.DE>, <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] instantiation order for a record*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Wed, 30 Oct 2013 13:52:30 +0100*In-reply-to*: <5270E2E8.1010404@TU-Berlin.DE>*References*: <5270E2E8.1010404@TU-Berlin.DE>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.0

Dear Sven,

Hence, your definition of less_eq should have the type ('a, 'b) TESTRECORD_ext => ('a, 'b) TESTRECORD_ext => bool However, type inference computes the type 'a TESTRECORD => 'a TESTRECORD => bool where 'a TESTRECORD abbreviates ('a, unit) TESTRECORD_ext, i.e, the type is too specialised.

2. The comparison is extended point-wise to the extension of the record (more D1 <= more D2)

definition lesseqTESTRECORD :: "('a, 'b :: ord) TESTRECORD_ext \<Rightarrow> ('a, 'b) TESTRECORD_ext \<Rightarrow> bool" where "lesseqTESTRECORD D1 D2 \<equiv> (prefix_elem D1 \<subseteq> prefix_elem D2) & more D1 <= more D2"

\<Rightarrow> bool" where "lessTESTRECORD D1 D2 \<equiv> lesseqTESTRECORD D1 D2 \<and> D1\<noteq>D2" instantiation "TESTRECORD_ext" :: (type,order) order begin

http://afp.sourceforge.net/browser_info/devel/AFP/Containers/Unit_Instantiations.html

Best, Andreas On 30/10/13 11:43, Sven Schneider wrote:

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 ==============================

**Follow-Ups**:**Re: [isabelle] instantiation order for a record***From:*Sven Schneider

**References**:**[isabelle] instantiation order for a record***From:*Sven Schneider

- Previous by Date: Re: [isabelle] (structure) and \<index>
- Next by Date: Re: [isabelle] instantiation order for a record
- Previous by Thread: [isabelle] instantiation order for a record
- Next by Thread: Re: [isabelle] instantiation order for a record
- Cl-isabelle-users October 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list