[isabelle] Baffling behavior: unable to prove P=>P



At a certain point in my proof I have the goal

 m = 0 ==> N = 0 ==> card {l. l = [] ∧ (∀n∈set l. n = 0)} = Suc 0

OK, Isabelle failed to do this with auto so I inserted some statements
before:

    have l: "{l::int list. l = [] ∧ (∀n∈set l. n = 0)} = {[]}"
      by auto
    hence l2: "card {l::int list. l = [] ∧ (∀n∈set l. n = 0)} = 1"
      by auto

Now apply (insert l2, auto) gives

 m = 0 ==>
    N = 0 ==>
    card {l. l = [] ∧ (∀n∈set l. n = 0)} = Suc 0 ==> card {l. l = [] ∧
(∀n∈set l. n = 0)} = Suc 0

The two statements are exactly the same (I checked the color of the
variables too, anyway they're all bound). try0 fails and sledgehammer
hangs. What gives?

-Holden



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