Re: [isabelle] Meta_impE and other tactics



Hi Peter,

your reasoning is not sound: Take, e.g., A=B=C=False, and D=E=True.
Then, your goal reads
[| [| False ; False |] ==> False ; True ; True ; False ==> True ; False ==> True |] ==> False

which simplifies to False, whereas you want to rewrite this to
[| [| True; True |] ==> False; True; True |] ==> False

which is True. The problem is that you need both A and B to show C, but you only have D and E, which are weaker than A and B.

Best regards,
Andreas

Peter Chapman schrieb:
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, I rewrite using the A ==> D and B ==> E inside the inner [| |] to get

[| [| D ; E |] ==> C ; D ; E |] ==> C

to

C

Is this logically sound? How can I rewrite the A and B within the inner brackets?

Thanks in advance

Peter









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