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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
