# [isabelle] Problem with unfolding definitions while instantiating class

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

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