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

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Mon Mar 12 15:47:24 CET 2012

Hi Lars,

> 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

I would suggest to push the changes as they are now since they are a 
step into the right direction; I have to look at the remaining problem 

Thanks a lot,


PGP available:

More information about the isabelle-dev mailing list