[isabelle-dev] <-> and <-->

In HOL, the ASCII syntax for \ is defined to be <-> but visually <--> would be more appropriate, closer to --> and would also leave room for an ASCII syntax for \ (namely <->). Any views on such a change? Tobias ___ isabelle-dev mailing list isabelle-..

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

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

Re: [isabelle-dev] ADTs in Scala

May I remind the participants of this thread that this is the Isabelle development mailing list, not a discussion forum on OO techniques in general. Thanks Tobias Am 16/04/2012 16:57, schrieb Holger Gast: >> b) Coding conventions and usual practice (my addition to the above): >> It is customary

Re: [isabelle-dev] Towards the next release

Am 12/04/2012 14:06, schrieb 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 con

Re: [isabelle-dev] [isabelle] Confusing behavior of a paired set comprehension

Am 04/04/2012 11:48, schrieb Tjark Weber: > Adhering to the principle of least astonishment, I suspect an error > message (or at least a warning) would be more helpful. Isabelle's well-tried principle of least astonishment is not to give too many helpful error messages or warnings ;-) Actually, i

[isabelle-dev] New tutorial Programming and Proving in Isabelle/HOL

An updated announcement of a new tutorial in the development version of Isabelle. Comments welcome! [If it does not build on your own machine, your tex distribution probably lacks the eulervm package.] * New tutorial "Programming and Proving in Isabelle/HOL". It completely supercedes "A Tutorial I

Re: [isabelle-dev] New manual Programming and Proving in Isabelle/HOL

Am 03/04/2012 22:51, schrieb Florian Haftmann: >>> I'm indedd quite curious, but unable to build the tex sources. The >>> first error complains about a missing »eulervm.sty«, with lot of >>> further messages following. >> >> You mean you couldn't run the tex sources? Unfortunately I can confirm >

Re: [isabelle-dev] New manual Programming and Proving in Isabelle/HOL

Am 02/04/2012 19:46, schrieb Florian Haftmann: > I'm indedd quite curious, but unable to build the tex sources. The first > error complains about a missing »eulervm.sty«, with lot of further messages > following. You mean you couldn't run the tex sources? Unfortunately I can confirm that. It appe

Re: [isabelle-dev] Isatest

Am 28/03/2012 23:30, schrieb Gerwin Klein: > On 29/03/2012, at 6:11 AM, Makarius wrote: > >> On Wed, 28 Mar 2012, Florian Haftmann wrote: >> >>> Once there has been the idea that everyone having commit access to the >>> Isabelle master repository (POSIX group isabelle at nfsbroy) is also a >>> i

Re: [isabelle-dev] Isatest

Sounds like a sensible idea to avoid test failures to go unnoticed. Tobias Am 28/03/2012 20:45, schrieb Florian Haftmann: > Hi all, > > Once there has been the idea that everyone having commit access to the > Isabelle master repository (POSIX group isabelle at nfsbroy) is also a > isatest subscr

Re: [isabelle-dev] Name for derived quotient_def theorem

Yes, "simps" should not be used for special purpose rules. Tobias Am 28/03/2012 09:22, schrieb Lukas Bulwahn: > Hi Florian, > > > Thank you for your suggestions. We will take them into account. > > On 03/28/2012 07:26 AM, Florian Haftmann wrote: >> http://isabelle.in.tum.de/reports/Isabelle/re

Re: [isabelle-dev] Towards the next release

Thanks for your input, I have added some of your lemmas to List (and will write to you about separately). No, there is no fixed process for adding such contributions. Until it becomes a nuisance ;-) you are welcome to post them here or send them to some active developer. Tobias Am 16/03/2012 10:

Re: [isabelle-dev] Quotient.invariant

Absolutely, thanks. Constants should be hidden if they are internal to some package. Especially with such a universal name as "invariant". Tobias Am 23/03/2012 17:34, schrieb Makarius: > Just a note on the following changeset: > > changeset: 47095:3ea48c19673e > user:kuncar > date:

[isabelle-dev] Fwd: status (AFP)

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 "/mnt/nfsbroy/home/isatest/afp/devel/thys/JinjaThreads/BV/BVSpecTypeS

[isabelle-dev] Fwd: status (AFP)

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)

Re: [isabelle-dev] README.html

I wonder if we should just get rid of them. I looked at a few and much of the information in there is outdated. Useful information could be moved into the pdf document. Tobias Am 17/02/2012 22:10, schrieb Florian Haftmann: > Hi all, > > recently I stumbled again over our famour ancient README fi

Re: [isabelle-dev] Explanation required

It allows to have one simplifier for == and translate the result from == into =. It is a convenience and we could eliminate all occurences of it from proofs if we cared. Tobias Am 17/02/2012 08:11, schrieb Christian Sternagel: > Hi Brian, > > thanks a lot for the pointer! > > What the comment n

Re: [isabelle-dev] Explanation required

Am 17/02/2012 03:46, schrieb Christian Sternagel: > Dear all, > > please forgive my annoying questioning. Could anybody elaborate on the > following comment (to be found in HOL.thy): > > ext: "(!!x::'a. (f x ::'b) = g x) ==> (%x. f x) = (%x. g x)" > -- {*Extensionality is built into the meta-

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

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 welco

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

Am 12/02/2012 11:24, 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 modify

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

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, b

Re: [isabelle-dev] Regain AFP sanity

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 inform

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

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.f

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

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 fur

Re: [isabelle-dev] Regain AFP sanity

This is the wrong way around. The AFP must contain the real thing that can be tweaked with some shell variable to skip certain parts. Not the other way around: the user has to do something special to get the right behaviour. Tobias Am 11/01/2012 15:40, schrieb Makarius: > Dear all, > > we've alr

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

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 s

Re: [isabelle-dev] Quickcheck_Exhaustive.unknown

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

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

> 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 cal

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

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 supp

[isabelle-dev] auto quickcheck and auto solve

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 Genera

Re: [isabelle-dev] Isabelle Verified Linux kernel

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 prov

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

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 predi

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

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 functi

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

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 bi

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

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 s

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

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 m

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

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] [isabelle] Error: Non-constructor pattern not allowed in sequential mode

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.

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

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 mat

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

9/06/2011 19:01, schrieb Brian Huffman: On Wed, Jun 29, 2011 at 9:19 AM, Tobias Nipkow wrote: Point taken. Although it makes me wonder if the default sort in HOLCF is too specialised. Why? What other sort do you think might be suitable as a default sort for HOLCF? Currently, the only purpose of th

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

"pcpo" or "domain") but it is often convenient to be able to infer unpointed types wherever they may occur (class "cpo" or "predomain"). - Brian On Wed, Jun 29, 2011 at 8:56 AM, Tobias Nipkow wrote: Yes, it is a problem of unintended generality. The questi

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

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 Nosch

[isabelle-dev] jedit

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 tha

Re: [isabelle-dev] Presburger proof term

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,

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

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 (http://www4.in.tum.de/lehre/vorlesungen/p

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

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 Andr

Re: [isabelle-dev] FYI: Isabelle at CASC

Just in case you are still wonderig which Hammer Jasmin has in mind: http://www.amazon.co.uk/Ultimate-Hammer-Collection-Disc-Box/dp/B000HN31KQ We are currently preparing a new film release, "The Proof of Dracula", and I expect you can guess which ATP will play the lead. Tobias Am 17/03/2011

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

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 y

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

Feb 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- >>

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

s that what you mean? 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. >>

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

>> 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 interested in the why than the when. Generating unpredictable nam

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

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. To

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

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] [Fwd: doc test failed]

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

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

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 FAIL

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

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 H

Re: [isabelle-dev] Isabelle release

hen large gulps 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

Re: [isabelle-dev] Isabelle release

I don't see any good reason for the skewed naming scheme of 2009-x in 2010 or 2011. We should use the year that the release was made in, period. That avoids unproductie arguments on how major or minor a release is. I guess my email is a case of "everything has been said already but not yet by ever

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

You are right, due was discontinued, and it was intentional. This may well have caused our problem - I had similar problems myself. Thanks for your fix. Tobias Makarius schrieb: > On Mon, 13 Dec 2010, Gerwin Klein wrote: > >>> Am 13.12.2010 10:38, schrieb Tobias Nipkow: >>

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

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 s

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

e and reject 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 >> beha

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

unsuspecting users should be subjected to it. Tobias Brian Huffman schrieb: > On Wed, Dec 1, 2010 at 11:50 PM, Tobias Nipkow wrote: >> Is the following behaviour really a good idea and useful? >> >> inductive P :: "nat => bool" where >> "P(suc n)&

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

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

[isabelle-dev] HOLCF problem

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 somethi

Re: [isabelle-dev] Coral and Sledgehammer

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

Re: [isabelle-dev] find_theorems raises UnequalLengths exception

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

Re: [isabelle-dev] find_theorems raises UnequalLengths exception

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 hav

Re: [isabelle-dev] find_theorems raises UnequalLengths exception

The code is mine and I haven't looked at it for some 15 years. I agree with Larry, there must be some undocumented precondition about the form of the terms, eg that they are eta expanded or contracted. Presumably the calling context used to ensure those preconditions (otherwise we would would have

Re: [isabelle-dev] Datatype alt_names

>> 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. > >

Re: [isabelle-dev] NEWS

nd possibly adding a > configuration option 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 > > Tobia

Re: [isabelle-dev] NEWS

mmer" Unification is appreciated ;-) Tobias Makarius schrieb: > 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 a

Re: [isabelle-dev] NEWS

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 B

[isabelle-dev] t_eqI and t_eq_iff

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 https://ma

[isabelle-dev] is_concealed

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 "

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

a doesn't even mention the "Pair" constructor) and "complex_Re_Im_cancel_iff" (also long, and I don't know what "cancel" is supposed to mean here). - Brian On Tue, Sep 7, 2010 at 9:45 AM, Tobias Nipkow wrote: I wanted to emphasize the mathematical conc

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

s, but I would like to be rid of the names "Pair_fst_snd_iff" (a bit long, and the lemma doesn't even mention the "Pair" constructor) and "complex_Re_Im_cancel_iff" (also long, and I don't know what "cancel" is supposed to mean here). - Brian On Tue, S

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

t is descriptive: When you see "simp add: expand_fun_eq" in a proof, there is no ambiguity about which way the rule is oriented. On the other hand, the "ext_iff" names are shorter. - Brian On Tue, Sep 7, 2010 at 3:06 AM, Tobias Nipkow wrote: __

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

___ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

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

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

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 upc

Re: [isabelle-dev] Ambiguous grammar

I think you are right. At least it would mean that the priorities are brought in line with those of the quantifiers (eg ALL), where the body has the same priority has the whole construct. Tobias Brian Huffman wrote: > Hello, > > I recently found an ambiguity in Isabelle/HOL's grammar: > > term

[isabelle-dev] proper use of "error" channel

Shouldn't this go into some documentation for future reference? Tobias Makarius schrieb: > A few hints on using the "error" function in Isabelle/ML properly. > > The ERROR exceptions being produced here are treated by the Isar > toplevel as "user-level error messages", i.e. are posted in clear t

[isabelle-dev] Sledgehammer renaming

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 sch

[isabelle-dev] Sledgehammer renaming

Before reorganizing, let alone improving s/h, the regression test tool should be in place. It is very easy to get things slightly wrong, and these tests are the only way to detect that. (Getting things badly wrong is not a problem because then the consequences are quickly felt) Tobias Jasmin Blan

[isabelle-dev] Pow

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

[isabelle-dev] Pow

I get to see 21 thms. Are you sure Set is included as an ancestor, eg via Main? Tobias Lawrence Paulson wrote: > 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 > > >

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

> So is the main thing which distinguishes a "logical framework" from a > "meta logic" the presence of a formal way to do meta-induction (and not > only prove all cases) and termination checks etc? What you are thinking of was once called a "meta logical framework" by David Basin and Bob Constable

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

> 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 >> e

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

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_RUL

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

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

[isabelle-dev] NEWS

* 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

[isabelle-dev] NEWS

* 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

* NewNumberTheory: Jeremy Avigad's new version of part of NumberTheory. If possible, use NewNumberTheory, not NumberTheory. Thanks Jeremy, we look forward to the rest of NumberTheory. Tobias

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

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

Looking at the source code, the "Bad executable" indicates that the file could not be found by Isabelle. But since it exists and is executable, as you have confirmed by executing it by hand, I can only guess that $ISABELLE_HOME is not pointing to the right place - but I don't know how to figure thi

[isabelle-dev] What's in Main

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] What's in Main

Sorry, correct version enclosed now. Danke, Sascha. Tobias -- next part -- A non-text attachment was scrubbed... Name: document.pdf Type: application/octetstream Size: 115710 bytes Desc: not available URL:

[isabelle-dev] What's in Main

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 iss

[isabelle-dev] {..n} and {..

On nat, the sets {0..n} and {..n} are the same, which can be irksome. Hence I discourage the use of {..n}. However, there are notations such as "SUM k<=n. t" which stand for "setsum (%k. t) {..n}" and introduce {..n} by the backdoor. I am tempted to get rid of this and related notations and restri

[isabelle-dev] Repository OK?

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 >

<    1   2   3   4   5   >