Re: [isabelle] Meta_impE and other tactics



Peter,

On Mon, 2009-03-16 at 16:11 +0000, Peter Chapman wrote:
> 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 [...]

it's not.  Isabelle finds a counterexample automatically:

  Counterexample found:
  
  A = False
  B = False
  C = False
  D = True
  E = True

If some of the implications are the other way round, the statement
becomes provable, e.g., by simp:

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

Regards,
Tjark






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