Re: [isabelle] [isabelle-dev] Partial functions

[Andreas Lochbihler]

Hi Roger,

Isabelle/HOL is a logic of total function, so very function is defined for all values of
the argument type. So, if you declare the type "nat => nat", it is always defined on all
natural numbers. As you have found out yourself, you can create types for subsets of
natural numbers, but you won't get happy with that, because all of your formalisation will
be cluttered with embeddings of one of these types into another.

The standard way to model partiality is the following: Wrap the return type in "option"
and use the value None to denote undefinedness.

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.

Best,
Andreas

PS: This is a standard user's topic, so it belongs to the mailing list isabelle-users, not
isabelle-dev.

On 22/05/13 13:35, Roger H. wrote:
>
> Hallo,
>
>
> i want to create a datatype that allows me to write functions from a nat subset to another
> nat subset.
> for example i wanna be able to write:
>
>
> definition f: {1,2,3} => {4,5}
> 1 -->4, 2-->4, 3-->5
>
>
> or another one:
>
>
> definition g : {6,8} => {2,3,4}
>
>
>
> So the thing i want to somehow parametrize is "which subset of the nat im using each time
> as domain and range" ,
>
>
> I thought about creating a new datatype : 'a nat
> The problem with this is that 'a is instantiated with datatypes, and not sets like {1,2,3}.
>
>
> Following solutions are bad:
>
>
> 1. Everytime i want declare a new function, i have to declare by "typedef" the nat
> subsets i want as domain and range
>
>
>
>
> 2. definition f : "nat => nat" where
> "f x = (if x : {1,2,3} then .... else undefined)
>
>
> This second approach is bad, cause i dont want the domain to be decided as late as the
> second line of the declaration, cause after this i want to be able to program a selector
> "domain f"
> that returns me the domain of f, thats why i want the domain of f to be somehow
> incapsulated (parametrized) in the first line "f: nat =>nat " so that i can use it later.
>
>
>
> What would you do in this situation?
>
>
> Many thanks!
>
>
>
>
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabel...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>

[Roger H.]

[Gottfried Barrow]

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

[Christian Sternagel]

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

[Gottfried Barrow]

Christian,

Thanks. I'll blame the simple oversight on trying to use and learn new
concepts.

I'm also working on trying to learn Scala. I did a lot of work to find
the best scripting language, to finally find out that a powerful
scripting language is already in the Isabelle distribution:
contrib\scala-2.10.3

People should try it out.

Put the Isabelle2013 Java and Scala bin paths in the jEdit Console
options path: contrib\jdk\x86-cygwin\bin and contrib\scala-2.10.3\bin

You can then run jEdit macros like these to run scala scripts in the
console panel:

runInSystemShell(view,"scala %f");

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

The variable %f is the current jEdit buffer file name, and %p is the
folder set by the current project of the Project Viewer plugin.

And there's the Scala IDE download, which is Eclipse completely set up
for Scala:

http://scala-ide.org/

Regards,
GB