[isabelle] Isabelle2008: Strange behavior with sets and intro!: ext or intro!: le_funI



Hi all,

I just tested some of my theories with Isabelle2008, and encountered the following strange behaviour:

Given a lemma:
 lemma fixes S:: "'a \<Rightarrow> 'b set" and S' shows "S'\<le>S"

I do
 apply (clarify intro!: le_funI)
and would expect (as in Isabelle2007):
 !!x xa. xa : S' x ==> xa : S x

instead, I get the subgoal:
 !!x xa. S' x xa ==> S x xa

In Isabelle 2007, this would not even typecheck, but Isabelle2008 seems to accept it valid (I think, using the characteristic function of the set). If this is intentional, how to get to the "xa : S x" representation again ? A search for lemmas of the form "?S ?b ==> ?b : ?S" gives no results, neither the trial to have "xa\<in>S x" using `S x xa` by blast or auto.

Btw.: Doing
   apply (rule le_funI)
   apply clarify

instead of (clarify intro!: le_funI)
gives the expected results, but is sometimes more tedious to use, e.g. if there are some preceeeding transformations.

I encountered the same Problem with lemma ext.

Regards
 Peter







This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.