Re: [isabelle] inductive_set and ordinal induction



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




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