[isabelle-dev] lemma addition
makarius at sketis.net
Thu Aug 1 17:19:20 CEST 2013
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
* 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"
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.)
More information about the isabelle-dev