#|
Fully Ordered Finite Sets, Version 0.91
Copyright (C) 2003-2006 by Jared Davis
This program is free software; you can redistribute it and/or
modify it under the terms of the GNU General Public License
as published by the Free Software Foundation; either version 2
of the License, or (at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public Lic-
ense along with this program; if not, write to the Free Soft-
ware Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
02111-1307, USA.
set-order.lisp
This is a top level file which you should use if you intend to
reason about the set order. Normally you should not do this,
but you might need it if you want to argue "from first principles"
that list operations create sets, i.e. for efficiency reasons.
Note that merely including this file will do nothing for you.
You need to also enable the relavent theories:
primitive-reasoning
basic definitions of the primitive functions. useful if you
have a very low level proof about the stucture of sets or
something. doesn't pertain to the order itself.
order-reasoning
properties of the order itself, and its relation to the set
primitives. most of the membership level is based on this.
cons-reasoning
properties relating cons to sets through the set order.
this might be useful if you are introducing new "fast"
functions, based on cons rather than insert to construct
sets. it is not easy to reason with.
|#
(in-package "SETS")
(set-verify-guards-eagerness 2)
(local (include-book "primitives"))
(local (include-book "membership"))
(local (include-book "fast"))
(include-book "sets")
; -------------------------------------------------------------------
; primitive-reasoning
(deftheory primitive-reasoning
'(setp
empty
head
tail
sfix
insert))
; -------------------------------------------------------------------
; order-reasoning
(defthmd <<-type
(or (equal (<< a b) t)
(equal (<< a b) nil))
:rule-classes :type-prescription)
(defthmd <<-irreflexive
(not (<< a a)))
(defthmd <<-transitive
(implies (and (<< a b) (<< b c))
(<< a c)))
(defthmd <<-asymmetric
(implies (<< a b)
(not (<< b a))))
(defthmd <<-trichotomy
(implies (and (not (<< b a))
(not (equal a b)))
(<< a b)))
(defthmd head-insert
(equal (head (insert a X))
(cond ((empty X) a)
((<< a (head X)) a)
(t (head X)))))
(defthmd tail-insert
(equal (tail (insert a X))
(cond ((empty X) (sfix X))
((<< a (head X)) (sfix X))
((equal a (head X)) (tail X))
(t (insert a (tail X))))))
(defthmd head-tail-order
(implies (not (empty (tail X)))
(<< (head X) (head (tail X)))))
(defthmd head-tail-order-contrapositive
(implies (not (<< (head X) (head (tail X))))
(empty (tail X))))
(deftheory order-reasoning
'(<<-type
<<-irreflexive
<<-transitive
<<-asymmetric
<<-trichotomy
(:induction insert)
head-insert
tail-insert
head-tail-order
head-tail-order-contrapositive))
; -------------------------------------------------------------------
; cons-reasoning
(defthmd cons-set
(equal (setp (cons a X))
(and (setp X)
(or (<< a (head X))
(empty X)))))
(defthmd cons-head
(implies (setp (cons a X))
(equal (head (cons a X)) a)))
(defthmd cons-to-insert-empty
(implies (and (setp X)
(empty X))
(equal (cons a X) (insert a X))))
(defthmd cons-to-insert-nonempty
(implies (and (setp X)
(<< a (head X)))
(equal (cons a X) (insert a X))))
(defthmd cons-in
(implies (and (setp (cons a X))
(setp X))
(equal (in b (cons a X))
(or (equal a b)
(in b X)))))
(deftheory cons-reasoning
'(cons-set
cons-head
cons-to-insert-empty
cons-to-insert-nonempty
cons-in))