Re: [isabelle] How to delete rules applied by clarify

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?


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?
> Best,
>   Peter

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.