--- 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' ]
--- 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
--- 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) \<approx>gen R f q (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>gen (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"
+ and "(bs, x) \<approx>res R f q (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>res (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"
+ and "(ds, x) \<approx>lst R f q (es, y) \<Longrightarrow> (p \<bullet> ds, p \<bullet> x) \<approx>lst (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> es, p \<bullet> 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) \<approx>gen R f 0 (bs, x)"
+ and "(bs, x) \<approx>res R f 0 (bs, x)"
+ and "(cs, x) \<approx>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 \<bullet> x) y \<Longrightarrow> R (- p \<bullet> y) x"
+ 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)"
+ unfolding alphas fresh_star_def
+ using a
+ by (auto simp add: fresh_minus_perm)
+
+lemma alpha_gen_sym_eqvt:
+ assumes a: "R (p \<bullet> x) y \<Longrightarrow> R y (p \<bullet> x)"
+ 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
+
+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"
+ shows "\<lbrakk>(bs, x) \<approx>gen R f p (cs, y); (cs, y) \<approx>gen R f q (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>gen R f (q + p) (ds, z)"
+ and "\<lbrakk>(bs, x) \<approx>res R f p (cs, y); (cs, y) \<approx>res R f q (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>res R f (q + p) (ds, z)"
+ and "\<lbrakk>(es, x) \<approx>lst R f p (gs, y); (gs, y) \<approx>lst R f q (hs, z)\<rbrakk> \<Longrightarrow> (es, x) \<approx>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) \<approx>gen R f 0 (bs, x)"
- and "(bs, x) \<approx>res R f 0 (bs, x)"
- and "(cs, x) \<approx>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 \<bullet> x) y \<Longrightarrow> R (- p \<bullet> y) x"
- 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)"
- unfolding alphas fresh_star_def
- using a
- by (auto simp add: fresh_minus_perm)
-
-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"
- shows "\<lbrakk>(bs, x) \<approx>gen R f p (cs, y); (cs, y) \<approx>gen R f q (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>gen R f (q + p) (ds, z)"
- and "\<lbrakk>(bs, x) \<approx>res R f p (cs, y); (cs, y) \<approx>res R f q (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>res R f (q + p) (ds, z)"
- and "\<lbrakk>(es, x) \<approx>lst R f p (gs, y); (gs, y) \<approx>lst R f q (hs, z)\<rbrakk> \<Longrightarrow> (es, x) \<approx>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) \<approx>gen R f q (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>gen (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"
- and "(bs, x) \<approx>res R f q (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>res (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"
- and "(ds, x) \<approx>lst R f q (es, y) \<Longrightarrow> (p \<bullet> ds, p \<bullet> x) \<approx>lst (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> es, p \<bullet> 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: "\<And>x y. R y x \<Longrightarrow> f x = f y"
--- 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]
--- 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 \<bullet> x) y \<Longrightarrow> R y (p \<bullet> x)"
+ 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)"
+ 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 \<bullet> alpha_tkind_raw = alpha_tkind_raw"
+and "p \<bullet> alpha_ckind_raw = alpha_ckind_raw"
+and "p \<bullet> alpha_ty_raw = alpha_ty_raw"
+and "p \<bullet> alpha_ty_lst_raw = alpha_ty_lst_raw"
+and "p \<bullet> alpha_co_raw = alpha_co_raw"
+and "p \<bullet> alpha_co_lst_raw = alpha_co_lst_raw"
+and "p \<bullet> alpha_trm_raw = alpha_trm_raw"
+and "p \<bullet> alpha_assoc_lst_raw = alpha_assoc_lst_raw"
+and "p \<bullet> alpha_pat_raw = alpha_pat_raw"
+and "p \<bullet> alpha_vars_raw = alpha_vars_raw"
+and "p \<bullet> alpha_tvars_raw = alpha_tvars_raw"
+and "p \<bullet> alpha_cvars_raw = alpha_cvars_raw"
+and "p \<bullet> alpha_bv_raw = alpha_bv_raw"
+and "p \<bullet> alpha_bv_vs_raw = alpha_bv_vs_raw"
+and "p \<bullet> alpha_bv_tvs_raw = alpha_bv_tvs_raw"
+and "p \<bullet> 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
--- 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
--- 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]
--- 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
--- 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
--- 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 \<bullet> alpha_trm_raw x1 y1 = alpha_trm_raw (p \<bullet> x1) (p \<bullet> y1)"
+ "p \<bullet> alpha_assg_raw x2 y2 = alpha_assg_raw (p \<bullet> x2) (p \<bullet> y2)"
+ "p \<bullet> alpha_bn_raw x3 y3 = alpha_bn_raw (p \<bullet> x3) (p \<bullet> 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: "\<exists>(q :: perm). P q \<Longrightarrow> \<exists>q. Q q \<Longrightarrow> (\<And>p q. P p \<Longrightarrow> Q q \<Longrightarrow> R (p + q)) \<Longrightarrow> \<exists>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) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> (\<forall>x. R x2 x \<longrightarrow> R x1 x)) f pi (bs, s)"
+ shows "(\<forall>x. R s x \<longrightarrow> R (pi \<bullet> t) x)"
+ using b
+ by (simp add: alphas)
+
+lemma test:
+ assumes b: "(as, t) \<approx>gen R f pi (bs, s)"
+ shows "R (pi \<bullet> t) s"
+ using b
+ by (simp add: alphas)
+
+lemma alpha_gen_trans_eqvt:
+ assumes a: "(bs, x) \<approx>gen R f p (cs, y)" and a1: "(cs, y) \<approx>gen R f q (ds, z)"
+ and b: "\<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)"
+ sorry
+
+
+lemma
+ "alpha_trm_raw x1 y1 \<Longrightarrow> (\<And>z1. alpha_trm_raw y1 z1 \<Longrightarrow> alpha_trm_raw x1 z1)"
+ "alpha_assg_raw x2 y2 \<Longrightarrow> (\<And>z2. alpha_assg_raw y2 z2 \<Longrightarrow> alpha_assg_raw x2 z2)"
+ "alpha_bn_raw x3 y3 \<Longrightarrow> (\<And>z3. alpha_bn_raw y3 z3 \<Longrightarrow> 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 \<bullet> 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
--- 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
--- 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 *)
--- 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
--- 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<presentation>{
- \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<presentation>{
- \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<presentation>{
\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<presentation>{
@@ -859,6 +880,51 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \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<presentation>{
+ \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<presentation>{
@@ -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<presentation>{
+ \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