\documentstyle[11pt,a4wide,noweb,fleqn]{report}
\advance \oddsidemargin -0.4in
\advance \evensidemargin -0.4in
\begin{document}
\filename{predicate.nw}
\begindocs{0}
\title{Lifted Predicate Calculus in HOL}
\author{ISWB Prasetya \\
        \small Rijkuniversiteit Utrecht, Vakgroep Informatica \\
        \small Postbus 80.089, 3508 TB Utrecht, Nederland \\
        \small Email: wishnu@cs.ruu.nl }

\input{UNITYsty}
\maketitle

\enddocs
\begindocs{1}

\tableofcontents

\chapter{Introduction}

HOL, Higher Order Logic, is one of the many theorem provers available
nowadays.  HOL, like any other theorem prover, can be considered as
another sort of pen and paper on which we can do our proofs. One
difference is that HOL imposes consistency, so we cannot generate a
false theorem.  On the negative side, HOL requires us to be very
precise in expressing our thought, which often mean a lot of typing of
what human intellect may consider as trivial information.

Nonetheless, HOL is still a promising tool to support verification. At
least in the field of hardware verification the results have been
positive. The application of HOL in program verification is however
still in the shade, mainly because not too many people has been
working on the field.

Our research aims to extend HOL with sufficient libraries to support
program verification. As predicate is the primitive concept by which
one describe program's state and behavior we start by extending HOL
with the definition of various predicates operators and their
properties. 

Predicate calculus is supported by standard HOL. The negation, the
standard logical connectives, and the quantors $\qA$ and $\qE$ are all
defined and some of their basic properties are part of HOL built-in
features. There is even a tautology checker to automatically prove the
validity of a proposition calculus formula.

In programming people extensively make use of predicate calculus, or
at least people pretend they use predicate calculus. The primitive
concept in programming is predicate, which is a function from some
domain to $\Bool$. Predicate is used, for example, to describe a set
of states, for example those states where the value of variable $z$ is
0.

If $P$ and $Q$ are predicates, the expression $P\AND Q$ cannot be a
formula in predicate calculus. The expression does not even make sense
since $\AND$ is a logical operator, so it expects Boolean arguments,
not predicates. Yet in programming, we pretend that the expression
does make sense and that it can be treated as a predicate calculus
formula.

What people has silently done is that they overload the symbol $\AND$
to denote the point-wise lift of the logical $\AND$. Indeed, the
lifted $\AND$ inherits all algebraic properties of the logical $\AND$.
But this does not mean that they are semantically the same thing.

What is actually applied in programming is the predicate calculus
lifted to the predicate level. It is a calculus of predicates rather
than predicate calculus. Because the inference rules of predicate
calculus also applies to the lifted predicate calculus, people then
pretend that they work with predicate calculus instead.

When it comes to formalization however, we have to be very precise. So
an explicit distinction between logical operators and lifted logical
operators has to be made.

In the library called \code{}predicate\edoc{} we provide the lifted operators of
predicate calculus and their basic properties, including finite
predicates induction. The library basically provides the user with the
lifted predicate calculus, which is not yet supported by the standard
HOL.

This report is a documentation of the \code{}predicate\edoc{} library. Actually,
it is an extensively annotated and nicely printed listing. This is to
follow the concept of literate programming that advocates that
programs should be presented in such a way that people can regard it
as a piece of reading rather than a stack of paper with lines of dull,
ASCI fonted codes. In fact, we use \code{}noweb\edoc{}, a smaller version of
\code{}WEB\edoc{}, a tool for literate programming by Donald E Knuth, to
generate both this document and the library itself. In \code{}noweb\edoc{} one
has a single source for both document and code. The tool
automatically takes care the extraction of each component. As
advantage, maintaining the consistency between documentation and code
becomes easier.

This document contains thus code, mainly the HOL proofs of various
properties. Of course they provide fine examples for the reader as how
to prove various properties of lifted predicate calculus operators.
More than this, the user probably does not need the code and can
simply skip them, unless of course if he wants, for whatever reason,
to modify the library.

\section{Notation}

HOL codes are printed in type-writer font like \code{}definition\edoc{}, while
slanted text between angled brackets like \CodeRef{Proof of Fizban
Law} is an abbreviation for a piece of code. Sort of macro thus.

Theorems generated by HOL are pretty printed in math font. Theorems
are put in a box and numbered and labeled like this:

\begin{theorem}{Flip-Flup-Fley Law}
\label{intro.Flip}
\[ \thf{FLIP\_THM}:\ \ \ \qA x\Dot f.x > 0 \] 
\end{theorem}

The label \thf{FLIP\_THM} at the left of the formula is the name
underwhich the theorem is saved in the theory file\footnote{A theory
is a HOL object containing a list of definitions and theorems. These
are stored in the theory file so that they can be referred again in
the future.}. The numbering is just a typographical device and the
string following it serves only to hint what the theorem asserts. In
the HOL code we refer the thorem as \thf{FLIP\_THM}. In the
documentation, we prefer to refer it as Flip-Flup-Fley Law, or simply
by Theorem \ref{intro.Flip}.

Definitions are also pretty printed and put in box. These are the
intended definitions and should be checked if they match the
definitions generated by HOL. Each intended definition is followed
directly by the corresponding HOL code, so comparing them is not
difficult. In any case, the list of definitions of a given theory can
be requested using ML-function \code{}definitions\edoc{}.

HOL denotes application of function $f$ to argument $x$ as $f\; x$. In
pretty printed formulas, this will be denoted with dot: $f.x$. The dot
binds stronger than any other operator.

HOL notation for quantification is rather non-standard. Yet, to ease
comparing pretty printed formulas with HOL code and output we will
addopt it anyway.

\begin{description} 
\item[Unrestricted Quantification]
Let $\cal T$ be a non-empty domain.  We write $(\qA i:{\cal T}\Dot
f.i)$ to denote the universal quantification over the whole domain
$\cal T$. However, since troughout this report it is always obvious
from the context what $\cal T$ is, we will drop it and write
$(\qA i\Dot f.i)$ instead.

\item[Restricted Quantification]
Let $\cal T$ be a non-empty domain and let $W:{\cal T}\fun\Bool$ be a
function that characterizes a subset of $\cal T$. We write $(\qA
i::W\Dot f.i)$ instead the usual $(\qA i:W.i: f.i)$ to denote the
universal quantification over $\cal T$ restricted by $W$.
\end{description}

The same convention applies to other quantified operators.

\section{Document Structure}

Chapter \ref{install} prescribes how to install and load the library
and Chapter \ref{global} describes the structure of the library source
code. 

Chapter \ref{def} contains the definition of the lifted predicate
calculus operators.  As mentioned earlier, the pretty printed
definitions are the intended definitions.  The HOL codes defining each
operator should be checked by hand if they indeed match the
corresponding intended definition.

Chapter \ref{proof} contains various basic properties of the lifted
operators and their HOL proofs. Many of the properties in the library
are basically simple and can be proved in much the same way. To
automate their proofs we also provide few tactics.

Chapter \ref{induction} contains the definition of finite predicates
and an induction law for finite predicates.

Appendix \ref{loader} decribes the loader. The loader is responsible
to configure the library when it is called by the user.

Appendix \ref{HOL def} is a quick reference to all definitions and
theorems provided by the library. The user can always get them by
typing \code{}print_theory\edoc{} \code{}`predicate`\edoc{} in HOL.

Appendix \ref{misc} describes some non-standard but useful tactics
either used in this library, or we have used in further application of
this library.





\chapter{How to Install and How to Load}
\label{install}
The whole package consists of several files:

\begin{quote}
\begin{tabular}{|l|l|} \hline
   noweb source & \code{}predicate.nw\edoc{} \\ \hline
   Makefile      & \code{}Makefile\edoc{} \\ \hline
   The Loader &  \code{}predicate.ml\edoc{} \\ \hline
   Code for the Library Itself &  \code{}mk_predicate.ml\edoc{} \\ \hline
   Support Files & \code{}my_misc.ml\edoc{} and 
                           \code{}predicate_SUP.ml\edoc{} \\ \hline
   Old Resolutions Tactics & \code{}OLD_RES.ml\edoc{} \\ \hline
   Documentation &  \code{}predicate.tex\edoc{} \\ \hline
   Style Files    &  \code{}UNITYsty.tex\edoc{}, \code{}noweb.sty\edoc{} \\ \hline
\end{tabular}
\end{quote}

Many of the files are in a sense redundant as they can be extracted
from the \code{}noweb\edoc{} source file \code{}predicate.nw\edoc{}. \code{}noweb\edoc{} is a
literate programming tool. The idea of literate programming is to have
the code presented like a textbook. Like this report. In \code{}noweb\edoc{} we
have one common source for document and code. This has additional
advantage that it is easier to maintain consistency between code and
document.

To use the library or to print this documentation \code{}noweb\edoc{} is not a
necessary ingredient. However, if you want to modify the library, then
you need \code{}noweb\edoc{}, or at least we strongly advise to use it because
the code extracted by \code{}notangle\edoc{} is deprived of any annotation
whatsoever. That is, the \code{}noweb\edoc{} source is much more readable than
the code extracted from it.

In case you don't have \code{}noweb\edoc{} yet, we have included it in the
distribution package of this library.

If you modify the \code{}noweb\edoc{} source, you can run the \code{}Makefile\edoc{} to
automatically update various library components:

\begin{quote}
\begin{tabular}{lcl}
    \code{}make Pred\edoc{} & : & updates \code{}mk_predicate.ml\edoc{} \\
    \code{}make LPred\edoc{} & : & updates \code{}predicate.ml\edoc{} \\
    \code{}make SPred\edoc{} & : & updates \code{}predicate_SUP.ml\edoc{} \\
    \code{}make SPredMisc\edoc{} & : & updates \code{}my_misc.ml\edoc{} \\
    \code{}make TexPred\edoc{} & : & updates \code{}predicate.tex\edoc{}
\end{tabular}
\end{quote}

The \LaTeX file \code{}predicate.tex\edoc{} can be compiled with \LaTeX to
generate this document. 

To install the library you need to run \code{}make TPred\edoc{}. This will
automatically build the theory file \code{}predicate.th\edoc{} by calling HOL to
execute \code{}mk_predicate.ml\edoc{}. The theory files is the one that contains
all definitions and theorems listed in this documentation.

The loader \code{}predicate.ml\edoc{} is the one the user call when he wants to use
the library. The loader is responsible of configuring some ML
variables necessary before one can use the library. Appendix
\ref{loader} contains a detailed description of the loader.

The support file \code{}my_misc.ml\edoc{} contains some non-standard rules and
tactics which are either used in the library or we have used in
further application of the library. 

The other support file, \code{}predicate_SUP.ml\edoc{}, contains the two tactics
\code{}pred_JADE_TAC\edoc{} and \code{}pred_CYAN_TAC\edoc{} which are useful to solve
simple statements in the lifted predicates calculus. The code and a
detailed description of the two tactics can be found in Section
\ref{JADE_CYAN}.

\section{How to Install}

To install the package do:
\begin{enumerate}
\item
Go to the default HOL library directory.

\item
Create there a new subdirectory called \code{}predicate\edoc{} then copy the
whole package to that new directory.

\item
Do \code{}make TPred\edoc{}. This will create the theorem file
\code{}predicate.th\edoc{} and finish the installation. 
\end{enumerate}

You can also choose to install the library in your personal directory.
Fortunately, only the loader is directory-dependant. The easiest way
for you to do is to change the definition of \code{}my_path\edoc{} below to the
directory you wish the library to be stored. The modification has to
be applied to the \code{}noweb\edoc{} source, that is, the file
\code{}predicate.nw\edoc{}.

\enddocs
\begincode{2}
\moddef{my path}\endmoddef
my_path = `/infix/5s0/wishnu/testhol/UNITY/`  
\endcode
\begindocs{3}


Then you will have to update the loader using \code{}noweb\edoc{}. Your source
chunk is \CodeRef{myloader} instead of \CodeRef{loader}. The
following command will do the update for you.
\begin{quote}
   \code{}rm predicate.ml ; noweb -Rmyloader predicate.nw > predicate.ml \edoc{}
\end{quote}

\enddocs
\begindocs{4}

\section{How to Load}

To load the library simply do
\begin{quotation}
   \code{}load_library `predicate` ;;\edoc{}
\end{quotation}
However if you have installed the library inside your personal directory
you will have to do 
\begin{quotation}
   \code{}loadf (my_path ^ `predicate`)\edoc{}
\end{quotation}
where \code{}my_path\edoc{} is the path of your \code{}predicate\edoc{} library.



\enddocs
\begindocs{5}

\chapter{The Global Structure of the Library}
\label{global}

The definitions and theorems of lifted predicates calculus are stored
in the theory file \code{}predicate.th\edoc{} which is produced by executing the
code in file \code{}mk_predicate.ml\edoc{}. This is done automatically by the
\code{}Makefile\edoc{}.  The source file \code{}mk_predicate.ml\edoc{} is organized as
follows:

\enddocs
\begincode{6}
\moddef{predicate}\endmoddef
\LA{}header\RA{}
\LA{}definition part\RA{}
\LA{}proving theorems\RA{}
\LA{}predicate and sets\RA{}
\LA{}trailer\RA{}
\endcode
\begindocs{7}


The header is simple. It opens a new theory called \code{}predicate\edoc{} and
load some file whose purpose is given in the table below:

\begin{quote}
    \begin{tabular}{|l|l|} \hline
     \code{}taut\edoc{} & tautology checker for proposition formulas \\ \hline
     \code{}sets\edoc{} & libraries about finite sets \\ \hline
     \code{}my_misc\edoc{} & some non-standard rules and tactics \\ \hline
     \code{}OLD_RES\edoc{} & old resolution tactics \\ \hline
    \end{tabular}
\end{quote}

The rules and tactics in \code{}my_misc.ml\edoc{} are described in Appendix
\ref{misc}.  


The \CodeRef{definition part} part defines the lifted predicate
calculus operators. The \CodeRef{proving theorems} part proves the
properties of the lifted operators. The \CodeRef{predicate and sets} part
proves the induction for finite predicates.

The trailer is simple. It merely closes the theory \code{}predicate\edoc{} and
thus saving all definitions and theorems in the theory file
\code{}predicate.th\edoc{}.

\enddocs
\begincode{8}
\moddef{header}\endmoddef
new_theory `predicate`;;
load_library `taut` ;;
load_library `sets` ;;
loadf `my_misc`;;
loadf `OLD_RES` ;;

\endcode
\begincode{9}
\moddef{trailer}\endmoddef
close_theory();;
\endcode
\begindocs{10}






\enddocs
\begindocs{11}

\chapter{The Definition Part}
\label{def}

Lifted predicate calculus is just the calculus that results by lifting
all predicate calculus operator to the predicate level. Although the
name may inspire something new, it is what we actually use in
programming. People pretend to work with predicate calculus because
the rules of predicate calculus also applies to the lifted calculus.

Formal proofs require us to be very precise however. So this means we
have to formally define the lifted calculus. That the rules in the
original calculus are also lifted to the new calculus is fine, but
this is something which also has to be formally proven. 

This chapter presents the definition of the lifted predicate
operators. It is nothing complicated, really. 

\section{Proposition and Predicate}

The fact that predicate calculus is the proposition calculus extended
with $\qA$ and $\qE$ is quite misleading that people often thinks that
therefore a predicate is just a proposition, possibly containing $\qA$
or $\qE$ in it. We must first clear this confusion and agree on what
predicates precisely are.

A {\em proposition} is an expression which interprets to either true
or false. So for example \begin{quote}
   {\em Jade is a bard}
\end{quote}
or
\[ x>0 \]
are both propositions. Furthermore we also have the logical operators
$\NOT, \AND, \OR$, and $\IMP$ with the usual interpretation. The
calculus of proposition with this operators is called {\em proposition
calculus}.

A {\em predicate} is a function from some domain to $\Bool$. A
predicate is thus not a proposition and a proposition not a predicate.

{\em Predicate calculus} is the proposition calculus extended with
$\qA$ and $\qE$ quantification. For example expression \[ \qA x\Dot
x>0 \] is a formula in the predicate calculus but it is not a formula
in the proposition calculus.  It is a proposition though, since it
evaluates to either true or false. And since it is a proposition it is
not a predicate.

{\em Proposition, proposition calculus formula, predicate, and
predicate calculus formula are four different things.}

Actually, if we follow the strict syntax of predicate calculus the
formula above should be written as \[ \qA x\Dot (\lambda\ y\Dot y>0).x
\] Notice the function $\lambda\ y\Dot y>0$ is a predicate since it is
a function from the domain of $x$ to $\Bool$. Here we indeed have an
explicit predicate in the formula (hence the name predicate calculus).

\section{Lifted Predicate Calculus}

Now we know for certain what predicates are, it should be clear that
expression $P \AND Q$ where $P$ and $Q$ are predicates does not make
sense. People have actually, and silently too, overloaded the symbol
$\AND$ to also denote the point-wise lift of the logical $\AND$. Even
with this overloading the expression would represent a predicate and
hence we are not entitled to work on it using the rules of predicate
calculus. It is true however that those rules can be lifted and will
apply on the lifted operators.

Below we define the point-wise lift of various predicate calculus
operators to the predicate level. Because in the current HOL version
we cannot have a true overloading we will have to assign different
symbols to the lifted operators.

As said, a predicate is a function from some domain, say $A$, to
$\Bool$. So it characterizes a subset of $A$. For example a state
predicate is a predicate over the set of all possible states of a
given program. It characterizes, for example, those states where the
Boolean variable $p$ has value $\false$.

The lifted predicate calculus is just the calculus that one gets by
lifting all operators in the predicate calculus to the predicate
level. 

There are ten operators, defined as follows. 

\enddocs
\begincode{12}
\moddef{definition part}\endmoddef
\LA{}unquantified operators\RA{}
\LA{}quantified operators\RA{}
\LA{}everywhere operator\RA{}
\endcode
\begindocs{13}


\begin{definition}{Unquantified Operators}
\[ \begin{array}{llcl}
     (1) & \TT & = & (\lambda s\Dot  \true) \\
     (2) & \FF & = & (\lambda s\Dot  \false) \\
     (3) & \pNOT P & = & (\lambda s\Dot  \NOT(P.s)) \\
     (4) & P \pAND Q & = & (\lambda s\Dot  P.s \AND Q.s) \\ 
     (5) & P \pOR Q & = & (\lambda s\Dot  P.s \OR Q.s) \\ 
     (6) & P \pIMP Q & = & (\lambda s\Dot  P.s \IMP Q.s) \\ 
     (7) & P \pEQU Q & = & (\lambda s\Dot  P.s = Q.s) 
   \end{array}\]
\end{definition}

\enddocs
\begincode{14}
\moddef{unquantified operators}\endmoddef
let TT_DEF = new_definition (`TT_DEF`, "(TT:*->bool) = \\s:*.T");;

let FF_DEF = new_definition (`FF_DEF`, "(FF:*->bool) = \\s:*.F");;

let pNOT_DEF = new_definition (`pNOT_DEF`, "NOT (p:*->bool) = \\s:*. ~p s");;

let pAND_DEF = new_infix_definition (`pAND_DEF`, 
    "AND (p:*->bool) (q:*->bool) = \\s:*. (p s) /\\ (q s)");;

let pOR_DEF = new_infix_definition (`pOR_DEF`, 
    "OR (p:*->bool) (q:*->bool) = \\s:*. (p s) \\/ (q s)");;

let pIMP_DEF = new_infix_definition (`pIMP_DEF`, 
    "IMP (p:*->bool) (q:*->bool) = \\s:*. (p s) ==> (q s)");;

let EQUAL_DEF = new_infix_definition (`EQUAL_DEF`, 
    "EQUAL (p:*->bool) (q:*->bool) = \\s:*. (p s) = (q s)");;
\endcode
\begindocs{15}


Quantified conjunction and disjunction will be respectively denoted by
$\pA$ and $\pE$.  Formal definition these operators is given below.

\begin{definition}{Quantified Operators}
\[ \begin{array}{llcl}
   (8) & (\pA i::W\Dot X.i) & = & (\lambda s\Dot  (\qA i::W\Dot  X.i)) \\
   (9) & (\pE i::W\Dot  X.i) & = & (\lambda s\Dot  (\qE i::W\Dot X.i)) 
   \end{array} \]
\end{definition}

Normally, a quantified operator is defined using
\code{}new_binder_definition\edoc{}. However, we also want to have restriction
on the quantification domain (thus, second order calculus). This is
the role of $W$ in above definition. To do this in HOL, we are
required to declare both $\pA$ and $\pE$ as binders with ML-function
\code{}new_binder\edoc{}, then associate their meaning using ML-function
\code{}associate_restriction\edoc{}.

\enddocs
\begincode{16}
\moddef{quantified operators}\endmoddef
new_binder(`!!`,":(*->**)->***") ;;
new_binder(`??`,":(*->**)->***") ;;

let RES_qAND = new_definition (`RES_qAND`,
   "RES_qAND (W:**->bool) (P:**->(*->bool)) = (\\s. (!i. W i ==> P i s))") ;;

let RES_qOR = new_definition (`RES_qOR`, 
   "RES_qOR (W:**->bool) (P:**->(*->bool)) = (\\s. ?i. W i /\\  P i s)") ;;

associate_restriction (`!!`, `RES_qAND`) ;;
associate_restriction (`??`, `RES_qOR`) ;;
\endcode
\begindocs{17}


\NOTE HOL does not save this association into the theory file, so the
loader will have to set this association up again when the user call
the library.

Because predicates are not Boolean objects, it does not make sense to
ask the truth value of a predicate $p$.  Still, it is very useful to
know which predicates are true on every point on its domain. For
example if we talk about state predicates, the state predicate $x=x$
holds in every state. In other words, such a predicate characterizes
the whole domain.

To formalize this concepts people use {\em everywhere} operator $[.]$.
The expression $[p]$ asserts that the predicate $p$ holds at every
point in its domain. The operator is defined as follows.

\begin{definition}{Everywhere Operator}
\[ \begin{array}{llcl}
   (10) & [P] & = & (\qA s\Dot  P.s) 
   \end{array} \]
\end{definition}

HOL cannot however parse this sort of bracketing operator, so we
choose to use prefix \code{}|==\edoc{} to represent $[.]$ in HOL. Also, as
\code{}|==\edoc{} is not part of HOL default special symbols, we have to declare
it as one using ML-function \code{}new_special_symbol\edoc{}.

\enddocs
\begincode{18}
\moddef{everywhere operator}\endmoddef
new_special_symbol `|==` ;;

let pSEQ_DEF = new_definition
  (`pSEQ_DEF`, "|== (p:*->bool) = !s:*. (p s)") ;;
\endcode
\begindocs{19}


\NOTE HOL does not save special symbol status to the theory file so
the loader must set it up again when the user call the library.









\chapter{The Theorems Part}
\label{proof}

The theorems part is devided as given below. The division will give
the reader some global insight to the theorems  provided by the
library.

Those theorems that do not involve quantified disjunction are
generally easy to prove using either either resolution or tautology
checker. Two tactics, the \code{}pred_CYAN_TAC\edoc{} and \code{}pred_JADE_TAC\edoc{} are
given for this purpose.

The quantified disjunction, $\pE$, is more difficult as it involves
existential quantification. As the domain of the quantification is
allowed to be infinite, this means that we will have to explicitly
supply HOL with the required witness.

\enddocs
\begincode{20}
\moddef{proving theorems}\endmoddef
\LA{}CYAN-and-JADE-tactics\RA{}
\LA{}abelian monoids in predicates\RA{}
\LA{}semi-rings in predicates\RA{}
\LA{}reflexivity of AND and OR\RA{}
\LA{}distributivity of AND(OR) over itself\RA{}
\LA{}IMP is a partial ordering\RA{}
\LA{}LUB and GLB\RA{}
\LA{}top and bottom\RA{}
\LA{}negation of true and false\RA{}
\LA{}de Morgan laws\RA{}
\LA{}contra position\RA{}
\LA{}quantified AND and OR over singleton\RA{}
\LA{}quantified AND and OR as generalization of AND and OR\RA{}
\LA{}continuity of AND\RA{}
\LA{}continuity of OR\RA{}
\LA{}domain split\RA{}

\endcode
\begindocs{21}

\section{The CYAN and JADE Tactics}
\label{JADE_CYAN}

The \code{}pred_JADE_TAC\edoc{} is intended to solve goal of the form
\begin{quote} \code{}!x. |== P\edoc{} \end{quote} where \code{}P\edoc{} does not contain
quantified disjunction operator.  

Given an $n>0$, the tactic will first unfold the definition of all
lifted operators involved and subsequently strips the goal as far as
it can.  Then, it tries to solve it by at most $n$ times resolving the
assumption.

The JADE tactic uses \code{}REPEAT_FIN\edoc{} tactical which is loaded from
library \code{}my_misc\edoc{}. Like the standard \code{}REPEAT\edoc{}, it applies a given
tactic, but at most a given $n$ times.

The \code{}pred_CYAN_TAC\edoc{} is intended to solve goal of the form
\begin{quote} \code{}!x. P = Q\edoc{} \end{quote} where both \code{}P\edoc{} and \code{}Q\edoc{} are
predicates expressions containing no quantified operator.

The tactic reduces the equality at the function level to an equality
at the domain level and then try to solve it by calling the tautology
checker.

The two tactics does not work well for goal involving quantified
disjunction. 

\enddocs
\begincode{22}
\moddef{CYAN-and-JADE-tactics}\endmoddef
let pred_JADE_TAC n =
    REWRITE_TAC (snd(split (definitions `predicate`)))
    THEN RESTRICT_DEF_TAC
    THEN (REPEAT STRIP_TAC)
    THEN (REPEAT_FIN n (ASM_REWRITE_TAC [] THEN RES_TAC)) ;;

let pred_CYAN_TAC =
    REWRITE_TAC (snd(split (definitions `predicate`)))
    THEN RESTRICT_DEF_TAC
    THEN REPEAT GEN_TAC THEN EXT_TAC THEN TAUT_TAC ;;
\endcode
\begindocs{23}



\section{Algebraic Structures in Predicates}

A binary operator is said to form a monoid if it is associative and it
has a unit element. If the operator is also commutative then it forms
an Abelian Monoid. The theorems below show that $\pAND$ and $\pOR$
each forms an Abelian Monoid.

\begin{theorem}{$\pAND$ forms an Abelian Monoid}
\Eline
\begin{thmlist} 
    \thf{pAND\_SYM} & : & \qA p,q\Dot  p\pAND q\ =\ q\pAND p \\
    \thf{pAND\_ASSOC} & : & 
          \qA p,q,r\Dot (p\pAND q)\pAND r\ =\ p\pAND(q\pAND r) \\
    \thf{pAND\_UNIT} & : & \qA p\Dot \TT\pAND p\ =\ p
\end{thmlist}
\end{theorem}

\begin{theorem}{$\pOR$ forms an Abelian Monoid}
\Eline
\begin{thmlist}
     \thf{pOR\_SYM}  & : & \qA p,q\Dot p\pOR q\ =\ q\pOR p \\
     \thf{pOR\_ASSOC} & : & 
          \qA p,q,r\Dot (p\pOR q)\pOR r\ =\ p\pOR(q\pOR r) \\
     \thf{pOR\_UNIT}  & : & \qA p\Dot \FF\pOR p\ =\ p
\end{thmlist}
\end{theorem}

\enddocs
\begincode{24}
\moddef{abelian monoids in predicates}\endmoddef
let pAND_SYM = prove_thm 
  (`pAND_SYM`, "!(p:*->bool) q. (p AND q) = (q AND p)", pred_CYAN_TAC) ;;

let pAND_ASSOC = prove_thm 
  (`pAND_ASSOC`, 
   "!(p:*->bool) q r. (p AND q) AND r = p AND (q AND r)", pred_CYAN_TAC) ;;

let pAND_UNIT = prove_thm 
  (`pAND_UNIT`, "!p:*->bool. (TT AND p) = p", pred_CYAN_TAC) ;;

let pOR_SYM = prove_thm 
  (`pOR_SYM`, "!(p:*->bool) q. (p OR q) = (q OR p)", pred_CYAN_TAC) ;;

let pOR_ASSOC = prove_thm 
  (`pOR_ASSOC`,
   "!(p:*->bool) q r. (p OR q) OR r =  p OR (q OR r)", pred_CYAN_TAC) ;;

let pOR_UNIT = prove_thm 
  (`pOR_UNIT`, "!p:*->bool. (FF OR p) = p", pred_CYAN_TAC) ;;
\endcode
\begindocs{25}


Two binary operators $(+,\times)$ are said to form a semi-ring if:
$\times$ is an monoids, and $+$ is an Abelien monoid, $\times$
distributes over $+$, and the unit of $+$ is also the zero of
$\times$.

We have two semi-rings: $(\pAND,\pOR)$ and $(\pOR,\pAND)$. As both has
been shown to form Abelian Monoids, it remains to prove the
distributivity and the zero element.

\begin{theorem}{$(\pOR,\pAND)$ Forms a Semi-ring}
\Eline
\begin{thmlist}
      \thf{pAND\_ZERO} & : & \qA p\Dot  \FF\pAND p\ =\ \FF \\
      \thf{pAND\_LOVER\_OR} & : &
           \qA p,q,r\Dot  p\pAND (q\pOR r)\ =\ (p\pAND q)\pOR (p\pAND r) \\
      \thf{pAND\_ROVER\_OR} & : &
           \qA p,q,r\Dot  (p\pOR q)\pAND r\ =\ (p\pAND r)\pOR (q\pAND r)
\end{thmlist}
\end{theorem}

\begin{theorem}{$(\pAND,\pOR)$ Forms a Semi-ring}
\Eline
\begin{thmlist}
      \thf{pOR\_ZERO} & : & \qA p\Dot  \TT\pOR p\ =\ \TT \\
      \thf{pOR\_LOVER\_AND} & : &
           \qA p,q,r\Dot  p\pOR (q\pAND r)\ =\ (p\pOR q)\pAND (p\pOR r) \\
      \thf{pOR\_ROVER\_AND} & : &
           \qA p,q,r\Dot  (p\pAND q)\pOR r\ =\ (p\pOR r)\pAND (q\pOR r)
\end{thmlist}
\end{theorem}   

\enddocs
\begincode{26}
\moddef{semi-rings in predicates}\endmoddef
let pAND_ZERO = prove_thm 
  (`pAND_ZERO`, "!p:*->bool. (FF AND p) = FF", pred_CYAN_TAC) ;;

let pAND_LOVER_OR = prove_thm 
  (`pAND_LOVER_OR`,
   "!(p:*->bool) q r. p AND (q OR r) = (p AND q) OR (p AND r)", 
    pred_CYAN_TAC) ;;

let pAND_ROVER_OR = prove_thm 
  (`pAND_ROVER_OR`,
   "!(p:*->bool) q r. (p OR q) AND r = (p AND r) OR (q AND r)", 
    pred_CYAN_TAC) ;;

let pOR_ZERO = prove_thm 
  (`pOR_ZERO`, "!p:*->bool. (TT OR p) = TT", pred_CYAN_TAC) ;;

let pOR_LOVER_AND = prove_thm 
  (`pOR_LOVER_AND`,
   "!(p:*->bool) q r. p OR (q AND r) = (p OR q) AND (p OR r)", 
    pred_CYAN_TAC) ;;

let pOR_ROVER_AND = prove_thm 
  (`pOR_ROVER_AND`,
   "!(p:*->bool) q r. (p AND q) OR r = (p OR r) AND (q OR r)", 
    pred_CYAN_TAC) ;;
\endcode
\begindocs{27}


If the $\times$ in the semi-ring $(+,\times)$ is reflexive the
semi-ring is also called Boolean semi-ring. Both semi-rings mentioned
above are Boolean semi-ring, as showed by the theorems below.

\begin{theorem}{$\pAND$ and $\pOR$ are Reflexive}
\Eline
\begin{thmlist}
      \thf{pAND\_REFL} & : & \qA p\Dot  p\pAND p\ =\ p \\
      \thf{pOR\_REFL}  & : & \qA p\Dot  p\pOR p\ =\ p
\end{thmlist}
\end{theorem}

\enddocs
\begincode{28}
\moddef{reflexivity of AND and OR}\endmoddef
let pAND_REFL = prove_thm 
  (`pAND_REFL`, "!p:*->bool. (p AND p) = p", pred_CYAN_TAC) ;;

let pOR_REFL = prove_thm 
  (`pOR_REFL`, "!p:*->bool. (p OR p) = p", pred_CYAN_TAC) ;;
\endcode
\begindocs{29}


As the corollary of its reflexivity and associativity, $\pAND$
distributes over itself, and so does $\pOR$.

\begin{theorem}{$\pAND (\pOR)$ Distributes over Itself}
\Eline
\begin{thmlist}
      \thf{pAND\_LOVER\_AND} & : &
           \qA p,q,r\Dot  p\pAND (q\pAND r)\ =\ (p\pAND q)\pAND (p\pAND r) \\
      \thf{pOR\_LOVER\_OR} & : &
           \qA p,q,r\Dot  p\pOR (q\pOR r)\ =\ (p\pOR q)\pOR (p\pOR r) \\
      \thf{pAND\_ROVER\_AND} & : &
           \qA p,q,r\Dot  (p\pAND q)\pAND r\ =\ (p\pAND r)\pAND (q\pAND r) \\
      \thf{pOR\_ROVER\_OR} & : &
           \qA p,q,r\Dot  (p\pOR q)\pOR r\ =\ (p\pOR r)\pOR (q\pOR r)
\end{thmlist}
\end{theorem}

\enddocs
\begincode{30}
\moddef{distributivity of AND(OR) over itself}\endmoddef
let pAND_LOVER_AND = prove_thm 
  (`pAND_LOVER_AND`,
   "!(p:*->bool) q r. p AND (q AND r) = (p AND q) AND (p AND r)", 
    pred_CYAN_TAC) ;;

let pOR_LOVER_OR = prove_thm 
  (`pOR_LOVER_OR`,
   "!(p:*->bool) q r. p OR (q OR r) = (p OR q) OR (p OR r)", 
    pred_CYAN_TAC) ;;

let pAND_ROVER_AND = prove_thm 
  (`pAND_ROVER_AND`,
   "!(p:*->bool) q r. (p AND q) AND r = (p AND r) AND (q AND r)", 
    pred_CYAN_TAC) ;;

let pOR_ROVER_OR = prove_thm 
  (`pOR_ROVER_OR`,
   "!(p:*->bool) q r. (p OR q) OR r = (p OR r) OR (q OR r)", 
    pred_CYAN_TAC) ;;
\endcode
\begindocs{31}


\section{The Lattice of Predicates}

A relation forms a partial ordering if it is reflexive, transitive,
and anti-symetric. The $\pIMP$-relation defined as follows: 
\[ q\ R\ p \ = \ [p\pIMP q] \] 
is such a relation. The theorems below show this.

\begin{theorem}{$\pIMP$ is a Partial Ordering}
\Eline
\begin{thmlist}
  \thf{pIMP\_REFL} & : & \qA p\Dot  [p \pIMP p] \\ 
  \thf{pIMP\_TRANS} & : & 
        \qA p,q,r\Dot  [p\pIMP q] \AND [q\pIMP r] \IMP [p\pIMP r]\\
  \thf{pIMP\_ANTISYM} & : &
        \qA p,q\Dot  [p\pIMP q] \AND [q\pIMP p] \IMP (p=q)
\end{thmlist}
\end{theorem}

\enddocs
\begincode{32}
\moddef{IMP is a partial ordering}\endmoddef
let pIMP_REFL = prove_thm
  (`pIMP_REFL`,
   "!P:*->bool. (|== (P IMP P))", pred_JADE_TAC 5) ;;

let pIMP_TRANS = prove_thm
  (`pIMP_TRANS`,
   "!(P:*->bool) Q R. (|== (P IMP Q)) /\\ (|== (Q IMP R)) ==>
                      (|== (P IMP R))",
    pred_JADE_TAC 5) ;;

let pIMP_ANTISYM = prove_thm
  (`pIMP_ANTISYM`,
   "!(P:*->bool) Q. (|== (P IMP Q)) /\\ (|== (Q IMP P)) ==>
                      (P=Q)",
    pred_JADE_TAC 1 THEN EXT_TAC
    THEN EQ_TAC THEN pred_JADE_TAC 5) ;;
\endcode
\begindocs{33}


The $\pIMP$-relation forms in fact a complete lattice. That is, every
set $W$ of predicates (over the same domain) has a supremum and
infimum, namely the $\pA$ and $\pE$ over the predicates in $W$. In
this lattice, $\FF$ is the top element and $\TT$ is the bottom.

\begin{theorem}{$\pA$ is the Supremum}
\Eline
\begin{thmlist}
  \thf{qAND\_GLB1} & : & 
        \qA W, P\Dot  (\qA i::W\Dot [(\pA\ j::W\Dot P.j)\pIMP P.i])\\
  \thf{qAND\_GLB2} & : &
        \qA W,P,q\Dot (\qA i::W\Dot [q\pIMP P.i]\ \IMP \
                 [q\pIMP (\pA\ i::W\Dot P.i)])
\end{thmlist}
\end{theorem}

\begin{theorem}{$\pE$ is the Infimum}
\Eline
\begin{thmlist}
\thf{qOR\_LUB1} & : & 
     \qA W, P\Dot  (\qA i::W\Dot [P.i \pIMP (\pE\ j::W\Dot P.j)]) \\
\thf{qOR\_LUB2} & : &
     \qA W,P,q\Dot (\qA i::W\ [P.i\pIMP q]\ \IMP\
                   [(\pE\ i::W\Dot P.i)\pIMP q])
\end{thmlist}
\end{theorem}
 
\enddocs
\begincode{34}
\moddef{LUB and GLB}\endmoddef
let qAND_GLB1 = prove_thm(`qAND_GLB1`,
    "!(W:**->bool) (P:**->(*->bool)). 
         !i:: W. |== ((!! j:: W. P j) IMP (P i))",
    pred_JADE_TAC 5) ;;

let qAND_GLB2 = prove_thm(`qAND_GLB2`,
    "!(W:**->bool) (P:**->(*->bool)) (q:*->bool).
         (!i:: W. |== (q IMP (P i))) ==> (|== (q IMP (!! j:: W. P j)))",
    pred_JADE_TAC 5) ;;

let qOR_LUB1 = prove_thm(`qOR_LUB1`,
    "!(W:**->bool) (P:**->(*->bool)).
         !i:: W. (|== ((P i) IMP (?? j:: W. P j)))",
    pred_JADE_TAC 0
    THEN EXISTS_TAC "x:**" THEN ASM_REWRITE_TAC[] ) ;;

let qOR_LUB2 = prove_thm(`qOR_LUB2`,
    "!(W:**->bool) (P:**->(*->bool)) (q:*->bool).
         (!i:: W. |== ((P i) IMP q)) ==> (|== ((?? j:: W. P j) IMP q))",
    pred_JADE_TAC 5) ;;
\endcode
\begindocs{35}


\begin{theorem}{$\FF$ is Top Element}
\Eline
\begin{thmlist}
  \thf{FF\_TOP} & : & \qA p\Dot [\FF \pIMP p] \\
  \thf{qOR\_EMPTY} & : & \qA P\Dot  (\pE\ i::\FF\Dot P.i) = \FF 
\end{thmlist}
\end{theorem}

\begin{theorem}{$\TT$ is Bottom Element}
\Eline
\begin{thmlist}
  \thf{TT\_BOTTOM} & : & \qA p\Dot [p \pIMP \TT] \\
  \thf{qAND\_EMPTY} & : & \qA P\Dot (\pA\ i::\FF\Dot P.i) = \TT
\end{thmlist}
\end{theorem}

Notice that CYAN tactic cannot prove \thf{qOR\_EMPTY} and {\thf
qAND\_EMPTY} as they are not in the form expected by the tactic.
Tactic \code{}EXT_TAC\edoc{} is used and then unfolding the definition of the
lifted operators will prove the theorem. \code{}EXT_TAC\edoc{} is loaded from
\code{}my_misc.ml\edoc{}. Its description can be found in the appendix.

\enddocs
\begincode{36}
\moddef{top and bottom}\endmoddef
let FF_TOP = prove_thm(`FF_TOP`,
    "!p:*->bool. |== (FF IMP p)", pred_JADE_TAC 5) ;;

let TT_BOTTOM = prove_thm(`TT_BOTTOM`,
    "!p:*->bool. |== (p IMP TT)", pred_JADE_TAC 5) ;;

let qOR_EMPTY = prove_thm (`qOR_EMPTY`,
    "!P:**->(*->bool). (??i:: FF. P i) = FF",
    EXT_TAC THEN pred_JADE_TAC 0) ;;

let qAND_EMPTY = prove_thm (`qAND_EMPTY`,
    "!P:**->(*->bool). (!!i:: FF. P i) = TT",
    EXT_TAC THEN pred_JADE_TAC 0) ;;
\endcode
\begindocs{37}


\section{More Properties of $\pA$ and $\pE$}

The quantified operator $\pA$ and $\pE$ behave as identity on
singletons. They are also the generalization of respectively $\pAND$
and $\pOR$. Furthermore, $\pAND$ and $\pOR$ are left and right $\pA$
and $\pE$-continous. That is, both $\pAND$ and $\pOR$ left and right
distribute over $\pA$ and $\pE$. The theorems below state these
facts. Notice that in some cases, continuity of $\pAND$ and $\pOR$
requires that the domain of quantification is non-empty.

The CYAN and JADE tactics cannot unfortunately on their own proves
those theorems because they are not in the form expected by either of
the tactics. 

Non standard tactics \code{}EXT_TAC\edoc{}, and \code{}XRULE_ASSUM_TAC\edoc{} are also
used. They are loaded from \code{}my_misc.ml\edoc{}. Their description can be
found in Appendix \ref{misc}.

\begin{theorem}{$\pA$ and $\pE$ over Singletons}
\Eline
\begin{thmlist}
   \thf{qAND\_SINGLETON} & : & 
         \qA P,a\Dot (\pA\ i::(\lambda j. a=j)\Dot P.i) = P.a \\
   \thf{qOR\_SINGLETON} & : & 
         \qA P,a\Dot (\pE\ i:(\lambda j. a=j)\Dot P.i) = P.a
\end{thmlist}
\end{theorem}

\enddocs
\begincode{38}
\moddef{quantified AND and OR over singleton}\endmoddef
let qAND_SINGLETON = prove_thm(`qAND_SINGLETON`,
    "!(P:**->(*->bool)) a. (!!i:: (\\j. a=j). P i) = (P a)",
    EXT_TAC THEN EQ_TAC 
    THEN pred_JADE_TAC 0
    THENL [ XRULE_ASSUM_TAC (REWRITE_RULE[] o (SPEC "a:**")) 
            THEN ASM_REWRITE_TAC[] ;
            XRULE_ASSUM_TAC SYM THEN ASM_REWRITE_TAC [] ] ) ;;

let qOR_SINGLETON = prove_thm(`qOR_SINGLETON`,
    "!(P:**->(*->bool)) a. (??i:: (\\j. a=j). P i) = (P a)",
    EXT_TAC THEN EQ_TAC
    THEN pred_JADE_TAC 0
    THENL [ALL_TAC ; EXISTS_TAC "a:**"]
    THEN ASM_REWRITE_TAC[] ) ;;
\endcode
\begindocs{39}


\begin{theorem}{$\pA$ and $\pE$ are generalization of $\pAND$ and
$\pOR$}
\Eline
\begin{thmlist}
   \thf{qAND\_AND} & : & 
         \qA p,q\Dot
         (\pA\ i::(\lambda j. (p=j)\OR(q=j))\Dot i) = (p \pAND q) \\
   \thf{qOR\_OR} & : & 
         \qA p,q\Dot
         (\pE\ i::(\lambda j. (p=j)\OR(q=j))\Dot i) = (p \pOR q)
\end{thmlist}
\end{theorem}

\enddocs
\begincode{40}
\moddef{quantified AND and OR as generalization of AND and OR}\endmoddef
let qAND_AND = prove_thm(`qAND_AND`,
    "!(p:*->bool) q. (!!i:: (\\j. (p=j) \\/ (q=j)). i) = (p AND q)",
    EXT_TAC THEN EQ_TAC
    THEN pred_JADE_TAC 1
    THEN XRULE_ASSUM_TAC SYM THEN ASM_REWRITE_TAC[]
    THENL 
    [ XRULE_ASSUM_TAC (REWRITE_RULE [] o (SPEC "p:*->bool")) ;
      XRULE_ASSUM_TAC (REWRITE_RULE [] o (SPEC "q:*->bool")) ]
    THEN ASM_REWRITE_TAC []) ;;

let qOR_OR = prove_thm(`qOR_OR`,
    "!(p:*->bool) q. (??i:: (\\j. (p=j) \\/ (q=j)). i) = (p OR q)",
    EXT_TAC THEN EQ_TAC
    THEN pred_JADE_TAC 1
    THEN XRULE_ASSUM_TAC SYM THEN ASM_REWRITE_TAC[]
    THENL [EXISTS_TAC "p:*->bool" ; EXISTS_TAC "q:*->bool"]
    THEN ASM_REWRITE_TAC []) ;;
\endcode
\begindocs{41}


\begin{theorem}{$\pAND$ is Left and Right $\pA$-Continous}
\Eline
\begin{thmlist}
   {qAND\_LEFT\_DISTR\_AND} & : & 
       \qA W,P,p\Dot \NOT(W=\FF)\ \IMP \\
   & & \TAB p\pAND (\qA\ i::W\Dot P.i) = (\qA\ i::W\Dot p\pAND P.i) \\
   {qAND\_RIGHT\_DISTR\_AND} & : & 
       \qA W,P,p\Dot \NOT(W=\FF)\ \IMP \\
   & & \TAB (\qA\ i::W\Dot P.i)\pAND p = (\qA\ i::W\Dot P.i\pAND p)
\end{thmlist}
\end{theorem}

\begin{theorem}{$\pAND$ is Left and Right $\pE$-Continous}
\Eline
\begin{thmlist}
   {qAND\_LEFT\_DISTR\_OR} & : & 
       \qA W,P,p\Dot 
            p\pAND (\qE\ i::W\Dot P.i) = (\qE\ i::W\Dot p\pAND P.i) \\
   {qAND\_RIGHT\_DISTR\_OR} & : & 
       \qA W,P,p\Dot 
            (\qE\ i::W\Dot P.i)\pAND p = (\qE\ i::W\Dot P.i\pAND p)
\end{thmlist}
\end{theorem}

\enddocs
\begincode{42}
\moddef{continuity of AND}\endmoddef
let qAND_RIGHT_DISTR_AND = prove_thm
  (`qAND_RIGHT_DISTR_AND`,
   "!W (P:**->(*->bool)) p. 
        ~(W=FF)  ==>  ((!!i::W. P i) AND p = (!!i::W. (P i) AND p))",
    REWRITE_TAC [FUN_EQ_CONV "(f:*->**)=g"]
    THEN pred_JADE_TAC 0
    THEN XRULE_ASSUM_TAC (REWRITE_RULE [NOT_FORALL_CONV "~(!x:**. ~W x)"])
    THEN UNDISCH_ALL_TAC THEN STRIP_TAC
    THEN EQ_TAC THEN pred_JADE_TAC 5) ;;

let qAND_LEFT_DISTR_AND = prove_thm
  (`qAND_LEFT_DISTR_AND`,
   "!W (P:**->(*->bool)) p. 
        ~(W=FF)  ==>  (p AND (!!i::W. P i) = (!!i::W. p AND (P i)))",
    ONCE_REWRITE_TAC [pAND_SYM]
    THEN ACCEPT_TAC qAND_RIGHT_DISTR_AND) ;;

let qAND_LEFT_DISTR_OR = prove_thm (`qAND_LEFT_DISTR_OR`,
    "!W (P:**->(*->bool)) p. (p AND (??i::W. P i)) = (??i::W. p AND P i)",
    EXT_TAC THEN EQ_TAC
    THEN pred_JADE_TAC 1
    THEN EXISTS_TAC "i:**" THEN ASM_REWRITE_TAC []) ;;

let qAND_RIGHT_DISTR_OR = prove_thm (`qAND_RIGHT_DISTR_OR`,
    "!W (P:**->(*->bool)) p. ((??i::W. P i) AND p) = (??i::W. (P i) AND p)",
    ONCE_REWRITE_TAC [pAND_SYM]
    THEN ACCEPT_TAC qAND_LEFT_DISTR_OR) ;;
\endcode
\begindocs{43}


\begin{theorem}{$\pOR$ is Left and Right $\pA$-continous}
\Eline
\begin{thmlist}
   {qOR\_LEFT\_DISTR\_AND} & : & 
       \qA W,P,p\Dot 
            p\pOR (\qA\ i::W\Dot P.i) = (\qA\ i::W\Dot p\pOR P.i) \\
   {qOR\_RIGHT\_DISTR\_AND} & : & 
       \qA W,P,p\Dot 
            (\qA\ i::W\Dot P.i)\pOR p = (\qA\ i::W\Dot P.i\pOR p)
\end{thmlist}
\end{theorem}

\begin{theorem}{$\pOR$ is Left and Right $\pE$-continous}
\Eline
\begin{thmlist}
   {qOR\_LEFT\_DISTR\_OR} & : & 
       \qA W,P,p\Dot \NOT(W=\FF)\ \IMP \\
       & & \TAB\TAB p\pOR (\qE\ i::W\Dot P.i) = (\qE\ i::W\Dot p\pOR P.i) \\
   {qOR\_RIGHT\_DISTR\_OR} & : & 
       \qA W,P,p\Dot \NOT(W=\FF)\ \IMP \\
       & & \TAB\TAB (\qE\ i::W\Dot P.i)\pOR p = (\qE\ i::W\Dot P.i\pOR p)
\end{thmlist}
\end{theorem}

\enddocs
\begincode{44}
\moddef{continuity of OR}\endmoddef
let qOR_RIGHT_DISTR_AND = prove_thm
  (`qOR_RIGHT_DISTR_AND`,
   "!W (P:**->(*->bool)) p. (!!i::W. P i) OR p = (!!i::W. (P i) OR p)",
   EXT_TAC THEN EQ_TAC 
   THEN pred_JADE_TAC 1
   THEN RES_TAC THEN ASM_REWRITE_TAC[]
   THEN ASM_CASES_TAC "(p:*->bool) x"
   THEN ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC
   THEN XRULE_ASSUM_TAC (REWRITE_RULE [ASSUME "~(p:*->bool) x"])
   THEN RES_TAC) ;;

let qOR_LEFT_DISTR_AND = prove_thm
  (`qOR_LEFT_DISTR_AND`,
   "!W (P:**->(*->bool)) p. p OR (!!i::W. P i) = (!!i::W. p OR (P i))",
    ONCE_REWRITE_TAC [pOR_SYM]
    THEN ACCEPT_TAC qOR_RIGHT_DISTR_AND) ;;

let qOR_RIGHT_DISTR_OR = prove_thm (`qOR_RIGHT_DISTR_OR`,
    "!W (P:**->(*->bool)) p. 
        ~(W=FF) ==> (((??i::W. P i) OR p) = (??i::W. (P i) OR p))",
    REWRITE_TAC [FUN_EQ_CONV "(f:*->**)=g"]
    THEN pred_JADE_TAC 0
    THEN XRULE_ASSUM_TAC (REWRITE_RULE [NOT_FORALL_CONV "~(!x:**. ~W x)"])
    THEN UNDISCH_ALL_TAC THEN STRIP_TAC
    THEN EQ_TAC THEN REPEAT STRIP_TAC 
    THENL [ EXISTS_TAC "i:**" ;
            EXISTS_TAC "x':**" ;
            DISJ1_TAC THEN EXISTS_TAC "i:**" ;
            ALL_TAC ]
    THEN ASM_REWRITE_TAC[]) ;;

let qOR_LEFT_DISTR_OR = prove_thm (`qOR_LEFT_DISTR_OR`,
    "!W (P:**->(*->bool)) p. 
        ~(W=FF) ==> ((p OR (??i::W. P i)) = (??i::W. p OR (P i)))",     
    ONCE_REWRITE_TAC [pOR_SYM]
    THEN ACCEPT_TAC qOR_RIGHT_DISTR_OR) ;;
\endcode
\begindocs{45}


Some other theorems that may be useful is the theorems for splitting the
quantification domain of $\pA$ and $\pE$.

\begin{theorem}{Splitting the Domain of $\pA$ and $\pE$}
\Eline
\begin{thmlist}
   qAND\_DOM\_SPLIT & : & 
   \qA W,P,a\Dot \\
   & & (\pA\ i::W\Dot P.i) \pAND P.a\ =\  
       (\pA\ i::(\lambda j. W.j \OR (a=j))\Dot P.i) \\
   qOR\_DOM\_SPLIT & : &
   \qA W,P,a\Dot \\
   & & (\pE\ i::W\Dot P.i) \pOR P.a\ =\  
       (\pE\ i::(\lambda j. W.j \OR (a=j))\Dot P.i)
\end{thmlist}
\end{theorem}

\enddocs
\begincode{46}
\moddef{domain split}\endmoddef
let qAND_DOM_SPLIT = prove_thm (`qAND_DOM_SPLIT`,
    "!W (P:**->(*->bool)) a. 
     ((!!i:: W. P i) AND (P a)) = (!!i::(\\j. (W j) \\/ (a=j)). P i)",
    EXT_TAC THEN EQ_TAC
    THEN pred_JADE_TAC 1
    THENL [ XRULE_ASSUM_TAC SYM THEN ASM_REWRITE_TAC[] ;
            XRULE_ASSUM_TAC (REWRITE_RULE [] o (SPEC "a:**"))
            THEN ASM_REWRITE_TAC[] ] ) ;;

let qOR_DOM_SPLIT = prove_thm (`qOR_DOM_SPLIT`,
    "!W (P:**->(*->bool)) a. 
        ((??i:: W. P i) OR (P a)) = (??i::(\\j. (W j) \\/ (a=j)). P i)",
    EXT_TAC THEN EQ_TAC
    THEN pred_JADE_TAC 0
    THENL [ EXISTS_TAC "i:**" ;
            EXISTS_TAC "a:**" ;
            DISJ1_TAC THEN EXISTS_TAC "i:**" ;
            ALL_TAC ]
    THEN ASM_REWRITE_TAC[]) ;;
\endcode
\begindocs{47}


\section{The Laws for Negation}

The most known one in engineering is the law of de Morgan that shows
that $\pAND$ and $\pOR$ are each other dual. Negation also reverses
the $\pIMP$ ordering (contra position law), and consequently top and
bottom are each other's negation.

\begin{theorem}{The Law of de Morgan}
\Eline
\begin{thmlist}
      \thf{pDEMORGAN2} & : &
           \qA p,q\Dot \ \pNOT(p \pAND q)\ =\  (\pNOT p) \pOR (\pNOT q) \\
      \thf{pDEMORGAN2} & : &
           \qA p,q\Dot \  \pNOT(p \pOR q)\ =\  (\pNOT p) \pAND (\pNOT q)
\end{thmlist}
\end{theorem}

\enddocs
\begincode{48}
\moddef{de Morgan laws}\endmoddef
let pDEMORGAN1 = prove_thm 
  (`pDEMORGAN1`, 
   "!(p:*->bool) q. (NOT (p AND q)) = ((NOT p) OR (NOT q))",
    pred_CYAN_TAC) ;;

let pDEMORGAN2 = prove_thm 
  (`pDEMORGAN2`, 
   "!(p:*->bool) q. (NOT (p OR q)) = ((NOT p) AND (NOT q))",
    pred_CYAN_TAC) ;;
\endcode
\begindocs{49}


\begin{theorem}{The Law of Contra-position}
\Eline
\begin{thmlist}
      \thf{pCONTRA\_POS} & : &
           \qA p,q\Dot \ p \IMP q\ =\  (\pNOT q) \IMP (\pNOT p)
\end{thmlist}
\end{theorem}

\enddocs
\begincode{50}
\moddef{contra position}\endmoddef
let pCONTRA_POS = prove_thm
  (`pCONTRA_POS`,
   "!(p:*->bool) q. (p IMP q) = ((NOT q) IMP (NOT p))",
    pred_CYAN_TAC) ;;
\endcode
\begindocs{51}


\begin{theorem}{$\TT$ and $\FF$ are Each Other's Inverse}
\Eline
\begin{thmlist}
      \thf{NOT\_TT} & : & \pNOT\TT = \FF \\
      \thf{NOT\_FF} & : & \pNOT\FF = \TT
\end{thmlist}
\end{theorem}

\enddocs
\begincode{52}
\moddef{negation of true and false}\endmoddef
let NOT_TT = prove_thm
  (`NOT_TT`, "NOT (TT:*->bool) = FF", pred_CYAN_TAC) ;;

let NOT_FF = prove_thm
  (`NOT_FF`, "NOT (FF:*->bool) = TT", pred_CYAN_TAC) ;;
\endcode
\begindocs{53}





\chapter{Finite Predicates Induction}
\label{induction}

In HOL there is a standard library called \code{}sets\edoc{} which provides
basic properties of finite sets, including finite set induction.
Still, manipulating predicates goes more fluent in HOL than sets. For
this practical reason one may prefer to calculate in terms of
predicates and keep in mind that predicates and sets are just two
sides of the same coin.

So far we have proved various properties of predicates. What is still
missing is the predicates analogous of the finite set induction
principle.

In the library \code{}sets\edoc{} there is a function $\SPEC$ that defines the
bijection between sets and predicates. So, for a given predicate $P$,
$\SPEC.P$ can be thought to denote the set represented by $P$. This is
given by the following theorem from \code{}sets\edoc{}:

\begin{theorem}{Specifying Set with Predicate (\thf{SPECIFICATION})}
\[ \qA P,x\Dot x\in\SPEC.P \ = \ P.x \]
\end{theorem}

The inverse of $\SPEC$ is called $\CHF$ (Characteristic Function).
That is, for all set $S$, $\CHF.S$ denotes the predicate representing
$S$.

In the library, finite sets are not defined in terms of enumeration by
natural number. Instead a set is called finite if it can be
characterized inductively.

\begin{definition}{Finite Sets} \\
For all set $S$:
\[ \begin{array}{l}
   \Fin.s\ = \
   ((\qA P\Dot  P.\Empty \AND 
        (\qA S'\Dot P.S' \IMP (\qA e\Dot P.(e \INSERT S'))))
        \ \IMP \ P.S)
   \end{array} \]
\end{definition}

It can be shown that all finite sets in above sense can be enumerated.
First, we will give the definition of cardinality, denoted by $\CARD$.
The cardinality of a finite set is simply the number of elements in
the set. It is defined inductively as follows.

\begin{definition}{Cardinality of Finite Sets}
\[ \begin{array}{l}
    \CARD.\Empty\ =\ 0 \ \ \AND \\
    (\qA S::\Fin\Dot 
    (\qA x\Dot \CARD(x \INSERT S)\ = \
     \left\{ \ \begin{array}{ll} 
                 \CARD.S & \mbox{if $x\in S$} \\
                 \SUC.(\CARD.S) & \mbox{if $x\not\in S$}
               \end{array} 
     \right.
   \end{array} \]
\end{definition}

Where $\SUC.n$ is the successor of the natural number $n$.

The following theorem from \code{}sets\edoc{} asserts that all finite sets are
enumerable. The converse of the theorem, namely that all enumerable
sets are finite, is not proven in \code{}sets\edoc{} although it will not be
difficult to derive it (note that enumerability implies that we can
apply natural number induction!).

\begin{theorem}{Enumerability of Finite Sets (\thf{FINITE\_ISO\_NUM})}
\Eline
$\begin{array}{l}
  \qA S::\Fin\Dot \qE f\Dot \\
  \TAB (\qA n,m\Dot  ((n < \CARD.S) \AND (m < \CARD.S)) 
                     \IMP (f.n = f.m) \IMP n = m) \ \AND \\
  \TAB (s = \Set{f.n \mid  n< \CARD.S})
\end{array}$
\end{theorem}

It follows quite straight forwardly from the definition of $\Fin$
that all predicates satisfying it will admit finite set induction.

\begin{theorem}{Finite Set Induction (\thf{FINITE\_INDUCT})}
\Eline
$\begin{array}{l}
  \qA P\Dot (P.\Empty \AND
      (\qA S\Dot (\Fin.S \AND P.s) \IMP 
           (\qA e\Dot e\not\in S \IMP P.(e \INSERT S))) \\
      \TAB \IMP \\
      \TAB (\qA S::\Fin\Dot P.s)
\end{array}$
\end{theorem}

What we want now is the analogous of above induction principle for
predicates. Let us first define a predicate $\CHFfin$ to characterize
all predicates that represent finite sets.

\begin{definition}{Finite Predicates}\\
For all predicate $W$:
\[ \CHFfin.W\ = \ \Fin.(\SPEC.W) \]
\end{definition}

\enddocs
\begincode{54}
\moddef{Finite Predicate, Definition}\endmoddef
let CHF_FINITE = new_definition(`CHF_FINITE`, 
   "CHF_FINITE (W:*->bool) = FINITE (SPEC W)" ) ;;
\endcode
\begindocs{55}


A predicate satisfying $\CHFfin$ is said to be finite. Below we derive
some properties relating predicates and sets, and finally also the
finite set induction principle.

\enddocs
\begincode{56}
\moddef{predicate and sets}\endmoddef
\LA{}Finite Predicate, Definition\RA{}
\LA{}FF Represents Empty Set\RA{}
\LA{}Inverse of CHF\RA{}
\LA{}Finite Predicate Direct Characterization\RA{}
\LA{}Finite Predicate Induction\RA{}
\endcode
\begindocs{57}


The following lemma states that $\FF$ represents empty set.

\begin{theorem}{Empty Set Lemma (\thf{EMPTY\_lemma})}
\[ \Empty \ = \ \SPEC.\FF \]
\end{theorem}

\enddocs
\begincode{58}
\moddef{FF Represents Empty Set}\endmoddef
let EMPTY_lemma = prove_thm(`EMPTY_lemma`,"\{\} = SPEC(FF:*->bool)",
    REWRITE_TAC [EMPTY_DEF ; FF_DEF]) ;;
\endcode
\begindocs{59}


Earlier we have said that $\CHF$ is the inverse of $\SPEC$. This fact
is easily derivable but not saved in \code{}sets\edoc{}. So, below is a theorem
that asserts this fact.

\begin{theorem}{Inverse of $\SPEC$ (\thf{CHF\_SPEC\_lemma})}
\[ \qA r\Dot \CHF(\SPEC.r) = r \]
\end{theorem}

\enddocs
\begincode{60}
\moddef{Inverse of CHF}\endmoddef
let CHF_SPEC_lemma = (REWRITE_RULE [] o BETA_RULE o CONJUNCT2) set_ISO_DEF ;;
save_thm (`CHF_SPEC_lemma` , CHF_SPEC_lemma) ;;
\endcode
\begindocs{61}


Instead of defining finite predicates in terms of finite sets, it can
be shown that they can be characterized directly in the way analogous
to the characterization of finite sets. We will need the following
three lemmas to prove it. The lemmas will not be saved.

\begin{theorem}{Set Lemma}
\Eline
$\begin{array}{l}
  \qA a,V\Dot \Set{y \mid  (y=a) \OR (y\in V)}\ = \
               \SPEC(\lambda\ y\Dot (y=a) \OR (\CHF.V). y)
\end{array}$
\end{theorem}

\enddocs
\begincode{62}
\moddef{SET Lemma}\endmoddef
let SET_lemma = prove_thm(`SET_lemma`,
   "!(a:*) V. \{y| (y=a) \\/ (y IN V)\} = SPEC(\\y.(y=a) \\/ ((CHF V) y))",
   REWRITE_TAC [IN_DEF] THEN REWRITE_TAC [GSPEC_DEF]
   THEN BETA_TAC THEN REWRITE_TAC [PAIR_EQ] THEN REPEAT GEN_TAC
   THEN AP_TERM_TAC THEN EXT_TAC
   THEN EQ_TAC THEN REPEAT STRIP_TAC
   THEN ASM_REWRITE_TAC[]
   THENL [ EXISTS_TAC "a:*" THEN ASM_REWRITE_TAC[] ;
           EXISTS_TAC "x:*" THEN ASM_REWRITE_TAC[] ] ) ;;
\endcode
\begindocs{63}


\begin{theorem}{Lemma1}
\Eline
$\begin{array}{l}
  (\qA V,a\Dot  X.V \IMP X.(\lambda\ x\Dot  (x=a) \OR V.x)) \\
  \IMP \\
  (\qA S\Dot X.(\CHF.S) \IMP  
      (\qA e\Dot X.(\lambda\ y\Dot (y=e) \OR \CHF.S.y)))
\end{array}$
\end{theorem}

\enddocs
\begincode{64}
\moddef{Finite Predicate Direct Characterization, Lemma1}\endmoddef
let lemma1 = prove(
   "(!V a. X V ==> X(\\x:*. (x=a) \\/ (V x))) ==>
    (!s:(*)set. X(CHF s) ==> (!e:*. X(\\y. (y=e) \\/ (CHF s y))))",
    REPEAT STRIP_TAC
    THEN RES_TAC THEN ASM_REWRITE_TAC[]) ;;
    
\endcode
\begindocs{65}


\begin{theorem}{Lemma2}
\Eline
$\begin{array}{l}
 (\qA s'\Dot P.s' \IMP 
     (\qA e\Dot P.(\SPEC(\lambda\ y\Dot (y=e) \OR CHF.s'.y)))) \\
 \IMP \\
 (\qA V,a\Dot P.(\SPEC.V) \IMP P.(\SPEC(\lambda\ x\Dot (x=a) \OR V.x)))
\end{array}$
\end{theorem}

\enddocs
\begincode{66}
\moddef{Finite Predicate Direct Characterization, Lemma2}\endmoddef
let lemma2 = prove(
   "(!s':(*)set. P s' ==> (!e:*. P(SPEC(\\y. (y=e) \\/ (CHF s' y)))))  ==>
    (!V (a:*). P(SPEC V) ==> P(SPEC(\\x:*. (x=a) \\/ V x)))",
    REPEAT STRIP_TAC
    THEN RES_TAC 
    THEN XRULE_ASSUM_TAC (REWRITE_RULE [CHF_SPEC_lemma])
    THEN ASM_REWRITE_TAC[]) ;;
\endcode
\begindocs{67}


The theorem below asserts that a predicate is finite if it can be
inductively characterized. The proof uses Set Lemma, Lemma1. and
Lemma2 given above.

\begin{theorem}{Direct Characterization of Finite Predicate 
(\thf{CHF\_FINITE\_def})}
\label{CHFfin.def2}
\Eline
$\begin{array}{l}
  \qA W\Dot \CHFfin.W\ = \\
  \TAB(\qA X\Dot (X.\FF \AND (\qA V,a\Dot X.V \IMP 
        X.(\lambda\ x\Dot (x=a) \OR V.x))) \ \IMP \ X.W)
\end{array}$
\end{theorem}

\enddocs
\begincode{68}
\moddef{Finite Predicate Direct Characterization}\endmoddef
\LA{}SET Lemma\RA{}
\LA{}Finite Predicate Direct Characterization, Lemma1\RA{}
\LA{}Finite Predicate Direct Characterization, Lemma2\RA{}

let CHF_FINITE_def = prove_thm 
  (`CHF_FINITE_def`,
   "!W:*->bool. (CHF_FINITE W) =
     (!X. (X FF) /\\ (!V a. (X V) ==> (X (\\x. (x=a) \\/ (V x))))  ==> (X W))",
   REWRITE_TAC [CHF_FINITE] THEN GEN_TAC
   THEN REWRITE_TAC [FINITE_DEF; INSERT_DEF]
   THEN REWRITE_TAC [SET_lemma ; EMPTY_lemma]
   THEN EQ_TAC THEN REPEAT STRIP_TAC
   THENL 
   [ IMP_RES_TAC lemma1
     THEN XRULE_ASSUM_TAC  
          ((REWRITE_RULE [CHF_SPEC_lemma]) o  BETA_RULE o (SPEC 
          "\\x:(*)set. (X:(*->bool)->bool) (CHF x)"))
     THEN RES_TAC ;
     OLD_IMP_RES_TAC lemma2
     THEN XRULE_ASSUM_TAC 
          (BETA_RULE o (SPEC "\\x:*->bool. (P:(*)set->bool)(SPEC x)"))
     THEN RES_TAC ]) ;;
\endcode
\begindocs{69}


Given the characterization of finite predicates as asserted by the
theorem above, it is not difficult to derive the following induction
priciple for finite predicates.

\begin{theorem}{Finite Predicates Induction 
(\thf{CHF\_INDUCTION})}
\label{pred.induct1}
\Eline
$\begin{array}{l}
  \qA X\Dot 
    (X.\FF \AND (\qA V,a\Dot X.V \IMP X.(\lambda\ x\Dot (x=a) \OR V.x))) \\
   \TAB \IMP \\
   \TAB (\qA V\Dot \CHFfin.V \IMP X.V)
\end{array}$
\end{theorem}

\enddocs
\begincode{70}
\moddef{Finite Predicate Induction}\endmoddef
let CHF_INDUCTION = prove_thm (`CHF_INDUCTION`,
   "!(X:(**->bool)->bool). 
    ((X FF) /\\ (!V a. (X V) ==> X(\\x. (x=a) \\/ (V x))))
    ==>
    (!V. (CHF_FINITE  V) ==> X V)",
   REWRITE_TAC [CHF_FINITE_def] THEN REPEAT STRIP_TAC
   THEN RES_TAC) ;;
\endcode
\begindocs{71}




\chapter{Future Work}

That in programming people pretend to work with predicate calculus may
not be formally justified but this is not entirely ungrounded because
the complete analogous of rules of predicates calculus simply holds in
the lifted calculus. The library \code{}predicate\edoc{} provides various basic
properties in the lifted calculus. A 'pretended' reference to a
certain property in predicate calculus is then formalized by a
reference to the corresponding property in the lifted calculus.

A more natural approach would be to provide a HOL rule to lift the
properties of logical operators to properties of lifted operators.
This way we can also pretend to use predicate calculus at the formal
level, only each 'pretended' reference must be encapsulated by the HOL
rule that lifts predicate calculus properties to lifted predicate
calculus properties.

This approach is nice because it will be more natural to the user. But
it also means that every pretended reference requires an explicit
lifting. So it is desirable that the lifting is effeciently
implemented. 



\appendix
\chapter{The Loader}
\label{loader}

When the loader is called from HOL using ML-function \code{}load_library\edoc{}
or \code{}load\edoc{}, it will attempt to load the theory \code{}predicate\edoc{} to the
current session. If the current theory is in draft mode\footnote{In
{\em draft mode} one can extend the theory with new types, new
definitions, or new parents. In the other mode, the {\em proof mode},
one can only add, or delete, theorems.} then the loader will also make
\code{}predicate\edoc{} a new parrent to the current theory.

Besides loading the theory \code{}predicate\edoc{}, the loader also does some
other things: 
\begin{enumerate} 
\item 
It adds the location of the library \code{}predicate\edoc{} to the search path
of HOL.  

\item 
It re-establishes the binder association for $\qA$ and $\qE$ and the
special symbol status for \code{}|==\edoc{}.

\item
It loads non-standard tactics and rules in \code{}my_misc.ml\edoc{}. Not all
rules and tactics in \code{}my_misc\edoc{} are necessary. Still the user may
find them useful. A description of \code{}my_misc\edoc{} is given in Appendix
\ref{misc}.

It also loads tactics \code{}pred_JADE_TAC\edoc{} and \code{}pred_CYAN_TAC\edoc{} from the
support file \code{}predicate_SUP.ml\edoc{}. The tactics can automatically prove
simple predicate properties. The code and description of the tactics
can be found in Section \ref{JADE_CYAN}.

\item
It sets up the auto loading function for definitions and theorems of
\code{}predicate\edoc{}.
\end{enumerate}

The structure of the loader is given below. Public version should use
\CodeRef{loader} while personal version should use \CodeRef{my
loader}.

\enddocs
\begincode{72}
\moddef{loader}\endmoddef
\LA{}adjust search path\RA{}
\LA{}loader independent part\RA{}

\endcode
\begincode{73}
\moddef{myloader}\endmoddef
\LA{}my adjust search path\RA{}
\LA{}loader independent part\RA{}

\endcode
\begincode{74}
\moddef{loader independent part}\endmoddef
\LA{}load theory\RA{}
\LA{}re-establish binders association\RA{}
\LA{}re-declare special symbols\RA{}
\LA{}load support rules and tactics\RA{}
\LA{}setup auto loading\RA{}
\endcode
\begindocs{75}


Below is the detail of each component. Notice that the difference
between the public and personal version is only in the setting of the
search path.

\enddocs
\begincode{76}
\moddef{adjust search path}\endmoddef
let pred_path = library_pathname() ^ `/predicate/` in
let sets_path = library_pathname() ^ `/sets/` in
    set_search_path (union (search_path()) [pred_path; sets_path]);
    print_string `(1) search path updated`; print_newline();;

\endcode
\begincode{77}
\moddef{my adjust search path}\endmoddef
let \LA{}my path\RA{} in
let sets_path = library_pathname() ^ `/sets/` in
set_search_path (union (search_path()) [my_path; sets_path]);;
print_string `(1) search path updated`;; print_newline();;

\endcode
\begincode{78}
\moddef{load theory}\endmoddef
if draft_mode() 
   then new_parent `predicate` else load_theory `predicate`;;

if draft_mode()
   then (print_string `(2) predicate declared as new parent` ;
         print_newline())
   else (if ((current_theory() = `predicate`))
         then (print_string `(2) theory predicate loaded` ;
               print_newline())
         else (print_string `Fail to load theory predicate!!` ;
               print_newline())) ;;

\endcode
\begincode{79}
\moddef{re-establish binders association}\endmoddef
associate_restriction (`!!`,`RES_qAND`) ;;
associate_restriction (`??`,`RES_qOR`) ;;

\endcode
\begincode{80}
\moddef{re-declare special symbols}\endmoddef
new_special_symbol `|==` ;;

\endcode
\begincode{81}
\moddef{load support rules and tactics}\endmoddef
load_library `taut` ;;
loadf `my_misc` ;;
if (draft_mode() or (current_theory() = `predicate`)) 
   then load(`predicate_SUP`, get_flag_value `print_lib`) ;;

\endcode
\begincode{82}
\moddef{setup auto loading}\endmoddef
if (draft_mode() or (current_theory() = `predicate`)) then
   let defs = map fst (definitions `predicate`) in
       map (\\name. autoload_theory(`definition`,`predicate`,name)) defs;
   let thms = map fst (theorems `predicate`) in
       map (\\name. autoload_theory(`theorem`,`predicate`,name)) thms; 
   delete_cache `predicate`; ();;

\endcode
\begindocs{83}

\chapter{HOL Definition for Predicate}
\label{HOL def}

Below is the list of the definition of lifted predicate calculus
operators as they has been entered to HOL. This should match the
intended definition given in Chapter \ref{def}.

\enddocs
\begincode{84}
\moddef{definitions}\endmoddef

The Theory predicate
Parents --  HOL     

Constants --
  AND        ":(* -> bool) -> ((* -> bool) -> (* -> bool))"
  OR         ":(* -> bool) -> ((* -> bool) -> (* -> bool))"
  IMP        ":(* -> bool) -> ((* -> bool) -> (* -> bool))"
  EQUAL      ":(* -> bool) -> ((* -> bool) -> (* -> bool))"
  TT         ":* -> bool"     
  FF         ":* -> bool"
  NOT        ":(* -> bool) -> (* -> bool)"     
  !!         ":(* -> **) -> ***"
  ??         ":(* -> **) -> ***"
  RES_qAND   ":(** -> bool) -> ((** -> (* -> bool)) -> (* -> bool))"
  RES_qOR    ":(** -> bool) -> ((** -> (* -> bool)) -> (* -> bool))"
  |==        ":(* -> bool) -> bool"     
  CHF_FINITE ":(* -> bool) -> bool"     

Infixes -- AND, OR, IMP, EQUAL

Binders -- !!, ??

Definitions --
  TT_DEF     |- TT = (\\s. T)
  FF_DEF     |- FF = (\\s. F)
  pNOT_DEF   |- !p. NOT p = (\\s. ~p s)
  pAND_DEF   |- !p q. p AND q = (\\s. p s /\\ q s)
  pOR_DEF    |- !p q. p OR q = (\\s. p s \\/ q s)
  pIMP_DEF   |- !p q. p IMP q = (\\s. p s ==> q s)
  EQUAL_DEF  |- !p q. p EQUAL q = (\\s. p s = q s)
  RES_qAND   |- !W P. RES_qAND W P = (\\s. !i. W i ==> P i s)
  RES_qOR    |- !W P. RES_qOR W P = (\\s. ?i. W i /\\ P i s)
  pSEQ_DEF   |- !p. |== p = (!s. p s)
  CHF_FINITE |- !W. CHF_FINITE W = FINITE(SPEC W)     

\endcode
\begindocs{85}


The definition of \code{}!!\edoc{} and \code{}??\edoc{} are associated by
\code{}associate_restriction\edoc{} to respectively \code{}RES_qAND\edoc{} and \code{}RES_qO\edoc{}.
So this means that 
\begin{quote}
   \code{}(!!x::W. P)\edoc{} and \code{}(??x::W.P)\edoc{}
\end{quote}
will be respectively parsed as
\begin{quote}
   \code{}RES_qAND W (\\x. P)\edoc{} and \code{}RES_qOR W (\\x. P)\edoc{}
\end{quote}
and by unfolding the definition of \code{}RES_qAND\edoc{} and \code{}RES_qOR\edoc{} above are equal to
\begin{quote}
   \code{}(\\s. (!i. W i ==> P i s)\edoc{} and \code{}(\\s. ?i. W i /\\ P i s)\edoc{}
\end{quote}

Below is the list of all theorems provided by the library
\code{}predicate\edoc{}. The user can always get it, together with the list of
definitions, by typing \code{}print_theory `predicate`\edoc{}.

\enddocs
\begincode{86}
\moddef{theorems}\endmoddef

  pAND_SYM        |- !p q. p AND q = q AND p
  pAND_ASSOC      |- !p q r. (p AND q) AND r = p AND (q AND r)
  pAND_UNIT       |- !p. TT AND p = p

  pOR_SYM         |- !p q. p OR q = q OR p
  pOR_ASSOC       |- !p q r. (p OR q) OR r = p OR (q OR r)
  pOR_UNIT        |- !p. FF OR p = p

  pAND_ZERO       |- !p. FF AND p = FF
  pAND_LOVER_OR   |- !p q r. p AND (q OR r) = (p AND q) OR (p AND r)
  pAND_ROVER_OR   |- !p q r. (p OR q) AND r = (p AND r) OR (q AND r)

  pOR_ZERO        |- !p. TT OR p = TT
  pOR_LOVER_AND   |- !p q r. p OR (q AND r) = (p OR q) AND (p OR r)
  pOR_ROVER_AND   |- !p q r. (p AND q) OR r = (p OR r) AND (q OR r)

  pAND_REFL       |- !p. p AND p = p
  pOR_REFL        |- !p. p OR p = p

  pAND_LOVER_AND  |- !p q r. p AND (q AND r) = (p AND q) AND (p AND r)
  pOR_LOVER_OR    |- !p q r. p OR (q OR r) = (p OR q) OR (p OR r)
  pAND_ROVER_AND  |- !p q r. (p AND q) AND r = (p AND r) AND (q AND r)
  pOR_ROVER_OR    |- !p q r. (p OR q) OR r = (p OR r) OR (q OR r)

  pIMP_REFL       |- !P. |==(P IMP P)
  pIMP_TRANS      |- !P Q R. |==(P IMP Q) /\\ |==(Q IMP R) ==> |==(P IMP R)
  pIMP_ANTISYM    |- !P Q. |==(P IMP Q) /\\ |==(Q IMP P) ==> (P = Q)

  qAND_GLB1       |- !W P. !i :: W. |==((!! j :: W. P j) IMP (P i))
  qAND_GLB2       |- !W P q. (!i :: W. |==(q IMP (P i))) ==> 
                             |==(q IMP (!! j :: W. P j))

  qOR_LUB1        |- !W P. !i :: W. |==((P i) IMP (?? j :: W. P j))
  qOR_LUB2        |- !W P q. (!i :: W. |==((P i) IMP q)) ==> 
                             |==((?? j :: W. P j) IMP q)

  FF_TOP          |- !p. |==(FF IMP p)
  TT_BOTTOM       |- !p. |==(p IMP TT)

  qOR_EMPTY       |- !P. (?? i :: FF. P i) = FF
  qAND_EMPTY      |- !P. (!! i :: FF. P i) = TT

  NOT_TT          |- NOT TT = FF
  NOT_FF          |- NOT FF = TT

  pDEMORGAN1      |- !p q. NOT(p AND q) = (NOT p) OR (NOT q)
  pDEMORGAN2      |- !p q. NOT(p OR q) = (NOT p) AND (NOT q)

  pCONTRA_POS     |- !p q. p IMP q = (NOT q) IMP (NOT p)

  qAND_SINGLETON  |- !P a. (!! i :: \\j. a = j. P i) = P a
  qOR_SINGLETON   |- !P a. (?? i :: \\j. a = j. P i) = P a

  qAND_AND        |- !p q. (!! i :: \\j. (p = j) \\/ (q = j). i) = p AND q
  qOR_OR          |- !p q. (?? i :: \\j. (p = j) \\/ (q = j). i) = p OR q

  qAND_RIGHT_DISTR_AND
                  |- !W P p. ~(W = FF) ==>
                     ((!! i :: W. P i) AND p = (!! i :: W. (P i) AND p))
  qAND_LEFT_DISTR_AND
                  |- !W P p.
                     ~(W = FF) ==>
                     (p AND (!! i :: W. P i) = (!! i :: W. p AND (P i)))

  qAND_LEFT_DISTR_OR
                  |- !W P p. p AND (?? i :: W. P i) = (?? i :: W. p AND (P i))
  qAND_RIGHT_DISTR_OR
                  |- !W P p. (?? i :: W. P i) AND p = (?? i :: W. (P i) AND p)

  qOR_RIGHT_DISTR_AND
                  |- !W P p. (!! i :: W. P i) OR p = (!! i :: W. (P i) OR p)
  qOR_LEFT_DISTR_AND
                  |- !W P p. p OR (!! i :: W. P i) = (!! i :: W. p OR (P i))

  qOR_RIGHT_DISTR_OR
                  |- !W P p. ~(W = FF) ==> 
                     ((?? i :: W. P i) OR p = (?? i :: W. (P i) OR p))
  qOR_LEFT_DISTR_OR
                  |- !W P p. ~(W = FF) ==> 
                     (p OR (?? i :: W. P i) = (?? i :: W. p OR (P i)))

  qAND_DOM_SPLIT  |- !W P a. (!! i :: W. P i) AND (P a) = 
                             (!! i :: \\j. W j \\/ (a = j). P i)
  qOR_DOM_SPLIT   |- !W P a. (?? i :: W. P i) OR (P a) = 
                             (?? i :: \\j. W j \\/ (a = j). P i)


  EMPTY_lemma     |- EMPTY = SPEC FF
  CHF_SPEC_lemma  |- !r. CHF(SPEC r) = r

  CHF_FINITE_def  |- !W. CHF_FINITE W =
                       (!X. X FF /\\ (!V a. X V ==> X(\\x. (x = a) \\/ V x))
                        ==> X W)

  CHF_INDUCTION   |- !X.
                       X FF /\\ (!V a. X V ==> X(\\x. (x = a) \\/ V x)) 
                       ==>
                       (!V. CHF_FINITE V ==> X V)
\endcode
\begindocs{87}


  

\chapter{Help Rules Tactics from my\_misc}
\label{misc}

This appendix contains the description of non-standard rules and
tactics in the support file \code{}my_misc.ml\edoc{}. Some of these rules and
tactics are indeed used in the library \code{}predicate\edoc{}. The other have
been included simply because we found them useful in further
application of this library. Other users may find them useful too,
otherwise one can always delete them from the \code{}my_misc.ml\edoc{}.

\enddocs
\begincode{88}
\moddef{mymisc}\endmoddef
\LA{}rules\RA{}
\LA{}tactics\RA{}
\endcode
\begindocs{89}


\section{Rules}

Below is an overview of rules provided in \code{}my_misc.ml\edoc{}.

\enddocs
\begincode{90}
\moddef{rules}\endmoddef
\LA{}RESTRICT\_DEF\_RULE\RA{}
\LA{}RESTRICT\_SHIFT\RA{}
\LA{}IMP\_LEFT\_RULE\RA{}
\LA{}IMP\_RIGHT\_RULE\RA{}
\endcode
\begindocs{91}


\begin{RULE}{RESTRICT\_DEF\_RULE} \\
The rule unfolds the definition of restricted $\qA$ and $\qE$:
\begin{quote}
$\begin{Drule}
   A \deriv\  \qA i::W\Dot P  \\ \hline
   A \deriv\  \qA i\Dot (W i) \IMP P
\end{Drule}$
\ \ \ and \ \ \
$\begin{Drule}
   A \deriv\ \qE i::W\Dot P  \\ \hline
   A \deriv\ \qE i\Dot (W i) \AND P 
\end{Drule}$
\end{quote}
\end{RULE}

\enddocs
\begincode{92}
\moddef{RESTRICT\_DEF\_RULE}\endmoddef
let RES_lst = 
    [ definition `bool` `RES_FORALL`; definition `bool` `RES_EXISTS`] ;;
let RESTRICT_DEF_RULE thm = BETA_RULE (REWRITE_RULE RES_lst thm) ;;
\endcode
\begindocs{93}


\begin{RULE}{RESTRICT\_SHIFT} \\
\[ \begin{Drule}
   A \deriv\ \qA i::W\Dot \qA j\Dot P  \\ \hline
   A \deriv\ \qA i,j\Dot (W i) \IMP  P
\end{Drule}\]
\end{RULE}

\enddocs
\begincode{94}
\moddef{RESTRICT\_SHIFT}\endmoddef
let RESTRICT_SHIFT thm =
    let th1 = SPEC_ALL (RESTRICT_DEF_RULE thm) in
    let asm = fst(dest_imp(concl th1)) in
    (GEN_ALL o (DISCH asm) o SPEC_ALL o UNDISCH) th1 ;;
\endcode
\begindocs{95}


\begin{RULE}{IMP\_LEFT\_RULE} \\
\[ \begin{Drule}
   A \deriv\ \qA i\Dot P \IMP Q \AND R  \\ \hline
   A \deriv\ \qA i\Dot P\IMP Q
\end{Drule} \]
\end{RULE}

\enddocs
\begincode{96}
\moddef{IMP\_LEFT\_RULE}\endmoddef
let IMP_LEFT_RULE thm =
    let th1 = SPEC_ALL thm in
    let asm = fst(dest_imp(concl th1)) in
    (GEN_ALL o (DISCH asm) o CONJUNCT1 o UNDISCH) th1 ;;
\endcode
\begindocs{97}


\begin{RULE}{IMP\_RIGHT\_RULE} \\
\[ \begin{Drule}
   A \deriv\ \qA i\Dot P \IMP Q \AND R  \\ \hline
   A \deriv\ \qA i\Dot P \IMP Q
\end{Drule}\]
\end{RULE}

\enddocs
\begincode{98}
\moddef{IMP\_RIGHT\_RULE}\endmoddef
let IMP_RIGHT_RULE thm =
    let th1 = SPEC_ALL thm in
    let asm = fst(dest_imp(concl th1)) in
    (GEN_ALL o (DISCH asm) o CONJUNCT2 o UNDISCH) th1 ;;
\endcode
\begindocs{99}



\section{Tactics and Tacticals}

Below is an overview of the tactics given in \code{}my_misc\edoc{}.

\enddocs
\begincode{100}
\moddef{tactics}\endmoddef
\LA{}RESTRICT\_DEF\_TAC\RA{}
\LA{}REPEAT\_FIN\RA{}
\LA{}UNDISCH\_ALL\_TAC\RA{}
\LA{}EXT\_TAC\RA{}
\LA{}ASM\_TAC\RA{}
\LA{}XRULE\_ASSUM\_TAC\RA{}
\endcode
\begindocs{101}


\begin{RULE}{RESTRICT\_DEF\_TAC} \\
The tactic unfolds the definition of restricted $\qA$ and $\qE$:
\begin{quote}
$\begin{Drule}
   A \goal\ \qA i::W\Dot P  \\ \hline
   A \goal\ \qA i\Dot (W i)\IMP P
\end{Drule}$
\ \ \ and \ \ \
$\begin{Drule}
   A \goal\ \qE i::W\Dot P  \\ \hline
   A \goal\ \qE i\Dot (W i) \AND P 
\end{Drule}$
\end{quote}
\end{RULE}

\enddocs
\begincode{102}
\moddef{RESTRICT\_DEF\_TAC}\endmoddef
let RESTRICT_DEF_TAC  = REWRITE_TAC RES_lst THEN BETA_TAC ;;
\endcode
\begindocs{103}


\begin{RULE}{REPEAT\_FIN} \\
For a given natural number \code{}n\edoc{} and a tactic \code{}tac\edoc{}, \code{}REPEAT_FIN n
tac\edoc{} simply applies \code{}tac\edoc{} \code{}n\edoc{} times to the goal.
\end{RULE}

\enddocs
\begincode{104}
\moddef{REPEAT\_FIN}\endmoddef
letrec REPEAT_FIN n tac =
    if n=0 then ALL_TAC
    else (tac THEN REPEAT_FIN (n-1) tac) ;;
\endcode
\begindocs{105}


\begin{RULE}{UNDISCH\_ALL\_TAC} \\
Undicharge all assumptions of the goal.
\end{RULE}

\enddocs
\begincode{106}
\moddef{UNDISCH\_ALL\_TAC}\endmoddef
letrec UNDISCH_ALL_TAC (asml,g) =
    if (asml = []) then ALL_TAC (asml,g)
    else (UNDISCH_TAC (hd asml) THEN UNDISCH_ALL_TAC) (asml,g) ;;
\endcode
\begindocs{107}


\begin{RULE}{EXT\_TAC}\\
\[ \begin{Drule}
   A \goal\  \qA i\Dot f=g  \\ \hline
   A \goal\  f x = g x 
\end{Drule}\]
\end{RULE}

\enddocs
\begincode{108}
\moddef{EXT\_TAC}\endmoddef
let EXT_TAC  =
    let EXT_SPEC_TAC (asml,g) = 
        (REWRITE_TAC [FUN_EQ_CONV g] 
        THEN BETA_TAC THEN GEN_TAC) (asml,g) in
    REPEAT GEN_TAC THEN EXT_SPEC_TAC ;;
\endcode
\begindocs{109}


\begin{RULE}{ASM\_TAC}\\
For a given rule \code{}R\edoc{}, \code{}ASM_TAC R\edoc{} applies \code{}R\edoc{} to every
assumption of the goal. For every assumption \code{}Ai\edoc{} where \code{}R\edoc{} does
not fail, the tactic adds the result of the application to the
assumption list.
\end{RULE}

\enddocs
\begincode{110}
\moddef{ASM\_TAC}\endmoddef
let ASM_TAC rule = EVERY_ASSUM (\\thm. ASSUME_TAC (rule thm) ? ALL_TAC) ;;
\endcode
\begindocs{111}


\begin{RULE}{XRULE\_ASSUM\_TAC}\\
For a given rule \code{}R\edoc{}, \code{}XRULE_ASSUM_TAC R\edoc{} applies \code{}R\edoc{} to every
assumption \code{}Ai\edoc{} of the goal. If \code{}R\edoc{} fails on \code{}Ai\edoc{} then \code{}Ai\edoc{}
remains, else it is replaced with the result of applying \code{}R\edoc{} to \code{}Ai\edoc{}.
\end{RULE}

\enddocs
\begincode{112}
\moddef{XRULE\_ASSUM\_TAC}\endmoddef
let XRULE_ASSUM_TAC rule = RULE_ASSUM_TAC (\\thm. rule thm ? thm) ;;
\endcode
\end{document}
