[isabelle-dev] Problem in AFP near 16e7d42ef7f4

[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 <lp15 at 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.haftmann at 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-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev