Re: [isabelle] Problem with sort constraints



Dear René,

> So my question is, whether this is also possible for class-constraints?
No. Type classes are explicitly made to prevent applications of overloaded constants when it is not clear that there is an instantiation.

> 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.
I do not see why you need a type class in this case at all. You could equally well define emb_list inside the proof itself and not introduce the type constraint at all:

function len :: "'a list => nat"
  where "len [] = 0"
      | "len (x # xs) = Suc (len xs)"
  by pat_completeness auto

termination len (* goal: All len_dom *)
proof
  def emb == "list_rec 0 (%x xs res. undefined + 2 * res + 1) :: 'a list => nat"
  let ?r = "inv_image ({(x,y). x < y}) emb"
  show "wf ?r"
    by (rule wf_inv_image[OF wf_less])
  fix x xs
  show "(xs, x # xs) : ?r" by(simp add: emb_def)
qed

Obviously, definitions inside proofs are not as convenient as top-level definitions. You could also define emb_list only for lists and use that, but possibly, your real use case is more complex and you do want to use the global emb.

If you want to do overloading without sort constraints, there's the overloading command (Isar-Ref manual 5.8) or the old-fashioned consts+defs (overloaded) pattern, without type classes at all. Note, however, that you then will lose the ability to generate code for whatever is to be implemented in terms of emb. To that end, you would have reintroduce the type class for code generation as follows:

(* not tested *)
consts emb :: "'a => nat"
defs (overloaded) emb_list_def:
  "emb = list_rec 0 (%x xs res. emb x + 2 * res + 1)"

class emb_code =
  fixes emb_code :: "'a => nat"
  assumes emb_code: "emb = emb_code"

declare emb_code[code]

instantiation list :: (emb) emb begin
definition "emb_code :: 'a list => nat == emb"
instance by(intro_locales)(simp add: emb_code_def)
end

Hope this helps,
Andreas

--
Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Am Fasanengarten 5, Geb. 50.34, Raum 025
76131 Karlsruhe

Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
http://pp.info.uni-karlsruhe.de
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft





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