# HG changeset patch # User Christian Urban # Date 1275903781 -7200 # Node ID 4da5c5c29009c131f49a650fd2090acc84b95485 # Parent dd3b9c046c7d17aa8acf9e37ed6b30184beb4cf7 work on transitivity proof diff -r dd3b9c046c7d -r 4da5c5c29009 Nominal-General/nominal_eqvt.ML --- a/Nominal-General/nominal_eqvt.ML Thu Jun 03 15:02:52 2010 +0200 +++ b/Nominal-General/nominal_eqvt.ML Mon Jun 07 11:43:01 2010 +0200 @@ -28,66 +28,6 @@ (Conv.params_conv ~1 (K (Conv.prems_conv ~1 atomize_conv)) ctxt)); -(** - given the theorem F[t]; proves the theorem F[f t] - - - F needs to be monotone - - f returns either SOME for a term it fires on - and NONE elsewhere -**) -fun map_term f t = - (case f t of - NONE => map_term' f t - | x => x) -and map_term' f (t $ u) = - (case (map_term f t, map_term f u) of - (NONE, NONE) => NONE - | (SOME t'', NONE) => SOME (t'' $ u) - | (NONE, SOME u'') => SOME (t $ u'') - | (SOME t'', SOME u'') => SOME (t'' $ u'')) - | map_term' f (Abs (s, T, t)) = - (case map_term f t of - NONE => NONE - | SOME t'' => SOME (Abs (s, T, t''))) - | map_term' _ _ = NONE; - -fun map_thm_tac ctxt tac thm = -let - val monos = Inductive.get_monos ctxt - val simps = HOL_basic_ss addsimps @{thms split_def} -in - EVERY [cut_facts_tac [thm] 1, etac rev_mp 1, - REPEAT_DETERM (FIRSTGOAL (simp_tac simps THEN' resolve_tac monos)), - REPEAT_DETERM (rtac impI 1 THEN (atac 1 ORELSE tac))] -end - -fun map_thm ctxt f tac thm = -let - val opt_goal_trm = map_term f (prop_of thm) -in - case opt_goal_trm of - NONE => thm - | SOME goal => - Goal.prove ctxt [] [] goal (fn _ => map_thm_tac ctxt tac thm) -end - -(* - inductive premises can be of the form - R ... /\ P ...; split_conj picks out - the part P ... -*) -fun transform_prem ctxt names thm = -let - fun split_conj names (Const ("op &", _) $ f1 $ f2) = - (case head_of f1 of - Const (name, _) => if member (op =) names name then SOME f2 else NONE - | _ => NONE) - | split_conj _ _ = NONE; -in - map_thm ctxt (split_conj names) (etac conjunct2 1) thm -end - - (** equivariance tactics **) val perm_boolE = @{thm permute_boolE} @@ -104,7 +44,7 @@ eqvt_strict_tac ctxt [] pred_names THEN' SUBPROOF (fn {prems, context as ctxt, ...} => let - val prems' = map (transform_prem ctxt pred_names) prems + val prems' = map (transform_prem2 ctxt pred_names) prems val tac1 = resolve_tac prems' val tac2 = EVERY' [ rtac pi_intro_rule, eqvt_strict_tac ctxt perm_cancel pred_names, resolve_tac prems' ] diff -r dd3b9c046c7d -r 4da5c5c29009 Nominal-General/nominal_library.ML --- a/Nominal-General/nominal_library.ML Thu Jun 03 15:02:52 2010 +0200 +++ b/Nominal-General/nominal_library.ML Mon Jun 07 11:43:01 2010 +0200 @@ -48,7 +48,9 @@ val pat_completeness_simp: thm list -> Proof.context -> tactic val prove_termination: Proof.context -> Function.info * local_theory - + (* transformations of premises in inductions *) + val transform_prem1: Proof.context -> string list -> thm -> thm + val transform_prem2: Proof.context -> string list -> thm -> thm end @@ -156,7 +158,9 @@ end -(** function package **) + +(** function package tactics **) + fun pat_completeness_auto lthy = Pat_Completeness.pat_completeness_tac lthy 1 THEN auto_tac (clasimpset_of lthy) @@ -173,6 +177,77 @@ Function.prove_termination NONE (Lexicographic_Order.lexicographic_order_tac true lthy) lthy + +(** transformations of premises (in inductive proofs) **) + +(* + given the theorem F[t]; proves the theorem F[f t] + + - F needs to be monotone + - f returns either SOME for a term it fires on + and NONE elsewhere +*) +fun map_term f t = + (case f t of + NONE => map_term' f t + | x => x) +and map_term' f (t $ u) = + (case (map_term f t, map_term f u) of + (NONE, NONE) => NONE + | (SOME t'', NONE) => SOME (t'' $ u) + | (NONE, SOME u'') => SOME (t $ u'') + | (SOME t'', SOME u'') => SOME (t'' $ u'')) + | map_term' f (Abs (s, T, t)) = + (case map_term f t of + NONE => NONE + | SOME t'' => SOME (Abs (s, T, t''))) + | map_term' _ _ = NONE; + +fun map_thm_tac ctxt tac thm = +let + val monos = Inductive.get_monos ctxt + val simps = HOL_basic_ss addsimps @{thms split_def} +in + EVERY [cut_facts_tac [thm] 1, etac rev_mp 1, + REPEAT_DETERM (FIRSTGOAL (simp_tac simps THEN' resolve_tac monos)), + REPEAT_DETERM (rtac impI 1 THEN (atac 1 ORELSE tac))] +end + +fun map_thm ctxt f tac thm = +let + val opt_goal_trm = map_term f (prop_of thm) +in + case opt_goal_trm of + NONE => thm + | SOME goal => + Goal.prove ctxt [] [] goal (fn _ => map_thm_tac ctxt tac thm) +end + +(* + inductive premises can be of the form + R ... /\ P ...; split_conj_i picks out + the part R or P part +*) +fun split_conj1 names (Const ("op &", _) $ f1 $ f2) = + (case head_of f1 of + Const (name, _) => if member (op =) names name then SOME f1 else NONE + | _ => NONE) +| split_conj1 _ _ = NONE; + +fun split_conj2 names (Const ("op &", _) $ f1 $ f2) = + (case head_of f1 of + Const (name, _) => if member (op =) names name then SOME f2 else NONE + | _ => NONE) +| split_conj2 _ _ = NONE; + +fun transform_prem1 ctxt names thm = + map_thm ctxt (split_conj1 names) (etac conjunct1 1) thm + +fun transform_prem2 ctxt names thm = + map_thm ctxt (split_conj2 names) (etac conjunct2 1) thm + + + end (* structure *) open Nominal_Library; \ No newline at end of file diff -r dd3b9c046c7d -r 4da5c5c29009 Nominal/Abs.thy --- a/Nominal/Abs.thy Thu Jun 03 15:02:52 2010 +0200 +++ b/Nominal/Abs.thy Mon Jun 07 11:43:01 2010 +0200 @@ -51,6 +51,73 @@ by (case_tac [!] bs, case_tac [!] cs) (auto simp add: le_fun_def le_bool_def alphas) +(* equivariance *) +lemma alpha_gen_eqvt[eqvt]: + shows "(bs, x) \gen R f q (cs, y) \ (p \ bs, p \ x) \gen (p \ R) (p \ f) (p \ q) (p \ cs, p \ y)" + and "(bs, x) \res R f q (cs, y) \ (p \ bs, p \ x) \res (p \ R) (p \ f) (p \ q) (p \ cs, p \ y)" + and "(ds, x) \lst R f q (es, y) \ (p \ ds, p \ x) \lst (p \ R) (p \ f) (p \ q) (p \ es, p \ y)" + unfolding alphas + unfolding permute_eqvt[symmetric] + unfolding set_eqvt[symmetric] + unfolding permute_fun_app_eq[symmetric] + unfolding Diff_eqvt[symmetric] + by (auto simp add: permute_bool_def fresh_star_permute_iff) + +(* equivalence *) +lemma alpha_gen_refl: + assumes a: "R x x" + shows "(bs, x) \gen R f 0 (bs, x)" + and "(bs, x) \res R f 0 (bs, x)" + and "(cs, x) \lst R f 0 (cs, x)" + using a + unfolding alphas + unfolding fresh_star_def + by (simp_all add: fresh_zero_perm) + +lemma alpha_gen_sym: + assumes a: "R (p \ x) y \ R (- p \ y) x" + 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)" + unfolding alphas fresh_star_def + using a + by (auto simp add: fresh_minus_perm) + +lemma alpha_gen_sym_eqvt: + assumes a: "R (p \ x) y \ R y (p \ x)" + 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 + +lemma alpha_gen_trans: + assumes a: "\R (p \ x) y; R (q \ y) z\ \ R ((q + p) \ x) z" + shows "\(bs, x) \gen R f p (cs, y); (cs, y) \gen R f q (ds, z)\ \ (bs, x) \gen R f (q + p) (ds, z)" + and "\(bs, x) \res R f p (cs, y); (cs, y) \res R f q (ds, z)\ \ (bs, x) \res R f (q + p) (ds, z)" + and "\(es, x) \lst R f p (gs, y); (gs, y) \lst R f q (hs, z)\ \ (es, x) \lst R f (q + p) (hs, z)" + using a + unfolding alphas fresh_star_def + by (simp_all add: fresh_plus_perm) + + + +section {* General Abstractions *} + fun alpha_abs where @@ -731,45 +798,7 @@ lemmas alphas_compose_trans2 = alpha_gen_compose_trans2 alpha_res_compose_trans2 alpha_lst_compose_trans2 -lemma alpha_gen_refl: - assumes a: "R x x" - shows "(bs, x) \gen R f 0 (bs, x)" - and "(bs, x) \res R f 0 (bs, x)" - and "(cs, x) \lst R f 0 (cs, x)" - using a - unfolding alphas - unfolding fresh_star_def - by (simp_all add: fresh_zero_perm) -lemma alpha_gen_sym: - assumes a: "R (p \ x) y \ R (- p \ y) x" - 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)" - unfolding alphas fresh_star_def - using a - by (auto simp add: fresh_minus_perm) - -lemma alpha_gen_trans: - assumes a: "\R (p \ x) y; R (q \ y) z\ \ R ((q + p) \ x) z" - shows "\(bs, x) \gen R f p (cs, y); (cs, y) \gen R f q (ds, z)\ \ (bs, x) \gen R f (q + p) (ds, z)" - and "\(bs, x) \res R f p (cs, y); (cs, y) \res R f q (ds, z)\ \ (bs, x) \res R f (q + p) (ds, z)" - and "\(es, x) \lst R f p (gs, y); (gs, y) \lst R f q (hs, z)\ \ (es, x) \lst R f (q + p) (hs, z)" - using a - unfolding alphas fresh_star_def - by (simp_all add: fresh_plus_perm) - - -lemma alpha_gen_eqvt[eqvt]: - shows "(bs, x) \gen R f q (cs, y) \ (p \ bs, p \ x) \gen (p \ R) (p \ f) (p \ q) (p \ cs, p \ y)" - and "(bs, x) \res R f q (cs, y) \ (p \ bs, p \ x) \res (p \ R) (p \ f) (p \ q) (p \ cs, p \ y)" - and "(ds, x) \lst R f q (es, y) \ (p \ ds, p \ x) \lst (p \ R) (p \ f) (p \ q) (p \ es, p \ y)" - unfolding alphas - unfolding permute_eqvt[symmetric] - unfolding set_eqvt[symmetric] - unfolding permute_fun_app_eq[symmetric] - unfolding Diff_eqvt[symmetric] - by (auto simp add: permute_bool_def fresh_star_permute_iff) lemma alpha_gen_simpler: assumes fv_rsp: "\x y. R y x \ f x = f y" diff -r dd3b9c046c7d -r 4da5c5c29009 Nominal/Ex/Classical.thy --- a/Nominal/Ex/Classical.thy Thu Jun 03 15:02:52 2010 +0200 +++ b/Nominal/Ex/Classical.thy Mon Jun 07 11:43:01 2010 +0200 @@ -11,12 +11,12 @@ nominal_datatype trm = Ax "name" "coname" -| Cut n::"coname" t1::"trm" c::"coname" t2::"trm" bind_set n in t1, bind_set c in t2 -| AndR c1::"coname" t1::"trm" c2::"coname" t2::"trm" "coname" bind_set c1 in t1, bind_set c2 in t2 -| AndL1 n::"name" t::"trm" "name" bind_set n in t -| AndL2 n::"name" t::"trm" "name" bind_set n in t -| ImpL c::"coname" t1::"trm" n::"name" t2::"trm" "name" bind_set c in t1, bind_set n in t2 -| ImpR c::"coname" n::"name" t::"trm" "coname" bind_set n c in t +| Cut n::"coname" t1::"trm" c::"coname" t2::"trm" bind n in t1, bind c in t2 +| AndR c1::"coname" t1::"trm" c2::"coname" t2::"trm" "coname" bind c1 in t1, bind c2 in t2 +| AndL1 n::"name" t::"trm" "name" bind n in t +| AndL2 n::"name" t::"trm" "name" bind n in t +| ImpL c::"coname" t1::"trm" n::"name" t2::"trm" "name" bind c in t1, bind n in t2 +| ImpR c::"coname" n::"name" t::"trm" "coname" bind n c in t thm alpha_trm_raw.intros[no_vars] diff -r dd3b9c046c7d -r 4da5c5c29009 Nominal/Ex/CoreHaskell.thy --- a/Nominal/Ex/CoreHaskell.thy Thu Jun 03 15:02:52 2010 +0200 +++ b/Nominal/Ex/CoreHaskell.thy Mon Jun 07 11:43:01 2010 +0200 @@ -8,7 +8,7 @@ atom_decl cvar atom_decl tvar -declare [[STEPS = 9]] +declare [[STEPS = 10]] nominal_datatype tkind = KStar @@ -85,7 +85,105 @@ | "bv_cvs CvsNil = []" | "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t" +lemma alpha_gen_sym_test: + assumes a: "R (p \ x) y \ R y (p \ x)" + 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)" + unfolding alphas fresh_star_def + apply(auto simp add: fresh_minus_perm) + apply(rule_tac p="p" in permute_boolE) + apply(perm_simp add: permute_minus_cancel b) + apply(simp add: a) + apply(rule_tac p="p" in permute_boolE) + apply(perm_simp add: permute_minus_cancel b) + apply(simp add: a) + apply(rule_tac p="p" in permute_boolE) + apply(perm_simp add: permute_minus_cancel b) + apply(simp add: a) + done +ML {* +(* for equalities *) +val tac1 = rtac @{thm sym} THEN' atac + +(* for "unbound" premises *) +val tac2 = atac + +fun trans_prem_tac pred_names ctxt = + SUBPROOF (fn {prems, context as ctxt, ...} => + let + val prems' = map (transform_prem1 ctxt pred_names) prems + val _ = tracing ("prems'\n" ^ cat_lines (map (Syntax.string_of_term ctxt o prop_of) prems')) + in + print_tac "goal" THEN resolve_tac prems' 1 + end) ctxt + +(* for "bound" premises *) +fun tac3 pred_names ctxt = + EVERY' [etac @{thm exi_neg}, + resolve_tac @{thms alpha_gen_sym_test}, + asm_full_simp_tac (HOL_ss addsimps @{thms split_conv permute_prod.simps + prod_alpha_def prod_rel.simps alphas}), + Nominal_Permeq.eqvt_tac ctxt [] [] THEN' rtac @{thm refl}, + trans_prem_tac pred_names ctxt] + +fun tac intro pred_names ctxt = + resolve_tac intro THEN_ALL_NEW FIRST' [tac1, tac2, tac3 pred_names ctxt] +*} + +lemma [eqvt]: +shows "p \ alpha_tkind_raw = alpha_tkind_raw" +and "p \ alpha_ckind_raw = alpha_ckind_raw" +and "p \ alpha_ty_raw = alpha_ty_raw" +and "p \ alpha_ty_lst_raw = alpha_ty_lst_raw" +and "p \ alpha_co_raw = alpha_co_raw" +and "p \ alpha_co_lst_raw = alpha_co_lst_raw" +and "p \ alpha_trm_raw = alpha_trm_raw" +and "p \ alpha_assoc_lst_raw = alpha_assoc_lst_raw" +and "p \ alpha_pat_raw = alpha_pat_raw" +and "p \ alpha_vars_raw = alpha_vars_raw" +and "p \ alpha_tvars_raw = alpha_tvars_raw" +and "p \ alpha_cvars_raw = alpha_cvars_raw" +and "p \ alpha_bv_raw = alpha_bv_raw" +and "p \ alpha_bv_vs_raw = alpha_bv_vs_raw" +and "p \ alpha_bv_tvs_raw = alpha_bv_tvs_raw" +and "p \ alpha_bv_cvs_raw = alpha_bv_cvs_raw" +sorry + +lemmas ii = alpha_tkind_raw_alpha_ckind_raw_alpha_ty_raw_alpha_ty_lst_raw_alpha_co_raw_alpha_co_lst_raw_alpha_trm_raw_alpha_assoc_lst_raw_alpha_pat_raw_alpha_vars_raw_alpha_tvars_raw_alpha_cvars_raw_alpha_bv_raw_alpha_bv_vs_raw_alpha_bv_tvs_raw_alpha_bv_cvs_raw.inducts + +lemmas ij = alpha_tkind_raw_alpha_ckind_raw_alpha_ty_raw_alpha_ty_lst_raw_alpha_co_raw_alpha_co_lst_raw_alpha_trm_raw_alpha_assoc_lst_raw_alpha_pat_raw_alpha_vars_raw_alpha_tvars_raw_alpha_cvars_raw_alpha_bv_raw_alpha_bv_vs_raw_alpha_bv_tvs_raw_alpha_bv_cvs_raw.intros + +ML {* +val pp = ["CoreHaskel.alpha_tkind_raw", "CoreHaskell.alpha_ckind_raw", "CoreHaskell.alpha_ty_raw", "CoreHaskell.alpha_ty_lst_raw", "CoreHaskell.alpha_co_raw", "CoreHaskell.alpha_co_lst_raw", "CoreHaskell.alpha_trm_raw", "CoreHaskell.alpha_assoc_lst_raw", "CoreHaskell.alpha_pat_raw", "CoreHaskell.alpha_vars_raw", "CoreHaskell.alpha_tvars_raw", "CoreHaskell.alpha_cvars_raw", "CoreHaskell.alpha_bv_raw", "CoreHaskell.alpha_bv_vs_raw", "CoreHaskell.alpha_bv_tvs_raw", "CoreHaskell.alpha_bv_cvs_raw"] +*} + +lemma +shows "alpha_tkind_raw x1 y1 ==> alpha_tkind_raw y1 x1" +and "alpha_ckind_raw x2 y2 ==> alpha_ckind_raw y2 x2" +and "alpha_ty_raw x3 y3 ==> alpha_ty_raw y3 x3" +and "alpha_ty_lst_raw x4 y4 ==> alpha_ty_lst_raw y4 x4" +and "alpha_co_raw x5 y5 ==> alpha_co_raw y5 x5" +and "alpha_co_lst_raw x6 y6 ==> alpha_co_lst_raw y6 x6" +and "alpha_trm_raw x7 y7 ==> alpha_trm_raw y7 x7" +and "alpha_assoc_lst_raw x8 y8 ==> alpha_assoc_lst_raw y8 x8" +and "alpha_pat_raw x9 y9 ==> alpha_pat_raw y9 x9" +and "alpha_vars_raw xa ya ==> alpha_vars_raw ya xa" +and "alpha_tvars_raw xb yb ==> alpha_tvars_raw yb xb" +and "alpha_cvars_raw xc yc ==> alpha_cvars_raw yc xc" +and "alpha_bv_raw xd yd ==> alpha_bv_raw yd xd" +and "alpha_bv_vs_raw xe ye ==> alpha_bv_vs_raw ye xe" +and "alpha_bv_tvs_raw xf yf ==> alpha_bv_tvs_raw yf xf" +and "alpha_bv_cvs_raw xg yg ==> alpha_bv_cvs_raw yg xg" +apply(induct rule: ii) +apply(tactic {* tac @{thms ij} pp @{context} 1 *})+ +done + + +lemma +alpha_tkind_raw, alpha_ckind_raw, alpha_ty_raw, alpha_ty_lst_raw, alpha_co_raw, alpha_co_lst_raw, alpha_trm_raw, alpha_assoc_lst_raw, alpha_pat_raw, alpha_vars_raw, alpha_tvars_raw, alpha_cvars_raw, alpha_bv_raw, alpha_bv_vs_raw, alpha_bv_tvs_raw, alpha_bv_cvs_raw lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.supp(1-9,11,13,15) lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.fv[simplified fv_supp] lemmas perm=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.perm diff -r dd3b9c046c7d -r 4da5c5c29009 Nominal/Ex/Ex1rec.thy --- a/Nominal/Ex/Ex1rec.thy Thu Jun 03 15:02:52 2010 +0200 +++ b/Nominal/Ex/Ex1rec.thy Mon Jun 07 11:43:01 2010 +0200 @@ -2,10 +2,9 @@ imports "../NewParser" begin -atom_decl name +declare [[STEPS = 9]] -ML {* val _ = cheat_supp_eq := true *} -ML {* val _ = cheat_equivp := true *} +atom_decl name nominal_datatype lam = Var "name" @@ -19,6 +18,9 @@ where "bi (Bp x t) = {atom x}" + +thm alpha_lam_raw_alpha_bp_raw_alpha_bi_raw.intros + thm lam_bp.fv thm lam_bp.eq_iff[no_vars] thm lam_bp.bn diff -r dd3b9c046c7d -r 4da5c5c29009 Nominal/Ex/Ex2.thy --- a/Nominal/Ex/Ex2.thy Thu Jun 03 15:02:52 2010 +0200 +++ b/Nominal/Ex/Ex2.thy Mon Jun 07 11:43:01 2010 +0200 @@ -23,7 +23,6 @@ | "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 dd3b9c046c7d -r 4da5c5c29009 Nominal/Ex/LF.thy --- a/Nominal/Ex/LF.thy Thu Jun 03 15:02:52 2010 +0200 +++ b/Nominal/Ex/LF.thy Mon Jun 07 11:43:01 2010 +0200 @@ -2,21 +2,23 @@ imports "../NewParser" begin +declare [[STEPS = 9]] + atom_decl name atom_decl ident nominal_datatype kind = Type - | KPi "ty" n::"name" k::"kind" bind_set n in k + | KPi "ty" n::"name" k::"kind" bind n in k and ty = TConst "ident" | TApp "ty" "trm" - | TPi "ty" n::"name" t::"ty" bind_set n in t + | TPi "ty" n::"name" t::"ty" bind n in t and trm = Const "ident" | Var "name" | App "trm" "trm" - | Lam "ty" n::"name" t::"trm" bind_set n in t + | Lam "ty" n::"name" t::"trm" bind n in t thm kind_ty_trm.supp diff -r dd3b9c046c7d -r 4da5c5c29009 Nominal/Ex/Lambda.thy --- a/Nominal/Ex/Lambda.thy Thu Jun 03 15:02:52 2010 +0200 +++ b/Nominal/Ex/Lambda.thy Mon Jun 07 11:43:01 2010 +0200 @@ -3,11 +3,12 @@ begin atom_decl name +declare [[STEPS = 9]] nominal_datatype lam = Var "name" | App "lam" "lam" -| Lam x::"name" l::"lam" bind_set x in l +| Lam x::"name" l::"lam" bind x in l thm lam.fv thm lam.supp diff -r dd3b9c046c7d -r 4da5c5c29009 Nominal/Ex/SingleLet.thy --- a/Nominal/Ex/SingleLet.thy Thu Jun 03 15:02:52 2010 +0200 +++ b/Nominal/Ex/SingleLet.thy Mon Jun 07 11:43:01 2010 +0200 @@ -4,15 +4,14 @@ atom_decl name -declare [[STEPS = 9]] - +declare [[STEPS = 10]] nominal_datatype trm = Var "name" | App "trm" "trm" | Lam x::"name" t::"trm" bind_set x in t | Let a::"assg" t::"trm" bind_set "bn a" in t -| Foo x::"name" y::"name" t::"trm" bind_set x in y t +| Foo x::"name" y::"name" t::"trm" t1::"trm" t2::"trm" bind_set x in y t t1 t2 | Bar x::"name" y::"name" t::"trm" bind y x in t x y and assg = As "name" "name" "trm" "name" @@ -21,6 +20,145 @@ 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 diff -r dd3b9c046c7d -r 4da5c5c29009 Nominal/NewParser.thy --- a/Nominal/NewParser.thy Thu Jun 03 15:02:52 2010 +0200 +++ b/Nominal/NewParser.thy Mon Jun 07 11:43:01 2010 +0200 @@ -405,18 +405,33 @@ val lthy_tmp' = snd (Local_Theory.note ((Binding.empty, [add_eqvt]), fv_eqvt) lthy_tmp) - val (alpha_eqvt, _) = + val (alpha_eqvt, lthy_tmp'') = if get_STEPS lthy > 8 - then Nominal_Eqvt.equivariance false alpha_trms alpha_induct alpha_intros lthy_tmp' + then Nominal_Eqvt.equivariance true (alpha_trms @ alpha_bn_trms) alpha_induct alpha_intros lthy_tmp' + else raise TEST lthy4 + + (* proving alpha equivalence *) + val _ = warning "Proving equivalence" + + val alpha_sym_thms = + if get_STEPS lthy > 9 + then raw_prove_sym (alpha_trms @ alpha_bn_trms) alpha_intros alpha_induct lthy_tmp'' else raise TEST lthy4 + val alpha_trans_thms = + if get_STEPS lthy > 10 + then raw_prove_trans (alpha_trms @ alpha_bn_trms) (distinct_thms @ inject_thms) + alpha_intros alpha_induct alpha_cases lthy_tmp'' + else raise TEST lthy4 + + + 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 _ = - if get_STEPS lthy > 9 + if get_STEPS lthy > 11 then true else raise TEST lthy4 - (* proving alpha equivalence *) - val _ = warning "Proving equivalence"; - val fv_alpha_all = combine_fv_alpha_bns (raw_fvs, raw_fv_bns) (alpha_trms, alpha_bn_trms) bn_nos val reflps = build_alpha_refl fv_alpha_all alpha_trms induct_thm alpha_eq_iff lthy4; @@ -424,6 +439,7 @@ if !cheat_equivp then map (equivp_hack lthy4) alpha_trms else build_equivps alpha_trms reflps alpha_induct inject_thms alpha_eq_iff distinct_thms alpha_cases alpha_eqvt lthy4; + val qty_binds = map (fn (_, b, _, _) => b) dts; val qty_names = map Name.of_binding qty_binds; val qty_full_names = map (Long_Name.qualify thy_name) qty_names diff -r dd3b9c046c7d -r 4da5c5c29009 Nominal/nominal_dt_alpha.ML --- a/Nominal/nominal_dt_alpha.ML Thu Jun 03 15:02:52 2010 +0200 +++ b/Nominal/nominal_dt_alpha.ML Mon Jun 07 11:43:01 2010 +0200 @@ -15,6 +15,9 @@ term list -> term list -> bn_info -> thm list * thm list val mk_alpha_eq_iff: Proof.context -> thm list -> thm list -> thm list -> thm list -> thm list + + val raw_prove_sym: term list -> thm list -> thm -> Proof.context -> thm list + val raw_prove_trans: term list -> thm list -> thm list -> thm -> thm list -> Proof.context -> thm list end structure Nominal_Dt_Alpha: NOMINAL_DT_ALPHA = @@ -288,6 +291,7 @@ (** produces the alpha_eq_iff simplification rules **) + (* in case a theorem is of the form (C.. = C..), it will be rewritten to ((C.. = C..) = True) *) fun mk_simp_rule thm = @@ -323,5 +327,123 @@ |> map mk_simp_rule end + + +(** symmetry proof for the alphas **) + +val exi_neg = @{lemma "(EX (p::perm). P p) ==> (!!q. P q ==> Q (- q)) ==> EX p. Q p" + by (erule exE, rule_tac x="-p" in exI, auto)} + +(* for premises that contain binders *) +fun prem_bound_tac pred_names ctxt = +let + fun trans_prem_tac pred_names ctxt = + SUBPROOF (fn {prems, context, ...} => + let + val prems' = map (transform_prem1 context pred_names) prems + in + resolve_tac prems' 1 + end) ctxt + val prod_simps = @{thms split_conv permute_prod.simps prod_alpha_def prod_rel.simps alphas} +in + EVERY' + [ etac exi_neg, + resolve_tac @{thms alpha_gen_sym_eqvt}, + asm_full_simp_tac (HOL_ss addsimps prod_simps), + Nominal_Permeq.eqvt_tac ctxt [] [] THEN' rtac @{thm refl}, + trans_prem_tac pred_names ctxt ] +end + +fun prove_sym_tac pred_names intros induct ctxt = +let + val prem_eq_tac = rtac @{thm sym} THEN' atac + val prem_unbound_tac = atac + + val prem_cases_tacs = FIRST' + [prem_eq_tac, prem_unbound_tac, prem_bound_tac pred_names ctxt] +in + HEADGOAL (rtac induct THEN_ALL_NEW + (resolve_tac intros THEN_ALL_NEW prem_cases_tacs)) +end + +fun prep_sym_goal alpha_trm (arg1, arg2) = +let + val lhs = alpha_trm $ arg1 $ arg2 + val rhs = alpha_trm $ arg2 $ arg1 +in + HOLogic.mk_imp (lhs, rhs) +end + +fun raw_prove_sym alpha_trms alpha_intros alpha_induct ctxt = +let + val alpha_names = map (fst o dest_Const) alpha_trms + val arg_tys = + alpha_trms + |> map fastype_of + |> map domain_type + val (arg_names1, (arg_names2, ctxt')) = + ctxt + |> Variable.variant_fixes (replicate (length arg_tys) "x") + ||> Variable.variant_fixes (replicate (length arg_tys) "y") + val args1 = map Free (arg_names1 ~~ arg_tys) + val args2 = map Free (arg_names2 ~~ arg_tys) + val goal = HOLogic.mk_Trueprop + (foldr1 HOLogic.mk_conj (map2 prep_sym_goal alpha_trms (args1 ~~ args2))) +in + Goal.prove ctxt' [] [] goal + (fn {context,...} => prove_sym_tac alpha_names alpha_intros alpha_induct context) + |> singleton (ProofContext.export ctxt' ctxt) + |> Datatype_Aux.split_conj_thm + |> map (fn th => zero_var_indexes (th RS mp)) +end + + +(** transitivity proof for alphas **) + +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 +in + HEADGOAL (rtac induct THEN_ALL_NEW tac) +end + +fun prep_trans_goal alpha_trm ((arg1, arg2), arg_ty) = +let + val lhs = alpha_trm $ arg1 $ arg2 + val mid = alpha_trm $ arg2 $ (Bound 0) + val rhs = alpha_trm $ arg1 $ (Bound 0) +in + HOLogic.mk_imp (lhs, + HOLogic.all_const arg_ty $ Abs ("z", arg_ty, + HOLogic.mk_imp (mid, rhs))) +end + +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 + val arg_tys = + alpha_trms + |> map fastype_of + |> map domain_type + val (arg_names1, (arg_names2, ctxt')) = + ctxt + |> Variable.variant_fixes (replicate (length arg_tys) "x") + ||> Variable.variant_fixes (replicate (length arg_tys) "y") + val args1 = map Free (arg_names1 ~~ arg_tys) + val args2 = map Free (arg_names2 ~~ arg_tys) + val goal = HOLogic.mk_Trueprop + (foldr1 HOLogic.mk_conj (map2 prep_trans_goal alpha_trms (args1 ~~ args2 ~~ arg_tys))) +in + Goal.prove ctxt' [] [] goal + (fn {context,...} => + 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 +end + end (* structure *) diff -r dd3b9c046c7d -r 4da5c5c29009 Nominal/nominal_dt_rawfuns.ML --- a/Nominal/nominal_dt_rawfuns.ML Thu Jun 03 15:02:52 2010 +0200 +++ b/Nominal/nominal_dt_rawfuns.ML Mon Jun 07 11:43:01 2010 +0200 @@ -246,6 +246,21 @@ (** equivarance proofs **) +val eqvt_apply_sym = @{thm eqvt_apply[symmetric]} + +fun subproof_tac const_names simps = + 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 (eqvt_apply_sym :: prems)))) + +fun prove_eqvt_tac insts ind_thms const_names simps ctxt = + HEADGOAL + (Object_Logic.full_atomize_tac + THEN' (DETERM o (InductTacs.induct_rules_tac ctxt insts ind_thms)) + THEN_ALL_NEW subproof_tac const_names simps ctxt) + fun mk_eqvt_goal pi const arg = let val lhs = mk_perm pi (const $ arg) @@ -254,13 +269,6 @@ 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 @@ -271,18 +279,15 @@ consts |> map fastype_of |> map domain_type - val (arg_names, ctxt'') = Variable.variant_fixes (Datatype_Prop.make_tnames 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' (DETERM o (InductTacs.induct_rules_tac ctxt insts ind_thms)) - THEN_ALL_NEW subproof_tac const_names simps ctxt + val const_names = map (fst o dest_Const) consts in - Goal.prove_multi ctxt'' [] [] goals (fn {context, ...} => (HEADGOAL (tac context))) + Goal.prove_multi ctxt'' [] [] goals (fn {context, ...} => + prove_eqvt_tac insts ind_thms const_names simps context) |> ProofContext.export ctxt'' ctxt end diff -r dd3b9c046c7d -r 4da5c5c29009 Slides/Slides1.thy --- a/Slides/Slides1.thy Thu Jun 03 15:02:52 2010 +0200 +++ b/Slides/Slides1.thy Mon Jun 07 11:43:01 2010 +0200 @@ -41,7 +41,7 @@ \mbox{}\\[-6mm] \begin{itemize} - \item old Nominal provided a reasoning infrastructure for single binders\medskip + \item the old Nominal Isabelle provided a reasoning infrastructure for single binders\medskip \begin{center} Lam [a].(Var a) @@ -64,7 +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\\ + \pgfuseshading{smallspherered} & Barendregt-style reasoning about bound variables\\ \end{tabular} \end{textblock}} @@ -235,7 +235,7 @@ \begin{itemize} \item this way of specifying binding is inspired by - Ott\onslide<2->{, \alert{\bf but} we made adjustments:}\medskip + {\bf Ott}\onslide<2->{, \alert{\bf but} we made some adjustments:}\medskip \only<2>{ @@ -264,11 +264,11 @@ \only<5>{ \begin{itemize} - \item we allow multiple binders and bodies\smallskip + \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 + the reason is that with our definitions of $\alpha$-equivalence \begin{center} \begin{tabular}{rcl} \isacommand{bind\_res} as \isacommand{in} x y & $\not\Leftrightarrow$ & @@ -296,7 +296,7 @@ \mbox{}\\[-3mm] \begin{itemize} - \item in old Nominal, we represented single binders as partial functions:\bigskip + \item in the old Nominal Isabelle, we represented single binders as partial functions:\bigskip \begin{center} \begin{tabular}{l} @@ -396,7 +396,7 @@ \only<1>{ \begin{textblock}{8}(3,8.5) \begin{tabular}{l@ {\hspace{2mm}}p{8cm}} - \pgfuseshading{smallspherered} & $as$ is a set of atoms\ldots the binders\\ + \pgfuseshading{smallspherered} & $as$ is a set of names\ldots the binders\\ \pgfuseshading{smallspherered} & $x$ is the body\\ \pgfuseshading{smallspherered} & $\approx_{\text{set}}$ is where the cardinality of the binders has to be the same\\ @@ -415,7 +415,7 @@ \only<8>{ \begin{textblock}{8}(3,13.8) - \footnotesize $^*$ $as$ and $bs$ are \alert{lists} of atoms + \footnotesize $^*$ $as$ and $bs$ are \alert{lists} of names \end{textblock}} \end{frame}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -424,7 +424,7 @@ text_raw {* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \mode{ - \begin{frame}<1-2> + \begin{frame}<1-3> \frametitle{\begin{tabular}{c}Examples\end{tabular}} \mbox{}\\[-3mm] @@ -445,7 +445,7 @@ \end{itemize} - \only<2->{ + \only<3->{ \begin{textblock}{4}(0.3,12) \begin{tikzpicture} \draw (0,0) node[inner sep=1mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] @@ -461,7 +461,7 @@ \end{minipage}}; \end{tikzpicture} \end{textblock}} - \only<2->{ + \only<3->{ \begin{textblock}{4}(5.2,12) \begin{tikzpicture} \draw (0,0) node[inner sep=1mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] @@ -477,7 +477,7 @@ \end{minipage}}; \end{tikzpicture} \end{textblock}} - \only<2->{ + \only<3->{ \begin{textblock}{4}(10.2,12) \begin{tikzpicture} \draw (0,0) node[inner sep=1mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] @@ -572,7 +572,7 @@ text_raw {* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \mode{ - \begin{frame}<1> + \begin{frame}<1-2> \frametitle{\begin{tabular}{c}Examples\end{tabular}} \mbox{}\\[-3mm] @@ -635,6 +635,21 @@ \end{tikzpicture} \end{textblock}} + \only<2>{ + \begin{textblock}{6}(2.5,4) + \begin{tikzpicture} + \draw (0,0) node[inner sep=5mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] + {\normalsize + \begin{minipage}{8cm}\raggedright + \begin{itemize} + \item \color{darkgray}$\alpha$-equivalences coincide when a single name is + abstracted + \item \color{darkgray}in that case they are equivalent to ``old-fashioned'' definitions of $\alpha$ + \end{itemize} + \end{minipage}}; + \end{tikzpicture} + \end{textblock}} + \end{frame}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *} @@ -647,10 +662,10 @@ \mbox{}\\[-7mm] \begin{itemize} - \item we take $(as, x) \approx\!\makebox[0mm][l]{${}_{\star}$}^{=,\text{supp}} (bs, y)$\medskip - \item they are equivalence relations\medskip + \item we take $(as, x) \approx\!\makebox[0mm][l]{${}_{{}*{}}$}^{=,\text{supp}} (bs, y)$\medskip + \item they are equivalence relations\medskip \item we can therefore use the quotient package to introduce the - types $\beta\;\text{abs}_\star$\bigskip + types $\beta\;\text{abs}_*$\bigskip \begin{center} \only<1>{$[as].\,x$} \only<2>{$\text{supp}([as].x) = \text{supp}(x) - as$} @@ -660,11 +675,15 @@ $\exists \pi.$ & $\text{supp}(x) - as = \text{supp}(y) - bs$\\ $\wedge$ & $\text{supp}(x) - as \fresh^* \pi$\\ $\wedge$ & $\pi \act x = y $\\ - $(\wedge$ & $\pi \act as = bs)\;^\star$\\ + $(\wedge$ & $\pi \act as = bs)\;^*$\\ \end{tabular}} \end{center} \end{itemize} + \only<1->{ + \begin{textblock}{8}(12,3.8) + \footnotesize $^*$ set, res, list + \end{textblock}} \end{frame}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -674,7 +693,7 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \mode{ \begin{frame}<1> - \frametitle{\begin{tabular}{c}One Problem\end{tabular}} + \frametitle{\begin{tabular}{c}A Problem\end{tabular}} \mbox{}\\[-3mm] \begin{center} @@ -824,14 +843,16 @@ {\text{Let}\;as\;t \approx_\alpha \text{Let}\;as'\;t'} {(\text{bn}(as), t) \approx\!\makebox[0mm][l]{${}_{\text{list}}$} ^{\approx_\alpha,\text{fv}} (\text{bn}(as'), t') & - \onslide<2>{as \approx_\alpha^{\text{bn}} as'}} - \] + \onslide<2->{as \approx_\alpha^{\text{bn}} as'}} + \]\bigskip + \onslide<1->{\small{}bn-function $\Rightarrow$ \alert{deep binders}} \end{frame}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *} + text_raw {* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \mode{ @@ -859,6 +880,51 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}<1> + \frametitle{\begin{tabular}{c}\LARGE``Raw'' Alpha-Equivalence\end{tabular}} + \mbox{}\\[6mm] + + \begin{center} + LetRec as::assn t::trm \hspace{10mm}\isacommand{bind} bn(as) \isacommand{in} t \alert{as}\\ + \end{center} + + + \[\mbox{}\hspace{-4mm} + \infer[\text{LetRec-}\!\approx_\alpha] + {\text{LetRec}\;as\;t \approx_\alpha \text{LetRec}\;as'\;t'} + {(\text{bn}(as), (t, as)) \approx\!\makebox[0mm][l]{${}_{\text{list}}$} + ^{R,fv} (\text{bn}(as'), (t', as'))} + \]\bigskip + + \onslide<1->{\alert{deep recursive binders}} + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}<1-> + \frametitle{\begin{tabular}{c}Restrictions\end{tabular}} + \mbox{}\\[-6mm] + + Our restrictions on binding specifications: + + \begin{itemize} + \item a body can only occur once in a list of binding clauses\medskip + \item you can only have one binding function for a deep binder\medskip + \item binding functions can return: the empty set, singletons, unions (similarly for lists) + \end{itemize} + + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + text_raw {* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \mode{ @@ -868,7 +934,7 @@ \begin{itemize} \item we can show that $\alpha$'s are equivalence relations\medskip - \item as a result we can use the quotient package to introduce the type(s) + \item as a result we can use our quotient package to introduce the type(s) of $\alpha$-equated terms \[ @@ -881,8 +947,7 @@ \item the properties for support are implied by the properties of $[\_].\_$ - \item we can derive strong induction principles (almost automatic---just a matter of - another week or two) + \item we can derive strong induction principles (almost automatic---matter of time) \end{itemize} @@ -928,7 +993,10 @@ \end{center} \begin{itemize} - \item Core Haskell: 11 types, 49 term-constructors, + \item Core Haskell: 11 types, 49 term-constructors, 7 binding functions + \begin{center} + $\sim$ 1 min + \end{center} \end{itemize} \end{frame}} @@ -992,6 +1060,21 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *} +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}<1->[c] + \frametitle{\begin{tabular}{c}Questions?\end{tabular}} + \mbox{}\\[-6mm] + + \begin{center} + \alert{\huge{Thanks!}} + \end{center} + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + (*<*) end (*>*) \ No newline at end of file