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

Never mind: it turned out one of the statements is l::nat list instead.
Still, sneaky...
-Holden
2014-08-27 23:10 GMT+01:00 Holden Lee <hl422 at cam.ac.uk>:
> 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.*