Re: [isabelle-dev] infix line breaking

We had already discussed this and decided that for "=", "<=" etc it makes sense. I find that the wrong associativity can be much more of a killer than where the infix op is placed. Tobias On 22/02/2019 17:20, Lawrence Paulson wrote: The pretty printing of infix operators looks pretty

Re: [isabelle-dev] Poly/ML x86_64_32 available for testing

This is really phantastic - at last I can build HOL-Analysis on my terrible new Mac without having to put it in the freezer and it does not fall over at the very end. It is also 20% faster. Great work! Tobias On 19/01/2019 21:43, Makarius wrote: Thanks to great work by David Matthews, there

Re: [isabelle-dev] mercurial accident

Hey, I wanted to join the party! But all bugs have been fixed now and Makarius will notify you of the correct changeset. Tobias On 18/01/2019 21:42, Makarius wrote: On 17/01/2019 22:54, Fabian Immler wrote: Luckily, a diff with a8faf6f15 revealed quite obviously what went wrong during the

Re: [isabelle-dev] cardinality primitives in Isabelle/HOL?

I agree with Florian wrt syntax. Tobias On 27/12/2018 13:39, Florian Haftmann wrote: I am inclined to introduce these definitions: definition lepoll :: "'a set ⇒ 'b set ⇒ bool" (infixl "≲" 50) where "lepoll A B ≡ ∃f. inj_on f A ∧ f ` A ⊆ B" definition eqpoll :: "'a set ⇒ 'b set ⇒ bool"

Re: [isabelle-dev] Lemma "sum_image_le"

Since Alexander cannot push changes, I have done so now. Tobias On 28/09/2018 18:44, Lawrence Paulson wrote: Sounds good to me! Larry On 28 Sep 2018, at 14:00, Alexander Maletzky > wrote: lemma "sum_image_le" in theory "Groups_Big", which is stated

Re: [isabelle-dev] Final consolidation for Isabelle2018-RC2

I have the same problem, and on my machine it is reproduceable (and it did not go away over the past week, although I tried different versions of the devel repository). However, I cannot reproduce the problem on testboard. Tobias On 18/07/2018 17:05, Manuel Eberl wrote: I had what seems to be

Re: [isabelle-dev] Vampire

On 06/07/2018 17:20, Lawrence Paulson wrote: On 4 Jul 2018, at 11:11, Blanchette, J.C. wrote: I’m at home today so don’t have access to that file. Please send it to me once you have a chance. It seems that I did finally succeed in getting the option set. My guess is that the Mac app

Re: [isabelle-dev] Bad session structure

This is because of a name change in the distribution. The AFP has been updated some 10 minutes later but your test run still saw the old version. It should work now. Tobias On 25/06/2018 15:25, Lawrence Paulson wrote: I still get this upon start-up. Any idea why? ebdd5508f386+ tip Larry

Re: [isabelle-dev] quaternions

Why not simply the AFP? Tobias On 18/06/2018 12:36, Lawrence Paulson wrote: I have just formalised most of the HOL Light development of quaternions. It's a great advertisement for type classes: showing that quaternions constitute a real normed division algebra and an inner product space

[isabelle-dev] Clicks are lost

I have recently (eg 6a0852b8e5a8) noticed the following behaviour, although it may be older: I start isabelle jedit Analysis.thy let it run for a little bit, then double-click on some of the early theories in the Theories panel (probably one it has processed already or is in the process of

Re: [isabelle-dev] NEWS: formal comments

This concerns only the inner syntax, where comments are rare. We should not give up the outer (* *) comments for something less convenient. Tobias On 06/02/2018 15:13, Lawrence Paulson wrote: Will there still be a way to comment out random junk? I often work with a mixture of Isabelle and

Re: [isabelle-dev] NEWS: op -> ()

Makarius, I think (simple) sections do indeed improve readbility. BUT in the light of your comments I am not keen on them in Isabelle. We do not need yet more syntactic sugar. Thanks Tobias On 01/02/2018 16:41, Makarius wrote: On 01/02/18 07:41, Tobias Nipkow wrote: At the time I was also

Re: [isabelle-dev] NEWS: op -> ()

wondering whether to allow `sections', eg "(+ 1)" or (1 +)" but did not want to overdo it. It sounds like that at least with your parser imporvements it might be ok? Tobias On 31/01/2018 22:02, Makarius wrote: On 10/01/18 20:17, Tobias Nipkow wrote: * The "op " syntax for

Re: [isabelle-dev] Gromov Hyperbolicity

cover Gödel's theorem, which we would not want to move to our core libraries. Larry On 18 Jan 2018, at 13:31, Tobias Nipkow <nip...@in.tum.de> wrote: It sounds like a reasonable criterion. Can you tell us what that means for Hausdorff_Distance, Metric_Completion and Isometries (as de

Re: [isabelle-dev] Gromov Hyperbolicity

On 18/01/2018 11:06, Fabian Immler wrote: Am 18.01.2018 um 08:32 schrieb Tobias Nipkow <nip...@in.tum.de>: 1. Library/Complement contains both new generic material like "t3_space" but also new concepts like [mono_intros] for more automation in proving of inequal

Re: [isabelle-dev] Gromov Hyperbolicity

On 18/01/2018 12:48, Lawrence Paulson wrote: We certainly need to solve this problem. Absolutely. For practical reasons I would put as much in the AFP as possible, (One could make exceptions for small theories, but this could get out of hand again). One possible criterion: which results

Re: [isabelle-dev] NEWS: op -> ()

Thanks for this discussion. Although I agree with Larry and Andreas, it is clear that there is no concensus. Hence there will be no blanket change of where line breaks go for infix operators. Tobias On 16/01/2018 17:34, Blanchette, J.C. wrote: This sort of claim needs to be justified by

[isabelle-dev] Gromov Hyperbolicity

For those of you interested in formalization of Analysis https://devel.isa-afp.org/entries/Gromov_Hyperbolicity.html I would like to call your attention to this entry because it is rich in concepts and theorems that are more general than the actual focus of the article. I believe quite a bit

[isabelle-dev] New AFP entry Gromov Hyperbolicity in devel

We have a new AFP entry in the development branch of the AFP: Gromov Hyperbolicity Sebastien Gouezel A geodesic metric space is Gromov hyperbolic if all its geodesic triangles are thin, i.e., every side is contained in a fixed thickening of the two other sides. While this definition looks

Re: [isabelle-dev] NEWS: op -> ()

On 11/01/2018 14:10, Makarius wrote: On 10/01/18 21:46, Tobias Nipkow wrote: I seem to remember Lamport makes a similar point but it is not in his "How to write a proof".] The paper is called "How to Write a Long Formula" and available e.g. here: https://lamport.az

Re: [isabelle-dev] NEWS: op -> ()

There are a number of different points here. - What is good style depends on what your math look like. Knuth writes nice traditional math, whereas Isabelle proof states can get quite ugly. In such cases I find that operator names on the next line improves readability, independent of what the

Re: [isabelle-dev] NEWS: op -> ()

On 10/01/2018 21:23, Makarius wrote: On 10/01/18 20:17, Tobias Nipkow wrote: Invoking "isabelle update_op" converts all files in the current directory (recursively). In case you want to exclude conversion of ML files (because the tool frequently also converts ML's "op" syn

[isabelle-dev] NEWS: op -> ()

* The "op " syntax for infix operators has been replaced by "()". If begins or ends with a "*", there needs to be a space between the "*" and the corresponding parenthesis. INCOMPATIBILITY. There is an Isabelle tool "update_op" that converts theory and ML files to the new syntax. Because it is

Re: [isabelle-dev] weird error message on startup

I have modified HOL-Analysis but broke latex as a result. I have undone it again just now. No idea if this has anything to do with your problem. Tobias On 06/12/2017 15:48, Lawrence Paulson wrote: I've just updated to a recent version (fa1173288322) and tried to run a session by the

Re: [isabelle-dev] NEWS: document_tags

On 05/12/2017 17:21, Makarius wrote: *** Document preparation *** * System option "document_tags" specifies a default for otherwise untagged commands. This is occasionally useful to control the global visibility of commands via session options (e.g. in ROOT). * Document markup commands

Re: [isabelle-dev] Slow builds due to excessive heap images

On 16/11/2017 12:43, Florian Haftmann wrote: Dear all, The idea above is to provide an option for the HOL codegen that is used specifically for applications like Flyspeck-Tame. It is mainly a question to codegen experts, if that can be done easily. streamlining execution of Flyspeck-Tame

Re: [isabelle-dev] Slow builds due to excessive heap images

On 08/11/2017 14:13, Makarius wrote: On 08/11/17 12:35, Tobias Nipkow wrote: On 07/11/2017 23:13, Makarius wrote: For Flyspeck-Tame a small performance loss remains. It might be worth trying to configure the Isabelle/HOL codegen to use FixedInt instead of regular (unbounded) Int. Thus

Re: [isabelle-dev] Slow builds due to excessive heap images

On 07/11/2017 23:13, Makarius wrote: For Flyspeck-Tame a small performance loss remains. It might be worth trying to configure the Isabelle/HOL codegen to use FixedInt instead of regular (unbounded) Int. Thus it could become faster with Poly/ML 5.7.1 than with 5.6. Just as for Isabelle

Re: [isabelle-dev] Slow builds due to excessive heap images

On 29/10/2017 21:52, Makarius wrote: On 28/10/17 22:26, Makarius wrote: Overall, performance is mostly the same as in Poly/ML 5.6 from Isabelle2017, but there are some dropouts. In particular, loading heap images has become relatively slow: this impacts long heap chains like HOL-Analysis or

Re: [isabelle-dev] AFP statistics

The whole project started with this AFP paper: http://www21.in.tum.de/~nipkow/pubs/cicm15.html First Max developed this just to support the statistics in the paper but then he and Lars made it part of the AFP. There is also a hidden part that generates tex files for these and a number of

Re: [isabelle-dev] Time

That did the job, many thanks. Tobias On 30/08/2017 23:02, Makarius wrote: On 30/08/17 21:50, Makarius wrote: On 30/08/17 09:21, Tobias Nipkow wrote: I still need to investigate the details, but it is probably just a very long failed attempt to find the hg root. I have now improved

[isabelle-dev] Time

I have a timing issue with b8a6f9337229 (and quite possibly other revisons): isabelle build takes 22 secs before it says "Running ...". Since creating latex documents requires many, many iterations, this is extremely painful. My setup is the following: session A = HOL + sessions

Re: [isabelle-dev] some results about "lex"

Dear Christian, They are useful, I have added them (and slightly modified the names): http://isabelle.in.tum.de/repos/isabelle/rev/5df7a346f07b Thanks Tobias On 25/08/2017 06:55, Christian Sternagel wrote: Dear list, maybe the following results about "lex" are worthwhile to add to the

Re: [isabelle-dev] [Spam] Fwd: added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy

eneral than allowing arbitrary (preorder?) relations. Peter Original Message Subject: Re: [isabelle-dev] [Spam] Fwd: added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy From: Makarius To: Tobias Nipkow ,isabelle-dev@mailbroy.informatik.tu-muenchen.de CC: On 16

Re: [isabelle-dev] [Spam] Fwd: added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy

I feel that take/drop_chain are too specialised for List, although of course this is subjective. Concerning "sorted_by" vs "sorted_wrt": the latter seems closer to informal usage. But if many people cry out for "by" we could change that. Tobias On 16/08/2017 12:10, Christian Sternagel

Re: [isabelle-dev] Fwd: added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy

The name "sorted_wrt" came from Manuel and I would like to keep it. For transtive predicates it is the same as sorted (I will add that lemma to List). I looked into your theory but did not find any further generic lemmas about "linked". Let me know if I missed any that should go into List.

Re: [isabelle-dev] [isabelle] Good name for "sublist" predicates

On 30/06/2017 20:41, Manuel Eberl wrote: By the way, I recently encountered a similar (and even more nasty) name clash, with compact. The following works perfectly It's "Topological_Spaces.compact" and that should definitely work. We should probably make the one from Complete_Partial_Order2

Re: [isabelle-dev] [isabelle] Good name for "sublist" predicates

thing as it is Incidentally, I wonder if it is possible to locally prefer one of the two constants, i.e. say that, in the following block, I want "subseq" to mean "Topological_Spaces.subseq". That might also mitigate the problem of long qualified names. Manuel On 2017-06-30 16:23, Tobias Nipk

Re: [isabelle-dev] [isabelle] Good name for "sublist" predicates

In theory that solves the problem, but the point is that Topological_Spaces.subseq is impractical for a frequently used symbol. It would be nice if non-quaified names could be found for this case. Tobias On 30/06/2017 16:14, Lawrence Paulson wrote: Indeed we do. Larry On 28 Jun 2017, at

Re: [isabelle-dev] [isabelle] Good name for "sublist" predicates

when I import HOL-Probability. Can this name clash be eliminated before the next release such that I don't have to write Topological_Spaces.subseq everywhere? Thanks, Andreas On 26/05/17 08:16, Tobias Nipkow wrote: Thank you for your research. I am perfectly happy with "su

Re: [isabelle-dev] Issue in AFP

I added two useful simp rules that broke (= mostly shortened) a number of proofs. I'll fix the slow sessions over the next few days - they are a bit of a challenge. Tobias On 18/06/2017 20:38, Florian Haftmann wrote: isabelle: 20304512a33b tip afp: 644957b424ee tip JinjaThreads FAILED (see

Re: [isabelle-dev] Bad theory import "Main"

On 24/04/2017 14:24, Makarius wrote: In the past 1.5 years, I've spent a lot of time trying to explain how the Isabelle administration works. If we don't manage to overcome the "blame game", things will decline further. If you think I was trying to blame you for having forgotten to commit a

Re: [isabelle-dev] Bad theory import "Main"

The Isabelle regression test system shows up a mistake in a commit of yours and you ask what its purpose is? And tell us your rarely look there? LOL Tobias On 23/04/2017 14:52, Makarius wrote: On 23/04/17 08:39, Tobias Nipkow wrote: The Isabelle regression test system shows similar

Re: [isabelle-dev] Bad theory import "Main"

The Isabelle regression test system shows similar behaviour: 23:23:27 *** No such file: "/media/data/jenkins/workspace/isabelle-repo-makeall/src/HOL/Main.thy" 23:23:27 *** The error(s) above occurred for theory "Main" (line 8 of

Re: [isabelle-dev] Access problems to repositories and NFS

On 12/04/2017 14:29, Makarius wrote: On 11/04/17 09:34, Lars Hupel wrote: In order to keep going with development, I've created a temporary clone on Bitbucket: I'm in the process of inviting people to that clone so they can keep working. I'll also

Re: [isabelle-dev] Access problems to repositories and NFS

On 11/04/2017 16:17, Makarius wrote: On 11/04/17 09:34, Lars Hupel wrote: In order to keep going with development, I've created a temporary clone on Bitbucket: I hope that this is just a temporary workaround (famous last words, I know ...).

Re: [isabelle-dev] Integers in Poly/ML

On 02/11/2016 15:58, Lawrence Paulson wrote: I have to say, I’m absolutely mystified by the response to my suggestion. This is a nontrivial change in the semantics. The programming language community has tried to get away from the "looks ok" approach to "here is some sound reasoning why it

Re: [isabelle-dev] Integers in Poly/ML

I value the guarantees we get from having proper integers a lot. No worries. With bounded integers, we would have to worry about what happens to over/underflow exceptions: can handlers for such exceptions in a piece of user code lead to unsoundness in the inference system? At first it seems

Re: [isabelle-dev] AFP broken

These are good suggestions, thanks, we'll add them to the submission system. Tobias On 19/10/2016 23:33, Makarius wrote: The situation can be easily improved: the AFP submission system merely needs to check for "Legacy feature" warnings, and tell the authors to eliminate them beforehand.

Re: [isabelle-dev] Distro broken

We never promised that the new test infrastructure would guarantee that nobody will break the repository anymore. You are perfectly aware of this. So stop trolling. Tobias On 19/10/2016 13:52, Makarius wrote: On 19/10/16 13:38, Lars Hupel wrote: Oh, nothing went wrong: Jenkins sent an

Re: [isabelle-dev] Jenkins maintenance

Sorry, I don't consider them useless. Tobias On 06/10/2016 17:00, Makarius wrote: This is actually my main point of criticism for the present situation: the Jenkins setup uses a lot of hardware resources, by doing too many useless tests. smime.p7s Description: S/MIME Cryptographic

Re: [isabelle-dev] Jenkins maintenance

On 06/10/2016 14:34, Makarius wrote: On 03/10/16 17:12, Manuel Eberl wrote: It would also be an effective safeguard against breaking the repository (and possibly even the AFP), which /does/ happen quite frequently. (cf. the current situation where things have been broken for days) I also

Re: [isabelle-dev] not-exists problem

This discussion clearly shows that ∃! with multiple bound variables is a recipe for confusion and should be avoided. Tobias On 14/09/2016 09:49, Peter Lammich wrote: On Di, 2016-09-13 at 23:35 +, michael.norr...@data61.csiro.au wrote: Note that ∃!x. ∃!y. P x y is not equivalent to ∃!xy.

Re: [isabelle-dev] not-exists problem

There is a method to this madness: if B is a binder, "B x y. t" is short for "B x. B y. t". However, I agree that for ∄ and ∃! this is confusing and one of the solutions proposed should be adopted. Tobias On 13/09/2016 09:45, Peter Lammich wrote: On Di, 2016-09-13 at 00:46 +0100, Lawrence

[isabelle-dev] NEWS: split!

* Splitter in simp, auto and friends: - The syntax "split add" has been discontinued, use plain "split". - For situations with many conditional or case expressions, there is an alternative splitting strategy that can be much faster. It is selected by writing "split!" instead of "split". It

Re: [isabelle-dev] Fwd: [Isabelle-ci] Build failure in Isabelle

On 08/08/2016 13:13, Manuel Eberl wrote: I've heard of negative thermal expansion in some materials, but I don't think RAM is subject to it. (scnr) In a more serious fashion: I don't see how ambient temperature could affect memory usage. I've run into "insufficient memory" and stack overflow

Re: [isabelle-dev] Multiset insert

On 28/07/2016 10:33, Peter Lammich wrote: On Do, 2016-07-28 at 10:21 +0200, Jasmin Blanchette wrote: Tobias wrote: How about definition add_mset :: "'a ⇒ 'a multiset ⇒ 'a multiset" ("add#") where "add# x M = {#x#} + M" This, however, may produce confusion with multiset union, which is an

Re: [isabelle-dev] Multiset insert

On 27/07/2016 11:39, Jasmin Blanchette wrote: Tobias wrote: Did we ever discuss the naming issue? "insert_mset" would be the canonical name, but it would make larger expressions hard to read. I'm not so sure "insert_mset" would be the right name. Its set-based terminology might suggest a

Re: [isabelle-dev] NEWS: Primes

Naming: can't we drop "is_"? Tobias On 27/07/2016 10:46, Manuel Eberl wrote: *** HOL *** * Number_Theory: algebraic foundation for primes: Introduction of predicates "is_prime", "irreducible", a "prime_factorization" function, the "factorial_ring" typeclass with instance proofs for nat, int,

Re: [isabelle-dev] Multiset insert

as On 08 Apr 2015, at 11:12, Larry Paulson <l...@cam.ac.uk> wrote: Sounds logical to me. Larry On 8 Apr 2015, at 08:13, Tobias Nipkow <nip...@in.tum.de> wrote: Currently the setup in Multiset is geared towards having the 3 basic (non-free) constructors: empty, singleton and uni

Re: [isabelle-dev] multiplicity and prime numbers

Are you sure that there is no standard definition of this concept in mathematics that we should follow? Tobias On 19/07/2016 12:03, Manuel Eberl wrote: Hallo, as some of you may already know, I am currently in the process of resructing Isabelle's definitions of prime numbers. Before these

Re: [isabelle-dev] \nexists

On 15/07/2016 20:33, Makarius wrote: On 15/07/16 17:08, Tobias Nipkow wrote: For me a default is something that a) is beneficial for the majority of users and b) can be overwritten if you don't like it. Isn't that possible here? That is the existing default of not insisting in Latex

Re: [isabelle-dev] \nexists

On 15/07/2016 15:32, Makarius wrote: On 15/07/16 13:53, Johannes Hölzl wrote: Am Freitag, den 15.07.2016, 12:15 +0200 schrieb Tobias Nipkow: LaTeX build problems are not infrequent and could be avoided easily if "build" produced the document by default. +1 -10 Every min

Re: [isabelle-dev] \nexists

LaTeX build problems are not infrequent and could be avoided easily if "build" produced the document by default. Tobias On 14/07/2016 17:50, Lawrence Paulson wrote: The recent failure in Multivariable_Analysis was caused by the \nexists macro, which is not defined: ! Undefined control

[isabelle-dev] NEWS

* Theory Library/LaTeXsugar.thy: New style "dummy_pats" for displaying equations in functional programming style: variables present on the left-hand but not on the righ-hand side are replaced by underscores. See the tutorial "LaTeX Sugar for Isabelle Documents". Tobias smime.p7s Description:

Re: [isabelle-dev] {0::nat..<n} = {..<n}

Florian, The whole setup has grown over time and initially I may have preferred {..

Re: [isabelle-dev] {0::nat..<n} = {..<n}

The problem with {..

Re: [isabelle-dev] Syntax for lattice operations?

On 12/06/2016 18:22, Florian Haftmann wrote: Thus I would like to understand why we cannot reuse Sup etc in HOLCF like we do for all the other variants of lattices we have. We would probably need a suitable type class because at the moment lub is unrestricted. For each type class, per type

Re: [isabelle-dev] Syntax for lattice operations?

On 11/06/2016 21:26, Florian Haftmann wrote: For the moment I think bold syntax in the first choice. In the middle run I would suggest to have a closer look at HOLCF/Porder.thy to see whether something can be done to integrate it more with the standard type classes; a least it formalizes a

Re: [isabelle-dev] Nonterminating AFP build

This requires Johannes' expertise, but he is away for a few days. Tobias On 12/05/2016 12:58, Lawrence Paulson wrote: There are multiple failures in PMF_OF_List. It looks like the behaviour of simplification has changed concerning the functions ennreal and ereal. Larry On 12 May 2016, at

Re: [isabelle-dev] Syntax for lattice operations?

On 10/03/2016 11:00, Florian Haftmann wrote: Hi all, traditionally, syntax for lattice operations (⊓ ⊔ ⊥ ⊤ etc.) has been kept in a separate library theory, to allow use of that quite generic notation for unforeseen applications. Meanwhile however all those operations to which

Re: [isabelle-dev] Explicit representation of multisets

Although I suggested we do this, and still think logically it is the right thing to do, I see one issue, the naming of insert#. The canonical name is insert_mset, but this leads to the rather lengthy "insert_mset x M" as opposed to the current "{#x#} + M". This would come up in all inductive

Re: [isabelle-dev] Preferred syntax for big GCD?

THE, LEAST, GCD. Tobias On 10/03/2016 10:46, Florian Haftmann wrote: Hi all, in 66a381d3f88f, the usual syntax for big operators has been added for GCD (and LCM): (a) Gcd x \ A. f x An alternative could be (b) GCD x \ A. f x The form (b) follows the tradition to have binders

Re: [isabelle-dev] Notation for not-exists

On 04/03/2016 12:34, Makarius wrote: The Isabelle symbol \ has been there for many years, even with a standard abbreviation "~?" for the Prover IDE. A comment in LaTeXsugar.thy from 2005 http://isabelle.in.tum.de/repos/isabelle/file/922e702ae8ca/src/HOL/Library/LaTeXsugar.thy#l23 says: (*

[isabelle-dev] Line breaks in pretty-printed output

One page in Concrete Semantics contains the following output that is a pretty-printed HOL formula: step S27 (x ::= Plus (V x) (N 1) {{}};; x ::= Plus (V x) (N 2) {Q}) = ... With db9996a84166 it prints like this: step S27 (x ::= Plus (V x) (N 1) {{}};; x ::= Plus (V x) (N 2) {Q})

Re: [isabelle-dev] Lemmas about tranclp and lexn

I added lexn_transI. Thanks Tobias On 30/12/2015 15:25, Mathias Fleury wrote: Dear list, I stumbled upon some lemmas that have a counterpart in Isabelle (like rtranclp_mono vs tranclp_mono), but are not included. Is there a reason why the following lemmas are not included in Isabelle?

Re: [isabelle-dev] Infinite_Set.thy

On 27/11/2015 16:11, Lawrence Paulson wrote: This theory proves a number of useful properties of infinite sets, and consequently, of finite sets. I’m wondering whether it makes sense to have this theory (a 17 KB file) in the Library when our main theory Finite_Set.thy (60 KB) is part of the

[isabelle-dev] popup in ce6320b9ef9b

In more than one example of locale interpretations with "where f = g", where g is a constant, if I hover over the g, the popup shows the type of g twice. Tobias smime.p7s Description: S/MIME Cryptographic Signature ___ isabelle-dev mailing list

Re: [isabelle-dev] MIR decision procedure

MIR is "documented" in Amine's IJCAR 2006 paper "Verifying Mixed Real-Integer Quantifier Elimination". Maybe the title gives you a hint what it is good for. Ferrack stands for Ferrante & Rackoff, who invented this QE algorithm. This one may only be "documented" in Amine's PhD. Tobias On

Re: [isabelle-dev] the function "real"

On 12/11/2015 13:03, Lawrence Paulson wrote: I’m going to try to make the other change as well. The problem is that for a great many theorems, their behaviour with the simplifier and/or blast differed according to which coercion function they were expressed with. This makes it impossible to

Re: [isabelle-dev] NEWS: State panel

On 10/11/2015 14:20, Gerwin Klein wrote: On 9 Nov 2015, at 9:41 pm, Makarius wrote: * The State panel manages explicit proof state output, with jEdit action "isabelle.update-state" (shortcut S+ENTER) to trigger update according to cursor position. * The Output panel no

Re: [isabelle-dev] Future of permanent_interpretation

On 28/10/2015 21:41, Clemens Ballarin wrote: On 26 October, 2015 10:38 CET, Tobias Nipkow <nip...@in.tum.de> wrote: My desire to generate code from locale interpretations w/o having to make a number of trivial function definitions was what started this whole business a number of year

Re: [isabelle-dev] Future of permanent_interpretation

I am very happy to see that we agree that a "defines" section is a useful addition to the interpretation command. But at the moment, this section only exists for "permanent_interpretation". It would be nice if "interpretation" were enhanced with "defines", in which case people could make use

Re: [isabelle-dev] NEWS: document preparation refinements

Thanks, that did the trick. Tobias On 26/10/2015 18:16, Makarius wrote: On Sat, 24 Oct 2015, Tobias Nipkow wrote: I don't know if this is related, but it must have happened recently: The [display] option for antiquotations now (eg 436b7fe89cdc) generates latex that indents the text following

Re: [isabelle-dev] Some thoughts on mixfix syntax partially applied [was: NEWS]

by the syntax error they get. But if your HOL4 experience suggests that this is not an issue, I would be in favour of "(sym)". Tobias Michael On 6 Oct 2015, at 23:12, Makarius <makar...@sketis.net> wrote: On Tue, 22 Sep 2015, Tobias Nipkow wrote: The "op" noation is

Re: [isabelle-dev] NEWS: toplevel theorem statements

On 06/10/2015 21:46, Makarius wrote: * Toplevel theorem statement 'proposition' is another alias for 'theorem'. Although this is consistent with the usage in mathematics, it is at odds with the usage in logic and in Isabelle where propositions are simply formulas, not necessarily provable

Re: [isabelle-dev] Some thoughts on mixfix syntax partially applied [was: NEWS]

The "op" noation is idiosyncratic, but there are examples (not in individual formulae) where I find some such notation convenient. I would welcome Haskell's "(+)", but that has a problem with "(*)". Unless we can make that notation work, I don't think we profit much by a change. Hence I am

Re: [isabelle-dev] Implicit eta-contraction during printing and product binders [was: NEWS]

Dear Florian, I get the definite impression that the whole operation is out of proportion wrt the benefits. As far as I can tell, the result is a unification of two previously distinct constants, split and prod_case. I must confess that this duplication has never bothered me. Now the

Re: [isabelle-dev] NEWS

I hope you will also restore the printing of "λ(x,y). x+y" as "λ(x,y). x+y" rather than "uncurry op +". Tobias On 10/09/2015 12:48, Florian Haftmann wrote: Hi Andreas, I noticed that the new printing interacts strangely with set comprehensions. In Isabelle/92858a52e45b, "{(x, y). P x y}"

Re: [isabelle-dev] NEWS

On 10/09/2015 12:19, Dmitriy Traytel wrote: Hi Florian, while I very much welcome the simplified printing rules and your effort of unifying case_prod/split, I am not sure if adding a third alternative name is the way to go. The situation reminds me of the one depicted in [1]. Clearly,

Re: [isabelle-dev] Deprecating legacy ASCII symbols?

I have no objection to phasing out some of the ASCII symbols. For me the main advantage is that they provide a graphic image that one can quickly recall as an input shortcut: == comes to mind more quickly than some alphabetic name and I would not want to lose that. But freeing them up in the

Re: [isabelle-dev] Fwd: test failed (Archive of Formal Proofs)

I hope I fixed that this morning. Tobias On 18/06/2015 21:31, Larry Paulson wrote: Looks like a recent change has broken Nominal2: *** Failed to load theory Nominal2_Abs (unresolved Nominal2_Base) *** Failed to load theory Nominal2_FCB (unresolved Nominal2_Abs) *** Failed to load theory

Re: [isabelle-dev] Remaining uses of defer_recdef?

On 11/06/2015 14:00, Makarius wrote: Is that just a question of which side of the river has greener grass? Function does a number of things very nicely, eg nested recursion and partiality. That is worth taking on board. Tobias smime.p7s Description: S/MIME Cryptographic Signature

Re: [isabelle-dev] Remaining uses of defer_recdef?

Function and recdef work very differently. Function first disambiguates the patterns, then it defines the graph of the function as an inductive definition. Recdef turns the definitions into a single recursion equation with case-expressions on the rhs. Concerning the minimum number of

Re: [isabelle-dev] Remaining uses of defer_recdef?

A frequent use case is this: you have 5-10 interesting patterns where stuff happens and an otherwise pattern with a simple rhs. In that case you do want to write those 5-10 patterns explicitly and let the definition facility take care of the hundreds of patterns that the default case expands

Re: [isabelle-dev] Remaining uses of defer_recdef?

The reason for the continued existence of recdef is that function can cause a combinatorial explosion the way it compiles pattern matches. I just tried Cooper.thy and changing one of the recdefs to function makes Isabelle go blue (purple) in the face until one gives up. Hardware alone will not

Re: [isabelle-dev] Remaining uses of defer_recdef?

On 06/06/2015 20:11, Larry Paulson wrote: Pattern matching is a convenience, and can always be eliminated manually. Is there really no reasonable way to re-express the definitions in Cooper.thy? You can always turn all patterns of the lhs into cases on the rhs and derive the individual

Re: [isabelle-dev] Infix syntax for division?

Indeed, the warning sign attached to div can be very helpful. Hence b). Tobias On 02/06/2015 21:10, Jasmin Blanchette wrote: Hi Florian, a) The radical solution: there is only »_ / _« for both field division and euclidean division. How natural is notation like »a / b * b + a mod b = a« then?

Re: [isabelle-dev] »real« considered harmful

For me the main point of real is the ease of writing. If we get rid of some lemma duplications but trade that in for many type annotations, I am not in favour. Tobias On 02/06/2015 20:18, Florian Haftmann wrote: Dear all, recently, I stumbled (once again) over the matter of the »real«

Re: [isabelle-dev] »real« considered harmful

obstructive abbreviations like e.g., real_N and real_Z, or real⇩N and real⇩Z. But I see that real_of_foo is much more uniform and you can immediately read off the type foo. Fabian Am 03.06.2015 um 10:11 schrieb Tobias Nipkow nip...@in.tum.de: For me the main point of real is the ease of writing. If we

  1   2   3   4   >