On 25.07.2013 04:16, Christian Sternagel wrote:
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].
auto's call to safe splits it to
goal (2 subgoals):
1. ⋀a b. A¯ ⊆ B¯ ⟹ (a, b) ∈ A ⟹ (a, b) ∈ B
2. ⋀a b. A ⊆ B ⟹ (b, a) ∈ A ⟹ (b, a) ∈ B
Both of which are discharged by blast. If we look at the theorems blast
uses to prove
⋀a b. A¯ ⊆ B¯ ⟹ (a, b) ∈ A ⟹ (a, b) ∈ B
(how this can be done is described in Section 3.7 of the Isabelle
Cookbook), we see that Relation.converse_iff plays a role, which was
declared with the iff attribute.
-- Lars
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
