Email Gateway (Aug 19 2022 at 10:59): Email Gateway (Aug 19 2022 at 10:59):From: Makarius <makarius@sketis.net>
This also belongs to isabelle-users.
It does not make any sense to post questions both to isabelle-users and
isabelle-dev at the same time -- it just causes confusion.
Makarius
---------- Forwarded message ----------
Date: Wed, 22 May 2013 13:50:45 +0200
From: Manuel Eberl <eberlm@in.tum.de>
To: isabelle-dev@mailbroy.informatik.tu-muenchen.de
Subject: Re: [isabelle-dev] Partial functions
Hallo,
partial function in Isabelle are usually modelled as 'a ⇀ 'b, which is
an abbreviation for 'a ⇒ 'b option. There is syntax such as "[1 ↦ 2, 3 ↦
4]", meaning, basically, "λx. if x = 1 then Some 2 else if x = 3 then
Some 4 else None". There is also update syntax for such function, such
as "f(1 ↦ 3)", meaning "λx. if x = 1 then 3 else f x".
You could therefore write something like
definition f :: "nat ⇀ nat" where "f = [1 ↦ 4, 2 ↦ 4, 3 ↦ 5]"
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}.
If you want to apply such a function, you can either do "case f x of
None ⇒ … | Some y ⇒ …", or you can simply write "the (f x)". "the" takes
an option value and extracts the "y" out of a "Some y" or returns
"undefined" if the option value is "None".
I hope that answers your question.
Cheers,
Manuel
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-->5or 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:
Everytime i want declare a new function, i have to declare by
"typedef" the nat subsets i want as domain and rangedefinition 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
isabelle-dev@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Email Gateway (Aug 19 2022 at 11:10):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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.
Email Gateway (Aug 19 2022 at 12:13):From: Gottfried Barrow <gottfried.barrow@gmx.com>
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
Email Gateway (Aug 19 2022 at 12:13):From: Christian Sternagel <c.sternagel@gmail.com>
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
Email Gateway (Aug 19 2022 at 12:13):From: Gottfried Barrow <gottfried.barrow@gmx.com>
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:
Regards,
GB
Last updated: Apr 23 2024 at 12:29 UTC