Email Gateway (Aug 19 2022 at 13:30): Email Gateway (Aug 19 2022 at 13:30):From: "Roger H." <s57076@hotmail.com>
Hi,
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?
Thank you!
Email Gateway (Aug 19 2022 at 13:30):From: Manuel Eberl <eberlm@in.tum.de>
Hallo,
in this case: apply (simp add: fun_upd_twist)
Whether this works for more complicated statements of this kind, I
cannot say. In particular, I suspect that this lemma could lead the
simplifier to loop in some instances – I don't know whether the
simplifier recognises that this lemma represents a kind of commutativity
and treats it accordingly automatically.
Also, I recommend you use find_theorems to find lemmas of this kind, or
sledgehammer if you don't want to search manually.
Cheers,
Manuel
Email Gateway (Aug 19 2022 at 13:30):From: IG BI <igbi@gmx.com>
Hi,
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:
http://isabelle.in.tum.de/website-Isabelle2013-2/dist/Isabelle2013-2/doc/prog-prove.pdf
http://isabelle.in.tum.de/website-Isabelle2013-2/dist/Isabelle2013-2/doc/tutorial.pdf
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:
http://www.cs.colorado.edu/~siek/7000/spring07/
http://www.cs.colorado.edu/~siek/7000/spring07/isabelle-notes.pdf
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.
Regards,
GB
Email Gateway (Aug 19 2022 at 13:30):From: IG BI <igbi@gmx.com>
I clarify some of what I said, where what I said are the statements of a
novice.
First, the basic idea behind what I said is that if by(auto) is
proving your formula above, I don't see why you need to add any rules.
The auto method calls simp, among other things, and it seems to be
doing a good job with what it has.
Also, if you did want to add custom rules, then you would create rules
more general than your formula, which I suppose you already know.
However, if auto already can solve the identity, then why add
anything? Maybe there are reasons, such as optimization.
You can use simp add: myThm to add a simp rule for simp to use,
but again, it found everything it needed.
The problem with mailing list subscriptions is that there's not an
option for it to be "read only". The web page has that functionality,
but it's convenient to get everything by email to be able to archive the
ones I want for future reference.
I'd rather only have "write mode" capability most of the time, but I
have it all the time, which is unfortunate.
Regards,
GB
Last updated: Oct 26 2025 at 16:24 UTC