Re: [isabelle] Summing/subtracting functions



Hi,

you are probably searching for

Lattices.fun_diff_def: "?A - ?B = (λx. ?A x - ?B x)"

cheers

chris


On 03/07/2011 01:10 PM, Steve W wrote:
Hi,

Is the summation (and/or subtraction) of functions already defined in the
library?

axiomatization
f :: "nat =>  nat" and
g :: "nat =>  nat" where
ax1 : "ALL x. f x = 2" and
ax2 : "ALL x. g x = 1"

lemma "f - g = g"
using ax1 ax2
apply auto

Presuming it's not, why not? It seems that there's only one definition for
summation/subtraction of functions anyway, i.e. "f - g<-->  ALL x. f x - g
x" -- is it not?

Thanks

Steve







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