\documentclass[dvipsnames,14pt,t]{beamer}

\usepackage{proof}

\usepackage{beamerthemeplainculight}

\usepackage[T1]{fontenc}

\usepackage[latin1]{inputenc}

\usepackage{mathpartir}

\usepackage{isabelle}

\usepackage{isabellesym}

\usepackage[absolute,overlay]{textpos}

\usepackage{ifthen}

\usepackage{tikz}

\usepackage{courier}

\usepackage{listings}

\usetikzlibrary{arrows}

\usetikzlibrary{positioning}

\usetikzlibrary{calc}

\usepackage{graphicx} 

\usetikzlibrary{shapes}

\usetikzlibrary{shadows}

\usetikzlibrary{plotmarks}

\isabellestyle{rm}

\renewcommand{\isastyle}{\rm}%

\renewcommand{\isastyleminor}{\rm}%

\renewcommand{\isastylescript}{\footnotesize\rm\slshape}%

\renewcommand{\isatagproof}{}

\renewcommand{\endisatagproof}{}

\renewcommand{\isamarkupcmt}[1]{#1}

% Isabelle characters

\renewcommand{\isacharunderscore}{\_}

\renewcommand{\isacharbar}{\isamath{\mid}}

\renewcommand{\isasymiota}{}

\renewcommand{\isacharbraceleft}{\{}

\renewcommand{\isacharbraceright}{\}}

\renewcommand{\isacharless}{$\langle$}

\renewcommand{\isachargreater}{$\rangle$}

\renewcommand{\isasymsharp}{\isamath{\#}}

\renewcommand{\isasymdots}{\isamath{...}}

\renewcommand{\isasymbullet}{\act}

\definecolor{javared}{rgb}{0.6,0,0} % for strings

\definecolor{javagreen}{rgb}{0.25,0.5,0.35} % comments

\definecolor{javapurple}{rgb}{0.5,0,0.35} % keywords

\definecolor{javadocblue}{rgb}{0.25,0.35,0.75} % javadoc

\lstset{language=Java,

	basicstyle=\ttfamily,

	keywordstyle=\color{javapurple}\bfseries,

	stringstyle=\color{javagreen},

	commentstyle=\color{javagreen},

	morecomment=[s][\color{javadocblue}]{/**}{*/},

	numbers=left,

	numberstyle=\tiny\color{black},

	stepnumber=1,

	numbersep=10pt,

	tabsize=2,

	showspaces=false,

	showstringspaces=false}

\lstdefinelanguage{scala}{

  morekeywords={abstract,case,catch,class,def,%

    do,else,extends,false,final,finally,%

    for,if,implicit,import,match,mixin,%

    new,null,object,override,package,%

    private,protected,requires,return,sealed,%

    super,this,throw,trait,true,try,%

    type,val,var,while,with,yield},

  otherkeywords={=>,<-,<\%,<:,>:,\#,@},

  sensitive=true,

  morecomment=[l]{//},

  morecomment=[n]{/*}{*/},

  morestring=[b]",

  morestring=[b]',

  morestring=[b]"""

}

\lstset{language=Scala,

	basicstyle=\ttfamily,

	keywordstyle=\color{javapurple}\bfseries,

	stringstyle=\color{javagreen},

	commentstyle=\color{javagreen},

	morecomment=[s][\color{javadocblue}]{/**}{*/},

	numbers=left,

	numberstyle=\tiny\color{black},

	stepnumber=1,

	numbersep=10pt,

	tabsize=2,

	showspaces=false,

	showstringspaces=false}

% beamer stuff 

\renewcommand{\slidecaption}{APP 09, King's College London, 27 November 2012}

\newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}% for definitions

\newcommand{\bl}[1]{\textcolor{blue}{#1}}

\begin{document}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\mode<presentation>{

\begin{frame}<1>[t]

\frametitle{%

  \begin{tabular}{@ {}c@ {}}

  \\

  \LARGE Access Control and \\[-3mm] 

  \LARGE Privacy Policies (10)\\[-6mm] 

  \end{tabular}}\bigskip\bigskip\bigskip

  %\begin{center}

  %\includegraphics[scale=1.3]{pics/barrier.jpg}

  %\end{center}

\normalsize

  \begin{center}

  \begin{tabular}{ll}

  Email:  & christian.urban at kcl.ac.uk\\

  Of$\!$fice: & S1.27 (1st floor Strand Building)\\

  Slides: & KEATS (also homework is there)\\

  \end{tabular}

  \end{center}

\end{frame}}

 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\mode<presentation>{

\begin{frame}[c]

\frametitle{Revision: Proofs}

\begin{center}

\includegraphics[scale=0.4]{pics/river-stones.jpg}

\end{center}

\begin{textblock}{5}(11.7,5)

goal

\end{textblock}

\begin{textblock}{5}(11.7,14)

start

\end{textblock}

\begin{textblock}{5}(0,7)

\begin{center}

\bl{\infer[\small\textcolor{black}{\text{axiom}}]{\quad\vdash\quad}{}}\\[8mm]

\bl{\infer{\vdash}{\quad\vdash\quad}}\\[8mm]

\bl{\infer{\vdash}{\quad\vdash\qquad\vdash\quad}}

\end{center}

\end{textblock}

\end{frame}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\mode<presentation>{

\begin{frame}[c]

\frametitle{Proof Example Proof}

\begin{center}

\bl{\infer{P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash Q\;\text{says}\;F_2 \wedge P\;\text{says}\;F_1}

         {\raisebox{2mm}{\text{\LARGE $?$}}}}

\end{center}

\end{frame}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\mode<presentation>{

\begin{frame}[c]

\frametitle{Proof Example Proof}

\begin{tabular}{@{\hspace{-6mm}}l}

\begin{minipage}{1.1\textwidth}

We have (by axiom)

\begin{center}

\begin{tabular}{@{}ll@{}}

(1) & \bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2$}

\end{tabular}

\end{center}

From (1) we get

\begin{center}

\begin{tabular}{@{}ll@{}}

(2) & \bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash P\;\text{says}\;F_1$}\\

(3) & \bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash Q\;\text{says}\;F_2$}\\

\end{tabular}

\end{center}

From (3) and (2) we get

\begin{center}

\begin{tabular}{@{}ll@{}}

\bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash Q\;\text{says}\;F_2 \wedge P\;\text{says}\;F_1$}

\end{tabular}

\end{center}

Done.

\end{minipage}

\end{tabular}

\end{frame}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

\end{document}

%%% Local Variables:  

%%% mode: latex

%%% TeX-master: t

%%% End: