# HG changeset patch # User Christian Urban # Date 1275558524 -7200 # Node ID 13f20fe02ff36da67ab600c5de8439bc003d661e # Parent 387fcbd33820d3554f4c5f89604287576f0236fe fixed problem with eqvt proofs diff -r 387fcbd33820 -r 13f20fe02ff3 Nominal/Ex/CoreHaskell.thy --- a/Nominal/Ex/CoreHaskell.thy Wed Jun 02 11:37:51 2010 +0200 +++ b/Nominal/Ex/CoreHaskell.thy Thu Jun 03 11:48:44 2010 +0200 @@ -8,7 +8,7 @@ atom_decl cvar atom_decl tvar -declare [[STEPS = 4]] +declare [[STEPS = 9]] nominal_datatype tkind = KStar @@ -83,8 +83,7 @@ | "bv_tvs TvsNil = []" | "bv_tvs (TvsCons v k t) = (atom v) # bv_tvs t" | "bv_cvs CvsNil = []" -| "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t" - +| "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t" lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.supp(1-9,11,13,15) diff -r 387fcbd33820 -r 13f20fe02ff3 Nominal/Ex/Ex2.thy --- a/Nominal/Ex/Ex2.thy Wed Jun 02 11:37:51 2010 +0200 +++ b/Nominal/Ex/Ex2.thy Thu Jun 03 11:48:44 2010 +0200 @@ -3,7 +3,7 @@ begin text {* example 2 *} -declare [[STEPS = 8]] +declare [[STEPS = 9]] atom_decl name @@ -23,6 +23,7 @@ | "f (PD x y) = {atom x, atom y}" | "f (PS x) = {atom x}" + thm fv_trm_raw.simps[no_vars] fv_pat_raw.simps[no_vars] fv_f_raw.simps[no_vars] f_raw.simps[no_vars] thm alpha_trm_raw_alpha_pat_raw_alpha_f_raw.intros[no_vars] diff -r 387fcbd33820 -r 13f20fe02ff3 Nominal/NewParser.thy --- a/Nominal/NewParser.thy Wed Jun 02 11:37:51 2010 +0200 +++ b/Nominal/NewParser.thy Thu Jun 03 11:48:44 2010 +0200 @@ -399,7 +399,8 @@ val fv_eqvt = if get_STEPS lthy > 7 - then raw_prove_eqvt (raw_fvs @ raw_fv_bns) raw_fv_bns_induct (raw_fv_defs @ raw_perm_defs) lthy_tmp + then raw_prove_eqvt (raw_fvs @ raw_fv_bns) raw_fv_bns_induct (raw_fv_defs @ raw_perm_defs) + (Local_Theory.restore lthy_tmp) else raise TEST lthy4 val lthy_tmp' = snd (Local_Theory.note ((Binding.empty, [add_eqvt]), fv_eqvt) lthy_tmp) @@ -409,10 +410,6 @@ then Nominal_Eqvt.equivariance false alpha_trms alpha_induct alpha_intros lthy_tmp' else raise TEST lthy4 - val _ = tracing ("bn_eqvts\n" ^ cat_lines (map @{make_string} bn_eqvt)) - val _ = tracing ("fv_eqvts\n" ^ cat_lines (map @{make_string} fv_eqvt)) - val _ = tracing ("alpha_eqvts\n" ^ cat_lines (map @{make_string} alpha_eqvt)) - val _ = if get_STEPS lthy > 9 then true else raise TEST lthy4 diff -r 387fcbd33820 -r 13f20fe02ff3 Nominal/nominal_dt_rawfuns.ML --- a/Nominal/nominal_dt_rawfuns.ML Wed Jun 02 11:37:51 2010 +0200 +++ b/Nominal/nominal_dt_rawfuns.ML Thu Jun 03 11:48:44 2010 +0200 @@ -226,9 +226,6 @@ val all_fun_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names) val all_fun_eqs = map (pair Attrib.empty_binding) (flat fv_eqs @ flat fv_bn_eqs) - val _ = tracing ("eqs\n" ^ cat_lines (map (Syntax.string_of_term lthy) ((flat fv_eqs) @ (flat fv_bn_eqs)))) - - val (_, lthy') = Function.add_function all_fun_names all_fun_eqs Function_Common.default_config (pat_completeness_simp constr_thms) lthy @@ -257,6 +254,13 @@ HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) end +fun subproof_tac const_names simps ctxt = + Subgoal.FOCUS (fn {prems, context, ...} => + HEADGOAL + (simp_tac (HOL_basic_ss addsimps simps) + THEN' Nominal_Permeq.eqvt_tac context [] const_names + THEN' simp_tac (HOL_basic_ss addsimps (@{thms eqvt_apply[symmetric]} @ prems)))) ctxt + fun raw_prove_eqvt consts ind_thms simps ctxt = if null consts then [] else @@ -267,20 +271,18 @@ consts |> map fastype_of |> map domain_type - val (arg_names, ctxt'') = Variable.variant_fixes (replicate (length arg_tys) "") ctxt' + val (arg_names, ctxt'') = Variable.variant_fixes (Datatype_Prop.make_tnames arg_tys) ctxt' val args = map Free (arg_names ~~ arg_tys) val goals = map2 (mk_eqvt_goal p) consts args val insts = map (single o SOME) arg_names val const_names = map (fst o dest_Const) consts + fun tac ctxt = Object_Logic.full_atomize_tac - THEN' InductTacs.induct_rules_tac ctxt insts ind_thms - THEN_ALL_NEW - (asm_full_simp_tac (HOL_basic_ss addsimps simps) - THEN' Nominal_Permeq.eqvt_tac ctxt simps const_names - THEN' asm_simp_tac HOL_basic_ss) + THEN' (DETERM o (InductTacs.induct_rules_tac ctxt insts ind_thms)) + THEN_ALL_NEW subproof_tac const_names simps ctxt in - Goal.prove_multi ctxt' [] [] goals (fn {context, ...} => (HEADGOAL (tac context))) + Goal.prove_multi ctxt'' [] [] goals (fn {context, ...} => (HEADGOAL (tac context))) |> ProofContext.export ctxt'' ctxt end diff -r 387fcbd33820 -r 13f20fe02ff3 Slides/Slides1.thy --- a/Slides/Slides1.thy Wed Jun 02 11:37:51 2010 +0200 +++ b/Slides/Slides1.thy Thu Jun 03 11:48:44 2010 +0200 @@ -11,7 +11,7 @@ text_raw {* - \renewcommand{\slidecaption}{TU Munich, 28.~May 2010} + \renewcommand{\slidecaption}{Cambridge, 8.~June 2010} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \mode{ \begin{frame}<1>[t] @@ -20,10 +20,13 @@ \\ \huge Nominal 2\\[-2mm] \large Or, How to Reason Conveniently with\\[-5mm] - \large General Bindings in Isabelle\\[15mm] + \large General Bindings in Isabelle/HOL\\[5mm] \end{tabular}} \begin{center} - joint work with {\bf Cezary} and Brian Huf\!fman\\[0mm] + Christian Urban + \end{center} + \begin{center} + joint work with {\bf Cezary Kaliszyk}\\[0mm] \end{center} \end{frame}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -34,197 +37,7 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \mode{ \begin{frame}<1-2> - \frametitle{\begin{tabular}{c}Part I: Nominal Theory\end{tabular}} - \mbox{}\\[-3mm] - - \begin{itemize} - \item sorted atoms and sort-respecting permutations\medskip - - \onslide<2->{ - \item[] in old Nominal: atoms have \underline{dif\!ferent} type\medskip - - \begin{center} - \begin{tabular}{c@ {\hspace{7mm}}c} - $[]\;\act\;c \dn c$ & - $(a\;b)\!::\!\pi\;\act\;c \dn$ - $\begin{cases} - b & \text{if}\; \pi \act c = a\\ - a & \text{if}\; \pi \act c = b\\ - \pi \act c & \text{otherwise} - \end{cases}$ - \end{tabular} - \end{center}} - \end{itemize} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -*} - -text_raw {* - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}<1> - \frametitle{\begin{tabular}{c}Problems\end{tabular}} - \mbox{}\\[-3mm] - - \begin{itemize} - \item @{text "_ \ _ :: \ perm \ \ \ \"}\bigskip - - \item @{text "supp _ :: \ \ \ set"} - - \begin{center} - $\text{finite} (\text{supp}\;x)_{\,\alpha_1\,\text{set}}$ \ldots - $\text{finite} (\text{supp}\;x)_{\,\alpha_n\,\text{set}}$ - \end{center}\bigskip - - \item $\forall \pi_{\alpha_1} \ldots \pi_{\alpha_n}\;.\; P$\bigskip - - \item type-classes - \end{itemize} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -*} - -text_raw {* - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}<1-4> - \frametitle{\begin{tabular}{c}Our New Solution\end{tabular}} - \mbox{}\\[-3mm] -*} -datatype atom = Atom string nat - -text_raw {* - \mbox{}\bigskip - \begin{itemize} - \item<2-> permutations are (restricted) bijective functions from @{text "atom \ atom"} - - \begin{itemize} - \item sort-respecting \hspace{5mm}($\forall a.\;\text{sort}(f a) = \text{sort}(a)$) - \item finite domain \hspace{5mm}($\text{finite} \{a.\;f a \not= a\}$) - \end{itemize}\medskip - - \item<3-> swappings: - \small - \[ - \begin{array}{l@ {\hspace{1mm}}l} - (a\;b) \dn & \text{if}\;\text{sort}(a) = \text{sort}(b)\\ - & \text{then}\;\lambda c. \text{if}\;a = c\;\text{then}\;b\;\text{else}\; - \text{if}\;b = c\;\text{then}\;a\;\text{else}\;c\\ - & \text{else}\;\only<3>{\mbox{\textcolor{red}{\bf ?}}}\only<4->{\text{id}} - \end{array} - \] - \end{itemize} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -*} - -text_raw {* - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}<1-6> - \frametitle{\begin{tabular}{c}\LARGE{}A Smoother Nominal Theory\end{tabular}} - \mbox{}\\[-3mm] - - \begin{itemize} - \item<1-> $(a\;b) = (b\;a) \onslide<3->{= (a\;c) + (b\;c) + (a\;c)}$\bigskip - - \item<2-> permutations are an instance of group\_add\\ $0$, $\pi_1 + \pi_2$, $- \pi$\bigskip - - \item<5-> $\_\;\act\;\_ :: \text{perm} \Rightarrow \alpha \Rightarrow \alpha$\medskip - - \begin{itemize} - \item $0\;\act\;x = x$\\ - \item $(\pi_1 + \pi_2)\;\act\;x = \pi_1\;\act\;(\pi_2\;\act\;x)$ - \end{itemize} - - \small - \onslide<6->{$\text{finite}(\text{supp}\;x)$, $\forall \pi. P$} - \end{itemize} - - \only<4>{ - \begin{textblock}{6}(2.5,11) - \begin{tikzpicture} - \draw (0,0) node[inner sep=3mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] - {\normalsize\color{darkgray} - \begin{minipage}{8cm}\raggedright - This is slightly odd, since in general: - \begin{center}$\pi_1 + \pi_2 \alert{\not=} \pi_2 + \pi_1$\end{center} - \end{minipage}}; - \end{tikzpicture} - \end{textblock}} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -*} - -text_raw {* - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}<1-3> - \frametitle{\begin{tabular}{c}Very Few Snatches\end{tabular}} - \mbox{}\\[-3mm] - - \begin{itemize} - \item \underline{concrete} atoms: - \end{itemize} -*} -(*<*) -consts sort :: "atom \ string" -(*>*) - -typedef name = "{a :: atom. sort a = ''name''}" (*<*)sorry(*>*) -typedef ident = "{a :: atom. sort a = ''ident''}" (*<*)sorry(*>*) - -text_raw {* - \mbox{}\bigskip\bigskip - \begin{itemize} - \item<2-> there is an overloaded function \underline{atom}, which injects concrete - atoms into generic ones\medskip - \begin{center} - \begin{tabular}{l} - $\text{atom}(a) \fresh x$\\ - $(a \leftrightarrow b) \dn (\text{atom}(a)\;\;\text{atom}(b))$ - \end{tabular} - \end{center}\bigskip\medskip - - \onslide<3-> - {I would like to have $a \fresh x$, $(a\; b)$, \ldots} - - \end{itemize} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -*} - -text_raw {* - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}<1-2>[c] - \frametitle{\begin{tabular}{c}\LARGE{}End of Part I\end{tabular}} - \mbox{}\\[-3mm] - - \begin{itemize} - \item the formalised version of the nominal theory is now much nicer to - work with (sorts are occasionally explicit)\bigskip - - \item permutations: ``be as abstract as you can'' (group\_add is a slight oddity)\bigskip - - \item allow sort-disrespecting swappings\onslide<2->{: just define them as the identity} - \end{itemize} - - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -*} - -text_raw {* - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}<1-2> - \frametitle{\begin{tabular}{c}\LARGE{}Part II: General Bindings\end{tabular}} + \frametitle{\begin{tabular}{c}Binding in Old Nominal\end{tabular}} \mbox{}\\[-6mm] \begin{itemize} @@ -240,7 +53,8 @@ $\forall\{a_1,\ldots,a_n\}.\; T$ \end{center}\medskip - with single binders is a \alert{major} pain; take my word for it! + with single binders and reasoning about it is a \alert{\bf major} pain; + take my word for it! \end{itemize} \only<1>{ @@ -250,6 +64,7 @@ \begin{tabular}{l@ {\hspace{2mm}}l} \pgfuseshading{smallspherered} & a $\fresh$ Lam [a]. t\\ \pgfuseshading{smallspherered} & Lam [a]. (Var a) \alert{$=$} Lam [b]. (Var b)\\ + \pgfuseshading{smallspherered} & Barendregt style reasoning about bound variables\\ \end{tabular} \end{textblock}} @@ -362,10 +177,10 @@ \begin{itemize} \item the order does not matter and alpha-equivelence is preserved under - vacuous binders (restriction)\medskip + vacuous binders \textcolor{gray}{(restriction)}\medskip \item the order does not matter, but the cardinality of the binders - must be the same (abstraction)\medskip + must be the same \textcolor{gray}{(abstraction)}\medskip \item the order does matter \end{itemize} @@ -401,8 +216,8 @@ \multicolumn{2}{l}{\hspace{5mm}\phantom{$|$} ANil}\\ \multicolumn{2}{l}{\hspace{5mm}$|$ ACons name trm assn}\\ \multicolumn{2}{l}{\onslide<3->{\isacommand{binder} bn \isacommand{where}}}\\ - \multicolumn{2}{l}{\onslide<3->{\hspace{5mm}\phantom{$|$} bn(ANil) $=$ $\varnothing$}}\\ - \multicolumn{2}{l}{\onslide<3->{\hspace{5mm}$|$ bn(ACons a t as) $=$ $\{$a$\}$ $\cup$ bn(as)}}\\ + \multicolumn{2}{l}{\onslide<3->{\hspace{5mm}\phantom{$|$} bn(ANil) $=$ []}}\\ + \multicolumn{2}{l}{\onslide<3->{\hspace{5mm}$|$ bn(ACons a t as) $=$ [a] @ bn(as)}}\\ \end{tabular} @@ -414,33 +229,65 @@ text_raw {* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \mode{ - \begin{frame}<1-4> - \frametitle{\begin{tabular}{c}Ott\end{tabular}} + \begin{frame}<1-5> + \frametitle{\begin{tabular}{c}Inspiration from Ott\end{tabular}} \mbox{}\\[-3mm] \begin{itemize} - \item this way of specifying binding is pretty much stolen from - Ott\onslide<2->{, \alert{\bf but} with adjustments:}\medskip + \item this way of specifying binding is inspired by + Ott\onslide<2->{, \alert{\bf but} we made adjustments:}\medskip + + \only<2>{ \begin{itemize} - \item<2-> Ott allows specifications like\smallskip + \item Ott allows specifications like\smallskip \begin{center} $t ::= t\;t\; |\;\lambda x.t$ - \end{center}\medskip + \end{center} + \end{itemize}} - \item<3-> whether something is bound can depend on other bound things\smallskip + \only<3-4>{ + \begin{itemize} + \item whether something is bound can depend in Ott on other bound things\smallskip \begin{center} - Foo $(\lambda x. t)\; s$ - \end{center}\medskip - \onslide<4->{this might make sense for ``raw'' terms, but not at all + \begin{tikzpicture} + \node (A) at (-0.5,1) {Foo $(\lambda y. \lambda x. t)$}; + \node (B) at ( 1.1,1) {$s$}; + \onslide<4>{\node (C) at (0.5,0) {$\{y, x\}$};} + \onslide<4>{\draw[->,red,line width=1mm] (A) -- (C);} + \onslide<4>{\draw[->,red,line width=1mm] (C) -- (B);} + \end{tikzpicture} + \end{center} + \onslide<4>{this might make sense for ``raw'' terms, but not at all for $\alpha$-equated terms} - \end{itemize} + \end{itemize}} + + \only<5>{ + \begin{itemize} + \item we allow multiple binders and bodies\smallskip + \begin{center} + \isacommand{bind} a b c \isacommand{in} x y z + \end{center}\bigskip\medskip + the reason is that in general + \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 + \end{tabular} + \end{tabular} + \end{center}\smallskip + + same with \isacommand{bind\_set} + \end{itemize}} \end{itemize} \end{frame}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *} + text_raw {* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \mode{ @@ -449,13 +296,13 @@ \mbox{}\\[-3mm] \begin{itemize} - \item in old Nominal we represented single binders as partial functions:\bigskip + \item in old Nominal, we represented single binders as partial functions:\bigskip \begin{center} \begin{tabular}{l} - Lam [$a$].$t$ $\;\dn$\\[2mm] + Lam [$a$].\,$t$ $\;{^\text{``}}\!\dn{}\!^{\text{''}}$\\[2mm] \;\;\;\;$\lambda b.$\;$\text{if}\;a = b\;\text{then}\;t\;\text{else}$\\ - \phantom{\;\;\;\;$\lambda b.$\;\;\;}$\text{if}\;b \fresh t\; + \phantom{\;\;\;\;$\lambda b.$\;\;\;\;\;\;}$\text{if}\;b \fresh t\; \text{then}\;(a\;b)\act t\;\text{else}\;\text{error}$ \end{tabular} \end{center} @@ -471,6 +318,66 @@ text_raw {* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \mode{ + \begin{frame}<1-> + \frametitle{\begin{tabular}{c}New Design\end{tabular}} + \mbox{}\\[4mm] + + \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] + (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] + (B) {\begin{minipage}{1.1cm}raw\\terms\end{minipage}};} + + \alt<4> + {\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] + (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] + (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] + (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] + (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] + (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); + \end{tikzpicture} + \end{center} + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + + + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ \begin{frame}<1-9> \frametitle{\begin{tabular}{c}Alpha-Equivalence\end{tabular}} \mbox{}\\[-3mm] @@ -815,8 +722,6 @@ \multicolumn{2}{l}{\hspace{5mm}$|$ bn(ACons a t as) $=$ $[$a$]$ @ bn(as)}\\ \end{tabular} - - \end{frame}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *} @@ -896,7 +801,7 @@ \] \footnotesize - where $R =\;\approx_\alpha\times\approx_\alpha$ and $fv = \text{fv}\times\text{fv}$ + where $R =\;\approx_\alpha\times\approx_\alpha$ and $fv = \text{fv}\cup\text{fv}$ \end{frame}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -988,6 +893,83 @@ text_raw {* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \mode{ + \begin{frame}<1>[t] + \frametitle{\begin{tabular}{c}Runtime is Acceptable\end{tabular}} + \mbox{}\\[-7mm]\mbox{} + + \footnotesize + \begin{center} + \begin{tikzpicture} + \draw (0,0) node[inner sep=2mm, ultra thick, draw=white, 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] + (B) {\begin{minipage}{0.8cm}raw\\terms\end{minipage}}; + + \draw (4,0) node[inner sep=2mm, ultra thick, draw=white, 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] + (D) {\begin{minipage}{0.8cm}quot.\\type\end{minipage}}; + + \draw (2,-2) node[inner sep=2mm, ultra thick, draw=white, 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] + (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] + (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); + \end{tikzpicture} + \end{center} + + \begin{itemize} + \item Core Haskell: 11 types, 49 term-constructors, + \end{itemize} + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}<1-> + \frametitle{\begin{tabular}{c}Interesting Phenomenon\end{tabular}} + \mbox{}\\[-6mm] + + \small + \mbox{}\hspace{10mm} + \begin{tabular}{ll} + \multicolumn{2}{l}{\isacommand{nominal\_datatype} trm $=$}\\ + \hspace{5mm}\phantom{$|$} Var name\\ + \hspace{5mm}$|$ App trm trm\\ + \hspace{5mm}$|$ Lam x::name t::trm + & \isacommand{bind} x \isacommand{in} t\\ + \hspace{5mm}$|$ Let as::assn t::trm + & \isacommand{bind} bn(as) \isacommand{in} t\\ + \multicolumn{2}{l}{\isacommand{and} assn $=$}\\ + \multicolumn{2}{l}{\hspace{5mm}\phantom{$|$} ANil}\\ + \multicolumn{2}{l}{\hspace{5mm}$|$ ACons name trm assn}\\ + \multicolumn{2}{l}{\isacommand{binder} bn \isacommand{where}}\\ + \multicolumn{2}{l}{\hspace{5mm}\phantom{$|$} bn(ANil) $=$ $[]$}\\ + \multicolumn{2}{l}{\hspace{5mm}$|$ bn(ACons a t as) $=$ $[$a$]$ @ bn(as)}\\ + \end{tabular}\bigskip\medskip + + we cannot quotient assn: ACons a \ldots $\not\approx_\alpha$ ACons b \ldots + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ \begin{frame}<1-> \frametitle{\begin{tabular}{c}Conclusion\end{tabular}} \mbox{}\\[-6mm] @@ -995,14 +977,14 @@ \begin{itemize} \item the user does not see anything of the raw level\medskip \only<1>{\begin{center} - Lam [a]. (Var a) \alert{$=$} Lam [b]. (Var b) + Lam a (Var a) \alert{$=$} Lam b (Var b) \end{center}\bigskip} \item<2-> we have not yet done function definitions (will come soon and we hope to make improvements over the old way there too)\medskip - \item<3-> it took quite some time to get here, but it seems worthwhile (POPL 2011 tutorial)\medskip - \item<4-> Thanks goes to Cezary!\\ - \only<5->{\hspace{3mm}\ldots{}and of course others $\in$ Isabelle-team!} + \item<3-> it took quite some time to get here, but it seems worthwhile + (Barendregt's variable convention is unsound in general, + found bugs in two paper proofs, quotient package, POPL 2011 tutorial)\medskip \end{itemize}