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?

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




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