Re: [isabelle] unexpected conversion from real to int



Thank you Lars: that's solved it.

(I knew that, at some point, I'd need to learn how to write a two line
proof.)

Best,

Colin

----------------------------------------------------------------------

Message: 1
Date: Fri, 6 May 2016 16:50:15 +0200
From: Lars Hupel <hupel at in.tum.de>
Subject: Re: [isabelle] unexpected conversion from real to int
To: cl-isabelle-users at lists.cam.ac.uk
Message-ID: <e58297a5-24fe-d435-98d3-cba44a1f6629 at in.tum.de>
Content-Type: text/plain; charset=windows-1252

Dear Colin,

> Can anyone tell me why this happens, and whether there's a cleaner 
> solution than to re-declare 'a' as real?

if you Ctrl-hover over your variables, you'll find that they are all natural
numbers. Applying the 'real' function to your variables does not declare
them as 'real'. Instead, try this:

lemma
  fixes a b c :: real
  shows "..."

Cheers
Lars



------------------------------

Message: 2
Date: Fri, 6 May 2016 16:59:02 +0200
From: Tobias Nipkow <nipkow at in.tum.de>
Subject: [isabelle] ISABELLE WORKSHOP 2016: Call for Papers
To: Isabelle Users <isabelle-users at cl.cam.ac.uk>
Message-ID: <a370eeea-f227-d5d8-9cd6-73159ac05cb0 at in.tum.de>
Content-Type: text/plain; charset="windows-1252"

			       Call for Papers

			   ISABELLE WORKSHOP 2016
                  http://www.in.tum.de/~nipkow/Isabelle2016/
		          August 25-26, 2016, Nancy

			       Associated with
	Interactive Theorem Proving (ITP 2016) http://itp2016.inria.fr


This informal workshop will again bring together Isabelle users and
developers. Participants are invited to present their research and projects,
including applications of Isabelle, internal developments, add-on tools, and
reports on work in progress. If you have missed the ITP deadline, this is an
excellent oppotunity to announce to the world your proof of the XYZ Theorem
or present some nifty new proof procedure!

The worshop will include demonstrations of recent Isabelle devlopments.
There will also be opportunities to discuss issues of interest to the
Isabelle community.

Please submit a paper (or extended abstract) of up to 20 pages. It will be
reviewed informally and accepted papers will be made available on the
workshop home page. There are no formal proceedings.

Submission site: http://www.easychair.org/conferences/?conf=isabelle2016

Important Dates:

     * Submission deadline:        June 19
     * Notification of acceptance: July 1
     * Workshop:                   August 25 (afternoon) and 26 (morning)

Organisers: Tobias Nipkow, Larry Paulson and Makarius Wenzel

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5135 bytes
Desc: S/MIME Cryptographic Signature
Url :
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/attachments/20160506/4e1
47db0/attachment.p7s 

------------------------------

Message: 3
Date: Mon, 9 May 2016 00:52:09 +0000
From: Gerwin Klein <Gerwin.Klein at nicta.com.au>
Subject: [isabelle] new in the AFP: A formal proof of the max-flow
	min-cut theorem for countable networks
To: isabelle-users <isabelle-users at cl.cam.ac.uk>
Message-ID: <49F3C05F-F386-438F-8BDD-BDADB503365C at nicta.com.au>
Content-Type: text/plain; charset="us-ascii"

Another new entry in the Archive, keep them coming!


A formal proof of the max-flow min-cut theorem for countable networks by
Andreas Lochbihler

This article formalises a proof of the maximum-flow minimal-cut theorem for
networks with countably many edges. A network is a directed graph with
non-negative real-valued edge labels and two dedicated vertices, the source
and the sink. A flow in a network assigns non-negative real numbers to the
edges such that for all vertices except for the source and the sink, the sum
of values on incoming edges equals the sum of values on outgoing edges. A
cut is a subset of the vertices which contains the source, but not the sink.
Our theorem states that in every network, there is a flow and a cut such
that the flow saturates all the edges going out of the cut and is zero on
all the incoming edges. The proof is based on the paper The Max-Flow Min-Cut
theorem for countable networksby Aharoni et al. As an application, we derive
a characterisation of the lifting operation for relations on discrete
probability distributions, which leads to a concise proof of its
distributivity over relation composition.

http://www.isa-afp.org/entries/MFMC_Countable.shtml


Enjoy!
Gerwin


________________________________

The information in this e-mail may be confidential and subject to legal
professional privilege and/or copyright. National ICT Australia Limited
accepts no liability for any damage caused by this email or its attachments.



------------------------------

Message: 4
Date: Mon, 9 May 2016 11:48:25 +0000
From: Moa Johansson <moa.johansson at chalmers.se>
Subject: [isabelle] Isabelle's environment and external executables
To: "isabelle-users at cl.cam.ac.uk" <isabelle-users at cl.cam.ac.uk>
Message-ID: <C4A95081-44F2-43EE-BBBD-BAB5479CB95F at chalmers.se>
Content-Type: text/plain; charset="utf-8"

Hi all,

I?m calling some external (Haskell) executables from inside Isabelle. If I
start isabelle from the shell (using the command ?isabelle jedit?) it works
fine, and my executables are picked up from my bash environment as they?re
in the PATH. However, if I start Isabelle by double-clicking, the
environment is different, and Isabelle no longer finds what is in my normal
path.

I?ve consulted the Isabelle Systems Manual, and tried to follow the
instructions to add the paths to the ISABELLE_TOOLS environment variable in
my $ISABELLE_HOME_USER/etc/settings, but that does not work. I?ve also tried
adding the path to $ISABELLE_HOME_USER/etc/components but that made no
difference either. 

Obviously doing something silly but wrong, as it should be easy to add
something to Isabelle?s environment.

Here are the gory details, my Isabelle extension is looking for two
executables called ?HipSpecifyer? and ?hipster-hipspec?, but fails to find
them: 

/var/folders/sl/hb1d9hld2tsfgn33xgsxt1lc0000gp/T/isabelle-moajohansson3147/b
ash_script1000488: line 1: HipSpecifyer: command not found
/var/folders/sl/hb1d9hld2tsfgn33xgsxt1lc0000gp/T/isabelle-moajohansson3147/b
ash_script1000491: line 1: hipster-hipspec: command not found

Best,
Moa

------------------------------

Message: 5
Date: Mon, 9 May 2016 14:22:50 +0200
From: Lars Hupel <hupel at in.tum.de>
Subject: Re: [isabelle] Isabelle's environment and external
	executables
To: Moa Johansson <moa.johansson at chalmers.se>,
	"isabelle-users at cl.cam.ac.uk" <isabelle-users at cl.cam.ac.uk>
Message-ID: <eb56f77a-bedc-c953-b016-6dc392237078 at in.tum.de>
Content-Type: text/plain; charset=utf-8

Hi Moa,

> I?m calling some external (Haskell) executables from inside Isabelle. If I
start isabelle from the shell (using the command ?isabelle jedit?) it works
fine, and my executables are picked up from my bash environment as they?re
in the PATH. However, if I start Isabelle by double-clicking, the
environment is different, and Isabelle no longer finds what is in my normal
path.

I would personally avoid calling tools via PATH, because things tend to not
work reliably (as you observed too).

> I?ve consulted the Isabelle Systems Manual, and tried to follow the
instructions to add the paths to the ISABELLE_TOOLS environment variable in
my $ISABELLE_HOME_USER/etc/settings, but that does not work. I?ve also tried
adding the path to $ISABELLE_HOME_USER/etc/components but that made no
difference either. 

An "Isabelle tool" is an executable which can be invoked using the "tool
wrapper", e.g. like this:

  $ isabelle build

Here, "build" is a "tool". You should register executables as tools if they
- require an Isabelle environment to work (e.g. $ISABELLE_HOME) *and*
- are supposed to be run directly by the user.

On the other hand, an "Isabelle component" acts more as an extension for
Isabelle. It looks like this would be the correct approach for your use
case.

However, Isabelle components require a little bit of setup. In essence, a
component is just a path somewhere on your file system which has been added
to "etc/components" (you did that already). Let's say this is
"/path/to/hipspec". Additionally, you need an "etc/settings" file in this
path.

  $ cat /path/to/hipspec/etc/settings
  HIPSPEC_HOME="$COMPONENT"

The special $COMPONENT variable is provided during initialization of the
component. The end result is that $HIPSPEC_HOME will refer to that path in a
stable and reproducible manner.

The very same mechanism is used to provide the $AFP variable from the AFP
repository.

Note that the above approaches are not mutually exclusive. You can also
register more Isabelle tools in the "etc/settings" file. Isabelle tools can
be executed from within Isabelle/ML using "Isabelle_System.isabelle_tool".

Hope that helps,
Lars



End of Cl-isabelle-users Digest, Vol 131, Issue 7
*************************************************





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