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
separately.
Thanks a lot,
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
