[isabelle-dev] inductive_set vs. 'a set

[Lawrence Paulson]

I got this message several times when converting theories. There is a workaround, but nevertheless, I think this is a bug.
Larry

On 9 Jan 2012, at 13:31, Makarius wrote:

> There is another drop-out concerning 'a set (in Isabelle/05a82dd869ed):
> 
> inductive_set
>  well_formed_gterm' :: "('f \<Rightarrow> nat) \<Rightarrow> 'f gterm set"
>  for arity :: "'f \<Rightarrow> nat"
> where
> step[intro!]: "\<lbrakk>args \<in> lists (well_formed_gterm' arity);
> 		length args = arity f\<rbrakk>
>               \<Longrightarrow> (Apply f args) \<in> well_formed_gterm' arity"
> monos lists_mono
> 
> *** Bad monotonicity theorem:
> *** {x. ?A x} <= {x. ?B x} ==> {x. listsp ?A x} <= {x. listsp ?B x}
> *** At command "inductive_set" (line 153 of "~~/doc-src/TutorialI/Inductive/Advanced.thy")
> 
> 
> That is probably a bit too exotic to expect NEWS to say what needs to be done.  Nonetheless I am curious about the reason of this failure.
> 
> 
> 	Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev