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