--- a/Nominal/Abs.thy Mon Jun 07 11:46:26 2010 +0200
+++ b/Nominal/Abs.thy Wed Jun 09 15:14:16 2010 +0200
@@ -88,22 +88,17 @@
and b: "p \<bullet> R = R"
shows "(bs, x) \<approx>gen R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>gen R f (- p) (bs, x)"
and "(bs, x) \<approx>res R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>res R f (- p) (bs, x)"
- and "(ds, x) \<approx>lst R f p (es, y) \<Longrightarrow> (es, y) \<approx>lst R f (- p) (ds, x)"
-proof -
- { assume "R (p \<bullet> x) y"
- then have "R y (p \<bullet> x)" using a by simp
- then have "R (- p \<bullet> y) x"
- apply(rule_tac p="p" in permute_boolE)
- apply(perm_simp add: permute_minus_cancel b)
- apply(assumption)
- done
- }
- then show "(bs, x) \<approx>gen R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>gen R f (- p) (bs, x)"
- and "(bs, x) \<approx>res R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>res R f (- p) (bs, x)"
- and "(ds, x) \<approx>lst R f p (es, y) \<Longrightarrow> (es, y) \<approx>lst R f (- p) (ds, x)"
- unfolding alphas fresh_star_def
- by (auto simp add: fresh_minus_perm)
-qed
+ and "(ds, x) \<approx>lst R f p (es, y) \<Longrightarrow> (es, y) \<approx>lst R f (- p) (ds, x)"
+apply(auto intro!: alpha_gen_sym)
+apply(drule_tac [!] a)
+apply(rule_tac [!] p="p" in permute_boolE)
+apply(perm_simp add: permute_minus_cancel b)
+apply(assumption)
+apply(perm_simp add: permute_minus_cancel b)
+apply(assumption)
+apply(perm_simp add: permute_minus_cancel b)
+apply(assumption)
+done
lemma alpha_gen_trans:
assumes a: "\<lbrakk>R (p \<bullet> x) y; R (q \<bullet> y) z\<rbrakk> \<Longrightarrow> R ((q + p) \<bullet> x) z"
@@ -115,6 +110,74 @@
by (simp_all add: fresh_plus_perm)
+lemma alpha_gen_trans_eqvt:
+ assumes b: "(cs, y) \<approx>gen R f q (ds, z)"
+ and a: "(bs, x) \<approx>gen R f p (cs, y)"
+ and d: "q \<bullet> R = R"
+ and c: "\<lbrakk>R (p \<bullet> x) y; R y (- q \<bullet> z)\<rbrakk> \<Longrightarrow> R (p \<bullet> x) (- q \<bullet> z)"
+ shows "(bs, x) \<approx>gen R f (q + p) (ds, z)"
+apply(rule alpha_gen_trans)
+defer
+apply(rule a)
+apply(rule b)
+apply(drule c)
+apply(rule_tac p="q" in permute_boolE)
+apply(perm_simp add: permute_minus_cancel d)
+apply(assumption)
+apply(rotate_tac -1)
+apply(drule_tac p="q" in permute_boolI)
+apply(perm_simp add: permute_minus_cancel d)
+apply(simp add: permute_eqvt[symmetric])
+done
+
+lemma alpha_res_trans_eqvt:
+ assumes b: "(cs, y) \<approx>res R f q (ds, z)"
+ and a: "(bs, x) \<approx>res R f p (cs, y)"
+ and d: "q \<bullet> R = R"
+ and c: "\<lbrakk>R (p \<bullet> x) y; R y (- q \<bullet> z)\<rbrakk> \<Longrightarrow> R (p \<bullet> x) (- q \<bullet> z)"
+ shows "(bs, x) \<approx>res R f (q + p) (ds, z)"
+apply(rule alpha_gen_trans)
+defer
+apply(rule a)
+apply(rule b)
+apply(drule c)
+apply(rule_tac p="q" in permute_boolE)
+apply(perm_simp add: permute_minus_cancel d)
+apply(assumption)
+apply(rotate_tac -1)
+apply(drule_tac p="q" in permute_boolI)
+apply(perm_simp add: permute_minus_cancel d)
+apply(simp add: permute_eqvt[symmetric])
+done
+
+lemma alpha_lst_trans_eqvt:
+ assumes b: "(cs, y) \<approx>lst R f q (ds, z)"
+ and a: "(bs, x) \<approx>lst R f p (cs, y)"
+ and d: "q \<bullet> R = R"
+ and c: "\<lbrakk>R (p \<bullet> x) y; R y (- q \<bullet> z)\<rbrakk> \<Longrightarrow> R (p \<bullet> x) (- q \<bullet> z)"
+ shows "(bs, x) \<approx>lst R f (q + p) (ds, z)"
+apply(rule alpha_gen_trans)
+defer
+apply(rule a)
+apply(rule b)
+apply(drule c)
+apply(rule_tac p="q" in permute_boolE)
+apply(perm_simp add: permute_minus_cancel d)
+apply(assumption)
+apply(rotate_tac -1)
+apply(drule_tac p="q" in permute_boolI)
+apply(perm_simp add: permute_minus_cancel d)
+apply(simp add: permute_eqvt[symmetric])
+done
+
+lemmas alpha_trans_eqvt = alpha_gen_trans_eqvt alpha_res_trans_eqvt alpha_lst_trans_eqvt
+
+lemma test:
+ shows "(as, t) \<approx>gen R f pi (bs, s) \<Longrightarrow> R (pi \<bullet> t) s"
+ and "(as, t) \<approx>res R f pi (bs, s) \<Longrightarrow> R (pi \<bullet> t) s"
+ and "(cs, t) \<approx>lst R f pi (ds, s) \<Longrightarrow> R (pi \<bullet> t) s"
+ by (simp_all add: alphas)
+
section {* General Abstractions *}
--- a/Slides/Slides1.thy Mon Jun 07 11:46:26 2010 +0200
+++ b/Slides/Slides1.thy Wed Jun 09 15:14:16 2010 +0200
@@ -18,9 +18,9 @@
\frametitle{%
\begin{tabular}{@ {\hspace{-3mm}}c@ {}}
\\
- \huge Nominal 2\\[-2mm]
- \large Or, How to Reason Conveniently with\\[-5mm]
- \large General Bindings in Isabelle/HOL\\[5mm]
+ \huge Nominal Isabelle 2\\[-2mm]
+ \large Or, How to Reason Conveniently\\[-5mm]
+ \large with General Bindings\\[5mm]
\end{tabular}}
\begin{center}
Christian Urban
@@ -182,7 +182,7 @@
\item the order does not matter, but the cardinality of the binders
must be the same \textcolor{gray}{(abstraction)}\medskip
- \item the order does matter
+ \item the order does matter \textcolor{gray}{(iterated single binders)}
\end{itemize}
\onslide<2->{
@@ -266,18 +266,19 @@
\begin{itemize}
\item we allow multiple ``binders'' and ``bodies''\smallskip
\begin{center}
- \isacommand{bind} a b c \isacommand{in} x y z
+ \begin{tabular}{l}
+ \isacommand{bind} a b c \ldots \isacommand{in} x y z \ldots\\
+ \isacommand{bind\_set} a b c \ldots \isacommand{in} x y z \ldots\\
+ \isacommand{bind\_res} a b c \ldots \isacommand{in} x y z \ldots
+ \end{tabular}
\end{center}\bigskip\medskip
- the reason is that with our definitions of $\alpha$-equivalence
+ the reason is that with our definition of $\alpha$-equivalence\medskip
\begin{center}
- \begin{tabular}{rcl}
- \isacommand{bind\_res} as \isacommand{in} x y & $\not\Leftrightarrow$ &
- \begin{tabular}{@ {}l}
- \isacommand{bind\_res} as \isacommand{in} x,\\
- \isacommand{bind\_res} as \isacommand{in} y
+ \begin{tabular}{l}
+ \isacommand{bind\_res} as \isacommand{in} x y $\not\Leftrightarrow$\\
+ \hspace{8mm}\isacommand{bind\_res} as \isacommand{in} x, \isacommand{bind\_res} as \isacommand{in} y
\end{tabular}
- \end{tabular}
- \end{center}\smallskip
+ \end{center}\medskip
same with \isacommand{bind\_set}
\end{itemize}}
@@ -324,48 +325,33 @@
\begin{center}
\begin{tikzpicture}
- \alt<2>
- {\draw (0,0) node[inner sep=3mm, ultra thick, draw=red, rounded corners=2mm]
- (A) {\textcolor{red}{\begin{minipage}{1.1cm}bind.\\spec.\end{minipage}}};}
- {\draw (0,0) node[inner sep=3mm, ultra thick, draw=white, rounded corners=2mm]
+ {\draw (0,0) node[inner sep=3mm, ultra thick, draw=fg, rounded corners=2mm]
(A) {\begin{minipage}{1.1cm}bind.\\spec.\end{minipage}};}
- \alt<3>
- {\draw (3,0) node[inner sep=3mm, ultra thick, draw=red, rounded corners=2mm]
- (B) {\textcolor{red}{\begin{minipage}{1.1cm}raw\\terms\end{minipage}}};}
- {\draw (3,0) node[inner sep=3mm, ultra thick, draw=white, rounded corners=2mm]
+ {\draw (3,0) node[inner sep=3mm, ultra thick, draw=fg, rounded corners=2mm]
(B) {\begin{minipage}{1.1cm}raw\\terms\end{minipage}};}
- \alt<4>
+ \alt<2>
{\draw (6,0) node[inner sep=3mm, ultra thick, draw=red, rounded corners=2mm]
(C) {\textcolor{red}{\begin{minipage}{1.1cm}$\alpha$-\\equiv.\end{minipage}}};}
- {\draw (6,0) node[inner sep=3mm, ultra thick, draw=white, rounded corners=2mm]
+ {\draw (6,0) node[inner sep=3mm, ultra thick, draw=fg, rounded corners=2mm]
(C) {\begin{minipage}{1.1cm}$\alpha$-\\equiv.\end{minipage}};}
- \alt<5>
- {\draw (0,-3) node[inner sep=3mm, ultra thick, draw=red, rounded corners=2mm]
- (D) {\textcolor{red}{\begin{minipage}{1.1cm}quot.\\type\end{minipage}}};}
- {\draw (0,-3) node[inner sep=3mm, ultra thick, draw=white, rounded corners=2mm]
+ {\draw (0,-3) node[inner sep=3mm, ultra thick, draw=fg, rounded corners=2mm]
(D) {\begin{minipage}{1.1cm}quot.\\type\end{minipage}};}
- \alt<6>
- {\draw (3,-3) node[inner sep=3mm, ultra thick, draw=red, rounded corners=2mm]
- (E) {\textcolor{red}{\begin{minipage}{1.1cm}lift\\thms\end{minipage}}};}
- {\draw (3,-3) node[inner sep=3mm, ultra thick, draw=white, rounded corners=2mm]
+ {\draw (3,-3) node[inner sep=3mm, ultra thick, draw=fg, rounded corners=2mm]
(E) {\begin{minipage}{1.1cm}lift\\thms\end{minipage}};}
- \alt<7>
- {\draw (6,-3) node[inner sep=3mm, ultra thick, draw=red, rounded corners=2mm]
- (F) {\textcolor{red}{\begin{minipage}{1.1cm}add.\\thms\end{minipage}}};}
- {\draw (6,-3) node[inner sep=3mm, ultra thick, draw=white, rounded corners=2mm]
+ {\draw (6,-3) node[inner sep=3mm, ultra thick, draw=fg, rounded corners=2mm]
(F) {\begin{minipage}{1.1cm}add.\\thms\end{minipage}};}
- \draw[->,white!50,line width=1mm] (A) -- (B);
- \draw[->,white!50,line width=1mm] (B) -- (C);
- \draw[->,white!50,line width=1mm, line join=round, rounded corners=2mm]
+ \draw[->,fg!50,line width=1mm] (A) -- (B);
+ \draw[->,fg!50,line width=1mm] (B) -- (C);
+ \draw[->,fg!50,line width=1mm, line join=round, rounded corners=2mm]
(C) -- (8,0) -- (8,-1.5) -- (-2,-1.5) -- (-2,-3) -- (D);
- \draw[->,white!50,line width=1mm] (D) -- (E);
- \draw[->,white!50,line width=1mm] (E) -- (F);
+ \draw[->,fg!50,line width=1mm] (D) -- (E);
+ \draw[->,fg!50,line width=1mm] (E) -- (F);
\end{tikzpicture}
\end{center}
@@ -378,7 +364,7 @@
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
- \begin{frame}<1-9>
+ \begin{frame}<1-8>
\frametitle{\begin{tabular}{c}Alpha-Equivalence\end{tabular}}
\mbox{}\\[-3mm]
@@ -386,9 +372,9 @@
\item lets first look at pairs\bigskip\medskip
\begin{tabular}{@ {\hspace{1cm}}l}
- $(as, x) \onslide<2->{\approx\!}\makebox[0mm][l]{\only<2-7>{${}_{\text{set}}$}%
- \only<8>{${}_{\text{\alert{list}}}$}%
- \only<9>{${}_{\text{\alert{res}}}$}}%
+ $(as, x) \onslide<2->{\approx\!}\makebox[0mm][l]{\only<2-6>{${}_{\text{set}}$}%
+ \only<7>{${}_{\text{\alert{list}}}$}%
+ \only<8>{${}_{\text{\alert{res}}}$}}%
\onslide<3->{^{R,\text{fv}}}\,\onslide<2->{(bs,y)}$
\end{tabular}\bigskip
\end{itemize}
@@ -397,7 +383,7 @@
\begin{textblock}{8}(3,8.5)
\begin{tabular}{l@ {\hspace{2mm}}p{8cm}}
\pgfuseshading{smallspherered} & $as$ is a set of names\ldots the binders\\
- \pgfuseshading{smallspherered} & $x$ is the body\\
+ \pgfuseshading{smallspherered} & $x$ is the body (might be a tuple)\\
\pgfuseshading{smallspherered} & $\approx_{\text{set}}$ is where the cardinality
of the binders has to be the same\\
\end{tabular}
@@ -408,13 +394,13 @@
\begin{tabular}{ll@ {\hspace{1mm}}l}
$\dn$ & \onslide<5->{$\exists \pi.\,$} & $\text{fv}(x) - as = \text{fv}(y) - bs$\\[1mm]
& \onslide<5->{$\;\;\;\wedge$} & \onslide<5->{$\text{fv}(x) - as \fresh^* \pi$}\\[1mm]
- & \onslide<6->{$\;\;\;\wedge$} & \onslide<6->{$(\pi \act x)\;R\;y$}\\[1mm]
- & \onslide<7-8>{$\;\;\;\wedge$} & \onslide<7-8>{$\pi \act as = bs$}\\
+ & \onslide<5->{$\;\;\;\wedge$} & \onslide<5->{$(\pi \act x)\;R\;y$}\\[1mm]
+ & \onslide<6-7>{$\;\;\;\wedge$} & \onslide<6-7>{$\pi \act as = bs$}\\
\end{tabular}
\end{textblock}}
- \only<8>{
- \begin{textblock}{8}(3,13.8)
+ \only<7>{
+ \begin{textblock}{7}(3,13.8)
\footnotesize $^*$ $as$ and $bs$ are \alert{lists} of names
\end{textblock}}
\end{frame}}
@@ -965,30 +951,30 @@
\footnotesize
\begin{center}
\begin{tikzpicture}
- \draw (0,0) node[inner sep=2mm, ultra thick, draw=white, rounded corners=2mm]
+ \draw (0,0) node[inner sep=2mm, ultra thick, draw=fg, rounded corners=2mm]
(A) {\begin{minipage}{0.8cm}bind.\\spec.\end{minipage}};
- \draw (2,0) node[inner sep=2mm, ultra thick, draw=white, rounded corners=2mm]
+ \draw (2,0) node[inner sep=2mm, ultra thick, draw=fg, rounded corners=2mm]
(B) {\begin{minipage}{0.8cm}raw\\terms\end{minipage}};
- \draw (4,0) node[inner sep=2mm, ultra thick, draw=white, rounded corners=2mm]
+ \draw (4,0) node[inner sep=2mm, ultra thick, draw=fg, rounded corners=2mm]
(C) {\begin{minipage}{0.8cm}$\alpha$-\\equiv.\end{minipage}};
- \draw (0,-2) node[inner sep=2mm, ultra thick, draw=white, rounded corners=2mm]
+ \draw (0,-2) node[inner sep=2mm, ultra thick, draw=fg, rounded corners=2mm]
(D) {\begin{minipage}{0.8cm}quot.\\type\end{minipage}};
- \draw (2,-2) node[inner sep=2mm, ultra thick, draw=white, rounded corners=2mm]
+ \draw (2,-2) node[inner sep=2mm, ultra thick, draw=fg, rounded corners=2mm]
(E) {\begin{minipage}{0.8cm}lift\\thms\end{minipage}};
- \draw (4,-2) node[inner sep=2mm, ultra thick, draw=white, rounded corners=2mm]
+ \draw (4,-2) node[inner sep=2mm, ultra thick, draw=fg, rounded corners=2mm]
(F) {\begin{minipage}{0.8cm}add.\\thms\end{minipage}};
- \draw[->,white!50,line width=1mm] (A) -- (B);
- \draw[->,white!50,line width=1mm] (B) -- (C);
- \draw[->,white!50,line width=1mm, line join=round, rounded corners=2mm]
+ \draw[->,fg!50,line width=1mm] (A) -- (B);
+ \draw[->,fg!50,line width=1mm] (B) -- (C);
+ \draw[->,fg!50,line width=1mm, line join=round, rounded corners=2mm]
(C) -- (5,0) -- (5,-1) -- (-1,-1) -- (-1,-2) -- (D);
- \draw[->,white!50,line width=1mm] (D) -- (E);
- \draw[->,white!50,line width=1mm] (E) -- (F);
+ \draw[->,fg!50,line width=1mm] (D) -- (E);
+ \draw[->,fg!50,line width=1mm] (E) -- (F);
\end{tikzpicture}
\end{center}
@@ -1012,7 +998,7 @@
\mbox{}\\[-6mm]
\small
- \mbox{}\hspace{10mm}
+ \mbox{}\hspace{20mm}
\begin{tabular}{ll}
\multicolumn{2}{l}{\isacommand{nominal\_datatype} trm $=$}\\
\hspace{5mm}\phantom{$|$} Var name\\
@@ -1031,6 +1017,15 @@
we cannot quotient assn: ACons a \ldots $\not\approx_\alpha$ ACons b \ldots
+ \only<1->{
+ \begin{textblock}{8}(0.2,7.3)
+ \alert{\begin{tabular}{p{2.6cm}}
+ \raggedright\footnotesize{}Should a ``naked'' assn be quotient?
+ \end{tabular}\hspace{-3mm}
+ $\begin{cases}
+ \mbox{} \\ \mbox{}
+ \end{cases}$}
+ \end{textblock}}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
@@ -1075,6 +1070,34 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}<1-2>[c]
+ \frametitle{\begin{tabular}{c}Examples\end{tabular}}
+ \mbox{}\\[-6mm]
+
+ \begin{center}
+ $(\{a,b\}, a \rightarrow b) \approx_\alpha (\{a, b\}, a \rightarrow b)$
+ $(\{a,b\}, a \rightarrow b) \approx_\alpha (\{a, b\}, b \rightarrow a)$
+ \end{center}
+
+ \begin{center}
+ $(\{a,b\}, (a \rightarrow b, a \rightarrow b))$\\
+ \hspace{17mm}$\not\approx_\alpha (\{a, b\}, (a \rightarrow b, b \rightarrow a))$
+ \end{center}
+
+ \onslide<2->
+ {1.) \hspace{3mm}\isacommand{bind\_set} as \isacommand{in} $\tau_1$,
+ \isacommand{bind\_set} as \isacommand{in} $\tau_2$\medskip
+
+ 2.) \hspace{3mm}\isacommand{bind\_set} as \isacommand{in} $\tau_1$ $\tau_2$
+ }
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
(*<*)
end
(*>*)
\ No newline at end of file