*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Problem with unfolding definitions while instantiating class*From*: David Cock <davec at cse.unsw.edu.au>*Date*: Fri, 06 Jun 2014 08:10:25 +1000*In-reply-to*: <CA+fzNkKLf8K2pxj2U=Rr=-s=4RRBY8c4uMNXoeB1KRYWonY2KA@mail.gmail.com>*References*: <CA+fzNkKLf8K2pxj2U=Rr=-s=4RRBY8c4uMNXoeB1KRYWonY2KA@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Icedove/24.5.0

Nils,

declare [[show_sorts = true]] thm Sup_fun_def

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

**Follow-Ups**:

**References**:**[isabelle] Problem with unfolding definitions while instantiating class***From:*Nils Jähnig

- Previous by Date: [isabelle] Fw: [Coq-Club] A new OpenSSL bug was found, thanks to Coq
- Next by Date: Re: [isabelle] Problem with unfolding definitions while instantiating class
- Previous by Thread: [isabelle] Problem with unfolding definitions while instantiating class
- Next by Thread: Re: [isabelle] Problem with unfolding definitions while instantiating class
- Cl-isabelle-users June 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list