Re: [isabelle] inductive_set and ordinal induction

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?


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.