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

[Florian Haftmann]

Hi all,

> 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

the issue is that order of pred_set_conv declarations matters as soon as
the lhss reps. rhss overlap.  If the most generic declarations are put
first, it works as expected.  Done in hg.

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20120317/f9575ed7/attachment.sig>