Re: [isabelle] strange behaviour with type instantiation



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


Attachment: signature.asc
Description: OpenPGP digital signature



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