Re: [isabelle] equality of functions

On 1/10/2014 9:54 AM, Roger H. wrote:

the lemma "[1 ↦ [4], 2 ↦ [5]] =  [2 ↦ [5], 1 ↦ [4]]" 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 MHonArc.