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



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


On 14 Apr 2014, at 18:49, Peter Lammich <lammich at in.tum.de> 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.