Email Gateway (Aug 22 2022 at 13:19): Email Gateway (Aug 22 2022 at 13:19):From: Colin Rowat <c.rowat@espero.org.uk>
The code below seeks to establish that any real triple (a,b,c) satisfying a
\<ge> b \<ge> c \<ge> 0 also satisfies at least one of the 10 conditions
below (expressions 6, 7/8, 9, 10, 11, 12, 13, 14, 15 or 16). I am running
it in Isabelle2016 under 64-bit Windows 7.
It seems to work, but with an ugly correction for an unexpected type
conversion: if expression 9 does not re-declare 'a' as a real (already
declared as such in expression 6), then 'a', 'b' and 'c' from that term are
cast to int, and the whole term cast back to real_of_int.
Can anyone tell me why this happens, and whether there's a cleaner solution
than to re-declare 'a' as real?
Thank you,
Colin Rowat
University of Birmingham
theory "160429-cores-partition"
imports Real
begin
lemma Coro1: " (* expression 6*)
((real a) < (real b) + (real c) -1.0
| (* expression 7 & 8 *)
(a - b - c \<ge> -1.0) \<and> (-(real a) + b - c) < -1.0
| (* expression 9 *)
(-(real a) + b - c \<ge> -1.0) \<and> (0.0 < c) \<and> (c < a
+b -1.0)
| (* expression 10 *)
(c = 0.0) \<and> (b > 0.0) \<and> (b = a -1.0)
| (* expression 11 *)
(c = 0.0) \<and> (b > abs(1.0 - a))
| (* expression 12 *)
(c \<ge> a + b - 1.0) \<and> (c > 0.0)
| (* expression 13 *)
(a = 1.0) \<and> (b = 0.0) \<and> (c = 0.0)
| (* expression 14 *)
(c = 0.0) \<and> (b > 0.0) \<and> (b \<le> 1.0 -a)
| (* expression 15 *)
(c = 0.0) \<and> (b = 0.0) \<and> (a > b) \<and> (a \<le> 1.0)
| (* expression 16 *)
(c = 0.0) \<and> (b = 0.0) \<and> (a = 0.0)
)
\<and> (a \<ge> b) \<and> (b \<ge> c) \<and> (c \<ge> 0)
" by arith
end
Email Gateway (Aug 22 2022 at 13:19):From: Lars Hupel <hupel@in.tum.de>
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
Email Gateway (Aug 22 2022 at 13:20):From: Colin Rowat <c.rowat@espero.org.uk>
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@in.tum.de>
Subject: Re: [isabelle] unexpected conversion from real to int
To: cl-isabelle-users@lists.cam.ac.uk
Message-ID: <e58297a5-24fe-d435-98d3-cba44a1f6629@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@in.tum.de>
Subject: [isabelle] ISABELLE WORKSHOP 2016: Call for Papers
To: Isabelle Users <isabelle-users@cl.cam.ac.uk>
Message-ID: <a370eeea-f227-d5d8-9cd6-73159ac05cb0@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@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@cl.cam.ac.uk>
Message-ID: <49F3C05F-F386-438F-8BDD-BDADB503365C@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@chalmers.se>
Subject: [isabelle] Isabelle's environment and external executables
To: "isabelle-users@cl.cam.ac.uk" <isabelle-users@cl.cam.ac.uk>
Message-ID: <C4A95081-44F2-43EE-BBBD-BAB5479CB95F@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@in.tum.de>
Subject: Re: [isabelle] Isabelle's environment and external
executables
To: Moa Johansson <moa.johansson@chalmers.se>,
"isabelle-users@cl.cam.ac.uk" <isabelle-users@cl.cam.ac.uk>
Message-ID: <eb56f77a-bedc-c953-b016-6dc392237078@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
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
Last updated: Apr 25 2024 at 04:18 UTC