1theory Contexts 2imports "HOL-Nominal.Nominal" 3begin 4 5text \<open> 6 7 We show here that the Plotkin-style of defining 8 beta-reduction (based on congruence rules) is 9 equivalent to the Felleisen-Hieb-style representation 10 (based on contexts). 11 12 The interesting point in this theory is that contexts 13 do not contain any binders. On the other hand the operation 14 of filling a term into a context produces an alpha-equivalent 15 term. 16 17\<close> 18 19atom_decl name 20 21text \<open> 22 Lambda-Terms - the Lam-term constructor binds a name 23\<close> 24 25nominal_datatype lam = 26 Var "name" 27 | App "lam" "lam" 28 | Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100) 29 30text \<open> 31 Contexts - the lambda case in contexts does not bind 32 a name, even if we introduce the notation [_]._ for CLam. 33\<close> 34 35nominal_datatype ctx = 36 Hole ("\<box>" 1000) 37 | CAppL "ctx" "lam" 38 | CAppR "lam" "ctx" 39 | CLam "name" "ctx" ("CLam [_]._" [100,100] 100) 40 41text \<open>Capture-Avoiding Substitution\<close> 42 43nominal_primrec 44 subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_[_::=_]" [100,100,100] 100) 45where 46 "(Var x)[y::=s] = (if x=y then s else (Var x))" 47| "(App t\<^sub>1 t\<^sub>2)[y::=s] = App (t\<^sub>1[y::=s]) (t\<^sub>2[y::=s])" 48| "x\<sharp>(y,s) \<Longrightarrow> (Lam [x].t)[y::=s] = Lam [x].(t[y::=s])" 49apply(finite_guess)+ 50apply(rule TrueI)+ 51apply(simp add: abs_fresh) 52apply(fresh_guess)+ 53done 54 55text \<open> 56 Filling is the operation that fills a term into a hole. 57 This operation is possibly capturing. 58\<close> 59 60nominal_primrec 61 filling :: "ctx \<Rightarrow> lam \<Rightarrow> lam" ("_\<lbrakk>_\<rbrakk>" [100,100] 100) 62where 63 "\<box>\<lbrakk>t\<rbrakk> = t" 64| "(CAppL E t')\<lbrakk>t\<rbrakk> = App (E\<lbrakk>t\<rbrakk>) t'" 65| "(CAppR t' E)\<lbrakk>t\<rbrakk> = App t' (E\<lbrakk>t\<rbrakk>)" 66| "(CLam [x].E)\<lbrakk>t\<rbrakk> = Lam [x].(E\<lbrakk>t\<rbrakk>)" 67by (rule TrueI)+ 68 69text \<open> 70 While contexts themselves are not alpha-equivalence classes, the 71 filling operation produces an alpha-equivalent lambda-term. 72\<close> 73 74lemma alpha_test: 75 shows "x\<noteq>y \<Longrightarrow> (CLam [x].\<box>) \<noteq> (CLam [y].\<box>)" 76 and "(CLam [x].\<box>)\<lbrakk>Var x\<rbrakk> = (CLam [y].\<box>)\<lbrakk>Var y\<rbrakk>" 77by (auto simp add: alpha ctx.inject lam.inject calc_atm fresh_atm) 78 79text \<open>The composition of two contexts.\<close> 80 81nominal_primrec 82 ctx_compose :: "ctx \<Rightarrow> ctx \<Rightarrow> ctx" ("_ \<circ> _" [100,100] 100) 83where 84 "\<box> \<circ> E' = E'" 85| "(CAppL E t') \<circ> E' = CAppL (E \<circ> E') t'" 86| "(CAppR t' E) \<circ> E' = CAppR t' (E \<circ> E')" 87| "(CLam [x].E) \<circ> E' = CLam [x].(E \<circ> E')" 88by (rule TrueI)+ 89 90lemma ctx_compose: 91 shows "(E1 \<circ> E2)\<lbrakk>t\<rbrakk> = E1\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>" 92by (induct E1 rule: ctx.induct) (auto) 93 94text \<open>Beta-reduction via contexts in the Felleisen-Hieb style.\<close> 95 96inductive 97 ctx_red :: "lam\<Rightarrow>lam\<Rightarrow>bool" ("_ \<longrightarrow>x _" [80,80] 80) 98where 99 xbeta[intro]: "E\<lbrakk>App (Lam [x].t) t'\<rbrakk> \<longrightarrow>x E\<lbrakk>t[x::=t']\<rbrakk>" 100 101text \<open>Beta-reduction via congruence rules in the Plotkin style.\<close> 102 103inductive 104 cong_red :: "lam\<Rightarrow>lam\<Rightarrow>bool" ("_ \<longrightarrow>o _" [80,80] 80) 105where 106 obeta[intro]: "App (Lam [x].t) t' \<longrightarrow>o t[x::=t']" 107| oapp1[intro]: "t \<longrightarrow>o t' \<Longrightarrow> App t t2 \<longrightarrow>o App t' t2" 108| oapp2[intro]: "t \<longrightarrow>o t' \<Longrightarrow> App t2 t \<longrightarrow>o App t2 t'" 109| olam[intro]: "t \<longrightarrow>o t' \<Longrightarrow> Lam [x].t \<longrightarrow>o Lam [x].t'" 110 111text \<open>The proof that shows both relations are equal.\<close> 112 113lemma cong_red_in_ctx: 114 assumes a: "t \<longrightarrow>o t'" 115 shows "E\<lbrakk>t\<rbrakk> \<longrightarrow>o E\<lbrakk>t'\<rbrakk>" 116using a 117by (induct E rule: ctx.induct) (auto) 118 119lemma ctx_red_in_ctx: 120 assumes a: "t \<longrightarrow>x t'" 121 shows "E\<lbrakk>t\<rbrakk> \<longrightarrow>x E\<lbrakk>t'\<rbrakk>" 122using a 123by (induct) (auto simp add: ctx_compose[symmetric]) 124 125theorem ctx_red_implies_cong_red: 126 assumes a: "t \<longrightarrow>x t'" 127 shows "t \<longrightarrow>o t'" 128using a by (induct) (auto intro: cong_red_in_ctx) 129 130theorem cong_red_implies_ctx_red: 131 assumes a: "t \<longrightarrow>o t'" 132 shows "t \<longrightarrow>x t'" 133using a 134proof (induct) 135 case (obeta x t' t) 136 have "\<box>\<lbrakk>App (Lam [x].t) t'\<rbrakk> \<longrightarrow>x \<box>\<lbrakk>t[x::=t']\<rbrakk>" by (rule xbeta) 137 then show "App (Lam [x].t) t' \<longrightarrow>x t[x::=t']" by simp 138qed (metis ctx_red_in_ctx filling.simps)+ (* found by SledgeHammer *) 139 140 141lemma ctx_existence: 142 assumes a: "t \<longrightarrow>o t'" 143 shows "\<exists>C s s'. t = C\<lbrakk>s\<rbrakk> \<and> t' = C\<lbrakk>s'\<rbrakk> \<and> s \<longrightarrow>o s'" 144using a 145by (induct) (metis cong_red.intros filling.simps)+ 146 147end 148