Re: [isabelle] inductive_set and ordinal induction



Dear Christoph,

The general answer first:
The rules generated by the inductive package suffice to prove that the predicate equals the internal construction. Thus, you can prove the same as you can prove with access the internal construction. However, this proof of equivalence can be quite tedious (which is why I support making the internal construction accessible).

In the specific case of lfp_ordinal_induct, you just have to look at its proof. It uses three properties of lfp and f:
1. Monotonicity of f: You have to prove this yourself manually, but this is doable.
2. lfp_unfold: This corresponds to X.simps[abs_def]
3. lfp_lowerbound: This corresponds to X.induct

Hope this helps,
Andreas

On 27/10/15 11:01, Christoph Dittmann wrote:
On 10/27/2015 09:56 AM, Andreas Lochbihler wrote:
You are right in that the rules generated by the inductive package
suffice for proving.

I don't see how ordinal induction (like lfp_ordinal_induct)
   "[| ... |] ==> P X"
is derivable from the pointwise induction rule
   "[| X x; ... |] ==> P x"
provided by the inductive package.

Or is it derivable?

Best,
Christoph






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