# HG changeset patch # User Christian Urban # Date 1276089256 -7200 # Node ID 25d2cdf7d7e4295a47df6ed275ee5df274140cdf # Parent ad03df7e80565c0045d68da6a7e95de872d58714 transitivity proofs done diff -r ad03df7e8056 -r 25d2cdf7d7e4 Nominal-General/nominal_library.ML --- a/Nominal-General/nominal_library.ML Mon Jun 07 11:46:26 2010 +0200 +++ b/Nominal-General/nominal_library.ML Wed Jun 09 15:14:16 2010 +0200 @@ -6,6 +6,8 @@ signature NOMINAL_LIBRARY = sig + val last2: 'a list -> 'a * 'a + val dest_listT: typ -> typ val mk_minus: term -> term @@ -57,7 +59,11 @@ structure Nominal_Library: NOMINAL_LIBRARY = struct -(* this function should be in hologic.ML *) +fun last2 [] = raise Empty + | last2 [_] = raise Empty + | last2 [x, y] = (x,y) + | last2 (_ :: xs) = last2 xs + fun dest_listT (Type (@{type_name list}, [T])) = T | dest_listT T = raise TYPE ("dest_listT: list type expected", [T], []) diff -r ad03df7e8056 -r 25d2cdf7d7e4 Nominal/Abs.thy --- 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 \ R = R" shows "(bs, x) \gen R f p (cs, y) \ (cs, y) \gen R f (- p) (bs, x)" and "(bs, x) \res R f p (cs, y) \ (cs, y) \res R f (- p) (bs, x)" - and "(ds, x) \lst R f p (es, y) \ (es, y) \lst R f (- p) (ds, x)" -proof - - { assume "R (p \ x) y" - then have "R y (p \ x)" using a by simp - then have "R (- p \ 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) \gen R f p (cs, y) \ (cs, y) \gen R f (- p) (bs, x)" - and "(bs, x) \res R f p (cs, y) \ (cs, y) \res R f (- p) (bs, x)" - and "(ds, x) \lst R f p (es, y) \ (es, y) \lst R f (- p) (ds, x)" - unfolding alphas fresh_star_def - by (auto simp add: fresh_minus_perm) -qed + and "(ds, x) \lst R f p (es, y) \ (es, y) \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: "\R (p \ x) y; R (q \ y) z\ \ R ((q + p) \ x) z" @@ -115,6 +110,74 @@ by (simp_all add: fresh_plus_perm) +lemma alpha_gen_trans_eqvt: + assumes b: "(cs, y) \gen R f q (ds, z)" + and a: "(bs, x) \gen R f p (cs, y)" + and d: "q \ R = R" + and c: "\R (p \ x) y; R y (- q \ z)\ \ R (p \ x) (- q \ z)" + shows "(bs, x) \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) \res R f q (ds, z)" + and a: "(bs, x) \res R f p (cs, y)" + and d: "q \ R = R" + and c: "\R (p \ x) y; R y (- q \ z)\ \ R (p \ x) (- q \ z)" + shows "(bs, x) \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) \lst R f q (ds, z)" + and a: "(bs, x) \lst R f p (cs, y)" + and d: "q \ R = R" + and c: "\R (p \ x) y; R y (- q \ z)\ \ R (p \ x) (- q \ z)" + shows "(bs, x) \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) \gen R f pi (bs, s) \ R (pi \ t) s" + and "(as, t) \res R f pi (bs, s) \ R (pi \ t) s" + and "(cs, t) \lst R f pi (ds, s) \ R (pi \ t) s" + by (simp_all add: alphas) + section {* General Abstractions *} diff -r ad03df7e8056 -r 25d2cdf7d7e4 Nominal/Ex/CoreHaskell.thy --- a/Nominal/Ex/CoreHaskell.thy Mon Jun 07 11:46:26 2010 +0200 +++ b/Nominal/Ex/CoreHaskell.thy Wed Jun 09 15:14:16 2010 +0200 @@ -8,7 +8,7 @@ atom_decl cvar atom_decl tvar -declare [[STEPS = 10]] +declare [[STEPS = 11]] nominal_datatype tkind = KStar diff -r ad03df7e8056 -r 25d2cdf7d7e4 Nominal/Ex/SingleLet.thy --- a/Nominal/Ex/SingleLet.thy Mon Jun 07 11:46:26 2010 +0200 +++ b/Nominal/Ex/SingleLet.thy Wed Jun 09 15:14:16 2010 +0200 @@ -2,9 +2,10 @@ imports "../NewParser" begin + atom_decl name -declare [[STEPS = 10]] +declare [[STEPS = 11]] nominal_datatype trm = Var "name" @@ -20,146 +21,7 @@ where "bn (As x y t z) = {atom x}" -thm alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros -thm alpha_trm_raw.cases alpha_assg_raw.cases alpha_bn_raw.cases - -lemma [eqvt]: - "p \ alpha_trm_raw x1 y1 = alpha_trm_raw (p \ x1) (p \ y1)" - "p \ alpha_assg_raw x2 y2 = alpha_assg_raw (p \ x2) (p \ y2)" - "p \ alpha_bn_raw x3 y3 = alpha_bn_raw (p \ x3) (p \ y3)" -sorry - -lemmas ii = alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros -lemmas cc = alpha_trm_raw.cases alpha_assg_raw.cases alpha_bn_raw.cases - -ML {* -length @{thms cc} -*} - -ML {* - val pp = ["SingleLet.alpha_trm_raw", "SingleLet.alpha_assg_raw", "SingleLet.alpha_bn_raw"] -*} - -lemma exi_sum: "\(q :: perm). P q \ \q. Q q \ (\p q. P p \ Q q \ R (p + q)) \ \r. R r" -apply(erule exE)+ -apply(rule_tac x="q + qa" in exI) -apply(simp) -done - -lemma alpha_gen_compose_trans: - assumes b: "(as, t) \gen (\x1 x2. R x1 x2 \ (\x. R x2 x \ R x1 x)) f pi (bs, s)" - shows "(\x. R s x \ R (pi \ t) x)" - using b - by (simp add: alphas) - -lemma test: - assumes b: "(as, t) \gen R f pi (bs, s)" - shows "R (pi \ t) s" - using b - by (simp add: alphas) - -lemma alpha_gen_trans_eqvt: - assumes a: "(bs, x) \gen R f p (cs, y)" and a1: "(cs, y) \gen R f q (ds, z)" - and b: "\R (p \ x) y; R y (- q \ z)\ \ R (p \ x) (- q \ z)" - shows "(bs, x) \gen R f (q + p) (ds, z)" - sorry - - -lemma - "alpha_trm_raw x1 y1 \ (\z1. alpha_trm_raw y1 z1 \ alpha_trm_raw x1 z1)" - "alpha_assg_raw x2 y2 \ (\z2. alpha_assg_raw y2 z2 \ alpha_assg_raw x2 z2)" - "alpha_bn_raw x3 y3 \ (\z3. alpha_bn_raw y3 z3 \ alpha_bn_raw x3 z3)" -apply(induct rule: alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.inducts) -(* 8 *) -prefer 8 -thm alpha_bn_raw.cases -apply(rotate_tac -1) -apply(erule alpha_bn_raw.cases) -apply(simp_all)[6] - - -apply(rotate_tac -1) -apply(erule cc) -apply(simp_all)[6] -apply(rule ii) -apply(simp) -(* 1 *) -apply(rotate_tac -1) -apply(erule cc) -apply(simp_all)[6] -apply(rule ii) -apply(simp) -apply(simp) -(* 2 *) -apply(rotate_tac -1) -apply(erule cc) -apply(simp_all)[6] -apply(rule ii) -apply(erule exE)+ -apply(rule_tac x="pa + p" in exI) -apply(rule alpha_gen_trans_eqvt) -prefer 2 -apply(assumption) -apply(simp add: alphas) -apply(metis) -apply(drule test) -apply(simp) -(* 3 *) -apply(rotate_tac -1) -apply(erule cc) -apply(simp_all)[6] -apply(rule ii) -apply(erule exE)+ -apply(rule_tac x="pa + p" in exI) -apply(rule alpha_gen_trans_eqvt) -prefer 2 -apply(assumption) -apply(simp add: alphas) -apply(metis) -apply(drule alpha_gen_compose_trans) -apply(simp) -apply(simp) -(* 4 *) -apply(rotate_tac -1) -apply(erule cc) -apply(simp_all)[6] -apply(rule ii) -apply(erule exE)+ -apply(rule_tac x="pa + p" in exI) -apply(rule alpha_gen_trans_eqvt) -prefer 2 -apply(assumption) -prefer 2 -apply(drule test) -apply(simp add: prod_alpha_def) -apply(simp add: alphas) - -apply(drule alpha_gen_compose_trans) -apply(drule_tac x="(- pa \ trm_rawaa)" in spec) -apply(simp) -apply(simp) -(* 4 *) -apply(assumption) -apply(simp) -apply(simp) - -(* 3 *) - -(* 4 *) - -(* 5 *) - -(* 6 *) - -(* 7 *) - -(* 8 *) - -(* 9 *) -done - -ML {* Inductive.the_inductive *} thm trm_assg.fv thm trm_assg.supp thm trm_assg.eq_iff diff -r ad03df7e8056 -r 25d2cdf7d7e4 Nominal/NewParser.thy --- a/Nominal/NewParser.thy Mon Jun 07 11:46:26 2010 +0200 +++ b/Nominal/NewParser.thy Wed Jun 09 15:14:16 2010 +0200 @@ -427,6 +427,8 @@ val _ = tracing ("alphas " ^ commas (map (Syntax.string_of_term lthy4) alpha_trms)) val _ = tracing ("alpha_bns " ^ commas (map (Syntax.string_of_term lthy4) alpha_bn_trms)) + val _ = tracing ("alpha_trans\n" ^ + cat_lines (map (Syntax.string_of_term lthy4 o prop_of) alpha_trans_thms)) val _ = if get_STEPS lthy > 11 diff -r ad03df7e8056 -r 25d2cdf7d7e4 Nominal/nominal_dt_alpha.ML --- a/Nominal/nominal_dt_alpha.ML Mon Jun 07 11:46:26 2010 +0200 +++ b/Nominal/nominal_dt_alpha.ML Wed Jun 09 15:14:16 2010 +0200 @@ -2,7 +2,7 @@ Author: Cezary Kaliszyk Author: Christian Urban - Definitions of the alpha relations. + Definitions and proofs for the alpha-relations. *) signature NOMINAL_DT_ALPHA = @@ -398,20 +398,56 @@ end + (** transitivity proof for alphas **) +fun ecases_tac cases = + Subgoal.FOCUS (fn {prems, ...} => + HEADGOAL (resolve_tac cases THEN' rtac (List.last prems))) + +fun aatac pred_names = + SUBPROOF (fn {prems, context, ...} => + HEADGOAL (resolve_tac (map (transform_prem1 context pred_names) prems))) + +val perm_inst_tac = + Subgoal.FOCUS (fn {params, ...} => + let + val (p, q) = pairself snd (last2 params) + val pq_inst = foldl1 (uncurry Thm.capply) [@{cterm "plus::perm => perm => perm"}, p, q] + val exi_inst = Drule.instantiate' [SOME (@{ctyp "perm"})] [NONE, SOME pq_inst] @{thm exI} + in + HEADGOAL (rtac exi_inst) + end) + +fun non_trivial_cases_tac pred_names intros ctxt = +let + val prod_simps = @{thms split_conv alphas permute_prod.simps prod_alpha_def prod_rel.simps} +in + resolve_tac intros + THEN_ALL_NEW (asm_simp_tac HOL_basic_ss THEN' + TRY o EVERY' + [ etac @{thm exE}, + etac @{thm exE}, + perm_inst_tac ctxt, + resolve_tac @{thms alpha_trans_eqvt}, + atac, + aatac pred_names ctxt, + Nominal_Permeq.eqvt_tac ctxt [] [] THEN' rtac @{thm refl}, + asm_full_simp_tac (HOL_ss addsimps prod_simps) ]) +end + fun prove_trans_tac pred_names raw_dt_thms intros induct cases ctxt = let - val _ = ("induct\n" ^ Syntax.string_of_term ctxt (prop_of induct)) - - val tac1 = asm_full_simp_tac (HOL_basic_ss addsimps raw_dt_thms) - fun tac i = (EVERY' [rtac @{thm allI}, rtac @{thm impI}, rotate_tac ~1, - etac (nth cases i) THEN_ALL_NEW tac1]) i + fun all_cases ctxt = + asm_full_simp_tac (HOL_basic_ss addsimps raw_dt_thms) + THEN' TRY o non_trivial_cases_tac pred_names intros ctxt in - HEADGOAL (rtac induct THEN_ALL_NEW tac) + HEADGOAL (rtac induct THEN_ALL_NEW + EVERY' [ rtac @{thm allI}, rtac @{thm impI}, + ecases_tac cases ctxt THEN_ALL_NEW all_cases ctxt ]) end -fun prep_trans_goal alpha_trm ((arg1, arg2), arg_ty) = +xfun prep_trans_goal alpha_trm ((arg1, arg2), arg_ty) = let val lhs = alpha_trm $ arg1 $ arg2 val mid = alpha_trm $ arg2 $ (Bound 0) @@ -422,6 +458,8 @@ HOLogic.mk_imp (mid, rhs))) end +val norm = @{lemma "A --> (!x. B x --> C x) ==> (!!x. [|A; B x|] ==> C x)" by simp} + fun raw_prove_trans alpha_trms raw_dt_thms alpha_intros alpha_induct alpha_cases ctxt = let val alpha_names = map (fst o dest_Const) alpha_trms @@ -443,6 +481,7 @@ prove_trans_tac alpha_names raw_dt_thms alpha_intros alpha_induct alpha_cases context) |> singleton (ProofContext.export ctxt' ctxt) |> Datatype_Aux.split_conj_thm + |> map (fn th => zero_var_indexes (th RS norm)) end end (* structure *) diff -r ad03df7e8056 -r 25d2cdf7d7e4 Slides/Slides1.thy --- 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{ - \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{ + \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