Re: [PVS-Help] nested recusive data types

[Natarajan Shankar <shankar@xxxxxxxxxxx>]

Sjaak:

You need to use a domain restriction as shown on the recursive
occurrence of map to get the termination proof obligation.

map(f:[V -> W]) (t:TERMS[V,S]) : RECURSIVE TERMS[W,S] =
      CASES t
        OF tvar(tvar1_var): tvar(f(tvar1_var)),
           tapp(tapp1_var, tapp2_var):
             tapp(tapp1_var,
                  map((LAMBDA (x: TERMS[V,S] | x << t): map(f)(x)), tapp2_var))
        ENDCASES
  MEASURE t BY <<

The attached dump file completes the proof.  You can use M-x
undump-pvs-files from PVS to extract its contents. 

-Shankar

%% PVS Version 4.2 - Allegro CL Enterprise Edition 8.1 [Linux (x86)] (Jul 20, 2008 2:00)
%% 8.1 [Linux (x86)] (Jul 20, 2008 2:00)
$$$PVSHOME/pvs-strategies
(in-package 'pvs)


$$$terms.pvs
TERMS [V,S:TYPE]: DATATYPE
BEGIN
    tvar(id:V): tvar?
    tapp (symb:S,args:list[TERMS]): tapp?
END TERMS


list_facts[T: TYPE]: THEORY
BEGIN

P, Q: VAR [T->bool]

ll: VAR list[T]

every_implies: LEMMA
  (FORALL (x: T): P(x) IMPLIES (Q(x))) AND
   every(P)(ll)
 IMPLIES every(Q)(ll)

END list_facts

myterms  [V,S, W:TYPE]
		: THEORY

  BEGIN

  IMPORTING TERMS[V, S], list_facts[TERMS[V,S]]


map(f:[V -> W]) (t:TERMS[V,S]) : RECURSIVE TERMS[W,S] =
      CASES t
        OF tvar(tvar1_var): tvar(f(tvar1_var)),
           tapp(tapp1_var, tapp2_var):
             tapp(tapp1_var,
                  map((LAMBDA (x: TERMS[V,S] | x << t): map(f)(x)), tapp2_var))
        ENDCASES
  MEASURE t BY <<
  

  END myterms

$$$terms.prf
(TERMS)
(list_facts
 (every_implies 0
  (every_implies-1 nil 3428177600 3428177606
   ("" (induct-and-simplify "ll") nil nil) proved
   ((list type-decl nil list_adt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (PRED type-eq-decl nil defined_types nil)
    (every adt-def-decl "boolean" list_adt nil)
    (T formal-type-decl nil list_facts nil)
    (list_induction formula-decl nil list_adt nil))
   6439 120 t shostak)))
(myterms
 (map_TCC1 0
  (map_TCC1-1 nil 3428173765 3428173765 ("" (termination-tcc) nil nil)
   unchecked nil 26 20 nil nil))
 (map_TCC2 0
  (map_TCC2-1 nil 3428173765 3428181351
   ("" (expand "<<")
    (("" (assert)
      (("" (skosimp*)
        (("" (replace -1 :hide? t)
          (("" (assert)
            (("" (generalize "tapp2_var!1" "ll")
              (("" (induct-and-simplify "ll")
                (("" (lemma "every_implies")
                  (("" (inst? :polarity? t)
                    (("" (ground)
                      (("" (inst? :polarity? t)
                        (("" (ground) (("" (skosimp*) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   proved
   ((V formal-type-decl nil myterms nil)
    (S formal-type-decl nil myterms nil)
    (TERMS type-decl nil TERMS_adt nil)
    (list type-decl nil list_adt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (PRED type-eq-decl nil defined_types nil)
    (every adt-def-decl "boolean" list_adt nil)
    (some adt-def-decl "boolean" list_adt nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (pred type-eq-decl nil defined_types nil)
    (every_implies formula-decl nil list_facts nil)
    (list_induction formula-decl nil list_adt nil)
    (<< adt-def-decl "(well_founded?[TERMS])" TERMS_adt nil))
   2993225 350 t nil)))