Re: [isabelle] instantiation order for a record



Dear Sven,

When you define the parameters of a type class in an instantiation, you must make sure that type inference infers exactly the expected type for the constant to be defined. If the type is not right, Isabelle does not recognize this as the definition of the parameter. In your example with record, you instantiate the type class for TESTRECORD_ext.
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.

Therefore, you have to generalise your definition of lesseqTESTRECORD and lessTESTRECORD to the raw type ('a, 'b) TESTRECORD_ext of the extensible record. In fact, if you just delete the type annotation for your definition of these two constants, the definitions will work, but you will not be able to show the order class axioms, because your comparison functions ignore any possible extensions of the record and therefore antisymmetry does not hold.

Instead, the comparison operations should work for any extension of the record. The following should work. There are three differences:

1. The types are generalised to TESTRECORD_ext with the extension type parameter 'b being of sort ord

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

3. The instantiation requires the sort order for the extension type parameter, as you will otherwise not be able to complete the proof.


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"

definition lessTESTRECORD :: "('a, 'b :: ord) TESTRECORD_ext \<Rightarrow> ('a, 'b) TESTRECORD_ext
\<Rightarrow> bool" where
  "lessTESTRECORD D1 D2 \<equiv> lesseqTESTRECORD D1 D2 \<and> D1\<noteq>D2"

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


There is just one remaining problem: In Isabelle2013, the unit type is not an instance of order, and neither in the coming release (but probably in Isabelle2014). So, you have to provide an instantiation for unit yourself. You can import, e.g., the theory from the Archive of Formal Proofs at
  http://afp.sourceforge.net/browser_info/devel/AFP/Containers/Unit_Instantiations.html


One further remark: It is generally better to avoid intermediate constants like lesseqTESTRECORD and instead to define the order operation directly inside the instantiation context, unless you have particular reasons.

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





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