Re: [isabelle-dev] infix line breaking

[Tobias Nipkow]

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 terrible in the presence of 
large terms.

I’d like to propose having infix operators breaking at the start of the line 
rather than at the end. Any thoughts?

Larry

inv⇘homology_group 0 (nsphere 0)⇙ hom_induced 0 (subtopology (nsphere 0) {pp}) 
{} (nsphere 0) {} r
d =
 hom_induced 0 (subtopology (nsphere 0) {nn}) {} (nsphere 0) {} id
  (hom_induced 0 (subtopology (nsphere 0) {pp}) {} (subtopology (nsphere 0) 
{nn}) {} r
(inv⇘homology_group 0 (subtopology (nsphere 0) {pp})⇙ d))
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Tobias Nipkow]

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 is now an Isabelle
component polyml-test-0a6ebca445fc (Isabelle/3b777286c3ec), which can be
enabled manually, e.g. in $ISABELLE_HOME_USER/etc/settings like this:

   init_component "$HOME/.isabelle/contrib/polyml-test-0a6ebca445fc"

It requires the usual "isabelle components -a" incantation afterwards.


This supports 3 platform variants:

   x86
   x86_64
   x86_64_32

x86 is still there for comparison, but will disappear soon.

x86_64 is the full 64-bit model as before, and subject to the system
option "ML_system_64 = true".

x86_64_32 is the default. It is a synthesis of the x86_64 architecture
(more memory, more registers etc.) with a 32-bit value model for ML.
Thus we get approx. 5 times more memory as in x86, without the penalty
of full 64-bit values.

Moreover, we have a proper "64-bit application" according to Apple (and
Linux distributions): it is getting increasingly hard to run old x86
executables, and soon it might be hardly possible at all. In other
words, Poly/ML is now getting ready for many more years to come.


The above component already works smoothly for all of Isabelle + AFP,
only with spurious drop-outs that can happen rarely. x86_64_32 is
already more stable than x86, which often suffers from out-of-memory
situations.


So this is the right time for further testing of applications:
Isabelle2018 should work as well, but I have not done any testing beyond
"isabelle build -g main" -- Isabelle development only moves forward in
one direction on a single branch.

For really big applications, it might occasionally help to use something
like "--maxheap 8g" in ML_OPTIONS: the implicit maximum is 16g, which is
sometimes too much for many parallel jobs on mid-range hardware. There
are additional memory requirements outside the ML heap, for program code
and stacks.


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] mercurial accident

[Tobias Nipkow]

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 merges, so I could easily redo Angeliki's tagging (689997a8).

We should be back to normal (regarding isabelle build -a).


That was Isabelle/94284d4dab98, but Tobias has just pushed a bad merge
again: Isabelle/aeceb14f387a.

I can only quote README_REPOSITORY once more:


Testing of changes (before push)


The integrity of the standard pull/push area of Isabelle needs the be
preserved at all time.  This means that a complete test with default
configuration needs to be finished successfully before push.  If the
preparation of the push involves a pull/merge phase, its result needs
to covered by the test as well.


Such testing of local changes plus the resulting merge is not optional,
but mandatory.

There is a natural routine of "hg commit" vs. "isabelle build -a" to
make it all work well without any effort.


Makarius





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Tobias Nipkow]

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" (infixl "≈" 50)
 where "eqpoll A B ≡ ∃f. bij_betw f A B”

They allow, for example, this:

theorem Schroeder_Bernstein_eqpoll:
   assumes "A ≲ B" "B ≲ A" shows "A ≈ B"
   using assms unfolding eqpoll_def lepoll_def by (metis Schroeder_Bernstein)

The names and syntax are borrowed from Isabelle/ZF, and they are needed for 
some HOL Light proofs.

But do they exist in some form already? And are there any comments on those 
relation symbols?


The notation itself is quite generic, so it is worth spending more
thoughts on how can we keep reusable.  Maybe it would be worth a try to
put the syntax into a bundle (there are already some applications of
that pattern):

bundle set_relation_syntax
begin

notation …

end

bundle no_set_relation_syntax
begin

no_notation …

end

…

unbundle set_relation_syntax

…

unbundle no_set_relation_syntax

The input abbreviation gepoll should be added as well.

Anyway, I am uncertain about the name »poll«.

Cheers,
Florian


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





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Lemma "sum_image_le"

[Tobias Nipkow]

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 for
type-class "ordered_ab_group_add", holds more generally for
"ordered_comm_monoid_add" (proof below). May I propose to change it
accordingly?

Best regards,
Alexander




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





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Tobias Nipkow]

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 a spurious failure of Probabilistic_Timed_Automata 
yesterday: https://ci.isabelle.systems/jenkins/job/testboard/50/consoleFull


The error message is:

*** exception THM 0 raised (line 1136 of "thm.ML"): generalize: bad index

I am quite sure that my (purely cosmetic) changes are completely unrelated to 
that error and a later test run of virtually the same thing worked fine.

Perhaps this should be investigated before the release.

Manuel


On 2018-07-18 12:53, Makarius wrote:

This is a reminder that we are in the final consolidation phase towards
Isabelle2018-RC2.

I will say more precisely when the fork of the isabelle-dev vs.
isabelle-release repositories will happen, presumably in the next few
days. After return from FLoC I still need to sort out many details, and
some genuine problems (apart from inevitable last-minute additions).


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev




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





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Vampire

[Tobias Nipkow]

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 doesn't necessarily save settings, depending on whether you exit with 
Isabelle > Quit Isabelle or File > Exit. And I’m not sure which one of these is 
supposed to work.


I have stopped using Isabelle > Quit Isabelle (cmd-Q) because it does not ask 
you if you want to save modified files; it doesn't save them but creates 
autosave files. Quite possibly it does not save settings either.


Tobias


But even if I somehow misspelt “yes” five times,

But maybe you wrote "true" five times?


certainly not.

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





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Bad session structure

[Tobias Nipkow]

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

Cannot load theory "HOL-Data_Structures.Priority_Queue"
The error(s) above occurred for theory "HOL-Data_Structures.Priority_Queue"
(required by "Priority_Queue_Braun.Priority_Queue_Braun") (line 7 of 
"/Users/lp15/isabelle/afp/devel/thys/Priority_Queue_Braun/Priority_Queue_Braun.thy")
No such file: "HOL-Data_Structures.Priority_Queue"
The error(s) above occurred in session "Priority_Queue_Braun" (line 3 of 
"/Users/lp15/isabelle/afp/devel/thys/Priority_Queue_Braun/ROOT")
Cannot load theory "HOL-Data_Structures.Priority_Queue"
The error(s) above occurred for theory "HOL-Data_Structures.Priority_Queue"
(required by "Amortized_Complexity.Skew_Heap_Analysis" via "Skew_Heap.Skew_Heap") (line 7 
of "/Users/lp15/isabelle/afp/devel/thys/Skew_Heap/Skew_Heap.thy")
No such file: "HOL-Data_Structures.Priority_Queue"
The error(s) above occurred in session "Amortized_Complexity" (line 3 of 
"/Users/lp15/isabelle/afp/devel/thys/Amortized_Complexity/ROOT")
Cannot load theory "HOL-Data_Structures.Priority_Queue"
The error(s) above occurred for theory "HOL-Data_Structures.Priority_Queue"
(required by "Skew_Heap.Skew_Heap") (line 7 of 
"/Users/lp15/isabelle/afp/devel/thys/Skew_Heap/Skew_Heap.thy")
No such file: "HOL-Data_Structures.Priority_Queue"
The error(s) above occurred in session "Skew_Heap" (line 3 of 
"/Users/lp15/isabelle/afp/devel/thys/Skew_Heap/ROOT")
Cannot load theory "HOL-Data_Structures.Priority_Queue"
The error(s) above occurred for theory "HOL-Data_Structures.Priority_Queue"
(required by "Pairing_Heap.Pairing_Heap_Tree") (line 8 of 
"/Users/lp15/isabelle/afp/devel/thys/Pairing_Heap/Pairing_Heap_Tree.thy")
No such file: "HOL-Data_Structures.Priority_Queue"
The error(s) above occurred in session "Pairing_Heap" (line 3 of 
"/Users/lp15/isabelle/afp/devel/thys/Pairing_Heap/ROOT")
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] quaternions

[Tobias Nipkow]

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 supersedes most of the 
HOL Light proofs (many files), which are devoted to developing the arithmetic 
and topological properties of quaternions. In the course of this, I also ported 
the HOL Light development of the three-dimensional vector cross product.

So where does this material belong? Arguably not in Analysis, which is already 
too large.

Another question: I did not port the quaternion material relating to the 
constant reflect_along, which is defined as follows:

(* Reflection of a vector about 0 along a line. *)

let reflect_along = new_definition
  `reflect_along v (x:real^N) = x - (&2 * (x dot v) / (v dot v)) % v`;;

Is this concept useful, and if so, where does it belong?

Larry

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





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] Clicks are lost

[Tobias Nipkow]

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 doing so) and after a little bit double-click on theory Analysis in the 
theory panel, this double click is usually ignored. Often a second double-click 
is ignored as well. Typically the fan is quite busy. Eventually (12-20 secs?) a 
third double-click returns me to Analysis.thy.


Tobias



smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: formal comments

[Tobias Nipkow]

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 commented-out HOL Light material.


Larry

On 26 Jan 2018, at 20:19, Makarius > wrote:


* Old-style inner comments (* ... *) within the term language are legacy
and will be discontinued soon: use formal comments "― ‹...›" or "⌦‹...›"
instead.




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





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Tobias Nipkow]

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


I am unsure -- my changes barely recovered the old performance. Anyway,
this is how to do measurements on the most relevant AFP sessions:

isabelle build -d '$AFP' -R -b -j4 HOL-ODE-Numerics
Encodability_Process_Calculi

isabelle build -d '$AFP' -o threads=1 -o profiling=time HOL-ODE-Numerics
Encodability_Process_Calculi

isabelle profiling_report
~/.isabelle/heaps/polyml-5.7.1_x86-linux/log/HOL-ODE-Numerics.gz

isabelle profiling_report
~/.isabelle/heaps/polyml-5.7.1_x86-linux/log/Encodability_Process_Calculi.gz

The tail of the latter looks like this:

318 List.filter
338 Same.map
481 eq-typ
521 Term.aconv
575 Lexicon.tokens_match_ord
712 Basics.fold
771 List.map
944 GARBAGE COLLECTION (minor collection)
944 GARBAGE COLLECTION (total)
   1147 Table().lookup_key
   1168 Table().defined
   2034 Table().lookup
   2178 Table().modify

Addition of grammar productions (for local syntax) shows up as
Table().lookup, Table().modify, Lexicon.tokens_match_ord. Actual parsing
also as List.filter.


Note that infix sections will require more than just a few grammar
changes: you need to introduce a lambda or auxiliary combinator for the
right section (+ a). Maybe based on some "abbreviation (input)"?

Here are also some notes from Haskell:
https://wiki.haskell.org/Section_of_an_infix_operator that immediately
raise more questions:

   * What to do with prefix "-" vs. infix "-"?

   * What to do with iterated sections (a + b +)?

   * Does all that actually help readability of expressions (e.g. for
mathematicians) or just appeal to strange Haskelloids?


Makarius





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Tobias Nipkow]

I was afraid of exactly this when I made the change but only looked at the build 
times for the distribution (which seemed fine) but not the AFP. Thank you for 
spotting and even undoing the performance regression. I look forward to having 
(*) in the inner syntax.


At the time I was also 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 infix operators has been replaced by
"()". If  begins or ends with a "*", there needs to
be a space between the "*" and the corresponding parenthesis.

In revision eab6ce8368fa


That change actually had significant performance impact on some AFP
sessions, see
http://isabelle.in.tum.de/devel/build_status/AFP around 11-Jan-2018,
e.g. HOL-ODE-Numerics, Psi_Calculi, Lorenz_Approximation,
Encodability_Process_Calculi.

Presumably, the reason for that is the grammar lookahead management with
infix operators that require extra space, e.g. '(' '*' ')'. In contrast
'(+)' is a distinctive token that does not interfere with other productions.


I have already spent a few days reworking the grammar management, see
various changes leading up to Isabelle/5f86e2a9c59c.

So the AFP performance charts are already converging back to normal, and
some sessions are now faster than before. (This also shows how important
AFP performance measurement is for continued Isabelle development.)


We can ultimately get rid of the extra space for (*) when inner comment
syntax is discontinued -- after the next release, according to the
normal schedule.


Makarius





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Gromov Hyperbolicity

[Tobias Nipkow]

So what is the situation wrt the theories I asked about?

Tobias

On 18/01/2018 15:11, Lawrence Paulson wrote:

This is mainly a negative criterion, i.e., something outside the undergraduate 
curriculum probably should not be in our core libraries. But I would guess for 
example mathematicians 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 detailed by Fabian)?






smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Gromov Hyperbolicity

[Tobias Nipkow]

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 inequalities. In 
short, there is a wealth of material that might be suitable for inclusion in HOL-Analysis.
I have already made a start by moving a few [simp] rules but that is it from me 
because I am not familiar enough with the Analysis material.

Most of this looks like it could go to HOL-Analysis.


2. Hausdorff_Dinstance, Metric_Completion and Isometries stronly smell of 
generic concepts that should go somewhere else.
We need a discussion on whether any of the theories deserve a separate AFP 
entry.

In my opinion, Hausdorff_Distance and Metric_Completion are general enough to 
put them to HOL-Analysis.
(They are also relatively short, so I am not sure if it is worth to create 
separate AFP entries.)

The theory Isometries contains Lipschitz maps, isometries, geodesic spaces, and 
quasi-isometries.
The very same definition of Lipschitz maps is also in 
AFP/Ordinary_Differential_Equations, so I take this as a strong indication to 
move Lipschitz maps to HOL-Analysis. Isometries also seem like a generically 
useful concept and could go to HOL-Analysis.


A lot of things are useful, but Isometries.thy is large and would also make a 
nice AFP entry.


Tobias


My impression is that geodesic spaces and quasi-isometries are more specialised 
concepts (but that might also be just because I have never come across them up 
to now...). I have no real opinion on what to do with them.


We do not have a precise specification of what HOL-Analysis is or should be. I 
think that makes it very hard to draw a line between material that should go to 
HOL-Analysis and what should remain in the AFP. So take this as just my 
personal view.

Fabian





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Gromov Hyperbolicity

[Tobias Nipkow]

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 
are part of a standard undergraduate  athematics curriculum?


It sounds like a reasonable criterion. Can you tell us what that means for 
Hausdorff_Distance, Metric_Completion and Isometries (as detailed by Fabian)?


Tobias


Larry

On 18 Jan 2018, at 10:06, Fabian Immler > wrote:


We do not have a precise specification of what HOL-Analysis is or should be. I 
think that makes it very hard to draw a line between material that should go 
to HOL-Analysis and what should remain in the AFP. So take this as just my 
personal view.




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





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Tobias Nipkow]

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 evidence. We had it the first way 
until the late 1990s. I changed it to the other way while working on large 
proof states connected with crypto protocols. It seemed more readable to me for 
such proofs.


I was taught at school to avoid starting every sentence with "I think" or "I 
believe", since obviously whatever I say is my opinion, but since this apparently leads to 
confusion, I'll happily relativize my previous statement: Just as you found one style more readable 
than another (without giving any evidence), *I* find

foo ==>
bar

and especially

foo ==> bar ==>
baz

much more readable than the alternative, because they yield less opportunities for what 
Bryan Garner (Modern Am. E. Usage) refers to as "miscues" when parsing. When I 
read the alternative, I get the same effect as when I listen to the Murder City Devils 
and they sing

God knows she's pretty
messed up

I don't think there's a need for a big empirical study to observe the miscue; 
it should be easily reproducible by any left-to-right reader. By the same 
token, I can understand that in the presence of [| ... |], the opposite 
convention has its benefits (as stressed by Andreas).

One more case: Suppose you have

foo ==>
bar ==> baz

Notice how the break falls naturally where you would insert the parentheses:

foo ==>
(bar ==> baz)

Compare with

foo ==> (bar
==> baz)

So I will be apologized, surely, for preferring the end-of-line treatment for 
operators that bind to the right, while realizing that I might be in the 
minority on this mailing list.

Jasmin





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] Gromov Hyperbolicity

[Tobias Nipkow]

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 of the material could be pulled out and made more visible. 
Here are some pointers:


1. Library/Complement contains both new generic material like "t3_space" but 
also new concepts like [mono_intros] for more automation in proving of 
inequalities. In short, there is a wealth of material that might be suitable for 
inclusion in HOL-Analysis.
I have already made a start by moving a few [simp] rules but that is it from me 
because I am not familiar enough with the Analysis material.


2. Hausdorff_Dinstance, Metric_Completion and Isometries stronly smell of 
generic concepts that should go somewhere else.

We need a discussion on whether any of the theories deserve a separate AFP 
entry.

Sebbastien has already made an effort to separate the generic from the specific. 
We should capitalize on that, but it needs a bit of voluntary work.


Tobias



smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Tobias Nipkow]

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 innocuous, it has proved extremely important 
and versatile in modern geometry since its introduction by Gromov. We formalize 
the basic classical properties of Gromov hyperbolic spaces, notably the Morse 
lemma asserting that quasigeodesics are close to geodesics, the invariance of 
hyperbolicity under quasi-isometries, we define and study the Gromov boundary 
and its associated distance, and prove that a quasi-isometry between Gromov 
hyperbolic spaces extends to a homeomorphism of the boundaries. We also prove a 
less classical theorem, by Bonk and Schramm, asserting that a Gromov hyperbolic 
space embeds isometrically in a geodesic Gromov-hyperbolic space. As the 
original proof uses a transfinite sequence of Cauchy completions, this is an 
interesting formalization exercise. Along the way, we introduce basic material 
on isometries, quasi-isometries, Lipschitz maps, geodesic spaces, the Hausdorff 
distance, the Cauchy completion of a metric space, and the exponential on 
extended real numbers.


https://devel.isa-afp.org/entries/Gromov_Hyperbolicity.html

You will also need to pull from the Isabelle development repo.

Enjoy!



smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Tobias Nipkow]

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.azurewebsites.net/pubs/lamport-howtowrite.ps.Z


I think that is the one I meant. Don't worry, I am not suggesting we do it like 
that ;-)


Tobias


In the early Isar years I have actually studied both "How to write ..."
papers with some interest, but ended up ignoring most of the ideas.


Makarius





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Tobias Nipkow]

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 operator is. However, unless there is significant
support, I won't press for a uniform change.

- The issue of multiple line breaks in the current unparsing of long formulas
like _ + _ + _ + _ + _ + _ is independent and very annoying. I would be
surprised if we wanted anything but fill every line, not just the first or last
one as happens right now. A solution of that one would be much appreciated.

- I also noticed that "=" is still at the end of the line while "<=" and
friends are at the beginning. That is indeed inconsistent, also with
traditional notation. I agree with Larry and am strongly in favour of
changing that.

Tobias

On 11/01/2018 13:20, Lawrence Paulson wrote:

On 10 Jan 2018, at 21:26, Makarius  wrote:

The Haskell community appears to have picked up a lot of such (slightly
odd) styles from Lamport. E.g. they put commas at the start of the line
instead of the end, which is typographically very strange.

I was educated by the original TeX Book, which in turn refers to the
top-quality mathematical typesetting from around 1900. Here the
operators and commas are in the traditional position: end of line.


I got in the habit of putting arithmetic operators at the start of a line while 
at university, having made too many errors from forgetting that the symbol at 
the end of the previous line was a minus sign. Of course, that consideration 
doesn't apply to commas, and it's amazing that Lamport (and Dijkstra?) managed 
to persuade people to adopt such crazy conventions.

Interactive theorem proving isn't the same thing as solving physics problems by 
hand, so I'm not against having operators at the end of the line if that's what 
people think would be best. Note however that the equals sign is an infix 
operator and is invariably put at the start of a line, never at the end.

Larry





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Tobias Nipkow]

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" syntax), use option "-m".

In revision eab6ce8368fa


These are more changes than I expected, but even that is to be expected
with the wealth of material we have accumulated :-)


BTW, in the follow-up change a82df75b7f85 ("tuned notation") the special
breaks introduced by Larry in 1996 got lost:

changeset:   2006:72754e060aa2
user:paulson
date:Mon Sep 23 17:47:49 1996 +0200
files:   src/HOL/Ord.thy src/HOL/Set.thy
description:
New infix syntax: breaks line BEFORE operator


I did wonder if it had been done on purpose and toyed with the idea of 
consulting the history but the "uniformity" drive won. Thanks for keeping me 
honest. But I do wonder: shouldn't all infix operators be printed in the same 
manner? Having the operator on the new line in case of a break makes a lot of 
sense to me because it clearly how this line is connected with the previous one. 
[I seem to remember Lamport makes a similar point but it is not in his "How to 
write a proof".]


How about a uniform change to "breaks line BEFORE operator"?

Tobias



Larry has recently done analogous changes (e.g. bdf25939a550), so it
appears to be still the state-of-the art to have these exceptions in
pretty printing.


Makarius





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Tobias Nipkow]

* 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 based on regular expression matching,
the result may need a bit of manual postprocessing. 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" syntax), use option "-m".

In revision eab6ce8368fa



smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Tobias Nipkow]

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 following command:

isabelle jedit -l HOL-Analysis CV.thy

And then I get an alert box containing the appended text. Any idea what's going 
wrong here?

Larry

Cannot load theory file 
"/Users/lp15/isabelle/afp/devel/thys/Markov_Models/Probability.thy"
The error(s) above occurred for theory "Markov_Models.Probability"
(required by "Markov_Models.Markov_Models" via "Markov_Models.Markov_Models_Auxiliary") 
(line 9 of "/Users/lp15/isabelle/afp/devel/thys/Markov_Models/Markov_Models_Auxiliary.thy")
No such file: 
"/Users/lp15/isabelle/afp/devel/thys/Markov_Models/Probability.thy"
The error(s) above occurred in session "Markov_Models" (line 3 of 
"/Users/lp15/isabelle/afp/devel/thys/Markov_Models/ROOT")
[ line 12 of 
"/Users/lp15/isabelle/afp/devel/thys/Lambda_Free_KBOs/Lambda_Free_KBO_App.thy"] error: 
keyword "begin" expected,
but string was found:
"\t"


^
The error(s) above occurred for theory "Lambda_Free_KBOs.Lambda_Free_KBO_App"
(required by "Lambda_Free_KBOs.Lambda_Free_KBOs") (line 12 of 
"/Users/lp15/isabelle/afp/devel/thys/Lambda_Free_KBOs/Lambda_Free_KBOs.thy")
[ line 15 of 
"/Users/lp15/isabelle/afp/devel/thys/Lambda_Free_KBOs/Lambda_Free_KBO_Std.thy"] error: 
keyword "begin" expected,
but string was found:
"\t"


^
The error(s) above occurred for theory "Lambda_Free_KBOs.Lambda_Free_KBO_Std"
(required by "Lambda_Free_KBOs.Lambda_Free_KBOs" via 
"Lambda_Free_KBOs.Lambda_Free_KBO_Basic") (line 9 of 
"/Users/lp15/isabelle/afp/devel/thys/Lambda_Free_KBOs/Lambda_Free_KBO_Basic.thy")
[ line 16 of 
"/Users/lp15/isabelle/afp/devel/thys/Lambda_Free_KBOs/Lambda_Free_TKBO_Coefs.thy"] error: 
keyword "begin" expected,
but string was found:
">p"


^
The error(s) above occurred for theory "Lambda_Free_KBOs.Lambda_Free_TKBO_Coefs"
(required by "Lambda_Free_KBOs.Lambda_Free_KBOs") (line 12 of 
"/Users/lp15/isabelle/afp/devel/thys/Lambda_Free_KBOs/Lambda_Free_KBOs.thy")
The error(s) above occurred in session "Lambda_Free_KBOs" (line 3 of 
"/Users/lp15/isabelle/afp/devel/thys/Lambda_Free_KBOs/ROOT")
Cannot load theory file 
"/Users/lp15/isabelle/afp/devel/thys/MFMC_Countable/Probability.thy"
The error(s) above occurred for theory "MFMC_Countable.Probability"
(required by "Probabilistic_While.While_SPMF" via "MFMC_Countable.Rel_PMF_Characterisation" via 
"MFMC_Countable.Matrix_For_Marginals" via "MFMC_Countable.MFMC_Misc") (line 6 of 
"/Users/lp15/isabelle/afp/devel/thys/MFMC_Countable/MFMC_Misc.thy")
Cannot load theory file 
"/Users/lp15/isabelle/afp/devel/thys/Probabilistic_While/Probability.thy"
The error(s) above occurred for theory "Probabilistic_While.Probability"
(required by "Probabilistic_While.Bernoulli") (line 8 of 
"/Users/lp15/isabelle/afp/devel/thys/Probabilistic_While/Bernoulli.thy")
No such file: 
"/Users/lp15/isabelle/afp/devel/thys/MFMC_Countable/Probability.thy"
No such file: 
"/Users/lp15/isabelle/afp/devel/thys/Probabilistic_While/Probability.thy"
The error(s) above occurred in session "Probabilistic_While" (line 3 of 
"/Users/lp15/isabelle/afp/devel/thys/Probabilistic_While/ROOT")
Cannot load theory file 
"/Users/lp15/isabelle/afp/devel/thys/Probabilistic_System_Zoo/Probability.thy"
The error(s) above occurred for theory "Probabilistic_System_Zoo.Probability"
(required by "Probabilistic_System_Zoo.Probabilistic_Hierarchy") (line 5 of 
"/Users/lp15/isabelle/afp/devel/thys/Probabilistic_System_Zoo/Probabilistic_Hierarchy.thy")
No such file: 
"/Users/lp15/isabelle/afp/devel/thys/Probabilistic_System_Zoo/Probability.thy"
The error(s) above occurred in session "Probabilistic_System_Zoo" (line 3 of 
"/Users/lp15/isabelle/afp/devel/thys/Probabilistic_System_Zoo/ROOT")
Cannot load theory file 
"/Users/lp15/isabelle/afp/devel/thys/Randomised_Social_Choice/Probability.thy"
The error(s) above occurred for theory "Randomised_Social_Choice.Probability"
(required by "Randomised_Social_Choice.Randomised_Social_Choice" via 
"Randomised_Social_Choice.SDS_Lowering" via "Randomised_Social_Choice.Social_Decision_Schemes") 
(line 13 of "/Users/lp15/isabelle/afp/devel/thys/Randomised_Social_Choice/Social_Decision_Schemes.thy")
No such file: 
"/Users/lp15/isabelle/afp/devel/thys/Randomised_Social_Choice/Probability.thy"
The error(s) above occurred in session "Randomised_Social_Choice" (line 3 of 
"/Users/lp15/isabelle/afp/devel/thys/Randomised_Social_Choice/ROOT")
Cannot load theory file 
"/Users/lp15/isabelle/afp/devel/thys/Quick_Sort_Cost/Probability.thy"
The error(s) above occurred for theory "Quick_Sort_Cost.Probability"
(required by "Quick_Sort_Cost.Randomised_Quick_Sort") (line 10 of 
"/Users/lp15/isabelle/afp/devel/thys/Quick_Sort_Cost/Randomised_Quick_Sort.thy")
No such file: 

Re: [isabelle-dev] NEWS: document_tags

[Tobias Nipkow]

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 ('section', 'text' etc.) are implicitly
tagged as "document" and visible by default. This avoids the application
of option "document_tags" to these commands.


Thanks for this. Just a bit of context info: this simplifies the creation of 
documents where only a few key parts of a theory are shown (eg main definitions 
and thms). This in turn can be used to produce readable documentation for large 
sessions (like HOL-Analysis).


Tobias



This refers to Isabelle/386a31d6d17a.

An example session is attached.


Makarius



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





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Tobias Nipkow]

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 without risking its integrity is
a struggle now carrying on twelve years.

The key question to me is whether the integers in the archives (the ML
files) are actually used for numeric calculation (+, *, …) or are just
mere identifiers (=, maybe <).  In the latter case there are a couple of
possibilities not explored so far.


They are just identifiers and I don't think they are computed with. However, I 
don't intend to change formalization beyond a global implementation of int by 
some fixed size integers, if that can be done easily. Otherwise we live with the 
increase in runtime from 7:20 to 8:20.


Tobias


Cheers,
Florian





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Tobias Nipkow]

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 it could become faster with Poly/ML 5.7.1
than with 5.6.


Just as for Isabelle itself, I don't want generated code to abort with
overflow or even worse to overflow silently.


I also don't want to see FixedInt used routinely instead of proper
mathematical Int.

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.


Then I misunderstood. An optional use of FixedInt for languages where overflow 
raises an exception is fine with me.



If the answer is "no", I personally don't mind. Flyspeck-Tame runs
de-facto only in background builds: 1-2h more or less does not matter so
much. Its classic runtime was actually 10h total, now we are at 7h.


In which case I would say that providing such an option should be balanced with 
the complexity it requires or introduces.


Tobias



Makarius





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Tobias Nipkow]

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 itself, I don't want generated code to abort with overflow 
or even worse to overflow silently.


Tobias



smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Tobias Nipkow]

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 big applications in AFP. E.g. see
http://isabelle.in.tum.de/devel/build_status/AFP/index.html#session_CAVA_LTL_Modelchecker
(timing vs. ML timing).

I've shown this to David Matthews already and await his answer. It could
be just an accident in Poly/ML 905dae2ebfda or inherent due to the new
heap + GC management that is more robust against out-of-memory failures.


David Matthews has done a great job to improve this in Poly/ML
e8d82343b692 (see Isabelle/d0f12783cd80). It means that loading of
complex heap hierarchies is now faster than in Poly/ML 5.6.


Very nice indeed!

Tobias




Independently of that, excessive use of intermediate heap images makes
builds much slower than necessary, because multithreading is reduced by
the structural serialization. Here is a typical example:


Here is an updated test, on different hardware:

Isabelle/d0f12783cd80
AFP/88218011955a

ML_PLATFORM="x86_64-linux"
ML_HOME="/home/makarius/.isabelle/contrib/polyml-test-e8d82343b692/x86_64-linux"
ML_SYSTEM="polyml-5.7.1"
ML_OPTIONS="--minheap 3000 --maxheap 16000"

$ isabelle build -o threads=6 -d '$AFP' -f Linear_Recurrences_Test
Finished Pure (0:00:19 elapsed time, 0:00:19 cpu time, factor 0.97)
Finished HOL (0:03:48 elapsed time, 0:11:11 cpu time, factor 2.93)
Finished HOL-Library (0:02:05 elapsed time, 0:08:49 cpu time, factor 4.24)
Finished HOL-Computational_Algebra (0:01:05 elapsed time, 0:02:44 cpu
time, factor 2.50)
Finished HOL-Algebra (0:01:44 elapsed time, 0:04:23 cpu time, factor 2.53)
Finished JNF-HOL-Lib (0:00:14 elapsed time, 0:00:23 cpu time, factor 1.58)
Finished JNF-AFP-Lib (0:01:36 elapsed time, 0:06:37 cpu time, factor 4.13)
Finished Jordan_Normal_Form (0:04:47 elapsed time, 0:13:25 cpu time,
factor 2.80)
Finished Subresultants (0:01:01 elapsed time, 0:02:33 cpu time, factor 2.48)
Finished Pre_BZ (0:01:31 elapsed time, 0:05:35 cpu time, factor 3.66)
Finished Berlekamp_Zassenhaus (0:02:29 elapsed time, 0:07:41 cpu time,
factor 3.09)
Finished Pre_Algebraic_Numbers (0:00:32 elapsed time, 0:01:06 cpu time,
factor 2.06)
Finished Algebraic_Numbers_Lib (0:01:25 elapsed time, 0:03:44 cpu time,
factor 2.62)
Finished Linear_Recurrences (0:00:43 elapsed time, 0:01:22 cpu time,
factor 1.88)
Finished Linear_Recurrences_Test (0:02:15 elapsed time, 0:07:49 cpu
time, factor 3.46)
0:26:13 elapsed time, 1:17:50 cpu time, factor 2.97

$ isabelle build -o threads=6 -o timeout_scale=4 -d '$AFP' -f
Linear_Recurrences_Test
Finished Pure (0:00:19 elapsed time, 0:00:18 cpu time, factor 0.97)
Finished HOL (0:03:52 elapsed time, 0:11:22 cpu time, factor 2.93)
Finished Linear_Recurrences_Test (0:12:02 elapsed time, 0:52:56 cpu
time, factor 4.40)
0:16:42 elapsed time, 1:04:38 cpu time, factor 3.87


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] AFP statistics

[Tobias Nipkow]

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 further statistics that I use for talks.


Concerning growth of articles. I am not sure we want to provide more finegrained 
statistics for every entry, but attached you find a summary slide. I cannot 
remember precisely what is measured, but at a first approximation it tells us 
that over time every second line of an AFP entry is modified.


Tobias

On 28/09/2017 14:02, Makarius wrote:

The AFP statistics https://www.isa-afp.org/statistics.html is very nice
-- I often show the last diagram in presentations, as a proof of success
of Isabelle as application platform over the years.

Who is actually responsible for this tool?

Is there a chance to take into account how AFP entries evolve over time?
Right now, it only shows the year of first appearance with the *current*
size. Thus incrementally added sources (or whole sessions) are
attributed to the wrong year.

A prominent example is JinjaThreads, but newer entries like
Ordinary_Differential_Equations have grown significantly, too.


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev



slides.pdf
Description: Adobe PDF document


smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Time

[Tobias Nipkow]

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 that as follows:

changeset:   66558:37b16f8af351
tag: tip
user:wenzelm
date:Wed Aug 30 22:48:50 2017 +0200
files:   src/Pure/General/mercurial.scala
description:
faster check for non-repository, especially relevant for find_repository
to avoid repeated invocation of "hg root";


A more profound approach to speed up repeated document builds works via
Isabelle/jEdit and the Console/Scala plugin.

The invocation of "isabelle build" within that already running Scala/JVM
environment works like this:

   Build.build(PIDE.options.value, new Console_Progress, select_dirs =
List(Path.explode("~/Slides/Curry-Club_Aug-2017")))

The second, third, ... run will be much faster.


That direct use of the Scala function also bypasses the repository
check, because check_unknown_files = false by default.

See also
http://isabelle.in.tum.de/repos/isabelle/file/37b16f8af351/src/Pure/Tools/build.scala#l342


Makarius





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] Time

[Tobias Nipkow]

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
"HOL-Library"
  theories
10 theories either local or in ~~/src/HOL

session B = A +
  theories
  ...
  document_files
  ...

None of my files are part of a Mercurial repository.

I start with building A:

isabelle build -v -d . A

It takes 6 secs until the build of A actually starts.

From now on I will always build B.

I start with an almost empty B: 0 theories and no document_files section.
It takes 6 secs before it starts the run.

Now I add a document_files section with 4 small (less than 3k each) tex files.
It takes 8 secs before it starts the run.

Now I add 8 pdf files of 70k each.
It takes 15 secs before it starts the run.

Now I add 10 theories that only import files that are part of session A.
It takes 22 secs before it starts the run.

All of this is linear: the more files I add, the longer it takes. In
Isabelle2016-1 it took 2 secs.

I have intentionally not included anything from the AFP. However, importing
an AFP session does not seem to make matters worse (although adding -d '$AFP'
to isabelle jedit does add 20 secs startup time.)

What am I doing wrong? How can I speed things up?

Thanks
Tobia



smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Tobias Nipkow]

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
library?

lemma lex_append_right:
   "(xs, ys) ∈ lex r ⟹ length vs = length us ⟹ (xs @ us, ys @ vs) ∈ lex r"
   by (force simp: lex_def lexn_conv)

lemma lex_append_left:
   "(ys, zs) ∈ lex r ⟹ (xs @ ys, xs @ zs) ∈ lex r"
   by (induct xs) auto

lemma lex_take_index:
   assumes "(xs, ys) ∈ lex r"
   obtains i where "i < length xs" and "i < length ys" and "take i xs =
take i ys"
 and "(xs ! i, ys ! i) ∈ r"
proof -
   obtain n us x xs' y ys' where "(xs, ys) ∈ lexn r n" and "length xs =
n" and "length ys = n"
 and "xs = us @ x # xs'" and "ys = us @ y # ys'" and "(x, y) ∈ r"
 using assms by (fastforce simp: lex_def lexn_conv)
   then show ?thesis by (intro that [of "length us"]) auto
qed

cheers

chris
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Tobias Nipkow]

Indeed, and that is consistent with informal language, eg "sorted by size". It 
looks like "wrt" is really better for relations.


Tobias

On 16/08/2017 17:04, Peter Lammich wrote:
However, sort_by takes a function mapping the elements into a linear order, 
which is less general 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/08/17 16:10, Tobias Nipkow wrote:
 >
 > 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.

In Isabelle/ML we used to have "sort_wrt" for some decades, but I have
changed that recently into into "sort_by" to make it coincide with the
terminology of the Scala library.

See
http://isabelle.in.tum.de/repos/isabelle/rev/610794dff23c


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Tobias Nipkow]

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 wrote:

Dear all,

speaking of "chain", for me the main motivation of introducing "linked
P" was in order to work well together with the corresponding
generalizations of "take_while" and "drop_while", which are called
"take_chain" and "drop_chain" in the AFP entry Efficient-Mergesort.


E.g., "take_chain (op >) [3,2,1,2] = [3,2,1]"

So besides very basic lemmas about "linked" (concerning append) there
are some concerning its interaction with "take_chain" and "drop_chain"
in Efficient_Sort.thy

chris

PS: another alternative name: "sorted_by" (I think the suffix "_by" is
far more common -- e.g., in Haskekll -- than "_wrt").

On 08/16/2017 11:53 AM, Blanchette, J.C. wrote:

Hi Christian, Tobias,


I think your "sorted_wrt" is almost (modulo "fun" vs. "inductive") my
"linked" from the AFP (Efficient_Mergesort).


https://www.isa-afp.org/browser_info/current/AFP/Efficient-Mergesort/Efficient_Sort.html

Maybe we could unify the constants/names somehow?

At the moment I somewhat prefer "linked" (or maybe "linked_by") since
sortedness implies that "P" is some kind of order, which it doesn't have
to be.


It also reminds me of my "derivation" predicate, which arose when formalizing 
Bachmair & Ganzinger's chapter in the Handbook of Automated Reasoning:

https://bitbucket.org/isafol/isafol/src/f0f585fb6cbd7097567cc1c493fe1b3c1223a8da/Bachmair_Ganzinger/Proving_Process.thy?at=master=file-view-default

It's a bit different because of the use of lazy lists (to allow infinite 
derivations) and the different handling of the empty list.

Underlying all of these appears to be the concept of a "chain". That's what we often call things of the form 
x1 > x2 > ... > xn (finite) or x1 > x2 > ... (infinite), where > is some binary relation. In the 
context of Bachmair & Ganzinger, or, indeed, for formalzing Definition 7.2.3 from Baader & Nipkow, it makes 
sense to use a relation > that is not transitive.

So maybe "chain" could be a good name for the finite concept?

Incidentally, Georges Gonthier believes that for nonempty paths in a graph (or 
more generally chains), the first element should be stored separately from the 
other ones. I guess the main benefit is when concatenating two paths, he can 
simply append. I'm not sure how relevant it is to us, though.

Jasmin

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


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





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Tobias Nipkow]

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.


Tobias

On 16/08/2017 10:44, Christian Sternagel wrote:

Dear Tobias,

I think your "sorted_wrt" is almost (modulo "fun" vs. "inductive") my
"linked" from the AFP (Efficient_Mergesort).


https://www.isa-afp.org/browser_info/current/AFP/Efficient-Mergesort/Efficient_Sort.html

Maybe we could unify the constants/names somehow?

At the moment I somewhat prefer "linked" (or maybe "linked_by") since
sortedness implies that "P" is some kind of order, which it doesn't have
to be.

kind regards,

chris


 Forwarded Message 
Subject:added sorted_wrt to List; added 
Data_Structures/Binomial_Heap.thy
Date:   Tue, 15 Aug 2017 19:47:08 +0200
From:   nipkow <>



added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy added
sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Tobias Nipkow]

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 qualified. In
my opinion, there is no question that "compact" should be "compact" in
the topological sense.


Yes, that's a no-brainer. I expect Andreas (the author) will not mind hiding or 
renaming that "compact" in the most appropriate way.


Tobias



smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Tobias Nipkow]

On 30/06/2017 16:39, Manuel Eberl wrote:
I do understand that argument, but I am not sure if Topological_Spaces.subseq is 
really used /that/ often. Actually, going one step further, it is nothing more 
than "strict_mono" restricted to "nat ⇒ nat", so one may well argue that it is 
superfluous anyway.


If we can get rid of it all together, surely that is the best option?

Tobias

The possibility of renaming one of them to "subsequence" or "is_subseq" is, in 
my opinion, not a satisfactory solution, since we would then /still/ have two 
completely different constants with essentially the same name, just with an 
arbitrary artificial difference. We might as well call one of them subseq'.


The advantage of qualified names is that they really allow us to add 
disambiguating context to ambiguous names when necessary, e.g. something like 
"List.subseq" and "Topological_Spaces.subseq". Still, as I said, I do understand 
that typing such lengthy names is tedious.


I currently see the following possible solutions:

– find another good name for one of the two things currently named "subseq" and 
rename it

– introduce an arbitrary distinction like "subsequence" or "is_subseq"
– move "subseq" to List.thy and make it qualified, so that one must write 
"List.subseq"

– remove Topological_Spaces.subseq entirely, replacing it by strict_mono
– leave everything 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 Nipkow wrote:
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 18:49, Manuel Eberl <ebe...@in.tum.de 
<mailto:ebe...@in.tum.de>> wrote:


Yes, I noticed that as well. I decided to leave it that way since, well,
we do have qualified names.




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





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




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





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Tobias Nipkow]

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 18:49, Manuel Eberl > wrote:


Yes, I noticed that as well. I decided to leave it that way since, well,
we do have qualified names.




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





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Tobias Nipkow]

Another possibility is to call one of them is_subseq.

Tobias

On 30/06/2017 08:17, Andreas Lochbihler wrote:

Hi Manuel,

Well, how about changing Sublist.subseq to Sublist.subsequence? And accordingly 
strict_subseq to strict_subsequence or ssubsequence?


Andreas

On 28/06/17 19:49, Manuel Eberl wrote:

Yes, I noticed that as well. I decided to leave it that way since, well,
we do have qualified names.

If anybody has better suggestions, I am open to implementing them.

Manuel


On 2017-06-28 17:05, Andreas Lochbihler wrote:

Dear all,

While porting some of my theories to the current development version,
I've just noticed that the renaming of sublisteq to subseq done by
Manuel in May (639eb3617a86) has one bad effect:

The name subseq is already used in Topological_Spaces to formalise the
concept of a subsequence. This name is now hidden by the definition in
Sublist, in particular 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 "sublist" (for
the contiguous case) and "subseq" (for the general case) and think we
should adopt it.

[Then we would rename sublisteq -> subseq and sublist :: "'a list ⇒
nat set ⇒ 'a list" (in List) to something else, eg sublist_index)

Tobias

On 25/05/2017 21:13, Jasmin Blanchette wrote:



On 25.05.2017, at 20:41, Tobias Nipkow <nip...@in.tum.de> wrote:

I don't think that sublist, subsequence and substring really have
much of a bias in either direction, except possibly substring, but
the latter does indeed sound too specialized.


Wikipedia has a clear bias (and I did not edit it, nor did I look it
up before writing my previous email):

 https://en.wikipedia.org/wiki/Subsequence
 https://en.wikipedia.org/wiki/Substring

Popular algorithm sbooks like Cormen et al. follow the same
definition of subsequence. Standard expressions like "longest
increasing subsequence" depend on this semantics.

As for sublist, all the examples I see by Googling either "sublist",
"is_sublist", "isSublist", or "indexOfSubList" in Java, Python,
Scala, etc., have the contiguous semantics. Including this page:

 http://www4.in.tum.de/lehre/praktika/psv/psv98/Vorlesung5/aufg4.html

I'm not saying we should rename the Isabelle concepts, just that
Isabelle is the odd (wo)man out.

Jasmin




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

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


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




smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Issue in AFP

[Tobias Nipkow]

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 also 
/srv/data/tum/isabelle/master/heaps/polyml-5.6_x86-linux/log/JinjaThreads)
***(\T.
***typeof\<^bsub>h\<^esub> v =
***\T\ \
***(\C.
***class_type_of' T =
***\C\ \
***(\Ts Tr D.
***  P \ C sees M: Ts\Tr = Native in D \
***  \external_defs D M
***then (\red0t (extTA2J0 P) P t h
***   (Val v\M(es), xs)
***   (Val v\M(es'), xs') \
***  countInitBlock (Val v\M(es1'))
***  < countInitBlock (Val v\M(es1)) \
***  Val v\M(es') =
***  Val v\M(es) \
***  xs' = xs) \
*** h' = h \
*** ta1 = \\ \
*** ta = \\
***else ta_bisim01 ta (extTA2J1 (compP1 P) ta1) \
*** (if call (Val v\M(es)) = None \
*** call1 (Val v\M(es1)) = None
***  then \e'' xs''.
***  \red0r (extTA2J0 P) P t h
*** (Val v\M(es), xs) (e'', xs'') \
***  extTA2J0
*** P,P,t \ \e'',(h, xs'')\ -ta\
***\Val v\M(es'),(h', xs')\ \
***  no_call P h e'' \
***  \ \move0 P h e''
***  else extTA2J0
***P,P,t \ \Val
***   v\M(es),
***  (h, xs)\ -ta\
*** \Val v\M(es'),(h', xs')\ \
***   no_call P h (Val v\M(es)) \
***   \ \move0 P h
*** (Val v\M(es
*** At command "apply" (line 911 of 
"/srv/data/tum/afp/master/thys/JinjaThreads/Compiler/Correctness1.thy")


Any hint what is going on?

Cheers,
Florian



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





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Tobias Nipkow]

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 file, 
that is a misunderstanding. I wasn't sure what had happened and merely brought 
to your attention the jenkins report. I didn't include any remark about the 
importance of not breaking the distribution.


Jenkins is giving me better coverage than before, which is what we wanted. If 
something does not work anymore and has to be worked around, it can hardly be 
the effect of an additional test system.


Tobias



smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Tobias Nipkow]

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 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
"/media/data/jenkins/workspace/isabelle-repo-makeall/src/HOL/ROOT")
23:23:27 *** The error(s) above occurred in session "HOL" (line 3 of
"/media/data/jenkins/workspace/isabelle-repo-makeall/src/HOL/ROOT")


I did not see this, because Jenkins is not "The Isabelle regression test
system" and I am rarely looking what happens there -- I do look
sometimes after significant changes of Isabelle/Scala, because I have no
intention to destroy such experiments on purpose.

Concerning the status of Jenkins wrt. isabelle-dev (not isabelle-group
at TUM), we are still lacking a proper discussion of its purpose and
general approach. When I started to ask some critical questions last
year, I did not get any answers and was merely blamed for that.


If there is anybody *outside* the TUM group, who uses the Jenkins setup
regularly, it would be interesting to discuss some basic things. What is
good about it? What is bad about it?


Makarius





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Tobias Nipkow]

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 
"/media/data/jenkins/workspace/isabelle-repo-makeall/src/HOL/ROOT")
23:23:27 *** The error(s) above occurred in session "HOL" (line 3 of 
"/media/data/jenkins/workspace/isabelle-repo-makeall/src/HOL/ROOT")


Tobias

On 22/04/2017 13:13, Makarius wrote:

On 22/04/17 11:48, Jasmin Blanchette wrote:

I get the error

Bad theory import "Main"

Steps to reproduce the problem:

cd src/HOL/Library
isabelle jedit Cancellation.thy


Odd. I cannot reproduce this on Linux or macOS Sierra.

What is your $ISABELLE_HOME actually? Is there anything special with the
underlying file-system?

Here is an example for the Console/Scala toplevel within Isabelle/jEdit:

scala> PIDE.resources.session_base.known.files.toList.find(p =>
p._2.exists(_.theory == "Main"))
res0: Option[(java.io.File, List[isabelle.Document.Node.Name])] =
Some((/home/makarius/isabelle/repos/src/HOL/Main.thy,List(Main)))


What is your result?


Makarius

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





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Tobias Nipkow]

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 update the URLs in Jenkins shortly.

If you need to push but I forgot to add you, please mail me your
Bitbucket user name and I'll add you ASAP.

I hope that this is just a temporary workaround (famous last words, I
know ...).


lxbroy10 is back to normal, see the proof
http://isabelle.in.tum.de/repos/isabelle/rev/f3cd78ba687c



Indeed it is, thanks to the invaluable help of Franz Huber. However, he spoke of 
a workaround when he notified us and wasn't 100% certain it works reliably. I 
felt we should wait a few more days before we move the repo back, but I am easy 
either way.


Tobias


Makarius


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





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Tobias Nipkow]

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


Thanks for taking care of this.

I noticed a problem with lxbroy10 on Sunday evening and only sent a
short notice to the TUM admin group (without getting a reaction so far).

With more and more resources removed from this group, problems are to be
expected. They are doing there best, but we definitely feel the natural
consequences of the global "austerity policy".


Since Manfred Broy retired the resources he provided are not available anymore, 
not because of some evil austerity policy but because they went back to where 
they came from, the department, or because they were external funds to start with.


Tobias


I hope we get back on lxbroy10 soon.


Makarius

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





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Tobias Nipkow]

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 is ok". I could indeed not construct an example where a new 
incorrect result arises because of a caught over/underflow exception (only new 
ways to construct results that could already arise before). But that isn't 
exactly a proof (although the proposition may well be a thm).


Otherwise I agree with Makarius.

Tobias


MetiTarski, which during execution relies heavily on large integers,
nevertheless benefits to the tune of 30% to having all other integers
fixed-precision. During its execution, Isabelle makes very heavy use of small
integers, in the representation of bound variables and flexible variables, which
are renamed by having an offset before each and every resolution step.

We have spent a lot of time discussing problems caused by the cost of regression
testing, and now we have the possibility of reducing that by 30%.

As to changes in behaviour that could be caused by overflows, I checked:
exception Overflow is explicitly caught in only two places throughout the
sources, both in HOL decision procedures (and therefore well outside the kernel)
while the wildcard exception is caught in three places in Pure. No exception
handlers had to be added when I converted MetiTarski to use fixed integers. An
uncaught exception doesn’t prove anything, of course.

Larry


On 2 Nov 2016, at 14:43, Makarius > wrote:

On 02/11/16 15:30, Lawrence Paulson wrote:


I actually can’t think of many places where Isabelle would need large
integers, so it would probably benefit even more than MetiTarski does.


"Can't think of" merely indicates a lack of empirical tests, against the
Isabelle repository and AFP. Afterwards the situation usually looks
quite different, and the initial hypothesis needs to be changed.

When we moved to proper int by default some years ago, there were
several tool implementors approaching me, asking to be delivered from
the curse of many different "int" types.

We also have conceptual reasons to stay true to the concept of an
integer that is an integer, a string that is a string etc. -- and thus
not using a machine word instead of an integer, or a "char" type that
cannot hold a textual character (not even in Unicode). Isabelle/ML is
meant to be a programming environment free from bad jokes like that.


Nonetheless, I do think that proper use of machine words in isolated
situations can help, but they should not be called "int" and used by
default.


Makarius







smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Tobias Nipkow]

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 that if such 
an exception propagates out of the kernel, no incorrect theorems can arise 
(because control has left the kernel). However, in the presence of higher-order 
functions (e.g. user functions can be passed to kernel code) this is not so 
clear to me.


Tobias

On 02/11/2016 13:07, Lawrence Paulson wrote:

David Matthews is working on a new release of Poly/ML in which the default type 
of integers is fixed-precision. A configuration option can restore the former 
set up, but that might be a mistake: I modified MetiTarski to use large 
integers only where needed and saw runtime decrease by around 30%. We could do 
the same. I imagine that we need large integers almost nowhere. Now consider 
that every bound variable is represented internally by an integer.

Larry

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





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] AFP broken

[Tobias Nipkow]

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.

Legacy features usually have one or two release cycles, before the
feature is removed. It seems that few people care about that themselves,
so they need to be informed explicitly.


Another possible improvement for AFP checks:

  isabelle check_sources '$AFP_BASE'

This is available in Isabelle/Scala module Check_Sources.


Makarius




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





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Distro broken

[Tobias Nipkow]

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 email immediately after the
push, and the status page also indicated the failure. Automation working
as expected.


But that did not help. Florian experienced the broken repository just in
the way it occasionally happens.

The open question is if the massive use of CPU resources by Jenkins is
justified to deliver its service. It is still unclear to me what this
service is in the first place.

So far there were only axioms about Jenkins, but no proofs.


Makarius

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





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Jenkins maintenance

[Tobias Nipkow]

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 Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Jenkins maintenance

[Tobias Nipkow]

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 prefer to have AFP working all the time, but that would require
much more resources, both hardware and humans.


For a growing number of Isabelle users, the AFP is just as important as the 
Isabelle repository. Hence the AFP needs to be tested and maintained just as 
much, which requires (at least) the hardware resources that we provide; we 
cannot dedicate half of it to manual testing.


Leaving the AFP entries broken actually increases the human resources required 
to fix them later.



A broken Isabelle repository is different: it means all wheels stand
still.


Both for the repository and the AFP, everything is selective. Most people do not 
suffer if HOL-Proofs does not build, for example. Just as many AFP entries are 
irrelevant to most of us. But in the end we want all of it to work.


Tobias


That can be easily avoided by spending about 20min with manual
tests before pushing -- on decent hardware.

When the Isabelle repository is broken, which happens about 2 times per
year, there are friendly mails on isabelle-dev about it, mostly
reminders of README_REPOSITORY. Can you point out a mail thread, where
anybody was seriously blamed for it?



Another improvement I can think of is
that it would be good to have a little more control over testing:
aborting tests when they are not necessary anymore, testing only the
repository (and not the AFP) etc. All of this we can talk about and find
a solution in time.


Yes. I read it as: ssh access to a proper test machine. That is the
traditional Isabelle development model.

When the Prover IDE learns to use remote machines eventually, that will
also use ssh for direct interaction with jobs.



The reality of it all is that our testing infrastructure was in shambles for
quite some time. Then Lars came along and put in a lot of effort to get
things up and running again. The main response on this mailing list were
vague insinuations that he does not understand how to do tests, or does
not care about doing it properly, which could hardly be farther removed
from the truth.


I had many private discussions with Lars in the past few months. I even
pointed out important requirements before the start of the Jenkins project.

The present situation is that we have no proper test environment after
isatest was shutdown prematurely. This is what I have called "flying
blind", because vital performance measurements are missing.

I need to improvise something for the coming release -- which is the
reason why I have been off-line for some days, and also postponed the
start of the hot phase for Isabelle2016-1.


Makarius

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





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] not-exists problem

[Tobias Nipkow]

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. P (fst xy) (snd
xy).

If you were going to support ∃!x y at all (and I can certainly see
the argument for forbidding it outright), I'd expect it to map to the
first formula above, and not the second.


So there seems to be no consensus on the meaning of "∃!x y".

Btw: I would strongly argue that a proposition like
"∃!x y. x = abs (y::int)" is wrong, however it holds with the "∃!x.
∃!y"-semantics.

--
  Peter





Michael

On 13/09/2016, 18:41, "isabelle-dev on behalf of Tjark Weber"  wrote:

On Tue, 2016-09-13 at 09:45 +0200, Peter Lammich wrote:
> I would have expected:
> (∄x y. P x y) ⟷ ¬(∃x y. P x y)
> and
> (∃!x y. P x y) ⟷ (∃!xy. P (fst x) (snd x))

+1

Best,
Tjark


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/is
abelle-dev


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabel
le-dev

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





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] not-exists problem

[Tobias Nipkow]

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 Paulson wrote:

We have a problem with the ∄ operator, when existential quantifiers
are nested:

lemma "(∄x. ∃y. P x y) = (~(∃x y. P x y))"
  by (rule refl)


I do not see a particular problem with this, however, not-exists and
also exists-one have funny semantics when used with multiple
variables:

lemma "(∄x y. P x y) ⟷ ¬(∃x. ¬(∃y. P x y))"
by (rule refl)

lemma "(∃!x y. P x y) ⟷ (∃!x. (∃!y. P x y))"
by (rule refl)

this leads to funny lemmas like:

lemma not_what_you_might_think: "∄x y. x+y = (3::int)"
  by presburger

lemma also_strange: "∃!x y. x = abs (y::int)"
  by (metis (no_types, hide_lams) abs_0_eq abs_minus_cancel
equal_neg_zero)


I would have expected:
(∄x y. P x y) ⟷ ¬(∃x y. P x y)
and
(∃!x y. P x y) ⟷ (∃!xy. P (fst x) (snd x))



We should either forbid multiple variables on those quantifiers, or try
to figure out whether there is a widely-accepted consensus on their
meaning.

--
  Peter




Note that ∄x y. P x y would be fine.

Larry

~/isabelle/Repos/src/HOL: hg id
dca6fabd8060 tip

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabel
le-dev

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





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] NEWS: split!

[Tobias Nipkow]

* 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 applies
safe introduction and elimination rules after each split rule.
As a result the subgoal may be split into several subgoals.

If you have long-running simp or auto calls in situations with a number of if 
and case expressions, split! could help. If you find it does, drop me a line, 
thanks.


Tobias

In f8e79d14d61f.



smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Tobias Nipkow]

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 problems in
Isabelle several times lately, usually sporadically and irreproducibly.


On my laptop this happens fairly reliably for some time now with HOL-Proofs or 
related sessions. I played around with PolyML parameters, but to no avail.


Tobias


Perhaps the times when 32 Bit Isabelle was enough for all applications are
indeed over.


Cheers,

Manuel


On 08/08/16 13:06, Makarius wrote:

On 08/08/16 11:14, Lars Hupel wrote:

the latest build failure for the repository is spurious:

*** exception Fail raised (line 83 of "./basis/PolyMLException.sml"):
Insufficient memory

This happened in HOL-Proofs.

I have tried Isabelle/1e7c5bbea36d once again with

  ML_PLATFORM="x86-linux"
  ML_HOME="/home/makarius/.isabelle/contrib/polyml-5.6-1/x86-linux"
  ML_SYSTEM="polyml-5.6"
  ML_OPTIONS="-H 1000 --gcthreads 2"

The result is:

Finished HOL-Proofs (0:17:18 elapsed time, 0:33:38 cpu time, factor 1.94)


Is the test hardware in an air-conditioned server room? Otherwise we
might be actually testing the surrounding temperature or some other
environmental effects.



Makarius, it may or may not be connected to
the recent changes you did in proof reconstruction (994d1a1105ef).

This is merely for printing, which normally does not happen at all.


Makarius

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




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





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Multiset insert

[Tobias Nipkow]

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
instance of the plus type classes, i.e., occupying the name
plus_multiset.


I think that the type clarifies the difference. If this is a real concern, one 
could go for "add1" instead of "add". Since Jasmin and Mathias have been working 
with and on multisets a lot, they are in a good position to judge which 
alternative works better.


Tobias


--
  Peter




Lovely!

Jasmin

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



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





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Multiset insert

[Tobias Nipkow]

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 definition like

insert_mset x M = {#x#} #∪ M


You have a point. I didn't even realize that we have #∪.


i.e. with #∪ instead of +. How about "add"?

add x M = {#x#} + M

Or "add1"? Or "add_mset" etc.?


I am all in favour of a variation of "add" - it corresponds nicely to "+". Of 
course not "add" by itself, that is too generic. How about


definition add_mset :: "'a ⇒ 'a multiset ⇒ 'a multiset" ("add#") where
"add# x M = {#x#} + M"

Tobias


Jasmin

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





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: Primes

[Tobias Nipkow]

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

* Probability: Code generation and QuickCheck for Probability Mass
Functions.



As for the former: There are now three new algebraic predicates:

- "irreducible", i.e. irreducible elements in a ring (cannot be decomposed into
two non-unit factors)
- "is_prime_elem", i.e. p is a prime element if for all x,y where p divides x *
y, it also divides x or y
- "is_prime" if p is a prime element and it is normalised

For instance, the integer "-3" is a prime element, but not a prime. This
corresponds nicely to the concept of a "prime number" on the integers. W.r.t.
the old definitions.

The "is_prime" predicate is necessary because normalisation is necessary for
some things, such as a unique prime factorisation.

The old "prime" constant is now a mere abbreviation for "is_prime" and can
perhaps be discontinued in the next version. This is not necessarily the final
naming scheme; I am open to better suggestions.


As a side note, there is a lot of material in this that subsumes material in
some AFP entries, most notably the "Algebraic Numbers" group by Thiemann et al.


Cheers,

Manuel
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev




smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Multiset insert

[Tobias Nipkow]

No, we keep talking about it (internally), but nobody at TUM has done anything 
about it. It would be great if you want to take this on. It is potentially 
tedious because there are many existing uses of multisets.


Did we ever discuss the naming issue? "insert_mset" would be the canonical name, 
but it would make larger expressions hard to read.


Tobias


On 26/07/2016 13:59, Mathias Fleury wrote:

Hello all,

(Relaunching this nearly-one-and-a-half-years-old thread.)


Before I start working on it, has anyone already done some work towards adding 
insert_mset?


Thanks,
Mathias


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 union. Although induction already has only two cases (empty and union with singleton), it would 
be nicer to have only two constructors, like for finite sets: empty and insert. In particular, this often 
avoids the use of ac_simps for union because representations are more canonical. The singleton constructor 
would be retained as an abbreviation for "insert_mset _ {#}" but "M + {#x#}" would be 
simplified to "insert_mset x M", like for sets.

Any views?

Tobias

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


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


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





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] multiplicity and prime numbers

[Tobias Nipkow]

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 changes, we had the
concept of "multiplicity". This was defined to be the multiplicity of a prime
factor in the prime decomposition of a natural number or an integer. The
multiplicity of a non-prime was defined to be 0.

I have now created an alternative definition of "multiplicity" which is simply
defined as "the highest power that is still a divisor" (as long as this is
well-defined); e.g. the multiplicity of -4 in 64 would be 3.

I see three possibilities:
1. redefine my "new", more general multiplicity to the "old" multiplicity
2. keep both notions of multiplicity around with different names
3. replace the old multilicity with the new one and adapt all lemmas accordingly

Currently, I tend towards the last options. Are there any other opinions on 
this?


Cheers,

Manuel
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev




smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] \nexists

[Tobias Nipkow]

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 documents in
every single point of history. When there is something wrong with Latex,
it is usually easy to repair afterwards.

Asking everybody to test Latex every time imposes a burden with little
benefit.

In contrast, a full "build -a" for the formal content is vital. The
shorter that takes, the more it becomes second nature to do it
frequently -- I often do it for every single changeset (before the local
commit).


Your notion of what is good for developers differs from their own notion, at 
least for the ones I talked to. But it turns out you are right: combining -a and 
-o document=pdf is not a good idea, it breaks Logics_ZF.


Tobias



The current Isabelle Jenkins setup has changed focus slightly. There are
more continuously built "artifacts", like documents, but important
"telemetry" data visualization is missing. So we are flying blind
concerning performance figures, not just for AFP (as we do for many
years), but also for the main repository.

What is really needed now, is a replacement for
Admin/isatest/isatest-statistics.

That also depends on good physical measurements: that was historically
done without Latex getting in between.


Makarius





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] \nexists

[Tobias Nipkow]

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 minute counts in the routine tests that I run continuously all the
time. We are in fact again above 30min for "isabelle build -a" for my 12
core machine, which is where the pain starts.


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?


Tobias


Latex tests add very little information for the extra time. It is
usually easy to figure out what needs to be done to make a broken
document work again. Moreover, the test often fails because of bad latex
installations, not because of bad documents.


This old problem has come back on us now, because the Jenkins test
always produces documents -- and thus a lot of mails if something is
broken there.

Latex should be tested occasionally, but it could be done in a less
intrusive manner. E.g. only once a day or once week.


Makarius

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





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] \nexists

[Tobias Nipkow]

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 sequence.
 \nexists

The corresponding source line is here:

Multivariate_Analysis/Brouwer_Fixpoint.thy:have nog: "\g.
continuous_on (S \ connected_component_set (- S) a) g \

What’s unfortunate is that the “negated exists” quantifier is available both for
input and output in Isabelle, just not as a TeX macro.

I’ve pushed a fix. However, ideally this macro should be defined somehow and my
change reverted.

Larry


This body part will be downloaded on demand.





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] NEWS

[Tobias Nipkow]

* 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: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Tobias Nipkow]

Florian,

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

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

[Tobias Nipkow]

The problem with {..

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

[Tobias Nipkow]

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 constructor there is at most *one*
instance.

If we use the standard HOL class hierarchy for HOLCF, we
would e.g. enforce the order on pairs to be component-wise due to the
required / given instance of cpo in HOLCF and hence rule out e.g.
lexicographic ordering on pairs.  Hence the use of a separate
type class hierarchy makes sense for that specific application.


You are saying that the problem is the ordering which would be shared, which is 
why we use "⊑" in HOLCF rather than "<=".


But that argument applies to any instantiation of the order on products. That 
is, any application that instantiates the product order should therefore not use 
the generic "<="? Probably not if it is a development that is supposed to be the 
basis for many others, like HOLCF?


So maybe the deeper reason is indeed the usual problem with type classes, in 
which case I would support the plain ASCII "LUB".


Tobias


Cheers,
Florian





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Tobias Nipkow]

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 lot about upper / lower bounds
which is not HOLCF-specific in any way, so it could go to HOL/Library
for example.


After a closer look I came to conclusion that the use of Sup syntax in
HOLCF/Porder.thy is very application-specific.  And it is a deliberate
separate type class hierarchy since these type classes are tailored
towards continuous function space.

So maybe the best option here is to stay with plain ASCII syntax: ‹LUB
x∈A. f x›. – to emphasize its somewhat specific application.


The lub operation in is a lattice-theoretic supremum. So in principle we should 
be able to use operator names and syntax for that; otherwise there is something 
wrong (or maybe our type classes are inadequate).


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.


Tobias


Cheers,
Florian



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





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Nonterminating AFP build

[Tobias Nipkow]

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 11:39, Lawrence Paulson  wrote:

It has no timeout, sorry, that was my fault. Now set to 300 seconds.

We don’t need a global timeout, but why not a default timeout? We could set up 
to the median runtime. Actually I think our typical value of 600 seconds is 
much too high, considering that a loop in a common library could make dozens of 
entries run forever.
Larry


On 11 May 2016, at 23:58, Gerwin Klein  wrote:

If it doesn’t have a timeout set, then that’s a mistake and should be fixed. 
It’d be good to have protection for all builds, not only through Jenkins.

We’ve avoided a global timeout so far, because it’d have to be fairly long, 
i.e. if you have a few entries that don’t terminate because of a change in 
Isabelle for instance, you might very quickly be looking at multiple days.

Might still be a good idea to add one anyway as an additional safety net.

Cheers,
Gerwin




On 12.05.2016, at 06:58, Lars Hupel  wrote:

Isabelle/8326aa594273
AFP/ffea2c11f257

We appear to have an issue with nonterminating builds. See here:
.
I had to manually kill the running poly process. I'm not quite sure
which session causes it, but it's possibly Randomised_Social_Choice. I
was under the assumption that all AFP sessions had timeouts set –
apparently this is not the case.

In order to avoid these problems in the future, I'll implement job
timeouts in Jenkins.

Cheers
Lars
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev





The information in this e-mail may be confidential and subject to legal 
professional privilege and/or copyright. National ICT Australia Limited accepts 
no liability for any damage caused by this email or its attachments.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev




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





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Tobias Nipkow]

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 that syntax is attached
to are members of syntactic type classes.  It could be worth to attempt
to make that syntax standard, using funny subscripts or similar for the
more exotic cases.


Florian, what are the more exotic cases?

Tobias


Cheers,
Florian



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





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Explicit representation of multisets

[Tobias Nipkow]

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 proofs. If we 
want to mimic sets, it actually seems unavoidable...


Tobias

On 10/03/2016 10:53, Florian Haftmann wrote:

Hi all,

in recent private discussion the question was raised whether the
explicit representation of multisets should follow that of sets.

For sets, we have:
{a, b, c} = insert a (insert b (insert c empty))

For multisets, we currently have:
{#a, b, c#} = single a + single b + single c

But the following would also be possible:
{#a, b, c#} = insert# a (insert# b (insert# c empty#))

Is there any evidence that we should not attempt this?

Cheers,
Florian



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





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Tobias Nipkow]

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 all-capitalized (SUP,
INF, UNION, INTER, THE, LEAST, SUM, PROD).

On the other hand nearly all those binders have pretty symbolic syntax,
such that the all-capitalized variants rarely show up in theory text.
Since there is no generally accepted symbolic syntax for gcd, it might
be better to let the (slightly more readable) form (a) stand.

I have no strong opinion on this.  Any suggestions?

Cheers,
Florian



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





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Tobias Nipkow]

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: (* should become standard syntax once x-symbols supports it *)


I wrote that comment and am still in favour.

Tobias


Proof General Emacs and the X-Symbol package no longer exist, and the
terminology of "x-symbols" is long-forgotten, but we have proper means to
introduce notation that works unconditionally in the Prover IDE and document
output:

abbreviation Not_Ex :: "('a ⇒ bool) ⇒ bool"  (binder "∄" 10)
   where "∄x. P x ≡ ¬ (∃x. P x)"


Trying this with find_theorems in HOL Main or Library shows relatively few
occurrences, so it is likely not to cause great confusion.

There is a conflict with old "HOL" print mode, though. It causes a mixture of "!
" and "? " versus "∄" in output. I can't imagine anybody using that print mode
seriously, so maybe it is time to make these syntax variants input-only, as a
preparation for removal at a later point.


 Makarius


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





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Tobias Nipkow]

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}) =
...

While I welcome this change(!), it seems to go against formatting in, for 
example, the Isabelle sources. Not an important point, just curious.


Tobias



smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Tobias Nipkow]

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?

rtranclp vs tranclp:

  * there is a rtranclp_mono "r ≤ s ==> r^** ≤ s^**", but no tranclp_mono. Given
the tranclp_mono, it should probably be:


lemma tranclp_mono:
   "r⇧+⇧+ a b ⟹ r ≤ s ⟹ s⇧+⇧+ a b"
 using rtranclp_mono by (auto dest!: tranclpD intro: 
rtranclp_into_tranclp2)


  * there is a rtranclp_idemp and a rtrancl_idemp marked as simp "(r^**)^** =
r^**", but no trancl_idemp nor tranclp_idemp


lemma trancl_idemp: "(r⇧+)⇧+ = r⇧+"
   by simp

lemmas tranclp_idemp = trancl_idemp[to_pred]


Transitivity of lexord vs lexn:

  * there is a lexord_transI "trans r ⟹ trans (lexord r)", but no lexn_transI


(I have not been able to factor the case distinction below; the proof uses
the new consider keyword)


lemma lexn_transI:
   assumes trans: "trans r"
   shows "trans (lexn r n)"
 unfolding trans_def
proof (intro allI impI)
   fix as bs cs
   assume asbs: "(as, bs) ∈ lexn r n" and bscs: "(bs, cs) ∈ lexn r n"

   obtain abs a b as' bs' where
 n: "length as = n" and "length bs = n" and
 as: "as = abs @ a # as'" and
 bs: "bs = abs @ b # bs'" and
 abr: "(a, b) ∈ r"
 using asbs unfolding lexn_conv by blast

   obtain bcs b' c' cs' bs' where
 n': "length cs = n" and "length bs = n" and
 bs': "bs = bcs @ b' # bs'" and
 cs: "cs = bcs @ c' # cs'" and
 b'c'r: "(b', c') ∈ r"
 using bscs unfolding lexn_conv by blast
   consider (le) "length bcs < length abs"
 | (eq) "length bcs = length abs"
 | (ge) "length bcs > length abs" by linarith
   then show "(as, cs) ∈ lexn r n"
 proof cases
   let ?k = "length bcs"
   case le
   hence "as ! ?k = bs ! ?k" unfolding as bs by (simp add: nth_append)
   hence "(as ! ?k, cs ! ?k) ∈ r" using b'c'r unfolding bs' cs by auto
   moreover
 have "length bcs < length as" using le unfolding as by simp
 from id_take_nth_drop[OF this] have "as = take ?k as @ as ! ?k #
drop (Suc ?k) as" .
   moreover
 have "length bcs < length cs" unfolding cs by simp
 from id_take_nth_drop[OF this] have "cs = take ?k cs @ cs ! ?k #
drop (Suc ?k) cs" .
   moreover have "take ?k as = take ?k cs"
 using le arg_cong[OF bs, of "take (length bcs)"] unfolding cs as
bs' by auto
   ultimately show ?thesis using n n' unfolding lexn_conv by auto
 next
   let ?k = "length abs"
   case ge
   hence "bs ! ?k = cs ! ?k" unfolding bs' cs by (simp add: nth_append)
   hence "(as ! ?k, cs ! ?k) ∈ r" using abr unfolding as bs by auto
   moreover
 have "length abs < length as" using ge unfolding as by simp
 from id_take_nth_drop[OF this] have "as = take ?k as @ as ! ?k #
drop (Suc ?k) as" .
   moreover
 have "length abs < length cs" using n n' unfolding as by simp
 from id_take_nth_drop[OF this] have "cs = take ?k cs @ cs ! ?k #
drop (Suc ?k) cs" .
   moreover have "take ?k as = take ?k cs"
 using ge arg_cong[OF bs', of "take (length abs)"] unfolding cs as
bs by auto
   ultimately show ?thesis using n n' unfolding lexn_conv by auto
 next
   let ?k = "length abs"
   case eq
   hence "abs = bcs" "b = b'" using bs bs' by auto
   moreover hence "(a, c') ∈ r" using abr b'c'r trans unfolding
trans_def by blast
   ultimately show ?thesis using n n' unfolding lexn_conv as bs cs by 
auto
 qed
qed



Best regards,

Mathias


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





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Infinite_Set.thy

[Tobias Nipkow]

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 standard HOL development. Of course we are all against 
bloat, but the separation of this material from the other material looks 
artificial.


I remember other people suggesting this as well, albeit not on this list. It 
seems fair to me. Only the function atmost_one at the very end should go 
somewhere else.


Tobias


Larry

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





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] popup in ce6320b9ef9b

[Tobias Nipkow]

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
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] MIR decision procedure

[Tobias Nipkow]

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 13/11/2015 17:05, Lawrence Paulson wrote:

The MIR decision procedure is again working. We still have the mystery of what 
it is good for. It is not used anywhere at all. Even the test suite consists of 
a mere five problems. And I have now stumbled across ferrack. It seems to be 
used quite a bit, but what does it do? Is it documented anywhere?

Larry

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





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Tobias Nipkow]

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 duplicate the prior behaviour. I have already observed that 
adding these additional simplification rules breaks a few proofs, so we have to 
see how it goes.


I am not surprised at all that the simplifier behaves differently because the 
simpset is modified all the time and is full of theorems wih coercions. But 
blast is another matter. Concrete questions:


- Are there any coercion-related permanent intro/dest/elim theorems (either 
before or now)?


- Could they kick in during a proof concerned only with basic set theory and 
first order logic?


I want to make sure that it is not something else that caused blast to break.

Tobias



smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: State panel

[Tobias Nipkow]

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 longer shows proof state output by default. This
reduces resource requirements of prover time and GUI space.
INCOMPATIBILITY, use the State panel instead or enable option
"editor_output_state".


This refers to Isabelle/bb20f11dd842.  The State panel has been around for a 
while, without mentioning it explicitly.  It should now be sufficiently 
consolidated for production use; even old GUI timing problems that caused 
excessive flashing due to repaints should no longer happen.


The separation looks like a good idea, but triggering state panel updates only 
on request doesn’t seem to mesh with how I use the interface these days. I’ve 
become very accustomed to the ability to immediately see the proof state by 
just navigating to the relevant command. It’s one of the things I really like 
about Isabelle/jEdit.


I couldn't agree more, and others I spoke to confirm this. Thus it is 
unfortunate that this mode of working now requires an explicit flag that novices 
won't know about, apparently motivated by resource considerations. It would be 
better if people who run into resource problems (novices typically don't) can 
set a flag to disable the state being shown.


Tobias


Maybe it’s because the shortcut doesn’t seem to be working for me (do I need to 
clear anything in my jedit settings first to get new defaults?), but even with 
a shortcut, I’ll now need two interactions to look at different proof states, 
when before I only needed one (navigate + shortcut as opposed to just navigate).

It’s true that producing proof state output for every single command in the 
document is a lot of overhead. Would triggering an update for each cursor 
movement (navigation/typing) be as bad as before in terms of overhead (or 
worse), or would it still be less?

Cheers,
Gerwin




The information in this e-mail may be confidential and subject to legal 
professional privilege and/or copyright. National ICT Australia Limited accepts 
no liability for any damage caused by this email or its attachments.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Future of permanent_interpretation

[Tobias Nipkow]

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 years back. Florian's very useful implementation of that really needs
to make it into Main.


It could simply be integrated with the current interpretation and sublocale commands, 
where the definitions could be supplied in a separate clause, as suggested by Florian, 
perhaps using "defines" as keyword.  Would this suit your needs?


That would be just fine.


(Independently I intend to change the keyword for the rewrite morphisms clause of these commands 
from "where" to "rewrites", to better distinguish it from named instantiations 
in locale expressions.)


My understanding of "sublocale" is that it is an interpretation within a locale
and I have used that explanation in papers because I find it very succinct. Thus
I would welcome if the same keyword is used.


This view is of course valid, but it isn't the whole story.  With "sublocale" these 
interpretations are orchestrated in a manner such that the locale hierarchy is effectively changed. 
 Now I can see that there might be domains where this more abstract view is not relevant, but when 
working with a hierarchy of locales representing algebraic structures it is certainly appropriate.  
It should also be kept in mind that "sublocale" is established in the locale 
documentation including my JAR paper [1].  If the desire for a different keyword is so strong, 
perhaps an alias might be a solution.


Thanks for the explanation. Since sublocale is more than a local interpretation, 
I withdraw my comment.


Tobias


Clemens

[1] Clemens Ballarin. Locales: a module system for mathematical theories. 
Journal of Automated Reasoning, 52(2):123–153, 2014.



On 25/10/2015 11:16, Clemens Ballarin wrote:

Hi Florian,

this proposal goes too far, of perhaps, not far enough.  Let me explain.

There is of course nothing wrong with providing new commands and enhancements 
for frequent use cases.  However, I don't see a good reason why users should be 
forced to write 'permanent_interpretation' where they could write 
'interpretation' or 'sublocale'.

I don't object to a careful evolution of the user interface to locales, but I 
don't think you're heading in the right direction.  Your 
'permanent_interpretation' lets users make some definitions followed by, 
depending on the context, an interpretation or a sublocale declaration.  This 
is certainly useful, but it is not general enough for making it the preferred 
command.  For example, it doesn't permit function declarations.  It also blurs 
the distinction between 'interpretation' and 'sublocale' by calling the latter 
'permanent_interpretation' when in a locale context, but not at the level of 
theories, but instead calling the former 'permanent_interpretation' at the 
level of theories.

It should be kept in mind that in the current design the 'interpretation' commands are effective for the lifetime of their context: in theories they are therefore permanent, in context blocks they persist for that block and within a proof 'interpret' provides services for that proof.  This is pretty straightforward.  On the other hand, 'locale' and 'sublocale' are theory-level commands that relate a locale to a locale expression (which in both cases becomes a sublocale of the locale).  Their only difference is that 'locale' declares a new locale while 'sublocale' refers to an existing one.  We have allowed the use of 'sublocale' in locale contexts as a notational convenience, but I don't consider it a good idea to further blur the distinction between 'interpretation' and 'sublocale'.  Calling 'sublocale' 'permanent_interpretation' in some contexts and 'sublocale' in others is certainly bad.  The current design is, of course, not cast in stone, but for changing it, there has to be 

a

consistent vision first, so we know where we are heading.


Certainly, your work has partly been inspired by the feeling that the current 
locale commands only provide the bare basics for manipulating locales.  For 
example, basing an interpretation or sublocale declaration on definitions is 
certainly something that could be done in a fancier manner.  The situation is 
perhaps a bit similar to that of 'axclass' several years ago, where your work 
on type classes has improved the user experience dramatically.  If you would 
like to bring locales forward, you might consider developing ideas along those 
lines.  The required definitions and proofs for an interpretation could for 
example be collected in a dedicated context in a step-by-step manner similar to 
that of class instantiation.  Your work also seems to be inspired by the desire 
to gradually rename 'sublocale' to 'interpretation', which I find su

Re: [isabelle-dev] Future of permanent_interpretation

[Tobias Nipkow]

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 of it w/o having to learn about and load 
"permanent_interpretation" (whose future is still under discussion).


Tobias

On 29/10/2015 11:31, Florian Haftmann wrote:

Hi Clemens et al.,

let me put things in a broader perspective. I think we have two views on
the whole machinery:

* The algebraic view with locales, sublocale statements and (somehow
global) interpretation statements. This view is important because it
essentially describes the implementation of the whole thing.

* The »local everything« view, where you have certain targets which
allow certain operations, most notably »notes«, »defines«, and something
which might internally be called »subscribes«, a permanent connection to
existing locales covered by a locale expression. Internally, this falls
back to existing mechanism, particularly »sublocale« for subscriptions
into locales. But note that this is only the typical sandwich principle
of target implementations, similiarly to definitions in locales which
are essentially global definitions plus an abbreviation, which appears
in theory text as plain »definition« nonetheless!

(Also note that »subclass« is something special between type classes
only, it is not a generic »local everything« construct.)

We may well come to the conclusion that both views are legitimate to be
present in user space, i.e. as isar keywords; although this is not very
common in Isabelle, it may be attributed to the complexity of the
machinery itself.

However I forsee two possible future extensions where both notions are
in conflict an a decision has to be made.

Starting point: there has been the decision that »interpretation« in
confined contexts (locales, classes, nested contexts, …) denotes
epheremal interpretation.  This fits nicely with »interpret« in proofs.

But

a) Also a theory is a confined context »theory … begin … end«; although
we are technically far off from that, in future it might be possible to
issue interpretation epheremal inside a particular theory only, and in
the current setting this would just be »interpretation«, demanding an
alternative keyword for subscriptions into theories.

b) Similarly, also interpretation in a »context … begin … end« block
might include a subscription into the surrounding target, leaving
additional premises in the results of subscription.  As a possible
example, think of conditionally complete lattices which subscribe to a
existing complete
lattice locale under the premise of an additional predicate.  Again, if
the surrounding target is a theory, how would the keyword look like, as
»interpretation« is already needed for epheremal interpretation?

So, if we want to maintain both views in the long run consistenly, we must
1) either find an alternative keyword for interpretation/subscription
into theories
2) or find an alternative keyword for epheremal interpretation.

In the light of this, some minor remarks:


Your 'permanent_interpretation' lets users make some definitions
followed by, depending on the context, an interpretation or a
sublocale declaration.


Note that it is just a restriction of the current implementation that
permanent_interpretation requires either a theory or a locale/class
target; each target is able to provide its own implementation for that,
and currently only these to do so.


It also blurs the distinction
between 'interpretation' and 'sublocale' by calling the latter
'permanent_interpretation' when in a locale context, but not at the
level of theories, but instead calling the former
'permanent_interpretation' at the level of theories.


This »blurring« is inherent in the »local everything« approach.
»definition« in locale targets is essentially an abbreviation, but
called that nonetheless.


It should be kept in mind that in the current design the
'interpretation' commands are effective for the lifetime of their
context: in theories they are therefore permanent


It is not clear whether the »lifetime« of theories should exceed the
final »end« or not.


Certainly, your work has partly been inspired by the feeling that
the current locale commands only provide the bare basics for
manipulating locales.  For example, basing an interpretation or
sublocale declaration on definitions is certainly something that
could be done in a fancier manner.


According to my feelings, the whole locale machinery is an excellent and
powerful part of the systems.  The addition of mixin definitions as
special case of mixin rewrites do not touch the foundations (locale.ML /
expression.ML) at all – there is no restriction to achieve the same
result withotuh them.


The situation is perhaps a bit
similar to that of 'axclass' several years ago, where your work on
type classes has 

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

[Tobias Nipkow]

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 the display, even if there is no newline in
between. This is in contrast to latex conventions (eg \[ \]) and I would
rather not have to insert lots of \nondent by hand.


There is indeed one \n too much, which may produce an unintended paragraph in
LaTeX.

I've changed that as follows:

changeset:   61516:8e3705d91cfa
tag: tip
user:wenzelm
date:Mon Oct 26 18:04:17 2015 +0100
summary: clarified Latex.environment (again, amending e16649b70107): avoid
additional paragraph, e.g. relevant for option [display];


 Makarius





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Tobias Nipkow]

On 07/10/2015 00:37, Michael Norrish wrote:

HOL4 and HOL Light both support the (sym) syntax to remove concrete syntax fixities.  I 
don't think HOL Light supports comments at this level.  HOL4 does, using SML's (* ... *). 
 So, if you want to write the escaped *, you have to use our older syntax for the same 
(using a $ for "op": $*), or you can just add spaces and write ( *), or ( * ).


Of course, "( * )" is ok. The only reason I have been a little wary of "(*)" is 
that people who are unaware of comments inside formulas would be totaly confused 
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 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 
inclined to leave things as they are.


"(*)" does not work, because it is in conflict with "(* comment *)" in inner syntax.  I have recently 
encountered a situation where it would have been better to replace inner comments by "-- ‹comment›", as known in outer 
syntax, but the double-minus was in conflict with some infix operators. The next idea was to replace "-- ‹comment›" by 
"— ‹comment›" with a newly introduced Isabelle symbol for the mdash.

So many clouds of dust, caused by trying to clean up obscure corners ...

At the moment I am also inclined to leave things unchanged.


   Makarius___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev





The information in this e-mail may be confidential and subject to legal 
professional privilege and/or copyright. National ICT Australia Limited accepts 
no liability for any damage caused by this email or its attachments.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Tobias Nipkow]

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


Tobias



smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Tobias Nipkow]

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 inclined to leave things as 
they are.


Tobias

On 22/09/2015 16:21, Florian Haftmann wrote:

The »op •« is infamous. Whatever you wish instead (my personal favorite
being no special syntax at all), problems include
a) to detect unintended printing behaviour
b) a suitable migration mechanisms

Concerning b), one you could imagine things like
a) alternative declarations (infix(l/r)_new beside infix(l/r),
infix(l/r) beside infix(l/r)_old)
b) a flag to control the semantics of infix(l/r)
c) a flag combined with a data slot to modify existing mixfix
declarations afterwards also

Personally I would appreciate some move here, but this only makes sense
if we agree what the goal is and whether it is worth the effort.

Cheers,
Florian



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





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Tobias Nipkow]

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 eta-contraction machinery needs to be 
revised, possibly resulting in a new syntactic constant, which is a further 
complication.


I would prefer to leave things as they are now. That print translation is ok and 
you would be moving the complications elsewhere. We really have more important 
issues to work on.


Tobias

On 22/09/2015 16:17, Florian Haftmann wrote:

The situation turned out more complicated than anticipated: implicit
eta-contraction happens at a rather late level in the printing machinery
using a print translation. Hence, any countermeasure must act on the
same (or a later level). However in the ecosystem as it is today, it
seems better to do such transformations at the uncheck level, i.e. quite
close to the logic.

For the moment, I installed the print translation from e6b1236f9b3d
again to retain the previous behavior in af7bed1360f3. Please report
remaining suspicious behavior.

To get ahead from there, I need to understand more about eta-contracted
printing.

According to my current understanding, this has been introduced once to
produce less surprises if proof tools perform spontaneous eta-expansion
(please correct me if this is wrong).

To get more fine-grained control there, I can foresee two approaches:
a) Move the eta-contract machinery to the uncheck level also.
b) Provide a special syntactic marker which is »syntactic identity« but
does not perform eta-contraction on its immediate argument. This would
allow uncheckers to protect certain abstractions using this marker.

b) seems preferable, since there is less risk to produce unexpected
deviations from current printing without being noticed.

Comments?

Florian





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS

[Tobias Nipkow]

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}" prints as
"Collect (uncurry P)" which I find rather hard to read. Are you aware of
this effect and could you please restore the former situation?


this is on my to-do list, together with other binder-related issues like
"{p. case p of (x, y) => P x y}".

Florian



Best,
Andreas

On 10/09/15 12:02, Florian Haftmann wrote:

* Combinator to represent case distinction on products is named
"uncurry", with "split" and "prod_case" retained as input abbreviations.

Partially applied occurences of "uncurry" with eta-contracted body
terms are not printed with special syntax, to provide a compact
notation and getting rid of a special-case print translation.

Hence, the "uncurry"-expressions are printed the following way:

a) fully applied "uncurry f p": explicit case-expression;

b) partially applied with explicit double lambda abstraction in
the body term "uncurry (%a b. t [a, b])": explicit paired abstraction;

c) partially applied with eta-contracted body term "uncurry f":
no special syntax, plain "uncurry" combinator.
This aims for maximum readability in a given subterm.
INCOMPATIBILITY.

This refers to e6b1236f9b3d.

This schema emerged after some experimentation and seems to be a
convenient compromise. The longer perspective is to overcome the
case_prod/split schism eventually and consolidate theorem names
accordingly.

The next step after this initial cleanup is to tackle the »let (a, b) =
… in …« issue.

 Florian



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






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





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS

[Tobias Nipkow]

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, case_prod is the "right" name from the perspective of the (co)datatype
package.


Yes, we should return to that name in the end.

Tobias


Dmitriy

[1] https://xkcd.com/927/

On 10.09.2015 12:02, Florian Haftmann wrote:

* Combinator to represent case distinction on products is named
"uncurry", with "split" and "prod_case" retained as input abbreviations.

Partially applied occurences of "uncurry" with eta-contracted body
terms are not printed with special syntax, to provide a compact
notation and getting rid of a special-case print translation.

Hence, the "uncurry"-expressions are printed the following way:

a) fully applied "uncurry f p": explicit case-expression;

b) partially applied with explicit double lambda abstraction in
the body term "uncurry (%a b. t [a, b])": explicit paired abstraction;

c) partially applied with eta-contracted body term "uncurry f":
no special syntax, plain "uncurry" combinator.
This aims for maximum readability in a given subterm.
INCOMPATIBILITY.

This refers to e6b1236f9b3d.

This schema emerged after some experimentation and seems to be a
convenient compromise. The longer perspective is to overcome the
case_prod/split schism eventually and consolidate theorem names accordingly.

The next step after this initial cleanup is to tackle the »let (a, b) =
… in …« issue.

Florian



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




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





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Tobias Nipkow]

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 input syntax (as opposed 
to the shortcuts) is not much of a gain because one cannot reasonably reuse 
them. But there is indeed quite a bit of duplication, eg  and /\, | and \/.


Some symbols like ! and ? are quick to type but I wouldn't call them graphical 
and am not particularly attached to them. In fact, one could then give factorial 
its standard syntax.


Tobias

On 30/06/2015 14:13, Makarius wrote:

On Tue, 30 Jun 2015, C. Diekmann wrote:


In HOL.thy, the conjunction (conj) is first introduced with the 
symbol. Later, the notation ∧ is introduced. In order to clean up
this difficult-to-understand theory, would it be possible to directly
introduce conjunction with the ∧ symbol? I see three advantages:

1) It simplifies the axiomatizations (a very critical part).
2) It may help in getting started with Isabelle since no confusing 
symbol would appear anywhere. Currently, if a ctrl-click on a lemma
sends me to HOL.thy, things look pretty scary.
3) It would free up the symbol  for custom theories.

This could also be done for %, --, ==, ~, and many more.


Interesting that you call this legacy ASCII syntax. In the manner it is done
until today, the ASCII syntax is still the official syntax and the xsymbols
variant some add-on. Only recently, the system default has changed to have
xsymbols always enabled by default.

Historically, there were good reasons of having the system act in plain ASCII by
default, due to a general lack of reliability in rendering Isabelle symbols on
various operating systems, terminal emulators, and versions of Emacs.

Now that the TTY loop and Proof General are removed, there is nothing to prevent
a fresh look at the situation.  Here are just the canonical questions (which are
never meant rhetoric):

   (1) Are there remaining uses of plain ASCII syntax in Isabelle output?

   (2) Are there remaining uses of plain ASCII syntax in Isabelle input?


As a start to the collection of material some possible points:

Concerning output:

   * Seemingly modern web frameworks might lack Unicode rendering quality
 to work with Isabelle symbols relibly.  1-2 years ago there were still
 problems on Stackoverflow.  Do they still exist?

 In contrast, plain HTML pages should be able to provide the
 IsabelleText font from the server side.  There is no need for the old
 HTML print mode.

Concerning input:

   * Compatibility: huge amounts of existing sources still use ASCII input.

 There are chances to make a systematic upgrade for formally checked
 text, but not for unchecked comments.

   * Convenience: users somethings find it too combersome to type proper
 Isabelle symbols.

 I never do that myself, but take the time to type things nicely.  It
 is actually not much time for me, since I implemented the input
 methods myself and know how they work.

Anything further points?

Once the collection of observation is complete, we can come up with further
migration plans to improve on the historical situation.


 Makarius


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





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Tobias Nipkow]

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 Nominal2 (unresolved Nominal2_Abs, Nominal2_Base, 
Nominal2_FCB)
*** Theorem must be of the form ?p \bullet c \equiv c, with c a constant 
or fixed parameter:
*** ?p \bullet ?y == ?y
*** At command lemma (line 2123 of 
/mnt/nfsbroy/home/isatest/afp/devel/thys/Nominal2/Nominal2_Base.thy)

Larry


Begin forwarded message:

From: isat...@macbroy2.informatik.tu-muenchen.de (Isabelle )
Subject: test failed (Archive of Formal Proofs)
Date: 18 June 2015 11:25:01 BST
To: undisclosed-recipients:;

Session [Incompleteness] in the automated afp test failed.

AFP version: development -- hg id dd9b5f6f3866
Isabelle version: devel -- hg id e0169291b31c
Test ended on: macbroy2, Thu Jun 18 12:25:01 CEST 2015.

To reproduce the error, check out the development version of the
archive from sourceforge and run isabelle make on your session.

This is an automatically generated email. To switch off these
notifications, edit thys/Incompleteness/config and hg commit and push the 
changes.

Have a nice day,
  isatest


This body part will be downloaded on demand.


This body part will be downloaded on demand.




smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Tobias Nipkow]

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
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Tobias Nipkow]

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 equations: neither definition facility finds a 
minimum, it is too hard: Alexander Krauss. Pattern minimization problems over 
recursive data types. ICFP 2008.


Tobias

On 10/06/2015 23:19, Larry Paulson wrote:

We need to figure out how recdef does it. The minimum number of equations is 
mathematically fixed, so recdef must be using conditional expressions or other 
tricks.
Larry


On 9 Jun 2015, at 23:07, Gerwin Klein gerwin.kl...@nicta.com.au wrote:

I can confirm that, at least that side is simple.

Tobias’ point about avoiding exponential blowup is important, though. Might 
still be too early to retire recdef entirely if it is substantially better for 
some kinds of definitions, esp if they are in use (I think the recdef in Simpl 
is one of these).

Cheers,
Gerwin


On 09.06.2015, at 11:27, Thomas Sewell thomas.sew...@nicta.com.au wrote:

I've had a quick scan over the NICTA repositories. It doesn't look like
there are any live original uses of recdef. There are recdefs in a copy
of Simpl-AFP, and in some backups of historical papers.

Short summary, NICTA doesn't have any stakes in recdef.

Cheers,
   Thomas.

On 08/06/15 06:13, Makarius wrote:

On Sat, 6 Jun 2015, Gerwin Klein wrote:




On 06.06.2015, at 21:23, Makarius makar...@sketis.net wrote:

(2) 'defer_recdef' which is unused in the directly visible Isabelle
  universe.  So it could be deleted today.

This mailing list thread is an opportunity to point out dark matter
in the Isabelle universe, where 'defer_recdef' still occurs.
Otherwise I will remove it soon, lets say within 1-2 weeks.


Unused in our part of the dark matter universe as well.


The thread has shifted over to actual 'recdef'. Are there remaining
uses of 'recdef' in the NICTA dark matter?

So far I always thought the remaining uses in HOL-Decision_Procs are
only a reminder that there are other important applications.


   Makarius





The information in this e-mail may be confidential and subject to legal 
professional privilege and/or copyright. National ICT Australia Limited accepts 
no liability for any damage caused by this email or its attachments.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


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





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Tobias Nipkow]

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 to. You don't really 
care that the induction has hundreds of cases because they are trivial. In 
contrast, rewriting such a definition to avoid the blowup is a pain in the 
backside and is not guaranteed to make proofs simpler.


Tobias

On 07/06/2015 21:46, Larry Paulson wrote:

I suggest looking for ways for users to avoid exponential blowup. Presumably 
this means avoiding deeply nested patterns in favour of conditional expressions 
in some cases. Such a formalisation might be easier to reason with too, who 
wants an induction rule with hundreds of cases?

But coming up with simple guidelines for users might be tricky.

Larry


On 7 Jun 2015, at 20:33, Florian Haftmann 
florian.haftm...@informatik.tu-muenchen.de wrote:

As far as I know, this is due to layered architecture of the function
package.  »recdef« does everything in one bunch and can hence optimize
for sequential pattern matching.  Each layer of »function« must feed its
result to its successor in a standardized form, and since there is no
overall concept of sequential pattern matching, it has to be compiled
away once and for all from the very beginning. (roughly spoken)

An optimization would require a modified architecture.


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





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Tobias Nipkow]

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 solve that one.


Now one could argue that since we need recdef, we should also keep the special 
variant defer_recdef, but if nobody speaks up for it, we don't have a proof that 
we really need it and it should go.


Tobias

On 06/06/2015 13:23, Makarius wrote:

On Sat, 6 Jun 2015, Larry Paulson wrote:


I’d be happy to see the complete phasing out of TFL. It’s had its day. It was
always a tricky thing to maintain. I’m amazed that it still works despite all
of the many fundamental changes to system APIs.


There are actually two remaining parts of TFL:

   (1) 'recdef' which is still used in Isabelle + AFP applications, but
 very rarely and some effort could be made to get rid of it.

   (2) 'defer_recdef' which is unused in the directly visible Isabelle
 universe.  So it could be deleted today.

This mailing list thread is an opportunity to point out dark matter in the
Isabelle universe, where 'defer_recdef' still occurs.  Otherwise I will remove
it soon, lets say within 1-2 weeks.


Apart from that we should also work on (1) eventually.  It has become a ritual
to ask about the purpose of old 'recdef', and it usually leads to the result as
still needed for odd reasons that I then forget immediately.  So I have
developed a reluctance to ask again.


 Makarius


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





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Tobias Nipkow]

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 equations as lemmas. You also need to derive an induction principle. 
I would rather keep recdef than do all that by hand.


Tobias


Larry


On 6 Jun 2015, at 16:11, Florian Haftmann 
florian.haftm...@informatik.tu-muenchen.de wrote:


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 solve that one.

Now one could argue that since we need recdef, we should also keep the
special variant defer_recdef, but if nobody speaks up for it, we don't
have a proof that we really need it and it should go.


At the time of their writing the recdef examples in (nowadays)
src/HOL/Decision_Procs were the power applications of their times.

Since then power applications have grown bigger and bigger and
fun/function have been used widespread.  It seems strange to me that no
application since then had never hit the same concrete wall again.

So are there any experience reports that the combinatorial explosion in
pattern matching in fun/function had to be worked around somehow?  Or do
we have to conclude that the pattern complexity of the applications in
src/HOL/Decision_Procs is indeed domain-specific?

Florian

--

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

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






smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Tobias Nipkow]

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?
b) The conservative solution: partial division has »_ div _«, an (the
more special) field division »_ / _«. This seems more sensible than the
other way round since »_ div _« suggests some kind of »incompleteness«.

Any opinions?


I’d vote for (b). I also find that “div” suggests some incompleteness. It 
serves as a warning signal; when you try to prove

 sum_sq n = n * (n + 1) * (2 * n + 1) div 6

you think twice and rewrite it into

 6 * sum_sq n = n * (n + 1) * (2 * n + 1)

I believe Maude (another system named after a French female, presumably) even 
had a different minus operator on “nat” as opposed to the other types. In a 
formal context, such precision is surely helpful. Indeed, minus is a nasty case 
for Dmitriy’s coercions.

Jasmin

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





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Tobias Nipkow]

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

There is an inclusion hierarchy (⊆) of numerical types

(num ⊆) nat ⊆ int ⊆ rat ⊆ real ⊆ complex

We can embed »smaller« into »bigger« types using conversions

(numeral ⊆) of_nat ⊆ of_int ⊆ of_rat ⊆ of_real

These conversions have solid generic algebraic definitions!

For historic reasons, there is also the conversion real :: 'a ⇒ real
which is overloaded and can be instantiated to arbitrary types. This
(co)conversion works in the other direction without any algebraic
foundation!

My impression is that having this conversion is a bad idea. For
illustration have a look at
http://isabelle.in.tum.de/repos/isabelle/file/3d696ccb7fa6/src/HOL/Archimedean_Field.thy#l312
which gives a wonderful generic lemma relating fraction division and
integer division:

»floor (of_int k / of_int l) = k div l«

Note that the result type of the of_int conversion is polymorphic and
can be instantiated to rat and real likewise!

In the presence of the »real« conversion, there is a second variant

»floor (real k / real l) = k div l«

which must be given separately!

For uniformity it would be much better to have »real« disappear in the
middle run. I see two potential inconveniences at the moment:
* Writing »of_foo« might demand a type annotation on its result in many
cases (n.b. operations of type foo ⇒ 'a are one of the rare cases where
explicit type annotations must be given in terms rather than at »fixes«).
* We have the existing abbreviations »real_of_foo« which have no type
ambiguity, but might seem a little bit verbose.
Anyway, the duplication seems more grivious to me than such syntax issues.

Any comments?
Florian



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





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Tobias Nipkow]

Thank you for reminding me of the reading part. My ability to read formulas 
decreases quadratically with their length. Trading in real_of_int for real 
makes things definitely worse.


I would want to see a concrete figures how much duplication is avoided in the 
current theories and how much additional annotation is needed. Note also that if 
some device helps to make the foundations elegant but complicates the 
applications it can be detrimental if the foundations remain fixed but the 
applications keep growing.


Tobias

On 03/06/2015 10:55, Fabian Immler wrote:

I think I could live without real: coercions save a lot of the writing.
Moreover, the real_of_foo abbreviations help to avoid type annotations:
I suppose that all of the current occurrences of real could be replaced with one 
particular real_of_foo.

For reading (subgoals etc), one could perhaps think about less 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 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« conversion.

There is an inclusion hierarchy (⊆) of numerical types

(num ⊆) nat ⊆ int ⊆ rat ⊆ real ⊆ complex

We can embed »smaller« into »bigger« types using conversions

(numeral ⊆) of_nat ⊆ of_int ⊆ of_rat ⊆ of_real

These conversions have solid generic algebraic definitions!

For historic reasons, there is also the conversion real :: 'a ⇒ real
which is overloaded and can be instantiated to arbitrary types. This
(co)conversion works in the other direction without any algebraic
foundation!

My impression is that having this conversion is a bad idea. For
illustration have a look at
http://isabelle.in.tum.de/repos/isabelle/file/3d696ccb7fa6/src/HOL/Archimedean_Field.thy#l312
which gives a wonderful generic lemma relating fraction division and
integer division:

»floor (of_int k / of_int l) = k div l«

Note that the result type of the of_int conversion is polymorphic and
can be instantiated to rat and real likewise!

In the presence of the »real« conversion, there is a second variant

»floor (real k / real l) = k div l«

which must be given separately!

For uniformity it would be much better to have »real« disappear in the
middle run. I see two potential inconveniences at the moment:
* Writing »of_foo« might demand a type annotation on its result in many
cases (n.b. operations of type foo ⇒ 'a are one of the rare cases where
explicit type annotations must be given in terms rather than at »fixes«).
* We have the existing abbreviations »real_of_foo« which have no type
ambiguity, but might seem a little bit verbose.
Anyway, the duplication seems more grivious to me than such syntax issues.

Any comments?
Florian



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



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






smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev