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