[isabelle-dev] Remaining uses of defer_recdef?

[Florian Haftmann]

> 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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 198 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20150607/503cd966/attachment.sig>