--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Term5a.thy	Mon Mar 08 14:31:04 2010 +0100
@@ -0,0 +1,38 @@
+theory Term5
+imports "Parser"
+begin
+
+atom_decl name
+
+ML {* restricted_nominal := 2 *}
+
+nominal_datatype trm5 =
+  Vr5 "name"
+| Ap5 "trm5" "trm5"
+| Lt5 l::"lts" t::"trm5"  bind "bv5 l" in t
+and lts =
+  Lnil
+| Lcons "name" "trm5" "lts"
+binder
+  bv5
+where
+  "bv5 Lnil = {}"
+| "bv5 (Lcons n t ltl) = {atom n} \<union> (bv5 ltl)"
+
+lemma lets_ok:
+  "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))"
+apply (simp add: trm5_lts_inject)
+apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
+apply (simp_all add: alpha_gen)
+apply (simp add: trm5_lts_perm fresh_star_def trm5_lts_fv trm5_lts_bn)
+done
+
+lemma lets_nok:
+  "x \<noteq> y \<Longrightarrow> (Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) \<noteq> (Lt5 (Lcons y (Vr5 x) Lnil) (Vr5 y))"
+apply (simp only: trm5_lts_inject not_ex)
+apply (rule allI)
+apply (simp add: alpha_gen)
+apply (simp add: trm5_lts_perm fresh_star_def trm5_lts_fv trm5_lts_bn trm5_lts_inject)
+done
+
+end