[isabelle-dev] lemma addition

[Lars Noschinski]

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