[isabelle-dev] sledgehammer issues

2007-09-06 Thread Lawrence Paulson
I have just committed a new version with various changes, including support for structured proofs with a new version of Vampire. Please download a new Vampire binary from http://www.cl.cam.ac.uk/research/ hvg/Isabelle/atp-linkup.html (Linux only) if you use Vampire. The environment variables

[isabelle-dev] position of Hilbert_Choice in the HOL theory hierarchy

2007-09-14 Thread Lawrence Paulson
Florian has suggested making sledgehammer available earlier in the construction of Main, before PreList at least. This could be useful to developers. However, it requires Hilbert_Choice, which must also be introduced earlier. We previously put some effort into making virtually all of HOL

[isabelle-dev] position of Hilbert_Choice in the HOL theory hierarchy

2007-09-14 Thread Lawrence Paulson
It needs at least Hilbert_Choice. It could go before Datatype. Some details need to be worked out to ensure that all theorems in Main.thy get converted to clause form. Larry On 14 Sep 2007, at 14:46, Florian Haftmann wrote: A PreList-Sledgehammer would be a nice thing to have, but it is not

[isabelle-dev] blast

2007-10-10 Thread Lawrence Paulson
I'm sure you are right. We could try taking it out, though I suspect this will break many proofs. Larry On 10 Oct 2007, at 12:03, Tobias Nipkow wrote: I have had problems with the conversion from ~ x = (0::nat) to x 0 as well. Can anyone recall why we installed that? I suspect it may

[isabelle-dev] HOL vs. HOL-Complex

2008-07-02 Thread Lawrence Paulson
I see a giant misconception coming. The point of nonstandard analysis is that it makes properties of limits, derivatives, and so forth much easier to prove than can be done with the standard definitions. They eliminate the necessity of arguments involving epsilon and delta. So it would be

[isabelle-dev] HOL vs. HOL-Complex

2008-07-03 Thread Lawrence Paulson
I am happy with this. I just wanted to remind everybody that the nonstandard system allows really simple, intuitive proofs. Larry On 2 Jul 2008, at 17:45, Brian Huffman wrote: Here's how I see it: If all you want to do is *use* analysis (e.g. maybe you just want to calculate derivatives)

[isabelle-dev] ZF and HOL in same session?

2008-08-21 Thread Lawrence Paulson
Unfortunately I don't know the answer to this. I have copied this message to the developers mailing list and maybe somebody else can help you. Larry On 21 Aug 2008, at 11:02, Norbert Voelker wrote: Larry/Tobias, the Isabelle2008 News contain the following intriguing sentence: *

[isabelle-dev] Mercurial conversion relaunch

2008-09-04 Thread Lawrence Paulson
Changing revision control systems would be a major upheaval, so I hope it will bring clear benefits. First, as a very obvious point, I assume that there is a way of importing the entire revision history (not just the current snapshot) into the new system. It would not be acceptable if we

[isabelle-dev] Fwd: Broken link

2008-10-01 Thread Lawrence Paulson
The error that he refers to concerns the relative links in the following HTML source code: ul lia href=HOL/index.htmlHOL (Higher-Order Logic)/a is a version of classical higher-order logic resembling that of the a href=http://www.cl.cam.ac.uk/Research/HVG/HOL/;HOL System/a./li lia

[isabelle-dev] An ARBITRARY question

2008-10-03 Thread Lawrence Paulson
What is the difference between willundefined and arbitrary? Larry On 2 Oct 2008, at 18:44, Tobias Nipkow wrote: undefined and default are used in a specific way. If you do not want that functionality (and accidental equalities), arbitrary is a good alternative. Tobias Florian Haftmann

[isabelle-dev] An ARBITRARY question

2008-10-03 Thread Lawrence Paulson
Apologies for that garbled message. I meant, What is the difference between undefined and arbitrary? Larry On 2 Oct 2008, at 18:44, Tobias Nipkow wrote: undefined and default are used in a specific way. If you do not want that functionality (and accidental equalities), arbitrary

[isabelle-dev] Numeral simplification: neg and iszero

2008-12-09 Thread Lawrence Paulson
When I introduced these constants, they were certainly necessary. Then, binary arithmetic executed by pure rewriting. I don't object to getting rid of them if they are now unnecessary. But it hardly seems worth investing a significant effort. They don't cause a problem, do they? It may be

[isabelle-dev] MacMercurial

2009-01-30 Thread Lawrence Paulson
Mac users may want to try this user interface to mercurial. It makes it easy to do the most common tasks, including fetch, push, commit and also to display differences. It is less good at showing differences between your copy of a file and the remote copy. MacMercurial is a graphic user

[isabelle-dev] setsum/setprod

2009-02-17 Thread Lawrence Paulson
We implement a nice syntax for summations indexed over intervals, but nothing comparable products. The code below is from the file SetInterval.thy. Products are treated instead in the file Finite_Set.thy. Is there a fundamental reason why sums and products are treated so differently? Larry

[isabelle-dev] Suc 0 necessary?

2009-02-23 Thread Lawrence Paulson
syntax and not help with the algebraic 1, but it may already satisfy some people. Tobias Lawrence Paulson wrote: My guess is that otherwise many obvious theorems involving 1 and primitive recursive functions will not be proved. We have tangled with this issue many times. It would be great

[isabelle-dev] Type error in metis call with Toplevel.debug

2009-06-15 Thread Lawrence Paulson
The offending code is here: fun fol_terms_to_hol ctxt fol_tms = let val ts = map (fol_term_to_hol_RAW ctxt) fol_tms val _ = Output.debug (fn () = calling type inference:) val _ = app (fn t = Output.debug (fn () = Syntax.string_of_term ctxt t)) ts val ts' =

[isabelle-dev] I'm a new Isabelle User!

2009-07-24 Thread Lawrence Paulson
I hope you do join the Isabelle users's mailing list, as I suggested in my previous message. However, I do not recommend that you join the list for developers. Larry Paulson On 22 Jul 2009, at 10:29, patrick dabou wrote: hi! my name is Nounamo Dabou Patrick, i'm student in the university

[isabelle-dev] HOL-Bali

2009-08-14 Thread Lawrence Paulson
I have no idea. With Mercurial I don't know how to compare what I have with what it should be. Larry On 14 Aug 2009, at 10:16, Stefan Berghofer wrote: it seems that the \^sup in r\^sup* has disappeared. Maybe some Emacs oddity?

[isabelle-dev] HOL-Bali

2009-08-14 Thread Lawrence Paulson
weren't visible yesterday. Larry On 14 Aug 2009, at 11:41, Alexander Krauss wrote: Lawrence Paulson wrote: I have no idea. With Mercurial I don't know how to compare what I have with what it should be. Does hg diff not help? Alex

[isabelle-dev] x-symbols

2009-08-26 Thread Lawrence Paulson
, at 19:02, David Aspinall wrote: Lawrence Paulson wrote: Does anybody know what would cause the symbols that look like this? It is the latest version of proof general running under GNU Emacs 22.2.1 Nobody else came running so I'll answer... First of all: everyone will have a *much* better

[isabelle-dev] MacMercurial

2009-08-27 Thread Lawrence Paulson
Possibly of interest to Mac users. It is particularly good at monitoring the status of your local files and comparing them with your local repository. http://www.jwwalker.com/pages/macmerc.html Larry -- next part -- An HTML attachment was scrubbed... URL:

[isabelle-dev] Mercurial

2009-09-07 Thread Lawrence Paulson
I recently had a number of problems with Mercurial. The cause of one of them turned out to be that Mercurial doesn't interact with MacOS X very well, so although the commit command launches an editor to request a commit message, this message never reaches mercurial. But a more serious

[isabelle-dev] HOL is not building

2009-10-20 Thread Lawrence Paulson
HOL is not building, see attached. Don't ask for the change set identifier because I couldn't tell you even to save my life. I can tell you that it has been like this for the past several hours. Larry *** Unknown attribute: smt_cert (line 22 of /Users/lp15/isabelle/

[isabelle-dev] NEWS

2009-10-28 Thread Lawrence Paulson
* New theory SupInf of the supremum and infimum operators for sets of reals. * New theory Probability, which contains a development of measure theory, eventually leading to Lebesgue integration and probability. Larry

[isabelle-dev] HOL FAILED

2009-10-01 Thread Lawrence Paulson
I have just done a fetch and can no longer build Isabelle/HOL. I hope somebody can fix this soon. Larry Building HOL ... HOL FAILED (see also /Users/lp15/.isabelle/heaps//polyml-5.2.1_x86-darwin/log/HOL) *** Warning: Pattern is not exhaustive. Found near *** val ( [ isom_def], cdef_thy) = |(

[isabelle-dev] Isabelle/HOL axiom ext is redundant

2009-11-12 Thread Lawrence Paulson
Briefly, x == y was intended to express the definition of x in terms of y. Larry On 11 Nov 2009, at 21:46, Alexander Krauss wrote: While we're discussing it: I wonder sometimes what the role of == was in earlier days of Isabelle. When viewing Pure as the natural deduction framework to

[isabelle-dev] Isabelle/HOL axiom ext is redundant

2009-11-12 Thread Lawrence Paulson
If you do these things, you put an end to all Isabelle logics other than Isabelle/HOL. Remember, an object logic does not need to possess an equality symbol or even an implication symbol. Having just translated some lengthy, incomprehensible HOL proofs into Isabelle, I appreciate more than

[isabelle-dev] Isabelle/HOL axiom ext is redundant

2009-11-12 Thread Lawrence Paulson
The situation regarding these inference rules is quite different. Isabelle is primarily based on resolution, which is a big, complicated piece of code implementing what is supposed to be a sound form of reasoning in intuitionistic Higher-order logic. However, it claims to be based on that

[isabelle-dev] Isabelle/HOL axiom ext is redundant

2009-11-13 Thread Lawrence Paulson
This sort of discussion is analogous to suggesting that we get rid of and/or/not/implies and write all formulas using the Scheffer stroke (NAND), or that Gentzen's sequent calculus should be replaced by the much simpler Hilbert system. It can be done, but who would want to do it? Larry

[isabelle-dev] Isabelle/HOL axiom ext is redundant[SEC=UNCLASSIFIED]

2009-11-16 Thread Lawrence Paulson
In the beginning, it was precisely as you describe. Even now, Isabelle/ZF and Isabelle/CTT continue to distinguish metalevel functions (which in ZF would be seen as operators or class functions) from the functions of the formalism. I published and implemented an early formalisation of simple

[isabelle-dev] Pow

2009-12-14 Thread Lawrence Paulson
Anybody know why find theorems can find nothing about the power set operator? Other set theoretic primitives, such as Union and insert, work fine. Larry -- next part -- A non-text attachment was scrubbed... Name: screen-capture.png Type: image/png Size: 24748 bytes Desc:

[isabelle-dev] Pow

2009-12-14 Thread Lawrence Paulson
Yes, Main is included; see below. Larry On 14 Dec 2009, at 12:46, Tobias Nipkow wrote: I get to see 21 thms. Are you sure Set is included as an ancestor, eg via Main? -- next part -- A non-text attachment was scrubbed... Name: screen-capture-1.png Type: image/png Size:

[isabelle-dev] wwwfind

2010-01-19 Thread Lawrence Paulson
We advertise wwwfind as the leading new feature of Isabelle 2009-1. But how is it actually invoked? I could find no mention of it in PG. On my Mac, it does this: ~: isabelle wwwfind Platform Darwin currently not supported by wwwfind component. On a Linux workstation, it does this: rhee:

[isabelle-dev] wwwfind

2010-01-20 Thread Lawrence Paulson
for each and every machine that needs to have lighttpd installed. This is quite a deterrent :-( Larry On 19 Jan 2010, at 22:11, Gerwin Klein wrote: On 19/01/2010, at 9:33 PM, Lawrence Paulson wrote: We advertise wwwfind as the leading new feature of Isabelle 2009-1. But how is it actually

[isabelle-dev] wwwfind

2010-01-20 Thread Lawrence Paulson
Ideally one could select between the standard libraries, the full libraries (everything within HOL) and the AFP by a menu. But there is no need to overcomplicate it the first time. The default should just be HOL/Library. Larry On 20 Jan 2010, at 11:13, Gerwin Klein wrote: This would be a good

[isabelle-dev] what's wrong with my system?

2010-03-01 Thread Lawrence Paulson
I'm not sure what has gone wrong with my system. I don't think I have changed anything. It may be that I downloaded and recompiled poly/ML. Now I can't build Isabelle any more: Loading theory Complex_Main val it = () : unit Error occurred during initialization of VM Unable to load native

Re: [isabelle-dev] construction of the real numbers

2010-05-10 Thread Lawrence Paulson
Thank you for doing this. It's interesting that you have found a shorter formalisation, because the approach previously adopted had been carefully selected to require the minimum effort. I agree that the old formalisation should be kept somewhere (possibly in the AFP) because comparing

Re: [isabelle-dev] Bug in linordered_ring_less_cancel_factor simproc

2010-05-10 Thread Lawrence Paulson
I have looked at this ancient code again, and think I understand the problem. prove_conv is mostly used to prove the conclusion of the simproc. If the two terms are equal, then it is unwanted, so the correct response is to fail. That is why the aconv test is there. But occasionally,

[isabelle-dev] Aquamacs emacs

2010-05-15 Thread Lawrence Paulson
Aquamacs 2.0 was released last week (http://aquamacs.org/), and it seems to be very much better than previous versions. I have been using it without difficulties in conjunction with proof general 4.0. I didn't notice any of the old problems. Symbols display correctly; cut and paste work

Re: [isabelle-dev] Aquamacs emacs

2010-05-15 Thread Lawrence Paulson
I've used PG Version 4.0pre091204 quite a bit, no problems. What goes wrong with it? Larry On 15 May 2010, at 15:32, Makarius wrote: Which version of PG 4 is this? I only know of ProofGeneral-4.0pre091204.tgz, and the repository version seems to be mostly identical to that, which means it

Re: [isabelle-dev] Aquamacs emacs

2010-05-17 Thread Lawrence Paulson
it again, but that was after hours of work. Perhaps something is different about our systems. I'm using a Mac with snow leopard. Larry On 17 May 2010, at 10:46, Makarius wrote: On Sat, 15 May 2010, Lawrence Paulson wrote: I've used PG Version 4.0pre091204 quite a bit, no problems. What goes wrong

Re: [isabelle-dev] [isabelle] safe for boolean equality

2010-06-14 Thread Lawrence Paulson
Equalities involving constants have never been eliminated in this way. The equality must involve a variable, free or bound. The method has no way of knowing about constraints on the variable that are not part of the goal. In the case of a structured proof, it would be appropriate and natural to

Re: [isabelle-dev] [isabelle] safe for boolean equality

2010-06-15 Thread Lawrence Paulson
. Yours, Thomas. ___ From: isabelle-dev-boun...@mailbroy.informatik.tu-muenchen.de [isabelle-dev-boun...@mailbroy.informatik.tu-muenchen.de] On Behalf Of Lawrence Paulson [l...@cam.ac.uk] Sent: Tuesday, June 15, 2010 1:12 AM To: Brian Huffman Cc: isabelle

Re: [isabelle-dev] [isabelle] safe for boolean equality

2010-06-15 Thread Lawrence Paulson
If there is an easy way to identify free variables that are constrained externally, then such a change would be beneficial. Failing that, the particular case of locales is particularly necessary to handle correctly. Larry On 15 Jun 2010, at 14:17, Brian Huffman wrote: Note that testing

Re: [isabelle-dev] [isabelle] safe for boolean equality

2010-06-16 Thread Lawrence Paulson
. This is bad advice if “auto” can render the problem impossible to prove. Larry On 15 Jun 2010, at 10:17, Jasmin Christian Blanchette wrote: Am 15.06.2010 um 11:03 schrieb Lawrence Paulson: Altering the behaviour of the safe method on locale constants might be feasible, because it would

Re: [isabelle-dev] Beta/Eta normalisation and net matching.

2010-08-04 Thread Lawrence Paulson
This practically goes back to the dawn of time. Any theorem produced by resolution would be beta-eta-normal. And this includes most theorems, but certainly not all. Larry On 4 Aug 2010, at 02:50, Thomas Sewell wrote: Hello Isabelle developers. I was about to have another attempt at

Re: [isabelle-dev] [isabelle] safe for boolean equality

2010-08-05 Thread Lawrence Paulson
This sort of thing is well-known but very rare these days. I guess it could trap an unwary user. It just isn't easy to fix, given the old strategy of using assumptions, discarding them, and repeating. Larry On 5 Aug 2010, at 06:33, John Matthews wrote: Was it ever resolved whether auto should

Re: [isabelle-dev] Safe approach to hypothesis substitution

2010-08-31 Thread Lawrence Paulson
Thanks for looking into this problem, which has been around in one way or another from the very beginning. Lost in all the technical discussions is the question of what the user will see. We have the option of leaving blast and force as they are now to minimise danger of incompatibility,

Re: [isabelle-dev] Safe approach to hypothesis substitution

2010-09-01 Thread Lawrence Paulson
This sounds logical. But what about auto? Like the other three, it is used to perform obvious steps in a proof, and it is not terminal. Larry On 1 Sep 2010, at 14:17, Thomas Sewell wrote: Let me try to explain the difference from the perspective of a user. There are three classical tools

Re: [isabelle-dev] Safe approach to hypothesis substitution

2010-09-01 Thread Lawrence Paulson
I always intended auto to be initial rather than terminal. I'm not aware of the unsafe mode you refer to, but it may have been introduced later. Larry On 1 Sep 2010, at 14:40, Thomas Sewell wrote: Good point - I think of auto as terminal. My understanding was that auto had both a safe and

Re: [isabelle-dev] find_theorems raises UnequalLengths exception

2010-11-18 Thread Lawrence Paulson
That is certainly my change, but I don't understand why preventing self-referential type instantiations should affect the find_theorems function. Can you get a full trace back from the exception? Larry On 18 Nov 2010, at 16:03, Brian Huffman wrote: Hello everyone, Recently I noticed that

Re: [isabelle-dev] typedef (open) unit

2010-11-19 Thread Lawrence Paulson
It looks like something that I put in long ago, but honestly I cannot see a use for it. Larry On 19 Nov 2010, at 10:43, Makarius wrote: If you think it is useful to have Isabelle/HOL provide a constant Product_Type.unit == {True}, then by all means put it back in. I don't know if that is

Re: [isabelle-dev] [isabelle] Higher-order matching against schematic variables

2010-11-19 Thread Lawrence Paulson
, Michael Chan wrote: On 18/11/10 16:07, Lawrence Paulson wrote: I can't see the answer to this, but something complicated is going on when you match (?f::((?'a=?'b)=?'c)) ?stuff against x y where x :: nat = nat. Thanks, Larry. Indeed, even without the predicate, it gives the same problem

Re: [isabelle-dev] [isabelle] Higher-order matching against schematic variables

2010-11-19 Thread Lawrence Paulson
Looking at this again, I'm not certain there is a bug. You are displaying the variable assignments, but are you first applying the type variable assignments? Both must be used in order to instantiate the object term. Larry On 19 Nov 2010, at 11:11, Michael Chan wrote: I can confirm that the

Re: [isabelle-dev] find_theorems raises UnequalLengths exception

2010-11-19 Thread Lawrence Paulson
. Just for the record: the code eta-expands terms on the fly, but the presence of beta-redexes may well confuse it. Tobias Lawrence Paulson schrieb: I'll give it a try. Larry On 19 Nov 2010, at 13:46, Tobias Nipkow wrote: The code is mine and I haven't looked at it for some 15 years. I

Re: [isabelle-dev] [isabelle] Higher-order matching against schematic variables

2010-11-19 Thread Lawrence Paulson
), you won't see the effect of the type variable assignments. Larry On 19 Nov 2010, at 13:02, Michael Chan wrote: On 19/11/10 12:28, Lawrence Paulson wrote: Looking at this again, I'm not certain there is a bug. You are displaying the variable assignments, but are you first applying the type

Re: [isabelle-dev] [isabelle] Higher-order matching against schematic variables

2010-11-19 Thread Lawrence Paulson
Indeed I find the code peculiar, in that it delivers the higher-order matchers followed by the first-order ones. But these are different things. And I imagine there is often redundancy. Larry On 19 Nov 2010, at 15:50, Michael Chan wrote: On 19/11/10 14:10, Lawrence Paulson wrote: If you look

Re: [isabelle-dev] Coral and Sledgehammer

2010-11-22 Thread Lawrence Paulson
Thanks for reminding me of this paper. It states that the modified version of SPASS implements answer literals, which would allow sledgehammer for the first time to handle variables in subgoals. This could be quite useful. What do others think? Of course, we would also have to consider the

Re: [isabelle-dev] Additional type variable(s) in specification

2010-12-02 Thread Lawrence Paulson
I agree! Larry On 2 Dec 2010, at 14:44, Brian Huffman wrote: Besides these two very specific cases, I think it would be best to reject definitions with extra type variables on the right-hand side. ___ isabelle-dev mailing list isabelle-...@in.tum.de

Re: [isabelle-dev] Isabelle release

2011-01-07 Thread Lawrence Paulson
I'm afraid that I originated the custom of not always linking the release name to the calendar year. The idea was to indicate that the new release consisted of little more than patches from the previous one. So, one option is to call it Isabelle 2009-3, which would mean that it is still

Re: [isabelle-dev] Isabelle release

2011-01-07 Thread Lawrence Paulson
I'm afraid that English wine production has been increasing year by year. Some of them are even said to be good. http://www.english-wine.com/vineyards.html Larry On 7 Jan 2011, at 09:30, Tobias Nipkow wrote: I like the wine connection! Not just French wines, but also Australian ones, and

[isabelle-dev] Fwd: [isabelle] Problem with frule_tac substitution

2011-02-08 Thread Lawrence Paulson
Obviously this proposal would involve a significant incompatibility. It may not even be very relevant any more, as this sort of instantiation is rather out of fashion. But it is worth a discussion. Larry Begin forwarded message: I would propose to simplify the parsing rules to work like this:

Re: [isabelle-dev] Fwd: [isabelle] Problem with frule_tac substitution

2011-02-09 Thread Lawrence Paulson
2011, at 17:19, Brian Huffman wrote: On Tue, Feb 8, 2011 at 9:01 AM, Lawrence Paulson l...@cam.ac.uk wrote: Historically, the point is that index numbers were regarded as very important in variable names, while identifiers ending with digits were not seen as important. And there are other ways

Re: [isabelle-dev] Fwd: [isabelle] Problem with frule_tac substitution

2011-02-09 Thread Lawrence Paulson
This indeed is probably one of the chief reasons for the existing arrangements. Larry On 9 Feb 2011, at 08:36, Alexander Krauss wrote: An incompatibility that will not be reported by tests is that intermediate goal states, where nonzero indexnames are quite frequent, will look significantly

[isabelle-dev] Mercurial failing as always

2011-03-01 Thread Lawrence Paulson
Does anybody know what to do here? Larry ~/isabelle/Repos: hg push pushing to http://isabelle.in.tum.de/repos/isabelle searching for changes http authorization required realm: Mercurial repositories user: ___ isabelle-dev mailing list

[isabelle-dev] Fwd: [isabelle] Exception in conv.ML

2011-05-27 Thread Lawrence Paulson
It looks like this exception is raised when gconv_rule cv i th is called and the specified subgoal does not exist. The function gconv_rule is called in only four places in Pure: ./Isar/element.ML: (Conv.gconv_rule Drule.beta_eta_conversion 1 r) ./raw_simplifier.ML: then Conv.gconv_rule

Re: [isabelle-dev] Fwd: [isabelle] Exception in conv.ML

2011-05-27 Thread Lawrence Paulson
Thank you for looking there! This is the most plausible culprit. But it is strange that this problem has arisen before. A possible fix is to replace the last line of the function timing_depth_tac in that file as follows: handle PROVE = Seq.empty | THM _ = Seq.empty; Andreas, do you want to

Re: [isabelle-dev] New Testing Infrastructure -- status report

2011-05-30 Thread Lawrence Paulson
Awesome! It looks positively industrial in scale. Larry On 30 May 2011, at 08:54, Alexander Krauss wrote: Hi all, In the past weeks, there has been some progress with our new testing infrastructure, which I would like to summarize here. Please give feedback, ask questions, and discuss.

Re: [isabelle-dev] Latex issue (Fwd: isabelle dist build failed)

2011-05-30 Thread Lawrence Paulson
My impression from fooling around a little is that this is a bug that has been around for a year and a half. The comment seems to suggest that | no longer works as an index item (even when protected using), so we have to give up index entries for the symbols | and |-|. I wonder whether there is

Re: [isabelle-dev] Latex issue (Fwd: isabelle dist build failed)

2011-05-30 Thread Lawrence Paulson
It seems it can be fixed by (a) using ! rather than | as the sort key (the sorting of special symbols is arbitrary anyway) (b) using \char124 to denote the | symbol I would expect to see this problem in any index entry involving the | symbol. Larry On 30 May 2011, at 14:58, Lawrence Paulson

Re: [isabelle-dev] Latex issue (Fwd: isabelle dist build failed)

2011-05-30 Thread Lawrence Paulson
There were broken index entries in most of the old documentation. For some reason, the | symbol didn't cause a problem in the tutorial. One index entry here was fixed to use ?? (as opposed to !) as the sort key. Larry On 30 May 2011, at 15:28, Lawrence Paulson wrote: It seems it can be fixed

Re: [isabelle-dev] Feedback from a Isabelle tutorial

2011-06-25 Thread Lawrence Paulson
Is it possible to restrict command completion to a select collection of commonly used commands? Or to make it the user-configurable? Larry On 24 Jun 2011, at 21:01, Alexander Krauss wrote: Suggestion: Simply kill completion of commands (not symbols)???

Re: [isabelle-dev] Evaluation of floor and ceiling

2011-07-08 Thread Lawrence Paulson
Is there any real cost to having so many type classes? Larry On 8 Jul 2011, at 02:13, Brian Huffman wrote: The drawback to this design is that it requires yet another type class, of which we have plenty already. ___ isabelle-dev mailing list

[isabelle-dev] Fwd: [isabelle] Odd failure to match local statement with pending goal.

2011-08-02 Thread Lawrence Paulson
We appear to be in danger of overlooking this problem, which could indicate a significant error somewhere. The names of bound variables should not be significant. Does anybody have any idea what could be causing this? Larry Begin forwarded message: From: Lars Noschinski nosch...@in.tum.de

Re: [isabelle-dev] [isabelle] Odd failure to match local statement with pending goal.

2011-08-03 Thread Lawrence Paulson
Many thanks for your analysis. It looks like an interaction involving fix and bound variables. But we need to move the discussion to isabelle-dev@mailbroy.informatik.tu-muenchen.de. Larry On 2 Aug 2011, at 22:55, Brian Huffman wrote: On Tue, Aug 2, 2011 at 2:10 PM, Bertram Felgenhauer

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-11 Thread Lawrence Paulson
I hope that my position on this question is obvious. And if we decide to revert to the former setup, I would be happy to help track down and fix some problems in theories. Larry On 11 Aug 2011, at 13:43, Florian Haftmann wrote: Why (I think) the current state concerning sets is a bad idea: *

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-12 Thread Lawrence Paulson
It's clear that for inductive definitions, relations are frequently more natural than sets. But I wonder whether a less drastic solution could have been found than abandoning sets altogether. (I'm trying to imagine some sort of magic operator to ease the transition between sets with various

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-19 Thread Lawrence Paulson
I am currently working on AFP/Coinductive, which is full of the sort of thing. Larry On 19 Aug 2011, at 00:31, Gerwin Klein wrote: Can't really quantify it, but I'm seeing this all the time from not-so-novice users over here. Mixing sets and predicates (e.g. using intersection on

[isabelle-dev] The type “'a set

2011-08-19 Thread Lawrence Paulson
To avoid duplication of effort, note that I'm currently trying to convert the AFP theories DataRefinementIBP and GraphMarkingIBP. Larry ___ isabelle-dev mailing list isabelle-...@in.tum.de

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-22 Thread Lawrence Paulson
I've come across something strange in the file isabelle/afp/devel/thys/DataRefinementIBP/Diagram.thy and was wondering if anybody could think of an explanation. A proof works only if I insert before it the following: instance set :: (type) complete_boolean_algebra proof qed (auto simp add:

Re: [isabelle-dev] [isabelle] (Re-)introducing set as a type constructor rather than as mere abbreviation[SEC=UNCLASSIFIED]

2011-08-23 Thread Lawrence Paulson
I'm starting to have doubts about this entire procedure. I thought the plan was to get these theories (particularly in the AFP) into a state where they no longer dependent on confusing sets with predicates so that they would work with either version of Isabelle. I'm not sure that's possible. I

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-24 Thread Lawrence Paulson
I've just been trying to get the proofs working, not to simplify them or even to understand them. Incidentally, let there be no illusions about people accidentally stumbling into a mixture of sets and predicates. Some of these theories were clearly designed from the ground upwards on the

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-26 Thread Lawrence Paulson
indeed yes I'm the person who decided that this primitive should introduce a type as a copy of an existing non-empty set. I have always preferred sets to predicates and the examples I have looked at lately have only strengthened my view. Not to mention numerous occasions when people have

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-26 Thread Lawrence Paulson
I shall take a look at this one. If anybody else is working on it, please let me know as soon as possible. Larry On 25 Aug 2011, at 21:45, Florian Haftmann wrote: HOL-Probability FAILED ___ isabelle-dev mailing list isabelle-...@in.tum.de

[isabelle-dev] inductive_set: Bad monotonicity theorem

2011-08-26 Thread Lawrence Paulson
I am trying to process the following declaration in Probability/Sigma_Algebra: inductive_set smallest_ccdi_sets :: ('a, 'b) algebra_scheme \Rightarrow 'a set set . . . monos Pow_mono I get the following error message (for the version with set types): *** Bad monotonicity theorem: ***

Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

2011-08-26 Thread Lawrence Paulson
I took a look at some of these. HOL-Library fails in your own Cset.thy, where presumably you know what you are doing (particularly as this theory involves execution I should stay away from it). Similarly I'm not sure I'm the right person to fix HOL-Nominal or HOL-MicroJava. PG is very fragile

Re: [isabelle-dev] Release reminder

2011-09-02 Thread Lawrence Paulson
I've got it. No problems with Isabelle. Larry On 2 Sep 2011, at 16:20, Jasmin Blanchette wrote: Am 02.09.2011 um 17:12 schrieb Makarius: Did anybody get Mac OS Lion already? Not that I'm aware of. Jasmin ___ isabelle-dev mailing list

Re: [isabelle-dev] NEWS - Redundant lemmas

2011-09-22 Thread Lawrence Paulson
I think this is a good idea. Larry On 22 Sep 2011, at 03:08, Brian Huffman wrote: Perhaps we should start using a standardized process for phasing out legacy theorems, like moving them into a separate theory file Legacy.thy that would not be imported by default, and would be cleared out

[isabelle-dev] Fwd: Needed ghostscript package to build PDF in Cygwin

2011-10-05 Thread Lawrence Paulson
A suggestion and some compliments... Larry Begin forwarded message: From: James Frank s...@gmx.com Subject: Needed ghostscript package to build PDF in Cygwin Date: 5 October 2011 15:54:30 GMT+01:00 To: l...@cam.ac.uk Dear Dr. Paulson, The problem I had with building the Isabelle PDF

Re: [isabelle-dev] Merge-Sort Implementation

2011-10-27 Thread Lawrence Paulson
If my memory is correct, quicksort was the clear winner in the performance tests that I undertook for my book. Larry On 27 Oct 2011, at 13:50, Florian Haftmann wrote: interesting to read that comment. The exiting quicksort implementation in HOL is indeed taken from Isabelle's ML library.

Re: [isabelle-dev] NEWS

2012-01-04 Thread Lawrence Paulson
I did quite a few of these conversions. Generally the changes were straightforward, EXCEPT for theories that explicitly treated sets as predicates. In the former case, the strategy is to rigorously confine yourself to set primitives, but in the latter case, you may find yourself with a

Re: [isabelle-dev] NEWS

2012-01-04 Thread Lawrence Paulson
It seems to me that we owe users an announcement on the mailing list so that they know that this is coming. They can then download a development snapshot to see what it will look like. Larry On 4 Jan 2012, at 21:10, Makarius wrote: On Wed, 4 Jan 2012, Lawrence Paulson wrote: I did quite

Re: [isabelle-dev] inductive_set vs. 'a set

2012-01-09 Thread Lawrence Paulson
I got this message several times when converting theories. There is a workaround, but nevertheless, I think this is a bug. Larry On 9 Jan 2012, at 13:31, Makarius wrote: There is another drop-out concerning 'a set (in Isabelle/05a82dd869ed): inductive_set well_formed_gterm' :: ('f

[isabelle-dev] syntax errors cause hanging

2012-03-06 Thread Lawrence Paulson
I remember when you could build a logic by typing “isabelle make, and if an error occurred somewhere, it would terminate with an error message. I am trying to make textual changes now, and I find that “isabelle make simply hangs. if I terminate it, I discover where I have introduced some sort

Re: [isabelle-dev] syntax errors cause hanging

2012-03-06 Thread Lawrence Paulson
I think I've worked this out. Something was looping in a parallel thread probably. Larry On 6 Mar 2012, at 12:00, Lawrence Paulson wrote: I remember when you could build a logic by typing “isabelle make, and if an error occurred somewhere, it would terminate with an error message. I am

Re: [isabelle-dev] MacHg 1.0 soon

2012-03-07 Thread Lawrence Paulson
I have tried both,And they are better at different things. I still find MacMercurial more intuitive for the basics. Larry On 7 Mar 2012, at 14:34, Makarius wrote: On Wed, 7 Mar 2012, Lawrence Paulson wrote: There is also MacMercurial, which gives access to all the basic commands That's

Re: [isabelle-dev] ZF/upair.thy failing

2012-03-16 Thread Lawrence Paulson
Also in ZF/Inductive_ZF.thy... Larry On 16 Mar 2012, at 10:35, Lawrence Paulson wrote: I have a problem with the current version (9ff441f295c2). See attachment. This prevents the use of PG within ZF. However, it builds at the command line. What is supposed to be here? Screen Shot 2012-03

Re: [isabelle-dev] Difference between induct and induct_tac

2012-03-27 Thread Lawrence Paulson
I have redirected your request to isabelle-us...@cl.cam.ac.uk. That is the appropriate mailing list for users' questions. The developers' mailing list is for use by the Isabelle developers. Larry Paulson On 27 Mar 2012, at 09:14, charmi panchal wrote: Hello, I am a beginner of Isabelle and

Re: [isabelle-dev] Towards the next release

2012-04-12 Thread Lawrence Paulson
There is something I'd like to mention, not a big deal, but worth considering. I've been doing some proofs lately after a long gap, making myself a combination of a novice and expert. And I've got confused by things that would probably confuse true novices even more. Here are two

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

  1   2   3   4   5   >