[isabelle-dev] Conversions between ('a * 'a) set and 'a => 'a => bool relations
Lars Noschinski
noschinl at in.tum.de
Mon Mar 12 15:14:55 CET 2012
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
More information about the isabelle-dev
mailing list