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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
