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