# [isabelle] Problem with sort constraints

Dear all,
I'm currently having a question concerning class-constraints:
In a locale where I just fix some constants without assuming anything about them, it
is always possible to get rid of the "locale-constraint".
So my question is, whether this is also possible for class-constraints? I.e., if I just
fix some function (emb in the example below) without making any assumptions about it,
can one get rid of the sort constraint (i.e., replace the "('a :: embed)list by ('a list)").
In the proof below, I just require the exakt definition of emb for lists, but it does not matter how emb
is defined on type 'a for the elements of the list.
In principle, I have shown "!! xs :: ('a :: embed) list. len_dom xs", and I would like to derive
"!! xs :: 'a list. len_dom xs" without the embed sort-constraint.
class embed =
fixes emb :: "'a ⇒ nat"
instantiation list :: (embed) embed
begin
fun emb_list where
"emb_list [] = 0"
| "emb_list (x # xs) = emb x + 2 * emb xs + 1"
instance ..
end
function len :: "('a :: embed) list => nat"
where "len [] = 0"
| "len (x # xs) = Suc (len xs)"
by pat_completeness auto
termination len (* goal: All len_dom *)
proof
let ?r = "inv_image ({(x,y). x < y}) (emb :: 'a list => nat)"
show "wf ?r"
by (rule wf_inv_image[OF wf_less])
fix x xs
show "(xs, x # xs) ∈ ?r" by simp
qed
Best regards,
René

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