Email Gateway (Aug 18 2022 at 16:51): Email Gateway (Aug 18 2022 at 16:51):From: Eg Gloor <egglue@gmail.com>
Hello list,
I'm still picking up Isabelle and thought I might try out some of the axioms
posted here earlier (which seemed to be consistent). I've made some
amendments just for experimenting. Assume we have:
axiomatization
S :: "real set" and
foo :: "real => real" and
bar :: "real => real" and
bax :: "real => real" and
c :: real
where ax1: "ALL f g. (ALL x y. x > c & y > c <-> f x = g y) --> f = g"
and ax2: "ALL a b. bax a > c & bax b > c <-> foo (bax a) = bar (bax b)"
lemma "foo = bar"
using ax1 ax2
apply auto
How come "x" and "y" can't be instantiated to "bax a" and "bax b", resp.? If
ax2 was:
ax2: "ALL a b. a > c & b > c <-> foo (a) = bar (b)"
then that works fine.
Any help will be much appreciated!
Regards
Email Gateway (Aug 18 2022 at 16:51):From: Brian Huffman <brianh@cs.pdx.edu>
Once again, we see that axioms are evil. Your ax1 is already
inconsistent all by itself:
lemma "False"
proof -
let ?f = "%x::real. if x > c then (0::real) else 1"
let ?g = "%x::real. if x > c then (0::real) else 2"
have "?f = ?g"
by (rule ax1 [rule_format], simp)
hence "?f c = ?g c"
by (rule arg_cong)
thus "False"
by simp
qed
Email Gateway (Aug 18 2022 at 16:51):From: egglue@gmail.com
I agree with your proof. But then, if it is to define how to approximate
a function f and a function g to be the same by comparing those x's and y's
c, then should the = operator be replaced here? It seems the problem here
is caused by overloading = with a form of approximated =, right? If so, how
should one go about introducing a new operator, say for approximation?
Thank
Eg
Last updated: Nov 21 2024 at 12:39 UTC