Email Gateway (Aug 18 2022 at 20:22): Email Gateway (Aug 18 2022 at 20:22):From: René Thiemann <rene.thiemann@uibk.ac.at>
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é
Email Gateway (Aug 18 2022 at 20:22):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
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
Email Gateway (Aug 18 2022 at 20:22):From: René Thiemann <rene.thiemann@uibk.ac.at>
Dear Andreas,
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.
thanks, this was the expected answer, which tells me that I have to do some work.
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:
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.
Exactly, for my presented (short) proof, it is easy to do it within the proof. In the general setting, I'll have to think about how to solve this problem.
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:
Thanks for the pointers. I'll have a look into it whether these techniques can be utilized to solve my problem.
Cheers,
René
Last updated: Apr 23 2024 at 12:29 UTC