Re: [isabelle] Summing/subtracting functions



Hi Steve,

Grepping for "instantiation \"fun\"", I found
HOL/Library/Function_Algebras.thy. It defines plus, zero, times, and
one for function types.

Note that subtraction and negation for functions are already defined
by default in the main HOL image (in HOL/Lattices.thy), to implement
the difference and complement operations for sets.

- Brian

On Mon, Mar 7, 2011 at 4:10 AM, Steve W <s.wong.731 at gmail.com> 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.