# Re: inst? and overloaded operators

```Hendrik Tews wrote:
>     ;;; Proof inj-1 for formula intval_test.inj
>     ;;; developed with shostak decision procedures
>     ("" (grind) (decompose-equality -3))
>
> so it looks like data type constructors are injective :-;

So it seems. I guess I trusted the omnipotence of grind too much,
thanks for pointing out decompose-equality!

> (You
> could have also checked the intval_adt.pvs file and applied the
> axioms in there manually).

I did, but I only found extensionality which goes the opposite
direction. Am I overlooking something?

>    My longer question concerns instantiation.
>
> Can you send the prove script that leads to this subgoal?

Sure, it is attached. The point is now kind of moot, because
the subgoal can be proved using decompose-equality without
touching the tcc at all, but I would still be interested in
what is going on.
--
pertti
```
```
%% PVS Version 3.1
%% 6.2 [Linux (x86)] (Feb 14, 2003 18:46)
\$\$\$intval_tcc.pvs
intval : DATATYPE
BEGIN
intval(v : int) : intval?
END intval

intval_test : THEORY
BEGIN
IMPORTING intval

intval_peeling : lemma
forall (f : [[int,int] -> int]) :
forall (i1, i2, i3, i4 : int) :
intval(i1) = intval(i2) and intval(i3) = intval(i4)
=> intval(f(i1,i3)) = intval(f(i2,i4))

intval_plus_peeling : lemma
forall (i1, i2, i3, i4 : int) :
intval(i1) = intval(i2) and intval(i3) = intval(i4)
=> intval(i1+i3) = intval(i2+i4)
END intval_test

\$\$\$intval_tcc.prf
(intval)
(intval_test
(intval_peeling 0
(intval_peeling-1 nil 3259569517 3260074235
("" (grind)
(("" (decompose-equality 1)
(("" (decompose-equality -5)
(("" (decompose-equality -6) (("" (ground) nil nil)) nil))
nil))
nil))
nil)
proved
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil))
30557 2790 t shostak))
(intval_plus_peeling 0
(intval_plus_peeling-2 "" 3260074439 3260074439
("" (skosimp*)
(("" (lemma "intval_peeling")
(("" (inst?)
(("1" (inst?) (("1" (ground) nil nil)) nil)
("2" (decompose-equality 2)
(("2" (decompose-equality -1)
(("2" (decompose-equality -2) (("2" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
proved nil 109919 4990 t shostak)
(intval_plus_peeling-1 nil 3259569888 3260074323
("" (skosimp*)
(("" (lemma "intval_peeling")
(("" (inst -1 "+" "i1!1" "i2!1" "i3!1" "i4!1")
(("" (grind) nil nil)) nil))
nil))
nil)
proved
((intval_peeling formula-decl nil intval_test nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(int nonempty-type-eq-decl nil integers nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields
nil))
27966 2260 t shostak)))

```