Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Summing/subtracting functions


view this post on Zulip Email Gateway (Aug 18 2022 at 17:20):

From: Steve W <s.wong.731@gmail.com>
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

view this post on Zulip Email Gateway (Aug 18 2022 at 17:20):

From: Christian Sternagel <christian.sternagel@uibk.ac.at>
Hi,

you are probably searching for

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

cheers

chris

view this post on Zulip Email Gateway (Aug 18 2022 at 17:20):

From: Brian Huffman <brianh@cs.pdx.edu>
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.


Last updated: Mar 28 2024 at 20:16 UTC