[isabelle-dev] inductive_set: Bad monotonicity theorem

[Lawrence Paulson]

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")

This doesn't make sense, because Pow_mono is

?A \<subseteq> ?B \<Longrightarrow> Pow ?A \<subseteq> Pow ?B

Looking in the file Tools/inductive_set, I decided the culprit might be this:

val mono_add_att = to_pred_att [] #> Inductive.mono_add;

This looks like it is transforming the monotonicity theorem into the language of predicates.

I replaced it by

val mono_add_att = Inductive.mono_add;

But this didn't help at all. If anybody has any suggestions, please let me know. Otherwise there is no way to make progress with Probability.

Larry