# Re: [isabelle] General nitpick/sledge... [got a more flexible solution anyway]

`By asking questions here, it makes me think harder and work harder, to
``try and keep from saying something that's wrong.
`

`First, one of the biggest things I got out of this is the idea of
``running Nitpick on both a theorem and it's negation. I'm thinking that
``if both a "theorem" and its negation are both false, then that's a
``problem. I'd still like to ask that question, "Uh, if Nitpick finds a
``counterexample, does that mean..." Negative logic can mess me up.
``"Inconsistent" isn't part of the vocabulary of a typical math education.
``I have to deprogram myself.
`

`I have just now had a revelation. If I can run Nitpick on a theorem and
``its negation, then I can run Sledgehammer on a theorem and its negation.
``I'll need to write some macros so I don't spend my life cutting,
``pasting, and typing, and eventually get that quad core notebook. I see
``that dummy_thf prover again. It never proves a thing.
`

`My more-flexible solution is to not use the HOL "=", but use my own
``undefined "EQ", like this:
`
consts eqS::"[sT,sT] => bool" (infixl "EQ" 51)

`Of course, I still want to make it easy to experiment, and switch in and
``out the HOL "=", so I comment out eqS, and use:
`
abbreviation eqS::"[sT,sT] => bool" (infixl "EQ" 51) where "x EQ y == x = y"

`My constant eqS is more conceptually satisfying because it doesn't make
``any sense to use it if it hasn't been defined in any way. If I use it
``without defining it, I end up with that same inconsistency that I get
``when I use the HOL "=", but the HOL "=" is defined, though it still
``might not make sense to use it the way I was using it.
`

`I also get an <-> that's not identical to my equal operator. As to how
``easy or hard it makes things to prove, I don't anything about that yet.
`
Regards,
GB

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