[isabelle-dev] inductive_set: Bad monotonicity theorem
Brian Huffman
brianh at cs.pdx.edu
Fri Aug 26 18:07:56 CEST 2011
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
More information about the isabelle-dev
mailing list