Re: [isabelle-dev] IH in induction-wrapper

2012-04-17 Thread Tobias Nipkow
I am afraid this is a known limitation: inductions on proper terms rather than just variables do not set up IH. We hope to generalise this one day... Tobias Am 17/04/2012 07:26, schrieb Christian Sternagel: Hi all, I think the possibility to refer to the induction hypothesis via, e.g.,

[isabelle-dev] - and --

2012-04-17 Thread Tobias Nipkow
In HOL, the ASCII syntax for \longleftrightarrow is defined to be - but visually -- would be more appropriate, closer to -- and would also leave room for an ASCII syntax for \leftrightarrow (namely -). Any views on such a change? Tobias ___

Re: [isabelle-dev] NEWS: auxiliary contexts

2012-04-17 Thread Lawrence Paulson
I look forward to seeing some documentation on these increasingly mysterious constructs… :-) Larry On 16 Apr 2012, at 11:14, Brian Huffman wrote: On Sun, Apr 15, 2012 at 2:54 PM, Makarius makar...@sketis.net wrote: * Auxiliary contexts indicate block structure for specifications with

Re: [isabelle-dev] Towards the next release

2012-04-17 Thread Gerwin Klein
On 12/04/2012, at 7:02 PM, Makarius wrote: we need to get to a more concrete release schedule. Presently I would like to aim for late May, which means we need to start consolidating and converging about now. Are there any further big things in the pipeline? There are two small things

Re: [isabelle-dev] - and --

2012-04-17 Thread Lawrence Paulson
I don't really mind, and I imagine that there aren't many uses at the moment, so you could get away with it. On the other hand, it does create an incompatibility between HOL and FOL (and therefore ZF). Larry On 17 Apr 2012, at 07:35, Tobias Nipkow wrote: In HOL, the ASCII syntax for

Re: [isabelle-dev] Publishing contributions as an external

2012-04-17 Thread Alexander Krauss
A completely different question is whether we can open testboard to externals. This might reduce some communication overhead we are seeing at the moment (I'm currently testing..., I have pushed..., etc.) Essentially, this is just a matter of setting up a proper push-via-https repository Since

Re: [isabelle-dev] IH in induction-wrapper

2012-04-17 Thread Tobias Nipkow
Revised answer. I was a bit surprised that it did not work and tried to get to the bottom of it with some tracing, but everything seemed to be fine. Then I realised that your inductions are overkill: your inductions are over a predicate, you do not need to give a variable or term as well. If you

Re: [isabelle-dev] IH in induction-wrapper

2012-04-17 Thread Christian Sternagel
Well this was just a stripped-down version of my real proof, in which the term seems to be necessary. Here is a less stripped-down version. notepad begin fix P :: bool and Q :: (nat ⇒ 'a set) ⇒ bool fix f :: nat = 'a set and n :: nat assume finite (f n) and Q f hence P proof

Re: [isabelle-dev] NEWS: auxiliary contexts

2012-04-17 Thread Makarius
On Tue, 17 Apr 2012, Lawrence Paulson wrote: I look forward to seeing some documentation on these increasingly mysterious constructs… :-) It is pretty close to the original concept of section that you've introduced with Florian Kammüller in 1998/1999, so it is much more basic than locales +

Re: [isabelle-dev] - and --

2012-04-17 Thread Makarius
On Tue, 17 Apr 2012, Tobias Nipkow wrote: In HOL, the ASCII syntax for \longleftrightarrow is defined to be - but visually -- would be more appropriate, closer to -- A brief look at the history and source archive shows that this ASCII art has already been there since Isabelle86. Larry might

Re: [isabelle-dev] - and --

2012-04-17 Thread Lawrence Paulson
As regards motivation, remember, back then it was a thing of beauty. I could easily remember the day when it was possible to use lowercase letters. I think you are right that ASCII syntax is almost completely irrelevant now. Hardly anybody sees it. Even on my MacBook where the Unicode

Re: [isabelle-dev] Towards the next release

2012-04-17 Thread Makarius
On Tue, 17 Apr 2012, Gerwin Klein wrote: - I would like to add a size limit to records beyond which no code generator setup is performed. The main reason is that on sizes 200 fields or so, the setup does not make any sense, but consumes very large amounts of memory (and time). Switching it

[isabelle-dev] record: fold_congs/unfold_congs

2012-04-17 Thread Makarius
This is probably mainly relevant to NICTA users of the record package. When doing some cleanup and performance tuning of the record package, I discovered the following mysterious fold_congs and unfold_congs:

Re: [isabelle-dev] Relations vs. Predicates

2012-04-17 Thread Makarius
Here is another follow-up to the relcomp story so far: changeset: 47508:85c6268b4071 tag: tip user:wenzelm date:Tue Apr 17 16:48:37 2012 +0200 files: doc-src/TutorialI/Sets/Relations.thy description: updated rel_comp ~ relcomp (cf. e1b761c216ac);

Re: [isabelle-dev] - and --

2012-04-17 Thread Tobias Nipkow
Am 17/04/2012 16:13, schrieb Makarius: On Tue, 17 Apr 2012, Tobias Nipkow wrote: and would also leave room for an ASCII syntax for \leftrightarrow (namely -). Using -- for - and making room for another - would also mean that the user has to type/read the longer unwieldy sequence by

Re: [isabelle-dev] - and --

2012-04-17 Thread Tobias Nipkow
Am 17/04/2012 16:27, schrieb Lawrence Paulson: I think you are right that ASCII syntax is almost completely irrelevant now. Hardly anybody sees it. It is relevant as an input method, and that is exactly what my suggestion is about. I am not interested in ASCII art but in a smooth input method.

Re: [isabelle-dev] - and --

2012-04-17 Thread Makarius
On Tue, 17 Apr 2012, Tobias Nipkow wrote: Am 17/04/2012 16:27, schrieb Lawrence Paulson: I think you are right that ASCII syntax is almost completely irrelevant now. Hardly anybody sees it. It is relevant as an input method, and that is exactly what my suggestion is about. I am not

Re: [isabelle-dev] - and --

2012-04-17 Thread Lawrence Paulson
I certainly care about it. Jedit is great for browsing existing theory developments, but there is no support for actually doing proofs. Larry On 17 Apr 2012, at 16:56, Makarius wrote: Anyway, who is maintaining Isabelle ProofGeneral now? The repository version does not work with Emacs 23

[isabelle-dev] Future of ProofGeneral

2012-04-17 Thread Makarius
On Tue, 17 Apr 2012, Lawrence Paulson wrote: I certainly care about it. Jedit is great for browsing existing theory developments, but there is no support for actually doing proofs. As I've said already 4 years ago, the double burden to keep ProofGeneral alive and make Isabelle/jEdit a full

Re: [isabelle-dev] - and --

2012-04-17 Thread Peter Lammich
Anyway, who is maintaining Isabelle ProofGeneral now? The repository version does not work with Emacs 23 for several months already. It seems that nobody cares about it anymore. For the release, I will package up official ProofGeneral-4.1 as last time. It is then up to its users to

Re: [isabelle-dev] - and --

2012-04-17 Thread Peter Lammich
Anyway, who is maintaining Isabelle ProofGeneral now? The repository version does not work with Emacs 23 for several months already. It seems that nobody cares about it anymore. For the release, I will package up official ProofGeneral-4.1 as last time. It is then up to its users to

Re: [isabelle-dev] - and --

2012-04-17 Thread Tobias Nipkow
Am 17/04/2012 17:56, schrieb Makarius: Why then the proposal to change the prover syntax? What I meant was not just the prover syntax but also the input syntax. In fact, primarily the input syntax. One could change merely the latter (which is what PG does), but that introduces an inconsistency:

Re: [isabelle-dev] - and --

2012-04-17 Thread Alexander Krauss
On 04/17/2012 05:41 PM, Tobias Nipkow wrote: This is what I would call unwieldy: instead of typing-- or- (and having them converted to the appropriate symbols) you always type-, but then you have to select from a menue. I don't see the progress. Could not agree more. These arrows are very

Re: [isabelle-dev] Future of ProofGeneral

2012-04-17 Thread Makarius
On Tue, 17 Apr 2012, Peter Lammich wrote: Anyway, who is maintaining Isabelle ProofGeneral now? The repository version does not work with Emacs 23 for several months already. It seems that nobody cares about it anymore. For the release, I will package up official ProofGeneral-4.1 as last

Re: [isabelle-dev] - and --

2012-04-17 Thread Makarius
On Tue, 17 Apr 2012, Alexander Krauss wrote: On 04/17/2012 05:41 PM, Tobias Nipkow wrote: This is what I would call unwieldy: instead of typing-- or- (and having them converted to the appropriate symbols) you always type-, but then you have to select from a menue. I don't see the progress.

Re: [isabelle-dev] Future of ProofGeneral

2012-04-17 Thread Lawrence Paulson
Sorry, I didn't intend to be tactless or demanding, but at least something analogous to the “Isabelle menu (offering access to show me/commands/prover settings) is needed. Unless it's there somewhere and I overlooked it. Larry On 17 Apr 2012, at 17:18, Makarius wrote: On Tue, 17 Apr 2012,

Re: [isabelle-dev] Future of ProofGeneral

2012-04-17 Thread Makarius
On Tue, 17 Apr 2012, Lawrence Paulson wrote: I didn't intend to be tactless or demanding, but at least something analogous to the “Isabelle menu (offering access to show me/commands/prover settings) is needed. Unless it's there somewhere and I overlooked it. No it is one of the known things

Re: [isabelle-dev] Towards the next release

2012-04-17 Thread Gerwin Klein
On 18/04/2012, at 12:29 AM, Makarius wrote: On Tue, 17 Apr 2012, Gerwin Klein wrote: - I would like to add a size limit to records beyond which no code generator setup is performed. The main reason is that on sizes 200 fields or so, the setup does not make any sense, but consumes very

Re: [isabelle-dev] Relations vs. Predicates

2012-04-17 Thread Christian Sternagel
Sorry for the inconveniences. On 04/17/2012 11:55 PM, Makarius wrote: Here is another follow-up to the relcomp story so far: changeset: 47508:85c6268b4071 tag: tip user: wenzelm date: Tue Apr 17 16:48:37 2012 +0200 files: doc-src/TutorialI/Sets/Relations.thy description: updated rel_comp ~

Re: [isabelle-dev] - and --

2012-04-17 Thread Christian Sternagel
Just for the record: I exclusively use jEdit for several weeks now and did quite a lot of actual proofs. My personal opinion: the user experience is much nicer than with emacs * I did not have any complete hangs yet (as with emacs) * the whole appearance is much nicer (remember, this is my

Re: [isabelle-dev] - and --

2012-04-17 Thread Christian Sternagel
+1 for -- (since it would agree, as Tobias pointed out, with the established =, ==, -, --). Concerning convenience of input and automatic replacement: I would not use automatic replacement at all, since it is at least as often a problem as it is of help (e.g., ML code inside theories = in

[isabelle-dev] jEdit

2012-04-17 Thread Christian Sternagel
Dear Makarius, it's very nice that after sledgehammer found a proof command to finish a proof, I can simply click on this command in the output buffer to include it in the main buffer! A slight oddity is that this merges lines. E.g., lemma ⟦xs @ ys = ys @ xs; length xs = length ys⟧ ⟹ xs =

Re: [isabelle-dev] record: fold_congs/unfold_congs

2012-04-17 Thread Thomas Sewell
The fold_congs theorems are not an accident. They are used as congruence rules to perform conversions such as rec (| x := rec x + 1 |) = x_update (%x. x + 1) rec. Note this removes the duplicated mention of the name rec. The name fold_congs is somewhat arbitrary, since either direction above

Re: [isabelle-dev] record: fold_congs/unfold_congs

2012-04-17 Thread Michael Norrish
On 18/04/12 1:46 PM, Thomas Sewell wrote: This is used in our modified version of the Schirmer Hoare VCG. I suppose that we've released the c-parser sources (which load extra fold_congs) but not the modified Hoare package (which uses them). The point is to avoid an exponential time/space