*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] [isabelle-dev] Partial functions*From*: Gottfried Barrow <gottfried.barrow at gmx.com>*Date*: Fri, 25 Oct 2013 10:45:38 -0500*In-reply-to*: <526A1754.3020909@gmail.com>*References*: <DUB124-W34753CEAC4B5C9BEBFCF9B8FA90@phx.gbl> <DUB124-W45D4B252949F10C4E01E678FA90@phx.gbl> <519CAFA1.8040804@inf.ethz.ch> <526A10E9.50301@gmx.com> <526A1754.3020909@gmail.com>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

Christian,

People should try it out.

runInSystemShell(view,"scala %f"); runInSystemShell(view,"scala %p\\..\\work\\src\\i2t_pdoc.scala %p");

http://scala-ide.org/ Regards, GB On 10/25/2013 2:01 AM, Christian Sternagel wrote:

How about unfolding the definition of "f"? Then it should work, e.g., as follows definition f :: "nat ⇒ nat option" where "f x = (if x ∈ {1, 2, 3} then Some 0 else None)" lemma "dom f = {1, 2, 3}" by (force simp: f_def dom_def) cheers chris On 10/25/2013 03:34 PM, Gottfried Barrow wrote:On 5/22/2013 6:44 AM, Andreas Lochbihler wrote:For example, definition f :: "nat => nat option" where "f x = (if x : {1,2,3} then Some .... else None)" Then, "dom f" returns the domain of f as {1,2,3} and "ran f" the range of f. There are a few more operations defined in theory Map, in particular map_of. Option.bind in theory Option is used for function composition.On 5/22/2013 6:50 AM, Manuel Eberl wrote:You can find out the domain/range of such a partial function using dom and ran. For instance, "dom f" is defined as {a. f a ≠ None}.I was looking at how to do a partial function with option, so I was looking at this old email thread. The two statements above make it sound like it should be easy to get "dom f = {1,2,3}". I do this: theorem "(dom f) = {1,2,3}" apply(unfold dom_def) And I get a goal: "{a. f a ≠ None} = {1, 2, 3}", with no easy automatic proof. Is there something simple I'm supposed to do get "(dom f) = {1,2,3}"? Thanks, GB

**References**:**Re: [isabelle] [isabelle-dev] Partial functions***From:*Gottfried Barrow

**Re: [isabelle] [isabelle-dev] Partial functions***From:*Christian Sternagel

- Previous by Date: Re: [isabelle] 2013-1-RC1: how to put generated Scala into a package without using code_include?
- Next by Date: Re: [isabelle] efficient code for ('a, 'b) map (as opposed to ('a, 'b) mapping
- Previous by Thread: Re: [isabelle] [isabelle-dev] Partial functions
- Next by Thread: [isabelle] [Isabelle2013-1 RC] Scalability problem with re-entrant build of the whole distribution
- Cl-isabelle-users October 2013 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