1theory Lam_Funs 2 imports "HOL-Nominal.Nominal" 3begin 4 5text \<open> 6 Provides useful definitions for reasoning 7 with lambda-terms. 8\<close> 9 10atom_decl name 11 12nominal_datatype lam = 13 Var "name" 14 | App "lam" "lam" 15 | Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100) 16 17text \<open>The depth of a lambda-term.\<close> 18 19nominal_primrec 20 depth :: "lam \<Rightarrow> nat" 21where 22 "depth (Var x) = 1" 23| "depth (App t1 t2) = (max (depth t1) (depth t2)) + 1" 24| "depth (Lam [a].t) = (depth t) + 1" 25 apply(finite_guess)+ 26 apply(rule TrueI)+ 27 apply(simp add: fresh_nat) 28 apply(fresh_guess)+ 29 done 30 31text \<open> 32 The free variables of a lambda-term. A complication in this 33 function arises from the fact that it returns a name set, which 34 is not a finitely supported type. Therefore we have to prove 35 the invariant that frees always returns a finite set of names. 36\<close> 37 38nominal_primrec (invariant: "\<lambda>s::name set. finite s") 39 frees :: "lam \<Rightarrow> name set" 40where 41 "frees (Var a) = {a}" 42| "frees (App t1 t2) = (frees t1) \<union> (frees t2)" 43| "frees (Lam [a].t) = (frees t) - {a}" 44apply(finite_guess)+ 45apply(simp)+ 46apply(simp add: fresh_def) 47apply(simp add: supp_of_fin_sets[OF pt_name_inst, OF at_name_inst, OF fs_at_inst[OF at_name_inst]]) 48apply(simp add: supp_atm) 49apply(blast) 50apply(fresh_guess)+ 51done 52 53text \<open> 54 We can avoid the definition of frees by 55 using the build in notion of support. 56\<close> 57 58lemma frees_equals_support: 59 shows "frees t = supp t" 60by (nominal_induct t rule: lam.strong_induct) 61 (simp_all add: lam.supp supp_atm abs_supp) 62 63text \<open>Parallel and single capture-avoiding substitution.\<close> 64 65fun 66 lookup :: "(name\<times>lam) list \<Rightarrow> name \<Rightarrow> lam" 67where 68 "lookup [] x = Var x" 69| "lookup ((y,e)#\<theta>) x = (if x=y then e else lookup \<theta> x)" 70 71lemma lookup_eqvt[eqvt]: 72 fixes pi::"name prm" 73 and \<theta>::"(name\<times>lam) list" 74 and X::"name" 75 shows "pi\<bullet>(lookup \<theta> X) = lookup (pi\<bullet>\<theta>) (pi\<bullet>X)" 76by (induct \<theta>) (auto simp add: eqvts) 77 78nominal_primrec 79 psubst :: "(name\<times>lam) list \<Rightarrow> lam \<Rightarrow> lam" ("_<_>" [95,95] 105) 80where 81 "\<theta><(Var x)> = (lookup \<theta> x)" 82| "\<theta><(App e\<^sub>1 e\<^sub>2)> = App (\<theta><e\<^sub>1>) (\<theta><e\<^sub>2>)" 83| "x\<sharp>\<theta> \<Longrightarrow> \<theta><(Lam [x].e)> = Lam [x].(\<theta><e>)" 84apply(finite_guess)+ 85apply(rule TrueI)+ 86apply(simp add: abs_fresh)+ 87apply(fresh_guess)+ 88done 89 90lemma psubst_eqvt[eqvt]: 91 fixes pi::"name prm" 92 and t::"lam" 93 shows "pi\<bullet>(\<theta><t>) = (pi\<bullet>\<theta>)<(pi\<bullet>t)>" 94by (nominal_induct t avoiding: \<theta> rule: lam.strong_induct) 95 (simp_all add: eqvts fresh_bij) 96 97abbreviation 98 subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_[_::=_]" [100,100,100] 100) 99where 100 "t[x::=t'] \<equiv> ([(x,t')])<t>" 101 102lemma subst[simp]: 103 shows "(Var x)[y::=t'] = (if x=y then t' else (Var x))" 104 and "(App t1 t2)[y::=t'] = App (t1[y::=t']) (t2[y::=t'])" 105 and "x\<sharp>(y,t') \<Longrightarrow> (Lam [x].t)[y::=t'] = Lam [x].(t[y::=t'])" 106by (simp_all add: fresh_list_cons fresh_list_nil) 107 108lemma subst_supp: 109 shows "supp(t1[a::=t2]) \<subseteq> (((supp(t1)-{a})\<union>supp(t2))::name set)" 110apply(nominal_induct t1 avoiding: a t2 rule: lam.strong_induct) 111apply(auto simp add: lam.supp supp_atm fresh_prod abs_supp) 112apply(blast)+ 113done 114 115text \<open> 116 Contexts - lambda-terms with a single hole. 117 Note that the lambda case in contexts does not bind a 118 name, even if we introduce the notation [_]._ for CLam. 119\<close> 120nominal_datatype clam = 121 Hole ("\<box>" 1000) 122 | CAppL "clam" "lam" 123 | CAppR "lam" "clam" 124 | CLam "name" "clam" ("CLam [_]._" [100,100] 100) 125 126text \<open>Filling a lambda-term into a context.\<close> 127 128nominal_primrec 129 filling :: "clam \<Rightarrow> lam \<Rightarrow> lam" ("_\<lbrakk>_\<rbrakk>" [100,100] 100) 130where 131 "\<box>\<lbrakk>t\<rbrakk> = t" 132| "(CAppL E t')\<lbrakk>t\<rbrakk> = App (E\<lbrakk>t\<rbrakk>) t'" 133| "(CAppR t' E)\<lbrakk>t\<rbrakk> = App t' (E\<lbrakk>t\<rbrakk>)" 134| "(CLam [x].E)\<lbrakk>t\<rbrakk> = Lam [x].(E\<lbrakk>t\<rbrakk>)" 135by (rule TrueI)+ 136 137text \<open>Composition od two contexts\<close> 138 139nominal_primrec 140 clam_compose :: "clam \<Rightarrow> clam \<Rightarrow> clam" ("_ \<circ> _" [100,100] 100) 141where 142 "\<box> \<circ> E' = E'" 143| "(CAppL E t') \<circ> E' = CAppL (E \<circ> E') t'" 144| "(CAppR t' E) \<circ> E' = CAppR t' (E \<circ> E')" 145| "(CLam [x].E) \<circ> E' = CLam [x].(E \<circ> E')" 146by (rule TrueI)+ 147 148lemma clam_compose: 149 shows "(E1 \<circ> E2)\<lbrakk>t\<rbrakk> = E1\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>" 150by (induct E1 rule: clam.induct) (auto) 151 152end 153