# HG changeset patch # User Cezary Kaliszyk # Date 1269620537 -3600 # Node ID d1293d30c65753a155d947ba5c137a0de2b5cb47 # Parent 758904445fb281bbb4fa8ed251f38e095204a3cf# Parent aacab5f67333e69fab9fef00f1e1cd75e401f596 merge diff -r 758904445fb2 -r d1293d30c657 Nominal/Abs.thy --- a/Nominal/Abs.thy Fri Mar 26 17:22:02 2010 +0100 +++ b/Nominal/Abs.thy Fri Mar 26 17:22:17 2010 +0100 @@ -51,145 +51,187 @@ by (case_tac [!] bs, case_tac [!] cs) (auto simp add: le_fun_def le_bool_def alphas) -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)" - using a - unfolding alphas - unfolding fresh_star_def - 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 - unfolding fresh_star_def - by (simp_all add: fresh_plus_perm) - -lemma alpha_gen_eqvt: - assumes a: "R (q \ x) y \ R (p \ (q \ x)) (p \ y)" - and b: "p \ (f x) = f (p \ x)" - and c: "p \ (f y) = f (p \ y)" - shows "(bs, x) \gen R f q (cs, y) \ (p \ bs, p \ x) \gen R f (p \ q) (p \ cs, p \ y)" - and "(bs, x) \res R f q (cs, y) \ (p \ bs, p \ x) \res R f (p \ q) (p \ cs, p \ y)" - and "(ds, x) \lst R f q (es, y) \ (p \ ds, p \ x) \lst R f (p \ q) (p \ es, p \ y)" - unfolding alphas - unfolding set_eqvt[symmetric] - unfolding b[symmetric] c[symmetric] - unfolding Diff_eqvt[symmetric] - unfolding permute_eqvt[symmetric] - using a - by (auto simp add: fresh_star_permute_iff) - fun alpha_abs where "alpha_abs (bs, x) (cs, y) \ (\p. (bs, x) \gen (op=) supp p (cs, y))" +fun + alpha_abs_lst +where + "alpha_abs_lst (bs, x) (cs, y) \ (\p. (bs, x) \lst (op=) supp p (cs, y))" + +fun + alpha_abs_res +where + "alpha_abs_res (bs, x) (cs, y) \ (\p. (bs, x) \res (op=) supp p (cs, y))" + notation - alpha_abs ("_ \abs _") + alpha_abs ("_ \abs _") and + alpha_abs_lst ("_ \abs'_lst _") and + alpha_abs_res ("_ \abs'_res _") + +lemmas alphas_abs = alpha_abs.simps alpha_abs_res.simps alpha_abs_lst.simps + +lemma alphas_abs_refl: + shows "(bs, x) \abs (bs, x)" + and "(bs, x) \abs_res (bs, x)" + and "(cs, x) \abs_lst (cs, x)" + unfolding alphas_abs + unfolding alphas + unfolding fresh_star_def + by (rule_tac [!] x="0" in exI) + (simp_all add: fresh_zero_perm) + +lemma alphas_abs_sym: + shows "(bs, x) \abs (cs, y) \ (cs, y) \abs (bs, x)" + and "(bs, x) \abs_res (cs, y) \ (cs, y) \abs_res (bs, x)" + and "(ds, x) \abs_lst (es, y) \ (es, y) \abs_lst (ds, x)" + unfolding alphas_abs + unfolding alphas + unfolding fresh_star_def + by (erule_tac [!] exE, rule_tac [!] x="-p" in exI) + (auto simp add: fresh_minus_perm) -lemma alpha_abs_swap: +lemma alphas_abs_trans: + shows "\(bs, x) \abs (cs, y); (cs, y) \abs (ds, z)\ \ (bs, x) \abs (ds, z)" + and "\(bs, x) \abs_res (cs, y); (cs, y) \abs_res (ds, z)\ \ (bs, x) \abs_res (ds, z)" + and "\(es, x) \abs_lst (gs, y); (gs, y) \abs_lst (hs, z)\ \ (es, x) \abs_lst (hs, z)" + unfolding alphas_abs + unfolding alphas + unfolding fresh_star_def + apply(erule_tac [!] exE, erule_tac [!] exE) + apply(rule_tac [!] x="pa + p" in exI) + by (simp_all add: fresh_plus_perm) + +lemma alphas_abs_eqvt: + shows "(bs, x) \abs (cs, y) \ (p \ bs, p \ x) \abs (p \ cs, p \ y)" + and "(bs, x) \abs_res (cs, y) \ (p \ bs, p \ x) \abs_res (p \ cs, p \ y)" + and "(ds, x) \abs_lst (es, y) \ (p \ ds, p \ x) \abs_lst (p \ es, p \ y)" + unfolding alphas_abs + unfolding alphas + unfolding set_eqvt[symmetric] + unfolding supp_eqvt[symmetric] + unfolding Diff_eqvt[symmetric] + apply(erule_tac [!] exE) + apply(rule_tac [!] x="p \ pa" in exI) + by (auto simp add: fresh_star_permute_iff permute_eqvt[symmetric]) + +lemma alphas_abs_swap1: assumes a1: "a \ (supp x) - bs" and a2: "b \ (supp x) - bs" shows "(bs, x) \abs ((a \ b) \ bs, (a \ b) \ x)" + and "(bs, x) \abs_res ((a \ b) \ bs, (a \ b) \ x)" using a1 a2 - unfolding Diff_iff - unfolding alpha_abs.simps + unfolding alphas_abs unfolding alphas - unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric] + unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric] unfolding fresh_star_def fresh_def unfolding swap_set_not_in[OF a1 a2] - by (rule_tac x="(a \ b)" in exI) + by (rule_tac [!] x="(a \ b)" in exI) + (auto simp add: supp_perm swap_atom) + +lemma alphas_abs_swap2: + assumes a1: "a \ (supp x) - (set bs)" + and a2: "b \ (supp x) - (set bs)" + shows "(bs, x) \abs_lst ((a \ b) \ bs, (a \ b) \ x)" + using a1 a2 + unfolding alphas_abs + unfolding alphas + unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric] set_eqvt[symmetric] + unfolding fresh_star_def fresh_def + unfolding swap_set_not_in[OF a1 a2] + by (rule_tac [!] x="(a \ b)" in exI) (auto simp add: supp_perm swap_atom) fun - supp_abs_fun + aux_set +where + "aux_set (bs, x) = (supp x) - bs" + +fun + aux_list where - "supp_abs_fun (bs, x) = (supp x) - bs" + "aux_list (cs, x) = (supp x) - (set cs)" +lemma aux_abs_lemma: + assumes a: "(bs, x) \abs (cs, y)" + shows "aux_set (bs, x) = aux_set (cs, y)" + using a + by (induct rule: alpha_abs.induct) + (simp add: alphas_abs alphas) -lemma supp_abs_fun_lemma: - assumes a: "x \abs y" - shows "supp_abs_fun x = supp_abs_fun y" +lemma aux_abs_res_lemma: + assumes a: "(bs, x) \abs_res (cs, y)" + shows "aux_set (bs, x) = aux_set (cs, y)" using a - apply(induct rule: alpha_abs.induct) - apply(simp add: alpha_gen) - done - + by (induct rule: alpha_abs_res.induct) + (simp add: alphas_abs alphas) + +lemma aux_abs_list_lemma: + assumes a: "(bs, x) \abs_lst (cs, y)" + shows "aux_list (bs, x) = aux_list (cs, y)" + using a + by (induct rule: alpha_abs_lst.induct) + (simp add: alphas_abs alphas) -quotient_type 'a abs_gen = "(atom set \ 'a::pt)" / "alpha_abs" - apply(rule equivpI) +quotient_type + 'a abs_gen = "(atom set \ 'a::pt)" / "alpha_abs" +and 'b abs_res = "(atom set \ 'b::pt)" / "alpha_abs_res" +and 'c abs_lst = "(atom list \ 'c::pt)" / "alpha_abs_lst" + apply(rule_tac [!] equivpI) unfolding reflp_def symp_def transp_def - apply(simp_all) - (* refl *) - apply(clarify) - apply(rule_tac x="0" in exI) - apply(rule alpha_gen_refl) - apply(simp) - (* symm *) - apply(clarify) - apply(rule_tac x="- p" in exI) - apply(rule alpha_gen_sym) - apply(clarsimp) - apply(assumption) - (* trans *) - apply(clarify) - apply(rule_tac x="pa + p" in exI) - apply(rule alpha_gen_trans) - apply(auto) - done + by (auto intro: alphas_abs_sym alphas_abs_refl alphas_abs_trans simp only:) quotient_definition "Abs::atom set \ ('a::pt) \ 'a abs_gen" is "Pair::atom set \ ('a::pt) \ (atom set \ 'a)" +quotient_definition + "Abs_res::atom set \ ('a::pt) \ 'a abs_res" +is + "Pair::atom set \ ('a::pt) \ (atom set \ 'a)" + +quotient_definition + "Abs_lst::atom list \ ('a::pt) \ 'a abs_lst" +is + "Pair::atom list \ ('a::pt) \ (atom list \ 'a)" + lemma [quot_respect]: - shows "((op =) ===> (op =) ===> alpha_abs) Pair Pair" - apply(clarsimp) - apply(rule exI) - apply(rule alpha_gen_refl) - apply(simp) - done + shows "(op= ===> op= ===> alpha_abs) Pair Pair" + and "(op= ===> op= ===> alpha_abs_res) Pair Pair" + and "(op= ===> op= ===> alpha_abs_lst) Pair Pair" + unfolding fun_rel_def + by (auto intro: alphas_abs_refl simp only:) lemma [quot_respect]: - shows "((op =) ===> alpha_abs ===> alpha_abs) permute permute" - apply(clarsimp) - apply(rule exI) - apply(rule alpha_gen_eqvt) - apply(simp_all add: supp_eqvt) - done + shows "(op= ===> alpha_abs ===> alpha_abs) permute permute" + and "(op= ===> alpha_abs_res ===> alpha_abs_res) permute permute" + and "(op= ===> alpha_abs_lst ===> alpha_abs_lst) permute permute" + unfolding fun_rel_def + by (auto intro: alphas_abs_eqvt simp only: Pair_eqvt) lemma [quot_respect]: - shows "(alpha_abs ===> (op =)) supp_abs_fun supp_abs_fun" - apply(simp add: supp_abs_fun_lemma) - done + shows "(alpha_abs ===> op=) aux_set aux_set" + and "(alpha_abs_res ===> op=) aux_set aux_set" + and "(alpha_abs_lst ===> op=) aux_list aux_list" + unfolding fun_rel_def + apply(rule_tac [!] allI) + apply(rule_tac [!] allI) + apply(case_tac [!] x, case_tac [!] y) + apply(rule_tac [!] impI) + by (simp_all only: aux_abs_lemma aux_abs_res_lemma aux_abs_list_lemma) -lemma abs_induct: - "\\as (x::'a::pt). P (Abs as x)\ \ P t" +lemma abs_inducts: + shows "(\as (x::'a::pt). P1 (Abs as x)) \ P1 x1" + and "(\as (x::'a::pt). P2 (Abs_res as x)) \ P2 x2" + and "(\as (x::'a::pt). P3 (Abs_lst as x)) \ P3 x3" apply(lifting prod.induct[where 'a="atom set" and 'b="'a"]) + apply(lifting prod.induct[where 'a="atom set" and 'b="'a"]) + apply(lifting prod.induct[where 'a="atom list" and 'b="'a"]) done -(* TEST case *) -lemmas abs_induct2 = prod.induct[where 'a="atom set" and 'b="'a::pt", quot_lifted] -thm abs_induct abs_induct2 - instantiation abs_gen :: (pt) pt begin @@ -198,351 +240,206 @@ is "permute:: perm \ (atom set \ 'a::pt) \ (atom set \ 'a::pt)" -(* ??? has to be 'a \ 'b does not work *) -lemma permute_ABS [simp]: +lemma permute_Abs[simp]: fixes x::"'a::pt" shows "(p \ (Abs as x)) = Abs (p \ as) (p \ x)" - thm permute_prod.simps - by (lifting permute_prod.simps(1)[where 'a="atom set" and 'b="'a"]) + by (lifting permute_prod.simps[where 'a="atom set" and 'b="'a"]) instance apply(default) - apply(induct_tac [!] x rule: abs_induct) + apply(induct_tac [!] x rule: abs_inducts(1)) + apply(simp_all) + done + +end + +instantiation abs_res :: (pt) pt +begin + +quotient_definition + "permute_abs_res::perm \ ('a::pt abs_res) \ 'a abs_res" +is + "permute:: perm \ (atom set \ 'a::pt) \ (atom set \ 'a::pt)" + +lemma permute_Abs_res[simp]: + fixes x::"'a::pt" + shows "(p \ (Abs_res as x)) = Abs_res (p \ as) (p \ x)" + by (lifting permute_prod.simps[where 'a="atom set" and 'b="'a"]) + +instance + apply(default) + apply(induct_tac [!] x rule: abs_inducts(2)) + apply(simp_all) + done + +end + +instantiation abs_lst :: (pt) pt +begin + +quotient_definition + "permute_abs_lst::perm \ ('a::pt abs_lst) \ 'a abs_lst" +is + "permute:: perm \ (atom list \ 'a::pt) \ (atom list \ 'a::pt)" + +lemma permute_Abs_lst[simp]: + fixes x::"'a::pt" + shows "(p \ (Abs_lst as x)) = Abs_lst (p \ as) (p \ x)" + by (lifting permute_prod.simps[where 'a="atom list" and 'b="'a"]) + +instance + apply(default) + apply(induct_tac [!] x rule: abs_inducts(3)) apply(simp_all) done end +lemmas permute_abs = permute_Abs permute_Abs_res permute_Abs_lst + + quotient_definition - "supp_Abs_fun :: ('a::pt) abs_gen \ atom \ bool" + "supp_gen :: ('a::pt) abs_gen \ atom set" is - "supp_abs_fun" + "aux_set" + +quotient_definition + "supp_res :: ('a::pt) abs_res \ atom set" +is + "aux_set" -lemma supp_Abs_fun_simp: - shows "supp_Abs_fun (Abs bs x) = (supp x) - bs" - by (lifting supp_abs_fun.simps(1)) +quotient_definition + "supp_lst :: ('a::pt) abs_lst \ atom set" +is + "aux_list" -lemma supp_Abs_fun_eqvt [eqvt]: - shows "(p \ supp_Abs_fun x) = supp_Abs_fun (p \ x)" - apply(induct_tac x rule: abs_induct) - apply(simp add: supp_Abs_fun_simp supp_eqvt Diff_eqvt) +lemma aux_supps: + shows "supp_gen (Abs bs x) = (supp x) - bs" + and "supp_res (Abs_res bs x) = (supp x) - bs" + and "supp_lst (Abs_lst cs x) = (supp x) - (set cs)" + apply(lifting aux_set.simps) + apply(lifting aux_set.simps) + apply(lifting aux_list.simps) done -lemma supp_Abs_fun_fresh: - shows "a \ Abs bs x \ a \ supp_Abs_fun (Abs bs x)" - apply(rule fresh_fun_eqvt_app) - apply(simp add: eqvts_raw) - apply(simp) +lemma aux_supp_eqvt[eqvt]: + shows "(p \ supp_gen x) = supp_gen (p \ x)" + and "(p \ supp_res y) = supp_res (p \ y)" + and "(p \ supp_lst z) = supp_lst (p \ z)" + apply(induct_tac x rule: abs_inducts(1)) + apply(simp add: aux_supps supp_eqvt Diff_eqvt) + apply(induct_tac y rule: abs_inducts(2)) + apply(simp add: aux_supps supp_eqvt Diff_eqvt) + apply(induct_tac z rule: abs_inducts(3)) + apply(simp add: aux_supps supp_eqvt Diff_eqvt set_eqvt) done -lemma Abs_swap: +lemma aux_fresh: + shows "a \ Abs bs x \ a \ supp_gen (Abs bs x)" + and "a \ Abs_res bs x \ a \ supp_res (Abs_res bs x)" + and "a \ Abs_lst cs x \ a \ supp_lst (Abs_lst cs x)" + apply(rule_tac [!] fresh_fun_eqvt_app) + apply(simp_all add: eqvts_raw) + done + +lemma abs_swap1: assumes a1: "a \ (supp x) - bs" and a2: "b \ (supp x) - bs" - shows "(Abs bs x) = (Abs ((a \ b) \ bs) ((a \ b) \ x))" - using a1 a2 by (lifting alpha_abs_swap) - -lemma Abs_supports: - shows "((supp x) - as) supports (Abs as x)" - unfolding supports_def - apply(clarify) - apply(simp (no_asm)) - apply(subst Abs_swap[symmetric]) - apply(simp_all) + shows "Abs bs x = Abs ((a \ b) \ bs) ((a \ b) \ x)" + and "Abs_res bs x = Abs_res ((a \ b) \ bs) ((a \ b) \ x)" + using a1 a2 + apply(lifting alphas_abs_swap1(1)) + apply(lifting alphas_abs_swap1(2)) done -lemma finite_supp_Abs_subset1: - assumes "finite (supp x)" +lemma abs_swap2: + assumes a1: "a \ (supp x) - (set bs)" + and a2: "b \ (supp x) - (set bs)" + shows "Abs_lst bs x = Abs_lst ((a \ b) \ bs) ((a \ b) \ x)" + using a1 a2 by (lifting alphas_abs_swap2) + +lemma abs_supports: + shows "((supp x) - as) supports (Abs as x)" + and "((supp x) - as) supports (Abs_res as x)" + and "((supp x) - (set bs)) supports (Abs_lst bs x)" + unfolding supports_def + unfolding permute_abs + by (simp_all add: abs_swap1[symmetric] abs_swap2[symmetric]) + +lemma supp_abs_subset1: + assumes a: "finite (supp x)" shows "(supp x) - as \ supp (Abs as x)" - apply(simp add: supp_conv_fresh) - apply(auto) - apply(drule_tac supp_Abs_fun_fresh) - apply(simp only: supp_Abs_fun_simp) - apply(simp add: fresh_def) - apply(simp add: supp_finite_atom_set assms) + and "(supp x) - as \ supp (Abs_res as x)" + and "(supp x) - (set bs) \ supp (Abs_lst bs x)" + unfolding supp_conv_fresh + apply(auto dest!: aux_fresh simp add: aux_supps) + apply(simp_all add: fresh_def supp_finite_atom_set a) done -lemma finite_supp_Abs_subset2: - assumes "finite (supp x)" +lemma supp_abs_subset2: + assumes a: "finite (supp x)" shows "supp (Abs as x) \ (supp x) - as" - apply(rule supp_is_subset) - apply(rule Abs_supports) - apply(simp add: assms) + and "supp (Abs_res as x) \ (supp x) - as" + and "supp (Abs_lst bs x) \ (supp x) - (set bs)" + apply(rule_tac [!] supp_is_subset) + apply(simp_all add: abs_supports a) done -lemma finite_supp_Abs: - assumes "finite (supp x)" +lemma abs_finite_supp: + assumes a: "finite (supp x)" shows "supp (Abs as x) = (supp x) - as" - apply(rule_tac subset_antisym) - apply(rule finite_supp_Abs_subset2[OF assms]) - apply(rule finite_supp_Abs_subset1[OF assms]) + and "supp (Abs_res as x) = (supp x) - as" + and "supp (Abs_lst bs x) = (supp x) - (set bs)" + apply(rule_tac [!] subset_antisym) + apply(simp_all add: supp_abs_subset1[OF a] supp_abs_subset2[OF a]) done -lemma supp_Abs: +lemma supp_abs: fixes x::"'a::fs" shows "supp (Abs as x) = (supp x) - as" - apply(rule finite_supp_Abs) - apply(simp add: finite_supp) + and "supp (Abs_res as x) = (supp x) - as" + and "supp (Abs_lst bs x) = (supp x) - (set bs)" + apply(rule_tac [!] abs_finite_supp) + apply(simp_all add: finite_supp) done instance abs_gen :: (fs) fs apply(default) - apply(induct_tac x rule: abs_induct) - apply(simp add: supp_Abs) - apply(simp add: finite_supp) + apply(induct_tac x rule: abs_inducts(1)) + apply(simp add: supp_abs finite_supp) done -lemma Abs_fresh_iff: - fixes x::"'a::fs" - shows "a \ Abs bs x \ a \ bs \ (a \ bs \ a \ x)" - apply(simp add: fresh_def) - apply(simp add: supp_Abs) - apply(auto) +instance abs_res :: (fs) fs + apply(default) + apply(induct_tac x rule: abs_inducts(2)) + apply(simp add: supp_abs finite_supp) + done + +instance abs_lst :: (fs) fs + apply(default) + apply(induct_tac x rule: abs_inducts(3)) + apply(simp add: supp_abs finite_supp) done -lemma Abs_eq_iff: - shows "Abs bs x = Abs cs y \ (\p. (bs, x) \gen (op =) supp p (cs, y))" - by (lifting alpha_abs.simps(1)) - - - -(* - below is a construction site for showing that in the - single-binder case, the old and new alpha equivalence - coincide -*) - -fun - alpha1 -where - "alpha1 (a, x) (b, y) \ (a = b \ x = y) \ (a \ b \ x = (a \ b) \ y \ a \ y)" - -notation - alpha1 ("_ \abs1 _") - -fun - alpha2 -where - "alpha2 (a, x) (b, y) \ (\c. c \ (a,b,x,y) \ ((c \ a) \ x) = ((c \ b) \ y))" - -notation - alpha2 ("_ \abs2 _") +lemma abs_fresh_iff: + fixes x::"'a::fs" + shows "a \ Abs bs x \ a \ bs \ (a \ bs \ a \ x)" + and "a \ Abs_res bs x \ a \ bs \ (a \ bs \ a \ x)" + and "a \ Abs_lst cs x \ a \ (set cs) \ (a \ (set cs) \ a \ x)" + unfolding fresh_def + unfolding supp_abs + by auto -lemma alpha_old_new: - assumes a: "(a, x) \abs1 (b, y)" "sort_of a = sort_of b" - shows "({a}, x) \abs ({b}, y)" -using a -apply(simp) -apply(erule disjE) -apply(simp) -apply(rule exI) -apply(rule alpha_gen_refl) -apply(simp) -apply(rule_tac x="(a \ b)" in exI) -apply(simp add: alpha_gen) -apply(simp add: fresh_def) -apply(rule conjI) -apply(rule_tac ?p1="(a \ b)" in permute_eq_iff[THEN iffD1]) -apply(rule trans) -apply(simp add: Diff_eqvt supp_eqvt) -apply(subst swap_set_not_in) -back -apply(simp) -apply(simp) -apply(simp add: permute_set_eq) -apply(rule conjI) -apply(rule_tac ?p1="(a \ b)" in fresh_star_permute_iff[THEN iffD1]) -apply(simp add: permute_self) -apply(simp add: Diff_eqvt supp_eqvt) -apply(simp add: permute_set_eq) -apply(subgoal_tac "supp (a \ b) \ {a, b}") -apply(simp add: fresh_star_def fresh_def) -apply(blast) -apply(simp add: supp_swap) -apply(simp add: eqvts) -done - - -lemma perm_induct_test: - fixes P :: "perm => bool" - assumes fin: "finite (supp p)" - assumes zero: "P 0" - assumes swap: "\a b. \sort_of a = sort_of b; a \ b\ \ P (a \ b)" - assumes plus: "\p1 p2. \supp p1 \ supp p2 = {}; P p1; P p2\ \ P (p1 + p2)" - shows "P p" -using fin -apply(induct F\"supp p" arbitrary: p rule: finite_induct) -oops - -lemma ii: - assumes "\x \ A. p \ x = x" - shows "p \ A = A" -using assms -apply(auto) -apply (metis Collect_def Collect_mem_eq Int_absorb assms eqvt_bound inf_Int_eq mem_def mem_permute_iff) -apply (metis Collect_def Collect_mem_eq Int_absorb assms eqvt_apply eqvt_bound eqvt_lambda inf_Int_eq mem_def mem_permute_iff permute_minus_cancel(2) permute_pure) -done - - - -lemma alpha_abs_Pair: - shows "(bs, (x1, x2)) \gen (\(x1,x2) (y1,y2). x1=y1 \ x2=y2) (\(x,y). supp x \ supp y) p (cs, (y1, y2)) - \ ((bs, x1) \gen (op=) supp p (cs, y1) \ (bs, x2) \gen (op=) supp p (cs, y2))" - apply(simp add: alpha_gen) - apply(simp add: fresh_star_def) - apply(simp add: ball_Un Un_Diff) - apply(rule iffI) - apply(simp) - defer - apply(simp) - apply(rule conjI) - apply(clarify) - apply(simp add: supp_eqvt[symmetric] Diff_eqvt[symmetric]) - apply(rule sym) - apply(rule ii) - apply(simp add: fresh_def supp_perm) - apply(clarify) - apply(simp add: supp_eqvt[symmetric] Diff_eqvt[symmetric]) - apply(simp add: fresh_def supp_perm) - apply(rule sym) - apply(rule ii) - apply(simp) +lemma abs_eq_iff: + shows "Abs bs x = Abs cs y \ (bs, x) \abs (cs, y)" + and "Abs_res bs x = Abs_res cs y \ (bs, x) \abs_res (cs, y)" + and "Abs_lst ds x = Abs_lst hs y \ (ds, x) \abs_lst (hs, y)" + apply(simp_all) + apply(lifting alphas_abs) done -lemma yy: - assumes "S1 - {x} = S2 - {x}" "x \ S1" "x \ S2" - shows "S1 = S2" -using assms -apply (metis insert_Diff_single insert_absorb) -done - -lemma kk: - assumes a: "p \ x = y" - shows "\a \ supp x. (p \ a) \ supp y" -using a -apply(auto) -apply(rule_tac p="- p" in permute_boolE) -apply(simp add: mem_eqvt supp_eqvt) -done - -lemma ww: - assumes "a \ supp x" "b \ supp x" "a \ b" "sort_of a = sort_of b" - shows "((a \ b) \ x) \ x" -apply(subgoal_tac "(supp x) supports x") -apply(simp add: supports_def) -using assms -apply - -apply(drule_tac x="a" in spec) -defer -apply(rule supp_supports) -apply(auto) -apply(rotate_tac 1) -apply(drule_tac p="(a \ b)" in permute_boolI) -apply(simp add: mem_eqvt supp_eqvt) -done - -lemma alpha_abs_sym: - assumes a: "({a}, x) \abs ({b}, y)" - shows "({b}, y) \abs ({a}, x)" -using a -apply(simp) -apply(erule exE) -apply(rule_tac x="- p" in exI) -apply(simp add: alpha_gen) -apply(simp add: fresh_star_def fresh_minus_perm) -apply (metis permute_minus_cancel(2)) -done - -lemma alpha_abs_trans: - assumes a: "({a1}, x1) \abs ({a2}, x2)" - assumes b: "({a2}, x2) \abs ({a3}, x3)" - shows "({a1}, x1) \abs ({a3}, x3)" -using a b -apply(simp) -apply(erule exE)+ -apply(rule_tac x="pa + p" in exI) -apply(simp add: alpha_gen) -apply(simp add: fresh_star_def fresh_plus_perm) -done - -lemma alpha_equal: - assumes a: "({a}, x) \abs ({a}, y)" - shows "(a, x) \abs1 (a, y)" -using a -apply(simp) -apply(erule exE) -apply(simp add: alpha_gen) -apply(erule conjE)+ -apply(case_tac "a \ supp x") -apply(simp) -apply(subgoal_tac "supp x \* p") -apply(drule supp_perm_eq) -apply(simp) -apply(simp) -apply(simp) -apply(case_tac "a \ supp y") -apply(simp) -apply(drule supp_perm_eq) -apply(clarify) -apply(simp (no_asm_use)) -apply(simp) -apply(simp) -apply(drule yy) -apply(simp) -apply(simp) -apply(simp) -apply(case_tac "a \ p") -apply(subgoal_tac "supp y \* p") -apply(drule supp_perm_eq) -apply(clarify) -apply(simp (no_asm_use)) -apply(metis) -apply(auto simp add: fresh_star_def)[1] -apply(frule_tac kk) -apply(drule_tac x="a" in bspec) -apply(simp) -apply(simp add: fresh_def) -apply(simp add: supp_perm) -apply(subgoal_tac "((p \ a) \ p)") -apply(simp add: fresh_def supp_perm) -apply(simp add: fresh_star_def) -done - -lemma alpha_unequal: - assumes a: "({a}, x) \abs ({b}, y)" "sort_of a = sort_of b" "a \ b" - shows "(a, x) \abs1 (b, y)" -using a -apply - -apply(subgoal_tac "a \ supp x - {a}") -apply(subgoal_tac "b \ supp x - {a}") -defer -apply(simp add: alpha_gen) -apply(simp) -apply(drule_tac alpha_abs_swap) -apply(assumption) -apply(simp only: insert_eqvt empty_eqvt swap_atom_simps) -apply(drule alpha_abs_sym) -apply(rotate_tac 4) -apply(drule_tac alpha_abs_trans) -apply(assumption) -apply(drule alpha_equal) -apply(simp) -apply(rule_tac p="(a \ b)" in permute_boolE) -apply(simp add: fresh_eqvt) -apply(simp add: fresh_def) -done - -lemma alpha_new_old: - assumes a: "({a}, x) \abs ({b}, y)" "sort_of a = sort_of b" - shows "(a, x) \abs1 (b, y)" -using a -apply(case_tac "a=b") -apply(simp only: alpha_equal) -apply(drule alpha_unequal) -apply(simp) -apply(simp) -apply(simp) -done +section {* BELOW is stuff that may or may not be needed *} (* support of concrete atom sets *) @@ -563,6 +460,12 @@ done (* TODO: The following lemmas can be moved somewhere... *) + +lemma Abs_eq_iff: + shows "Abs bs x = Abs cs y \ (\p. (bs, x) \gen (op =) supp p (cs, y))" + by (lifting alpha_abs.simps(1)) + + lemma split_rsp2[quot_respect]: "((R1 ===> R2 ===> prod_rel R1 R2 ===> op =) ===> prod_rel R1 R2 ===> prod_rel R1 R2 ===> op =) split split" by auto @@ -673,5 +576,51 @@ apply(simp) done +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)" + using a + unfolding alphas + unfolding fresh_star_def + 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 + unfolding fresh_star_def + by (simp_all add: fresh_plus_perm) + +lemma alpha_gen_eqvt: + assumes a: "R (q \ x) y \ R (p \ (q \ x)) (p \ y)" + and b: "p \ (f x) = f (p \ x)" + and c: "p \ (f y) = f (p \ y)" + shows "(bs, x) \gen R f q (cs, y) \ (p \ bs, p \ x) \gen R f (p \ q) (p \ cs, p \ y)" + and "(bs, x) \res R f q (cs, y) \ (p \ bs, p \ x) \res R f (p \ q) (p \ cs, p \ y)" + and "(ds, x) \lst R f q (es, y) \ (p \ ds, p \ x) \lst R f (p \ q) (p \ es, p \ y)" + unfolding alphas + unfolding set_eqvt[symmetric] + unfolding b[symmetric] c[symmetric] + unfolding Diff_eqvt[symmetric] + unfolding permute_eqvt[symmetric] + using a + by (auto simp add: fresh_star_permute_iff) + + end diff -r 758904445fb2 -r d1293d30c657 Nominal/Abs_equiv.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/Abs_equiv.thy Fri Mar 26 17:22:17 2010 +0100 @@ -0,0 +1,244 @@ +theory Abs_equiv +imports Abs +begin + +(* + below is a construction site for showing that in the + single-binder case, the old and new alpha equivalence + coincide +*) + +fun + alpha1 +where + "alpha1 (a, x) (b, y) \ (a = b \ x = y) \ (a \ b \ x = (a \ b) \ y \ a \ y)" + +notation + alpha1 ("_ \abs1 _") + +fun + alpha2 +where + "alpha2 (a, x) (b, y) \ (\c. c \ (a,b,x,y) \ ((c \ a) \ x) = ((c \ b) \ y))" + +notation + alpha2 ("_ \abs2 _") + +lemma alpha_old_new: + assumes a: "(a, x) \abs1 (b, y)" "sort_of a = sort_of b" + shows "({a}, x) \abs ({b}, y)" +using a +apply(simp) +apply(erule disjE) +apply(simp) +apply(rule exI) +apply(rule alpha_gen_refl) +apply(simp) +apply(rule_tac x="(a \ b)" in exI) +apply(simp add: alpha_gen) +apply(simp add: fresh_def) +apply(rule conjI) +apply(rule_tac ?p1="(a \ b)" in permute_eq_iff[THEN iffD1]) +apply(rule trans) +apply(simp add: Diff_eqvt supp_eqvt) +apply(subst swap_set_not_in) +back +apply(simp) +apply(simp) +apply(simp add: permute_set_eq) +apply(rule conjI) +apply(rule_tac ?p1="(a \ b)" in fresh_star_permute_iff[THEN iffD1]) +apply(simp add: permute_self) +apply(simp add: Diff_eqvt supp_eqvt) +apply(simp add: permute_set_eq) +apply(subgoal_tac "supp (a \ b) \ {a, b}") +apply(simp add: fresh_star_def fresh_def) +apply(blast) +apply(simp add: supp_swap) +apply(simp add: eqvts) +done + + +lemma perm_induct_test: + fixes P :: "perm => bool" + assumes fin: "finite (supp p)" + assumes zero: "P 0" + assumes swap: "\a b. \sort_of a = sort_of b; a \ b\ \ P (a \ b)" + assumes plus: "\p1 p2. \supp p1 \ supp p2 = {}; P p1; P p2\ \ P (p1 + p2)" + shows "P p" +using fin +apply(induct F\"supp p" arbitrary: p rule: finite_induct) +oops + +lemma ii: + assumes "\x \ A. p \ x = x" + shows "p \ A = A" +using assms +apply(auto) +apply (metis Collect_def Collect_mem_eq Int_absorb assms eqvt_bound inf_Int_eq mem_def mem_permute_iff) +apply (metis Collect_def Collect_mem_eq Int_absorb assms eqvt_apply eqvt_bound eqvt_lambda inf_Int_eq mem_def mem_permute_iff permute_minus_cancel(2) permute_pure) +done + + + +lemma alpha_abs_Pair: + shows "(bs, (x1, x2)) \gen (\(x1,x2) (y1,y2). x1=y1 \ x2=y2) (\(x,y). supp x \ supp y) p (cs, (y1, y2)) + \ ((bs, x1) \gen (op=) supp p (cs, y1) \ (bs, x2) \gen (op=) supp p (cs, y2))" + apply(simp add: alpha_gen) + apply(simp add: fresh_star_def) + apply(simp add: ball_Un Un_Diff) + apply(rule iffI) + apply(simp) + defer + apply(simp) + apply(rule conjI) + apply(clarify) + apply(simp add: supp_eqvt[symmetric] Diff_eqvt[symmetric]) + apply(rule sym) + apply(rule ii) + apply(simp add: fresh_def supp_perm) + apply(clarify) + apply(simp add: supp_eqvt[symmetric] Diff_eqvt[symmetric]) + apply(simp add: fresh_def supp_perm) + apply(rule sym) + apply(rule ii) + apply(simp) + done + + +lemma yy: + assumes "S1 - {x} = S2 - {x}" "x \ S1" "x \ S2" + shows "S1 = S2" +using assms +apply (metis insert_Diff_single insert_absorb) +done + +lemma kk: + assumes a: "p \ x = y" + shows "\a \ supp x. (p \ a) \ supp y" +using a +apply(auto) +apply(rule_tac p="- p" in permute_boolE) +apply(simp add: mem_eqvt supp_eqvt) +done + +lemma ww: + assumes "a \ supp x" "b \ supp x" "a \ b" "sort_of a = sort_of b" + shows "((a \ b) \ x) \ x" +apply(subgoal_tac "(supp x) supports x") +apply(simp add: supports_def) +using assms +apply - +apply(drule_tac x="a" in spec) +defer +apply(rule supp_supports) +apply(auto) +apply(rotate_tac 1) +apply(drule_tac p="(a \ b)" in permute_boolI) +apply(simp add: mem_eqvt supp_eqvt) +done + +lemma alpha_abs_sym: + assumes a: "({a}, x) \abs ({b}, y)" + shows "({b}, y) \abs ({a}, x)" +using a +apply(simp) +apply(erule exE) +apply(rule_tac x="- p" in exI) +apply(simp add: alpha_gen) +apply(simp add: fresh_star_def fresh_minus_perm) +apply (metis permute_minus_cancel(2)) +done + +lemma alpha_abs_trans: + assumes a: "({a1}, x1) \abs ({a2}, x2)" + assumes b: "({a2}, x2) \abs ({a3}, x3)" + shows "({a1}, x1) \abs ({a3}, x3)" +using a b +apply(simp) +apply(erule exE)+ +apply(rule_tac x="pa + p" in exI) +apply(simp add: alpha_gen) +apply(simp add: fresh_star_def fresh_plus_perm) +done + +lemma alpha_equal: + assumes a: "({a}, x) \abs ({a}, y)" + shows "(a, x) \abs1 (a, y)" +using a +apply(simp) +apply(erule exE) +apply(simp add: alpha_gen) +apply(erule conjE)+ +apply(case_tac "a \ supp x") +apply(simp) +apply(subgoal_tac "supp x \* p") +apply(drule supp_perm_eq) +apply(simp) +apply(simp) +apply(simp) +apply(case_tac "a \ supp y") +apply(simp) +apply(drule supp_perm_eq) +apply(clarify) +apply(simp (no_asm_use)) +apply(simp) +apply(simp) +apply(drule yy) +apply(simp) +apply(simp) +apply(simp) +apply(case_tac "a \ p") +apply(subgoal_tac "supp y \* p") +apply(drule supp_perm_eq) +apply(clarify) +apply(simp (no_asm_use)) +apply(metis) +apply(auto simp add: fresh_star_def)[1] +apply(frule_tac kk) +apply(drule_tac x="a" in bspec) +apply(simp) +apply(simp add: fresh_def) +apply(simp add: supp_perm) +apply(subgoal_tac "((p \ a) \ p)") +apply(simp add: fresh_def supp_perm) +apply(simp add: fresh_star_def) +done + +lemma alpha_unequal: + assumes a: "({a}, x) \abs ({b}, y)" "sort_of a = sort_of b" "a \ b" + shows "(a, x) \abs1 (b, y)" +using a +apply - +apply(subgoal_tac "a \ supp x - {a}") +apply(subgoal_tac "b \ supp x - {a}") +defer +apply(simp add: alpha_gen) +apply(simp) +apply(drule_tac abs_swap1) +apply(assumption) +apply(simp only: insert_eqvt empty_eqvt swap_atom_simps) +apply(simp only: abs_eq_iff) +apply(drule alphas_abs_sym) +apply(rotate_tac 4) +apply(drule_tac alpha_abs_trans) +apply(assumption) +apply(drule alpha_equal) +apply(rule_tac p="(a \ b)" in permute_boolE) +apply(simp add: fresh_eqvt) +apply(simp add: fresh_def) +done + +lemma alpha_new_old: + assumes a: "({a}, x) \abs ({b}, y)" "sort_of a = sort_of b" + shows "(a, x) \abs1 (b, y)" +using a +apply(case_tac "a=b") +apply(simp only: alpha_equal) +apply(drule alpha_unequal) +apply(simp) +apply(simp) +apply(simp) +done + +end \ No newline at end of file diff -r 758904445fb2 -r d1293d30c657 Nominal/ExCoreHaskell.thy --- a/Nominal/ExCoreHaskell.thy Fri Mar 26 17:22:02 2010 +0100 +++ b/Nominal/ExCoreHaskell.thy Fri Mar 26 17:22:17 2010 +0100 @@ -194,7 +194,7 @@ apply (simp add: alphas) apply (simp add: perm_bv2[symmetric]) apply (simp add: eqvts[symmetric]) - apply (simp add: supp_Abs) + apply (simp add: supp_abs) apply (simp add: fv_supp) apply (simp add: alpha_perm_bn) apply (rule supp_perm_eq[symmetric]) @@ -394,7 +394,7 @@ and s="TAll (pa \ p \ tvar) (p \ tkind) (pa \ p \ ty)" in subst) apply (simp only: eq_iff) apply (rule_tac x="-pa" in exI) - apply (simp add: alphas eqvts eqvts_raw supp_Abs fv_supp) + apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp) apply (rule_tac t="supp (pa \ p \ ty) - {atom (pa \ p \ tvar)}" and s="pa \ (p \ supp ty - {p \ atom tvar})" in subst) apply (simp add: eqvts) @@ -422,7 +422,7 @@ apply (simp add: finite_supp) apply (simp add: finite_supp) apply (simp add: fresh_def) - apply (simp only: supp_Abs eqvts) + apply (simp only: supp_abs eqvts) apply blast (* GOAL2 *) @@ -434,7 +434,7 @@ and s="CAll (pa \ p \ tvar) (p \ ckind) (pa \ p \ co)" in subst) apply (simp only: eq_iff) apply (rule_tac x="-pa" in exI) - apply (simp add: alphas eqvts eqvts_raw supp_Abs fv_supp) + apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp) apply (rule_tac t="supp (pa \ p \ co) - {atom (pa \ p \ tvar)}" and s="pa \ (p \ supp co - {p \ atom tvar})" in subst) apply (simp add: eqvts) @@ -462,7 +462,7 @@ apply (simp add: finite_supp) apply (simp add: finite_supp) apply (simp add: fresh_def) - apply (simp only: supp_Abs eqvts) + apply (simp only: supp_abs eqvts) apply blast @@ -475,7 +475,7 @@ and s="LAMT (pa \ p \ tvar) (p \ tkind) (pa \ p \ trm)" in subst) apply (simp only: eq_iff) apply (rule_tac x="-pa" in exI) - apply (simp add: alphas eqvts eqvts_raw supp_Abs fv_supp) + apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp) apply (rule_tac t="supp (pa \ p \ trm) - {atom (pa \ p \ tvar)}" and s="pa \ (p \ supp trm - {p \ atom tvar})" in subst) apply (simp add: eqvts) @@ -503,7 +503,7 @@ apply (simp add: finite_supp) apply (simp add: finite_supp) apply (simp add: fresh_def) - apply (simp only: supp_Abs eqvts) + apply (simp only: supp_abs eqvts) apply blast (* GOAL4 a copy-and-paste *) @@ -515,7 +515,7 @@ and s="LAMC (pa \ p \ tvar) (p \ ckind) (pa \ p \ trm)" in subst) apply (simp only: eq_iff) apply (rule_tac x="-pa" in exI) - apply (simp add: alphas eqvts eqvts_raw supp_Abs fv_supp) + apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp) apply (rule_tac t="supp (pa \ p \ trm) - {atom (pa \ p \ tvar)}" and s="pa \ (p \ supp trm - {p \ atom tvar})" in subst) apply (simp add: eqvts) @@ -543,7 +543,7 @@ apply (simp add: finite_supp) apply (simp add: finite_supp) apply (simp add: fresh_def) - apply (simp only: supp_Abs eqvts) + apply (simp only: supp_abs eqvts) apply blast @@ -556,7 +556,7 @@ and s="Lam (pa \ p \ var) (p \ ty) (pa \ p \ trm)" in subst) apply (simp only: eq_iff) apply (rule_tac x="-pa" in exI) - apply (simp add: alphas eqvts eqvts_raw supp_Abs fv_supp) + apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp) apply (rule_tac t="supp (pa \ p \ trm) - {atom (pa \ p \ var)}" and s="pa \ (p \ supp trm - {p \ atom var})" in subst) apply (simp add: eqvts) @@ -584,7 +584,7 @@ apply (simp add: finite_supp) apply (simp add: finite_supp) apply (simp add: fresh_def) - apply (simp only: supp_Abs eqvts) + apply (simp only: supp_abs eqvts) apply blast @@ -597,7 +597,7 @@ and s="Let (pa \ p \ var) (p \ ty) (p \ trm1) (pa \ p \ trm2)" in subst) apply (simp only: eq_iff) apply (rule_tac x="-pa" in exI) - apply (simp add: alphas eqvts eqvts_raw supp_Abs fv_supp) + apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp) apply (rule_tac t="supp (pa \ p \ trm2) - {atom (pa \ p \ var)}" and s="pa \ (p \ supp trm2 - {p \ atom var})" in subst) apply (simp add: eqvts) @@ -626,7 +626,7 @@ apply (simp add: finite_supp) apply (simp add: finite_supp) apply (simp add: fresh_def) - apply (simp only: supp_Abs eqvts) + apply (simp only: supp_abs eqvts) apply blast (* MAIN ACons Goal *) @@ -647,10 +647,10 @@ apply (rule at_set_avoiding2) apply (simp add: fin_bv) apply (simp add: finite_supp) - apply (simp add: supp_Abs) + apply (simp add: supp_abs) apply (rule finite_Diff) apply (simp add: finite_supp) - apply (simp add: fresh_star_def fresh_def supp_Abs eqvts) + apply (simp add: fresh_star_def fresh_def supp_abs eqvts) done then have b: "P1 a (0 \ tkind)" and "P2 b (0 \ ckind)" "P3 c (0 \ ty)" and "P4 d (0 \ ty_lst)" and "P5 e (0 \ co)" and "P6 f (0 \ co_lst)" and "P7 g (0 \ trm)" and "P8 h (0 \ assoc_lst)" by (blast+) moreover have "P9 i (permute_bv 0 (0 \ pat))" and "P10 j (permute_bv_vt 0 (0 \ vt_lst))" and "P11 k (permute_bv_tvtk 0 (0 \ tvtk_lst))" and "P12 l (permute_bv_tvck 0 (0 \ tvck_lst))" using a1 a2 a3 a4 by (blast+) diff -r 758904445fb2 -r d1293d30c657 Nominal/ExLet.thy --- a/Nominal/ExLet.thy Fri Mar 26 17:22:02 2010 +0100 +++ b/Nominal/ExLet.thy Fri Mar 26 17:22:17 2010 +0100 @@ -87,7 +87,7 @@ apply (simp add: permute_bn_alpha_bn) apply (simp add: perm_bn[symmetric]) apply (simp add: eqvts[symmetric]) - apply (simp add: supp_Abs) + apply (simp add: supp_abs) apply (simp add: trm_lts.supp) apply (rule supp_perm_eq[symmetric]) apply (subst supp_finite_atom_set) @@ -157,10 +157,10 @@ apply(rule at_set_avoiding2) apply(rule fin_bn) apply(simp add: finite_supp) - apply(simp add: supp_Abs) + apply(simp add: supp_abs) apply(rule finite_Diff) apply(simp add: finite_supp) - apply(simp add: fresh_star_def fresh_def supp_Abs) + apply(simp add: fresh_star_def fresh_def supp_abs) apply(simp add: eqvts permute_bn) apply(rule a5) apply(simp add: permute_bn) diff -r 758904445fb2 -r d1293d30c657 Nominal/Fv.thy --- a/Nominal/Fv.thy Fri Mar 26 17:22:02 2010 +0100 +++ b/Nominal/Fv.thy Fri Mar 26 17:22:17 2010 +0100 @@ -872,7 +872,7 @@ *} lemma supp_abs_sum: "supp (Abs x (a :: 'a :: fs)) \ supp (Abs x (b :: 'b :: fs)) = supp (Abs x (a, b))" - apply (simp add: supp_Abs supp_Pair) + apply (simp add: supp_abs supp_Pair) apply blast done @@ -880,10 +880,10 @@ fun supp_eq_tac ind fv perm eqiff ctxt = rel_indtac ind THEN_ALL_NEW asm_full_simp_tac (HOL_basic_ss addsimps fv) THEN_ALL_NEW - asm_full_simp_tac (HOL_basic_ss addsimps @{thms supp_Abs[symmetric]}) THEN_ALL_NEW + asm_full_simp_tac (HOL_basic_ss addsimps @{thms supp_abs[symmetric]}) THEN_ALL_NEW simp_tac (HOL_basic_ss addsimps @{thms supp_abs_sum}) THEN_ALL_NEW simp_tac (HOL_basic_ss addsimps @{thms supp_def}) THEN_ALL_NEW - simp_tac (HOL_basic_ss addsimps (@{thm permute_ABS} :: perm)) THEN_ALL_NEW + simp_tac (HOL_basic_ss addsimps (@{thm permute_Abs} :: perm)) THEN_ALL_NEW simp_tac (HOL_basic_ss addsimps (@{thm Abs_eq_iff} :: eqiff)) THEN_ALL_NEW simp_tac (HOL_basic_ss addsimps @{thms alpha_gen2}) THEN_ALL_NEW simp_tac (HOL_basic_ss addsimps @{thms alpha_gen}) THEN_ALL_NEW diff -r 758904445fb2 -r d1293d30c657 Paper/Paper.thy --- a/Paper/Paper.thy Fri Mar 26 17:22:02 2010 +0100 +++ b/Paper/Paper.thy Fri Mar 26 17:22:17 2010 +0100 @@ -3,15 +3,35 @@ imports "../Nominal/Test" "LaTeXsugar" begin +consts + fv :: "'a \ 'b" + abs_set :: "'a \ 'b \ 'c" + Abs_lst :: "'a \ 'b \ 'c" + Abs_res :: "'a \ 'b \ 'c" + +definition + "equal \ (op =)" + notation (latex output) swap ("'(_ _')" [1000, 1000] 1000) and fresh ("_ # _" [51, 51] 50) and fresh_star ("_ #* _" [51, 51] 50) and supp ("supp _" [78] 73) and uminus ("-_" [78] 73) and - If ("if _ then _ else _" 10) + If ("if _ then _ else _" 10) and + alpha_gen ("_ \\<^raw:\makebox[0mm][l]{$\,_{\textit{set}}$}>\<^bsup>_,_,_\<^esup> _") and + alpha_lst ("_ \\<^raw:\makebox[0mm][l]{$\,_{\textit{list}}$}>\<^bsup>_,_,_\<^esup> _") and + alpha_res ("_ \\<^raw:\makebox[0mm][l]{$\,_{\textit{res}}$}>\<^bsup>_,_,_\<^esup> _") and + abs_set ("_ \\<^raw:{$\,_{\textit{abs\_set}}$}> _") and + fv ("fv'(_')" [100] 100) and + equal ("=") and + alpha_abs ("_ \\<^raw:{$\,_{\textit{abs\_set}}$}> _") and + Abs ("[_]\<^raw:$\!$>\<^bsub>set\<^esub>._") and + Abs_lst ("[_]\<^raw:$\!$>\<^bsub>list\<^esub>._") and + Abs_res ("[_]\<^raw:$\!$>\<^bsub>res\<^esub>._") (*>*) + section {* Introduction *} text {* @@ -19,12 +39,12 @@ alpha-equated terms, for example \begin{center} - $t ::= x \mid t\;t \mid \lambda x. t$ + @{text "t ::= x | t t | \x. t"} \end{center} \noindent where free and bound variables have names. For such terms Nominal Isabelle - derives automatically a reasoning infrastructure that has been used + derives automatically a reasoning infrastructure that has been used successfully in formalisations of an equivalence checking algorithm for LF \cite{UrbanCheneyBerghofer08}, Typed Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for concurrency @@ -39,7 +59,8 @@ % \begin{equation}\label{tysch} \begin{array}{l} - T ::= x \mid T \rightarrow T \hspace{5mm} S ::= \forall \{x_1,\ldots, x_n\}. T + @{text "T ::= x | T \ T"}\hspace{5mm} + @{text "S ::= \{x\<^isub>1,\, x\<^isub>n}. T"} \end{array} \end{equation} @@ -59,38 +80,38 @@ we would like to regard the following two type-schemes as alpha-equivalent % \begin{equation}\label{ex1} - \forall \{x, y\}. x \rightarrow y \;\approx_\alpha\; \forall \{y, x\}. y \rightarrow x + @{text "\{x,y}. x \ y \\<^isub>\ \{y,x}. y \ x"} \end{equation} \noindent - but assuming that $x$, $y$ and $z$ are distinct variables, + but assuming that @{text x}, @{text y} and @{text z} are distinct variables, the following two should \emph{not} be alpha-equivalent % \begin{equation}\label{ex2} - \forall \{x, y\}. x \rightarrow y \;\not\approx_\alpha\; \forall \{z\}. z \rightarrow z + @{text "\{x,y}. x \ y \\<^isub>\ \{z}. z \ z"} \end{equation} \noindent - Moreover, we like to regard type-schemes as - alpha-equivalent, if they differ only on \emph{vacuous} binders, such as + Moreover, we like to regard type-schemes as alpha-equivalent, if they differ + only on \emph{vacuous} binders, such as % \begin{equation}\label{ex3} - \forall \{x\}. x \rightarrow y \;\approx_\alpha\; \forall \{x, z\}. x \rightarrow y + @{text "\{x}. x \ y \\<^isub>\ \{x,z}. x \ y"} \end{equation} \noindent - where $z$ does not occur freely in the type. - In this paper we will give a general binding mechanism and associated - notion of alpha-equivalence that can be used to faithfully represent - this kind of binding in Nominal Isabelle. The difficulty of finding the right notion - for alpha-equivalence can be appreciated in this case by considering that the - definition given by Leroy in \cite{Leroy92} is incorrect (it omits a side-condition). + where @{text z} does not occur freely in the type. In this paper we will + give a general binding mechanism and associated notion of alpha-equivalence + that can be used to faithfully represent this kind of binding in Nominal + Isabelle. The difficulty of finding the right notion for alpha-equivalence + can be appreciated in this case by considering that the definition given by + Leroy in \cite{Leroy92} is incorrect (it omits a side-condition). - However, the notion of alpha-equivalence that is preserved by vacuous binders is not - always wanted. For example in terms like + However, the notion of alpha-equivalence that is preserved by vacuous + binders is not always wanted. For example in terms like % \begin{equation}\label{one} - \LET x = 3 \AND y = 2 \IN x\,-\,y \END + @{text "\ x = 3 \ y = 2 \ x - y \"} \end{equation} \noindent @@ -99,7 +120,7 @@ with % \begin{center} - $\LET x = 3 \AND y = 2 \AND z = loop \IN x\,-\,y \END$ + @{text "\ x = 3 \ y = 2 \ z = loop \ x - y \"} \end{center} \noindent @@ -109,10 +130,10 @@ However, we found that this is still not sufficient for dealing with language constructs frequently occurring in programming language - research. For example in $\mathtt{let}$s containing patterns + research. For example in @{text "\"}s containing patterns % \begin{equation}\label{two} - \LET (x, y) = (3, 2) \IN x\,-\,y \END + @{text "\ (x, y) = (3, 2) \ x - y \"} \end{equation} \noindent @@ -121,72 +142,79 @@ we do not want to regard \eqref{two} as alpha-equivalent with % \begin{center} - $\LET (y, x) = (3, 2) \IN x\,- y\,\END$ + @{text "\ (y, x) = (3, 2) \ x - y \"} \end{center} \noindent - As a result, we provide three general binding mechanisms each of which binds multiple - variables at once, and let the user chose which one is intended when formalising a - programming language calculus. + As a result, we provide three general binding mechanisms each of which binds + multiple variables at once, and let the user chose which one is intended + when formalising a programming language calculus. - By providing these general binding mechanisms, however, we have to work around - a problem that has been pointed out by Pottier \cite{Pottier06} and Cheney - \cite{Cheney05}: in $\mathtt{let}$-constructs of the form + By providing these general binding mechanisms, however, we have to work + around a problem that has been pointed out by Pottier \cite{Pottier06} and + Cheney \cite{Cheney05}: in @{text "\"}-constructs of the form % \begin{center} - $\LET x_1 = t_1 \AND \ldots \AND x_n = t_n \IN s \END$ + @{text "\ x\<^isub>1 = t\<^isub>1 \ \ \ x\<^isub>n = t\<^isub>n \ s \"} \end{center} \noindent - which bind all the $x_i$ in $s$, we might not care about the order in - which the $x_i = t_i$ are given, but we do care about the information that there are - as many $x_i$ as there are $t_i$. We lose this information if we represent the - $\mathtt{let}$-constructor by something like + which bind all the @{text "x\<^isub>i"} in @{text s}, we might not care + about the order in which the @{text "x\<^isub>i = t\<^isub>i"} are given, + but we do care about the information that there are as many @{text + "x\<^isub>i"} as there are @{text "t\<^isub>i"}. We lose this information if + we represent the @{text "\"}-constructor by something like % \begin{center} - $\LET [x_1,\ldots,x_n].s\;\; [t_1,\ldots,t_n]$ + @{text "\ [x\<^isub>1,\,x\<^isub>n].s [t\<^isub>1,\,t\<^isub>n]"} \end{center} \noindent - where the notation $[\_\!\_].\_\!\_$ indicates that the $x_i$ become bound - in $s$. In this representation the term \mbox{$\LET [x].s\;\;[t_1,t_2]$} - would be a perfectly legal instance. To exclude such terms, additional - predicates about well-formed terms are needed in order to ensure that the two - lists are of equal length. This can result into very messy reasoning (see - for example~\cite{BengtsonParow09}). To avoid this, we will allow type specifications - for $\mathtt{let}$s as follows + where the notation @{text "[_]._"} indicates that the @{text "x\<^isub>i"} + become bound in @{text s}. In this representation the term + \mbox{@{text "\ [x].s [t\<^isub>1,t\<^isub>2]"}} would be a perfectly legal + instance. To exclude such terms, additional predicates about well-formed + terms are needed in order to ensure that the two lists are of equal + length. This can result into very messy reasoning (see for + example~\cite{BengtsonParow09}). To avoid this, we will allow type + specifications for $\mathtt{let}$s as follows % \begin{center} \begin{tabular}{r@ {\hspace{2mm}}r@ {\hspace{2mm}}l} - $trm$ & $::=$ & \ldots\\ - & $\mid$ & $\mathtt{let}\;a\!::\!assn\;\;s\!::\!trm\quad\mathtt{bind}\;bn\,(a) \IN s$\\[1mm] - $assn$ & $::=$ & $\mathtt{anil}$\\ - & $\mid$ & $\mathtt{acons}\;\;name\;\;trm\;\;assn$ + @{text trm} & @{text "::="} & @{text "\"}\\ + & @{text "|"} & @{text "\ a::assn s::trm"}\hspace{4mm} + \isacommand{bind} @{text "bn(a)"} \isacommand{in} @{text "s"}\\[1mm] + @{text assn} & @{text "::="} & @{text "\"}\\ + & @{text "|"} & @{text "\ name trm assn"} \end{tabular} \end{center} \noindent - where $assn$ is an auxiliary type representing a list of assignments - and $bn$ an auxiliary function identifying the variables to be bound by - the $\mathtt{let}$. This function is defined by recursion over $assn$ as follows + where @{text assn} is an auxiliary type representing a list of assignments + and @{text bn} an auxiliary function identifying the variables to be bound + by the @{text "\"}. This function is defined by recursion over @{text + assn} as follows \begin{center} - $bn\,(\mathtt{anil}) = \varnothing \qquad bn\,(\mathtt{acons}\;x\;t\;as) = \{x\} \cup bn\,(as)$ + @{text "bn(\) ="} @{term "{}"} \hspace{5mm} + @{text "bn(\ x t as) = {x} \ bn(as)"} \end{center} \noindent The scope of the binding is indicated by labels given to the types, for - example \mbox{$s\!::\!trm$}, and a binding clause, in this case - $\mathtt{bind}\;bn\,(a) \IN s$, that states to bind in $s$ all the names the - function call $bn\,(a)$ returns. This style of specifying terms and bindings is - heavily inspired by the syntax of the Ott-tool \cite{ott-jfp}. + example @{text "s::trm"}, and a binding clause, in this case + \isacommand{bind} @{text "bn(a)"} \isacommand{in} @{text "s"}, that states + to bind in @{text s} all the names the function call @{text "bn(a)"} returns. + This style of specifying terms and bindings is heavily inspired by the + syntax of the Ott-tool \cite{ott-jfp}. + However, we will not be able to deal with all specifications that are allowed by Ott. One reason is that Ott lets the user to specify ``empty'' types like \begin{center} - $t ::= t\;t \mid \lambda x. t$ + @{text "t ::= t t | \x. t"} \end{center} \noindent @@ -204,32 +232,31 @@ two type-schemes (with $x$, $y$ and $z$ being distinct) \begin{center} - $\forall \{x\}. x \rightarrow y \;=\; \forall \{x, z\}. x \rightarrow y$ + @{text "\{x}. x \ y = \{x,z}. x \ y"} \end{center} \noindent - are not just alpha-equal, but actually \emph{equal}. As a - result, we can only support specifications that make sense on the level of - alpha-equated terms (offending specifications, which for example bind a variable - according to a variable bound somewhere else, are not excluded by Ott, but we - have to). Our - insistence on reasoning with alpha-equated terms comes from the wealth of - experience we gained with the older version of Nominal Isabelle: for - non-trivial properties, reasoning about alpha-equated terms is much easier - than reasoning with raw terms. The fundamental reason for this is that the - HOL-logic underlying Nominal Isabelle allows us to replace - ``equals-by-equals''. In contrast, replacing ``alpha-equals-by-alpha-equals'' - in a representation based on raw terms requires a lot of extra reasoning work. + are not just alpha-equal, but actually \emph{equal}. As a result, we can + only support specifications that make sense on the level of alpha-equated + terms (offending specifications, which for example bind a variable according + to a variable bound somewhere else, are not excluded by Ott, but we have + to). Our insistence on reasoning with alpha-equated terms comes from the + wealth of experience we gained with the older version of Nominal Isabelle: + for non-trivial properties, reasoning about alpha-equated terms is much + easier than reasoning with raw terms. The fundamental reason for this is + that the HOL-logic underlying Nominal Isabelle allows us to replace + ``equals-by-equals''. In contrast, replacing + ``alpha-equals-by-alpha-equals'' in a representation based on raw terms + requires a lot of extra reasoning work. - Although in informal settings a reasoning infrastructure for alpha-equated - terms is nearly always taken for granted, establishing - it automatically in the Isabelle/HOL theorem prover is a rather non-trivial task. - For every specification we will need to construct a type containing as - elements the alpha-equated terms. To do so, we use - the standard HOL-technique of defining a new type by - identifying a non-empty subset of an existing type. The construction we - perform in HOL can be illustrated by the following picture: - + Although in informal settings a reasoning infrastructure for alpha-equated + terms is nearly always taken for granted, establishing it automatically in + the Isabelle/HOL theorem prover is a rather non-trivial task. For every + specification we will need to construct a type containing as elements the + alpha-equated terms. To do so, we use the standard HOL-technique of defining + a new type by identifying a non-empty subset of an existing type. The + construction we perform in HOL can be illustrated by the following picture: + \begin{center} \begin{tikzpicture} %\draw[step=2mm] (-4,-1) grid (4,1); @@ -255,45 +282,45 @@ \end{center} \noindent - We take as the starting point a definition of raw terms (defined as a - datatype in Isabelle/HOL); identify then the - alpha-equivalence classes in the type of sets of raw terms according to our - alpha-equivalence relation and finally define the new type as these - alpha-equivalence classes (non-emptiness is satisfied whenever the raw terms are - definable as datatype in Isabelle/HOL and the fact that our relation for - alpha-equivalence is indeed an equivalence relation). + We take as the starting point a definition of raw terms (defined as a + datatype in Isabelle/HOL); identify then the alpha-equivalence classes in + the type of sets of raw terms according to our alpha-equivalence relation + and finally define the new type as these alpha-equivalence classes + (non-emptiness is satisfied whenever the raw terms are definable as datatype + in Isabelle/HOL and the fact that our relation for alpha-equivalence is + indeed an equivalence relation). - The fact that we obtain an isomorphism between the new type and the non-empty - subset shows that the new type is a faithful representation of alpha-equated terms. - That is not the case for example for terms using the locally - nameless representation of binders \cite{McKinnaPollack99}: in this representation - there are ``junk'' terms that need to - be excluded by reasoning about a well-formedness predicate. + The fact that we obtain an isomorphism between the new type and the + non-empty subset shows that the new type is a faithful representation of + alpha-equated terms. That is not the case for example for terms using the + locally nameless representation of binders \cite{McKinnaPollack99}: in this + representation there are ``junk'' terms that need to be excluded by + reasoning about a well-formedness predicate. - The problem with introducing a new type in Isabelle/HOL is that in order to be useful, - a reasoning infrastructure needs to be ``lifted'' from the underlying subset to - the new type. This is usually a tricky and arduous task. To ease it, - we re-implemented in Isabelle/HOL the quotient package described by Homeier - \cite{Homeier05} for the HOL4 system. This package - allows us to lift definitions and theorems involving raw terms - to definitions and theorems involving alpha-equated terms. For example - if we define the free-variable function over raw lambda-terms + The problem with introducing a new type in Isabelle/HOL is that in order to + be useful, a reasoning infrastructure needs to be ``lifted'' from the + underlying subset to the new type. This is usually a tricky and arduous + task. To ease it, we re-implemented in Isabelle/HOL the quotient package + described by Homeier \cite{Homeier05} for the HOL4 system. This package + allows us to lift definitions and theorems involving raw terms to + definitions and theorems involving alpha-equated terms. For example if we + define the free-variable function over raw lambda-terms \begin{center} - $\fv(x) = \{x\}$\hspace{10mm} - $\fv(t_1\;t_2) = \fv(t_1) \cup \fv(t_2)$\\[1mm] - $\fv(\lambda x.t) = \fv(t) - \{x\}$ + @{text "fv(x) = {x}"}\hspace{10mm} + @{text "fv(t\<^isub>1 t\<^isub>2) = fv(t\<^isub>1) \ fv(t\<^isub>2)"}\\[1mm] + @{text "fv(\x.t) = fv(t) - {x}"} \end{center} \noindent - then with not too great effort we obtain a function $\fv^\alpha$ + then with not too great effort we obtain a function @{text "fv\<^sup>\"} operating on quotients, or alpha-equivalence classes of lambda-terms. This lifted function is characterised by the equations \begin{center} - $\fv^\alpha(x) = \{x\}$\hspace{10mm} - $\fv^\alpha(t_1\;t_2) = \fv^\alpha(t_1) \cup \fv^\alpha(t_2)$\\[1mm] - $\fv^\alpha(\lambda x.t) = \fv^\alpha(t) - \{x\}$ + @{text "fv\<^sup>\(x) = {x}"}\hspace{10mm} + @{text "fv\<^sup>\(t\<^isub>1 t\<^isub>2) = fv\<^sup>\(t\<^isub>1) \ fv\<^sup>\(t\<^isub>2)"}\\[1mm] + @{text "fv\<^sup>\(\x.t) = fv\<^sup>\(t) - {x}"} \end{center} \noindent @@ -400,44 +427,47 @@ from this specification (remember that Nominal Isabelle is a definitional extension of Isabelle/HOL, which does not introduce any new axioms). - - In order to keep our work manageable, we will wherever possible state - definitions and perform proofs inside Isabelle, as opposed to write custom - ML-code that generates them anew for each specification. To that - end, we will consider pairs @{text "(as, x)"} of type @{text "(atom set) \ \"}. - These pairs are intended to represent the abstraction, or binding, of the set @{text "as"} - in the body @{text "x"}. + In order to keep our work with deriving the reasoning infrastructure + manageable, we will wherever possible state definitions and perform proofs + on the user-level of Isabelle/HOL, as opposed to write custom ML-code that + generates them anew for each specification. To that end, we will consider + first pairs @{text "(as, x)"} of type @{text "(atom set) \ \"}. These pairs + are intended to represent the abstraction, or binding, of the set @{text + "as"} in the body @{text "x"}. - The first question we have to answer is when the pairs $(as, x)$ and $(bs, y)$ are - alpha-equivalent? (At the moment we are interested in - the notion of alpha-equivalence that is \emph{not} preserved by adding - vacuous binders.) To answer this, we identify four conditions: {\it i)} given - a free-variable function $\fv$ of type \mbox{@{text "\ \ atom set"}}, then @{text x} and @{text y} - need to have the same set of free variables; moreover there must be a permutation - @{text p} such that {\it ii)} it leaves the free variables of @{text x} and @{text y} unchanged, - but {\it iii)} ``moves'' their bound names so that we obtain modulo a relation, - say \mbox{@{text "_ R _"}}, two equal terms. We also require {\it iv)} that @{text p} makes - the abstracted sets @{text as} and @{text bs} equal. The requirements {\it i)} to {\it iv)} can - be stated formally as follows: + The first question we have to answer is when the pairs @{text "(as, x)"} and + @{text "(bs, y)"} are alpha-equivalent? (At the moment we are interested in + the notion of alpha-equivalence that is \emph{not} preserved by adding + vacuous binders.) To answer this, we identify four conditions: {\it i)} + given a free-variable function @{text "fv"} of type \mbox{@{text "\ \ atom + set"}}, then @{text x} and @{text y} need to have the same set of free + variables; moreover there must be a permutation @{text p} such that {\it + ii)} it leaves the free variables of @{text x} and @{text y} unchanged, but + {\it iii)} ``moves'' their bound names so that we obtain modulo a relation, + say \mbox{@{text "_ R _"}}, two equal terms. We also require {\it iv)} that + @{text p} makes the abstracted sets @{text as} and @{text bs} equal. The + requirements {\it i)} to {\it iv)} can be stated formally as follows: % \begin{equation}\label{alphaset} \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l} - \multicolumn{2}{l}{(as, x) \approx\hspace{0.05mm}_{set}^{\fv, R, p} (bs, y) \;\dn\hspace{30mm}\;}\\[1mm] - & @{text "fv(x) - as = fv(y) - bs"}\\ - \wedge & @{text "(fv(x) - as) #* p"}\\ - \wedge & @{text "(p \ x) R y"}\\ - \wedge & @{text "(p \ as) = bs"}\\ + \multicolumn{2}{l}{@{term "(as, x) \gen R fv p (bs, y)"} @{text "\"}\hspace{30mm}}\\ + & @{term "fv(x) - as = fv(y) - bs"}\\ + @{text "\"} & @{term "(fv(x) - as) \* p"}\\ + @{text "\"} & @{text "(p \ x) R y"}\\ + @{text "\"} & @{term "(p \ as) = bs"}\\ \end{array} \end{equation} \noindent - Note that this relation is dependent on $p$. Alpha-equivalence is then the relation where - we existentially quantify over this $p$. - Also note that the relation is dependent on a free-variable function $\fv$ and a relation - $R$. The reason for this extra generality is that we will use $\approx_{set}$ for both - ``raw'' terms and alpha-equated terms. In the latter case, $R$ will be replaced by - equality $(op =)$ and we are going to prove that $\fv$ will be equal to the support - of $x$ and $y$. + Note that this relation is dependent on the permutation @{text + "p"}. Alpha-equivalence between two pairs is then the relation where we + existentially quantify over this @{text "p"}. Also note that the relation is + dependent on a free-variable function @{text "fv"} and a relation @{text + "R"}. The reason for this extra generality is that we will use + $\approx_{\textit{set}}$ for both ``raw'' terms and alpha-equated terms. In + the latter case, $R$ will be replaced by equality @{text "="} and for raw terms we + will prove that @{text "fv"} is equal to the support of @{text + x} and @{text y}. The definition in \eqref{alphaset} does not make any distinction between the order of abstracted variables. If we want this, then we can define alpha-equivalence @@ -446,26 +476,27 @@ % \begin{equation}\label{alphalist} \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l} - \multicolumn{2}{l}{(as, x) \approx\hspace{0.05mm}_{list}^{\fv, R, p} (bs, y) \;\dn\hspace{30mm}\;}\\[1mm] - & @{text "fv(x) - (set as) = fv(y) - (set bs)"}\\ - \wedge & @{text "(fv(x) - set as) #* p"}\\ + \multicolumn{2}{l}{@{term "(as, x) \lst R fv p (bs, y)"} @{text "\"}\hspace{30mm}}\\[1mm] + & @{term "fv(x) - (set as) = fv(y) - (set bs)"}\\ + \wedge & @{term "(fv(x) - set as) \* p"}\\ \wedge & @{text "(p \ x) R y"}\\ - \wedge & @{text "(p \ as) = bs"}\\ + \wedge & @{term "(p \ as) = bs"}\\ \end{array} \end{equation} \noindent - where $set$ is the function that coerces a list of atoms into a set of atoms. + where @{term set} is a function that coerces a list of atoms into a set of atoms. + Now the last clause ensures that the order of the binders matters. - If we do not want to make any difference between the order of binders and + If we do not want to make any difference between the order of binders \emph{and} also allow vacuous binders, then we keep sets of binders, but drop the fourth condition in \eqref{alphaset}: % \begin{equation}\label{alphares} \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l} - \multicolumn{2}{l}{(as, x) \approx\hspace{0.05mm}_{res}^{\fv, R, p} (bs, y) \;\dn\hspace{30mm}\;}\\[1mm] - & @{text "fv(x) - as = fv(y) - bs"}\\ - \wedge & @{text "(fv(x) - as) #* p"}\\ + \multicolumn{2}{l}{@{term "(as, x) \res R fv p (bs, y)"} @{text "\"}\hspace{30mm}}\\[1mm] + & @{term "fv(x) - as = fv(y) - bs"}\\ + \wedge & @{term "(fv(x) - as) \* p"}\\ \wedge & @{text "(p \ x) R y"}\\ \end{array} \end{equation} @@ -473,52 +504,116 @@ \begin{exmple}\rm It might be useful to consider some examples for how these definitions pan out in practise. For this consider the case of abstracting a set of variables over types (as in type-schemes). - We set $R$ to be the equality and for $\fv(T)$ we define + We set @{text R} to be the equality and for @{text "fv(T)"} we define \begin{center} - $\fv(x) = \{x\} \qquad \fv(T_1 \rightarrow T_2) = \fv(T_1) \cup \fv(T_2)$ + @{text "fv(x) = {x}"} \hspace{5mm} @{text "fv(T\<^isub>1 \ T\<^isub>2) = fv(T\<^isub>1) \ fv(T\<^isub>2)"} \end{center} \noindent - Now recall the examples shown in \eqref{ex1}, \eqref{ex2} and \eqref{ex3}. It can be easily - checked that @{text "({x, y}, x \ y)"} and - @{text "({y, x}, y \ x)"} are equal according to $\approx_{set}$ and $\approx_{res}$ by taking $p$ to - be the swapping @{term "(x \ y)"}. In case of @{text "x \ y"}, then - $([x, y], x \rightarrow y) \not\approx_{list} ([y,x], x \rightarrow y)$ since there is no permutation that - makes the lists @{text "[x, y]"} and @{text "[y, x]"} equal, and also leaves the - type \mbox{@{text "x \ y"}} unchanged. Another examples is - $(\{x\}, x) \approx_{res} (\{x,y\}, x)$ which holds by taking $p$ to be the identity permutation. - However, if @{text "x \ y"}, then - $(\{x\}, x) \not\approx_{set} (\{x,y\}, x)$ since there is no permutation that makes - the sets $\{x\}$ and $\{x,y\}$ equal (similarly for $\approx_{list}$). + Now recall the examples shown in \eqref{ex1}, \eqref{ex2} and + \eqref{ex3}. It can be easily checked that @{text "({x,y}, x \ y)"} and + @{text "({y,x}, y \ x)"} are equal according to $\approx_{\textit{set}}$ and + $\approx_{\textit{res}}$ by taking @{text p} to be the swapping @{term "(x \ + y)"}. In case of @{text "x \ y"}, then @{text "([x, y], x \ y)"} + $\not\approx_{\textit{list}}$ @{text "([y,x], x \ y)"} since there is no permutation + that makes the lists @{text "[x, y]"} and @{text "[y, x]"} equal, and also + leaves the type \mbox{@{text "x \ y"}} unchanged. Another example is + @{text "({x}, x)"} $\approx_{\textit{res}}$ @{text "({x,y}, x)"} which holds by + taking @{text p} to be the + identity permutation. However, if @{text "x \ y"}, then @{text "({x}, x)"} + $\not\approx_{\textit{set}}$ @{text "({x,y}, x)"} since there is no permutation + that makes the + sets @{text "{x}"} and @{text "{x,y}"} equal (similarly for $\approx_{\textit{list}}$). \end{exmple} + % looks too ugly + %\noindent + %Let $\star$ range over $\{set, res, list\}$. We prove next under which + %conditions the $\approx\hspace{0.05mm}_\star^{\fv, R, p}$ are equivalence + %relations and equivariant: + % + %\begin{lemma} + %{\it i)} Given the fact that $x\;R\;x$ holds, then + %$(as, x) \approx\hspace{0.05mm}^{\fv, R, 0}_\star (as, x)$. {\it ii)} Given + %that @{text "(p \ x) R y"} implies @{text "(-p \ y) R x"}, then + %$(as, x) \approx\hspace{0.05mm}^{\fv, R, p}_\star (bs, y)$ implies + %$(bs, y) \approx\hspace{0.05mm}^{\fv, R, - p}_\star (as, x)$. {\it iii)} Given + %that @{text "(p \ x) R y"} and @{text "(q \ y) R z"} implies + %@{text "((q + p) \ x) R z"}, then $(as, x) \approx\hspace{0.05mm}^{\fv, R, p}_\star (bs, y)$ + %and $(bs, y) \approx\hspace{0.05mm}^{\fv, R, q}_\star (cs, z)$ implies + %$(as, x) \approx\hspace{0.05mm}^{\fv, R, q + p}_\star (cs, z)$. Given + %@{text "(q \ x) R y"} implies @{text "(p \ (q \ x)) R (p \ y)"} and + %@{text "p \ (fv x) = fv (p \ x)"} then @{text "p \ (fv y) = fv (p \ y)"}, then + %$(as, x) \approx\hspace{0.05mm}^{\fv, R, q}_\star (bs, y)$ implies + %$(p \;\isasymbullet\; as, p \;\isasymbullet\; x) \approx\hspace{0.05mm}^{\fv, R, q}_\star + %(p \;\isasymbullet\; bs, p \;\isasymbullet\; y)$. + %\end{lemma} + + %\begin{proof} + %All properties are by unfolding the definitions and simple calculations. + %\end{proof} + + + In the rest of this section we are going to introduce a type- and term-constructor + for abstractions. For this we define + % + \begin{equation} + @{term "abs_set (as, x) (bs, x) \ \p. alpha_gen (as, x) equal supp p (bs, x)"} + \end{equation} + \noindent - Let $\star$ range over $\{set, res, list\}$. We prove next under which - conditions the $\approx\hspace{0.05mm}_\star^{\fv, R, p}$ are equivalence - relations and equivariant: + Similarly for @{text "abs_list"} and @{text "abs_res"}. We can show that these + relations are equivalence relations and equivariant + (we only show the $\approx_{\textit{abs\_set}}$-case). \begin{lemma} - {\it i)} Given the fact that $x\;R\;x$ holds, then - $(as, x) \approx\hspace{0.05mm}^{\fv, R, 0}_\star (as, x)$. {\it ii)} Given - that @{text "(p \ x) R y"} implies @{text "(-p \ y) R x"}, then - $(as, x) \approx\hspace{0.05mm}^{\fv, R, p}_\star (bs, y)$ implies - $(bs, y) \approx\hspace{0.05mm}^{\fv, R, - p}_\star (as, x)$. {\it iii)} Given - that @{text "(p \ x) R y"} and @{text "(q \ y) R z"} implies - @{text "((q + p) \ x) R z"}, then $(as, x) \approx\hspace{0.05mm}^{\fv, R, p}_\star (bs, y)$ - and $(bs, y) \approx\hspace{0.05mm}^{\fv, R, q}_\star (cs, z)$ implies - $(as, x) \approx\hspace{0.05mm}^{\fv, R, q + p}_\star (cs, z)$. Given - @{text "(q \ x) R y"} implies @{text "(p \ (q \ x)) R (p \ y)"} and - @{text "p \ (fv x) = fv (p \ x)"} then @{text "p \ (fv y) = fv (p \ y)"}, then - $(as, x) \approx\hspace{0.05mm}^{\fv, R, q}_\star (bs, y)$ implies - $(p \;\isasymbullet\; as, p \;\isasymbullet\; x) \approx\hspace{0.05mm}^{\fv, R, q}_\star - (p \;\isasymbullet\; bs, p \;\isasymbullet\; y)$. + $\approx_{\textit{abs\_set}}$ is an equivalence + relations, and if @{term "abs_set (as, x) (bs, x)"} then also + @{term "abs_set (p \ as, p \ x) (p \ bs, p \ x)"}. + \end{lemma} + + \begin{proof} + Reflexivity is by taking @{text "p"} to be @{text "0"}. For symmetry we have + a permutation @{text p} and for the proof obligation take @{term "-p"}. In case + of transitivity we have two permutations @{text p} and @{text q}, and for the + proof obligation use @{text "q + p"}. All the conditions are then by simple + calculations. + \end{proof} + + \noindent + The following lemma (and similar ones for $\approx_{\textit{abs\_list}}$ and + $\approx_{\textit{abs\_res}}$) will be crucial below: + + \begin{lemma} + @{thm[mode=IfThen] alpha_abs_swap[no_vars]} \end{lemma} - + \begin{proof} - All properties are by unfolding the definitions and simple calculations. + This lemma is straightforward by observing that the assumptions give us + @{term "(a \ b) \ (supp x - bs) = (supp x - bs)"} and that @{text supp} + is equivariant. \end{proof} + \noindent + We are also define the following + + @{text "aux (as, x) \ supp x - as"} + + + + \noindent + This allows us to use our quotient package and introduce new types + @{text "\ abs_set"}, @{text "\ abs_res"} and @{text "\ abs_list"} + representing the alpha-equivalence classes. Elements in these types + we will, respectively, write as: + + \begin{center} + @{term "Abs as x"} \hspace{5mm} + @{term "Abs_lst as x"} \hspace{5mm} + @{term "Abs_res as x"} + \end{center} + \begin{lemma} $supp ([as]set. x) = supp x - as$ @@ -834,7 +929,7 @@ \begin{tabular}{cp{7cm}} $\bullet$ & @{text "{atom x\<^isub>i} - bnds"} provided @{term "x\<^isub>i"} is an atom\\ $\bullet$ & @{text "(atoms x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a set of atoms\\ - $\bullet$ & @{text "(atoml x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a list of atoms\\ + $\bullet$ & @{text "(atoms (set x\<^isub>i)) - bnds"} provided @{term "x\<^isub>i"} is a list of atoms\\ $\bullet$ & @{text "(fv_ty\<^isub>i x\<^isub>i) - bnds"} provided @{term "ty\<^isub>i"} is a nominal datatype\\ $\bullet$ & @{term "{}"} otherwise \end{tabular} diff -r 758904445fb2 -r d1293d30c657 Paper/document/root.tex --- a/Paper/document/root.tex Fri Mar 26 17:22:02 2010 +0100 +++ b/Paper/document/root.tex Fri Mar 26 17:22:17 2010 +0100 @@ -23,6 +23,14 @@ \renewcommand{\isasymequiv}{$\dn$} \renewcommand{\isasymiota}{} \renewcommand{\isasymemptyset}{$\varnothing$} +\newcommand{\isasymnotapprox}{$\not\approx$} +\newcommand{\isasymLET}{$\mathtt{let}$} +\newcommand{\isasymAND}{$\mathtt{and}$} +\newcommand{\isasymIN}{$\mathtt{in}$} +\newcommand{\isasymEND}{$\mathtt{end}$} +\newcommand{\isasymBIND}{$\mathtt{bind}$} +\newcommand{\isasymANIL}{$\mathtt{anil}$} +\newcommand{\isasymACONS}{$\mathtt{acons}$} \newcommand{\LET}{\;\mathtt{let}\;} \newcommand{\IN}{\;\mathtt{in}\;} \newcommand{\END}{\;\mathtt{end}\;} @@ -56,8 +64,8 @@ programming language calculi involving named bound variables (as opposed to de-Bruijn indices). In this paper we present an extension of Nominal Isabelle for dealing with general bindings, that means -term-constructors where multiple variables are bound at once. Such binding -structures are ubiquitous in programming language research and only very +term-constructors where multiple variables are bound at once. Such general +bindings are ubiquitous in programming language research and only very poorly supported with single binders, such as lambda-abstractions. Our extension includes novel definitions of alpha-equivalence and establishes automatically the reasoning infrastructure for alpha-equated terms. We