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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
