[isabelle] strange behaviour with type instantiation

[Burkhart Wolff]

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

[Florian Haftmann]

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

[Florian Haftmann]

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::'\<alpha> list) < t

> \<longleftrightarrow> s \<le> t \<and> s \<noteq> t"

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

[Burkhart Wolff]

Hi Florian,

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

> ...
>

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