--- a/Nominal/Ex/SingleLetFoo.thy	Sun Aug 29 12:17:25 2010 +0800
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,81 +0,0 @@
-theory SingleLetFoo
-imports "../NewParser"
-begin
-
-
-declare [[STEPS = 5]]
-
-atom_decl name
-
-nominal_datatype trm =
-  Var "name"
-| App "trm" "trm"
-| Lam x::"name" t::"trm"  bind_set x in t
-| Let a::"assg" t::"trm"  bind_set "bn a" in t
-| Foo1 a1::"assg" a2::"assg" t::"trm" bind_set "bn a1" "bn a2" in t
-| Foo2 x::name a::"assg" t::"trm" bind_set x "bn a" in t
-
-and assg =
-  As "name" "trm"
-binder
-  bn::"assg \<Rightarrow> atom set"
-where
-  "bn (As x t) = {atom x}"
-
-thm trm_assg.distinct
-thm trm_assg.eq_iff
-thm trm_assg.supp
-thm trm_assg.perm
-thm trm_assg.fv[simplified trm_assg.supp(1-2),no_vars]
-
-thm permute_trm_raw_permute_assg_raw.simps
-thm fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps[no_vars]
-
-thm alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros[no_vars]
-
-
-lemmas all = alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros
-
-lemma test: "p \<bullet> bn_raw \<equiv> bn_raw" sorry
-
-lemma
-  assumes "distinct [x,y, z, u]"
-  shows "alpha_trm_raw (Foo2_raw z (As_raw x (Var_raw z)) (Var_raw z))
-                       (Foo2_raw u (As_raw y (Var_raw z)) (Var_raw u))"
-using assms
-apply(rule_tac all)
-apply(rule_tac x="(z \<leftrightarrow> u) + (x \<leftrightarrow> y)" in exI)
-apply(simp only: alphas)
-apply(rule conjI)
-apply(simp)
-apply(simp add: supp_at_base fresh_star_def)
-apply(rule conjI)
-apply(simp add: supp_at_base fresh_star_def)
-apply(rule conjI)
-apply(simp)
-apply(rule all)
-apply(simp)
-unfolding flip_def
-apply(perm_simp add: test)
-unfolding flip_def[symmetric]
-apply(simp)
-apply(subst flip_at_base_simps(3))
-apply(auto)[2]
-apply(simp)
-apply(rule all)
-apply(rule all)
-apply(simp)
-done
-
-lemma
-  assumes "distinct [x,y,z,u]"
-  shows "fv_trm_raw (Foo2_raw z (As_raw x (Var_raw z)) (Var_raw z)) = {atom z}"
-using assms
-apply(simp add: supp_at_base)
-done
-
-
-end
-
-
-