[isabelle-dev] lemma addition

[Dmitriy Traytel]

Am 25.07.2013 04:16, schrieb 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?
I think the usual policy is to have at least two applications before 
adding such a lemma. However we use the corresponding lemma about 
conversep in the (co)datatype package. Since the latter will sooner or 
later become part of the HOL session anyway, I think it's fine to add 
both versions to Relation.thy. I'll do that (under the name 
converse(p)_mono).

Dmitriy

PS: for me this looks like an isabelle-users thread ;-)