[isabelle] Isabelle2008: Strange behavior with sets and intro!: ext or intro!: le_funI
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"
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
apply (rule le_funI)
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and