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