[isabelle-dev] Conversions between ('a * 'a) set and 'a => 'a => bool relations

[Florian Haftmann]

>> I have now patches queued to enabled all of the commented out theorems
>> and pred_set_conv declarations, except for the generalited versions of
>> SUP_UN_eq and INF_INT_eq. Using generalized versions of SUP_UN_eq
>> changes the theorems generated by inductive set in a negative way:

>> inductive_set
>> TFin :: "'a set set \<Rightarrow> 'a set set set"
>> for S :: "'a set set"
>> where
>> succI: "x : TFin S \<Longrightarrow> succ S x : TFin S"
>> | Pow_UnionI: "Y : Pow(TFin S) \<Longrightarrow> Union(Y) : TFin S"
>>
>> generates for example the theorem:
>>
>> TFin.Pow_UnionI: ?Y ∈ Pow (TFin ?S) ⟹ (⋃i ∈ ?Y. i) ∈ TFin ?S
>>
>> instead of:
>>
>> TFin.Pow_UnionI: ?Y ∈ Pow (TFin ?S) ⟹ ⋃?Y ∈ TFin ?S

When I adapted Relation.thy, it appeared to me suspicious that SUP_UN_eq 
and INF_INT_eq where not as general as they would naturally be;  maybe 
the problem you experience now has been experienced already by Stefan 
when he introduced this.  Stefan, does this sound somehow familiar to you?

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de