[isabelle-dev] Duraraion of AFP session AODV

[Florian Haftmann]

Hi Tim,

> 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
> changes.

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

Cheers,
	Florian

-- 

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: 181 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20141127/e163b1d7/attachment.sig>