[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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
   ((intval adt-constructor-decl "[int -> (intval?)]" intval_adt nil)
    (intval_intval_extensionality formula-decl nil intval_adt nil)
    (intval type-decl nil intval_adt nil)
    (intval? adt-recognizer-decl "[intval -> boolean]" intval_adt nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (v adt-accessor-decl "[intval -> int]" intval_adt 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)
    (intval adt-constructor-decl "[int -> (intval?)]" intval_adt nil)
    (intval_intval_extensionality formula-decl nil intval_adt nil)
    (intval type-decl nil intval_adt nil)
    (intval? adt-recognizer-decl "[intval -> boolean]" intval_adt nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (v adt-accessor-decl "[intval -> int]" intval_adt 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)))