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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
