Email Gateway (Aug 18 2022 at 11:59): Email Gateway (Aug 18 2022 at 11:59):From: Peter Lammich <peter.lammich@uni-muenster.de>
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
Email Gateway (Aug 18 2022 at 12:00):From: Makarius <makarius@sketis.net>
This is due to a fundamental change in HOL, see the NEWS where it says
``Turned the type of sets "'a set" into an abbreviation for "'a =>
bool"''; there are also some hints how to convert existing theories.
Makarius
Last updated: May 03 2024 at 04:19 UTC