Re: [isabelle] equality of functions
On 1/10/2014 9:54 AM, Roger H. wrote:
the lemma "[1 ↦ , 2 ↦ ] = [2 ↦ , 1 ↦ ]" can be proven by auto,
but is there any automatic proof, meaning some existing lemma, which i can add to the simplifier,
so that such identities that occur in the middle of proofs are solved automatically?
Your question is vague enough that I have a lot of freedom here to be
right, rather than wrong. I take "solved" to mean that either the
formula resolves to `True`, or that the left-hand side of `=` will be
replaced by the right-hand side.
If, with auto, you can prove the formula you stated as a lemma, then
anywhere that the formula is a proof goal, the command `apply(auto)`
will prove it.
To find the specifics of how `auto` is proving your formula, you would
have to "investigate", such as using `simp_trace`, though `simp` rules
may not be the only thing `auto` is using.
If you still feel the need to have a custom rule for your formula, then
you just add it as a `simp` rule, as others have explained, with the
intent that the left-hand side of the formula will be replaced with the
right-hand side, or that "=" will resolve to "True". However, it's
possible that your `simp` rule will never be used, because other `simp`
rules might get to it first and do some rewriting, with the result that
your rule can no longer be applied.
Because it takes so much work to work through textbooks and tutorials, I
get value from questions that other's ask and that are answered by
others. However, for a more comprehensive knowledge on some of these
basics, I recommend two distribution tutorials:
I also pick one non-distribution web page by Jeremy Siek that, for my
needs, will be very helpful in learning how to do non-auto natural
deduction proof steps:
I myself have yet to work through any of these completely, so at times,
I feel the urge to lash out at the establishment, and become a
revolutionary in the Eastern hemisphere.
What could be easy, though time-consuming, becomes hard, because the
right kind of textbooks for Isabelle don't exist, such as Martin
Odersky's book on Scala, his Coursera video on Scala, and the 10 or so
other textbooks that take you from beginning to moderate level Scala.
Controlling my emotions, and forcing myself to think rationally, I come
up with a logical argument as to why affairs are the way they are,
though I have little ability to implement such an argument in
Isabelle/HOL, other than with Sledgehammer, auto, simp, fastforce, fast,
presburger, etc. You get the picture.
Thinking rationally, I then feel no obligation to become a revolutionary
in the Eastern hemisphere. Rather than do the tedius work of working
through tutorials, I make an easy contribution to the mailing list, it
being 17:48 in the German part of the Eastern hemisphere, on Friday, the
Germans having gone home for the weekend.
This archive was generated by a fusion of
Pipermail (Mailman edition) and