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 <l...@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.haftm...@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-...@in.tum.de
>>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>>
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-...@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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
