Re: [isabelle-dev] Problem in AFP near 16e7d42ef7f4
I took a look, and it all runs perfectly well, except here:
show xs ∈ T⇩c ∧ ys ∈ T⇩c ∧
ipurge_tr_rev I⇩c id u xs = ipurge_tr_rev I⇩c id u ys ⟶
{x. u = x ∧ xs @ [x] ∈ T⇩c} = {x. u = x ∧ ys @ [x] ∈ T⇩c}
(* The following proof step performs an exhaustive case distinction over
all traces and domains,
and then can take long to be completed. *)
by (simp add: T⇩c_def I⇩c_def, rule impI, (erule conjE)+, cases u,
(((erule disjE)+)?, simp, blast?)+)
The comment doesn’t tell us whether to wait minutes or hours. Clearly this is a
fragile step. Any sort of change could break this.
Larry
On 25 Jun 2015, at 14:00, Florian Haftmann
florian.haftm...@informatik.tu-muenchen.de wrote:
isabelle: 19c277ea65ae tip
afp: 16e7d42ef7f4 tip
Running Noninterference_Generic_Unwinding ...
*** Timeout
Noninterference_Generic_Unwinding FAILED
(see also
/mnt/home/haftmann/data/isabelle/master/heaps/polyml-5.5.2_x86-linux/log/Noninterference_Generic_Unwinding)
val it = (): unit
Loading theory GenericUnwinding
Proofs for inductive predicate(s) rel_induct_auxp
Proving monotonicity ...
Proving the introduction rules ...
Proving the elimination rules ...
Proving the induction rule ...
Proving the simplification rules ...
### theory GenericUnwinding
### 1.941s elapsed time, 11.008s cpu time, 0.136s GC time
Any hints what could have gone wrong?
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
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Fwd: [isabelle] find_theorems and locales
Nobody has commented on this issue, and I would like to re-raise it, as it affects the development version. It simply doesn’t make sense that fundamental axioms such as dist_norm are concealed from find_theorems. I imagine it would be very easy to change this behaviour. Larry Begin forwarded message: From: Larry Paulson l...@cam.ac.uk Subject: Re: [isabelle] find_theorems and locales Date: 19 June 2015 16:22:53 BST To: Florian Haftmann florian.haftm...@informatik.tu-muenchen.de Cc: Bertram Felgenhauer bertram.felgenha...@googlemail.com, cl-isabelle-us...@lists.cam.ac.uk I've stumbled across a related issue with find_theorems that certainly seems wrong. I was searching for the theorem Real_Vector_Spaces.dist_norm_class.dist_norm, which is introduced as a type class axiom here: class dist_norm = dist + norm + minus + assumes dist_norm: dist x y = norm (x - y) Calling find_theorems with suitable patterns, such as dist norm (_-_)” does not return this theorem among the results, but clearly it should. Larry ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Problem in AFP near 16e7d42ef7f4
isabelle: 19c277ea65ae tip afp: 16e7d42ef7f4 tip Running Noninterference_Generic_Unwinding ... *** Timeout Noninterference_Generic_Unwinding FAILED (see also /mnt/home/haftmann/data/isabelle/master/heaps/polyml-5.5.2_x86-linux/log/Noninterference_Generic_Unwinding) val it = (): unit Loading theory GenericUnwinding Proofs for inductive predicate(s) rel_induct_auxp Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... ### theory GenericUnwinding ### 1.941s elapsed time, 11.008s cpu time, 0.136s GC time Any hints what could have gone wrong? Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Problem in AFP near 16e7d42ef7f4
Maybe this is hitting the concrete wall set by hardware constraints. I am building on lxbroy10; relevant settings might include ISABELLE_BUILD_JAVA_OPTIONS=-Xmx4096m -Xss2m ISABELLE_PLATFORM32=x86-linux ISABELLE_JAVA_SYSTEM_OPTIONS=-server -Dfile.encoding=UTF-8 -Disabelle.threads=0 ISABELLE_PLATFORM64=x86_64-linux ISABELLE_PLATFORM=x86-linux ISABELLE_SCALA_BUILD_OPTIONS=-encoding UTF-8 -nowarn -target:jvm-1.7 -Xmax-classfile-name 130 In my view lxbroy10 still has some status as a reference machine, and I am seriously concerned as soon as resources appear to be too tiny there. Anybody else experiencing similar problems? Florian Am 25.06.2015 um 15:00 schrieb Florian Haftmann: isabelle: 19c277ea65ae tip afp: 16e7d42ef7f4 tip Running Noninterference_Generic_Unwinding ... *** Timeout Noninterference_Generic_Unwinding FAILED (see also /mnt/home/haftmann/data/isabelle/master/heaps/polyml-5.5.2_x86-linux/log/Noninterference_Generic_Unwinding) val it = (): unit Loading theory GenericUnwinding Proofs for inductive predicate(s) rel_induct_auxp Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... ### theory GenericUnwinding ### 1.941s elapsed time, 11.008s cpu time, 0.136s GC time Any hints what could have gone wrong? Florian ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Problem in AFP near 16e7d42ef7f4
Hi Larry,
thanks for finding out so quickly!
Florian
Am 25.06.2015 um 16:02 schrieb Larry Paulson:
This does it nicely (20s):
apply (simp add: T⇩c_def I⇩c_def)
apply clarify
apply (cases u; elim disjE; simp; blast)
Larry
On 25 Jun 2015, at 14:52, Larry Paulson l...@cam.ac.uk wrote:
I took a look, and it all runs perfectly well, except here:
show xs ∈ T⇩c ∧ ys ∈ T⇩c ∧
ipurge_tr_rev I⇩c id u xs = ipurge_tr_rev I⇩c id u ys ⟶
{x. u = x ∧ xs @ [x] ∈ T⇩c} = {x. u = x ∧ ys @ [x] ∈ T⇩c}
(* The following proof step performs an exhaustive case distinction over
all traces and domains,
and then can take long to be completed. *)
by (simp add: T⇩c_def I⇩c_def, rule impI, (erule conjE)+, cases u,
(((erule disjE)+)?, simp, blast?)+)
The comment doesn’t tell us whether to wait minutes or hours. Clearly this
is a fragile step. Any sort of change could break this.
Larry
On 25 Jun 2015, at 14:00, Florian Haftmann
florian.haftm...@informatik.tu-muenchen.de wrote:
isabelle: 19c277ea65ae tip
afp: 16e7d42ef7f4 tip
Running Noninterference_Generic_Unwinding ...
*** Timeout
Noninterference_Generic_Unwinding FAILED
(see also
/mnt/home/haftmann/data/isabelle/master/heaps/polyml-5.5.2_x86-linux/log/Noninterference_Generic_Unwinding)
val it = (): unit
Loading theory GenericUnwinding
Proofs for inductive predicate(s) rel_induct_auxp
Proving monotonicity ...
Proving the introduction rules ...
Proving the elimination rules ...
Proving the induction rule ...
Proving the simplification rules ...
### theory GenericUnwinding
### 1.941s elapsed time, 11.008s cpu time, 0.136s GC time
Any hints what could have gone wrong?
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
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Problem in AFP near 16e7d42ef7f4
This does it nicely (20s):
apply (simp add: T⇩c_def I⇩c_def)
apply clarify
apply (cases u; elim disjE; simp; blast)
Larry
On 25 Jun 2015, at 14:52, Larry Paulson l...@cam.ac.uk wrote:
I took a look, and it all runs perfectly well, except here:
show xs ∈ T⇩c ∧ ys ∈ T⇩c ∧
ipurge_tr_rev I⇩c id u xs = ipurge_tr_rev I⇩c id u ys ⟶
{x. u = x ∧ xs @ [x] ∈ T⇩c} = {x. u = x ∧ ys @ [x] ∈ T⇩c}
(* The following proof step performs an exhaustive case distinction over
all traces and domains,
and then can take long to be completed. *)
by (simp add: T⇩c_def I⇩c_def, rule impI, (erule conjE)+, cases u,
(((erule disjE)+)?, simp, blast?)+)
The comment doesn’t tell us whether to wait minutes or hours. Clearly this is
a fragile step. Any sort of change could break this.
Larry
On 25 Jun 2015, at 14:00, Florian Haftmann
florian.haftm...@informatik.tu-muenchen.de wrote:
isabelle: 19c277ea65ae tip
afp: 16e7d42ef7f4 tip
Running Noninterference_Generic_Unwinding ...
*** Timeout
Noninterference_Generic_Unwinding FAILED
(see also
/mnt/home/haftmann/data/isabelle/master/heaps/polyml-5.5.2_x86-linux/log/Noninterference_Generic_Unwinding)
val it = (): unit
Loading theory GenericUnwinding
Proofs for inductive predicate(s) rel_induct_auxp
Proving monotonicity ...
Proving the introduction rules ...
Proving the elimination rules ...
Proving the induction rule ...
Proving the simplification rules ...
### theory GenericUnwinding
### 1.941s elapsed time, 11.008s cpu time, 0.136s GC time
Any hints what could have gone wrong?
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
___
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] Euclidean Ring
Hallo,
thanks for all the good work. It's nice to finally see my work
integrated so neatly into HOL.
1. Normalization. Currently, there is normalization_factor such that a
div normalization_factor a yields the normalized elements. My impression
is that the latter should be an operation on its own, say normalize, and
that normalization_factor is a misleading name since it suggests that
actually a * normalization_factor a is the normalized element. Have we
any other plausible name, say »orientation«? The idea is that normalize
and orientation work on integers like abs and sgn.
I do not remember why I chose to do it that way. I do remember weighing
normalization_factor against a ‘normalize’ operation and deciding for
the former. I take it that you have worked with the definitions for a
while now, so if, after that, you think that a ‘normalize’ operation is
better, I defer to your judgement.
As for the terminology, I think I did not find this concept in the
literature and just invented names that seemed reasonable to me at the
time. I agree that normalization_factor perhaps gives the wrong idea; if
you want to change it to something else, I have no objections, but I do
think ‘orient’ sounds a bit strange, especially for rings like the
polynomials.
2. A generic lcm definition. In ordinary lattices, inf and sup are dual
to each other and there is little reason to prefer one over that other.
Concerning gcd and lcm, I have the strong impression that gcd is the
more primitive one and lcm should be solely derived from it. This is
supported by the observation that instantiation proofs get horrible if
you have to derive the characteristic properties of gcd and lcm on, say,
nat, simultaneously. Hence I argue that the specification of
semiring_gcd should contain a plain definition of lcm. Since the plain
semiring_gcd is not supposed to know anything about normalization, this
would lead to a plain »lcm a b = a * b div gcd a b«, in contrast to the
current »lcm a b = a * b div gcd a b div normalization_factor (a * b)«.
Do you foresee any difficulties here?
I think so. With this definition, ‘lcm (2X²) (2X²)’ would return ‘4X²’,
which is certainly not what we want. If you put this definition in
semiring_gcd, you cannot change it later either. Or am I missing
something here?
3. Gcd/Lcm. In your Gcd/Lcm approach, Lcm is the »more primitive«
definition. Did you just take this over from src/HOL/GCD.thy, or is
there a deeper reason to do it this way round?
I don't remember. I remember that it took me quite a long time to make
this definition work; the case of what to do when you want to take the
Gcd/Lcm of an infinite set was tricky. I think I was under the
impression that handling the case of infinitely many elements was easier
to handle in Lcm, but I do not remember why. I may also be mistaken.
A further observation concerns algebraic closedness of normalized
elements. The properties »normalization_factor 1 = 1« and
»normalization_factor (a * b) = normalization_factor a *
normalization_factor b« state that normalized elements form a
multiplicative group. I did not find a reasonable characterization for
the additive behaviour, i.e. a way to enforce that for int normalization
goes for positive elements only and not a funny mixture like 1, -2, 3,
4, 5, -6, 7, -8. The tempting option to demand closedness under addition
does not work for polynomials, since x + x = 2 * x is not normalized any
longer. On the other hand, the theory works without any such enforcement.
Well, normalisation can be seen as a map sending a ring element to the
equivalence class of all associated elements. In the case of units,
there is an obvious candidate for a canonical representative for this
equivalence class, namely 1. For other equivalence classes, I do not
think that is the case. One could intuitively argue that, in the ring of
polynomials, X is a better representative than -X. In other rings,
like the ring of Gaussian integers, things are not so clear. What should
be the representative of the associated elements {1+i, 1-i, i-1, -1-i}?
I do not think there is an obvious candidate.
I therefore think that the choice of what is normalised and what is not
is somewhat arbitrary and it is therefore not possible to find a
restriction that does what you want to do in general. Again, I could be
wrong about this; it has been one and a half years since I last worked
on this.
I am wondering about changeset f2f1f6860959, ‘generalized to definition
from literature, which covers also polynomials’. Where did you find this
in the literature? What does it achieve?
Cheers,
Manuel
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
