*To*: <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] unexpected conversion from real to int*From*: "Colin Rowat" <c.rowat at espero.org.uk>*Date*: Mon, 9 May 2016 20:14:59 +0100*Thread-index*: AdGqIoi6ZcE6n8zESXOfbJVyFq9OvA==

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 *************************************************

- Previous by Date: [isabelle] Localization of code generator (and thus quickcheck)
- Next by Date: [isabelle] primrec or fun
- Previous by Thread: Re: [isabelle] unexpected conversion from real to int
- Next by Thread: [isabelle] ISABELLE WORKSHOP 2016: Call for Papers
- Cl-isabelle-users May 2016 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