[isabelle-dev] NEWS: List comprehension

2007-08-20 Thread Tobias Nipkow
* HOL finally supports full list comprehensions as in Haskell, except that . is used instead of |. As a by-product, pattern-matching abstractions % pat1 = e1 | ... are supported as well.

[isabelle-dev] NEWS: List comprehension

2007-08-20 Thread Tobias Nipkow
I assume, `% pat1 = e1 | pat2 = e2' is equivalent to % a0 . case a0 of pat1 = e1 | pat2 = e2 with `a0' being a fresh identifier. Yes. How does a multiple-arguments (automatically curried) lambda look like? It doesn't exist. At least not in Isabelle. BTW, list comprehension is

[isabelle-dev] [Fwd: status changed (AFP)]

2007-08-03 Thread Tobias Nipkow
Somebody broke Flyspeck. Pls fix. Tobias Original-Nachricht Betreff: status changed (AFP) Datum: Fri, 3 Aug 2007 09:13:34 +0200 (CEST) Von: isatest at informatik.tu-muenchen.de (Account Isatest) An: undisclosed-recipients: ; The status of the following AFP entries changed:

[isabelle-dev] quickcheck on type real

2007-09-02 Thread Tobias Nipkow
*** DIVZERO *** At command quickcheck. I also ran into this one (and notified Stefan). lemma inverse (a::real) = (1 / a) Counterexample found: a = -1 I love it, a false counterexample to a false thm ;-) Thanks! Tobias

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

2007-09-16 Thread Tobias Nipkow
That's fine with me. I would not insist on breaking the current careful separation of the constructive part of HOL. Tobias Lawrence Paulson schrieb: So, metis becomes available just before List.thy? This might be a good compromise. Larry On 14 Sep 2007, at 15:26, Florian Haftmann

[isabelle-dev] ML goes mainstream!

2007-10-24 Thread Tobias Nipkow
Ja, F# wird zum offiziellen MS Produkt. Tobias Steven Obua wrote: http://www.artima.com/forums/flat.jsp?forum=278thread=217150 ___ Isabelle-dev mailing list Isabelle-dev at mailbroy.informatik.tu-muenchen.de

[isabelle-dev] prems

2007-11-21 Thread Tobias Nipkow
Not to mention foo_tac ;-) The English language has the term blacklist. Isar has a redlist. Tobias Stefan Berghofer wrote: Clemens Ballarin wrote: The new PG seems to colour the word prems red wherever it occurs. I think this is overdoing it a bit: prems is just a name and doesn't

[isabelle-dev] [Fwd: Re: [isabelle] Codegen from Hoare logics?]

2007-11-26 Thread Tobias Nipkow
Original Message Subject: Re: [isabelle] Codegen from Hoare logics? Date: Mon, 26 Nov 2007 03:02:42 -0600 From: Luke Wagner and...@gmail.com To: Tobias Nipkow nipkow at in.tum.de References: 79f699ca0711251218q37dc8956m66264fc37dae3d54 at mail.gmail.com 474A8662.4090205

[isabelle-dev] finite_intvl_succ

2008-01-28 Thread Tobias Nipkow
Intentionally. The main purpose of that class is to provide the list interval notation [_.._]. For nat there is already [_.._] with lots of lemmas. Having both intervals on nat will require lots of bridging lemmas. Tobias Amine Chaieb wrote: This is a nice generalization for intervals, but on

[isabelle-dev] [isabelle] Simplification in locales

2008-06-27 Thread Tobias Nipkow
I agree that the locale abstraction is being violated in this case. Even if locale-defined constants are implemented as abbreviations, this should not be apparent to the user. Here's my idea for a possible remedy: Within the locale, the simplifier should use a congruence rule that

[isabelle-dev] HOL vs. HOL-Complex

2008-07-02 Thread Tobias Nipkow
Got it. In which case I agree with the split. Tobias Brian Huffman wrote: Quoting Tobias Nipkow nipkow at in.tum.de: I don't use Complex, but I strikes me as odd that some of our complex theories should be in the HOL image and other should not be. What is the rational for splitting

[isabelle-dev] Desperately Seeking Mathematical Truth

2008-07-20 Thread Tobias Nipkow
Via http://www.nongnu.org/isarmathlib/ I found this link http://www.ams.org/notices/200807/tx080700773p.pdf Indeed. Tobias

[isabelle-dev] Some experiences with MicroJava, Jinja, JinjaThreads

2008-07-28 Thread Tobias Nipkow
The three obfuscating issues were: A) Archaic, hardly readable and fragile proof techniques: * unfolding definitions of predicates over logical formulae instead of proper intro/elim-rules This is mere dogma. It is perfectly standard to reason about logical concepts by unfolding their

[isabelle-dev] [Fwd: status (AFP)]

2008-09-01 Thread Tobias Nipkow
Integration has been failing for a couple of days now. Anybody feel responsible for fixing it? Most likely something to do with the reals... Tobias Original Message Subject: status (AFP) Date: Mon, 1 Sep 2008 12:07:05 +0200 (CEST) From:

[isabelle-dev] [Fwd: [Fwd: status (AFP)]]

2008-09-01 Thread Tobias Nipkow
Oops, that was my own fault - sorry! Tobias Original Message Subject: [isabelle-dev] [Fwd: status (AFP)] Date: Mon, 01 Sep 2008 12:12:00 +0200 From: Tobias Nipkow nip...@in.tum.de To: DEV Isabelle isabelle-dev at in.tum.de Integration has been failing for a couple of days now

[isabelle-dev] [Fwd: SourceForge.net CVS Migration and Downtime Announcement]

2008-09-30 Thread Tobias Nipkow
I can live with cvs. Tobias Gerwin Klein schrieb: Looks like the AFP cvs will be down for most of the day today. While we're at it: what is the general feeling towards migrating the AFP to svn? (Mercurial would be nicer, but sourceforge offers only CVS and SVN). pro: more flexible,

[isabelle-dev] NEWS

2008-09-01 Thread Tobias Nipkow
* ATP selection (E/Vampire/Spass) is now via PG's settings menu. Tobias

[isabelle-dev] An ARBITRARY question

2008-10-02 Thread Tobias Nipkow
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 schrieb: Some years ago two further constants were introduces into HOL.thy: undefined and default. The idea then was to

[isabelle-dev] [Fwd: Fwd: E Equational Theorem Prover 1.0 Temi released]

2008-10-24 Thread Tobias Nipkow
In case anybody feels like trying the latest Version of E (via sledgehammer). Tobias Original Message From: Stephan Schulz schulz at informatik.tu-muenchen.de Date: 23 October 2008 00:41:54 BST To: undisclosed-recipients: ; Subject: E Equational Theorem Prover 1.0 Temi

[isabelle-dev] NEWS

2008-11-19 Thread Tobias Nipkow
* HOL/Finite_Set: added a new fold combinator of type ('a = 'b = 'b) = 'b = 'a set = 'b Occasionally this is more convenient than the old fold combinator which is now defined in terms of the new one and renamed to fold_image. Tobias

[isabelle-dev] Numeral simplification: neg and iszero

2008-12-03 Thread Tobias Nipkow
They have been on my get-rid-of list for some time, but when I initially tried, I noticed they were needed for doing arithmetic. Now that somebody (Florian?) added less_int_code, it may indeed be a simple job. Go for it! Tobias Brian Huffman schrieb: Is there any good reason why the constants

[isabelle-dev] floats

2008-12-05 Thread Tobias Nipkow
* The real numbers now offer decimal input syntax: 12.34 is translated into 1234/10^4. This translation is not reversed upon output. If somebody wants to develop this further, they should feel free to do so. Tobias

[isabelle-dev] Polynomial theory

2009-01-11 Thread Tobias Nipkow
The theory is certainly welcome. Ideally both concrete and abstract polynomials should be in the same place and should reference each other, to facilitate choice between the theories. What is the main advantage of abstract polynomials? That = is what you want it to be? And the main drawback?

[isabelle-dev] typrep?

2009-01-21 Thread Tobias Nipkow
Now that I'm beginning to understand what typerep is, I most certainly agree that it is too specialized to force it on everybody. Tobias Alexander Krauss wrote: Brian Huffman wrote: I, for one, am rather alarmed at the hurdles that Amine was forced to overcome to do a simple merge of two

[isabelle-dev] NEWS

2009-01-28 Thread Tobias Nipkow
* HOL/Ring_and_Field and HOL/OrderedGroup: The lemmas group_simps and ring_simps have been replaced by algebra_simps (which can be extended with further lemmas!). At the moment both still exist but the former will disappear at some point.

[isabelle-dev] Factorials and binomial coefficients

2009-01-29 Thread Tobias Nipkow
That theory should be cleaned up and separated into its core and the real-related lemmas that are trivial consequences. The real-related stuff should go where it is used, or better, be removed: eg real (fact n) = 0 is pointless, at least as a simp rule. Such cleaning up is greatly appreciated

[isabelle-dev] setsum/setprod

2009-02-17 Thread Tobias Nipkow
I assume I simply forgot products, or possibly they did not exist when I added the fancy sum syntax. Feel free to make a product copy of the sum syntax. Tobias Lawrence Paulson wrote: We implement a nice syntax for summations indexed over intervals, but nothing comparable products. The code

[isabelle-dev] NEWS

2009-02-21 Thread Tobias Nipkow
* HOL/IntDiv: removed most (all?) lemmas that are instances of class-based generalizations (from Divides and Ring_and_Field). INCOMPATIBILITY. Rename old lemmas as follows: dvd_diff - nat_dvd_diff dvd_zminus_iff - dvd_minus_iff nat_mod_add_left_eq- mod_add_left_eq

[isabelle-dev] Suc 0 necessary?

2009-02-23 Thread Tobias Nipkow
to be a simp rule? - Brian Quoting Tobias Nipkow nipkow at in.tum.de: This translation is not in there by default because it is bound to confuse novices and sometimes even experts: they see 1 in their proof state and 1 in their theorem and wonder why Isabelle refuses to apply the theorem

[isabelle-dev] Suc 0 necessary?

2009-02-23 Thread Tobias Nipkow
This is exactly the point: recursive functions defined by pattern matching expect Suc. They tend to dominate the scene in CS-oriented applications. Hence Suc 0 is made the default. However, for math applications this tends to be inconvenient, esp in connection with abstract algebra

[isabelle-dev] Suc 0 necessary?

2009-02-23 Thread Tobias Nipkow
to #n would have been very helpful. The difference between #n and n would have to be clearly documented, of course. Larry On 23 Feb 2009, at 15:42, Tobias Nipkow wrote: This is exactly the point: recursive functions defined by pattern matching expect Suc. They tend to dominate

[isabelle-dev] Nitpick counterexample generator now available

2009-02-27 Thread Tobias Nipkow
lemma k dvd n == k dvd (n+1::nat) nitpick But even with SAT4J I get Nitpicking~ Nitpick found no counterexample. Of course this is not ideal nitpick country, but still... Tobias Jasmin Christian Blanchette schrieb: I am pleased to announce the first release of Nitpick, a Kodkod (Alloy)

[isabelle-dev] A better policy for the typerep class

2009-02-28 Thread Tobias Nipkow
If this is so, then maybe it is a good idea to move ATP_Linkup so that it is imported by Plain? I know that some library theories import only Plain and Presburger, for example; if ATP_Linkup were included with Plain, it might avoid wasting resources in those cases. I've discussed that

[isabelle-dev] [Fwd: Isabelle, refute and nitpick]

2009-03-03 Thread Tobias Nipkow
Not sure, possibly Leo II. No other ITP is in the competition. Tobias Amine Chaieb schrieb: Second best??? But who is roaring ahead? Amine. Tobias Nipkow wrote: :-) Tobias Original-Nachricht Betreff: Isabelle, refute and nitpick Datum: Tue, 3 Mar 2009 02:32:44

[isabelle-dev] [Fwd: Isabelle, refute and nitpick]

2009-03-03 Thread Tobias Nipkow
sure with Jasmin's and Sascha's new ideas and approaches second best won't last very long :) Amine. Tobias Nipkow wrote: Not sure, possibly Leo II. No other ITP is in the competition. Tobias Amine Chaieb schrieb: Second best??? But who is roaring ahead? Amine. Tobias

[isabelle-dev] Repository OK?

2009-03-04 Thread Tobias Nipkow
Fixed, sorry. Tobias Amine Chaieb wrote: Hi, I updated and get the following error. What is Option? Amine. bash-3.2$ hg fetch Password: pulling from ssh://chaieb at atbroy100.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle searching for changes adding

[isabelle-dev] What's in Main

2009-03-10 Thread Tobias Nipkow
I have attached a document that summarizes the main constants and their syntax. It is intentionally restricted to (about) 10 pages to make it easy to browse and get a quick overview. For details one still has to read the theories. If you have any suggestions or issues, please let me know. One

[isabelle-dev] What's in Main

2009-03-10 Thread Tobias Nipkow
Please ignore the attachment to my previous email. I have already sent the correct one but it is waiting for the list moderator approval because it exceeds 100kb. Tobias

[isabelle-dev] antiquotation @{thm[locale=...

2009-05-17 Thread Tobias Nipkow
What happened to this option? I cannot run one of my draft papers anymore. How do I have to write it these days? I couldn't find anything in NEWS. Tobias

[isabelle-dev] NEWS

2009-07-22 Thread Tobias Nipkow
* GCD now has functions Gcd/GCD and Lcm/LCM for the gcd and lcm of finite and infinite sets. It is shown that they form a complete lattice.

[isabelle-dev] NEWS

2009-07-29 Thread Tobias Nipkow
* New proof method sos (sum of squares) for nonlinear real arithmetic (originally due to John Harison). It requires Library/Sum_Of_Squares. It is not a complete decision procedure but works well in practice on quantifier-free real arithmetic with +, -, *, ^, =, = and , i.e. boolean combinations of

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

2009-11-11 Thread Tobias Nipkow
Hi Brian, When I defined HOL and put in ext, eq_reflection did not exist and hence I could not derive ext. Now we can. But this relies on eq_reflection, which is admissible, but I only added it to make the simplifier work better and don't want to rely on it if it can be helped. But thanks for

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

2009-11-12 Thread Tobias Nipkow
This is more subtle. I copied the axioms from Mike Gordon's TR 68. Neither of us seems to have noticed the redundancy. If you look at HOL done right by John Harrison, he does not seem to comment on the redundancy either but sets the system up a bit differently: he includes iff (IMP_ANTISYM_RULE)

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

2009-11-12 Thread Tobias Nipkow
So eq_reflection is an axiom, but we all agree to pretend it's not an axiom? This is just weird. I prefer not to rely on it unless we have to in case it disappears again. Although I notice it is used quite a lot. While we're discussing it: I wonder sometimes what the role of == was in

[isabelle-dev] Pow

2009-12-14 Thread Tobias Nipkow
I used the release, that's the reason. There is indeed a problem now. See the next email by Robert. Thanks Tobias Lawrence Paulson wrote: 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

[isabelle-dev] Sledgehammer renaming

2010-01-13 Thread Tobias Nipkow
PS Since I suggested to Jasmin to work on s/h, I obviously welcome his initiative. It is important that we have one person who has the time and the responsibility, just like other people feel responsible for fun etc. Tobias Jasmin Blanchette wrote: Hi Makarius, Am 13.01.2010 um 17:57 schrieb

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

2010-05-10 Thread Tobias Nipkow
That sounds very worthwhile, thanks! Tobias Brian Huffman wrote: Hello all, I recently finished a formalization of real numbers that uses Cauchy sequences. I thought it might be good to replace the current formalization (which uses Dedekind cuts) with this new one in time for the upcoming

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

2010-08-03 Thread Tobias Nipkow
There is no requirement or guarantee that theorems in general are in any kind of normal form. Tobias Thomas Sewell schrieb: Hello Isabelle developers. I was about to have another attempt at speeding up a tactic we implemented for L4.verified using net-matching. In reading Pure/net.ML I

[isabelle-dev] NEWS: expand_fun_eq - ext_iff, expand_set_eq - set_ext_iff

2010-09-07 Thread Tobias Nipkow
___ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: expand_fun_eq - ext_iff, expand_set_eq - set_ext_iff

2010-09-07 Thread Tobias Nipkow
I wanted to emphasize the mathematical concept, not the operational view. And indeed, it is shorter. For functional objects the ext_iff convention fits perfectly. For example, for polynomials we already have poly_ext in one direction. I have to admit, though, that for pairs it would be a bit

[isabelle-dev] is_concealed

2010-09-09 Thread Tobias Nipkow
Lars noticed an anomaly and Gerwin tracked it down: Command find_consts searches only for `visible' constants. Those defined by primrec and fun are visible, but those defined by inductive(_set) are concealed. It seems that the latter should be visible, too, right? If so, can somebody close to

[isabelle-dev] t_eqI and t_eq_iff

2010-09-13 Thread Tobias Nipkow
I have now changed the lemma names to the above schema we agreed las week for t=fun and t=(multi)set. You are invited to make the same change for other types. Tobias ___ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de

Re: [isabelle-dev] NEWS

2010-10-29 Thread Tobias Nipkow
Unless I have a lapse of memory, the timeout specifications for s/h and Nitpick are also in seconds, possibly with an s appended. As a user I am glad about that, because I do not think in ms and would not like to write 3 instead of 30. Tobias Makarius schrieb: On Fri, 29 Oct 2010, Lukas

Re: [isabelle-dev] NEWS

2010-10-29 Thread Tobias Nipkow
: On Fri, 29 Oct 2010, Tobias Nipkow wrote: Unless I have a lapse of memory, the timeout specifications for s/h and Nitpick are also in seconds, possibly with an s appended. As a user I am glad about that, because I do not think in ms and would not like to write 3 instead of 30. I have

Re: [isabelle-dev] NEWS

2010-10-29 Thread Tobias Nipkow
scheme for times (besides the existing bool, int and string schemes)? It seems that this could and should be provided be provided by the system to have a uniform interface and prevent further confusion. Sascha Tobias Nipkow wrote: As I said, I was entirely unconfused that it is in seconds

Re: [isabelle-dev] Datatype alt_names

2010-11-03 Thread Tobias Nipkow
The 'typedef' command supports a similar option for alternative names; I am sure that it was originally created for use with non-alphanumeric type names. One could also ask whether the existence of this feature for typedef is still justified, when all types have regular names now. Do you

Re: [isabelle-dev] find_theorems raises UnequalLengths exception

2010-11-19 Thread Tobias Nipkow
Thanks. 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

Re: [isabelle-dev] find_theorems raises UnequalLengths exception

2010-11-19 Thread Tobias Nipkow
The idea was that that code would be incomplete but not incorrect outside the HO pattern term language. But indeed, th actual code has not been verified... Tobias Makarius schrieb: On Fri, 19 Nov 2010, Tobias Nipkow wrote: Just for the record: the code eta-expands terms on the fly

Re: [isabelle-dev] Coral and Sledgehammer

2010-11-22 Thread Tobias Nipkow
I rarely feel the need for answer literals, i.e. to let provers synthesize terms for me. And I doubt it would often work (although in that paper they do benefit from it). Given that Sledgehammer is not a trivial piece of engineering, I would not want to burden it with more proactive functionality

[isabelle-dev] HOLCF problem

2010-11-28 Thread Tobias Nipkow
Brian's latest patch remove HOLCF from build script, since it no longer works has an unfortunate effect: the isabelle script now terminates immediately with Bad Isabelle component: /Users/nipkow/isabelle/src/HOLCF Which is annoying, given that I do not want to use HOLCF at all. Can I do something

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

2010-12-01 Thread Tobias Nipkow
Is the following behaviour really a good idea and useful? inductive P :: nat = bool where P(suc n) is accepted but defines P :: 'a itself = nat = bool It does kind of warn me by saying ### Additional type variable(s) in specification of P: 'a but if you miss that warning, you will be very

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

2010-12-02 Thread Tobias Nipkow
that unsuspecting users should be subjected to it. Tobias Brian Huffman schrieb: On Wed, Dec 1, 2010 at 11:50 PM, Tobias Nipkow nip...@in.tum.de wrote: Is the following behaviour really a good idea and useful? inductive P :: nat = bool where P(suc n) is accepted but defines P :: 'a itself

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

2010-12-02 Thread Tobias Nipkow
it on the top level, or have a vesion of the underlying function that does not do the parametrisation in the first place? Tobias Makarius schrieb: On Thu, 2 Dec 2010, Tobias Nipkow wrote: Florian explained to me that for the function package this new behaviour is an improvement, but that does

Re: [isabelle-dev] sporadic failures of AFP tests

2010-12-13 Thread Tobias Nipkow
Are you referring to *** Failed to prepare dependency graph This is the response if some file was not created. Which indicates that something might be amiss on the system level. This error first occured a few months ago. After a week or two it went away. Now it is back. I don't believe that the

Re: [isabelle-dev] Isabelle release

2011-01-07 Thread Tobias Nipkow
are involved... or the effect on the palate of annually increasing Scala overtones; it shall be grand! On a more serious note, +1 for calling it Isabelle 2011. Rafal Kolanski. On 07/01/11 20:00, Michael Norrish wrote: On 7/01/11 7:53 PM, Tobias Nipkow wrote: I don't see any good reason

Re: [isabelle-dev] Sort Annotation vs. Class Context for Lemmas

2011-01-21 Thread Tobias Nipkow
One issue can be that if some sort involves multiple type classes, the corresponding class may not have been defined. That is the one advantage of sorts: you can create conjunctions/intersection of type classes on the fly. Tobias Tjark Weber schrieb: Hi, I noticed that numerous lemmas in HOL

[isabelle-dev] [Fwd: doc test failed]

2011-02-06 Thread Tobias Nipkow
Seit Wochen wenn nicht Monaten bekomme ich alle paar Tage diese Fehlermeldung: Running ZF-IsarRef ... Unknown logic ZF -- no heap file found in: /home/isatest/isabelle-at-poly/heaps/polyml-5.2_x86-linux /mnt/home/isatest/isadist/Isabelle_06-Feb-2011/heaps/polyml-5.2_x86-linux ZF-IsarRef

Re: [isabelle-dev] [Fwd: doc test failed]

2011-02-06 Thread Tobias Nipkow
Yes, the missing ZF image is to be the problem. For some reason that has changed, as Slawomir Kolodynski also noticed. So we should either build ZF again or stop that test. Tobias Alexander Krauss schrieb: (please keep postings to isabelle-dev in English) Tobias Nipkow wrote: Seit Wochen

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

2011-02-08 Thread Tobias Nipkow
I don't mind one way or the other, but also wonder if it is worth it - I will certainly not rush in to change it. Tobias Lawrence Paulson schrieb: Obviously this proposal would involve a significant incompatibility. It may not even be very relevant any more, as this sort of instantiation is

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

2011-02-08 Thread Tobias Nipkow
Having to instantiate an indexed ?-variable can require a bit of experimentation if you don't remember the exact syntax. I am all for an improvement here, and as Gerwin pointed out, one of our flagship projects is using apply's heavily, where it probably comes up more frequently than otherwise.

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

2011-02-09 Thread Tobias Nipkow
? Tobias Makarius schrieb: On Wed, 9 Feb 2011, Tobias Nipkow wrote: It is interesting that local scopes within structured proofs generate theorems with nonzero indices, but of course that is a separate matter. Yes, that is a new aspect that was introduced around 1998/1999. I would be more

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

2011-02-09 Thread Tobias Nipkow
2011, Tobias Nipkow wrote: If your analogy with lambda calculus is correct, than there are situations when one must rename something exported from a proof block. That I do not understand. Take this example: lemma True proof- { fix n::nat have n=n by auto } produces ?n2 = ?n2. I do not see

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

2011-02-09 Thread Tobias Nipkow
those instantiations break. But if the indices are normalized, then only those almost never cases break. Tobias Makarius schrieb: On Wed, 9 Feb 2011, Tobias Nipkow wrote: I can see the technical reason for having to rename sometimes (almost never, as you write), but disagree with renaming

Re: [isabelle-dev] [isabelle] Congruence rules for the code preprocessor

2011-05-29 Thread Tobias Nipkow
Does the current attribute mechanism support selective attributes such as [code_inline cong], maybe along the lines of [simp del]? If it does, I assume it would be easy to add that information in the place that Florian pointed to? Tobias Am 28/05/2011 14:45, schrieb Florian Haftmann: Hi

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

2011-06-26 Thread Tobias Nipkow
Command completion needs to be context aware to work well. Otherwise it can indeed become a distraction. Tobias Am 24/06/2011 22:01, schrieb Alexander Krauss: Hi all, Now that this topic is already active, here is more: In a small course here at TUM

Re: [isabelle-dev] Presburger proof term

2011-06-27 Thread Tobias Nipkow
All of the lemmas involved are either arihmetic or logical inference rules and make sense. Presburger is a generic and complex decision procedure. I am not surprised and would not want to optimize presburger to use fewer lemmas. Tobias Am 28/06/2011 00:08, schrieb Jasmin Blanchette: Hi all,

[isabelle-dev] jedit

2011-06-29 Thread Tobias Nipkow
I just had the situation were I opened a thy file and it simply stayed pink. Even after I closed all other buffers. Exiting and restarting jedit helped, but maybe there is some other way? A suggestion concerning colour: numbers in magenta are on the loude side and give them more prominence

Re: [isabelle-dev] Type variables without default sort

2011-06-29 Thread Tobias Nipkow
Yes, it is a problem of unintended generality. The question remains: are there known situations where it is intended, or could one restrict the generated type variables in the same way as the explicitly stated ones. Tobias Am 29/06/2011 17:23, schrieb Makarius: On Wed, 29 Jun 2011, Lars

Re: [isabelle-dev] Type variables without default sort

2011-06-29 Thread Tobias Nipkow
Point taken. Although it makes me wonder if the default sort in HOLCF is too specialised. Tobias Am 29/06/2011 18:12, schrieb Brian Huffman: These kinds of situations come up in HOLCF, which declares a default sort other than type. Type variables default to being pointed (class pcpo or

Re: [isabelle-dev] [isabelle] Error: Non-constructor pattern not allowed in sequential mode

2011-07-05 Thread Tobias Nipkow
I agree with Gerwin. Records are datatypes. Hence one should be able to pattern match against them as in FP languages. The record package can arrange for this very easily via rep_datatype. On performance: I recently came across an example of a short ML function with very complicated pattern

Re: [isabelle-dev] [isabelle] Error: Non-constructor pattern not allowed in sequential mode

2011-07-06 Thread Tobias Nipkow
That email talks about recursion through records in datatype definitions. That is not what this thread is about. Here we were talking about pattern matching only. Tobias Am 06/07/2011 11:09, schrieb Makarius: On Tue, 5 Jul 2011, Tobias Nipkow wrote: I agree with Gerwin. Records are datatypes

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

2011-08-11 Thread Tobias Nipkow
The benefits of getting rid of set were smaller than expected but quite a bit of pain was and is inflicted. Sticking with something merely to avoid change is not a strong argument. This time we know what we go back to and the real benefits (and the few losses). Hence I would be in favour. Tobias

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

2011-08-12 Thread Tobias Nipkow
Am 12/08/2011 11:27, schrieb Alexander Krauss: On 08/12/2011 07:51 AM, Tobias Nipkow wrote: The benefits of getting rid of set were smaller than expected but quite a bit of pain was and is inflicted. Do you know of any more pain, apart from what Florian already mentioned? I think he omitted

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

2011-08-12 Thread Tobias Nipkow
Surely we want to maintain both inductive and inductive_set? Tobias Am 12/08/2011 13:01, schrieb 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

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

2011-08-18 Thread Tobias Nipkow
Am 19/08/2011 00:10, schrieb Stefan Berghofer: Tobias Nipkow wrote: Am 12/08/2011 11:27, schrieb Alexander Krauss: On 08/12/2011 07:51 AM, Tobias Nipkow wrote: The benefits of getting rid of set were smaller than expected but quite a bit of pain was and is inflicted. Do you know of any more

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

2011-08-18 Thread Tobias Nipkow
Am 19/08/2011 00:00, schrieb Stefan Berghofer: Alexander Krauss wrote: I want to emphasize that the limitation of the code generator mentioned here not only applies to sets-as-predicates but also to maps-as-functions and other abstract types that are often specified in terms of functions

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

2011-08-26 Thread Tobias Nipkow
I agree. Since predicates are primitive, starting from them is appropriate. Tobias Am 26/08/2011 18:33, schrieb Brian Huffman: Here's one possible approach to the set-axiomatization/typedef issue: As a new primitive, we could have something like a pred_typedef operation that uses

Re: [isabelle-dev] Isabelle Verified Linux kernel

2011-10-04 Thread Tobias Nipkow
Am 05/10/2011 00:23, schrieb David Blubaugh: Has anyone ever developed a verified and validated version of the Linux kernel by utilizing the Isabelle / HOL environment ?? Not that I have heard about it ;-) Does Isabelle support non-determinsitic model checking as well as theorem proving

[isabelle-dev] auto quickcheck and auto solve

2011-10-12 Thread Tobias Nipkow
I find it very objectionable that the new release does no longer support these two auto features in Proof General. They are part of ongoing research in Munich and are appreciated by many users. If you do not know how to make them work with jedit, this is no reason to disable them under Proof

Re: [isabelle-dev] auto quickcheck and auto solve

2011-10-12 Thread Tobias Nipkow
with the release version and it worked fine. (There is a small PG problem that lead one of the two people to think it did not work, but that is irrelevant here). Again, my apologies Tobias Am 12/10/2011 16:32, schrieb Tobias Nipkow: I find it very objectionable that the new release does no longer support

Re: [isabelle-dev] Why do cancellation simprocs call Lin_Arith.simproc

2011-10-29 Thread Tobias Nipkow
One set of simprocs will cancel factors from inequalities, rewriting terms like x * z y * z to either x y or y x, depending on whether it can prove 0 z or z 0. What I don't understand is the method they use to try to prove 0 z or z 0: Instead of recursively calling the full simplifier

Re: [isabelle-dev] Quickcheck_Exhaustive.unknown

2011-11-30 Thread Tobias Nipkow
Am 30/11/2011 12:27, schrieb Makarius: This concerns Isabelle/3d6ee9c7d7ef: Adding a global constant Quickcheck_Exhaustive.unknown with rather generic notation ? to main HOL is a bit dangerous. The name unknown is also a candidate for hide_const (open). I would like to emphasize this.

Re: [isabelle-dev] proposal for new numeral representation

2011-12-05 Thread Tobias Nipkow
Am 25/11/2011 16:56, schrieb Makarius: Broken proof methods sos_cert some uses in Library/Sum_of_Squares.thy BTW the regular sos method with the server communication is broken for some months already. It would be nice if someone could volunteer to recover this nice student project

Re: [isabelle-dev] canonical left-fold combinator for lists

2012-01-13 Thread Tobias Nipkow
I agree very strongly. I am not tied to any particular argument order, but there should only be 2, not 3 folds. And there should be no claims of canonicity. If anything, the canonical fold operator (with some sensible argument order) is foldr f c which replaces :: by f and [] by c. And to avoid

Re: [isabelle-dev] canonical left-fold combinator for lists

2012-01-14 Thread Tobias Nipkow
Am 13/01/2012 21:13, schrieb Florian Haftmann: Hi all, Here is what I suggest: If there is a concensus that the argument order of List.fold is more useful than the existing foldl, then we should simply *replace* foldl with the new fold. Otherwise we should get rid of the new List.fold.

Re: [isabelle-dev] Regain AFP sanity

2012-01-18 Thread Tobias Nipkow
Yes, this is a very reasonable test. Tobias Am 18/01/2012 21:55, schrieb Makarius: BTW, this versions merely skips the really slow proofs of same4, same5, same6, but runs the fast one of same3 unconditionally. Superficially this looks like a reasonable test. Or is their significant

[isabelle-dev] *** exception Empty raised (line 331 of library.ML)

2012-02-09 Thread Tobias Nipkow
instantiation list :: (order) order begin fun le_list :: ('a::order)list = 'a list = bool where le_list [] [] = True | le_list (x#xs) (y#ys) = (x = y xs = ys) | le_list _ _ = False *** exception Empty raised (line 331 of library.ML) Of course it should be less_eq instead of le, but still...

Re: [isabelle-dev] canonical left-fold combinator for lists

2012-02-13 Thread Tobias Nipkow
Am 13/02/2012 13:22, schrieb Florian Haftmann: Anyway, personally I have no strong opinion about this, so anybody who wants to get hands on should feel invited to do so. It would have been better to discuss such a change beforehand rather than make it and then say that we are welcome to

[isabelle-dev] Fwd: status (AFP)

2012-03-07 Thread Tobias Nipkow
Since fixing JinjaThreads gets worse as time elapses, pls fix it asap. It has been broken for a number of days now. *** Unknown fact num_AB_s (line 129 of /mnt/nfsbroy/home/isatest/afp/devel/thys/JinjaThreads/Common/BinOp.thy) Tobias Original-Nachricht Betreff: status (AFP)

[isabelle-dev] Fwd: status (AFP)

2012-03-11 Thread Tobias Nipkow
One error in JinjaThreads was fixed, here is the next one: *** Unknown fact list_all2_update_cong2 (line 467 of /mnt/nfsbroy/home/isatest/afp/devel/thys/JinjaThreads/BV/BVSpecTypeSafe.thy) *** At command apply (line 467 of

  1   2   3   4   >