(all x : type (all y : x ((assoc y []) = [])))
(all x : type (all y : (list x) (all z : x (all x1 : (list (list x)) ((assoc z [[z | y] | x1]) = [z | y])))))
(all x : type (all y : (list (list x)) (all z : x (all x1 : (list x) ((all y1 : (list (list x)) (all z1 : (list x) ((~ (x1 = [z | z1])) v (~ (y = y1))))) => ((assoc z [x1 | y]) = (assoc z y)))))))
(all x : type (all y : (list x) ((difference [] y) = [])))
(all x : type (all y : (list x) (all z : (list x) (all x1 : x ((difference [x1 | z] y) = (if (element? x1 y) (difference z y) [x1 | (difference z y)]))))))
(all x : type (all y : type (all z : y (all x1 : x ((do x1 z) = z)))))
(all x : type (all y : x ((element? y []) = false)))
(all x : type (all y : (list x) (all z : x ((element? z [z | y]) = true))))
(all x : type (all y : (list x) (all z : x (all x1 : x ((~ (z = x1)) => ((element? z [x1 | y]) = (element? z y)))))))
(all x : type (all y : (list x) (all z : x (((~ (y = [])) & ((all x1 : (list x) (~ (y = [z | x1]))) & (all y1 : (list x) (all z1 : x (~ (y = [z1 | y1])))))) => ((element? z y) = (simple-error "attempt to find an element in a non-list"))))))
(all x : type (all y : type (all z : y (all x1 : (x --> x) (all y1 : x ((fix x1 y1) = (let z (x1 y1) (if (= y1 z) y1 (fix x1 z)))))))))
(all x : type (all y : x (all z : (list x) ((head [y | z]) = y))))
(all x : type (all y : (list x) ((all z : (list x) (all x1 : x (~ (y = [x1 | z])))) => ((head y) = (simple-error "head expects a non-empty list")))))
(all x : type (all y : (list x) (all z : x ((tail [z | y]) = y))))
(all x : type (all y : (list x) ((all z : (list x) (all x1 : x (~ (y = [x1 | z])))) => ((tail y) = (simple-error "tail expects a non-empty list")))))
((reverse []) = [])
(all x : type (all y : x (all z : (list x) ((reverse [y | z]) = (append (reverse z) [y])))))
(all x : type (all y : type (all z : y (all x1 : x ((fst (@p z x1)) = z)))))
(all x : type (all y : type (all z : y (all x1 : x ((snd (@p x1 z)) = z)))))
(all x : type (all y : (list x) ((union [] y) = y)))
(all x : type (all y : (list x) (all z : (list x) (all x1 : x ((union [x1 | z] y) = (if (element? x1 y) (union z y) [x1 | (union z y)]))))))
(all x : type (all y : type (all z : (y --> x) ((map z []) = []))))
(all x : type (all y : type (all z : (list x) (all x1 : (x --> y) (all y1 : x ((map x1 [y1 | z]) = [(x1 y1) | (map x1 z)]))))))
((length []) = 0)
(all x : type (all y : (list x) (all z : x ((length [z | y]) = (+ 1 (length y))))))
(all x : type (all y : x (all z : (list x) ((nth 1 [y | z]) = y))))
(all x : type (all y : (list x) (all z : number (all x1 : x ((~ (z = 1)) => ((nth z [x1 | y]) = (nth (- z 1) y)))))))
(all x : type (all y : (list x) (all z : number ((((~ (z = 1)) v (all x1 : (list x) (all y1 : x (~ (y = [y1 | x1]))))) & (all z1 : (list x) (all x2 : x (~ (y = [x2 | z1]))))) => ((nth z y) = (simple-error "attempt to find the nth element of a non-list"))))))
(all x : type (all y : (list x) ((append [] y) = y)))
(all x : type (all y : (list x) (all z : (list x) (all x1 : x ((append [x1 | z] y) = [x1 | (append z y)])))))
(all x : type (all y : (list x) (all z : x ((adjoin z y) = (if (element? z y) y [z | y])))))
(all x : type (all y : type (all z : (y --> (list x)) ((mapcan z []) = []))))
(all x : type (all y : type (all z : (list x) (all x1 : (x --> (list y)) (all y1 : x ((mapcan x1 [y1 | z]) = (append (x1 y1) (mapcan x1 z))))))))
(all x : number ((+ 0 x) = 0))
(all x : natnum (all y : natnum ((~ (y = 0)) => ((+ y x) = (s (+ (p y) x))))))
(all x : number ((* 0 x) = 0))
(all x : natnum (all y : natnum ((~ (y = 0)) => ((* y x) = (+ x (* (p y) x))))))
If you want to repeat my proof of the associativity of append.
(pvs (introduce (@p []
[all A : type [all x : [list A]
[all y : [list A]
[all z : [list A]
[[append x [append
y z]]
= [append
[append x y] z]]]]]])))
starts the ball rolling. For those courageous enough, the sequence of tactics needed to solve the problem is:
(omega append) \\ draw in the axioms wrt 'append' in KW
(allr a) \\ instantiate the conclusion by a
lind \\ list induction
(thin 3)
(allr y)
(allr z)
(alll &&a) \\ instantiate the lading assumption by &&a
hyp
(alll &&y)
hyp
(l->r 1 0) \\ use the idenityt in 1 to rewrite the 0th wff i.e. the conclusion
(thin 1)
(alll [append &&y &&z])
tr \\ invoke the type checker to solve the problem
(l->r 1 0)
=r
(thin 2)
(allr y1)
(allr x)
=>r
(allr y)
(allr z)
(swap 1 7) \\ exchange the positions of wff 1 and 7
(alll &&a)
hyp
(thin 2)
(alll [append &&y &&z])
tr
(alll &&x)
hyp
(alll &&y1)
hyp
(l->r 1 0)
(thin 1)
(thin 1)
(thin 1)
(alll &&y)
hyp
(alll &&x)
hyp
(alll &&y1)
hyp
(l->r 1 0)
(thin 1)
(thin 1)
(thin 1)
(alll &&z)
hyp
(alll [append &&x &&y])
tr
(alll &&y1)
hyp
(l->r 1 0)
(thin 1)
(thin 1)
(thin 1)
(thin 1)
(alll &&y)
hyp
(alll &&z)
hyp
(l->r 1 0)
=r \\ prove x = x for all x
That's about as far as I'm going to take this for the while. Back to the Ring this week.
Mark
