Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] strange behaviour with type instantiation

Email Gateway (Aug 18 2022 at 13:31):

From: Burkhart Wolff <Burkhart.Wolff@lri.fr>
Dear all,

I'd like to do the following standard type instantiation:

>

instantiation list :: (type) ord
begin

definition le_list_def : "s \<le> t \<longleftrightarrow> (\<exists>
r. s @ r = t)"
definition less_list_def: "s < t \<longleftrightarrow> s \<le> t
\<and> s \<noteq> t"

(*
definition less_list_def : "less \<equiv> \<lambda> x y. (x \<le> y
\<and> x \<noteq> y)"
*)
instance ..

end

<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<
However, I got the following respionse (under Isabelle 2008):

*** Bad head of lhs: existing constant "op <"
*** The error(s) above occurred in definition: "s < t s ~ t ~ s ~ t"
*** At command "definition".

Exchanging the offending s < t by the core notation (see comments)
no avail.

Can anyone help me out ?

Best regards,

bu

Email Gateway (Aug 18 2022 at 13:31):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Burkhart,

instantiation list :: (type) ord
begin

definition le_list_def : "s \<le> t \<longleftrightarrow> (\<exists>
r. s @ r = t)"
definition less_list_def: "s < t \<longleftrightarrow> s \<le> t \<and>
s \<noteq> t"

(*
definition less_list_def : "less \<equiv> \<lambda> x y. (x \<le> y
\<and> x \<noteq> y)"
*)
instance ..

end

The problem is that the inferred type for less_list is too general.
Type annotations help:

instantiation list :: (type) ord
begin

instantiation list :: (type) ord
begin

definition le_list_def : "s \<le> t \<longleftrightarrow> (\<exists> r. s @ r = t)"
definition less_list_def: "(s :: 'a list) < t \<longleftrightarrow> s \<le> t \<and> s \<noteq> t"

...

AFAIK there are some theories in HOL/Library which define different
orders on lists (Prefix_ord.thy, ...). Perhaps these are helpful also.

Hope this helps
Florian
signature.asc

Email Gateway (Aug 18 2022 at 13:31):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Burkhart,
This is a misunderstanding how type variables work wrt. instantiation:
type variables for instance specifications are locally fixes during the
whole instantiation block. Thus you have to write "'a" instead of
"'\<alpha>".

Hope this helps,

Florian
signature.asc

Email Gateway (Aug 18 2022 at 13:32):

From: Burkhart Wolff <Burkhart.Wolff@lri.fr>
Hi Florian,

did you actually try this ?

I did of course, among other variants, and I still get:

instantiation list :: (type) ord
begin

definition le_list_def : "s \<le> t \<longleftrightarrow> (\<exists>
r. s @ r = t)"

definition less_list_def: "(s::'\<alpha> list) < t
\<longleftrightarrow> s \<le> t \<and> s \<noteq> t"
(*
definition less_list_def : "less \<equiv> \<lambda> x y. (x \<le> y
\<and> x \<noteq> y)"
*)
instance ..

end

and still get the same error message:

*** Bad head of lhs: existing constant "op <"
*** The error(s) above occurred in definition: "s < t == s <= t & s ~=
t"
*** At command "definition".

Best,

bu

Last updated: May 03 2024 at 04:19 UTC