[isabelle-dev] inductive_set: Bad monotonicity theorem

[Brian Huffman]

On Fri, Aug 26, 2011 at 7:06 AM, Lawrence Paulson <LP15 at cam.ac.uk> wrote:
> I am trying to process the following declaration in Probability/Sigma_Algebra:
>
> inductive_set
>  smallest_ccdi_sets :: "('a, 'b) algebra_scheme \<Rightarrow> 'a set set"
>  .
>  .
>  .
>  monos Pow_mono
>
>  I get the following error message (for the version with set types):
>
> *** Bad monotonicity theorem:
> *** {x. ?A x} \<subseteq> {x. ?B x} \<Longrightarrow> {x. Powp ?A x} \<subseteq> {x. Powp ?B x}
> *** At command "inductive_set" (line 1125 of "/Users/lp15/isabelle_set/src/HOL/Probability/Sigma_Algebra.thy")

I came across this same problem when adapting Lazy-Lists-II to work
with a set type. Here is my changeset:

http://afp.hg.sourceforge.net/hgweb/afp/afp/rev/3c3a4115e273

I got the idea for the workaround from the following line in
Predicates.thy from the distribution:

lemmas Powp_mono [mono] = Pow_mono [to_pred pred_subset_eq]

Hope this helps,

- Brian