Email Gateway (Aug 19 2022 at 14:18): Email Gateway (Aug 19 2022 at 14:18):From: Peter Lammich <lammich@in.tum.de>
Hi list,
when doing
lemma "~ a \<subseteq> b ==> P"
apply clarify_step
I get the subgoal
!!x. [|~P; x:a|] ==> x:b
However, I cannot find any rule in the claset (print_claset) that seems
to be responsible for this transformation.
A deeper inspection reveals that there is the rule
"¬ A1 ⊆ B1 ⟹ (⋀x. ¬ R ⟹ x ∈ A1 ⟹ x ∈ B1) ⟹ R"
in the "safep_netpair" - component of the claset. (which is not printed
by print_claset)
Moreover, there seems to be no way to get the rule out there. A
[rule del] just sais "undeclared classical rule".
So what is going on here, and, more important:
How to stop clarify from doing this transformation, and leaving the
original conclusion of the subgoal intact?
Best,
Peter
Email Gateway (Aug 19 2022 at 14:18):From: Peter Lammich <lammich@in.tum.de>
Here is a partial answer to my question that I found when inspecting the
problem further:
The classical reasoner is set up to add, for each introduction rule,
also an elimination rule that is produced by "swapping" the intro-rule,
i.e. resolving with "~ P ==> (~ R ==> P) ==> R".
This creates the rule that I found in the safep_netpair - component,
from the "subsetI" - rule.
It looks like it is not possible to get rid of the swapped rule while
keeping the original rule?
Email Gateway (Aug 19 2022 at 14:19):From: Lawrence Paulson <lp15@cam.ac.uk>
The point is that logically there is no difference between
"~ a \<subseteq> b ==> P”
and
“~P ==> a \<subseteq> b”.
The classical reasoner is designed to do the same thing in both cases.
You could try some other proof method, such as intro, for finer control over which rules are applied.
Larry Paulson
Email Gateway (Aug 19 2022 at 14:19):From: Makarius <makarius@sketis.net>
More on the design of the classical reasoner is available in
http://isabelle.in.tum.de/dist/Isabelle2013-2/doc/isar-ref.pdf section
9.4.
That is a refurbished version of really ancient explanations by Larry, but
this material is still interesting, and should be up-to-date concerning
current Isabelle.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC