# Re: [isabelle] Using implications

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

On Jan 26, 2011 6:23pm, Brian Huffman <brianh at cs.pdx.edu> wrote:
```
```On Wed, Jan 26, 2011 at 10:14 AM, Eg Gloor egglue at gmail.com> wrote:
```
```
```
```> 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 > cfx = gy) --> f = g"
```
```
```
```> and ax2: "ALL a b. bax a > c & bax b > c foo (bax a) = bar (bax b)"
```
```

```
```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 "?fc = ?g c"
```
```
```
```by (rule arg_cong)
```
```
```
```thus "False"
```
```
```
```by simp
```
```
```
```qed
```
```

```
```-> Brian
```
```

```

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