*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Problem with unfolding definitions while instantiating class*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Fri, 06 Jun 2014 13:14:46 +0200*In-reply-to*: <CA+fzNk+uQ-92XbTbwwKz2ydYB5NfGHywSDC_G-+U4Uftuadcqg@mail.gmail.com>*References*: <CA+fzNkKLf8K2pxj2U=Rr=-s=4RRBY8c4uMNXoeB1KRYWonY2KA@mail.gmail.com> <5390EAD1.2070908@cse.unsw.edu.au> <CA+fzNk+uQ-92XbTbwwKz2ydYB5NfGHywSDC_G-+U4Uftuadcqg@mail.gmail.com>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.9; rv:24.0) Gecko/20100101 Thunderbird/24.5.0

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 at 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 >>> >>> >> >>

**Follow-Ups**:**Re: [isabelle] Problem with unfolding definitions while instantiating class***From:*Nils Jähnig

**Re: [isabelle] Problem with unfolding definitions while instantiating class***From:*Florian Haftmann

**References**:

- Previous by Date: Re: [isabelle] Problem with unfolding definitions while instantiating class
- Next by Date: Re: [isabelle] Problem with unfolding definitions while instantiating class
- Previous by Thread: Re: [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