[isabelle-dev] lemma addition

[Makarius]

On Thu, 25 Jul 2013, Lars Noschinski wrote:

> 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.

I did not understand this mysterious reference.  Which version of the 
Cookbook, which page exactly?

Using only canonical information reveals these possibilities that might be 
little known:

   * print_options: blast_trace, blast_stats, but this looks a bit chatty
     and of limited practical use

   * method "step" (see isar-ref manual)

     lemma "A¯ ⊆ B¯ ⟷ A ⊆ B"
       apply step
       apply step
       apply step
       apply step
       apply step
       apply step
       apply step
       apply step
       apply step
       done

Note that these steps refer to the classic Classical Reasoner by Larry 
(safe, fast, best), while blast might work slightly differently.

(This refers to Isabelle/b7a83845bc93.)


 	Makarius