Re: [isabelle] Summing/subtracting functions
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.
On Mon, Mar 7, 2011 at 4:10 AM, Steve W <s.wong.731 at gmail.com> wrote:
> Is the summation (and/or subtraction) of functions already defined in the
> 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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and