[isabelle-dev] inductive_set: Bad monotonicity theorem
Lawrence Paulson
LP15 at CAM.AC.UK
Fri Aug 26 16:06:34 CEST 2011
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
More information about the isabelle-dev
mailing list