--- a/Nominal/Ex/Exec/Name_Exec.thy	Tue Feb 19 05:38:46 2013 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,56 +0,0 @@
-theory Name_Exec
-imports "../../Nominal2"
-begin
-
-atom_decl name
-
-definition Name :: "nat \<Rightarrow> name" where "Name n = Abs_name (Atom (Sort ''Name_Exec.name'' []) n)"
-
-definition "nat_of_name n = nat_of (Rep_name n)"
-
-code_datatype Name
-
-definition [code]: "N0 = Name 0"
-definition [code]: "N1 = Name 1"
-definition [code]: "N2 = Name 2"
-
-instantiation name :: equal begin
-
-definition equal_name_def: "equal_name a b \<longleftrightarrow> nat_of_name a = nat_of_name b"
-
-instance
-  by default
-    (metis (lifting) Rep_name_inject atom_components_eq_iff atom_name_def equal_name_def nat_of_name_def sort_of_atom_eq)
-
-end
-
-lemma [simp]: "nat_of_name (Name n) = n"
-  unfolding nat_of_name_def Name_def
-  by (simp add: Abs_name_inverse)
-
-lemma equal_name_code [code]: "(equal_class.equal (Name x) (Name y)) \<longleftrightarrow> (x = y)"
-  by (auto simp add: equal_name_def)
-
-lemma atom_name_code[code]:
-  "atom (Name n) = Atom (Sort ''Name_Exec.name'' []) n"
-  by (simp add: Abs_name_inject[symmetric] Name_def)
-     (simp add: atom_name_def Rep_name_inverse)
-
-lemma permute_name_code[code]: "p \<bullet> n = Name (nat_of (p \<bullet> (atom n)))"
-  apply (simp add: atom_eqvt)
-  apply (simp add: atom_name_def Name_def)
-  by (metis Rep_name_inverse atom_name_def atom_name_sort nat_of.simps sort_of.simps atom.exhaust)
-
-(*
-Test:
-definition "t \<longleftrightarrow> 0 = (N0 \<leftrightarrow> N1)"
-
-export_code t in SML
-
-value "(N0 \<leftrightarrow> N1) + (N1 \<leftrightarrow> N0) = 0"
-*)
-
-end
-
-
-