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

[Lars Noschinski]

On 09.03.2012 00:14, Stefan Berghofer wrote:
> Florian Haftmann wrote:
>> * This is mainly a question to Stefan: there are some theorems
>> commented out (e.g. »thm sym_INTER [to_pred]«) on which
>> pred_set_conv chokes.  I guess this is due to a higher-order
>> situation, but I would be reassuring if you can confirm that.
>
> I have fixed this bug now, see changeset b1d15637381a. Note that
> converting the above theorem (and the other theorems in Relation.thy
> marked with "FIXME") to predicate notation requires the generalized
> versions of theorems INF_INT_eq2 and SUP_UN_eq2, which should replace
> the more specific versions.

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



   -- Lars