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



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

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













This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.