# HG changeset patch # User Cezary Kaliszyk # Date 1274264948 -7200 # Node ID d76667e51d307bc41dca2d176b763aaeee85e5fd # Parent 64f353098721d966da2253cb7f40a467eab01d44 more subst experiments diff -r 64f353098721 -r d76667e51d30 Nominal/Ex/Lambda.thy --- a/Nominal/Ex/Lambda.thy Wed May 19 11:29:42 2010 +0200 +++ b/Nominal/Ex/Lambda.thy Wed May 19 12:29:08 2010 +0200 @@ -475,101 +475,61 @@ (* Substitution *) definition new where - "new s = (THE x. \a \ s. x \ a)" - -term "let n = new {s, x} in b" + "new s = (THE x. \a \ s. atom x \ a)" lemma size_no_change: "size (p \ (t :: lam_raw)) = size t" by (induct t) simp_all function - subst_var_raw :: "lam_raw \ name \ name \ lam_raw" + subst_raw :: "lam_raw \ name \ lam_raw \ lam_raw" where - "subst_var_raw (Var_raw x) y s = (if x=y then (Var_raw s) else (Var_raw x))" -| "subst_var_raw (App_raw l r) y s = App_raw (subst_var_raw l y s) (subst_var_raw r y s)" -| "subst_var_raw (Lam_raw x t) y s = - Lam_raw (new {s, y, x}) (subst_var_raw ((x \ new {s, y, x}) \ t) y s)" + "subst_raw (Var_raw x) y s = (if x=y then s else (Var_raw x))" +| "subst_raw (App_raw l r) y s = App_raw (subst_raw l y s) (subst_raw r y s)" +| "subst_raw (Lam_raw x t) y s = + Lam_raw (new ({atom y} \ fv_lam_raw s \ fv_lam_raw t - {atom x})) + (subst_raw ((x \ (new ({atom y} \ fv_lam_raw s \ fv_lam_raw t - {atom x}))) \ t) y s)" by (pat_completeness, auto) termination apply (relation "measure (\(t, y, s). (size t))") apply (auto simp add: size_no_change) done +lemma fv_subst[simp]: "fv_lam_raw (subst_raw t y s) = + (if (atom y \ fv_lam_raw t) then fv_lam_raw s \ (fv_lam_raw t - {atom y}) else fv_lam_raw t)" + apply (induct t arbitrary: s) + apply (auto simp add: supp_at_base)[1] + apply (auto simp add: supp_at_base)[1] + apply (simp only: fv_lam_raw.simps) + apply simp + apply (rule conjI) + apply clarify + sorry + +thm supp_at_base lemma new_eqvt[eqvt]: "p \ (new s) = new (p \ s)" sorry -lemma subst_var_raw_eqvt[eqvt]: "p \ (subst_var_raw t y s) = subst_var_raw (p \ t) (p \ y) (p \ s)" +lemma subst_var_raw_eqvt[eqvt]: "p \ (subst_raw t y s) = subst_raw (p \ t) (p \ y) (p \ s)" apply (induct t arbitrary: p y s) apply simp_all apply(perm_simp) apply simp sorry -lemma subst_id: "alpha_lam_raw (subst_var_raw x d d) x" +lemma subst_id: "alpha_lam_raw (subst_raw x d (Var_raw d)) x" apply (induct x arbitrary: d) apply (simp_all add: alpha_lam_raw.intros) apply (rule alpha_lam_raw.intros) - apply (rule_tac x="((new {d, name}) \ name)" in exI) - - apply (rule_tac s="subst_var_raw ((name \ n) \ x) d d" and - t="(name \ n) \ (subst_var_raw x ((name \ n) \ d) ((name \ n) \ d))" in subst) - sorry - -(* Should be true? *) -lemma "(alpha_lam_raw ===> op = ===> op = ===> alpha_lam_raw) subst_var_raw subst_var_raw" - proof (intro fun_relI, (simp, clarify)) - fix a b c d - assume a: "alpha_lam_raw a b" - show "alpha_lam_raw (subst_var_raw a c d) (subst_var_raw b c d)" using a - apply (induct a b arbitrary: c d rule: alpha_lam_raw.induct) - apply (simp add: equivp_reflp[OF lam_equivp]) - apply (simp add: alpha_lam_raw.intros) - apply clarify -(* apply (case_tac "c = d") - apply clarify - apply (simp only: subst_id) - apply (rule alpha_lam_raw.intros) - apply (rule_tac x="p" in exI) - apply (simp add: alphas) - apply clarify - apply simp*) - apply (rename_tac x l y r c d p) - apply simp - unfolding Let_def - apply (rule alpha_lam_raw.intros) - apply (simp add: alphas) - apply clarify - apply simp - apply (rule conjI) - defer (* The fv one looks ok *) - apply (rule_tac x="p + (x \ new {d, c, x}) + (y \ new {d, c, y})" in exI) - apply (rule conjI) - defer (* should do sth like subst fresh_star_permute_iff[symmetric] *) - apply (simp only: eqvts) - apply simp - apply clarify - sorry - qed - -fun - subst_raw :: "lam_raw \ name \ lam_raw \ lam_raw" -where - "subst_raw (Var_raw x) y s = (if x=y then s else (Var_raw x))" -| "subst_raw (App_raw l r) y s = App_raw (subst_raw l y s) (subst_raw r y s)" -| "subst_raw (Lam_raw x t) y s = - (if x = y then t else - (if atom x \ (fv_lam_raw s) then (Lam_raw x (subst_raw t y s)) else undefined))" -(* termination/lifting fail with sth like: -| "subst_raw (Lam_raw x t) y s = - (FRESH v. Lam_raw v (subst_raw (subst_var_raw t x v) y s))" -*) + apply (rule_tac x="(name \ new (insert (atom d) (supp d)))" in exI) + apply (simp add: alphas) + oops quotient_definition subst ("_ [ _ ::= _ ]" [100,100,100] 100) where "subst :: lam \ name \ lam \ lam" is "subst_raw" -lemmas fv_rsp = quot_respect(10)[simplified,rulify] +lemmas fv_rsp = quot_respect(10)[simplified] lemma subst_rsp_pre1: assumes a: "alpha_lam_raw a b" @@ -581,14 +541,21 @@ apply (simp only: alphas) apply clarify apply (simp only: subst_raw.simps) + apply (rule alpha_lam_raw.intros) + apply (simp only: alphas) sorry lemma subst_rsp_pre2: assumes a: "alpha_lam_raw a b" shows "alpha_lam_raw (subst_raw c y a) (subst_raw c y b)" + using a + apply (induct c arbitrary: a b y) + apply (simp add: equivp_reflp[OF lam_equivp]) + apply (simp add: alpha_lam_raw.intros) + apply simp + apply (rule alpha_lam_raw.intros) sorry -(* The below is definitely not true... *) lemma [quot_respect]: "(alpha_lam_raw ===> op = ===> alpha_lam_raw ===> alpha_lam_raw) subst_raw subst_raw" proof (intro fun_relI, simp) @@ -603,8 +570,14 @@ qed lemma simp3: - "x \ y \ atom x \ fv_lam_raw s \ subst_raw (Lam_raw x t) y s = Lam_raw x (subst_raw t y s)" - by simp + "x \ y \ atom x \ fv_lam_raw s \ alpha_lam_raw (subst_raw (Lam_raw x t) y s) (Lam_raw x (subst_raw t y s))" + apply simp + apply (rule alpha_lam_raw.intros) + apply (rule_tac x ="(x \ (new (insert (atom y) (fv_lam_raw s \ fv_lam_raw t) - + {atom x})))" in exI) + apply (simp only: alphas) + apply simp + sorry lemmas subst_simps = subst_raw.simps(1-2)[quot_lifted,no_vars] simp3[quot_lifted,simplified lam.supp,simplified fresh_def[symmetric], no_vars]