[isabelle-dev] lemma addition
c.sternagel at gmail.com
Thu Jul 25 04:16:11 CEST 2013
While the following lemma is proved automatically
"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
Anyway, I found this lemma useful to have around explicitly. Maybe it
could be added to Relation.thy? Any thoughts?
More information about the isabelle-dev