On 27/10/2015 16:16, Johannes HÃlzl wrote:
As far as I understood Stefan, the _def theorems are actually internal. I think you should be on the save side with your last suggestion, i.e. defining the functional F_def and then prove: inductive X ... definition F where "F = ..." lemma "X = lfp F" unfolding X_def F_def by simp Then you should be on the save side if we change the internals of the inductive package.
No, you are not: the simp proof may well fail if X_def changes, and if it disappears altogether the unfolding breaks.
- Johannes Am Dienstag, den 27.10.2015, 15:22 +0100 schrieb Christoph Dittmann:Dear Johannes, thank you, and also Andreas for your answers. On 10/27/2015 02:26 PM, Johannes HÃlzl wrote:As Andreas points out, you can directly use the definition of the predicate (<inductive pred>_def) and then manually prove monotonicity. Then you can apply lfp_ordinal_induct.<inductive_pred>_def is "<inductive_pred> == lfp <something_very_long>". Can I somehow bind <something_very_long> to a name so that I do not need to copy&paste it? I tried pattern matching like note X_def (is "_ == lfp ?f") but this doesn't work (the isar manual agrees). Is <inductive_pred>_def considered part of the stable interface to the inductive package? If not, maybe my approach of redefining the inductive predicate explicitly via lfp and proving equality could be more robust against changes in the inductive package? Best, Christoph
Description: S/MIME Cryptographic Signature