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:
> 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!

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