Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Problem with unfolding definitions while insta...

Email Gateway (Aug 19 2022 at 14:40):

From: Nils Jähnig <nils.jaehnig@tu-berlin.de>
Dear Isabelle Users,

I am trying to instantiate a class, and can not see how to unfold the
predefined fixed definitions.
My question is: how do I figure out the right rules or definition names?

I'll use two example to explain:

Example 1

theory fun_ccpo
imports Complete_Partial_Order
begin

instantiation "fun" :: (type, ccpo) ccpo
begin
instance
apply(intro_classes)
(* First subgoal:

1. ⋀A x. chain op ≤ A ⟹ x ∈ A ⟹ x ≤ ⨆A
   *)
   (* I found those two definition and can unfold them*)
   apply(unfold chain_def)[]
   apply(unfold le_fun_def)[]
   (* but I am not able to find the right Sup definition
   neither do I know how to overwrite the Sup definition *)
   thm Sup_fun_def
   (* Those don't work *)
   apply(unfold Sup_fun_def)
   apply(simp add: Sup_fun_def)
   sorry

end
end

Example 2, uses HOLCF

theory fun_pcpo
imports Fun_Cpo
begin

datatype nat_bot = N nat | Bot

instantiation nat_bot :: pcpo
begin
definition "below_nat_bot a b == a=b ∨ a=Bot"
instance
apply(default)
apply(unfold below_nat_bot_def, simp)[]
apply(unfold below_nat_bot_def, auto)[]
apply(unfold below_nat_bot_def, auto)[]
(* First Subgoal

1. ⋀S. chain S ⟹ ∃x. range S <<| x
   *)
   (* How do i unfold chain, range and <<| *)
   thm chain_def
   thm is_lub_def
   sorry

end
end

Thanks for any help
Nils

Email Gateway (Aug 19 2022 at 14:40):

From: David Cock <davec@cse.unsw.edu.au>
Nils,
Your problem in the first instance is that Sup_fun is only defined
where the result type is a complete lattice. Try:

declare [[show_sorts = true]]
thm Sup_fun_def

Sup_fun_def won't unfold, as you're assuming that the result type is in
class ccpo, not complete_lattice. This is a bit of a nuisance, as the
definition of Sup_fun only really needs the result type to be in class Sup.

Dave

Email Gateway (Aug 19 2022 at 14:40):

From: Tobias Nipkow <nipkow@in.tum.de>
On 06/06/2014 11:15, Nils Jähnig wrote:

Hello Dave,

thanks for the information! I was suspecting this, but was not sure.

Is there any way to re-define Sup_fun for ccpos?
When there is no definition at all, I am asked to give a definition (e.g.
when I instantiate Sup with nat). I would like to override definitions in
the same way.

This is not possible. As Dave pointed out, the problem goes away if in Main the
instantiation of "fun" on class complete_lattice is done in stages, where in a
first step one merely instantiates Sup and Inf.

@ Florian: any objections to that?

And is it just me not understanding the type classes or overloading, or is
it really strange that definitions of one type class use definitions of
another (stronger!) type class?

What do you mean?

I would also be grateful for explanations why it doesn't work, or why I am
trying in a wrong direction.

As Dave said, it is not your fault, the setup in Main is not fine-grained
enough. You can modify Complete_Lattice as follows to make it work, but your
theories will no longer work with the distribution: replace the block

instantiation "fun" :: (type, complete_lattice) complete_lattice
...
end

by the following:

instantiation "fun" :: (type, Inf) Inf
begin

definition
"\<Sqinter>A = (\<lambda>x. \<Sqinter>f\<in>A. f x)"

lemma Inf_apply [simp, code]:
"(\<Sqinter>A) x = (\<Sqinter>f\<in>A. f x)"
by (simp add: Inf_fun_def)

instance ..

end

instantiation "fun" :: (type, Sup) Sup
begin

definition
"\<Squnion>A = (\<lambda>x. \<Squnion>f\<in>A. f x)"

lemma Sup_apply [simp, code]:
"(\<Squnion>A) x = (\<Squnion>f\<in>A. f x)"
by (simp add: Sup_fun_def)

instance ..

end

instantiation "fun" :: (type, complete_lattice) complete_lattice
begin

instance proof
qed (auto simp add: le_fun_def intro: INF_lower INF_greatest SUP_upper SUP_least)

end

Tobias

PS Do not import individual theories that are part of Main (like
Complete_Partial_Order), start from Main instead. Otherwise you get some
fragment of Main with unpredictable behaviour.

Thanks in advance
Nils

2014-06-06 0:10 GMT+02:00 David Cock <davec@cse.unsw.edu.au>:

Nils,
Your problem in the first instance is that Sup_fun is only defined where
the result type is a complete lattice. Try:

declare [[show_sorts = true]]
thm Sup_fun_def

Sup_fun_def won't unfold, as you're assuming that the result type is in
class ccpo, not complete_lattice. This is a bit of a nuisance, as the
definition of Sup_fun only really needs the result type to be in class Sup.

Dave

On 05/06/14 00:40, Nils Jähnig wrote:

Dear Isabelle Users,

I am trying to instantiate a class, and can not see how to unfold the
predefined fixed definitions.
My question is: how do I figure out the right rules or definition names?

I'll use two example to explain:

---

-

---

Example 1

theory fun_ccpo
imports Complete_Partial_Order
begin

instantiation "fun" :: (type, ccpo) ccpo
begin
instance
apply(intro_classes)
(* First subgoal:
1. ⋀A x. chain op ≤ A ⟹ x ∈ A ⟹ x ≤ ⨆A
*)
(* I found those two definition and can unfold them*)
apply(unfold chain_def)[]
apply(unfold le_fun_def)[]
(* but I am not able to find the right Sup definition
neither do I know how to overwrite the Sup definition *)
thm Sup_fun_def
(* Those don't work *)
apply(unfold Sup_fun_def)
apply(simp add: Sup_fun_def)
sorry

end
end

---

-

---

Example 2, uses HOLCF

theory fun_pcpo
imports Fun_Cpo
begin

datatype nat_bot = N nat | Bot

instantiation nat_bot :: pcpo
begin
definition "below_nat_bot a b == a=b ∨ a=Bot"
instance
apply(default)
apply(unfold below_nat_bot_def, simp)[]
apply(unfold below_nat_bot_def, auto)[]
apply(unfold below_nat_bot_def, auto)[]
(* First Subgoal
1. ⋀S. chain S ⟹ ∃x. range S <<| x
*)
(* How do i unfold chain, range and <<| *)
thm chain_def
thm is_lub_def
sorry

end
end

---

-

---

Thanks for any help
Nils

Email Gateway (Aug 19 2022 at 14:41):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
No. This would finally conclude the »syntactification« of Sup and Inf
initiated by Larry (AFAIR).

Florian
signature.asc

Email Gateway (Aug 19 2022 at 14:41):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Nils,

I'm not sure if I am thinking to object oriented.

without following you in detail, your use of the phrase »object
oriented« suggests that you see a relationship between classes as
inlanguages like Java and Isabelle's type classes. But there is, well,
none.

If you want to approach Isabelle's type classes from a programming
language perspective, Haskell's type classes are their nearest cousins.
There is also a tutorial on type classes coming with the Isabelle
distribution which gives some examples.

Hope this helps,
Florian
signature.asc

Email Gateway (Aug 19 2022 at 14:41):

From: Tobias Nipkow <nipkow@in.tum.de>
On 06/06/2014 15:17, Nils Jähnig wrote:

Hello Tobias,

thank you for your answer.

And is it just me not understanding the type classes or overloading, or
is
it really strange that definitions of one type class use definitions of
another (stronger!) type class?

What do you mean?

I expected the following behavior:
"fun"::(type, ccpo) does not care about definitions for "fun"::(type,
lattice) [1]. Different type, different definitions.

In order to have most general types, the set of all instantiations must satisfy
certain constraints.

Tobias

If the type "inherits" from another type (i.e. is a supertype, as ccpo is
to order and sup), then it is wanted to "inherit" defintions [2].
I'm not sure if I am thinking to object oriented.

I thought locals introduce some sort of namespace, which could be used to
differentiate between different Sup definitions for different types.

I would also be grateful for explanations why it doesn't work, or why I
am
trying in a wrong direction.

As Dave said, it is not your fault, the setup in Main is not fine-grained
enough. You can modify Complete_Lattice as follows to make it work, but
your
theories will no longer work with the distribution: replace the block [...]

Thank you for the tip, but I don't want to modify the distribution
theories. I was hoping more for something lika a "redefine" command inside
of a type instantiation.
Just out of curiosity, is there a place where I could vote for a change of
Complete_lattices.thy? And would it be a complete waste of time to do so?

PS Do not import individual theories that are part of Main (like
Complete_Partial_Order), start from Main instead. Otherwise you get some
fragment of Main with unpredictable behaviour.

I was hoping to not load Complete_lattices and its definitions this way,
and thereby be prompted to define Sup_fun by myself.

Nils

[1]:

attempting to
instantiation "fun" :: (type, ccpo) sup
begin

threw the error
Conflict of type arities:
fun :: (type, ccpo) sup and
fun :: (type, lattice) sup

[2]:
I solved my other problem, how to access the definition for chain while
instantiating pcpo, by instantiating cpo first, where the defintion was
available.
My (unmet) expectation was that either I am prompted to define, or it is
defined (and the definition accessible).

Email Gateway (Aug 19 2022 at 14:41):

From: Tobias Nipkow <nipkow@in.tum.de>
It is in now. This means that with the next release one can use Inf and Sup on
functions without forcing things to be complete lattices.

Tobias

Last updated: Nov 21 2024 at 12:39 UTC