--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/Exec/Name_Exec.thy	Tue May 22 14:55:58 2012 +0200
@@ -0,0 +1,56 @@
+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
+
+
+