# [isabelle-dev] Problem in AFP near 16e7d42ef7f4

Larry Paulson lp15 at cam.ac.uk
Thu Jun 25 15:52:26 CEST 2015

```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.haftmann at informatik.tu-muenchen.de> wrote:
>
> isabelle: 19c277ea65ae tip
> afp: 16e7d42ef7f4 tip
>
> Running Noninterference_Generic_Unwinding ...
> *** Timeout
> Noninterference_Generic_Unwinding FAILED
> /mnt/home/haftmann/data/isabelle/master/heaps/polyml-5.5.2_x86-linux/log/Noninterference_Generic_Unwinding)
>
> val it = (): unit
> 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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

```