1theory Height 2 imports "HOL-Nominal.Nominal" 3begin 4 5text \<open> 6 A small problem suggested by D. Wang. It shows how 7 the height of a lambda-terms behaves under substitution. 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>Definition of the height-function on lambda-terms.\<close> 18 19nominal_primrec 20 height :: "lam \<Rightarrow> int" 21where 22 "height (Var x) = 1" 23| "height (App t1 t2) = (max (height t1) (height t2)) + 1" 24| "height (Lam [a].t) = (height t) + 1" 25 apply(finite_guess add: perm_int_def)+ 26 apply(rule TrueI)+ 27 apply(simp add: fresh_int) 28 apply(fresh_guess add: perm_int_def)+ 29 done 30 31text \<open>Definition of capture-avoiding substitution.\<close> 32 33nominal_primrec 34 subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_[_::=_]" [100,100,100] 100) 35where 36 "(Var x)[y::=t'] = (if x=y then t' else (Var x))" 37| "(App t1 t2)[y::=t'] = App (t1[y::=t']) (t2[y::=t'])" 38| "\<lbrakk>x\<sharp>y; x\<sharp>t'\<rbrakk> \<Longrightarrow> (Lam [x].t)[y::=t'] = Lam [x].(t[y::=t'])" 39apply(finite_guess)+ 40apply(rule TrueI)+ 41apply(simp add: abs_fresh) 42apply(fresh_guess)+ 43done 44 45text\<open>The next lemma is needed in the Var-case of the theorem below.\<close> 46 47lemma height_ge_one: 48 shows "1 \<le> (height e)" 49by (nominal_induct e rule: lam.strong_induct) (simp_all) 50 51text \<open> 52 Unlike the proplem suggested by Wang, however, the 53 theorem is here formulated entirely by using functions. 54\<close> 55 56theorem height_subst: 57 shows "height (e[x::=e']) \<le> ((height e) - 1) + (height e')" 58proof (nominal_induct e avoiding: x e' rule: lam.strong_induct) 59 case (Var y) 60 have "1 \<le> height e'" by (rule height_ge_one) 61 then show "height (Var y[x::=e']) \<le> height (Var y) - 1 + height e'" by simp 62next 63 case (Lam y e1) 64 hence ih: "height (e1[x::=e']) \<le> ((height e1) - 1) + (height e')" by simp 65 moreover 66 have vc: "y\<sharp>x" "y\<sharp>e'" by fact+ (* usual variable convention *) 67 ultimately show "height ((Lam [y].e1)[x::=e']) \<le> height (Lam [y].e1) - 1 + height e'" by simp 68next 69 case (App e1 e2) 70 hence ih1: "height (e1[x::=e']) \<le> ((height e1) - 1) + (height e')" 71 and ih2: "height (e2[x::=e']) \<le> ((height e2) - 1) + (height e')" by simp_all 72 then show "height ((App e1 e2)[x::=e']) \<le> height (App e1 e2) - 1 + height e'" by simp 73qed 74 75end 76