# Re: [isabelle] Problem with unfolding definitions while instantiating class

```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)
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

```
```

```

• Follow-Ups:

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