# HG changeset patch
# User urbanc
# Date 1209687427 -7200
# Node ID 805eece49928242ecd0e664da4dd9945b28a934c
# Parent  fba4995cb0f9ebcc409a65137e733178457248c6
extended to be a library of general facts about the lambda calculus

diff -r fba4995cb0f9 -r 805eece49928 src/HOL/Nominal/Examples/Lam_Funs.thy
--- a/src/HOL/Nominal/Examples/Lam_Funs.thy	Fri May 02 02:16:10 2008 +0200
+++ b/src/HOL/Nominal/Examples/Lam_Funs.thy	Fri May 02 02:17:07 2008 +0200
@@ -4,7 +4,10 @@
   imports "../Nominal"
 begin
 
-text {* Defines some functions over lambda-terms *}
+text {* 
+  Provides useful definitions for reasoning
+  with lambda-terms. 
+*}
 
 atom_decl name
 
@@ -13,15 +16,15 @@
   | App "lam" "lam"
   | Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100)
 
-text {* Depth of a lambda-term *}
+text {* The depth of a lambda-term. *}
 
 consts 
   depth :: "lam \<Rightarrow> nat"
 
 nominal_primrec
-  "depth (Var x) = (1::nat)"
+  "depth (Var x) = 1"
   "depth (App t1 t2) = (max (depth t1) (depth t2)) + 1"
-  "depth (Lam [a].t) = (depth t) + (1::nat)"
+  "depth (Lam [a].t) = (depth t) + 1"
   apply(finite_guess)+
   apply(rule TrueI)+
   apply(simp add: fresh_nat)
@@ -29,11 +32,10 @@
   done
 
 text {* 
-  Free variables of a lambda-term. The complication of this
-  function is the fact that it returns a name set, which is
-  not automatically a finitely supported type. So we have to
-  prove the invariant that frees always returns a finite set
-  of names. 
+  The free variables of a lambda-term. A complication in this
+  function arises from the fact that it returns a name set, which 
+  is not a finitely supported type. Therefore we have to prove 
+  the invariant that frees always returns a finite set of names. 
 *}
 
 consts 
@@ -48,36 +50,65 @@
 apply(simp add: fresh_def)
 apply(simp add: supp_of_fin_sets[OF pt_name_inst, OF at_name_inst, OF fs_at_inst[OF at_name_inst]])
 apply(simp add: supp_atm)
-apply(force)
+apply(blast)
 apply(fresh_guess)+
 done
 
+text {* 
+  We can avoid the definition of frees by
+  using the build in notion of support.
+*}
+
 lemma frees_equals_support:
   shows "frees t = supp t"
 by (nominal_induct t rule: lam.induct)
    (simp_all add: lam.supp supp_atm abs_supp)
 
-text {* Capture-avoiding substitution *}
+text {* Parallel and single capture-avoiding substitution. *}
+
+fun
+  lookup :: "(name\<times>lam) list \<Rightarrow> name \<Rightarrow> lam"   
+where
+  "lookup [] x        = Var x"
+| "lookup ((y,e)#\<theta>) x = (if x=y then e else lookup \<theta> x)"
+
+lemma lookup_eqvt[eqvt]:
+  fixes pi::"name prm"
+  and   \<theta>::"(name\<times>lam) list"
+  and   X::"name"
+  shows "pi\<bullet>(lookup \<theta> X) = lookup (pi\<bullet>\<theta>) (pi\<bullet>X)"
+by (induct \<theta>) (auto simp add: eqvts)
 
 consts
-  subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_[_::=_]" [100,100,100] 100)
-
+  psubst :: "(name\<times>lam) list \<Rightarrow> lam \<Rightarrow> lam"  ("_<_>" [95,95] 105)
+ 
 nominal_primrec
-  "(Var x)[y::=t'] = (if x=y then t' else (Var x))"
-  "(App t1 t2)[y::=t'] = App (t1[y::=t']) (t2[y::=t'])"
-  "x\<sharp>(y,t') \<Longrightarrow> (Lam [x].t)[y::=t'] = Lam [x].(t[y::=t'])"
+  "\<theta><(Var x)> = (lookup \<theta> x)"
+  "\<theta><(App e\<^isub>1 e\<^isub>2)> = App (\<theta><e\<^isub>1>) (\<theta><e\<^isub>2>)"
+  "x\<sharp>\<theta> \<Longrightarrow> \<theta><(Lam [x].e)> = Lam [x].(\<theta><e>)"
 apply(finite_guess)+
 apply(rule TrueI)+
-apply(simp add: abs_fresh)
+apply(simp add: abs_fresh)+
 apply(fresh_guess)+
 done
 
-lemma subst_eqvt[eqvt]:
-  fixes pi:: "name prm"
-  shows "pi\<bullet>(t1[b::=t2]) = (pi\<bullet>t1)[(pi\<bullet>b)::=(pi\<bullet>t2)]"
-apply(nominal_induct t1 avoiding: b t2 rule: lam.induct)
-apply(auto simp add: perm_bij fresh_prod fresh_atm fresh_bij)
-done
+lemma psubst_eqvt[eqvt]:
+  fixes pi::"name prm" 
+  and   t::"lam"
+  shows "pi\<bullet>(\<theta><t>) = (pi\<bullet>\<theta>)<(pi\<bullet>t)>"
+by (nominal_induct t avoiding: \<theta> rule: lam.induct)
+   (simp_all add: eqvts fresh_bij)
+
+abbreviation 
+  subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_[_::=_]" [100,100,100] 100)
+where 
+  "t[x::=t']  \<equiv> ([(x,t')])<t>" 
+
+lemma subst[simp]:
+  shows "(Var x)[y::=t'] = (if x=y then t' else (Var x))"
+  and   "(App t1 t2)[y::=t'] = App (t1[y::=t']) (t2[y::=t'])"
+  and   "x\<sharp>(y,t') \<Longrightarrow> (Lam [x].t)[y::=t'] = Lam [x].(t[y::=t'])"
+by (simp_all add: fresh_list_cons fresh_list_nil)
 
 lemma subst_supp: 
   shows "supp(t1[a::=t2]) \<subseteq> (((supp(t1)-{a})\<union>supp(t2))::name set)"
@@ -86,44 +117,43 @@
 apply(blast)+
 done
 
-text{* Parallel substitution *}
-
-consts
- psubst :: "(name\<times>lam) list \<Rightarrow> lam \<Rightarrow> lam" ("_<_>" [100,100] 900)
-
-fun
-  lookup :: "(name\<times>lam) list \<Rightarrow> name \<Rightarrow> lam"   
-where
-  "lookup [] x        = Var x"
-| "lookup ((y,T)#\<theta>) x = (if x=y then T else lookup \<theta> x)"
+text {* 
+  Contexts - lambda-terms with a single hole.
+  Note that the lambda case in contexts does not bind a 
+  name, even if we introduce the notation [_]._ for CLam.
+*}
+nominal_datatype clam = 
+    Hole ("\<box>" 1000)  
+  | CAppL "clam" "lam"
+  | CAppR "lam" "clam" 
+  | CLam "name" "clam"  ("CLam [_]._" [100,100] 100) 
 
-lemma lookup_eqvt[eqvt]:
-  fixes pi::"name prm"
-  shows "pi\<bullet>(lookup \<theta> x) = lookup (pi\<bullet>\<theta>) (pi\<bullet>x)"
-by (induct \<theta>) (auto simp add: perm_bij)
+text {* Filling a lambda-term into a context. *}
 
-lemma lookup_fresh:
-  fixes z::"name"
-  assumes "z\<sharp>\<theta>" "z\<sharp>x"
-  shows "z\<sharp> lookup \<theta> x"
-using assms 
-by (induct rule: lookup.induct) (auto simp add: fresh_list_cons)
-
-lemma lookup_fresh':
-  assumes "z\<sharp>\<theta>"
-  shows "lookup \<theta> z = Var z"
-using assms 
-by (induct rule: lookup.induct)
-   (auto simp add: fresh_list_cons fresh_prod fresh_atm)
+consts 
+  filling :: "clam \<Rightarrow> lam \<Rightarrow> lam" ("_\<lbrakk>_\<rbrakk>" [100,100] 100)
 
 nominal_primrec
-  "\<theta><(Var x)> = (lookup \<theta> x)"
-  "\<theta><(App t1 t2)> = App (\<theta><t1>) (\<theta><t2>)"
-  "x\<sharp>\<theta>\<Longrightarrow>\<theta><(Lam [x].t)> = Lam [x].(\<theta><t>)"
-apply(finite_guess)+
-apply(rule TrueI)+
-apply(simp add: abs_fresh)
-apply(fresh_guess)+
-done
+  "\<box>\<lbrakk>t\<rbrakk> = t"
+  "(CAppL E t')\<lbrakk>t\<rbrakk> = App (E\<lbrakk>t\<rbrakk>) t'"
+  "(CAppR t' E)\<lbrakk>t\<rbrakk> = App t' (E\<lbrakk>t\<rbrakk>)"
+  "(CLam [x].E)\<lbrakk>t\<rbrakk> = Lam [x].(E\<lbrakk>t\<rbrakk>)" 
+by (rule TrueI)+
+
+text {* Composition od two contexts *}
+
+consts 
+ clam_compose :: "clam \<Rightarrow> clam \<Rightarrow> clam" ("_ \<circ> _" [100,100] 100)
+
+nominal_primrec
+  "\<box> \<circ> E' = E'"
+  "(CAppL E t') \<circ> E' = CAppL (E \<circ> E') t'"
+  "(CAppR t' E) \<circ> E' = CAppR t' (E \<circ> E')"
+  "(CLam [x].E) \<circ> E' = CLam [x].(E \<circ> E')"
+by (rule TrueI)+
+  
+lemma clam_compose:
+  shows "(E1 \<circ> E2)\<lbrakk>t\<rbrakk> = E1\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>"
+by (induct E1 rule: clam.weak_induct) (auto)
 
 end