# HG changeset patch # User urbanc # Date 1196271593 -3600 # Node ID 7e0ad4838ce97fe13838f4db06e9bedddf22fbdb # Parent f781564f3605e42b475a07ad42b49c71ac34b91f an example file for how to treat Felleisen-Hieb-style contexts in nominal diff -r f781564f3605 -r 7e0ad4838ce9 src/HOL/Nominal/Examples/Contexts.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Nominal/Examples/Contexts.thy Wed Nov 28 18:39:53 2007 +0100 @@ -0,0 +1,191 @@ +(* $Id: *) + +theory Contexts +imports "../Nominal" +begin + +text {* + + We show here that the Plotkin-style of defining + reductions relation based on congruence rules is + equivalent to the Felleisen-Hieb-style representation + based on contexts. + + The interesting point is that contexts do not bind + anything. On the other hand the operation of replacing + a term into a context produces an alpha-equivalent term. + +*} + +atom_decl name + +text {* terms *} + +nominal_datatype lam = + Var "name" + | App "lam" "lam" + | Lam "\name\lam" ("Lam [_]._" [100,100] 100) + +text {* contexts - the context-lambda does not bind anything *} + +nominal_datatype ctx = + Hole + | CAppL "ctx" "lam" + | CAppR "lam" "ctx" + | CLam "name" "ctx" ("CLam [_]._" [100,100] 100) + +text {* Capture-avoiding substitution and three lemmas *} + +consts subst :: "lam \ name \ lam \ lam" ("_[_::=_]" [100,100,100] 100) + +nominal_primrec + "(Var x)[y::=s] = (if x=y then s else (Var x))" + "(App t\<^isub>1 t\<^isub>2)[y::=s] = App (t\<^isub>1[y::=s]) (t\<^isub>2[y::=s])" + "x\(y,s) \ (Lam [x].t)[y::=s] = Lam [x].(t[y::=s])" +apply(finite_guess)+ +apply(rule TrueI)+ +apply(simp add: abs_fresh) +apply(fresh_guess)+ +done + +lemma subst_eqvt[eqvt]: + fixes pi::"name prm" + shows "pi\t1[x::=t2] = (pi\t1)[(pi\x)::=(pi\t2)]" +by (nominal_induct t1 avoiding: x t2 rule: lam.induct) + (auto simp add: perm_bij fresh_atm fresh_bij) + +lemma subst_fresh: + fixes x y::"name" + and t t'::"lam" + shows "y\([x].t,t') \ y\t[x::=t']" +by (nominal_induct t avoiding: x y t' rule: lam.inducts) + (auto simp add: abs_fresh fresh_prod fresh_atm) + +lemma subst_swap: + fixes x y::"name" + and t t'::"lam" + shows "y\t \ ([(y,x)]\t)[y::=t'] = t[x::=t']" +by (nominal_induct t avoiding: x y t' rule: lam.inducts) + (auto simp add: lam.inject calc_atm fresh_atm abs_fresh) + +text {* + The operation that fills one term into a hole. While + contexts are not alpha-equivalence classes, the filling + operation produces an alpha-equivalent lambda-term. +*} + +consts + replace :: "ctx \ lam \ lam" ("_<_>" [100,100] 100) + +nominal_primrec + "Hole = t" + "(CAppL E t') = App (E) t'" + "(CAppR t' E) = App t' (E)" + "(CLam [x].E) = Lam [x].(E)" +by (rule TrueI)+ + +lemma alpha_test: + shows "(CLam [x].Hole) = (CLam [y].Hole)" +by (auto simp add: alpha lam.inject calc_atm fresh_atm) + +lemma replace_eqvt[eqvt]: + fixes pi:: "name prm" + shows "pi\(E) = (pi\E)<(pi\e)>" +by (nominal_induct E rule: ctx.inducts) (auto) + +lemma replace_fresh: + fixes x::"name" + and E::"ctx" + and t::"lam" + shows "x\(E,t) \ x\E" +by (induct E rule: ctx.weak_induct) + (auto simp add: fresh_prod abs_fresh) + +text {* composition of two contexts *} + +consts + ctx_replace :: "ctx \ ctx \ ctx" ("_ \ _" [100,100] 100) + +nominal_primrec + "Hole \ E' = E'" + "(CAppL E t') \ E' = CAppL (E \ E') t'" + "(CAppR t' E) \ E' = CAppR t' (E \ E')" + "(CLam [x].E) \ E' = CLam [x].(E \ E')" +by (rule TrueI)+ + +lemma ctx_compose: + shows "E1> = (E1 \ E2)" +by (induct E1 rule: ctx.weak_induct) (auto) + +lemma ctx_compose_fresh: + fixes x::"name" + and E1 E2::"ctx" + shows "x\(E1,E2) \ x\(E1\E2)" +by (induct E1 rule: ctx.weak_induct) + (auto simp add: fresh_prod) + +text {* beta-reduction via contexts *} + +inductive + ctx_red :: "lam\lam\bool" ("_ \x _" [80,80] 80) +where + xbeta[intro]: "x\(E,t') \ E \x E" + +equivariance ctx_red + +nominal_inductive ctx_red + by (simp_all add: replace_fresh subst_fresh abs_fresh) + +text {* beta-reduction via congruence rules *} + +inductive + cong_red :: "lam\lam\bool" ("_ \o _" [80,80] 80) +where + obeta[intro]: "x\t' \ App (Lam [x].t) t' \o t[x::=t']" +| oapp1[intro]: "t \o t' \ App t t2 \o App t' t2" +| oapp2[intro]: "t \o t' \ App t2 t \o App t2 t'" +| olam[intro]: "t \o t' \ Lam [x].t \o Lam [x].t'" + +equivariance cong_red + +nominal_inductive cong_red + by (simp_all add: subst_fresh abs_fresh) + +text {* the proof that shows both relations are equal *} + +lemma cong_red_ctx: + assumes a: "t \o t'" + shows "E \o E" +using a +by (induct E rule: ctx.weak_induct) (auto) + +lemma ctx_red_ctx: + assumes a: "t \x t'" + shows "E \x E" +using a +by (nominal_induct t t' avoiding: E rule: ctx_red.strong_induct) + (auto simp add: ctx_compose ctx_compose_fresh) + +lemma ctx_red_hole: + assumes a: "Hole \x Hole" + shows "t \x t'" +using a by simp + +theorem ctx_red_cong_red: + assumes a: "t \x t'" + shows "t \o t'" +using a +by (induct) (auto intro!: cong_red_ctx) + +theorem cong_red_ctx_red: + assumes a: "t \o t'" + shows "t \x t'" +using a +apply(induct) +apply(rule ctx_red_hole) +apply(rule xbeta) +apply(simp) +apply(metis ctx_red_ctx replace.simps)+ (* found by SledgeHammer *) +done + +end