Re: [isabelle-dev] Isabelle (proof assistant) - Wikipedia, the free encyclopedia
Hi, Am Freitag, den 22.02.2013, 08:49 +0100 schrieb Gergely Buday: Wiki is old-fashioned these days, how about using Stack Exchange for Isabelle user communication? What do you think about this? I guess this is getting off-topic for isabelle-dev and should rather be discussed on the users list. Anyways: I find SE a good format for the typical questions that are raised on the users list, but I am not sure if the community is large enough to provide reasonable fast and good answers there to make it useful. But it could be worth a try. 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
[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
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] Code export to Haskell and lower-case theory names
Hi, Am Freitag, den 29.03.2013, 13:24 +0100 schrieb Makarius: This has got nothing to do with Isabelle's informal conventions but is all about the target language's formal rules. The conventions about theory names and locale/class names are not that informal. If you violate them systematically, certain name space policies will break down. That is then a general user error. Are there really things that break if I deviate from the convention? Then it should be a hard rule enforced by the system. If that is not the case, then it should be fully supported and up to the user to choose his naming, even if it deviate from what others use (she might have reasons for that). Greetings and happy easter to those who care, 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] Code export to Haskell and lower-case theory names
Hi, Am Freitag, den 29.03.2013, 15:32 -0700 schrieb Brian Huffman: On Fri, Mar 29, 2013 at 10:40 AM, Joachim Breitner breit...@kit.edu wrote: Am Freitag, den 29.03.2013, 13:24 +0100 schrieb Makarius: This has got nothing to do with Isabelle's informal conventions but is all about the target language's formal rules. The conventions about theory names and locale/class names are not that informal. If you violate them systematically, certain name space policies will break down. That is then a general user error. Are there really things that break if I deviate from the convention? The main problem I know about is that qualified names can become ambiguous: e.g. if foo.bar.baz and bar.boo.baz are both in scope, then bar.baz could refer to either of them. The problem is avoided if theory names and locale/type/constant names are kept disjoint. See also this old thread: https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2011-July/001674.html but in every case there is a more qualified name that can be used to identify each entity? I would not consider that a hard problem, just an annoyance. I read this as “if you deviate from the suggested scheme, things might become a little bit less convenient, but everything still works” which I find fair enough. 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] Code export to Haskell and lower-case theory names
Hi, Am Dienstag, den 02.04.2013, 12:31 +0200 schrieb Makarius: So far there were no reasons given on this thread why the convention should not be followed first place. Are there any? ignorance? I was using Isabelle for quite a while before I heard about these conventions, and even longer before I learned that not following them can cause severe issues. As I said: If it can cause issues beyond inconvenience (and you say it can), then the convention should become the rule and enforced by the system, to prevent users from accidentally not following the rule. 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] Interpretation in arbitrary targets.
Hi, Am Mittwoch, den 24.04.2013, 19:16 +0200 schrieb Florian Haftmann: This is a great triumph of the »local everything« approach. I’m not sure that I understand all that is going on, but I have the feeling that the theory that I’m working on will greatly benefit from your development, and I’m looking forward to Isabelle 2013-2 (or 2014). So thanks in advance from my side! 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] Proper AFP history on the web
Hi, Am Freitag, den 12.07.2013, 13:09 +0200 schrieb Makarius: On Wed, 10 Jul 2013, Gerwin Klein wrote: Looking once more at http://sourceforge.net/p/afp/code/ci/default/tree I still cannot see a proper way to get an overview of changes, covering all files that are touched. The Browse Commits view shows again only single files with their history (and the graph is rendered in very low quality). A little bit hidden, but there is http://sourceforge.net/p/afp/code/ci/tip/log/ which seems to list all commits to the repository, and from there you get to links like http://sourceforge.net/p/afp/code/ci/908304753f7d30177997524427d78029ea77a331/ that cleanly shows all changes of that commit. You can manually shorten it to http://sourceforge.net/p/afp/code/ci/908304 and it still works. 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] Orphaned theory in AFP
Hi, Am Freitag, den 25.10.2013, 21:32 +0200 schrieb Florian Haftmann: (69ff07418cc2) Free-Groups/NielsenSchreier.thy that must be an artefact of my failure to use mercurial correctly. I have that file in a local feature branch and must have merged it wrongly at some time. Feel free to remove it. 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] Isabelle World Map
Hi, Am Freitag, den 24.01.2014, 14:13 +0100 schrieb Makarius: On Fri, 24 Jan 2014, Tobias Nipkow wrote: the number of pins is not that impressive There is always this unknown variable of actual Isabelle users. We have occasionally made some statistics from the server log of the mirror sites, to guess the number of downloads. Maybe we should to this again, but I don't know how it works. well, doesn’t Isabelle ship by default with the spy features^W^Wremote remote solvers enabled for sledgehammer? Assuming that a representative portion of users use sledgehammer and do not disable these, measuring those remote requests should give you pretty precise numbers. And I believe one of them disabled itself for me after heavy use, and told me that I used up my allowance, so there must already be some user-tracking and identifying in place (...scary, BTW). 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] NEWS: method facts
Hi, Am Mittwoch, den 08.06.2016, 19:46 +0200 schrieb Makarius: > There are further possibilities for "use", e.g. to eliminate > auxiliary > "-" or "insert" steps, notably: > > qed (insert a, auto) ~> qed (use a in auto) does this mean that the old idiom of lemma foo: assumes "inductive_predicate x" shows "something_about x" using assms proof(induction x) ... qed can (and should) now become the slightly nicer lemma foo: assumes "inductive_predicate x" shows "something_about x" p roof(use assms in ‹induction x›) ... qed or is the need for method nesting no better than the extra using assms? Thanks, Joachim -- Dr. rer. nat. 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] NEWS: method facts
Dear Markarius, Am Donnerstag, den 09.06.2016, 15:58 +0200 schrieb Makarius: > > [..] Turning 'using' into "use" is a downgrade of proof command into proof > method. This is occasionally useful, like e.g. using attribute > expressions instead of proof methods, but not something I would do all > the time. > > First-class tickets on the Isar train are preferable. thanks for that view on things, and the stratificationof the lange makes sense. But while I like "using" inside an proof, it does not please my sense of aesthetic to have such a command before the initial "proof" command. Maybe a way out would be to take inspiration of how we can avoid some explicit fact chaining inside proof..qed blocks, namely using "thus" instead of "then show", and apply the usual logic of “appending s moves a command from the local variant to the corresponding context specification command”. This would allow me to write (applying the usual rules of the English grammer): lemma foo: assumes "inductive_predicate x" thuses "something_about x" proof(use assms in ‹induction x›) ... qed SCNR, Joachim -- Dr. rer. nat. 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
