[isabelle-dev] Duraraion of AFP session AODV
florian.haftmann at informatik.tu-muenchen.de
Thu Nov 27 11:59:48 CET 2014
> The development includes a single main model with associated invariant
> proofs and five variant models each with updated proofs. The protocol
> model only changes slightly in each variant and only a few lemmas
> usually require updating to reestablish the main property. We
> untangled as many dependencies as we could, but ultimately we did not
> find a better solution than copy-paste-modify. We tried to minimize
> changes between the variants so that a diff only shows relevant
> This idea of variant models seems quite natural to me—one of the
> advantages of mechanising such models and proofs is the ease of
> experimenting with variations to the model—and I think it would be
> worthwhile to solve the problem properly but I do not have any good
> ideas for the present.
I guess you have already considered using locales to abstract over the
different bootstrapping properties?
> 2. A handful of the sledgehammer generated proofs are quite intensive.
> I would like to fix these by doing more manual work (i.e., more
> steps in Isar), I just have to find the time.
So, a starting step would be to open the timing panel in Isabelle/jEdit
and start working on the most time-consuming metis-proofs? Would be a
nice task for a maintainance volunteer.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 181 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev