On Mon, 11 Mar 2013, Lars Noschinski wrote:
Indeed and I'm in happy situation that I'm able to share my sources.
Unfortunately, due to necessary background theory, this example is quite
large and depends on autocorres[1] and hence Isabelle 2012.
[1]
There is not yet a version of the C parser for Isabelle 2013, but there will be
soon.
Michael
On 26/03/2013, at 4:01, Lars Noschinski nosch...@in.tum.de wrote:
On 25.03.2013 17:21, Makarius wrote:
On Mon, 11 Mar 2013, Lars Noschinski wrote:
Indeed and I'm in happy situation that I'm able
On 08/03/13 23:46, Joachim Breitner wrote:
Sometimes, when I’m writing apply-script style proofs, I have wanted
a way to modify a proof method foo to “Try foo on the first goal. If
it solves the goal, good, if it does not solve it, fail”.
[...]
I wanted to see if I could implement such a
I agree with you, and it seems a mistake to expect jEdit to do all kinds of
things that could very easily be done otherwise.
Larry
On 14 Mar 2013, at 07:57, David Greenaway david.greena...@nicta.com.au wrote:
On 08/03/13 23:46, Joachim Breitner wrote:
Sometimes, when I’m writing
On Thu, 14 Mar 2013, David Greenaway wrote:
On 08/03/13 23:46, Joachim Breitner wrote:
Sometimes, when I’m writing apply-script style proofs, I have wanted
a way to modify a proof method foo to “Try foo on the first goal. If
it solves the goal, good, if it does not solve it, fail”.
[...]
I
On Thu, 14 Mar 2013, Lawrence Paulson wrote:
I agree with you, and it seems a mistake to expect jEdit to do all kinds
of things that could very easily be done otherwise.
The easily here is ex falso quodlibet consequitur. The system is
definitely easy to break by adhoc patching ...
Before
On Mon, 11 Mar 2013, David Greenaway wrote:
As a data point, inside the seL4 proof, a largish application of
Isabelle, such a solve-or-fail mechanism would have been very helpful.
So can you show the sources for that, to give an idea what is done there?
Makarius
On Sun, 10 Mar 2013, Lars Noschinski wrote:
There is definitely an use case for such an operation. When doing
program verification, I often have long sequences of apply commands.
These are either applications of the VCG or (mostly) oneliners to solve
the verification conditions.
Can you
On 11/03/2013, at 11:42 AM, Makarius makar...@sketis.net wrote:
On Mon, 11 Mar 2013, David Greenaway wrote:
As a data point, inside the seL4 proof, a largish application of Isabelle,
such a solve-or-fail mechanism would have been very helpful.
So can you show the sources for that, to give
On Mon, 11 Mar 2013, Gerwin Klein wrote:
A very typical situation in those proofs are scripts that look like
this:
lemma some statement
apply wp
apply simp
apply fastforce
apply (auto simp: some_rule intro!: other_rule)[1]
apply clarsimp
apply (simp add: other_things)
apply
I can also imagine a use for this sort of thing. I use structured proofs when I
can, but in some situations it really isn't possible.
Larry
On 11 Mar 2013, at 16:51, Makarius makar...@sketis.net wrote:
This looks just like making the meaning of indentation a bit more formal.
Lets say as a
On 11.03.2013 17:51, Makarius wrote:
This looks just like making the meaning of indentation a bit more
formal. Lets say as a mode of checking in the Prover IDE: fail if
something is wrong in that respect, or paint things in funny colors.
We shortly thought about this earlier and it has the
Hi,
Am Montag, den 11.03.2013, 18:11 +0100 schrieb Lars Noschinski:
On 11.03.2013 17:51, Makarius wrote:
This looks just like making the meaning of indentation a bit more
formal. Lets say as a mode of checking in the Prover IDE: fail if
something is wrong in that respect, or paint things
On Mon, 11 Mar 2013, Lars Noschinski wrote:
Markup.proof_state is there for a long time already, to turn it into
some use.
Does this mean this could be implemented exclusively on the jEdit side,
without touching the prover?
It depends what this actually shall mean here. There is always
On Mon, 11 Mar 2013, Joachim Breitner wrote:
This lets you say assert_goals 5 in your apply scripts where you think
there should be 5 goals.
Of course there is always a possibility to devise new commands. Critical
review will only start when such things show up in publicly accessible
On 10/03/13 07:03, Makarius wrote:
On Fri, 8 Mar 2013, Joachim Breitner wrote:
Sometimes, when I’m writing apply-script style proofs, I have wanted
a way to modify a proof method foo to “Try foo on the first goal. If
it solves the goal, good, if it does not solve it, fail”.
The Isar proof
On Fri, 8 Mar 2013, Joachim Breitner wrote:
Sometimes, when I’m writing apply-script style proofs, I have wanted a
way to modify a proof method foo to “Try foo on the first goal. If it
solves the goal, good, if it does not solve it, fail”.
Such non-trivial control structures are usually done
There is definitely an use case for such an operation. When doing program
verification, I often have long sequences of apply commands. These are either
applications of the VCG or (mostly) oneliners to solve the verification
conditions. To keep the proof as robust as possible, I use the
Dear Isabelle developers,
I’d like to suggest a feature, and submit a patch:
Sometimes, when I’m writing apply-script style proofs, I have wanted a
way to modify a proof method foo to “Try foo on the first goal. If it
solves the goal, good, if it does not solve it, fail”.
This came up in the
19 matches
Mail list logo
