--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Tutorial/Lambda.thy	Wed Jan 19 19:06:52 2011 +0100
@@ -0,0 +1,124 @@
+theory Lambda
+imports "../Nominal/Nominal2" 
+begin
+
+section {* Definitions for Lambda Terms *}
+
+text {* type of variables *}
+
+atom_decl name
+
+
+subsection {* Alpha-Equated Lambda Terms *}
+
+nominal_datatype lam =
+  Var "name"
+| App "lam" "lam"
+| Lam x::"name" l::"lam" bind x in l ("Lam [_]. _" [100, 100] 100)
+
+
+text {* some automatically derived theorems *}
+
+thm lam.distinct
+thm lam.eq_iff
+thm lam.fresh
+thm lam.size
+thm lam.exhaust 
+thm lam.strong_exhaust
+thm lam.induct
+thm lam.strong_induct
+
+
+subsection {* Height Function *}
+
+nominal_primrec
+  height :: "lam \<Rightarrow> int"
+where
+  "height (Var x) = 1"
+| "height (App t1 t2) = max (height t1) (height t2) + 1"
+| "height (Lam [x].t) = height t + 1"
+apply(rule_tac y="x" in lam.exhaust)
+apply(auto simp add: lam.distinct lam.eq_iff)
+apply(simp add: Abs_eq_iff alphas)
+apply(clarify)
+apply(subst (4) supp_perm_eq[where p="p", symmetric])
+apply(simp add: pure_supp fresh_star_def)
+apply(simp add: eqvt_at_def)
+done
+
+termination
+  by (relation "measure size") (simp_all add: lam.size)
+  
+
+subsection {* Capture-avoiding Substitution *}
+
+nominal_primrec
+  subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_ [_ ::= _]" [90,90,90] 90)
+where
+  "(Var x)[y ::= s] = (if x = y then s else (Var x))"
+| "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])"
+| "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])"
+apply(auto simp add: lam.distinct lam.eq_iff)
+apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust)
+apply(blast)+
+apply(simp add: fresh_star_def)
+apply(subgoal_tac "atom xa \<sharp> [[atom x]]lst. t \<and> atom x \<sharp> [[atom xa]]lst. ta")
+apply(subst (asm) Abs_eq_iff2)
+apply(simp add: alphas atom_eqvt)
+apply(clarify)
+apply(rule trans)
+apply(rule_tac p="p" in supp_perm_eq[symmetric])
+apply(rule fresh_star_supp_conv)
+apply(drule fresh_star_perm_set_conv)
+apply(simp add: finite_supp)
+apply(subgoal_tac "{atom (p \<bullet> x), atom x} \<sharp>* ([[atom x]]lst. subst_sumC (t, ya, sa))")
+apply(auto simp add: fresh_star_def)[1]
+apply(simp (no_asm) add: fresh_star_def)
+apply(rule conjI)
+apply(simp (no_asm) add: Abs_fresh_iff)
+apply(clarify)
+apply(drule_tac a="atom (p \<bullet> x)" in fresh_eqvt_at)
+apply(simp add: finite_supp)
+apply(simp (no_asm_use) add: fresh_Pair)
+apply(simp add: Abs_fresh_iff)
+apply(simp)
+apply(simp add: Abs_fresh_iff)
+apply(subgoal_tac "p \<bullet> ya = ya")
+apply(subgoal_tac "p \<bullet> sa = sa")
+apply(simp add: atom_eqvt eqvt_at_def)
+apply(rule perm_supp_eq)
+apply(auto simp add: fresh_star_def fresh_Pair)[1]
+apply(rule perm_supp_eq)
+apply(auto simp add: fresh_star_def fresh_Pair)[1]
+apply(rule conjI)
+apply(simp add: Abs_fresh_iff)
+apply(drule sym)
+apply(simp add: Abs_fresh_iff)
+done
+
+termination
+  by (relation "measure (\<lambda>(t,_,_). size t)")
+     (simp_all add: lam.size)
+
+lemma subst_eqvt[eqvt]:
+  shows "(p \<bullet> t[x ::= s]) = (p \<bullet> t)[(p \<bullet> x) ::= (p \<bullet> s)]"
+by (induct t x s rule: subst.induct) (simp_all)
+
+
+subsection {* Single-Step Beta-Reduction *}
+
+inductive 
+  beta :: "lam \<Rightarrow> lam \<Rightarrow> bool" (" _ \<longrightarrow>b _" [80,80] 80)
+where
+  b1[intro]: "t1 \<longrightarrow>b t2 \<Longrightarrow> App t1 s \<longrightarrow>b App t2 s"
+| b2[intro]: "s1 \<longrightarrow>b s2 \<Longrightarrow> App t s1 \<longrightarrow>b App t s2"
+| b3[intro]: "t1 \<longrightarrow>b t2 \<Longrightarrow> Lam [x]. t1 \<longrightarrow>b Lam [x]. t2"
+| b4[intro]: "App (Lam [x]. t) s \<longrightarrow>b t[x ::= s]"
+
+
+
+
+end
+
+
+