Re: [isabelle] inductive_set and ordinal induction

Stefan, you could call it something like mono_internal, thus expressing that it may change.


On 28/10/2015 09:48, Johannes HÃlzl wrote:
Yes, it should be considered fixed, and I support Andreas' idea of
exporting the monotonicity theorem.

  - Johannes

Am Dienstag, den 27.10.2015, 16:27 +0100 schrieb Tobias Nipkow:
On 27/10/2015 16:16, Johannes HÃlzl wrote:
As far as I understood Stefan, the _def theorems are actually internal.

But it is exported, and hasn't changed over many years and I don't see any
impending change there either.


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.

   - 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.