Email Gateway (Aug 19 2022 at 12:16): Email Gateway (Aug 19 2022 at 12:16):From: Sven Schneider <Sven.Schneider@TU-Berlin.DE>
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
==============================
Email Gateway (Aug 19 2022 at 12:16):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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:
The types are generalised to TESTRECORD_ext with the extension type parameter 'b being
of sort ord
The comparison is extended point-wise to the extension of the record (more D1 <= more D2)
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
Email Gateway (Aug 19 2022 at 12:16):From: Sven Schneider <Sven.Schneider@TU-Berlin.DE>
Dear Andreas,
thank you very much.
With your help I could solve my actual problem/.
/Best regards,
Sven
Last updated: Apr 25 2024 at 12:23 UTC