Re: [isabelle-dev] Problem in AFP near 16e7d42ef7f4

2015-06-25 Thread Larry Paulson
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

[isabelle-dev] Fwd: [isabelle] find_theorems and locales

2015-06-25 Thread Larry Paulson
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

[isabelle-dev] Problem in AFP near 16e7d42ef7f4

2015-06-25 Thread 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

Re: [isabelle-dev] Problem in AFP near 16e7d42ef7f4

2015-06-25 Thread Florian Haftmann
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

Re: [isabelle-dev] Problem in AFP near 16e7d42ef7f4

2015-06-25 Thread Florian Haftmann
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

Re: [isabelle-dev] Problem in AFP near 16e7d42ef7f4

2015-06-25 Thread 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

Re: [isabelle-dev] Euclidean Ring

2015-06-25 Thread Manuel Eberl
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