[isabelle-dev] inductive_set vs. 'a set

Makarius makarius at sketis.net
Mon Jan 9 14:31:21 CET 2012

There is another drop-out concerning 'a set (in Isabelle/05a82dd869ed):

   well_formed_gterm' :: "('f \<Rightarrow> nat) \<Rightarrow> 'f gterm set"
   for arity :: "'f \<Rightarrow> nat"
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 

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.


More information about the isabelle-dev mailing list