|
1 \documentclass[dvipsnames,14pt,t]{beamer} |
|
2 \usepackage{proof} |
|
3 \usepackage{beamerthemeplainculight} |
|
4 \usepackage[T1]{fontenc} |
|
5 \usepackage[latin1]{inputenc} |
|
6 \usepackage{mathpartir} |
|
7 \usepackage{isabelle} |
|
8 \usepackage{isabellesym} |
|
9 \usepackage[absolute,overlay]{textpos} |
|
10 \usepackage{ifthen} |
|
11 \usepackage{tikz} |
|
12 \usepackage{courier} |
|
13 \usepackage{listings} |
|
14 \usetikzlibrary{arrows} |
|
15 \usetikzlibrary{positioning} |
|
16 \usetikzlibrary{calc} |
|
17 \usepackage{graphicx} |
|
18 \usetikzlibrary{shapes} |
|
19 \usetikzlibrary{shadows} |
|
20 \usetikzlibrary{plotmarks} |
|
21 |
|
22 |
|
23 \isabellestyle{rm} |
|
24 \renewcommand{\isastyle}{\rm}% |
|
25 \renewcommand{\isastyleminor}{\rm}% |
|
26 \renewcommand{\isastylescript}{\footnotesize\rm\slshape}% |
|
27 \renewcommand{\isatagproof}{} |
|
28 \renewcommand{\endisatagproof}{} |
|
29 \renewcommand{\isamarkupcmt}[1]{#1} |
|
30 |
|
31 % Isabelle characters |
|
32 \renewcommand{\isacharunderscore}{\_} |
|
33 \renewcommand{\isacharbar}{\isamath{\mid}} |
|
34 \renewcommand{\isasymiota}{} |
|
35 \renewcommand{\isacharbraceleft}{\{} |
|
36 \renewcommand{\isacharbraceright}{\}} |
|
37 \renewcommand{\isacharless}{$\langle$} |
|
38 \renewcommand{\isachargreater}{$\rangle$} |
|
39 \renewcommand{\isasymsharp}{\isamath{\#}} |
|
40 \renewcommand{\isasymdots}{\isamath{...}} |
|
41 \renewcommand{\isasymbullet}{\act} |
|
42 |
|
43 |
|
44 |
|
45 \definecolor{javared}{rgb}{0.6,0,0} % for strings |
|
46 \definecolor{javagreen}{rgb}{0.25,0.5,0.35} % comments |
|
47 \definecolor{javapurple}{rgb}{0.5,0,0.35} % keywords |
|
48 \definecolor{javadocblue}{rgb}{0.25,0.35,0.75} % javadoc |
|
49 |
|
50 \lstset{language=Java, |
|
51 basicstyle=\ttfamily, |
|
52 keywordstyle=\color{javapurple}\bfseries, |
|
53 stringstyle=\color{javagreen}, |
|
54 commentstyle=\color{javagreen}, |
|
55 morecomment=[s][\color{javadocblue}]{/**}{*/}, |
|
56 numbers=left, |
|
57 numberstyle=\tiny\color{black}, |
|
58 stepnumber=1, |
|
59 numbersep=10pt, |
|
60 tabsize=2, |
|
61 showspaces=false, |
|
62 showstringspaces=false} |
|
63 |
|
64 \lstdefinelanguage{scala}{ |
|
65 morekeywords={abstract,case,catch,class,def,% |
|
66 do,else,extends,false,final,finally,% |
|
67 for,if,implicit,import,match,mixin,% |
|
68 new,null,object,override,package,% |
|
69 private,protected,requires,return,sealed,% |
|
70 super,this,throw,trait,true,try,% |
|
71 type,val,var,while,with,yield}, |
|
72 otherkeywords={=>,<-,<\%,<:,>:,\#,@}, |
|
73 sensitive=true, |
|
74 morecomment=[l]{//}, |
|
75 morecomment=[n]{/*}{*/}, |
|
76 morestring=[b]", |
|
77 morestring=[b]', |
|
78 morestring=[b]""" |
|
79 } |
|
80 |
|
81 \lstset{language=Scala, |
|
82 basicstyle=\ttfamily, |
|
83 keywordstyle=\color{javapurple}\bfseries, |
|
84 stringstyle=\color{javagreen}, |
|
85 commentstyle=\color{javagreen}, |
|
86 morecomment=[s][\color{javadocblue}]{/**}{*/}, |
|
87 numbers=left, |
|
88 numberstyle=\tiny\color{black}, |
|
89 stepnumber=1, |
|
90 numbersep=10pt, |
|
91 tabsize=2, |
|
92 showspaces=false, |
|
93 showstringspaces=false} |
|
94 |
|
95 % beamer stuff |
|
96 \renewcommand{\slidecaption}{APP 09, King's College London, 27 November 2012} |
|
97 \newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}% for definitions |
|
98 \newcommand{\bl}[1]{\textcolor{blue}{#1}} |
|
99 |
|
100 \begin{document} |
|
101 |
|
102 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
103 \mode<presentation>{ |
|
104 \begin{frame}<1>[t] |
|
105 \frametitle{% |
|
106 \begin{tabular}{@ {}c@ {}} |
|
107 \\ |
|
108 \LARGE Access Control and \\[-3mm] |
|
109 \LARGE Privacy Policies (10)\\[-6mm] |
|
110 \end{tabular}}\bigskip\bigskip\bigskip |
|
111 |
|
112 %\begin{center} |
|
113 %\includegraphics[scale=1.3]{pics/barrier.jpg} |
|
114 %\end{center} |
|
115 |
|
116 \normalsize |
|
117 \begin{center} |
|
118 \begin{tabular}{ll} |
|
119 Email: & christian.urban at kcl.ac.uk\\ |
|
120 Of$\!$fice: & S1.27 (1st floor Strand Building)\\ |
|
121 Slides: & KEATS (also homework is there)\\ |
|
122 \end{tabular} |
|
123 \end{center} |
|
124 |
|
125 \end{frame}} |
|
126 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
127 |
|
128 |
|
129 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
130 \mode<presentation>{ |
|
131 \begin{frame}[c] |
|
132 \frametitle{Revision: Proofs} |
|
133 |
|
134 \begin{center} |
|
135 \includegraphics[scale=0.4]{pics/river-stones.jpg} |
|
136 \end{center} |
|
137 |
|
138 \begin{textblock}{5}(11.7,5) |
|
139 goal |
|
140 \end{textblock} |
|
141 |
|
142 \begin{textblock}{5}(11.7,14) |
|
143 start |
|
144 \end{textblock} |
|
145 |
|
146 \begin{textblock}{5}(0,7) |
|
147 \begin{center} |
|
148 \bl{\infer[\small\textcolor{black}{\text{axiom}}]{\quad\vdash\quad}{}}\\[8mm] |
|
149 \bl{\infer{\vdash}{\quad\vdash\quad}}\\[8mm] |
|
150 \bl{\infer{\vdash}{\quad\vdash\qquad\vdash\quad}} |
|
151 \end{center} |
|
152 \end{textblock} |
|
153 |
|
154 \end{frame}} |
|
155 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
156 |
|
157 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
158 \mode<presentation>{ |
|
159 \begin{frame}[c] |
|
160 \frametitle{Proof Example Proof} |
|
161 |
|
162 \begin{center} |
|
163 \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} |
|
164 {\raisebox{2mm}{\text{\LARGE $?$}}}} |
|
165 \end{center} |
|
166 |
|
167 |
|
168 \end{frame}} |
|
169 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
170 |
|
171 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
172 \mode<presentation>{ |
|
173 \begin{frame}[c] |
|
174 \frametitle{Proof Example Proof} |
|
175 |
|
176 \begin{tabular}{@{\hspace{-6mm}}l} |
|
177 \begin{minipage}{1.1\textwidth} |
|
178 We have (by axiom) |
|
179 |
|
180 \begin{center} |
|
181 \begin{tabular}{@{}ll@{}} |
|
182 (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$} |
|
183 \end{tabular} |
|
184 \end{center} |
|
185 |
|
186 Fom (1) we get |
|
187 |
|
188 \begin{center} |
|
189 \begin{tabular}{@{}ll@{}} |
|
190 (2) & \bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash P\;\text{says}\;F_1$}\\ |
|
191 (3) & \bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash Q\;\text{says}\;F_2$}\\ |
|
192 \end{tabular} |
|
193 \end{center} |
|
194 |
|
195 Fom (3) and (2) we get |
|
196 |
|
197 \begin{center} |
|
198 \begin{tabular}{@{}ll@{}} |
|
199 \bl{$P\;\text{says}\;F_1 \wedge Q\;\text{says}\;F_2 \vdash Q\;\text{says}\;F_2 \wedge P\;\text{says}\;F_1$} |
|
200 \end{tabular} |
|
201 \end{center} |
|
202 |
|
203 Done. |
|
204 \end{minipage} |
|
205 \end{tabular} |
|
206 |
|
207 \end{frame}} |
|
208 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
209 |
|
210 |
|
211 \end{document} |
|
212 |
|
213 %%% Local Variables: |
|
214 %%% mode: latex |
|
215 %%% TeX-master: t |
|
216 %%% End: |
|
217 |