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