Re: [isabelle] inductive_set and ordinal induction
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,
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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and