> I could not believe that recdef could not be replaced by fun, so here is > the patch that removes usages of recdef from Decision_Procs. The proof > rules that come out of the function package are fine (one just needs a > few split_format (complete) attributes in a few places).
Let me emphasize this particular point. When you give a specification
in Isabelle, there are two expectations:
a) The system is able to construct something which satisfies this
specification (the primitive definition)
AND
b) The system provides a mechanism to actually *reason* about resulting
properties in a (natural, intuitive, straight-forward) way (for
non-trivial specifications, typically an induction rule)
Practically, a) is of little (or at least reduced) value without b)
Hence, if there is evidence that working around function's pattern
explosion diminishes b), it is definitely a restriction and not just a
matter of taste how to construct and design specifications.
The question what can really be done to improve the situation, however,
is written on a different sheet.
Florian
P.S: Just a remark: in my personal view b) is even the dominant role of
advanced specification tools – the way how a specification is given
suggests how proofs can be conducted successfully. Hence I still prefer
»primrec« if applicable since this makes it immediately clear that
proofs most likely will require induction on the corresponding datatype.
--
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
