[isabelle] How to delete rules applied by clarify



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.