[isabelle-dev] inductive_set: Bad monotonicity theorem

[Lawrence Paulson]

Thank you, that may be a useful workaround. But isn't the current behaviour simply wrong? It transforms a monotonicity theorem into something of the wrong format.
Larry

On 26 Aug 2011, at 17:07, Brian Huffman wrote:

> 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