Re: [isabelle-dev] NEWS: proof outline with cases

[Andreas Lochbihler]

Hi Makarius,

Just a quick feedback on the proof outlines: they are great! But sometimes quotes are 
needed around the case name (e.g., if it is a keyword like "try" or "oracle", or if it is 
a case of an induction rule by the function package for an equation which has been split 
up by the sequential option, i.e., 3_1 and 3_2). Could you add the missing quotes to the 
outline?


(For reference: tested with Isabelle/eca71be9c948)

Best,
Andreas

On 16/07/16 13:14, Makarius wrote:

*** Prover IDE -- Isabelle/Scala/jEdit ***

* Command 'proof' provides information about proof outline with cases,
e.g. for proof methods "cases", "induct", "goal_cases".


This refers to Isabelle/6c46a1e786da. The main functionality is in
Isabelle/9f8d06f23c09, which also demonstrates how to do such things
with existing PIDE infrastructure.


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

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

[Makarius]

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

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

[Manuel Eberl]

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.


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

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] Fwd: [Isabelle-ci] Build failure in Isabelle

[Lars Hupel]

> Is the test hardware in an air-conditioned server room?

Of course.
___
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

[Makarius]

On 08/08/16 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.

The point is that a hot CPU runs slower. Memory management in Poly/ML
works on multiple cores, and the runtime behaviour changes the
characteristics of how the heap is cleaned up and resized dynamically.


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

I don't think that this is the case here.


Makarius


___
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

[Makarius]

On 08/08/16 11:14, Lars Hupel wrote:
> Dear all,
> 
> 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. Makarius, it may or may not be connected to
> the recent changes you did in proof reconstruction (994d1a1105ef).

This situation illustrates what "flying blind means" concerning
continuous testing.

With a chart showing performance parameters (CPU time, elapsed time,
heap size) in the past few weeks, it should be normally easy to see a
small step or spike for HOL-Proofs or its applications.


Makarius

___
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

[Lars Hupel]

> With a chart showing performance parameters (CPU time, elapsed time,
> heap size) in the past few weeks, it should be normally easy to see a
> small step or spike for HOL-Proofs or its applications.

Happy to assist with that. In a previous mail you indicated that these
parameters can be found in the log files. Luckily, Jenkins archives all
of them indefinitely.

For HOL-Proofs, the relevant job is "isabelle-repo-makeall". A catalog
of all builds and all archived logs can be found under the following URL:




This catalog also contains a timestamp (which I believe is the regular
Unix timestamp but with milliseconds instead of seconds).

The URLs where the specific log files can be found is easy to construct,
e.g.




That should contain all necessary data for plotting performance graphs.

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

Re: [isabelle-dev] [isabelle] Proposal: An update to Multiset theory

[Bertram Felgenhauer]

Florian Haftmann wrote:
> Hi Bertram,
> 
> > How shall we proceed? As I hinted at earlier I do not have (nor want, at
> > this point) push access, but I can prepare a patch or clone of the repo,
> > if that helps, or just provide a plain theory file that works with the
> > development version of Isabelle.
> 
> a repo URL or a patch is indeed the best thing to proceed: there is not
> »the« development version but an ongoing agile development.

Okay, I have exported a series of two patches against 1e7c5bbea36d,
the first adding monotonicity lemmata and the second for cancellation
and `multp`, `multeq`. See the attached file.

Cheers,

Bertram
# HG changeset patch
# User Bertram Felgenhauer 
# Date 1470657709 -7200
#  Mon Aug 08 14:01:49 2016 +0200
# Node ID 852c841c2ecde57bd9d0695edbad5b392ab418b5
# Parent  1e7c5bbea36dd2dd56705630f8e456de91b9788a
add monotonicity propertyies of `mult1` and `mult`

diff -r 1e7c5bbea36d -r 852c841c2ecd src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Sun Aug 07 12:10:49 2016 +0200
+++ b/src/HOL/Library/Multiset.thy	Mon Aug 08 14:01:49 2016 +0200
@@ -2214,6 +2214,14 @@
   obtains a M0 K where "M = M0 + {#a#}" "N = M0 + K" "\b. b \# K \ (b, a) \ r"
   using assms unfolding mult1_def by blast
 
+lemma mono_mult1:
+  assumes "r \ r'" shows "mult1 r \ mult1 r'"
+unfolding mult1_def using assms by blast
+
+lemma mono_mult:
+  assumes "r \ r'" shows "mult r \ mult r'"
+unfolding mult_def using mono_mult1[OF assms] trancl_mono by blast
+
 lemma not_less_empty [iff]: "(M, {#}) \ mult1 r"
 by (simp add: mult1_def)
 
# HG changeset patch
# User Bertram Felgenhauer 
# Date 1470657822 -7200
#  Mon Aug 08 14:03:42 2016 +0200
# Node ID 842352253b462144ba8a26e45080f53a1cefe2d8
# Parent  852c841c2ecde57bd9d0695edbad5b392ab418b5
prove monotonicity of `mult1` and `mult`

diff -r 852c841c2ecd -r 842352253b46 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Mon Aug 08 14:01:49 2016 +0200
+++ b/src/HOL/Library/Multiset.thy	Mon Aug 08 14:03:42 2016 +0200
@@ -2404,115 +2404,103 @@
 \ (I + K, I + J) \ mult r"
 using one_step_implies_mult_aux by blast
 
-subsection \A quasi-executable characterization\
-
-text \
-  The decreasing parts \A\ and \B\ of multisets in a multiset-comparison
-  \(I + B, I + A) \ mult r\, can always be made disjoint.
-\
-lemma decreasing_parts_disj:
-  assumes "irrefl r" and "trans r"
-and "A \ {#}" and *: "\b\#B. \a\#A. (b, a) \ r"
-  defines "Z \ A #\ B"
-  defines "X \ A - Z"
-  defines "Y \ B - Z"
-  shows "X \ {#} \ X #\ Y = {#} \
-A = X + Z \ B = Y + Z \ (\y\#Y. \x\#X. (y, x) \ r)"
+
+subsection \The multiset extension is cancellative for multiset union\
+
+lemma mult_cancel:
+  assumes "trans s" and "irrefl s"
+  shows "(X + Z, Y + Z) \ mult s \ (X, Y) \ mult s" (is "?L \ ?R")
+proof
+  assume ?L thus ?R
+  proof (induct Z)
+case (add Z z)
+obtain X' Y' Z' where *: "X + Z + {#z#} = Z' + X'" "Y + Z + {#z#} = Z' + Y'" "Y' \ {#}"
+  "\x \ set_mset X'. \y \ set_mset Y'. (x, y) \ s"
+  using mult_implies_one_step[OF `trans s` add(2)] unfolding add.assoc by blast
+consider Z2 where "Z' = Z2 + {#z#}" | X2 Y2 where "X' = X2 + {#z#}" "Y' = Y2 + {#z#}"
+  using *(1,2) by (metis mset_add union_iff union_single_eq_member)
+thus ?case
+proof (cases)
+  case 1 thus ?thesis using * one_step_implies_mult[of Y' X' s Z2]
+by (auto simp: add.commute[of _ "{#_#}"] add.assoc intro: add(1))
+next
+  case 2 then obtain y where "y \ set_mset Y2" "(z, y) \ s" using *(4) `irrefl s`
+by (auto simp: irrefl_def)
+  moreover from this transD[OF `trans s` _ this(2)]
+  have "x' \ set_mset X2 \ \y \ set_mset Y2. (x', y) \ s" for x'
+using 2 *(4)[rule_format, of x'] by auto
+  ultimately show ?thesis using  * one_step_implies_mult[of Y2 X2 s Z'] 2
+by (force simp: add.commute[of "{#_#}"] add.assoc[symmetric] intro: add(1))
+qed
+  qed auto
+next
+  assume ?R then obtain I J K
+where "Y = I + J" "X = I + K" "J \ {#}" "\k \ set_mset K. \j \ set_mset J. (k, j) \ s"
+using mult_implies_one_step[OF `trans s`] by blast
+  thus ?L using one_step_implies_mult[of J K s "I + Z"] by (auto simp: ac_simps)
+qed
+
+lemma mult_cancel_max:
+  assumes "trans s" and "irrefl s"
+  shows "(X, Y) \ mult s \ (X - X #\ Y, Y - X #\ Y) \ mult s" (is "?L \ ?R")
 proof -
-  define D
-where "D = set_mset A \ set_mset B"
-  let ?r = "r \ D \ D"
-  have "irrefl ?r" and "trans ?r" and "finite ?r"
-using \irrefl r\ and \trans r\ by (auto simp: D_def irrefl_def trans_Restr)
-  note wf_converse_induct = wf_induct [OF wf_converse [OF this]]
-  { fix b assume "b \# B"
-then have "\x. x \# X \ (b, x) \ r"
-proof (induction rule: wf_converse_induct)
-  case (1 b)
-  then obtain a where "b \# B" and "a \# A" and "(b, a) \ r"
-using * by blast
-  then show ?case
-  proof (cases "a \# X")
-case False
-then have "a \# B" using \a \# A\
-   

[isabelle-dev] NEWS: Rename HOL-Multivariate_Analysis to HOL-Analysis and move measure theory from HOL-Probability to HOL-Analysis

[Johannes Hölzl]

* Renamed session HOL-Multivariate_Analysis to HOL-Analysis.

* Moved measure theory from HOL-Probability to HOL-Analysis. When importing
HOL-Analysis some theorems need additional name spaces prefixes due to name
clashes.
INCOMPATIBILITY.




The incompatibility is obviously due to the renaming, but we also have
currently two integrals which share now some theorem names. The problem
is that one integral does not subsume the other:

* The /Bochner/ integral is defined on arbitrary measures, but 
  restricted to be absolutely integrable, i.e. when a function is 
  integrable than also its norm is integrable. 

* The /Henstock-Kurzweil/ integral is restricted to Euclidean spaces 
  (and the Lebesgue measure on it), but it is not restricted to 
  absolutely integrable functions.
My idea would be to rename both integrals into something like:
  has_bc_integral, bc_integrable, bc_integral,
  has_hk_integral, hk_integrable, hk_integral
and consequently rename the integral theorems.

Currently the measure theory is based on the stuff in the former
Multivariate_Analysis. My plan is to integrate it further down and then
replace some old stuff by more generic definitions/proofs from measure
theory.

There are currently further restrictions where we are not sure how to
solve them:

* Dominated convergence is very general on the Bochner integral it
  works for integrals into Banach spaces, while for the HK integral 
  it is currently only proven for Euclidean spaces.

* We require dominated convergence to prove that both integrals are 
  equal. Hence currently equality is only proven for Euclidean spaces.

* FTC for the Bochner integral is derived from FTC for the HK integral.
  Hence FTC for the Bochner integral is only available for Euclidean 
  spaces.

 - Johannes

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

Re: [isabelle-dev] NEWS: Rename HOL-Multivariate_Analysis to HOL-Analysis and move measure theory from HOL-Probability to HOL-Analysis

[Lawrence Paulson]

Thank you for making this change!

> My idea would be to rename both integrals into something like:
>   has_bc_integral, bc_integrable, bc_integral,
>   has_hk_integral, hk_integrable, hk_integral
> and consequently rename the integral theorems.

I would greatly prefer renaming the relevant theories instead so that we have 
Bochner.has_integral versus Gauge.has_integral, etc. That is the point of 
having compound names. I would go so far as to suggest that equivalent theorems 
with slightly different names should be rationalised.

Larry

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

Re: [isabelle-dev] NEWS: Rename HOL-Multivariate_Analysis to HOL-Analysis and move measure theory from HOL-Probability to HOL-Analysis

[Johannes Hölzl]

Am Montag, den 08.08.2016, 15:03 +0100 schrieb Lawrence Paulson:
> Thank you for making this change!
> 
> > 
> > My idea would be to rename both integrals into something like:
> >   has_bc_integral, bc_integrable, bc_integral,
> >   has_hk_integral, hk_integrable, hk_integral
> > and consequently rename the integral theorems.
> I would greatly prefer renaming the relevant theories instead so that
> we have Bochner.has_integral versus Gauge.has_integral, etc. That is
> the point of having compound names. I would go so far as to suggest
> that equivalent theorems with slightly different names should be
> rationalised.

I would prefer this too,  but has_integral is not a name. It is special
syntax, one writes:   (f has_integral x) s

Either we remove the syntax (and add it to a locale to be interpreted
locally) or rename it. Unfortunately the first option is still
problematic. For example, one needs to setup a context to use it, and
then one is not allowed to enter a locale context.

Another problem is that the theory which gets loaded later is always
slightly preferred as it does not need the theory prefix. Only way to
avoid this would be to hide the theorem names. Or put it in a context
and add the "qualified" command prefix.

Unifying the different names (i.e. integral_minus, sub, diff, uminus,
cmult, mult_left, ...) is also on my TODO list.

 - Johannes






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

Re: [isabelle-dev] NEWS: Rename HOL-Multivariate_Analysis to HOL-Analysis and move measure theory from HOL-Probability to HOL-Analysis

[Andreas Lochbihler]

Hi Johannes,

You could define the syntax for has_integral to be literally

  "(f Bochner.has_integral x) s"

and similarly for the other. Additionally, you could declare bundles with the existing 
notation


  "(f has_integral x) s"

for both of them (like is nowadays done for the Lifting package syntax). Then, you can 
locally include the notation for the desired integral with "includes", which is more 
flexible than a locale interpretation.


Andreas

On 08/08/16 16:57, Johannes Hölzl wrote:

Am Montag, den 08.08.2016, 15:03 +0100 schrieb Lawrence Paulson:

Thank you for making this change!



My idea would be to rename both integrals into something like:
  has_bc_integral, bc_integrable, bc_integral,
  has_hk_integral, hk_integrable, hk_integral
and consequently rename the integral theorems.

I would greatly prefer renaming the relevant theories instead so that
we have Bochner.has_integral versus Gauge.has_integral, etc. That is
the point of having compound names. I would go so far as to suggest
that equivalent theorems with slightly different names should be
rationalised.


I would prefer this too,  but has_integral is not a name. It is special
syntax, one writes:   (f has_integral x) s

Either we remove the syntax (and add it to a locale to be interpreted
locally) or rename it. Unfortunately the first option is still
problematic. For example, one needs to setup a context to use it, and
then one is not allowed to enter a locale context.

Another problem is that the theory which gets loaded later is always
slightly preferred as it does not need the theory prefix. Only way to
avoid this would be to hide the theorem names. Or put it in a context
and add the "qualified" command prefix.

Unifying the different names (i.e. integral_minus, sub, diff, uminus,
cmult, mult_left, ...) is also on my TODO list.

 - Johannes






___
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

Re: [isabelle-dev] NEWS: Rename HOL-Multivariate_Analysis to HOL-Analysis and move measure theory from HOL-Probability to HOL-Analysis

[Makarius]

On 08/08/16 17:09, Andreas Lochbihler wrote:
> 
> Additionally, you could declare bundles
> with the existing notation
> 
>   "(f has_integral x) s"
> 
> for both of them (like is nowadays done for the Lifting package syntax).
> Then, you can locally include the notation for the desired integral with
> "includes", which is more flexible than a locale interpretation.

It is also possible to 'unbundle' syntax bundles globally. With two
bundles: foo_syntax, no_foo_syntax, it becomes possible to switch back
and forth.

E.g. see finfun_syntax vs. no_finfun_syntax.


Makarius

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