Re: [isabelle] Meta_impE and other tactics



Am Montag, den 16.03.2009, 16:11 +0000 schrieb Peter Chapman:
> Hi
> 
> I have the following premisses and goal (the details are unimportant,  
> it is the structure which is important):
> 
> [|  [| A ; B |] ==> C ; D ; E ; A ==> D ; B ==> E |] ==> C
> 
> I think this should be provable

Indeed it is not, if you enter

lemma "[| [| A ; B |] ==> C ; D ; E ; A ==> D ; B ==> E |] ==> C"

Isabelle answers

Counterexample found:

A = False
B = False
C = False
D = True
E = True


> , I rewrite using the A ==> D and B ==>  
> E inside the inner [| |] to get
> 
> [| [| D ; E |] ==> C ; D ; E |] ==> C

This is actually not sound as the occurrences of A and B are negative.
Just because you need A and A implies D you can't use D instead. On the
Other hand, if you have D and D implies A you may use A. If you reverse
the other implications the thing becomes provable.

lemma "[|  [| A ; B |] ==> C ; D ; E ; D ==> A ; E ==> B |] ==> C"
by simp


> to
> 
> C
> 
> Is this logically sound?  How can I rewrite the A and B within the  
> inner brackets?
> 
> Thanks in advance
> 
> Peter



-- 
Gruß
Christian Doczkal

Attachment: smime.p7s
Description: S/MIME cryptographic signature



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