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.