Re: [isabelle-dev] Feature suggestion: apply (meth[1!])
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] http://ssrg.nicta.com.au/projects/TS/autocorres/ Is there a version for Isabelle2013? Note that Isabelle2012 - Isabelle2013 involves unusually few incompatibilities, so the update would spare anybody from struggling with old IsaMakefiles again. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Feature suggestion: apply (meth[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 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] http://ssrg.nicta.com.au/projects/TS/autocorres/ Is there a version for Isabelle2013? Note that Isabelle2012 - Isabelle2013 involves unusually few incompatibilities, so the update would spare anybody from struggling with old IsaMakefiles again. Not that I know of. But maybe David has already ported it? -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Feature suggestion: apply (meth[1!])
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 feature myself and came up with the attached patch – maybe it is already sufficient? Sorry to raise this thread again, but what was the outcome of this patch? Was the general concept of a solve tactical rejected, or just the particular choice of syntax / implementation? (If so, how could it be improved?) Or have the core developers just been busy? (I apologise if so!) I know that the conversion moved on how jEdit might additionally assist users in determining where a proof script became broken, but I didn't come to understand why this simple patch would be mutually exclusive to other more elaborate options. Cheers, David 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. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Feature suggestion: apply (meth[1!])
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 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 feature myself and came up with the attached patch – maybe it is already sufficient? Sorry to raise this thread again, but what was the outcome of this patch? Was the general concept of a solve tactical rejected, or just the particular choice of syntax / implementation? (If so, how could it be improved?) Or have the core developers just been busy? (I apologise if so!) I know that the conversion moved on how jEdit might additionally assist users in determining where a proof script became broken, but I didn't come to understand why this simple patch would be mutually exclusive to other more elaborate options. Cheers, David 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. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Feature suggestion: apply (meth[1!])
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 wanted to see if I could implement such a feature myself and came up with the attached patch – maybe it is already sufficient? Sorry to raise this thread again, but what was the outcome of this patch? Was the general concept of a solve tactical rejected, or just the particular choice of syntax / implementation? (If so, how could it be improved?) Or have the core developers just been busy? (I apologise if so!) Isar method syntax does not have tacticals at all. The few method combinators are fixed, and not meant to be extended by adhoc patching. It is also conceptually hard to do that, because of the way how a method differs from a tactic in its notion of proof state and goal addressing. So the proposed patch did not make it beyond thise first static type-check. Just last week, I was myself reconsidering the old question if there could be a parallel method combinator, to speedup things like blast+ or force+, but failed to fit it adequately into the existing structures. So its simply not going to happen now. Applying force works for some proofs, but not for systems doing proofs that are meant to be around a bit longer. Of course, I don't want to discourage experimentation, and discussing ideas with an open mind. Getting things accepted into the main code base is a few more orders of magnitude more difficult, though. Even ideas that are commonly understood and generally found beneficial usually sit in the pipeline for several years before they hit the repository. (Compared to Sun/Oracle/Apple and Java the Isabelle development process is incredibly fast; even just compared to Coq.) Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Feature suggestion: apply (meth[1!])
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 we run again into a noisy thread that leads nowhere: the system development process is run by the people doing the actual work. This sounds like a trivial tautology, but is often forgotten. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Feature suggestion: apply (meth[1!])
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 ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Feature suggestion: apply (meth[1!])
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 also show me the concrete sources? Isabelle has so many ways to do things. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Feature suggestion: apply (meth[1!])
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 an idea what is done there? You know we'd be much happier if we could share these proof sources, but it's not under our control (General Dynamics is the owner, I can give you contact details, who knows maybe it actually helps if they start getting emails about this ;-)). But we can show some things. 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 simp done Lars' will probably look very similar. This is not that specific to our proofs, it's an issue with any larger apply-style development, esp with anything that solves verification conditions which aren't that nice to write down in structured proofs, because they tend to be large and uninteresting. It's clear from indentation what is supposed to solve a goal, but it would be much easier for maintenance if proofs failed early. There should be plenty of examples in the AFP, maybe also some in the distribution that would benefit. I'm not sure the ! syntax is the best choice, but that's a separate discussion. Cheers, 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. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Feature suggestion: apply (meth[1!])
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 simp done Lars' will probably look very similar. This is not that specific to our proofs, it's an issue with any larger apply-style development, esp with anything that solves verification conditions which aren't that nice to write down in structured proofs, because they tend to be large and uninteresting. It's clear from indentation what is supposed to solve a goal, but it would be much easier for maintenance if proofs failed early. There should be plenty of examples in the AFP, maybe also some in the distribution that would benefit. 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. Markup.proof_state is there for a long time already, to turn it into some use. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Feature suggestion: apply (meth[1!])
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 mode of checking in the Prover IDE: fail if something is wrong in that respect, or paint things in funny colors. Markup.proof_state is there for a long time already, to turn it into some use. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Feature suggestion: apply (meth[1!])
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 appeal of formalizing an already established convention, which is definitely useful. However, there are two things which make me slightly uncomfortable with this solution: - when I'm exploring a proof which I expect to collapse into a one-line by-statement I usually don't (and don't want to) bother with indentation (this is obviously less of issue when using funny colors). - Isabelle does not have significant whitespace anywhere else (I'm aware of). It does not even consider linebreaks to be relevant. So my initial feeling about this suggestion is neat hack. 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? -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Feature suggestion: apply (meth[1!])
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 in funny colors.
We shortly thought about this earlier and it has the appeal of
formalizing an already established convention, which is definitely
useful. However, there are two things which make me slightly
uncomfortable with this solution:
- when I'm exploring a proof which I expect to collapse into a
one-line by-statement I usually don't (and don't want to) bother
with indentation (this is obviously less of issue when using funny
colors).
- Isabelle does not have significant whitespace anywhere else (I'm
aware of). It does not even consider linebreaks to be relevant. So
my initial feeling about this suggestion is neat hack.
if you want to experiment with assertions about the number of goals at a
specific point in your proof, you can try this:
theory Assert_Goals imports Main
keywords assert_goals :: prf_script % proof
begin
ML {*
fun check_goal_n n state =
let val {context = _, goal = thm} = Proof.simple_goal state
in nprems_of thm = n
end;
Outer_Syntax.command @{command_spec assert_goals} Assert number of goals
(Parse.nat (fn n = Toplevel.proof (fn state = if check_goal_n n state
then state else error Not the expected number of goals)));
*}
end
This lets you say assert_goals 5 in your apply scripts where you think
there should be 5 goals. If that is not the case, then jEdit shows some
red wiggles, but otherwise allows you to continue as before. The error
message could be more verbose, e.g. showing the current goal.
It is a bit verbose and does not work inside a (...)+ nesting, so I’d
still like the [!] or a similar method-level syntax, but at least it
works without modifying the prover.
Greetings,
Joachim
--
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner
signature.asc
Description: This is a digitally signed message part
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Feature suggestion: apply (meth[1!])
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 some interplay of both Isabelle/ML and Isabelle/Scale to be expected, though. Recently I have occasionally revisited the old question of indentation, mainly for structured proofs. This is particularly relevant for editing partial (structurally broken) proof texts, and getting somehow expected errors, not just a red bloodshed over some odd script. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Feature suggestion: apply (meth[1!])
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 Isabelle example sessions, or even the main code base. You can also experiment with something similar as proof method: there is no problem to emit warnings, and then do nothing. You only need to look thrice how it generally interacts with the lazy enumeration scheme of goal states in method expressions (including backtracking). If that is not the case, then jEdit shows some red wiggles, but otherwise allows you to continue as before. That aspect is just an accident of the very weak error recovery of the interactive document processing. After the next round of reforms, an unstructured apply script will stop after the first failed command -- at that level of nested proof structure. Getting that right has much higher priority than adding features elsewhere. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Feature suggestion: apply (meth[1!])
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 method language was designed a certain way, to arrive at stilized specifications of some operational aspects in the proof text. It has excluded any kind of programming or sophisticated control structures on purpose. In 1998 it was not clear yet if that would work out, since the big applications of that time (e.g. HOL-Bali) were done differently. In retrospect the Isar method language was more succesful in this respect than I had anticipated. We see big applications today without lots of specialized goal-state manipulation. As a data point, inside the seL4 proof, a largish application of Isabelle, such a solve-or-fail mechanism would have been very helpful. First of all, we found that examples such as that given by Joachim come up quite frequently. Additionally, such syntax would be very helpful in proof maintenance, where you ideally want the proof script to break at the source of an error, instead of 12 lines further down. Liberal use of apply (foo)! in the more complex proof scripts would help maintainers find the source of an error more quickly. Cheers, David -- 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. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Feature suggestion: apply (meth[1!])
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 via tactics and tacticals. There is a whole zoo of tacticals, and no point to hardwire them in the Isar method combinator syntax. The implementation manual in Isabelle2013 contains an up-to-date chapter 4 on tactical reasoning, which was derived from the classic Isabelle manuals from many years ago. There is also some explanation what it means formally to be a tactic and a proof method. The method_setup command can then be used to provide concrete Isar syntax to suitable methods in the usual manner. The Isar proof method language was designed a certain way, to arrive at stilized specifications of some operational aspects in the proof text. It has excluded any kind of programming or sophisticated control structures on purpose. In 1998 it was not clear yet if that would work out, since the big applications of that time (e.g. HOL-Bali) were done differently. In retrospect the Isar method language was more succesful in this respect than I had anticipated. We see big applications today without lots of specialized goal-state manipulation. In general the problem of what is a good proof interaction language is a very delicate one. To make serious progress, one would have to revisit what you see as Ltac and SSReflect in Coq today, and revisit it on the background of profound understanding how Isar works. Then maybe also combine it with IDE-style templating and outlines produced by the prover. Makarius___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Feature suggestion: apply (meth[1!])
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 classical method of indentation (=number of goals) and try to use only fastforce. But there are cases where I need to use auto[] or simp and in this cases it would be neat if I easily could indicate that a step has to solve a subgoal. Makarius makar...@sketis.net schrieb: 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 via tactics and tacticals. There is a whole zoo of tacticals, and no point to hardwire them in the Isar method combinator syntax. The implementation manual in Isabelle2013 contains an up-to-date chapter 4 on tactical reasoning, which was derived from the classic Isabelle manuals from many years ago. There is also some explanation what it means formally to be a tactic and a proof method. The method_setup command can then be used to provide concrete Isar syntax to suitable methods in the usual manner. The Isar proof method language was designed a certain way, to arrive at stilized specifications of some operational aspects in the proof text. It has excluded any kind of programming or sophisticated control structures on purpose. In 1998 it was not clear yet if that would work out, since the big applications of that time (e.g. HOL-Bali) were done differently. In retrospect the Isar method language was more succesful in this respect than I had anticipated. We see big applications today without lots of specialized goal-state manipulation. In general the problem of what is a good proof interaction language is a very delicate one. To make serious progress, one would have to revisit what you see as Ltac and SSReflect in Coq today, and revisit it on the background of profound understanding how Isar works. Then maybe also combine it with IDE-style templating and outlines produced by the prover. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Feature suggestion: apply (meth[1!])
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 following code: qed (subst fibs.simps, (subst fib.simps)?, simp add: nth_zipWith nth_tail)+ After some change further up, the call to simp would not fully solve a goal any more, and then this would loop. If I could have specified something like qed ((subst fibs.simps, (subst fib.simps)?, simp add: nth_zipWith nth_tail)[1!])+ It would have stopped at the first goal that was not solvable by this script. (Originally posted at http://stackoverflow.com/questions/15290300) It would also be useful to annotate large apply-script style proof, to record where goals are closed. This way, after later changes, it is easier to fix the proofs. I’d like to propose a syntax that extends the existing [n] modifier by an exclamation mark, with the intended meaning that I know or expect the method to solve these goals, and that I want it to fail if it does not. As the n in [n] is already optional with a default to 1, this implies that appending [!] to a method will either solve the first goal or fail. I wanted to see if I could implement such a feature myself and came up with the attached patch – maybe it is already sufficient? If accepted I will follow up with a documentation patch to §6.3.1 of the reference manual. Greetings, Joachim -- Dipl.-Math. Dipl.-Inform. Joachim Breitner Wissenschaftlicher Mitarbeiter http://pp.ipd.kit.edu/~breitner BinÀrdateien Isabelle2013/heaps/polyml-5.5.0_x86-linux/HOL and Isabelle2013-hacked/heaps/polyml-5.5.0_x86-linux/HOL sind verschieden. BinÀrdateien Isabelle2013/heaps/polyml-5.5.0_x86-linux/log/HOL.gz and Isabelle2013-hacked/heaps/polyml-5.5.0_x86-linux/log/HOL.gz sind verschieden. BinÀrdateien Isabelle2013/heaps/polyml-5.5.0_x86-linux/log/Pure.gz and Isabelle2013-hacked/heaps/polyml-5.5.0_x86-linux/log/Pure.gz sind verschieden. BinÀrdateien Isabelle2013/heaps/polyml-5.5.0_x86-linux/Pure and Isabelle2013-hacked/heaps/polyml-5.5.0_x86-linux/Pure sind verschieden. diff -ur Isabelle2013/src/HOL/Tools/try0.ML Isabelle2013-hacked/src/HOL/Tools/try0.ML --- Isabelle2013/src/HOL/Tools/try0.ML 2013-02-12 14:31:12.0 +0100 +++ Isabelle2013-hacked/src/HOL/Tools/try0.ML 2013-03-08 12:48:15.176748616 +0100 @@ -61,7 +61,7 @@ method | parse_method | Method.method thy | Method.Basic - | curry Method.SelectGoals 1 + | (fn t = Method.SelectGoals (1, false, t)) | Proof.refine handle ERROR _ = K Seq.empty (* e.g., the method isn't available yet *) diff -ur Isabelle2013/src/Pure/Isar/method.ML Isabelle2013-hacked/src/Pure/Isar/method.ML --- Isabelle2013/src/Pure/Isar/method.ML 2013-02-12 14:31:14.0 +0100 +++ Isabelle2013-hacked/src/Pure/Isar/method.ML 2013-03-08 12:43:45.464758381 +0100 @@ -53,7 +53,7 @@ Orelse of text list | Try of text | Repeat1 of text | -SelectGoals of int * text +SelectGoals of int * bool * text val primitive_text: (thm - thm) - text val succeed_text: text val default_text: text @@ -289,7 +289,7 @@ Orelse of text list | Try of text | Repeat1 of text | - SelectGoals of int * text; + SelectGoals of int * bool *text; fun primitive_text r = Basic (K (SIMPLE_METHOD (PRIMITIVE r))); val succeed_text = Basic (K succeed); @@ -407,7 +407,7 @@ and meth3 x = (meth4 --| Parse.$$$ ? Try || meth4 --| Parse.$$$ + Repeat1 || - meth4 -- (Parse.$$$ [ |-- Scan.optional Parse.nat 1 --| Parse.$$$ ]) (SelectGoals o swap) || + meth4 -- (Parse.$$$ [ |-- (Scan.optional Parse.nat 1) -- (Scan.optional (Parse.$$$ ! K true) false) --| Parse.$$$ ]) (SelectGoals o Parse.triple1 o swap) || meth4) x and meth2 x = (Parse.position (Parse.xname -- Args.parse1 is_symid_meth) (Source o Args.src) || diff -ur Isabelle2013/src/Pure/Isar/proof.ML Isabelle2013-hacked/src/Pure/Isar/proof.ML --- Isabelle2013/src/Pure/Isar/proof.ML 2013-02-12 14:31:14.0 +0100 +++ Isabelle2013-hacked/src/Pure/Isar/proof.ML 2013-03-08 13:33:58.404649325 +0100 @@ -403,7 +403,7 @@ (K (statement, [], using, goal', before_qed, after_qed)) I) end; -fun select_goals n meth state = +fun select_goals n solve meth state = state | (#2 o #2 o get_goal) | ALLGOALS Goal.conjunction_tac @@ -411,6 +411,7 @@ state | Seq.lift provide_goal (Goal.extract 1 n goal | Seq.maps (Goal.conjunction_tac 1)) | Seq.maps meth +| (if solve then Seq.filter (Thm.no_prems o #2 o #2 o get_goal) else I) | Seq.maps (fn state' = state' | Seq.lift provide_goal (Goal.retrofit 1 n (#2 (#2 (get_goal state'))) goal)) | Seq.maps (apply_method true (K Method.succeed))); @@ -426,7 +427,7 @@ | eval (Method.Orelse txts) = Seq.FIRST (map eval txts) | eval (Method.Try txt) =
