Re: [isabelle] equality of functions
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.
On 10/01/14 16:54, 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?
> Thank you!
This archive was generated by a fusion of
Pipermail (Mailman edition) and