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

Re: "<<" TCC ?



Hi,

   After typecheckeing I've got TCC which is unprovable. Could you hint  
   me: what do I wrong ? 
   
which TCC is unprovable? I adjusted your example such that it
typechecks and proved all TCC's (see appended dump).

Bye,

Hendrik


%% PVS Version 3.1
%% 6.2 [Linux (x86)] (Feb 14, 2003 18:46)
$$$t.pvs
gen_tree[T: TYPE]: DATATYPE
BEGIN

  leaf(fringe: list[T]): isLeaf?
  node(val: T, desc: list[gen_tree]): isNode?

END gen_tree


T : Theory
Begin
  IMPORTING gen_tree

  sum(ls: list[nat]): RECURSIVE nat =
  CASES ls OF
	  null: 0,
	  cons(x, ls1): x + sum(ls1)
  ENDCASES
  MEASURE ls BY <<

  %size function
  size(tr : gen_tree[nat]): RECURSIVE nat = 
  CASEs tr OF  
	  leaf(tr): length(tr),
	  node(val,desc): 1 + sum(map(size ,desc))
  ENDCASES
  MEASURE tr BY <<
end T

$$$t.prf
(gen_tree)
(T
 (sum_TCC1 0
  (sum_TCC1-1 nil 3262925471 3262925471 ("" (termination-tcc) nil nil)
   proved ((<< adt-def-decl "(well_founded?[list])" list_adt nil)) 359
   180 nil shostak))
 (size_TCC1 0
  (size_TCC1-1 nil 3262925471 3262928168
   ("" (skosimp*)
    ((""
      (case "Forall(l1,l2 : list[gen_tree[nat]]) : tr!1 = node(val!1, append(l1,l2)) IMPLIES every[gen_tree[nat]] (LAMBDA (z: gen_tree[nat]): <<[nat](z, tr!1))(l2)")
      (("1" (inst -1 "null" "desc!1")
        (("1" (expand "append") (("1" (assert) nil nil)) nil)) nil)
       ("2" (hide-all-but 1)
        (("2" (induct "l2")
          (("1" (grind) nil nil)
           ("2" (skosimp*)
            (("2" (expand "every" 1)
              (("2" (prop)
                (("1" (replace -2 * lr)
                  (("1" (hide -1 -2)
                    (("1" (expand "<<")
                      (("1" (generalize "cons1_var!1" "t")
                        (("1" (generalize "cons2_var!1" "l2")
                          (("1" (generalize "l1!1" "l1")
                            (("1" (induct "l1")
                              (("1" (grind) nil nil)
                               ("2"
                                (skosimp*)
                                (("2"
                                  (expand "append" 1)
                                  (("2"
                                    (expand "some" 1)
                                    (("2" (rewrite -1) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (inst -1 "append(l1!1, cons(cons1_var!1, null))")
                  (("2" (prop)
                    (("2" (hide 2)
                      (("2" (apply-extensionality :hide? t)
                        (("1" (decompose-equality) nil nil)
                         ("2" (replace -1 * lr)
                          (("2" (assert)
                            (("2" (hide -1)
                              (("2"
                                (generalize "cons1_var!1" "t")
                                (("2"
                                  (generalize "cons2_var!1" "l2")
                                  (("2"
                                    (generalize "l1!1" "l1")
                                    (("2"
                                      (induct "l1")
                                      (("1"
                                        (expand "append")
                                        (("1"
                                          (expand "append")
                                          (("1" (propax) nil nil))
                                          nil))
                                        nil)
                                       ("2"
                                        (skosimp*)
                                        (("2"
                                          (expand "append" 1)
                                          (("2" (rewrite -1) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   proved
   ((<< adt-def-decl "(well_founded?[gen_tree])" gen_tree_adt nil)
    (well_founded? const-decl "bool" orders nil)
    (pred type-eq-decl nil defined_types nil)
    (append def-decl "list[T]" list_props nil)
    (node adt-constructor-decl "[[T, list[gen_tree]] -> (isNode?)]"
     gen_tree_adt nil)
    (isNode? adt-recognizer-decl "[gen_tree -> boolean]" gen_tree_adt
     nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (every adt-def-decl "boolean" gen_tree_adt nil)
    (every adt-def-decl "boolean" list_adt nil)
    (PRED type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (list type-decl nil list_adt nil)
    (gen_tree type-decl nil gen_tree_adt nil)
    (number nonempty-type-decl nil numbers nil)
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (null adt-constructor-decl "(null?)" list_adt nil)
    (list_induction formula-decl nil list_adt nil)
    (desc adt-accessor-decl "[(isNode?) -> list[gen_tree]]"
     gen_tree_adt nil)
    (val adt-accessor-decl "[(isNode?) -> T]" gen_tree_adt nil)
    (tr!1 skolem-const-decl "gen_tree[nat]" T nil)
    (gen_tree_node_extensionality formula-decl nil gen_tree_adt nil)
    (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil)
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (some adt-def-decl "boolean" list_adt nil))
   2648857 77530 t shostak)))