[isabelle-dev] lemma addition

[Christian Sternagel]

Dear developers,

While the following lemma is proved automatically

   lemma converse_subset:
   "A¯ ⊆ B¯ ⟷ A ⊆ B" by auto

I'm not sure exactly how, since "simp_trace" shows no application of 
simplification rules and neither of the rules suggested by different 
ATPs through sledgehammer are -- as far as I can tell -- automatic rules 
in the sense of [intro], [elim], [dest].

Sledgehammer indicates that the following lemmas are relevant in the proof:

always: converse_Un converse_converse
plus either of:
   - inf_absorb2 and inf_le1
   - subset_Un_eq
   - le_iff_inf

Anyway, I found this lemma useful to have around explicitly. Maybe it 
could be added to Relation.thy? Any thoughts?

cheers

chris