[isabelle-dev] fconv_rule

2007-07-03 Thread Lawrence Paulson
It was called that in Cambridge LCF in 1983. %Forward proof rule for conversions: A - where fconv A is A = B B % let FCONV_RULE fconv = set_fail_prefix `FCONV_RULE` (\th. MP (CONJUNCT1 (IFF_CONJ (fconv (concl th th);; Larry On 3 Jul 2007, at 11:14,

[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] sledgehammer issues

2007-09-07 Thread Lawrence Paulson
Proof reconstruction should be working again. If you d/l the new Vampire, it too supports proof reconstruction, but Vampire proofs sometimes contain strange steps, when you'll only get an apply-proof. Larry On 6 Sep 2007, at 16:08, Lawrence Paulson wrote: I have just committed a new

[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] binary arithmetic optimization

2008-02-12 Thread Lawrence Paulson
Certainly an interesting idea. HOL4 also uses separate constants. Thanks for trying this out! I don't know who is going to fix code generation though... Larry On 12 Feb 2008, at 02:21, Brian Huffman wrote: Hello all, Recently I tested a variation of HOL/ex/Binary.thy: Instead of using

[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] MetiTarski

2008-08-22 Thread Lawrence Paulson
I wonder whether any of you would like to try out the MetiTarski prover: http://www.cl.cam.ac.uk/~lp15/papers/Arith/ It is probably not ready for a general public release but maybe some of you will find it interesting. Note that I shall be away all next week, so if that doesn't work you

[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] isar-theorem-at-point

2009-02-10 Thread Lawrence Paulson
Some time ago, David Aspinall gave me some code that would display the theorem whose identifier was currently pointed out in Proof General. This command was bound to the key combination C-c C-a C-t. It did not work if the identifier contained a qualified name (.) however. The attached

[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
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 to just have 1, but not if that requires complicated and fragile tricks. Larry On 23 Feb 2009, at 14:47, Brian

[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] [Fwd: Isabelle, refute and nitpick]

2009-03-03 Thread Lawrence Paulson
As Isabelle contains no specifically higher order theorem proving components, this is an amazing result. It would be great to see Isabelle entered at CASC. Are any of us going to CADE this year? Larry On 3 Mar 2009, at 08:22, Tobias Nipkow wrote: :-) Tobias Original-Nachricht

[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] HOL-Bali

2009-08-14 Thread Lawrence Paulson
I am trying to test some minor changes, but I can't get HOL to run. The crazy thing is that I cannot see anything wrong with the syntax of that lemma: lemma triangle_lemma: \lbrakk \And a b c. \lbrakk(a,b)\inr; (a,c)\inr\rbrakk \Longrightarrow b=c; (a,x)\inr*; (a,y)\inr*\rbrakk

[isabelle-dev] x-symbols

2009-09-04 Thread Lawrence Paulson
It is not available in with Aquamacs (http://aquamacs.org/). I will try the other Emacs that you mention. Larry On 3 Sep 2009, at 20:10, David Aspinall wrote: On Emacs 23, there should be Options - Set Default Font... instead. Do you have that option?

[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] NEWS

2009-09-17 Thread Lawrence Paulson
NEWS * New method metisFT: A version of metis that uses full type information in order to avoid failures of proof reconstruction. It hasn't been tested much. Ultimately, the idea is to incorporate it into Metis itself so that it is called automatically if the untyped version raises an

[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] Document preparation failure

2010-02-19 Thread Lawrence Paulson
Something is wrong with the markup in theory Quotient.thy: *** [819]) (./Quotient.tex [820] [821] [822] [823] [824] *** ! Missing $ inserted. *** inserted text *** $ *** l.797 ...vable; which is why we need to use apply_ *** rsp

[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] Fwd: [isabelle] Exception in conv.ML

2011-05-30 Thread Lawrence Paulson
Done now, I hope Larry On 30 May 2011, at 08:10, Andreas Lochbihler wrote: This fix solves the problem with the exception. I tried it with 574613b47583. Can you add it to the repository as I do not have wirte access to that. ___ isabelle-dev

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] [isabelle] power2_sum outside of rings

2011-06-22 Thread Lawrence Paulson
As I recall, the number class is for all types where numerals have a meaning. Of course, it is a constituent of number_ring, to which many numeric types belong, but not the naturals. Larry On 22 Jun 2011, at 19:55, Florian Haftmann wrote: A more drastic solution would be to just get rid of

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

  1   2   3   4   5   >