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.


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