\documentclass{slides}

\usepackage{amsmath}
\usepackage{latexsym}
\usepackage{amssymb}
\usepackage{exptrees}

\input{/home/arp/disk1/rpg/papers/sld/gore-defs}

\renewcommand\invrule[2]{ 
% for use in non-math mode, args interpreted in math mode
  \begin{tabular}{@{}c@{}}
  $ #1 $ \\ \hline \hline $ #2 $
  \end{tabular}}
\newcommand\slrule[2]{ % similar to \frac, except
% for use in non-math mode, args interpreted in math mode
  \begin{tabular}{@{}c@{}}
  $ #1 $ \\ \hline $ #2 $
  \end{tabular}}

\newcommand\dRA{{\boldmath $\delta$}\textbf{RA}}

\newenvironment{heading}{\noindent\centering\large\bf}{\par}
\newenvironment{Heading}{\noindent\centering\Large\bf}{\par}

\begin{document}


\title{ }
\begin{slide}
  \begin{Heading}
{Embedding Display Calculi into Logical Frameworks}
  \end{Heading}

\begin{tabular*}{\linewidth}{@{}l@{\extracolsep{\fill}}l@{}} 
Jeremy Dawson & Rajeev Gor\'{e} \\
\multicolumn 2 c {Automated Reasoning Group and} \\
\multicolumn 2 c {Dept.\ of Computer Science}\\
\multicolumn 2 c {Australian National University} \\ 
\multicolumn 2 c {Canberra, Australia} \\
{\tt jeremy@arp.anu.edu.au} &   {\tt rpg@arp.anu.edu.au}
  \end{tabular*}

\small
Dawson supported by Australian Research Council Small \& Large Grants

Gor\'e supported by an Australian Research Council QEII Fellowship
\end{slide}

\begin{slide}
  \begin{heading}
    {Introduction}
  \end{heading}


\begin{itemize}
\item Display logic is a modular proof-theoretic framework using sequents
\item it admits a general cut-elimination proof
\item used for many undecidable substructural logics, so need interactive
prover
\item want to use existing theorem provers
\item want to use syntactic proof-theoretic methods, not semantic embeddings
\item we discuss and compare three mechanisations
\end{itemize}

\end{slide}

\begin{slide}
  \begin{heading}
    { Display Logic}
  \end{heading}

  \begin{itemize}
  \item Display logic is a generalised Gentzen formulation due to Nuel
    Belnap

  \item We consider the particular display calculus \dRA\ for 
  relation algebra

  \item Structural connectives: \hfill $I$ \hfill $\ast$ \hfill $\bullet$
                                \hfill , \hfill ;

  \item Structure % (for relation algebra, \dRA):\\
  (where $\varphi$ is a formula): \\
  \hfill $X \hfill ::= \hfill \varphi \hfill \mid \hfill I 
		      \hfill \mid \hfill \ast X 
		      \hfill \mid \hfill \bullet X 
		      \hfill  \mid \hfill X , X
		      \hfill  \mid \hfill X ; X $ \\


  \item Sequent: \hfill $X \vdash Y$ \hfill where $X, Y$ are
    structures

  \item There is a single cut-elimination theorem
    applying to all display calculi (modulo conditions on the rules),
    our aim is to mechanise its proof

  \end{itemize}

\end{slide}

\begin{slide}
  \begin{heading}
    { Display Logic Rules}
  \end{heading}

\begin{itemize}
  \item These two rules \hfill $p \vdash p$ \hfill 
                       \brule{}
		       {$X \vdash \varphi$}
                                    {$\varphi \vdash Y$}
                                    {$X  \vdash Y$}

\item Display postulates, can move structures around
(can display any substructure)

\hfill
\slrule {X, Y \vdash Z} {Y \vdash *X, Z} (dp)
\hfill
\slrule {*X \vdash Y} {*Y \vdash X} (dp)
\hfill \mbox{}
\item Structural rules, give properties of logic

\hfill
\slrule {X, X \vdash Z} {X \vdash Z} (contr)
\hfill
\slrule {X, Y \vdash Z} {Y, X \vdash Z} (comm)
\hfill \mbox{}
\item Logical introduction rules 
(left and right)

\hfill
\slrule {X \vdash A, B} {X \vdash A \lor B}  ($\vdash \lor$)
\hfill
\slrule {A \vdash X \quad B \vdash Y } {A \lor B \vdash X,Y }  ($\lor \vdash$)
\hfill \mbox{}

Formula introduced is always displayed
\end{itemize}


\end{slide}

\begin{slide} \setlength\parskip{0.8\parskip}
  \begin{heading}
    { Isabelle/Pure implementation}
  \end{heading}

\begin{itemize}
\item Isabelle's meta-logic is intuitionistic (higher-order) logic 
\item User can supply own object-logic, or use one supplied
\item Facilitates natural-deduction style proofs,
can program combinations of proof steps
\item To embed sequent system, use sequent (not formula) as top object
language construct
% \item for example, the ($\lor \vdash $) rule,
% \slrule {A \vdash X \quad B \vdash Y } {A \lor B \vdash X,Y } 
% appears as \texttt{[| ?A |- \$?X; ?B |- \$?Y |] ==> ?A v ?B |- \$?X, \$?Y}

\item 
\slrule {A \vdash X \quad B \vdash Y } {A \lor B \vdash X,Y } 
\begin{tabular}{c}
\texttt{[| ?A |- \$?X; ?B |- \$?Y |]} \\
\texttt{==>} \\
\texttt{?A v ?B |- \$?X, \$?Y}
\end{tabular}

\item This is a \emph{shallow} embedding - we can do derivations, but can't 
prove things about them
\end{itemize}

\end{slide}

\begin{slide}
  \begin{heading}
    { The Curry-Howard Isomorphism}
  \end{heading}

\begin{itemize}
\item Type theory rules correspond to intuitionistic logic rules.
\item note: Natural Deduction style, $\vdash$ is type context 
  (not sequent calculus or \dRA)
\item type $A$ $\leadsto$ proposition $A$
\item  $t: A$ $\leadsto$ $t$ ``is'' proof of proposition $A$
\end{itemize}

\begin{center}
\begin{tabular}{c@{\qquad}c}
\slrule {f : A \to B \quad a : A }
{f(a) : B }
&
\slrule {\pi[A] : A \to B \quad \rho : A } {\pi[A:=\rho] : B }
\\[4.0ex]
\slrule {\Gamma, v:A \vdash e : B }
{\Gamma \vdash \lambda v. e : A \to B }
&
\slrule {\pi:A \vdash \rho[\pi] : B }
{\vdash \rho[\pi := A] : A \to B }
\end{tabular}
\end{center}

\end{slide}

\begin{slide}
  \begin{heading}
    { Dependent Types}
  \end{heading}

\begin{itemize}
\item A type can be a function of a term -- eg curried \texttt{printf}

\item We can use this in two ways -- firstly, quantifier logic 

\item $I = $\{individuals\}, for $i \in I$, let $A(i)$ be a type
(dependent on $i$)

\item Function $\rho$, domain $I$, $\rho(i) : A(i)$

\item With expressions as proofs, $\rho(i)$ is a proof of $A(i)$

\item $\rho$ is a recipe for proving any $A(i)$, ie $\rho$ is a proof of
$\forall i A(i)$
\end{itemize}

\end{slide}

\begin{slide}
  \begin{heading}
    { A Second Use of Dependent Types}
  \end{heading}

\begin{itemize}
\item $F = $\{formulae\}, for $f \in F$, let $P(f)$ be a type,
  representing derivations of formula $f$

\item Rule \slrule {A \to B \quad A} {B} is (an object of) the type 
${P(a \to b) \to P(a)} \to {P(b)}$ ($a, b$ variables)

\item $f : P(a) \to P(c)$ gives $f' : P(a) \to P(b) \to P(c)$, so 
  rule \slrule {A} {C} gives rule \slrule {A \quad B} {C} 

\item similarly contraction, exchange 

\item We use $\vdash$ (binary infix) for $P$
\end{itemize}

\end{slide}

\begin{slide}
  \begin{heading}
    { The Twelf Implementation}
  \end{heading}

Twelf -- a system based on Dependent Types

\begin{tabular}{c@{\quad}l}
1 & \texttt{str : type.      } \\
2 & \texttt{|- : str -> str -> type. \%infix none 10 |-.} \\
3 & \texttt{*  : str -> str.         \%prefix 200 *.} \\
  & \\
4 & \texttt{\% Display postulates } \\
5 & \texttt{sA :    (* X |- Y) -> (* Y |- X).} \\
6 & \texttt{sS :    (X |- * Y) -> (Y |- * X).} \\
  & \\
7 & \texttt{\% Derived structural rules} \\
8 & \texttt{ssASl = [D] sA (sS D).}\\
  & \texttt{\quad \% (X |- * * Y) -> (* * X |- Y)} 

\end{tabular}

\begin{center}
Lines 5,6 are
\hfill
\slrule { *X \vdash Y } { *Y \vdash X } (\texttt{sA}) \qquad
\hfill
\slrule { X \vdash *Y } { Y \vdash *X } (\texttt{sS}) \qquad
\end{center}

Line 8 means $\lambda D. sA (sS D)$, rule 
\slrule { X \vdash **Y } { **X \vdash Y } 
$$
\stackrel {\mbox{deriv of}}{U \vdash * * V} \quad
\stackrel{\texttt{sS}} \longrightarrow \quad
\stackrel {\mbox{deriv of}}{* V \vdash * U} \quad
\stackrel{\texttt{sA}} \longrightarrow \quad
\stackrel {\mbox{deriv of}}{* * U \vdash V} 
$$


\end{slide}

\begin{slide} \setlength\parskip{0.8\parskip}
  \begin{heading}
    { Twelf -- Conclusions}
  \end{heading}

\begin{itemize}
\item typechecker good for building proofs
\item but no programmable proof search
\item theorem prover under extensive development,
workings not documented
\end{itemize}

\end{slide}

\begin{slide} \setlength\parskip{1.0\parskip}
  \begin{heading}
    { Isabelle/CTT implementation}
  \end{heading}

\begin{itemize}
\item Constructive Type Theory, has dependent types, similar to Twelf
\item Isabelle tactics can be used -- not all suitable
\item more tactics can be programmed -- ML programmability valuable
\end{itemize}

  
\begin{center}
Some type rules
\end{center}
\begin{verbatim}
strT  "str type"
seqT  "[| A : str ; B : str |] ==> A |- B type"
stT   "X : str ==> * X : str"
\end{verbatim}

\end{slide}

\begin{slide} \setlength\parskip{1.0\parskip}
  \begin{heading}
    { CTT -- Recording Proofs}
  \end{heading}

Record of proof comes automatically

\begin{verbatim}
goal dkt.thy "[| X : str ; Y : str |] ==>
  ?P : ( * * X |- Y) --> ( X |- * * Y)"
\end{verbatim}
Next step uses rule 
  $$ \frac {A \  \texttt{type} \qquad f : A \to B \qquad g : B \to C}
    {f \  \texttt{oo} \  g : A \to C} $$
\begin{verbatim}
?g oo ?f : * * X |- Y --> X |- * * Y
 1. * * X |- Y type
 2. ?f : * * X |- Y --> ?B
 3. ?g : ?B --> X |- * * Y
\end{verbatim}
Using \texttt{sA : * ?X |- ?Y --> * ?Y |- ?X \\ \indent
  sS : ?X |- * ?Y --> ?Y |- * ?X}
\begin{verbatim}
sS oo sA : * * X |- Y --> X |- * * Y
 1. * * X |- Y type
\end{verbatim}
\end{slide}

\begin{slide} \setlength\parskip{1.0\parskip}
  \begin{heading}
    { Dependent Types -- Conclusions}
  \end{heading}

\begin{itemize}
\item Attraction was to get derivations modelled for free
\item Term representing derivation 
\begin{itemize}
\item can be built up automatically
\item cannot freely place or manipulate it
\end{itemize}
\item  can't express arbitrary properties of derivation 
\item  need an even ``deeper'' embedding
\end{itemize}

\end{slide}

\begin{slide}
  \begin{heading}
    { The Isabelle/HOL implementation}
  \end{heading}
\begin{itemize}
\item based on Church's higher-order logic, has logical and functional language
constructs
\item deep embedding, we can look at the shape, content of sequents,
derivations \emph{in the logical framework} (not just by writing ML code)
\end{itemize}

\begin{verbatim} 
datatype structr = Comma structr structr
                 | SemiC structr structr
                 | Star structr
                 | Blob structr
                 ...
                 | Structform formula
                 | SV string
\end{verbatim} 

\begin{verbatim} 
datatype pftree = Pr sequent rule (pftree list)
                | Unf sequent
\end{verbatim} 


\end{slide}

\begin{slide}
Example -- given a proof tree, find the premises (unproved leaves)
\begin{verbatim} 
primrec
  "premsPT (Unf seq) = [seq]"
  "premsPT (Pr rule pts) = 
    premsPTl (premsRule rule) pts"

  "premsPTl prems [] = []"
  "premsPTl prems (pt # pts) =
    premsPT pt @ premsPTl (tl prems) pts"
\end{verbatim} 

Aim to mechanically verify Belnap's general
cut-elimination theorem for Display Logic --
have now done this, and a proof of
strong normalization of cut-elimination (later paper)

\end{slide}

\begin{slide}
  \begin{heading}
    { Deep vs Shallow Embeddings}
  \end{heading}

\begin{tabular}{p{7.0em}@{\qquad}p{9.0em}}
\begin{center}\textbf{\centering Shallow} \end{center}&
\begin{center}\textbf{\centering Deep}\end{center} \\
 & \\ 
we derive some sequent in \dRA &
we prove that a given sequent is derivable from
a given set of rules (those of \dRA) \\
 & \\ 
we write an ML function to convert a proof with cuts into a cut-free proof 
&
we mechanise the proof of the cut-elimination theorem \\
 & \\ 
Isabelle variable to represent any structure; Isabelle substitutes for these &
Isabelle term \texttt{SV ?str} represents structure variable; we define
substitution functions
\end{tabular}
\end{slide}

% SINGLE SLIDE ON CUT-ELIMINATION & STRONG NORMALIZATION WORK
\begin{slide} \setlength\parskip{0.6\parskip}
\begin{heading}
  { Outcomes of the Deep Embedding}
  \\ (slide omitted when detail of cut-elimination given)
\end{heading}
\begin{itemize}
\item Isabelle proof of cut-elimination theorem.
\item Attempted Isabelle proof of Strong Normalization of
  cut-elimination.
\item Discovered error in textbook proof. 
\item New proof of Strong Normalization -- \\
  successfully implemented in Isabelle!
\item Paper -- 35 pages + more needed.
\end{itemize}
\end{slide}

\newcommand\up[1]{\vspace{-#1ex}}
\newcommand\oall{\bigcirc_\forall}

% CUT-ELIMINATION & STRONG NORMALIZATION WORK
\begin{slide} \setlength\parskip{0.6\parskip}
\begin{heading}
  { Principal Cut} % -- before}
\end{heading}
\textbf{Defn} A cut is \emph{principal} if the 
cut-formula is introduced immediately above, on both sides.

\begin{center}
For example,

\bpf
\A "$\Pi_{ZAB}$"
\U "$Z \vdash A, B$"
\U "$Z \vdash A \lor B$" "($\vdash \lor $)"
\A "$\Pi_{AX}$"
\U "$A \vdash X$"
\A "$\Pi_{BY}$"
\U "$B \vdash Y$"
\B [1em] "$A \lor B \vdash X, Y$" "($\lor \vdash $)"
\B [2em] "$Z \vdash X, Y$" "($cut$)"
\epf

is transformed to
\end{center}
\end{slide}

\begin{slide} \setlength\parskip{0.6\parskip}
\begin{heading}
  { Principal Cut -- after}
\end{heading}
\begin{center}
\bpf
\A "$\Pi_{ZAB}$"
\U "$Z \vdash A, B$"
\U "$*A, Z \vdash B$" "($cs1$)"
\A "$\Pi_{BY}$"
\U "$B \vdash Y$"
\B [2em] "$*A, Z \vdash Y$" "($cut$)"
\U "$Z \vdash A, Y$" "($\overline{cs1}$)"
\U "$Z, *Y \vdash A$" "($cs2$)"
\A "$\Pi_{AX}$"
\U "$A \vdash X$"
\B [2em] "$Z, *Y \vdash X$" "($cut$)"
\U "$Z \vdash X, Y$" "($\overline{cs2}$)"
\epf
\end{center}
\end{slide}

\begin{slide}
\begin{heading}
  { Making a Cut Left-Principal}
\end{heading}

\begin{center}
\bpf
\A "$\Pi'$"
\U "$X' \vdash A $" "(intro-$A$)"
\U "$\Pi_L$" "($\pi$)"
\U "$X \vdash A $" "($\rho$)"
\A "$\Pi_R$"
\U "$A \vdash Y$"
\B [2em] "$X \vdash Y$" "($cut$)"
\epf

is transformed to

\bpf
\A "$\Pi'$"
\U "$X' \vdash A $" "(intro-$A$)"
\A "$\Pi_R$"
\U "$A \vdash Y$"
\B [2em] "$X' \vdash Y$" "($cut$)"
\U "$\Pi_L[A \,?\!= Y]$" "($\pi$)"
\U "$X \vdash Y $" "($\rho$)"
\epf
\end{center}

\end{slide}

\begin{slide}
\begin{heading}
  { How the proofs work}
\end{heading}
\begin{itemize}
\item Proof requires combining several inductive results.
\item Arbitrary cut $\leadsto$ Left-principal cut(s) \\
\texttt{canElimAll (cutIsLP ?A) ==> \\
  \mbox{\ \ \ }  canElim (cutOnFmls \{?A\})} 
\item Left-principal cut $\leadsto$ Principal cut(s) \\
\texttt{canElimAll (cutIsLRP ?A) ==> \\
  \mbox{\ \ \ }  canElim (cutIsLP ?A)} 
\item Principal cut $\leadsto$ Cuts on smaller cut-formulae \\
\texttt{canElimAll (cutOnFmls \{?A, ?B\}) ==> \\
  \mbox{\ \ \ }  canElim (cutIsLRP (?A v ?B))}
\item For simple proof -- always deal with topmost cut.
\end{itemize}
\end{slide}

\begin{slide}
\begin{heading}
  { Putting them together}
\end{heading}
Put the above together using the following
\begin{verbatim}
canElim (cutIsLRP ?A) ==>
    canElimAll (cutIsLRP ?A)
canElim (cutIsLP ?A) ==>
    canElimAll (cutIsLP ?A)
canElim (cutOnFmls ?s) ==>
    canElimAll (cutOnFmls ?s) 
\end{verbatim}
and then do induction on size of cut-formula.

Higher-order predicates and functions crucial, eg above, or \\[1ex]
\texttt{allPT :: "(pftree => bool) => pftree => bool"}  \\[1ex]
\texttt{allPT f tree} returns true if every subtree of \texttt{tree} satisfies 
the boolean valued function \texttt{f}
\end{slide}

\begin{slide}
\begin{heading}
  { Branch in left subtree}
\end{heading}
\begin{center}
\bpf
\A "$\Pi'$"
\U "$X' \vdash A $" "(intro-$A$)"
\A "$\Pi''$"
\U "$X'' \vdash A $" "(intro-$A$)"
\B [1em] "$\Pi_L$" "($\pi$)"
\U "$X \vdash A $" "($\rho$)"
\A "$\Pi_R$"
\U "$A \vdash Y$"
\B [0em] "$X \vdash Y$" "($cut$)"
\epf

is transformed to

\bpf
\A "$\Pi'$"
\U "$X' \vdash A $" % "(intro-$A$)"
\A "$\Pi_R$"
\U "$A \vdash Y$"
\B [1em] "$X' \vdash Y$" "($cut$)"
\A "$\Pi''$"
\U "$X'' \vdash A $" % "(intro-$A$)"
\A "$\Pi_R$"
\U "$A \vdash Y$"
\B [1em] "$X'' \vdash Y$" "($cut$)"
\B [1em] "$\Pi_L[A \,?\!= Y]$" "($\pi$)"
\U "$X \vdash Y $" "($\rho$)"
\epf
\end{center}
\end{slide}

\begin{slide}
\begin{heading}
  { Two successive introductions -- before}
\end{heading}

\begin{center}
\bpf
\A "$\Pi$"
\U "$X, B \vdash * B $" "($\rho$)"
\U "$X, B \vdash \lnot B $" "($\vdash \lnot$)"
\U "$*\lnot B, X \vdash *B $" "(dp)"
\U "$*\lnot B, X \vdash \lnot B $" "($\vdash \lnot$)"
\U "$X \vdash \lnot B, \lnot B $" "(dp)"
\U "$X \vdash \lnot B $" "($\vdash \mbox{cont}$)"
\A "$\Pi_R$"
\U "$\lnot B \vdash Y$"
\B [2em] "$X \vdash Y$" "($cut$)"
\epf
\end{center}
\end{slide}

\begin{slide}
\begin{heading}
  { Two successive introductions -- after}
\end{heading}
\begin{center}
\bpf
\A "$\Pi$"
\U "$X, B \vdash * B $" "($\rho$)"
\U "$X, B \vdash \lnot B $" "($\vdash \lnot$)"
\A "$\Pi_R$"
\U "$\lnot B \vdash Y$"
\B [2em] "$X, B \vdash Y $" "($cut$)"
\U "$*Y, X \vdash * B $" "(dp)"
\U "$*Y, X \vdash \lnot B $" "($\vdash \lnot$)"
\A "$\Pi_R$"
\U "$\lnot B \vdash Y$"
\B [0em] "$*Y, X \vdash Y $" "($cut$)"
\U "$X \vdash Y, Y $" "(dp)"
\U "$X \vdash Y $" "($\vdash \mbox{cont}$)"
\epf
\end{center}
\end{slide}

\begin{slide}
\begin{heading}
  { Strong normalization}
\end{heading}
\begin{itemize}
\item Alternatively, can perform a reduction step at any point in the tree.
\item Want to prove that this terminates.
\item Textbook proof wrong (assimilates two previous cases).
\item This discovered only in implementing proof in Isabelle!
\item Alternative proof found and performed in Isabelle
  (paper: 35 pages + more to come!).
\end{itemize}

\end{slide}
% APPLICATION IN FAIRTLOUGH / MENDLER PROJECT

% NOTE - FOLLOWING SLIDES USED IN SEPARATE TALK (TPHOLS 2002), 
% THIS FILE NOT UPDATED WITH ANY CHANGES
\begin{slide}
\begin{heading}
  { Use in Hardware Design / Verification}
\end{heading}
\begin{itemize}
  \item Work by Fairtlough \& Mendler
  \item Same idea used in Hardware Timing Constraints
  \item Construct proof around basic logic of gates -- $\land$, $\lor$, etc,
    plus Lax Logic $\bigcirc$
  \item Timing constraints recorded automatically
  \item $s \in P$ means $P$ true at time $s$
  \item $S \in \oall P$ means $P$ true at any time $s \in S$
\end{itemize}

\end{slide}

\begin{slide}
\begin{heading}
  { Lax Logic (Fairtlough \& Mendler)}
\end{heading}
As intuitionistic logic, with operator $\bigcirc$
\begin{description}
\item[] $\bigcirc R$ : $M \to \bigcirc M$ 
  % \qquad or \qquad \slrule M {\bigcirc M}
\item[] $\bigcirc M$ : $\bigcirc \bigcirc M \to \bigcirc M$
  % \qquad or \qquad \slrule {\bigcirc \bigcirc M} {\bigcirc M}
\item[] $\bigcirc F$ : $(M \to N) \to (\bigcirc M \to \bigcirc N)$ 
  % \quad or \quad \slrule {M \to N} {\bigcirc M \to \bigcirc N} 
  % \quad or \quad \slrule {M \to N \quad \bigcirc M} { \bigcirc N} 

\end{description}
Note similarity to types of monad functions

\end{slide}

\begin{slide}
\begin{heading}
  { Some rules as implemented }
\end{heading}
\begin{center}
\begin{tabular}{c@{\qquad}c@{\qquad}c}
Abstract & Concrete \\[3ex]
$\displaystyle \frac {P \quad Q} {P \land Q} (\land I)$ &
$\displaystyle \frac {p \in P \quad q \in Q} {(p, q) \in (P \sqcap Q)}
  (\sqcap I)$ 
 \\[3ex]

$\displaystyle \frac {P \to Q \quad P} {Q} (\to E)$ &
$\displaystyle \frac {f \in P \sqsupset Q \quad p \in P} 
  {f p \in Q} (\sqsupset E)$  
 \\[3ex]

$\displaystyle \frac {\forall y. P y} {P x} (\forall E)$ &
$\displaystyle \frac {f \in \sqcap y. P y} {f x \in P x}$  
 \\[3ex]

$\displaystyle \frac {\oall (\oall P) } {\oall P} (\oall M)$ &
$\displaystyle \frac {S \in \oall (\oall P) }
  {\bigcup S \in \bigcirc_\forall P}$ 

\end{tabular}
\end{center}

\end{slide}

\begin{slide} \setlength\parskip{0.9\parskip}
\begin{heading}
  { Example (Fairtlough, Mendler \& Cheng) }
\end{heading}
% Original equations are
\begin{description}
\item[] $\psi_1 : \forall s. s \geq 5 \to s \in P_1 a$
\item[] $\psi_2 : \forall s y. s \geq 9y \to s \in P_2 (f y)$
\item[] $\psi_3 : \forall t s y_1 y_2. ( t \geq s + 35 \land
  s \in P_1 y_1 \land s \in P_2 y_2) \to t \in  Q (g (y_1, y_2))$
\end{description}

Rewrite them to 
\begin{description}
\item[] $\psi_1^{\sharp} : \{s \geq 5 \} \in \oall (P_1 a)$
\item[] $\psi_2^{\sharp} : \forall y. \{s \geq 9y \} \in \oall (P_2 (f y))$
\item[] $\psi_3^{\sharp} : \forall y_1 y_2 s_1 s_2.
  s_1 \in P_1 y_1 \land s_2 \in P_2 y_2 \to $ \\ $
  \{ t \,|\, s_1 = s_2 \land t >= s_1 + 35\} \in \oall (Q (g (y_1, y_2)))$
\end{description}

\end{slide}

\begin{slide} \setlength\parskip{1.0\parskip}
\begin{heading}
  { Proof of Lax Logic version }
\end{heading}
\begin{center}
\up{3}
\bpf
\A "$\psi_3$"
\U "$ \forall y_1 y_2.
  P_1 y_1 \land P_2 y_2 \to \oall (Q (g (y_1, y_2)))$"
% \U "$ \forall y_2. P_1 a \land P_2 y_2 \to \oall (Q (g (a, y_2)))$"
  % "($\forall E$)"
\U "$ P_1 a \land P_2 (f b) \to \oall (Q (g (a, f b)))$"
  "($\forall E, \forall E$)"
\U "$\vdots$"
\epf

\bpf
\A "$\vdots$"
\U ['] "$\vdots$"
\U ['] "$\vdots$"
\A "$\psi_1$"
\U "$\oall (P_1 a)$"
\A "$\psi_2$"
\U "$\forall y. \oall (P_2 (f y))$"
\U "$\oall (P_2 (f b))$" "($\forall E$)"
\B [2em] "$\oall (P_1 a \land P_2 (f b))$" "($\oall S$)"
\B [2em] "$\oall (Q (g (a, f b)))$" "($\oall E$)"
\U "$\exists v. \oall (Q v)$" "($\exists I$)"
\epf
\end{center}

\end{slide}

\begin{slide} \setlength\parskip{1.0\parskip}
Further rewrite equations from
\begin{description}
\item[] $\psi_1^{\sharp} : \{s \geq 5 \} \in \oall (P_1 a)$
\item[] $\psi_2^{\sharp} : \forall y. \{s \geq 9y \} \in \oall (P_2 (f y))$
\item[] $\psi_3^{\sharp} : \forall y_1 y_2 s_1 s_2.
  s_1 \in P_1 y_1 \land s_2 \in P_2 y_2 \to $ \\ $
  \{ t \,|\, s_1 = s_2 \land t >= s_1 + 35\} \in \oall (Q (g (y_1, y_2)))$
\end{description}
to
\begin{description}
\item[] $\psi_1^{\sharp} : \{s \geq 5 \} \in \oall (P_1 a)$
\item[] $\psi_2^{\sharp} :
  \lambda y. \{s \geq 9y \} \in \sqcap y. \oall (P_2 (f y))$
\item[] $\psi_3^{\sharp} : \lambda y_1 y_2.
  \lambda (s_1, s_2). \{ t \,|\, s_1 = s_2 \land t \geq s_1 + 35 \}
  \in \sqcap y_1 y_2.
  P_1 y_1 \land P_2 y_2 \to \oall (Q (g (y_1, y_2)))$
\end{description}

\end{slide}
\begin{slide} \setlength\parskip{1.0\parskip}
\begin{heading}
  { Proof in Isabelle }
\end{heading}

\begin{verbatim}

goal Tiny_thy "?p : (SUM v. Oall(Q v))"

Level 2 (2 subgoals)
[?x1;Union (?r8 ` ?a2)] :
   SUM v. (Oall (Q v))
 1. ?r8 : (?P8 ---> Oall (Q ?x1))
 2. ?a2 : Oall ?P8

Level 4 (2 subgoals)
[g (?y10, ?y9);
 Union (((%y1 y2 (z1, z2).
   {t. z1 = z2 & z1 + #35 <= t}) `` ?y10 `` ?y9) `
   (?p11 <*> ?q11))]
: SUM v. (Oall (Q v))
 1. ?p11 : Oall (P1 ?y10)
 2. ?q11 : Oall (P2 ?y9)

\end{verbatim}

\end{slide}

\begin{slide} \setlength\parskip{1.0\parskip}

\begin{verbatim}
Level 6
[g (a, f ?y12);
 Union (((%y1 y2 (z1, z2).
   {t. z1 = z2 & z1 + #35 <= t}) `` a `` f ?y12) `
   (Collect (op <= #5) <*>
     ((%y. Collect (op <= (#9 * y))) `` ?y12)))]
: SUM v. (Oall (Q v))
No subgoals!

\end{verbatim}

The above uses

\begin{verbatim}
p3 = "(%y1 y2 (z1, z2).
   {t. z1 = z2 & z1 + #35 <= t})
 : PROD y1 y2. (P1 y1 && P2 y2 --->
   Oall (Q (g (y1, y2))))"

p3 RS Prodd_Ep p3 RS Prodd_Ep =
"(%y1 y2 (z1, z2).
   {t. z1 = z2 & z1 + #35 <= t}) `` ?y1 `` ?y
 : (P1 ?y1 && P2 ?y ---> Oall (Q (g (?y1, ?y))))"
\end{verbatim}

\end{slide}
\end{document}
