[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.