[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.