[isabelle-dev] Problem in AFP near 16e7d42ef7f4

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

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 198 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20150625/fc60a862/attachment.sig>