Re: [isabelle] How to delete rules applied by clarify
Here is a partial answer to my question that I found when inspecting the
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?
On Mo, 2014-04-14 at 19:49 +0200, Peter Lammich wrote:
> 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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and