diff -r a6f3e1b08494 -r b6873d123f9b Tutorial/Lambda.thy
--- a/Tutorial/Lambda.thy	Sat May 12 21:05:59 2012 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,91 +0,0 @@
-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" binds 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(simp add: eqvt_def height_graph_def)
-apply (rule, perm_simp, rule)
-apply(rule TrueI)
-apply(rule_tac y="x" in lam.exhaust)
-apply(auto)
-apply(erule_tac c="()" in Abs_lst1_fcb2)
-apply(simp_all add: fresh_def pure_supp eqvt_at_def fresh_star_def)
-done
-
-termination (eqvt)
-  by lexicographic_order
-  
-
-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])"
-  unfolding eqvt_def subst_graph_def
-  apply(rule, perm_simp, rule)
-  apply(rule TrueI)
-  apply(auto)
-  apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust)
-  apply(blast)+
-  apply(simp_all add: fresh_star_def fresh_Pair_elim)
-  apply(erule_tac c="(ya,sa)" in Abs_lst1_fcb2)
-  apply(simp_all add: Abs_fresh_iff)
-  apply(simp add: fresh_star_def fresh_Pair)
-  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
-  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
-done
-
-termination (eqvt)
-  by lexicographic_order
-
-lemma fresh_fact:
-  assumes a: "atom z \<sharp> s"
-  and b: "z = y \<or> atom z \<sharp> t"
-  shows "atom z \<sharp> t[y ::= s]"
-using a b
-by (nominal_induct t avoiding: z y s rule: lam.strong_induct)
-   (auto simp add: lam.fresh fresh_at_base)
-
-
-end
-
-
-