[isabelle-dev] lemma addition
Lars Noschinski
noschinl at in.tum.de
Thu Jul 25 09:16:08 CEST 2013
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
More information about the isabelle-dev
mailing list